0.00/0.51 NO 0.00/0.51 0.00/0.51 Problem: 0.00/0.51 s(a()) -> c() 0.00/0.51 s(b()) -> c() 0.00/0.51 c() -> t(k()) 0.00/0.51 c() -> t(l()) 0.00/0.51 f(x) -> z <= s(x) = z 0.00/0.51 g(x, x) -> h(x, x) 0.00/0.51 0.00/0.51 Proof: 0.00/0.51 This system is not confluent. 0.00/0.51 This system is oriented. 0.00/0.51 For the unconditional CP t(k()) = t(l()) ctcap(t(k())) and ctcap(t(l())) wrt R_u are not unifiable. 0.00/0.51 0.00/0.53 EOF