0.00/0.00 MAYBE 0.00/0.00 0.00/0.00 Succeeded in reading "/export/starexec/sandbox/benchmark/theBenchmark.trs". 0.00/0.00 (CONDITIONTYPE ORIENTED) 0.00/0.00 (VAR x y ys x2 x1) 0.00/0.00 (RULES 0.00/0.00 lt(x,0) -> false 0.00/0.00 lt(0,s(y)) -> true 0.00/0.00 lt(s(x),s(y)) -> lt(x,y) 0.00/0.00 cons(x,cons(y,ys)) -> cons(y,cons(x,ys)) | lt(x,y) == true 0.00/0.00 ) 0.00/0.00 (COMMENT COPS 337) 0.00/0.00 (COMMENT submitted by: Naoki Nishida) 0.00/0.00 0.00/0.00 No "->="-rules. 0.00/0.00 0.00/0.00 Decomposed conditions and removed infeasible rules if possible. 0.00/0.00 (CONDITIONTYPE ORIENTED) 0.00/0.00 (VAR x y ys x2 x1) 0.00/0.00 (RULES 0.00/0.00 lt(x,0) -> false 0.00/0.00 lt(0,s(y)) -> true 0.00/0.00 lt(s(x),s(y)) -> lt(x,y) 0.00/0.00 cons(x,cons(y,ys)) -> cons(y,cons(x,ys)) | lt(x,y) == true 0.00/0.00 ) 0.00/0.00 (COMMENT COPS 337) 0.00/0.00 (COMMENT submitted by: Naoki Nishida) 0.00/0.00 0.00/0.00 (VAR x2 x1 x) 0.00/0.00 (CONDITION 0.00/0.00 lt(x,x1) == true, lt(x1,x2) == true 0.00/0.00 ) 0.00/0.00 0.00/0.00 Optimized the infeasibility problem if possible. 0.00/0.00 0.00/0.00 (VAR x2 x1 x) 0.00/0.00 (CONDITION 0.00/0.00 lt(x,x1) == true, lt(x1,x2) == true 0.00/0.00 ) 0.00/0.00 0.00/0.00 This is not ultra-RL and deterministic. 0.00/0.00 0.00/0.00 The inverted system is ultra-RL and deterministic. 0.00/0.00 0.00/0.00 0.00/0.00 MAYBE 0.00/0.00 EOF