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