1.19/1.31	NO
1.19/1.31	
1.19/1.31	Problem:
1.19/1.31	 a() -> f(a(),b())
1.19/1.31	 f(a(),b()) -> f(b(),a())
1.19/1.31	
1.19/1.31	Proof:
1.19/1.31	 Nonconfluence Processor:
1.19/1.31	  terms: f(f(b(),f(a(),b())),b()) *<- f(a(),b()) ->* f(b(),f(b(),a()))
1.19/1.31	  Qed
1.19/1.31	EOF