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