0.00/0.13 NO 0.00/0.13 (ignored inputs)COMMENT doi:10.1016/j.tcs.2012.09.005 [72] Example 10 ( R'_ssp ) submitted by: Thomas Sternagel and Aart Middeldorp 0.00/0.13 Conditional Rewrite Rules: 0.00/0.13 [ ssp'(?xs,0) -> nil, 0.00/0.13 ssp'(cons(?y',?ws),?v) -> cons(?y',?ys') | sub(?v,?y') == ?w,ssp'(?ws,?w) == ?ys', 0.00/0.13 ssp'(cons(?x',?xs'),?v) -> cons(?y',?ys') | get(?xs') == tp2(?y',?zs),sub(?v,?y') == ?w,ssp'(cons(?x',?zs),?w) == ?ys', 0.00/0.13 sub(?z,0) -> ?z, 0.00/0.13 sub(s(?v),s(?w)) -> ?z | sub(?v,?w) == ?z, 0.00/0.13 get(cons(?y,?ys)) -> tp2(?y,?ys), 0.00/0.13 get(cons(?x',?xs')) -> tp2(?y,cons(?x',?zs)) | get(?xs') == tp2(?y,?zs) ] 0.00/0.13 Check whether all rules are type 3 0.00/0.13 OK 0.00/0.13 Check whether the input is deterministic 0.00/0.13 OK 0.00/0.13 Result of unraveling: 0.00/0.13 [ ssp'(?xs,0) -> nil, 0.00/0.13 ssp'(cons(?y',?ws),?v) -> U0(sub(?v,?y'),?v,?y',?ws), 0.00/0.13 U0(?w,?v,?y',?ws) -> U1(ssp'(?ws,?w),?v,?y',?ws,?w), 0.00/0.13 U1(?ys',?v,?y',?ws,?w) -> cons(?y',?ys'), 0.00/0.13 ssp'(cons(?x',?xs'),?v) -> U2(get(?xs'),?v,?x',?xs'), 0.00/0.13 U2(tp2(?y',?zs),?v,?x',?xs') -> U3(sub(?v,?y'),?v,?x',?xs',?y',?zs), 0.00/0.13 U3(?w,?v,?x',?xs',?y',?zs) -> U4(ssp'(cons(?x',?zs),?w),?v,?x',?xs',?y',?zs,?w), 0.00/0.13 U4(?ys',?v,?x',?xs',?y',?zs,?w) -> cons(?y',?ys'), 0.00/0.13 sub(?z,0) -> ?z, 0.00/0.13 sub(s(?v),s(?w)) -> U5(sub(?v,?w),?v,?w), 0.00/0.13 U5(?z,?v,?w) -> ?z, 0.00/0.13 get(cons(?y,?ys)) -> tp2(?y,?ys), 0.00/0.13 get(cons(?x',?xs')) -> U6(get(?xs'),?x',?xs'), 0.00/0.13 U6(tp2(?y,?zs),?x',?xs') -> tp2(?y,cons(?x',?zs)) ] 0.00/0.13 Check whether U(R) is terminating 0.00/0.13 OK 0.00/0.13 Check whether the input is weakly left-linear 0.00/0.13 OK 0.00/0.13 Check whether U(R) is confluent 0.00/0.13 U(R) is not confluent 0.00/0.13 Conditional critical pairs (CCPs): 0.00/0.13 [ cons(?y'_1,?ys'_1) = nil | sub(0,?y'_1) == ?w_1,ssp'(?ws_1,?w_1) == ?ys'_1, 0.00/0.13 cons(?y'_2,?ys'_2) = nil | get(?xs'_2) == tp2(?y'_2,?zs_2),sub(0,?y'_2) == ?w_2,ssp'(cons(?x'_2,?zs_2),?w_2) == ?ys'_2, 0.00/0.13 nil = cons(?y'_1,?ys'_1) | sub(0,?y'_1) == ?w_1,ssp'(?ws_1,?w_1) == ?ys'_1, 0.00/0.13 cons(?y'_2,?ys'_2) = cons(?x'_2,?ys'_1) | get(?xs'_2) == tp2(?y'_2,?zs_2),sub(?v_2,?y'_2) == ?w_2,ssp'(cons(?x'_2,?zs_2),?w_2) == ?ys'_2,sub(?v_2,?x'_2) == ?w_1,ssp'(?xs'_2,?w_1) == ?ys'_1, 0.00/0.13 nil = cons(?y'_2,?ys'_2) | get(?xs'_2) == tp2(?y'_2,?zs_2),sub(0,?y'_2) == ?w_2,ssp'(cons(?x'_2,?zs_2),?w_2) == ?ys'_2, 0.00/0.13 cons(?y'_1,?ys'_1) = cons(?y'_2,?ys'_2) | sub(?v_1,?y'_1) == ?w_1,ssp'(?ws_1,?w_1) == ?ys'_1,get(?ws_1) == tp2(?y'_2,?zs_2),sub(?v_1,?y'_2) == ?w_2,ssp'(cons(?y'_1,?zs_2),?w_2) == ?ys'_2, 0.00/0.13 tp2(?y_6,cons(?x'_6,?zs_6)) = tp2(?x'_6,?xs'_6) | get(?xs'_6) == tp2(?y_6,?zs_6), 0.00/0.13 tp2(?y_5,?ys_5) = tp2(?y_6,cons(?y_5,?zs_6)) | get(?ys_5) == tp2(?y_6,?zs_6) ] 0.00/0.13 Check whether the input is almost orthogonale 0.00/0.13 not almost orthogonal 0.00/0.13 OK 0.00/0.13 Check whether the input is absolutely irreducible 0.00/0.13 OK 0.00/0.13 Check whether all CCPs are joinable 0.00/0.13 Some ccp may be feasible but not joinable 0.00/0.13 [ cons(?y'_1,?ys'_1) = nil | sub(0,?y'_1) == ?w_1,ssp'(?ws_1,?w_1) == ?ys'_1, 0.00/0.13 cons(?y'_2,?ys'_2) = nil | get(?xs'_2) == tp2(?y'_2,?zs_2),sub(0,?y'_2) == ?w_2,ssp'(cons(?x'_2,?zs_2),?w_2) == ?ys'_2, 0.00/0.13 nil = cons(?y'_1,?ys'_1) | sub(0,?y'_1) == ?w_1,ssp'(?ws_1,?w_1) == ?ys'_1, 0.00/0.13 cons(?y'_2,?ys'_2) = cons(?x'_2,?ys'_1) | get(?xs'_2) == tp2(?y'_2,?zs_2),sub(?v_2,?y'_2) == ?w_2,ssp'(cons(?x'_2,?zs_2),?w_2) == ?ys'_2,sub(?v_2,?x'_2) == ?w_1,ssp'(?xs'_2,?w_1) == ?ys'_1, 0.00/0.13 nil = cons(?y'_2,?ys'_2) | get(?xs'_2) == tp2(?y'_2,?zs_2),sub(0,?y'_2) == ?w_2,ssp'(cons(?x'_2,?zs_2),?w_2) == ?ys'_2, 0.00/0.13 cons(?y'_1,?ys'_1) = cons(?y'_2,?ys'_2) | sub(?v_1,?y'_1) == ?w_1,ssp'(?ws_1,?w_1) == ?ys'_1,get(?ws_1) == tp2(?y'_2,?zs_2),sub(?v_1,?y'_2) == ?w_2,ssp'(cons(?y'_1,?zs_2),?w_2) == ?ys'_2, 0.00/0.13 tp2(?y_6,cons(?x'_6,?zs_6)) = tp2(?x'_6,?xs'_6) | get(?xs'_6) == tp2(?y_6,?zs_6), 0.00/0.13 tp2(?y_5,?ys_5) = tp2(?y_6,cons(?y_5,?zs_6)) | get(?ys_5) == tp2(?y_6,?zs_6) ] 0.00/0.13 A non-joinable pair: cons(?y'_1,ssp'(?ws_1,sub(0,?y'_1))) <-*- o -*-> nil 0.00/0.13 instanciated and reduced from cons(?y'_1,?ys'_1) = nil | sub(0,?y'_1) == ?w_1,ssp'(?ws_1,?w_1) == ?ys'_1 0.00/0.13 /export/starexec/sandbox/benchmark/theBenchmark.trs: Success(not CR) 0.00/0.13 (52 msec.) 0.00/0.13 EOF