0.00/0.02 MAYBE 0.00/0.02 (ignored inputs)COMMENT doi:10.1016/j.tcs.2012.09.005 [72] Example 10 submitted by: Thomas Sternagel and Aart Middeldorp 0.00/0.02 Conditional Rewrite Rules: 0.00/0.02 [ ssp'(?xs,?v) -> ?ys | subseteq_m(?ys,?xs) == tt,sum(?ys) == ?v, 0.00/0.02 subseteq_m(nil,?ys) -> tt, 0.00/0.02 subseteq_m(cons(?x,?xs),?ys) -> ?z | del(?x,?ys) == some(?ws),subseteq_m(?xs,?ws) == ?z, 0.00/0.02 del(?x,nil) -> none, 0.00/0.02 del(?x,cons(?x,?ys)) -> some(?ys), 0.00/0.02 del(?x,cons(?y,?ys)) -> some(cons(?y,?zs)) | del(?x,?ys) == some(?zs), 0.00/0.02 sum(nil) -> 0, 0.00/0.02 add(?x,0) -> ?x, 0.00/0.02 add(?x,s(?y)) -> s(?z) | add(?x,?y) == ?z ] 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 No. non-deterministic rule: ssp'(?xs,?v) -> ?ys | subseteq_m(?ys,?xs) == tt,sum(?ys) == ?v 0.00/0.02 Conditional critical pairs (CCPs): 0.00/0.02 [ some(cons(?y_5,?zs_5)) = some(?ys_5) | del(?y_5,?ys_5) == some(?zs_5), 0.00/0.02 some(?ys_4) = some(cons(?x_4,?zs_5)) | del(?x_4,?ys_4) == some(?zs_5) ] 0.00/0.02 Check whether the input is almost orthogonale 0.00/0.02 not almost orthogonal 0.00/0.02 /export/starexec/sandbox/benchmark/theBenchmark.trs: Failure(unknown CR) 0.00/0.02 (0 msec.) 0.00/0.03 EOF