0.00/0.00 YES 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 x1) 0.00/0.00 (RULES 0.00/0.00 e(0) -> true 0.00/0.00 e(s(x)) -> true | o(x) == true 0.00/0.00 e(s(x)) -> false | e(x) == true 0.00/0.00 o(0) -> false 0.00/0.00 o(s(x)) -> true | e(x) == true 0.00/0.00 o(s(x)) -> false | o(x) == true 0.00/0.00 ) 0.00/0.00 (COMMENT COPS 522) 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 (CONDITION 0.00/0.00 e(x1) == true, o(x1) == true 0.00/0.00 ) 0.00/0.00 0.00/0.00 This is ultra-RL and deterministic. 0.00/0.00 0.00/0.00 This is operationally terminating and confluent. 0.00/0.00 0.00/0.00 (RTG_of_NARROWINGTREE 0.00/0.00 (START 0.00/0.00 Gamma[e(x1) == true : { e, 1 } & o(x1) == true : { e, 1 }] 0.00/0.00 ) 0.00/0.00 (NONTERMINALS 0.00/0.00 Gamma[e(x1) == true : { e, 1 } & o(x1) == true : { e, 1 }] 0.00/0.00 Gamma[e(x344) == true : { e, 1 }] 0.00/0.00 Gamma[o(x349) == true : { e, 1 }] 0.00/0.00 ) 0.00/0.00 (RULES 0.00/0.00 Gamma[e(x1) == true : { e, 1 } & o(x1) == true : { e, 1 }] -> EmptySet 0.00/0.00 Gamma[e(x344) == true : { e, 1 }] -> { x344 -> 0 } 0.00/0.00 Gamma[e(x344) == true : { e, 1 }] -> (Rec(Gamma[o(x349) == true : { e, 1 }], { x350 -> x349 }) . { x344 -> s(x350) }) 0.00/0.00 Gamma[o(x349) == true : { e, 1 }] -> (Rec(Gamma[e(x344) == true : { e, 1 }], { x364 -> x344 }) . { x349 -> s(x364) }) 0.00/0.00 ) 0.00/0.00 ) 0.00/0.00 0.00/0.00 YES 0.00/0.00 EOF