0.00/0.70 NO 0.00/0.70 0.00/0.70 Problem: 0.00/0.70 f(x) -> x <= x = e() 0.00/0.70 g(d(), x, x) -> A() 0.00/0.70 h(x, x) -> g(x, x, f(k())) 0.00/0.70 a() -> c() 0.00/0.70 a() -> d() 0.00/0.70 b() -> c() 0.00/0.70 b() -> d() 0.00/0.70 c() -> e() 0.00/0.70 c() -> l() 0.00/0.70 k() -> l() 0.00/0.70 k() -> m() 0.00/0.70 d() -> m() 0.00/0.70 0.00/0.70 Proof: 0.00/0.70 This system is not confluent. 0.00/0.70 This system is oriented. 0.00/0.70 For the unconditional CP g(m(), x, x) = A() ctcap(g(m(), x, x)) and ctcap(A()) wrt R_u are not unifiable. 0.00/0.70 0.00/0.71 EOF