3.93/2.04 MAYBE 3.93/2.04 3.93/2.04 Proof: 3.93/2.04 ConCon could not decide confluence of the system. 3.93/2.04 Removed infeasible rules from system R. 3.93/2.04 \cite{ALS94}, Theorem 4.1 does not apply. 3.93/2.04 This system is of type 3 or smaller. 3.93/2.04 This system is strongly deterministic. 3.93/2.04 This system is quasi-decreasing. 3.93/2.04 By \cite{O02}, p. 214, Proposition 7.2.50. 3.93/2.04 This system is of type 3 or smaller. 3.93/2.04 This system is deterministic. 3.93/2.04 System R transformed to U(R). 3.93/2.04 This system is terminating. 3.93/2.04 Call external tool: 3.93/2.04 ./ttt2.sh 3.93/2.04 Input: 3.93/2.04 (VAR x) 3.93/2.04 (RULES 3.93/2.04 h(d) -> c(a) 3.93/2.04 h(d) -> c(b) 3.93/2.04 f(k(a), k(b), x) -> f(x, x, x) 3.93/2.04 ) 3.93/2.04 3.93/2.04 DP Processor: 3.93/2.04 DPs: 3.93/2.04 f#(k(a()),k(b()),x) -> f#(x,x,x) 3.93/2.04 TRS: 3.93/2.04 h(d()) -> c(a()) 3.93/2.05 h(d()) -> c(b()) 3.93/2.05 f(k(a()),k(b()),x) -> f(x,x,x) 3.93/2.05 EDG Processor: 3.93/2.05 DPs: 3.93/2.05 f#(k(a()),k(b()),x) -> f#(x,x,x) 3.93/2.05 TRS: 3.93/2.05 h(d()) -> c(a()) 3.93/2.05 h(d()) -> c(b()) 3.93/2.05 f(k(a()),k(b()),x) -> f(x,x,x) 3.93/2.05 graph: 3.93/2.05 3.93/2.05 SCC Processor: 3.93/2.05 #sccs: 0 3.93/2.05 #rules: 0 3.93/2.05 #arcs: 0/1 3.93/2.05 3.93/2.05 ConCon could not decide whether all 2 critical pairs are joinable or not. 3.93/2.05 Overlap: (rule1: h(d) -> c(b), rule2: h(d) -> c(a), pos: ε, mgu: {}) 3.93/2.05 CP: c(a) = c(b) 3.93/2.05 ConCon could not decide context-joinability of this critical pair. 3.93/2.05 5.97/2.45 EOF