2.75/1.32	YES
2.75/1.32	
2.75/1.32	Problem:
2.75/1.32	a() -> c()
2.75/1.32	a() -> d()
2.75/1.32	b() -> c()
2.75/1.32	b() -> d()
2.75/1.32	c() -> e()
2.75/1.32	d() -> e()
2.75/1.32	k() -> e()
2.75/1.32	l() -> e()
2.75/1.32	s(c()) -> t(k())
2.75/1.32	s(c()) -> t(l())
2.75/1.32	s(e()) -> t(e())
2.75/1.32	g(x, x) -> h(x, x)
2.75/1.32	f(x) -> pair(x, y) <= s(x) = t(y)
2.75/1.32	
2.75/1.33	Proof:
2.75/1.33	This system is confluent.
2.75/1.33	By \cite{ALS94}, Theorem 4.1.
2.75/1.33	This system is of type 3 or smaller.
2.75/1.33	This system is strongly deterministic.
2.75/1.33	All 8 critical pairs are joinable.
2.75/1.33	CP: d() = c():
2.75/1.33	This critical pair is context-joinable.
2.75/1.33	CP: s(e()) = t(k()):
2.75/1.33	This critical pair is context-joinable.
2.75/1.33	CP: c() = d():
2.75/1.33	This critical pair is context-joinable.
2.75/1.33	CP: t(l()) = t(k()):
2.75/1.33	This critical pair is context-joinable.
2.75/1.33	CP: s(e()) = t(l()):
2.75/1.33	This critical pair is context-joinable.
2.75/1.33	CP: c() = d():
2.75/1.33	This critical pair is context-joinable.
2.75/1.33	CP: d() = c():
2.75/1.33	This critical pair is context-joinable.
2.75/1.33	CP: t(k()) = t(l()):
2.75/1.33	This critical pair is context-joinable.
2.75/1.33	This system is quasi-decreasing.
2.75/1.33	By \cite{A14}, Theorem 11.5.9.
2.75/1.33	This system is of type 3 or smaller.
2.75/1.33	This system is deterministic.
2.75/1.33	System R transformed to V(R) + Emb.
2.75/1.33	This system is terminating.
2.75/1.33	Call external tool:
2.75/1.33	./ttt2.sh
2.75/1.33	Input:
2.75/1.33	  a() -> c()
2.75/1.33	  a() -> d()
2.75/1.33	  b() -> c()
2.75/1.33	  b() -> d()
2.75/1.33	  c() -> e()
2.75/1.33	  d() -> e()
2.75/1.33	  k() -> e()
2.75/1.33	  l() -> e()
2.75/1.33	  s(c()) -> t(k())
2.75/1.33	  s(c()) -> t(l())
2.75/1.33	  s(e()) -> t(e())
2.75/1.33	  g(x, x) -> h(x, x)
2.75/1.33	  f(x) -> pair(x, s(x))
2.75/1.33	  f(x) -> s(x)
2.75/1.33	  h(x, y) -> x
2.75/1.33	  h(x, y) -> y
2.75/1.33	  pair(x, y) -> x
2.75/1.33	  pair(x, y) -> y
2.75/1.33	  s(x) -> x
2.75/1.33	  g(x, y) -> x
2.75/1.33	  g(x, y) -> y
2.75/1.33	  t(x) -> x
2.75/1.33	  f(x) -> x
2.75/1.33	
2.75/1.33	 Matrix Interpretation Processor: dim=1
2.75/1.33	  
2.75/1.33	  interpretation:
2.75/1.33	   [pair](x0, x1) = 2x0 + 2x1,
2.75/1.34	   
2.75/1.34	   [f](x0) = 7x0 + 4,
2.75/1.34	   
2.75/1.34	   [h](x0, x1) = 4x0 + 2x1,
2.75/1.34	   
2.75/1.34	   [g](x0, x1) = 2x0 + 4x1,
2.75/1.34	   
2.75/1.34	   [t](x0) = x0 + 2,
2.75/1.34	   
2.75/1.34	   [s](x0) = 2x0 + 2,
2.75/1.34	   
2.75/1.34	   [l] = 6,
2.75/1.34	   
2.75/1.34	   [k] = 6,
2.75/1.34	   
2.75/1.34	   [e] = 2,
2.75/1.34	   
2.75/1.34	   [b] = 3,
2.75/1.34	   
2.75/1.34	   [d] = 3,
2.75/1.34	   
2.75/1.34	   [c] = 3,
2.75/1.34	   
2.75/1.34	   [a] = 3
2.75/1.34	  orientation:
2.75/1.34	   a() = 3 >= 3 = c()
2.75/1.34	   
2.75/1.34	   a() = 3 >= 3 = d()
2.75/1.34	   
2.75/1.34	   b() = 3 >= 3 = c()
2.75/1.34	   
2.75/1.34	   b() = 3 >= 3 = d()
2.75/1.34	   
2.75/1.34	   c() = 3 >= 2 = e()
2.75/1.34	   
2.75/1.34	   d() = 3 >= 2 = e()
2.75/1.34	   
2.75/1.34	   k() = 6 >= 2 = e()
2.75/1.34	   
2.75/1.34	   l() = 6 >= 2 = e()
2.75/1.34	   
2.75/1.34	   s(c()) = 8 >= 8 = t(k())
2.75/1.34	   
2.75/1.34	   s(c()) = 8 >= 8 = t(l())
2.75/1.34	   
2.75/1.34	   s(e()) = 6 >= 4 = t(e())
2.75/1.34	   
2.75/1.34	   g(x,x) = 6x >= 6x = h(x,x)
2.75/1.34	   
2.75/1.34	   f(x) = 7x + 4 >= 6x + 4 = pair(x,s(x))
2.75/1.34	   
2.75/1.34	   f(x) = 7x + 4 >= 2x + 2 = s(x)
2.75/1.34	   
2.75/1.34	   h(x,y) = 4x + 2y >= x = x
2.75/1.34	   
2.75/1.34	   h(x,y) = 4x + 2y >= y = y
2.75/1.34	   
2.75/1.34	   pair(x,y) = 2x + 2y >= x = x
2.75/1.34	   
2.75/1.34	   pair(x,y) = 2x + 2y >= y = y
2.75/1.34	   
2.75/1.34	   s(x) = 2x + 2 >= x = x
2.75/1.34	   
2.75/1.34	   g(x,y) = 2x + 4y >= x = x
2.75/1.34	   
2.75/1.34	   g(x,y) = 2x + 4y >= y = y
2.75/1.34	   
2.75/1.34	   t(x) = x + 2 >= x = x
2.75/1.34	   
2.75/1.34	   f(x) = 7x + 4 >= x = x
2.75/1.34	  problem:
2.75/1.34	   a() -> c()
2.75/1.34	   a() -> d()
2.75/1.34	   b() -> c()
2.75/1.34	   b() -> d()
2.75/1.34	   s(c()) -> t(k())
2.75/1.34	   s(c()) -> t(l())
2.75/1.34	   g(x,x) -> h(x,x)
2.75/1.34	   f(x) -> pair(x,s(x))
2.75/1.34	   h(x,y) -> x
2.75/1.34	   h(x,y) -> y
2.75/1.34	   pair(x,y) -> x
2.75/1.34	   pair(x,y) -> y
2.75/1.34	   g(x,y) -> x
2.75/1.34	   g(x,y) -> y
2.75/1.34	  Matrix Interpretation Processor: dim=1
2.75/1.34	   
2.75/1.34	   interpretation:
2.75/1.34	    [pair](x0, x1) = x0 + x1,
2.75/1.34	    
2.75/1.34	    [f](x0) = 7x0 + 7,
2.75/1.34	    
2.75/1.34	    [h](x0, x1) = x0 + 2x1,
2.75/1.34	    
2.75/1.34	    [g](x0, x1) = x0 + 4x1,
2.75/1.34	    
2.75/1.34	    [t](x0) = 3x0 + 3,
2.75/1.34	    
2.75/1.34	    [s](x0) = 6x0 + 6,
2.75/1.34	    
2.75/1.35	    [l] = 7,
2.75/1.35	    
2.75/1.35	    [k] = 4,
2.75/1.35	    
2.75/1.35	    [b] = 3,
2.75/1.35	    
2.75/1.35	    [d] = 0,
2.75/1.35	    
2.75/1.35	    [c] = 3,
2.75/1.35	    
2.75/1.35	    [a] = 4
2.75/1.35	   orientation:
2.75/1.35	    a() = 4 >= 3 = c()
2.75/1.35	    
2.75/1.35	    a() = 4 >= 0 = d()
2.75/1.35	    
2.75/1.35	    b() = 3 >= 3 = c()
2.75/1.35	    
2.75/1.35	    b() = 3 >= 0 = d()
2.75/1.35	    
2.75/1.35	    s(c()) = 24 >= 15 = t(k())
2.75/1.35	    
2.75/1.35	    s(c()) = 24 >= 24 = t(l())
2.75/1.35	    
2.75/1.35	    g(x,x) = 5x >= 3x = h(x,x)
2.75/1.35	    
2.75/1.35	    f(x) = 7x + 7 >= 7x + 6 = pair(x,s(x))
2.75/1.35	    
2.75/1.35	    h(x,y) = x + 2y >= x = x
2.75/1.35	    
2.75/1.35	    h(x,y) = x + 2y >= y = y
2.75/1.35	    
2.75/1.35	    pair(x,y) = x + y >= x = x
2.75/1.35	    
2.75/1.35	    pair(x,y) = x + y >= y = y
2.75/1.35	    
2.75/1.35	    g(x,y) = x + 4y >= x = x
2.75/1.35	    
2.75/1.35	    g(x,y) = x + 4y >= y = y
2.75/1.35	   problem:
2.75/1.35	    b() -> c()
2.75/1.35	    s(c()) -> t(l())
2.75/1.35	    g(x,x) -> h(x,x)
2.75/1.35	    h(x,y) -> x
2.75/1.35	    h(x,y) -> y
2.75/1.35	    pair(x,y) -> x
2.75/1.35	    pair(x,y) -> y
2.75/1.35	    g(x,y) -> x
2.75/1.35	    g(x,y) -> y
2.75/1.35	   Matrix Interpretation Processor: dim=1
2.75/1.35	    
2.75/1.35	    interpretation:
2.75/1.35	     [pair](x0, x1) = x0 + 2x1 + 1,
2.75/1.35	     
2.75/1.36	     [h](x0, x1) = x0 + x1 + 1,
2.75/1.36	     
2.75/1.36	     [g](x0, x1) = 4x0 + 2x1 + 2,
2.75/1.36	     
2.75/1.36	     [t](x0) = 2x0 + 5,
2.75/1.36	     
2.75/1.36	     [s](x0) = 4x0,
2.75/1.36	     
2.75/1.36	     [l] = 4,
2.75/1.36	     
2.75/1.36	     [b] = 5,
2.75/1.36	     
2.75/1.36	     [c] = 4
2.75/1.36	    orientation:
2.75/1.36	     b() = 5 >= 4 = c()
2.75/1.36	     
2.75/1.36	     s(c()) = 16 >= 13 = t(l())
2.75/1.36	     
2.75/1.36	     g(x,x) = 6x + 2 >= 2x + 1 = h(x,x)
2.75/1.36	     
2.75/1.36	     h(x,y) = x + y + 1 >= x = x
2.75/1.36	     
2.75/1.36	     h(x,y) = x + y + 1 >= y = y
2.75/1.36	     
2.75/1.36	     pair(x,y) = x + 2y + 1 >= x = x
2.75/1.36	     
2.75/1.36	     pair(x,y) = x + 2y + 1 >= y = y
2.75/1.36	     
2.75/1.36	     g(x,y) = 4x + 2y + 2 >= x = x
2.75/1.36	     
2.75/1.36	     g(x,y) = 4x + 2y + 2 >= y = y
2.75/1.36	    problem:
2.75/1.36	     
2.75/1.36	    Qed
2.75/1.36	
3.57/1.56	EOF