0.00/0.02 YES 0.00/0.02 (ignored inputs)COMMENT doi:10.1016/0022-0000 ( 86 ) 90033-4 [47] Example 2.6.2 submitted by: Thomas Sternagel and Aart Middeldorp 0.00/0.02 Conditional Rewrite Rules: 0.00/0.02 [ p(q(?x)) -> 0, 0.00/0.02 c -> c, 0.00/0.02 a(?x) -> b | p(?x) == 0 ] 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 [ p(q(?x)) -> 0, 0.00/0.02 c -> c, 0.00/0.02 a(?x) -> U0(p(?x),?x), 0.00/0.02 U0(0,?x) -> b ] 0.00/0.02 Check whether U(R) is terminating 0.00/0.02 failed to show termination 0.00/0.02 Check whether the input is weakly left-linear 0.00/0.02 OK 0.00/0.02 Conditional critical pairs (CCPs): 0.00/0.02 [ ] 0.00/0.02 Check whether the input is almost orthogonale 0.00/0.02 OK 0.00/0.02 Check whether the input is properly oriented 0.00/0.02 OK 0.00/0.02 Check whether the input is right-stable 0.00/0.02 OK 0.00/0.02 R is almost orthogonal, properly oriented, right stable 0.00/0.02 /export/starexec/sandbox/benchmark/theBenchmark.trs: Success(CR) 0.00/0.02 (0 msec.) 0.00/0.02 EOF