3.25/1.39	MAYBE
3.25/1.39	
3.25/1.39	Proof:
3.25/1.39	ConCon could not decide confluence of the system.
3.25/1.39	\cite{ALS94}, Theorem 4.1 does not apply.
3.25/1.39	This system is of type 3 or smaller.
3.25/1.39	This system is strongly deterministic.
3.25/1.39	This system is quasi-decreasing.
3.25/1.39	By \cite{A14}, Theorem 11.5.9.
3.25/1.39	This system is of type 3 or smaller.
3.25/1.39	This system is deterministic.
3.25/1.39	System R transformed to V(R) + Emb.
3.25/1.39	This system is terminating.
3.25/1.39	Call external tool:
3.25/1.39	./ttt2.sh
3.25/1.39	Input:
3.25/1.39	  a -> c
3.25/1.39	  a -> d
3.25/1.39	  b -> c
3.25/1.39	  b -> d
3.25/1.39	  f(x) -> x
3.25/1.39	  g(x, x) -> h(x, x)
3.25/1.39	  h(x, f(x)) -> x
3.25/1.39	  h(x, y) -> x
3.25/1.39	  h(x, y) -> y
3.25/1.39	  g(x, y) -> x
3.25/1.39	  g(x, y) -> y
3.25/1.39	  f(x) -> x
3.25/1.39	
3.25/1.39	 Matrix Interpretation Processor: dim=3
3.25/1.39	  
3.25/1.39	  interpretation:
3.25/1.39	                 [1 0 0]     [1 1 0]  
3.25/1.39	   [h](x0, x1) = [0 1 0]x0 + [0 1 0]x1
3.25/1.40	                 [0 1 1]     [0 0 1]  ,
3.25/1.40	   
3.25/1.40	                      [1 1 0]     [1]
3.25/1.40	   [g](x0, x1) = x0 + [0 1 0]x1 + [0]
3.25/1.40	                      [0 1 1]     [0],
3.25/1.40	   
3.25/1.40	             [1 0 0]  
3.25/1.40	   [f](x0) = [1 1 0]x0
3.25/1.40	             [0 0 1]  ,
3.25/1.40	   
3.25/1.40	         [1]
3.25/1.40	   [b] = [0]
3.25/1.40	         [0],
3.25/1.40	   
3.25/1.40	         [0]
3.25/1.40	   [d] = [0]
3.25/1.40	         [0],
3.25/1.40	   
3.25/1.40	         [0]
3.25/1.40	   [c] = [0]
3.25/1.40	         [0],
3.25/1.40	   
3.25/1.40	         [1]
3.25/1.40	   [a] = [0]
3.25/1.40	         [0]
3.25/1.40	  orientation:
3.25/1.40	         [1]    [0]      
3.25/1.40	   a() = [0] >= [0] = c()
3.25/1.40	         [0]    [0]      
3.25/1.40	   
3.25/1.40	         [1]    [0]      
3.25/1.40	   a() = [0] >= [0] = d()
3.25/1.40	         [0]    [0]      
3.25/1.40	   
3.25/1.40	         [1]    [0]      
3.25/1.40	   b() = [0] >= [0] = c()
3.25/1.40	         [0]    [0]      
3.25/1.40	   
3.25/1.40	         [1]    [0]      
3.25/1.40	   b() = [0] >= [0] = d()
3.25/1.40	         [0]    [0]      
3.25/1.40	   
3.25/1.40	          [1 0 0]          
3.25/1.40	   f(x) = [1 1 0]x >= x = x
3.25/1.40	          [0 0 1]          
3.25/1.40	   
3.25/1.40	            [2 1 0]    [1]    [2 1 0]          
3.25/1.40	   g(x,x) = [0 2 0]x + [0] >= [0 2 0]x = h(x,x)
3.25/1.40	            [0 1 2]    [0]    [0 1 2]          
3.25/1.40	   
3.25/1.40	               [3 1 0]          
3.25/1.40	   h(x,f(x)) = [1 2 0]x >= x = x
3.25/1.40	               [0 1 2]          
3.25/1.40	   
3.25/1.40	            [1 0 0]    [1 1 0]          
3.25/1.40	   h(x,y) = [0 1 0]x + [0 1 0]y >= x = x
3.25/1.40	            [0 1 1]    [0 0 1]          
3.25/1.40	   
3.25/1.40	            [1 0 0]    [1 1 0]          
3.25/1.40	   h(x,y) = [0 1 0]x + [0 1 0]y >= y = y
3.25/1.40	            [0 1 1]    [0 0 1]          
3.25/1.40	   
3.25/1.40	                [1 1 0]    [1]         
3.25/1.40	   g(x,y) = x + [0 1 0]y + [0] >= x = x
3.25/1.40	                [0 1 1]    [0]         
3.25/1.40	   
3.25/1.40	                [1 1 0]    [1]         
3.25/1.40	   g(x,y) = x + [0 1 0]y + [0] >= y = y
3.25/1.40	                [0 1 1]    [0]         
3.25/1.40	  problem:
3.25/1.40	   f(x) -> x
3.25/1.40	   h(x,f(x)) -> x
3.25/1.40	   h(x,y) -> x
3.25/1.40	   h(x,y) -> y
3.25/1.40	  Matrix Interpretation Processor: dim=1
3.25/1.40	   
3.25/1.40	   interpretation:
3.25/1.40	    [h](x0, x1) = x0 + 5x1 + 1,
3.25/1.40	    
3.25/1.40	    [f](x0) = x0 + 3
3.25/1.40	   orientation:
3.25/1.40	    f(x) = x + 3 >= x = x
3.25/1.40	    
3.25/1.40	    h(x,f(x)) = 6x + 16 >= x = x
3.25/1.40	    
3.25/1.40	    h(x,y) = x + 5y + 1 >= x = x
3.25/1.40	    
3.25/1.40	    h(x,y) = x + 5y + 1 >= y = y
3.25/1.40	   problem:
3.25/1.40	    
3.25/1.40	   Qed
3.25/1.40	Overlap: (rule1: h(y, f(y)) -> y, rule2: f(z) -> z <= z = c, pos: 2, mgu: {(z,y)})
3.25/1.40	CP: h(y, y) = y <= y = c
3.25/1.40	This critical pair is infeasible.
3.25/1.40	This critical pair is conditional.
3.25/1.40	This critical pair has some non-trivial conditions.
3.25/1.40	Call external tool:
3.25/1.40	./waldmeister
3.25/1.40	Input:
3.25/1.40	  a -> c
3.25/1.40	  a -> d
3.25/1.40	  b -> c
3.25/1.40	  b -> d
3.25/1.40	  f(x) -> x <= x = c
3.25/1.40	  g(x, x) -> h(x, x)
3.25/1.40	  h(x, f(x)) -> x
3.25/1.40	
3.25/1.41	By Waldmeister.
3.25/1.41	This critical pair is not unfeasible.
3.25/1.41	ConCon could not decide whether all 5 critical pairs are joinable or not.
3.25/1.41	Overlap: (rule1: b -> c, rule2: b -> d, pos: ε, mgu: {})
3.25/1.41	CP: d = c
3.25/1.41	This critical pair is not unfeasible.
3.25/1.41	
3.34/1.43	EOF