%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SET654+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 : n022.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:10 EDT 2022 % Result : Theorem 3.06s 3.28s % Output : Proof 3.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SET654+3 : TPTP v8.1.0. Released v2.2.0. % 0.12/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n022.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 : Sat Jul 9 16:04:10 EDT 2022 % 0.12/0.33 % CPUTime : % 3.06/3.28 % SZS status Theorem % 3.06/3.28 (* PROOF-FOUND *) % 3.06/3.28 (* BEGIN-PROOF *) % 3.06/3.28 % SZS output start Proof % 3.06/3.28 1. (ilf_type T_0 (set_type)) (-. (ilf_type T_0 (set_type))) ### Axiom % 3.06/3.28 2. (ilf_type T_1 (set_type)) (-. (ilf_type T_1 (set_type))) ### Axiom % 3.06/3.28 3. (ilf_type T_2 (set_type)) (-. (ilf_type T_2 (set_type))) ### Axiom % 3.06/3.28 4. (ilf_type T_3 (relation_type T_2 T_0)) (-. (ilf_type T_3 (relation_type T_2 T_0))) ### Axiom % 3.06/3.28 5. (ilf_type T_0 (set_type)) (-. (ilf_type T_0 (set_type))) ### Axiom % 3.06/3.28 6. (ilf_type T_0 (set_type)) (-. (ilf_type T_0 (set_type))) ### Axiom % 3.06/3.28 7. (ilf_type T_1 (set_type)) (-. (ilf_type T_1 (set_type))) ### Axiom % 3.06/3.28 8. (ilf_type T_1 (set_type)) (-. (ilf_type T_1 (set_type))) ### Axiom % 3.06/3.28 9. (subset T_0 T_1) (-. (subset T_0 T_1)) ### Axiom % 3.06/3.28 10. (-. (All D, ((ilf_type D (set_type)) => ((member D T_0) => (member D T_1))))) (All D, ((ilf_type D (set_type)) => ((member D T_0) => (member D T_1)))) ### Axiom % 3.06/3.28 11. ((subset T_0 T_1) <=> (All D, ((ilf_type D (set_type)) => ((member D T_0) => (member D T_1))))) (-. (All D, ((ilf_type D (set_type)) => ((member D T_0) => (member D T_1))))) (subset T_0 T_1) ### Equiv 9 10 % 3.06/3.28 12. ((ilf_type T_1 (set_type)) => ((subset T_0 T_1) <=> (All D, ((ilf_type D (set_type)) => ((member D T_0) => (member D T_1)))))) (subset T_0 T_1) (-. (All D, ((ilf_type D (set_type)) => ((member D T_0) => (member D T_1))))) (ilf_type T_1 (set_type)) ### Imply 8 11 % 3.06/3.28 13. (All C, ((ilf_type C (set_type)) => ((subset T_0 C) <=> (All D, ((ilf_type D (set_type)) => ((member D T_0) => (member D C))))))) (ilf_type T_1 (set_type)) (-. (All D, ((ilf_type D (set_type)) => ((member D T_0) => (member D T_1))))) (subset T_0 T_1) ### All 12 % 3.06/3.28 14. (-. (ilf_type (range_of T_3) (set_type))) (ilf_type (range_of T_3) (set_type)) ### Axiom % 3.06/3.28 15. (All B, (ilf_type B (set_type))) (-. (ilf_type (range_of T_3) (set_type))) ### All 14 % 3.06/3.28 16. (ilf_type T_1 (set_type)) (-. (ilf_type T_1 (set_type))) ### Axiom % 3.06/3.28 17. (ilf_type T_0 (set_type)) (-. (ilf_type T_0 (set_type))) ### Axiom % 3.06/3.28 18. (ilf_type T_2 (set_type)) (-. (ilf_type T_2 (set_type))) ### Axiom % 3.06/3.28 19. (ilf_type T_0 (set_type)) (-. (ilf_type T_0 (set_type))) ### Axiom % 3.06/3.28 20. (ilf_type T_3 (relation_type T_2 T_0)) (-. (ilf_type T_3 (relation_type T_2 T_0))) ### Axiom % 3.06/3.28 21. (-. (subset (range_of T_3) T_0)) (subset (range_of T_3) T_0) ### Axiom % 3.06/3.28 22. ((subset (domain_of T_3) T_2) /\ (subset (range_of T_3) T_0)) (-. (subset (range_of T_3) T_0)) ### And 21 % 3.06/3.28 23. ((ilf_type T_3 (relation_type T_2 T_0)) => ((subset (domain_of T_3) T_2) /\ (subset (range_of T_3) T_0))) (-. (subset (range_of T_3) T_0)) (ilf_type T_3 (relation_type T_2 T_0)) ### Imply 20 22 % 3.06/3.28 24. (All D, ((ilf_type D (relation_type T_2 T_0)) => ((subset (domain_of D) T_2) /\ (subset (range_of D) T_0)))) (ilf_type T_3 (relation_type T_2 T_0)) (-. (subset (range_of T_3) T_0)) ### All 23 % 3.06/3.28 25. ((ilf_type T_0 (set_type)) => (All D, ((ilf_type D (relation_type T_2 T_0)) => ((subset (domain_of D) T_2) /\ (subset (range_of D) T_0))))) (-. (subset (range_of T_3) T_0)) (ilf_type T_3 (relation_type T_2 T_0)) (ilf_type T_0 (set_type)) ### Imply 19 24 % 3.06/3.28 26. (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (relation_type T_2 C)) => ((subset (domain_of D) T_2) /\ (subset (range_of D) C)))))) (ilf_type T_0 (set_type)) (ilf_type T_3 (relation_type T_2 T_0)) (-. (subset (range_of T_3) T_0)) ### All 25 % 3.06/3.28 27. ((ilf_type T_2 (set_type)) => (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (relation_type T_2 C)) => ((subset (domain_of D) T_2) /\ (subset (range_of D) C))))))) (-. (subset (range_of T_3) T_0)) (ilf_type T_3 (relation_type T_2 T_0)) (ilf_type T_0 (set_type)) (ilf_type T_2 (set_type)) ### Imply 18 26 % 3.06/3.28 28. (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (relation_type B C)) => ((subset (domain_of D) B) /\ (subset (range_of D) C)))))))) (ilf_type T_2 (set_type)) (ilf_type T_0 (set_type)) (ilf_type T_3 (relation_type T_2 T_0)) (-. (subset (range_of T_3) T_0)) ### All 27 % 3.06/3.28 29. (ilf_type T_4 (set_type)) (-. (ilf_type T_4 (set_type))) ### Axiom % 3.06/3.28 30. (ilf_type T_4 (set_type)) (-. (ilf_type T_4 (set_type))) ### Axiom % 3.06/3.28 31. (member T_4 (range_of T_3)) (-. (member T_4 (range_of T_3))) ### Axiom % 3.06/3.28 32. (-. (member T_4 T_0)) (member T_4 T_0) ### Axiom % 3.06/3.28 33. ((ilf_type T_4 (set_type)) => ((member T_4 (range_of T_3)) => (member T_4 T_0))) (-. (member T_4 T_0)) (member T_4 (range_of T_3)) (ilf_type T_4 (set_type)) ### DisjTree 30 31 32 % 3.06/3.28 34. (All D, ((ilf_type D (set_type)) => ((member D (range_of T_3)) => (member D T_0)))) (ilf_type T_4 (set_type)) (member T_4 (range_of T_3)) (-. (member T_4 T_0)) ### All 33 % 3.06/3.28 35. (-. (member T_4 T_1)) (member T_4 T_1) ### Axiom % 3.06/3.28 36. ((ilf_type T_4 (set_type)) => ((member T_4 T_0) => (member T_4 T_1))) (-. (member T_4 T_1)) (member T_4 (range_of T_3)) (All D, ((ilf_type D (set_type)) => ((member D (range_of T_3)) => (member D T_0)))) (ilf_type T_4 (set_type)) ### DisjTree 29 34 35 % 3.06/3.28 37. (All D, ((ilf_type D (set_type)) => ((member D T_0) => (member D T_1)))) (ilf_type T_4 (set_type)) (All D, ((ilf_type D (set_type)) => ((member D (range_of T_3)) => (member D T_0)))) (member T_4 (range_of T_3)) (-. (member T_4 T_1)) ### All 36 % 3.06/3.28 38. ((subset (range_of T_3) T_0) <=> (All D, ((ilf_type D (set_type)) => ((member D (range_of T_3)) => (member D T_0))))) (-. (member T_4 T_1)) (member T_4 (range_of T_3)) (ilf_type T_4 (set_type)) (All D, ((ilf_type D (set_type)) => ((member D T_0) => (member D T_1)))) (ilf_type T_3 (relation_type T_2 T_0)) (ilf_type T_0 (set_type)) (ilf_type T_2 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (relation_type B C)) => ((subset (domain_of D) B) /\ (subset (range_of D) C)))))))) ### Equiv 28 37 % 3.06/3.28 39. ((ilf_type T_0 (set_type)) => ((subset (range_of T_3) T_0) <=> (All D, ((ilf_type D (set_type)) => ((member D (range_of T_3)) => (member D T_0)))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (relation_type B C)) => ((subset (domain_of D) B) /\ (subset (range_of D) C)))))))) (ilf_type T_2 (set_type)) (ilf_type T_3 (relation_type T_2 T_0)) (All D, ((ilf_type D (set_type)) => ((member D T_0) => (member D T_1)))) (ilf_type T_4 (set_type)) (member T_4 (range_of T_3)) (-. (member T_4 T_1)) (ilf_type T_0 (set_type)) ### Imply 17 38 % 3.06/3.28 40. (All C, ((ilf_type C (set_type)) => ((subset (range_of T_3) C) <=> (All D, ((ilf_type D (set_type)) => ((member D (range_of T_3)) => (member D C))))))) (ilf_type T_0 (set_type)) (-. (member T_4 T_1)) (member T_4 (range_of T_3)) (ilf_type T_4 (set_type)) (All D, ((ilf_type D (set_type)) => ((member D T_0) => (member D T_1)))) (ilf_type T_3 (relation_type T_2 T_0)) (ilf_type T_2 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (relation_type B C)) => ((subset (domain_of D) B) /\ (subset (range_of D) C)))))))) ### All 39 % 3.06/3.28 41. (-. ((ilf_type T_4 (set_type)) => ((member T_4 (range_of T_3)) => (member T_4 T_1)))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (relation_type B C)) => ((subset (domain_of D) B) /\ (subset (range_of D) C)))))))) (ilf_type T_2 (set_type)) (ilf_type T_3 (relation_type T_2 T_0)) (All D, ((ilf_type D (set_type)) => ((member D T_0) => (member D T_1)))) (ilf_type T_0 (set_type)) (All C, ((ilf_type C (set_type)) => ((subset (range_of T_3) C) <=> (All D, ((ilf_type D (set_type)) => ((member D (range_of T_3)) => (member D C))))))) ### ConjTree 40 % 3.06/3.28 42. (-. (All D, ((ilf_type D (set_type)) => ((member D (range_of T_3)) => (member D T_1))))) (All C, ((ilf_type C (set_type)) => ((subset (range_of T_3) C) <=> (All D, ((ilf_type D (set_type)) => ((member D (range_of T_3)) => (member D C))))))) (ilf_type T_0 (set_type)) (All D, ((ilf_type D (set_type)) => ((member D T_0) => (member D T_1)))) (ilf_type T_3 (relation_type T_2 T_0)) (ilf_type T_2 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (relation_type B C)) => ((subset (domain_of D) B) /\ (subset (range_of D) C)))))))) ### NotAllEx 41 % 3.06/3.28 43. (-. (subset (range_of T_3) T_1)) (subset (range_of T_3) T_1) ### Axiom % 3.06/3.28 44. ((subset (range_of T_3) T_1) <=> (All D, ((ilf_type D (set_type)) => ((member D (range_of T_3)) => (member D T_1))))) (-. (subset (range_of T_3) T_1)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (relation_type B C)) => ((subset (domain_of D) B) /\ (subset (range_of D) C)))))))) (ilf_type T_2 (set_type)) (ilf_type T_3 (relation_type T_2 T_0)) (All D, ((ilf_type D (set_type)) => ((member D T_0) => (member D T_1)))) (ilf_type T_0 (set_type)) (All C, ((ilf_type C (set_type)) => ((subset (range_of T_3) C) <=> (All D, ((ilf_type D (set_type)) => ((member D (range_of T_3)) => (member D C))))))) ### Equiv 42 43 % 3.13/3.31 45. ((ilf_type T_1 (set_type)) => ((subset (range_of T_3) T_1) <=> (All D, ((ilf_type D (set_type)) => ((member D (range_of T_3)) => (member D T_1)))))) (All C, ((ilf_type C (set_type)) => ((subset (range_of T_3) C) <=> (All D, ((ilf_type D (set_type)) => ((member D (range_of T_3)) => (member D C))))))) (ilf_type T_0 (set_type)) (All D, ((ilf_type D (set_type)) => ((member D T_0) => (member D T_1)))) (ilf_type T_3 (relation_type T_2 T_0)) (ilf_type T_2 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (relation_type B C)) => ((subset (domain_of D) B) /\ (subset (range_of D) C)))))))) (-. (subset (range_of T_3) T_1)) (ilf_type T_1 (set_type)) ### Imply 16 44 % 3.13/3.31 46. (ilf_type T_1 (set_type)) (-. (subset (range_of T_3) T_1)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (relation_type B C)) => ((subset (domain_of D) B) /\ (subset (range_of D) C)))))))) (ilf_type T_2 (set_type)) (ilf_type T_3 (relation_type T_2 T_0)) (All D, ((ilf_type D (set_type)) => ((member D T_0) => (member D T_1)))) (ilf_type T_0 (set_type)) (All C, ((ilf_type C (set_type)) => ((subset (range_of T_3) C) <=> (All D, ((ilf_type D (set_type)) => ((member D (range_of T_3)) => (member D C))))))) ### All 45 % 3.13/3.31 47. ((ilf_type (range_of T_3) (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset (range_of T_3) C) <=> (All D, ((ilf_type D (set_type)) => ((member D (range_of T_3)) => (member D C)))))))) (ilf_type T_0 (set_type)) (All D, ((ilf_type D (set_type)) => ((member D T_0) => (member D T_1)))) (ilf_type T_3 (relation_type T_2 T_0)) (ilf_type T_2 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (relation_type B C)) => ((subset (domain_of D) B) /\ (subset (range_of D) C)))))))) (-. (subset (range_of T_3) T_1)) (ilf_type T_1 (set_type)) (All B, (ilf_type B (set_type))) ### Imply 15 46 % 3.13/3.31 48. (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B 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)) (-. (subset (range_of T_3) T_1)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (relation_type B C)) => ((subset (domain_of D) B) /\ (subset (range_of D) C)))))))) (ilf_type T_2 (set_type)) (ilf_type T_3 (relation_type T_2 T_0)) (All D, ((ilf_type D (set_type)) => ((member D T_0) => (member D T_1)))) (ilf_type T_0 (set_type)) ### All 47 % 3.13/3.31 49. ((member T_0 (power_set T_1)) <=> (All D, ((ilf_type D (set_type)) => ((member D T_0) => (member D T_1))))) (ilf_type T_0 (set_type)) (ilf_type T_3 (relation_type T_2 T_0)) (ilf_type T_2 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (relation_type B C)) => ((subset (domain_of D) B) /\ (subset (range_of D) C)))))))) (-. (subset (range_of T_3) T_1)) (All B, (ilf_type B (set_type))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (subset T_0 T_1) (ilf_type T_1 (set_type)) (All C, ((ilf_type C (set_type)) => ((subset T_0 C) <=> (All D, ((ilf_type D (set_type)) => ((member D T_0) => (member D C))))))) ### Equiv 13 48 % 3.13/3.31 50. ((ilf_type T_1 (set_type)) => ((member T_0 (power_set T_1)) <=> (All D, ((ilf_type D (set_type)) => ((member D T_0) => (member D T_1)))))) (All C, ((ilf_type C (set_type)) => ((subset T_0 C) <=> (All D, ((ilf_type D (set_type)) => ((member D T_0) => (member D C))))))) (subset T_0 T_1) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (All B, (ilf_type B (set_type))) (-. (subset (range_of T_3) T_1)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (relation_type B C)) => ((subset (domain_of D) B) /\ (subset (range_of D) C)))))))) (ilf_type T_2 (set_type)) (ilf_type T_3 (relation_type T_2 T_0)) (ilf_type T_0 (set_type)) (ilf_type T_1 (set_type)) ### Imply 7 49 % 3.13/3.31 51. (All C, ((ilf_type C (set_type)) => ((member T_0 (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D T_0) => (member D C))))))) (ilf_type T_1 (set_type)) (ilf_type T_0 (set_type)) (ilf_type T_3 (relation_type T_2 T_0)) (ilf_type T_2 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (relation_type B C)) => ((subset (domain_of D) B) /\ (subset (range_of D) C)))))))) (-. (subset (range_of T_3) T_1)) (All B, (ilf_type B (set_type))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (subset T_0 T_1) (All C, ((ilf_type C (set_type)) => ((subset T_0 C) <=> (All D, ((ilf_type D (set_type)) => ((member D T_0) => (member D C))))))) ### All 50 % 3.13/3.31 52. ((ilf_type T_0 (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset T_0 C) <=> (All D, ((ilf_type D (set_type)) => ((member D T_0) => (member D C)))))))) (subset T_0 T_1) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (All B, (ilf_type B (set_type))) (-. (subset (range_of T_3) T_1)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (relation_type B C)) => ((subset (domain_of D) B) /\ (subset (range_of D) C)))))))) (ilf_type T_2 (set_type)) (ilf_type T_3 (relation_type T_2 T_0)) (ilf_type T_1 (set_type)) (All C, ((ilf_type C (set_type)) => ((member T_0 (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D T_0) => (member D C))))))) (ilf_type T_0 (set_type)) ### Imply 6 51 % 3.13/3.31 53. (ilf_type T_0 (set_type)) (All C, ((ilf_type C (set_type)) => ((member T_0 (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D T_0) => (member D C))))))) (ilf_type T_1 (set_type)) (ilf_type T_3 (relation_type T_2 T_0)) (ilf_type T_2 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (relation_type B C)) => ((subset (domain_of D) B) /\ (subset (range_of D) C)))))))) (-. (subset (range_of T_3) T_1)) (All B, (ilf_type B (set_type))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (subset T_0 T_1) ### All 52 % 3.13/3.31 54. ((ilf_type T_0 (set_type)) => (All C, ((ilf_type C (set_type)) => ((member T_0 (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D T_0) => (member D C)))))))) (subset T_0 T_1) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (All B, (ilf_type B (set_type))) (-. (subset (range_of T_3) T_1)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (relation_type B C)) => ((subset (domain_of D) B) /\ (subset (range_of D) C)))))))) (ilf_type T_2 (set_type)) (ilf_type T_3 (relation_type T_2 T_0)) (ilf_type T_1 (set_type)) (ilf_type T_0 (set_type)) ### Imply 5 53 % 3.13/3.31 55. (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 T_0 (set_type)) (ilf_type T_1 (set_type)) (ilf_type T_3 (relation_type T_2 T_0)) (ilf_type T_2 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (relation_type B C)) => ((subset (domain_of D) B) /\ (subset (range_of D) C)))))))) (-. (subset (range_of T_3) T_1)) (All B, (ilf_type B (set_type))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (subset T_0 T_1) ### All 54 % 3.13/3.35 56. (-. (ilf_type T_3 (relation_type T_2 T_1))) (ilf_type T_3 (relation_type T_2 T_1)) ### Axiom % 3.13/3.35 57. ((ilf_type T_3 (relation_type T_2 T_0)) => ((subset (range_of T_3) T_1) => (ilf_type T_3 (relation_type T_2 T_1)))) (-. (ilf_type T_3 (relation_type T_2 T_1))) (subset T_0 T_1) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B 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)) => (All D, ((ilf_type D (relation_type B C)) => ((subset (domain_of D) B) /\ (subset (range_of D) C)))))))) (ilf_type T_2 (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)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (ilf_type T_3 (relation_type T_2 T_0)) ### DisjTree 4 55 56 % 3.13/3.35 58. (All E, ((ilf_type E (relation_type T_2 T_0)) => ((subset (range_of E) T_1) => (ilf_type E (relation_type T_2 T_1))))) (ilf_type T_3 (relation_type T_2 T_0)) (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 T_0 (set_type)) (ilf_type T_1 (set_type)) (ilf_type T_2 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (relation_type B C)) => ((subset (domain_of D) B) /\ (subset (range_of D) C)))))))) (All B, (ilf_type B (set_type))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (subset T_0 T_1) (-. (ilf_type T_3 (relation_type T_2 T_1))) ### All 57 % 3.13/3.35 59. ((ilf_type T_2 (set_type)) => (All E, ((ilf_type E (relation_type T_2 T_0)) => ((subset (range_of E) T_1) => (ilf_type E (relation_type T_2 T_1)))))) (-. (ilf_type T_3 (relation_type T_2 T_1))) (subset T_0 T_1) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B 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)) => (All D, ((ilf_type D (relation_type B C)) => ((subset (domain_of D) B) /\ (subset (range_of D) C)))))))) (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)) => ((member B (power_set C)) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (ilf_type T_3 (relation_type T_2 T_0)) (ilf_type T_2 (set_type)) ### Imply 3 58 % 3.13/3.35 60. (All D, ((ilf_type D (set_type)) => (All E, ((ilf_type E (relation_type D T_0)) => ((subset (range_of E) T_1) => (ilf_type E (relation_type D T_1))))))) (ilf_type T_2 (set_type)) (ilf_type T_3 (relation_type T_2 T_0)) (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 T_0 (set_type)) (ilf_type T_1 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (relation_type B C)) => ((subset (domain_of D) B) /\ (subset (range_of D) C)))))))) (All B, (ilf_type B (set_type))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (subset T_0 T_1) (-. (ilf_type T_3 (relation_type T_2 T_1))) ### All 59 % 3.13/3.35 61. ((ilf_type T_1 (set_type)) => (All D, ((ilf_type D (set_type)) => (All E, ((ilf_type E (relation_type D T_0)) => ((subset (range_of E) T_1) => (ilf_type E (relation_type D T_1)))))))) (-. (ilf_type T_3 (relation_type T_2 T_1))) (subset T_0 T_1) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B 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)) => (All D, ((ilf_type D (relation_type B C)) => ((subset (domain_of D) B) /\ (subset (range_of D) C)))))))) (ilf_type T_0 (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))))))))) (ilf_type T_3 (relation_type T_2 T_0)) (ilf_type T_2 (set_type)) (ilf_type T_1 (set_type)) ### Imply 2 60 % 3.13/3.35 62. (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (set_type)) => (All E, ((ilf_type E (relation_type D T_0)) => ((subset (range_of E) C) => (ilf_type E (relation_type D C))))))))) (ilf_type T_1 (set_type)) (ilf_type T_2 (set_type)) (ilf_type T_3 (relation_type T_2 T_0)) (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 T_0 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (relation_type B C)) => ((subset (domain_of D) B) /\ (subset (range_of D) C)))))))) (All B, (ilf_type B (set_type))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (subset T_0 T_1) (-. (ilf_type T_3 (relation_type T_2 T_1))) ### All 61 % 3.13/3.35 63. ((ilf_type T_0 (set_type)) => (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (set_type)) => (All E, ((ilf_type E (relation_type D T_0)) => ((subset (range_of E) C) => (ilf_type E (relation_type D C)))))))))) (-. (ilf_type T_3 (relation_type T_2 T_1))) (subset T_0 T_1) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B 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)) => (All D, ((ilf_type D (relation_type B C)) => ((subset (domain_of D) B) /\ (subset (range_of D) 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 T_3 (relation_type T_2 T_0)) (ilf_type T_2 (set_type)) (ilf_type T_1 (set_type)) (ilf_type T_0 (set_type)) ### Imply 1 62 % 3.13/3.35 64. (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (set_type)) => (All E, ((ilf_type E (relation_type D B)) => ((subset (range_of E) C) => (ilf_type E (relation_type D C))))))))))) (ilf_type T_0 (set_type)) (ilf_type T_1 (set_type)) (ilf_type T_2 (set_type)) (ilf_type T_3 (relation_type T_2 T_0)) (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, ((ilf_type C (set_type)) => (All D, ((ilf_type D (relation_type B C)) => ((subset (domain_of D) B) /\ (subset (range_of D) C)))))))) (All B, (ilf_type B (set_type))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) (subset T_0 T_1) (-. (ilf_type T_3 (relation_type T_2 T_1))) ### All 63 % 3.13/3.35 65. (-. ((ilf_type T_3 (relation_type T_2 T_0)) => ((subset T_0 T_1) => (ilf_type T_3 (relation_type T_2 T_1))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B 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)) => (All D, ((ilf_type D (relation_type B C)) => ((subset (domain_of D) B) /\ (subset (range_of D) 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 T_2 (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)) => (All D, ((ilf_type D (set_type)) => (All E, ((ilf_type E (relation_type D B)) => ((subset (range_of E) C) => (ilf_type E (relation_type D C))))))))))) ### ConjTree 64 % 3.20/3.37 66. (-. (All E, ((ilf_type E (relation_type T_2 T_0)) => ((subset T_0 T_1) => (ilf_type E (relation_type T_2 T_1)))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (set_type)) => (All E, ((ilf_type E (relation_type D B)) => ((subset (range_of E) C) => (ilf_type E (relation_type D C))))))))))) (ilf_type T_0 (set_type)) (ilf_type T_1 (set_type)) (ilf_type T_2 (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)) => (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (relation_type B C)) => ((subset (domain_of D) B) /\ (subset (range_of D) C)))))))) (All B, (ilf_type B (set_type))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) ### NotAllEx 65 % 3.20/3.37 67. (-. ((ilf_type T_2 (set_type)) => (All E, ((ilf_type E (relation_type T_2 T_0)) => ((subset T_0 T_1) => (ilf_type E (relation_type T_2 T_1))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B 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)) => (All D, ((ilf_type D (relation_type B C)) => ((subset (domain_of D) B) /\ (subset (range_of D) 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 T_1 (set_type)) (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 (set_type)) => (All E, ((ilf_type E (relation_type D B)) => ((subset (range_of E) C) => (ilf_type E (relation_type D C))))))))))) ### NotImply 66 % 3.20/3.37 68. (-. (All D, ((ilf_type D (set_type)) => (All E, ((ilf_type E (relation_type D T_0)) => ((subset T_0 T_1) => (ilf_type E (relation_type D T_1)))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (set_type)) => (All E, ((ilf_type E (relation_type D B)) => ((subset (range_of E) C) => (ilf_type E (relation_type D C))))))))))) (ilf_type T_0 (set_type)) (ilf_type T_1 (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)) => (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (relation_type B C)) => ((subset (domain_of D) B) /\ (subset (range_of D) C)))))))) (All B, (ilf_type B (set_type))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) ### NotAllEx 67 % 3.20/3.37 69. (-. ((ilf_type T_1 (set_type)) => (All D, ((ilf_type D (set_type)) => (All E, ((ilf_type E (relation_type D T_0)) => ((subset T_0 T_1) => (ilf_type E (relation_type D T_1))))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B 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)) => (All D, ((ilf_type D (relation_type B C)) => ((subset (domain_of D) B) /\ (subset (range_of D) 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 T_0 (set_type)) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (set_type)) => (All E, ((ilf_type E (relation_type D B)) => ((subset (range_of E) C) => (ilf_type E (relation_type D C))))))))))) ### NotImply 68 % 3.20/3.37 70. (-. (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (set_type)) => (All E, ((ilf_type E (relation_type D T_0)) => ((subset T_0 C) => (ilf_type E (relation_type D C)))))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (set_type)) => (All E, ((ilf_type E (relation_type D B)) => ((subset (range_of E) C) => (ilf_type E (relation_type D C))))))))))) (ilf_type T_0 (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)) => (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (relation_type B C)) => ((subset (domain_of D) B) /\ (subset (range_of D) C)))))))) (All B, (ilf_type B (set_type))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) ### NotAllEx 69 % 3.20/3.37 71. (-. ((ilf_type T_0 (set_type)) => (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (set_type)) => (All E, ((ilf_type E (relation_type D T_0)) => ((subset T_0 C) => (ilf_type E (relation_type D C))))))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B 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)) => (All D, ((ilf_type D (relation_type B C)) => ((subset (domain_of D) B) /\ (subset (range_of D) 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))))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (set_type)) => (All E, ((ilf_type E (relation_type D B)) => ((subset (range_of E) C) => (ilf_type E (relation_type D C))))))))))) ### NotImply 70 % 3.20/3.37 72. (-. (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (set_type)) => (All E, ((ilf_type E (relation_type D B)) => ((subset B C) => (ilf_type E (relation_type D C)))))))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (set_type)) => (All E, ((ilf_type E (relation_type D B)) => ((subset (range_of E) C) => (ilf_type E (relation_type D 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))))))))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => (All D, ((ilf_type D (relation_type B C)) => ((subset (domain_of D) B) /\ (subset (range_of D) C)))))))) (All B, (ilf_type B (set_type))) (All B, ((ilf_type B (set_type)) => (All C, ((ilf_type C (set_type)) => ((subset B C) <=> (All D, ((ilf_type D (set_type)) => ((member D B) => (member D C))))))))) ### NotAllEx 71 % 3.20/3.37 % SZS output end Proof % 3.20/3.37 (* END-PROOF *) %------------------------------------------------------------------------------