1.16/1.32	NO
1.16/1.32	
1.16/1.32	Problem:
1.16/1.32	 a(a(x)) -> b(x)
1.16/1.32	 b(a(x)) -> a(b(x))
1.16/1.32	 b(b(c(x))) -> c(a(x))
1.16/1.32	 b(b(x)) -> a(a(a(x)))
1.16/1.32	 c(a(x)) -> b(a(c(x)))
1.16/1.32	
1.16/1.32	Proof:
1.16/1.32	 Nonconfluence Processor:
1.16/1.32	  terms: c(b(x1013)) *<- c(a(a(x1013))) ->* a(b(c(x1013)))
1.16/1.32	  Qed
1.69/1.32	EOF