3.76/1.87	YES
3.76/1.87	
3.76/1.87	Proof:
3.76/1.87	This system is confluent.
3.76/1.88	By \cite{ALS94}, Theorem 4.1.
3.76/1.88	This system is of type 3 or smaller.
3.76/1.88	This system is strongly deterministic.
3.76/1.88	This system is quasi-decreasing.
3.76/1.88	By \cite{O02}, p. 214, Proposition 7.2.50.
3.76/1.88	This system is of type 3 or smaller.
3.76/1.88	This system is deterministic.
3.76/1.88	System R transformed to optimized U(R).
3.76/1.88	This system is terminating.
3.76/1.88	Call external tool:
3.76/1.88	./ttt2.sh
3.76/1.88	Input:
3.76/1.88	(VAR x)
3.76/1.88	(RULES
3.76/1.88	  not(x) -> ?1(x, x)
3.76/1.88	  ?1(true, x) -> false
3.76/1.88	  not(x) -> ?1(x, x)
3.76/1.88	  ?1(false, x) -> true
3.76/1.88	)
3.76/1.88	
3.76/1.88	 Polynomial Interpretation Processor:
3.76/1.88	  dimension: 1
3.76/1.88	  interpretation:
3.76/1.88	   [false] = 4,
3.76/1.88	   
3.76/1.88	   [true] = 5,
3.76/1.88	   
3.76/1.88	   [?1](x0, x1) = -3x0 + 4x0x0 + 3x1x1,
3.76/1.88	   
3.76/1.88	   [not](x0) = 7x0x0 + 1
3.76/1.88	  orientation:
3.76/1.88	   not(x) = 7x*x + 1 >= -3x + 7x*x = ?1(x,x)
3.76/1.88	   
3.76/1.88	   ?1(true(),x) = 3x*x + 85 >= 4 = false()
3.76/1.88	   
3.76/1.88	   ?1(false(),x) = 3x*x + 52 >= 5 = true()
3.76/1.88	  problem:
3.76/1.88	   
3.76/1.88	  Qed
3.76/1.88	All 2 critical pairs are joinable.
3.76/1.88	Overlap: (rule1: not(y) -> true <= y = false, rule2: not(z) -> false <= z = true, pos: ε, mgu: {(y,z)})
3.76/1.88	CP: false = true <= z = false, z = true
3.76/1.88	This critical pair is unfeasible.
3.76/1.88	Overlap: (rule1: not(y) -> false <= y = true, rule2: not(z) -> true <= z = false, pos: ε, mgu: {(y,z)})
3.76/1.88	CP: true = false <= z = true, z = false
3.76/1.88	This critical pair is unfeasible.
3.76/1.88	
4.00/1.92	EOF