3.68/1.86	MAYBE
3.68/1.86	
3.68/1.86	Proof:
3.68/1.86	ConCon could not decide confluence of the system.
3.68/1.86	Inlined conditions in System R.
3.68/1.86	\cite{ALS94}, Theorem 4.1 does not apply.
3.68/1.86	This system is of type 3 or smaller.
3.68/1.86	This system is strongly deterministic.
3.68/1.86	This system is quasi-decreasing.
3.68/1.86	By \cite{O02}, p. 214, Proposition 7.2.50.
3.68/1.86	This system is of type 3 or smaller.
3.68/1.86	This system is deterministic.
3.68/1.86	System R transformed to optimized U(R).
3.68/1.86	This system is terminating.
3.68/1.86	Call external tool:
3.68/1.86	./ttt2.sh
3.68/1.86	Input:
3.68/1.86	(VAR x)
3.68/1.86	(RULES
3.68/1.86	  c -> t(k)
3.68/1.86	  f(x) -> s(x)
3.68/1.86	  c -> t(l)
3.68/1.86	  s(b) -> c
3.68/1.86	  g(x, x) -> h(x, x)
3.68/1.86	  s(a) -> c
3.68/1.86	)
3.68/1.86	
3.68/1.86	 Polynomial Interpretation Processor:
3.68/1.86	  dimension: 1
3.68/1.86	  interpretation:
3.68/1.86	   [a] = 2,
3.68/1.86	   
3.68/1.86	   [h](x0, x1) = 3x0 + 5x1 + 2x0x0,
3.68/1.86	   
3.68/1.86	   [g](x0, x1) = 7x0 + 6x1 + 2x1x1 + 2,
3.68/1.86	   
3.68/1.86	   [b] = 4,
3.68/1.86	   
3.68/1.86	   [l] = 0,
3.68/1.86	   
3.68/1.86	   [s](x0) = x0 + 4x0x0 + 4,
3.68/1.86	   
3.68/1.86	   [f](x0) = 4x0 + 7x0x0 + 6,
3.68/1.86	   
3.68/1.86	   [t](x0) = 5x0 + x0x0,
3.68/1.86	   
3.68/1.86	   [k] = 0,
3.68/1.86	   
3.68/1.86	   [c] = 4
3.68/1.86	  orientation:
3.68/1.86	   c() = 4 >= 0 = t(k())
3.68/1.86	   
3.68/1.86	   f(x) = 4x + 7x*x + 6 >= x + 4x*x + 4 = s(x)
3.68/1.86	   
3.68/1.86	   c() = 4 >= 0 = t(l())
3.68/1.86	   
3.68/1.86	   s(b()) = 72 >= 4 = c()
3.68/1.86	   
3.68/1.86	   g(x,x) = 13x + 2x*x + 2 >= 8x + 2x*x = h(x,x)
3.79/1.86	   
3.79/1.87	   s(a()) = 22 >= 4 = c()
3.79/1.87	  problem:
3.79/1.87	   
3.79/1.87	  Qed
3.79/1.87	ConCon could not decide whether all 2 critical pairs are joinable or not.
3.79/1.87	Overlap: (rule1: c -> t(l), rule2: c -> t(k), pos: ε, mgu: {})
3.79/1.87	CP: t(k) = t(l)
3.79/1.87	ConCon could not decide context-joinability of this critical pair.
3.79/1.87	
3.79/1.87	EOF