MAYBE Time: 0.208970 TRS: { +(x, +(y, z)) -> +(+(x, y), z), +(+(x, *(y, z)), *(y, u)) -> +(x, *(y, +(z, u))), *(x, +(y, z)) -> +(*(x, y), *(x, z))} DP: DP: { +#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z), +#(+(x, *(y, z)), *(y, u)) -> +#(x, *(y, +(z, u))), +#(+(x, *(y, z)), *(y, u)) -> +#(z, u), +#(+(x, *(y, z)), *(y, u)) -> *#(y, +(z, u)), *#(x, +(y, z)) -> +#(*(x, y), *(x, z)), *#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z)} TRS: { +(x, +(y, z)) -> +(+(x, y), z), +(+(x, *(y, z)), *(y, u)) -> +(x, *(y, +(z, u))), *(x, +(y, z)) -> +(*(x, y), *(x, z))} UR: { +(x, +(y, z)) -> +(+(x, y), z), +(+(x, *(y, z)), *(y, u)) -> +(x, *(y, +(z, u))), *(x, +(y, z)) -> +(*(x, y), *(x, z)), a(w, v) -> w, a(w, v) -> v} EDG: {(+#(+(x, *(y, z)), *(y, u)) -> +#(z, u), +#(+(x, *(y, z)), *(y, u)) -> *#(y, +(z, u))) (+#(+(x, *(y, z)), *(y, u)) -> +#(z, u), +#(+(x, *(y, z)), *(y, u)) -> +#(z, u)) (+#(+(x, *(y, z)), *(y, u)) -> +#(z, u), +#(+(x, *(y, z)), *(y, u)) -> +#(x, *(y, +(z, u)))) (+#(+(x, *(y, z)), *(y, u)) -> +#(z, u), +#(x, +(y, z)) -> +#(+(x, y), z)) (+#(+(x, *(y, z)), *(y, u)) -> +#(z, u), +#(x, +(y, z)) -> +#(x, y)) (*#(x, +(y, z)) -> +#(*(x, y), *(x, z)), +#(+(x, *(y, z)), *(y, u)) -> *#(y, +(z, u))) (*#(x, +(y, z)) -> +#(*(x, y), *(x, z)), +#(+(x, *(y, z)), *(y, u)) -> +#(z, u)) (*#(x, +(y, z)) -> +#(*(x, y), *(x, z)), +#(+(x, *(y, z)), *(y, u)) -> +#(x, *(y, +(z, u)))) (*#(x, +(y, z)) -> +#(*(x, y), *(x, z)), +#(x, +(y, z)) -> +#(+(x, y), z)) (*#(x, +(y, z)) -> +#(*(x, y), *(x, z)), +#(x, +(y, z)) -> +#(x, y)) (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z)) (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> *#(x, z)) (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (+#(x, +(y, z)) -> +#(+(x, y), z), +#(x, +(y, z)) -> +#(x, y)) (+#(x, +(y, z)) -> +#(+(x, y), z), +#(x, +(y, z)) -> +#(+(x, y), z)) (+#(x, +(y, z)) -> +#(+(x, y), z), +#(+(x, *(y, z)), *(y, u)) -> +#(x, *(y, +(z, u)))) (+#(x, +(y, z)) -> +#(+(x, y), z), +#(+(x, *(y, z)), *(y, u)) -> +#(z, u)) (+#(x, +(y, z)) -> +#(+(x, y), z), +#(+(x, *(y, z)), *(y, u)) -> *#(y, +(z, u))) (+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(x, y)) (+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z)) (+#(x, +(y, z)) -> +#(x, y), +#(+(x, *(y, z)), *(y, u)) -> +#(x, *(y, +(z, u)))) (+#(x, +(y, z)) -> +#(x, y), +#(+(x, *(y, z)), *(y, u)) -> +#(z, u)) (+#(x, +(y, z)) -> +#(x, y), +#(+(x, *(y, z)), *(y, u)) -> *#(y, +(z, u))) (+#(+(x, *(y, z)), *(y, u)) -> *#(y, +(z, u)), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (+#(+(x, *(y, z)), *(y, u)) -> *#(y, +(z, u)), *#(x, +(y, z)) -> *#(x, y)) (+#(+(x, *(y, z)), *(y, u)) -> *#(y, +(z, u)), *#(x, +(y, z)) -> *#(x, z)) (+#(+(x, *(y, z)), *(y, u)) -> +#(x, *(y, +(z, u))), +#(x, +(y, z)) -> +#(x, y)) (+#(+(x, *(y, z)), *(y, u)) -> +#(x, *(y, +(z, u))), +#(x, +(y, z)) -> +#(+(x, y), z)) (+#(+(x, *(y, z)), *(y, u)) -> +#(x, *(y, +(z, u))), +#(+(x, *(y, z)), *(y, u)) -> +#(x, *(y, +(z, u)))) (+#(+(x, *(y, z)), *(y, u)) -> +#(x, *(y, +(z, u))), +#(+(x, *(y, z)), *(y, u)) -> +#(z, u)) (+#(+(x, *(y, z)), *(y, u)) -> +#(x, *(y, +(z, u))), +#(+(x, *(y, z)), *(y, u)) -> *#(y, +(z, u)))} STATUS: arrows: 0.468750 SCCS (1): Scc: { +#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z), +#(+(x, *(y, z)), *(y, u)) -> +#(x, *(y, +(z, u))), +#(+(x, *(y, z)), *(y, u)) -> +#(z, u), +#(+(x, *(y, z)), *(y, u)) -> *#(y, +(z, u)), *#(x, +(y, z)) -> +#(*(x, y), *(x, z)), *#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z)} SCC (8): Strict: { +#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z), +#(+(x, *(y, z)), *(y, u)) -> +#(x, *(y, +(z, u))), +#(+(x, *(y, z)), *(y, u)) -> +#(z, u), +#(+(x, *(y, z)), *(y, u)) -> *#(y, +(z, u)), *#(x, +(y, z)) -> +#(*(x, y), *(x, z)), *#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z)} Weak: { +(x, +(y, z)) -> +(+(x, y), z), +(+(x, *(y, z)), *(y, u)) -> +(x, *(y, +(z, u))), *(x, +(y, z)) -> +(*(x, y), *(x, z))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [+](x0, x1) = x0 + x1 + 1, [*](x0, x1) = x0, [+#](x0, x1) = x0 + x1 + 1, [*#](x0, x1) = x0 + 1 Strict: *#(x, +(y, z)) -> *#(x, z) 2 + 0x + 1y + 1z >= 1 + 0x + 1z *#(x, +(y, z)) -> *#(x, y) 2 + 0x + 1y + 1z >= 1 + 0x + 1y *#(x, +(y, z)) -> +#(*(x, y), *(x, z)) 2 + 0x + 1y + 1z >= 1 + 0x + 1y + 1z +#(+(x, *(y, z)), *(y, u)) -> *#(y, +(z, u)) 2 + 1x + 0y + 1z + 1u >= 2 + 0y + 1z + 1u +#(+(x, *(y, z)), *(y, u)) -> +#(z, u) 2 + 1x + 0y + 1z + 1u >= 1 + 1z + 1u +#(+(x, *(y, z)), *(y, u)) -> +#(x, *(y, +(z, u))) 2 + 1x + 0y + 1z + 1u >= 2 + 1x + 0y + 1z + 1u +#(x, +(y, z)) -> +#(+(x, y), z) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z +#(x, +(y, z)) -> +#(x, y) 2 + 1x + 1y + 1z >= 1 + 1x + 1y Weak: *(x, +(y, z)) -> +(*(x, y), *(x, z)) 1 + 0x + 1y + 1z >= 1 + 0x + 1y + 1z +(+(x, *(y, z)), *(y, u)) -> +(x, *(y, +(z, u))) 2 + 1x + 0y + 1z + 1u >= 2 + 1x + 0y + 1z + 1u +(x, +(y, z)) -> +(+(x, y), z) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z SCCS (1): Scc: { +#(x, +(y, z)) -> +#(+(x, y), z), +#(+(x, *(y, z)), *(y, u)) -> +#(x, *(y, +(z, u)))} SCC (2): Strict: { +#(x, +(y, z)) -> +#(+(x, y), z), +#(+(x, *(y, z)), *(y, u)) -> +#(x, *(y, +(z, u)))} Weak: { +(x, +(y, z)) -> +(+(x, y), z), +(+(x, *(y, z)), *(y, u)) -> +(x, *(y, +(z, u))), *(x, +(y, z)) -> +(*(x, y), *(x, z))} Fail