%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SET805+4 : TPTP v8.1.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n010.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:44:05 EDT 2022 % Result : Theorem 0.78s 0.96s % Output : Proof 0.78s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : SET805+4 : TPTP v8.1.0. Released v3.2.0. % 0.12/0.14 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.14/0.35 % Computer : n010.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 600 % 0.14/0.35 % DateTime : Sat Jul 9 23:34:45 EDT 2022 % 0.14/0.35 % CPUTime : % 0.78/0.96 % SZS status Theorem % 0.78/0.96 (* PROOF-FOUND *) % 0.78/0.96 (* BEGIN-PROOF *) % 0.78/0.96 % SZS output start Proof % 0.78/0.96 1. (member T_0 T_1) (-. (member T_0 T_1)) ### Axiom % 0.78/0.96 2. (-. (member T_0 T_2)) (member T_0 T_2) ### Axiom % 0.78/0.96 3. ((member T_0 T_1) => (member T_0 T_2)) (-. (member T_0 T_2)) (member T_0 T_1) ### Imply 1 2 % 0.78/0.96 4. (All X, ((member X T_1) => (member X T_2))) (member T_0 T_1) (-. (member T_0 T_2)) ### All 3 % 0.78/0.96 5. (-. (apply T_3 T_0 T_0)) (apply T_3 T_0 T_0) ### Axiom % 0.78/0.96 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 % 0.78/0.96 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 % 0.78/0.96 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 % 0.78/0.96 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 % 0.78/0.96 10. (member T_4 T_1) (-. (member T_4 T_1)) ### Axiom % 0.78/0.96 11. (-. (member T_4 T_2)) (member T_4 T_2) ### Axiom % 0.78/0.96 12. ((member T_4 T_1) => (member T_4 T_2)) (-. (member T_4 T_2)) (member T_4 T_1) ### Imply 10 11 % 0.78/0.96 13. (All X, ((member X T_1) => (member X T_2))) (member T_4 T_1) (-. (member T_4 T_2)) ### All 12 % 0.78/0.96 14. (member T_5 T_1) (-. (member T_5 T_1)) ### Axiom % 0.78/0.96 15. (member T_5 T_2) (-. (member T_5 T_2)) ### Axiom % 0.78/0.96 16. (member T_4 T_2) (-. (member T_4 T_2)) ### Axiom % 0.78/0.96 17. (apply T_3 T_5 T_4) (-. (apply T_3 T_5 T_4)) ### Axiom % 0.78/0.96 18. (apply T_3 T_4 T_5) (-. (apply T_3 T_4 T_5)) ### Axiom % 0.78/0.96 19. (T_4 != T_5) (T_5 = T_4) ### Sym(=) % 0.78/0.96 20. (((member T_5 T_2) /\ (member T_4 T_2)) => (((apply T_3 T_5 T_4) /\ (apply T_3 T_4 T_5)) => (T_5 = T_4))) (T_4 != T_5) (apply T_3 T_4 T_5) (apply T_3 T_5 T_4) (member T_4 T_2) (member T_5 T_2) ### DisjTree 15 16 17 18 19 % 0.78/0.96 21. (All Y, (((member T_5 T_2) /\ (member Y T_2)) => (((apply T_3 T_5 Y) /\ (apply T_3 Y T_5)) => (T_5 = Y)))) (member T_5 T_2) (member T_4 T_2) (apply T_3 T_5 T_4) (apply T_3 T_4 T_5) (T_4 != T_5) ### All 20 % 0.78/0.96 22. (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => (((apply T_3 X Y) /\ (apply T_3 Y X)) => (X = Y))))) (T_4 != T_5) (apply T_3 T_4 T_5) (apply T_3 T_5 T_4) (member T_4 T_2) (member T_5 T_2) ### All 21 % 0.78/0.96 23. (-. (-. (member T_5 T_2))) (member T_4 T_2) (apply T_3 T_5 T_4) (apply T_3 T_4 T_5) (T_4 != T_5) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => (((apply T_3 X Y) /\ (apply T_3 Y X)) => (X = Y))))) ### NotNot 22 % 0.78/0.96 24. (-. ((member T_5 T_1) /\ (-. (member T_5 T_2)))) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => (((apply T_3 X Y) /\ (apply T_3 Y X)) => (X = Y))))) (T_4 != T_5) (apply T_3 T_4 T_5) (apply T_3 T_5 T_4) (member T_4 T_2) (member T_5 T_1) ### NotAnd 14 23 % 0.78/0.96 25. (member T_5 T_1) (-. (member T_5 T_1)) ### Axiom % 0.78/0.96 26. (-. (member T_5 T_2)) (member T_5 T_2) ### Axiom % 0.78/0.96 27. ((member T_5 T_1) => (member T_5 T_2)) (-. (member T_5 T_2)) (member T_5 T_1) ### Imply 25 26 % 0.78/0.96 28. (All X, ((member X T_1) => (member X T_2))) (member T_5 T_1) (-. (member T_5 T_2)) ### All 27 % 0.78/0.96 29. ((member T_5 T_1) /\ (-. (member T_5 T_2))) (member T_5 T_1) (All X, ((member X T_1) => (member X T_2))) ### And 28 % 0.78/0.96 30. ((member T_5 (difference T_1 T_2)) <=> ((member T_5 T_1) /\ (-. (member T_5 T_2)))) (All X, ((member X T_1) => (member X T_2))) (member T_5 T_1) (member T_4 T_2) (apply T_3 T_5 T_4) (apply T_3 T_4 T_5) (T_4 != T_5) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => (((apply T_3 X Y) /\ (apply T_3 Y X)) => (X = Y))))) ### Equiv 24 29 % 0.78/0.96 31. (All E, ((member T_5 (difference E T_2)) <=> ((member T_5 E) /\ (-. (member T_5 T_2))))) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => (((apply T_3 X Y) /\ (apply T_3 Y X)) => (X = Y))))) (T_4 != T_5) (apply T_3 T_4 T_5) (apply T_3 T_5 T_4) (member T_4 T_2) (member T_5 T_1) (All X, ((member X T_1) => (member X T_2))) ### All 30 % 0.78/0.96 32. (All A, (All E, ((member T_5 (difference E A)) <=> ((member T_5 E) /\ (-. (member T_5 A)))))) (All X, ((member X T_1) => (member X T_2))) (member T_5 T_1) (member T_4 T_2) (apply T_3 T_5 T_4) (apply T_3 T_4 T_5) (T_4 != T_5) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => (((apply T_3 X Y) /\ (apply T_3 Y X)) => (X = Y))))) ### All 31 % 0.78/0.96 33. (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => (((apply T_3 X Y) /\ (apply T_3 Y X)) => (X = Y))))) (T_4 != T_5) (apply T_3 T_4 T_5) (apply T_3 T_5 T_4) (member T_4 T_2) (member T_5 T_1) (All X, ((member X T_1) => (member X T_2))) ### All 32 % 0.78/0.96 34. (-. (-. (member T_4 T_2))) (All X, ((member X T_1) => (member X T_2))) (member T_5 T_1) (apply T_3 T_5 T_4) (apply T_3 T_4 T_5) (T_4 != T_5) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => (((apply T_3 X Y) /\ (apply T_3 Y X)) => (X = Y))))) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) ### NotNot 33 % 0.78/0.96 35. (-. ((member T_4 T_2) /\ (-. (member T_4 T_2)))) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => (((apply T_3 X Y) /\ (apply T_3 Y X)) => (X = Y))))) (T_4 != T_5) (apply T_3 T_4 T_5) (apply T_3 T_5 T_4) (member T_5 T_1) (member T_4 T_1) (All X, ((member X T_1) => (member X T_2))) ### NotAnd 13 34 % 0.78/0.96 36. (-. (member T_4 T_2)) (member T_4 T_2) ### Axiom % 0.78/0.96 37. ((member T_4 T_2) /\ (-. (member T_4 T_2))) ### And 36 % 0.78/0.96 38. ((member T_4 (difference T_2 T_2)) <=> ((member T_4 T_2) /\ (-. (member T_4 T_2)))) (All X, ((member X T_1) => (member X T_2))) (member T_4 T_1) (member T_5 T_1) (apply T_3 T_5 T_4) (apply T_3 T_4 T_5) (T_4 != T_5) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => (((apply T_3 X Y) /\ (apply T_3 Y X)) => (X = Y))))) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) ### Equiv 35 37 % 0.78/0.96 39. (All E, ((member T_4 (difference E T_2)) <=> ((member T_4 E) /\ (-. (member T_4 T_2))))) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => (((apply T_3 X Y) /\ (apply T_3 Y X)) => (X = Y))))) (T_4 != T_5) (apply T_3 T_4 T_5) (apply T_3 T_5 T_4) (member T_5 T_1) (member T_4 T_1) (All X, ((member X T_1) => (member X T_2))) ### All 38 % 0.78/0.96 40. (All A, (All E, ((member T_4 (difference E A)) <=> ((member T_4 E) /\ (-. (member T_4 A)))))) (All X, ((member X T_1) => (member X T_2))) (member T_4 T_1) (member T_5 T_1) (apply T_3 T_5 T_4) (apply T_3 T_4 T_5) (T_4 != T_5) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => (((apply T_3 X Y) /\ (apply T_3 Y X)) => (X = Y))))) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) ### All 39 % 0.78/0.96 41. (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => (((apply T_3 X Y) /\ (apply T_3 Y X)) => (X = Y))))) (T_4 != T_5) (apply T_3 T_4 T_5) (apply T_3 T_5 T_4) (member T_5 T_1) (member T_4 T_1) (All X, ((member X T_1) => (member X T_2))) ### All 40 % 0.78/0.96 42. (-. (((member T_4 T_1) /\ (member T_5 T_1)) => (((apply T_3 T_4 T_5) /\ (apply T_3 T_5 T_4)) => (T_4 = T_5)))) (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)) => (X = Y))))) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) ### ConjTree 41 % 0.78/0.96 43. (-. (All Y, (((member T_4 T_1) /\ (member Y T_1)) => (((apply T_3 T_4 Y) /\ (apply T_3 Y T_4)) => (T_4 = Y))))) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => (((apply T_3 X Y) /\ (apply T_3 Y X)) => (X = Y))))) (All X, ((member X T_1) => (member X T_2))) ### NotAllEx 42 % 0.78/0.96 44. (-. (All X, (All Y, (((member X T_1) /\ (member Y T_1)) => (((apply T_3 X Y) /\ (apply T_3 Y X)) => (X = Y)))))) (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)) => (X = Y))))) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) ### NotAllEx 43 % 0.78/0.98 45. (member T_6 T_1) (-. (member T_6 T_1)) ### Axiom % 0.78/0.98 46. (-. (member T_6 T_2)) (member T_6 T_2) ### Axiom % 0.78/0.98 47. ((member T_6 T_1) => (member T_6 T_2)) (-. (member T_6 T_2)) (member T_6 T_1) ### Imply 45 46 % 0.78/0.98 48. (All X, ((member X T_1) => (member X T_2))) (member T_6 T_1) (-. (member T_6 T_2)) ### All 47 % 0.78/0.98 49. (member T_7 T_1) (-. (member T_7 T_1)) ### Axiom % 0.78/0.98 50. (-. (member T_7 T_2)) (member T_7 T_2) ### Axiom % 0.78/0.98 51. ((member T_7 T_1) => (member T_7 T_2)) (-. (member T_7 T_2)) (member T_7 T_1) ### Imply 49 50 % 0.78/0.98 52. (All X, ((member X T_1) => (member X T_2))) (member T_7 T_1) (-. (member T_7 T_2)) ### All 51 % 0.78/0.98 53. (member T_7 (empty_set)) (-. (member T_7 (empty_set))) ### Axiom % 0.78/0.98 54. (All X, (-. (member X (empty_set)))) (member T_7 (empty_set)) ### All 53 % 0.78/0.98 55. (-. (-. (member T_7 (empty_set)))) (All X, (-. (member X (empty_set)))) ### NotNot 54 % 0.78/0.98 56. (-. ((member T_7 T_2) /\ (-. (member T_7 (empty_set))))) (All X, (-. (member X (empty_set)))) (member T_7 T_1) (All X, ((member X T_1) => (member X T_2))) ### NotAnd 52 55 % 0.78/0.98 57. (member T_8 T_1) (-. (member T_8 T_1)) ### Axiom % 0.78/0.98 58. (-. (member T_8 T_2)) (member T_8 T_2) ### Axiom % 0.78/0.98 59. ((member T_8 T_1) => (member T_8 T_2)) (-. (member T_8 T_2)) (member T_8 T_1) ### Imply 57 58 % 0.78/0.98 60. (All X, ((member X T_1) => (member X T_2))) (member T_8 T_1) (-. (member T_8 T_2)) ### All 59 % 0.78/0.98 61. (member T_6 T_2) (-. (member T_6 T_2)) ### Axiom % 0.78/0.98 62. (member T_7 T_2) (-. (member T_7 T_2)) ### Axiom % 0.78/0.98 63. (member T_8 T_2) (-. (member T_8 T_2)) ### Axiom % 0.78/0.98 64. (apply T_3 T_6 T_7) (-. (apply T_3 T_6 T_7)) ### Axiom % 0.78/0.98 65. (apply T_3 T_7 T_8) (-. (apply T_3 T_7 T_8)) ### Axiom % 0.78/0.98 66. (-. (apply T_3 T_6 T_8)) (apply T_3 T_6 T_8) ### Axiom % 0.78/0.98 67. (((member T_6 T_2) /\ ((member T_7 T_2) /\ (member T_8 T_2))) => (((apply T_3 T_6 T_7) /\ (apply T_3 T_7 T_8)) => (apply T_3 T_6 T_8))) (-. (apply T_3 T_6 T_8)) (apply T_3 T_7 T_8) (apply T_3 T_6 T_7) (member T_8 T_2) (member T_7 T_2) (member T_6 T_2) ### DisjTree 61 62 63 64 65 66 % 0.78/0.98 68. (All Z, (((member T_6 T_2) /\ ((member T_7 T_2) /\ (member Z T_2))) => (((apply T_3 T_6 T_7) /\ (apply T_3 T_7 Z)) => (apply T_3 T_6 Z)))) (member T_6 T_2) (member T_7 T_2) (member T_8 T_2) (apply T_3 T_6 T_7) (apply T_3 T_7 T_8) (-. (apply T_3 T_6 T_8)) ### All 67 % 0.78/0.98 69. (All Y, (All Z, (((member T_6 T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 T_6 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_6 Z))))) (-. (apply T_3 T_6 T_8)) (apply T_3 T_7 T_8) (apply T_3 T_6 T_7) (member T_8 T_2) (member T_7 T_2) (member T_6 T_2) ### All 68 % 0.78/0.98 70. (-. (-. (member T_8 T_2))) (member T_6 T_2) (member T_7 T_2) (apply T_3 T_6 T_7) (apply T_3 T_7 T_8) (-. (apply T_3 T_6 T_8)) (All Y, (All Z, (((member T_6 T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 T_6 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_6 Z))))) ### NotNot 69 % 0.78/0.98 71. (-. ((member T_8 T_2) /\ (-. (member T_8 T_2)))) (All Y, (All Z, (((member T_6 T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 T_6 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_6 Z))))) (-. (apply T_3 T_6 T_8)) (apply T_3 T_7 T_8) (apply T_3 T_6 T_7) (member T_7 T_2) (member T_6 T_2) (member T_8 T_1) (All X, ((member X T_1) => (member X T_2))) ### NotAnd 60 70 % 0.78/0.98 72. (-. (member T_8 T_2)) (member T_8 T_2) ### Axiom % 0.78/0.98 73. ((member T_8 T_2) /\ (-. (member T_8 T_2))) ### And 72 % 0.78/0.98 74. ((member T_8 (difference T_2 T_2)) <=> ((member T_8 T_2) /\ (-. (member T_8 T_2)))) (All X, ((member X T_1) => (member X T_2))) (member T_8 T_1) (member T_6 T_2) (member T_7 T_2) (apply T_3 T_6 T_7) (apply T_3 T_7 T_8) (-. (apply T_3 T_6 T_8)) (All Y, (All Z, (((member T_6 T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 T_6 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_6 Z))))) ### Equiv 71 73 % 0.78/0.98 75. (All E, ((member T_8 (difference E T_2)) <=> ((member T_8 E) /\ (-. (member T_8 T_2))))) (All Y, (All Z, (((member T_6 T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 T_6 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_6 Z))))) (-. (apply T_3 T_6 T_8)) (apply T_3 T_7 T_8) (apply T_3 T_6 T_7) (member T_7 T_2) (member T_6 T_2) (member T_8 T_1) (All X, ((member X T_1) => (member X T_2))) ### All 74 % 0.78/0.98 76. ((member T_7 T_2) /\ (-. (member T_7 (empty_set)))) (All X, ((member X T_1) => (member X T_2))) (member T_8 T_1) (member T_6 T_2) (apply T_3 T_6 T_7) (apply T_3 T_7 T_8) (-. (apply T_3 T_6 T_8)) (All Y, (All Z, (((member T_6 T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 T_6 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_6 Z))))) (All E, ((member T_8 (difference E T_2)) <=> ((member T_8 E) /\ (-. (member T_8 T_2))))) ### And 75 % 0.78/0.98 77. ((member T_7 (difference T_2 (empty_set))) <=> ((member T_7 T_2) /\ (-. (member T_7 (empty_set))))) (All E, ((member T_8 (difference E T_2)) <=> ((member T_8 E) /\ (-. (member T_8 T_2))))) (All Y, (All Z, (((member T_6 T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 T_6 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_6 Z))))) (-. (apply T_3 T_6 T_8)) (apply T_3 T_7 T_8) (apply T_3 T_6 T_7) (member T_6 T_2) (member T_8 T_1) (All X, ((member X T_1) => (member X T_2))) (member T_7 T_1) (All X, (-. (member X (empty_set)))) ### Equiv 56 76 % 0.78/0.98 78. (All E, ((member T_7 (difference E (empty_set))) <=> ((member T_7 E) /\ (-. (member T_7 (empty_set)))))) (All X, (-. (member X (empty_set)))) (member T_7 T_1) (All X, ((member X T_1) => (member X T_2))) (member T_8 T_1) (member T_6 T_2) (apply T_3 T_6 T_7) (apply T_3 T_7 T_8) (-. (apply T_3 T_6 T_8)) (All Y, (All Z, (((member T_6 T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 T_6 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_6 Z))))) (All E, ((member T_8 (difference E T_2)) <=> ((member T_8 E) /\ (-. (member T_8 T_2))))) ### All 77 % 0.78/0.98 79. (All A, (All E, ((member T_8 (difference E A)) <=> ((member T_8 E) /\ (-. (member T_8 A)))))) (All Y, (All Z, (((member T_6 T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 T_6 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_6 Z))))) (-. (apply T_3 T_6 T_8)) (apply T_3 T_7 T_8) (apply T_3 T_6 T_7) (member T_6 T_2) (member T_8 T_1) (All X, ((member X T_1) => (member X T_2))) (member T_7 T_1) (All X, (-. (member X (empty_set)))) (All E, ((member T_7 (difference E (empty_set))) <=> ((member T_7 E) /\ (-. (member T_7 (empty_set)))))) ### All 78 % 0.78/0.98 80. (All A, (All E, ((member T_7 (difference E A)) <=> ((member T_7 E) /\ (-. (member T_7 A)))))) (All X, (-. (member X (empty_set)))) (member T_7 T_1) (All X, ((member X T_1) => (member X T_2))) (member T_8 T_1) (member T_6 T_2) (apply T_3 T_6 T_7) (apply T_3 T_7 T_8) (-. (apply T_3 T_6 T_8)) (All Y, (All Z, (((member T_6 T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 T_6 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_6 Z))))) (All A, (All E, ((member T_8 (difference E A)) <=> ((member T_8 E) /\ (-. (member T_8 A)))))) ### All 79 % 0.78/0.98 81. (-. (-. (member T_6 T_2))) (All A, (All E, ((member T_8 (difference E A)) <=> ((member T_8 E) /\ (-. (member T_8 A)))))) (All Y, (All Z, (((member T_6 T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 T_6 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_6 Z))))) (-. (apply T_3 T_6 T_8)) (apply T_3 T_7 T_8) (apply T_3 T_6 T_7) (member T_8 T_1) (All X, ((member X T_1) => (member X T_2))) (member T_7 T_1) (All X, (-. (member X (empty_set)))) (All A, (All E, ((member T_7 (difference E A)) <=> ((member T_7 E) /\ (-. (member T_7 A)))))) ### NotNot 80 % 0.78/0.98 82. (-. ((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)))))) (All X, (-. (member X (empty_set)))) (member T_7 T_1) (member T_8 T_1) (apply T_3 T_6 T_7) (apply T_3 T_7 T_8) (-. (apply T_3 T_6 T_8)) (All Y, (All Z, (((member T_6 T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 T_6 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_6 Z))))) (All A, (All E, ((member T_8 (difference E A)) <=> ((member T_8 E) /\ (-. (member T_8 A)))))) (member T_6 T_1) (All X, ((member X T_1) => (member X T_2))) ### NotAnd 48 81 % 0.78/0.98 83. (-. (member T_6 T_2)) (member T_6 T_2) ### Axiom % 0.78/0.98 84. ((member T_6 T_2) /\ (-. (member T_6 T_2))) ### And 83 % 0.78/1.00 85. ((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 A, (All E, ((member T_8 (difference E A)) <=> ((member T_8 E) /\ (-. (member T_8 A)))))) (All Y, (All Z, (((member T_6 T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 T_6 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_6 Z))))) (-. (apply T_3 T_6 T_8)) (apply T_3 T_7 T_8) (apply T_3 T_6 T_7) (member T_8 T_1) (member T_7 T_1) (All X, (-. (member X (empty_set)))) (All A, (All E, ((member T_7 (difference E A)) <=> ((member T_7 E) /\ (-. (member T_7 A)))))) ### Equiv 82 84 % 0.78/1.00 86. (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)))))) (All X, (-. (member X (empty_set)))) (member T_7 T_1) (member T_8 T_1) (apply T_3 T_6 T_7) (apply T_3 T_7 T_8) (-. (apply T_3 T_6 T_8)) (All Y, (All Z, (((member T_6 T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 T_6 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_6 Z))))) (All A, (All E, ((member T_8 (difference E A)) <=> ((member T_8 E) /\ (-. (member T_8 A)))))) (member T_6 T_1) (All X, ((member X T_1) => (member X T_2))) ### All 85 % 0.78/1.00 87. (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 A, (All E, ((member T_8 (difference E A)) <=> ((member T_8 E) /\ (-. (member T_8 A)))))) (All Y, (All Z, (((member T_6 T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 T_6 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_6 Z))))) (-. (apply T_3 T_6 T_8)) (apply T_3 T_7 T_8) (apply T_3 T_6 T_7) (member T_8 T_1) (member T_7 T_1) (All X, (-. (member X (empty_set)))) (All A, (All E, ((member T_7 (difference E A)) <=> ((member T_7 E) /\ (-. (member T_7 A)))))) ### All 86 % 0.78/1.00 88. (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) (All A, (All E, ((member T_7 (difference E A)) <=> ((member T_7 E) /\ (-. (member T_7 A)))))) (All X, (-. (member X (empty_set)))) (member T_7 T_1) (member T_8 T_1) (apply T_3 T_6 T_7) (apply T_3 T_7 T_8) (-. (apply T_3 T_6 T_8)) (All Y, (All Z, (((member T_6 T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 T_6 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_6 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 87 % 0.78/1.00 89. (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 Y, (All Z, (((member T_6 T_2) /\ ((member Y T_2) /\ (member Z T_2))) => (((apply T_3 T_6 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_6 Z))))) (-. (apply T_3 T_6 T_8)) (apply T_3 T_7 T_8) (apply T_3 T_6 T_7) (member T_8 T_1) (member T_7 T_1) (All X, (-. (member X (empty_set)))) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) ### All 88 % 0.78/1.00 90. (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 B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) (All X, (-. (member X (empty_set)))) (member T_7 T_1) (member T_8 T_1) (apply T_3 T_6 T_7) (apply T_3 T_7 T_8) (-. (apply T_3 T_6 T_8)) (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 89 % 0.78/1.00 91. (All X, ((member X T_1) => (member X T_2))) (member T_6 T_1) (-. (apply T_3 T_6 T_8)) (apply T_3 T_7 T_8) (apply T_3 T_6 T_7) (member T_8 T_1) (member T_7 T_1) (All X, (-. (member X (empty_set)))) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) (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 90 % 0.78/1.00 92. (-. (((member T_6 T_1) /\ ((member T_7 T_1) /\ (member T_8 T_1))) => (((apply T_3 T_6 T_7) /\ (apply T_3 T_7 T_8)) => (apply T_3 T_6 T_8)))) (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 B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) (All X, (-. (member X (empty_set)))) (All X, ((member X T_1) => (member X T_2))) ### ConjTree 91 % 0.78/1.00 93. (-. (All Z, (((member T_6 T_1) /\ ((member T_7 T_1) /\ (member Z T_1))) => (((apply T_3 T_6 T_7) /\ (apply T_3 T_7 Z)) => (apply T_3 T_6 Z))))) (All X, ((member X T_1) => (member X T_2))) (All X, (-. (member X (empty_set)))) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) (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)))))) ### NotAllEx 92 % 0.78/1.00 94. (-. (All Y, (All Z, (((member T_6 T_1) /\ ((member Y T_1) /\ (member Z T_1))) => (((apply T_3 T_6 Y) /\ (apply T_3 Y Z)) => (apply T_3 T_6 Z)))))) (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 B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) (All X, (-. (member X (empty_set)))) (All X, ((member X T_1) => (member X T_2))) ### NotAllEx 93 % 0.78/1.00 95. (-. (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, (-. (member X (empty_set)))) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) (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)))))) ### NotAllEx 94 % 0.78/1.00 96. (-. ((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)) => (X = Y))))) /\ (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, (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 (empty_set)))) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => (((apply T_3 X Y) /\ (apply T_3 Y X)) => (X = Y))))) (All X, ((member X T_1) => (member X T_2))) (All X, ((member X T_2) => (apply T_3 X X))) ### DisjTree 9 44 95 % 0.78/1.00 97. (-. (order 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)) => (X = Y))))) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) (All X, (-. (member X (empty_set)))) (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)))))) ### Definition-Pseudo(order) 96 % 0.78/1.00 98. (subset T_1 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, (-. (member X (empty_set)))) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => (((apply T_3 X Y) /\ (apply T_3 Y X)) => (X = Y))))) (All X, ((member X T_2) => (apply T_3 X X))) (-. (order T_3 T_1)) ### Definition-Pseudo(subset) 97 % 0.78/1.00 99. (-. ((subset T_1 T_2) => (order T_3 T_1))) (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)) => (X = Y))))) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) (All X, (-. (member X (empty_set)))) (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)))))) ### NotImply 98 % 0.78/1.00 100. (-. (All X, ((subset X T_2) => (order T_3 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, (-. (member X (empty_set)))) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) (All X, (All Y, (((member X T_2) /\ (member Y T_2)) => (((apply T_3 X Y) /\ (apply T_3 Y X)) => (X = Y))))) (All X, ((member X T_2) => (apply T_3 X X))) ### NotAllEx 99 % 0.78/1.00 101. ((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)) => (X = Y))))) /\ (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 B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) (All X, (-. (member X (empty_set)))) (-. (All X, ((subset X T_2) => (order T_3 X)))) ### ConjTree 100 % 0.78/1.00 102. (order T_3 T_2) (-. (All X, ((subset X T_2) => (order T_3 X)))) (All X, (-. (member X (empty_set)))) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) ### Definition-Pseudo(order) 101 % 0.78/1.00 103. (-. ((order T_3 T_2) => (All X, ((subset X T_2) => (order T_3 X))))) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) (All X, (-. (member X (empty_set)))) ### NotImply 102 % 0.78/1.00 104. (-. (All E, ((order T_3 E) => (All X, ((subset X E) => (order T_3 X)))))) (All X, (-. (member X (empty_set)))) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) ### NotAllEx 103 % 0.78/1.00 105. (-. (All R, (All E, ((order R E) => (All X, ((subset X E) => (order R X))))))) (All B, (All A, (All E, ((member B (difference E A)) <=> ((member B E) /\ (-. (member B A))))))) (All X, (-. (member X (empty_set)))) ### NotAllEx 104 % 0.78/1.00 % SZS output end Proof % 0.78/1.00 (* END-PROOF *) %------------------------------------------------------------------------------