3.41/1.44	MAYBE
3.41/1.44	
3.41/1.44	Proof:
3.41/1.44	ConCon could not decide confluence of the system.
3.41/1.44	\cite{ALS94}, Theorem 4.1 does not apply.
3.41/1.44	This system is of type 3 or smaller.
3.41/1.44	This system is strongly deterministic.
3.41/1.44	This system is quasi-decreasing.
3.41/1.44	By \cite{O02}, p. 214, Proposition 7.2.50.
3.41/1.44	This system is of type 3 or smaller.
3.41/1.44	This system is deterministic.
3.41/1.44	System R transformed to optimized U(R).
3.41/1.44	This system is terminating.
3.41/1.44	Call external tool:
3.41/1.44	./ttt2.sh
3.41/1.44	Input:
3.41/1.44	  b -> d
3.41/1.44	  c -> l
3.41/1.44	  a -> d
3.41/1.44	  h(x, x) -> g(x, x, f(k))
3.41/1.44	  d -> m
3.41/1.44	  b -> c
3.41/1.44	  k -> l
3.41/1.44	  c -> e
3.41/1.44	  f(x) -> ?1(x, x)
3.41/1.44	  ?1(e, x) -> x
3.41/1.44	  g(d, x, x) -> A
3.41/1.44	  a -> c
3.41/1.44	  k -> m
3.41/1.44	
3.41/1.44	 Matrix Interpretation Processor: dim=1
3.41/1.44	  
3.41/1.44	  interpretation:
3.41/1.44	   [A] = 0,
3.41/1.44	   
3.41/1.44	   [?1](x0, x1) = 2x0 + x1 + 1,
3.41/1.44	   
3.41/1.44	   [e] = 4,
3.41/1.44	   
3.41/1.44	   [m] = 0,
3.41/1.44	   
3.41/1.44	   [g](x0, x1, x2) = x0 + 4x1 + x2,
3.41/1.44	   
3.41/1.44	   [f](x0) = 4x0 + 4,
3.41/1.44	   
3.41/1.44	   [k] = 0,
3.41/1.44	   
3.41/1.44	   [h](x0, x1) = x0 + 4x1 + 4,
3.41/1.44	   
3.41/1.44	   [a] = 4,
3.41/1.44	   
3.41/1.44	   [l] = 0,
3.41/1.44	   
3.41/1.44	   [c] = 4,
3.41/1.44	   
3.41/1.44	   [d] = 4,
3.41/1.44	   
3.41/1.44	   [b] = 4
3.41/1.44	  orientation:
3.41/1.44	   b() = 4 >= 4 = d()
3.41/1.44	   
3.41/1.44	   c() = 4 >= 0 = l()
3.41/1.44	   
3.41/1.44	   a() = 4 >= 4 = d()
3.41/1.44	   
3.41/1.44	   h(x,x) = 5x + 4 >= 5x + 4 = g(x,x,f(k()))
3.41/1.44	   
3.41/1.44	   d() = 4 >= 0 = m()
3.41/1.44	   
3.41/1.44	   b() = 4 >= 4 = c()
3.41/1.44	   
3.41/1.44	   k() = 0 >= 0 = l()
3.41/1.44	   
3.41/1.44	   c() = 4 >= 4 = e()
3.41/1.44	   
3.41/1.44	   f(x) = 4x + 4 >= 3x + 1 = ?1(x,x)
3.41/1.44	   
3.41/1.44	   ?1(e(),x) = x + 9 >= x = x
3.41/1.44	   
3.41/1.44	   g(d(),x,x) = 5x + 4 >= 0 = A()
3.41/1.44	   
3.41/1.45	   a() = 4 >= 4 = c()
3.41/1.45	   
3.41/1.45	   k() = 0 >= 0 = m()
3.41/1.45	  problem:
3.41/1.45	   b() -> d()
3.41/1.45	   a() -> d()
3.41/1.45	   h(x,x) -> g(x,x,f(k()))
3.41/1.45	   b() -> c()
3.41/1.45	   k() -> l()
3.41/1.45	   c() -> e()
3.41/1.45	   a() -> c()
3.41/1.45	   k() -> m()
3.41/1.45	  Matrix Interpretation Processor: dim=3
3.41/1.45	   
3.41/1.45	   interpretation:
3.41/1.45	          [0]
3.41/1.45	    [e] = [0]
3.41/1.45	          [0],
3.41/1.45	    
3.41/1.45	          [0]
3.41/1.45	    [m] = [0]
3.41/1.45	          [1],
3.41/1.45	    
3.41/1.45	                      [1 0 0]     [1 0 0]     [1 0 0]     [0]
3.41/1.45	    [g](x0, x1, x2) = [0 0 0]x0 + [0 0 0]x1 + [0 0 0]x2 + [0]
3.41/1.45	                      [0 0 0]     [0 0 0]     [0 0 0]     [1],
3.41/1.45	    
3.41/1.45	              [1 0 0]     [0]
3.41/1.45	    [f](x0) = [0 0 1]x0 + [1]
3.41/1.45	              [0 0 0]     [0],
3.41/1.45	    
3.41/1.45	          [0]
3.41/1.45	    [k] = [0]
3.41/1.45	          [1],
3.41/1.45	    
3.41/1.45	                  [1 0 0]     [1 0 0]     [1]
3.41/1.45	    [h](x0, x1) = [1 0 0]x0 + [1 0 0]x1 + [1]
3.41/1.45	                  [0 0 0]     [0 0 0]     [1],
3.41/1.45	    
3.41/1.45	          [1]
3.41/1.45	    [a] = [1]
3.41/1.45	          [0],
3.41/1.45	    
3.41/1.45	          [0]
3.41/1.45	    [l] = [0]
3.41/1.45	          [1],
3.41/1.45	    
3.41/1.45	          [0]
3.41/1.45	    [c] = [0]
3.41/1.45	          [0],
3.41/1.45	    
3.41/1.45	          [0]
3.41/1.45	    [d] = [0]
3.41/1.45	          [0],
3.41/1.45	    
3.41/1.45	          [0]
3.41/1.45	    [b] = [0]
3.41/1.45	          [0]
3.41/1.45	   orientation:
3.41/1.45	          [0]    [0]      
3.41/1.45	    b() = [0] >= [0] = d()
3.41/1.45	          [0]    [0]      
3.41/1.45	    
3.41/1.45	          [1]    [0]      
3.41/1.45	    a() = [1] >= [0] = d()
3.41/1.45	          [0]    [0]      
3.41/1.45	    
3.41/1.45	             [2 0 0]    [1]    [2 0 0]    [0]                
3.41/1.45	    h(x,x) = [2 0 0]x + [1] >= [0 0 0]x + [0] = g(x,x,f(k()))
3.41/1.45	             [0 0 0]    [1]    [0 0 0]    [1]                
3.41/1.45	    
3.41/1.45	          [0]    [0]      
3.41/1.45	    b() = [0] >= [0] = c()
3.41/1.45	          [0]    [0]      
3.41/1.45	    
3.41/1.45	          [0]    [0]      
3.41/1.45	    k() = [0] >= [0] = l()
3.41/1.45	          [1]    [1]      
3.41/1.45	    
3.41/1.45	          [0]    [0]      
3.41/1.45	    c() = [0] >= [0] = e()
3.41/1.45	          [0]    [0]      
3.41/1.45	    
3.41/1.45	          [1]    [0]      
3.41/1.45	    a() = [1] >= [0] = c()
3.41/1.45	          [0]    [0]      
3.41/1.45	    
3.41/1.45	          [0]    [0]      
3.41/1.45	    k() = [0] >= [0] = m()
3.41/1.45	          [1]    [1]      
3.41/1.45	   problem:
3.41/1.45	    b() -> d()
3.41/1.45	    b() -> c()
3.41/1.45	    k() -> l()
3.41/1.45	    c() -> e()
3.41/1.45	    k() -> m()
3.41/1.45	   Matrix Interpretation Processor: dim=3
3.41/1.45	    
3.41/1.45	    interpretation:
3.41/1.45	           [0]
3.41/1.45	     [e] = [0]
3.41/1.45	           [0],
3.41/1.45	     
3.41/1.45	           [0]
3.65/1.45	     [m] = [0]
3.65/1.45	           [0],
3.65/1.45	     
3.65/1.45	           [1]
3.65/1.45	     [k] = [0]
3.65/1.45	           [0],
3.65/1.45	     
3.65/1.45	           [0]
3.65/1.45	     [l] = [0]
3.65/1.45	           [0],
3.65/1.45	     
3.65/1.45	           [0]
3.65/1.45	     [c] = [0]
3.65/1.45	           [0],
3.65/1.45	     
3.65/1.45	           [0]
3.65/1.45	     [d] = [0]
3.65/1.45	           [0],
3.65/1.45	     
3.65/1.45	           [1]
3.65/1.45	     [b] = [0]
3.65/1.45	           [0]
3.65/1.45	    orientation:
3.65/1.45	           [1]    [0]      
3.65/1.45	     b() = [0] >= [0] = d()
3.65/1.45	           [0]    [0]      
3.65/1.45	     
3.65/1.45	           [1]    [0]      
3.65/1.45	     b() = [0] >= [0] = c()
3.65/1.46	           [0]    [0]      
3.65/1.46	     
3.65/1.46	           [1]    [0]      
3.65/1.46	     k() = [0] >= [0] = l()
3.65/1.46	           [0]    [0]      
3.65/1.46	     
3.65/1.46	           [0]    [0]      
3.65/1.46	     c() = [0] >= [0] = e()
3.65/1.46	           [0]    [0]      
3.65/1.46	     
3.65/1.46	           [1]    [0]      
3.65/1.46	     k() = [0] >= [0] = m()
3.65/1.46	           [0]    [0]      
3.65/1.46	    problem:
3.65/1.46	     c() -> e()
3.65/1.46	    Matrix Interpretation Processor: dim=3
3.65/1.46	     
3.65/1.46	     interpretation:
3.65/1.46	            [0]
3.65/1.46	      [e] = [0]
3.65/1.46	            [0],
3.65/1.46	      
3.65/1.46	            [1]
3.65/1.46	      [c] = [0]
3.65/1.46	            [1]
3.65/1.46	     orientation:
3.65/1.46	            [1]    [0]      
3.65/1.46	      c() = [0] >= [0] = e()
3.65/1.46	            [1]    [0]      
3.65/1.46	     problem:
3.65/1.46	      
3.65/1.46	     Qed
3.65/1.46	This critical pair is not infeasible.
3.65/1.46	This critical pair is unconditional.
3.65/1.46	
3.65/1.47	EOF