2.67/1.25	YES
2.67/1.25	
2.67/1.25	Proof:
2.67/1.25	This system is confluent.
2.67/1.25	By \cite{ALS94}, Theorem 4.1.
2.67/1.25	This system is of type 3 or smaller.
2.67/1.25	This system is strongly deterministic.
2.67/1.25	This system is quasi-decreasing.
2.67/1.25	By \cite{O02}, p. 214, Proposition 7.2.50.
2.67/1.25	This system is of type 3 or smaller.
2.67/1.25	This system is deterministic.
2.67/1.25	System R transformed to optimized U(R).
2.67/1.25	This system is terminating.
2.67/1.25	Call external tool:
2.67/1.25	./ttt2.sh
2.67/1.25	Input:
2.67/1.25	  add(x, 0) -> x
2.67/1.25	  add(x, s(y)) -> ?1(add(x, y), x, y)
2.67/1.25	  ?1(z, x, y) -> s(z)
2.67/1.25	
2.67/1.25	 DP Processor:
2.67/1.25	  DPs:
2.67/1.25	   add#(x,s(y)) -> add#(x,y)
2.67/1.25	   add#(x,s(y)) -> ?1#(add(x,y),x,y)
2.67/1.25	  TRS:
2.67/1.25	   add(x,0()) -> x
2.67/1.25	   add(x,s(y)) -> ?1(add(x,y),x,y)
2.67/1.25	   ?1(z,x,y) -> s(z)
2.67/1.25	  TDG Processor:
2.67/1.25	   DPs:
2.67/1.25	    add#(x,s(y)) -> add#(x,y)
2.67/1.25	    add#(x,s(y)) -> ?1#(add(x,y),x,y)
2.67/1.25	   TRS:
2.67/1.25	    add(x,0()) -> x
2.67/1.25	    add(x,s(y)) -> ?1(add(x,y),x,y)
2.67/1.25	    ?1(z,x,y) -> s(z)
2.67/1.26	   graph:
2.67/1.26	    add#(x,s(y)) -> add#(x,y) -> add#(x,s(y)) -> ?1#(add(x,y),x,y)
2.67/1.26	    add#(x,s(y)) -> add#(x,y) -> add#(x,s(y)) -> add#(x,y)
2.67/1.26	   SCC Processor:
2.67/1.26	    #sccs: 1
2.67/1.26	    #rules: 1
2.67/1.26	    #arcs: 2/4
2.67/1.26	    DPs:
2.67/1.26	     add#(x,s(y)) -> add#(x,y)
2.67/1.26	    TRS:
2.67/1.26	     add(x,0()) -> x
2.67/1.26	     add(x,s(y)) -> ?1(add(x,y),x,y)
2.67/1.26	     ?1(z,x,y) -> s(z)
2.67/1.26	    Subterm Criterion Processor:
2.67/1.26	     simple projection:
2.67/1.26	      pi(add#) = 1
2.67/1.26	     problem:
2.67/1.26	      DPs:
2.67/1.26	       
2.67/1.26	      TRS:
2.67/1.26	       add(x,0()) -> x
2.67/1.26	       add(x,s(y)) -> ?1(add(x,y),x,y)
2.67/1.26	       ?1(z,x,y) -> s(z)
2.67/1.26	     Qed
2.67/1.26	All 0 critical pairs are joinable.
2.67/1.26	
2.67/1.28	EOF