%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SYN938+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 : n009.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:23 EDT 2022 % Result : Theorem 0.22s 0.47s % Output : Proof 0.37s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.13 % Problem : SYN938+1 : TPTP v8.1.0. Released v3.1.0. % 0.08/0.14 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.15/0.36 % Computer : n009.cluster.edu % 0.15/0.36 % Model : x86_64 x86_64 % 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.36 % Memory : 8042.1875MB % 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.36 % CPULimit : 300 % 0.15/0.36 % WCLimit : 600 % 0.15/0.36 % DateTime : Mon Jul 11 21:16:07 EDT 2022 % 0.15/0.36 % CPUTime : % 0.22/0.47 % SZS status Theorem % 0.22/0.47 (* PROOF-FOUND *) % 0.22/0.47 (* BEGIN-PROOF *) % 0.22/0.47 % SZS output start Proof % 0.22/0.47 1. (-. (p1 (f zenon_X0))) (p1 (f zenon_X0)) ### Axiom % 0.22/0.47 2. (-. ((p1 (f zenon_X0)) => (p1 (f zenon_X0)))) (-. (p1 (f zenon_X0))) ### NotImply 1 % 0.22/0.47 3. (-. (p1 (f T_1))) (p1 (f T_1)) ### Axiom % 0.22/0.47 4. (-. ((p1 (f T_1)) => (p1 (f T_1)))) ### NotImply 3 % 0.22/0.47 5. (-. (r1 T_1)) (r1 T_1) ### Axiom % 0.22/0.47 6. (-. ((r1 T_1) => ((r1 T_1) /\ (r1 T_2)))) (-. (r1 T_1)) ### NotImply 5 % 0.22/0.47 7. (q1 (f T_1)) (-. (q1 (f T_1))) ### Axiom % 0.22/0.47 8. (-. (((p1 (f T_1)) => (p1 (f T_1))) /\ (((r1 T_1) => ((r1 T_1) /\ (r1 T_2))) /\ (q1 (f T_1))))) (q1 (f T_1)) (-. (r1 T_1)) ### DisjTree 4 6 7 % 0.22/0.47 9. (-. (Ex Y, (((p1 (f Y)) => (p1 (f T_1))) /\ (((r1 Y) => ((r1 T_1) /\ (r1 T_2))) /\ (q1 (f T_1)))))) (-. (r1 T_1)) (q1 (f T_1)) ### NotExists 8 % 0.22/0.47 10. (-. (Ex X, (Ex Y, (((p1 (f Y)) => (p1 X)) /\ (((r1 Y) => ((r1 T_1) /\ (r1 T_2))) /\ (q1 X)))))) (q1 (f T_1)) (-. (r1 T_1)) ### NotExists 9 % 0.22/0.47 11. (All Z, (q1 (f Z))) (-. (r1 T_1)) (-. (Ex X, (Ex Y, (((p1 (f Y)) => (p1 X)) /\ (((r1 Y) => ((r1 T_1) /\ (r1 T_2))) /\ (q1 X)))))) ### All 10 % 0.22/0.47 12. (-. (p1 (f T_2))) (p1 (f T_2)) ### Axiom % 0.22/0.47 13. (-. ((p1 (f T_2)) => (p1 (f T_2)))) ### NotImply 12 % 0.22/0.47 14. (-. (r1 T_2)) (r1 T_2) ### Axiom % 0.22/0.47 15. (-. ((r1 T_2) => ((r1 T_1) /\ (r1 T_2)))) (-. (r1 T_2)) ### NotImply 14 % 0.22/0.47 16. (q1 (f T_2)) (-. (q1 (f T_2))) ### Axiom % 0.22/0.47 17. (-. (((p1 (f T_2)) => (p1 (f T_2))) /\ (((r1 T_2) => ((r1 T_1) /\ (r1 T_2))) /\ (q1 (f T_2))))) (q1 (f T_2)) (-. (r1 T_2)) ### DisjTree 13 15 16 % 0.22/0.47 18. (-. (Ex Y, (((p1 (f Y)) => (p1 (f T_2))) /\ (((r1 Y) => ((r1 T_1) /\ (r1 T_2))) /\ (q1 (f T_2)))))) (-. (r1 T_2)) (q1 (f T_2)) ### NotExists 17 % 0.22/0.47 19. (-. (Ex X, (Ex Y, (((p1 (f Y)) => (p1 X)) /\ (((r1 Y) => ((r1 T_1) /\ (r1 T_2))) /\ (q1 X)))))) (q1 (f T_2)) (-. (r1 T_2)) ### NotExists 18 % 0.22/0.47 20. (All Z, (q1 (f Z))) (-. (r1 T_2)) (-. (Ex X, (Ex Y, (((p1 (f Y)) => (p1 X)) /\ (((r1 Y) => ((r1 T_1) /\ (r1 T_2))) /\ (q1 X)))))) ### All 19 % 0.22/0.47 21. (-. ((r1 T_1) /\ (r1 T_2))) (-. (Ex X, (Ex Y, (((p1 (f Y)) => (p1 X)) /\ (((r1 Y) => ((r1 T_1) /\ (r1 T_2))) /\ (q1 X)))))) (All Z, (q1 (f Z))) ### NotAnd 11 20 % 0.22/0.47 22. (-. ((r1 zenon_X0) => ((r1 T_1) /\ (r1 T_2)))) (All Z, (q1 (f Z))) (-. (Ex X, (Ex Y, (((p1 (f Y)) => (p1 X)) /\ (((r1 Y) => ((r1 T_1) /\ (r1 T_2))) /\ (q1 X)))))) ### NotImply 21 % 0.22/0.47 23. (q1 (f zenon_X0)) (-. (q1 (f zenon_X0))) ### Axiom % 0.22/0.47 24. (-. (((p1 (f zenon_X0)) => (p1 (f zenon_X0))) /\ (((r1 zenon_X0) => ((r1 T_1) /\ (r1 T_2))) /\ (q1 (f zenon_X0))))) (q1 (f zenon_X0)) (-. (Ex X, (Ex Y, (((p1 (f Y)) => (p1 X)) /\ (((r1 Y) => ((r1 T_1) /\ (r1 T_2))) /\ (q1 X)))))) (All Z, (q1 (f Z))) (-. (p1 (f zenon_X0))) ### DisjTree 2 22 23 % 0.22/0.47 25. (-. (Ex Y, (((p1 (f Y)) => (p1 (f zenon_X0))) /\ (((r1 Y) => ((r1 T_1) /\ (r1 T_2))) /\ (q1 (f zenon_X0)))))) (-. (p1 (f zenon_X0))) (All Z, (q1 (f Z))) (-. (Ex X, (Ex Y, (((p1 (f Y)) => (p1 X)) /\ (((r1 Y) => ((r1 T_1) /\ (r1 T_2))) /\ (q1 X)))))) (q1 (f zenon_X0)) ### NotExists 24 % 0.22/0.47 26. (-. ((p1 (f zenon_X3)) => (p1 (f zenon_X0)))) (q1 (f zenon_X0)) (-. (Ex X, (Ex Y, (((p1 (f Y)) => (p1 X)) /\ (((r1 Y) => ((r1 T_1) /\ (r1 T_2))) /\ (q1 X)))))) (All Z, (q1 (f Z))) (-. (Ex Y, (((p1 (f Y)) => (p1 (f zenon_X0))) /\ (((r1 Y) => ((r1 T_1) /\ (r1 T_2))) /\ (q1 (f zenon_X0)))))) ### NotImply 25 % 0.22/0.47 27. (-. ((r1 zenon_X3) => ((r1 T_1) /\ (r1 T_2)))) (All Z, (q1 (f Z))) (-. (Ex X, (Ex Y, (((p1 (f Y)) => (p1 X)) /\ (((r1 Y) => ((r1 T_1) /\ (r1 T_2))) /\ (q1 X)))))) ### NotImply 21 % 0.22/0.47 28. (q1 (f zenon_X0)) (-. (q1 (f zenon_X0))) ### Axiom % 0.22/0.47 29. (-. (((p1 (f zenon_X3)) => (p1 (f zenon_X0))) /\ (((r1 zenon_X3) => ((r1 T_1) /\ (r1 T_2))) /\ (q1 (f zenon_X0))))) (-. (Ex Y, (((p1 (f Y)) => (p1 (f zenon_X0))) /\ (((r1 Y) => ((r1 T_1) /\ (r1 T_2))) /\ (q1 (f zenon_X0)))))) (All Z, (q1 (f Z))) (-. (Ex X, (Ex Y, (((p1 (f Y)) => (p1 X)) /\ (((r1 Y) => ((r1 T_1) /\ (r1 T_2))) /\ (q1 X)))))) (q1 (f zenon_X0)) ### DisjTree 26 27 28 % 0.22/0.47 30. (q1 (f zenon_X0)) (-. (Ex X, (Ex Y, (((p1 (f Y)) => (p1 X)) /\ (((r1 Y) => ((r1 T_1) /\ (r1 T_2))) /\ (q1 X)))))) (All Z, (q1 (f Z))) (-. (Ex Y, (((p1 (f Y)) => (p1 (f zenon_X0))) /\ (((r1 Y) => ((r1 T_1) /\ (r1 T_2))) /\ (q1 (f zenon_X0)))))) ### NotExists 29 % 0.22/0.47 31. (All Z, (q1 (f Z))) (-. (Ex X, (Ex Y, (((p1 (f Y)) => (p1 X)) /\ (((r1 Y) => ((r1 T_1) /\ (r1 T_2))) /\ (q1 X)))))) (q1 (f zenon_X0)) ### NotExists 30 % 0.22/0.47 32. (-. (Ex X, (Ex Y, (((p1 (f Y)) => (p1 X)) /\ (((r1 Y) => ((r1 T_1) /\ (r1 T_2))) /\ (q1 X)))))) (All Z, (q1 (f Z))) ### All 31 % 0.22/0.47 33. (-. ((All Z, (q1 (f Z))) => (Ex X, (Ex Y, (((p1 (f Y)) => (p1 X)) /\ (((r1 Y) => ((r1 T_1) /\ (r1 T_2))) /\ (q1 X))))))) ### NotImply 32 % 0.22/0.47 34. (-. (All B, ((All Z, (q1 (f Z))) => (Ex X, (Ex Y, (((p1 (f Y)) => (p1 X)) /\ (((r1 Y) => ((r1 B) /\ (r1 T_2))) /\ (q1 X)))))))) ### NotAllEx 33 % 0.22/0.47 35. (-. (All C, (All B, ((All Z, (q1 (f Z))) => (Ex X, (Ex Y, (((p1 (f Y)) => (p1 X)) /\ (((r1 Y) => ((r1 B) /\ (r1 C))) /\ (q1 X))))))))) ### NotAllEx 34 % 0.22/0.47 36. (-. (p1 (f zenon_X0))) (p1 (f zenon_X0)) ### Axiom % 0.22/0.47 37. (-. ((p1 (f zenon_X0)) => ((p1 (f zenon_X0)) /\ ((r1 zenon_X0) => ((r1 T_4) /\ (r1 T_5)))))) (-. (p1 (f zenon_X0))) ### NotImply 36 % 0.22/0.47 38. (q1 (f zenon_X0)) (-. (q1 (f zenon_X0))) ### Axiom % 0.22/0.47 39. (-. (((p1 (f zenon_X0)) => ((p1 (f zenon_X0)) /\ ((r1 zenon_X0) => ((r1 T_4) /\ (r1 T_5))))) /\ (q1 (f zenon_X0)))) (q1 (f zenon_X0)) (-. (p1 (f zenon_X0))) ### NotAnd 37 38 % 0.22/0.47 40. (-. (Ex Y, (((p1 (f Y)) => ((p1 (f zenon_X0)) /\ ((r1 Y) => ((r1 T_4) /\ (r1 T_5))))) /\ (q1 (f zenon_X0))))) (-. (p1 (f zenon_X0))) (q1 (f zenon_X0)) ### NotExists 39 % 0.22/0.47 41. (p1 (f T_4)) (-. (p1 (f T_4))) ### Axiom % 0.22/0.47 42. (-. (r1 T_4)) (r1 T_4) ### Axiom % 0.22/0.47 43. (-. ((r1 T_4) => ((r1 T_4) /\ (r1 T_5)))) (-. (r1 T_4)) ### NotImply 42 % 0.22/0.47 44. (-. ((p1 (f T_4)) /\ ((r1 T_4) => ((r1 T_4) /\ (r1 T_5))))) (-. (r1 T_4)) (p1 (f T_4)) ### NotAnd 41 43 % 0.22/0.47 45. (-. ((p1 (f T_4)) => ((p1 (f T_4)) /\ ((r1 T_4) => ((r1 T_4) /\ (r1 T_5)))))) (p1 (f T_4)) (-. (r1 T_4)) ### NotImply 44 % 0.22/0.47 46. (q1 (f T_4)) (-. (q1 (f T_4))) ### Axiom % 0.22/0.47 47. (-. (((p1 (f T_4)) => ((p1 (f T_4)) /\ ((r1 T_4) => ((r1 T_4) /\ (r1 T_5))))) /\ (q1 (f T_4)))) (q1 (f T_4)) (-. (r1 T_4)) (p1 (f T_4)) ### NotAnd 45 46 % 0.22/0.47 48. (-. (Ex Y, (((p1 (f Y)) => ((p1 (f T_4)) /\ ((r1 Y) => ((r1 T_4) /\ (r1 T_5))))) /\ (q1 (f T_4))))) (p1 (f T_4)) (-. (r1 T_4)) (q1 (f T_4)) ### NotExists 47 % 0.22/0.47 49. (-. (Ex X, (Ex Y, (((p1 (f Y)) => ((p1 X) /\ ((r1 Y) => ((r1 T_4) /\ (r1 T_5))))) /\ (q1 X))))) (q1 (f T_4)) (-. (r1 T_4)) (p1 (f T_4)) ### NotExists 48 % 0.22/0.47 50. (All Z, (q1 (f Z))) (p1 (f T_4)) (-. (r1 T_4)) (-. (Ex X, (Ex Y, (((p1 (f Y)) => ((p1 X) /\ ((r1 Y) => ((r1 T_4) /\ (r1 T_5))))) /\ (q1 X))))) ### All 49 % 0.22/0.47 51. (-. ((p1 (f T_4)) => ((p1 (f zenon_X0)) /\ ((r1 T_4) => ((r1 T_4) /\ (r1 T_5)))))) (-. (Ex X, (Ex Y, (((p1 (f Y)) => ((p1 X) /\ ((r1 Y) => ((r1 T_4) /\ (r1 T_5))))) /\ (q1 X))))) (-. (r1 T_4)) (All Z, (q1 (f Z))) ### NotImply 50 % 0.22/0.47 52. (q1 (f zenon_X0)) (-. (q1 (f zenon_X0))) ### Axiom % 0.22/0.47 53. (-. (((p1 (f T_4)) => ((p1 (f zenon_X0)) /\ ((r1 T_4) => ((r1 T_4) /\ (r1 T_5))))) /\ (q1 (f zenon_X0)))) (q1 (f zenon_X0)) (All Z, (q1 (f Z))) (-. (r1 T_4)) (-. (Ex X, (Ex Y, (((p1 (f Y)) => ((p1 X) /\ ((r1 Y) => ((r1 T_4) /\ (r1 T_5))))) /\ (q1 X))))) ### NotAnd 51 52 % 0.22/0.47 54. (-. (Ex Y, (((p1 (f Y)) => ((p1 (f zenon_X0)) /\ ((r1 Y) => ((r1 T_4) /\ (r1 T_5))))) /\ (q1 (f zenon_X0))))) (-. (Ex X, (Ex Y, (((p1 (f Y)) => ((p1 X) /\ ((r1 Y) => ((r1 T_4) /\ (r1 T_5))))) /\ (q1 X))))) (-. (r1 T_4)) (All Z, (q1 (f Z))) (q1 (f zenon_X0)) ### NotExists 53 % 0.22/0.47 55. (p1 (f T_5)) (-. (p1 (f T_5))) ### Axiom % 0.22/0.47 56. (-. (r1 T_5)) (r1 T_5) ### Axiom % 0.22/0.47 57. (-. ((r1 T_5) => ((r1 T_4) /\ (r1 T_5)))) (-. (r1 T_5)) ### NotImply 56 % 0.22/0.47 58. (-. ((p1 (f T_5)) /\ ((r1 T_5) => ((r1 T_4) /\ (r1 T_5))))) (-. (r1 T_5)) (p1 (f T_5)) ### NotAnd 55 57 % 0.22/0.47 59. (-. ((p1 (f T_5)) => ((p1 (f T_5)) /\ ((r1 T_5) => ((r1 T_4) /\ (r1 T_5)))))) (p1 (f T_5)) (-. (r1 T_5)) ### NotImply 58 % 0.22/0.47 60. (q1 (f T_5)) (-. (q1 (f T_5))) ### Axiom % 0.22/0.47 61. (-. (((p1 (f T_5)) => ((p1 (f T_5)) /\ ((r1 T_5) => ((r1 T_4) /\ (r1 T_5))))) /\ (q1 (f T_5)))) (q1 (f T_5)) (-. (r1 T_5)) (p1 (f T_5)) ### NotAnd 59 60 % 0.22/0.47 62. (-. (Ex Y, (((p1 (f Y)) => ((p1 (f T_5)) /\ ((r1 Y) => ((r1 T_4) /\ (r1 T_5))))) /\ (q1 (f T_5))))) (p1 (f T_5)) (-. (r1 T_5)) (q1 (f T_5)) ### NotExists 61 % 0.22/0.48 63. (-. (Ex X, (Ex Y, (((p1 (f Y)) => ((p1 X) /\ ((r1 Y) => ((r1 T_4) /\ (r1 T_5))))) /\ (q1 X))))) (q1 (f T_5)) (-. (r1 T_5)) (p1 (f T_5)) ### NotExists 62 % 0.22/0.48 64. (All Z, (q1 (f Z))) (p1 (f T_5)) (-. (r1 T_5)) (-. (Ex X, (Ex Y, (((p1 (f Y)) => ((p1 X) /\ ((r1 Y) => ((r1 T_4) /\ (r1 T_5))))) /\ (q1 X))))) ### All 63 % 0.22/0.48 65. (-. ((p1 (f T_5)) => ((p1 (f zenon_X0)) /\ ((r1 T_5) => ((r1 T_4) /\ (r1 T_5)))))) (-. (Ex X, (Ex Y, (((p1 (f Y)) => ((p1 X) /\ ((r1 Y) => ((r1 T_4) /\ (r1 T_5))))) /\ (q1 X))))) (-. (r1 T_5)) (All Z, (q1 (f Z))) ### NotImply 64 % 0.22/0.48 66. (q1 (f zenon_X0)) (-. (q1 (f zenon_X0))) ### Axiom % 0.22/0.48 67. (-. (((p1 (f T_5)) => ((p1 (f zenon_X0)) /\ ((r1 T_5) => ((r1 T_4) /\ (r1 T_5))))) /\ (q1 (f zenon_X0)))) (q1 (f zenon_X0)) (All Z, (q1 (f Z))) (-. (r1 T_5)) (-. (Ex X, (Ex Y, (((p1 (f Y)) => ((p1 X) /\ ((r1 Y) => ((r1 T_4) /\ (r1 T_5))))) /\ (q1 X))))) ### NotAnd 65 66 % 0.22/0.48 68. (-. (Ex Y, (((p1 (f Y)) => ((p1 (f zenon_X0)) /\ ((r1 Y) => ((r1 T_4) /\ (r1 T_5))))) /\ (q1 (f zenon_X0))))) (-. (Ex X, (Ex Y, (((p1 (f Y)) => ((p1 X) /\ ((r1 Y) => ((r1 T_4) /\ (r1 T_5))))) /\ (q1 X))))) (-. (r1 T_5)) (All Z, (q1 (f Z))) (q1 (f zenon_X0)) ### NotExists 67 % 0.22/0.48 69. (-. ((r1 T_4) /\ (r1 T_5))) (q1 (f zenon_X0)) (All Z, (q1 (f Z))) (-. (Ex X, (Ex Y, (((p1 (f Y)) => ((p1 X) /\ ((r1 Y) => ((r1 T_4) /\ (r1 T_5))))) /\ (q1 X))))) (-. (Ex Y, (((p1 (f Y)) => ((p1 (f zenon_X0)) /\ ((r1 Y) => ((r1 T_4) /\ (r1 T_5))))) /\ (q1 (f zenon_X0))))) ### NotAnd 54 68 % 0.22/0.48 70. (-. ((r1 zenon_X6) => ((r1 T_4) /\ (r1 T_5)))) (-. (Ex Y, (((p1 (f Y)) => ((p1 (f zenon_X0)) /\ ((r1 Y) => ((r1 T_4) /\ (r1 T_5))))) /\ (q1 (f zenon_X0))))) (-. (Ex X, (Ex Y, (((p1 (f Y)) => ((p1 X) /\ ((r1 Y) => ((r1 T_4) /\ (r1 T_5))))) /\ (q1 X))))) (All Z, (q1 (f Z))) (q1 (f zenon_X0)) ### NotImply 69 % 0.22/0.48 71. (-. ((p1 (f zenon_X0)) /\ ((r1 zenon_X6) => ((r1 T_4) /\ (r1 T_5))))) (All Z, (q1 (f Z))) (-. (Ex X, (Ex Y, (((p1 (f Y)) => ((p1 X) /\ ((r1 Y) => ((r1 T_4) /\ (r1 T_5))))) /\ (q1 X))))) (q1 (f zenon_X0)) (-. (Ex Y, (((p1 (f Y)) => ((p1 (f zenon_X0)) /\ ((r1 Y) => ((r1 T_4) /\ (r1 T_5))))) /\ (q1 (f zenon_X0))))) ### NotAnd 40 70 % 0.22/0.48 72. (-. ((p1 (f zenon_X6)) => ((p1 (f zenon_X0)) /\ ((r1 zenon_X6) => ((r1 T_4) /\ (r1 T_5)))))) (-. (Ex Y, (((p1 (f Y)) => ((p1 (f zenon_X0)) /\ ((r1 Y) => ((r1 T_4) /\ (r1 T_5))))) /\ (q1 (f zenon_X0))))) (q1 (f zenon_X0)) (-. (Ex X, (Ex Y, (((p1 (f Y)) => ((p1 X) /\ ((r1 Y) => ((r1 T_4) /\ (r1 T_5))))) /\ (q1 X))))) (All Z, (q1 (f Z))) ### NotImply 71 % 0.22/0.48 73. (q1 (f zenon_X0)) (-. (q1 (f zenon_X0))) ### Axiom % 0.22/0.48 74. (-. (((p1 (f zenon_X6)) => ((p1 (f zenon_X0)) /\ ((r1 zenon_X6) => ((r1 T_4) /\ (r1 T_5))))) /\ (q1 (f zenon_X0)))) (All Z, (q1 (f Z))) (-. (Ex X, (Ex Y, (((p1 (f Y)) => ((p1 X) /\ ((r1 Y) => ((r1 T_4) /\ (r1 T_5))))) /\ (q1 X))))) (q1 (f zenon_X0)) (-. (Ex Y, (((p1 (f Y)) => ((p1 (f zenon_X0)) /\ ((r1 Y) => ((r1 T_4) /\ (r1 T_5))))) /\ (q1 (f zenon_X0))))) ### NotAnd 72 73 % 0.22/0.48 75. (-. (Ex Y, (((p1 (f Y)) => ((p1 (f zenon_X0)) /\ ((r1 Y) => ((r1 T_4) /\ (r1 T_5))))) /\ (q1 (f zenon_X0))))) (q1 (f zenon_X0)) (-. (Ex X, (Ex Y, (((p1 (f Y)) => ((p1 X) /\ ((r1 Y) => ((r1 T_4) /\ (r1 T_5))))) /\ (q1 X))))) (All Z, (q1 (f Z))) ### NotExists 74 % 0.22/0.48 76. (All Z, (q1 (f Z))) (-. (Ex X, (Ex Y, (((p1 (f Y)) => ((p1 X) /\ ((r1 Y) => ((r1 T_4) /\ (r1 T_5))))) /\ (q1 X))))) (q1 (f zenon_X0)) ### NotExists 75 % 0.22/0.48 77. (-. (Ex X, (Ex Y, (((p1 (f Y)) => ((p1 X) /\ ((r1 Y) => ((r1 T_4) /\ (r1 T_5))))) /\ (q1 X))))) (All Z, (q1 (f Z))) ### All 76 % 0.22/0.48 78. (-. ((All Z, (q1 (f Z))) => (Ex X, (Ex Y, (((p1 (f Y)) => ((p1 X) /\ ((r1 Y) => ((r1 T_4) /\ (r1 T_5))))) /\ (q1 X)))))) ### NotImply 77 % 0.22/0.48 79. (-. (All C, ((All Z, (q1 (f Z))) => (Ex X, (Ex Y, (((p1 (f Y)) => ((p1 X) /\ ((r1 Y) => ((r1 T_4) /\ (r1 C))))) /\ (q1 X))))))) ### NotAllEx 78 % 0.22/0.48 80. (-. (All B, (All C, ((All Z, (q1 (f Z))) => (Ex X, (Ex Y, (((p1 (f Y)) => ((p1 X) /\ ((r1 Y) => ((r1 B) /\ (r1 C))))) /\ (q1 X)))))))) ### NotAllEx 79 % 0.22/0.48 81. (-. (p1 (f T_7))) (p1 (f T_7)) ### Axiom % 0.22/0.48 82. (-. ((p1 (f T_7)) => ((p1 (f T_7)) /\ ((r1 T_7) => ((r1 T_7) /\ (r1 T_8)))))) (-. (p1 (f T_7))) ### NotImply 81 % 0.22/0.48 83. (q1 (f T_7)) (-. (q1 (f T_7))) ### Axiom % 0.22/0.48 84. (-. (((p1 (f T_7)) => ((p1 (f T_7)) /\ ((r1 T_7) => ((r1 T_7) /\ (r1 T_8))))) /\ (q1 (f T_7)))) (q1 (f T_7)) (-. (p1 (f T_7))) ### NotAnd 82 83 % 0.22/0.48 85. (-. (Ex Y, (((p1 (f Y)) => ((p1 (f T_7)) /\ ((r1 Y) => ((r1 T_7) /\ (r1 T_8))))) /\ (q1 (f T_7))))) (-. (p1 (f T_7))) (q1 (f T_7)) ### NotExists 84 % 0.22/0.48 86. (p1 (f T_7)) (-. (p1 (f T_7))) ### Axiom % 0.22/0.48 87. (-. (r1 T_7)) (r1 T_7) ### Axiom % 0.22/0.48 88. (-. ((r1 T_7) => ((r1 T_7) /\ (r1 T_8)))) (-. (r1 T_7)) ### NotImply 87 % 0.22/0.48 89. (-. ((p1 (f T_7)) /\ ((r1 T_7) => ((r1 T_7) /\ (r1 T_8))))) (-. (r1 T_7)) (p1 (f T_7)) ### NotAnd 86 88 % 0.22/0.48 90. (-. ((p1 (f T_7)) => ((p1 (f T_7)) /\ ((r1 T_7) => ((r1 T_7) /\ (r1 T_8)))))) (-. (r1 T_7)) ### NotImply 89 % 0.22/0.48 91. (q1 (f T_7)) (-. (q1 (f T_7))) ### Axiom % 0.22/0.48 92. (-. (((p1 (f T_7)) => ((p1 (f T_7)) /\ ((r1 T_7) => ((r1 T_7) /\ (r1 T_8))))) /\ (q1 (f T_7)))) (q1 (f T_7)) (-. (r1 T_7)) ### NotAnd 90 91 % 0.22/0.48 93. (-. (Ex Y, (((p1 (f Y)) => ((p1 (f T_7)) /\ ((r1 Y) => ((r1 T_7) /\ (r1 T_8))))) /\ (q1 (f T_7))))) (-. (r1 T_7)) (q1 (f T_7)) ### NotExists 92 % 0.22/0.48 94. (-. (r1 T_8)) (r1 T_8) ### Axiom % 0.22/0.48 95. (-. ((r1 T_8) => ((r1 T_7) /\ (r1 T_8)))) (-. (r1 T_8)) ### NotImply 94 % 0.22/0.48 96. (-. ((p1 (f T_7)) /\ ((r1 T_8) => ((r1 T_7) /\ (r1 T_8))))) (-. (r1 T_8)) (q1 (f T_7)) (-. (Ex Y, (((p1 (f Y)) => ((p1 (f T_7)) /\ ((r1 Y) => ((r1 T_7) /\ (r1 T_8))))) /\ (q1 (f T_7))))) ### NotAnd 85 95 % 0.22/0.48 97. (-. ((p1 (f T_8)) => ((p1 (f T_7)) /\ ((r1 T_8) => ((r1 T_7) /\ (r1 T_8)))))) (-. (Ex Y, (((p1 (f Y)) => ((p1 (f T_7)) /\ ((r1 Y) => ((r1 T_7) /\ (r1 T_8))))) /\ (q1 (f T_7))))) (q1 (f T_7)) (-. (r1 T_8)) ### NotImply 96 % 0.22/0.48 98. (q1 (f T_7)) (-. (q1 (f T_7))) ### Axiom % 0.22/0.48 99. (-. (((p1 (f T_8)) => ((p1 (f T_7)) /\ ((r1 T_8) => ((r1 T_7) /\ (r1 T_8))))) /\ (q1 (f T_7)))) (-. (r1 T_8)) (q1 (f T_7)) (-. (Ex Y, (((p1 (f Y)) => ((p1 (f T_7)) /\ ((r1 Y) => ((r1 T_7) /\ (r1 T_8))))) /\ (q1 (f T_7))))) ### NotAnd 97 98 % 0.22/0.48 100. (-. (Ex Y, (((p1 (f Y)) => ((p1 (f T_7)) /\ ((r1 Y) => ((r1 T_7) /\ (r1 T_8))))) /\ (q1 (f T_7))))) (q1 (f T_7)) (-. (r1 T_8)) ### NotExists 99 % 0.22/0.48 101. (-. ((r1 T_7) /\ (r1 T_8))) (q1 (f T_7)) (-. (Ex Y, (((p1 (f Y)) => ((p1 (f T_7)) /\ ((r1 Y) => ((r1 T_7) /\ (r1 T_8))))) /\ (q1 (f T_7))))) ### NotAnd 93 100 % 0.22/0.48 102. (-. ((r1 zenon_X9) => ((r1 T_7) /\ (r1 T_8)))) (-. (Ex Y, (((p1 (f Y)) => ((p1 (f T_7)) /\ ((r1 Y) => ((r1 T_7) /\ (r1 T_8))))) /\ (q1 (f T_7))))) (q1 (f T_7)) ### NotImply 101 % 0.22/0.48 103. (-. ((p1 (f T_7)) /\ ((r1 zenon_X9) => ((r1 T_7) /\ (r1 T_8))))) (q1 (f T_7)) (-. (Ex Y, (((p1 (f Y)) => ((p1 (f T_7)) /\ ((r1 Y) => ((r1 T_7) /\ (r1 T_8))))) /\ (q1 (f T_7))))) ### NotAnd 85 102 % 0.22/0.48 104. (-. ((p1 (f zenon_X9)) => ((p1 (f T_7)) /\ ((r1 zenon_X9) => ((r1 T_7) /\ (r1 T_8)))))) (-. (Ex Y, (((p1 (f Y)) => ((p1 (f T_7)) /\ ((r1 Y) => ((r1 T_7) /\ (r1 T_8))))) /\ (q1 (f T_7))))) (q1 (f T_7)) ### NotImply 103 % 0.22/0.48 105. (q1 (f T_7)) (-. (q1 (f T_7))) ### Axiom % 0.22/0.48 106. (-. (((p1 (f zenon_X9)) => ((p1 (f T_7)) /\ ((r1 zenon_X9) => ((r1 T_7) /\ (r1 T_8))))) /\ (q1 (f T_7)))) (q1 (f T_7)) (-. (Ex Y, (((p1 (f Y)) => ((p1 (f T_7)) /\ ((r1 Y) => ((r1 T_7) /\ (r1 T_8))))) /\ (q1 (f T_7))))) ### NotAnd 104 105 % 0.22/0.48 107. (-. (Ex Y, (((p1 (f Y)) => ((p1 (f T_7)) /\ ((r1 Y) => ((r1 T_7) /\ (r1 T_8))))) /\ (q1 (f T_7))))) (q1 (f T_7)) ### NotExists 106 % 0.22/0.48 108. (-. (Ex X, (Ex Y, (((p1 (f Y)) => ((p1 X) /\ ((r1 Y) => ((r1 T_7) /\ (r1 T_8))))) /\ (q1 X))))) (q1 (f T_7)) ### NotExists 107 % 0.22/0.48 109. (-. ((q1 (f T_7)) => (Ex X, (Ex Y, (((p1 (f Y)) => ((p1 X) /\ ((r1 Y) => ((r1 T_7) /\ (r1 T_8))))) /\ (q1 X)))))) ### NotImply 108 % 0.22/0.48 110. (-. (All C, ((q1 (f T_7)) => (Ex X, (Ex Y, (((p1 (f Y)) => ((p1 X) /\ ((r1 Y) => ((r1 T_7) /\ (r1 C))))) /\ (q1 X))))))) ### NotAllEx 109 % 0.22/0.48 111. (-. (All B, (All C, ((q1 (f B)) => (Ex X, (Ex Y, (((p1 (f Y)) => ((p1 X) /\ ((r1 Y) => ((r1 B) /\ (r1 C))))) /\ (q1 X)))))))) ### NotAllEx 110 % 0.22/0.48 112. (a1 T_10) (-. (a1 T_10)) ### Axiom % 0.22/0.48 113. (-. (b T_10)) (b T_10) ### Axiom % 0.22/0.48 114. (a1 T_10) (-. (a1 T_10)) ### Axiom % 0.22/0.48 115. (c T_10) (-. (c T_10)) ### Axiom % 0.22/0.48 116. (-. ((a1 T_10) /\ (c T_10))) (c T_10) (a1 T_10) ### NotAnd 114 115 % 0.22/0.48 117. (-. (Ex X, ((a1 X) /\ (c X)))) (a1 T_10) (c T_10) ### NotExists 116 % 0.22/0.50 118. ((a1 T_10) => ((b T_10) \/ (c T_10))) (-. (Ex X, ((a1 X) /\ (c X)))) (-. (b T_10)) (a1 T_10) ### DisjTree 112 113 117 % 0.22/0.50 119. (All X, ((a1 X) => ((b X) \/ (c X)))) (a1 T_10) (-. (b T_10)) (-. (Ex X, ((a1 X) /\ (c X)))) ### All 118 % 0.22/0.50 120. (-. ((a1 T_10) => (b T_10))) (-. (Ex X, ((a1 X) /\ (c X)))) (All X, ((a1 X) => ((b X) \/ (c X)))) ### NotImply 119 % 0.22/0.50 121. (-. (All X, ((a1 X) => (b X)))) (All X, ((a1 X) => ((b X) \/ (c X)))) (-. (Ex X, ((a1 X) /\ (c X)))) ### NotAllEx 120 % 0.22/0.50 122. (-. (((All X, ((a1 X) => ((b X) \/ (c X)))) /\ (-. (All X, ((a1 X) => (b X))))) => (Ex X, ((a1 X) /\ (c X))))) ### ConjTree 121 % 0.22/0.50 123. (e T_11) (-. (e T_11)) ### Axiom % 0.22/0.50 124. (p1 T_11) (-. (p1 T_11)) ### Axiom % 0.22/0.50 125. (g T_11) (-. (g T_11)) ### Axiom % 0.22/0.50 126. (-. ((p1 T_11) /\ (g T_11))) (g T_11) (p1 T_11) ### NotAnd 124 125 % 0.22/0.50 127. (-. (((p1 T_11) /\ ((e T_11) /\ (((e T_11) => ((g T_11) \/ (s T_11 (f T_11)))) /\ (((e zenon_X12) => ((g zenon_X12) \/ (c (f zenon_X12)))) /\ ((s T_11 zenon_X13) => (p1 zenon_X13)))))) => (((p1 T_11) /\ (g T_11)) \/ ((p1 zenon_X14) /\ (c zenon_X14))))) (p1 T_11) (g T_11) ### ConjTree 126 % 0.22/0.50 128. (-. (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e T_11) => ((g T_11) \/ (s T_11 (f T_11)))) /\ (((e zenon_X12) => ((g zenon_X12) \/ (c (f zenon_X12)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 T_11) /\ (g T_11)) \/ ((p1 zenon_X14) /\ (c zenon_X14)))))) (g T_11) (p1 T_11) ### NotExists 127 % 0.22/0.50 129. (-. (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e T_11) => ((g T_11) \/ (s T_11 (f T_11)))) /\ (((e zenon_X12) => ((g zenon_X12) \/ (c (f zenon_X12)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 T_11) /\ (g T_11)) \/ ((p1 X4) /\ (c X4))))))) (p1 T_11) (g T_11) ### NotExists 128 % 0.22/0.50 130. (-. (Ex X3, (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e T_11) => ((g T_11) \/ (s T_11 (f T_11)))) /\ (((e zenon_X12) => ((g zenon_X12) \/ (c (f zenon_X12)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 X3) /\ (g X3)) \/ ((p1 X4) /\ (c X4)))))))) (g T_11) (p1 T_11) ### NotExists 129 % 0.22/0.50 131. (e T_11) (-. (e T_11)) ### Axiom % 0.22/0.50 132. (-. (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e T_11) => ((g T_11) \/ (c (f T_11)))) /\ ((s T_11 zenon_X16) => (p1 zenon_X16)))))) => (((p1 T_11) /\ (g T_11)) \/ ((p1 zenon_X17) /\ (c zenon_X17))))) (p1 T_11) (g T_11) ### ConjTree 126 % 0.22/0.50 133. (-. (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e T_11) => ((g T_11) \/ (c (f T_11)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 T_11) /\ (g T_11)) \/ ((p1 zenon_X17) /\ (c zenon_X17)))))) (g T_11) (p1 T_11) ### NotExists 132 % 0.22/0.50 134. (-. (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e T_11) => ((g T_11) \/ (c (f T_11)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 T_11) /\ (g T_11)) \/ ((p1 X4) /\ (c X4))))))) (p1 T_11) (g T_11) ### NotExists 133 % 0.22/0.50 135. (-. (Ex X3, (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e T_11) => ((g T_11) \/ (c (f T_11)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 X3) /\ (g X3)) \/ ((p1 X4) /\ (c X4)))))))) (g T_11) (p1 T_11) ### NotExists 134 % 0.22/0.50 136. (s T_11 (f T_11)) (-. (s T_11 (f T_11))) ### Axiom % 0.22/0.50 137. (-. (p1 (f T_11))) (p1 (f T_11)) ### Axiom % 0.22/0.50 138. ((s T_11 (f T_11)) => (p1 (f T_11))) (-. (p1 (f T_11))) (s T_11 (f T_11)) ### Imply 136 137 % 0.22/0.50 139. (-. (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e zenon_X18) => ((g zenon_X18) \/ (c (f zenon_X18)))) /\ ((s T_11 (f T_11)) => (p1 (f T_11))))))) => (((p1 zenon_X19) /\ (g zenon_X19)) \/ ((p1 (f zenon_X18)) /\ (c (f zenon_X18)))))) (s T_11 (f T_11)) (-. (p1 (f T_11))) ### ConjTree 138 % 0.22/0.50 140. (-. (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e zenon_X18) => ((g zenon_X18) \/ (c (f zenon_X18)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 zenon_X19) /\ (g zenon_X19)) \/ ((p1 (f zenon_X18)) /\ (c (f zenon_X18))))))) (-. (p1 (f T_11))) (s T_11 (f T_11)) ### NotExists 139 % 0.22/0.50 141. (c (f T_11)) (-. (c (f T_11))) ### Axiom % 0.22/0.50 142. (-. ((p1 (f T_11)) /\ (c (f T_11)))) (c (f T_11)) (s T_11 (f T_11)) (-. (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e zenon_X18) => ((g zenon_X18) \/ (c (f zenon_X18)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 zenon_X19) /\ (g zenon_X19)) \/ ((p1 (f zenon_X18)) /\ (c (f zenon_X18))))))) ### NotAnd 140 141 % 0.22/0.50 143. (-. (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e T_11) => ((g T_11) \/ (c (f T_11)))) /\ ((s T_11 zenon_X20) => (p1 zenon_X20)))))) => (((p1 zenon_X21) /\ (g zenon_X21)) \/ ((p1 (f T_11)) /\ (c (f T_11)))))) (-. (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e zenon_X18) => ((g zenon_X18) \/ (c (f zenon_X18)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 zenon_X19) /\ (g zenon_X19)) \/ ((p1 (f zenon_X18)) /\ (c (f zenon_X18))))))) (s T_11 (f T_11)) (c (f T_11)) ### ConjTree 142 % 0.22/0.50 144. (-. (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e T_11) => ((g T_11) \/ (c (f T_11)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 zenon_X21) /\ (g zenon_X21)) \/ ((p1 (f T_11)) /\ (c (f T_11))))))) (c (f T_11)) (s T_11 (f T_11)) (-. (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e zenon_X18) => ((g zenon_X18) \/ (c (f zenon_X18)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 zenon_X19) /\ (g zenon_X19)) \/ ((p1 (f zenon_X18)) /\ (c (f zenon_X18))))))) ### NotExists 143 % 0.22/0.50 145. (-. (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e T_11) => ((g T_11) \/ (c (f T_11)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 zenon_X21) /\ (g zenon_X21)) \/ ((p1 X4) /\ (c X4))))))) (-. (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e zenon_X18) => ((g zenon_X18) \/ (c (f zenon_X18)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 zenon_X19) /\ (g zenon_X19)) \/ ((p1 (f zenon_X18)) /\ (c (f zenon_X18))))))) (s T_11 (f T_11)) (c (f T_11)) ### NotExists 144 % 0.22/0.50 146. ((e T_11) => ((g T_11) \/ (c (f T_11)))) (s T_11 (f T_11)) (-. (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e zenon_X18) => ((g zenon_X18) \/ (c (f zenon_X18)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 zenon_X19) /\ (g zenon_X19)) \/ ((p1 (f zenon_X18)) /\ (c (f zenon_X18))))))) (-. (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e T_11) => ((g T_11) \/ (c (f T_11)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 zenon_X21) /\ (g zenon_X21)) \/ ((p1 X4) /\ (c X4))))))) (p1 T_11) (-. (Ex X3, (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e T_11) => ((g T_11) \/ (c (f T_11)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 X3) /\ (g X3)) \/ ((p1 X4) /\ (c X4)))))))) (e T_11) ### DisjTree 131 135 145 % 0.22/0.50 147. (-. (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e T_11) => ((g T_11) \/ (c (f T_11)))) /\ ((s T_11 zenon_X22) => (p1 zenon_X22)))))) => (((p1 zenon_X21) /\ (g zenon_X21)) \/ ((p1 zenon_X23) /\ (c zenon_X23))))) (e T_11) (-. (Ex X3, (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e T_11) => ((g T_11) \/ (c (f T_11)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 X3) /\ (g X3)) \/ ((p1 X4) /\ (c X4)))))))) (p1 T_11) (-. (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e T_11) => ((g T_11) \/ (c (f T_11)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 zenon_X21) /\ (g zenon_X21)) \/ ((p1 X4) /\ (c X4))))))) (-. (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e zenon_X18) => ((g zenon_X18) \/ (c (f zenon_X18)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 zenon_X19) /\ (g zenon_X19)) \/ ((p1 (f zenon_X18)) /\ (c (f zenon_X18))))))) (s T_11 (f T_11)) ### ConjTree 146 % 0.22/0.51 148. (-. (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e T_11) => ((g T_11) \/ (c (f T_11)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 zenon_X21) /\ (g zenon_X21)) \/ ((p1 zenon_X23) /\ (c zenon_X23)))))) (s T_11 (f T_11)) (-. (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e zenon_X18) => ((g zenon_X18) \/ (c (f zenon_X18)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 zenon_X19) /\ (g zenon_X19)) \/ ((p1 (f zenon_X18)) /\ (c (f zenon_X18))))))) (-. (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e T_11) => ((g T_11) \/ (c (f T_11)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 zenon_X21) /\ (g zenon_X21)) \/ ((p1 X4) /\ (c X4))))))) (p1 T_11) (-. (Ex X3, (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e T_11) => ((g T_11) \/ (c (f T_11)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 X3) /\ (g X3)) \/ ((p1 X4) /\ (c X4)))))))) (e T_11) ### NotExists 147 % 0.22/0.51 149. (e T_11) (-. (Ex X3, (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e T_11) => ((g T_11) \/ (c (f T_11)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 X3) /\ (g X3)) \/ ((p1 X4) /\ (c X4)))))))) (p1 T_11) (-. (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e T_11) => ((g T_11) \/ (c (f T_11)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 zenon_X21) /\ (g zenon_X21)) \/ ((p1 X4) /\ (c X4))))))) (-. (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e zenon_X18) => ((g zenon_X18) \/ (c (f zenon_X18)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 zenon_X19) /\ (g zenon_X19)) \/ ((p1 (f zenon_X18)) /\ (c (f zenon_X18))))))) (s T_11 (f T_11)) ### NotExists 148 % 0.22/0.51 150. (s T_11 (f T_11)) (-. (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e zenon_X18) => ((g zenon_X18) \/ (c (f zenon_X18)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 zenon_X19) /\ (g zenon_X19)) \/ ((p1 (f zenon_X18)) /\ (c (f zenon_X18))))))) (p1 T_11) (-. (Ex X3, (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e T_11) => ((g T_11) \/ (c (f T_11)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 X3) /\ (g X3)) \/ ((p1 X4) /\ (c X4)))))))) (e T_11) ### NotExists 149 % 0.22/0.51 151. (-. (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 X3) /\ (g X3)) \/ ((p1 X4) /\ (c X4))))))))) (e T_11) (p1 T_11) (-. (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e zenon_X18) => ((g zenon_X18) \/ (c (f zenon_X18)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 zenon_X19) /\ (g zenon_X19)) \/ ((p1 (f zenon_X18)) /\ (c (f zenon_X18))))))) (s T_11 (f T_11)) ### NotExists 150 % 0.22/0.51 152. ((e T_11) => ((g T_11) \/ (s T_11 (f T_11)))) (-. (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e zenon_X18) => ((g zenon_X18) \/ (c (f zenon_X18)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 zenon_X19) /\ (g zenon_X19)) \/ ((p1 (f zenon_X18)) /\ (c (f zenon_X18))))))) (-. (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 X3) /\ (g X3)) \/ ((p1 X4) /\ (c X4))))))))) (p1 T_11) (-. (Ex X3, (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e T_11) => ((g T_11) \/ (s T_11 (f T_11)))) /\ (((e zenon_X12) => ((g zenon_X12) \/ (c (f zenon_X12)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 X3) /\ (g X3)) \/ ((p1 X4) /\ (c X4)))))))) (e T_11) ### DisjTree 123 130 151 % 0.22/0.51 153. (-. (((p1 T_11) /\ ((e T_11) /\ (((e T_11) => ((g T_11) \/ (s T_11 (f T_11)))) /\ (((e zenon_X12) => ((g zenon_X12) \/ (c (f zenon_X12)))) /\ ((s T_11 zenon_X24) => (p1 zenon_X24)))))) => (((p1 zenon_X25) /\ (g zenon_X25)) \/ ((p1 zenon_X26) /\ (c zenon_X26))))) (e T_11) (-. (Ex X3, (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e T_11) => ((g T_11) \/ (s T_11 (f T_11)))) /\ (((e zenon_X12) => ((g zenon_X12) \/ (c (f zenon_X12)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 X3) /\ (g X3)) \/ ((p1 X4) /\ (c X4)))))))) (p1 T_11) (-. (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 X3) /\ (g X3)) \/ ((p1 X4) /\ (c X4))))))))) (-. (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e zenon_X18) => ((g zenon_X18) \/ (c (f zenon_X18)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 zenon_X19) /\ (g zenon_X19)) \/ ((p1 (f zenon_X18)) /\ (c (f zenon_X18))))))) ### ConjTree 152 % 0.22/0.51 154. (-. (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e T_11) => ((g T_11) \/ (s T_11 (f T_11)))) /\ (((e zenon_X12) => ((g zenon_X12) \/ (c (f zenon_X12)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 zenon_X25) /\ (g zenon_X25)) \/ ((p1 zenon_X26) /\ (c zenon_X26)))))) (-. (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e zenon_X18) => ((g zenon_X18) \/ (c (f zenon_X18)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 zenon_X19) /\ (g zenon_X19)) \/ ((p1 (f zenon_X18)) /\ (c (f zenon_X18))))))) (-. (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 X3) /\ (g X3)) \/ ((p1 X4) /\ (c X4))))))))) (p1 T_11) (-. (Ex X3, (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e T_11) => ((g T_11) \/ (s T_11 (f T_11)))) /\ (((e zenon_X12) => ((g zenon_X12) \/ (c (f zenon_X12)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 X3) /\ (g X3)) \/ ((p1 X4) /\ (c X4)))))))) (e T_11) ### NotExists 153 % 0.22/0.51 155. (-. (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e T_11) => ((g T_11) \/ (s T_11 (f T_11)))) /\ (((e zenon_X12) => ((g zenon_X12) \/ (c (f zenon_X12)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 zenon_X25) /\ (g zenon_X25)) \/ ((p1 X4) /\ (c X4))))))) (e T_11) (-. (Ex X3, (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e T_11) => ((g T_11) \/ (s T_11 (f T_11)))) /\ (((e zenon_X12) => ((g zenon_X12) \/ (c (f zenon_X12)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 X3) /\ (g X3)) \/ ((p1 X4) /\ (c X4)))))))) (p1 T_11) (-. (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 X3) /\ (g X3)) \/ ((p1 X4) /\ (c X4))))))))) (-. (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e zenon_X18) => ((g zenon_X18) \/ (c (f zenon_X18)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 zenon_X19) /\ (g zenon_X19)) \/ ((p1 (f zenon_X18)) /\ (c (f zenon_X18))))))) ### NotExists 154 % 0.22/0.51 156. (-. (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e zenon_X18) => ((g zenon_X18) \/ (c (f zenon_X18)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 zenon_X19) /\ (g zenon_X19)) \/ ((p1 (f zenon_X18)) /\ (c (f zenon_X18))))))) (-. (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 X3) /\ (g X3)) \/ ((p1 X4) /\ (c X4))))))))) (p1 T_11) (-. (Ex X3, (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e T_11) => ((g T_11) \/ (s T_11 (f T_11)))) /\ (((e zenon_X12) => ((g zenon_X12) \/ (c (f zenon_X12)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 X3) /\ (g X3)) \/ ((p1 X4) /\ (c X4)))))))) (e T_11) ### NotExists 155 % 0.22/0.51 157. (-. (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e T_11) => ((g T_11) \/ (s T_11 (f T_11)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 X3) /\ (g X3)) \/ ((p1 X4) /\ (c X4))))))))) (e T_11) (p1 T_11) (-. (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 X3) /\ (g X3)) \/ ((p1 X4) /\ (c X4))))))))) (-. (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e zenon_X18) => ((g zenon_X18) \/ (c (f zenon_X18)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 zenon_X19) /\ (g zenon_X19)) \/ ((p1 (f zenon_X18)) /\ (c (f zenon_X18))))))) ### NotExists 156 % 0.22/0.51 158. (-. (Ex X, (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e X) => ((g X) \/ (s X (f X)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 X3) /\ (g X3)) \/ ((p1 X4) /\ (c X4)))))))))) (-. (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e zenon_X18) => ((g zenon_X18) \/ (c (f zenon_X18)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 zenon_X19) /\ (g zenon_X19)) \/ ((p1 (f zenon_X18)) /\ (c (f zenon_X18))))))) (-. (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 X3) /\ (g X3)) \/ ((p1 X4) /\ (c X4))))))))) (p1 T_11) (e T_11) ### NotExists 157 % 0.22/0.51 159. (-. (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e zenon_X18) => ((g zenon_X18) \/ (c (f zenon_X18)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 zenon_X19) /\ (g zenon_X19)) \/ ((p1 X4) /\ (c X4))))))) (e T_11) (p1 T_11) (-. (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 X3) /\ (g X3)) \/ ((p1 X4) /\ (c X4))))))))) (-. (Ex X, (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e X) => ((g X) \/ (s X (f X)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 X3) /\ (g X3)) \/ ((p1 X4) /\ (c X4)))))))))) ### NotExists 158 % 0.22/0.51 160. (-. (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e zenon_X18) => ((g zenon_X18) \/ (c (f zenon_X18)))) /\ ((s T_11 zenon_X27) => (p1 zenon_X27)))))) => (((p1 zenon_X19) /\ (g zenon_X19)) \/ ((p1 zenon_X28) /\ (c zenon_X28))))) (-. (Ex X, (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e X) => ((g X) \/ (s X (f X)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 X3) /\ (g X3)) \/ ((p1 X4) /\ (c X4)))))))))) (-. (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 X3) /\ (g X3)) \/ ((p1 X4) /\ (c X4))))))))) (-. (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e zenon_X18) => ((g zenon_X18) \/ (c (f zenon_X18)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 zenon_X19) /\ (g zenon_X19)) \/ ((p1 X4) /\ (c X4))))))) ### ConjTree 159 % 0.22/0.51 161. (-. (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e zenon_X18) => ((g zenon_X18) \/ (c (f zenon_X18)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 zenon_X19) /\ (g zenon_X19)) \/ ((p1 zenon_X28) /\ (c zenon_X28)))))) (-. (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e zenon_X18) => ((g zenon_X18) \/ (c (f zenon_X18)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 zenon_X19) /\ (g zenon_X19)) \/ ((p1 X4) /\ (c X4))))))) (-. (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 X3) /\ (g X3)) \/ ((p1 X4) /\ (c X4))))))))) (-. (Ex X, (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e X) => ((g X) \/ (s X (f X)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 X3) /\ (g X3)) \/ ((p1 X4) /\ (c X4)))))))))) ### NotExists 160 % 0.22/0.51 162. (-. (Ex X, (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e X) => ((g X) \/ (s X (f X)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 X3) /\ (g X3)) \/ ((p1 X4) /\ (c X4)))))))))) (-. (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 X3) /\ (g X3)) \/ ((p1 X4) /\ (c X4))))))))) (-. (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e zenon_X18) => ((g zenon_X18) \/ (c (f zenon_X18)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 zenon_X19) /\ (g zenon_X19)) \/ ((p1 X4) /\ (c X4))))))) ### NotExists 161 % 0.22/0.51 163. (-. (Ex X3, (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e zenon_X18) => ((g zenon_X18) \/ (c (f zenon_X18)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 X3) /\ (g X3)) \/ ((p1 X4) /\ (c X4)))))))) (-. (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 X3) /\ (g X3)) \/ ((p1 X4) /\ (c X4))))))))) (-. (Ex X, (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e X) => ((g X) \/ (s X (f X)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 X3) /\ (g X3)) \/ ((p1 X4) /\ (c X4)))))))))) ### NotExists 162 % 0.22/0.51 164. (-. (Ex X, (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e X) => ((g X) \/ (s X (f X)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 X3) /\ (g X3)) \/ ((p1 X4) /\ (c X4)))))))))) (-. (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e zenon_X15) => ((g zenon_X15) \/ (s zenon_X15 (f zenon_X15)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 X3) /\ (g X3)) \/ ((p1 X4) /\ (c X4))))))))) ### NotExists 163 % 0.22/0.51 165. (-. (Ex X, (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p1 T_11) /\ ((e T_11) /\ (((e X) => ((g X) \/ (s X (f X)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_11 Y) => (p1 Y)))))) => (((p1 X3) /\ (g X3)) \/ ((p1 X4) /\ (c X4)))))))))) ### NotExists 164 % 0.22/0.51 166. (-. (All A, (Ex X, (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p1 A) /\ ((e A) /\ (((e X) => ((g X) \/ (s X (f X)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s A Y) => (p1 Y)))))) => (((p1 X3) /\ (g X3)) \/ ((p1 X4) /\ (c X4))))))))))) ### NotAllEx 165 % 0.22/0.51 167. (s1 T_29) (-. (s1 T_29)) ### Axiom % 0.22/0.51 168. (-. (p1 T_29)) (p1 T_29) ### Axiom % 0.22/0.51 169. ((s1 T_29) => (p1 T_29)) (-. (p1 T_29)) (s1 T_29) ### Imply 167 168 % 0.22/0.51 170. (All X, ((s1 X) => (p1 X))) (s1 T_29) (-. (p1 T_29)) ### All 169 % 0.22/0.51 171. (r T_29 T_30) (-. (r T_29 T_30)) ### Axiom % 0.22/0.51 172. (-. (q T_29 T_30)) (q T_29 T_30) ### Axiom % 0.22/0.51 173. ((r T_29 T_30) => (q T_29 T_30)) (-. (q T_29 T_30)) (r T_29 T_30) ### Imply 171 172 % 0.22/0.51 174. (All Y, ((r T_29 Y) => (q T_29 Y))) (r T_29 T_30) (-. (q T_29 T_30)) ### All 173 % 0.22/0.51 175. (All X, (All Y, ((r X Y) => (q X Y)))) (-. (q T_29 T_30)) (r T_29 T_30) ### All 174 % 0.22/0.51 176. (-. ((p1 T_29) /\ (q T_29 T_30))) (r T_29 T_30) (All X, (All Y, ((r X Y) => (q X Y)))) (s1 T_29) (All X, ((s1 X) => (p1 X))) ### NotAnd 170 175 % 0.22/0.51 177. (-. (Ex Y, ((p1 T_29) /\ (q T_29 Y)))) (All X, ((s1 X) => (p1 X))) (s1 T_29) (All X, (All Y, ((r X Y) => (q X Y)))) (r T_29 T_30) ### NotExists 176 % 0.22/0.51 178. (-. (Ex X, (Ex Y, ((p1 X) /\ (q X Y))))) (r T_29 T_30) (All X, (All Y, ((r X Y) => (q X Y)))) (s1 T_29) (All X, ((s1 X) => (p1 X))) ### NotExists 177 % 0.22/0.52 179. (-. (((s1 T_31) /\ ((s1 T_29) /\ ((r T_29 T_30) /\ ((All X, ((s1 X) => (p1 X))) /\ (All X, (All Y, ((r X Y) => (q X Y)))))))) => (Ex X, (Ex Y, ((p1 X) /\ (q X Y)))))) ### ConjTree 178 % 0.22/0.52 180. (-. (All C, (((s1 T_31) /\ ((s1 T_29) /\ ((r T_29 C) /\ ((All X, ((s1 X) => (p1 X))) /\ (All X, (All Y, ((r X Y) => (q X Y)))))))) => (Ex X, (Ex Y, ((p1 X) /\ (q X Y))))))) ### NotAllEx 179 % 0.22/0.52 181. (-. (All B, (All C, (((s1 T_31) /\ ((s1 B) /\ ((r B C) /\ ((All X, ((s1 X) => (p1 X))) /\ (All X, (All Y, ((r X Y) => (q X Y)))))))) => (Ex X, (Ex Y, ((p1 X) /\ (q X Y)))))))) ### NotAllEx 180 % 0.22/0.52 182. (-. (All A, (All B, (All C, (((s1 A) /\ ((s1 B) /\ ((r B C) /\ ((All X, ((s1 X) => (p1 X))) /\ (All X, (All Y, ((r X Y) => (q X Y)))))))) => (Ex X, (Ex Y, ((p1 X) /\ (q X Y))))))))) ### NotAllEx 181 % 0.22/0.52 183. (-. (p1 T_32)) (p1 T_32) ### Axiom % 0.22/0.52 184. (All X, (p1 X)) (-. (p1 T_32)) ### All 183 % 0.22/0.52 185. (-. (p1 T_33)) (p1 T_33) ### Axiom % 0.22/0.52 186. (All X, (p1 X)) (-. (p1 T_33)) ### All 185 % 0.22/0.52 187. (-. ((p1 T_32) /\ (p1 T_33))) (All X, (p1 X)) ### NotAnd 184 186 % 0.22/0.52 188. (-. (All B, ((p1 T_32) /\ (p1 B)))) (All X, (p1 X)) ### NotAllEx 187 % 0.22/0.52 189. (-. (All A, (All B, ((p1 A) /\ (p1 B))))) (All X, (p1 X)) ### NotAllEx 188 % 0.22/0.52 190. (-. ((All X, (p1 X)) => (All A, (All B, ((p1 A) /\ (p1 B)))))) ### NotImply 189 % 0.22/0.52 191. (-. (p1 T_34)) (p1 T_34) ### Axiom % 0.22/0.52 192. (All X, (p1 X)) (-. (p1 T_34)) ### All 191 % 0.22/0.52 193. (-. ((p1 T_34) \/ (r1 zenon_X35))) (All X, (p1 X)) ### NotOr 192 % 0.22/0.52 194. (-. (All Y, ((p1 Y) \/ (r1 zenon_X35)))) (All X, (p1 X)) ### NotAllEx 193 % 0.22/0.52 195. (-. (Ex Z, (All Y, ((p1 Y) \/ (r1 Z))))) (All X, (p1 X)) ### NotExists 194 % 0.22/0.52 196. (-. (((All X, (p1 X)) /\ (Ex Y, (q1 Y))) => (Ex Z, (All Y, ((p1 Y) \/ (r1 Z)))))) ### ConjTree 195 % 0.22/0.52 197. (-. (p1 T_34)) (p1 T_34) ### Axiom % 0.22/0.52 198. ((p1 T_34) /\ (q1 T_36)) (-. (p1 T_34)) ### And 197 % 0.22/0.52 199. (Ex Y, ((p1 T_34) /\ (q1 Y))) (-. (p1 T_34)) ### Exists 198 % 0.22/0.52 200. (All X, (Ex Y, ((p1 X) /\ (q1 Y)))) (-. (p1 T_34)) ### All 199 % 0.22/0.52 201. (-. ((p1 T_34) \/ (r1 zenon_X35))) (All X, (Ex Y, ((p1 X) /\ (q1 Y)))) ### NotOr 200 % 0.22/0.52 202. (-. (All Y, ((p1 Y) \/ (r1 zenon_X35)))) (All X, (Ex Y, ((p1 X) /\ (q1 Y)))) ### NotAllEx 201 % 0.22/0.52 203. (-. (Ex Z, (All Y, ((p1 Y) \/ (r1 Z))))) (All X, (Ex Y, ((p1 X) /\ (q1 Y)))) ### NotExists 202 % 0.22/0.52 204. (-. ((All X, (Ex Y, ((p1 X) /\ (q1 Y)))) => (Ex Z, (All Y, ((p1 Y) \/ (r1 Z)))))) ### NotImply 203 % 0.22/0.52 205. (a T_37 T_37) (-. (a T_37 T_37)) ### Axiom % 0.22/0.52 206. (-. (Ex Z, (a Z Z))) (a T_37 T_37) ### NotExists 205 % 0.22/0.52 207. ((a zenon_X38 T_37) /\ (a T_37 T_37)) (-. (Ex Z, (a Z Z))) ### And 206 % 0.22/0.52 208. (Ex Y, ((a zenon_X38 Y) /\ (a Y Y))) (-. (Ex Z, (a Z Z))) ### Exists 207 % 0.22/0.52 209. (All X, (Ex Y, ((a X Y) /\ (a Y Y)))) (-. (Ex Z, (a Z Z))) ### All 208 % 0.22/0.52 210. (-. ((All X, (Ex Y, ((a X Y) /\ (a Y Y)))) => (Ex Z, (a Z Z)))) ### NotImply 209 % 0.22/0.52 211. (-. (p1 T_39)) (p1 T_39) ### Axiom % 0.22/0.52 212. (-. ((p1 T_39) => (p1 T_39))) (-. (p1 T_39)) ### NotImply 211 % 0.22/0.52 213. (-. (p1 T_40)) (p1 T_40) ### Axiom % 0.22/0.52 214. (-. ((p1 T_40) => (p1 T_39))) (-. (p1 T_40)) ### NotImply 213 % 0.22/0.52 215. (-. (q1 T_40)) (q1 T_40) ### Axiom % 0.22/0.52 216. (-. ((q1 T_40) => (p1 T_40))) (-. (q1 T_40)) ### NotImply 215 % 0.22/0.52 217. (-. (((p1 T_40) => (p1 T_39)) /\ ((q1 T_40) => (p1 T_40)))) (-. (q1 T_40)) (-. (p1 T_40)) ### NotAnd 214 216 % 0.22/0.52 218. (-. (Ex X, (((p1 X) => (p1 T_39)) /\ ((q1 X) => (p1 T_40))))) (-. (p1 T_40)) (-. (q1 T_40)) ### NotExists 217 % 0.22/0.52 219. (-. (p1 T_40)) (p1 T_40) ### Axiom % 0.22/0.52 220. ((q1 T_40) => (p1 T_40)) (-. (p1 T_40)) (-. (Ex X, (((p1 X) => (p1 T_39)) /\ ((q1 X) => (p1 T_40))))) ### Imply 218 219 % 0.22/0.52 221. (All Y, ((q1 Y) => (p1 Y))) (-. (Ex X, (((p1 X) => (p1 T_39)) /\ ((q1 X) => (p1 T_40))))) (-. (p1 T_40)) ### All 220 % 0.22/0.52 222. (-. ((q1 T_39) => (p1 T_40))) (-. (Ex X, (((p1 X) => (p1 T_39)) /\ ((q1 X) => (p1 T_40))))) (All Y, ((q1 Y) => (p1 Y))) ### NotImply 221 % 0.22/0.52 223. (-. (((p1 T_39) => (p1 T_39)) /\ ((q1 T_39) => (p1 T_40)))) (All Y, ((q1 Y) => (p1 Y))) (-. (Ex X, (((p1 X) => (p1 T_39)) /\ ((q1 X) => (p1 T_40))))) (-. (p1 T_39)) ### NotAnd 212 222 % 0.22/0.52 224. (-. (p1 T_39)) (-. (Ex X, (((p1 X) => (p1 T_39)) /\ ((q1 X) => (p1 T_40))))) (All Y, ((q1 Y) => (p1 Y))) ### NotExists 223 % 0.22/0.52 225. (-. ((p1 zenon_X41) => (p1 T_39))) (All Y, ((q1 Y) => (p1 Y))) (-. (Ex X, (((p1 X) => (p1 T_39)) /\ ((q1 X) => (p1 T_40))))) ### NotImply 224 % 0.22/0.52 226. (-. ((q1 zenon_X41) => (p1 T_40))) (-. (Ex X, (((p1 X) => (p1 T_39)) /\ ((q1 X) => (p1 T_40))))) (All Y, ((q1 Y) => (p1 Y))) ### NotImply 221 % 0.22/0.52 227. (-. (((p1 zenon_X41) => (p1 T_39)) /\ ((q1 zenon_X41) => (p1 T_40)))) (-. (Ex X, (((p1 X) => (p1 T_39)) /\ ((q1 X) => (p1 T_40))))) (All Y, ((q1 Y) => (p1 Y))) ### NotAnd 225 226 % 0.22/0.52 228. (All Y, ((q1 Y) => (p1 Y))) (-. (Ex X, (((p1 X) => (p1 T_39)) /\ ((q1 X) => (p1 T_40))))) ### NotExists 227 % 0.22/0.52 229. (-. ((All Y, ((q1 Y) => (p1 Y))) => (Ex X, (((p1 X) => (p1 T_39)) /\ ((q1 X) => (p1 T_40)))))) ### NotImply 228 % 0.22/0.52 230. (-. (All B, ((All Y, ((q1 Y) => (p1 Y))) => (Ex X, (((p1 X) => (p1 T_39)) /\ ((q1 X) => (p1 B))))))) ### NotAllEx 229 % 0.22/0.52 231. (-. (All A, (All B, ((All Y, ((q1 Y) => (p1 Y))) => (Ex X, (((p1 X) => (p1 A)) /\ ((q1 X) => (p1 B)))))))) ### NotAllEx 230 % 0.22/0.52 232. (Ex X, (p1 X)) (-. (Ex X, (p1 X))) ### Axiom % 0.22/0.52 233. (-. (-. (b0))) (-. (b0)) ### Axiom % 0.22/0.52 234. (-. ((b0) \/ (-. (b0)))) ### NotOr 233 % 0.22/0.52 235. (-. (q0)) (q0) ### P-NotP % 0.22/0.52 236. (-. ((q0) => (q0))) ### NotImply 235 % 0.22/0.52 237. (-. (((b0) \/ (-. (b0))) /\ ((q0) => (q0)))) ### NotAnd 234 236 % 0.22/0.52 238. (-. ((a0) => (((b0) \/ (-. (b0))) /\ ((q0) => (q0))))) ### NotImply 237 % 0.22/0.52 239. (-. ((Ex X, (p1 X)) /\ ((a0) => (((b0) \/ (-. (b0))) /\ ((q0) => (q0)))))) (Ex X, (p1 X)) ### NotAnd 232 238 % 0.22/0.52 240. (-. ((Ex X, (p1 X)) => ((Ex X, (p1 X)) /\ ((a0) => (((b0) \/ (-. (b0))) /\ ((q0) => (q0))))))) ### NotImply 239 % 0.22/0.52 241. (p1 zenon_X42) (-. (p1 zenon_X42)) ### Axiom % 0.22/0.52 242. (-. (Ex X, (p1 X))) (p1 zenon_X42) ### NotExists 241 % 0.22/0.52 243. (All X, (p1 X)) (-. (Ex X, (p1 X))) ### All 242 % 0.22/0.52 244. (-. ((All X, (p1 X)) => (Ex X, (p1 X)))) ### NotImply 243 % 0.22/0.52 245. (-. (p1 T_43)) (p1 T_43) ### Axiom % 0.22/0.52 246. (All X, (p1 X)) (-. (p1 T_43)) ### All 245 % 0.22/0.52 247. (-. (q1 T_43)) (q1 T_43) ### Axiom % 0.22/0.52 248. ((p1 T_43) => (q1 T_43)) (-. (q1 T_43)) (All X, (p1 X)) ### Imply 246 247 % 0.22/0.52 249. (All X, ((p1 X) => (q1 X))) (All X, (p1 X)) (-. (q1 T_43)) ### All 248 % 0.22/0.52 250. (-. (All X, (q1 X))) (All X, (p1 X)) (All X, ((p1 X) => (q1 X))) ### NotAllEx 249 % 0.22/0.52 251. (-. ((All X, ((p1 X) => (q1 X))) => ((All X, (p1 X)) => (All X, (q1 X))))) ### ConjTree 250 % 0.22/0.52 252. (a1 T_44) (-. (a1 T_44)) ### Axiom % 0.22/0.52 253. (b T_44) (-. (b T_44)) ### Axiom % 0.22/0.52 254. (-. (Ex X, (b X))) (b T_44) ### NotExists 253 % 0.22/0.52 255. ((a1 T_44) => (b T_44)) (-. (Ex X, (b X))) (a1 T_44) ### Imply 252 254 % 0.22/0.52 256. (All X, ((a1 X) => (b X))) (a1 T_44) (-. (Ex X, (b X))) ### All 255 % 0.22/0.52 257. (Ex X, (a1 X)) (-. (Ex X, (b X))) (All X, ((a1 X) => (b X))) ### Exists 256 % 0.22/0.52 258. (-. ((All X, ((a1 X) => (b X))) => ((Ex X, (a1 X)) => (Ex X, (b X))))) ### ConjTree 257 % 0.22/0.52 259. (-. (a1 T_45)) (a1 T_45) ### Axiom % 0.22/0.52 260. (All X, (a1 X)) (-. (a1 T_45)) ### All 259 % 0.22/0.52 261. (b T_45) (-. (b T_45)) ### Axiom % 0.22/0.52 262. (-. (Ex X, (b X))) (b T_45) ### NotExists 261 % 0.22/0.52 263. ((a1 T_45) => (b T_45)) (-. (Ex X, (b X))) (All X, (a1 X)) ### Imply 260 262 % 0.22/0.52 264. (Ex X, ((a1 X) => (b X))) (All X, (a1 X)) (-. (Ex X, (b X))) ### Exists 263 % 0.22/0.52 265. (-. ((Ex X, ((a1 X) => (b X))) => ((All X, (a1 X)) => (Ex X, (b X))))) ### ConjTree 264 % 0.22/0.52 266. (-. (-. (a T_46 T_46))) (-. (a T_46 T_46)) ### Axiom % 0.22/0.52 267. (-. (a T_46 T_46)) (a T_46 T_46) ### Axiom % 0.22/0.52 268. ((a T_46 T_46) <=> (-. (a T_46 T_46))) ### Equiv 266 267 % 0.22/0.52 269. (All X, ((a X T_46) <=> (-. (a X X)))) ### All 268 % 0.22/0.52 270. (Ex Y, (All X, ((a X Y) <=> (-. (a X X))))) ### Exists 269 % 0.22/0.52 271. (a1 T_44) (-. (a1 T_44)) ### Axiom % 0.22/0.52 272. (b T_44) (-. (b T_44)) ### Axiom % 0.22/0.52 273. (-. ((a1 T_44) /\ (b T_44))) (b T_44) (a1 T_44) ### NotAnd 271 272 % 0.22/0.52 274. (-. (Ex X, ((a1 X) /\ (b X)))) (a1 T_44) (b T_44) ### NotExists 273 % 0.22/0.52 275. (All X, (b X)) (a1 T_44) (-. (Ex X, ((a1 X) /\ (b X)))) ### All 274 % 0.22/0.52 276. (Ex X, (a1 X)) (-. (Ex X, ((a1 X) /\ (b X)))) (All X, (b X)) ### Exists 275 % 0.22/0.52 277. (-. (((Ex X, (a1 X)) /\ (All X, (b X))) => (Ex X, ((a1 X) /\ (b X))))) ### ConjTree 276 % 0.22/0.52 278. (b T_47) (-. (b T_47)) ### Axiom % 0.37/0.52 279. (-. ((a1 T_47) \/ (b T_47))) (b T_47) ### NotOr 278 % 0.37/0.52 280. (-. (Ex X, ((a1 X) \/ (b X)))) (b T_47) ### NotExists 279 % 0.37/0.52 281. (Ex X, (b X)) (-. (Ex X, ((a1 X) \/ (b X)))) ### Exists 280 % 0.37/0.52 282. (-. ((Ex X, (b X)) => (Ex X, ((a1 X) \/ (b X))))) ### NotImply 281 % 0.37/0.52 283. (a T_48 T_49) (-. (a T_48 T_49)) ### Axiom % 0.37/0.52 284. (-. (Ex Y, (a T_48 Y))) (a T_48 T_49) ### NotExists 283 % 0.37/0.52 285. (-. (Ex X, (Ex Y, (a X Y)))) (a T_48 T_49) ### NotExists 284 % 0.37/0.52 286. (Ex X, (a X T_49)) (-. (Ex X, (Ex Y, (a X Y)))) ### Exists 285 % 0.37/0.52 287. (Ex Y, (Ex X, (a X Y))) (-. (Ex X, (Ex Y, (a X Y)))) ### Exists 286 % 0.37/0.52 288. (a T_50 T_51) (-. (a T_50 T_51)) ### Axiom % 0.37/0.52 289. (-. (Ex X, (a X T_51))) (a T_50 T_51) ### NotExists 288 % 0.37/0.52 290. (-. (Ex Y, (Ex X, (a X Y)))) (a T_50 T_51) ### NotExists 289 % 0.37/0.52 291. (Ex Y, (a T_50 Y)) (-. (Ex Y, (Ex X, (a X Y)))) ### Exists 290 % 0.37/0.52 292. (Ex X, (Ex Y, (a X Y))) (-. (Ex Y, (Ex X, (a X Y)))) ### Exists 291 % 0.37/0.52 293. (-. ((Ex X, (Ex Y, (a X Y))) <=> (Ex Y, (Ex X, (a X Y))))) ### NotEquiv 287 292 % 0.37/0.52 294. (-. (p1 T_52)) (p1 T_52) ### Axiom % 0.37/0.52 295. (All X, (p1 X)) (-. (p1 T_52)) ### All 294 % 0.37/0.52 296. (-. (p1 T_53)) (p1 T_53) ### Axiom % 0.37/0.52 297. (All X, (p1 X)) (-. (p1 T_53)) ### All 296 % 0.37/0.52 298. (-. ((p1 T_52) /\ (p1 T_53))) (All X, (p1 X)) ### NotAnd 295 297 % 0.37/0.52 299. (-. ((All X, (p1 X)) => ((p1 T_52) /\ (p1 T_53)))) ### NotImply 298 % 0.37/0.52 300. (-. (All B, ((All X, (p1 X)) => ((p1 T_52) /\ (p1 B))))) ### NotAllEx 299 % 0.37/0.52 301. (-. (All A, (All B, ((All X, (p1 X)) => ((p1 A) /\ (p1 B)))))) ### NotAllEx 300 % 0.37/0.52 302. (All X, (p1 X)) (-. (All X, (p1 X))) ### Axiom % 0.37/0.52 303. (All X, (p1 X)) (-. (All X, (p1 X))) ### Axiom % 0.37/0.52 304. (-. ((All X, (p1 X)) /\ (All X, (p1 X)))) (All X, (p1 X)) ### NotAnd 302 303 % 0.37/0.52 305. (-. ((All X, (p1 X)) => ((All X, (p1 X)) /\ (All X, (p1 X))))) ### NotImply 304 % 0.37/0.52 306. (Ex X, (p1 X)) (-. (Ex X, (p1 X))) ### Axiom % 0.37/0.52 307. (-. (Ex X, (p1 X))) (Ex X, (p1 X)) ### Axiom % 0.37/0.52 308. (-. ((Ex X, (p1 X)) <=> (Ex X, (p1 X)))) ### NotEquiv 306 307 % 0.37/0.52 309. (-. (Ex X, (p1 X))) (Ex X, (p1 X)) ### Axiom % 0.37/0.52 310. (-. ((Ex X, (p1 X)) => (Ex X, (p1 X)))) ### NotImply 309 % 0.37/0.52 311. (p T_54 T_54) (-. (p T_54 T_54)) ### Axiom % 0.37/0.52 312. (-. (Ex W, (p W T_54))) (p T_54 T_54) ### NotExists 311 % 0.37/0.52 313. (-. ((p T_54 T_54) => (Ex W, (p W T_54)))) ### NotImply 312 % 0.37/0.52 314. (p zenon_X55 T_54) (-. (p zenon_X55 T_54)) ### Axiom % 0.37/0.52 315. (-. (Ex W, (p W T_54))) (p zenon_X55 T_54) ### NotExists 314 % 0.37/0.52 316. (-. ((p T_54 T_56) => (Ex W, (p W T_54)))) (p zenon_X55 T_54) ### NotImply 315 % 0.37/0.52 317. (-. (p T_54 T_54)) (p T_54 T_54) ### Axiom % 0.37/0.52 318. (-. (((p T_54 T_54) /\ (p T_54 T_54)) => (p T_54 T_56))) (-. (p T_54 T_54)) ### ConjTree 317 % 0.37/0.52 319. (-. (((p T_54 T_56) => (Ex W, (p W T_54))) /\ (((p T_54 T_54) /\ (p T_54 T_54)) => (p T_54 T_56)))) (-. (p T_54 T_54)) (p zenon_X55 T_54) ### NotAnd 316 318 % 0.37/0.52 320. (-. (Ex Y, (((p Y T_56) => (Ex W, (p W Y))) /\ (((p T_54 Y) /\ (p Y T_54)) => (p Y T_56))))) (p zenon_X55 T_54) (-. (p T_54 T_54)) ### NotExists 319 % 0.37/0.52 321. (-. (All X, (Ex Y, (((p Y X) => (Ex W, (p W Y))) /\ (((p T_54 Y) /\ (p Y T_54)) => (p Y X)))))) (-. (p T_54 T_54)) (p zenon_X55 T_54) ### NotAllEx 320 % 0.37/0.52 322. (-. (Ex Z, (All X, (Ex Y, (((p Y X) => (Ex W, (p W Y))) /\ (((p Z Y) /\ (p Y Z)) => (p Y X))))))) (p zenon_X55 T_54) (-. (p T_54 T_54)) ### NotExists 321 % 0.37/0.52 323. (-. (((p zenon_X55 T_54) /\ (p T_54 zenon_X55)) => (p T_54 T_54))) (-. (Ex Z, (All X, (Ex Y, (((p Y X) => (Ex W, (p W Y))) /\ (((p Z Y) /\ (p Y Z)) => (p Y X))))))) ### ConjTree 322 % 0.37/0.52 324. (-. (((p T_54 T_54) => (Ex W, (p W T_54))) /\ (((p zenon_X55 T_54) /\ (p T_54 zenon_X55)) => (p T_54 T_54)))) (-. (Ex Z, (All X, (Ex Y, (((p Y X) => (Ex W, (p W Y))) /\ (((p Z Y) /\ (p Y Z)) => (p Y X))))))) ### NotAnd 313 323 % 0.37/0.52 325. (-. (Ex Y, (((p Y T_54) => (Ex W, (p W Y))) /\ (((p zenon_X55 Y) /\ (p Y zenon_X55)) => (p Y T_54))))) (-. (Ex Z, (All X, (Ex Y, (((p Y X) => (Ex W, (p W Y))) /\ (((p Z Y) /\ (p Y Z)) => (p Y X))))))) ### NotExists 324 % 0.37/0.52 326. (-. (All X, (Ex Y, (((p Y X) => (Ex W, (p W Y))) /\ (((p zenon_X55 Y) /\ (p Y zenon_X55)) => (p Y X)))))) (-. (Ex Z, (All X, (Ex Y, (((p Y X) => (Ex W, (p W Y))) /\ (((p Z Y) /\ (p Y Z)) => (p Y X))))))) ### NotAllEx 325 % 0.37/0.52 327. (-. (Ex Z, (All X, (Ex Y, (((p Y X) => (Ex W, (p W Y))) /\ (((p Z Y) /\ (p Y Z)) => (p Y X))))))) ### NotExists 326 % 0.37/0.52 328. (eq T_57 T_58) (-. (eq T_57 T_58)) ### Axiom % 0.37/0.52 329. (a_member_of T_59 T_57) (-. (a_member_of T_59 T_57)) ### Axiom % 0.37/0.52 330. (-. (a_member_of T_59 T_58)) (a_member_of T_59 T_58) ### Axiom % 0.37/0.52 331. ((a_member_of T_59 T_57) <=> (a_member_of T_59 T_58)) (-. (a_member_of T_59 T_58)) (a_member_of T_59 T_57) ### Equiv 329 330 % 0.37/0.52 332. (All Z, ((a_member_of Z T_57) <=> (a_member_of Z T_58))) (a_member_of T_59 T_57) (-. (a_member_of T_59 T_58)) ### All 331 % 0.37/0.52 333. ((eq T_57 T_58) <=> (All Z, ((a_member_of Z T_57) <=> (a_member_of Z T_58)))) (-. (a_member_of T_59 T_58)) (a_member_of T_59 T_57) (eq T_57 T_58) ### Equiv 328 332 % 0.37/0.52 334. (All Y, ((eq T_57 Y) <=> (All Z, ((a_member_of Z T_57) <=> (a_member_of Z Y))))) (eq T_57 T_58) (a_member_of T_59 T_57) (-. (a_member_of T_59 T_58)) ### All 333 % 0.37/0.52 335. (All X, (All Y, ((eq X Y) <=> (All Z, ((a_member_of Z X) <=> (a_member_of Z Y)))))) (-. (a_member_of T_59 T_58)) (a_member_of T_59 T_57) (eq T_57 T_58) ### All 334 % 0.37/0.52 336. (eq T_57 T_58) (-. (eq T_57 T_58)) ### Axiom % 0.37/0.52 337. (a_member_of T_59 T_58) (-. (a_member_of T_59 T_58)) ### Axiom % 0.37/0.52 338. (-. (a_member_of T_59 T_57)) (a_member_of T_59 T_57) ### Axiom % 0.37/0.52 339. ((a_member_of T_59 T_57) <=> (a_member_of T_59 T_58)) (-. (a_member_of T_59 T_57)) (a_member_of T_59 T_58) ### Equiv 337 338 % 0.37/0.52 340. (All Z, ((a_member_of Z T_57) <=> (a_member_of Z T_58))) (a_member_of T_59 T_58) (-. (a_member_of T_59 T_57)) ### All 339 % 0.37/0.52 341. ((eq T_57 T_58) <=> (All Z, ((a_member_of Z T_57) <=> (a_member_of Z T_58)))) (-. (a_member_of T_59 T_57)) (a_member_of T_59 T_58) (eq T_57 T_58) ### Equiv 336 340 % 0.37/0.52 342. (All Y, ((eq T_57 Y) <=> (All Z, ((a_member_of Z T_57) <=> (a_member_of Z Y))))) (eq T_57 T_58) (a_member_of T_59 T_58) (-. (a_member_of T_59 T_57)) ### All 341 % 0.37/0.52 343. (All X, (All Y, ((eq X Y) <=> (All Z, ((a_member_of Z X) <=> (a_member_of Z Y)))))) (-. (a_member_of T_59 T_57)) (a_member_of T_59 T_58) (eq T_57 T_58) ### All 342 % 0.37/0.52 344. (-. ((a_member_of T_59 T_58) <=> (a_member_of T_59 T_57))) (eq T_57 T_58) (All X, (All Y, ((eq X Y) <=> (All Z, ((a_member_of Z X) <=> (a_member_of Z Y)))))) ### NotEquiv 335 343 % 0.37/0.52 345. (-. (All Z, ((a_member_of Z T_58) <=> (a_member_of Z T_57)))) (All X, (All Y, ((eq X Y) <=> (All Z, ((a_member_of Z X) <=> (a_member_of Z Y)))))) (eq T_57 T_58) ### NotAllEx 344 % 0.37/0.52 346. (-. (eq T_58 T_57)) (eq T_58 T_57) ### Axiom % 0.37/0.52 347. ((eq T_58 T_57) <=> (All Z, ((a_member_of Z T_58) <=> (a_member_of Z T_57)))) (-. (eq T_58 T_57)) (eq T_57 T_58) (All X, (All Y, ((eq X Y) <=> (All Z, ((a_member_of Z X) <=> (a_member_of Z Y)))))) ### Equiv 345 346 % 0.37/0.52 348. (All Y, ((eq T_58 Y) <=> (All Z, ((a_member_of Z T_58) <=> (a_member_of Z Y))))) (All X, (All Y, ((eq X Y) <=> (All Z, ((a_member_of Z X) <=> (a_member_of Z Y)))))) (eq T_57 T_58) (-. (eq T_58 T_57)) ### All 347 % 0.37/0.52 349. (-. (eq T_58 T_57)) (eq T_57 T_58) (All X, (All Y, ((eq X Y) <=> (All Z, ((a_member_of Z X) <=> (a_member_of Z Y)))))) ### All 348 % 0.37/0.52 350. (-. ((eq T_57 T_58) => (eq T_58 T_57))) (All X, (All Y, ((eq X Y) <=> (All Z, ((a_member_of Z X) <=> (a_member_of Z Y)))))) ### NotImply 349 % 0.37/0.52 351. (-. (All B, ((eq T_57 B) => (eq B T_57)))) (All X, (All Y, ((eq X Y) <=> (All Z, ((a_member_of Z X) <=> (a_member_of Z Y)))))) ### NotAllEx 350 % 0.37/0.52 352. (-. (All A, (All B, ((eq A B) => (eq B A))))) (All X, (All Y, ((eq X Y) <=> (All Z, ((a_member_of Z X) <=> (a_member_of Z Y)))))) ### NotAllEx 351 % 0.37/0.52 353. (-. ((All X, (All Y, ((eq X Y) <=> (All Z, ((a_member_of Z X) <=> (a_member_of Z Y)))))) => (All A, (All B, ((eq A B) => (eq B A)))))) ### NotImply 352 % 0.37/0.52 354. (-. (p1 T_60)) (p1 T_60) ### Axiom % 0.37/0.52 355. (-. ((p1 T_60) => (p1 T_61))) (-. (p1 T_60)) ### NotImply 354 % 0.37/0.52 356. (-. (All Y, ((p1 T_60) => (p1 Y)))) (-. (p1 T_60)) ### NotAllEx 355 % 0.37/0.52 357. (-. (Ex X, (All Y, ((p1 X) => (p1 Y))))) (-. (p1 T_60)) ### NotExists 356 % 0.37/0.52 358. (-. ((p1 zenon_X62) => (p1 T_60))) (-. (Ex X, (All Y, ((p1 X) => (p1 Y))))) ### NotImply 357 % 0.37/0.53 359. (-. (All Y, ((p1 zenon_X62) => (p1 Y)))) (-. (Ex X, (All Y, ((p1 X) => (p1 Y))))) ### NotAllEx 358 % 0.37/0.53 360. (-. (Ex X, (All Y, ((p1 X) => (p1 Y))))) ### NotExists 359 % 0.37/0.53 361. (r1 T_63) (-. (r1 T_63)) ### Axiom % 0.37/0.53 362. (-. (p1 T_63)) (p1 T_63) ### Axiom % 0.37/0.53 363. ((r1 T_63) => (p1 T_63)) (-. (p1 T_63)) (r1 T_63) ### Imply 361 362 % 0.37/0.53 364. (All Y, ((r1 Y) => (p1 Y))) (r1 T_63) (-. (p1 T_63)) ### All 363 % 0.37/0.53 365. (-. (q1 T_63)) (q1 T_63) ### Axiom % 0.37/0.53 366. ((p1 T_63) => (q1 T_63)) (-. (q1 T_63)) (r1 T_63) (All Y, ((r1 Y) => (p1 Y))) ### Imply 364 365 % 0.37/0.53 367. (All X, ((p1 X) => (q1 X))) (All Y, ((r1 Y) => (p1 Y))) (r1 T_63) (-. (q1 T_63)) ### All 366 % 0.37/0.53 368. (-. (((All X, ((p1 X) => (q1 X))) /\ (r1 T_63)) => ((All Y, ((r1 Y) => (p1 Y))) => (q1 T_63)))) ### ConjTree 367 % 0.37/0.53 369. (-. (All B, (((All X, ((p1 X) => (q1 X))) /\ (r1 B)) => ((All Y, ((r1 Y) => (p1 Y))) => (q1 B))))) ### NotAllEx 368 % 0.37/0.53 370. (p1 T_64) (-. (p1 T_64)) ### Axiom % 0.37/0.53 371. (-. (r1 T_65)) (r1 T_65) ### Axiom % 0.37/0.53 372. ((p1 T_64) => (r1 T_65)) (-. (r1 T_65)) (p1 T_64) ### Imply 370 371 % 0.37/0.53 373. (-. (((p1 T_64) => (r1 T_65)) => ((p1 T_64) => (r1 T_65)))) (p1 T_64) (-. (r1 T_65)) ### ConjTree 372 % 0.37/0.53 374. (-. (Ex Y, (((p1 T_64) => (r1 Y)) => ((p1 T_64) => (r1 T_65))))) (-. (r1 T_65)) (p1 T_64) ### NotExists 373 % 0.37/0.53 375. (-. (Ex X, (Ex Y, (((p1 X) => (r1 Y)) => ((p1 T_64) => (r1 T_65)))))) (p1 T_64) (-. (r1 T_65)) ### NotExists 374 % 0.37/0.53 376. (-. (((p1 zenon_X66) => (r1 zenon_X67)) => ((p1 T_64) => (r1 T_65)))) (-. (Ex X, (Ex Y, (((p1 X) => (r1 Y)) => ((p1 T_64) => (r1 T_65)))))) ### ConjTree 375 % 0.37/0.53 377. (-. (Ex Y, (((p1 zenon_X66) => (r1 Y)) => ((p1 T_64) => (r1 T_65))))) (-. (Ex X, (Ex Y, (((p1 X) => (r1 Y)) => ((p1 T_64) => (r1 T_65)))))) ### NotExists 376 % 0.37/0.53 378. (-. (Ex X, (Ex Y, (((p1 X) => (r1 Y)) => ((p1 T_64) => (r1 T_65)))))) ### NotExists 377 % 0.37/0.53 379. (-. (All B, (Ex X, (Ex Y, (((p1 X) => (r1 Y)) => ((p1 T_64) => (r1 B))))))) ### NotAllEx 378 % 0.37/0.53 380. (-. (All A, (All B, (Ex X, (Ex Y, (((p1 X) => (r1 Y)) => ((p1 A) => (r1 B)))))))) ### NotAllEx 379 % 0.37/0.53 381. (p1 T_68) (-. (p1 T_68)) ### Axiom % 0.37/0.53 382. (-. ((Ex X, (p1 X)) => (p1 T_68))) (p1 T_68) ### NotImply 381 % 0.37/0.53 383. (-. (Ex Y, ((Ex X, (p1 X)) => (p1 Y)))) (p1 T_68) ### NotExists 382 % 0.37/0.53 384. (Ex X, (p1 X)) (-. (Ex Y, ((Ex X, (p1 X)) => (p1 Y)))) ### Exists 383 % 0.37/0.53 385. (-. ((Ex X, (p1 X)) => (p1 zenon_X69))) (-. (Ex Y, ((Ex X, (p1 X)) => (p1 Y)))) ### NotImply 384 % 0.37/0.53 386. (-. (Ex Y, ((Ex X, (p1 X)) => (p1 Y)))) ### NotExists 385 % 0.37/0.53 387. (p T_70 T_71) (-. (p T_70 T_71)) ### Axiom % 0.37/0.53 388. (-. (Ex W, (p W T_71))) (p T_70 T_71) ### NotExists 387 % 0.37/0.53 389. (All Y, (p T_70 Y)) (-. (Ex W, (p W T_71))) ### All 388 % 0.37/0.53 390. (-. (All Y, (Ex W, (p W Y)))) (All Y, (p T_70 Y)) ### NotAllEx 389 % 0.37/0.53 391. (Ex X, (All Y, (p X Y))) (-. (All Y, (Ex W, (p W Y)))) ### Exists 390 % 0.37/0.53 392. (-. ((Ex X, (All Y, (p X Y))) => (All Y, (Ex W, (p W Y))))) ### NotImply 391 % 0.37/0.53 393. (-. (p1 (z))) (p1 (z)) ### Axiom % 0.37/0.53 394. (-. ((p1 (z)) => (p1 (z)))) ### NotImply 393 % 0.37/0.53 395. (-. (p T_72 T_72)) (p T_72 T_72) ### Axiom % 0.37/0.53 396. (All Y, (p T_72 Y)) (-. (p T_72 T_72)) ### All 395 % 0.37/0.53 397. (All X, (All Y, (p X Y))) (-. (p T_72 T_72)) ### All 396 % 0.37/0.53 398. (-. (All X, (p X X))) (All X, (All Y, (p X Y))) ### NotAllEx 397 % 0.37/0.53 399. (-. ((All X, (All Y, (p X Y))) => (All X, (p X X)))) ### NotImply 398 % 0.37/0.53 400. (-. (q1 T_73)) (q1 T_73) ### Axiom % 0.37/0.53 401. ((p1 T_73) /\ (q1 T_73)) (-. (q1 T_73)) ### And 400 % 0.37/0.53 402. (All X, ((p1 X) /\ (q1 X))) (-. (q1 T_73)) ### All 401 % 0.37/0.53 403. (-. ((((f0) \/ (g0)) /\ (All X, ((p1 X) /\ (q1 X)))) => (q1 T_73))) ### ConjTree 402 % 0.37/0.53 404. (-. (All A, ((((f0) \/ (g0)) /\ (All X, ((p1 X) /\ (q1 X)))) => (q1 A)))) ### NotAllEx 403 % 0.37/0.53 405. (-. (b0)) (b0) ### P-NotP % 0.37/0.53 406. (-. (a0)) (a0) ### P-NotP % 0.37/0.53 407. (-. ((a0) <=> (b0))) (-. (a0)) (-. (b0)) ### NotEquiv 405 406 % 0.37/0.53 408. (-. (((a0) <=> (b0)) \/ ((a0) \/ (b0)))) ### ConjTree 407 % 0.37/0.53 409. (-. ((a0) <=> (b0))) (b0) (a0) ### NotEquiv 406 405 % 0.37/0.53 410. (-. (((a0) /\ (b0)) => ((a0) <=> (b0)))) ### ConjTree 409 % 0.37/0.53 411. (s1 T_74) (-. (s1 T_74)) ### Axiom % 0.37/0.53 412. (-. (p T_74 T_75)) (p T_74 T_75) ### Axiom % 0.37/0.53 413. ((s1 T_74) => (p T_74 T_75)) (-. (p T_74 T_75)) (s1 T_74) ### Imply 411 412 % 0.37/0.53 414. (-. ((((q1 T_74) => (p T_74 T_74)) /\ ((q1 T_74) /\ ((q1 T_75) /\ (((r1 T_75) => (p T_75 T_75)) /\ ((r1 T_74) /\ ((r1 T_75) /\ (((s1 T_74) => (p T_74 T_75)) /\ (s1 T_74)))))))) => (p T_74 T_75))) (s1 T_74) (-. (p T_74 T_75)) ### ConjTree 413 % 0.37/0.53 415. (-. (Ex Y, ((((q1 T_74) => (p T_74 T_74)) /\ ((q1 T_74) /\ ((q1 T_75) /\ (((r1 Y) => (p T_75 Y)) /\ ((r1 T_74) /\ ((r1 T_75) /\ (((s1 T_74) => (p T_74 Y)) /\ (s1 T_74)))))))) => (p T_74 T_75)))) (-. (p T_74 T_75)) (s1 T_74) ### NotExists 414 % 0.37/0.53 416. (-. (Ex X, (Ex Y, ((((q1 X) => (p X T_74)) /\ ((q1 T_74) /\ ((q1 T_75) /\ (((r1 Y) => (p T_75 Y)) /\ ((r1 T_74) /\ ((r1 T_75) /\ (((s1 T_74) => (p X Y)) /\ (s1 T_74)))))))) => (p T_74 T_75))))) (s1 T_74) (-. (p T_74 T_75)) ### NotExists 415 % 0.37/0.53 417. (-. ((((q1 zenon_X76) => (p zenon_X76 T_74)) /\ ((q1 T_74) /\ ((q1 T_75) /\ (((r1 zenon_X77) => (p T_75 zenon_X77)) /\ ((r1 T_74) /\ ((r1 T_75) /\ (((s1 T_74) => (p zenon_X76 zenon_X77)) /\ (s1 T_74)))))))) => (p T_74 T_75))) (-. (Ex X, (Ex Y, ((((q1 X) => (p X T_74)) /\ ((q1 T_74) /\ ((q1 T_75) /\ (((r1 Y) => (p T_75 Y)) /\ ((r1 T_74) /\ ((r1 T_75) /\ (((s1 T_74) => (p X Y)) /\ (s1 T_74)))))))) => (p T_74 T_75))))) ### ConjTree 416 % 0.37/0.53 418. (-. (Ex Y, ((((q1 zenon_X76) => (p zenon_X76 T_74)) /\ ((q1 T_74) /\ ((q1 T_75) /\ (((r1 Y) => (p T_75 Y)) /\ ((r1 T_74) /\ ((r1 T_75) /\ (((s1 T_74) => (p zenon_X76 Y)) /\ (s1 T_74)))))))) => (p T_74 T_75)))) (-. (Ex X, (Ex Y, ((((q1 X) => (p X T_74)) /\ ((q1 T_74) /\ ((q1 T_75) /\ (((r1 Y) => (p T_75 Y)) /\ ((r1 T_74) /\ ((r1 T_75) /\ (((s1 T_74) => (p X Y)) /\ (s1 T_74)))))))) => (p T_74 T_75))))) ### NotExists 417 % 0.37/0.53 419. (-. (Ex X, (Ex Y, ((((q1 X) => (p X T_74)) /\ ((q1 T_74) /\ ((q1 T_75) /\ (((r1 Y) => (p T_75 Y)) /\ ((r1 T_74) /\ ((r1 T_75) /\ (((s1 T_74) => (p X Y)) /\ (s1 T_74)))))))) => (p T_74 T_75))))) ### NotExists 418 % 0.37/0.53 420. (-. (All B, (Ex X, (Ex Y, ((((q1 X) => (p X T_74)) /\ ((q1 T_74) /\ ((q1 B) /\ (((r1 Y) => (p B Y)) /\ ((r1 T_74) /\ ((r1 B) /\ (((s1 T_74) => (p X Y)) /\ (s1 T_74)))))))) => (p T_74 B)))))) ### NotAllEx 419 % 0.37/0.53 421. (-. (All A, (All B, (Ex X, (Ex Y, ((((q1 X) => (p X A)) /\ ((q1 A) /\ ((q1 B) /\ (((r1 Y) => (p B Y)) /\ ((r1 A) /\ ((r1 B) /\ (((s1 A) => (p X Y)) /\ (s1 A)))))))) => (p A B))))))) ### NotAllEx 420 % 0.37/0.53 422. (r1 T_78) (-. (r1 T_78)) ### Axiom % 0.37/0.53 423. (-. ((r1 T_78) => (r1 T_78))) (r1 T_78) ### NotImply 422 % 0.37/0.53 424. (p (f T_78) T_78) (-. (p (f T_78) T_78)) ### Axiom % 0.37/0.53 425. (-. (q (f T_78) T_78)) (q (f T_78) T_78) ### Axiom % 0.37/0.53 426. (-. ((q (f T_78) T_78) => (q (f T_78) T_78))) ### NotImply 425 % 0.37/0.53 427. (-. ((p (f T_78) T_78) /\ ((q (f T_78) T_78) => (q (f T_78) T_78)))) (p (f T_78) T_78) ### NotAnd 424 426 % 0.37/0.53 428. (-. (Ex Y, ((p (f T_78) Y) /\ ((q (f T_78) T_78) => (q (f T_78) Y))))) (p (f T_78) T_78) ### NotExists 427 % 0.37/0.53 429. (-. (Ex X, (Ex Y, ((p X Y) /\ ((q (f T_78) T_78) => (q X Y)))))) (p (f T_78) T_78) ### NotExists 428 % 0.37/0.53 430. (((r1 T_78) => (r1 T_78)) => (p (f T_78) T_78)) (-. (Ex X, (Ex Y, ((p X Y) /\ ((q (f T_78) T_78) => (q X Y)))))) (r1 T_78) ### Imply 423 429 % 0.37/0.53 431. (All Y, (((r1 T_78) => (r1 Y)) => (p (f Y) Y))) (r1 T_78) (-. (Ex X, (Ex Y, ((p X Y) /\ ((q (f T_78) T_78) => (q X Y)))))) ### All 430 % 0.37/0.53 432. (-. ((r1 T_78) => (r1 zenon_X79))) (-. (Ex X, (Ex Y, ((p X Y) /\ ((q (f T_78) T_78) => (q X Y)))))) (All Y, (((r1 T_78) => (r1 Y)) => (p (f Y) Y))) ### NotImply 431 % 0.37/0.53 433. (p (f zenon_X79) zenon_X79) (-. (p (f zenon_X79) zenon_X79)) ### Axiom % 0.37/0.53 434. (-. (r1 T_78)) (r1 T_78) ### Axiom % 0.37/0.53 435. (-. ((r1 T_78) => (r1 T_78))) ### NotImply 434 % 0.37/0.53 436. (-. (p (f T_78) T_78)) (p (f T_78) T_78) ### Axiom % 0.37/0.53 437. (((r1 T_78) => (r1 T_78)) => (p (f T_78) T_78)) (-. (p (f T_78) T_78)) ### Imply 435 436 % 0.37/0.53 438. (All Y, (((r1 T_78) => (r1 Y)) => (p (f Y) Y))) (-. (p (f T_78) T_78)) ### All 437 % 0.37/0.53 439. (q (f T_78) T_78) (-. (q (f T_78) T_78)) ### Axiom % 0.37/0.53 440. (-. ((q (f T_78) T_78) => (q (f T_78) T_78))) (q (f T_78) T_78) ### NotImply 439 % 0.37/0.53 441. (-. ((p (f T_78) T_78) /\ ((q (f T_78) T_78) => (q (f T_78) T_78)))) (q (f T_78) T_78) (All Y, (((r1 T_78) => (r1 Y)) => (p (f Y) Y))) ### NotAnd 438 440 % 0.37/0.53 442. (-. (Ex Y, ((p (f T_78) Y) /\ ((q (f T_78) T_78) => (q (f T_78) Y))))) (All Y, (((r1 T_78) => (r1 Y)) => (p (f Y) Y))) (q (f T_78) T_78) ### NotExists 441 % 0.37/0.53 443. (-. (Ex X, (Ex Y, ((p X Y) /\ ((q (f T_78) T_78) => (q X Y)))))) (q (f T_78) T_78) (All Y, (((r1 T_78) => (r1 Y)) => (p (f Y) Y))) ### NotExists 442 % 0.37/0.53 444. (-. ((q (f T_78) T_78) => (q (f zenon_X79) zenon_X79))) (All Y, (((r1 T_78) => (r1 Y)) => (p (f Y) Y))) (-. (Ex X, (Ex Y, ((p X Y) /\ ((q (f T_78) T_78) => (q X Y)))))) ### NotImply 443 % 0.37/0.53 445. (-. ((p (f zenon_X79) zenon_X79) /\ ((q (f T_78) T_78) => (q (f zenon_X79) zenon_X79)))) (-. (Ex X, (Ex Y, ((p X Y) /\ ((q (f T_78) T_78) => (q X Y)))))) (All Y, (((r1 T_78) => (r1 Y)) => (p (f Y) Y))) (p (f zenon_X79) zenon_X79) ### NotAnd 433 444 % 0.37/0.53 446. (-. (Ex Y, ((p (f zenon_X79) Y) /\ ((q (f T_78) T_78) => (q (f zenon_X79) Y))))) (p (f zenon_X79) zenon_X79) (All Y, (((r1 T_78) => (r1 Y)) => (p (f Y) Y))) (-. (Ex X, (Ex Y, ((p X Y) /\ ((q (f T_78) T_78) => (q X Y)))))) ### NotExists 445 % 0.37/0.53 447. (-. (Ex X, (Ex Y, ((p X Y) /\ ((q (f T_78) T_78) => (q X Y)))))) (All Y, (((r1 T_78) => (r1 Y)) => (p (f Y) Y))) (p (f zenon_X79) zenon_X79) ### NotExists 446 % 0.37/0.53 448. (((r1 T_78) => (r1 zenon_X79)) => (p (f zenon_X79) zenon_X79)) (All Y, (((r1 T_78) => (r1 Y)) => (p (f Y) Y))) (-. (Ex X, (Ex Y, ((p X Y) /\ ((q (f T_78) T_78) => (q X Y)))))) ### Imply 432 447 % 0.37/0.53 449. (-. (Ex X, (Ex Y, ((p X Y) /\ ((q (f T_78) T_78) => (q X Y)))))) (All Y, (((r1 T_78) => (r1 Y)) => (p (f Y) Y))) ### All 448 % 0.37/0.53 450. (-. ((All Y, (((r1 T_78) => (r1 Y)) => (p (f Y) Y))) => (Ex X, (Ex Y, ((p X Y) /\ ((q (f T_78) T_78) => (q X Y))))))) ### NotImply 449 % 0.37/0.53 451. (-. (All B, ((All Y, (((r1 B) => (r1 Y)) => (p (f Y) Y))) => (Ex X, (Ex Y, ((p X Y) /\ ((q (f B) B) => (q X Y)))))))) ### NotAllEx 450 % 0.37/0.53 452. (-. (p1 T_80)) (p1 T_80) ### Axiom % 0.37/0.53 453. (-. ((p1 T_80) => (r1 T_80))) (-. (p1 T_80)) ### NotImply 452 % 0.37/0.53 454. (-. (Ex Z, ((p1 Z) => (r1 Z)))) (-. (p1 T_80)) ### NotExists 453 % 0.37/0.53 455. (-. (q1 T_80)) (q1 T_80) ### Axiom % 0.37/0.53 456. ((p1 T_80) => (q1 T_80)) (-. (q1 T_80)) (-. (Ex Z, ((p1 Z) => (r1 Z)))) ### Imply 454 455 % 0.37/0.53 457. (All X, ((p1 X) => (q1 X))) (-. (Ex Z, ((p1 Z) => (r1 Z)))) (-. (q1 T_80)) ### All 456 % 0.37/0.53 458. (r1 T_80) (-. (r1 T_80)) ### Axiom % 0.37/0.53 459. (-. ((p1 T_80) => (r1 T_80))) (r1 T_80) ### NotImply 458 % 0.37/0.53 460. (-. (Ex Z, ((p1 Z) => (r1 Z)))) (r1 T_80) ### NotExists 459 % 0.37/0.53 461. ((q1 T_80) => (r1 T_80)) (-. (Ex Z, ((p1 Z) => (r1 Z)))) (All X, ((p1 X) => (q1 X))) ### Imply 457 460 % 0.37/0.53 462. (Ex Y, ((q1 Y) => (r1 Y))) (All X, ((p1 X) => (q1 X))) (-. (Ex Z, ((p1 Z) => (r1 Z)))) ### Exists 461 % 0.37/0.53 463. (-. (((All X, ((p1 X) => (q1 X))) /\ (Ex Y, ((q1 Y) => (r1 Y)))) => (Ex Z, ((p1 Z) => (r1 Z))))) ### ConjTree 462 % 0.37/0.53 464. (-. ((All C, (All B, ((All Z, (q1 (f Z))) => (Ex X, (Ex Y, (((p1 (f Y)) => (p1 X)) /\ (((r1 Y) => ((r1 B) /\ (r1 C))) /\ (q1 X)))))))) /\ ((All B, (All C, ((All Z, (q1 (f Z))) => (Ex X, (Ex Y, (((p1 (f Y)) => ((p1 X) /\ ((r1 Y) => ((r1 B) /\ (r1 C))))) /\ (q1 X))))))) /\ ((All B, (All C, ((q1 (f B)) => (Ex X, (Ex Y, (((p1 (f Y)) => ((p1 X) /\ ((r1 Y) => ((r1 B) /\ (r1 C))))) /\ (q1 X))))))) /\ ((((All X, ((a1 X) => ((b X) \/ (c X)))) /\ (-. (All X, ((a1 X) => (b X))))) => (Ex X, ((a1 X) /\ (c X)))) /\ ((All A, (Ex X, (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p1 A) /\ ((e A) /\ (((e X) => ((g X) \/ (s X (f X)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s A Y) => (p1 Y)))))) => (((p1 X3) /\ (g X3)) \/ ((p1 X4) /\ (c X4)))))))))) /\ ((All A, (All B, (All C, (((s1 A) /\ ((s1 B) /\ ((r B C) /\ ((All X, ((s1 X) => (p1 X))) /\ (All X, (All Y, ((r X Y) => (q X Y)))))))) => (Ex X, (Ex Y, ((p1 X) /\ (q X Y)))))))) /\ (((All X, (p1 X)) => (All A, (All B, ((p1 A) /\ (p1 B))))) /\ ((((All X, (p1 X)) /\ (Ex Y, (q1 Y))) => (Ex Z, (All Y, ((p1 Y) \/ (r1 Z))))) /\ (((All X, (Ex Y, ((p1 X) /\ (q1 Y)))) => (Ex Z, (All Y, ((p1 Y) \/ (r1 Z))))) /\ (((All X, (Ex Y, ((a X Y) /\ (a Y Y)))) => (Ex Z, (a Z Z))) /\ ((All A, (All B, (All C, (((s1 A) /\ ((s1 B) /\ ((r B C) /\ ((All X, ((s1 X) => (p1 X))) /\ (All X, (All Y, ((r X Y) => (q X Y)))))))) => (Ex X, (Ex Y, ((p1 X) /\ (q X Y)))))))) /\ ((All A, (All B, ((All Y, ((q1 Y) => (p1 Y))) => (Ex X, (((p1 X) => (p1 A)) /\ ((q1 X) => (p1 B))))))) /\ (((Ex X, (p1 X)) => ((Ex X, (p1 X)) /\ ((a0) => (((b0) \/ (-. (b0))) /\ ((q0) => (q0)))))) /\ (((All X, (p1 X)) => (Ex X, (p1 X))) /\ (((All X, ((p1 X) => (q1 X))) => ((All X, (p1 X)) => (All X, (q1 X)))) /\ ((All A, (All B, ((All Y, ((q1 Y) => (p1 Y))) => (Ex X, (((p1 X) => (p1 A)) /\ ((q1 X) => (p1 B))))))) /\ (((All X, ((a1 X) => (b X))) => ((Ex X, (a1 X)) => (Ex X, (b X)))) /\ (((Ex X, ((a1 X) => (b X))) => ((All X, (a1 X)) => (Ex X, (b X)))) /\ ((-. (Ex Y, (All X, ((a X Y) <=> (-. (a X X)))))) /\ ((((Ex X, (a1 X)) /\ (All X, (b X))) => (Ex X, ((a1 X) /\ (b X)))) /\ (((Ex X, (b X)) => (Ex X, ((a1 X) \/ (b X)))) /\ (((Ex X, (Ex Y, (a X Y))) <=> (Ex Y, (Ex X, (a X Y)))) /\ ((All A, (All B, ((All X, (p1 X)) => ((p1 A) /\ (p1 B))))) /\ (((All X, (p1 X)) => ((All X, (p1 X)) /\ (All X, (p1 X)))) /\ (((Ex X, (p1 X)) <=> (Ex X, (p1 X))) /\ (((Ex X, (p1 X)) => (Ex X, (p1 X))) /\ ((Ex Z, (All X, (Ex Y, (((p Y X) => (Ex W, (p W Y))) /\ (((p Z Y) /\ (p Y Z)) => (p Y X)))))) /\ (((All X, (All Y, ((eq X Y) <=> (All Z, ((a_member_of Z X) <=> (a_member_of Z Y)))))) => (All A, (All B, ((eq A B) => (eq B A))))) /\ ((All A, (All B, ((All Y, ((q1 Y) => (p1 Y))) => (Ex X, (((p1 X) => (p1 A)) /\ ((q1 X) => (p1 B))))))) /\ ((Ex X, (All Y, ((p1 X) => (p1 Y)))) /\ ((All B, (((All X, ((p1 X) => (q1 X))) /\ (r1 B)) => ((All Y, ((r1 Y) => (p1 Y))) => (q1 B)))) /\ ((All A, (All B, (Ex X, (Ex Y, (((p1 X) => (r1 Y)) => ((p1 A) => (r1 B))))))) /\ ((Ex Y, ((Ex X, (p1 X)) => (p1 Y))) /\ (((Ex X, (All Y, (p X Y))) => (All Y, (Ex W, (p W Y)))) /\ (((p1 (z)) => (p1 (z))) /\ (((Ex X, (p1 X)) => (Ex X, (p1 X))) /\ (((All X, (All Y, (p X Y))) => (All X, (p X X))) /\ ((All A, ((((f0) \/ (g0)) /\ (All X, ((p1 X) /\ (q1 X)))) => (q1 A))) /\ ((((a0) <=> (b0)) \/ ((a0) \/ (b0))) /\ ((((a0) /\ (b0)) => ((a0) <=> (b0))) /\ ((All A, (All B, (Ex X, (Ex Y, ((((q1 X) => (p X A)) /\ ((q1 A) /\ ((q1 B) /\ (((r1 Y) => (p B Y)) /\ ((r1 A) /\ ((r1 B) /\ (((s1 A) => (p X Y)) /\ (s1 A)))))))) => (p A B)))))) /\ ((All B, ((All Y, (((r1 B) => (r1 Y)) => (p (f Y) Y))) => (Ex X, (Ex Y, ((p X Y) /\ ((q (f B) B) => (q X Y))))))) /\ (((All X, ((p1 X) => (q1 X))) /\ (Ex Y, ((q1 Y) => (r1 Y)))) => (Ex Z, ((p1 Z) => (r1 Z))))))))))))))))))))))))))))))))))))))))))))))) ### DisjTree 35 80 111 122 166 182 190 196 204 210 182 231 240 244 251 231 258 265 270 277 282 293 301 305 308 310 327 353 231 360 369 380 386 392 394 310 399 404 408 410 421 451 463 % 0.37/0.53 % SZS output end Proof % 0.37/0.53 (* END-PROOF *) %------------------------------------------------------------------------------