4.67/2.10	YES
4.67/2.10	
4.67/2.10	Proof:
4.67/2.10	This system is confluent.
4.67/2.10	By \cite{ALS94}, Theorem 4.1.
4.67/2.10	This system is of type 3 or smaller.
4.67/2.10	This system is strongly deterministic.
4.67/2.10	This system is quasi-decreasing.
4.67/2.10	By \cite{A14}, Theorem 11.5.9.
4.67/2.10	This system is of type 3 or smaller.
4.67/2.10	This system is deterministic.
4.67/2.10	System R transformed to V(R) + Emb.
4.67/2.10	This system is terminating.
4.67/2.10	Call external tool:
4.67/2.10	./ttt2.sh
4.67/2.10	Input:
4.67/2.10	(VAR x y)
4.67/2.10	(RULES
4.67/2.10	  last(cons(x, y)) -> x
4.67/2.10	  last(cons(x, y)) -> y
4.67/2.10	  last(cons(x, y)) -> last(y)
4.67/2.10	  cons(x, y) -> x
4.67/2.10	  cons(x, y) -> y
4.67/2.10	  last(x) -> x
4.67/2.10	)
4.67/2.10	
4.67/2.10	 Matrix Interpretation Processor: dim=3
4.67/2.10	  
4.67/2.10	  interpretation:
4.67/2.10	                  
4.67/2.10	   [last](x0) = x0
4.67/2.10	                  ,
4.67/2.10	   
4.67/2.10	                    [1 0 0]          [1]
4.67/2.10	   [cons](x0, x1) = [1 1 0]x0 + x1 + [0]
4.67/2.10	                    [0 0 1]          [0]
4.67/2.10	  orientation:
4.67/2.10	                     [1 0 0]        [1]         
4.67/2.10	   last(cons(x,y)) = [1 1 0]x + y + [0] >= x = x
4.67/2.10	                     [0 0 1]        [0]         
4.67/2.10	   
4.67/2.10	                     [1 0 0]        [1]         
4.67/2.10	   last(cons(x,y)) = [1 1 0]x + y + [0] >= y = y
4.67/2.10	                     [0 0 1]        [0]         
4.67/2.10	   
4.67/2.10	                     [1 0 0]        [1]               
4.67/2.10	   last(cons(x,y)) = [1 1 0]x + y + [0] >= y = last(y)
4.67/2.10	                     [0 0 1]        [0]               
4.67/2.10	   
4.67/2.10	               [1 0 0]        [1]         
4.67/2.10	   cons(x,y) = [1 1 0]x + y + [0] >= x = x
4.67/2.10	               [0 0 1]        [0]         
4.67/2.10	   
4.67/2.10	               [1 0 0]        [1]         
4.67/2.10	   cons(x,y) = [1 1 0]x + y + [0] >= y = y
4.67/2.10	               [0 0 1]        [0]         
4.67/2.10	   
4.67/2.10	                       
4.67/2.10	   last(x) = x >= x = x
4.67/2.10	                       
4.67/2.10	  problem:
4.67/2.10	   last(x) -> x
4.67/2.10	  Matrix Interpretation Processor: dim=3
4.67/2.10	   
4.67/2.10	   interpretation:
4.67/2.10	                      [1]
4.67/2.10	    [last](x0) = x0 + [0]
4.67/2.10	                      [0]
4.67/2.10	   orientation:
4.67/2.10	                  [1]         
4.67/2.10	    last(x) = x + [0] >= x = x
4.67/2.10	                  [0]         
4.67/2.10	   problem:
4.67/2.10	    
4.67/2.10	   Qed
4.67/2.10	All 2 critical pairs are joinable.
4.67/2.10	Overlap: (rule1: last(cons($1, y')) -> $2 <= y' = cons(z', x'), last(y') = $2, rule2: last(cons(z, $3)) -> z <= $3 = nil, pos: ε, mgu: {($1,z), (y',$3)})
4.67/2.10	CP: z = $2 <= $3 = cons(z', x'), last($3) = $2, $3 = nil
4.67/2.10	This critical pair is unfeasible.
4.67/2.10	Overlap: (rule1: last(cons(z, x')) -> z <= x' = nil, rule2: last(cons($1, y')) -> $2 <= y' = cons($3, z'), last(y') = $2, pos: ε, mgu: {(z,$1), (x',y')})
4.67/2.10	CP: $2 = $1 <= y' = nil, y' = cons($3, z'), last(y') = $2
4.67/2.10	This critical pair is unfeasible.
4.67/2.10	
4.88/2.13	EOF