2.00/1.58 MAYBE 2.00/1.58 2.00/1.58 Proof: 2.00/1.58 ConCon could not decide confluence of the system. 2.00/1.58 \cite{ALS94}, Theorem 4.1 does not apply. 2.00/1.58 This system is of type 3 or smaller. 2.00/1.58 This system is strongly deterministic. 2.00/1.58 This system is of type 3 or smaller. 2.00/1.58 This system is deterministic. 2.00/1.58 This system is non-terminating. 2.00/1.58 Call external tool: 2.00/1.58 ./ttt2.sh 2.00/1.58 Input: 2.00/1.59 (VAR x y) 2.00/1.59 (RULES 2.00/1.59 f(x, y) -> g(s(x)) 2.00/1.59 f(x, y) -> c(g(x)) 2.00/1.59 f(x, y) -> h(s(x)) 2.00/1.59 f(x, y) -> c(h(x)) 2.00/1.59 g(s(x)) -> x 2.00/1.59 h(s(x)) -> x 2.00/1.59 b -> b 2.00/1.59 h(x) -> x 2.00/1.59 s(x) -> x 2.00/1.59 c(x) -> x 2.00/1.59 g(x) -> x 2.00/1.59 f(x, y) -> x 2.00/1.59 f(x, y) -> y 2.00/1.59 ) 2.00/1.59 2.00/1.59 Containment Processor: loop length: 1 2.00/1.59 terms: 2.00/1.59 b() 2.00/1.59 context: [] 2.00/1.59 substitution: 2.00/1.59 2.00/1.59 Qed 2.00/1.59 ConCon could not decide if this system is quasi-decreasing. 2.00/1.59 \cite{A14}, Theorem 11.5.9 does not apply. 2.00/1.59 This system is of type 3 or smaller. 2.00/1.59 This system is deterministic. 2.00/1.59 This system is non-terminating. 2.00/1.59 Call external tool: 2.00/1.59 ./ttt2.sh 2.00/1.59 Input: 2.00/1.59 (VAR x y) 2.00/1.59 (RULES 2.00/1.59 f(x, y) -> g(s(x)) 2.00/1.59 f(x, y) -> c(g(x)) 2.00/1.59 f(x, y) -> h(s(x)) 2.00/1.59 f(x, y) -> c(h(x)) 2.00/1.59 g(s(x)) -> x 2.00/1.59 h(s(x)) -> x 2.00/1.59 b -> b 2.00/1.59 h(x) -> x 2.00/1.59 s(x) -> x 2.00/1.59 c(x) -> x 2.00/1.59 g(x) -> x 2.00/1.59 f(x, y) -> x 2.00/1.59 f(x, y) -> y 2.00/1.59 ) 2.00/1.59 2.00/1.59 Containment Processor: loop length: 1 2.00/1.59 terms: 2.00/1.59 b() 2.00/1.59 context: [] 2.00/1.59 substitution: 2.00/1.59 2.00/1.59 Qed 2.00/1.59 2.92/1.59 EOF