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.58 (VAR x y) 2.00/1.58 (RULES 2.00/1.58 f(x, y) -> g(s(x)) 2.00/1.58 f(x, y) -> c(g(x)) 2.00/1.58 f(x, y) -> h(s(x)) 2.00/1.58 f(x, y) -> c(h(x)) 2.00/1.58 g(s(x)) -> x 2.00/1.58 h(s(x)) -> x 2.00/1.58 b -> b 2.00/1.58 h(x) -> x 2.00/1.58 s(x) -> x 2.00/1.58 c(x) -> x 2.00/1.58 g(x) -> x 2.00/1.58 f(x, y) -> x 2.00/1.58 f(x, y) -> y 2.00/1.58 ) 2.00/1.58 2.00/1.58 Containment Processor: loop length: 1 2.00/1.58 terms: 2.00/1.58 b() 2.00/1.58 context: [] 2.00/1.58 substitution: 2.00/1.58 2.00/1.58 Qed 2.00/1.58 ConCon could not decide if this system is quasi-decreasing. 2.00/1.58 \cite{A14}, Theorem 11.5.9 does not apply. 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.58 (VAR x y) 2.00/1.58 (RULES 2.00/1.58 f(x, y) -> g(s(x)) 2.00/1.58 f(x, y) -> c(g(x)) 2.00/1.58 f(x, y) -> h(s(x)) 2.00/1.58 f(x, y) -> c(h(x)) 2.00/1.58 g(s(x)) -> x 2.00/1.58 h(s(x)) -> x 2.00/1.58 b -> b 2.00/1.58 h(x) -> x 2.00/1.58 s(x) -> x 2.00/1.58 c(x) -> x 2.00/1.58 g(x) -> x 2.00/1.58 f(x, y) -> x 2.00/1.58 f(x, y) -> y 2.00/1.58 ) 2.00/1.58 2.00/1.58 Containment Processor: loop length: 1 2.00/1.58 terms: 2.00/1.58 b() 2.00/1.58 context: [] 2.00/1.58 substitution: 2.00/1.58 2.00/1.58 Qed 2.00/1.58 2.93/1.61 EOF