9.43/3.60	NO
9.43/3.60	
9.43/3.60	Problem:
9.43/3.60	 f(x,x) -> g(x)
9.43/3.60	 f(x,g(x)) -> b()
9.43/3.60	 h(c(),y) -> f(h(y,c()),h(y,y))
9.43/3.60	
9.43/3.60	Proof:
9.43/3.60	 Church Rosser Transformation Processor:
9.43/3.60	  strict:
9.43/3.60	   
9.43/3.60	  weak:
9.43/3.60	   
9.43/3.60	  critical peaks: 0
9.43/3.60	  Redundant Rules Transformation:
9.43/3.60	   f(x,x) -> g(x)
9.43/3.60	   f(x,g(x)) -> b()
9.43/3.60	   h(c(),y) -> f(h(y,c()),h(y,y))
9.43/3.60	   h(c(),c()) -> g(h(c(),c()))
9.43/3.60	   f(x,f(x,x)) -> b()
9.43/3.60	   Nonconfluence Processor:
9.43/3.60	    terms: b() *<- h(c(),c()) ->* g(g(g(h(c(),c()))))
9.43/3.60	    Qed
9.43/3.60	EOF