6.64/2.52	YES
6.64/2.52	
6.64/2.52	Proof:
6.64/2.52	This system is confluent.
6.64/2.52	By \cite{ALS94}, Theorem 4.1.
6.64/2.52	This system is of type 3 or smaller.
6.64/2.52	This system is strongly deterministic.
6.64/2.52	This system is quasi-decreasing.
6.64/2.52	By \cite{O02}, p. 214, Proposition 7.2.50.
6.64/2.52	This system is of type 3 or smaller.
6.64/2.52	This system is deterministic.
6.64/2.52	System R transformed to U(R).
6.64/2.52	This system is terminating.
6.64/2.52	Call external tool:
6.64/2.52	./ttt2.sh
6.64/2.52	Input:
6.64/2.52	(VAR x y)
6.64/2.52	(RULES
6.64/2.52	  a -> c
6.64/2.52	  a -> d
6.64/2.52	  b -> c
6.64/2.52	  b -> d
6.64/2.52	  c -> e
6.64/2.52	  d -> e
6.64/2.52	  k -> e
6.64/2.52	  l -> e
6.64/2.52	  s(c) -> t(k)
6.64/2.52	  s(c) -> t(l)
6.64/2.52	  s(e) -> t(e)
6.64/2.52	  g(x, x) -> h(x, x)
6.64/2.52	  ?1(t(y), x) -> pair(x, y)
6.64/2.52	  f(x) -> ?1(s(x), x)
6.64/2.52	)
6.64/2.52	
6.64/2.53	 Matrix Interpretation Processor: dim=1
6.64/2.53	  
6.64/2.53	  interpretation:
6.64/2.53	   [f](x0) = 7x0 + 4,
6.64/2.53	   
6.64/2.53	   [pair](x0, x1) = x0 + x1,
6.64/2.53	   
6.64/2.53	   [?1](x0, x1) = 2x0 + x1,
6.64/2.53	   
6.64/2.53	   [h](x0, x1) = 4x0 + 4x1,
6.64/2.53	   
6.64/2.53	   [g](x0, x1) = 6x0 + 2x1 + 4,
6.64/2.53	   
6.64/2.53	   [t](x0) = 2x0 + 2,
6.64/2.53	   
6.64/2.53	   [s](x0) = 3x0 + 2,
6.64/2.53	   
6.68/2.53	   [l] = 4,
6.68/2.53	   
6.68/2.53	   [k] = 3,
6.68/2.53	   
6.68/2.53	   [e] = 0,
6.68/2.53	   
6.68/2.53	   [b] = 3,
6.68/2.53	   
6.68/2.53	   [d] = 1,
6.68/2.53	   
6.68/2.53	   [c] = 3,
6.68/2.53	   
6.68/2.53	   [a] = 3
6.68/2.53	  orientation:
6.68/2.53	   a() = 3 >= 3 = c()
6.68/2.53	   
6.68/2.53	   a() = 3 >= 1 = d()
6.68/2.53	   
6.68/2.53	   b() = 3 >= 3 = c()
6.68/2.53	   
6.68/2.53	   b() = 3 >= 1 = d()
6.68/2.53	   
6.68/2.53	   c() = 3 >= 0 = e()
6.68/2.53	   
6.68/2.53	   d() = 1 >= 0 = e()
6.68/2.53	   
6.68/2.53	   k() = 3 >= 0 = e()
6.68/2.53	   
6.68/2.53	   l() = 4 >= 0 = e()
6.68/2.53	   
6.68/2.53	   s(c()) = 11 >= 8 = t(k())
6.68/2.53	   
6.68/2.53	   s(c()) = 11 >= 10 = t(l())
6.68/2.53	   
6.68/2.53	   s(e()) = 2 >= 2 = t(e())
6.68/2.53	   
6.68/2.53	   g(x,x) = 8x + 4 >= 8x = h(x,x)
6.68/2.53	   
6.68/2.53	   ?1(t(y),x) = x + 4y + 4 >= x + y = pair(x,y)
6.68/2.53	   
6.68/2.53	   f(x) = 7x + 4 >= 7x + 4 = ?1(s(x),x)
6.68/2.53	  problem:
6.68/2.53	   a() -> c()
6.68/2.53	   b() -> c()
6.68/2.53	   s(e()) -> t(e())
6.68/2.53	   f(x) -> ?1(s(x),x)
6.68/2.53	  Matrix Interpretation Processor: dim=1
6.68/2.53	   
6.68/2.53	   interpretation:
6.68/2.53	    [f](x0) = 6x0 + 1,
6.68/2.53	    
6.68/2.53	    [?1](x0, x1) = x0 + 5x1,
6.68/2.53	    
6.68/2.53	    [t](x0) = x0,
6.68/2.53	    
6.68/2.53	    [s](x0) = x0,
6.68/2.53	    
6.68/2.53	    [e] = 4,
6.68/2.53	    
6.68/2.53	    [b] = 0,
6.68/2.53	    
6.68/2.53	    [c] = 0,
6.68/2.53	    
6.68/2.53	    [a] = 0
6.68/2.53	   orientation:
6.68/2.53	    a() = 0 >= 0 = c()
6.68/2.53	    
6.68/2.53	    b() = 0 >= 0 = c()
6.68/2.53	    
6.68/2.53	    s(e()) = 4 >= 4 = t(e())
6.68/2.54	    
6.68/2.54	    f(x) = 6x + 1 >= 6x = ?1(s(x),x)
6.68/2.54	   problem:
6.68/2.54	    a() -> c()
6.68/2.54	    b() -> c()
6.68/2.54	    s(e()) -> t(e())
6.68/2.54	   Matrix Interpretation Processor: dim=3
6.68/2.54	    
6.68/2.54	    interpretation:
6.68/2.54	               [1 0 0]  
6.68/2.54	     [t](x0) = [0 0 0]x0
6.68/2.54	               [0 0 0]  ,
6.68/2.54	     
6.68/2.54	               [1 0 0]     [1]
6.68/2.54	     [s](x0) = [0 0 0]x0 + [0]
6.68/2.54	               [0 0 0]     [0],
6.68/2.54	     
6.68/2.54	           [0]
6.68/2.54	     [e] = [0]
6.68/2.54	           [0],
6.68/2.54	     
6.68/2.54	           [0]
6.68/2.54	     [b] = [0]
6.68/2.54	           [0],
6.68/2.54	     
6.68/2.54	           [0]
6.68/2.54	     [c] = [0]
6.68/2.54	           [0],
6.68/2.54	     
6.68/2.54	           [0]
6.68/2.54	     [a] = [0]
6.68/2.54	           [0]
6.68/2.54	    orientation:
6.68/2.54	           [0]    [0]      
6.68/2.54	     a() = [0] >= [0] = c()
6.68/2.54	           [0]    [0]      
6.68/2.54	     
6.68/2.54	           [0]    [0]      
6.68/2.54	     b() = [0] >= [0] = c()
6.68/2.54	           [0]    [0]      
6.68/2.54	     
6.68/2.54	              [1]    [0]         
6.68/2.54	     s(e()) = [0] >= [0] = t(e())
6.68/2.54	              [0]    [0]         
6.68/2.54	    problem:
6.68/2.54	     a() -> c()
6.68/2.54	     b() -> c()
6.68/2.54	    Matrix Interpretation Processor: dim=3
6.68/2.54	     
6.68/2.54	     interpretation:
6.68/2.54	            [1]
6.68/2.54	      [b] = [0]
6.68/2.54	            [0],
6.68/2.54	      
6.68/2.54	            [0]
6.68/2.54	      [c] = [0]
6.68/2.54	            [0],
6.68/2.54	      
6.68/2.54	            [0]
6.68/2.54	      [a] = [0]
6.68/2.54	            [0]
6.68/2.54	     orientation:
6.68/2.54	            [0]    [0]      
6.68/2.54	      a() = [0] >= [0] = c()
6.68/2.54	            [0]    [0]      
6.68/2.54	      
6.68/2.54	            [1]    [0]      
6.68/2.54	      b() = [0] >= [0] = c()
6.68/2.54	            [0]    [0]      
6.68/2.54	     problem:
6.68/2.54	      a() -> c()
6.68/2.54	     Matrix Interpretation Processor: dim=3
6.68/2.54	      
6.68/2.54	      interpretation:
6.68/2.54	             [0]
6.68/2.54	       [c] = [0]
6.68/2.54	             [0],
6.68/2.54	       
6.68/2.54	             [1]
6.68/2.54	       [a] = [0]
6.68/2.54	             [1]
6.68/2.54	      orientation:
6.68/2.54	             [1]    [0]      
6.68/2.54	       a() = [0] >= [0] = c()
6.68/2.54	             [1]    [0]      
6.68/2.54	      problem:
6.68/2.54	       
6.68/2.54	      Qed
6.68/2.54	All 8 critical pairs are joinable.
6.68/2.54	Overlap: (rule1: s(c) -> t(k), rule2: s(c) -> t(l), pos: ε, mgu: {})
6.68/2.54	CP: t(l) = t(k)
6.68/2.54	This critical pair is context-joinable.
6.68/2.54	Overlap: (rule1: b -> c, rule2: b -> d, pos: ε, mgu: {})
6.68/2.54	CP: d = c
6.68/2.54	This critical pair is context-joinable.
6.68/2.54	Overlap: (rule1: a -> d, rule2: a -> c, pos: ε, mgu: {})
6.68/2.54	CP: c = d
6.68/2.54	This critical pair is context-joinable.
6.68/2.54	Overlap: (rule1: b -> d, rule2: b -> c, pos: ε, mgu: {})
6.68/2.54	CP: c = d
6.68/2.54	This critical pair is context-joinable.
6.68/2.54	Overlap: (rule1: s(c) -> t(k), rule2: c -> e, pos: 1, mgu: {})
6.68/2.54	CP: s(e) = t(k)
6.68/2.54	This critical pair is context-joinable.
6.68/2.54	Overlap: (rule1: a -> c, rule2: a -> d, pos: ε, mgu: {})
6.68/2.54	CP: d = c
6.68/2.54	This critical pair is context-joinable.
6.68/2.54	Overlap: (rule1: s(c) -> t(l), rule2: s(c) -> t(k), pos: ε, mgu: {})
6.68/2.54	CP: t(k) = t(l)
6.68/2.54	This critical pair is context-joinable.
6.68/2.54	Overlap: (rule1: s(c) -> t(l), rule2: c -> e, pos: 1, mgu: {})
6.68/2.54	CP: s(e) = t(l)
6.68/2.54	This critical pair is context-joinable.
6.68/2.54	
6.81/2.62	EOF