%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SYN917+1 : TPTP v8.1.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n008.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 : Thu Jul 21 12:47:15 EDT 2022 % Result : Theorem 0.21s 0.44s % Output : Proof 0.21s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.14 % Problem : SYN917+1 : TPTP v8.1.0. Released v3.1.0. % 0.04/0.14 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.14/0.36 % Computer : n008.cluster.edu % 0.14/0.36 % Model : x86_64 x86_64 % 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.36 % Memory : 8042.1875MB % 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.36 % CPULimit : 300 % 0.14/0.36 % WCLimit : 600 % 0.14/0.36 % DateTime : Mon Jul 11 16:28:23 EDT 2022 % 0.14/0.36 % CPUTime : % 0.21/0.44 % SZS status Theorem % 0.21/0.44 (* PROOF-FOUND *) % 0.21/0.44 (* BEGIN-PROOF *) % 0.21/0.44 % SZS output start Proof % 0.21/0.44 1. (f zenon_X0) (-. (f zenon_X0)) ### Axiom % 0.21/0.44 2. (g zenon_X0) (-. (g zenon_X0)) ### Axiom % 0.21/0.44 3. (-. (h zenon_X0)) (h zenon_X0) ### Axiom % 0.21/0.44 4. (-. ((f zenon_X0) /\ ((g zenon_X0) /\ (-. (h zenon_X0))))) (-. (h zenon_X0)) (g zenon_X0) (f zenon_X0) ### DisjTree 1 2 3 % 0.21/0.44 5. (-. (Ex V, ((f V) /\ ((g V) /\ (-. (h V)))))) (f zenon_X0) (g zenon_X0) (-. (h zenon_X0)) ### NotExists 4 % 0.21/0.44 6. (-. (((f zenon_X0) /\ (g zenon_X0)) => (h zenon_X0))) (-. (Ex V, ((f V) /\ ((g V) /\ (-. (h V)))))) ### ConjTree 5 % 0.21/0.44 7. (f T_1) (-. (f T_1)) ### Axiom % 0.21/0.44 8. (-. (g T_1)) (g T_1) ### Axiom % 0.21/0.44 9. ((f T_1) => (g T_1)) (-. (g T_1)) (f T_1) ### Imply 7 8 % 0.21/0.44 10. (All W, ((f W) => (g W))) (f T_1) (-. (g T_1)) ### All 9 % 0.21/0.44 11. (f T_1) (-. (f T_1)) ### Axiom % 0.21/0.44 12. (f T_1) (-. (f T_1)) ### Axiom % 0.21/0.44 13. (-. (h T_1)) (h T_1) ### Axiom % 0.21/0.44 14. ((f T_1) => (h T_1)) (-. (h T_1)) (f T_1) ### Imply 12 13 % 0.21/0.44 15. (All Z, ((f Z) => (h Z))) (f T_1) (-. (h T_1)) ### All 14 % 0.21/0.44 16. (-. (g T_1)) (g T_1) ### Axiom % 0.21/0.44 17. (((f T_1) /\ (h T_1)) => (g T_1)) (-. (g T_1)) (All Z, ((f Z) => (h Z))) (f T_1) ### DisjTree 11 15 16 % 0.21/0.44 18. (All R, (((f R) /\ (h R)) => (g R))) (f T_1) (All Z, ((f Z) => (h Z))) (-. (g T_1)) ### All 17 % 0.21/0.44 19. ((All W, ((f W) => (g W))) \/ (All Z, ((f Z) => (h Z)))) (All R, (((f R) /\ (h R)) => (g R))) (-. (g T_1)) (f T_1) ### Or 10 18 % 0.21/0.44 20. ((f T_1) /\ (-. (g T_1))) (All R, (((f R) /\ (h R)) => (g R))) ((All W, ((f W) => (g W))) \/ (All Z, ((f Z) => (h Z)))) ### And 19 % 0.21/0.44 21. (Ex Y, ((f Y) /\ (-. (g Y)))) ((All W, ((f W) => (g W))) \/ (All Z, ((f Z) => (h Z)))) (All R, (((f R) /\ (h R)) => (g R))) ### Exists 20 % 0.21/0.44 22. ((((f zenon_X0) /\ (g zenon_X0)) => (h zenon_X0)) => (Ex Y, ((f Y) /\ (-. (g Y))))) (All R, (((f R) /\ (h R)) => (g R))) ((All W, ((f W) => (g W))) \/ (All Z, ((f Z) => (h Z)))) (-. (Ex V, ((f V) /\ ((g V) /\ (-. (h V)))))) ### Imply 6 21 % 0.21/0.44 23. (All X, ((((f X) /\ (g X)) => (h X)) => (Ex Y, ((f Y) /\ (-. (g Y)))))) (-. (Ex V, ((f V) /\ ((g V) /\ (-. (h V)))))) ((All W, ((f W) => (g W))) \/ (All Z, ((f Z) => (h Z)))) (All R, (((f R) /\ (h R)) => (g R))) ### All 22 % 0.21/0.44 24. (-. (((All X, ((((f X) /\ (g X)) => (h X)) => (Ex Y, ((f Y) /\ (-. (g Y)))))) /\ ((All W, ((f W) => (g W))) \/ (All Z, ((f Z) => (h Z))))) => ((All R, (((f R) /\ (h R)) => (g R))) => (Ex V, ((f V) /\ ((g V) /\ (-. (h V)))))))) ### ConjTree 23 % 0.21/0.44 25. (r T_2 T_3) (-. (r T_2 T_3)) ### Axiom % 0.21/0.44 26. (r T_2 T_3) (-. (r T_2 T_3)) ### Axiom % 0.21/0.44 27. (r T_3 T_2) (-. (r T_3 T_2)) ### Axiom % 0.21/0.44 28. (-. (r T_2 T_2)) (r T_2 T_2) ### Axiom % 0.21/0.44 29. (((r T_2 T_3) /\ (r T_3 T_2)) => (r T_2 T_2)) (-. (r T_2 T_2)) (r T_3 T_2) (r T_2 T_3) ### DisjTree 26 27 28 % 0.21/0.44 30. (All Z, (((r T_2 T_3) /\ (r T_3 Z)) => (r T_2 Z))) (r T_2 T_3) (r T_3 T_2) (-. (r T_2 T_2)) ### All 29 % 0.21/0.44 31. (All Y, (All Z, (((r T_2 Y) /\ (r Y Z)) => (r T_2 Z)))) (-. (r T_2 T_2)) (r T_3 T_2) (r T_2 T_3) ### All 30 % 0.21/0.44 32. ((r T_2 T_3) => (r T_3 T_2)) (-. (r T_2 T_2)) (All Y, (All Z, (((r T_2 Y) /\ (r Y Z)) => (r T_2 Z)))) (r T_2 T_3) ### Imply 25 31 % 0.21/0.44 33. (All Y, ((r T_2 Y) => (r Y T_2))) (r T_2 T_3) (All Y, (All Z, (((r T_2 Y) /\ (r Y Z)) => (r T_2 Z)))) (-. (r T_2 T_2)) ### All 32 % 0.21/0.44 34. (All X, (All Y, ((r X Y) => (r Y X)))) (-. (r T_2 T_2)) (All Y, (All Z, (((r T_2 Y) /\ (r Y Z)) => (r T_2 Z)))) (r T_2 T_3) ### All 33 % 0.21/0.44 35. (All X, (All Y, (All Z, (((r X Y) /\ (r Y Z)) => (r X Z))))) (r T_2 T_3) (-. (r T_2 T_2)) (All X, (All Y, ((r X Y) => (r Y X)))) ### All 34 % 0.21/0.44 36. (-. ((r T_2 T_3) => (r T_2 T_2))) (All X, (All Y, ((r X Y) => (r Y X)))) (All X, (All Y, (All Z, (((r X Y) /\ (r Y Z)) => (r X Z))))) ### NotImply 35 % 0.21/0.44 37. (-. (All Y, ((r T_2 Y) => (r T_2 T_2)))) (All X, (All Y, (All Z, (((r X Y) /\ (r Y Z)) => (r X Z))))) (All X, (All Y, ((r X Y) => (r Y X)))) ### NotAllEx 36 % 0.21/0.44 38. (-. (All X, (All Y, ((r X Y) => (r X X))))) (All X, (All Y, ((r X Y) => (r Y X)))) (All X, (All Y, (All Z, (((r X Y) /\ (r Y Z)) => (r X Z))))) ### NotAllEx 37 % 0.21/0.44 39. (-. (((All X, (All Y, ((r X Y) => (r Y X)))) /\ (All X, (All Y, (All Z, (((r X Y) /\ (r Y Z)) => (r X Z)))))) => (All X, (All Y, ((r X Y) => (r X X)))))) ### ConjTree 38 % 0.21/0.44 40. (f T_4) (-. (f T_4)) ### Axiom % 0.21/0.44 41. (g T_4) (-. (g T_4)) ### Axiom % 0.21/0.44 42. (-. (h T_4)) (h T_4) ### Axiom % 0.21/0.44 43. (-. ((f T_4) /\ ((g T_4) /\ (-. (h T_4))))) (-. (h T_4)) (g T_4) (f T_4) ### DisjTree 40 41 42 % 0.21/0.44 44. (-. (Ex V, ((f V) /\ ((g V) /\ (-. (h V)))))) (f T_4) (g T_4) (-. (h T_4)) ### NotExists 43 % 0.21/0.44 45. (-. (((f T_4) /\ (g T_4)) => (h T_4))) (-. (Ex V, ((f V) /\ ((g V) /\ (-. (h V)))))) ### ConjTree 44 % 0.21/0.44 46. (-. (All X, (((f X) /\ (g X)) => (h X)))) (-. (Ex V, ((f V) /\ ((g V) /\ (-. (h V)))))) ### NotAllEx 45 % 0.21/0.44 47. ((All X, (((f X) /\ (g X)) => (h X))) => (Ex Y, ((f Y) /\ (-. (g Y))))) (All R, (((f R) /\ (h R)) => (g R))) ((All W, ((f W) => (g W))) \/ (All Z, ((f Z) => (h Z)))) (-. (Ex V, ((f V) /\ ((g V) /\ (-. (h V)))))) ### Imply 46 21 % 0.21/0.44 48. (-. ((((All X, (((f X) /\ (g X)) => (h X))) => (Ex Y, ((f Y) /\ (-. (g Y))))) /\ ((All W, ((f W) => (g W))) \/ (All Z, ((f Z) => (h Z))))) => ((All R, (((f R) /\ (h R)) => (g R))) => (Ex V, ((f V) /\ ((g V) /\ (-. (h V)))))))) ### ConjTree 47 % 0.21/0.44 49. (-. (p T_5)) (p T_5) ### Axiom % 0.21/0.44 50. (-. (((p T_6) => (q T_5)) => ((p T_5) => (q T_5)))) (-. (p T_5)) ### ConjTree 49 % 0.21/0.44 51. (-. (All Y, (((p Y) => (q T_5)) => ((p T_5) => (q T_5))))) (-. (p T_5)) ### NotAllEx 50 % 0.21/0.44 52. (-. (Ex X, (All Y, (((p Y) => (q X)) => ((p X) => (q X)))))) (-. (p T_5)) ### NotExists 51 % 0.21/0.44 53. (-. (q zenon_X7)) (q zenon_X7) ### Axiom % 0.21/0.44 54. ((p T_5) => (q zenon_X7)) (-. (q zenon_X7)) (-. (Ex X, (All Y, (((p Y) => (q X)) => ((p X) => (q X)))))) ### Imply 52 53 % 0.21/0.44 55. (-. (((p T_5) => (q zenon_X7)) => ((p zenon_X7) => (q zenon_X7)))) (-. (Ex X, (All Y, (((p Y) => (q X)) => ((p X) => (q X)))))) ### ConjTree 54 % 0.21/0.44 56. (-. (All Y, (((p Y) => (q zenon_X7)) => ((p zenon_X7) => (q zenon_X7))))) (-. (Ex X, (All Y, (((p Y) => (q X)) => ((p X) => (q X)))))) ### NotAllEx 55 % 0.21/0.44 57. (-. (Ex X, (All Y, (((p Y) => (q X)) => ((p X) => (q X)))))) ### NotExists 56 % 0.21/0.44 58. (-. (p T_8)) (p T_8) ### Axiom % 0.21/0.44 59. (All X, (p X)) (-. (p T_8)) ### All 58 % 0.21/0.44 60. (-. (q T_8)) (q T_8) ### Axiom % 0.21/0.44 61. (All X, (q X)) (-. (q T_8)) ### All 60 % 0.21/0.44 62. (-. ((p T_8) /\ (q T_8))) (All X, (q X)) (All X, (p X)) ### NotAnd 59 61 % 0.21/0.44 63. ((All X, (p X)) /\ (All X, (q X))) (-. ((p T_8) /\ (q T_8))) ### And 62 % 0.21/0.44 64. (-. (All X, ((p X) /\ (q X)))) ((All X, (p X)) /\ (All X, (q X))) ### NotAllEx 63 % 0.21/0.44 65. (-. (p T_9)) (p T_9) ### Axiom % 0.21/0.44 66. ((p T_9) /\ (q T_9)) (-. (p T_9)) ### And 65 % 0.21/0.44 67. (All X, ((p X) /\ (q X))) (-. (p T_9)) ### All 66 % 0.21/0.44 68. (-. (All X, (p X))) (All X, ((p X) /\ (q X))) ### NotAllEx 67 % 0.21/0.44 69. (-. (q T_10)) (q T_10) ### Axiom % 0.21/0.44 70. ((p T_10) /\ (q T_10)) (-. (q T_10)) ### And 69 % 0.21/0.44 71. (All X, ((p X) /\ (q X))) (-. (q T_10)) ### All 70 % 0.21/0.44 72. (-. (All X, (q X))) (All X, ((p X) /\ (q X))) ### NotAllEx 71 % 0.21/0.44 73. (-. ((All X, (p X)) /\ (All X, (q X)))) (All X, ((p X) /\ (q X))) ### NotAnd 68 72 % 0.21/0.44 74. (-. ((All X, ((p X) /\ (q X))) <=> ((All X, (p X)) /\ (All X, (q X))))) ### NotEquiv 64 73 % 0.21/0.44 75. (-. (p T_11)) (p T_11) ### Axiom % 0.21/0.44 76. (All X, (p X)) (-. (p T_11)) ### All 75 % 0.21/0.44 77. (-. (q T_11)) (q T_11) ### Axiom % 0.21/0.44 78. (All X, (q X)) (-. (q T_11)) ### All 77 % 0.21/0.44 79. ((All X, (p X)) \/ (All X, (q X))) (-. (q T_11)) (-. (p T_11)) ### Or 76 78 % 0.21/0.44 80. (-. ((p T_11) \/ (q T_11))) ((All X, (p X)) \/ (All X, (q X))) ### NotOr 79 % 0.21/0.44 81. (-. (All X, ((p X) \/ (q X)))) ((All X, (p X)) \/ (All X, (q X))) ### NotAllEx 80 % 0.21/0.44 82. (-. (((All X, (p X)) \/ (All X, (q X))) => (All X, ((p X) \/ (q X))))) ### NotImply 81 % 0.21/0.44 83. (p T_12) (-. (p T_12)) ### Axiom % 0.21/0.44 84. (-. ((p T_12) \/ (q T_12))) (p T_12) ### NotOr 83 % 0.21/0.44 85. (-. (Ex X, ((p X) \/ (q X)))) (p T_12) ### NotExists 84 % 0.21/0.44 86. (Ex X, (p X)) (-. (Ex X, ((p X) \/ (q X)))) ### Exists 85 % 0.21/0.44 87. (q T_13) (-. (q T_13)) ### Axiom % 0.21/0.44 88. (-. ((p T_13) \/ (q T_13))) (q T_13) ### NotOr 87 % 0.21/0.44 89. (-. (Ex X, ((p X) \/ (q X)))) (q T_13) ### NotExists 88 % 0.21/0.44 90. (Ex X, (q X)) (-. (Ex X, ((p X) \/ (q X)))) ### Exists 89 % 0.21/0.44 91. ((Ex X, (p X)) \/ (Ex X, (q X))) (-. (Ex X, ((p X) \/ (q X)))) ### Or 86 90 % 0.21/0.44 92. (p T_14) (-. (p T_14)) ### Axiom % 0.21/0.44 93. (-. (Ex X, (p X))) (p T_14) ### NotExists 92 % 0.21/0.44 94. (q T_14) (-. (q T_14)) ### Axiom % 0.21/0.44 95. (-. (Ex X, (q X))) (q T_14) ### NotExists 94 % 0.21/0.44 96. ((p T_14) \/ (q T_14)) (-. (Ex X, (q X))) (-. (Ex X, (p X))) ### Or 93 95 % 0.21/0.44 97. (-. ((Ex X, (p X)) \/ (Ex X, (q X)))) ((p T_14) \/ (q T_14)) ### NotOr 96 % 0.21/0.44 98. (Ex X, ((p X) \/ (q X))) (-. ((Ex X, (p X)) \/ (Ex X, (q X)))) ### Exists 97 % 0.21/0.44 99. (-. ((Ex X, ((p X) \/ (q X))) <=> ((Ex X, (p X)) \/ (Ex X, (q X))))) ### NotEquiv 91 98 % 0.21/0.44 100. (-. (p T_9)) (p T_9) ### Axiom % 0.21/0.44 101. (-. ((p T_9) => (All X, (p X)))) (-. (p T_9)) ### NotImply 100 % 0.21/0.44 102. (-. (Ex Y, ((p Y) => (All X, (p X))))) (-. (p T_9)) ### NotExists 101 % 0.21/0.44 103. (-. (All X, (p X))) (-. (Ex Y, ((p Y) => (All X, (p X))))) ### NotAllEx 102 % 0.21/0.44 104. (-. ((p zenon_X15) => (All X, (p X)))) (-. (Ex Y, ((p Y) => (All X, (p X))))) ### NotImply 103 % 0.21/0.44 105. (-. (Ex Y, ((p Y) => (All X, (p X))))) ### NotExists 104 % 0.21/0.44 106. (p T_16) (-. (p T_16)) ### Axiom % 0.21/0.44 107. (-. (Ex X, (p X))) (p T_16) ### NotExists 106 % 0.21/0.44 108. (q T_16) (-. (q T_16)) ### Axiom % 0.21/0.44 109. (-. (Ex X, (q X))) (q T_16) ### NotExists 108 % 0.21/0.44 110. (-. ((Ex X, (p X)) /\ (Ex X, (q X)))) (q T_16) (p T_16) ### NotAnd 107 109 % 0.21/0.44 111. ((p T_16) /\ (q T_16)) (-. ((Ex X, (p X)) /\ (Ex X, (q X)))) ### And 110 % 0.21/0.44 112. (Ex X, ((p X) /\ (q X))) (-. ((Ex X, (p X)) /\ (Ex X, (q X)))) ### Exists 111 % 0.21/0.44 113. (-. ((Ex X, ((p X) /\ (q X))) => ((Ex X, (p X)) /\ (Ex X, (q X))))) ### NotImply 112 % 0.21/0.44 114. (-. (p T_17)) (p T_17) ### Axiom % 0.21/0.44 115. (All X, (p X)) (-. (p T_17)) ### All 114 % 0.21/0.44 116. (-. ((All X, (p X)) => (p T_17))) ### NotImply 115 % 0.21/0.44 117. (-. (All Y, ((All X, (p X)) => (p Y)))) ### NotAllEx 116 % 0.21/0.44 118. (p zenon_X18) (-. (p zenon_X18)) ### Axiom % 0.21/0.44 119. (-. (Ex X, (p X))) (p zenon_X18) ### NotExists 118 % 0.21/0.44 120. (All X, (p X)) (-. (Ex X, (p X))) ### All 119 % 0.21/0.44 121. (-. ((All X, (p X)) => (Ex X, (p X)))) ### NotImply 120 % 0.21/0.44 122. (-. (Ex X, (p X))) (Ex X, (p X)) ### Axiom % 0.21/0.44 123. (-. ((Ex X, (p X)) => (p T_19))) (-. (Ex X, (p X))) ### NotImply 122 % 0.21/0.44 124. (-. (All Y, ((Ex X, (p X)) => (p Y)))) (-. (Ex X, (p X))) ### NotAllEx 123 % 0.21/0.44 125. (-. ((-. (Ex X, (p X))) => (All Y, ((Ex X, (p X)) => (p Y))))) ### NotImply 124 % 0.21/0.44 126. (-. (p T_20)) (p T_20) ### Axiom % 0.21/0.44 127. (All X, (p X)) (-. (p T_20)) ### All 126 % 0.21/0.44 128. (-. (c)) (c) ### P-NotP % 0.21/0.44 129. ((All X, (p X)) \/ (c)) (-. (c)) (-. (p T_20)) ### Or 127 128 % 0.21/0.44 130. (-. ((p T_20) \/ (c))) ((All X, (p X)) \/ (c)) ### NotOr 129 % 0.21/0.44 131. (-. (All X, ((p X) \/ (c)))) ((All X, (p X)) \/ (c)) ### NotAllEx 130 % 0.21/0.44 132. (-. (p T_9)) (p T_9) ### Axiom % 0.21/0.44 133. ((p T_9) \/ (c)) (-. (c)) (-. (p T_9)) ### Or 132 128 % 0.21/0.44 134. (All X, ((p X) \/ (c))) (-. (p T_9)) (-. (c)) ### All 133 % 0.21/0.44 135. (-. (All X, (p X))) (-. (c)) (All X, ((p X) \/ (c))) ### NotAllEx 134 % 0.21/0.44 136. (-. ((All X, (p X)) \/ (c))) (All X, ((p X) \/ (c))) ### NotOr 135 % 0.21/0.44 137. (-. ((All X, ((p X) \/ (c))) <=> ((All X, (p X)) \/ (c)))) ### NotEquiv 131 136 % 0.21/0.44 138. (p T_12) (-. (p T_12)) ### Axiom % 0.21/0.44 139. (-. ((p T_12) /\ (c))) (c) (p T_12) ### NotAnd 138 128 % 0.21/0.44 140. (-. (Ex X, ((p X) /\ (c)))) (p T_12) (c) ### NotExists 139 % 0.21/0.44 141. (Ex X, (p X)) (c) (-. (Ex X, ((p X) /\ (c)))) ### Exists 140 % 0.21/0.44 142. ((Ex X, (p X)) /\ (c)) (-. (Ex X, ((p X) /\ (c)))) ### And 141 % 0.21/0.44 143. (p T_21) (-. (p T_21)) ### Axiom % 0.21/0.44 144. (-. (Ex X, (p X))) (p T_21) ### NotExists 143 % 0.21/0.44 145. (-. ((Ex X, (p X)) /\ (c))) (c) (p T_21) ### NotAnd 144 128 % 0.21/0.44 146. ((p T_21) /\ (c)) (-. ((Ex X, (p X)) /\ (c))) ### And 145 % 0.21/0.44 147. (Ex X, ((p X) /\ (c))) (-. ((Ex X, (p X)) /\ (c))) ### Exists 146 % 0.21/0.44 148. (-. ((Ex X, ((p X) /\ (c))) <=> ((Ex X, (p X)) /\ (c)))) ### NotEquiv 142 147 % 0.21/0.44 149. (-. (Ex X, (c))) (c) ### NotExists 128 % 0.21/0.44 150. (Ex X, (c)) (-. (c)) ### Exists 128 % 0.21/0.44 151. (-. ((Ex X, (c)) <=> (c))) ### NotEquiv 149 150 % 0.21/0.44 152. (-. (All X, (c))) (c) ### NotAllEx 128 % 0.21/0.44 153. (All X, (c)) (-. (c)) ### All 128 % 0.21/0.44 154. (-. ((All X, (c)) <=> (c))) ### NotEquiv 152 153 % 0.21/0.44 155. (-. ((c) => (p zenon_X22))) (-. (c)) ### NotImply 128 % 0.21/0.44 156. (-. (Ex X, ((c) => (p X)))) (-. (c)) ### NotExists 155 % 0.21/0.44 157. (p T_12) (-. (p T_12)) ### Axiom % 0.21/0.44 158. (-. ((c) => (p T_12))) (p T_12) ### NotImply 157 % 0.21/0.44 159. (-. (Ex X, ((c) => (p X)))) (p T_12) ### NotExists 158 % 0.21/0.44 160. (Ex X, (p X)) (-. (Ex X, ((c) => (p X)))) ### Exists 159 % 0.21/0.44 161. ((c) => (Ex X, (p X))) (-. (Ex X, ((c) => (p X)))) ### Imply 156 160 % 0.21/0.44 162. (p T_23) (-. (p T_23)) ### Axiom % 0.21/0.44 163. (-. (Ex X, (p X))) (p T_23) ### NotExists 162 % 0.21/0.44 164. ((c) => (p T_23)) (-. (Ex X, (p X))) (c) ### Imply 128 163 % 0.21/0.44 165. (-. ((c) => (Ex X, (p X)))) ((c) => (p T_23)) ### NotImply 164 % 0.21/0.44 166. (Ex X, ((c) => (p X))) (-. ((c) => (Ex X, (p X)))) ### Exists 165 % 0.21/0.44 167. (-. ((Ex X, ((c) => (p X))) <=> ((c) => (Ex X, (p X))))) ### NotEquiv 161 166 % 0.21/0.44 168. (-. (p T_9)) (p T_9) ### Axiom % 0.21/0.44 169. (-. ((p T_9) => (c))) (-. (p T_9)) ### NotImply 168 % 0.21/0.44 170. (-. (Ex X, ((p X) => (c)))) (-. (p T_9)) ### NotExists 169 % 0.21/0.44 171. (-. (All X, (p X))) (-. (Ex X, ((p X) => (c)))) ### NotAllEx 170 % 0.21/0.44 172. (-. ((p zenon_X24) => (c))) (c) ### NotImply 128 % 0.21/0.44 173. (-. (Ex X, ((p X) => (c)))) (c) ### NotExists 172 % 0.21/0.44 174. ((All X, (p X)) => (c)) (-. (Ex X, ((p X) => (c)))) ### Imply 171 173 % 0.21/0.44 175. (-. (p T_25)) (p T_25) ### Axiom % 0.21/0.44 176. (All X, (p X)) (-. (p T_25)) ### All 175 % 0.21/0.44 177. ((p T_25) => (c)) (-. (c)) (All X, (p X)) ### Imply 176 128 % 0.21/0.44 178. (-. ((All X, (p X)) => (c))) ((p T_25) => (c)) ### NotImply 177 % 0.21/0.44 179. (Ex X, ((p X) => (c))) (-. ((All X, (p X)) => (c))) ### Exists 178 % 0.21/0.44 180. (-. ((Ex X, ((p X) => (c))) <=> ((All X, (p X)) => (c)))) ### NotEquiv 174 179 % 0.21/0.44 181. (-. (p T_26)) (p T_26) ### Axiom % 0.21/0.44 182. (All X, (p X)) (-. (p T_26)) ### All 181 % 0.21/0.44 183. ((c) => (All X, (p X))) (-. (p T_26)) (c) ### Imply 128 182 % 0.21/0.44 184. (-. ((c) => (p T_26))) ((c) => (All X, (p X))) ### NotImply 183 % 0.21/0.44 185. (-. (All X, ((c) => (p X)))) ((c) => (All X, (p X))) ### NotAllEx 184 % 0.21/0.44 186. (-. (p T_9)) (p T_9) ### Axiom % 0.21/0.44 187. ((c) => (p T_9)) (-. (p T_9)) (c) ### Imply 128 186 % 0.21/0.44 188. (All X, ((c) => (p X))) (c) (-. (p T_9)) ### All 187 % 0.21/0.44 189. (-. (All X, (p X))) (c) (All X, ((c) => (p X))) ### NotAllEx 188 % 0.21/0.44 190. (-. ((c) => (All X, (p X)))) (All X, ((c) => (p X))) ### NotImply 189 % 0.21/0.44 191. (-. ((All X, ((c) => (p X))) <=> ((c) => (All X, (p X))))) ### NotEquiv 185 190 % 0.21/0.44 192. (p T_27) (-. (p T_27)) ### Axiom % 0.21/0.44 193. (-. (Ex X, (p X))) (p T_27) ### NotExists 192 % 0.21/0.44 194. ((Ex X, (p X)) => (c)) (-. (c)) (p T_27) ### Imply 193 128 % 0.21/0.44 195. (-. ((p T_27) => (c))) ((Ex X, (p X)) => (c)) ### NotImply 194 % 0.21/0.44 196. (-. (All X, ((p X) => (c)))) ((Ex X, (p X)) => (c)) ### NotAllEx 195 % 0.21/0.44 197. (p T_12) (-. (p T_12)) ### Axiom % 0.21/0.44 198. ((p T_12) => (c)) (-. (c)) (p T_12) ### Imply 197 128 % 0.21/0.44 199. (All X, ((p X) => (c))) (p T_12) (-. (c)) ### All 198 % 0.21/0.44 200. (Ex X, (p X)) (-. (c)) (All X, ((p X) => (c))) ### Exists 199 % 0.21/0.44 201. (-. ((Ex X, (p X)) => (c))) (All X, ((p X) => (c))) ### NotImply 200 % 0.21/0.44 202. (-. ((All X, ((p X) => (c))) <=> ((Ex X, (p X)) => (c)))) ### NotEquiv 196 201 % 0.21/0.44 203. (-. ((((All X, ((((f X) /\ (g X)) => (h X)) => (Ex Y, ((f Y) /\ (-. (g Y)))))) /\ ((All W, ((f W) => (g W))) \/ (All Z, ((f Z) => (h Z))))) => ((All R, (((f R) /\ (h R)) => (g R))) => (Ex V, ((f V) /\ ((g V) /\ (-. (h V))))))) /\ ((((All X, (All Y, ((r X Y) => (r Y X)))) /\ (All X, (All Y, (All Z, (((r X Y) /\ (r Y Z)) => (r X Z)))))) => (All X, (All Y, ((r X Y) => (r X X))))) /\ (((((All X, (((f X) /\ (g X)) => (h X))) => (Ex Y, ((f Y) /\ (-. (g Y))))) /\ ((All W, ((f W) => (g W))) \/ (All Z, ((f Z) => (h Z))))) => ((All R, (((f R) /\ (h R)) => (g R))) => (Ex V, ((f V) /\ ((g V) /\ (-. (h V))))))) /\ ((Ex X, (All Y, (((p Y) => (q X)) => ((p X) => (q X))))) /\ (((All X, ((p X) /\ (q X))) <=> ((All X, (p X)) /\ (All X, (q X)))) /\ ((((All X, (p X)) \/ (All X, (q X))) => (All X, ((p X) \/ (q X)))) /\ (((Ex X, ((p X) \/ (q X))) <=> ((Ex X, (p X)) \/ (Ex X, (q X)))) /\ ((Ex Y, ((p Y) => (All X, (p X)))) /\ (((Ex X, ((p X) /\ (q X))) => ((Ex X, (p X)) /\ (Ex X, (q X)))) /\ ((All Y, ((All X, (p X)) => (p Y))) /\ (((All X, (p X)) => (Ex X, (p X))) /\ (((-. (Ex X, (p X))) => (All Y, ((Ex X, (p X)) => (p Y)))) /\ (((All X, ((p X) \/ (c))) <=> ((All X, (p X)) \/ (c))) /\ (((Ex X, ((p X) /\ (c))) <=> ((Ex X, (p X)) /\ (c))) /\ (((Ex X, (c)) <=> (c)) /\ (((All X, (c)) <=> (c)) /\ (((Ex X, ((c) => (p X))) <=> ((c) => (Ex X, (p X)))) /\ (((Ex X, ((p X) => (c))) <=> ((All X, (p X)) => (c))) /\ (((All X, ((c) => (p X))) <=> ((c) => (All X, (p X)))) /\ ((All X, ((p X) => (c))) <=> ((Ex X, (p X)) => (c))))))))))))))))))))))) ### DisjTree 24 39 48 57 74 82 99 105 113 117 121 125 137 148 151 154 167 180 191 202 % 0.21/0.44 % SZS output end Proof % 0.21/0.44 (* END-PROOF *) %------------------------------------------------------------------------------