0.00/0.04	NO
0.00/0.04	(ignored inputs)COMMENT doi:10.1016/j.tcs.2012.09.005 [72] Example 9 ( R_ssp ) submitted by: Thomas Sternagel and Aart Middeldorp
0.00/0.04	Conditional Rewrite Rules:
0.00/0.04	   [ ssp(nil,0) -> nil,
0.00/0.04	     ssp(cons(?y,?ys'),?v) -> ?xs | ssp(?ys',?v) == ?xs,
0.00/0.04	     ssp(cons(?y,?ys'),?v) -> cons(?y,?xs') | sub(?v,?y) == ?w,ssp(?ys',?w) == ?xs',
0.00/0.04	     sub(?z,0) -> ?z,
0.00/0.04	     sub(s(?v),s(?w)) -> ?z | sub(?v,?w) == ?z ]
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	   [ ssp(nil,0) -> nil,
0.00/0.04	     ssp(cons(?y,?ys'),?v) -> U1(ssp(?ys',?v),?v,?y,?ys'),
0.00/0.04	     U1(?xs,?v,?y,?ys') -> ?xs,
0.00/0.04	     ssp(cons(?y,?ys'),?v) -> U1(sub(?v,?y),?v,?y,?ys'),
0.00/0.04	     U1(?w,?v,?y,?ys') -> U2(ssp(?ys',?w),?v,?y,?ys',?w),
0.00/0.04	     U2(?xs',?v,?y,?ys',?w) -> cons(?y,?xs'),
0.00/0.04	     sub(?z,0) -> ?z,
0.00/0.04	     sub(s(?v),s(?w)) -> U3(sub(?v,?w),?v,?w),
0.00/0.04	     U3(?z,?v,?w) -> ?z ]
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	   [ cons(?y_1,?xs'_1) = ?xs | sub(?v_1,?y_1) == ?w_1,ssp(?ys'_1,?w_1) == ?xs'_1,ssp(?ys'_1,?v_1) == ?xs,
0.00/0.04	     ?xs = cons(?y,?xs'_1) | ssp(?ys',?v) == ?xs,sub(?v,?y) == ?w_1,ssp(?ys',?w_1) == ?xs'_1 ]
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	   [ cons(?y_1,?xs'_1) = ?xs | sub(?v_1,?y_1) == ?w_1,ssp(?ys'_1,?w_1) == ?xs'_1,ssp(?ys'_1,?v_1) == ?xs,
0.00/0.04	     ?xs = cons(?y,?xs'_1) | ssp(?ys',?v) == ?xs,sub(?v,?y) == ?w_1,ssp(?ys',?w_1) == ?xs'_1 ]
0.00/0.04	A non-joinable pair: cons(?y_1,ssp(?ys'_1,sub(?v_1,?y_1))) <-*- o -*-> ssp(?ys'_1,?v_1)
0.00/0.04	instanciated and reduced from cons(?y_1,?xs'_1) = ?xs | sub(?v_1,?y_1) == ?w_1,ssp(?ys'_1,?w_1) == ?xs'_1,ssp(?ys'_1,?v_1) == ?xs
0.00/0.04	/export/starexec/sandbox/benchmark/theBenchmark.trs: Success(not CR)
0.00/0.04	(8 msec.)
0.00/0.04	EOF