7.09/2.68	MAYBE
7.09/2.68	
7.09/2.68	Proof:
7.09/2.68	ConCon could not decide confluence of the system.
7.09/2.68	\cite{ALS94}, Theorem 4.1 does not apply.
7.09/2.68	This system is of type 3 or smaller.
7.09/2.68	This system is strongly deterministic.
7.09/2.68	This system is quasi-decreasing.
7.09/2.68	By \cite{A14}, Theorem 11.5.9.
7.09/2.68	This system is of type 3 or smaller.
7.09/2.68	This system is deterministic.
7.09/2.68	System R transformed to V(R) + Emb.
7.09/2.68	This system is terminating.
7.09/2.68	Call external tool:
7.09/2.68	./ttt2.sh
7.09/2.68	Input:
7.09/2.68	(VAR x)
7.09/2.68	(RULES
7.09/2.68	  s(p(x)) -> x
7.09/2.68	  p(s(x)) -> x
7.09/2.68	  pos(0) -> false
7.09/2.68	  pos(s(0)) -> true
7.09/2.68	  pos(s(x)) -> true
7.09/2.68	  pos(s(x)) -> pos(x)
7.09/2.68	  pos(p(x)) -> false
7.09/2.68	  pos(p(x)) -> pos(x)
7.09/2.68	  pos(x) -> x
7.09/2.68	  p(x) -> x
7.09/2.68	  s(x) -> x
7.09/2.68	)
7.09/2.68	
7.09/2.68	 Matrix Interpretation Processor: dim=3
7.09/2.68	  
7.09/2.68	  interpretation:
7.09/2.68	            [0]
7.09/2.68	   [true] = [0]
7.09/2.68	            [0],
7.09/2.68	   
7.09/2.68	             [0]
7.09/2.68	   [false] = [0]
7.09/2.68	             [0],
7.09/2.68	   
7.09/2.68	                    [1]
7.09/2.68	   [pos](x0) = x0 + [0]
7.09/2.68	                    [0],
7.09/2.68	   
7.09/2.68	         [0]
7.09/2.68	   [0] = [0]
7.09/2.68	         [0],
7.09/2.68	   
7.09/2.68	               
7.09/2.68	   [s](x0) = x0
7.09/2.68	               ,
7.09/2.69	   
7.09/2.69	               
7.09/2.69	   [p](x0) = x0
7.09/2.69	               
7.09/2.69	  orientation:
7.09/2.69	                       
7.09/2.69	   s(p(x)) = x >= x = x
7.09/2.69	                       
7.09/2.69	   
7.09/2.69	                       
7.09/2.69	   p(s(x)) = x >= x = x
7.09/2.69	                       
7.09/2.69	   
7.09/2.69	              [1]    [0]          
7.09/2.69	   pos(0()) = [0] >= [0] = false()
7.09/2.69	              [0]    [0]          
7.09/2.69	   
7.09/2.69	                 [1]    [0]         
7.09/2.69	   pos(s(0())) = [0] >= [0] = true()
7.09/2.69	                 [0]    [0]         
7.09/2.69	   
7.09/2.69	                   [1]    [0]         
7.09/2.69	   pos(s(x)) = x + [0] >= [0] = true()
7.09/2.69	                   [0]    [0]         
7.09/2.69	   
7.09/2.69	                   [1]        [1]         
7.09/2.69	   pos(s(x)) = x + [0] >= x + [0] = pos(x)
7.09/2.69	                   [0]        [0]         
7.09/2.69	   
7.09/2.69	                   [1]    [0]          
7.09/2.69	   pos(p(x)) = x + [0] >= [0] = false()
7.09/2.69	                   [0]    [0]          
7.09/2.69	   
7.09/2.69	                   [1]        [1]         
7.09/2.69	   pos(p(x)) = x + [0] >= x + [0] = pos(x)
7.09/2.69	                   [0]        [0]         
7.09/2.69	   
7.09/2.69	                [1]         
7.09/2.69	   pos(x) = x + [0] >= x = x
7.09/2.69	                [0]         
7.09/2.69	   
7.09/2.69	                    
7.09/2.69	   p(x) = x >= x = x
7.09/2.69	                    
7.09/2.69	   
7.09/2.69	                    
7.09/2.69	   s(x) = x >= x = x
7.09/2.69	                    
7.09/2.69	  problem:
7.09/2.69	   s(p(x)) -> x
7.09/2.69	   p(s(x)) -> x
7.09/2.69	   pos(s(x)) -> pos(x)
7.09/2.69	   pos(p(x)) -> pos(x)
7.09/2.69	   p(x) -> x
7.09/2.69	   s(x) -> x
7.09/2.69	  Matrix Interpretation Processor: dim=3
7.09/2.69	   
7.09/2.69	   interpretation:
7.09/2.69	                [1 0 1]  
7.09/2.69	    [pos](x0) = [0 0 0]x0
7.09/2.69	                [0 0 0]  ,
7.09/2.69	    
7.09/2.69	                   [0]
7.09/2.69	    [s](x0) = x0 + [0]
7.09/2.69	                   [1],
7.09/2.69	    
7.09/2.69	                   [1]
7.09/2.69	    [p](x0) = x0 + [0]
7.09/2.69	                   [0]
7.09/2.69	   orientation:
7.09/2.69	                  [1]         
7.09/2.69	    s(p(x)) = x + [0] >= x = x
7.09/2.69	                  [1]         
7.09/2.69	    
7.09/2.69	                  [1]         
7.09/2.69	    p(s(x)) = x + [0] >= x = x
7.09/2.69	                  [1]         
7.09/2.69	    
7.09/2.69	                [1 0 1]    [1]    [1 0 1]          
7.09/2.69	    pos(s(x)) = [0 0 0]x + [0] >= [0 0 0]x = pos(x)
7.09/2.69	                [0 0 0]    [0]    [0 0 0]          
7.09/2.69	    
7.09/2.69	                [1 0 1]    [1]    [1 0 1]          
7.09/2.69	    pos(p(x)) = [0 0 0]x + [0] >= [0 0 0]x = pos(x)
7.09/2.69	                [0 0 0]    [0]    [0 0 0]          
7.09/2.69	    
7.09/2.69	               [1]         
7.09/2.69	    p(x) = x + [0] >= x = x
7.09/2.69	               [0]         
7.09/2.69	    
7.09/2.69	               [0]         
7.09/2.69	    s(x) = x + [0] >= x = x
7.09/2.69	               [1]         
7.09/2.69	   problem:
7.09/2.69	    s(x) -> x
7.09/2.69	   Matrix Interpretation Processor: dim=3
7.09/2.69	    
7.09/2.69	    interpretation:
7.09/2.69	                    [1]
7.09/2.69	     [s](x0) = x0 + [0]
7.09/2.69	                    [0]
7.09/2.69	    orientation:
7.09/2.69	                [1]         
7.09/2.69	     s(x) = x + [0] >= x = x
7.09/2.69	                [0]         
7.09/2.69	    problem:
7.09/2.69	     
7.09/2.69	    Qed
7.09/2.69	Overlap: (rule1: s(p(y)) -> y, rule2: p(s(z)) -> z, pos: 1, mgu: {(y,s(z))})
7.09/2.69	CP: s(z) = s(z)
7.09/2.69	This critical pair is context-joinable.
7.09/2.69	Overlap: (rule1: p(s(y)) -> y, rule2: s(p(z)) -> z, pos: 1, mgu: {(y,p(z))})
7.09/2.69	CP: p(z) = p(z)
7.09/2.69	This critical pair is context-joinable.
7.09/2.69	Overlap: (rule1: pos(s(0)) -> true, rule2: pos(s(y)) -> true <= pos(y) = true, pos: ε, mgu: {(y,0)})
7.09/2.69	CP: true = true <= pos(0) = true
7.09/2.69	This critical pair is context-joinable.
7.09/2.69	This critical pair is conditional.
7.09/2.69	This critical pair has some non-trivial conditions.
7.09/2.69	ConCon could not decide whether all 6 critical pairs are joinable or not.
7.09/2.69	Overlap: (rule1: pos(s(y)) -> true <= pos(y) = true, rule2: s(p(z)) -> z, pos: 1, mgu: {(y,p(z))})
7.09/2.69	CP: pos(z) = true <= pos(p(z)) = true
7.09/2.69	ConCon could not decide infeasibility of this critical pair.
7.09/2.69	
7.32/3.14	EOF