1.22/1.35	NO
1.22/1.35	
1.22/1.35	Problem:
1.22/1.35	 a(b(x)) -> b(c(x))
1.22/1.35	 a(c(x)) -> c(a(x))
1.22/1.35	 b(b(x)) -> a(c(x))
1.22/1.35	 c(b(x)) -> b(c(x))
1.22/1.35	 c(b(x)) -> c(c(x))
1.22/1.35	 c(c(x)) -> c(b(x))
1.22/1.35	 0(1(2(x))) -> 2(0(1(x)))
1.22/1.35	 2(2(2(2(2(2(2(1(1(1(1(2(x)))))))))))) -> 2(1(2(2(0(1(2(1(1(0(1(0(x))))))))))))
1.22/1.35	
1.22/1.35	Proof:
1.22/1.35	 sorted: (order-sorted)
1.22/1.35	 0:0(1(2(x))) -> 2(0(1(x)))
1.22/1.35	   2(2(2(2(2(2(2(1(1(1(1(2(x)))))))))))) -> 2(1(2(2(0(1(2(1(1(0(1(0(x))))))))))))
1.22/1.35	 1:a(b(x)) -> b(c(x))
1.22/1.35	   a(c(x)) -> c(a(x))
1.22/1.35	   b(b(x)) -> a(c(x))
1.22/1.35	   c(b(x)) -> b(c(x))
1.22/1.35	   c(b(x)) -> c(c(x))
1.22/1.35	   c(c(x)) -> c(b(x))
1.22/1.35	 -----
1.22/1.35	 sorts
1.22/1.35	   []
1.22/1.35	 sort attachment (non-strict)
1.22/1.35	   a : 1 -> 1
1.22/1.35	   b : 1 -> 1
1.22/1.35	   c : 1 -> 1
1.22/1.35	   0 : 0 -> 0
1.22/1.35	   1 : 0 -> 0
1.22/1.35	   2 : 0 -> 0
1.22/1.35	 -----
1.22/1.35	 0:0(1(2(x))) -> 2(0(1(x)))
1.22/1.35	   2(2(2(2(2(2(2(1(1(1(1(2(x)))))))))))) -> 2(1(2(2(0(1(2(1(1(0(1(0(x))))))))))))
1.22/1.35	   Nonconfluence Processor:
1.22/1.35	    terms: 2(0(1(1(2(2(2(0(1(1(1(0(1(0(x270)))))))))))))) *<- 0(1(2(2
1.22/1.35	                                                                    (
1.22/1.35	                                                                    2
1.22/1.35	                                                                    (
1.22/1.35	                                                                    2(2(2(2(1(1(1(1(2(x270)))))))))))))) ->* 
1.22/1.35	    2(2(2(2(2(2(2(0(1(1(1(1(1(2(x270))))))))))))))
1.22/1.35	    Qed
1.22/1.35	 
1.22/1.35	 
1.22/1.35	 1:a(b(x)) -> b(c(x))
1.22/1.35	   a(c(x)) -> c(a(x))
1.22/1.35	   b(b(x)) -> a(c(x))
1.22/1.35	   c(b(x)) -> b(c(x))
1.22/1.35	   c(b(x)) -> c(c(x))
1.22/1.35	   c(c(x)) -> c(b(x))
1.22/1.35	   Open
1.22/1.35	 
1.22/1.35	EOF