6.35/3.00	YES
6.35/3.00	
6.35/3.00	Proof:
6.35/3.00	This system is confluent.
6.35/3.00	By \cite{ALS94}, Theorem 4.1.
6.35/3.00	This system is of type 3 or smaller.
6.35/3.00	This system is strongly deterministic.
6.35/3.00	This system is quasi-decreasing.
6.35/3.00	By \cite{O02}, p. 214, Proposition 7.2.50.
6.35/3.00	This system is of type 3 or smaller.
6.35/3.00	This system is deterministic.
6.35/3.00	System R transformed to optimized U(R).
6.35/3.00	This system is terminating.
6.35/3.00	Call external tool:
6.35/3.00	./ttt2.sh
6.35/3.00	Input:
6.35/3.00	(VAR x y)
6.35/3.00	(RULES
6.35/3.00	  f(x, y) -> ?1(c(g(x)), x, y)
6.35/3.00	  ?1(c(a), x, y) -> g(x)
6.35/3.00	  f(x, y) -> ?2(c(h(x)), x, y)
6.35/3.00	  ?2(c(a), x, y) -> h(x)
6.35/3.00	  g(s(x)) -> x
6.35/3.00	  h(s(x)) -> x
6.35/3.00	)
6.35/3.00	
6.35/3.00	 Matrix Interpretation Processor: dim=1
6.35/3.00	  
6.35/3.00	  interpretation:
6.35/3.00	   [s](x0) = 2x0 + 4,
6.35/3.00	   
6.35/3.00	   [?2](x0, x1, x2) = 2x0 + 4x1 + x2,
6.35/3.00	   
6.35/3.00	   [h](x0) = x0,
6.35/3.00	   
6.35/3.00	   [a] = 1,
6.35/3.00	   
6.35/3.00	   [?1](x0, x1, x2) = x0 + x1 + 2x2,
6.35/3.00	   
6.35/3.00	   [c](x0) = x0,
6.35/3.00	   
6.35/3.00	   [g](x0) = x0 + 1,
6.52/3.03	   
6.52/3.03	   [f](x0, x1) = 6x0 + 3x1 + 1
6.52/3.03	  orientation:
6.52/3.03	   f(x,y) = 6x + 3y + 1 >= 2x + 2y + 1 = ?1(c(g(x)),x,y)
6.52/3.03	   
6.52/3.03	   ?1(c(a()),x,y) = x + 2y + 1 >= x + 1 = g(x)
6.52/3.03	   
6.52/3.03	   f(x,y) = 6x + 3y + 1 >= 6x + y = ?2(c(h(x)),x,y)
6.52/3.03	   
6.52/3.03	   ?2(c(a()),x,y) = 4x + y + 2 >= x = h(x)
6.52/3.03	   
6.52/3.03	   g(s(x)) = 2x + 5 >= x = x
6.52/3.03	   
6.52/3.03	   h(s(x)) = 2x + 4 >= x = x
6.52/3.03	  problem:
6.52/3.03	   f(x,y) -> ?1(c(g(x)),x,y)
6.52/3.03	   ?1(c(a()),x,y) -> g(x)
6.52/3.03	  Matrix Interpretation Processor: dim=1
6.52/3.03	   
6.52/3.03	   interpretation:
6.52/3.03	    [a] = 0,
6.52/3.03	    
6.52/3.03	    [?1](x0, x1, x2) = x0 + x1 + x2,
6.52/3.03	    
6.52/3.03	    [c](x0) = x0 + 6,
6.52/3.03	    
6.52/3.03	    [g](x0) = x0,
6.52/3.03	    
6.52/3.03	    [f](x0, x1) = 3x0 + x1 + 6
6.52/3.03	   orientation:
6.52/3.03	    f(x,y) = 3x + y + 6 >= 2x + y + 6 = ?1(c(g(x)),x,y)
6.52/3.03	    
6.52/3.03	    ?1(c(a()),x,y) = x + y + 6 >= x = g(x)
6.52/3.03	   problem:
6.52/3.03	    f(x,y) -> ?1(c(g(x)),x,y)
6.52/3.03	   Matrix Interpretation Processor: dim=1
6.52/3.03	    
6.52/3.03	    interpretation:
6.52/3.03	     [?1](x0, x1, x2) = 3x0 + x1 + 4x2,
6.52/3.03	     
6.52/3.03	     [c](x0) = x0,
6.52/3.03	     
6.52/3.03	     [g](x0) = 2x0,
6.52/3.03	     
6.52/3.03	     [f](x0, x1) = 7x0 + 4x1 + 1
6.52/3.03	    orientation:
6.52/3.03	     f(x,y) = 7x + 4y + 1 >= 7x + 4y = ?1(c(g(x)),x,y)
6.52/3.03	    problem:
6.52/3.03	     
6.52/3.03	    Qed
6.52/3.03	All 2 critical pairs are joinable.
6.52/3.03	Overlap: (rule1: f(z, x') -> h(z) <= c(h(z)) = c(a), rule2: f(y', z') -> g(y') <= c(g(y')) = c(a), pos: ε, mgu: {(z,y'), (x',z')})
6.52/3.03	CP: g(y') = h(y') <= c(h(y')) = c(a), c(g(y')) = c(a)
6.52/3.03	This critical pair is infeasible.
6.52/3.03	This critical pair is conditional.
6.52/3.03	This critical pair has some non-trivial conditions.
6.52/3.03	Call external tool:
6.52/3.03	./waldmeister
6.52/3.03	Input:
6.52/3.03	  f(x, y) -> g(x) <= c(g(x)) = c(a)
6.52/3.03	  f(x, y) -> h(x) <= c(h(x)) = c(a)
6.52/3.03	  g(s(x)) -> x
6.52/3.03	  h(s(x)) -> x
6.52/3.03	
6.52/3.03	By Waldmeister.
6.52/3.03	Overlap: (rule1: f(z, x') -> g(z) <= c(g(z)) = c(a), rule2: f(y', z') -> h(y') <= c(h(y')) = c(a), pos: ε, mgu: {(z,y'), (x',z')})
6.52/3.03	CP: h(y') = g(y') <= c(g(y')) = c(a), c(h(y')) = c(a)
6.52/3.03	This critical pair is infeasible.
6.52/3.03	This critical pair is conditional.
6.52/3.03	This critical pair has some non-trivial conditions.
6.52/3.03	Call external tool:
6.52/3.03	./waldmeister
6.52/3.03	Input:
6.52/3.03	  f(x, y) -> g(x) <= c(g(x)) = c(a)
6.52/3.03	  f(x, y) -> h(x) <= c(h(x)) = c(a)
6.52/3.03	  g(s(x)) -> x
6.52/3.03	  h(s(x)) -> x
6.52/3.03	
6.52/3.03	By Waldmeister.
6.52/3.03	
6.56/3.07	EOF