0.00/0.04 MAYBE 0.00/0.04 (ignored inputs)COMMENT [121] Example 9.6; adaptation of Cops #292 submitted by: Thomas Sternagel 0.00/0.04 Conditional Rewrite Rules: 0.00/0.04 [ le(?x,0) -> false, 0.00/0.04 le(0,s(?y)) -> true, 0.00/0.04 le(s(?x),s(?y)) -> le(?x,?y), 0.00/0.04 min(cons(?x,nil)) -> ?x, 0.00/0.04 min(cons(?x,?xs)) -> ?x | min(?xs) == ?y,le(?x,?y) == true, 0.00/0.04 min(cons(?x,?xs)) -> ?y | min(?xs) == ?y,le(?x,?y) == false ] 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 [ le(?x,0) -> false, 0.00/0.04 le(0,s(?y)) -> true, 0.00/0.04 le(s(?x),s(?y)) -> le(?x,?y), 0.00/0.04 min(cons(?x,nil)) -> ?x, 0.00/0.04 min(cons(?x,?xs)) -> U2(min(?xs),?x,?xs), 0.00/0.04 U2(?y,?x,?xs) -> U3(le(?x,?y),?x,?xs,?y), 0.00/0.04 U3(true,?x,?xs,?y) -> ?x, 0.00/0.04 U3(false,?x,?xs,?y) -> ?y ] 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 U(R) is not confluent 0.00/0.04 Conditional critical pairs (CCPs): 0.00/0.04 [ ?x_4 = ?x_4 | min(nil) == ?y_4,le(?x_4,?y_4) == true, 0.00/0.04 ?y_5 = ?x_5 | min(nil) == ?y_5,le(?x_5,?y_5) == false, 0.00/0.04 ?x_3 = ?x_3 | min(nil) == ?y_4,le(?x_3,?y_4) == true, 0.00/0.04 ?y_5 = ?x_5 | min(?xs_5) == ?y_5,le(?x_5,?y_5) == false,min(?xs_5) == ?y_4,le(?x_5,?y_4) == true, 0.00/0.04 ?x_3 = ?y_5 | min(nil) == ?y_5,le(?x_3,?y_5) == false, 0.00/0.04 ?x_4 = ?y_5 | min(?xs_4) == ?y_4,le(?x_4,?y_4) == true,min(?xs_4) == ?y_5,le(?x_4,?y_5) == false ] 0.00/0.04 Check whether the input is almost orthogonale 0.00/0.04 not almost orthogonal 0.00/0.04 OK 0.00/0.04 Check whether the input is absolutely irreducible 0.00/0.04 OK 0.00/0.04 Check whether all CCPs are joinable 0.00/0.04 Some ccp may be feasible but not joinable 0.00/0.04 [ ?y_5 = ?x_5 | min(nil) == ?y_5,le(?x_5,?y_5) == false, 0.00/0.04 ?y_5 = ?x_5 | min(?xs_5) == ?y_5,le(?x_5,?y_5) == false,min(?xs_5) == ?y_4,le(?x_5,?y_4) == true, 0.00/0.04 ?x_3 = ?y_5 | min(nil) == ?y_5,le(?x_3,?y_5) == false, 0.00/0.04 ?x_4 = ?y_5 | min(?xs_4) == ?y_4,le(?x_4,?y_4) == true,min(?xs_4) == ?y_5,le(?x_4,?y_5) == false ] 0.00/0.04 /export/starexec/sandbox/benchmark/theBenchmark.trs: Failure(unknown CR) 0.00/0.04 (8 msec.) 0.00/0.04 EOF