3.78/1.55	YES
3.78/1.55	
3.78/1.55	Proof:
3.78/1.55	This system is confluent.
3.78/1.56	By \cite{ALS94}, Theorem 4.1.
3.78/1.56	This system is of type 3 or smaller.
3.78/1.56	This system is strongly deterministic.
3.78/1.56	This system is quasi-decreasing.
3.78/1.56	By \cite{O02}, p. 214, Proposition 7.2.50.
3.78/1.56	This system is of type 3 or smaller.
3.78/1.56	This system is deterministic.
3.78/1.56	System R transformed to U(R).
3.78/1.56	This system is terminating.
3.78/1.56	Call external tool:
3.78/1.56	./ttt2.sh
3.78/1.56	Input:
3.78/1.56	  ?1(nil, x, y) -> x
3.78/1.56	  last(cons(x, y)) -> ?1(y, x, y)
3.78/1.56	  ?3(z, x, y, u, v) -> z
3.78/1.56	  ?2(cons(u, v), x, y) -> ?3(last(y), x, y, u, v)
3.78/1.56	  last(cons(x, y)) -> ?2(y, x, y)
3.78/1.56	
3.78/1.56	 Matrix Interpretation Processor: dim=1
3.78/1.56	  
3.78/1.56	  interpretation:
3.78/1.56	   [?2](x0, x1, x2) = 2x0 + 4x1 + 6x2 + 6,
3.78/1.56	   
3.78/1.56	   [?3](x0, x1, x2, x3, x4) = x0 + 2x1 + 2x2 + x3 + 2x4 + 1,
3.78/1.56	   
3.78/1.56	   [last](x0) = 4x0,
3.78/1.56	   
3.78/1.56	   [cons](x0, x1) = x0 + 2x1 + 4,
3.78/1.56	   
3.78/1.56	   [?1](x0, x1, x2) = 6x0 + 4x1 + 2x2 + 1,
3.78/1.56	   
3.78/1.56	   [nil] = 2
3.78/1.56	  orientation:
3.78/1.56	   ?1(nil(),x,y) = 4x + 2y + 13 >= x = x
3.78/1.56	   
3.78/1.56	   last(cons(x,y)) = 4x + 8y + 16 >= 4x + 8y + 1 = ?1(y,x,y)
3.78/1.56	   
3.78/1.56	   ?3(z,x,y,u,v) = u + 2v + 2x + 2y + z + 1 >= z = z
3.78/1.56	   
3.78/1.56	   ?2(cons(u,v),x,y) = 2u + 4v + 4x + 6y + 14 >= u + 2v + 2x + 6y + 1 = ?3(last(y),x,y,u,v)
3.78/1.56	   
3.78/1.56	   last(cons(x,y)) = 4x + 8y + 16 >= 4x + 8y + 6 = ?2(y,x,y)
3.78/1.56	  problem:
3.78/1.56	   
3.78/1.56	  Qed
3.78/1.56	All 2 critical pairs are joinable.
3.78/1.56	Overlap: (rule1: last(cons($1, y')) -> $2 <= y' = cons(z', x'), last(y') = $2, rule2: last(cons(z, $3)) -> z <= $3 = nil, pos: ε, mgu: {(z,$1), ($3,y')})
3.78/1.56	CP: $1 = $2 <= y' = cons(z', x'), last(y') = $2, y' = nil
3.78/1.56	This critical pair is unfeasible.
3.78/1.56	Overlap: (rule1: last(cons(z, x')) -> z <= x' = nil, rule2: last(cons($1, y')) -> $2 <= y' = cons($3, z'), last(y') = $2, pos: ε, mgu: {($1,z), (y',x')})
3.78/1.56	CP: $2 = z <= x' = nil, x' = cons($3, z'), last(x') = $2
3.78/1.56	This critical pair is unfeasible.
3.78/1.56	
4.22/2.00	EOF