%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : KRS122+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 : n018.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:58 EDT 2022 % Result : Unsatisfiable 11.95s 12.16s % Output : Proof 11.95s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : KRS122+1 : TPTP v8.1.0. Released v3.1.0. % 0.11/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n018.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 10:54:05 EDT 2022 % 0.12/0.33 % CPUTime : % 11.95/12.16 % SZS status Theorem % 11.95/12.16 (* PROOF-FOUND *) % 11.95/12.16 (* BEGIN-PROOF *) % 11.95/12.16 % SZS output start Proof % 11.95/12.16 1. (rf (i2003_11_14_17_21_55116) T_0) (-. (rf (i2003_11_14_17_21_55116) T_0)) ### Axiom % 11.95/12.16 2. (-. (rinvF T_0 (i2003_11_14_17_21_55116))) (rf (i2003_11_14_17_21_55116) T_0) ### Definition-Pseudo(rinvF) 1 % 11.95/12.16 3. (rf (i2003_11_14_17_21_55116) T_0) (-. (rf (i2003_11_14_17_21_55116) T_0)) ### Axiom % 11.95/12.16 4. (rf (i2003_11_14_17_21_55116) T_1) (-. (rf (i2003_11_14_17_21_55116) T_1)) ### Axiom % 11.95/12.16 5. (T_0 = T_1) (T_0 != T_1) ### Axiom % 11.95/12.16 6. ((cp1 T_0) /\ (All Y, ((rinvF T_0 Y) => (ca_Vx3 Y)))) (-. ((cp1 T_0) /\ (All Y, ((rinvF T_0 Y) => (ca_Vx3 Y))))) ### Axiom % 11.95/12.16 7. (-. (ca_Ax2 T_0)) ((cp1 T_0) /\ (All Y, ((rinvF T_0 Y) => (ca_Vx3 Y)))) ### Definition-Pseudo(ca_Ax2) 6 % 11.95/12.16 8. (Ex Y, (ra_Px1 T_1 Y)) (-. (Ex Y, (ra_Px1 T_1 Y))) ### Axiom % 11.95/12.16 9. (cp1 T_1) (Ex Y, (ra_Px1 T_1 Y)) ### Definition-Pseudo(cp1) 8 % 11.95/12.16 10. ((cp1 T_1) /\ (All Y, ((rinvF T_1 Y) => (ca_Vx3 Y)))) (Ex Y, (ra_Px1 T_1 Y)) ### And 9 % 11.95/12.16 11. (ca_Ax2 T_1) (Ex Y, (ra_Px1 T_1 Y)) ### Definition-Pseudo(ca_Ax2) 10 % 11.95/12.16 12. (((T_0 = T_1) /\ (ca_Ax2 T_0)) => (ca_Ax2 T_1)) (Ex Y, (ra_Px1 T_1 Y)) ((cp1 T_0) /\ (All Y, ((rinvF T_0 Y) => (ca_Vx3 Y)))) (T_0 = T_1) ### DisjTree 5 7 11 % 11.95/12.16 13. (All B, (((T_0 = B) /\ (ca_Ax2 T_0)) => (ca_Ax2 B))) (T_0 = T_1) ((cp1 T_0) /\ (All Y, ((rinvF T_0 Y) => (ca_Vx3 Y)))) (Ex Y, (ra_Px1 T_1 Y)) ### All 12 % 11.95/12.16 14. (All A, (All B, (((A = B) /\ (ca_Ax2 A)) => (ca_Ax2 B)))) (Ex Y, (ra_Px1 T_1 Y)) ((cp1 T_0) /\ (All Y, ((rinvF T_0 Y) => (ca_Vx3 Y)))) (T_0 = T_1) ### All 13 % 11.95/12.16 15. (((rf (i2003_11_14_17_21_55116) T_0) /\ (rf (i2003_11_14_17_21_55116) T_1)) => (T_0 = T_1)) ((cp1 T_0) /\ (All Y, ((rinvF T_0 Y) => (ca_Vx3 Y)))) (Ex Y, (ra_Px1 T_1 Y)) (All A, (All B, (((A = B) /\ (ca_Ax2 A)) => (ca_Ax2 B)))) (rf (i2003_11_14_17_21_55116) T_1) (rf (i2003_11_14_17_21_55116) T_0) ### DisjTree 3 4 14 % 11.95/12.16 16. (All Z, (((rf (i2003_11_14_17_21_55116) T_0) /\ (rf (i2003_11_14_17_21_55116) Z)) => (T_0 = Z))) (rf (i2003_11_14_17_21_55116) T_0) (rf (i2003_11_14_17_21_55116) T_1) (All A, (All B, (((A = B) /\ (ca_Ax2 A)) => (ca_Ax2 B)))) (Ex Y, (ra_Px1 T_1 Y)) ((cp1 T_0) /\ (All Y, ((rinvF T_0 Y) => (ca_Vx3 Y)))) ### All 15 % 11.95/12.16 17. (cp1xcomp T_1) ((cp1 T_0) /\ (All Y, ((rinvF T_0 Y) => (ca_Vx3 Y)))) (All A, (All B, (((A = B) /\ (ca_Ax2 A)) => (ca_Ax2 B)))) (rf (i2003_11_14_17_21_55116) T_1) (rf (i2003_11_14_17_21_55116) T_0) (All Z, (((rf (i2003_11_14_17_21_55116) T_0) /\ (rf (i2003_11_14_17_21_55116) Z)) => (T_0 = Z))) ### Definition-Pseudo(cp1xcomp) 16 % 11.95/12.16 18. ((rf (i2003_11_14_17_21_55116) T_1) /\ (cp1xcomp T_1)) (All Z, (((rf (i2003_11_14_17_21_55116) T_0) /\ (rf (i2003_11_14_17_21_55116) Z)) => (T_0 = Z))) (rf (i2003_11_14_17_21_55116) T_0) (All A, (All B, (((A = B) /\ (ca_Ax2 A)) => (ca_Ax2 B)))) ((cp1 T_0) /\ (All Y, ((rinvF T_0 Y) => (ca_Vx3 Y)))) ### And 17 % 11.95/12.16 19. (Ex Y, ((rf (i2003_11_14_17_21_55116) Y) /\ (cp1xcomp Y))) ((cp1 T_0) /\ (All Y, ((rinvF T_0 Y) => (ca_Vx3 Y)))) (All A, (All B, (((A = B) /\ (ca_Ax2 A)) => (ca_Ax2 B)))) (rf (i2003_11_14_17_21_55116) T_0) (All Z, (((rf (i2003_11_14_17_21_55116) T_0) /\ (rf (i2003_11_14_17_21_55116) Z)) => (T_0 = Z))) ### Exists 18 % 11.95/12.16 20. (ca_Vx3 (i2003_11_14_17_21_55116)) (All Z, (((rf (i2003_11_14_17_21_55116) T_0) /\ (rf (i2003_11_14_17_21_55116) Z)) => (T_0 = Z))) (rf (i2003_11_14_17_21_55116) T_0) (All A, (All B, (((A = B) /\ (ca_Ax2 A)) => (ca_Ax2 B)))) ((cp1 T_0) /\ (All Y, ((rinvF T_0 Y) => (ca_Vx3 Y)))) ### Definition-Pseudo(ca_Vx3) 19 % 11.95/12.16 21. ((rinvF T_0 (i2003_11_14_17_21_55116)) => (ca_Vx3 (i2003_11_14_17_21_55116))) ((cp1 T_0) /\ (All Y, ((rinvF T_0 Y) => (ca_Vx3 Y)))) (All A, (All B, (((A = B) /\ (ca_Ax2 A)) => (ca_Ax2 B)))) (All Z, (((rf (i2003_11_14_17_21_55116) T_0) /\ (rf (i2003_11_14_17_21_55116) Z)) => (T_0 = Z))) (rf (i2003_11_14_17_21_55116) T_0) ### Imply 2 20 % 11.95/12.16 22. (All Y, ((rinvF T_0 Y) => (ca_Vx3 Y))) (rf (i2003_11_14_17_21_55116) T_0) (All Z, (((rf (i2003_11_14_17_21_55116) T_0) /\ (rf (i2003_11_14_17_21_55116) Z)) => (T_0 = Z))) (All A, (All B, (((A = B) /\ (ca_Ax2 A)) => (ca_Ax2 B)))) ((cp1 T_0) /\ (All Y, ((rinvF T_0 Y) => (ca_Vx3 Y)))) ### All 21 % 11.95/12.16 23. (All Y, (All Z, (((rf (i2003_11_14_17_21_55116) Y) /\ (rf (i2003_11_14_17_21_55116) Z)) => (Y = Z)))) ((cp1 T_0) /\ (All Y, ((rinvF T_0 Y) => (ca_Vx3 Y)))) (All A, (All B, (((A = B) /\ (ca_Ax2 A)) => (ca_Ax2 B)))) (rf (i2003_11_14_17_21_55116) T_0) (All Y, ((rinvF T_0 Y) => (ca_Vx3 Y))) ### All 22 % 11.95/12.16 24. (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All Y, ((rinvF T_0 Y) => (ca_Vx3 Y))) (rf (i2003_11_14_17_21_55116) T_0) (All A, (All B, (((A = B) /\ (ca_Ax2 A)) => (ca_Ax2 B)))) ((cp1 T_0) /\ (All Y, ((rinvF T_0 Y) => (ca_Vx3 Y)))) ### All 23 % 11.95/12.16 25. ((cp1 T_0) /\ (All Y, ((rinvF T_0 Y) => (ca_Vx3 Y)))) (All A, (All B, (((A = B) /\ (ca_Ax2 A)) => (ca_Ax2 B)))) (rf (i2003_11_14_17_21_55116) T_0) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) ### And 24 % 11.95/12.16 26. (ca_Ax2 T_0) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (rf (i2003_11_14_17_21_55116) T_0) (All A, (All B, (((A = B) /\ (ca_Ax2 A)) => (ca_Ax2 B)))) ### Definition-Pseudo(ca_Ax2) 25 % 11.95/12.16 27. ((rf (i2003_11_14_17_21_55116) T_0) /\ (ca_Ax2 T_0)) (All A, (All B, (((A = B) /\ (ca_Ax2 A)) => (ca_Ax2 B)))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) ### And 26 % 11.95/12.16 28. (Ex Y, ((rf (i2003_11_14_17_21_55116) Y) /\ (ca_Ax2 Y))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All A, (All B, (((A = B) /\ (ca_Ax2 A)) => (ca_Ax2 B)))) ### Exists 27 % 11.95/12.16 29. (cUnsatisfiable (i2003_11_14_17_21_55116)) (All A, (All B, (((A = B) /\ (ca_Ax2 A)) => (ca_Ax2 B)))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) ### Definition-Pseudo(cUnsatisfiable) 28 % 11.95/12.16 % SZS output end Proof % 11.95/12.16 (* END-PROOF *) %------------------------------------------------------------------------------