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