0.00/0.01 YES 0.00/0.01 0.00/0.01 Succeeded in reading "/export/starexec/sandbox2/benchmark/theBenchmark.trs". 0.00/0.01 (CONDITIONTYPE ORIENTED) 0.00/0.01 (VAR x) 0.00/0.01 (RULES 0.00/0.01 s(p(x)) -> x 0.00/0.01 p(s(x)) -> x 0.00/0.01 pos(0) -> false 0.00/0.01 pos(s(0)) -> true 0.00/0.01 pos(s(x)) -> true | pos(x) == true 0.00/0.01 pos(p(x)) -> false | pos(x) == false 0.00/0.01 ) 0.00/0.01 (COMMENT COPS 365) 0.00/0.01 (COMMENT submitted by: Naoki Nishida) 0.00/0.01 0.00/0.01 No "->="-rules. 0.00/0.01 0.00/0.01 Decomposed conditions and removed infeasible rules if possible. 0.00/0.01 (CONDITIONTYPE ORIENTED) 0.00/0.01 (VAR x) 0.00/0.01 (RULES 0.00/0.01 s(p(x)) -> x 0.00/0.01 p(s(x)) -> x 0.00/0.01 pos(0) -> false 0.00/0.01 pos(s(0)) -> true 0.00/0.01 pos(s(x)) -> true | pos(x) == true 0.00/0.01 pos(p(x)) -> false | pos(x) == false 0.00/0.01 ) 0.00/0.01 (COMMENT COPS 365) 0.00/0.01 (COMMENT submitted by: Naoki Nishida) 0.00/0.01 0.00/0.01 (CONDITION 0.00/0.01 pos(0) == true 0.00/0.01 ) 0.00/0.01 0.00/0.01 Optimized the infeasibility problem if possible. 0.00/0.01 0.00/0.01 (CONDITION 0.00/0.01 pos(0) == true 0.00/0.01 ) 0.00/0.01 0.00/0.01 This is ultra-RL and deterministic. 0.00/0.01 0.00/0.01 This is not operationally terminating and confluent. 0.00/0.01 0.00/0.01 (RTG_of_NARROWINGTREE 0.00/0.01 (START 0.00/0.01 Gamma[pos(0) == true : { e, 1, 1.1 }] 0.00/0.01 ) 0.00/0.01 (NONTERMINALS 0.00/0.01 Gamma[pos(0) == true : { e, 1, 1.1 }] 0.00/0.01 ) 0.00/0.01 (RULES 0.00/0.01 Gamma[pos(0) == true : { e, 1, 1.1 }] -> EmptySet 0.00/0.01 ) 0.00/0.01 ) 0.00/0.01 0.00/0.01 YES 0.00/0.01 EOF