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