0.00/0.00 YES 0.00/0.00 0.00/0.00 Succeeded in reading "/export/starexec/sandbox2/benchmark/theBenchmark.trs". 0.00/0.00 (CONDITIONTYPE ORIENTED) 0.00/0.00 (VAR x y x2 x1) 0.00/0.00 (RULES 0.00/0.00 pin(a) -> pout(b) 0.00/0.00 pin(b) -> pout(c) 0.00/0.00 tc(x) -> x 0.00/0.00 tc(x) -> y | pin(x) == pout(z), tc(z) == y 0.00/0.00 ) 0.00/0.00 (COMMENT COPS 288) 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 x2 x1) 0.00/0.00 (RULES 0.00/0.00 pin(a) -> pout(b) 0.00/0.00 pin(b) -> pout(c) 0.00/0.00 tc(x) -> x 0.00/0.00 tc(x) -> y | pin(x) == pout(z), tc(z) == y 0.00/0.00 ) 0.00/0.00 (COMMENT COPS 288) 0.00/0.00 (COMMENT submitted by: Naoki Nishida) 0.00/0.00 0.00/0.00 (VAR x2 x1) 0.00/0.00 (CONDITION 0.00/0.00 pin(x1) == pout(z), tc(z) == x2 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) 0.00/0.00 (CONDITION 0.00/0.00 pin(x1) == pout(z), tc(z) == x2 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 not operationally terminating and confluent. 0.00/0.00 0.00/0.00 This is a constructor-based system. 0.00/0.00 0.00/0.00 (RTG_of_NARROWINGTREE 0.00/0.00 (START 0.00/0.00 Gamma[pin(x1) == pout(z) : { e, 1 } & tc(z) == x2 : { e, 1, 1.1 }] 0.00/0.00 ) 0.00/0.00 (NONTERMINALS 0.00/0.00 Gamma[pin(x1) == pout(z) : { e, 1 } & tc(z) == x2 : { e, 1, 1.1 }] 0.00/0.00 Gamma[pin(x37) == pout(z) : { e, 1 }] 0.00/0.00 Gamma[tc(z2) == x43 : { e, 1 }] 0.00/0.00 ) 0.00/0.00 (RULES 0.00/0.00 Gamma[pin(x1) == pout(z) : { e, 1 } & tc(z) == x2 : { e, 1, 1.1 }] -> EmptySet 0.00/0.00 Gamma[tc(z2) == x43 : { e, 1 }] -> { x43 -> tc(z2) } 0.00/0.00 Gamma[tc(z2) == x43 : { e, 1 }] -> { x49 -> x51, x43 -> x51, z2 -> x51 } 0.00/0.00 Gamma[tc(z2) == x43 : { e, 1 }] -> ((Rec(Gamma[pin(x37) == pout(z) : { e, 1 }], { x50 -> x37 }) & ({ z3 -> z, y5 -> x59, x43 -> x59 } & Rec(Gamma[tc(z2) == x43 : { e, 1 }], { y5 -> x43, z3 -> z2 }))) . { z2 -> x50 }) 0.00/0.00 ) 0.00/0.00 ) 0.00/0.00 0.00/0.00 YES 0.00/0.00 EOF