%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SET600+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 : n028.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:42:35 EDT 2022 % Result : Theorem 2.02s 2.24s % Output : Proof 2.02s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : SET600+3 : TPTP v8.1.0. Released v2.2.0. % 0.07/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.13/0.35 % Computer : n028.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 600 % 0.13/0.35 % DateTime : Sat Jul 9 23:26:26 EDT 2022 % 0.13/0.35 % CPUTime : % 2.02/2.24 % SZS status Theorem % 2.02/2.24 (* PROOF-FOUND *) % 2.02/2.24 (* BEGIN-PROOF *) % 2.02/2.24 % SZS output start Proof % 2.02/2.24 1. (T_0 = (empty_set)) (T_0 != (empty_set)) ### Axiom % 2.02/2.24 2. (T_1 != T_1) ### Refl(=) % 2.02/2.24 3. (T_0 != T_0) ### Refl(=) % 2.02/2.24 4. (T_2 = (empty_set)) (T_2 != (empty_set)) ### Axiom % 2.02/2.24 5. ((union T_0 T_2) != (union T_0 (empty_set))) (T_2 = (empty_set)) ### NotEqual 3 4 % 2.02/2.24 6. (-. (member T_1 (union T_0 (empty_set)))) (member T_1 (union T_0 T_2)) (T_2 = (empty_set)) ### P-NotP 2 5 % 2.02/2.24 7. (-. (member T_1 T_0)) (member T_1 T_0) ### Axiom % 2.02/2.24 8. (-. (member T_1 (empty_set))) (member T_1 (empty_set)) ### Axiom % 2.02/2.24 9. ((member T_1 T_0) \/ (member T_1 (empty_set))) (-. (member T_1 (empty_set))) (-. (member T_1 T_0)) ### Or 7 8 % 2.02/2.24 10. ((member T_1 (union T_0 (empty_set))) <=> ((member T_1 T_0) \/ (member T_1 (empty_set)))) (-. (member T_1 T_0)) (-. (member T_1 (empty_set))) (T_2 = (empty_set)) (member T_1 (union T_0 T_2)) ### Equiv 6 9 % 2.02/2.24 11. (All D, ((member D (union T_0 (empty_set))) <=> ((member D T_0) \/ (member D (empty_set))))) (member T_1 (union T_0 T_2)) (T_2 = (empty_set)) (-. (member T_1 (empty_set))) (-. (member T_1 T_0)) ### All 10 % 2.02/2.24 12. (All C, (All D, ((member D (union T_0 C)) <=> ((member D T_0) \/ (member D C))))) (-. (member T_1 T_0)) (-. (member T_1 (empty_set))) (T_2 = (empty_set)) (member T_1 (union T_0 T_2)) ### All 11 % 2.02/2.24 13. (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) (member T_1 (union T_0 T_2)) (T_2 = (empty_set)) (-. (member T_1 (empty_set))) (-. (member T_1 T_0)) ### All 12 % 2.02/2.24 14. (-. (member T_1 (empty_set))) (member T_1 (empty_set)) ### Axiom % 2.02/2.24 15. ((member T_1 T_0) <=> (member T_1 (empty_set))) (-. (member T_1 (empty_set))) (T_2 = (empty_set)) (member T_1 (union T_0 T_2)) (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) ### Equiv 13 14 % 2.02/2.24 16. (All D, ((member D T_0) <=> (member D (empty_set)))) (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) (member T_1 (union T_0 T_2)) (T_2 = (empty_set)) (-. (member T_1 (empty_set))) ### All 15 % 2.02/2.24 17. (member T_1 (empty_set)) (-. (member T_1 (empty_set))) ### Axiom % 2.02/2.24 18. (All B, (-. (member B (empty_set)))) (member T_1 (empty_set)) ### All 17 % 2.02/2.24 19. (-. ((member T_1 (empty_set)) <=> (member T_1 (union T_0 T_2)))) (All B, (-. (member B (empty_set)))) (T_2 = (empty_set)) (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) (All D, ((member D T_0) <=> (member D (empty_set)))) ### NotEquiv 16 18 % 2.02/2.24 20. (-. (All D, ((member D (empty_set)) <=> (member D (union T_0 T_2))))) (All D, ((member D T_0) <=> (member D (empty_set)))) (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) (T_2 = (empty_set)) (All B, (-. (member B (empty_set)))) ### NotAllEx 19 % 2.02/2.24 21. ((union T_0 T_2) != (empty_set)) ((empty_set) = (union T_0 T_2)) ### Sym(=) % 2.02/2.24 22. (((empty_set) = (union T_0 T_2)) <=> (All D, ((member D (empty_set)) <=> (member D (union T_0 T_2))))) ((union T_0 T_2) != (empty_set)) (All B, (-. (member B (empty_set)))) (T_2 = (empty_set)) (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) (All D, ((member D T_0) <=> (member D (empty_set)))) ### Equiv 20 21 % 2.02/2.24 23. (All C, (((empty_set) = C) <=> (All D, ((member D (empty_set)) <=> (member D C))))) (All D, ((member D T_0) <=> (member D (empty_set)))) (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) (T_2 = (empty_set)) (All B, (-. (member B (empty_set)))) ((union T_0 T_2) != (empty_set)) ### All 22 % 2.02/2.24 24. ((T_0 = (empty_set)) <=> (All D, ((member D T_0) <=> (member D (empty_set))))) ((union T_0 T_2) != (empty_set)) (All B, (-. (member B (empty_set)))) (T_2 = (empty_set)) (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) (All C, (((empty_set) = C) <=> (All D, ((member D (empty_set)) <=> (member D C))))) (T_0 = (empty_set)) ### Equiv 1 23 % 2.02/2.24 25. (All C, ((T_0 = C) <=> (All D, ((member D T_0) <=> (member D C))))) (T_0 = (empty_set)) (All C, (((empty_set) = C) <=> (All D, ((member D (empty_set)) <=> (member D C))))) (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) (T_2 = (empty_set)) (All B, (-. (member B (empty_set)))) ((union T_0 T_2) != (empty_set)) ### All 24 % 2.02/2.24 26. (All B, (All C, ((B = C) <=> (All D, ((member D B) <=> (member D C)))))) ((union T_0 T_2) != (empty_set)) (All B, (-. (member B (empty_set)))) (T_2 = (empty_set)) (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) (All C, (((empty_set) = C) <=> (All D, ((member D (empty_set)) <=> (member D C))))) (T_0 = (empty_set)) ### All 25 % 2.02/2.24 27. (T_0 = (empty_set)) (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) (T_2 = (empty_set)) (All B, (-. (member B (empty_set)))) ((union T_0 T_2) != (empty_set)) (All B, (All C, ((B = C) <=> (All D, ((member D B) <=> (member D C)))))) ### All 26 % 2.02/2.24 28. ((T_0 = (empty_set)) /\ (T_2 = (empty_set))) (All B, (All C, ((B = C) <=> (All D, ((member D B) <=> (member D C)))))) ((union T_0 T_2) != (empty_set)) (All B, (-. (member B (empty_set)))) (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) ### And 27 % 2.02/2.24 29. (member T_3 (empty_set)) (-. (member T_3 (empty_set))) ### Axiom % 2.02/2.24 30. (All B, (-. (member B (empty_set)))) (member T_3 (empty_set)) ### All 29 % 2.02/2.24 31. (-. ((member T_3 (empty_set)) => (member T_3 T_2))) (All B, (-. (member B (empty_set)))) ### NotImply 30 % 2.02/2.24 32. (-. (All D, ((member D (empty_set)) => (member D T_2)))) (All B, (-. (member B (empty_set)))) ### NotAllEx 31 % 2.02/2.24 33. (-. (subset (empty_set) T_2)) (All B, (-. (member B (empty_set)))) ### Definition-Pseudo(subset) 32 % 2.02/2.24 34. ((union T_0 T_2) = (empty_set)) ((union T_0 T_2) != (empty_set)) ### Axiom % 2.02/2.24 35. (member T_4 T_2) (-. (member T_4 T_2)) ### Axiom % 2.02/2.24 36. (-. ((member T_4 T_0) \/ (member T_4 T_2))) (member T_4 T_2) ### NotOr 35 % 2.02/2.24 37. (-. (member T_4 (union T_0 T_2))) (member T_4 (union T_0 T_2)) ### Axiom % 2.02/2.24 38. ((member T_4 (union T_0 T_2)) <=> ((member T_4 T_0) \/ (member T_4 T_2))) (-. (member T_4 (union T_0 T_2))) (member T_4 T_2) ### Equiv 36 37 % 2.02/2.24 39. (All D, ((member D (union T_0 T_2)) <=> ((member D T_0) \/ (member D T_2)))) (member T_4 T_2) (-. (member T_4 (union T_0 T_2))) ### All 38 % 2.02/2.24 40. (All C, (All D, ((member D (union T_0 C)) <=> ((member D T_0) \/ (member D C))))) (-. (member T_4 (union T_0 T_2))) (member T_4 T_2) ### All 39 % 2.02/2.24 41. (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) (member T_4 T_2) (-. (member T_4 (union T_0 T_2))) ### All 40 % 2.02/2.24 42. (-. (member T_4 (empty_set))) (member T_4 (empty_set)) ### Axiom % 2.02/2.24 43. ((member T_4 (union T_0 T_2)) => (member T_4 (empty_set))) (-. (member T_4 (empty_set))) (member T_4 T_2) (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) ### Imply 41 42 % 2.02/2.24 44. (All D, ((member D (union T_0 T_2)) => (member D (empty_set)))) (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) (member T_4 T_2) (-. (member T_4 (empty_set))) ### All 43 % 2.02/2.24 45. (subset (union T_0 T_2) (empty_set)) (-. (member T_4 (empty_set))) (member T_4 T_2) (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) ### Definition-Pseudo(subset) 44 % 2.02/2.24 46. ((subset (union T_0 T_2) (empty_set)) /\ (subset (empty_set) (union T_0 T_2))) (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) (member T_4 T_2) (-. (member T_4 (empty_set))) ### And 45 % 2.02/2.24 47. (((union T_0 T_2) = (empty_set)) <=> ((subset (union T_0 T_2) (empty_set)) /\ (subset (empty_set) (union T_0 T_2)))) (-. (member T_4 (empty_set))) (member T_4 T_2) (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) ((union T_0 T_2) = (empty_set)) ### Equiv 34 46 % 2.02/2.24 48. (All C, (((union T_0 T_2) = C) <=> ((subset (union T_0 T_2) C) /\ (subset C (union T_0 T_2))))) ((union T_0 T_2) = (empty_set)) (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) (member T_4 T_2) (-. (member T_4 (empty_set))) ### All 47 % 2.02/2.24 49. (All B, (All C, ((B = C) <=> ((subset B C) /\ (subset C B))))) (-. (member T_4 (empty_set))) (member T_4 T_2) (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) ((union T_0 T_2) = (empty_set)) ### All 48 % 2.02/2.25 50. (-. ((member T_4 T_2) => (member T_4 (empty_set)))) ((union T_0 T_2) = (empty_set)) (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) (All B, (All C, ((B = C) <=> ((subset B C) /\ (subset C B))))) ### NotImply 49 % 2.02/2.25 51. (-. (All D, ((member D T_2) => (member D (empty_set))))) (All B, (All C, ((B = C) <=> ((subset B C) /\ (subset C B))))) (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) ((union T_0 T_2) = (empty_set)) ### NotAllEx 50 % 2.02/2.25 52. (-. (subset T_2 (empty_set))) ((union T_0 T_2) = (empty_set)) (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) (All B, (All C, ((B = C) <=> ((subset B C) /\ (subset C B))))) ### Definition-Pseudo(subset) 51 % 2.02/2.25 53. (-. ((subset (empty_set) T_2) /\ (subset T_2 (empty_set)))) (All B, (All C, ((B = C) <=> ((subset B C) /\ (subset C B))))) (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) ((union T_0 T_2) = (empty_set)) (All B, (-. (member B (empty_set)))) ### NotAnd 33 52 % 2.02/2.25 54. ((empty_set) != T_2) ((empty_set) = T_2) ### Axiom % 2.02/2.25 55. (((empty_set) = T_2) <=> ((subset (empty_set) T_2) /\ (subset T_2 (empty_set)))) ((empty_set) != T_2) (All B, (-. (member B (empty_set)))) ((union T_0 T_2) = (empty_set)) (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) (All B, (All C, ((B = C) <=> ((subset B C) /\ (subset C B))))) ### Equiv 53 54 % 2.02/2.25 56. (All C, (((empty_set) = C) <=> ((subset (empty_set) C) /\ (subset C (empty_set))))) (All B, (All C, ((B = C) <=> ((subset B C) /\ (subset C B))))) (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) ((union T_0 T_2) = (empty_set)) (All B, (-. (member B (empty_set)))) ((empty_set) != T_2) ### All 55 % 2.02/2.25 57. ((union T_0 T_2) = (empty_set)) ((empty_set) != (union T_0 T_2)) ### Sym(=) % 2.02/2.25 58. (T_5 != T_5) ### Refl(=) % 2.02/2.25 59. (T_0 != T_0) ### Refl(=) % 2.02/2.25 60. ((empty_set) = T_2) ((empty_set) != T_2) ### Axiom % 2.02/2.25 61. ((union T_0 (empty_set)) != (union T_0 T_2)) ((empty_set) = T_2) ### NotEqual 59 60 % 2.02/2.25 62. (-. (member T_5 (union T_0 T_2))) (member T_5 (union T_0 (empty_set))) ((empty_set) = T_2) ### P-NotP 58 61 % 2.02/2.25 63. (-. (member T_5 (empty_set))) (member T_5 (empty_set)) ### Axiom % 2.02/2.25 64. ((member T_5 (union T_0 T_2)) => (member T_5 (empty_set))) (-. (member T_5 (empty_set))) ((empty_set) = T_2) (member T_5 (union T_0 (empty_set))) ### Imply 62 63 % 2.02/2.25 65. (All D, ((member D (union T_0 T_2)) => (member D (empty_set)))) (member T_5 (union T_0 (empty_set))) ((empty_set) = T_2) (-. (member T_5 (empty_set))) ### All 64 % 2.02/2.25 66. (-. ((member T_5 (union T_0 (empty_set))) => (member T_5 (empty_set)))) ((empty_set) = T_2) (All D, ((member D (union T_0 T_2)) => (member D (empty_set)))) ### NotImply 65 % 2.02/2.25 67. (-. (All D, ((member D (union T_0 (empty_set))) => (member D (empty_set))))) (All D, ((member D (union T_0 T_2)) => (member D (empty_set)))) ((empty_set) = T_2) ### NotAllEx 66 % 2.02/2.25 68. (-. (subset (union T_0 (empty_set)) (empty_set))) ((empty_set) = T_2) (All D, ((member D (union T_0 T_2)) => (member D (empty_set)))) ### Definition-Pseudo(subset) 67 % 2.02/2.25 69. (member T_6 (empty_set)) (-. (member T_6 (empty_set))) ### Axiom % 2.02/2.25 70. (All B, (-. (member B (empty_set)))) (member T_6 (empty_set)) ### All 69 % 2.02/2.25 71. (-. ((member T_6 (empty_set)) => (member T_6 (union T_0 (empty_set))))) (All B, (-. (member B (empty_set)))) ### NotImply 70 % 2.02/2.25 72. (-. (All D, ((member D (empty_set)) => (member D (union T_0 (empty_set)))))) (All B, (-. (member B (empty_set)))) ### NotAllEx 71 % 2.02/2.25 73. (-. (subset (empty_set) (union T_0 (empty_set)))) (All B, (-. (member B (empty_set)))) ### Definition-Pseudo(subset) 72 % 2.02/2.25 74. (-. ((subset (union T_0 (empty_set)) (empty_set)) /\ (subset (empty_set) (union T_0 (empty_set))))) (All B, (-. (member B (empty_set)))) (All D, ((member D (union T_0 T_2)) => (member D (empty_set)))) ((empty_set) = T_2) ### NotAnd 68 73 % 2.02/2.25 75. ((union T_0 (empty_set)) = (empty_set)) ((union T_0 (empty_set)) != (empty_set)) ### Axiom % 2.02/2.25 76. (member T_7 T_0) (-. (member T_7 T_0)) ### Axiom % 2.02/2.25 77. (-. ((member T_7 T_0) \/ (member T_7 (empty_set)))) (member T_7 T_0) ### NotOr 76 % 2.02/2.25 78. (-. (member T_7 (union T_0 (empty_set)))) (member T_7 (union T_0 (empty_set))) ### Axiom % 2.02/2.25 79. ((member T_7 (union T_0 (empty_set))) <=> ((member T_7 T_0) \/ (member T_7 (empty_set)))) (-. (member T_7 (union T_0 (empty_set)))) (member T_7 T_0) ### Equiv 77 78 % 2.02/2.25 80. (All D, ((member D (union T_0 (empty_set))) <=> ((member D T_0) \/ (member D (empty_set))))) (member T_7 T_0) (-. (member T_7 (union T_0 (empty_set)))) ### All 79 % 2.02/2.25 81. (-. (member T_7 (empty_set))) (member T_7 (empty_set)) ### Axiom % 2.02/2.25 82. ((member T_7 (union T_0 (empty_set))) <=> (member T_7 (empty_set))) (-. (member T_7 (empty_set))) (member T_7 T_0) (All D, ((member D (union T_0 (empty_set))) <=> ((member D T_0) \/ (member D (empty_set))))) ### Equiv 80 81 % 2.02/2.25 83. (All D, ((member D (union T_0 (empty_set))) <=> (member D (empty_set)))) (All D, ((member D (union T_0 (empty_set))) <=> ((member D T_0) \/ (member D (empty_set))))) (member T_7 T_0) (-. (member T_7 (empty_set))) ### All 82 % 2.02/2.25 84. (member T_7 (empty_set)) (-. (member T_7 (empty_set))) ### Axiom % 2.02/2.25 85. (All B, (-. (member B (empty_set)))) (member T_7 (empty_set)) ### All 84 % 2.02/2.25 86. (-. ((member T_7 (empty_set)) <=> (member T_7 T_0))) (All B, (-. (member B (empty_set)))) (All D, ((member D (union T_0 (empty_set))) <=> ((member D T_0) \/ (member D (empty_set))))) (All D, ((member D (union T_0 (empty_set))) <=> (member D (empty_set)))) ### NotEquiv 83 85 % 2.02/2.25 87. (-. (All D, ((member D (empty_set)) <=> (member D T_0)))) (All D, ((member D (union T_0 (empty_set))) <=> (member D (empty_set)))) (All D, ((member D (union T_0 (empty_set))) <=> ((member D T_0) \/ (member D (empty_set))))) (All B, (-. (member B (empty_set)))) ### NotAllEx 86 % 2.02/2.25 88. (T_0 != (empty_set)) ((empty_set) = T_0) ### Sym(=) % 2.02/2.25 89. (((empty_set) = T_0) <=> (All D, ((member D (empty_set)) <=> (member D T_0)))) (T_0 != (empty_set)) (All B, (-. (member B (empty_set)))) (All D, ((member D (union T_0 (empty_set))) <=> ((member D T_0) \/ (member D (empty_set))))) (All D, ((member D (union T_0 (empty_set))) <=> (member D (empty_set)))) ### Equiv 87 88 % 2.02/2.25 90. (All C, (((empty_set) = C) <=> (All D, ((member D (empty_set)) <=> (member D C))))) (All D, ((member D (union T_0 (empty_set))) <=> (member D (empty_set)))) (All D, ((member D (union T_0 (empty_set))) <=> ((member D T_0) \/ (member D (empty_set))))) (All B, (-. (member B (empty_set)))) (T_0 != (empty_set)) ### All 89 % 2.02/2.25 91. (((union T_0 (empty_set)) = (empty_set)) <=> (All D, ((member D (union T_0 (empty_set))) <=> (member D (empty_set))))) (T_0 != (empty_set)) (All B, (-. (member B (empty_set)))) (All D, ((member D (union T_0 (empty_set))) <=> ((member D T_0) \/ (member D (empty_set))))) (All C, (((empty_set) = C) <=> (All D, ((member D (empty_set)) <=> (member D C))))) ((union T_0 (empty_set)) = (empty_set)) ### Equiv 75 90 % 2.02/2.25 92. (All C, (((union T_0 (empty_set)) = C) <=> (All D, ((member D (union T_0 (empty_set))) <=> (member D C))))) ((union T_0 (empty_set)) = (empty_set)) (All C, (((empty_set) = C) <=> (All D, ((member D (empty_set)) <=> (member D C))))) (All D, ((member D (union T_0 (empty_set))) <=> ((member D T_0) \/ (member D (empty_set))))) (All B, (-. (member B (empty_set)))) (T_0 != (empty_set)) ### All 91 % 2.02/2.25 93. (All B, (All C, ((B = C) <=> (All D, ((member D B) <=> (member D C)))))) (T_0 != (empty_set)) (All B, (-. (member B (empty_set)))) (All D, ((member D (union T_0 (empty_set))) <=> ((member D T_0) \/ (member D (empty_set))))) (All C, (((empty_set) = C) <=> (All D, ((member D (empty_set)) <=> (member D C))))) ((union T_0 (empty_set)) = (empty_set)) ### All 92 % 2.02/2.25 94. (((union T_0 (empty_set)) = (empty_set)) <=> ((subset (union T_0 (empty_set)) (empty_set)) /\ (subset (empty_set) (union T_0 (empty_set))))) (All C, (((empty_set) = C) <=> (All D, ((member D (empty_set)) <=> (member D C))))) (All D, ((member D (union T_0 (empty_set))) <=> ((member D T_0) \/ (member D (empty_set))))) (T_0 != (empty_set)) (All B, (All C, ((B = C) <=> (All D, ((member D B) <=> (member D C)))))) ((empty_set) = T_2) (All D, ((member D (union T_0 T_2)) => (member D (empty_set)))) (All B, (-. (member B (empty_set)))) ### Equiv 74 93 % 2.02/2.25 95. (All C, (((union T_0 (empty_set)) = C) <=> ((subset (union T_0 (empty_set)) C) /\ (subset C (union T_0 (empty_set)))))) (All B, (-. (member B (empty_set)))) (All D, ((member D (union T_0 T_2)) => (member D (empty_set)))) ((empty_set) = T_2) (All B, (All C, ((B = C) <=> (All D, ((member D B) <=> (member D C)))))) (T_0 != (empty_set)) (All D, ((member D (union T_0 (empty_set))) <=> ((member D T_0) \/ (member D (empty_set))))) (All C, (((empty_set) = C) <=> (All D, ((member D (empty_set)) <=> (member D C))))) ### All 94 % 2.02/2.25 96. (All B, (All C, ((B = C) <=> ((subset B C) /\ (subset C B))))) (All C, (((empty_set) = C) <=> (All D, ((member D (empty_set)) <=> (member D C))))) (All D, ((member D (union T_0 (empty_set))) <=> ((member D T_0) \/ (member D (empty_set))))) (T_0 != (empty_set)) (All B, (All C, ((B = C) <=> (All D, ((member D B) <=> (member D C)))))) ((empty_set) = T_2) (All D, ((member D (union T_0 T_2)) => (member D (empty_set)))) (All B, (-. (member B (empty_set)))) ### All 95 % 2.02/2.25 97. (All C, (All D, ((member D (union T_0 C)) <=> ((member D T_0) \/ (member D C))))) (All B, (-. (member B (empty_set)))) (All D, ((member D (union T_0 T_2)) => (member D (empty_set)))) ((empty_set) = T_2) (All B, (All C, ((B = C) <=> (All D, ((member D B) <=> (member D C)))))) (T_0 != (empty_set)) (All C, (((empty_set) = C) <=> (All D, ((member D (empty_set)) <=> (member D C))))) (All B, (All C, ((B = C) <=> ((subset B C) /\ (subset C B))))) ### All 96 % 2.02/2.25 98. (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) (All B, (All C, ((B = C) <=> ((subset B C) /\ (subset C B))))) (All C, (((empty_set) = C) <=> (All D, ((member D (empty_set)) <=> (member D C))))) (T_0 != (empty_set)) (All B, (All C, ((B = C) <=> (All D, ((member D B) <=> (member D C)))))) ((empty_set) = T_2) (All D, ((member D (union T_0 T_2)) => (member D (empty_set)))) (All B, (-. (member B (empty_set)))) ### All 97 % 2.02/2.25 99. (subset (union T_0 T_2) (empty_set)) (All B, (-. (member B (empty_set)))) ((empty_set) = T_2) (All B, (All C, ((B = C) <=> (All D, ((member D B) <=> (member D C)))))) (T_0 != (empty_set)) (All C, (((empty_set) = C) <=> (All D, ((member D (empty_set)) <=> (member D C))))) (All B, (All C, ((B = C) <=> ((subset B C) /\ (subset C B))))) (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) ### Definition-Pseudo(subset) 98 % 2.02/2.25 100. ((subset (empty_set) (union T_0 T_2)) /\ (subset (union T_0 T_2) (empty_set))) (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) (All B, (All C, ((B = C) <=> ((subset B C) /\ (subset C B))))) (All C, (((empty_set) = C) <=> (All D, ((member D (empty_set)) <=> (member D C))))) (T_0 != (empty_set)) (All B, (All C, ((B = C) <=> (All D, ((member D B) <=> (member D C)))))) ((empty_set) = T_2) (All B, (-. (member B (empty_set)))) ### And 99 % 2.02/2.25 101. (((empty_set) = (union T_0 T_2)) <=> ((subset (empty_set) (union T_0 T_2)) /\ (subset (union T_0 T_2) (empty_set)))) (All B, (-. (member B (empty_set)))) ((empty_set) = T_2) (All B, (All C, ((B = C) <=> (All D, ((member D B) <=> (member D C)))))) (T_0 != (empty_set)) (All C, (((empty_set) = C) <=> (All D, ((member D (empty_set)) <=> (member D C))))) (All B, (All C, ((B = C) <=> ((subset B C) /\ (subset C B))))) (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) ((union T_0 T_2) = (empty_set)) ### Equiv 57 100 % 2.02/2.25 102. (All C, (((empty_set) = C) <=> ((subset (empty_set) C) /\ (subset C (empty_set))))) ((union T_0 T_2) = (empty_set)) (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) (All B, (All C, ((B = C) <=> ((subset B C) /\ (subset C B))))) (All C, (((empty_set) = C) <=> (All D, ((member D (empty_set)) <=> (member D C))))) (T_0 != (empty_set)) (All B, (All C, ((B = C) <=> (All D, ((member D B) <=> (member D C)))))) ((empty_set) = T_2) (All B, (-. (member B (empty_set)))) ### All 101 % 2.02/2.25 103. (((empty_set) = T_2) <=> (All D, ((member D (empty_set)) <=> (member D T_2)))) (All B, (All C, ((B = C) <=> (All D, ((member D B) <=> (member D C)))))) (T_0 != (empty_set)) (All C, (((empty_set) = C) <=> (All D, ((member D (empty_set)) <=> (member D C))))) (All B, (-. (member B (empty_set)))) ((union T_0 T_2) = (empty_set)) (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) (All B, (All C, ((B = C) <=> ((subset B C) /\ (subset C B))))) (All C, (((empty_set) = C) <=> ((subset (empty_set) C) /\ (subset C (empty_set))))) ### Equiv 56 102 % 2.02/2.25 104. (All C, (((empty_set) = C) <=> ((subset (empty_set) C) /\ (subset C (empty_set))))) (All B, (All C, ((B = C) <=> ((subset B C) /\ (subset C B))))) (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) ((union T_0 T_2) = (empty_set)) (All B, (-. (member B (empty_set)))) (All C, (((empty_set) = C) <=> (All D, ((member D (empty_set)) <=> (member D C))))) (T_0 != (empty_set)) (All B, (All C, ((B = C) <=> (All D, ((member D B) <=> (member D C)))))) ### All 103 % 2.02/2.25 105. (All B, (All C, ((B = C) <=> (All D, ((member D B) <=> (member D C)))))) (T_0 != (empty_set)) (All C, (((empty_set) = C) <=> (All D, ((member D (empty_set)) <=> (member D C))))) (All B, (-. (member B (empty_set)))) ((union T_0 T_2) = (empty_set)) (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) (All B, (All C, ((B = C) <=> ((subset B C) /\ (subset C B))))) ### All 104 % 2.02/2.25 106. (All B, (All C, ((B = C) <=> ((subset B C) /\ (subset C B))))) (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) ((union T_0 T_2) = (empty_set)) (All B, (-. (member B (empty_set)))) (T_0 != (empty_set)) (All B, (All C, ((B = C) <=> (All D, ((member D B) <=> (member D C)))))) ### All 105 % 2.02/2.25 107. (-. ((subset T_2 (empty_set)) /\ (subset (empty_set) T_2))) (All B, (-. (member B (empty_set)))) (All B, (All C, ((B = C) <=> ((subset B C) /\ (subset C B))))) (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) ((union T_0 T_2) = (empty_set)) ### NotAnd 52 33 % 2.02/2.25 108. (T_2 != (empty_set)) (T_2 = (empty_set)) ### Axiom % 2.02/2.25 109. ((T_2 = (empty_set)) <=> ((subset T_2 (empty_set)) /\ (subset (empty_set) T_2))) (T_2 != (empty_set)) ((union T_0 T_2) = (empty_set)) (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) (All B, (All C, ((B = C) <=> ((subset B C) /\ (subset C B))))) (All B, (-. (member B (empty_set)))) ### Equiv 107 108 % 2.02/2.25 110. (All C, ((T_2 = C) <=> ((subset T_2 C) /\ (subset C T_2)))) (All B, (-. (member B (empty_set)))) (All B, (All C, ((B = C) <=> ((subset B C) /\ (subset C B))))) (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) ((union T_0 T_2) = (empty_set)) (T_2 != (empty_set)) ### All 109 % 2.02/2.25 111. (T_2 != (empty_set)) ((union T_0 T_2) = (empty_set)) (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) (All B, (All C, ((B = C) <=> ((subset B C) /\ (subset C B))))) (All B, (-. (member B (empty_set)))) ### All 110 % 2.02/2.25 112. (-. ((T_0 = (empty_set)) /\ (T_2 = (empty_set)))) (All B, (All C, ((B = C) <=> (All D, ((member D B) <=> (member D C)))))) (All B, (-. (member B (empty_set)))) ((union T_0 T_2) = (empty_set)) (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) (All B, (All C, ((B = C) <=> ((subset B C) /\ (subset C B))))) ### NotAnd 106 111 % 2.02/2.25 113. (-. (((union T_0 T_2) = (empty_set)) <=> ((T_0 = (empty_set)) /\ (T_2 = (empty_set))))) (All B, (All C, ((B = C) <=> ((subset B C) /\ (subset C B))))) (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) (All B, (-. (member B (empty_set)))) (All B, (All C, ((B = C) <=> (All D, ((member D B) <=> (member D C)))))) ### NotEquiv 28 112 % 2.02/2.25 114. (-. (All C, (((union T_0 C) = (empty_set)) <=> ((T_0 = (empty_set)) /\ (C = (empty_set)))))) (All B, (All C, ((B = C) <=> (All D, ((member D B) <=> (member D C)))))) (All B, (-. (member B (empty_set)))) (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) (All B, (All C, ((B = C) <=> ((subset B C) /\ (subset C B))))) ### NotAllEx 113 % 2.02/2.26 115. (-. (All B, (All C, (((union B C) = (empty_set)) <=> ((B = (empty_set)) /\ (C = (empty_set))))))) (All B, (All C, ((B = C) <=> ((subset B C) /\ (subset C B))))) (All B, (All C, (All D, ((member D (union B C)) <=> ((member D B) \/ (member D C)))))) (All B, (-. (member B (empty_set)))) (All B, (All C, ((B = C) <=> (All D, ((member D B) <=> (member D C)))))) ### NotAllEx 114 % 2.02/2.26 % SZS output end Proof % 2.02/2.26 (* END-PROOF *) %------------------------------------------------------------------------------