%------------------------------------------------------------------------------ % File : Moca---0.1 % Problem : BOO002-1 : TPTP v8.1.0. Released v1.0.0. % Transfm : none % Format : tptp:raw % Command : moca.sh %s % Computer : n019.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Thu Jul 14 23:46:11 EDT 2022 % Result : Unsatisfiable 71.17s 71.22s % Output : Proof 71.17s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : BOO002-1 : TPTP v8.1.0. Released v1.0.0. % 0.12/0.13 % Command : moca.sh %s % 0.14/0.35 % Computer : n019.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 600 % 0.14/0.35 % DateTime : Wed Jun 1 19:39:55 EDT 2022 % 0.14/0.35 % CPUTime : % 71.17/71.22 % SZS status Unsatisfiable % 71.17/71.22 % SZS output start Proof % 71.17/71.22 The input problem is unsatisfiable because % 71.17/71.22 % 71.17/71.22 [1] the following set of Horn clauses is unsatisfiable: % 71.17/71.22 % 71.17/71.22 multiply(multiply(V, W, X), Y, multiply(V, W, Z)) = multiply(V, W, multiply(X, Y, Z)) % 71.17/71.22 multiply(Y, X, X) = X % 71.17/71.22 multiply(X, X, Y) = X % 71.17/71.22 multiply(inverse(Y), Y, X) = X % 71.17/71.22 multiply(a, inverse(a), b) = b ==> \bottom % 71.17/71.22 % 71.17/71.22 This holds because % 71.17/71.22 % 71.17/71.22 [2] the following E entails the following G (Claessen-Smallbone's transformation (2018)): % 71.17/71.22 % 71.17/71.22 E: % 71.17/71.22 f1(b) = false__ % 71.17/71.22 f1(multiply(a, inverse(a), b)) = true__ % 71.17/71.22 multiply(X, X, Y) = X % 71.17/71.22 multiply(Y, X, X) = X % 71.17/71.22 multiply(inverse(Y), Y, X) = X % 71.17/71.22 multiply(multiply(V, W, X), Y, multiply(V, W, Z)) = multiply(V, W, multiply(X, Y, Z)) % 71.17/71.22 G: % 71.17/71.22 true__ = false__ % 71.17/71.22 % 71.17/71.22 This holds because % 71.17/71.22 % 71.17/71.22 [3] E entails the following ordered TRS and the lhs and rhs of G join by the TRS: % 71.17/71.22 % 71.17/71.22 multiply(X1, Y0, multiply(Y2, Y3, Y0)) = multiply(Y0, multiply(X1, Y0, Y2), multiply(Y2, Y3, Y0)) % 71.17/71.22 multiply(X2, Y1, multiply(X3, multiply(X2, Y1, multiply(Y1, Y2, X3)), Y1)) = multiply(Y1, Y2, multiply(X2, Y1, X3)) % 71.17/71.22 multiply(X3, multiply(Y1, X2, multiply(Y1, Y2, X3)), Y1) = multiply(Y1, Y2, multiply(Y1, X2, X3)) % 71.17/71.22 multiply(X3, multiply(Y2, X2, multiply(Y1, Y2, X3)), Y2) = multiply(Y1, Y2, multiply(Y2, X2, X3)) % 71.17/71.22 multiply(Y0, X2, multiply(Y0, multiply(Y0, X2, X3), multiply(Y0, Y2, X3))) = multiply(Y0, Y2, multiply(Y0, X2, X3)) % 71.17/71.22 multiply(Y0, X2, multiply(Y0, multiply(Y0, X2, X3), multiply(Y2, Y0, X3))) = multiply(Y2, Y0, multiply(Y0, X2, X3)) % 71.17/71.22 multiply(Y0, X2, multiply(Y0, multiply(Y0, X2, multiply(Y1, Y0, X3)), X3)) = multiply(Y1, Y0, multiply(Y0, X2, X3)) % 71.17/71.22 multiply(Y0, Y1, multiply(X0, X1, multiply(X2, Y0, X4))) = multiply(multiply(X0, X1, X2), Y0, multiply(Y0, Y1, multiply(X0, X1, X4))) % 71.17/71.22 multiply(Y0, Y1, multiply(X0, Y3, multiply(X2, Y0, Y3))) = multiply(multiply(X0, Y3, X2), Y0, multiply(Y0, Y1, Y3)) % 71.17/71.22 multiply(Y0, Y1, multiply(X1, Y0, Y3)) = multiply(Y0, multiply(X1, Y0, Y3), multiply(Y0, Y1, Y3)) % 71.17/71.22 multiply(Y0, Y1, multiply(X1, Y1, Y3)) = multiply(Y1, multiply(X1, Y1, Y3), multiply(Y0, Y1, Y3)) % 71.17/71.22 multiply(Y0, Y1, multiply(X1, Y3, Y0)) = multiply(Y0, multiply(X1, Y3, Y0), multiply(Y0, Y1, Y3)) % 71.17/71.22 multiply(Y0, Y1, multiply(X1, Y3, Y1)) = multiply(Y1, multiply(X1, Y3, Y1), multiply(Y0, Y1, Y3)) % 71.17/71.22 multiply(Y0, Y1, multiply(X2, Y0, multiply(Y0, Y2, X3))) = multiply(Y0, Y2, multiply(Y0, Y1, multiply(X2, Y0, X3))) % 71.17/71.22 multiply(Y0, Y1, multiply(X2, Y1, multiply(Y1, Y2, X3))) = multiply(Y1, Y2, multiply(Y0, Y1, multiply(X2, Y1, X3))) % 71.17/71.22 multiply(Y0, Y1, multiply(X2, Y2, multiply(Y2, Y0, X3))) = multiply(Y2, Y0, multiply(Y0, Y1, multiply(X2, Y2, X3))) % 71.17/71.22 multiply(Y0, Y1, multiply(Y0, X1, Y3)) = multiply(Y0, multiply(Y0, X1, Y3), multiply(Y0, Y1, Y3)) % 71.17/71.22 multiply(Y0, Y1, multiply(Y0, X2, multiply(Y0, Y2, X3))) = multiply(Y0, Y2, multiply(Y0, Y1, multiply(Y0, X2, X3))) % 71.17/71.22 multiply(Y0, Y1, multiply(Y0, X2, multiply(Y2, Y0, X3))) = multiply(Y2, Y0, multiply(Y0, Y1, multiply(Y0, X2, X3))) % 71.17/71.22 multiply(Y0, Y1, multiply(Y1, X1, Y3)) = multiply(Y1, multiply(Y1, X1, Y3), multiply(Y0, Y1, Y3)) % 71.17/71.22 multiply(Y0, Y1, multiply(Y1, X2, multiply(Y1, Y2, X3))) = multiply(Y1, Y2, multiply(Y0, Y1, multiply(Y1, X2, X3))) % 71.17/71.22 multiply(Y0, Y1, multiply(Y2, X2, multiply(Y0, Y2, X3))) = multiply(Y0, Y2, multiply(Y0, Y1, multiply(Y2, X2, X3))) % 71.17/71.22 multiply(Y0, Y1, multiply(Y2, X2, multiply(Y1, Y2, X3))) = multiply(Y1, Y2, multiply(Y0, Y1, multiply(Y2, X2, X3))) % 71.17/71.22 multiply(Y0, Y1, multiply(Y2, X2, multiply(Y2, Y0, X3))) = multiply(Y2, Y0, multiply(Y0, Y1, multiply(Y2, X2, X3))) % 71.17/71.22 multiply(Y0, Y1, multiply(Y3, X1, multiply(X2, Y0, Y3))) = multiply(multiply(Y3, X1, X2), Y0, multiply(Y0, Y1, Y3)) % 71.17/71.22 multiply(Y0, Y1, multiply(Y3, X2, Y0)) = multiply(Y0, multiply(Y3, X2, Y0), multiply(Y0, Y1, Y3)) % 71.17/71.22 multiply(Y0, Y1, multiply(Y3, X2, Y1)) = multiply(Y1, multiply(Y3, X2, Y1), multiply(Y0, Y1, Y3)) % 71.17/71.22 multiply(Y0, multiply(X0, X1, X2), multiply(X0, X1, multiply(X2, Y2, X4))) = multiply(multiply(X0, X1, X2), Y2, multiply(Y0, multiply(X0, X1, X2), multiply(X0, X1, X4))) % 71.17/71.22 multiply(Y0, multiply(X0, Y3, X2), multiply(X0, Y3, multiply(X2, Y2, Y3))) = multiply(multiply(X0, Y3, X2), Y2, multiply(Y0, multiply(X0, Y3, X2), Y3)) % 71.17/71.22 multiply(Y0, multiply(X2, Y0, X3), multiply(X2, Y0, multiply(Y0, Y2, X3))) = multiply(Y0, Y2, multiply(X2, Y0, X3)) % 71.17/71.22 multiply(Y0, multiply(X2, Y1, multiply(Y1, Y0, X3)), multiply(X2, Y1, X3)) = multiply(Y1, Y0, multiply(X2, Y1, X3)) % 71.17/71.22 multiply(Y0, multiply(X2, Y2, X3), multiply(X2, Y2, multiply(Y2, Y0, X3))) = multiply(Y2, Y0, multiply(X2, Y2, X3)) % 71.17/71.22 multiply(Y0, multiply(X2, Y3, X3), multiply(Y2, Y0, multiply(X2, Y3, multiply(Y3, Y0, X3)))) = multiply(Y2, Y0, multiply(Y3, Y0, multiply(X2, Y3, X3))) % 71.17/71.22 multiply(Y0, multiply(Y0, X2, X3), multiply(Y0, X2, multiply(Y2, Y0, X3))) = multiply(Y2, Y0, multiply(Y0, X2, X3)) % 71.17/71.22 multiply(Y0, multiply(Y1, X2, multiply(Y1, Y0, X3)), multiply(Y1, X2, X3)) = multiply(Y1, Y0, multiply(Y1, X2, X3)) % 71.17/71.22 multiply(Y0, multiply(Y2, X2, X3), multiply(Y2, X2, multiply(Y2, Y0, X3))) = multiply(Y2, Y0, multiply(Y2, X2, X3)) % 71.17/71.22 multiply(Y0, multiply(Y2, X2, Y0), multiply(X2, Y3, Y0)) = multiply(Y0, multiply(Y2, X2, Y0), multiply(Y2, Y3, Y0)) % 71.17/71.22 multiply(Y0, multiply(Y3, X1, X2), multiply(Y3, X1, multiply(X2, Y2, Y3))) = multiply(multiply(Y3, X1, X2), Y2, multiply(Y0, multiply(Y3, X1, X2), Y3)) % 71.17/71.22 multiply(Y2, X2, multiply(X3, multiply(Y2, X2, multiply(Y1, Y2, X3)), Y2)) = multiply(Y1, Y2, multiply(Y2, X2, X3)) % 71.17/71.22 multiply(Y2, Y3, multiply(Y0, Y2, Y4)) = multiply(Y0, Y2, multiply(Y2, Y3, Y4)) % 71.17/71.22 multiply(Y2, Y3, multiply(Y2, Y1, Y4)) = multiply(Y2, Y1, multiply(Y2, Y3, Y4)) % 71.17/71.22 multiply(Y2, multiply(X2, X3, Y2), multiply(multiply(X2, X3, Y2), Y1, multiply(Y1, Y2, X3))) = multiply(Y1, Y2, multiply(X2, X3, Y2)) % 71.17/71.22 multiply(multiply(Y2, X2, X3), multiply(Y2, X2, multiply(Y1, Y2, X3)), Y1) = multiply(Y1, Y2, multiply(Y2, X2, X3)) % 71.17/71.22 f1(b) -> false__ % 71.17/71.22 f1(multiply(a, inverse(a), b)) -> true__ % 71.17/71.22 multiply(X, X, Y) -> X % 71.17/71.22 multiply(X0, X1, multiply(X2, multiply(X0, X1, X4), multiply(X2, Y2, X4))) -> multiply(X0, X1, multiply(X2, Y2, X4)) % 71.17/71.22 multiply(X0, X1, multiply(X4, multiply(X0, X1, X2), multiply(X2, Y2, X4))) -> multiply(X0, X1, multiply(X2, Y2, X4)) % 71.17/71.22 multiply(X2, multiply(Y1, Y2, X2), multiply(X3, Y1, multiply(Y1, Y2, X2))) -> multiply(Y1, Y2, X2) % 71.17/71.22 multiply(X2, multiply(Y2, Y1, X2), multiply(X3, Y1, multiply(Y2, Y1, X2))) -> multiply(Y2, Y1, X2) % 71.17/71.22 multiply(Y, X, X) -> X % 71.17/71.22 multiply(Y0, X1, multiply(Y0, multiply(Y0, X1, X2), multiply(X2, Y2, Y0))) -> multiply(Y0, X1, multiply(X2, Y2, Y0)) % 71.17/71.22 multiply(Y0, X2, multiply(Y0, Y1, multiply(multiply(Y0, X2, multiply(Y0, Y1, X3)), Y0, X3))) -> multiply(Y0, Y1, multiply(Y0, X2, X3)) % 71.17/71.22 multiply(Y0, X2, multiply(Y0, multiply(Y0, X2, multiply(Y0, Y1, X3)), X3)) -> multiply(Y0, Y1, multiply(Y0, X2, X3)) % 71.17/71.22 multiply(Y0, Y1, multiply(X0, Y1, multiply(X2, Y0, Y1))) -> multiply(X0, Y1, multiply(X2, Y0, Y1)) % 71.17/71.22 multiply(Y0, Y1, multiply(X0, Y3, multiply(X2, multiply(Y0, Y1, Y3), Y3))) -> multiply(Y0, Y1, Y3) % 71.17/71.22 multiply(Y0, Y1, multiply(X0, Y3, multiply(X2, multiply(Y0, Y1, multiply(X0, Y3, X2)), Y3))) -> multiply(Y0, Y1, multiply(X0, Y3, X2)) % 71.17/71.22 multiply(Y0, Y1, multiply(X1, Y1, Y0)) -> multiply(X1, Y1, Y0) % 71.17/71.22 multiply(Y0, Y1, multiply(X2, Y0, multiply(X3, Y3, multiply(Y0, Y1, X3)))) -> multiply(Y0, Y1, multiply(X2, Y0, X3)) % 71.17/71.22 multiply(Y0, Y1, multiply(X2, Y0, multiply(Y0, Y1, X3))) -> multiply(Y0, Y1, multiply(X2, Y0, X3)) % 71.17/71.22 multiply(Y0, Y1, multiply(X2, Y0, multiply(multiply(Y0, Y1, X3), Y0, X3))) -> multiply(Y0, Y1, multiply(X2, Y0, X3)) % 71.17/71.22 multiply(Y0, Y1, multiply(X2, Y0, multiply(multiply(Y0, Y1, X3), Y3, X3))) -> multiply(Y0, Y1, multiply(X2, Y0, X3)) % 71.17/71.22 multiply(Y0, Y1, multiply(X2, Y1, multiply(Y0, Y3, Y1))) -> multiply(X2, Y1, multiply(Y0, Y3, Y1)) % 71.17/71.22 multiply(Y0, Y1, multiply(X2, Y2, multiply(Y0, Y1, Y2))) -> multiply(Y0, Y1, Y2) % 71.17/71.22 multiply(Y0, Y1, multiply(X2, Y2, multiply(Y2, multiply(Y0, Y1, Y2), X3))) -> multiply(Y0, Y1, Y2) % 71.17/71.22 multiply(Y0, Y1, multiply(X2, Y2, multiply(Y2, multiply(Y0, Y1, multiply(X2, Y2, X3)), X3))) -> multiply(Y0, Y1, multiply(X2, Y2, X3)) % 71.17/71.22 multiply(Y0, Y1, multiply(Y0, X2, multiply(X3, Y3, multiply(Y0, Y1, X3)))) -> multiply(Y0, Y1, multiply(Y0, X2, X3)) % 71.17/71.22 multiply(Y0, Y1, multiply(Y0, X2, multiply(Y0, Y1, X3))) -> multiply(Y0, Y1, multiply(Y0, X2, X3)) % 71.17/71.22 multiply(Y0, Y1, multiply(Y0, X2, multiply(multiply(Y0, Y1, X3), Y3, X3))) -> multiply(Y0, Y1, multiply(Y0, X2, X3)) % 71.17/71.22 multiply(Y0, Y1, multiply(Y0, Y1, Y3)) -> multiply(Y0, Y1, Y3) % 71.17/71.22 multiply(Y0, Y1, multiply(Y2, X2, multiply(Y0, Y1, Y2))) -> multiply(Y0, Y1, Y2) % 71.17/71.22 multiply(Y0, Y1, multiply(Y2, X2, multiply(Y2, multiply(Y0, Y1, Y2), X3))) -> multiply(Y0, Y1, Y2) % 71.17/71.22 multiply(Y0, Y1, multiply(Y2, X2, multiply(Y2, multiply(Y0, Y1, multiply(Y2, X2, X3)), X3))) -> multiply(Y0, Y1, multiply(Y2, X2, X3)) % 71.17/71.22 multiply(Y0, Y1, multiply(Y2, Y3, multiply(Y0, Y1, X2))) -> multiply(Y0, Y1, multiply(Y2, Y3, X2)) % 71.17/71.22 multiply(Y0, Y1, multiply(Y2, inverse(multiply(Y0, Y1, Y2)), Y0)) -> Y0 % 71.17/71.22 multiply(Y0, Y1, multiply(Y2, inverse(multiply(Y0, Y1, Y2)), Y1)) -> Y1 % 71.17/71.22 multiply(Y0, Y1, multiply(Y2, multiply(X1, Y0, multiply(Y0, Y1, Y2)), Y0)) -> multiply(X1, Y0, multiply(Y0, Y1, Y2)) % 71.17/71.22 multiply(Y0, Y1, multiply(Y2, multiply(X1, Y1, multiply(Y0, Y1, Y2)), Y1)) -> multiply(X1, Y1, multiply(Y0, Y1, Y2)) % 71.17/71.22 multiply(Y0, Y1, multiply(Y2, multiply(X1, multiply(Y0, Y1, Y2), Y0), Y0)) -> multiply(X1, multiply(Y0, Y1, Y2), Y0) % 71.17/71.22 multiply(Y0, Y1, multiply(Y2, multiply(X1, multiply(Y0, Y1, Y2), Y1), Y1)) -> multiply(X1, multiply(Y0, Y1, Y2), Y1) % 71.17/71.22 multiply(Y0, Y1, multiply(Y2, multiply(X2, Y0, X3), multiply(X2, Y0, multiply(Y0, Y1, X3)))) -> multiply(Y0, Y1, multiply(X2, Y0, X3)) % 71.17/71.22 multiply(Y0, Y1, multiply(Y2, multiply(X2, Y0, multiply(Y0, Y1, X3)), multiply(X2, Y0, X3))) -> multiply(Y0, Y1, multiply(X2, Y0, X3)) % 71.17/71.22 multiply(Y0, Y1, multiply(Y2, multiply(X2, multiply(Y0, Y1, X2), X3), X2)) -> multiply(Y0, Y1, X2) % 71.17/71.22 multiply(Y0, Y1, multiply(Y2, multiply(X2, multiply(Y0, Y1, X3), X3), X3)) -> multiply(Y0, Y1, X3) % 71.17/71.22 multiply(Y0, Y1, multiply(Y2, multiply(Y0, X2, X3), multiply(Y0, X2, multiply(Y0, Y1, X3)))) -> multiply(Y0, Y1, multiply(Y0, X2, X3)) % 71.17/71.22 multiply(Y0, Y1, multiply(Y2, multiply(Y0, X2, multiply(Y0, Y1, X3)), multiply(Y0, X2, X3))) -> multiply(Y0, Y1, multiply(Y0, X2, X3)) % 71.17/71.22 multiply(Y0, Y1, multiply(Y2, multiply(Y0, X2, multiply(Y0, Y1, Y2)), Y0)) -> multiply(Y0, X2, multiply(Y0, Y1, Y2)) % 71.17/71.22 multiply(Y0, Y1, multiply(Y2, multiply(Y0, Y1, X2), multiply(X2, X3, multiply(Y0, Y1, X2)))) -> multiply(Y0, Y1, X2) % 71.17/71.22 multiply(Y0, Y1, multiply(Y2, multiply(Y0, Y1, X2), multiply(X2, multiply(Y0, Y1, X2), X3))) -> multiply(Y0, Y1, X2) % 71.17/71.22 multiply(Y0, Y1, multiply(Y2, multiply(Y0, Y1, X2), multiply(multiply(Y0, Y1, X2), X3, X2))) -> multiply(Y0, Y1, X2) % 71.17/71.22 multiply(Y0, Y1, multiply(Y2, multiply(Y0, Y1, X2), multiply(multiply(Y0, Y1, X2), Y0, X2))) -> multiply(Y0, Y1, X2) % 71.17/71.22 multiply(Y0, Y1, multiply(Y2, multiply(Y0, Y1, X3), multiply(X2, X3, multiply(Y0, Y1, X3)))) -> multiply(Y0, Y1, X3) % 71.17/71.22 multiply(Y0, Y1, multiply(Y2, multiply(Y0, Y1, X3), multiply(X2, multiply(Y0, Y1, X3), X3))) -> multiply(Y0, Y1, X3) % 71.17/71.22 multiply(Y0, Y1, multiply(Y2, multiply(Y0, Y1, Y2), Y4)) -> multiply(Y0, Y1, Y2) % 71.17/71.22 multiply(Y0, Y1, multiply(Y2, multiply(Y0, Y1, Y4), Y4)) -> multiply(Y0, Y1, Y4) % 71.17/71.22 multiply(Y0, Y1, multiply(Y2, multiply(Y0, Y1, multiply(Y2, X1, Y1)), Y1)) -> multiply(Y0, Y1, multiply(Y2, X1, Y1)) % 71.17/71.22 multiply(Y0, Y1, multiply(Y2, multiply(Y1, X2, X3), multiply(Y1, X2, multiply(Y0, Y1, X3)))) -> multiply(Y0, Y1, multiply(Y1, X2, X3)) % 71.17/71.22 multiply(Y0, Y1, multiply(Y2, multiply(Y1, X2, multiply(Y0, Y1, X3)), multiply(Y1, X2, X3))) -> multiply(Y0, Y1, multiply(Y1, X2, X3)) % 71.17/71.22 multiply(Y0, Y1, multiply(Y2, multiply(Y1, X2, multiply(Y0, Y1, Y2)), Y1)) -> multiply(Y1, X2, multiply(Y0, Y1, Y2)) % 71.17/71.22 multiply(Y0, Y1, multiply(Y3, X1, multiply(X2, multiply(Y0, Y1, Y3), Y3))) -> multiply(Y0, Y1, Y3) % 71.17/71.22 multiply(Y0, Y1, multiply(Y3, X1, multiply(X2, multiply(Y0, Y1, multiply(Y3, X1, X2)), Y3))) -> multiply(Y0, Y1, multiply(Y3, X1, X2)) % 71.17/71.22 multiply(Y0, Y1, multiply(Y3, X2, multiply(multiply(Y0, Y1, multiply(Y3, X2, X3)), Y3, X3))) -> multiply(Y0, Y1, multiply(Y3, X2, X3)) % 71.17/71.22 multiply(Y0, Y1, multiply(multiply(X2, X3, Y0), Y1, multiply(X3, Y3, Y1))) -> multiply(Y0, Y1, multiply(X3, Y3, Y1)) % 71.17/71.22 multiply(Y0, Y1, multiply(multiply(X2, X3, multiply(Y0, Y1, X3)), multiply(Y0, Y1, X3), Y3)) -> multiply(Y0, Y1, X3) % 71.17/71.22 multiply(Y0, Y1, multiply(multiply(X2, Y0, X3), multiply(X2, Y0, multiply(Y0, Y1, X3)), Y3)) -> multiply(Y0, Y1, multiply(X2, Y0, X3)) % 71.17/71.22 multiply(Y0, Y1, multiply(multiply(X2, Y0, Y1), Y3, Y1)) -> multiply(multiply(X2, Y0, Y1), Y3, Y1) % 71.17/71.22 multiply(Y0, Y1, multiply(multiply(X2, Y1, Y0), Y3, Y0)) -> multiply(multiply(X2, Y1, Y0), Y3, Y0) % 71.17/71.22 multiply(Y0, Y1, multiply(multiply(X2, multiply(Y0, Y1, X2), X3), Y3, Y0)) -> multiply(Y0, Y1, multiply(X2, Y3, Y0)) % 71.17/71.22 multiply(Y0, Y1, multiply(multiply(X2, multiply(Y0, Y1, X2), X3), Y3, Y1)) -> multiply(Y0, Y1, multiply(X2, Y3, Y1)) % 71.17/71.22 multiply(Y0, Y1, multiply(multiply(X2, multiply(Y0, Y1, X2), X3), multiply(Y0, Y1, X2), Y3)) -> multiply(Y0, Y1, X2) % 71.17/71.22 multiply(Y0, Y1, multiply(multiply(X2, multiply(Y0, Y1, X3), X3), Y3, X3)) -> multiply(Y0, Y1, X3) % 71.17/71.22 multiply(Y0, Y1, multiply(multiply(X2, multiply(Y0, Y1, X3), X3), Y3, Y0)) -> multiply(Y0, Y1, multiply(X3, Y3, Y0)) % 71.17/71.22 multiply(Y0, Y1, multiply(multiply(X2, multiply(Y0, Y1, X3), X3), Y3, Y1)) -> multiply(Y0, Y1, multiply(X3, Y3, Y1)) % 71.17/71.22 multiply(Y0, Y1, multiply(multiply(X2, multiply(Y0, Y1, X3), X3), multiply(Y0, Y1, X3), Y3)) -> multiply(Y0, Y1, X3) % 71.17/71.22 multiply(Y0, Y1, multiply(multiply(Y0, X2, X3), multiply(Y0, X2, multiply(Y0, Y1, X3)), Y3)) -> multiply(Y0, Y1, multiply(Y0, X2, X3)) % 71.17/71.22 multiply(Y0, Y1, multiply(multiply(Y0, X2, Y1), Y3, Y1)) -> multiply(multiply(Y0, X2, Y1), Y3, Y1) % 71.17/71.22 multiply(Y0, Y1, multiply(multiply(Y0, Y1, X2), Y3, Y4)) -> multiply(Y0, Y1, multiply(X2, Y3, Y4)) % 71.17/71.22 multiply(Y0, Y1, multiply(multiply(Y0, Y1, Y2), X2, Y2)) -> multiply(Y0, Y1, Y2) % 71.17/71.22 multiply(Y0, Y1, multiply(multiply(Y1, X2, X3), multiply(Y1, X2, multiply(Y0, Y1, X3)), Y3)) -> multiply(Y0, Y1, multiply(Y1, X2, X3)) % 71.17/71.22 multiply(Y0, Y1, multiply(multiply(Y1, X2, Y0), Y3, Y0)) -> multiply(multiply(Y1, X2, Y0), Y3, Y0) % 71.17/71.22 multiply(Y0, Y1, multiply(multiply(multiply(Y0, Y1, X2), X3, X2), Y3, Y1)) -> multiply(Y0, Y1, multiply(X2, Y3, Y1)) % 71.17/71.22 multiply(Y0, Y1, multiply(multiply(multiply(Y0, Y1, X2), Y0, X2), Y3, Y1)) -> multiply(Y0, Y1, multiply(X2, Y3, Y1)) % 71.17/71.22 multiply(Y0, Y1, multiply(multiply(multiply(Y0, Y1, X2), Y0, X2), multiply(Y0, Y1, X2), Y3)) -> multiply(Y0, Y1, X2) % 71.17/71.22 multiply(Y0, Y2, multiply(Y0, Y1, multiply(X2, X3, multiply(Y0, Y2, X3)))) -> multiply(Y0, Y1, multiply(Y0, Y2, X3)) % 71.17/71.22 multiply(Y0, Y2, multiply(Y0, Y1, multiply(X2, Y0, Y2))) -> multiply(Y0, Y1, multiply(X2, Y0, Y2)) % 71.17/71.22 multiply(Y0, Y2, multiply(Y0, Y1, multiply(X2, Y2, Y0))) -> multiply(Y0, Y1, multiply(X2, Y2, Y0)) % 71.17/71.22 multiply(Y0, Y2, multiply(Y0, Y1, multiply(X2, multiply(Y0, Y2, X2), X3))) -> multiply(Y0, Y1, multiply(Y0, Y2, X2)) % 71.17/71.22 multiply(Y0, Y2, multiply(Y0, Y1, multiply(X2, multiply(Y0, Y2, X3), X3))) -> multiply(Y0, Y1, multiply(Y0, Y2, X3)) % 71.17/71.22 multiply(Y0, Y2, multiply(Y0, Y1, multiply(Y0, X2, Y2))) -> multiply(Y0, Y1, multiply(Y0, X2, Y2)) % 71.17/71.22 multiply(Y0, Y2, multiply(Y0, Y1, multiply(Y0, Y2, X2))) -> multiply(Y0, Y1, multiply(Y0, Y2, X2)) % 71.17/71.22 multiply(Y0, Y2, multiply(Y0, Y1, multiply(Y2, X2, Y0))) -> multiply(Y0, Y1, multiply(Y2, X2, Y0)) % 71.17/71.22 multiply(Y0, Y2, multiply(Y0, Y1, multiply(multiply(Y0, Y2, X2), Y0, X2))) -> multiply(Y0, Y1, multiply(Y0, Y2, X2)) % 71.17/71.22 multiply(Y0, Y2, multiply(Y0, multiply(X1, Y0, multiply(Y0, Y2, Y3)), Y3)) -> multiply(X1, Y0, multiply(Y0, Y2, Y3)) % 71.17/71.22 multiply(Y0, Y2, multiply(Y0, multiply(X1, multiply(Y0, Y2, Y3), Y0), Y3)) -> multiply(X1, multiply(Y0, Y2, Y3), Y0) % 71.17/71.22 multiply(Y0, Y2, multiply(Y0, multiply(Y0, X1, multiply(Y0, Y2, Y3)), Y3)) -> multiply(Y0, X1, multiply(Y0, Y2, Y3)) % 71.17/71.22 multiply(Y0, Y2, multiply(Y0, multiply(Y0, Y2, X2), multiply(Y0, multiply(X2, X3, multiply(Y0, Y2, X2)), X2))) -> multiply(Y0, Y2, X2) % 71.17/71.22 multiply(Y0, Y2, multiply(Y0, multiply(Y0, Y2, X2), multiply(Y0, multiply(X2, multiply(Y0, Y2, X2), X3), X2))) -> multiply(Y0, Y2, X2) % 71.17/71.22 multiply(Y0, Y2, multiply(Y0, multiply(Y0, Y2, X2), multiply(Y0, multiply(multiply(Y0, Y2, X2), X3, X2), X2))) -> multiply(Y0, Y2, X2) % 71.17/71.22 multiply(Y0, Y2, multiply(Y0, multiply(Y0, Y2, X2), multiply(Y0, multiply(multiply(Y0, Y2, X2), Y0, X2), X2))) -> multiply(Y0, Y2, X2) % 71.17/71.22 multiply(Y0, Y2, multiply(Y0, multiply(Y0, Y2, X3), multiply(Y0, multiply(X2, X3, multiply(Y0, Y2, X3)), X3))) -> multiply(Y0, Y2, X3) % 71.17/71.22 multiply(Y0, Y2, multiply(Y0, multiply(Y0, Y2, X3), multiply(Y0, multiply(X2, multiply(Y0, Y2, X3), X3), X3))) -> multiply(Y0, Y2, X3) % 71.17/71.22 multiply(Y0, Y2, multiply(Y0, multiply(Y0, Y2, multiply(Y3, X2, Y0)), Y3)) -> multiply(Y0, Y2, multiply(Y3, X2, Y0)) % 71.17/71.22 multiply(Y0, Y3, multiply(Y1, multiply(X2, Y0, Y3), Y0)) -> multiply(Y1, multiply(X2, Y0, Y3), Y0) % 71.17/71.22 multiply(Y0, Y3, multiply(Y1, multiply(Y0, Y3, X2), Y0)) -> multiply(Y1, multiply(Y0, Y3, X2), Y0) % 71.17/71.22 multiply(Y0, Y3, multiply(Y1, multiply(Y3, X2, Y0), Y0)) -> multiply(Y1, multiply(Y3, X2, Y0), Y0) % 71.17/71.22 multiply(Y0, multiply(X0, X1, X4), multiply(X0, X1, multiply(X2, Y0, X4))) -> multiply(X0, X1, multiply(X2, Y0, X4)) % 71.17/71.22 multiply(Y0, multiply(X0, Y0, X2), multiply(X0, Y0, multiply(X2, Y2, Y0))) -> multiply(X0, Y0, multiply(X2, Y2, Y0)) % 71.17/71.22 multiply(Y0, multiply(X0, Y0, X2), multiply(Y0, multiply(X0, Y0, multiply(X2, Y2, Y0)), X2)) -> multiply(X0, Y0, multiply(X2, Y2, Y0)) % 71.17/71.22 multiply(Y0, multiply(X0, Y0, multiply(X2, Y2, Y0)), Y2) -> multiply(X0, Y0, multiply(X2, Y2, Y0)) % 71.17/71.22 multiply(Y0, multiply(X0, Y2, multiply(X2, Y0, Y2)), Y2) -> multiply(X0, Y2, multiply(X2, Y0, Y2)) % 71.17/71.22 multiply(Y0, multiply(X1, Y0, X2), multiply(X1, X2, Y0)) -> multiply(X1, X2, Y0) % 71.17/71.22 multiply(Y0, multiply(X1, Y0, Y1), Y1) -> multiply(X1, Y0, Y1) % 71.17/71.22 multiply(Y0, multiply(X1, Y0, Y2), multiply(Y2, Y3, multiply(X1, Y0, Y2))) -> multiply(X1, Y0, Y2) % 71.17/71.22 multiply(Y0, multiply(X1, Y0, Y2), multiply(Y2, multiply(X1, Y0, Y2), Y3)) -> multiply(X1, Y0, Y2) % 71.17/71.22 multiply(Y0, multiply(X1, Y0, Y3), multiply(Y2, Y3, multiply(X1, Y0, Y3))) -> multiply(X1, Y0, Y3) % 71.17/71.22 multiply(Y0, multiply(X1, Y0, Y3), multiply(Y2, multiply(X1, Y0, Y3), Y3)) -> multiply(X1, Y0, Y3) % 71.17/71.22 multiply(Y0, multiply(X1, Y2, Y0), multiply(Y2, Y3, multiply(X1, Y2, Y0))) -> multiply(X1, Y2, Y0) % 71.17/71.22 multiply(Y0, multiply(X1, Y2, Y0), multiply(Y2, multiply(X1, Y2, Y0), Y3)) -> multiply(X1, Y2, Y0) % 71.17/71.22 multiply(Y0, multiply(X1, Y3, Y0), multiply(Y2, multiply(X1, Y3, Y0), Y3)) -> multiply(X1, Y3, Y0) % 71.17/71.22 multiply(Y0, multiply(X2, X3, multiply(Y2, Y0, X2)), multiply(Y2, Y0, X2)) -> multiply(Y2, Y0, X2) % 71.17/71.22 multiply(Y0, multiply(X2, X3, multiply(Y2, Y0, X3)), multiply(Y2, Y0, X3)) -> multiply(Y2, Y0, X3) % 71.17/71.22 multiply(Y0, multiply(X2, Y0, multiply(Y0, Y1, X3)), multiply(X2, Y0, X3)) -> multiply(Y0, Y1, multiply(X2, Y0, X3)) % 71.17/71.22 multiply(Y0, multiply(X2, Y3, X3), multiply(X2, Y3, multiply(X3, Y2, multiply(Y3, Y0, X3)))) -> multiply(X2, Y3, multiply(X3, Y2, multiply(Y3, Y0, X3))) % 71.17/71.22 multiply(Y0, multiply(X2, multiply(Y2, Y0, X2), X3), multiply(Y2, Y0, X2)) -> multiply(Y2, Y0, X2) % 71.17/71.22 multiply(Y0, multiply(X2, multiply(Y2, Y0, X3), X3), multiply(Y2, Y0, X3)) -> multiply(Y2, Y0, X3) % 71.17/71.22 multiply(Y0, multiply(Y0, X1, Y2), multiply(Y2, Y3, Y0)) -> multiply(Y0, X1, multiply(Y2, Y3, Y0)) % 71.17/71.22 multiply(Y0, multiply(Y0, X1, Y2), multiply(Y2, Y3, multiply(Y0, X1, Y2))) -> multiply(Y0, X1, Y2) % 71.17/71.22 multiply(Y0, multiply(Y0, X1, Y2), multiply(Y2, multiply(Y0, X1, Y2), Y3)) -> multiply(Y0, X1, Y2) % 71.17/71.22 multiply(Y0, multiply(Y0, X1, Y3), multiply(Y2, Y3, multiply(Y0, X1, Y3))) -> multiply(Y0, X1, Y3) % 71.17/71.22 multiply(Y0, multiply(Y0, X1, Y3), multiply(Y2, multiply(Y0, X1, Y3), Y3)) -> multiply(Y0, X1, Y3) % 71.17/71.22 multiply(Y0, multiply(Y0, X1, multiply(X2, Y2, Y0)), Y2) -> multiply(Y0, X1, multiply(X2, Y2, Y0)) % 71.17/71.22 multiply(Y0, multiply(Y0, X2, Y1), Y1) -> multiply(Y0, X2, Y1) % 71.17/71.22 multiply(Y0, multiply(Y1, X2, multiply(Y0, Y1, X3)), multiply(Y1, X2, X3)) -> multiply(Y0, Y1, multiply(Y1, X2, X3)) % 71.17/71.22 multiply(Y0, multiply(Y2, X1, multiply(X2, Y0, Y2)), Y2) -> multiply(Y2, X1, multiply(X2, Y0, Y2)) % 71.17/71.22 multiply(Y0, multiply(Y2, X2, X3), multiply(Y2, X2, multiply(Y0, Y2, X3))) -> multiply(Y0, Y2, multiply(Y2, X2, X3)) % 71.17/71.22 multiply(Y0, multiply(Y2, X2, Y0), multiply(Y2, Y3, multiply(Y2, X2, Y0))) -> multiply(Y2, X2, Y0) % 71.17/71.22 multiply(Y0, multiply(Y2, X2, Y0), multiply(Y2, multiply(Y2, X2, Y0), Y3)) -> multiply(Y2, X2, Y0) % 71.17/71.22 multiply(Y0, multiply(Y2, Y3, Y0), Y3) -> multiply(Y2, Y3, Y0) % 71.17/71.22 multiply(Y0, multiply(Y2, Y3, Y0), multiply(Y0, multiply(X1, multiply(Y2, Y3, Y0), Y0), Y3)) -> multiply(X1, multiply(Y2, Y3, Y0), Y0) % 71.17/71.22 multiply(Y0, multiply(Y3, X2, X3), multiply(Y3, X2, multiply(X3, Y2, multiply(Y3, Y0, X3)))) -> multiply(Y3, X2, multiply(X3, Y2, multiply(Y3, Y0, X3))) % 71.17/71.22 multiply(Y0, multiply(Y3, X2, Y0), multiply(Y2, multiply(Y3, X2, Y0), Y3)) -> multiply(Y3, X2, Y0) % 71.17/71.22 multiply(Y0, multiply(multiply(Y2, Y0, X2), X3, X2), multiply(Y2, Y0, X2)) -> multiply(Y2, Y0, X2) % 71.17/71.22 multiply(Y0, multiply(multiply(Y2, Y0, X2), Y2, X2), multiply(Y2, Y0, X2)) -> multiply(Y2, Y0, X2) % 71.17/71.22 multiply(Y1, Y2, multiply(X2, X3, multiply(multiply(Y1, Y2, X2), Y1, X2))) -> multiply(Y1, Y2, X2) % 71.17/71.22 multiply(Y1, Y2, multiply(X2, X3, multiply(multiply(Y1, Y2, X3), Y1, X3))) -> multiply(Y1, Y2, X3) % 71.17/71.22 multiply(Y1, Y2, multiply(X2, multiply(X2, X3, multiply(Y1, Y2, X2)), multiply(X3, Y1, X2))) -> multiply(Y1, Y2, X2) % 71.17/71.22 multiply(Y1, Y2, multiply(Y0, Y1, multiply(X2, X3, multiply(Y1, Y2, X3)))) -> multiply(Y0, Y1, multiply(Y1, Y2, X3)) % 71.17/71.22 multiply(Y1, Y2, multiply(Y0, Y1, multiply(X2, Y1, Y2))) -> multiply(Y0, Y1, multiply(X2, Y1, Y2)) % 71.17/71.22 multiply(Y1, Y2, multiply(Y0, Y1, multiply(X2, Y2, Y1))) -> multiply(Y0, Y1, multiply(X2, Y2, Y1)) % 71.17/71.22 multiply(Y1, Y2, multiply(Y0, Y1, multiply(X2, multiply(Y1, Y2, X2), X3))) -> multiply(Y0, Y1, multiply(Y1, Y2, X2)) % 71.17/71.22 multiply(Y1, Y2, multiply(Y0, Y1, multiply(X2, multiply(Y1, Y2, X3), X3))) -> multiply(Y0, Y1, multiply(Y1, Y2, X3)) % 71.17/71.22 multiply(Y1, Y2, multiply(Y0, Y1, multiply(Y1, X2, Y2))) -> multiply(Y0, Y1, multiply(Y1, X2, Y2)) % 71.17/71.22 multiply(Y1, Y2, multiply(Y0, Y1, multiply(Y1, Y2, X2))) -> multiply(Y0, Y1, multiply(Y1, Y2, X2)) % 71.17/71.22 multiply(Y1, Y2, multiply(Y0, Y1, multiply(Y2, X2, Y1))) -> multiply(Y0, Y1, multiply(Y2, X2, Y1)) % 71.17/71.22 multiply(Y1, Y2, multiply(multiply(Y1, Y2, Y3), Y1, Y3)) -> multiply(Y1, Y2, Y3) % 71.17/71.22 multiply(Y1, Y3, Y1) -> Y1 % 71.17/71.22 multiply(Y1, Y3, multiply(Y0, Y1, Y3)) -> multiply(Y0, Y1, Y3) % 71.17/71.22 multiply(Y1, inverse(Y1), Y2) -> Y2 % 71.17/71.22 multiply(Y1, multiply(Y2, Y3, Y1), multiply(Y2, Y1, Y3)) -> multiply(Y2, Y3, Y1) % 71.17/71.22 multiply(Y2, Y0, multiply(Y0, Y1, multiply(X2, X3, multiply(Y2, Y0, X2)))) -> multiply(Y0, Y1, multiply(Y2, Y0, X2)) % 71.17/71.22 multiply(Y2, Y0, multiply(Y0, Y1, multiply(X2, X3, multiply(Y2, Y0, X3)))) -> multiply(Y0, Y1, multiply(Y2, Y0, X3)) % 71.17/71.22 multiply(Y2, Y0, multiply(Y0, Y1, multiply(X2, Y0, Y2))) -> multiply(Y0, Y1, multiply(X2, Y0, Y2)) % 71.17/71.22 multiply(Y2, Y0, multiply(Y0, Y1, multiply(X2, Y2, Y0))) -> multiply(Y0, Y1, multiply(X2, Y2, Y0)) % 71.17/71.22 multiply(Y2, Y0, multiply(Y0, Y1, multiply(X2, multiply(Y2, Y0, X2), X3))) -> multiply(Y0, Y1, multiply(Y2, Y0, X2)) % 71.17/71.22 multiply(Y2, Y0, multiply(Y0, Y1, multiply(X2, multiply(Y2, Y0, X3), X3))) -> multiply(Y0, Y1, multiply(Y2, Y0, X3)) % 71.17/71.22 multiply(Y2, Y0, multiply(Y0, Y1, multiply(Y0, X2, Y2))) -> multiply(Y0, Y1, multiply(Y0, X2, Y2)) % 71.17/71.22 multiply(Y2, Y0, multiply(Y0, Y1, multiply(Y0, X2, multiply(X3, Y2, Y0)))) -> multiply(Y0, Y1, multiply(Y0, X2, multiply(X3, Y2, Y0))) % 71.17/71.22 multiply(Y2, Y0, multiply(Y0, Y1, multiply(Y2, X2, Y0))) -> multiply(Y0, Y1, multiply(Y2, X2, Y0)) % 71.17/71.22 multiply(Y2, Y0, multiply(Y0, Y1, multiply(Y2, Y0, X2))) -> multiply(Y0, Y1, multiply(Y2, Y0, X2)) % 71.17/71.22 multiply(Y2, Y0, multiply(Y0, Y1, multiply(multiply(Y2, Y0, X2), X3, X2))) -> multiply(Y0, Y1, multiply(Y2, Y0, X2)) % 71.17/71.22 multiply(Y2, Y0, multiply(Y0, Y1, multiply(multiply(Y2, Y0, X2), Y2, X2))) -> multiply(Y0, Y1, multiply(Y2, Y0, X2)) % 71.17/71.22 multiply(Y2, Y0, multiply(Y0, multiply(X1, Y0, multiply(Y2, Y0, Y3)), Y3)) -> multiply(X1, Y0, multiply(Y2, Y0, Y3)) % 71.17/71.22 multiply(Y2, Y0, multiply(Y0, multiply(X1, multiply(Y2, Y0, Y3), Y0), Y3)) -> multiply(X1, multiply(Y2, Y0, Y3), Y0) % 71.17/71.22 multiply(Y2, Y0, multiply(Y0, multiply(Y0, X1, multiply(Y2, Y0, Y3)), Y3)) -> multiply(Y0, X1, multiply(Y2, Y0, Y3)) % 71.17/71.22 multiply(Y2, Y0, multiply(Y0, multiply(Y2, Y0, multiply(Y3, X2, Y0)), Y3)) -> multiply(Y2, Y0, multiply(Y3, X2, Y0)) % 71.17/71.22 multiply(Y2, Y1, multiply(Y2, Y3, Y1)) -> multiply(Y2, Y3, Y1) % 71.17/71.22 multiply(Y2, multiply(X1, Y2, Y3), multiply(Y3, multiply(X1, Y2, Y3), multiply(Y2, Y1, Y3))) -> multiply(X1, Y2, Y3) % 71.17/71.22 multiply(Y2, multiply(X1, Y3, Y2), multiply(X1, Y3, multiply(Y2, Y1, Y3))) -> multiply(X1, Y3, Y2) % 71.17/71.22 multiply(Y2, multiply(Y0, Y1, Y2), Y0) -> multiply(Y0, Y1, Y2) % 71.17/71.22 multiply(Y2, multiply(Y0, Y1, multiply(Y2, X1, Y0)), Y0) -> multiply(Y0, Y1, multiply(Y2, X1, Y0)) % 71.17/71.22 multiply(Y2, multiply(Y2, X1, Y3), multiply(Y3, multiply(Y2, X1, Y3), multiply(X1, Y1, Y3))) -> multiply(Y2, X1, Y3) % 71.17/71.22 multiply(Y2, multiply(Y3, X2, Y2), multiply(Y3, X2, multiply(Y2, Y1, Y3))) -> multiply(Y3, X2, Y2) % 71.17/71.22 multiply(Y3, X2, multiply(multiply(Y0, multiply(Y3, X2, X3), Y2), Y3, X3)) -> multiply(Y0, multiply(Y3, X2, X3), multiply(Y2, Y3, multiply(Y3, X2, X3))) % 71.17/71.22 multiply(Y3, X2, multiply(multiply(multiply(Y3, X2, X3), Y1, Y2), Y3, X3)) -> multiply(multiply(Y3, X2, X3), Y1, multiply(Y2, Y3, multiply(Y3, X2, X3))) % 71.17/71.22 multiply(Y3, Y0, multiply(Y0, Y1, Y3)) -> multiply(Y0, Y1, Y3) % 71.17/71.22 multiply(Y3, Y0, multiply(Y0, multiply(Y2, Y3, multiply(Y3, Y0, Y4)), multiply(Y2, Y3, Y4))) -> multiply(Y2, Y3, multiply(Y3, Y0, Y4)) % 71.17/71.22 multiply(Y3, Y0, multiply(Y1, multiply(X2, Y3, Y0), Y0)) -> multiply(Y1, multiply(X2, Y3, Y0), Y0) % 71.17/71.22 multiply(Y3, Y0, multiply(Y1, multiply(Y0, X2, Y3), Y0)) -> multiply(Y1, multiply(Y0, X2, Y3), Y0) % 71.17/71.22 multiply(inverse(Y), Y, X) -> X % 71.17/71.22 multiply(multiply(V, W, X), Y, multiply(V, W, Z)) -> multiply(V, W, multiply(X, Y, Z)) % 71.17/71.22 multiply(multiply(X0, X1, X2), Y0, multiply(Y0, Y1, multiply(X2, Y0, X1))) -> multiply(Y0, Y1, multiply(X2, Y0, X1)) % 71.17/71.22 multiply(multiply(X0, X1, multiply(X2, Y1, X4)), Y3, multiply(multiply(X0, X1, X2), Y1, Y4)) -> multiply(multiply(X0, X1, X2), Y1, multiply(multiply(X0, X1, X4), Y3, Y4)) % 71.17/71.22 multiply(multiply(X0, Y2, X2), Y1, multiply(Y2, Y3, multiply(X0, Y2, X2))) -> multiply(X0, Y2, multiply(X2, Y1, multiply(Y2, Y3, X2))) % 71.17/71.22 multiply(multiply(X0, Y2, X2), Y1, multiply(Y2, multiply(X0, Y2, multiply(X2, Y1, Y2)), Y3)) -> multiply(X0, Y2, multiply(X2, Y1, Y2)) % 71.17/71.22 multiply(multiply(X0, Y2, multiply(X2, Y1, Y2)), Y3, Y1) -> multiply(multiply(X0, Y2, X2), Y1, multiply(Y2, Y3, Y1)) % 71.17/71.22 multiply(multiply(X0, Y3, X2), Y1, multiply(Y2, Y3, multiply(X0, Y3, multiply(X2, Y1, Y3)))) -> multiply(X0, Y3, multiply(X2, Y1, Y3)) % 71.17/71.22 multiply(multiply(X0, Y3, X2), Y1, multiply(Y2, multiply(X0, Y3, multiply(X2, Y1, Y3)), Y3)) -> multiply(X0, Y3, multiply(X2, Y1, Y3)) % 71.17/71.22 multiply(multiply(X1, X2, Y2), multiply(X3, Y2, X2), multiply(X3, Y2, multiply(X1, X2, Y2))) -> multiply(Y2, multiply(X1, X2, Y2), multiply(X3, Y2, X2)) % 71.17/71.22 multiply(multiply(X1, X2, Y2), multiply(Y2, X3, X2), multiply(Y2, X3, multiply(X1, X2, Y2))) -> multiply(Y2, multiply(X1, X2, Y2), multiply(Y2, X3, X2)) % 71.17/71.22 multiply(multiply(X1, Y2, Y0), Y3, Y0) -> multiply(Y0, multiply(X1, Y2, Y0), multiply(Y2, Y3, Y0)) % 71.17/71.22 multiply(multiply(X1, Y2, Y0), Y3, multiply(Y2, Y3, Y0)) -> multiply(Y2, Y3, Y0) % 71.17/71.22 multiply(multiply(X2, X3, Y1), Y2, multiply(Y1, Y2, X2)) -> multiply(Y1, Y2, X2) % 71.17/71.22 multiply(multiply(X2, X3, Y1), Y2, multiply(Y1, Y2, X3)) -> multiply(Y1, Y2, X3) % 71.17/71.22 multiply(multiply(X2, X3, multiply(Y1, Y2, X2)), multiply(Y1, Y2, X2), Y1) -> multiply(Y1, Y2, X2) % 71.17/71.22 multiply(multiply(X2, X3, multiply(Y1, Y2, X3)), multiply(Y1, Y2, X3), Y1) -> multiply(Y1, Y2, X3) % 71.17/71.22 multiply(multiply(X2, Y0, Y1), Y3, multiply(Y0, Y1, Y4)) -> multiply(Y0, Y1, multiply(multiply(X2, Y0, Y1), Y3, Y4)) % 71.17/71.22 multiply(multiply(X2, Y0, multiply(Y0, Y1, X3)), Y3, Y1) -> multiply(Y0, Y1, multiply(multiply(X2, Y0, X3), Y3, Y1)) % 71.17/71.22 multiply(multiply(X2, Y0, multiply(Y0, Y1, X3)), Y3, multiply(Y0, Y1, Y4)) -> multiply(Y0, Y1, multiply(multiply(X2, Y0, X3), Y3, Y4)) % 71.17/71.22 multiply(multiply(X2, Y0, multiply(Y0, Y1, X3)), Y3, multiply(multiply(X2, Y0, X3), Y3, Y1)) -> multiply(multiply(X2, Y0, X3), Y3, Y1) % 71.17/71.22 multiply(multiply(X2, Y1, X3), multiply(X2, Y1, multiply(Y1, Y2, X3)), Y2) -> multiply(Y1, Y2, multiply(X2, Y1, X3)) % 71.17/71.22 multiply(multiply(X2, multiply(Y1, Y2, X2), X3), multiply(Y1, Y2, X2), Y1) -> multiply(Y1, Y2, X2) % 71.17/71.22 multiply(multiply(X2, multiply(Y1, Y2, X2), X3), multiply(Y1, Y2, X2), Y2) -> multiply(Y1, Y2, X2) % 71.17/71.22 multiply(multiply(X2, multiply(Y1, Y2, X3), X3), multiply(Y1, Y2, X3), Y1) -> multiply(Y1, Y2, X3) % 71.17/71.22 multiply(multiply(X2, multiply(Y1, Y2, X3), X3), multiply(Y1, Y2, X3), Y2) -> multiply(Y1, Y2, X3) % 71.17/71.22 multiply(multiply(Y0, X2, Y1), Y3, multiply(Y0, Y1, Y4)) -> multiply(Y0, Y1, multiply(multiply(Y0, X2, Y1), Y3, Y4)) % 71.17/71.22 multiply(multiply(Y0, X2, multiply(Y0, Y1, X3)), Y3, Y1) -> multiply(Y0, Y1, multiply(multiply(Y0, X2, X3), Y3, Y1)) % 71.17/71.22 multiply(multiply(Y0, X2, multiply(Y0, Y1, X3)), Y3, multiply(Y0, Y1, Y4)) -> multiply(Y0, Y1, multiply(multiply(Y0, X2, X3), Y3, Y4)) % 71.17/71.22 multiply(multiply(Y0, Y1, Y2), Y3, multiply(X2, Y0, Y1)) -> multiply(Y0, Y1, multiply(Y2, Y3, multiply(X2, Y0, Y1))) % 71.17/71.22 multiply(multiply(Y0, Y1, Y2), Y3, multiply(X2, Y0, multiply(Y0, Y1, X3))) -> multiply(Y0, Y1, multiply(Y2, Y3, multiply(X2, Y0, X3))) % 71.17/71.22 multiply(multiply(Y0, Y1, Y2), Y3, multiply(Y0, X2, Y1)) -> multiply(Y0, Y1, multiply(Y2, Y3, multiply(Y0, X2, Y1))) % 71.17/71.22 multiply(multiply(Y0, Y1, Y2), Y3, multiply(Y0, X2, multiply(Y0, Y1, X3))) -> multiply(Y0, Y1, multiply(Y2, Y3, multiply(Y0, X2, X3))) % 71.17/71.22 multiply(multiply(Y0, Y1, Y2), Y3, multiply(Y1, X2, Y0)) -> multiply(Y0, Y1, multiply(Y2, Y3, multiply(Y1, X2, Y0))) % 71.17/71.22 multiply(multiply(Y0, Y1, Y2), Y3, multiply(Y1, X2, multiply(Y0, Y1, X3))) -> multiply(Y0, Y1, multiply(Y2, Y3, multiply(Y1, X2, X3))) % 71.17/71.22 multiply(multiply(Y0, Y4, Y2), Y3, Y4) -> multiply(Y0, Y4, multiply(Y2, Y3, Y4)) % 71.17/71.22 multiply(multiply(Y0, multiply(X2, Y2, X3), Y2), Y3, multiply(X2, Y2, multiply(Y2, Y3, X3))) -> multiply(Y2, Y3, multiply(X2, Y2, X3)) % 71.17/71.22 multiply(multiply(Y0, multiply(Y2, Y3, Y4), Y2), Y3, multiply(multiply(Y0, multiply(Y2, Y3, Y4), Y4), Y5, Y6)) -> multiply(multiply(Y2, Y3, Y4), Y5, multiply(multiply(Y0, multiply(Y2, Y3, Y4), Y2), Y3, Y6)) % 71.17/71.22 multiply(multiply(Y1, X2, X3), multiply(Y1, X2, multiply(Y1, Y2, X3)), Y2) -> multiply(Y1, Y2, multiply(Y1, X2, X3)) % 71.17/71.22 multiply(multiply(Y1, X2, Y0), Y3, multiply(Y0, Y1, Y4)) -> multiply(Y0, Y1, multiply(multiply(Y1, X2, Y0), Y3, Y4)) % 71.17/71.22 multiply(multiply(Y1, X2, multiply(Y0, Y1, X3)), Y3, Y0) -> multiply(Y0, Y1, multiply(multiply(Y1, X2, X3), Y3, Y0)) % 71.17/71.22 multiply(multiply(Y1, X2, multiply(Y0, Y1, X3)), Y3, multiply(Y0, Y1, Y4)) -> multiply(Y0, Y1, multiply(multiply(Y1, X2, X3), Y3, Y4)) % 71.17/71.22 multiply(multiply(Y2, X1, X2), Y1, multiply(Y2, multiply(Y2, X1, multiply(X2, Y1, Y2)), Y3)) -> multiply(Y2, X1, multiply(X2, Y1, Y2)) % 71.17/71.22 multiply(multiply(Y2, X1, multiply(X2, Y1, Y2)), Y3, Y1) -> multiply(multiply(Y2, X1, X2), Y1, multiply(Y2, Y3, Y1)) % 71.17/71.22 multiply(multiply(Y2, X2, Y0), Y3, multiply(Y2, Y3, Y0)) -> multiply(Y2, Y3, Y0) % 71.17/71.22 multiply(multiply(Y2, Y1, X2), multiply(X2, X3, multiply(Y2, Y1, X2)), multiply(X3, Y1, multiply(Y2, Y1, X2))) -> multiply(Y2, Y1, X2) % 71.17/71.22 multiply(multiply(Y3, X1, X2), Y1, multiply(Y2, multiply(Y3, X1, multiply(X2, Y1, Y3)), Y3)) -> multiply(Y3, X1, multiply(X2, Y1, Y3)) % 71.17/71.22 multiply(multiply(Y4, Y1, Y2), Y3, Y4) -> multiply(Y4, Y1, multiply(Y2, Y3, Y4)) % 71.17/71.22 multiply(multiply(multiply(X0, X1, X2), Y1, Y2), Y3, multiply(X0, X1, multiply(X2, Y1, X4))) -> multiply(multiply(X0, X1, X2), Y1, multiply(Y2, Y3, multiply(X0, X1, X4))) % 71.17/71.22 multiply(multiply(multiply(Y1, Y2, X2), Y1, X2), multiply(Y1, Y2, X2), Y2) -> multiply(Y1, Y2, X2) % 71.17/71.22 true__ -> false__ % 71.17/71.22 with the LPO induced by % 71.17/71.22 a > b > f1 > inverse > multiply > true__ > false__ % 71.17/71.22 % 71.17/71.22 % SZS output end Proof % 71.17/71.22 %------------------------------------------------------------------------------