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