5.21/2.23	MAYBE
5.21/2.23	
5.21/2.23	Proof:
5.21/2.23	ConCon could not decide confluence of the system.
5.21/2.23	\cite{ALS94}, Theorem 4.1 does not apply.
5.21/2.23	This system is of type 3 or smaller.
5.21/2.23	This system is strongly deterministic.
5.21/2.23	This system is quasi-decreasing.
5.21/2.23	By \cite{O02}, p. 214, Proposition 7.2.50.
5.21/2.23	This system is of type 3 or smaller.
5.21/2.23	This system is deterministic.
5.21/2.23	System R transformed to optimized U(R).
5.21/2.23	This system is terminating.
5.21/2.23	Call external tool:
5.21/2.23	./ttt2.sh
5.21/2.23	Input:
5.21/2.23	(VAR x)
5.21/2.23	(RULES
5.21/2.23	  f(g(x)) -> ?1(x, x)
5.21/2.23	  ?1(s(0), x) -> x
5.21/2.23	  g(s(x)) -> g(x)
5.21/2.23	)
5.21/2.23	
5.21/2.23	 Matrix Interpretation Processor: dim=1
5.21/2.23	  
5.21/2.23	  interpretation:
5.21/2.23	   [s](x0) = x0,
5.21/2.23	   
5.21/2.23	   [0] = 0,
5.21/2.23	   
5.21/2.23	   [?1](x0, x1) = x0 + x1 + 5,
5.21/2.23	   
5.21/2.23	   [f](x0) = x0 + 1,
5.21/2.23	   
5.21/2.23	   [g](x0) = 2x0 + 4
5.21/2.23	  orientation:
5.21/2.23	   f(g(x)) = 2x + 5 >= 2x + 5 = ?1(x,x)
5.65/2.23	   
5.65/2.23	   ?1(s(0()),x) = x + 5 >= x = x
5.65/2.23	   
5.65/2.23	   g(s(x)) = 2x + 4 >= 2x + 4 = g(x)
5.65/2.23	  problem:
5.65/2.23	   f(g(x)) -> ?1(x,x)
5.65/2.23	   g(s(x)) -> g(x)
5.65/2.23	  Matrix Interpretation Processor: dim=3
5.65/2.23	   
5.65/2.23	   interpretation:
5.65/2.23	              [1 0 0]     [0]
5.65/2.23	    [s](x0) = [0 0 0]x0 + [0]
5.65/2.23	              [0 0 1]     [1],
5.65/2.23	    
5.65/2.23	                   [1 0 0]     [1 0 1]  
5.65/2.23	    [?1](x0, x1) = [0 0 0]x0 + [0 0 0]x1
5.65/2.23	                   [0 0 0]     [0 0 0]  ,
5.65/2.23	    
5.65/2.23	              [1 1 0]     [1]
5.65/2.23	    [f](x0) = [0 0 0]x0 + [0]
5.65/2.23	              [0 0 0]     [0],
5.65/2.23	    
5.65/2.23	              [1 0 1]     [1]
5.65/2.23	    [g](x0) = [1 0 0]x0 + [0]
5.65/2.23	              [0 0 0]     [0]
5.65/2.23	   orientation:
5.65/2.23	              [2 0 1]    [2]    [2 0 1]           
5.65/2.23	    f(g(x)) = [0 0 0]x + [0] >= [0 0 0]x = ?1(x,x)
5.65/2.23	              [0 0 0]    [0]    [0 0 0]           
5.65/2.23	    
5.65/2.23	              [1 0 1]    [2]    [1 0 1]    [1]       
5.65/2.23	    g(s(x)) = [1 0 0]x + [0] >= [1 0 0]x + [0] = g(x)
5.65/2.23	              [0 0 0]    [0]    [0 0 0]    [0]       
5.65/2.23	   problem:
5.65/2.23	    
5.65/2.23	   Qed
5.65/2.23	This critical pair is conditional.
5.65/2.23	This critical pair has some non-trivial conditions.
5.65/2.23	ConCon could not decide whether all 1 critical pairs are joinable or not.
5.65/2.23	Overlap: (rule1: f(g(y)) -> y <= y = s(0), rule2: g(s(z)) -> g(z), pos: 1, mgu: {(y,s(z))})
5.65/2.23	CP: f(g(z)) = s(z) <= s(z) = s(0)
5.65/2.23	ConCon could not decide infeasibility of this critical pair.
5.65/2.23	don't know if infeasible
5.65/2.23	
5.65/2.26	EOF