0.00/0.04 YES 0.00/0.04 (ignored inputs)COMMENT [121] Example 6.3 submitted by: Thomas Sternagel 0.00/0.04 Conditional Rewrite Rules: 0.00/0.04 [ f(b) -> f(a), 0.00/0.04 b -> c, 0.00/0.04 a -> c | b == c ] 0.00/0.04 Check whether all rules are type 3 0.00/0.04 OK 0.00/0.04 Check whether the input is deterministic 0.00/0.04 OK 0.00/0.04 Result of unraveling: 0.00/0.04 [ f(b) -> f(a), 0.00/0.04 b -> c, 0.00/0.04 a -> U0(b), 0.00/0.04 U0(c) -> c ] 0.00/0.04 Check whether U(R) is terminating 0.00/0.04 OK 0.00/0.04 Check whether the input is weakly left-linear 0.00/0.04 OK 0.00/0.04 Check whether U(R) is confluent 0.00/0.04 OK 0.00/0.04 R is deterministic, weakly left-linear and U(R) is confluent 0.00/0.04 /export/starexec/sandbox/benchmark/theBenchmark.trs: Success(CR) 0.00/0.04 (8 msec.) 0.00/0.04 EOF