%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SET765+4 : 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 : n013.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:50 EDT 2022 % Result : Theorem 1.17s 1.35s % Output : Proof 1.17s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SET765+4 : TPTP v8.1.0. Released v2.2.0. % 0.11/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.13/0.34 % Computer : n013.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Mon Jul 11 00:54:00 EDT 2022 % 0.13/0.34 % CPUTime : % 1.17/1.35 % SZS status Theorem % 1.17/1.35 (* PROOF-FOUND *) % 1.17/1.35 (* BEGIN-PROOF *) % 1.17/1.35 % SZS output start Proof % 1.17/1.35 1. (member T_0 T_1) (-. (member T_0 T_1)) ### Axiom % 1.17/1.35 2. (-. (member T_0 T_2)) (member T_0 T_2) ### Axiom % 1.17/1.35 3. ((member T_0 T_1) => (member T_0 T_2)) (-. (member T_0 T_2)) (member T_0 T_1) ### Imply 1 2 % 1.17/1.35 4. (All X, ((member X T_1) => (member X T_2))) (member T_0 T_1) (-. (member T_0 T_2)) ### All 3 % 1.17/1.35 5. (-. (apply T_3 T_0 T_0)) (apply T_3 T_0 T_0) ### Axiom % 1.17/1.35 6. ((member T_0 T_2) => (apply T_3 T_0 T_0)) (-. (apply T_3 T_0 T_0)) (member T_0 T_1) (All X, ((member X T_1) => (member X T_2))) ### Imply 4 5 % 1.17/1.35 7. (All X, ((member X T_2) => (apply T_3 X X))) (All X, ((member X T_1) => (member X T_2))) (member T_0 T_1) (-. (apply T_3 T_0 T_0)) ### All 6 % 1.17/1.35 8. (-. ((member T_0 T_1) => (apply T_3 T_0 T_0))) (All X, ((member X T_1) => (member X T_2))) (All X, ((member X T_2) => (apply T_3 X X))) ### NotImply 7 % 1.17/1.35 9. (-. (All X, ((member X T_1) => (apply T_3 X X)))) (All X, ((member X T_2) => (apply T_3 X X))) (All X, ((member X T_1) => (member X T_2))) ### NotAllEx 8 % 1.17/1.35 10. (member T_4 T_1) (-. (member T_4 T_1)) ### Axiom % 1.17/1.35 11. (-. (member T_4 T_2)) (member T_4 T_2) ### Axiom % 1.17/1.35 12. ((member T_4 T_1) => (member T_4 T_2)) (-. (member T_4 T_2)) (member T_4 T_1) ### Imply 10 11 % 1.17/1.35 13. (All X, ((member X T_1) => (member X T_2))) (member T_4 T_1) (-. (member T_4 T_2)) ### All 12 % 1.17/1.35 14. (member T_5 T_1) (-. (member T_5 T_1)) ### Axiom % 1.17/1.35 15. (-. (member T_5 T_2)) (member T_5 T_2) ### Axiom % 1.17/1.35 16. ((member T_5 T_1) => (member T_5 T_2)) (-. (member T_5 T_2)) (member T_5 T_1) ### Imply 14 15 % 1.17/1.35 17. (All X, ((member X T_1) => (member X T_2))) (member T_5 T_1) (-. (member T_5 T_2)) ### All 16 % 1.17/1.35 18. (apply T_3 T_4 T_5) (-. (apply T_3 T_4 T_5)) ### Axiom % 1.17/1.35 19. (-. (apply T_3 T_5 T_4)) (apply T_3 T_5 T_4) ### Axiom % 1.17/1.35 20. (((member T_4 T_2) /\ (member T_5 T_2)) => ((apply T_3 T_4 T_5) => (apply T_3 T_5 T_4))) (-. (apply T_3 T_5 T_4)) (apply T_3 T_4 T_5) (member T_5 T_1) (member T_4 T_1) (All X, ((member X T_1) => (member X T_2))) ### DisjTree 13 17 18 19 % 1.17/1.35 21. (All Y, (((member T_4 T_2) /\ (member Y T_2)) => ((apply T_3 T_4 Y) => (apply T_3 Y T_4)))) (All X, ((member X T_1) => (member X T_2))) (member T_4 T_1) (member T_5 T_1) (apply T_3 T_4 T_5) (-. (apply T_3 T_5 T_4)) ### All 20 % 1.17/1.35 22. (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => ((apply T_3 X Y) => (apply T_3 Y X))))) (-. (apply T_3 T_5 T_4)) (apply T_3 T_4 T_5) (member T_5 T_1) (member T_4 T_1) (All X, ((member X T_1) => (member X T_2))) ### All 21 % 1.17/1.35 23. (-. (((member T_4 T_1) /\ (member T_5 T_1)) => ((apply T_3 T_4 T_5) => (apply T_3 T_5 T_4)))) (All X, ((member X T_1) => (member X T_2))) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => ((apply T_3 X Y) => (apply T_3 Y X))))) ### ConjTree 22 % 1.17/1.35 24. (-. (All Y, (((member T_4 T_1) /\ (member Y T_1)) => ((apply T_3 T_4 Y) => (apply T_3 Y T_4))))) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => ((apply T_3 X Y) => (apply T_3 Y X))))) (All X, ((member X T_1) => (member X T_2))) ### NotAllEx 23 % 1.17/1.35 25. (-. (All X, (All Y, (((member X T_1) /\ (member Y T_1)) => ((apply T_3 X Y) => (apply T_3 Y X)))))) (All X, ((member X T_1) => (member X T_2))) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => ((apply T_3 X Y) => (apply T_3 Y X))))) ### NotAllEx 24 % 1.17/1.35 26. (member T_6 T_1) (-. (member T_6 T_1)) ### Axiom % 1.17/1.35 27. (-. (member T_6 T_2)) (member T_6 T_2) ### Axiom % 1.17/1.35 28. ((member T_6 T_1) => (member T_6 T_2)) (-. (member T_6 T_2)) (member T_6 T_1) ### Imply 26 27 % 1.17/1.35 29. (All X, ((member X T_1) => (member X T_2))) (member T_6 T_1) (-. (member T_6 T_2)) ### All 28 % 1.17/1.35 30. (member T_7 T_1) (-. (member T_7 T_1)) ### Axiom % 1.17/1.35 31. (-. (member T_7 T_2)) (member T_7 T_2) ### Axiom % 1.17/1.35 32. ((member T_7 T_1) => (member T_7 T_2)) (-. (member T_7 T_2)) (member T_7 T_1) ### Imply 30 31 % 1.17/1.35 33. (All X, ((member X T_1) => (member X T_2))) (member T_7 T_1) (-. (member T_7 T_2)) ### All 32 % 1.17/1.35 34. (member T_8 T_1) (-. (member T_8 T_1)) ### Axiom % 1.17/1.35 35. (-. (member T_8 T_2)) (member T_8 T_2) ### Axiom % 1.17/1.35 36. ((member T_8 T_1) => (member T_8 T_2)) (-. (member T_8 T_2)) (member T_8 T_1) ### Imply 34 35 % 1.17/1.35 37. (All X, ((member X T_1) => (member X T_2))) (member T_8 T_1) (-. (member T_8 T_2)) ### All 36 % 1.17/1.35 38. (-. ((member T_8 T_2) /\ (member T_8 T_2))) (member T_8 T_1) (All X, ((member X T_1) => (member X T_2))) ### NotAnd 37 37 % 1.17/1.35 39. (member T_8 T_2) (-. (member T_8 T_2)) ### Axiom % 1.17/1.35 40. (member T_6 T_2) (-. (member T_6 T_2)) ### Axiom % 1.17/1.35 41. (member T_7 T_2) (-. (member T_7 T_2)) ### Axiom % 1.17/1.35 42. (apply T_3 T_8 T_6) (-. (apply T_3 T_8 T_6)) ### Axiom % 1.17/1.35 43. (apply T_3 T_6 T_7) (-. (apply T_3 T_6 T_7)) ### Axiom % 1.17/1.35 44. (-. (apply T_3 T_8 T_7)) (apply T_3 T_8 T_7) ### Axiom % 1.17/1.35 45. (((member T_8 T_2) /\ ((member T_6 T_2) /\ (member T_7 T_2))) => (((apply T_3 T_8 T_6) /\ (apply T_3 T_6 T_7)) => (apply T_3 T_8 T_7))) (-. (apply T_3 T_8 T_7)) (apply T_3 T_6 T_7) (apply T_3 T_8 T_6) (member T_7 T_2) (member T_6 T_2) (member T_8 T_2) ### DisjTree 39 40 41 42 43 44 % 1.17/1.35 46. (All Z, (((member T_8 T_2) /\ ((member T_6 T_2) /\ (member Z T_2))) => (((apply T_3 T_8 T_6) /\ (apply T_3 T_6 Z)) => (apply T_3 T_8 Z)))) (member T_8 T_2) (member T_6 T_2) (member T_7 T_2) (apply T_3 T_8 T_6) (apply T_3 T_6 T_7) (-. (apply T_3 T_8 T_7)) ### All 45 % 1.17/1.35 47. ((member T_8 T_2) /\ (member T_8 T_2)) (-. (apply T_3 T_8 T_7)) (apply T_3 T_6 T_7) (apply T_3 T_8 T_6) (member T_7 T_2) (member T_6 T_2) (All Z, (((member T_8 T_2) /\ ((member T_6 T_2) /\ (member Z T_2))) => (((apply T_3 T_8 T_6) /\ (apply T_3 T_6 Z)) => (apply T_3 T_8 Z)))) ### And 46 % 1.17/1.35 48. ((member T_8 (intersection T_2 T_2)) <=> ((member T_8 T_2) /\ (member T_8 T_2))) (All Z, (((member T_8 T_2) /\ ((member T_6 T_2) /\ (member Z T_2))) => (((apply T_3 T_8 T_6) /\ (apply T_3 T_6 Z)) => (apply T_3 T_8 Z)))) (member T_6 T_2) (member T_7 T_2) (apply T_3 T_8 T_6) (apply T_3 T_6 T_7) (-. (apply T_3 T_8 T_7)) (All X, ((member X T_1) => (member X T_2))) (member T_8 T_1) ### Equiv 38 47 % 1.17/1.35 49. (All B, ((member T_8 (intersection T_2 B)) <=> ((member T_8 T_2) /\ (member T_8 B)))) (member T_8 T_1) (All X, ((member X T_1) => (member X T_2))) (-. (apply T_3 T_8 T_7)) (apply T_3 T_6 T_7) (apply T_3 T_8 T_6) (member T_7 T_2) (member T_6 T_2) (All Z, (((member T_8 T_2) /\ ((member T_6 T_2) /\ (member Z T_2))) => (((apply T_3 T_8 T_6) /\ (apply T_3 T_6 Z)) => (apply T_3 T_8 Z)))) ### All 48 % 1.17/1.35 50. (All Y, (All Z, (((member T_8 T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 T_8 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_8 Z))))) (member T_6 T_2) (member T_7 T_2) (apply T_3 T_8 T_6) (apply T_3 T_6 T_7) (-. (apply T_3 T_8 T_7)) (All X, ((member X T_1) => (member X T_2))) (member T_8 T_1) (All B, ((member T_8 (intersection T_2 B)) <=> ((member T_8 T_2) /\ (member T_8 B)))) ### All 49 % 1.17/1.35 51. (All A, (All B, ((member T_8 (intersection A B)) <=> ((member T_8 A) /\ (member T_8 B))))) (member T_8 T_1) (All X, ((member X T_1) => (member X T_2))) (-. (apply T_3 T_8 T_7)) (apply T_3 T_6 T_7) (apply T_3 T_8 T_6) (member T_7 T_2) (member T_6 T_2) (All Y, (All Z, (((member T_8 T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 T_8 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_8 Z))))) ### All 50 % 1.17/1.35 52. (All X, (All A, (All B, ((member X (intersection A B)) <=> ((member X A) /\ (member X B)))))) (All Y, (All Z, (((member T_8 T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 T_8 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_8 Z))))) (member T_6 T_2) (member T_7 T_2) (apply T_3 T_8 T_6) (apply T_3 T_6 T_7) (-. (apply T_3 T_8 T_7)) (All X, ((member X T_1) => (member X T_2))) (member T_8 T_1) ### All 51 % 1.17/1.35 53. (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (member T_8 T_1) (All X, ((member X T_1) => (member X T_2))) (-. (apply T_3 T_8 T_7)) (apply T_3 T_6 T_7) (apply T_3 T_8 T_6) (member T_7 T_2) (member T_6 T_2) (All X, (All A, (All B, ((member X (intersection A B)) <=> ((member X A) /\ (member X B)))))) ### All 52 % 1.17/1.35 54. (-. (-. (member T_7 T_2))) (All X, (All A, (All B, ((member X (intersection A B)) <=> ((member X A) /\ (member X B)))))) (member T_6 T_2) (apply T_3 T_8 T_6) (apply T_3 T_6 T_7) (-. (apply T_3 T_8 T_7)) (All X, ((member X T_1) => (member X T_2))) (member T_8 T_1) (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) ### NotNot 53 % 1.17/1.38 55. (-. ((member T_7 T_2) /\ (-. (member T_7 T_2)))) (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (member T_8 T_1) (-. (apply T_3 T_8 T_7)) (apply T_3 T_6 T_7) (apply T_3 T_8 T_6) (member T_6 T_2) (All X, (All A, (All B, ((member X (intersection A B)) <=> ((member X A) /\ (member X B)))))) (member T_7 T_1) (All X, ((member X T_1) => (member X T_2))) ### NotAnd 33 54 % 1.17/1.38 56. (-. (member T_7 T_2)) (member T_7 T_2) ### Axiom % 1.17/1.38 57. ((member T_7 T_2) /\ (-. (member T_7 T_2))) ### And 56 % 1.17/1.38 58. ((member T_7 (difference T_2 T_2)) <=> ((member T_7 T_2) /\ (-. (member T_7 T_2)))) (All X, ((member X T_1) => (member X T_2))) (member T_7 T_1) (All X, (All A, (All B, ((member X (intersection A B)) <=> ((member X A) /\ (member X B)))))) (member T_6 T_2) (apply T_3 T_8 T_6) (apply T_3 T_6 T_7) (-. (apply T_3 T_8 T_7)) (member T_8 T_1) (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) ### Equiv 55 57 % 1.17/1.38 59. (All E, ((member T_7 (difference E T_2)) <=> ((member T_7 E) /\ (-. (member T_7 T_2))))) (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (member T_8 T_1) (-. (apply T_3 T_8 T_7)) (apply T_3 T_6 T_7) (apply T_3 T_8 T_6) (member T_6 T_2) (All X, (All A, (All B, ((member X (intersection A B)) <=> ((member X A) /\ (member X B)))))) (member T_7 T_1) (All X, ((member X T_1) => (member X T_2))) ### All 58 % 1.17/1.38 60. (All A, (All E, ((member T_7 (difference E A)) <=> ((member T_7 E) /\ (-. (member T_7 A)))))) (All X, ((member X T_1) => (member X T_2))) (member T_7 T_1) (All X, (All A, (All B, ((member X (intersection A B)) <=> ((member X A) /\ (member X B)))))) (member T_6 T_2) (apply T_3 T_8 T_6) (apply T_3 T_6 T_7) (-. (apply T_3 T_8 T_7)) (member T_8 T_1) (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) ### All 59 % 1.17/1.38 61. (-. (-. (member T_6 T_2))) (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (member T_8 T_1) (-. (apply T_3 T_8 T_7)) (apply T_3 T_6 T_7) (apply T_3 T_8 T_6) (All X, (All A, (All B, ((member X (intersection A B)) <=> ((member X A) /\ (member X B)))))) (member T_7 T_1) (All X, ((member X T_1) => (member X T_2))) (All A, (All E, ((member T_7 (difference E A)) <=> ((member T_7 E) /\ (-. (member T_7 A)))))) ### NotNot 60 % 1.17/1.38 62. (-. ((member T_6 T_2) /\ (-. (member T_6 T_2)))) (All A, (All E, ((member T_7 (difference E A)) <=> ((member T_7 E) /\ (-. (member T_7 A)))))) (member T_7 T_1) (All X, (All A, (All B, ((member X (intersection A B)) <=> ((member X A) /\ (member X B)))))) (apply T_3 T_8 T_6) (apply T_3 T_6 T_7) (-. (apply T_3 T_8 T_7)) (member T_8 T_1) (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (member T_6 T_1) (All X, ((member X T_1) => (member X T_2))) ### NotAnd 29 61 % 1.17/1.38 63. (-. (member T_6 T_2)) (member T_6 T_2) ### Axiom % 1.17/1.38 64. ((member T_6 T_2) /\ (-. (member T_6 T_2))) ### And 63 % 1.17/1.38 65. ((member T_6 (difference T_2 T_2)) <=> ((member T_6 T_2) /\ (-. (member T_6 T_2)))) (All X, ((member X T_1) => (member X T_2))) (member T_6 T_1) (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (member T_8 T_1) (-. (apply T_3 T_8 T_7)) (apply T_3 T_6 T_7) (apply T_3 T_8 T_6) (All X, (All A, (All B, ((member X (intersection A B)) <=> ((member X A) /\ (member X B)))))) (member T_7 T_1) (All A, (All E, ((member T_7 (difference E A)) <=> ((member T_7 E) /\ (-. (member T_7 A)))))) ### Equiv 62 64 % 1.17/1.38 66. (All E, ((member T_6 (difference E T_2)) <=> ((member T_6 E) /\ (-. (member T_6 T_2))))) (All A, (All E, ((member T_7 (difference E A)) <=> ((member T_7 E) /\ (-. (member T_7 A)))))) (member T_7 T_1) (All X, (All A, (All B, ((member X (intersection A B)) <=> ((member X A) /\ (member X B)))))) (apply T_3 T_8 T_6) (apply T_3 T_6 T_7) (-. (apply T_3 T_8 T_7)) (member T_8 T_1) (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (member T_6 T_1) (All X, ((member X T_1) => (member X T_2))) ### All 65 % 1.17/1.38 67. (All A, (All E, ((member T_6 (difference E A)) <=> ((member T_6 E) /\ (-. (member T_6 A)))))) (All X, ((member X T_1) => (member X T_2))) (member T_6 T_1) (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (member T_8 T_1) (-. (apply T_3 T_8 T_7)) (apply T_3 T_6 T_7) (apply T_3 T_8 T_6) (All X, (All A, (All B, ((member X (intersection A B)) <=> ((member X A) /\ (member X B)))))) (member T_7 T_1) (All A, (All E, ((member T_7 (difference E A)) <=> ((member T_7 E) /\ (-. (member T_7 A)))))) ### All 66 % 1.17/1.38 68. (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) (member T_7 T_1) (All X, (All A, (All B, ((member X (intersection A B)) <=> ((member X A) /\ (member X B)))))) (apply T_3 T_8 T_6) (apply T_3 T_6 T_7) (-. (apply T_3 T_8 T_7)) (member T_8 T_1) (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (member T_6 T_1) (All X, ((member X T_1) => (member X T_2))) (All A, (All E, ((member T_6 (difference E A)) <=> ((member T_6 E) /\ (-. (member T_6 A)))))) ### All 67 % 1.17/1.38 69. (All X, ((member X T_1) => (member X T_2))) (member T_6 T_1) (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (member T_8 T_1) (-. (apply T_3 T_8 T_7)) (apply T_3 T_6 T_7) (apply T_3 T_8 T_6) (All X, (All A, (All B, ((member X (intersection A B)) <=> ((member X A) /\ (member X B)))))) (member T_7 T_1) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) ### All 68 % 1.17/1.38 70. (-. (((member T_8 T_1) /\ ((member T_6 T_1) /\ (member T_7 T_1))) => (((apply T_3 T_8 T_6) /\ (apply T_3 T_6 T_7)) => (apply T_3 T_8 T_7)))) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) (All X, (All A, (All B, ((member X (intersection A B)) <=> ((member X A) /\ (member X B)))))) (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (All X, ((member X T_1) => (member X T_2))) ### ConjTree 69 % 1.17/1.38 71. (-. (All Z, (((member T_8 T_1) /\ ((member T_6 T_1) /\ (member Z T_1))) => (((apply T_3 T_8 T_6) /\ (apply T_3 T_6 Z)) => (apply T_3 T_8 Z))))) (All X, ((member X T_1) => (member X T_2))) (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (All X, (All A, (All B, ((member X (intersection A B)) <=> ((member X A) /\ (member X B)))))) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) ### NotAllEx 70 % 1.17/1.38 72. (-. (All Y, (All Z, (((member T_8 T_1) /\ ((member Y T_1) /\ (member Z T_1))) => (((apply T_3 T_8 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_8 Z)))))) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) (All X, (All A, (All B, ((member X (intersection A B)) <=> ((member X A) /\ (member X B)))))) (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (All X, ((member X T_1) => (member X T_2))) ### NotAllEx 71 % 1.17/1.38 73. (-. (All X, (All Y, (All Z, (((member X T_1) /\ ((member Y T_1) /\ (member Z T_1))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z))))))) (All X, ((member X T_1) => (member X T_2))) (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (All X, (All A, (All B, ((member X (intersection A B)) <=> ((member X A) /\ (member X B)))))) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) ### NotAllEx 72 % 1.17/1.39 74. (-. ((All X, ((member X T_1) => (apply T_3 X X))) /\ ((All X, (All Y, (((member X T_1) /\ (member Y T_1)) => ((apply T_3 X Y) => (apply T_3 Y X))))) /\ (All X, (All Y, (All Z, (((member X T_1) /\ ((member Y T_1) /\ (member Z T_1))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z))))))))) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) (All X, (All A, (All B, ((member X (intersection A B)) <=> ((member X A) /\ (member X B)))))) (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => ((apply T_3 X Y) => (apply T_3 Y X))))) (All X, ((member X T_1) => (member X T_2))) (All X, ((member X T_2) => (apply T_3 X X))) ### DisjTree 9 25 73 % 1.17/1.39 75. (-. (equivalence T_3 T_1)) (All X, ((member X T_2) => (apply T_3 X X))) (All X, ((member X T_1) => (member X T_2))) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => ((apply T_3 X Y) => (apply T_3 Y X))))) (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (All X, (All A, (All B, ((member X (intersection A B)) <=> ((member X A) /\ (member X B)))))) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) ### Definition-Pseudo(equivalence) 74 % 1.17/1.39 76. (subset T_1 T_2) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) (All X, (All A, (All B, ((member X (intersection A B)) <=> ((member X A) /\ (member X B)))))) (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => ((apply T_3 X Y) => (apply T_3 Y X))))) (All X, ((member X T_2) => (apply T_3 X X))) (-. (equivalence T_3 T_1)) ### Definition-Pseudo(subset) 75 % 1.17/1.39 77. ((All X, ((member X T_2) => (apply T_3 X X))) /\ ((All X, (All Y, (((member X T_2) /\ (member Y T_2)) => ((apply T_3 X Y) => (apply T_3 Y X))))) /\ (All X, (All Y, (All Z, (((member X T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 X Y) /\ (apply T_3 Y Z)) => (apply T_3 X Z)))))))) (-. (equivalence T_3 T_1)) (All X, (All A, (All B, ((member X (intersection A B)) <=> ((member X A) /\ (member X B)))))) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) (subset T_1 T_2) ### ConjTree 76 % 1.17/1.39 78. (equivalence T_3 T_2) (subset T_1 T_2) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) (All X, (All A, (All B, ((member X (intersection A B)) <=> ((member X A) /\ (member X B)))))) (-. (equivalence T_3 T_1)) ### Definition-Pseudo(equivalence) 77 % 1.17/1.39 79. (-. (((equivalence T_3 T_2) /\ (subset T_1 T_2)) => (equivalence T_3 T_1))) (All X, (All A, (All B, ((member X (intersection A B)) <=> ((member X A) /\ (member X B)))))) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) ### ConjTree 78 % 1.17/1.39 80. (-. (All X, (((equivalence T_3 T_2) /\ (subset X T_2)) => (equivalence T_3 X)))) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) (All X, (All A, (All B, ((member X (intersection A B)) <=> ((member X A) /\ (member X B)))))) ### NotAllEx 79 % 1.17/1.39 81. (-. (All R, (All X, (((equivalence R T_2) /\ (subset X T_2)) => (equivalence R X))))) (All X, (All A, (All B, ((member X (intersection A B)) <=> ((member X A) /\ (member X B)))))) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) ### NotAllEx 80 % 1.17/1.39 82. (-. (All E, (All R, (All X, (((equivalence R E) /\ (subset X E)) => (equivalence R X)))))) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) (All X, (All A, (All B, ((member X (intersection A B)) <=> ((member X A) /\ (member X B)))))) ### NotAllEx 81 % 1.17/1.39 % SZS output end Proof % 1.17/1.39 (* END-PROOF *) %------------------------------------------------------------------------------