  In this paper we use the decreasing diagrams technique to show that a
left-linear term rewrite system R is confluent if all its critical pairs are
joinable and the critical pair steps are relatively terminating with respect to
R. We further show how to encode the rule-labeling heuristic for decreasing
diagrams as a satisfiability problem. Experimental data for both methods are
presented.
