%------------------------------------------------------------------------------ % File : Moca---0.1 % Problem : GRP206-1 : TPTP v8.1.0. Released v2.3.0. % Transfm : none % Format : tptp:raw % Command : moca.sh %s % Computer : n028.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 : Sat Jul 16 10:54:06 EDT 2022 % Result : Unsatisfiable 1.11s 1.32s % Output : Proof 1.11s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : GRP206-1 : TPTP v8.1.0. Released v2.3.0. % 0.07/0.12 % Command : moca.sh %s % 0.12/0.33 % Computer : n028.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Mon Jun 13 15:17:22 EDT 2022 % 0.12/0.33 % CPUTime : % 1.11/1.32 % SZS status Unsatisfiable % 1.11/1.32 % SZS output start Proof % 1.11/1.32 The input problem is unsatisfiable because % 1.11/1.32 % 1.11/1.32 [1] the following set of Horn clauses is unsatisfiable: % 1.11/1.32 % 1.11/1.32 multiply(identity, X) = X % 1.11/1.32 multiply(X, identity) = X % 1.11/1.32 multiply(X, left_division(X, Y)) = Y % 1.11/1.32 left_division(X, multiply(X, Y)) = Y % 1.11/1.32 multiply(right_division(X, Y), Y) = X % 1.11/1.32 right_division(multiply(X, Y), Y) = X % 1.11/1.32 multiply(X, right_inverse(X)) = identity % 1.11/1.32 multiply(left_inverse(X), X) = identity % 1.11/1.32 multiply(X, multiply(multiply(Y, Z), X)) = multiply(multiply(X, Y), multiply(Z, X)) % 1.11/1.32 multiply(multiply(a, multiply(b, c)), a) = multiply(multiply(a, b), multiply(c, a)) ==> \bottom % 1.11/1.32 % 1.11/1.32 This holds because % 1.11/1.32 % 1.11/1.32 [2] the following E entails the following G (Claessen-Smallbone's transformation (2018)): % 1.11/1.32 % 1.11/1.32 E: % 1.11/1.32 f1(multiply(multiply(a, b), multiply(c, a))) = false__ % 1.11/1.32 f1(multiply(multiply(a, multiply(b, c)), a)) = true__ % 1.11/1.32 left_division(X, multiply(X, Y)) = Y % 1.11/1.32 multiply(X, identity) = X % 1.11/1.32 multiply(X, left_division(X, Y)) = Y % 1.11/1.32 multiply(X, multiply(multiply(Y, Z), X)) = multiply(multiply(X, Y), multiply(Z, X)) % 1.11/1.32 multiply(X, right_inverse(X)) = identity % 1.11/1.32 multiply(identity, X) = X % 1.11/1.32 multiply(left_inverse(X), X) = identity % 1.11/1.32 multiply(right_division(X, Y), Y) = X % 1.11/1.32 right_division(multiply(X, Y), Y) = X % 1.11/1.32 G: % 1.11/1.32 true__ = false__ % 1.11/1.32 % 1.11/1.32 This holds because % 1.11/1.32 % 1.11/1.32 [3] E entails the following ordered TRS and the lhs and rhs of G join by the TRS: % 1.11/1.32 % 1.11/1.32 left_division(X0, X0) = left_division(Y0, Y0) % 1.11/1.32 left_division(X0, X0) = right_division(Y0, Y0) % 1.11/1.32 left_division(Y0, Y0) = identity % 1.11/1.32 left_division(Y0, Y0) = right_division(false__, false__) % 1.11/1.32 left_division(Y0, multiply(Y2, Y0)) = multiply(multiply(left_division(Y0, right_division(false__, false__)), Y2), Y0) % 1.11/1.32 left_division(Y0, multiply(multiply(Y0, Y1), X0)) = multiply(multiply(Y1, right_division(X0, Y0)), Y0) % 1.11/1.32 left_division(multiply(X0, X1), multiply(X0, X0)) = multiply(left_division(X1, right_division(false__, false__)), X0) % 1.11/1.32 multiply(X, multiply(multiply(Y, Z), X)) = multiply(multiply(X, Y), multiply(Z, X)) % 1.11/1.32 multiply(X0, multiply(left_division(Y1, Y2), right_division(X0, Y1))) = multiply(right_division(X0, Y1), multiply(Y2, right_division(X0, Y1))) % 1.11/1.32 multiply(X0, multiply(left_division(Y1, right_division(false__, false__)), right_division(X0, Y1))) = multiply(right_division(X0, Y1), right_division(X0, Y1)) % 1.11/1.32 multiply(Y0, multiply(multiply(X0, multiply(multiply(X1, X2), X0)), Y0)) = multiply(multiply(Y0, multiply(X0, X1)), multiply(multiply(X2, X0), Y0)) % 1.11/1.32 multiply(Y0, multiply(multiply(Y1, multiply(Y2, Y1)), Y0)) = multiply(multiply(Y0, multiply(Y1, Y2)), multiply(Y1, Y0)) % 1.11/1.32 multiply(Y0, multiply(multiply(left_division(Y3, right_division(false__, false__)), Y2), Y0)) = multiply(multiply(Y0, left_division(Y3, right_division(false__, false__))), multiply(multiply(multiply(Y2, Y3), left_division(Y3, right_division(false__, false__))), Y0)) % 1.11/1.32 multiply(Y0, multiply(multiply(multiply(Y1, X1), multiply(X2, Y1)), Y0)) = multiply(multiply(Y0, Y1), multiply(multiply(multiply(X1, X2), Y1), Y0)) % 1.11/1.32 multiply(left_division(Y1, Y2), right_division(right_division(false__, false__), Y1)) = multiply(right_division(right_division(false__, false__), Y1), multiply(Y2, right_division(right_division(false__, false__), Y1))) % 1.11/1.32 multiply(left_division(Y2, right_division(false__, false__)), right_division(Y1, Y2)) = multiply(left_division(Y2, right_division(false__, false__)), multiply(Y1, left_division(Y2, right_division(false__, false__)))) % 1.11/1.32 multiply(multiply(X0, X0), multiply(X0, X1)) = multiply(multiply(X0, X1), multiply(multiply(left_division(X1, right_division(false__, false__)), X0), multiply(X0, X1))) % 1.11/1.32 multiply(multiply(X0, X0), multiply(X0, right_division(right_division(false__, false__), X1))) = multiply(multiply(X0, right_division(right_division(false__, false__), X1)), multiply(multiply(X1, X0), multiply(X0, right_division(right_division(false__, false__), X1)))) % 1.11/1.32 multiply(multiply(X0, X0), multiply(left_division(multiply(X1, X0), right_division(false__, false__)), multiply(X0, right_division(right_division(false__, false__), X1)))) = multiply(multiply(X0, right_division(right_division(false__, false__), X1)), multiply(X0, right_division(right_division(false__, false__), X1))) % 1.11/1.32 multiply(multiply(X0, multiply(multiply(X1, X2), X0)), multiply(Y2, multiply(X0, X1))) = multiply(multiply(X0, X1), multiply(multiply(multiply(X2, X0), Y2), multiply(X0, X1))) % 1.11/1.32 multiply(multiply(X2, Y1), multiply(Y1, multiply(multiply(Y2, X2), Y1))) = multiply(multiply(multiply(X2, Y1), Y1), multiply(Y2, multiply(X2, Y1))) % 1.11/1.32 multiply(multiply(Y2, Y1), left_division(Y1, Y1)) = multiply(multiply(left_division(Y1, Y1), Y2), Y1) % 1.11/1.32 multiply(multiply(left_division(Y2, X1), Y1), X1) = multiply(left_division(Y2, X1), multiply(multiply(Y1, Y2), left_division(Y2, X1))) % 1.11/1.32 multiply(multiply(multiply(X2, X0), Y1), multiply(X0, multiply(multiply(X1, X2), X0))) = multiply(multiply(X2, X0), multiply(multiply(Y1, multiply(X0, X1)), multiply(X2, X0))) % 1.11/1.32 multiply(multiply(multiply(multiply(X1, X2), Y2), Y1), multiply(multiply(Y2, X1), multiply(X2, Y2))) = multiply(multiply(multiply(X1, X2), Y2), multiply(multiply(Y1, Y2), multiply(multiply(X1, X2), Y2))) % 1.11/1.32 multiply(right_division(Y1, Y1), multiply(Y1, Y2)) = multiply(Y1, multiply(Y2, right_division(Y1, Y1))) % 1.11/1.32 right_division(X0, X0) = right_division(Y0, Y0) % 1.11/1.32 right_division(Y1, Y1) = identity % 1.11/1.32 right_division(Y1, Y1) = right_division(false__, false__) % 1.11/1.32 right_division(multiply(X0, X0), multiply(X1, X0)) = multiply(X0, right_division(right_division(false__, false__), X1)) % 1.11/1.32 f1(multiply(multiply(a, b), multiply(c, a))) -> false__ % 1.11/1.32 f1(multiply(multiply(a, multiply(b, c)), a)) -> true__ % 1.11/1.32 left_division(X, multiply(X, Y)) -> Y % 1.11/1.32 left_division(Y0, multiply(X1, multiply(Y2, Y0))) -> multiply(multiply(left_division(Y0, X1), Y2), Y0) % 1.11/1.32 left_division(Y0, multiply(multiply(Y0, X1), multiply(X2, Y0))) -> multiply(multiply(X1, X2), Y0) % 1.11/1.32 left_division(identity, Y1) -> Y1 % 1.11/1.32 left_division(left_division(X0, X0), Y0) -> Y0 % 1.11/1.32 left_division(left_division(X0, X0), right_division(false__, false__)) -> right_division(false__, false__) % 1.11/1.32 left_division(left_division(Y2, X1), multiply(multiply(left_division(Y2, X1), Y1), X1)) -> multiply(multiply(Y1, Y2), left_division(Y2, X1)) % 1.11/1.32 left_division(left_inverse(Y1), identity) -> Y1 % 1.11/1.32 left_division(multiply(X0, X1), multiply(X0, multiply(X2, X0))) -> multiply(left_division(X1, X2), X0) % 1.11/1.32 left_division(multiply(X0, X1), multiply(X0, multiply(multiply(X1, X2), X0))) -> multiply(X2, X0) % 1.11/1.32 left_division(multiply(X0, right_division(X1, X2)), multiply(X0, multiply(X1, X0))) -> multiply(X2, X0) % 1.11/1.32 left_division(multiply(X0, right_division(right_division(false__, false__), X1)), multiply(X0, X0)) -> multiply(X1, X0) % 1.11/1.32 left_division(multiply(Y0, Y1), multiply(Y0, multiply(Y1, Y0))) -> Y0 % 1.11/1.32 left_division(multiply(left_division(multiply(Y1, Y2), X1), Y1), multiply(left_division(multiply(Y1, Y2), X1), X1)) -> multiply(Y2, left_division(multiply(Y1, Y2), X1)) % 1.11/1.32 left_division(multiply(left_division(multiply(Y1, Y2), right_division(false__, false__)), Y1), left_division(multiply(Y1, Y2), right_division(false__, false__))) -> multiply(Y2, left_division(multiply(Y1, Y2), right_division(false__, false__))) % 1.11/1.32 left_division(right_division(X0, X0), Y0) -> Y0 % 1.11/1.32 left_division(right_division(X0, X0), right_division(false__, false__)) -> right_division(false__, false__) % 1.11/1.32 left_division(right_division(X0, Y1), X0) -> Y1 % 1.11/1.32 left_division(right_division(X0, Y1), multiply(X0, multiply(Y2, right_division(X0, Y1)))) -> multiply(multiply(Y1, Y2), right_division(X0, Y1)) % 1.11/1.32 left_division(right_division(right_division(false__, false__), Y0), left_division(X0, X0)) -> Y0 % 1.11/1.32 left_division(right_division(right_division(false__, false__), Y0), right_division(X0, X0)) -> Y0 % 1.11/1.32 left_division(right_division(right_division(false__, false__), Y1), multiply(Y2, right_division(right_division(false__, false__), Y1))) -> multiply(multiply(Y1, Y2), right_division(right_division(false__, false__), Y1)) % 1.11/1.32 left_inverse(Y1) -> right_division(identity, Y1) % 1.11/1.32 left_inverse(identity) -> identity % 1.11/1.32 multiply(X, identity) -> X % 1.11/1.32 multiply(X, left_division(X, Y)) -> Y % 1.11/1.32 multiply(X, right_inverse(X)) -> identity % 1.11/1.32 multiply(X1, multiply(left_division(left_division(Y0, X1), Y2), Y0)) -> multiply(Y0, multiply(Y2, Y0)) % 1.11/1.32 multiply(X1, multiply(left_division(left_division(Y0, X1), right_division(false__, false__)), Y0)) -> multiply(Y0, Y0) % 1.11/1.32 multiply(Y0, left_division(X0, X0)) -> Y0 % 1.11/1.32 multiply(Y0, multiply(left_division(Y0, X1), Y0)) -> multiply(X1, Y0) % 1.11/1.32 multiply(Y0, multiply(left_division(Y0, right_division(false__, false__)), Y0)) -> Y0 % 1.11/1.32 multiply(Y0, multiply(multiply(Y1, right_division(right_division(false__, false__), Y0)), Y0)) -> multiply(Y0, Y1) % 1.11/1.32 multiply(Y0, right_division(X0, X0)) -> Y0 % 1.11/1.32 multiply(Y0, right_division(Y1, right_division(right_division(false__, false__), Y0))) -> multiply(Y0, multiply(Y1, Y0)) % 1.11/1.32 multiply(Y0, right_division(right_division(false__, false__), right_division(right_division(false__, false__), Y0))) -> multiply(Y0, Y0) % 1.11/1.32 multiply(identity, X) -> X % 1.11/1.32 multiply(left_division(X0, X0), Y0) -> Y0 % 1.11/1.32 multiply(left_division(X0, right_division(false__, false__)), multiply(multiply(multiply(X1, X0), left_division(X0, right_division(false__, false__))), left_division(X0, right_division(false__, false__)))) -> multiply(left_division(X0, right_division(false__, false__)), multiply(X1, left_division(X0, right_division(false__, false__)))) % 1.11/1.32 multiply(left_division(Y0, right_division(false__, false__)), multiply(multiply(Y0, multiply(X1, Y0)), left_division(Y0, right_division(false__, false__)))) -> multiply(left_division(Y0, right_division(false__, false__)), multiply(Y0, X1)) % 1.11/1.32 multiply(left_division(Y0, right_division(false__, false__)), multiply(multiply(Y1, Y0), left_division(Y0, right_division(false__, false__)))) -> multiply(left_division(Y0, right_division(false__, false__)), Y1) % 1.11/1.32 multiply(left_division(Y1, Y1), multiply(multiply(Y2, Y1), left_division(Y1, Y1))) -> multiply(Y2, Y1) % 1.11/1.32 multiply(left_division(Y1, right_division(false__, false__)), right_division(right_division(false__, false__), Y1)) -> multiply(left_division(Y1, right_division(false__, false__)), left_division(Y1, right_division(false__, false__))) % 1.11/1.32 multiply(left_division(left_division(Y0, right_division(false__, false__)), Y2), Y0) -> multiply(Y0, multiply(Y2, Y0)) % 1.11/1.32 multiply(left_division(left_division(Y0, right_division(false__, false__)), right_division(false__, false__)), Y0) -> multiply(Y0, Y0) % 1.11/1.32 multiply(left_division(left_division(Y1, Y2), right_division(false__, false__)), multiply(Y2, left_division(left_division(Y1, Y2), right_division(false__, false__)))) -> multiply(left_division(left_division(Y1, Y2), right_division(false__, false__)), Y1) % 1.11/1.32 multiply(left_division(left_division(Y1, right_division(false__, false__)), right_division(false__, false__)), left_division(left_division(Y1, right_division(false__, false__)), right_division(false__, false__))) -> multiply(left_division(left_division(Y1, right_division(false__, false__)), right_division(false__, false__)), Y1) % 1.11/1.32 multiply(left_inverse(X), X) -> identity % 1.11/1.32 multiply(left_inverse(Y1), multiply(multiply(Y1, Y2), left_inverse(Y1))) -> multiply(Y2, left_inverse(Y1)) % 1.11/1.32 multiply(multiply(X0, X0), multiply(left_division(multiply(left_division(X1, right_division(false__, false__)), X0), right_division(false__, false__)), multiply(X0, X1))) -> multiply(multiply(X0, X1), multiply(X0, X1)) % 1.11/1.32 multiply(multiply(Y0, Y1), Y0) -> multiply(Y0, multiply(Y1, Y0)) % 1.11/1.32 multiply(multiply(Y0, Y1), multiply(left_division(Y1, X1), Y0)) -> multiply(Y0, multiply(X1, Y0)) % 1.11/1.32 multiply(multiply(Y0, Y1), multiply(multiply(multiply(Y2, right_division(right_division(false__, false__), Y1)), Y1), Y0)) -> multiply(Y0, multiply(multiply(Y1, Y2), Y0)) % 1.11/1.32 multiply(multiply(Y0, Y1), multiply(right_inverse(Y1), Y0)) -> multiply(Y0, Y0) % 1.11/1.32 multiply(multiply(Y0, left_inverse(Y2)), multiply(Y2, Y0)) -> multiply(Y0, Y0) % 1.11/1.32 multiply(multiply(Y0, multiply(multiply(Y1, Y2), Y0)), multiply(Y0, Y1)) -> multiply(multiply(Y0, Y1), multiply(multiply(Y2, Y0), multiply(Y0, Y1))) % 1.11/1.32 multiply(multiply(Y0, right_division(X0, Y2)), multiply(Y2, Y0)) -> multiply(Y0, multiply(X0, Y0)) % 1.11/1.32 multiply(multiply(Y0, right_division(Y1, right_division(X0, Y0))), X0) -> multiply(Y0, multiply(Y1, Y0)) % 1.11/1.32 multiply(multiply(Y0, right_division(right_division(false__, false__), Y2)), multiply(multiply(multiply(Y2, Y3), right_division(right_division(false__, false__), Y2)), Y0)) -> multiply(Y0, multiply(multiply(Y3, right_division(right_division(false__, false__), Y2)), Y0)) % 1.11/1.32 multiply(multiply(Y0, right_division(right_division(false__, false__), multiply(Y0, X1))), multiply(Y0, multiply(X1, Y0))) -> multiply(Y0, Y0) % 1.11/1.32 multiply(multiply(Y0, right_division(right_division(false__, false__), right_division(X0, Y0))), X0) -> multiply(Y0, Y0) % 1.11/1.32 multiply(multiply(Y1, Y1), multiply(Y2, Y1)) -> multiply(Y1, multiply(Y1, multiply(Y2, Y1))) % 1.11/1.32 multiply(multiply(Y1, Y2), left_division(Y2, right_division(false__, false__))) -> Y1 % 1.11/1.32 multiply(multiply(Y1, Y2), right_division(Y1, Y1)) -> multiply(Y1, multiply(Y2, right_division(Y1, Y1))) % 1.11/1.32 multiply(multiply(Y1, multiply(X1, Y1)), multiply(Y1, X1)) -> multiply(multiply(Y1, X1), multiply(Y1, multiply(Y1, X1))) % 1.11/1.32 multiply(multiply(Y1, multiply(X1, Y1)), multiply(left_division(Y1, right_division(false__, false__)), multiply(Y1, X1))) -> multiply(multiply(Y1, X1), multiply(Y1, X1)) % 1.11/1.32 multiply(multiply(Y1, right_division(right_division(false__, false__), Y0)), Y0) -> Y1 % 1.11/1.32 multiply(multiply(left_division(Y1, X1), right_division(right_division(false__, false__), Y1)), X1) -> multiply(left_division(Y1, X1), left_division(Y1, X1)) % 1.11/1.32 multiply(multiply(left_division(Y1, Y1), Y2), Y1) -> multiply(left_division(Y1, Y1), multiply(Y2, Y1)) % 1.11/1.32 multiply(multiply(left_division(Y2, X1), right_division(Y1, Y2)), X1) -> multiply(left_division(Y2, X1), multiply(Y1, left_division(Y2, X1))) % 1.11/1.32 multiply(multiply(multiply(left_division(X1, right_division(false__, false__)), X0), right_division(right_division(false__, false__), multiply(X0, X1))), multiply(X0, X0)) -> multiply(multiply(left_division(X1, right_division(false__, false__)), X0), multiply(left_division(X1, right_division(false__, false__)), X0)) % 1.11/1.32 multiply(multiply(right_division(right_division(false__, false__), Y1), multiply(X1, right_division(right_division(false__, false__), Y1))), multiply(Y1, multiply(right_division(right_division(false__, false__), Y1), X1))) -> multiply(multiply(right_division(right_division(false__, false__), Y1), X1), multiply(right_division(right_division(false__, false__), Y1), X1)) % 1.11/1.32 multiply(right_division(X, Y), Y) -> X % 1.11/1.32 multiply(right_division(X0, X0), Y0) -> Y0 % 1.11/1.32 multiply(right_division(X0, Y1), multiply(Y1, right_division(X0, Y1))) -> multiply(X0, right_division(X0, Y1)) % 1.11/1.32 multiply(right_division(X0, Y1), multiply(multiply(Y1, Y2), right_division(X0, Y1))) -> multiply(X0, multiply(Y2, right_division(X0, Y1))) % 1.11/1.32 multiply(right_division(X0, right_division(Y1, Y2)), multiply(Y1, right_division(X0, right_division(Y1, Y2)))) -> multiply(X0, multiply(Y2, right_division(X0, right_division(Y1, Y2)))) % 1.11/1.32 multiply(right_division(X0, right_division(right_division(false__, false__), Y1)), right_division(X0, right_division(right_division(false__, false__), Y1))) -> multiply(X0, multiply(Y1, right_division(X0, right_division(right_division(false__, false__), Y1)))) % 1.11/1.32 multiply(right_division(false__, false__), multiply(Y1, right_division(right_division(false__, false__), Y0))) -> multiply(Y1, right_division(right_division(false__, false__), Y0)) % 1.11/1.32 multiply(right_division(right_division(false__, false__), Y0), multiply(Y0, right_division(right_division(false__, false__), Y0))) -> right_division(right_division(false__, false__), Y0) % 1.11/1.32 multiply(right_division(right_division(false__, false__), Y1), right_division(right_division(false__, false__), Y1)) -> multiply(left_division(Y1, right_division(false__, false__)), right_division(right_division(false__, false__), Y1)) % 1.11/1.32 multiply(right_division(right_division(false__, false__), right_division(Y1, Y2)), multiply(Y1, right_division(right_division(false__, false__), right_division(Y1, Y2)))) -> multiply(Y2, right_division(right_division(false__, false__), right_division(Y1, Y2))) % 1.11/1.32 multiply(right_division(right_division(false__, false__), right_division(right_division(false__, false__), Y1)), right_division(right_division(false__, false__), right_division(right_division(false__, false__), Y1))) -> multiply(Y1, right_division(right_division(false__, false__), right_division(right_division(false__, false__), Y1))) % 1.11/1.32 multiply(right_inverse(Y2), multiply(multiply(Y1, Y2), right_inverse(Y2))) -> multiply(right_inverse(Y2), Y1) % 1.11/1.32 right_division(X1, left_division(Y0, X1)) -> Y0 % 1.11/1.32 right_division(Y0, identity) -> Y0 % 1.11/1.32 right_division(Y0, left_division(X0, X0)) -> Y0 % 1.11/1.32 right_division(Y0, right_division(X0, X0)) -> Y0 % 1.11/1.32 right_division(identity, right_inverse(Y0)) -> Y0 % 1.11/1.32 right_division(left_division(X0, X0), left_division(Y0, right_division(false__, false__))) -> Y0 % 1.11/1.32 right_division(left_division(multiply(Y1, Y2), right_division(false__, false__)), multiply(Y2, left_division(multiply(Y1, Y2), right_division(false__, false__)))) -> multiply(left_division(multiply(Y1, Y2), right_division(false__, false__)), Y1) % 1.11/1.32 right_division(multiply(X, Y), Y) -> X % 1.11/1.32 right_division(multiply(X0, X0), multiply(left_division(X1, right_division(false__, false__)), X0)) -> multiply(X0, X1) % 1.11/1.32 right_division(multiply(X0, multiply(X2, X0)), multiply(left_division(X1, X2), X0)) -> multiply(X0, X1) % 1.11/1.32 right_division(multiply(X0, multiply(multiply(X1, X2), X0)), multiply(X2, X0)) -> multiply(X0, X1) % 1.11/1.32 right_division(multiply(X1, multiply(Y2, Y0)), multiply(multiply(left_division(Y0, X1), Y2), Y0)) -> Y0 % 1.11/1.32 right_division(multiply(Y0, Y1), multiply(multiply(Y1, right_division(right_division(false__, false__), Y0)), Y0)) -> Y0 % 1.11/1.32 right_division(multiply(Y0, multiply(Y1, Y0)), Y0) -> multiply(Y0, Y1) % 1.11/1.32 right_division(multiply(Y1, Y2), multiply(Y1, Y2)) -> right_division(false__, false__) % 1.11/1.32 right_division(multiply(Y2, Y0), multiply(multiply(left_division(Y0, right_division(false__, false__)), Y2), Y0)) -> Y0 % 1.11/1.32 right_division(multiply(Y2, right_division(right_division(false__, false__), Y1)), multiply(multiply(Y1, Y2), right_division(right_division(false__, false__), Y1))) -> right_division(right_division(false__, false__), Y1) % 1.11/1.32 right_division(multiply(left_division(Y2, right_division(false__, false__)), Y1), multiply(multiply(Y1, Y2), left_division(Y2, right_division(false__, false__)))) -> left_division(Y2, right_division(false__, false__)) % 1.11/1.32 right_division(multiply(multiply(Y0, X1), multiply(X2, Y0)), multiply(multiply(X1, X2), Y0)) -> Y0 % 1.11/1.32 right_division(multiply(multiply(left_division(Y2, X1), Y1), X1), multiply(multiply(Y1, Y2), left_division(Y2, X1))) -> left_division(Y2, X1) % 1.11/1.32 right_division(right_division(X0, X0), left_division(Y0, right_division(false__, false__))) -> Y0 % 1.11/1.32 right_division(right_division(false__, false__), left_division(X0, X0)) -> right_division(false__, false__) % 1.11/1.32 right_division(right_division(false__, false__), right_division(X0, X0)) -> right_division(false__, false__) % 1.11/1.32 right_inverse(Y0) -> left_division(Y0, identity) % 1.11/1.32 right_inverse(identity) -> identity % 1.11/1.32 true__ -> false__ % 1.11/1.32 with the LPO induced by % 1.11/1.32 c > b > a > f1 > left_inverse > right_inverse > identity > right_division > left_division > multiply > true__ > false__ % 1.11/1.32 % 1.11/1.32 % SZS output end Proof % 1.11/1.32 %------------------------------------------------------------------------------