MAYBE Time: 0.011390 TRS: { +(*(x, y), *(x, z)) -> *(x, +(y, z)), +(*(x, y), +(*(x, z), u())) -> +(*(x, +(y, z)), u()), +(+(x, y), z) -> +(x, +(y, z))} DP: DP: { +#(*(x, y), *(x, z)) -> +#(y, z), +#(*(x, y), +(*(x, z), u())) -> +#(y, z), +#(*(x, y), +(*(x, z), u())) -> +#(*(x, +(y, z)), u()), +#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z)} TRS: { +(*(x, y), *(x, z)) -> *(x, +(y, z)), +(*(x, y), +(*(x, z), u())) -> +(*(x, +(y, z)), u()), +(+(x, y), z) -> +(x, +(y, z))} UR: { +(*(x, y), *(x, z)) -> *(x, +(y, z)), +(*(x, y), +(*(x, z), u())) -> +(*(x, +(y, z)), u()), +(+(x, y), z) -> +(x, +(y, z))} EDG: {(+#(*(x, y), +(*(x, z), u())) -> +#(*(x, +(y, z)), u()), +#(+(x, y), z) -> +#(y, z)) (+#(*(x, y), +(*(x, z), u())) -> +#(*(x, +(y, z)), u()), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(*(x, y), +(*(x, z), u())) -> +#(*(x, +(y, z)), u()), +#(*(x, y), +(*(x, z), u())) -> +#(*(x, +(y, z)), u())) (+#(*(x, y), +(*(x, z), u())) -> +#(*(x, +(y, z)), u()), +#(*(x, y), +(*(x, z), u())) -> +#(y, z)) (+#(*(x, y), +(*(x, z), u())) -> +#(*(x, +(y, z)), u()), +#(*(x, y), *(x, z)) -> +#(y, z)) (+#(*(x, y), +(*(x, z), u())) -> +#(y, z), +#(+(x, y), z) -> +#(y, z)) (+#(*(x, y), +(*(x, z), u())) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(*(x, y), +(*(x, z), u())) -> +#(y, z), +#(*(x, y), +(*(x, z), u())) -> +#(*(x, +(y, z)), u())) (+#(*(x, y), +(*(x, z), u())) -> +#(y, z), +#(*(x, y), +(*(x, z), u())) -> +#(y, z)) (+#(*(x, y), +(*(x, z), u())) -> +#(y, z), +#(*(x, y), *(x, z)) -> +#(y, z)) (+#(+(x, y), z) -> +#(y, z), +#(*(x, y), *(x, z)) -> +#(y, z)) (+#(+(x, y), z) -> +#(y, z), +#(*(x, y), +(*(x, z), u())) -> +#(y, z)) (+#(+(x, y), z) -> +#(y, z), +#(*(x, y), +(*(x, z), u())) -> +#(*(x, +(y, z)), u())) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z)) (+#(*(x, y), *(x, z)) -> +#(y, z), +#(*(x, y), *(x, z)) -> +#(y, z)) (+#(*(x, y), *(x, z)) -> +#(y, z), +#(*(x, y), +(*(x, z), u())) -> +#(y, z)) (+#(*(x, y), *(x, z)) -> +#(y, z), +#(*(x, y), +(*(x, z), u())) -> +#(*(x, +(y, z)), u())) (+#(*(x, y), *(x, z)) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(*(x, y), *(x, z)) -> +#(y, z), +#(+(x, y), z) -> +#(y, z)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(*(x, y), *(x, z)) -> +#(y, z)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(*(x, y), +(*(x, z), u())) -> +#(y, z)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(*(x, y), +(*(x, z), u())) -> +#(*(x, +(y, z)), u())) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z))} EDG: {(+#(*(x, y), +(*(x, z), u())) -> +#(y, z), +#(+(x, y), z) -> +#(y, z)) (+#(*(x, y), +(*(x, z), u())) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(*(x, y), +(*(x, z), u())) -> +#(y, z), +#(*(x, y), +(*(x, z), u())) -> +#(*(x, +(y, z)), u())) (+#(*(x, y), +(*(x, z), u())) -> +#(y, z), +#(*(x, y), +(*(x, z), u())) -> +#(y, z)) (+#(*(x, y), +(*(x, z), u())) -> +#(y, z), +#(*(x, y), *(x, z)) -> +#(y, z)) (+#(+(x, y), z) -> +#(y, z), +#(*(x, y), *(x, z)) -> +#(y, z)) (+#(+(x, y), z) -> +#(y, z), +#(*(x, y), +(*(x, z), u())) -> +#(y, z)) (+#(+(x, y), z) -> +#(y, z), +#(*(x, y), +(*(x, z), u())) -> +#(*(x, +(y, z)), u())) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z)) (+#(*(x, y), *(x, z)) -> +#(y, z), +#(*(x, y), *(x, z)) -> +#(y, z)) (+#(*(x, y), *(x, z)) -> +#(y, z), +#(*(x, y), +(*(x, z), u())) -> +#(y, z)) (+#(*(x, y), *(x, z)) -> +#(y, z), +#(*(x, y), +(*(x, z), u())) -> +#(*(x, +(y, z)), u())) (+#(*(x, y), *(x, z)) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(*(x, y), *(x, z)) -> +#(y, z), +#(+(x, y), z) -> +#(y, z)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(*(x, y), *(x, z)) -> +#(y, z)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(*(x, y), +(*(x, z), u())) -> +#(y, z)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(*(x, y), +(*(x, z), u())) -> +#(*(x, +(y, z)), u())) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z))} EDG: {(+#(*(x, y), +(*(x, z), u())) -> +#(y, z), +#(+(x, y), z) -> +#(y, z)) (+#(*(x, y), +(*(x, z), u())) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(*(x, y), +(*(x, z), u())) -> +#(y, z), +#(*(x, y), +(*(x, z), u())) -> +#(*(x, +(y, z)), u())) (+#(*(x, y), +(*(x, z), u())) -> +#(y, z), +#(*(x, y), +(*(x, z), u())) -> +#(y, z)) (+#(*(x, y), +(*(x, z), u())) -> +#(y, z), +#(*(x, y), *(x, z)) -> +#(y, z)) (+#(+(x, y), z) -> +#(y, z), +#(*(x, y), *(x, z)) -> +#(y, z)) (+#(+(x, y), z) -> +#(y, z), +#(*(x, y), +(*(x, z), u())) -> +#(y, z)) (+#(+(x, y), z) -> +#(y, z), +#(*(x, y), +(*(x, z), u())) -> +#(*(x, +(y, z)), u())) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z)) (+#(*(x, y), *(x, z)) -> +#(y, z), +#(*(x, y), *(x, z)) -> +#(y, z)) (+#(*(x, y), *(x, z)) -> +#(y, z), +#(*(x, y), +(*(x, z), u())) -> +#(y, z)) (+#(*(x, y), *(x, z)) -> +#(y, z), +#(*(x, y), +(*(x, z), u())) -> +#(*(x, +(y, z)), u())) (+#(*(x, y), *(x, z)) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(*(x, y), *(x, z)) -> +#(y, z), +#(+(x, y), z) -> +#(y, z)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z))} EDG: {(+#(*(x, y), +(*(x, z), u())) -> +#(y, z), +#(+(x, y), z) -> +#(y, z)) (+#(*(x, y), +(*(x, z), u())) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(*(x, y), +(*(x, z), u())) -> +#(y, z), +#(*(x, y), +(*(x, z), u())) -> +#(*(x, +(y, z)), u())) (+#(*(x, y), +(*(x, z), u())) -> +#(y, z), +#(*(x, y), +(*(x, z), u())) -> +#(y, z)) (+#(*(x, y), +(*(x, z), u())) -> +#(y, z), +#(*(x, y), *(x, z)) -> +#(y, z)) (+#(+(x, y), z) -> +#(y, z), +#(*(x, y), *(x, z)) -> +#(y, z)) (+#(+(x, y), z) -> +#(y, z), +#(*(x, y), +(*(x, z), u())) -> +#(y, z)) (+#(+(x, y), z) -> +#(y, z), +#(*(x, y), +(*(x, z), u())) -> +#(*(x, +(y, z)), u())) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z)) (+#(*(x, y), *(x, z)) -> +#(y, z), +#(*(x, y), *(x, z)) -> +#(y, z)) (+#(*(x, y), *(x, z)) -> +#(y, z), +#(*(x, y), +(*(x, z), u())) -> +#(y, z)) (+#(*(x, y), *(x, z)) -> +#(y, z), +#(*(x, y), +(*(x, z), u())) -> +#(*(x, +(y, z)), u())) (+#(*(x, y), *(x, z)) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(*(x, y), *(x, z)) -> +#(y, z), +#(+(x, y), z) -> +#(y, z)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z))} STATUS: arrows: 0.320000 SCCS (1): Scc: { +#(*(x, y), *(x, z)) -> +#(y, z), +#(*(x, y), +(*(x, z), u())) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z)} SCC (4): Strict: { +#(*(x, y), *(x, z)) -> +#(y, z), +#(*(x, y), +(*(x, z), u())) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z)} Weak: { +(*(x, y), *(x, z)) -> *(x, +(y, z)), +(*(x, y), +(*(x, z), u())) -> +(*(x, +(y, z)), u()), +(+(x, y), z) -> +(x, +(y, z))} Open