6.45/2.58	MAYBE
6.45/2.58	
6.45/2.58	Proof:
6.45/2.58	ConCon could not decide confluence of the system.
6.45/2.58	\cite{ALS94}, Theorem 4.1 does not apply.
6.45/2.58	This system is of type 3 or smaller.
6.45/2.58	This system is strongly deterministic.
6.45/2.58	This system is quasi-decreasing.
6.45/2.58	By \cite{A14}, Theorem 11.5.9.
6.45/2.58	This system is of type 3 or smaller.
6.45/2.58	This system is deterministic.
6.45/2.58	System R transformed to V(R) + Emb.
6.45/2.58	This system is terminating.
6.45/2.58	Call external tool:
6.45/2.58	./ttt2.sh
6.45/2.58	Input:
6.45/2.58	(VAR x y)
6.45/2.58	(RULES
6.45/2.58	  f(x, y) -> g(x)
6.45/2.58	  f(x, y) -> a
6.45/2.58	  f(x, y) -> h(x)
6.45/2.58	  f(x, y) -> b
6.45/2.58	  g(s(x)) -> x
6.45/2.58	  h(s(x)) -> x
6.45/2.58	  a -> d
6.45/2.58	  b -> d
6.45/2.58	  h(x) -> x
6.45/2.58	  s(x) -> x
6.45/2.58	  g(x) -> x
6.45/2.58	  f(x, y) -> x
6.45/2.58	  f(x, y) -> y
6.45/2.58	)
6.45/2.58	
6.45/2.58	 Polynomial Interpretation Processor:
6.45/2.58	  dimension: 1
6.45/2.58	  interpretation:
6.45/2.58	   [d] = 0,
6.45/2.58	   
6.45/2.58	   [s](x0) = x0 + 3,
6.45/2.58	   
6.45/2.58	   [b] = 1,
6.45/2.58	   
6.45/2.58	   [h](x0) = 4x0 + 4,
6.45/2.58	   
6.45/2.58	   [a] = 2,
6.45/2.58	   
6.45/2.58	   [g](x0) = 4x0 + 4,
6.45/2.58	   
6.45/2.58	   [f](x0, x1) = 4x0 + 4x1 + 7
6.45/2.58	  orientation:
6.45/2.58	   f(x,y) = 4x + 4y + 7 >= 4x + 4 = g(x)
6.45/2.58	   
6.45/2.58	   f(x,y) = 4x + 4y + 7 >= 2 = a()
6.45/2.58	   
6.45/2.58	   f(x,y) = 4x + 4y + 7 >= 4x + 4 = h(x)
6.45/2.58	   
6.45/2.58	   f(x,y) = 4x + 4y + 7 >= 1 = b()
6.45/2.58	   
6.45/2.58	   g(s(x)) = 4x + 16 >= x = x
6.45/2.58	   
6.45/2.58	   h(s(x)) = 4x + 16 >= x = x
6.45/2.58	   
6.45/2.58	   a() = 2 >= 0 = d()
6.45/2.58	   
6.45/2.58	   b() = 1 >= 0 = d()
6.45/2.58	   
6.45/2.58	   h(x) = 4x + 4 >= x = x
6.45/2.58	   
6.45/2.58	   s(x) = x + 3 >= x = x
6.45/2.58	   
6.45/2.58	   g(x) = 4x + 4 >= x = x
6.45/2.58	   
6.45/2.58	   f(x,y) = 4x + 4y + 7 >= x = x
6.45/2.58	   
6.45/2.58	   f(x,y) = 4x + 4y + 7 >= y = y
6.45/2.58	  problem:
6.45/2.58	   
6.45/2.58	  Qed
6.45/2.58	This critical pair is conditional.
6.45/2.58	This critical pair has some non-trivial conditions.
6.45/2.58	ConCon could not decide whether all 2 critical pairs are joinable or not.
6.45/2.58	Overlap: (rule1: f(z, x') -> h(z) <= b = d, rule2: f(y', z') -> g(y') <= a = d, pos: ε, mgu: {(z,y'), (x',z')})
6.45/2.58	CP: g(y') = h(y') <= b = d, a = d
6.45/2.58	ConCon could not decide infeasibility of this critical pair.
6.45/2.58	
6.45/2.60	EOF