%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : KRS189+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 : n017.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:09 EDT 2022 % Result : Theorem 5.71s 5.91s % Output : Proof 5.71s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : KRS189+1 : TPTP v8.1.0. Bugfixed v5.4.0. % 0.03/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n017.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 17:24:02 EDT 2022 % 0.12/0.33 % CPUTime : % 5.71/5.91 % SZS status Theorem % 5.71/5.91 (* PROOF-FOUND *) % 5.71/5.91 (* BEGIN-PROOF *) % 5.71/5.91 % SZS output start Proof % 5.71/5.91 1. (Ex I1, (model I1 T_0)) (-. (Ex I1, (model I1 T_0))) ### Axiom % 5.71/5.91 2. (status T_0 T_1 (eth)) (-. (status T_0 T_1 (eth))) ### Axiom % 5.71/5.91 3. (-. (All I2, ((model I2 T_0) <=> (model I2 T_1)))) (All I2, ((model I2 T_0) <=> (model I2 T_1))) ### Axiom % 5.71/5.91 4. ((Ex I1, (model I1 T_0)) /\ ((Ex I2, (-. (model I2 T_0))) /\ (All I2, ((model I2 T_0) <=> (model I2 T_1))))) (-. (All I2, ((model I2 T_0) <=> (model I2 T_1)))) ### ConjTree 3 % 5.71/5.91 5. (((Ex I1, (model I1 T_0)) /\ ((Ex I2, (-. (model I2 T_0))) /\ (All I2, ((model I2 T_0) <=> (model I2 T_1))))) <=> (status T_0 T_1 (eth))) (-. (All I2, ((model I2 T_0) <=> (model I2 T_1)))) (status T_0 T_1 (eth)) ### Equiv 2 4 % 5.71/5.91 6. (All C, (((Ex I1, (model I1 T_0)) /\ ((Ex I2, (-. (model I2 T_0))) /\ (All I2, ((model I2 T_0) <=> (model I2 C))))) <=> (status T_0 C (eth)))) (status T_0 T_1 (eth)) (-. (All I2, ((model I2 T_0) <=> (model I2 T_1)))) ### All 5 % 5.71/5.91 7. (-. ((Ex I1, (model I1 T_0)) /\ (All I2, ((model I2 T_0) <=> (model I2 T_1))))) (status T_0 T_1 (eth)) (All C, (((Ex I1, (model I1 T_0)) /\ ((Ex I2, (-. (model I2 T_0))) /\ (All I2, ((model I2 T_0) <=> (model I2 C))))) <=> (status T_0 C (eth)))) (Ex I1, (model I1 T_0)) ### NotAnd 1 6 % 5.71/5.91 8. (model T_2 T_0) (-. (model T_2 T_0)) ### Axiom % 5.71/5.91 9. (-. (model T_2 T_1)) (model T_2 T_1) ### Axiom % 5.71/5.91 10. ((model T_2 T_0) <=> (model T_2 T_1)) (-. (model T_2 T_1)) (model T_2 T_0) ### Equiv 8 9 % 5.71/5.91 11. (All I2, ((model I2 T_0) <=> (model I2 T_1))) (model T_2 T_0) (-. (model T_2 T_1)) ### All 10 % 5.71/5.91 12. ((Ex I1, (model I1 T_0)) /\ (All I2, ((model I2 T_0) <=> (model I2 T_1)))) (-. (model T_2 T_1)) (model T_2 T_0) ### And 11 % 5.71/5.91 13. (((Ex I1, (model I1 T_0)) /\ (All I2, ((model I2 T_0) <=> (model I2 T_1)))) <=> (status T_0 T_1 (eqv))) (model T_2 T_0) (-. (model T_2 T_1)) (Ex I1, (model I1 T_0)) (All C, (((Ex I1, (model I1 T_0)) /\ ((Ex I2, (-. (model I2 T_0))) /\ (All I2, ((model I2 T_0) <=> (model I2 C))))) <=> (status T_0 C (eth)))) (status T_0 T_1 (eth)) ### Equiv 7 12 % 5.71/5.91 14. (All C, (((Ex I1, (model I1 T_0)) /\ (All I2, ((model I2 T_0) <=> (model I2 C)))) <=> (status T_0 C (eqv)))) (status T_0 T_1 (eth)) (All C, (((Ex I1, (model I1 T_0)) /\ ((Ex I2, (-. (model I2 T_0))) /\ (All I2, ((model I2 T_0) <=> (model I2 C))))) <=> (status T_0 C (eth)))) (Ex I1, (model I1 T_0)) (-. (model T_2 T_1)) (model T_2 T_0) ### All 13 % 5.71/5.91 15. (-. (-. (Ex I1, (model I1 T_0)))) (model T_2 T_0) (-. (model T_2 T_1)) (All C, (((Ex I1, (model I1 T_0)) /\ ((Ex I2, (-. (model I2 T_0))) /\ (All I2, ((model I2 T_0) <=> (model I2 C))))) <=> (status T_0 C (eth)))) (status T_0 T_1 (eth)) (All C, (((Ex I1, (model I1 T_0)) /\ (All I2, ((model I2 T_0) <=> (model I2 C)))) <=> (status T_0 C (eqv)))) ### NotNot 14 % 5.71/5.91 16. (model T_2 T_0) (-. (model T_2 T_0)) ### Axiom % 5.71/5.91 17. (-. (Ex I1, (model I1 T_0))) (model T_2 T_0) ### NotExists 16 % 5.71/5.91 18. ((-. (Ex I1, (model I1 T_0))) <=> (status T_0 zenon_X3 (cax))) (All C, (((Ex I1, (model I1 T_0)) /\ (All I2, ((model I2 T_0) <=> (model I2 C)))) <=> (status T_0 C (eqv)))) (status T_0 T_1 (eth)) (All C, (((Ex I1, (model I1 T_0)) /\ ((Ex I2, (-. (model I2 T_0))) /\ (All I2, ((model I2 T_0) <=> (model I2 C))))) <=> (status T_0 C (eth)))) (-. (model T_2 T_1)) (model T_2 T_0) ### Equiv 15 17 % 5.71/5.91 19. (All C, ((-. (Ex I1, (model I1 T_0))) <=> (status T_0 C (cax)))) (model T_2 T_0) (-. (model T_2 T_1)) (All C, (((Ex I1, (model I1 T_0)) /\ ((Ex I2, (-. (model I2 T_0))) /\ (All I2, ((model I2 T_0) <=> (model I2 C))))) <=> (status T_0 C (eth)))) (status T_0 T_1 (eth)) (All C, (((Ex I1, (model I1 T_0)) /\ (All I2, ((model I2 T_0) <=> (model I2 C)))) <=> (status T_0 C (eqv)))) ### All 18 % 5.71/5.91 20. (All Ax, (All C, ((-. (Ex I1, (model I1 Ax))) <=> (status Ax C (cax))))) (All C, (((Ex I1, (model I1 T_0)) /\ (All I2, ((model I2 T_0) <=> (model I2 C)))) <=> (status T_0 C (eqv)))) (status T_0 T_1 (eth)) (All C, (((Ex I1, (model I1 T_0)) /\ ((Ex I2, (-. (model I2 T_0))) /\ (All I2, ((model I2 T_0) <=> (model I2 C))))) <=> (status T_0 C (eth)))) (-. (model T_2 T_1)) (model T_2 T_0) ### All 19 % 5.71/5.91 21. (All Ax, (All C, (((Ex I1, (model I1 Ax)) /\ ((Ex I2, (-. (model I2 Ax))) /\ (All I2, ((model I2 Ax) <=> (model I2 C))))) <=> (status Ax C (eth))))) (model T_2 T_0) (-. (model T_2 T_1)) (status T_0 T_1 (eth)) (All C, (((Ex I1, (model I1 T_0)) /\ (All I2, ((model I2 T_0) <=> (model I2 C)))) <=> (status T_0 C (eqv)))) (All Ax, (All C, ((-. (Ex I1, (model I1 Ax))) <=> (status Ax C (cax))))) ### All 20 % 5.71/5.91 22. (All Ax, (All C, (((Ex I1, (model I1 Ax)) /\ (All I2, ((model I2 Ax) <=> (model I2 C)))) <=> (status Ax C (eqv))))) (All Ax, (All C, ((-. (Ex I1, (model I1 Ax))) <=> (status Ax C (cax))))) (status T_0 T_1 (eth)) (-. (model T_2 T_1)) (model T_2 T_0) (All Ax, (All C, (((Ex I1, (model I1 Ax)) /\ ((Ex I2, (-. (model I2 Ax))) /\ (All I2, ((model I2 Ax) <=> (model I2 C))))) <=> (status Ax C (eth))))) ### All 21 % 5.71/5.91 23. (-. ((model T_2 T_0) => (model T_2 T_1))) (All Ax, (All C, (((Ex I1, (model I1 Ax)) /\ ((Ex I2, (-. (model I2 Ax))) /\ (All I2, ((model I2 Ax) <=> (model I2 C))))) <=> (status Ax C (eth))))) (status T_0 T_1 (eth)) (All Ax, (All C, ((-. (Ex I1, (model I1 Ax))) <=> (status Ax C (cax))))) (All Ax, (All C, (((Ex I1, (model I1 Ax)) /\ (All I2, ((model I2 Ax) <=> (model I2 C)))) <=> (status Ax C (eqv))))) ### NotImply 22 % 5.71/5.91 24. (-. (All I1, ((model I1 T_0) => (model I1 T_1)))) (All Ax, (All C, (((Ex I1, (model I1 Ax)) /\ (All I2, ((model I2 Ax) <=> (model I2 C)))) <=> (status Ax C (eqv))))) (All Ax, (All C, ((-. (Ex I1, (model I1 Ax))) <=> (status Ax C (cax))))) (status T_0 T_1 (eth)) (All Ax, (All C, (((Ex I1, (model I1 Ax)) /\ ((Ex I2, (-. (model I2 Ax))) /\ (All I2, ((model I2 Ax) <=> (model I2 C))))) <=> (status Ax C (eth))))) ### NotAllEx 23 % 5.71/5.91 25. (-. (status T_0 T_1 (thm))) (status T_0 T_1 (thm)) ### Axiom % 5.71/5.91 26. ((All I1, ((model I1 T_0) => (model I1 T_1))) <=> (status T_0 T_1 (thm))) (-. (status T_0 T_1 (thm))) (All Ax, (All C, (((Ex I1, (model I1 Ax)) /\ ((Ex I2, (-. (model I2 Ax))) /\ (All I2, ((model I2 Ax) <=> (model I2 C))))) <=> (status Ax C (eth))))) (status T_0 T_1 (eth)) (All Ax, (All C, ((-. (Ex I1, (model I1 Ax))) <=> (status Ax C (cax))))) (All Ax, (All C, (((Ex I1, (model I1 Ax)) /\ (All I2, ((model I2 Ax) <=> (model I2 C)))) <=> (status Ax C (eqv))))) ### Equiv 24 25 % 5.71/5.91 27. (All C, ((All I1, ((model I1 T_0) => (model I1 C))) <=> (status T_0 C (thm)))) (All Ax, (All C, (((Ex I1, (model I1 Ax)) /\ (All I2, ((model I2 Ax) <=> (model I2 C)))) <=> (status Ax C (eqv))))) (All Ax, (All C, ((-. (Ex I1, (model I1 Ax))) <=> (status Ax C (cax))))) (status T_0 T_1 (eth)) (All Ax, (All C, (((Ex I1, (model I1 Ax)) /\ ((Ex I2, (-. (model I2 Ax))) /\ (All I2, ((model I2 Ax) <=> (model I2 C))))) <=> (status Ax C (eth))))) (-. (status T_0 T_1 (thm))) ### All 26 % 5.71/5.91 28. (All Ax, (All C, ((All I1, ((model I1 Ax) => (model I1 C))) <=> (status Ax C (thm))))) (-. (status T_0 T_1 (thm))) (All Ax, (All C, (((Ex I1, (model I1 Ax)) /\ ((Ex I2, (-. (model I2 Ax))) /\ (All I2, ((model I2 Ax) <=> (model I2 C))))) <=> (status Ax C (eth))))) (status T_0 T_1 (eth)) (All Ax, (All C, ((-. (Ex I1, (model I1 Ax))) <=> (status Ax C (cax))))) (All Ax, (All C, (((Ex I1, (model I1 Ax)) /\ (All I2, ((model I2 Ax) <=> (model I2 C)))) <=> (status Ax C (eqv))))) ### All 27 % 5.71/5.91 29. (-. ((status T_0 T_1 (eth)) => (status T_0 T_1 (thm)))) (All Ax, (All C, (((Ex I1, (model I1 Ax)) /\ (All I2, ((model I2 Ax) <=> (model I2 C)))) <=> (status Ax C (eqv))))) (All Ax, (All C, ((-. (Ex I1, (model I1 Ax))) <=> (status Ax C (cax))))) (All Ax, (All C, (((Ex I1, (model I1 Ax)) /\ ((Ex I2, (-. (model I2 Ax))) /\ (All I2, ((model I2 Ax) <=> (model I2 C))))) <=> (status Ax C (eth))))) (All Ax, (All C, ((All I1, ((model I1 Ax) => (model I1 C))) <=> (status Ax C (thm))))) ### NotImply 28 % 5.71/5.91 30. (-. (All C, ((status T_0 C (eth)) => (status T_0 C (thm))))) (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 Ax))) /\ (All I2, ((model I2 Ax) <=> (model I2 C))))) <=> (status Ax C (eth))))) (All Ax, (All C, ((-. (Ex I1, (model I1 Ax))) <=> (status Ax C (cax))))) (All Ax, (All C, (((Ex I1, (model I1 Ax)) /\ (All I2, ((model I2 Ax) <=> (model I2 C)))) <=> (status Ax C (eqv))))) ### NotAllEx 29 % 5.71/5.91 31. (-. (All Ax, (All C, ((status Ax C (eth)) => (status Ax C (thm)))))) (All Ax, (All C, (((Ex I1, (model I1 Ax)) /\ (All I2, ((model I2 Ax) <=> (model I2 C)))) <=> (status Ax C (eqv))))) (All Ax, (All C, ((-. (Ex I1, (model I1 Ax))) <=> (status Ax C (cax))))) (All Ax, (All C, (((Ex I1, (model I1 Ax)) /\ ((Ex I2, (-. (model I2 Ax))) /\ (All I2, ((model I2 Ax) <=> (model I2 C))))) <=> (status Ax C (eth))))) (All Ax, (All C, ((All I1, ((model I1 Ax) => (model I1 C))) <=> (status Ax C (thm))))) ### NotAllEx 30 % 5.71/5.91 32. (-. (isa (eth) (thm))) (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 Ax))) /\ (All I2, ((model I2 Ax) <=> (model I2 C))))) <=> (status Ax C (eth))))) (All Ax, (All C, ((-. (Ex I1, (model I1 Ax))) <=> (status Ax C (cax))))) (All Ax, (All C, (((Ex I1, (model I1 Ax)) /\ (All I2, ((model I2 Ax) <=> (model I2 C)))) <=> (status Ax C (eqv))))) ### Definition-Pseudo(isa) 31 % 5.71/5.91 % SZS output end Proof % 5.71/5.91 (* END-PROOF *) %------------------------------------------------------------------------------