0.00/0.03 YES 0.00/0.03 (ignored inputs)COMMENT doi:10.1017/CBO9781139172752 [4] p. 209 submitted by: Thomas Sternagel and Aart Middeldorp 0.00/0.03 Conditional Rewrite Rules: 0.00/0.03 [ pos(s(0)) -> true, 0.00/0.03 pos(0) -> false, 0.00/0.03 pos(s(?x)) -> true | pos(?x) == true, 0.00/0.03 pos(p(?x)) -> false | pos(?x) == false ] 0.00/0.03 Check whether all rules are type 3 0.00/0.03 OK 0.00/0.03 Check whether the input is deterministic 0.00/0.03 OK 0.00/0.03 Result of unraveling: 0.00/0.03 [ pos(s(0)) -> true, 0.00/0.03 pos(0) -> false, 0.00/0.03 pos(s(?x)) -> U0(pos(?x),?x), 0.00/0.03 U0(true,?x) -> true, 0.00/0.03 pos(p(?x)) -> U1(pos(?x),?x), 0.00/0.03 U1(false,?x) -> false ] 0.00/0.03 Check whether U(R) is terminating 0.00/0.03 OK 0.00/0.03 Check whether the input is weakly left-linear 0.00/0.03 OK 0.00/0.03 Check whether U(R) is confluent 0.00/0.03 U(R) is not confluent 0.00/0.03 Conditional critical pairs (CCPs): 0.00/0.03 [ true = true | pos(0) == true, 0.00/0.03 true = true | pos(0) == true ] 0.00/0.03 Check whether the input is almost orthogonale 0.00/0.03 OK 0.00/0.03 Check whether the input is properly oriented 0.00/0.03 OK 0.00/0.03 Check whether the input is right-stable 0.00/0.03 OK 0.00/0.03 R is almost orthogonal, properly oriented, right stable 0.00/0.03 /export/starexec/sandbox/benchmark/theBenchmark.trs: Success(CR) 0.00/0.03 (4 msec.) 0.00/0.03 EOF