%------------------------------------------------------------------------------ % File : Moca---0.1 % Problem : BOO011-1 : TPTP v8.1.0. Released v1.0.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 : Thu Jul 14 23:46:21 EDT 2022 % Result : Unsatisfiable 72.94s 72.93s % Output : Proof 72.94s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : BOO011-1 : TPTP v8.1.0. Released v1.0.0. % 0.11/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 : Wed Jun 1 17:28:07 EDT 2022 % 0.12/0.33 % CPUTime : % 72.94/72.93 % SZS status Unsatisfiable % 72.94/72.93 % SZS output start Proof % 72.94/72.93 The input problem is unsatisfiable because % 72.94/72.93 % 72.94/72.93 [1] the following set of Horn clauses is unsatisfiable: % 72.94/72.93 % 72.94/72.93 sum(X, Y, add(X, Y)) % 72.94/72.93 product(X, Y, multiply(X, Y)) % 72.94/72.93 sum(X, Y, Z) ==> sum(Y, X, Z) % 72.94/72.93 product(X, Y, Z) ==> product(Y, X, Z) % 72.94/72.93 sum(additive_identity, X, X) % 72.94/72.93 sum(X, additive_identity, X) % 72.94/72.93 product(multiplicative_identity, X, X) % 72.94/72.93 product(X, multiplicative_identity, X) % 72.94/72.93 product(X, Y, V1) & product(X, Z, V2) & sum(Y, Z, V3) & product(X, V3, V4) ==> sum(V1, V2, V4) % 72.94/72.93 product(X, Y, V1) & product(X, Z, V2) & sum(Y, Z, V3) & sum(V1, V2, V4) ==> product(X, V3, V4) % 72.94/72.93 product(Y, X, V1) & product(Z, X, V2) & sum(Y, Z, V3) & product(V3, X, V4) ==> sum(V1, V2, V4) % 72.94/72.93 product(Y, X, V1) & product(Z, X, V2) & sum(Y, Z, V3) & sum(V1, V2, V4) ==> product(V3, X, V4) % 72.94/72.93 sum(X, Y, V1) & sum(X, Z, V2) & product(Y, Z, V3) & sum(X, V3, V4) ==> product(V1, V2, V4) % 72.94/72.93 sum(X, Y, V1) & sum(X, Z, V2) & product(Y, Z, V3) & product(V1, V2, V4) ==> sum(X, V3, V4) % 72.94/72.93 sum(Y, X, V1) & sum(Z, X, V2) & product(Y, Z, V3) & sum(V3, X, V4) ==> product(V1, V2, V4) % 72.94/72.93 sum(Y, X, V1) & sum(Z, X, V2) & product(Y, Z, V3) & product(V1, V2, V4) ==> sum(V3, X, V4) % 72.94/72.93 sum(inverse(X), X, multiplicative_identity) % 72.94/72.93 sum(X, inverse(X), multiplicative_identity) % 72.94/72.93 product(inverse(X), X, additive_identity) % 72.94/72.93 product(X, inverse(X), additive_identity) % 72.94/72.93 sum(X, Y, U) & sum(X, Y, V) ==> U = V % 72.94/72.93 product(X, Y, U) & product(X, Y, V) ==> U = V % 72.94/72.93 inverse(additive_identity) = multiplicative_identity ==> \bottom % 72.94/72.93 % 72.94/72.93 This holds because % 72.94/72.93 % 72.94/72.93 [2] the following E entails the following G (Claessen-Smallbone's transformation (2018)): % 72.94/72.93 % 72.94/72.93 E: % 72.94/72.93 f1(sum(X, Y, Z), Y, X, Z) = true__ % 72.94/72.93 f1(true__, Y, X, Z) = sum(Y, X, Z) % 72.94/72.93 f10(sum(V1, V2, V4), Y, Z, V3, X, V2, V1, V4) = true__ % 72.94/72.93 f10(true__, Y, Z, V3, X, V2, V1, V4) = f9(sum(Y, Z, V3), X, Z, V2, Y, V1, V3, V4) % 72.94/72.93 f11(true__, V1, V2, V4) = sum(V1, V2, V4) % 72.94/72.93 f12(true__, Y, X, V1, V2, V4) = f11(product(Y, X, V1), V1, V2, V4) % 72.94/72.93 f13(true__, Z, X, V2, Y, V1, V4) = f12(product(Z, X, V2), Y, X, V1, V2, V4) % 72.94/72.93 f14(product(V3, X, V4), Y, Z, V3, X, V2, V1, V4) = true__ % 72.94/72.93 f14(true__, Y, Z, V3, X, V2, V1, V4) = f13(sum(Y, Z, V3), Z, X, V2, Y, V1, V4) % 72.94/72.93 f15(true__, V3, X, V4) = product(V3, X, V4) % 72.94/72.93 f16(true__, Y, X, V1, V3, V4) = f15(product(Y, X, V1), V3, X, V4) % 72.94/72.93 f17(true__, Z, X, V2, Y, V1, V3, V4) = f16(product(Z, X, V2), Y, X, V1, V3, V4) % 72.94/72.93 f18(sum(V1, V2, V4), Y, Z, V3, X, V2, V1, V4) = true__ % 72.94/72.93 f18(true__, Y, Z, V3, X, V2, V1, V4) = f17(sum(Y, Z, V3), Z, X, V2, Y, V1, V3, V4) % 72.94/72.93 f19(true__, V1, V2, V4) = product(V1, V2, V4) % 72.94/72.93 f2(product(X, Y, Z), Y, X, Z) = true__ % 72.94/72.93 f2(true__, Y, X, Z) = product(Y, X, Z) % 72.94/72.93 f20(true__, X, Y, V1, V2, V4) = f19(sum(X, Y, V1), V1, V2, V4) % 72.94/72.93 f21(true__, X, Z, V2, Y, V1, V4) = f20(sum(X, Z, V2), X, Y, V1, V2, V4) % 72.94/72.93 f22(sum(X, V3, V4), Y, Z, V3, X, V2, V1, V4) = true__ % 72.94/72.93 f22(true__, Y, Z, V3, X, V2, V1, V4) = f21(product(Y, Z, V3), X, Z, V2, Y, V1, V4) % 72.94/72.93 f23(true__, X, V3, V4) = sum(X, V3, V4) % 72.94/72.93 f24(true__, X, Y, V1, V3, V4) = f23(sum(X, Y, V1), X, V3, V4) % 72.94/72.93 f25(true__, X, Z, V2, Y, V1, V3, V4) = f24(sum(X, Z, V2), X, Y, V1, V3, V4) % 72.94/72.93 f26(product(V1, V2, V4), Y, Z, V3, X, V2, V1, V4) = true__ % 72.94/72.93 f26(true__, Y, Z, V3, X, V2, V1, V4) = f25(product(Y, Z, V3), X, Z, V2, Y, V1, V3, V4) % 72.94/72.93 f27(true__, V1, V2, V4) = product(V1, V2, V4) % 72.94/72.93 f28(true__, Y, X, V1, V2, V4) = f27(sum(Y, X, V1), V1, V2, V4) % 72.94/72.93 f29(true__, Z, X, V2, Y, V1, V4) = f28(sum(Z, X, V2), Y, X, V1, V2, V4) % 72.94/72.93 f3(true__, V1, V2, V4) = sum(V1, V2, V4) % 72.94/72.93 f30(sum(V3, X, V4), Y, Z, V3, X, V2, V1, V4) = true__ % 72.94/72.93 f30(true__, Y, Z, V3, X, V2, V1, V4) = f29(product(Y, Z, V3), Z, X, V2, Y, V1, V4) % 72.94/72.93 f31(true__, V3, X, V4) = sum(V3, X, V4) % 72.94/72.93 f32(true__, Y, X, V1, V3, V4) = f31(sum(Y, X, V1), V3, X, V4) % 72.94/72.93 f33(true__, Z, X, V2, Y, V1, V3, V4) = f32(sum(Z, X, V2), Y, X, V1, V3, V4) % 72.94/72.93 f34(product(V1, V2, V4), Y, Z, V3, X, V2, V1, V4) = true__ % 72.94/72.93 f34(true__, Y, Z, V3, X, V2, V1, V4) = f33(product(Y, Z, V3), Z, X, V2, Y, V1, V3, V4) % 72.94/72.93 f35(true__, U, V) = U % 72.94/72.93 f36(sum(X, Y, V), X, Y, U, V) = V % 72.94/72.93 f36(true__, X, Y, U, V) = f35(sum(X, Y, U), U, V) % 72.94/72.93 f37(true__, U, V) = U % 72.94/72.93 f38(product(X, Y, V), X, Y, U, V) = V % 72.94/72.93 f38(true__, X, Y, U, V) = f37(product(X, Y, U), U, V) % 72.94/72.93 f39(inverse(additive_identity)) = true__ % 72.94/72.93 f39(multiplicative_identity) = false__ % 72.94/72.93 f4(true__, X, Y, V1, V2, V4) = f3(product(X, Y, V1), V1, V2, V4) % 72.94/72.93 f5(true__, X, Z, V2, Y, V1, V4) = f4(product(X, Z, V2), X, Y, V1, V2, V4) % 72.94/72.93 f6(product(X, V3, V4), Y, Z, V3, X, V2, V1, V4) = true__ % 72.94/72.93 f6(true__, Y, Z, V3, X, V2, V1, V4) = f5(sum(Y, Z, V3), X, Z, V2, Y, V1, V4) % 72.94/72.93 f7(true__, X, V3, V4) = product(X, V3, V4) % 72.94/72.93 f8(true__, X, Y, V1, V3, V4) = f7(product(X, Y, V1), X, V3, V4) % 72.94/72.93 f9(true__, X, Z, V2, Y, V1, V3, V4) = f8(product(X, Z, V2), X, Y, V1, V3, V4) % 72.94/72.93 product(X, Y, multiply(X, Y)) = true__ % 72.94/72.93 product(X, inverse(X), additive_identity) = true__ % 72.94/72.93 product(X, multiplicative_identity, X) = true__ % 72.94/72.93 product(inverse(X), X, additive_identity) = true__ % 72.94/72.93 product(multiplicative_identity, X, X) = true__ % 72.94/72.93 sum(X, Y, add(X, Y)) = true__ % 72.94/72.93 sum(X, additive_identity, X) = true__ % 72.94/72.93 sum(X, inverse(X), multiplicative_identity) = true__ % 72.94/72.93 sum(additive_identity, X, X) = true__ % 72.94/72.93 sum(inverse(X), X, multiplicative_identity) = true__ % 72.94/72.93 G: % 72.94/72.93 true__ = false__ % 72.94/72.93 % 72.94/72.93 This holds because % 72.94/72.93 % 72.94/72.93 [3] E entails the following ordered TRS and the lhs and rhs of G join by the TRS: % 72.94/72.93 % 72.94/72.93 % 72.94/72.93 add(Y0, inverse(Y0)) -> multiplicative_identity % 72.94/72.93 add(Y0, inverse(multiplicative_identity)) -> Y0 % 72.94/72.93 add(inverse(Y0), Y0) -> multiplicative_identity % 72.94/72.93 add(inverse(multiplicative_identity), Y0) -> Y0 % 72.94/72.93 additive_identity -> inverse(multiplicative_identity) % 72.94/72.93 f1(f1(true__, Y0, Y1, Y2), Y1, Y0, Y2) -> true__ % 72.94/72.93 f1(true__, Y0, Y1, add(Y0, Y1)) -> true__ % 72.94/72.93 f1(true__, Y0, inverse(multiplicative_identity), Y0) -> true__ % 72.94/72.93 f1(true__, Y1, Y0, add(Y0, Y1)) -> true__ % 72.94/72.93 f1(true__, Y1, inverse(Y1), multiplicative_identity) -> true__ % 72.94/72.93 f1(true__, inverse(Y0), Y0, multiplicative_identity) -> true__ % 72.94/72.93 f1(true__, inverse(multiplicative_identity), Y0, Y0) -> true__ % 72.94/72.93 f10(f1(true__, Y0, Y1, Y2), Y3, Y4, Y5, Y6, Y1, Y0, Y2) -> true__ % 72.94/72.93 f10(true__, Y, Z, V3, X, V2, V1, V4) -> f9(f1(true__, Y, Z, V3), X, Z, V2, Y, V1, V3, V4) % 72.94/72.93 f11(true__, V1, V2, V4) -> f1(true__, V1, V2, V4) % 72.94/72.93 f12(true__, Y, X, V1, V2, V4) -> f11(f2(true__, Y, X, V1), V1, V2, V4) % 72.94/72.93 f13(true__, Z, X, V2, Y, V1, V4) -> f12(f2(true__, Z, X, V2), Y, X, V1, V2, V4) % 72.94/72.93 f14(product(V3, X, V4), Y, Z, V3, X, V2, V1, V4) -> true__ % 72.94/72.93 f14(true__, Y, Z, V3, X, V2, V1, V4) -> f13(f1(true__, Y, Z, V3), Z, X, V2, Y, V1, V4) % 72.94/72.93 f15(true__, V3, X, V4) -> f2(true__, V3, X, V4) % 72.94/72.93 f16(true__, Y, X, V1, V3, V4) -> f15(f2(true__, Y, X, V1), V3, X, V4) % 72.94/72.93 f17(true__, Z, X, V2, Y, V1, V3, V4) -> f16(f2(true__, Z, X, V2), Y, X, V1, V3, V4) % 72.94/72.93 f18(sum(V1, V2, V4), Y, Z, V3, X, V2, V1, V4) -> true__ % 72.94/72.93 f18(true__, Y, Z, V3, X, V2, V1, V4) -> f17(f1(true__, Y, Z, V3), Z, X, V2, Y, V1, V3, V4) % 72.94/72.93 f19(true__, V1, V2, V4) -> f2(true__, V1, V2, V4) % 72.94/72.93 f2(f2(true__, Y0, Y1, Y2), Y1, Y0, Y2) -> true__ % 72.94/72.93 f2(true__, Y0, Y1, multiply(Y0, Y1)) -> true__ % 72.94/72.93 f2(true__, Y0, inverse(Y0), inverse(multiplicative_identity)) -> true__ % 72.94/72.93 f2(true__, Y1, Y0, multiply(Y0, Y1)) -> true__ % 72.94/72.93 f2(true__, Y2, multiplicative_identity, Y2) -> true__ % 72.94/72.93 f2(true__, inverse(Y0), Y0, inverse(multiplicative_identity)) -> true__ % 72.94/72.93 f2(true__, multiplicative_identity, Y2, Y2) -> true__ % 72.94/72.93 f20(true__, X, Y, V1, V2, V4) -> f19(f1(true__, X, Y, V1), V1, V2, V4) % 72.94/72.93 f21(true__, X, Z, V2, Y, V1, V4) -> f20(f1(true__, X, Z, V2), X, Y, V1, V2, V4) % 72.94/72.93 f22(sum(X, V3, V4), Y, Z, V3, X, V2, V1, V4) -> true__ % 72.94/72.93 f22(true__, Y, Z, V3, X, V2, V1, V4) -> f21(f2(true__, Y, Z, V3), X, Z, V2, Y, V1, V4) % 72.94/72.93 f23(true__, X, V3, V4) -> f1(true__, X, V3, V4) % 72.94/72.93 f24(true__, X, Y, V1, V3, V4) -> f23(f1(true__, X, Y, V1), X, V3, V4) % 72.94/72.93 f25(true__, X, Z, V2, Y, V1, V3, V4) -> f24(f1(true__, X, Z, V2), X, Y, V1, V3, V4) % 72.94/72.93 f26(product(V1, V2, V4), Y, Z, V3, X, V2, V1, V4) -> true__ % 72.94/72.93 f26(true__, Y, Z, V3, X, V2, V1, V4) -> f25(f2(true__, Y, Z, V3), X, Z, V2, Y, V1, V3, V4) % 72.94/72.93 f27(true__, V1, V2, V4) -> f2(true__, V1, V2, V4) % 72.94/72.93 f28(true__, Y, X, V1, V2, V4) -> f27(f1(true__, Y, X, V1), V1, V2, V4) % 72.94/72.93 f29(true__, Z, X, V2, Y, V1, V4) -> f28(f1(true__, Z, X, V2), Y, X, V1, V2, V4) % 72.94/72.93 f3(true__, V1, V2, V4) -> f1(true__, V1, V2, V4) % 72.94/72.93 f30(sum(V3, X, V4), Y, Z, V3, X, V2, V1, V4) -> true__ % 72.94/72.93 f30(true__, Y, Z, V3, X, V2, V1, V4) -> f29(f2(true__, Y, Z, V3), Z, X, V2, Y, V1, V4) % 72.94/72.93 f31(true__, V3, X, V4) -> f1(true__, V3, X, V4) % 72.94/72.93 f32(true__, Y, X, V1, V3, V4) -> f31(f1(true__, Y, X, V1), V3, X, V4) % 72.94/72.93 f33(true__, Z, X, V2, Y, V1, V3, V4) -> f32(f1(true__, Z, X, V2), Y, X, V1, V3, V4) % 72.94/72.93 f34(product(V1, V2, V4), Y, Z, V3, X, V2, V1, V4) -> true__ % 72.94/72.93 f34(true__, Y, Z, V3, X, V2, V1, V4) -> f33(f2(true__, Y, Z, V3), Z, X, V2, Y, V1, V3, V4) % 72.94/72.93 f35(f1(true__, Y0, Y1, Y3), Y3, add(Y1, Y0)) -> add(Y1, Y0) % 72.94/72.93 f35(f1(true__, Y0, inverse(Y0), Y3), Y3, multiplicative_identity) -> multiplicative_identity % 72.94/72.93 f35(f1(true__, Y2, inverse(multiplicative_identity), Y3), Y3, Y2) -> Y2 % 72.94/72.93 f35(f1(true__, inverse(Y1), Y1, Y3), Y3, multiplicative_identity) -> multiplicative_identity % 72.94/72.93 f35(f1(true__, inverse(multiplicative_identity), Y2, Y3), Y3, Y2) -> Y2 % 72.94/72.93 f35(true__, U, V) -> U % 72.94/72.93 f36(f1(true__, Y0, Y1, Y2), Y0, Y1, Y3, Y2) -> Y2 % 72.94/72.93 f36(true__, X, Y, U, V) -> f35(f1(true__, X, Y, U), U, V) % 72.94/72.93 f37(f2(true__, Y2, multiplicative_identity, Y3), Y3, Y2) -> Y2 % 72.94/72.93 f37(f2(true__, inverse(Y0), Y0, Y1), Y1, inverse(multiplicative_identity)) -> inverse(multiplicative_identity) % 72.94/72.93 f37(f2(true__, multiplicative_identity, Y2, Y3), Y3, Y2) -> Y2 % 72.94/72.93 f37(true__, U, V) -> U % 72.94/72.93 f38(f2(true__, Y0, Y1, Y2), Y0, Y1, Y3, Y2) -> Y2 % 72.94/72.93 f38(true__, X, Y, U, V) -> f37(f2(true__, X, Y, U), U, V) % 72.94/72.93 f39(inverse(inverse(multiplicative_identity))) -> true__ % 72.94/72.93 f39(multiplicative_identity) -> false__ % 72.94/72.93 f4(true__, X, Y, V1, V2, V4) -> f3(f2(true__, X, Y, V1), V1, V2, V4) % 72.94/72.93 f5(true__, X, Z, V2, Y, V1, V4) -> f4(f2(true__, X, Z, V2), X, Y, V1, V2, V4) % 72.94/72.93 f6(product(X, V3, V4), Y, Z, V3, X, V2, V1, V4) -> true__ % 72.94/72.93 f6(true__, Y, Z, V3, X, V2, V1, V4) -> f5(f1(true__, Y, Z, V3), X, Z, V2, Y, V1, V4) % 72.94/72.93 f7(true__, X, V3, V4) -> f2(true__, X, V3, V4) % 72.94/72.93 f8(true__, X, Y, V1, V3, V4) -> f7(f2(true__, X, Y, V1), X, V3, V4) % 72.94/72.93 f9(true__, X, Z, V2, Y, V1, V3, V4) -> f8(f2(true__, X, Z, V2), X, Y, V1, V3, V4) % 72.94/72.93 inverse(inverse(multiplicative_identity)) -> multiplicative_identity % 72.94/72.93 multiply(Y0, inverse(Y0)) -> inverse(multiplicative_identity) % 72.94/72.93 multiply(Y0, multiplicative_identity) -> Y0 % 72.94/72.93 multiply(inverse(Y0), Y0) -> inverse(multiplicative_identity) % 72.94/72.93 multiply(multiplicative_identity, Y0) -> Y0 % 72.94/72.93 product(Y, X, Z) -> f2(true__, Y, X, Z) % 72.94/72.93 sum(Y, X, Z) -> f1(true__, Y, X, Z) % 72.94/72.93 true__ -> false__ % 72.94/72.93 with the LPO induced by % 72.94/72.93 f34 > f26 > f18 > f17 > f10 > f9 > f14 > f13 > f12 > f30 > f29 > f22 > f21 > f6 > f5 > f28 > f20 > f16 > f8 > f4 > f3 > f38 > f37 > f27 > f15 > f19 > f7 > product > f2 > f33 > f32 > f36 > f25 > f31 > f11 > f24 > f23 > sum > f1 > add > multiply > additive_identity > inverse > multiplicative_identity > f35 > f39 > true__ > false__ % 72.94/72.93 % 72.94/72.93 % SZS output end Proof % 72.94/72.93 %------------------------------------------------------------------------------