%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SEU317+1 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n020.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 : Tue Jul 19 14:50:12 EDT 2022 % Result : Theorem 114.88s 115.18s % Output : Proof 114.88s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SEU317+1 : TPTP v8.1.0. Released v3.3.0. % 0.07/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.14/0.34 % Computer : n020.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 600 % 0.14/0.34 % DateTime : Sat Jun 18 19:14:33 EDT 2022 % 0.14/0.34 % CPUTime : % 114.88/115.18 % SZS status Theorem % 114.88/115.18 (* PROOF-FOUND *) % 114.88/115.18 (* BEGIN-PROOF *) % 114.88/115.18 % SZS output start Proof % 114.88/115.18 1. (top_str T_0) (-. (top_str T_0)) ### Axiom % 114.88/115.18 2. (element T_1 (powerset (the_carrier T_0))) (-. (element T_1 (powerset (the_carrier T_0)))) ### Axiom % 114.88/115.18 3. (element T_1 (powerset (the_carrier T_0))) (-. (element T_1 (powerset (the_carrier T_0)))) ### Axiom % 114.88/115.18 4. (in T_2 T_1) (-. (in T_2 T_1)) ### Axiom % 114.88/115.18 5. (-. (in T_2 (the_carrier T_0))) (in T_2 (the_carrier T_0)) ### Axiom % 114.88/115.18 6. ((in T_2 T_1) => (in T_2 (the_carrier T_0))) (-. (in T_2 (the_carrier T_0))) (in T_2 T_1) ### Imply 4 5 % 114.88/115.18 7. (All C, ((in C T_1) => (in C (the_carrier T_0)))) (in T_2 T_1) (-. (in T_2 (the_carrier T_0))) ### All 6 % 114.88/115.18 8. (subset T_1 (the_carrier T_0)) (-. (in T_2 (the_carrier T_0))) (in T_2 T_1) ### Definition-Pseudo(subset) 7 % 114.88/115.18 9. ((element T_1 (powerset (the_carrier T_0))) <=> (subset T_1 (the_carrier T_0))) (in T_2 T_1) (-. (in T_2 (the_carrier T_0))) (element T_1 (powerset (the_carrier T_0))) ### Equiv 3 8 % 114.88/115.18 10. (All B, ((element T_1 (powerset B)) <=> (subset T_1 B))) (element T_1 (powerset (the_carrier T_0))) (-. (in T_2 (the_carrier T_0))) (in T_2 T_1) ### All 9 % 114.88/115.18 11. (in T_2 T_1) (-. (in T_2 T_1)) ### Axiom % 114.88/115.18 12. (-. (in T_2 T_3)) (in T_2 T_3) ### Axiom % 114.88/115.18 13. ((in T_2 T_1) => (in T_2 T_3)) (-. (in T_2 T_3)) (in T_2 T_1) ### Imply 11 12 % 114.88/115.18 14. (All C, ((in C T_1) => (in C T_3))) (in T_2 T_1) (-. (in T_2 T_3)) ### All 13 % 114.88/115.18 15. (subset T_1 T_3) (-. (in T_2 T_3)) (in T_2 T_1) ### Definition-Pseudo(subset) 14 % 114.88/115.18 16. (-. ((element T_3 (powerset (the_carrier T_0))) => (((closed_subset T_3 T_0) /\ (subset T_1 T_3)) => (in T_2 T_3)))) (in T_2 T_1) ### ConjTree 15 % 114.88/115.18 17. (-. (All D, ((element D (powerset (the_carrier T_0))) => (((closed_subset D T_0) /\ (subset T_1 D)) => (in T_2 D))))) (in T_2 T_1) ### NotAllEx 16 % 114.88/115.18 18. (-. (in T_2 (topstr_closure T_0 T_1))) (in T_2 (topstr_closure T_0 T_1)) ### Axiom % 114.88/115.18 19. ((in T_2 (topstr_closure T_0 T_1)) <=> (All D, ((element D (powerset (the_carrier T_0))) => (((closed_subset D T_0) /\ (subset T_1 D)) => (in T_2 D))))) (-. (in T_2 (topstr_closure T_0 T_1))) (in T_2 T_1) ### Equiv 17 18 % 114.88/115.18 20. ((in T_2 (the_carrier T_0)) => ((in T_2 (topstr_closure T_0 T_1)) <=> (All D, ((element D (powerset (the_carrier T_0))) => (((closed_subset D T_0) /\ (subset T_1 D)) => (in T_2 D)))))) (-. (in T_2 (topstr_closure T_0 T_1))) (in T_2 T_1) (element T_1 (powerset (the_carrier T_0))) (All B, ((element T_1 (powerset B)) <=> (subset T_1 B))) ### Imply 10 19 % 114.88/115.18 21. (All C, ((in C (the_carrier T_0)) => ((in C (topstr_closure T_0 T_1)) <=> (All D, ((element D (powerset (the_carrier T_0))) => (((closed_subset D T_0) /\ (subset T_1 D)) => (in C D))))))) (All B, ((element T_1 (powerset B)) <=> (subset T_1 B))) (element T_1 (powerset (the_carrier T_0))) (in T_2 T_1) (-. (in T_2 (topstr_closure T_0 T_1))) ### All 20 % 114.88/115.18 22. ((element T_1 (powerset (the_carrier T_0))) => (All C, ((in C (the_carrier T_0)) => ((in C (topstr_closure T_0 T_1)) <=> (All D, ((element D (powerset (the_carrier T_0))) => (((closed_subset D T_0) /\ (subset T_1 D)) => (in C D)))))))) (-. (in T_2 (topstr_closure T_0 T_1))) (in T_2 T_1) (All B, ((element T_1 (powerset B)) <=> (subset T_1 B))) (element T_1 (powerset (the_carrier T_0))) ### Imply 2 21 % 114.88/115.18 23. (All B, ((element B (powerset (the_carrier T_0))) => (All C, ((in C (the_carrier T_0)) => ((in C (topstr_closure T_0 B)) <=> (All D, ((element D (powerset (the_carrier T_0))) => (((closed_subset D T_0) /\ (subset B D)) => (in C D))))))))) (element T_1 (powerset (the_carrier T_0))) (All B, ((element T_1 (powerset B)) <=> (subset T_1 B))) (in T_2 T_1) (-. (in T_2 (topstr_closure T_0 T_1))) ### All 22 % 114.88/115.18 24. ((top_str T_0) => (All B, ((element B (powerset (the_carrier T_0))) => (All C, ((in C (the_carrier T_0)) => ((in C (topstr_closure T_0 B)) <=> (All D, ((element D (powerset (the_carrier T_0))) => (((closed_subset D T_0) /\ (subset B D)) => (in C D)))))))))) (-. (in T_2 (topstr_closure T_0 T_1))) (in T_2 T_1) (All B, ((element T_1 (powerset B)) <=> (subset T_1 B))) (element T_1 (powerset (the_carrier T_0))) (top_str T_0) ### Imply 1 23 % 114.88/115.18 25. (All A, ((top_str A) => (All B, ((element B (powerset (the_carrier A))) => (All C, ((in C (the_carrier A)) => ((in C (topstr_closure A B)) <=> (All D, ((element D (powerset (the_carrier A))) => (((closed_subset D A) /\ (subset B D)) => (in C D))))))))))) (top_str T_0) (element T_1 (powerset (the_carrier T_0))) (All B, ((element T_1 (powerset B)) <=> (subset T_1 B))) (in T_2 T_1) (-. (in T_2 (topstr_closure T_0 T_1))) ### All 24 % 114.88/115.18 26. (All A, (All B, ((element A (powerset B)) <=> (subset A B)))) (-. (in T_2 (topstr_closure T_0 T_1))) (in T_2 T_1) (element T_1 (powerset (the_carrier T_0))) (top_str T_0) (All A, ((top_str A) => (All B, ((element B (powerset (the_carrier A))) => (All C, ((in C (the_carrier A)) => ((in C (topstr_closure A B)) <=> (All D, ((element D (powerset (the_carrier A))) => (((closed_subset D A) /\ (subset B D)) => (in C D))))))))))) ### All 25 % 114.88/115.18 27. (-. ((in T_2 T_1) => (in T_2 (topstr_closure T_0 T_1)))) (All A, ((top_str A) => (All B, ((element B (powerset (the_carrier A))) => (All C, ((in C (the_carrier A)) => ((in C (topstr_closure A B)) <=> (All D, ((element D (powerset (the_carrier A))) => (((closed_subset D A) /\ (subset B D)) => (in C D))))))))))) (top_str T_0) (element T_1 (powerset (the_carrier T_0))) (All A, (All B, ((element A (powerset B)) <=> (subset A B)))) ### NotImply 26 % 114.88/115.18 28. (-. (All C, ((in C T_1) => (in C (topstr_closure T_0 T_1))))) (All A, (All B, ((element A (powerset B)) <=> (subset A B)))) (element T_1 (powerset (the_carrier T_0))) (top_str T_0) (All A, ((top_str A) => (All B, ((element B (powerset (the_carrier A))) => (All C, ((in C (the_carrier A)) => ((in C (topstr_closure A B)) <=> (All D, ((element D (powerset (the_carrier A))) => (((closed_subset D A) /\ (subset B D)) => (in C D))))))))))) ### NotAllEx 27 % 114.88/115.18 29. (-. (subset T_1 (topstr_closure T_0 T_1))) (All A, ((top_str A) => (All B, ((element B (powerset (the_carrier A))) => (All C, ((in C (the_carrier A)) => ((in C (topstr_closure A B)) <=> (All D, ((element D (powerset (the_carrier A))) => (((closed_subset D A) /\ (subset B D)) => (in C D))))))))))) (top_str T_0) (element T_1 (powerset (the_carrier T_0))) (All A, (All B, ((element A (powerset B)) <=> (subset A B)))) ### Definition-Pseudo(subset) 28 % 114.88/115.18 30. (-. ((element T_1 (powerset (the_carrier T_0))) => (subset T_1 (topstr_closure T_0 T_1)))) (All A, (All B, ((element A (powerset B)) <=> (subset A B)))) (top_str T_0) (All A, ((top_str A) => (All B, ((element B (powerset (the_carrier A))) => (All C, ((in C (the_carrier A)) => ((in C (topstr_closure A B)) <=> (All D, ((element D (powerset (the_carrier A))) => (((closed_subset D A) /\ (subset B D)) => (in C D))))))))))) ### NotImply 29 % 114.88/115.18 31. (-. (All B, ((element B (powerset (the_carrier T_0))) => (subset B (topstr_closure T_0 B))))) (All A, ((top_str A) => (All B, ((element B (powerset (the_carrier A))) => (All C, ((in C (the_carrier A)) => ((in C (topstr_closure A B)) <=> (All D, ((element D (powerset (the_carrier A))) => (((closed_subset D A) /\ (subset B D)) => (in C D))))))))))) (top_str T_0) (All A, (All B, ((element A (powerset B)) <=> (subset A B)))) ### NotAllEx 30 % 114.88/115.18 32. (-. ((top_str T_0) => (All B, ((element B (powerset (the_carrier T_0))) => (subset B (topstr_closure T_0 B)))))) (All A, (All B, ((element A (powerset B)) <=> (subset A B)))) (All A, ((top_str A) => (All B, ((element B (powerset (the_carrier A))) => (All C, ((in C (the_carrier A)) => ((in C (topstr_closure A B)) <=> (All D, ((element D (powerset (the_carrier A))) => (((closed_subset D A) /\ (subset B D)) => (in C D))))))))))) ### NotImply 31 % 114.88/115.18 33. (-. (All A, ((top_str A) => (All B, ((element B (powerset (the_carrier A))) => (subset B (topstr_closure A B))))))) (All A, ((top_str A) => (All B, ((element B (powerset (the_carrier A))) => (All C, ((in C (the_carrier A)) => ((in C (topstr_closure A B)) <=> (All D, ((element D (powerset (the_carrier A))) => (((closed_subset D A) /\ (subset B D)) => (in C D))))))))))) (All A, (All B, ((element A (powerset B)) <=> (subset A B)))) ### NotAllEx 32 % 114.88/115.18 % SZS output end Proof % 114.88/115.18 (* END-PROOF *) %------------------------------------------------------------------------------