%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : KRS254+1 : TPTP v8.1.0. Bugfixed v5.4.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n026.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:32:17 EDT 2022 % Result : Theorem 3.53s 3.75s % Output : Proof 3.53s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : KRS254+1 : TPTP v8.1.0. Bugfixed v5.4.0. % 0.07/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.13/0.33 % Computer : n026.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Tue Jun 7 14:50:16 EDT 2022 % 0.13/0.33 % CPUTime : % 3.53/3.75 % SZS status Theorem % 3.53/3.75 (* PROOF-FOUND *) % 3.53/3.75 (* BEGIN-PROOF *) % 3.53/3.75 % SZS output start Proof % 3.53/3.75 1. (-. (model T_0 T_1)) (model T_0 T_1) ### Axiom % 3.53/3.75 2. (All I, (model I T_1)) (-. (model T_0 T_1)) ### All 1 % 3.53/3.75 3. (-. ((model T_0 T_2) => (model T_0 T_1))) (All I, (model I T_1)) ### NotImply 2 % 3.53/3.75 4. (-. (All I1, ((model I1 T_2) => (model I1 T_1)))) (All I, (model I T_1)) ### NotAllEx 3 % 3.53/3.75 5. (Ex I1, (model I1 T_2)) (-. (Ex I1, (model I1 T_2))) ### Axiom % 3.53/3.75 6. (-. ((-. (Ex I1, (model I1 T_2))) => (-. (Ex I2, (model I2 T_1))))) (Ex I1, (model I1 T_2)) ### NotImply 5 % 3.53/3.75 7. (-. (status T_2 T_1 (unp))) (status T_2 T_1 (unp)) ### Axiom % 3.53/3.75 8. (((-. (Ex I1, (model I1 T_2))) => (-. (Ex I2, (model I2 T_1)))) <=> (status T_2 T_1 (unp))) (-. (status T_2 T_1 (unp))) (Ex I1, (model I1 T_2)) ### Equiv 6 7 % 3.53/3.75 9. (All C, (((-. (Ex I1, (model I1 T_2))) => (-. (Ex I2, (model I2 C)))) <=> (status T_2 C (unp)))) (Ex I1, (model I1 T_2)) (-. (status T_2 T_1 (unp))) ### All 8 % 3.53/3.75 10. (All Ax, (All C, (((-. (Ex I1, (model I1 Ax))) => (-. (Ex I2, (model I2 C)))) <=> (status Ax C (unp))))) (-. (status T_2 T_1 (unp))) (Ex I1, (model I1 T_2)) ### All 9 % 3.53/3.75 11. (status T_2 T_1 (thm)) (-. (status T_2 T_1 (thm))) ### Axiom % 3.53/3.75 12. (-. ((status T_2 T_1 (unp)) /\ (status T_2 T_1 (thm)))) (status T_2 T_1 (thm)) (Ex I1, (model I1 T_2)) (All Ax, (All C, (((-. (Ex I1, (model I1 Ax))) => (-. (Ex I2, (model I2 C)))) <=> (status Ax C (unp))))) ### NotAnd 10 11 % 3.53/3.75 13. (-. (Ex C, ((status T_2 C (unp)) /\ (status T_2 C (thm))))) (All Ax, (All C, (((-. (Ex I1, (model I1 Ax))) => (-. (Ex I2, (model I2 C)))) <=> (status Ax C (unp))))) (Ex I1, (model I1 T_2)) (status T_2 T_1 (thm)) ### NotExists 12 % 3.53/3.75 14. ((All I1, ((model I1 T_2) => (model I1 T_1))) <=> (status T_2 T_1 (thm))) (Ex I1, (model I1 T_2)) (All Ax, (All C, (((-. (Ex I1, (model I1 Ax))) => (-. (Ex I2, (model I2 C)))) <=> (status Ax C (unp))))) (-. (Ex C, ((status T_2 C (unp)) /\ (status T_2 C (thm))))) (All I, (model I T_1)) ### Equiv 4 13 % 3.53/3.75 15. (All C, ((All I1, ((model I1 T_2) => (model I1 C))) <=> (status T_2 C (thm)))) (All I, (model I T_1)) (-. (Ex C, ((status T_2 C (unp)) /\ (status T_2 C (thm))))) (All Ax, (All C, (((-. (Ex I1, (model I1 Ax))) => (-. (Ex I2, (model I2 C)))) <=> (status Ax C (unp))))) (Ex I1, (model I1 T_2)) ### All 14 % 3.53/3.75 16. (All Ax, (All C, ((All I1, ((model I1 Ax) => (model I1 C))) <=> (status Ax C (thm))))) (Ex I1, (model I1 T_2)) (All Ax, (All C, (((-. (Ex I1, (model I1 Ax))) => (-. (Ex I2, (model I2 C)))) <=> (status Ax C (unp))))) (-. (Ex C, ((status T_2 C (unp)) /\ (status T_2 C (thm))))) (All I, (model I T_1)) ### All 15 % 3.53/3.75 17. (-. (Ex Ax, (Ex C, ((status Ax C (unp)) /\ (status Ax C (thm)))))) (All I, (model I T_1)) (All Ax, (All C, (((-. (Ex I1, (model I1 Ax))) => (-. (Ex I2, (model I2 C)))) <=> (status Ax C (unp))))) (Ex I1, (model I1 T_2)) (All Ax, (All C, ((All I1, ((model I1 Ax) => (model I1 C))) <=> (status Ax C (thm))))) ### NotExists 16 % 3.53/3.75 18. (Ex F, (All I, (model I F))) (All Ax, (All C, ((All I1, ((model I1 Ax) => (model I1 C))) <=> (status Ax C (thm))))) (Ex I1, (model I1 T_2)) (All Ax, (All C, (((-. (Ex I1, (model I1 Ax))) => (-. (Ex I2, (model I2 C)))) <=> (status Ax C (unp))))) (-. (Ex Ax, (Ex C, ((status Ax C (unp)) /\ (status Ax C (thm)))))) ### Exists 17 % 3.53/3.75 19. ((Ex I1, (model I1 T_2)) /\ ((All I1, ((model I1 T_2) => (model I1 T_3))) /\ ((Ex I3, ((-. (model I3 T_2)) /\ (model I3 T_3))) /\ (Ex I4, (-. (model I4 T_3)))))) (-. (Ex Ax, (Ex C, ((status Ax C (unp)) /\ (status Ax C (thm)))))) (All Ax, (All C, (((-. (Ex I1, (model I1 Ax))) => (-. (Ex I2, (model I2 C)))) <=> (status Ax C (unp))))) (All Ax, (All C, ((All I1, ((model I1 Ax) => (model I1 C))) <=> (status Ax C (thm))))) (Ex F, (All I, (model I F))) ### ConjTree 18 % 3.53/3.75 20. (Ex C, ((Ex I1, (model I1 T_2)) /\ ((All I1, ((model I1 T_2) => (model I1 C))) /\ ((Ex I3, ((-. (model I3 T_2)) /\ (model I3 C))) /\ (Ex I4, (-. (model I4 C))))))) (Ex F, (All I, (model I F))) (All Ax, (All C, ((All I1, ((model I1 Ax) => (model I1 C))) <=> (status Ax C (thm))))) (All Ax, (All C, (((-. (Ex I1, (model I1 Ax))) => (-. (Ex I2, (model I2 C)))) <=> (status Ax C (unp))))) (-. (Ex Ax, (Ex C, ((status Ax C (unp)) /\ (status Ax C (thm)))))) ### Exists 19 % 3.53/3.75 21. (Ex Ax, (Ex C, ((Ex I1, (model I1 Ax)) /\ ((All I1, ((model I1 Ax) => (model I1 C))) /\ ((Ex I3, ((-. (model I3 Ax)) /\ (model I3 C))) /\ (Ex I4, (-. (model I4 C)))))))) (-. (Ex Ax, (Ex C, ((status Ax C (unp)) /\ (status Ax C (thm)))))) (All Ax, (All C, (((-. (Ex I1, (model I1 Ax))) => (-. (Ex I2, (model I2 C)))) <=> (status Ax C (unp))))) (All Ax, (All C, ((All I1, ((model I1 Ax) => (model I1 C))) <=> (status Ax C (thm))))) (Ex F, (All I, (model I F))) ### Exists 20 % 3.53/3.75 22. (-. (mighta (unp) (thm))) (Ex F, (All I, (model I F))) (All Ax, (All C, ((All I1, ((model I1 Ax) => (model I1 C))) <=> (status Ax C (thm))))) (All Ax, (All C, (((-. (Ex I1, (model I1 Ax))) => (-. (Ex I2, (model I2 C)))) <=> (status Ax C (unp))))) (Ex Ax, (Ex C, ((Ex I1, (model I1 Ax)) /\ ((All I1, ((model I1 Ax) => (model I1 C))) /\ ((Ex I3, ((-. (model I3 Ax)) /\ (model I3 C))) /\ (Ex I4, (-. (model I4 C)))))))) ### Definition-Pseudo(mighta) 21 % 3.53/3.75 % SZS output end Proof % 3.53/3.75 (* END-PROOF *) %------------------------------------------------------------------------------