0.00/0.03 MAYBE 0.00/0.03 (ignored inputs)COMMENT [79] Example 8; correction of Cops #404 submitted by: Thomas Sternagel 0.00/0.03 Conditional Rewrite Rules: 0.00/0.03 [ e(0) -> true, 0.00/0.03 e(s(?x)) -> true | o(?x) == true, 0.00/0.03 e(s(?x)) -> false | e(?x) == true, 0.00/0.03 o(0) -> false, 0.00/0.03 o(s(?x)) -> true | e(?x) == true, 0.00/0.03 o(s(?x)) -> false | o(?x) == true ] 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 [ e(0) -> true, 0.00/0.03 e(s(?x)) -> U1(o(?x),?x), 0.00/0.03 U1(true,?x) -> true, 0.00/0.03 e(s(?x)) -> U1(e(?x),?x), 0.00/0.03 U1(true,?x) -> false, 0.00/0.03 o(0) -> false, 0.00/0.03 o(s(?x)) -> U3(e(?x),?x), 0.00/0.03 U3(true,?x) -> true, 0.00/0.03 o(s(?x)) -> U3(o(?x),?x), 0.00/0.03 U3(true,?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 [ false = true | e(?x_1) == true,o(?x_1) == true, 0.00/0.03 true = false | o(?x) == true,e(?x) == true, 0.00/0.03 false = true | o(?x_3) == true,e(?x_3) == true, 0.00/0.03 true = false | e(?x_2) == true,o(?x_2) == true ] 0.00/0.03 Check whether the input is almost orthogonale 0.00/0.03 not almost orthogonal 0.00/0.03 OK 0.00/0.03 Check whether the input is absolutely irreducible 0.00/0.03 OK 0.00/0.03 Check whether all CCPs are joinable 0.00/0.03 Some ccp may be feasible but not joinable 0.00/0.03 [ false = true | e(?x_1) == true,o(?x_1) == true, 0.00/0.03 true = false | o(?x) == true,e(?x) == true, 0.00/0.03 false = true | o(?x_3) == true,e(?x_3) == true, 0.00/0.03 true = false | e(?x_2) == true,o(?x_2) == true ] 0.00/0.03 /export/starexec/sandbox2/benchmark/theBenchmark.trs: Failure(unknown CR) 0.00/0.03 (4 msec.) 0.00/0.03 EOF