MAYBE Time: 0.005670 TRS: {+(+(x, y), z) -> +(x, +(y, z)), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(+(y, z), x) -> +(*(x, y), *(x, z)), *(*(x, y), z) -> *(x, *(y, z))} DP: DP: {+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z), *#(x, +(y, z)) -> +#(*(x, y), *(x, z)), *#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z), *#(+(y, z), x) -> +#(*(x, y), *(x, z)), *#(+(y, z), x) -> *#(x, y), *#(+(y, z), x) -> *#(x, z), *#(*(x, y), z) -> *#(x, *(y, z)), *#(*(x, y), z) -> *#(y, z)} TRS: {+(+(x, y), z) -> +(x, +(y, z)), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(+(y, z), x) -> +(*(x, y), *(x, z)), *(*(x, y), z) -> *(x, *(y, z))} EDG: {(*#(x, +(y, z)) -> +#(*(x, y), *(x, z)), +#(+(x, y), z) -> +#(y, z)) (*#(x, +(y, z)) -> +#(*(x, y), *(x, z)), +#(+(x, y), z) -> +#(x, +(y, z))) (*#(*(x, y), z) -> *#(x, *(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)), *#(+(y, z), x) -> *#(x, z)) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(+(y, z), x) -> *#(x, y)) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(+(y, z), x) -> +#(*(x, y), *(x, z))) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(x, +(y, z)) -> *#(x, z)) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(x, +(y, z)) -> *#(x, y)) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (*#(x, +(y, z)) -> *#(x, z), *#(*(x, y), z) -> *#(y, z)) (*#(x, +(y, z)) -> *#(x, z), *#(*(x, y), z) -> *#(x, *(y, z))) (*#(x, +(y, z)) -> *#(x, z), *#(+(y, z), x) -> *#(x, z)) (*#(x, +(y, z)) -> *#(x, z), *#(+(y, z), x) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, z), *#(+(y, z), x) -> +#(*(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) -> *#(y, z), *#(*(x, y), z) -> *#(y, z)) (*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(x, *(y, z))) (*#(*(x, y), z) -> *#(y, z), *#(+(y, z), x) -> *#(x, z)) (*#(*(x, y), z) -> *#(y, z), *#(+(y, z), x) -> *#(x, y)) (*#(*(x, y), z) -> *#(y, z), *#(+(y, z), x) -> +#(*(x, y), *(x, z))) (*#(*(x, y), z) -> *#(y, z), *#(x, +(y, z)) -> *#(x, z)) (*#(*(x, y), z) -> *#(y, z), *#(x, +(y, z)) -> *#(x, y)) (*#(*(x, y), z) -> *#(y, z), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (*#(+(y, z), x) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)) (*#(+(y, z), x) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z))) (*#(+(y, z), x) -> *#(x, y), *#(+(y, z), x) -> *#(x, z)) (*#(+(y, z), x) -> *#(x, y), *#(+(y, z), x) -> *#(x, y)) (*#(+(y, z), x) -> *#(x, y), *#(+(y, z), x) -> +#(*(x, y), *(x, z))) (*#(+(y, z), x) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z)) (*#(+(y, z), x) -> *#(x, y), *#(x, +(y, z)) -> *#(x, y)) (*#(+(y, z), x) -> *#(x, y), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z)) (*#(x, +(y, z)) -> *#(x, y), *#(+(y, z), x) -> +#(*(x, y), *(x, z))) (*#(x, +(y, z)) -> *#(x, y), *#(+(y, z), x) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, y), *#(+(y, z), x) -> *#(x, z)) (*#(x, +(y, z)) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z))) (*#(x, +(y, z)) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)) (*#(+(y, z), x) -> *#(x, z), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (*#(+(y, z), x) -> *#(x, z), *#(x, +(y, z)) -> *#(x, y)) (*#(+(y, z), x) -> *#(x, z), *#(x, +(y, z)) -> *#(x, z)) (*#(+(y, z), x) -> *#(x, z), *#(+(y, z), x) -> +#(*(x, y), *(x, z))) (*#(+(y, z), x) -> *#(x, z), *#(+(y, z), x) -> *#(x, y)) (*#(+(y, z), x) -> *#(x, z), *#(+(y, z), x) -> *#(x, z)) (*#(+(y, z), x) -> *#(x, z), *#(*(x, y), z) -> *#(x, *(y, z))) (*#(+(y, z), x) -> *#(x, z), *#(*(x, y), z) -> *#(y, z)) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z)) (*#(+(y, z), x) -> +#(*(x, y), *(x, z)), +#(+(x, y), z) -> +#(x, +(y, z))) (*#(+(y, z), x) -> +#(*(x, y), *(x, 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, z)) -> +#(*(x, y), *(x, z)), +#(+(x, y), z) -> +#(y, z)) (*#(x, +(y, z)) -> +#(*(x, y), *(x, z)), +#(+(x, y), z) -> +#(x, +(y, z))) (*#(*(x, y), z) -> *#(x, *(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)), *#(+(y, z), x) -> *#(x, z)) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(+(y, z), x) -> *#(x, y)) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(+(y, z), x) -> +#(*(x, y), *(x, z))) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(x, +(y, z)) -> *#(x, z)) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(x, +(y, z)) -> *#(x, y)) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (*#(x, +(y, z)) -> *#(x, z), *#(*(x, y), z) -> *#(y, z)) (*#(x, +(y, z)) -> *#(x, z), *#(*(x, y), z) -> *#(x, *(y, z))) (*#(x, +(y, z)) -> *#(x, z), *#(+(y, z), x) -> *#(x, z)) (*#(x, +(y, z)) -> *#(x, z), *#(+(y, z), x) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, z), *#(+(y, z), x) -> +#(*(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) -> *#(y, z), *#(*(x, y), z) -> *#(y, z)) (*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(x, *(y, z))) (*#(*(x, y), z) -> *#(y, z), *#(+(y, z), x) -> *#(x, z)) (*#(*(x, y), z) -> *#(y, z), *#(+(y, z), x) -> *#(x, y)) (*#(*(x, y), z) -> *#(y, z), *#(+(y, z), x) -> +#(*(x, y), *(x, z))) (*#(*(x, y), z) -> *#(y, z), *#(x, +(y, z)) -> *#(x, z)) (*#(*(x, y), z) -> *#(y, z), *#(x, +(y, z)) -> *#(x, y)) (*#(*(x, y), z) -> *#(y, z), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (*#(+(y, z), x) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)) (*#(+(y, z), x) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z))) (*#(+(y, z), x) -> *#(x, y), *#(+(y, z), x) -> *#(x, z)) (*#(+(y, z), x) -> *#(x, y), *#(+(y, z), x) -> *#(x, y)) (*#(+(y, z), x) -> *#(x, y), *#(+(y, z), x) -> +#(*(x, y), *(x, z))) (*#(+(y, z), x) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z)) (*#(+(y, z), x) -> *#(x, y), *#(x, +(y, z)) -> *#(x, y)) (*#(+(y, z), x) -> *#(x, y), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z)) (*#(x, +(y, z)) -> *#(x, y), *#(+(y, z), x) -> +#(*(x, y), *(x, z))) (*#(x, +(y, z)) -> *#(x, y), *#(+(y, z), x) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, y), *#(+(y, z), x) -> *#(x, z)) (*#(x, +(y, z)) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z))) (*#(x, +(y, z)) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)) (*#(+(y, z), x) -> *#(x, z), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (*#(+(y, z), x) -> *#(x, z), *#(x, +(y, z)) -> *#(x, y)) (*#(+(y, z), x) -> *#(x, z), *#(x, +(y, z)) -> *#(x, z)) (*#(+(y, z), x) -> *#(x, z), *#(+(y, z), x) -> +#(*(x, y), *(x, z))) (*#(+(y, z), x) -> *#(x, z), *#(+(y, z), x) -> *#(x, y)) (*#(+(y, z), x) -> *#(x, z), *#(+(y, z), x) -> *#(x, z)) (*#(+(y, z), x) -> *#(x, z), *#(*(x, y), z) -> *#(x, *(y, z))) (*#(+(y, z), x) -> *#(x, z), *#(*(x, y), z) -> *#(y, z)) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z)) (*#(+(y, z), x) -> +#(*(x, y), *(x, z)), +#(+(x, y), z) -> +#(x, +(y, z))) (*#(+(y, z), x) -> +#(*(x, y), *(x, 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, z)) -> +#(*(x, y), *(x, z)), +#(+(x, y), z) -> +#(y, z)) (*#(x, +(y, z)) -> +#(*(x, y), *(x, z)), +#(+(x, y), z) -> +#(x, +(y, z))) (*#(*(x, y), z) -> *#(x, *(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)), *#(+(y, z), x) -> *#(x, z)) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(+(y, z), x) -> *#(x, y)) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(+(y, z), x) -> +#(*(x, y), *(x, z))) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(x, +(y, z)) -> *#(x, z)) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(x, +(y, z)) -> *#(x, y)) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (*#(x, +(y, z)) -> *#(x, z), *#(*(x, y), z) -> *#(y, z)) (*#(x, +(y, z)) -> *#(x, z), *#(*(x, y), z) -> *#(x, *(y, z))) (*#(x, +(y, z)) -> *#(x, z), *#(+(y, z), x) -> *#(x, z)) (*#(x, +(y, z)) -> *#(x, z), *#(+(y, z), x) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, z), *#(+(y, z), x) -> +#(*(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) -> *#(y, z), *#(*(x, y), z) -> *#(y, z)) (*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(x, *(y, z))) (*#(*(x, y), z) -> *#(y, z), *#(+(y, z), x) -> *#(x, z)) (*#(*(x, y), z) -> *#(y, z), *#(+(y, z), x) -> *#(x, y)) (*#(*(x, y), z) -> *#(y, z), *#(+(y, z), x) -> +#(*(x, y), *(x, z))) (*#(*(x, y), z) -> *#(y, z), *#(x, +(y, z)) -> *#(x, z)) (*#(*(x, y), z) -> *#(y, z), *#(x, +(y, z)) -> *#(x, y)) (*#(*(x, y), z) -> *#(y, z), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (*#(+(y, z), x) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)) (*#(+(y, z), x) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z))) (*#(+(y, z), x) -> *#(x, y), *#(+(y, z), x) -> *#(x, z)) (*#(+(y, z), x) -> *#(x, y), *#(+(y, z), x) -> *#(x, y)) (*#(+(y, z), x) -> *#(x, y), *#(+(y, z), x) -> +#(*(x, y), *(x, z))) (*#(+(y, z), x) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z)) (*#(+(y, z), x) -> *#(x, y), *#(x, +(y, z)) -> *#(x, y)) (*#(+(y, z), x) -> *#(x, y), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z)) (*#(x, +(y, z)) -> *#(x, y), *#(+(y, z), x) -> +#(*(x, y), *(x, z))) (*#(x, +(y, z)) -> *#(x, y), *#(+(y, z), x) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, y), *#(+(y, z), x) -> *#(x, z)) (*#(x, +(y, z)) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z))) (*#(x, +(y, z)) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)) (*#(+(y, z), x) -> *#(x, z), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (*#(+(y, z), x) -> *#(x, z), *#(x, +(y, z)) -> *#(x, y)) (*#(+(y, z), x) -> *#(x, z), *#(x, +(y, z)) -> *#(x, z)) (*#(+(y, z), x) -> *#(x, z), *#(+(y, z), x) -> +#(*(x, y), *(x, z))) (*#(+(y, z), x) -> *#(x, z), *#(+(y, z), x) -> *#(x, y)) (*#(+(y, z), x) -> *#(x, z), *#(+(y, z), x) -> *#(x, z)) (*#(+(y, z), x) -> *#(x, z), *#(*(x, y), z) -> *#(x, *(y, z))) (*#(+(y, z), x) -> *#(x, z), *#(*(x, y), z) -> *#(y, z)) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z)) (*#(+(y, z), x) -> +#(*(x, y), *(x, z)), +#(+(x, y), z) -> +#(x, +(y, z))) (*#(+(y, z), x) -> +#(*(x, y), *(x, 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, z)) -> +#(*(x, y), *(x, z)), +#(+(x, y), z) -> +#(y, z)) (*#(x, +(y, z)) -> +#(*(x, y), *(x, z)), +#(+(x, y), z) -> +#(x, +(y, z))) (*#(*(x, y), z) -> *#(x, *(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)), *#(+(y, z), x) -> *#(x, z)) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(+(y, z), x) -> *#(x, y)) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(+(y, z), x) -> +#(*(x, y), *(x, z))) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(x, +(y, z)) -> *#(x, z)) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(x, +(y, z)) -> *#(x, y)) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (*#(x, +(y, z)) -> *#(x, z), *#(*(x, y), z) -> *#(y, z)) (*#(x, +(y, z)) -> *#(x, z), *#(*(x, y), z) -> *#(x, *(y, z))) (*#(x, +(y, z)) -> *#(x, z), *#(+(y, z), x) -> *#(x, z)) (*#(x, +(y, z)) -> *#(x, z), *#(+(y, z), x) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, z), *#(+(y, z), x) -> +#(*(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) -> *#(y, z), *#(*(x, y), z) -> *#(y, z)) (*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(x, *(y, z))) (*#(*(x, y), z) -> *#(y, z), *#(+(y, z), x) -> *#(x, z)) (*#(*(x, y), z) -> *#(y, z), *#(+(y, z), x) -> *#(x, y)) (*#(*(x, y), z) -> *#(y, z), *#(+(y, z), x) -> +#(*(x, y), *(x, z))) (*#(*(x, y), z) -> *#(y, z), *#(x, +(y, z)) -> *#(x, z)) (*#(*(x, y), z) -> *#(y, z), *#(x, +(y, z)) -> *#(x, y)) (*#(*(x, y), z) -> *#(y, z), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (*#(+(y, z), x) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)) (*#(+(y, z), x) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z))) (*#(+(y, z), x) -> *#(x, y), *#(+(y, z), x) -> *#(x, z)) (*#(+(y, z), x) -> *#(x, y), *#(+(y, z), x) -> *#(x, y)) (*#(+(y, z), x) -> *#(x, y), *#(+(y, z), x) -> +#(*(x, y), *(x, z))) (*#(+(y, z), x) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z)) (*#(+(y, z), x) -> *#(x, y), *#(x, +(y, z)) -> *#(x, y)) (*#(+(y, z), x) -> *#(x, y), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z)) (*#(x, +(y, z)) -> *#(x, y), *#(+(y, z), x) -> +#(*(x, y), *(x, z))) (*#(x, +(y, z)) -> *#(x, y), *#(+(y, z), x) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, y), *#(+(y, z), x) -> *#(x, z)) (*#(x, +(y, z)) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z))) (*#(x, +(y, z)) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)) (*#(+(y, z), x) -> *#(x, z), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (*#(+(y, z), x) -> *#(x, z), *#(x, +(y, z)) -> *#(x, y)) (*#(+(y, z), x) -> *#(x, z), *#(x, +(y, z)) -> *#(x, z)) (*#(+(y, z), x) -> *#(x, z), *#(+(y, z), x) -> +#(*(x, y), *(x, z))) (*#(+(y, z), x) -> *#(x, z), *#(+(y, z), x) -> *#(x, y)) (*#(+(y, z), x) -> *#(x, z), *#(+(y, z), x) -> *#(x, z)) (*#(+(y, z), x) -> *#(x, z), *#(*(x, y), z) -> *#(x, *(y, z))) (*#(+(y, z), x) -> *#(x, z), *#(*(x, y), z) -> *#(y, z)) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z)) (*#(+(y, z), x) -> +#(*(x, y), *(x, z)), +#(+(x, y), z) -> +#(x, +(y, z))) (*#(+(y, z), x) -> +#(*(x, y), *(x, 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.440000 SCCS (2): Scc: {*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z), *#(+(y, z), x) -> *#(x, y), *#(+(y, z), x) -> *#(x, z), *#(*(x, y), z) -> *#(x, *(y, z)), *#(*(x, y), z) -> *#(y, z)} Scc: {+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z)} SCC (6): Strict: {*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z), *#(+(y, z), x) -> *#(x, y), *#(+(y, z), x) -> *#(x, z), *#(*(x, y), z) -> *#(x, *(y, z)), *#(*(x, y), z) -> *#(y, z)} Weak: {+(+(x, y), z) -> +(x, +(y, z)), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(+(y, z), x) -> +(*(x, y), *(x, z)), *(*(x, y), z) -> *(x, *(y, z))} Open SCC (2): Strict: {+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z)} Weak: {+(+(x, y), z) -> +(x, +(y, z)), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(+(y, z), x) -> +(*(x, y), *(x, z)), *(*(x, y), z) -> *(x, *(y, z))} Open