8.32/3.06	YES
8.32/3.06	
8.32/3.06	Proof:
8.32/3.06	This system is confluent.
8.32/3.06	By \cite{ALS94}, Theorem 4.1.
8.32/3.06	This system is of type 3 or smaller.
8.32/3.06	This system is strongly deterministic.
8.32/3.06	This system is quasi-decreasing.
8.32/3.06	By \cite{O02}, p. 214, Proposition 7.2.50.
8.32/3.06	This system is of type 3 or smaller.
8.32/3.06	This system is deterministic.
8.32/3.06	System R transformed to U(R).
8.32/3.06	This system is terminating.
8.32/3.06	Call external tool:
8.32/3.06	./ttt2.sh
8.32/3.06	Input:
8.32/3.06	(VAR x y)
8.32/3.06	(RULES
8.32/3.06	  ?1(c(a(b)), x, y) -> a(a(x))
8.32/3.06	  f(c(x), c(c(y))) -> ?1(c(f(x, y)), x, y)
8.32/3.06	  ?2(c(a(a(b))), x, y) -> a(y)
8.32/3.06	  f(c(c(c(x))), y) -> ?2(c(f(c(x), c(c(y)))), x, y)
8.32/3.06	  h(b) -> b
8.32/3.06	  ?3(b, x) -> a(b)
8.32/3.06	  h(a(a(x))) -> ?3(h(x), x)
8.32/3.06	)
8.32/3.06	
8.32/3.06	 DP Processor:
8.32/3.06	  DPs:
8.32/3.06	   f#(c(x),c(c(y))) -> f#(x,y)
8.32/3.06	   f#(c(x),c(c(y))) -> ?1#(c(f(x,y)),x,y)
8.32/3.06	   f#(c(c(c(x))),y) -> f#(c(x),c(c(y)))
8.32/3.06	   f#(c(c(c(x))),y) -> ?2#(c(f(c(x),c(c(y)))),x,y)
8.32/3.06	   h#(a(a(x))) -> h#(x)
8.32/3.06	   h#(a(a(x))) -> ?3#(h(x),x)
8.32/3.06	  TRS:
8.32/3.06	   ?1(c(a(b())),x,y) -> a(a(x))
8.32/3.06	   f(c(x),c(c(y))) -> ?1(c(f(x,y)),x,y)
8.32/3.06	   ?2(c(a(a(b()))),x,y) -> a(y)
8.32/3.06	   f(c(c(c(x))),y) -> ?2(c(f(c(x),c(c(y)))),x,y)
8.32/3.06	   h(b()) -> b()
8.32/3.06	   ?3(b(),x) -> a(b())
8.32/3.06	   h(a(a(x))) -> ?3(h(x),x)
8.32/3.06	  TDG Processor:
8.32/3.06	   DPs:
8.32/3.06	    f#(c(x),c(c(y))) -> f#(x,y)
8.32/3.06	    f#(c(x),c(c(y))) -> ?1#(c(f(x,y)),x,y)
8.32/3.06	    f#(c(c(c(x))),y) -> f#(c(x),c(c(y)))
8.32/3.06	    f#(c(c(c(x))),y) -> ?2#(c(f(c(x),c(c(y)))),x,y)
8.32/3.06	    h#(a(a(x))) -> h#(x)
8.32/3.06	    h#(a(a(x))) -> ?3#(h(x),x)
8.32/3.06	   TRS:
8.32/3.06	    ?1(c(a(b())),x,y) -> a(a(x))
8.32/3.06	    f(c(x),c(c(y))) -> ?1(c(f(x,y)),x,y)
8.32/3.06	    ?2(c(a(a(b()))),x,y) -> a(y)
8.32/3.06	    f(c(c(c(x))),y) -> ?2(c(f(c(x),c(c(y)))),x,y)
8.32/3.06	    h(b()) -> b()
8.32/3.06	    ?3(b(),x) -> a(b())
8.32/3.08	    h(a(a(x))) -> ?3(h(x),x)
8.32/3.08	   graph:
8.32/3.08	    h#(a(a(x))) -> h#(x) -> h#(a(a(x))) -> ?3#(h(x),x)
8.32/3.08	    h#(a(a(x))) -> h#(x) -> h#(a(a(x))) -> h#(x)
8.32/3.08	    f#(c(c(c(x))),y) -> f#(c(x),c(c(y))) ->
8.32/3.08	    f#(c(c(c(x))),y) -> ?2#(c(f(c(x),c(c(y)))),x,y)
8.32/3.08	    f#(c(c(c(x))),y) -> f#(c(x),c(c(y))) ->
8.32/3.08	    f#(c(c(c(x))),y) -> f#(c(x),c(c(y)))
8.32/3.08	    f#(c(c(c(x))),y) -> f#(c(x),c(c(y))) ->
8.32/3.08	    f#(c(x),c(c(y))) -> ?1#(c(f(x,y)),x,y)
8.32/3.08	    f#(c(c(c(x))),y) -> f#(c(x),c(c(y))) -> f#(c(x),c(c(y))) -> f#(x,y)
8.32/3.08	    f#(c(x),c(c(y))) -> f#(x,y) ->
8.32/3.08	    f#(c(c(c(x))),y) -> ?2#(c(f(c(x),c(c(y)))),x,y)
8.32/3.08	    f#(c(x),c(c(y))) -> f#(x,y) -> f#(c(c(c(x))),y) -> f#(c(x),c(c(y)))
8.32/3.08	    f#(c(x),c(c(y))) -> f#(x,y) ->
8.32/3.08	    f#(c(x),c(c(y))) -> ?1#(c(f(x,y)),x,y)
8.32/3.08	    f#(c(x),c(c(y))) -> f#(x,y) -> f#(c(x),c(c(y))) -> f#(x,y)
8.32/3.08	   SCC Processor:
8.32/3.08	    #sccs: 2
8.32/3.08	    #rules: 3
8.32/3.08	    #arcs: 10/36
8.32/3.08	    DPs:
8.32/3.08	     f#(c(c(c(x))),y) -> f#(c(x),c(c(y)))
8.32/3.08	     f#(c(x),c(c(y))) -> f#(x,y)
8.32/3.08	    TRS:
8.32/3.08	     ?1(c(a(b())),x,y) -> a(a(x))
8.32/3.08	     f(c(x),c(c(y))) -> ?1(c(f(x,y)),x,y)
8.32/3.08	     ?2(c(a(a(b()))),x,y) -> a(y)
8.32/3.08	     f(c(c(c(x))),y) -> ?2(c(f(c(x),c(c(y)))),x,y)
8.32/3.08	     h(b()) -> b()
8.32/3.08	     ?3(b(),x) -> a(b())
8.32/3.08	     h(a(a(x))) -> ?3(h(x),x)
8.32/3.08	    Subterm Criterion Processor:
8.32/3.08	     simple projection:
8.32/3.09	      pi(f#) = 0
8.32/3.09	     problem:
8.32/3.09	      DPs:
8.32/3.09	       
8.32/3.09	      TRS:
8.32/3.09	       ?1(c(a(b())),x,y) -> a(a(x))
8.32/3.09	       f(c(x),c(c(y))) -> ?1(c(f(x,y)),x,y)
8.32/3.09	       ?2(c(a(a(b()))),x,y) -> a(y)
8.32/3.09	       f(c(c(c(x))),y) -> ?2(c(f(c(x),c(c(y)))),x,y)
8.32/3.09	       h(b()) -> b()
8.32/3.09	       ?3(b(),x) -> a(b())
8.32/3.09	       h(a(a(x))) -> ?3(h(x),x)
8.32/3.09	     Qed
8.32/3.09	    
8.32/3.09	    DPs:
8.32/3.09	     h#(a(a(x))) -> h#(x)
8.32/3.09	    TRS:
8.32/3.09	     ?1(c(a(b())),x,y) -> a(a(x))
8.32/3.09	     f(c(x),c(c(y))) -> ?1(c(f(x,y)),x,y)
8.32/3.09	     ?2(c(a(a(b()))),x,y) -> a(y)
8.32/3.09	     f(c(c(c(x))),y) -> ?2(c(f(c(x),c(c(y)))),x,y)
8.32/3.09	     h(b()) -> b()
8.32/3.09	     ?3(b(),x) -> a(b())
8.32/3.09	     h(a(a(x))) -> ?3(h(x),x)
8.32/3.09	    Subterm Criterion Processor:
8.32/3.09	     simple projection:
8.32/3.09	      pi(h#) = 0
8.32/3.09	     problem:
8.32/3.09	      DPs:
8.32/3.09	       
8.32/3.09	      TRS:
8.32/3.09	       ?1(c(a(b())),x,y) -> a(a(x))
8.32/3.09	       f(c(x),c(c(y))) -> ?1(c(f(x,y)),x,y)
8.32/3.09	       ?2(c(a(a(b()))),x,y) -> a(y)
8.32/3.09	       f(c(c(c(x))),y) -> ?2(c(f(c(x),c(c(y)))),x,y)
8.32/3.09	       h(b()) -> b()
8.32/3.09	       ?3(b(),x) -> a(b())
8.32/3.09	       h(a(a(x))) -> ?3(h(x),x)
8.32/3.09	     Qed
8.32/3.09	All 2 critical pairs are joinable.
8.32/3.09	Overlap: (rule1: f(c(c(c(z))), x') -> a(x') <= c(f(c(z), c(c(x')))) = c(a(a(b))), rule2: f(c(y'), c(c(z'))) -> a(a(y')) <= c(f(y', z')) = c(a(b)), pos: ε, mgu: {(y',c(c(z))), (x',c(c(z')))})
8.32/3.09	CP: a(a(c(c(z)))) = a(c(c(z'))) <= c(f(c(z), c(c(c(c(z')))))) = c(a(a(b))), c(f(c(c(z)), z')) = c(a(b))
8.32/3.09	This critical pair is infeasible.
8.32/3.09	This critical pair is conditional.
8.32/3.09	This critical pair has some non-trivial conditions.
8.32/3.09	Call external tool:
8.32/3.09	./waldmeister
8.32/3.09	Input:
8.32/3.09	  f(c(x), c(c(y))) -> a(a(x)) <= c(f(x, y)) = c(a(b))
8.32/3.09	  f(c(c(c(x))), y) -> a(y) <= c(f(c(x), c(c(y)))) = c(a(a(b)))
8.32/3.09	  h(b) -> b
8.32/3.09	  h(a(a(x))) -> a(b) <= h(x) = b
8.32/3.09	
8.32/3.09	By Waldmeister.
8.32/3.09	Overlap: (rule1: f(c(z), c(c(x'))) -> a(a(z)) <= c(f(z, x')) = c(a(b)), rule2: f(c(c(c(y'))), z') -> a(z') <= c(f(c(y'), c(c(z')))) = c(a(a(b))), pos: ε, mgu: {(z,c(c(y'))), (z',c(c(x')))})
8.32/3.09	CP: a(c(c(x'))) = a(a(c(c(y')))) <= c(f(c(c(y')), x')) = c(a(b)), c(f(c(y'), c(c(c(c(x')))))) = c(a(a(b)))
8.32/3.09	This critical pair is infeasible.
8.32/3.09	This critical pair is conditional.
8.32/3.09	This critical pair has some non-trivial conditions.
8.32/3.09	Call external tool:
8.32/3.09	./waldmeister
8.32/3.09	Input:
8.32/3.09	  f(c(x), c(c(y))) -> a(a(x)) <= c(f(x, y)) = c(a(b))
8.32/3.09	  f(c(c(c(x))), y) -> a(y) <= c(f(c(x), c(c(y)))) = c(a(a(b)))
8.32/3.09	  h(b) -> b
8.32/3.09	  h(a(a(x))) -> a(b) <= h(x) = b
8.32/3.09	
8.32/3.09	By Waldmeister.
8.32/3.09	
8.65/3.15	EOF