0.00/0.02 YES 0.00/0.02 (ignored inputs)COMMENT [75] Example 33 submitted by: Thomas Sternagel and Aart Middeldorp 0.00/0.02 Conditional Rewrite Rules: 0.00/0.02 [ f(?x) -> ?x | ?x == a, 0.00/0.02 g(?x) -> C | A == B, 0.00/0.02 A -> B ] 0.00/0.02 Check whether all rules are type 3 0.00/0.02 OK 0.00/0.02 Check whether the input is deterministic 0.00/0.02 OK 0.00/0.02 Result of unraveling: 0.00/0.02 [ f(?x) -> U0(?x,?x), 0.00/0.02 U0(a,?x) -> ?x, 0.00/0.02 g(?x) -> U1(A,?x), 0.00/0.02 U1(B,?x) -> C, 0.00/0.02 A -> B ] 0.00/0.02 Check whether U(R) is terminating 0.00/0.02 OK 0.00/0.02 Check whether the input is weakly left-linear 0.00/0.02 OK 0.00/0.02 Check whether U(R) is confluent 0.00/0.02 OK 0.00/0.02 R is deterministic, weakly left-linear and U(R) is confluent 0.00/0.02 /export/starexec/sandbox/benchmark/theBenchmark.trs: Success(CR) 0.00/0.02 (0 msec.) 0.00/0.02 EOF