MAYBE Time: 0.672109 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))} 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)))} 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)))} 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))} Open