%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : KRS088+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:52 EDT 2022 % Result : Unsatisfiable 9.51s 9.70s % Output : Proof 9.51s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : KRS088+1 : TPTP v8.1.0. Released v3.1.0. % 0.03/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.13/0.34 % Computer : n022.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Tue Jun 7 19:40:20 EDT 2022 % 0.13/0.34 % CPUTime : % 9.51/9.70 % SZS status Theorem % 9.51/9.70 (* PROOF-FOUND *) % 9.51/9.70 (* BEGIN-PROOF *) % 9.51/9.70 % SZS output start Proof % 9.51/9.70 1. (rf (i2003_11_14_17_19_49673) T_0) (-. (rf (i2003_11_14_17_19_49673) T_0)) ### Axiom % 9.51/9.70 2. (-. (rinvF T_0 (i2003_11_14_17_19_49673))) (rf (i2003_11_14_17_19_49673) T_0) ### Definition-Pseudo(rinvF) 1 % 9.51/9.70 3. (rf (i2003_11_14_17_19_49673) T_0) (-. (rf (i2003_11_14_17_19_49673) T_0)) ### Axiom % 9.51/9.70 4. (rf (i2003_11_14_17_19_49673) T_1) (-. (rf (i2003_11_14_17_19_49673) T_1)) ### Axiom % 9.51/9.70 5. (T_0 != T_1) (T_0 = T_1) ### Axiom % 9.51/9.70 6. (((rf (i2003_11_14_17_19_49673) T_0) /\ (rf (i2003_11_14_17_19_49673) T_1)) => (T_0 = T_1)) (T_0 != T_1) (rf (i2003_11_14_17_19_49673) T_1) (rf (i2003_11_14_17_19_49673) T_0) ### DisjTree 3 4 5 % 9.51/9.70 7. (All Z, (((rf (i2003_11_14_17_19_49673) T_0) /\ (rf (i2003_11_14_17_19_49673) Z)) => (T_0 = Z))) (rf (i2003_11_14_17_19_49673) T_0) (rf (i2003_11_14_17_19_49673) T_1) (T_0 != T_1) ### All 6 % 9.51/9.70 8. (cp1 T_0) (-. (cp1 T_0)) ### Axiom % 9.51/9.70 9. (-. (cp1 T_1)) (cp1 T_1) ### Axiom % 9.51/9.70 10. (((T_0 = T_1) /\ (cp1 T_0)) => (cp1 T_1)) (-. (cp1 T_1)) (cp1 T_0) (rf (i2003_11_14_17_19_49673) T_1) (rf (i2003_11_14_17_19_49673) T_0) (All Z, (((rf (i2003_11_14_17_19_49673) T_0) /\ (rf (i2003_11_14_17_19_49673) Z)) => (T_0 = Z))) ### DisjTree 7 8 9 % 9.51/9.70 11. (All B, (((T_0 = B) /\ (cp1 T_0)) => (cp1 B))) (All Z, (((rf (i2003_11_14_17_19_49673) T_0) /\ (rf (i2003_11_14_17_19_49673) Z)) => (T_0 = Z))) (rf (i2003_11_14_17_19_49673) T_0) (rf (i2003_11_14_17_19_49673) T_1) (cp1 T_0) (-. (cp1 T_1)) ### All 10 % 9.51/9.70 12. ((rf (i2003_11_14_17_19_49673) T_1) /\ (-. (cp1 T_1))) (cp1 T_0) (rf (i2003_11_14_17_19_49673) T_0) (All Z, (((rf (i2003_11_14_17_19_49673) T_0) /\ (rf (i2003_11_14_17_19_49673) Z)) => (T_0 = Z))) (All B, (((T_0 = B) /\ (cp1 T_0)) => (cp1 B))) ### And 11 % 9.51/9.70 13. (Ex W, ((rf (i2003_11_14_17_19_49673) W) /\ (-. (cp1 W)))) (All B, (((T_0 = B) /\ (cp1 T_0)) => (cp1 B))) (All Z, (((rf (i2003_11_14_17_19_49673) T_0) /\ (rf (i2003_11_14_17_19_49673) Z)) => (T_0 = Z))) (rf (i2003_11_14_17_19_49673) T_0) (cp1 T_0) ### Exists 12 % 9.51/9.70 14. ((rinvF T_0 (i2003_11_14_17_19_49673)) => (Ex W, ((rf (i2003_11_14_17_19_49673) W) /\ (-. (cp1 W))))) (cp1 T_0) (All Z, (((rf (i2003_11_14_17_19_49673) T_0) /\ (rf (i2003_11_14_17_19_49673) Z)) => (T_0 = Z))) (All B, (((T_0 = B) /\ (cp1 T_0)) => (cp1 B))) (rf (i2003_11_14_17_19_49673) T_0) ### Imply 2 13 % 9.51/9.70 15. (All Z, ((rinvF T_0 Z) => (Ex W, ((rf Z W) /\ (-. (cp1 W)))))) (rf (i2003_11_14_17_19_49673) T_0) (All B, (((T_0 = B) /\ (cp1 T_0)) => (cp1 B))) (All Z, (((rf (i2003_11_14_17_19_49673) T_0) /\ (rf (i2003_11_14_17_19_49673) Z)) => (T_0 = Z))) (cp1 T_0) ### All 14 % 9.51/9.70 16. (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (cp1 T_0) (All Z, (((rf (i2003_11_14_17_19_49673) T_0) /\ (rf (i2003_11_14_17_19_49673) Z)) => (T_0 = Z))) (rf (i2003_11_14_17_19_49673) T_0) (All Z, ((rinvF T_0 Z) => (Ex W, ((rf Z W) /\ (-. (cp1 W)))))) ### All 15 % 9.51/9.70 17. (All Y, (All Z, (((rf (i2003_11_14_17_19_49673) Y) /\ (rf (i2003_11_14_17_19_49673) Z)) => (Y = Z)))) (All Z, ((rinvF T_0 Z) => (Ex W, ((rf Z W) /\ (-. (cp1 W)))))) (rf (i2003_11_14_17_19_49673) T_0) (cp1 T_0) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) ### All 16 % 9.51/9.70 18. (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (cp1 T_0) (rf (i2003_11_14_17_19_49673) T_0) (All Z, ((rinvF T_0 Z) => (Ex W, ((rf Z W) /\ (-. (cp1 W)))))) ### All 17 % 9.51/9.70 19. ((rf (i2003_11_14_17_19_49673) T_0) /\ ((All Z, ((rinvF T_0 Z) => (Ex W, ((rf Z W) /\ (-. (cp1 W)))))) /\ (cp1 T_0))) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) ### ConjTree 18 % 9.51/9.70 20. (Ex Y, ((rf (i2003_11_14_17_19_49673) Y) /\ ((All Z, ((rinvF Y Z) => (Ex W, ((rf Z W) /\ (-. (cp1 W)))))) /\ (cp1 Y)))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) ### Exists 19 % 9.51/9.70 21. (cUnsatisfiable (i2003_11_14_17_19_49673)) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (All X, (All Y, (All Z, (((rf X Y) /\ (rf X Z)) => (Y = Z))))) ### Definition-Pseudo(cUnsatisfiable) 20 % 9.51/9.70 % SZS output end Proof % 9.51/9.70 (* END-PROOF *) %------------------------------------------------------------------------------