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