%------------------------------------------------------------------------------ % File : Moca---0.1 % Problem : ALG235-1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : moca.sh %s % Computer : n029.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 17:41:54 EDT 2022 % Result : Unsatisfiable 0.90s 1.12s % Output : Proof 0.90s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : ALG235-1 : TPTP v8.1.0. Released v4.0.0. % 0.06/0.12 % Command : moca.sh %s % 0.12/0.33 % Computer : n029.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 8 16:08:06 EDT 2022 % 0.12/0.33 % CPUTime : % 0.90/1.12 % SZS status Unsatisfiable % 0.90/1.12 % SZS output start Proof % 0.90/1.12 The input problem is unsatisfiable because % 0.90/1.12 % 0.90/1.12 [1] the following set of Horn clauses is unsatisfiable: % 0.90/1.12 % 0.90/1.12 mult(A, mult(B, mult(A, B))) = mult(A, B) % 0.90/1.12 mult(A, mult(B, mult(C, D))) = mult(C, mult(B, mult(A, D))) % 0.90/1.12 mult(mult(A, mult(B, mult(C, B))), D) = mult(A, mult(D, mult(mult(C, B), D))) % 0.90/1.12 mult(a, mult(b, mult(a, mult(c, mult(d, c))))) = mult(a, mult(b, mult(d, c))) ==> \bottom % 0.90/1.12 % 0.90/1.12 This holds because % 0.90/1.12 % 0.90/1.12 [2] the following E entails the following G (Claessen-Smallbone's transformation (2018)): % 0.90/1.12 % 0.90/1.12 E: % 0.90/1.12 f1(mult(a, mult(b, mult(a, mult(c, mult(d, c)))))) = true__ % 0.90/1.12 f1(mult(a, mult(b, mult(d, c)))) = false__ % 0.90/1.12 mult(A, mult(B, mult(A, B))) = mult(A, B) % 0.90/1.12 mult(A, mult(B, mult(C, D))) = mult(C, mult(B, mult(A, D))) % 0.90/1.12 mult(mult(A, mult(B, mult(C, B))), D) = mult(A, mult(D, mult(mult(C, B), D))) % 0.90/1.12 G: % 0.90/1.12 true__ = false__ % 0.90/1.12 % 0.90/1.12 This holds because % 0.90/1.12 % 0.90/1.12 [3] E entails the following ordered TRS and the lhs and rhs of G join by the TRS: % 0.90/1.12 % 0.90/1.12 mult(A, mult(B, mult(C, D))) = mult(C, mult(B, mult(A, D))) % 0.90/1.12 mult(Y0, mult(X2, mult(Y2, mult(Y1, X3)))) = mult(Y2, mult(Y1, mult(Y0, mult(X2, X3)))) % 0.90/1.12 mult(Y0, mult(Y1, mult(X2, mult(X1, mult(Y2, X3))))) = mult(Y2, mult(Y1, mult(Y0, mult(X1, mult(X2, X3))))) % 0.90/1.12 mult(Y0, mult(Y1, mult(Y2, X1))) = mult(Y2, mult(Y1, mult(Y0, mult(X1, mult(Y2, X1))))) % 0.90/1.12 mult(mult(A, mult(B, mult(C, B))), D) = mult(A, mult(D, mult(mult(C, B), D))) % 0.90/1.12 mult(mult(Y0, mult(mult(X1, mult(Y2, X1)), mult(Y2, X1))), Y3) = mult(Y0, mult(Y3, mult(mult(Y2, X1), Y3))) % 0.90/1.12 f1(mult(a, mult(b, mult(a, mult(c, mult(d, c)))))) -> true__ % 0.90/1.12 f1(mult(a, mult(b, mult(d, c)))) -> false__ % 0.90/1.12 mult(A, mult(B, mult(A, B))) -> mult(A, B) % 0.90/1.12 mult(Y0, mult(X1, mult(X2, mult(mult(X1, mult(X2, X3)), mult(Y0, X3))))) -> mult(Y0, mult(X1, mult(X2, X3))) % 0.90/1.12 mult(Y0, mult(X1, mult(X2, mult(mult(X1, mult(X2, mult(X1, Y0))), Y0)))) -> mult(X2, mult(X1, Y0)) % 0.90/1.12 mult(Y0, mult(X2, mult(Y0, mult(mult(X2, X3), X3)))) -> mult(Y0, mult(X2, X3)) % 0.90/1.12 mult(Y0, mult(mult(X1, mult(Y0, X1)), mult(Y0, X1))) -> mult(Y0, X1) % 0.90/1.12 mult(Y0, mult(mult(mult(X1, mult(Y0, X1)), mult(Y0, X1)), mult(Y0, X1))) -> mult(Y0, X1) % 0.90/1.12 mult(Y2, mult(Y1, mult(Y0, mult(Y1, Y2)))) -> mult(Y0, mult(Y1, Y2)) % 0.90/1.12 mult(Y2, mult(Y3, mult(mult(Y2, Y1), Y3))) -> mult(mult(Y2, Y1), Y3) % 0.90/1.12 mult(mult(X1, mult(Y1, X1)), mult(Y1, mult(Y2, mult(Y1, X1)))) -> mult(Y2, mult(Y1, X1)) % 0.90/1.12 mult(mult(Y2, Y1), Y1) -> mult(Y2, Y1) % 0.90/1.12 true__ -> false__ % 0.90/1.12 with the LPO induced by % 0.90/1.12 c > d > b > a > f1 > mult > true__ > false__ % 0.90/1.12 % 0.90/1.12 % SZS output end Proof % 0.90/1.12 %------------------------------------------------------------------------------