%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SEU394+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 : n015.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:49 EDT 2022 % Result : Theorem 240.68s 240.88s % Output : Proof 240.68s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SEU394+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.13/0.34 % Computer : n015.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 : Sun Jun 19 18:54:45 EDT 2022 % 0.13/0.34 % CPUTime : % 240.68/240.88 % SZS status Theorem % 240.68/240.88 (* PROOF-FOUND *) % 240.68/240.88 (* BEGIN-PROOF *) % 240.68/240.88 % SZS output start Proof % 240.68/240.88 1. (-. (empty_carrier T_0)) (empty_carrier T_0) ### Axiom % 240.68/240.88 2. (one_sorted_str T_0) (-. (one_sorted_str T_0)) ### Axiom % 240.68/240.88 3. (-. (empty T_1)) (empty T_1) ### Axiom % 240.68/240.88 4. (filtered_subset T_1 (boole_POSet (cast_as_carrier_subset T_0))) (-. (filtered_subset T_1 (boole_POSet (cast_as_carrier_subset T_0)))) ### Axiom % 240.68/240.88 5. (upper_relstr_subset T_1 (boole_POSet (cast_as_carrier_subset T_0))) (-. (upper_relstr_subset T_1 (boole_POSet (cast_as_carrier_subset T_0)))) ### Axiom % 240.68/240.88 6. (element T_1 (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))) (-. (element T_1 (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0)))))) ### Axiom % 240.68/240.88 7. (-. (empty_carrier T_0)) (empty_carrier T_0) ### Axiom % 240.68/240.88 8. (one_sorted_str T_0) (-. (one_sorted_str T_0)) ### Axiom % 240.68/240.88 9. (empty (cast_as_carrier_subset T_0)) (-. (empty (cast_as_carrier_subset T_0))) ### Axiom % 240.68/240.88 10. (((-. (empty_carrier T_0)) /\ (one_sorted_str T_0)) => (-. (empty (cast_as_carrier_subset T_0)))) (empty (cast_as_carrier_subset T_0)) (one_sorted_str T_0) (-. (empty_carrier T_0)) ### DisjTree 7 8 9 % 240.68/240.88 11. (All A, (((-. (empty_carrier A)) /\ (one_sorted_str A)) => (-. (empty (cast_as_carrier_subset A))))) (-. (empty_carrier T_0)) (one_sorted_str T_0) (empty (cast_as_carrier_subset T_0)) ### All 10 % 240.68/240.88 12. (-. (-. (empty (cast_as_carrier_subset T_0)))) (one_sorted_str T_0) (-. (empty_carrier T_0)) (All A, (((-. (empty_carrier A)) /\ (one_sorted_str A)) => (-. (empty (cast_as_carrier_subset A))))) ### NotNot 11 % 240.68/240.88 13. (-. (empty T_1)) (empty T_1) ### Axiom % 240.68/240.88 14. (filtered_subset T_1 (boole_POSet (cast_as_carrier_subset T_0))) (-. (filtered_subset T_1 (boole_POSet (cast_as_carrier_subset T_0)))) ### Axiom % 240.68/240.88 15. (upper_relstr_subset T_1 (boole_POSet (cast_as_carrier_subset T_0))) (-. (upper_relstr_subset T_1 (boole_POSet (cast_as_carrier_subset T_0)))) ### Axiom % 240.68/240.88 16. (proper_element T_1 (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))) (-. (proper_element T_1 (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0)))))) ### Axiom % 240.68/240.88 17. (element T_1 (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))) (-. (element T_1 (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0)))))) ### Axiom % 240.68/240.88 18. (in (empty_set) T_1) (-. (in (empty_set) T_1)) ### Axiom % 240.68/240.88 19. (empty (empty_set)) (-. (empty (empty_set))) ### Axiom % 240.68/240.88 20. (-. ((in (empty_set) T_1) /\ (empty (empty_set)))) (empty (empty_set)) (in (empty_set) T_1) ### NotAnd 18 19 % 240.68/240.88 21. (All C, (-. ((in C T_1) /\ (empty C)))) (in (empty_set) T_1) (empty (empty_set)) ### All 20 % 240.68/240.88 22. (((-. (empty T_1)) /\ ((filtered_subset T_1 (boole_POSet (cast_as_carrier_subset T_0))) /\ ((upper_relstr_subset T_1 (boole_POSet (cast_as_carrier_subset T_0))) /\ ((proper_element T_1 (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))) /\ (element T_1 (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))))))) => (All C, (-. ((in C T_1) /\ (empty C))))) (empty (empty_set)) (in (empty_set) T_1) (element T_1 (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))) (proper_element T_1 (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))) (upper_relstr_subset T_1 (boole_POSet (cast_as_carrier_subset T_0))) (filtered_subset T_1 (boole_POSet (cast_as_carrier_subset T_0))) (-. (empty T_1)) ### DisjTree 13 14 15 16 17 21 % 240.68/240.88 23. (All B, (((-. (empty B)) /\ ((filtered_subset B (boole_POSet (cast_as_carrier_subset T_0))) /\ ((upper_relstr_subset B (boole_POSet (cast_as_carrier_subset T_0))) /\ ((proper_element B (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))) /\ (element B (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))))))) => (All C, (-. ((in C B) /\ (empty C)))))) (-. (empty T_1)) (filtered_subset T_1 (boole_POSet (cast_as_carrier_subset T_0))) (upper_relstr_subset T_1 (boole_POSet (cast_as_carrier_subset T_0))) (proper_element T_1 (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))) (element T_1 (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))) (in (empty_set) T_1) (empty (empty_set)) ### All 22 % 240.68/240.88 24. ((-. (empty (cast_as_carrier_subset T_0))) => (All B, (((-. (empty B)) /\ ((filtered_subset B (boole_POSet (cast_as_carrier_subset T_0))) /\ ((upper_relstr_subset B (boole_POSet (cast_as_carrier_subset T_0))) /\ ((proper_element B (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))) /\ (element B (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))))))) => (All C, (-. ((in C B) /\ (empty C))))))) (empty (empty_set)) (in (empty_set) T_1) (element T_1 (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))) (proper_element T_1 (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))) (upper_relstr_subset T_1 (boole_POSet (cast_as_carrier_subset T_0))) (filtered_subset T_1 (boole_POSet (cast_as_carrier_subset T_0))) (-. (empty T_1)) (All A, (((-. (empty_carrier A)) /\ (one_sorted_str A)) => (-. (empty (cast_as_carrier_subset A))))) (-. (empty_carrier T_0)) (one_sorted_str T_0) ### Imply 12 23 % 240.68/240.88 25. (All A, ((-. (empty A)) => (All B, (((-. (empty B)) /\ ((filtered_subset B (boole_POSet A)) /\ ((upper_relstr_subset B (boole_POSet A)) /\ ((proper_element B (powerset (the_carrier (boole_POSet A)))) /\ (element B (powerset (the_carrier (boole_POSet A)))))))) => (All C, (-. ((in C B) /\ (empty C)))))))) (one_sorted_str T_0) (-. (empty_carrier T_0)) (All A, (((-. (empty_carrier A)) /\ (one_sorted_str A)) => (-. (empty (cast_as_carrier_subset A))))) (-. (empty T_1)) (filtered_subset T_1 (boole_POSet (cast_as_carrier_subset T_0))) (upper_relstr_subset T_1 (boole_POSet (cast_as_carrier_subset T_0))) (proper_element T_1 (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))) (element T_1 (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))) (in (empty_set) T_1) (empty (empty_set)) ### All 24 % 240.68/240.88 26. (-. (-. (in (empty_set) T_1))) (empty (empty_set)) (element T_1 (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))) (proper_element T_1 (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))) (upper_relstr_subset T_1 (boole_POSet (cast_as_carrier_subset T_0))) (filtered_subset T_1 (boole_POSet (cast_as_carrier_subset T_0))) (-. (empty T_1)) (All A, (((-. (empty_carrier A)) /\ (one_sorted_str A)) => (-. (empty (cast_as_carrier_subset A))))) (-. (empty_carrier T_0)) (one_sorted_str T_0) (All A, ((-. (empty A)) => (All B, (((-. (empty B)) /\ ((filtered_subset B (boole_POSet A)) /\ ((upper_relstr_subset B (boole_POSet A)) /\ ((proper_element B (powerset (the_carrier (boole_POSet A)))) /\ (element B (powerset (the_carrier (boole_POSet A)))))))) => (All C, (-. ((in C B) /\ (empty C)))))))) ### NotNot 25 % 240.68/240.88 27. (T_1 != (set_difference T_1 (singleton (empty_set)))) ((set_difference T_1 (singleton (empty_set))) = T_1) ### Sym(=) % 240.68/240.88 28. (((set_difference T_1 (singleton (empty_set))) = T_1) <=> (-. (in (empty_set) T_1))) (T_1 != (set_difference T_1 (singleton (empty_set)))) (All A, ((-. (empty A)) => (All B, (((-. (empty B)) /\ ((filtered_subset B (boole_POSet A)) /\ ((upper_relstr_subset B (boole_POSet A)) /\ ((proper_element B (powerset (the_carrier (boole_POSet A)))) /\ (element B (powerset (the_carrier (boole_POSet A)))))))) => (All C, (-. ((in C B) /\ (empty C)))))))) (one_sorted_str T_0) (-. (empty_carrier T_0)) (All A, (((-. (empty_carrier A)) /\ (one_sorted_str A)) => (-. (empty (cast_as_carrier_subset A))))) (-. (empty T_1)) (filtered_subset T_1 (boole_POSet (cast_as_carrier_subset T_0))) (upper_relstr_subset T_1 (boole_POSet (cast_as_carrier_subset T_0))) (proper_element T_1 (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))) (element T_1 (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))) (empty (empty_set)) ### Equiv 26 27 % 240.68/240.88 29. (All B, (((set_difference T_1 (singleton B)) = T_1) <=> (-. (in B T_1)))) (empty (empty_set)) (element T_1 (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))) (proper_element T_1 (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))) (upper_relstr_subset T_1 (boole_POSet (cast_as_carrier_subset T_0))) (filtered_subset T_1 (boole_POSet (cast_as_carrier_subset T_0))) (-. (empty T_1)) (All A, (((-. (empty_carrier A)) /\ (one_sorted_str A)) => (-. (empty (cast_as_carrier_subset A))))) (-. (empty_carrier T_0)) (one_sorted_str T_0) (All A, ((-. (empty A)) => (All B, (((-. (empty B)) /\ ((filtered_subset B (boole_POSet A)) /\ ((upper_relstr_subset B (boole_POSet A)) /\ ((proper_element B (powerset (the_carrier (boole_POSet A)))) /\ (element B (powerset (the_carrier (boole_POSet A)))))))) => (All C, (-. ((in C B) /\ (empty C)))))))) (T_1 != (set_difference T_1 (singleton (empty_set)))) ### All 28 % 240.68/240.89 30. (All A, (All B, (((set_difference A (singleton B)) = A) <=> (-. (in B A))))) (T_1 != (set_difference T_1 (singleton (empty_set)))) (All A, ((-. (empty A)) => (All B, (((-. (empty B)) /\ ((filtered_subset B (boole_POSet A)) /\ ((upper_relstr_subset B (boole_POSet A)) /\ ((proper_element B (powerset (the_carrier (boole_POSet A)))) /\ (element B (powerset (the_carrier (boole_POSet A)))))))) => (All C, (-. ((in C B) /\ (empty C)))))))) (one_sorted_str T_0) (-. (empty_carrier T_0)) (All A, (((-. (empty_carrier A)) /\ (one_sorted_str A)) => (-. (empty (cast_as_carrier_subset A))))) (-. (empty T_1)) (filtered_subset T_1 (boole_POSet (cast_as_carrier_subset T_0))) (upper_relstr_subset T_1 (boole_POSet (cast_as_carrier_subset T_0))) (proper_element T_1 (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))) (element T_1 (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))) (empty (empty_set)) ### All 29 % 240.68/240.89 31. ((filter_of_net_str T_0 (net_of_bool_filter T_0 (cast_as_carrier_subset T_0) T_1)) != (filter_of_net_str T_0 (net_of_bool_filter T_0 (cast_as_carrier_subset T_0) T_1))) ### Refl(=) % 240.68/240.89 32. ((filter_of_net_str T_0 (net_of_bool_filter T_0 (cast_as_carrier_subset T_0) T_1)) != (filter_of_net_str T_0 (net_of_bool_filter T_0 (cast_as_carrier_subset T_0) T_1))) ### Refl(=) % 240.68/240.89 33. (T_1 != (filter_of_net_str T_0 (net_of_bool_filter T_0 (cast_as_carrier_subset T_0) T_1))) ((set_difference T_1 (singleton (empty_set))) = (filter_of_net_str T_0 (net_of_bool_filter T_0 (cast_as_carrier_subset T_0) T_1))) (empty (empty_set)) (element T_1 (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))) (proper_element T_1 (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))) (upper_relstr_subset T_1 (boole_POSet (cast_as_carrier_subset T_0))) (filtered_subset T_1 (boole_POSet (cast_as_carrier_subset T_0))) (-. (empty T_1)) (All A, (((-. (empty_carrier A)) /\ (one_sorted_str A)) => (-. (empty (cast_as_carrier_subset A))))) (-. (empty_carrier T_0)) (one_sorted_str T_0) (All A, ((-. (empty A)) => (All B, (((-. (empty B)) /\ ((filtered_subset B (boole_POSet A)) /\ ((upper_relstr_subset B (boole_POSet A)) /\ ((proper_element B (powerset (the_carrier (boole_POSet A)))) /\ (element B (powerset (the_carrier (boole_POSet A)))))))) => (All C, (-. ((in C B) /\ (empty C)))))))) (All A, (All B, (((set_difference A (singleton B)) = A) <=> (-. (in B A))))) ### TransEq 30 31 32 % 240.68/240.89 34. (((-. (empty T_1)) /\ ((filtered_subset T_1 (boole_POSet (cast_as_carrier_subset T_0))) /\ ((upper_relstr_subset T_1 (boole_POSet (cast_as_carrier_subset T_0))) /\ (element T_1 (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0)))))))) => ((set_difference T_1 (singleton (empty_set))) = (filter_of_net_str T_0 (net_of_bool_filter T_0 (cast_as_carrier_subset T_0) T_1)))) (All A, (All B, (((set_difference A (singleton B)) = A) <=> (-. (in B A))))) (All A, ((-. (empty A)) => (All B, (((-. (empty B)) /\ ((filtered_subset B (boole_POSet A)) /\ ((upper_relstr_subset B (boole_POSet A)) /\ ((proper_element B (powerset (the_carrier (boole_POSet A)))) /\ (element B (powerset (the_carrier (boole_POSet A)))))))) => (All C, (-. ((in C B) /\ (empty C)))))))) (one_sorted_str T_0) (-. (empty_carrier T_0)) (All A, (((-. (empty_carrier A)) /\ (one_sorted_str A)) => (-. (empty (cast_as_carrier_subset A))))) (proper_element T_1 (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))) (empty (empty_set)) (T_1 != (filter_of_net_str T_0 (net_of_bool_filter T_0 (cast_as_carrier_subset T_0) T_1))) (element T_1 (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))) (upper_relstr_subset T_1 (boole_POSet (cast_as_carrier_subset T_0))) (filtered_subset T_1 (boole_POSet (cast_as_carrier_subset T_0))) (-. (empty T_1)) ### DisjTree 3 4 5 6 33 % 240.68/240.89 35. (All B, (((-. (empty B)) /\ ((filtered_subset B (boole_POSet (cast_as_carrier_subset T_0))) /\ ((upper_relstr_subset B (boole_POSet (cast_as_carrier_subset T_0))) /\ (element B (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0)))))))) => ((set_difference B (singleton (empty_set))) = (filter_of_net_str T_0 (net_of_bool_filter T_0 (cast_as_carrier_subset T_0) B))))) (-. (empty T_1)) (filtered_subset T_1 (boole_POSet (cast_as_carrier_subset T_0))) (upper_relstr_subset T_1 (boole_POSet (cast_as_carrier_subset T_0))) (element T_1 (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))) (T_1 != (filter_of_net_str T_0 (net_of_bool_filter T_0 (cast_as_carrier_subset T_0) T_1))) (empty (empty_set)) (proper_element T_1 (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))) (All A, (((-. (empty_carrier A)) /\ (one_sorted_str A)) => (-. (empty (cast_as_carrier_subset A))))) (-. (empty_carrier T_0)) (one_sorted_str T_0) (All A, ((-. (empty A)) => (All B, (((-. (empty B)) /\ ((filtered_subset B (boole_POSet A)) /\ ((upper_relstr_subset B (boole_POSet A)) /\ ((proper_element B (powerset (the_carrier (boole_POSet A)))) /\ (element B (powerset (the_carrier (boole_POSet A)))))))) => (All C, (-. ((in C B) /\ (empty C)))))))) (All A, (All B, (((set_difference A (singleton B)) = A) <=> (-. (in B A))))) ### All 34 % 240.68/240.89 36. (((-. (empty_carrier T_0)) /\ (one_sorted_str T_0)) => (All B, (((-. (empty B)) /\ ((filtered_subset B (boole_POSet (cast_as_carrier_subset T_0))) /\ ((upper_relstr_subset B (boole_POSet (cast_as_carrier_subset T_0))) /\ (element B (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0)))))))) => ((set_difference B (singleton (empty_set))) = (filter_of_net_str T_0 (net_of_bool_filter T_0 (cast_as_carrier_subset T_0) B)))))) (All A, (All B, (((set_difference A (singleton B)) = A) <=> (-. (in B A))))) (All A, ((-. (empty A)) => (All B, (((-. (empty B)) /\ ((filtered_subset B (boole_POSet A)) /\ ((upper_relstr_subset B (boole_POSet A)) /\ ((proper_element B (powerset (the_carrier (boole_POSet A)))) /\ (element B (powerset (the_carrier (boole_POSet A)))))))) => (All C, (-. ((in C B) /\ (empty C)))))))) (All A, (((-. (empty_carrier A)) /\ (one_sorted_str A)) => (-. (empty (cast_as_carrier_subset A))))) (proper_element T_1 (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))) (empty (empty_set)) (T_1 != (filter_of_net_str T_0 (net_of_bool_filter T_0 (cast_as_carrier_subset T_0) T_1))) (element T_1 (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))) (upper_relstr_subset T_1 (boole_POSet (cast_as_carrier_subset T_0))) (filtered_subset T_1 (boole_POSet (cast_as_carrier_subset T_0))) (-. (empty T_1)) (one_sorted_str T_0) (-. (empty_carrier T_0)) ### DisjTree 1 2 35 % 240.68/240.89 37. (All A, (((-. (empty_carrier A)) /\ (one_sorted_str A)) => (All B, (((-. (empty B)) /\ ((filtered_subset B (boole_POSet (cast_as_carrier_subset A))) /\ ((upper_relstr_subset B (boole_POSet (cast_as_carrier_subset A))) /\ (element B (powerset (the_carrier (boole_POSet (cast_as_carrier_subset A)))))))) => ((set_difference B (singleton (empty_set))) = (filter_of_net_str A (net_of_bool_filter A (cast_as_carrier_subset A) B))))))) (-. (empty_carrier T_0)) (one_sorted_str T_0) (-. (empty T_1)) (filtered_subset T_1 (boole_POSet (cast_as_carrier_subset T_0))) (upper_relstr_subset T_1 (boole_POSet (cast_as_carrier_subset T_0))) (element T_1 (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))) (T_1 != (filter_of_net_str T_0 (net_of_bool_filter T_0 (cast_as_carrier_subset T_0) T_1))) (empty (empty_set)) (proper_element T_1 (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))) (All A, (((-. (empty_carrier A)) /\ (one_sorted_str A)) => (-. (empty (cast_as_carrier_subset A))))) (All A, ((-. (empty A)) => (All B, (((-. (empty B)) /\ ((filtered_subset B (boole_POSet A)) /\ ((upper_relstr_subset B (boole_POSet A)) /\ ((proper_element B (powerset (the_carrier (boole_POSet A)))) /\ (element B (powerset (the_carrier (boole_POSet A)))))))) => (All C, (-. ((in C B) /\ (empty C)))))))) (All A, (All B, (((set_difference A (singleton B)) = A) <=> (-. (in B A))))) ### All 36 % 240.68/240.90 38. ((empty (empty_set)) /\ (relation (empty_set))) (All A, (All B, (((set_difference A (singleton B)) = A) <=> (-. (in B A))))) (All A, ((-. (empty A)) => (All B, (((-. (empty B)) /\ ((filtered_subset B (boole_POSet A)) /\ ((upper_relstr_subset B (boole_POSet A)) /\ ((proper_element B (powerset (the_carrier (boole_POSet A)))) /\ (element B (powerset (the_carrier (boole_POSet A)))))))) => (All C, (-. ((in C B) /\ (empty C)))))))) (All A, (((-. (empty_carrier A)) /\ (one_sorted_str A)) => (-. (empty (cast_as_carrier_subset A))))) (proper_element T_1 (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))) (T_1 != (filter_of_net_str T_0 (net_of_bool_filter T_0 (cast_as_carrier_subset T_0) T_1))) (element T_1 (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))) (upper_relstr_subset T_1 (boole_POSet (cast_as_carrier_subset T_0))) (filtered_subset T_1 (boole_POSet (cast_as_carrier_subset T_0))) (-. (empty T_1)) (one_sorted_str T_0) (-. (empty_carrier T_0)) (All A, (((-. (empty_carrier A)) /\ (one_sorted_str A)) => (All B, (((-. (empty B)) /\ ((filtered_subset B (boole_POSet (cast_as_carrier_subset A))) /\ ((upper_relstr_subset B (boole_POSet (cast_as_carrier_subset A))) /\ (element B (powerset (the_carrier (boole_POSet (cast_as_carrier_subset A)))))))) => ((set_difference B (singleton (empty_set))) = (filter_of_net_str A (net_of_bool_filter A (cast_as_carrier_subset A) B))))))) ### And 37 % 240.68/240.90 39. (-. (((-. (empty T_1)) /\ ((filtered_subset T_1 (boole_POSet (cast_as_carrier_subset T_0))) /\ ((upper_relstr_subset T_1 (boole_POSet (cast_as_carrier_subset T_0))) /\ ((proper_element T_1 (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))) /\ (element T_1 (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))))))) => (T_1 = (filter_of_net_str T_0 (net_of_bool_filter T_0 (cast_as_carrier_subset T_0) T_1))))) (All A, (((-. (empty_carrier A)) /\ (one_sorted_str A)) => (All B, (((-. (empty B)) /\ ((filtered_subset B (boole_POSet (cast_as_carrier_subset A))) /\ ((upper_relstr_subset B (boole_POSet (cast_as_carrier_subset A))) /\ (element B (powerset (the_carrier (boole_POSet (cast_as_carrier_subset A)))))))) => ((set_difference B (singleton (empty_set))) = (filter_of_net_str A (net_of_bool_filter A (cast_as_carrier_subset A) B))))))) (-. (empty_carrier T_0)) (one_sorted_str T_0) (All A, (((-. (empty_carrier A)) /\ (one_sorted_str A)) => (-. (empty (cast_as_carrier_subset A))))) (All A, ((-. (empty A)) => (All B, (((-. (empty B)) /\ ((filtered_subset B (boole_POSet A)) /\ ((upper_relstr_subset B (boole_POSet A)) /\ ((proper_element B (powerset (the_carrier (boole_POSet A)))) /\ (element B (powerset (the_carrier (boole_POSet A)))))))) => (All C, (-. ((in C B) /\ (empty C)))))))) (All A, (All B, (((set_difference A (singleton B)) = A) <=> (-. (in B A))))) ((empty (empty_set)) /\ (relation (empty_set))) ### ConjTree 38 % 240.68/240.90 40. (-. (All B, (((-. (empty B)) /\ ((filtered_subset B (boole_POSet (cast_as_carrier_subset T_0))) /\ ((upper_relstr_subset B (boole_POSet (cast_as_carrier_subset T_0))) /\ ((proper_element B (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))) /\ (element B (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))))))) => (B = (filter_of_net_str T_0 (net_of_bool_filter T_0 (cast_as_carrier_subset T_0) B)))))) ((empty (empty_set)) /\ (relation (empty_set))) (All A, (All B, (((set_difference A (singleton B)) = A) <=> (-. (in B A))))) (All A, ((-. (empty A)) => (All B, (((-. (empty B)) /\ ((filtered_subset B (boole_POSet A)) /\ ((upper_relstr_subset B (boole_POSet A)) /\ ((proper_element B (powerset (the_carrier (boole_POSet A)))) /\ (element B (powerset (the_carrier (boole_POSet A)))))))) => (All C, (-. ((in C B) /\ (empty C)))))))) (All A, (((-. (empty_carrier A)) /\ (one_sorted_str A)) => (-. (empty (cast_as_carrier_subset A))))) (one_sorted_str T_0) (-. (empty_carrier T_0)) (All A, (((-. (empty_carrier A)) /\ (one_sorted_str A)) => (All B, (((-. (empty B)) /\ ((filtered_subset B (boole_POSet (cast_as_carrier_subset A))) /\ ((upper_relstr_subset B (boole_POSet (cast_as_carrier_subset A))) /\ (element B (powerset (the_carrier (boole_POSet (cast_as_carrier_subset A)))))))) => ((set_difference B (singleton (empty_set))) = (filter_of_net_str A (net_of_bool_filter A (cast_as_carrier_subset A) B))))))) ### NotAllEx 39 % 240.68/240.90 41. (-. (((-. (empty_carrier T_0)) /\ (one_sorted_str T_0)) => (All B, (((-. (empty B)) /\ ((filtered_subset B (boole_POSet (cast_as_carrier_subset T_0))) /\ ((upper_relstr_subset B (boole_POSet (cast_as_carrier_subset T_0))) /\ ((proper_element B (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))) /\ (element B (powerset (the_carrier (boole_POSet (cast_as_carrier_subset T_0))))))))) => (B = (filter_of_net_str T_0 (net_of_bool_filter T_0 (cast_as_carrier_subset T_0) B))))))) (All A, (((-. (empty_carrier A)) /\ (one_sorted_str A)) => (All B, (((-. (empty B)) /\ ((filtered_subset B (boole_POSet (cast_as_carrier_subset A))) /\ ((upper_relstr_subset B (boole_POSet (cast_as_carrier_subset A))) /\ (element B (powerset (the_carrier (boole_POSet (cast_as_carrier_subset A)))))))) => ((set_difference B (singleton (empty_set))) = (filter_of_net_str A (net_of_bool_filter A (cast_as_carrier_subset A) B))))))) (All A, (((-. (empty_carrier A)) /\ (one_sorted_str A)) => (-. (empty (cast_as_carrier_subset A))))) (All A, ((-. (empty A)) => (All B, (((-. (empty B)) /\ ((filtered_subset B (boole_POSet A)) /\ ((upper_relstr_subset B (boole_POSet A)) /\ ((proper_element B (powerset (the_carrier (boole_POSet A)))) /\ (element B (powerset (the_carrier (boole_POSet A)))))))) => (All C, (-. ((in C B) /\ (empty C)))))))) (All A, (All B, (((set_difference A (singleton B)) = A) <=> (-. (in B A))))) ((empty (empty_set)) /\ (relation (empty_set))) ### ConjTree 40 % 240.68/240.90 42. (-. (All A, (((-. (empty_carrier A)) /\ (one_sorted_str A)) => (All B, (((-. (empty B)) /\ ((filtered_subset B (boole_POSet (cast_as_carrier_subset A))) /\ ((upper_relstr_subset B (boole_POSet (cast_as_carrier_subset A))) /\ ((proper_element B (powerset (the_carrier (boole_POSet (cast_as_carrier_subset A))))) /\ (element B (powerset (the_carrier (boole_POSet (cast_as_carrier_subset A))))))))) => (B = (filter_of_net_str A (net_of_bool_filter A (cast_as_carrier_subset A) B)))))))) ((empty (empty_set)) /\ (relation (empty_set))) (All A, (All B, (((set_difference A (singleton B)) = A) <=> (-. (in B A))))) (All A, ((-. (empty A)) => (All B, (((-. (empty B)) /\ ((filtered_subset B (boole_POSet A)) /\ ((upper_relstr_subset B (boole_POSet A)) /\ ((proper_element B (powerset (the_carrier (boole_POSet A)))) /\ (element B (powerset (the_carrier (boole_POSet A)))))))) => (All C, (-. ((in C B) /\ (empty C)))))))) (All A, (((-. (empty_carrier A)) /\ (one_sorted_str A)) => (-. (empty (cast_as_carrier_subset A))))) (All A, (((-. (empty_carrier A)) /\ (one_sorted_str A)) => (All B, (((-. (empty B)) /\ ((filtered_subset B (boole_POSet (cast_as_carrier_subset A))) /\ ((upper_relstr_subset B (boole_POSet (cast_as_carrier_subset A))) /\ (element B (powerset (the_carrier (boole_POSet (cast_as_carrier_subset A)))))))) => ((set_difference B (singleton (empty_set))) = (filter_of_net_str A (net_of_bool_filter A (cast_as_carrier_subset A) B))))))) ### NotAllEx 41 % 240.68/240.90 % SZS output end Proof % 240.68/240.90 (* END-PROOF *) %------------------------------------------------------------------------------