116.82/30.75 MAYBE 116.82/30.75 116.82/30.75 Proof: 116.82/30.75 ConCon could not decide confluence of the system. 116.82/30.75 \cite{ALS94}, Theorem 4.1 does not apply. 116.82/30.75 This system is of type 3 or smaller. 116.82/30.75 This system is strongly deterministic. 116.82/30.75 This system is of type 3 or smaller. 116.82/30.75 This system is deterministic. 116.82/30.75 ConCon could not decide if this system is quasi-decreasing. 116.82/30.75 \cite{O02}, p. 214, Proposition 7.2.50 does not apply. 116.82/30.75 This system is of type 3 or smaller. 116.82/30.75 This system is deterministic. 116.82/30.75 System R transformed to optimized U(R). 116.82/30.75 The external tool could not decide termination of the system. 116.82/30.75 Call external tool: 116.82/30.75 ./ttt2.sh 116.82/30.75 Input: 116.82/30.75 (VAR x y) 116.82/30.75 (RULES 116.82/30.75 f(x) -> ?1(a, x) 116.82/30.75 ?1(h(y), x) -> y 116.82/30.75 g(x, b) -> ?2(f(b), x) 116.82/30.75 ?2(x, x) -> ?3(x, x) 116.82/30.75 ?3(c, x) -> g(f(c), x) 116.82/30.75 a -> h(b) 116.82/30.75 a -> h(c) 116.82/30.75 ) 116.82/30.75 116.82/30.75 116.82/30.76 EOF