0.75/0.96 NO 0.75/0.96 0.75/0.96 Problem: 0.75/0.96 a(a(x)) -> b(b(b(x))) 0.75/0.96 b(b(b(b(x)))) -> a(a(a(x))) 0.75/0.96 0.75/0.96 Proof: 0.75/0.96 Nonconfluence Processor: 0.75/0.96 terms: a(b(b(b(x13)))) *<- a(a(a(x13))) ->* b(b(b(a(x13)))) 0.75/0.96 Qed 0.75/0.97 EOF