%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SET662+3 : TPTP v8.1.0. Released v2.2.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n027.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 05:43:13 EDT 2022 % Result : Theorem 2.86s 3.05s % Output : Proof 2.86s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SET662+3 : TPTP v8.1.0. Released v2.2.0. % 0.11/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.14/0.33 % Computer : n027.cluster.edu % 0.14/0.33 % Model : x86_64 x86_64 % 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.33 % Memory : 8042.1875MB % 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.33 % CPULimit : 300 % 0.14/0.33 % WCLimit : 600 % 0.14/0.33 % DateTime : Sun Jul 10 03:53:32 EDT 2022 % 0.14/0.33 % CPUTime : % 2.86/3.05 % SZS status Theorem % 2.86/3.05 (* PROOF-FOUND *) % 2.86/3.05 (* BEGIN-PROOF *) % 2.86/3.05 % SZS output start Proof % 2.86/3.05 1. (ilf_type T_0 (set_type)) (-. (ilf_type T_0 (set_type))) ### Axiom % 2.86/3.05 2. (ilf_type T_1 (set_type)) (-. (ilf_type T_1 (set_type))) ### Axiom % 2.86/3.05 3. (ilf_type T_0 (set_type)) (-. (ilf_type T_0 (set_type))) ### Axiom % 2.86/3.05 4. (ilf_type T_1 (set_type)) (-. (ilf_type T_1 (set_type))) ### Axiom % 2.86/3.05 5. (-. (ilf_type (cross_product T_0 T_1) (set_type))) (ilf_type (cross_product T_0 T_1) (set_type)) ### Axiom % 2.86/3.05 6. ((ilf_type T_1 (set_type)) => (ilf_type (cross_product T_0 T_1) (set_type))) (-. (ilf_type (cross_product T_0 T_1) (set_type))) (ilf_type T_1 (set_type)) ### Imply 4 5 % 2.86/3.05 7. (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product T_0 C) (set_type)))) (ilf_type T_1 (set_type)) (-. (ilf_type (cross_product T_0 T_1) (set_type))) ### All 6 % 2.86/3.05 8. ((ilf_type T_0 (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product T_0 C) (set_type))))) (-. (ilf_type (cross_product T_0 T_1) (set_type))) (ilf_type T_1 (set_type)) (ilf_type T_0 (set_type)) ### Imply 3 7 % 2.86/3.05 9. (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (ilf_type T_0 (set_type)) (ilf_type T_1 (set_type)) (-. (ilf_type (cross_product T_0 T_1) (set_type))) ### All 8 % 2.86/3.05 10. (-. (ilf_type (empty_set) (set_type))) (ilf_type (empty_set) (set_type)) ### Axiom % 2.86/3.05 11. (All B, (ilf_type B (set_type))) (-. (ilf_type (empty_set) (set_type))) ### All 10 % 2.86/3.05 12. (-. (ilf_type (power_set (cross_product T_0 T_1)) (set_type))) (ilf_type (power_set (cross_product T_0 T_1)) (set_type)) ### Axiom % 2.86/3.05 13. ((-. (empty (power_set (cross_product T_0 T_1)))) /\ (ilf_type (power_set (cross_product T_0 T_1)) (set_type))) (-. (ilf_type (power_set (cross_product T_0 T_1)) (set_type))) ### And 12 % 2.86/3.05 14. ((ilf_type (cross_product T_0 T_1) (set_type)) => ((-. (empty (power_set (cross_product T_0 T_1)))) /\ (ilf_type (power_set (cross_product T_0 T_1)) (set_type)))) (-. (ilf_type (power_set (cross_product T_0 T_1)) (set_type))) (ilf_type T_1 (set_type)) (ilf_type T_0 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) ### Imply 9 13 % 2.86/3.05 15. (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (ilf_type T_0 (set_type)) (ilf_type T_1 (set_type)) (-. (ilf_type (power_set (cross_product T_0 T_1)) (set_type))) ### All 14 % 2.86/3.05 16. (-. (empty (power_set (cross_product T_0 T_1)))) (empty (power_set (cross_product T_0 T_1))) ### Axiom % 2.86/3.05 17. (ilf_type T_2 (set_type)) (-. (ilf_type T_2 (set_type))) ### Axiom % 2.86/3.05 18. (member T_2 (empty_set)) (-. (member T_2 (empty_set))) ### Axiom % 2.86/3.05 19. ((ilf_type T_2 (set_type)) => (-. (member T_2 (empty_set)))) (member T_2 (empty_set)) (ilf_type T_2 (set_type)) ### Imply 17 18 % 2.86/3.05 20. (All B, ((ilf_type B (set_type)) => (-. (member B (empty_set))))) (ilf_type T_2 (set_type)) (member T_2 (empty_set)) ### All 19 % 2.86/3.05 21. (-. ((ilf_type T_2 (set_type)) => ((member T_2 (empty_set)) => (member T_2 (cross_product T_0 T_1))))) (All B, ((ilf_type B (set_type)) => (-. (member B (empty_set))))) ### ConjTree 20 % 2.86/3.05 22. (-. (All D, ((ilf_type D (set_type)) => ((member D (empty_set)) => (member D (cross_product T_0 T_1)))))) (All B, ((ilf_type B (set_type)) => (-. (member B (empty_set))))) ### NotAllEx 21 % 2.86/3.05 23. (-. (member (empty_set) (power_set (cross_product T_0 T_1)))) (member (empty_set) (power_set (cross_product T_0 T_1))) ### Axiom % 2.86/3.05 24. ((member (empty_set) (power_set (cross_product T_0 T_1))) <=> (All D, ((ilf_type D (set_type)) => ((member D (empty_set)) => (member D (cross_product T_0 T_1)))))) (-. (member (empty_set) (power_set (cross_product T_0 T_1)))) (All B, ((ilf_type B (set_type)) => (-. (member B (empty_set))))) ### Equiv 22 23 % 2.86/3.05 25. ((ilf_type (cross_product T_0 T_1) (set_type)) => ((member (empty_set) (power_set (cross_product T_0 T_1))) <=> (All D, ((ilf_type D (set_type)) => ((member D (empty_set)) => (member D (cross_product T_0 T_1))))))) (All B, ((ilf_type B (set_type)) => (-. (member B (empty_set))))) (-. (member (empty_set) (power_set (cross_product T_0 T_1)))) (ilf_type T_1 (set_type)) (ilf_type T_0 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) ### Imply 9 24 % 2.86/3.05 26. (All C, ((ilf_type C (set_type)) => ((member (empty_set) (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D (empty_set)) => (member D C))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (ilf_type T_0 (set_type)) (ilf_type T_1 (set_type)) (-. (member (empty_set) (power_set (cross_product T_0 T_1)))) (All B, ((ilf_type B (set_type)) => (-. (member B (empty_set))))) ### All 25 % 2.86/3.05 27. (-. (ilf_type (empty_set) (member_type (power_set (cross_product T_0 T_1))))) (ilf_type (empty_set) (member_type (power_set (cross_product T_0 T_1)))) ### Axiom % 2.86/3.05 28. ((ilf_type (empty_set) (member_type (power_set (cross_product T_0 T_1)))) <=> (member (empty_set) (power_set (cross_product T_0 T_1)))) (-. (ilf_type (empty_set) (member_type (power_set (cross_product T_0 T_1))))) (All B, ((ilf_type B (set_type)) => (-. (member B (empty_set))))) (ilf_type T_1 (set_type)) (ilf_type T_0 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (All C, ((ilf_type C (set_type)) => ((member (empty_set) (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D (empty_set)) => (member D C))))))) ### Equiv 26 27 % 2.86/3.05 29. (((-. (empty (power_set (cross_product T_0 T_1)))) /\ (ilf_type (power_set (cross_product T_0 T_1)) (set_type))) => ((ilf_type (empty_set) (member_type (power_set (cross_product T_0 T_1)))) <=> (member (empty_set) (power_set (cross_product T_0 T_1))))) (All C, ((ilf_type C (set_type)) => ((member (empty_set) (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D (empty_set)) => (member D C))))))) (All B, ((ilf_type B (set_type)) => (-. (member B (empty_set))))) (-. (ilf_type (empty_set) (member_type (power_set (cross_product T_0 T_1))))) (ilf_type T_1 (set_type)) (ilf_type T_0 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (-. (empty (power_set (cross_product T_0 T_1)))) ### DisjTree 16 15 28 % 2.86/3.05 30. (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type (empty_set) (member_type C)) <=> (member (empty_set) C)))) (-. (empty (power_set (cross_product T_0 T_1)))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (ilf_type T_0 (set_type)) (ilf_type T_1 (set_type)) (-. (ilf_type (empty_set) (member_type (power_set (cross_product T_0 T_1))))) (All B, ((ilf_type B (set_type)) => (-. (member B (empty_set))))) (All C, ((ilf_type C (set_type)) => ((member (empty_set) (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D (empty_set)) => (member D C))))))) ### All 29 % 2.86/3.05 31. ((ilf_type (empty_set) (set_type)) => (All C, ((ilf_type C (set_type)) => ((member (empty_set) (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D (empty_set)) => (member D C)))))))) (All B, ((ilf_type B (set_type)) => (-. (member B (empty_set))))) (-. (ilf_type (empty_set) (member_type (power_set (cross_product T_0 T_1))))) (ilf_type T_1 (set_type)) (ilf_type T_0 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (-. (empty (power_set (cross_product T_0 T_1)))) (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type (empty_set) (member_type C)) <=> (member (empty_set) C)))) (All B, (ilf_type B (set_type))) ### Imply 11 30 % 2.86/3.07 32. (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (All B, (ilf_type B (set_type))) (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type (empty_set) (member_type C)) <=> (member (empty_set) C)))) (-. (empty (power_set (cross_product T_0 T_1)))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (ilf_type T_0 (set_type)) (ilf_type T_1 (set_type)) (-. (ilf_type (empty_set) (member_type (power_set (cross_product T_0 T_1))))) (All B, ((ilf_type B (set_type)) => (-. (member B (empty_set))))) ### All 31 % 2.86/3.07 33. (empty (power_set (cross_product T_0 T_1))) (-. (empty (power_set (cross_product T_0 T_1)))) ### Axiom % 2.86/3.07 34. ((-. (empty (power_set (cross_product T_0 T_1)))) /\ (ilf_type (power_set (cross_product T_0 T_1)) (set_type))) (empty (power_set (cross_product T_0 T_1))) ### And 33 % 2.86/3.07 35. ((ilf_type (cross_product T_0 T_1) (set_type)) => ((-. (empty (power_set (cross_product T_0 T_1)))) /\ (ilf_type (power_set (cross_product T_0 T_1)) (set_type)))) (empty (power_set (cross_product T_0 T_1))) (ilf_type T_1 (set_type)) (ilf_type T_0 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) ### Imply 9 34 % 2.86/3.07 36. (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (ilf_type T_0 (set_type)) (ilf_type T_1 (set_type)) (empty (power_set (cross_product T_0 T_1))) ### All 35 % 2.86/3.07 37. ((empty (power_set (cross_product T_0 T_1))) <=> (All C, ((ilf_type C (set_type)) => (-. (member C (power_set (cross_product T_0 T_1))))))) (All B, ((ilf_type B (set_type)) => (-. (member B (empty_set))))) (-. (ilf_type (empty_set) (member_type (power_set (cross_product T_0 T_1))))) (ilf_type T_1 (set_type)) (ilf_type T_0 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type (empty_set) (member_type C)) <=> (member (empty_set) C)))) (All B, (ilf_type B (set_type))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) ### Equiv 32 36 % 2.86/3.07 38. ((ilf_type (power_set (cross_product T_0 T_1)) (set_type)) => ((empty (power_set (cross_product T_0 T_1))) <=> (All C, ((ilf_type C (set_type)) => (-. (member C (power_set (cross_product T_0 T_1)))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (All B, (ilf_type B (set_type))) (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type (empty_set) (member_type C)) <=> (member (empty_set) C)))) (-. (ilf_type (empty_set) (member_type (power_set (cross_product T_0 T_1))))) (All B, ((ilf_type B (set_type)) => (-. (member B (empty_set))))) (ilf_type T_1 (set_type)) (ilf_type T_0 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) ### Imply 15 37 % 2.86/3.07 39. (All B, ((ilf_type B (set_type)) => ((empty B) <=> (All C, ((ilf_type C (set_type)) => (-. (member C B))))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (ilf_type T_0 (set_type)) (ilf_type T_1 (set_type)) (All B, ((ilf_type B (set_type)) => (-. (member B (empty_set))))) (-. (ilf_type (empty_set) (member_type (power_set (cross_product T_0 T_1))))) (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type (empty_set) (member_type C)) <=> (member (empty_set) C)))) (All B, (ilf_type B (set_type))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) ### All 38 % 2.86/3.07 40. ((ilf_type (empty_set) (set_type)) => (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type (empty_set) (member_type C)) <=> (member (empty_set) C))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (-. (ilf_type (empty_set) (member_type (power_set (cross_product T_0 T_1))))) (All B, ((ilf_type B (set_type)) => (-. (member B (empty_set))))) (ilf_type T_1 (set_type)) (ilf_type T_0 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => ((empty B) <=> (All C, ((ilf_type C (set_type)) => (-. (member C B))))))) (All B, (ilf_type B (set_type))) ### Imply 11 39 % 2.86/3.07 41. (All B, ((ilf_type B (set_type)) => (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type B (member_type C)) <=> (member B C)))))) (All B, (ilf_type B (set_type))) (All B, ((ilf_type B (set_type)) => ((empty B) <=> (All C, ((ilf_type C (set_type)) => (-. (member C B))))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (ilf_type T_0 (set_type)) (ilf_type T_1 (set_type)) (All B, ((ilf_type B (set_type)) => (-. (member B (empty_set))))) (-. (ilf_type (empty_set) (member_type (power_set (cross_product T_0 T_1))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) ### All 40 % 2.86/3.07 42. (-. (ilf_type (empty_set) (subset_type (cross_product T_0 T_1)))) (ilf_type (empty_set) (subset_type (cross_product T_0 T_1))) ### Axiom % 2.86/3.07 43. ((ilf_type (empty_set) (subset_type (cross_product T_0 T_1))) <=> (ilf_type (empty_set) (member_type (power_set (cross_product T_0 T_1))))) (-. (ilf_type (empty_set) (subset_type (cross_product T_0 T_1)))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (All B, ((ilf_type B (set_type)) => (-. (member B (empty_set))))) (ilf_type T_1 (set_type)) (ilf_type T_0 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => ((empty B) <=> (All C, ((ilf_type C (set_type)) => (-. (member C B))))))) (All B, (ilf_type B (set_type))) (All B, ((ilf_type B (set_type)) => (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type B (member_type C)) <=> (member B C)))))) ### Equiv 41 42 % 2.86/3.07 44. ((ilf_type (empty_set) (set_type)) => ((ilf_type (empty_set) (subset_type (cross_product T_0 T_1))) <=> (ilf_type (empty_set) (member_type (power_set (cross_product T_0 T_1)))))) (All B, ((ilf_type B (set_type)) => (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type B (member_type C)) <=> (member B C)))))) (All B, ((ilf_type B (set_type)) => ((empty B) <=> (All C, ((ilf_type C (set_type)) => (-. (member C B))))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (ilf_type T_0 (set_type)) (ilf_type T_1 (set_type)) (All B, ((ilf_type B (set_type)) => (-. (member B (empty_set))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (-. (ilf_type (empty_set) (subset_type (cross_product T_0 T_1)))) (All B, (ilf_type B (set_type))) ### Imply 11 43 % 2.86/3.08 45. (All C, ((ilf_type C (set_type)) => ((ilf_type C (subset_type (cross_product T_0 T_1))) <=> (ilf_type C (member_type (power_set (cross_product T_0 T_1))))))) (All B, (ilf_type B (set_type))) (-. (ilf_type (empty_set) (subset_type (cross_product T_0 T_1)))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (All B, ((ilf_type B (set_type)) => (-. (member B (empty_set))))) (ilf_type T_1 (set_type)) (ilf_type T_0 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => ((empty B) <=> (All C, ((ilf_type C (set_type)) => (-. (member C B))))))) (All B, ((ilf_type B (set_type)) => (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type B (member_type C)) <=> (member B C)))))) ### All 44 % 2.86/3.08 46. ((ilf_type (cross_product T_0 T_1) (set_type)) => (All C, ((ilf_type C (set_type)) => ((ilf_type C (subset_type (cross_product T_0 T_1))) <=> (ilf_type C (member_type (power_set (cross_product T_0 T_1)))))))) (All B, ((ilf_type B (set_type)) => (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type B (member_type C)) <=> (member B C)))))) (All B, ((ilf_type B (set_type)) => ((empty B) <=> (All C, ((ilf_type C (set_type)) => (-. (member C B))))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => (-. (member B (empty_set))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (-. (ilf_type (empty_set) (subset_type (cross_product T_0 T_1)))) (All B, (ilf_type B (set_type))) (ilf_type T_1 (set_type)) (ilf_type T_0 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) ### Imply 9 45 % 2.86/3.08 47. (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((ilf_type C (subset_type B)) <=> (ilf_type C (member_type (power_set B)))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (ilf_type T_0 (set_type)) (ilf_type T_1 (set_type)) (All B, (ilf_type B (set_type))) (-. (ilf_type (empty_set) (subset_type (cross_product T_0 T_1)))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (All B, ((ilf_type B (set_type)) => (-. (member B (empty_set))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => ((empty B) <=> (All C, ((ilf_type C (set_type)) => (-. (member C B))))))) (All B, ((ilf_type B (set_type)) => (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type B (member_type C)) <=> (member B C)))))) ### All 46 % 2.86/3.08 48. (-. (ilf_type (empty_set) (relation_type T_0 T_1))) (ilf_type (empty_set) (relation_type T_0 T_1)) ### Axiom % 2.86/3.08 49. ((ilf_type (empty_set) (subset_type (cross_product T_0 T_1))) => (ilf_type (empty_set) (relation_type T_0 T_1))) (-. (ilf_type (empty_set) (relation_type T_0 T_1))) (All B, ((ilf_type B (set_type)) => (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type B (member_type C)) <=> (member B C)))))) (All B, ((ilf_type B (set_type)) => ((empty B) <=> (All C, ((ilf_type C (set_type)) => (-. (member C B))))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => (-. (member B (empty_set))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (All B, (ilf_type B (set_type))) (ilf_type T_1 (set_type)) (ilf_type T_0 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((ilf_type C (subset_type B)) <=> (ilf_type C (member_type (power_set B)))))))) ### Imply 47 48 % 2.86/3.08 50. (All D, ((ilf_type D (subset_type (cross_product T_0 T_1))) => (ilf_type D (relation_type T_0 T_1)))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((ilf_type C (subset_type B)) <=> (ilf_type C (member_type (power_set B)))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (ilf_type T_0 (set_type)) (ilf_type T_1 (set_type)) (All B, (ilf_type B (set_type))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (All B, ((ilf_type B (set_type)) => (-. (member B (empty_set))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => ((empty B) <=> (All C, ((ilf_type C (set_type)) => (-. (member C B))))))) (All B, ((ilf_type B (set_type)) => (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type B (member_type C)) <=> (member B C)))))) (-. (ilf_type (empty_set) (relation_type T_0 T_1))) ### All 49 % 2.86/3.08 51. ((All D, ((ilf_type D (subset_type (cross_product T_0 T_1))) => (ilf_type D (relation_type T_0 T_1)))) /\ (All E, ((ilf_type E (relation_type T_0 T_1)) => (ilf_type E (subset_type (cross_product T_0 T_1)))))) (-. (ilf_type (empty_set) (relation_type T_0 T_1))) (All B, ((ilf_type B (set_type)) => (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type B (member_type C)) <=> (member B C)))))) (All B, ((ilf_type B (set_type)) => ((empty B) <=> (All C, ((ilf_type C (set_type)) => (-. (member C B))))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => (-. (member B (empty_set))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (All B, (ilf_type B (set_type))) (ilf_type T_1 (set_type)) (ilf_type T_0 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((ilf_type C (subset_type B)) <=> (ilf_type C (member_type (power_set B)))))))) ### And 50 % 2.86/3.08 52. ((ilf_type T_1 (set_type)) => ((All D, ((ilf_type D (subset_type (cross_product T_0 T_1))) => (ilf_type D (relation_type T_0 T_1)))) /\ (All E, ((ilf_type E (relation_type T_0 T_1)) => (ilf_type E (subset_type (cross_product T_0 T_1))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((ilf_type C (subset_type B)) <=> (ilf_type C (member_type (power_set B)))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (ilf_type T_0 (set_type)) (All B, (ilf_type B (set_type))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (All B, ((ilf_type B (set_type)) => (-. (member B (empty_set))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => ((empty B) <=> (All C, ((ilf_type C (set_type)) => (-. (member C B))))))) (All B, ((ilf_type B (set_type)) => (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type B (member_type C)) <=> (member B C)))))) (-. (ilf_type (empty_set) (relation_type T_0 T_1))) (ilf_type T_1 (set_type)) ### Imply 2 51 % 2.86/3.09 53. (All C, ((ilf_type C (set_type)) => ((All D, ((ilf_type D (subset_type (cross_product T_0 C))) => (ilf_type D (relation_type T_0 C)))) /\ (All E, ((ilf_type E (relation_type T_0 C)) => (ilf_type E (subset_type (cross_product T_0 C)))))))) (ilf_type T_1 (set_type)) (-. (ilf_type (empty_set) (relation_type T_0 T_1))) (All B, ((ilf_type B (set_type)) => (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type B (member_type C)) <=> (member B C)))))) (All B, ((ilf_type B (set_type)) => ((empty B) <=> (All C, ((ilf_type C (set_type)) => (-. (member C B))))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => (-. (member B (empty_set))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (All B, (ilf_type B (set_type))) (ilf_type T_0 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((ilf_type C (subset_type B)) <=> (ilf_type C (member_type (power_set B)))))))) ### All 52 % 2.86/3.09 54. ((ilf_type T_0 (set_type)) => (All C, ((ilf_type C (set_type)) => ((All D, ((ilf_type D (subset_type (cross_product T_0 C))) => (ilf_type D (relation_type T_0 C)))) /\ (All E, ((ilf_type E (relation_type T_0 C)) => (ilf_type E (subset_type (cross_product T_0 C))))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((ilf_type C (subset_type B)) <=> (ilf_type C (member_type (power_set B)))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (All B, (ilf_type B (set_type))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (All B, ((ilf_type B (set_type)) => (-. (member B (empty_set))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => ((empty B) <=> (All C, ((ilf_type C (set_type)) => (-. (member C B))))))) (All B, ((ilf_type B (set_type)) => (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type B (member_type C)) <=> (member B C)))))) (-. (ilf_type (empty_set) (relation_type T_0 T_1))) (ilf_type T_1 (set_type)) (ilf_type T_0 (set_type)) ### Imply 1 53 % 2.86/3.09 55. (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((All D, ((ilf_type D (subset_type (cross_product B C))) => (ilf_type D (relation_type B C)))) /\ (All E, ((ilf_type E (relation_type B C)) => (ilf_type E (subset_type (cross_product B C)))))))))) (ilf_type T_0 (set_type)) (ilf_type T_1 (set_type)) (-. (ilf_type (empty_set) (relation_type T_0 T_1))) (All B, ((ilf_type B (set_type)) => (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type B (member_type C)) <=> (member B C)))))) (All B, ((ilf_type B (set_type)) => ((empty B) <=> (All C, ((ilf_type C (set_type)) => (-. (member C B))))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => (-. (member B (empty_set))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (All B, (ilf_type B (set_type))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((ilf_type C (subset_type B)) <=> (ilf_type C (member_type (power_set B)))))))) ### All 54 % 2.86/3.09 56. (-. ((ilf_type T_1 (set_type)) => (ilf_type (empty_set) (relation_type T_0 T_1)))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((ilf_type C (subset_type B)) <=> (ilf_type C (member_type (power_set B)))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (All B, (ilf_type B (set_type))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (All B, ((ilf_type B (set_type)) => (-. (member B (empty_set))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => ((empty B) <=> (All C, ((ilf_type C (set_type)) => (-. (member C B))))))) (All B, ((ilf_type B (set_type)) => (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type B (member_type C)) <=> (member B C)))))) (ilf_type T_0 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((All D, ((ilf_type D (subset_type (cross_product B C))) => (ilf_type D (relation_type B C)))) /\ (All E, ((ilf_type E (relation_type B C)) => (ilf_type E (subset_type (cross_product B C)))))))))) ### NotImply 55 % 2.86/3.09 57. (-. (All C, ((ilf_type C (set_type)) => (ilf_type (empty_set) (relation_type T_0 C))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((All D, ((ilf_type D (subset_type (cross_product B C))) => (ilf_type D (relation_type B C)))) /\ (All E, ((ilf_type E (relation_type B C)) => (ilf_type E (subset_type (cross_product B C)))))))))) (ilf_type T_0 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type B (member_type C)) <=> (member B C)))))) (All B, ((ilf_type B (set_type)) => ((empty B) <=> (All C, ((ilf_type C (set_type)) => (-. (member C B))))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => (-. (member B (empty_set))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (All B, (ilf_type B (set_type))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((ilf_type C (subset_type B)) <=> (ilf_type C (member_type (power_set B)))))))) ### NotAllEx 56 % 2.86/3.09 58. (-. ((ilf_type T_0 (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (empty_set) (relation_type T_0 C)))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((ilf_type C (subset_type B)) <=> (ilf_type C (member_type (power_set B)))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (All B, (ilf_type B (set_type))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (All B, ((ilf_type B (set_type)) => (-. (member B (empty_set))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => ((empty B) <=> (All C, ((ilf_type C (set_type)) => (-. (member C B))))))) (All B, ((ilf_type B (set_type)) => (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type B (member_type C)) <=> (member B C)))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((All D, ((ilf_type D (subset_type (cross_product B C))) => (ilf_type D (relation_type B C)))) /\ (All E, ((ilf_type E (relation_type B C)) => (ilf_type E (subset_type (cross_product B C)))))))))) ### NotImply 57 % 2.86/3.10 59. (-. (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (empty_set) (relation_type B C))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((All D, ((ilf_type D (subset_type (cross_product B C))) => (ilf_type D (relation_type B C)))) /\ (All E, ((ilf_type E (relation_type B C)) => (ilf_type E (subset_type (cross_product B C)))))))))) (All B, ((ilf_type B (set_type)) => (All C, (((-. (empty C)) /\ (ilf_type C (set_type))) => ((ilf_type B (member_type C)) <=> (member B C)))))) (All B, ((ilf_type B (set_type)) => ((empty B) <=> (All C, ((ilf_type C (set_type)) => (-. (member C B))))))) (All B, ((ilf_type B (set_type)) => ((-. (empty (power_set B))) /\ (ilf_type (power_set B) (set_type))))) (All B, ((ilf_type B (set_type)) => (-. (member B (empty_set))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (All B, (ilf_type B (set_type))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (ilf_type (cross_product B C) (set_type)))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((ilf_type C (subset_type B)) <=> (ilf_type C (member_type (power_set B)))))))) ### NotAllEx 58 % 2.86/3.10 % SZS output end Proof % 2.86/3.10 (* END-PROOF *) %------------------------------------------------------------------------------