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