YES Time: 0.106743 TRS: { +(p2(), +(p2(), p2())) -> +(p1(), p5()), +(p2(), +(p2(), +(p2(), x))) -> +(p1(), +(p5(), x)), +(p2(), +(p1(), x)) -> +(p1(), +(p2(), x)), +(p2(), p1()) -> +(p1(), p2()), +(+(x, y), z) -> +(x, +(y, z)), +(p1(), +(p2(), p2())) -> p5(), +(p1(), +(p2(), +(p2(), x))) -> +(p5(), x), +(p1(), +(p1(), x)) -> +(p2(), x), +(p1(), p1()) -> p2(), +(p5(), p2()) -> +(p2(), p5()), +(p5(), +(p2(), x)) -> +(p2(), +(p5(), x)), +(p5(), +(p1(), x)) -> +(p1(), +(p5(), x)), +(p5(), +(p5(), x)) -> +(p10(), x), +(p5(), p1()) -> +(p1(), p5()), +(p5(), p5()) -> p10(), +(p10(), p2()) -> +(p2(), p10()), +(p10(), +(p2(), x)) -> +(p2(), +(p10(), x)), +(p10(), +(p1(), x)) -> +(p1(), +(p10(), x)), +(p10(), +(p5(), x)) -> +(p5(), +(p10(), x)), +(p10(), p1()) -> +(p1(), p10()), +(p10(), p5()) -> +(p5(), p10())} DP: DP: { +#(p2(), +(p2(), p2())) -> +#(p1(), p5()), +#(p2(), +(p2(), +(p2(), x))) -> +#(p1(), +(p5(), x)), +#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p2(), +(p1(), x)) -> +#(p2(), x), +#(p2(), +(p1(), x)) -> +#(p1(), +(p2(), x)), +#(p2(), p1()) -> +#(p1(), p2()), +#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z), +#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p1(), +(p1(), x)) -> +#(p2(), x), +#(p5(), p2()) -> +#(p2(), p5()), +#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x)), +#(p5(), +(p2(), x)) -> +#(p5(), x), +#(p5(), +(p1(), x)) -> +#(p1(), +(p5(), x)), +#(p5(), +(p1(), x)) -> +#(p5(), x), +#(p5(), +(p5(), x)) -> +#(p10(), x), +#(p5(), p1()) -> +#(p1(), p5()), +#(p10(), p2()) -> +#(p2(), p10()), +#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x)), +#(p10(), +(p2(), x)) -> +#(p10(), x), +#(p10(), +(p1(), x)) -> +#(p1(), +(p10(), x)), +#(p10(), +(p1(), x)) -> +#(p10(), x), +#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x)), +#(p10(), +(p5(), x)) -> +#(p10(), x), +#(p10(), p1()) -> +#(p1(), p10()), +#(p10(), p5()) -> +#(p5(), p10())} TRS: { +(p2(), +(p2(), p2())) -> +(p1(), p5()), +(p2(), +(p2(), +(p2(), x))) -> +(p1(), +(p5(), x)), +(p2(), +(p1(), x)) -> +(p1(), +(p2(), x)), +(p2(), p1()) -> +(p1(), p2()), +(+(x, y), z) -> +(x, +(y, z)), +(p1(), +(p2(), p2())) -> p5(), +(p1(), +(p2(), +(p2(), x))) -> +(p5(), x), +(p1(), +(p1(), x)) -> +(p2(), x), +(p1(), p1()) -> p2(), +(p5(), p2()) -> +(p2(), p5()), +(p5(), +(p2(), x)) -> +(p2(), +(p5(), x)), +(p5(), +(p1(), x)) -> +(p1(), +(p5(), x)), +(p5(), +(p5(), x)) -> +(p10(), x), +(p5(), p1()) -> +(p1(), p5()), +(p5(), p5()) -> p10(), +(p10(), p2()) -> +(p2(), p10()), +(p10(), +(p2(), x)) -> +(p2(), +(p10(), x)), +(p10(), +(p1(), x)) -> +(p1(), +(p10(), x)), +(p10(), +(p5(), x)) -> +(p5(), +(p10(), x)), +(p10(), p1()) -> +(p1(), p10()), +(p10(), p5()) -> +(p5(), p10())} UR: { +(p2(), +(p2(), p2())) -> +(p1(), p5()), +(p2(), +(p2(), +(p2(), x))) -> +(p1(), +(p5(), x)), +(p2(), +(p1(), x)) -> +(p1(), +(p2(), x)), +(p2(), p1()) -> +(p1(), p2()), +(+(x, y), z) -> +(x, +(y, z)), +(p1(), +(p2(), p2())) -> p5(), +(p1(), +(p2(), +(p2(), x))) -> +(p5(), x), +(p1(), +(p1(), x)) -> +(p2(), x), +(p1(), p1()) -> p2(), +(p5(), p2()) -> +(p2(), p5()), +(p5(), +(p2(), x)) -> +(p2(), +(p5(), x)), +(p5(), +(p1(), x)) -> +(p1(), +(p5(), x)), +(p5(), +(p5(), x)) -> +(p10(), x), +(p5(), p1()) -> +(p1(), p5()), +(p5(), p5()) -> p10(), +(p10(), p2()) -> +(p2(), p10()), +(p10(), +(p2(), x)) -> +(p2(), +(p10(), x)), +(p10(), +(p1(), x)) -> +(p1(), +(p10(), x)), +(p10(), +(p5(), x)) -> +(p5(), +(p10(), x)), +(p10(), p1()) -> +(p1(), p10()), +(p10(), p5()) -> +(p5(), p10())} EDG: { (+#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), p1()) -> +#(p1(), p5())) (+#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), +(p5(), x)) -> +#(p10(), x)) (+#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), +(p1(), x)) -> +#(p5(), x)) (+#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), +(p1(), x)) -> +#(p1(), +(p5(), x))) (+#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), +(p2(), x)) -> +#(p5(), x)) (+#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x))) (+#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), p2()) -> +#(p2(), p5())) (+#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), p1()) -> +#(p1(), p5())) (+#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), +(p5(), x)) -> +#(p10(), x)) (+#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), +(p1(), x)) -> +#(p5(), x)) (+#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), +(p1(), x)) -> +#(p1(), +(p5(), x))) (+#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), +(p2(), x)) -> +#(p5(), x)) (+#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x))) (+#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), p2()) -> +#(p2(), p5())) (+#(p5(), +(p2(), x)) -> +#(p5(), x), +#(p5(), p1()) -> +#(p1(), p5())) (+#(p5(), +(p2(), x)) -> +#(p5(), x), +#(p5(), +(p5(), x)) -> +#(p10(), x)) (+#(p5(), +(p2(), x)) -> +#(p5(), x), +#(p5(), +(p1(), x)) -> +#(p5(), x)) (+#(p5(), +(p2(), x)) -> +#(p5(), x), +#(p5(), +(p1(), x)) -> +#(p1(), +(p5(), x))) (+#(p5(), +(p2(), x)) -> +#(p5(), x), +#(p5(), +(p2(), x)) -> +#(p5(), x)) (+#(p5(), +(p2(), x)) -> +#(p5(), x), +#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x))) (+#(p5(), +(p2(), x)) -> +#(p5(), x), +#(p5(), p2()) -> +#(p2(), p5())) (+#(p5(), +(p5(), x)) -> +#(p10(), x), +#(p10(), p5()) -> +#(p5(), p10())) (+#(p5(), +(p5(), x)) -> +#(p10(), x), +#(p10(), p1()) -> +#(p1(), p10())) (+#(p5(), +(p5(), x)) -> +#(p10(), x), +#(p10(), +(p5(), x)) -> +#(p10(), x)) (+#(p5(), +(p5(), x)) -> +#(p10(), x), +#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x))) (+#(p5(), +(p5(), x)) -> +#(p10(), x), +#(p10(), +(p1(), x)) -> +#(p10(), x)) (+#(p5(), +(p5(), x)) -> +#(p10(), x), +#(p10(), +(p1(), x)) -> +#(p1(), +(p10(), x))) (+#(p5(), +(p5(), x)) -> +#(p10(), x), +#(p10(), +(p2(), x)) -> +#(p10(), x)) (+#(p5(), +(p5(), x)) -> +#(p10(), x), +#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x))) (+#(p5(), +(p5(), x)) -> +#(p10(), x), +#(p10(), p2()) -> +#(p2(), p10())) (+#(p10(), +(p1(), x)) -> +#(p10(), x), +#(p10(), p5()) -> +#(p5(), p10())) (+#(p10(), +(p1(), x)) -> +#(p10(), x), +#(p10(), p1()) -> +#(p1(), p10())) (+#(p10(), +(p1(), x)) -> +#(p10(), x), +#(p10(), +(p5(), x)) -> +#(p10(), x)) (+#(p10(), +(p1(), x)) -> +#(p10(), x), +#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x))) (+#(p10(), +(p1(), x)) -> +#(p10(), x), +#(p10(), +(p1(), x)) -> +#(p10(), x)) (+#(p10(), +(p1(), x)) -> +#(p10(), x), +#(p10(), +(p1(), x)) -> +#(p1(), +(p10(), x))) (+#(p10(), +(p1(), x)) -> +#(p10(), x), +#(p10(), +(p2(), x)) -> +#(p10(), x)) (+#(p10(), +(p1(), x)) -> +#(p10(), x), +#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x))) (+#(p10(), +(p1(), x)) -> +#(p10(), x), +#(p10(), p2()) -> +#(p2(), p10())) (+#(+(x, y), z) -> +#(y, z), +#(p10(), p5()) -> +#(p5(), p10())) (+#(+(x, y), z) -> +#(y, z), +#(p10(), p1()) -> +#(p1(), p10())) (+#(+(x, y), z) -> +#(y, z), +#(p10(), +(p5(), x)) -> +#(p10(), x)) (+#(+(x, y), z) -> +#(y, z), +#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x))) (+#(+(x, y), z) -> +#(y, z), +#(p10(), +(p1(), x)) -> +#(p10(), x)) (+#(+(x, y), z) -> +#(y, z), +#(p10(), +(p1(), x)) -> +#(p1(), +(p10(), x))) (+#(+(x, y), z) -> +#(y, z), +#(p10(), +(p2(), x)) -> +#(p10(), x)) (+#(+(x, y), z) -> +#(y, z), +#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x))) (+#(+(x, y), z) -> +#(y, z), +#(p10(), p2()) -> +#(p2(), p10())) (+#(+(x, y), z) -> +#(y, z), +#(p5(), p1()) -> +#(p1(), p5())) (+#(+(x, y), z) -> +#(y, z), +#(p5(), +(p5(), x)) -> +#(p10(), x)) (+#(+(x, y), z) -> +#(y, z), +#(p5(), +(p1(), x)) -> +#(p5(), x)) (+#(+(x, y), z) -> +#(y, z), +#(p5(), +(p1(), x)) -> +#(p1(), +(p5(), x))) (+#(+(x, y), z) -> +#(y, z), +#(p5(), +(p2(), x)) -> +#(p5(), x)) (+#(+(x, y), z) -> +#(y, z), +#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x))) (+#(+(x, y), z) -> +#(y, z), +#(p5(), p2()) -> +#(p2(), p5())) (+#(+(x, y), z) -> +#(y, z), +#(p1(), +(p1(), x)) -> +#(p2(), x)) (+#(+(x, y), z) -> +#(y, z), +#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x)) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z)) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(+(x, y), z) -> +#(y, z), +#(p2(), p1()) -> +#(p1(), p2())) (+#(+(x, y), z) -> +#(y, z), +#(p2(), +(p1(), x)) -> +#(p1(), +(p2(), x))) (+#(+(x, y), z) -> +#(y, z), +#(p2(), +(p1(), x)) -> +#(p2(), x)) (+#(+(x, y), z) -> +#(y, z), +#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x)) (+#(+(x, y), z) -> +#(y, z), +#(p2(), +(p2(), +(p2(), x))) -> +#(p1(), +(p5(), x))) (+#(+(x, y), z) -> +#(y, z), +#(p2(), +(p2(), p2())) -> +#(p1(), p5())) (+#(p2(), +(p1(), x)) -> +#(p1(), +(p2(), x)), +#(p1(), +(p1(), x)) -> +#(p2(), x)) (+#(p2(), +(p1(), x)) -> +#(p1(), +(p2(), x)), +#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x)) (+#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x)), +#(p2(), +(p1(), x)) -> +#(p1(), +(p2(), x))) (+#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x)), +#(p2(), +(p1(), x)) -> +#(p2(), x)) (+#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x)), +#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x)) (+#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x)), +#(p2(), +(p2(), +(p2(), x))) -> +#(p1(), +(p5(), x))) (+#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x)), +#(p2(), +(p2(), p2())) -> +#(p1(), p5())) (+#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x)), +#(p2(), +(p1(), x)) -> +#(p1(), +(p2(), x))) (+#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x)), +#(p2(), +(p1(), x)) -> +#(p2(), x)) (+#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x)), +#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x)) (+#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x)), +#(p2(), +(p2(), +(p2(), x))) -> +#(p1(), +(p5(), x))) (+#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x)), +#(p2(), +(p2(), p2())) -> +#(p1(), p5())) (+#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x)), +#(p5(), +(p5(), x)) -> +#(p10(), x)) (+#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x)), +#(p5(), +(p1(), x)) -> +#(p5(), x)) (+#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x)), +#(p5(), +(p1(), x)) -> +#(p1(), +(p5(), x))) (+#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x)), +#(p5(), +(p2(), x)) -> +#(p5(), x)) (+#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x)), +#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x))) (+#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x)), +#(p5(), p2()) -> +#(p2(), p5())) (+#(p10(), +(p1(), x)) -> +#(p1(), +(p10(), x)), +#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x)) (+#(p10(), +(p1(), x)) -> +#(p1(), +(p10(), x)), +#(p1(), +(p1(), x)) -> +#(p2(), x)) (+#(p5(), +(p1(), x)) -> +#(p1(), +(p5(), x)), +#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x)) (+#(p5(), +(p1(), x)) -> +#(p1(), +(p5(), x)), +#(p1(), +(p1(), x)) -> +#(p2(), x)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p2(), +(p2(), p2())) -> +#(p1(), p5())) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p2(), +(p2(), +(p2(), x))) -> +#(p1(), +(p5(), x))) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p2(), +(p1(), x)) -> +#(p2(), x)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p2(), +(p1(), x)) -> +#(p1(), +(p2(), x))) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p1(), +(p1(), x)) -> +#(p2(), x)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p5(), p2()) -> +#(p2(), p5())) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x))) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p5(), +(p2(), x)) -> +#(p5(), x)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p5(), +(p1(), x)) -> +#(p1(), +(p5(), x))) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p5(), +(p1(), x)) -> +#(p5(), x)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p5(), +(p5(), x)) -> +#(p10(), x)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p10(), p2()) -> +#(p2(), p10())) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x))) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p10(), +(p2(), x)) -> +#(p10(), x)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p10(), +(p1(), x)) -> +#(p1(), +(p10(), x))) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p10(), +(p1(), x)) -> +#(p10(), x)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x))) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p10(), +(p5(), x)) -> +#(p10(), x)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p10(), p5()) -> +#(p5(), p10())) (+#(p2(), +(p2(), +(p2(), x))) -> +#(p1(), +(p5(), x)), +#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x)) (+#(p2(), +(p2(), +(p2(), x))) -> +#(p1(), +(p5(), x)), +#(p1(), +(p1(), x)) -> +#(p2(), x)) (+#(p10(), +(p5(), x)) -> +#(p10(), x), +#(p10(), p2()) -> +#(p2(), p10())) (+#(p10(), +(p5(), x)) -> +#(p10(), x), +#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x))) (+#(p10(), +(p5(), x)) -> +#(p10(), x), +#(p10(), +(p2(), x)) -> +#(p10(), x)) (+#(p10(), +(p5(), x)) -> +#(p10(), x), +#(p10(), +(p1(), x)) -> +#(p1(), +(p10(), x))) (+#(p10(), +(p5(), x)) -> +#(p10(), x), +#(p10(), +(p1(), x)) -> +#(p10(), x)) (+#(p10(), +(p5(), x)) -> +#(p10(), x), +#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x))) (+#(p10(), +(p5(), x)) -> +#(p10(), x), +#(p10(), +(p5(), x)) -> +#(p10(), x)) (+#(p10(), +(p5(), x)) -> +#(p10(), x), +#(p10(), p1()) -> +#(p1(), p10())) (+#(p10(), +(p5(), x)) -> +#(p10(), x), +#(p10(), p5()) -> +#(p5(), p10())) (+#(p10(), +(p2(), x)) -> +#(p10(), x), +#(p10(), p2()) -> +#(p2(), p10())) (+#(p10(), +(p2(), x)) -> +#(p10(), x), +#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x))) (+#(p10(), +(p2(), x)) -> +#(p10(), x), +#(p10(), +(p2(), x)) -> +#(p10(), x)) (+#(p10(), +(p2(), x)) -> +#(p10(), x), +#(p10(), +(p1(), x)) -> +#(p1(), +(p10(), x))) (+#(p10(), +(p2(), x)) -> +#(p10(), x), +#(p10(), +(p1(), x)) -> +#(p10(), x)) (+#(p10(), +(p2(), x)) -> +#(p10(), x), +#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x))) (+#(p10(), +(p2(), x)) -> +#(p10(), x), +#(p10(), +(p5(), x)) -> +#(p10(), x)) (+#(p10(), +(p2(), x)) -> +#(p10(), x), +#(p10(), p1()) -> +#(p1(), p10())) (+#(p10(), +(p2(), x)) -> +#(p10(), x), +#(p10(), p5()) -> +#(p5(), p10())) (+#(p5(), +(p1(), x)) -> +#(p5(), x), +#(p5(), p2()) -> +#(p2(), p5())) (+#(p5(), +(p1(), x)) -> +#(p5(), x), +#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x))) (+#(p5(), +(p1(), x)) -> +#(p5(), x), +#(p5(), +(p2(), x)) -> +#(p5(), x)) (+#(p5(), +(p1(), x)) -> +#(p5(), x), +#(p5(), +(p1(), x)) -> +#(p1(), +(p5(), x))) (+#(p5(), +(p1(), x)) -> +#(p5(), x), +#(p5(), +(p1(), x)) -> +#(p5(), x)) (+#(p5(), +(p1(), x)) -> +#(p5(), x), +#(p5(), +(p5(), x)) -> +#(p10(), x)) (+#(p5(), +(p1(), x)) -> +#(p5(), x), +#(p5(), p1()) -> +#(p1(), p5())) (+#(p1(), +(p1(), x)) -> +#(p2(), x), +#(p2(), +(p2(), p2())) -> +#(p1(), p5())) (+#(p1(), +(p1(), x)) -> +#(p2(), x), +#(p2(), +(p2(), +(p2(), x))) -> +#(p1(), +(p5(), x))) (+#(p1(), +(p1(), x)) -> +#(p2(), x), +#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x)) (+#(p1(), +(p1(), x)) -> +#(p2(), x), +#(p2(), +(p1(), x)) -> +#(p2(), x)) (+#(p1(), +(p1(), x)) -> +#(p2(), x), +#(p2(), +(p1(), x)) -> +#(p1(), +(p2(), x))) (+#(p1(), +(p1(), x)) -> +#(p2(), x), +#(p2(), p1()) -> +#(p1(), p2())) (+#(p2(), +(p1(), x)) -> +#(p2(), x), +#(p2(), +(p2(), p2())) -> +#(p1(), p5())) (+#(p2(), +(p1(), x)) -> +#(p2(), x), +#(p2(), +(p2(), +(p2(), x))) -> +#(p1(), +(p5(), x))) (+#(p2(), +(p1(), x)) -> +#(p2(), x), +#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x)) (+#(p2(), +(p1(), x)) -> +#(p2(), x), +#(p2(), +(p1(), x)) -> +#(p2(), x)) (+#(p2(), +(p1(), x)) -> +#(p2(), x), +#(p2(), +(p1(), x)) -> +#(p1(), +(p2(), x))) (+#(p2(), +(p1(), x)) -> +#(p2(), x), +#(p2(), p1()) -> +#(p1(), p2())) } STATUS: arrows: 0.779586 SCCS (2): Scc: {+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z)} Scc: {+#(p2(), +(p2(), +(p2(), x))) -> +#(p1(), +(p5(), x)), +#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p2(), +(p1(), x)) -> +#(p2(), x), +#(p2(), +(p1(), x)) -> +#(p1(), +(p2(), x)), +#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p1(), +(p1(), x)) -> +#(p2(), x), +#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x)), +#(p5(), +(p2(), x)) -> +#(p5(), x), +#(p5(), +(p1(), x)) -> +#(p1(), +(p5(), x)), +#(p5(), +(p1(), x)) -> +#(p5(), x), +#(p5(), +(p5(), x)) -> +#(p10(), x), +#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x)), +#(p10(), +(p2(), x)) -> +#(p10(), x), +#(p10(), +(p1(), x)) -> +#(p1(), +(p10(), x)), +#(p10(), +(p1(), x)) -> +#(p10(), x), +#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x)), +#(p10(), +(p5(), x)) -> +#(p10(), x)} SCC (2): Strict: {+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z)} Weak: { +(p2(), +(p2(), p2())) -> +(p1(), p5()), +(p2(), +(p2(), +(p2(), x))) -> +(p1(), +(p5(), x)), +(p2(), +(p1(), x)) -> +(p1(), +(p2(), x)), +(p2(), p1()) -> +(p1(), p2()), +(+(x, y), z) -> +(x, +(y, z)), +(p1(), +(p2(), p2())) -> p5(), +(p1(), +(p2(), +(p2(), x))) -> +(p5(), x), +(p1(), +(p1(), x)) -> +(p2(), x), +(p1(), p1()) -> p2(), +(p5(), p2()) -> +(p2(), p5()), +(p5(), +(p2(), x)) -> +(p2(), +(p5(), x)), +(p5(), +(p1(), x)) -> +(p1(), +(p5(), x)), +(p5(), +(p5(), x)) -> +(p10(), x), +(p5(), p1()) -> +(p1(), p5()), +(p5(), p5()) -> p10(), +(p10(), p2()) -> +(p2(), p10()), +(p10(), +(p2(), x)) -> +(p2(), +(p10(), x)), +(p10(), +(p1(), x)) -> +(p1(), +(p10(), x)), +(p10(), +(p5(), x)) -> +(p5(), +(p10(), x)), +(p10(), p1()) -> +(p1(), p10()), +(p10(), p5()) -> +(p5(), p10())} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [+](x0, x1) = x0 + x1 + 1, [p2] = 1, [p1] = 1, [p5] = 1, [p10] = 1, [+#](x0, x1) = x0 + x1 Strict: +#(+(x, y), z) -> +#(y, z) 1 + 1x + 1y + 1z >= 0 + 1y + 1z +#(+(x, y), z) -> +#(x, +(y, z)) 1 + 1x + 1y + 1z >= 1 + 1x + 1y + 1z Weak: +(p10(), p5()) -> +(p5(), p10()) 3 >= 3 +(p10(), p1()) -> +(p1(), p10()) 3 >= 3 +(p10(), +(p5(), x)) -> +(p5(), +(p10(), x)) 4 + 1x >= 4 + 1x +(p10(), +(p1(), x)) -> +(p1(), +(p10(), x)) 4 + 1x >= 4 + 1x +(p10(), +(p2(), x)) -> +(p2(), +(p10(), x)) 4 + 1x >= 4 + 1x +(p10(), p2()) -> +(p2(), p10()) 3 >= 3 +(p5(), p5()) -> p10() 3 >= 1 +(p5(), p1()) -> +(p1(), p5()) 3 >= 3 +(p5(), +(p5(), x)) -> +(p10(), x) 4 + 1x >= 2 + 1x +(p5(), +(p1(), x)) -> +(p1(), +(p5(), x)) 4 + 1x >= 4 + 1x +(p5(), +(p2(), x)) -> +(p2(), +(p5(), x)) 4 + 1x >= 4 + 1x +(p5(), p2()) -> +(p2(), p5()) 3 >= 3 +(p1(), p1()) -> p2() 3 >= 1 +(p1(), +(p1(), x)) -> +(p2(), x) 4 + 1x >= 2 + 1x +(p1(), +(p2(), +(p2(), x))) -> +(p5(), x) 6 + 1x >= 2 + 1x +(p1(), +(p2(), p2())) -> p5() 5 >= 1 +(+(x, y), z) -> +(x, +(y, z)) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z +(p2(), p1()) -> +(p1(), p2()) 3 >= 3 +(p2(), +(p1(), x)) -> +(p1(), +(p2(), x)) 4 + 1x >= 4 + 1x +(p2(), +(p2(), +(p2(), x))) -> +(p1(), +(p5(), x)) 6 + 1x >= 4 + 1x +(p2(), +(p2(), p2())) -> +(p1(), p5()) 5 >= 3 SCCS (1): Scc: {+#(+(x, y), z) -> +#(x, +(y, z))} SCC (1): Strict: {+#(+(x, y), z) -> +#(x, +(y, z))} Weak: { +(p2(), +(p2(), p2())) -> +(p1(), p5()), +(p2(), +(p2(), +(p2(), x))) -> +(p1(), +(p5(), x)), +(p2(), +(p1(), x)) -> +(p1(), +(p2(), x)), +(p2(), p1()) -> +(p1(), p2()), +(+(x, y), z) -> +(x, +(y, z)), +(p1(), +(p2(), p2())) -> p5(), +(p1(), +(p2(), +(p2(), x))) -> +(p5(), x), +(p1(), +(p1(), x)) -> +(p2(), x), +(p1(), p1()) -> p2(), +(p5(), p2()) -> +(p2(), p5()), +(p5(), +(p2(), x)) -> +(p2(), +(p5(), x)), +(p5(), +(p1(), x)) -> +(p1(), +(p5(), x)), +(p5(), +(p5(), x)) -> +(p10(), x), +(p5(), p1()) -> +(p1(), p5()), +(p5(), p5()) -> p10(), +(p10(), p2()) -> +(p2(), p10()), +(p10(), +(p2(), x)) -> +(p2(), +(p10(), x)), +(p10(), +(p1(), x)) -> +(p1(), +(p10(), x)), +(p10(), +(p5(), x)) -> +(p5(), +(p10(), x)), +(p10(), p1()) -> +(p1(), p10()), +(p10(), p5()) -> +(p5(), p10())} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [+](x0, x1) = x0 + 1, [p2] = 0, [p1] = 0, [p5] = 1, [p10] = 1, [+#](x0, x1) = x0 Strict: +#(+(x, y), z) -> +#(x, +(y, z)) 1 + 1x + 0y + 0z >= 0 + 1x + 0y + 0z Weak: +(p10(), p5()) -> +(p5(), p10()) 2 >= 2 +(p10(), p1()) -> +(p1(), p10()) 2 >= 1 +(p10(), +(p5(), x)) -> +(p5(), +(p10(), x)) 2 + 0x >= 2 + 0x +(p10(), +(p1(), x)) -> +(p1(), +(p10(), x)) 2 + 0x >= 1 + 0x +(p10(), +(p2(), x)) -> +(p2(), +(p10(), x)) 2 + 0x >= 1 + 0x +(p10(), p2()) -> +(p2(), p10()) 2 >= 1 +(p5(), p5()) -> p10() 2 >= 1 +(p5(), p1()) -> +(p1(), p5()) 2 >= 1 +(p5(), +(p5(), x)) -> +(p10(), x) 2 + 0x >= 2 + 0x +(p5(), +(p1(), x)) -> +(p1(), +(p5(), x)) 2 + 0x >= 1 + 0x +(p5(), +(p2(), x)) -> +(p2(), +(p5(), x)) 2 + 0x >= 1 + 0x +(p5(), p2()) -> +(p2(), p5()) 2 >= 1 +(p1(), p1()) -> p2() 1 >= 0 +(p1(), +(p1(), x)) -> +(p2(), x) 1 + 0x >= 1 + 0x +(p1(), +(p2(), +(p2(), x))) -> +(p5(), x) 1 + 0x >= 2 + 0x +(p1(), +(p2(), p2())) -> p5() 1 >= 1 +(+(x, y), z) -> +(x, +(y, z)) 2 + 1x + 0y + 0z >= 1 + 1x + 0y + 0z +(p2(), p1()) -> +(p1(), p2()) 1 >= 1 +(p2(), +(p1(), x)) -> +(p1(), +(p2(), x)) 1 + 0x >= 1 + 0x +(p2(), +(p2(), +(p2(), x))) -> +(p1(), +(p5(), x)) 1 + 0x >= 1 + 0x +(p2(), +(p2(), p2())) -> +(p1(), p5()) 1 >= 1 Qed SCC (17): Strict: {+#(p2(), +(p2(), +(p2(), x))) -> +#(p1(), +(p5(), x)), +#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p2(), +(p1(), x)) -> +#(p2(), x), +#(p2(), +(p1(), x)) -> +#(p1(), +(p2(), x)), +#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p1(), +(p1(), x)) -> +#(p2(), x), +#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x)), +#(p5(), +(p2(), x)) -> +#(p5(), x), +#(p5(), +(p1(), x)) -> +#(p1(), +(p5(), x)), +#(p5(), +(p1(), x)) -> +#(p5(), x), +#(p5(), +(p5(), x)) -> +#(p10(), x), +#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x)), +#(p10(), +(p2(), x)) -> +#(p10(), x), +#(p10(), +(p1(), x)) -> +#(p1(), +(p10(), x)), +#(p10(), +(p1(), x)) -> +#(p10(), x), +#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x)), +#(p10(), +(p5(), x)) -> +#(p10(), x)} Weak: { +(p2(), +(p2(), p2())) -> +(p1(), p5()), +(p2(), +(p2(), +(p2(), x))) -> +(p1(), +(p5(), x)), +(p2(), +(p1(), x)) -> +(p1(), +(p2(), x)), +(p2(), p1()) -> +(p1(), p2()), +(+(x, y), z) -> +(x, +(y, z)), +(p1(), +(p2(), p2())) -> p5(), +(p1(), +(p2(), +(p2(), x))) -> +(p5(), x), +(p1(), +(p1(), x)) -> +(p2(), x), +(p1(), p1()) -> p2(), +(p5(), p2()) -> +(p2(), p5()), +(p5(), +(p2(), x)) -> +(p2(), +(p5(), x)), +(p5(), +(p1(), x)) -> +(p1(), +(p5(), x)), +(p5(), +(p5(), x)) -> +(p10(), x), +(p5(), p1()) -> +(p1(), p5()), +(p5(), p5()) -> p10(), +(p10(), p2()) -> +(p2(), p10()), +(p10(), +(p2(), x)) -> +(p2(), +(p10(), x)), +(p10(), +(p1(), x)) -> +(p1(), +(p10(), x)), +(p10(), +(p5(), x)) -> +(p5(), +(p10(), x)), +(p10(), p1()) -> +(p1(), p10()), +(p10(), p5()) -> +(p5(), p10())} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [+](x0, x1) = x0 + x1, [p2] = 1, [p1] = 1, [p5] = 1, [p10] = 1, [+#](x0, x1) = x0 Strict: +#(p10(), +(p5(), x)) -> +#(p10(), x) 1 + 1x >= 0 + 1x +#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x)) 1 + 1x >= 1 + 1x +#(p10(), +(p1(), x)) -> +#(p10(), x) 1 + 1x >= 0 + 1x +#(p10(), +(p1(), x)) -> +#(p1(), +(p10(), x)) 1 + 1x >= 1 + 1x +#(p10(), +(p2(), x)) -> +#(p10(), x) 1 + 1x >= 0 + 1x +#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x)) 1 + 1x >= 1 + 1x +#(p5(), +(p5(), x)) -> +#(p10(), x) 1 + 1x >= 0 + 1x +#(p5(), +(p1(), x)) -> +#(p5(), x) 1 + 1x >= 0 + 1x +#(p5(), +(p1(), x)) -> +#(p1(), +(p5(), x)) 1 + 1x >= 1 + 1x +#(p5(), +(p2(), x)) -> +#(p5(), x) 1 + 1x >= 0 + 1x +#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x)) 1 + 1x >= 1 + 1x +#(p1(), +(p1(), x)) -> +#(p2(), x) 1 + 1x >= 0 + 1x +#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x) 2 + 1x >= 0 + 1x +#(p2(), +(p1(), x)) -> +#(p1(), +(p2(), x)) 1 + 1x >= 1 + 1x +#(p2(), +(p1(), x)) -> +#(p2(), x) 1 + 1x >= 0 + 1x +#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x) 2 + 1x >= 0 + 1x +#(p2(), +(p2(), +(p2(), x))) -> +#(p1(), +(p5(), x)) 2 + 1x >= 1 + 1x Weak: +(p10(), p5()) -> +(p5(), p10()) 2 >= 2 +(p10(), p1()) -> +(p1(), p10()) 2 >= 2 +(p10(), +(p5(), x)) -> +(p5(), +(p10(), x)) 2 + 1x >= 2 + 1x +(p10(), +(p1(), x)) -> +(p1(), +(p10(), x)) 2 + 1x >= 2 + 1x +(p10(), +(p2(), x)) -> +(p2(), +(p10(), x)) 2 + 1x >= 2 + 1x +(p10(), p2()) -> +(p2(), p10()) 2 >= 2 +(p5(), p5()) -> p10() 2 >= 1 +(p5(), p1()) -> +(p1(), p5()) 2 >= 2 +(p5(), +(p5(), x)) -> +(p10(), x) 2 + 1x >= 1 + 1x +(p5(), +(p1(), x)) -> +(p1(), +(p5(), x)) 2 + 1x >= 2 + 1x +(p5(), +(p2(), x)) -> +(p2(), +(p5(), x)) 2 + 1x >= 2 + 1x +(p5(), p2()) -> +(p2(), p5()) 2 >= 2 +(p1(), p1()) -> p2() 2 >= 1 +(p1(), +(p1(), x)) -> +(p2(), x) 2 + 1x >= 1 + 1x +(p1(), +(p2(), +(p2(), x))) -> +(p5(), x) 3 + 1x >= 1 + 1x +(p1(), +(p2(), p2())) -> p5() 3 >= 1 +(+(x, y), z) -> +(x, +(y, z)) 0 + 1x + 1y + 1z >= 0 + 1x + 1y + 1z +(p2(), p1()) -> +(p1(), p2()) 2 >= 2 +(p2(), +(p1(), x)) -> +(p1(), +(p2(), x)) 2 + 1x >= 2 + 1x +(p2(), +(p2(), +(p2(), x))) -> +(p1(), +(p5(), x)) 3 + 1x >= 2 + 1x +(p2(), +(p2(), p2())) -> +(p1(), p5()) 3 >= 2 SCCS (0):