1.21/1.27 NO 1.21/1.27 1.21/1.27 Problem: 1.21/1.27 a(a(x)) -> b(b(b(x))) 1.21/1.27 b(b(b(b(x)))) -> a(a(a(x))) 1.21/1.27 1.21/1.27 Proof: 1.21/1.27 Nonconfluence Processor: 1.21/1.27 terms: a(b(b(b(x13)))) *<- a(a(a(x13))) ->* b(b(b(a(x13)))) 1.21/1.27 Qed 1.21/1.28 EOF