%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SEU319+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 : n004.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:13 EDT 2022 % Result : Theorem 0.19s 0.45s % Output : Proof 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SEU319+1 : TPTP v8.1.0. Released v3.3.0. % 0.03/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.13/0.34 % Computer : n004.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 : Mon Jun 20 10:43:38 EDT 2022 % 0.13/0.34 % CPUTime : % 0.19/0.45 % SZS status Theorem % 0.19/0.45 (* PROOF-FOUND *) % 0.19/0.45 (* BEGIN-PROOF *) % 0.19/0.45 % SZS output start Proof % 0.19/0.45 1. (top_str T_0) (-. (top_str T_0)) ### Axiom % 0.19/0.45 2. (subset T_1 (the_carrier T_0)) (-. (subset T_1 (the_carrier T_0))) ### Axiom % 0.19/0.45 3. (-. (element T_1 (powerset (the_carrier T_0)))) (subset T_1 (the_carrier T_0)) ### Extension/test/not_t3_subset 2 % 0.19/0.45 4. ((subset_complement (the_carrier T_0) T_1) != (subset_difference (the_carrier T_0) (cast_as_carrier_subset T_0) T_1)) ((subset_complement (the_carrier T_0) T_1) = (subset_difference (the_carrier T_0) (cast_as_carrier_subset T_0) T_1)) ### Axiom % 0.19/0.45 5. (one_sorted_str T_0) ((subset_complement (the_carrier T_0) T_1) != (subset_difference (the_carrier T_0) (cast_as_carrier_subset T_0) T_1)) (subset T_1 (the_carrier T_0)) ### Extension/test/t17_pre_topc_inst 3 4 % 0.19/0.45 6. (T_0 != T_0) ### Refl(=) % 0.19/0.45 7. (-. (open_subset (subset_difference (the_carrier T_0) (cast_as_carrier_subset T_0) T_1) T_0)) (open_subset (subset_complement (the_carrier T_0) T_1) T_0) (subset T_1 (the_carrier T_0)) (one_sorted_str T_0) ### P-NotP 5 6 % 0.19/0.45 8. (-. (closed_subset T_1 T_0)) (closed_subset T_1 T_0) ### Axiom % 0.19/0.45 9. ((closed_subset T_1 T_0) <=> (open_subset (subset_difference (the_carrier T_0) (cast_as_carrier_subset T_0) T_1) T_0)) (-. (closed_subset T_1 T_0)) (one_sorted_str T_0) (subset T_1 (the_carrier T_0)) (open_subset (subset_complement (the_carrier T_0) T_1) T_0) ### Equiv 7 8 % 0.19/0.45 10. ((element T_1 (powerset (the_carrier T_0))) => ((closed_subset T_1 T_0) <=> (open_subset (subset_difference (the_carrier T_0) (cast_as_carrier_subset T_0) T_1) T_0))) (open_subset (subset_complement (the_carrier T_0) T_1) T_0) (one_sorted_str T_0) (-. (closed_subset T_1 T_0)) (subset T_1 (the_carrier T_0)) ### Imply 3 9 % 0.19/0.45 11. (All B, ((element B (powerset (the_carrier T_0))) => ((closed_subset B T_0) <=> (open_subset (subset_difference (the_carrier T_0) (cast_as_carrier_subset T_0) B) T_0)))) (subset T_1 (the_carrier T_0)) (-. (closed_subset T_1 T_0)) (one_sorted_str T_0) (open_subset (subset_complement (the_carrier T_0) T_1) T_0) ### All 10 % 0.19/0.45 12. ((top_str T_0) => (All B, ((element B (powerset (the_carrier T_0))) => ((closed_subset B T_0) <=> (open_subset (subset_difference (the_carrier T_0) (cast_as_carrier_subset T_0) B) T_0))))) (open_subset (subset_complement (the_carrier T_0) T_1) T_0) (one_sorted_str T_0) (-. (closed_subset T_1 T_0)) (subset T_1 (the_carrier T_0)) (top_str T_0) ### Imply 1 11 % 0.19/0.45 13. (All A, ((top_str A) => (All B, ((element B (powerset (the_carrier A))) => ((closed_subset B A) <=> (open_subset (subset_difference (the_carrier A) (cast_as_carrier_subset A) B) A)))))) (top_str T_0) (subset T_1 (the_carrier T_0)) (-. (closed_subset T_1 T_0)) (one_sorted_str T_0) (open_subset (subset_complement (the_carrier T_0) T_1) T_0) ### All 12 % 0.19/0.45 14. (top_str T_0) (-. (top_str T_0)) ### Axiom % 0.19/0.45 15. (closed_subset T_1 T_0) (-. (closed_subset T_1 T_0)) ### Axiom % 0.19/0.45 16. ((subset_difference (the_carrier T_0) (cast_as_carrier_subset T_0) T_1) != (subset_complement (the_carrier T_0) T_1)) ((subset_complement (the_carrier T_0) T_1) = (subset_difference (the_carrier T_0) (cast_as_carrier_subset T_0) T_1)) ### Sym(=) % 0.19/0.45 17. (one_sorted_str T_0) ((subset_difference (the_carrier T_0) (cast_as_carrier_subset T_0) T_1) != (subset_complement (the_carrier T_0) T_1)) (subset T_1 (the_carrier T_0)) ### Extension/test/t17_pre_topc_inst 3 16 % 0.19/0.45 18. (T_0 != T_0) ### Refl(=) % 0.19/0.45 19. (-. (open_subset (subset_complement (the_carrier T_0) T_1) T_0)) (open_subset (subset_difference (the_carrier T_0) (cast_as_carrier_subset T_0) T_1) T_0) (subset T_1 (the_carrier T_0)) (one_sorted_str T_0) ### P-NotP 17 18 % 0.19/0.45 20. ((closed_subset T_1 T_0) <=> (open_subset (subset_difference (the_carrier T_0) (cast_as_carrier_subset T_0) T_1) T_0)) (one_sorted_str T_0) (subset T_1 (the_carrier T_0)) (-. (open_subset (subset_complement (the_carrier T_0) T_1) T_0)) (closed_subset T_1 T_0) ### Equiv 15 19 % 0.19/0.45 21. ((element T_1 (powerset (the_carrier T_0))) => ((closed_subset T_1 T_0) <=> (open_subset (subset_difference (the_carrier T_0) (cast_as_carrier_subset T_0) T_1) T_0))) (closed_subset T_1 T_0) (-. (open_subset (subset_complement (the_carrier T_0) T_1) T_0)) (one_sorted_str T_0) (subset T_1 (the_carrier T_0)) ### Imply 3 20 % 0.19/0.46 22. (All B, ((element B (powerset (the_carrier T_0))) => ((closed_subset B T_0) <=> (open_subset (subset_difference (the_carrier T_0) (cast_as_carrier_subset T_0) B) T_0)))) (subset T_1 (the_carrier T_0)) (one_sorted_str T_0) (-. (open_subset (subset_complement (the_carrier T_0) T_1) T_0)) (closed_subset T_1 T_0) ### All 21 % 0.19/0.46 23. ((top_str T_0) => (All B, ((element B (powerset (the_carrier T_0))) => ((closed_subset B T_0) <=> (open_subset (subset_difference (the_carrier T_0) (cast_as_carrier_subset T_0) B) T_0))))) (closed_subset T_1 T_0) (-. (open_subset (subset_complement (the_carrier T_0) T_1) T_0)) (one_sorted_str T_0) (subset T_1 (the_carrier T_0)) (top_str T_0) ### Imply 14 22 % 0.19/0.46 24. (All A, ((top_str A) => (All B, ((element B (powerset (the_carrier A))) => ((closed_subset B A) <=> (open_subset (subset_difference (the_carrier A) (cast_as_carrier_subset A) B) A)))))) (top_str T_0) (subset T_1 (the_carrier T_0)) (one_sorted_str T_0) (-. (open_subset (subset_complement (the_carrier T_0) T_1) T_0)) (closed_subset T_1 T_0) ### All 23 % 0.19/0.46 25. (-. ((closed_subset T_1 T_0) <=> (open_subset (subset_complement (the_carrier T_0) T_1) T_0))) (one_sorted_str T_0) (subset T_1 (the_carrier T_0)) (top_str T_0) (All A, ((top_str A) => (All B, ((element B (powerset (the_carrier A))) => ((closed_subset B A) <=> (open_subset (subset_difference (the_carrier A) (cast_as_carrier_subset A) B) A)))))) ### NotEquiv 13 24 % 0.19/0.46 26. (element T_1 (powerset (the_carrier T_0))) (All A, ((top_str A) => (All B, ((element B (powerset (the_carrier A))) => ((closed_subset B A) <=> (open_subset (subset_difference (the_carrier A) (cast_as_carrier_subset A) B) A)))))) (top_str T_0) (one_sorted_str T_0) (-. ((closed_subset T_1 T_0) <=> (open_subset (subset_complement (the_carrier T_0) T_1) T_0))) ### Extension/test/t3_subset 25 % 0.19/0.46 27. (-. ((element T_1 (powerset (the_carrier T_0))) => ((closed_subset T_1 T_0) <=> (open_subset (subset_complement (the_carrier T_0) T_1) T_0)))) (one_sorted_str T_0) (top_str T_0) (All A, ((top_str A) => (All B, ((element B (powerset (the_carrier A))) => ((closed_subset B A) <=> (open_subset (subset_difference (the_carrier A) (cast_as_carrier_subset A) B) A)))))) ### NotImply 26 % 0.19/0.46 28. (-. (All B, ((element B (powerset (the_carrier T_0))) => ((closed_subset B T_0) <=> (open_subset (subset_complement (the_carrier T_0) B) T_0))))) (All A, ((top_str A) => (All B, ((element B (powerset (the_carrier A))) => ((closed_subset B A) <=> (open_subset (subset_difference (the_carrier A) (cast_as_carrier_subset A) B) A)))))) (top_str T_0) (one_sorted_str T_0) ### NotAllEx 27 % 0.19/0.46 29. (top_str T_0) (All A, ((top_str A) => (All B, ((element B (powerset (the_carrier A))) => ((closed_subset B A) <=> (open_subset (subset_difference (the_carrier A) (cast_as_carrier_subset A) B) A)))))) (-. (All B, ((element B (powerset (the_carrier T_0))) => ((closed_subset B T_0) <=> (open_subset (subset_complement (the_carrier T_0) B) T_0))))) ### Extension/test/dt_l1_pre_topc 28 % 0.19/0.46 30. (-. ((top_str T_0) => (All B, ((element B (powerset (the_carrier T_0))) => ((closed_subset B T_0) <=> (open_subset (subset_complement (the_carrier T_0) B) T_0)))))) (All A, ((top_str A) => (All B, ((element B (powerset (the_carrier A))) => ((closed_subset B A) <=> (open_subset (subset_difference (the_carrier A) (cast_as_carrier_subset A) B) A)))))) ### NotImply 29 % 0.19/0.46 31. (-. (All A, ((top_str A) => (All B, ((element B (powerset (the_carrier A))) => ((closed_subset B A) <=> (open_subset (subset_complement (the_carrier A) B) A))))))) (All A, ((top_str A) => (All B, ((element B (powerset (the_carrier A))) => ((closed_subset B A) <=> (open_subset (subset_difference (the_carrier A) (cast_as_carrier_subset A) B) A)))))) ### NotAllEx 30 % 0.19/0.46 % SZS output end Proof % 0.19/0.46 (* END-PROOF *) %------------------------------------------------------------------------------