%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : KRS114+1 : TPTP v8.1.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n022.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 : Sun Jul 17 03:31:57 EDT 2022 % Result : Unsatisfiable 4.19s 4.40s % Output : Proof 4.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : KRS114+1 : TPTP v8.1.0. Released v3.1.0. % 0.03/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n022.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 : Tue Jun 7 07:19:05 EDT 2022 % 0.12/0.33 % CPUTime : % 4.19/4.40 % SZS status Theorem % 4.19/4.40 (* PROOF-FOUND *) % 4.19/4.40 (* BEGIN-PROOF *) % 4.19/4.40 % SZS output start Proof % 4.19/4.40 1. (rr T_0 T_1) (-. (rr T_0 T_1)) ### Axiom % 4.19/4.40 2. (-. (rinvR T_1 T_0)) (rr T_0 T_1) ### Definition-Pseudo(rinvR) 1 % 4.19/4.40 3. (rr (i2003_11_14_17_21_262) T_1) (-. (rr (i2003_11_14_17_21_262) T_1)) ### Axiom % 4.19/4.40 4. (-. (rinvR T_1 (i2003_11_14_17_21_262))) (rr (i2003_11_14_17_21_262) T_1) ### Definition-Pseudo(rinvR) 3 % 4.19/4.40 5. (T_0 = (i2003_11_14_17_21_262)) ((i2003_11_14_17_21_262) != T_0) ### Sym(=) % 4.19/4.40 6. (rs (i2003_11_14_17_21_262) T_2) (-. (rs (i2003_11_14_17_21_262) T_2)) ### Axiom % 4.19/4.40 7. (-. (rs T_0 T_2)) (rs T_0 T_2) ### Axiom % 4.19/4.40 8. ((((i2003_11_14_17_21_262) = T_0) /\ (rs (i2003_11_14_17_21_262) T_2)) => (rs T_0 T_2)) (-. (rs T_0 T_2)) (rs (i2003_11_14_17_21_262) T_2) (T_0 = (i2003_11_14_17_21_262)) ### DisjTree 5 6 7 % 4.19/4.40 9. (All C, ((((i2003_11_14_17_21_262) = T_0) /\ (rs (i2003_11_14_17_21_262) C)) => (rs T_0 C))) (T_0 = (i2003_11_14_17_21_262)) (rs (i2003_11_14_17_21_262) T_2) (-. (rs T_0 T_2)) ### All 8 % 4.19/4.40 10. (All B, (All C, ((((i2003_11_14_17_21_262) = B) /\ (rs (i2003_11_14_17_21_262) C)) => (rs B C)))) (-. (rs T_0 T_2)) (rs (i2003_11_14_17_21_262) T_2) (T_0 = (i2003_11_14_17_21_262)) ### All 9 % 4.19/4.40 11. (All A, (All B, (All C, (((A = B) /\ (rs A C)) => (rs B C))))) (T_0 = (i2003_11_14_17_21_262)) (rs (i2003_11_14_17_21_262) T_2) (-. (rs T_0 T_2)) ### All 10 % 4.19/4.40 12. (((rinvR T_1 T_0) /\ (rinvR T_1 (i2003_11_14_17_21_262))) => (T_0 = (i2003_11_14_17_21_262))) (-. (rs T_0 T_2)) (rs (i2003_11_14_17_21_262) T_2) (All A, (All B, (All C, (((A = B) /\ (rs A C)) => (rs B C))))) (rr (i2003_11_14_17_21_262) T_1) (rr T_0 T_1) ### DisjTree 2 4 11 % 4.19/4.40 13. (All Y1, (((rinvR T_1 T_0) /\ (rinvR T_1 Y1)) => (T_0 = Y1))) (rr T_0 T_1) (rr (i2003_11_14_17_21_262) T_1) (All A, (All B, (All C, (((A = B) /\ (rs A C)) => (rs B C))))) (rs (i2003_11_14_17_21_262) T_2) (-. (rs T_0 T_2)) ### All 12 % 4.19/4.40 14. (Ex Y, (ra_Px1 T_2 Y)) (-. (Ex Y, (ra_Px1 T_2 Y))) ### Axiom % 4.19/4.40 15. (cp T_2) (Ex Y, (ra_Px1 T_2 Y)) ### Definition-Pseudo(cp) 14 % 4.19/4.40 16. ((rs T_0 T_2) => (cp T_2)) (Ex Y, (ra_Px1 T_2 Y)) (rs (i2003_11_14_17_21_262) T_2) (All A, (All B, (All C, (((A = B) /\ (rs A C)) => (rs B C))))) (rr (i2003_11_14_17_21_262) T_1) (rr T_0 T_1) (All Y1, (((rinvR T_1 T_0) /\ (rinvR T_1 Y1)) => (T_0 = Y1))) ### Imply 13 15 % 4.19/4.40 17. (All Y, ((rs T_0 Y) => (cp Y))) (All Y1, (((rinvR T_1 T_0) /\ (rinvR T_1 Y1)) => (T_0 = Y1))) (rr T_0 T_1) (rr (i2003_11_14_17_21_262) T_1) (All A, (All B, (All C, (((A = B) /\ (rs A C)) => (rs B C))))) (rs (i2003_11_14_17_21_262) T_2) (Ex Y, (ra_Px1 T_2 Y)) ### All 16 % 4.19/4.40 18. (All Y0, (All Y1, (((rinvR T_1 Y0) /\ (rinvR T_1 Y1)) => (Y0 = Y1)))) (Ex Y, (ra_Px1 T_2 Y)) (rs (i2003_11_14_17_21_262) T_2) (All A, (All B, (All C, (((A = B) /\ (rs A C)) => (rs B C))))) (rr (i2003_11_14_17_21_262) T_1) (rr T_0 T_1) (All Y, ((rs T_0 Y) => (cp Y))) ### All 17 % 4.19/4.40 19. (cpxcomp T_2) (All Y, ((rs T_0 Y) => (cp Y))) (rr T_0 T_1) (rr (i2003_11_14_17_21_262) T_1) (All A, (All B, (All C, (((A = B) /\ (rs A C)) => (rs B C))))) (rs (i2003_11_14_17_21_262) T_2) (All Y0, (All Y1, (((rinvR T_1 Y0) /\ (rinvR T_1 Y1)) => (Y0 = Y1)))) ### Definition-Pseudo(cpxcomp) 18 % 4.19/4.40 20. ((cqxcomp T_2) /\ (cpxcomp T_2)) (All Y0, (All Y1, (((rinvR T_1 Y0) /\ (rinvR T_1 Y1)) => (Y0 = Y1)))) (rs (i2003_11_14_17_21_262) T_2) (All A, (All B, (All C, (((A = B) /\ (rs A C)) => (rs B C))))) (rr (i2003_11_14_17_21_262) T_1) (rr T_0 T_1) (All Y, ((rs T_0 Y) => (cp Y))) ### And 19 % 4.19/4.40 21. (ca_Ax3 T_2) (All Y, ((rs T_0 Y) => (cp Y))) (rr T_0 T_1) (rr (i2003_11_14_17_21_262) T_1) (All A, (All B, (All C, (((A = B) /\ (rs A C)) => (rs B C))))) (rs (i2003_11_14_17_21_262) T_2) (All Y0, (All Y1, (((rinvR T_1 Y0) /\ (rinvR T_1 Y1)) => (Y0 = Y1)))) ### Definition-Pseudo(ca_Ax3) 20 % 4.19/4.40 22. ((rs (i2003_11_14_17_21_262) T_2) /\ (ca_Ax3 T_2)) (All Y0, (All Y1, (((rinvR T_1 Y0) /\ (rinvR T_1 Y1)) => (Y0 = Y1)))) (All A, (All B, (All C, (((A = B) /\ (rs A C)) => (rs B C))))) (rr (i2003_11_14_17_21_262) T_1) (rr T_0 T_1) (All Y, ((rs T_0 Y) => (cp Y))) ### And 21 % 4.19/4.40 23. (Ex Y, ((rs (i2003_11_14_17_21_262) Y) /\ (ca_Ax3 Y))) (All Y, ((rs T_0 Y) => (cp Y))) (rr T_0 T_1) (rr (i2003_11_14_17_21_262) T_1) (All A, (All B, (All C, (((A = B) /\ (rs A C)) => (rs B C))))) (All Y0, (All Y1, (((rinvR T_1 Y0) /\ (rinvR T_1 Y1)) => (Y0 = Y1)))) ### Exists 22 % 4.19/4.40 24. (ca_Vx5 T_0) (All Y0, (All Y1, (((rinvR T_1 Y0) /\ (rinvR T_1 Y1)) => (Y0 = Y1)))) (All A, (All B, (All C, (((A = B) /\ (rs A C)) => (rs B C))))) (rr (i2003_11_14_17_21_262) T_1) (rr T_0 T_1) (Ex Y, ((rs (i2003_11_14_17_21_262) Y) /\ (ca_Ax3 Y))) ### Definition-Pseudo(ca_Vx5) 23 % 4.19/4.40 25. (rinvR T_1 T_0) (Ex Y, ((rs (i2003_11_14_17_21_262) Y) /\ (ca_Ax3 Y))) (rr (i2003_11_14_17_21_262) T_1) (All A, (All B, (All C, (((A = B) /\ (rs A C)) => (rs B C))))) (All Y0, (All Y1, (((rinvR T_1 Y0) /\ (rinvR T_1 Y1)) => (Y0 = Y1)))) (ca_Vx5 T_0) ### Definition-Pseudo(rinvR) 24 % 4.19/4.40 26. ((rinvR T_1 T_0) /\ (ca_Vx5 T_0)) (All Y0, (All Y1, (((rinvR T_1 Y0) /\ (rinvR T_1 Y1)) => (Y0 = Y1)))) (All A, (All B, (All C, (((A = B) /\ (rs A C)) => (rs B C))))) (rr (i2003_11_14_17_21_262) T_1) (Ex Y, ((rs (i2003_11_14_17_21_262) Y) /\ (ca_Ax3 Y))) ### And 25 % 4.19/4.40 27. (Ex Y, ((rinvR T_1 Y) /\ (ca_Vx5 Y))) (Ex Y, ((rs (i2003_11_14_17_21_262) Y) /\ (ca_Ax3 Y))) (rr (i2003_11_14_17_21_262) T_1) (All A, (All B, (All C, (((A = B) /\ (rs A C)) => (rs B C))))) (All Y0, (All Y1, (((rinvR T_1 Y0) /\ (rinvR T_1 Y1)) => (Y0 = Y1)))) ### Exists 26 % 4.19/4.40 28. ((All Y0, (All Y1, (((rinvR T_1 Y0) /\ (rinvR T_1 Y1)) => (Y0 = Y1)))) /\ (Ex Y, ((rinvR T_1 Y) /\ (ca_Vx5 Y)))) (All A, (All B, (All C, (((A = B) /\ (rs A C)) => (rs B C))))) (rr (i2003_11_14_17_21_262) T_1) (Ex Y, ((rs (i2003_11_14_17_21_262) Y) /\ (ca_Ax3 Y))) ### And 27 % 4.19/4.40 29. (ca_Ax4 T_1) (Ex Y, ((rs (i2003_11_14_17_21_262) Y) /\ (ca_Ax3 Y))) (rr (i2003_11_14_17_21_262) T_1) (All A, (All B, (All C, (((A = B) /\ (rs A C)) => (rs B C))))) ### Definition-Pseudo(ca_Ax4) 28 % 4.19/4.40 30. ((rr (i2003_11_14_17_21_262) T_1) /\ (ca_Ax4 T_1)) (All A, (All B, (All C, (((A = B) /\ (rs A C)) => (rs B C))))) (Ex Y, ((rs (i2003_11_14_17_21_262) Y) /\ (ca_Ax3 Y))) ### And 29 % 4.19/4.40 31. (Ex Y, ((rr (i2003_11_14_17_21_262) Y) /\ (ca_Ax4 Y))) (Ex Y, ((rs (i2003_11_14_17_21_262) Y) /\ (ca_Ax3 Y))) (All A, (All B, (All C, (((A = B) /\ (rs A C)) => (rs B C))))) ### Exists 30 % 4.19/4.40 32. ((Ex Y, ((rr (i2003_11_14_17_21_262) Y) /\ (ca_Ax4 Y))) /\ (Ex Y, ((rs (i2003_11_14_17_21_262) Y) /\ (ca_Ax3 Y)))) (All A, (All B, (All C, (((A = B) /\ (rs A C)) => (rs B C))))) ### And 31 % 4.19/4.40 33. (cUnsatisfiable (i2003_11_14_17_21_262)) (All A, (All B, (All C, (((A = B) /\ (rs A C)) => (rs B C))))) ### Definition-Pseudo(cUnsatisfiable) 32 % 4.19/4.40 % SZS output end Proof % 4.19/4.40 (* END-PROOF *) %------------------------------------------------------------------------------