0.00/0.50 NO 0.00/0.50 0.00/0.50 Problem: 0.00/0.50 a() -> c() 0.00/0.50 a() -> d() 0.00/0.50 b() -> c() 0.00/0.50 b() -> d() 0.00/0.50 g(x, x) -> h(x, x) 0.00/0.50 f(x) -> x <= x = c() 0.00/0.50 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 c() = d() the left- and right-hand sides are two different normal forms wrt R_u. 0.00/0.51 0.00/0.52 EOF