9.37/3.26	MAYBE
9.37/3.26	
9.37/3.26	Proof:
9.37/3.26	ConCon could not decide confluence of the system.
9.37/3.26	\cite{ALS94}, Theorem 4.1 does not apply.
9.37/3.26	This system is of type 3 or smaller.
9.37/3.26	This system is strongly deterministic.
9.37/3.26	This system is quasi-decreasing.
9.37/3.26	By \cite{O02}, p. 214, Proposition 7.2.50.
9.37/3.26	This system is of type 3 or smaller.
9.37/3.26	This system is deterministic.
9.37/3.26	System R transformed to U(R).
9.37/3.26	This system is terminating.
9.37/3.26	Call external tool:
9.37/3.26	./ttt2.sh
9.37/3.26	Input:
9.37/3.26	(VAR x)
9.37/3.26	(RULES
9.37/3.26	  even(0) -> true
9.37/3.26	  ?1(true, x) -> true
9.37/3.26	  even(s(x)) -> ?1(odd(x), x)
9.37/3.26	  ?2(true, x) -> false
9.37/3.26	  even(s(x)) -> ?2(even(x), x)
9.37/3.26	  odd(0) -> false
9.37/3.26	  ?3(true, x) -> true
9.37/3.26	  odd(s(x)) -> ?3(even(x), x)
9.37/3.26	  ?4(true, x) -> false
9.37/3.26	  odd(s(x)) -> ?4(odd(x), x)
9.37/3.26	)
9.37/3.26	
9.37/3.26	 Matrix Interpretation Processor: dim=1
9.37/3.26	  
9.37/3.26	  interpretation:
9.37/3.26	   [?4](x0, x1) = 2x0 + 2x1 + 4,
9.37/3.26	   
9.37/3.26	   [?3](x0, x1) = 2x0 + 4x1 + 6,
9.37/3.26	   
9.37/3.26	   [false] = 0,
9.37/3.26	   
9.37/3.26	   [?2](x0, x1) = 2x0 + x1,
9.37/3.26	   
9.37/3.26	   [odd](x0) = 4x0 + 4,
9.37/3.26	   
9.37/3.26	   [s](x0) = 6x0 + 2,
9.37/3.26	   
9.37/3.26	   [?1](x0, x1) = x0 + 2x1 + 2,
9.37/3.26	   
9.37/3.26	   [true] = 6,
9.37/3.26	   
9.37/3.26	   [even](x0) = 2x0 + 3,
9.37/3.26	   
9.37/3.27	   [0] = 2
9.37/3.27	  orientation:
9.37/3.27	   even(0()) = 7 >= 6 = true()
9.37/3.27	   
9.37/3.27	   ?1(true(),x) = 2x + 8 >= 6 = true()
9.37/3.27	   
9.37/3.27	   even(s(x)) = 12x + 7 >= 6x + 6 = ?1(odd(x),x)
9.37/3.27	   
9.37/3.27	   ?2(true(),x) = x + 12 >= 0 = false()
9.37/3.27	   
9.37/3.27	   even(s(x)) = 12x + 7 >= 5x + 6 = ?2(even(x),x)
9.37/3.27	   
9.37/3.27	   odd(0()) = 12 >= 0 = false()
9.37/3.27	   
9.37/3.27	   ?3(true(),x) = 4x + 18 >= 6 = true()
9.37/3.27	   
9.37/3.27	   odd(s(x)) = 24x + 12 >= 8x + 12 = ?3(even(x),x)
9.37/3.27	   
9.37/3.27	   ?4(true(),x) = 2x + 16 >= 0 = false()
9.37/3.27	   
9.37/3.27	   odd(s(x)) = 24x + 12 >= 10x + 12 = ?4(odd(x),x)
9.37/3.27	  problem:
9.37/3.27	   odd(s(x)) -> ?3(even(x),x)
9.37/3.27	   odd(s(x)) -> ?4(odd(x),x)
9.37/3.27	  Matrix Interpretation Processor: dim=3
9.37/3.27	   
9.37/3.27	   interpretation:
9.37/3.27	                   [1 1 0]     [1 0 0]  
9.37/3.27	    [?4](x0, x1) = [0 0 0]x0 + [0 0 0]x1
9.37/3.27	                   [0 0 0]     [0 0 0]  ,
9.37/3.27	    
9.37/3.27	                   [1 0 1]     [1 0 1]  
9.37/3.27	    [?3](x0, x1) = [0 0 0]x0 + [0 0 0]x1
9.37/3.27	                   [0 0 0]     [0 0 0]  ,
9.37/3.27	    
9.37/3.27	                [1 0 1]  
9.37/3.27	    [odd](x0) = [0 1 0]x0
9.37/3.27	                [0 0 0]  ,
9.37/3.27	    
9.37/3.27	              [1 1 0]     [1]
9.37/3.27	    [s](x0) = [0 0 0]x0 + [0]
9.37/3.27	              [1 0 1]     [0],
9.37/3.27	    
9.37/3.27	                 [1 0 0]     [1]
9.37/3.27	    [even](x0) = [0 0 0]x0 + [0]
9.37/3.27	                 [0 1 0]     [0]
9.37/3.27	   orientation:
9.37/3.27	                [2 1 1]    [1]    [2 1 1]    [1]                
9.37/3.27	    odd(s(x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = ?3(even(x),x)
9.37/3.27	                [0 0 0]    [0]    [0 0 0]    [0]                
9.37/3.27	    
9.37/3.27	                [2 1 1]    [1]    [2 1 1]                
9.37/3.27	    odd(s(x)) = [0 0 0]x + [0] >= [0 0 0]x = ?4(odd(x),x)
9.37/3.27	                [0 0 0]    [0]    [0 0 0]                
9.37/3.27	   problem:
9.37/3.27	    odd(s(x)) -> ?3(even(x),x)
9.37/3.27	   Matrix Interpretation Processor: dim=3
9.37/3.27	    
9.37/3.27	    interpretation:
9.37/3.27	                    [1 1 0]     [1 0 0]  
9.37/3.27	     [?3](x0, x1) = [0 0 0]x0 + [0 0 0]x1
9.37/3.27	                    [0 0 0]     [0 0 0]  ,
9.37/3.27	     
9.37/3.27	                 [1 1 1]     [1]
9.37/3.27	     [odd](x0) = [0 0 0]x0 + [0]
9.37/3.27	                 [0 0 0]     [0],
9.37/3.27	     
9.37/3.27	               [1 0 0]  
9.37/3.27	     [s](x0) = [1 0 0]x0
9.37/3.27	               [1 0 0]  ,
9.37/3.27	     
9.37/3.27	                  [1 0 0]  
9.37/3.27	     [even](x0) = [1 0 0]x0
9.37/3.27	                  [0 0 0]  
9.37/3.27	    orientation:
9.37/3.27	                 [3 0 0]    [1]    [3 0 0]                 
9.37/3.27	     odd(s(x)) = [0 0 0]x + [0] >= [0 0 0]x = ?3(even(x),x)
9.37/3.27	                 [0 0 0]    [0]    [0 0 0]                 
9.37/3.27	    problem:
9.37/3.27	     
9.37/3.27	    Qed
9.37/3.27	This critical pair is conditional.
9.37/3.27	This critical pair has some non-trivial conditions.
9.37/3.27	ConCon could not decide whether all 4 critical pairs are joinable or not.
9.37/3.27	Overlap: (rule1: even(s(y)) -> false <= even(y) = true, rule2: even(s(z)) -> true <= odd(z) = true, pos: ε, mgu: {(y,z)})
9.37/3.27	CP: true = false <= even(z) = true, odd(z) = true
9.37/3.27	ConCon could not decide infeasibility of this critical pair.
9.37/3.27	
9.37/3.31	EOF