%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SYN723+1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n029.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:46:07 EDT 2022 % Result : Theorem 0.20s 0.43s % Output : Proof 0.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : SYN723+1 : TPTP v8.1.0. Released v2.5.0. % 0.04/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.13/0.34 % Computer : n029.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Tue Jul 12 02:33:17 EDT 2022 % 0.13/0.34 % CPUTime : % 0.20/0.43 % SZS status Theorem % 0.20/0.43 (* PROOF-FOUND *) % 0.20/0.43 (* BEGIN-PROOF *) % 0.20/0.43 % SZS output start Proof % 0.20/0.43 1. (s T_0) (-. (s T_0)) ### Axiom % 0.20/0.43 2. (-. (Ex X, (s X))) (s T_0) ### NotExists 1 % 0.20/0.43 3. (-. (s T_1)) (s T_1) ### Axiom % 0.20/0.43 4. (-. ((s T_1) <=> (s T_0))) (-. (s T_1)) (-. (Ex X, (s X))) ### NotEquiv 2 3 % 0.20/0.43 5. (-. (All Y, ((s T_1) <=> (s Y)))) (-. (Ex X, (s X))) (-. (s T_1)) ### NotAllEx 4 % 0.20/0.43 6. (-. (Ex X, (All Y, ((s X) <=> (s Y))))) (-. (s T_1)) (-. (Ex X, (s X))) ### NotExists 5 % 0.20/0.43 7. (q T_2) (-. (q T_2)) ### Axiom % 0.20/0.43 8. (-. (Ex X, (q X))) (q T_2) ### NotExists 7 % 0.20/0.43 9. (-. (q T_3)) (q T_3) ### Axiom % 0.20/0.43 10. (-. ((q T_3) <=> (q T_2))) (-. (q T_3)) (-. (Ex X, (q X))) ### NotEquiv 8 9 % 0.20/0.43 11. (-. (All Y, ((q T_3) <=> (q Y)))) (-. (Ex X, (q X))) (-. (q T_3)) ### NotAllEx 10 % 0.20/0.43 12. (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (q T_3)) (-. (Ex X, (q X))) ### NotExists 11 % 0.20/0.43 13. (-. (All Y, (q Y))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) ### NotAllEx 12 % 0.20/0.43 14. (p T_4) (-. (p T_4)) ### Axiom % 0.20/0.43 15. (-. (p T_5)) (p T_5) ### Axiom % 0.20/0.43 16. (All Y, (p Y)) (-. (p T_5)) ### All 15 % 0.20/0.43 17. (-. ((p T_4) <=> (p T_5))) (All Y, (p Y)) (p T_4) ### NotEquiv 14 16 % 0.20/0.43 18. (-. (All Y, ((p T_4) <=> (p Y)))) (p T_4) (All Y, (p Y)) ### NotAllEx 17 % 0.20/0.43 19. (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (All Y, (p Y)) (p T_4) ### NotExists 18 % 0.20/0.43 20. (Ex X, (p X)) (All Y, (p Y)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) ### Exists 19 % 0.20/0.43 21. ((Ex X, (p X)) <=> (All Y, (q Y))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (All Y, (p Y)) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) ### Equiv 13 20 % 0.20/0.43 22. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (All Y, (p Y)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (s X))) (-. (s T_1)) ### Equiv 6 21 % 0.20/0.43 23. (p T_6) (-. (p T_6)) ### Axiom % 0.20/0.43 24. (-. (Ex X, (p X))) (p T_6) ### NotExists 23 % 0.20/0.43 25. (-. (p T_7)) (p T_7) ### Axiom % 0.20/0.43 26. (-. ((p T_7) <=> (p T_6))) (-. (p T_7)) (-. (Ex X, (p X))) ### NotEquiv 24 25 % 0.20/0.43 27. (-. (All Y, ((p T_7) <=> (p Y)))) (-. (Ex X, (p X))) (-. (p T_7)) ### NotAllEx 26 % 0.20/0.43 28. (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (p T_7)) (-. (Ex X, (p X))) ### NotExists 27 % 0.20/0.43 29. (-. ((Ex X, (p X)) <=> (All Y, (q Y)))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) (-. (p T_7)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) ### NotEquiv 28 13 % 0.20/0.43 30. (s T_8) (-. (s T_8)) ### Axiom % 0.20/0.43 31. (-. (s T_9)) (s T_9) ### Axiom % 0.20/0.43 32. ((s T_9) <=> (s T_8)) (-. (s T_9)) (s T_8) ### Equiv 30 31 % 0.20/0.43 33. (All Y, ((s T_9) <=> (s Y))) (s T_8) (-. (s T_9)) ### All 32 % 0.20/0.43 34. (s T_9) (-. (s T_9)) ### Axiom % 0.20/0.43 35. (-. (s T_1)) (s T_1) ### Axiom % 0.20/0.43 36. ((s T_9) <=> (s T_1)) (-. (s T_1)) (s T_9) ### Equiv 34 35 % 0.20/0.43 37. (All Y, ((s T_9) <=> (s Y))) (s T_9) (-. (s T_1)) ### All 36 % 0.20/0.43 38. ((s T_9) <=> (s zenon_X10)) (-. (s T_1)) (s T_8) (All Y, ((s T_9) <=> (s Y))) ### Equiv 33 37 % 0.20/0.43 39. (All Y, ((s T_9) <=> (s Y))) (s T_8) (-. (s T_1)) ### All 38 % 0.20/0.43 40. (Ex X, (All Y, ((s X) <=> (s Y)))) (-. (s T_1)) (s T_8) ### Exists 39 % 0.20/0.43 41. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (s T_8) (-. (s T_1)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (p T_7)) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) ### Equiv 29 40 % 0.20/0.43 42. (-. (All Y, (p Y))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (s T_1)) (s T_8) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) ### NotAllEx 41 % 0.20/0.43 43. (Ex X, (s X)) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (-. (s T_1)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (All Y, (p Y))) ### Exists 42 % 0.20/0.43 44. (-. ((Ex X, (s X)) <=> (All Y, (p Y)))) (-. (s T_1)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) ### NotEquiv 22 43 % 0.20/0.43 45. (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (p T_7)) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (s X))) (-. (s T_1)) ### NotEquiv 6 29 % 0.20/0.43 46. (-. (All Y, (p Y))) (-. (s T_1)) (-. (Ex X, (s X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) ### NotAllEx 45 % 0.20/0.43 47. (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (s T_8) (-. (s T_1)) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (All Y, (p Y)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) ### NotEquiv 21 40 % 0.20/0.43 48. (Ex X, (s X)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (All Y, (p Y)) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) (-. (s T_1)) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) ### Exists 47 % 0.20/0.43 49. ((Ex X, (s X)) <=> (All Y, (p Y))) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (s T_1)) ### Equiv 46 48 % 0.20/0.43 50. (-. (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (s T_1)) ### NotEquiv 44 49 % 0.20/0.43 51. (-. (r T_11)) (r T_11) ### Axiom % 0.20/0.43 52. (All Y, (r Y)) (-. (r T_11)) ### All 51 % 0.20/0.43 53. (r T_11) (-. (r T_11)) ### Axiom % 0.20/0.43 54. (-. (Ex X, (r X))) (r T_11) ### NotExists 53 % 0.20/0.43 55. ((r T_11) <=> (r zenon_X12)) (-. (Ex X, (r X))) (All Y, (r Y)) ### Equiv 52 54 % 0.20/0.43 56. (All Y, ((r T_11) <=> (r Y))) (All Y, (r Y)) (-. (Ex X, (r X))) ### All 55 % 0.20/0.43 57. (Ex X, (All Y, ((r X) <=> (r Y)))) (-. (Ex X, (r X))) (All Y, (r Y)) ### Exists 56 % 0.20/0.43 58. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (All Y, (r Y)) (-. (Ex X, (r X))) (-. (s T_1)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) ### Equiv 50 57 % 0.20/0.43 59. (-. (All Y, (s Y))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (r X))) (All Y, (r Y)) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) ### NotAllEx 58 % 0.20/0.43 60. (r T_13) (-. (r T_13)) ### Axiom % 0.20/0.43 61. (-. (r T_14)) (r T_14) ### Axiom % 0.20/0.43 62. (All Y, (r Y)) (-. (r T_14)) ### All 61 % 0.20/0.43 63. (-. ((r T_13) <=> (r T_14))) (All Y, (r Y)) (r T_13) ### NotEquiv 60 62 % 0.20/0.43 64. (-. (All Y, ((r T_13) <=> (r Y)))) (r T_13) (All Y, (r Y)) ### NotAllEx 63 % 0.20/0.43 65. (-. (Ex X, (All Y, ((r X) <=> (r Y))))) (All Y, (r Y)) (r T_13) ### NotExists 64 % 0.20/0.43 66. (-. (s T_9)) (s T_9) ### Axiom % 0.20/0.43 67. (All Y, (s Y)) (-. (s T_9)) ### All 66 % 0.20/0.43 68. (s T_9) (-. (s T_9)) ### Axiom % 0.20/0.43 69. (-. (Ex X, (s X))) (s T_9) ### NotExists 68 % 0.20/0.43 70. ((s T_9) <=> (s zenon_X10)) (-. (Ex X, (s X))) (All Y, (s Y)) ### Equiv 67 69 % 0.20/0.43 71. (All Y, ((s T_9) <=> (s Y))) (All Y, (s Y)) (-. (Ex X, (s X))) ### All 70 % 0.20/0.43 72. (Ex X, (All Y, ((s X) <=> (s Y)))) (-. (Ex X, (s X))) (All Y, (s Y)) ### Exists 71 % 0.20/0.43 73. (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (All Y, (s Y)) (-. (Ex X, (s X))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (All Y, (p Y)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) ### NotEquiv 21 72 % 0.20/0.43 74. (s T_8) (-. (s T_8)) ### Axiom % 0.20/0.43 75. (-. (s T_15)) (s T_15) ### Axiom % 0.20/0.43 76. (All Y, (s Y)) (-. (s T_15)) ### All 75 % 0.20/0.43 77. (-. ((s T_8) <=> (s T_15))) (All Y, (s Y)) (s T_8) ### NotEquiv 74 76 % 0.20/0.43 78. (-. (All Y, ((s T_8) <=> (s Y)))) (s T_8) (All Y, (s Y)) ### NotAllEx 77 % 0.20/0.43 79. (-. (Ex X, (All Y, ((s X) <=> (s Y))))) (All Y, (s Y)) (s T_8) ### NotExists 78 % 0.20/0.43 80. (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (p T_7)) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (s T_8) (All Y, (s Y)) ### NotEquiv 79 29 % 0.20/0.44 81. (-. (All Y, (p Y))) (All Y, (s Y)) (s T_8) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) ### NotAllEx 80 % 0.20/0.44 82. (Ex X, (s X)) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (All Y, (s Y)) (-. (All Y, (p Y))) ### Exists 81 % 0.20/0.44 83. (-. ((Ex X, (s X)) <=> (All Y, (p Y)))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) (All Y, (s Y)) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) ### NotEquiv 73 82 % 0.20/0.44 84. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (All Y, (s Y)) (-. (Ex X, (s X))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (p T_7)) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) ### Equiv 29 72 % 0.20/0.44 85. (-. (All Y, (p Y))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (s X))) (All Y, (s Y)) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) ### NotAllEx 84 % 0.20/0.44 86. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (All Y, (p Y)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (s T_8) (All Y, (s Y)) ### Equiv 79 21 % 0.20/0.44 87. (Ex X, (s X)) (All Y, (s Y)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (All Y, (p Y)) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) ### Exists 86 % 0.20/0.44 88. ((Ex X, (s X)) <=> (All Y, (p Y))) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (All Y, (s Y)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) ### Equiv 85 87 % 0.20/0.44 89. (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (All Y, (s Y)) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) ### Equiv 83 88 % 0.20/0.44 90. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) (All Y, (s Y)) (r T_13) (All Y, (r Y)) ### Equiv 65 89 % 0.20/0.44 91. (Ex X, (r X)) (All Y, (r Y)) (All Y, (s Y)) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) ### Exists 90 % 0.20/0.44 92. ((Ex X, (r X)) <=> (All Y, (s Y))) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (All Y, (r Y)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) ### Equiv 59 91 % 0.20/0.44 93. (-. (q T_16)) (q T_16) ### Axiom % 0.20/0.44 94. (All Y, (q Y)) (-. (q T_16)) ### All 93 % 0.20/0.44 95. (q T_16) (-. (q T_16)) ### Axiom % 0.20/0.44 96. (-. (Ex X, (q X))) (q T_16) ### NotExists 95 % 0.20/0.44 97. ((q T_16) <=> (q zenon_X17)) (-. (Ex X, (q X))) (All Y, (q Y)) ### Equiv 94 96 % 0.20/0.44 98. (All Y, ((q T_16) <=> (q Y))) (All Y, (q Y)) (-. (Ex X, (q X))) ### All 97 % 0.20/0.44 99. (-. ((Ex X, (p X)) <=> (All Y, (q Y)))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (All Y, (p Y)) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) ### NotEquiv 98 20 % 0.20/0.44 100. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (All Y, (s Y)) (-. (Ex X, (s X))) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) (All Y, (p Y)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) ### Equiv 99 72 % 0.20/0.44 101. ((Ex X, (p X)) <=> (All Y, (q Y))) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) (-. (p T_7)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) ### Equiv 28 98 % 0.20/0.44 102. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (p T_7)) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) (s T_8) (All Y, (s Y)) ### Equiv 79 101 % 0.20/0.44 103. (-. (All Y, (p Y))) (All Y, (s Y)) (s T_8) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) ### NotAllEx 102 % 0.20/0.44 104. (Ex X, (s X)) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) (All Y, (s Y)) (-. (All Y, (p Y))) ### Exists 103 % 0.20/0.44 105. (-. ((Ex X, (s X)) <=> (All Y, (p Y)))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) (All Y, (s Y)) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) ### NotEquiv 100 104 % 0.20/0.44 106. (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (All Y, (s Y)) (-. (Ex X, (s X))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (p T_7)) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) ### NotEquiv 101 72 % 0.20/0.44 107. (-. (All Y, (p Y))) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (s X))) (All Y, (s Y)) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) ### NotAllEx 106 % 0.20/0.44 108. (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) (All Y, (p Y)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (s T_8) (All Y, (s Y)) ### NotEquiv 79 99 % 0.20/0.44 109. (Ex X, (s X)) (All Y, (s Y)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (All Y, (p Y)) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) ### Exists 108 % 0.20/0.44 110. ((Ex X, (s X)) <=> (All Y, (p Y))) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (All Y, (s Y)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) ### Equiv 107 109 % 0.20/0.44 111. (-. (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (All Y, (s Y)) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) ### NotEquiv 105 110 % 0.20/0.44 112. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (All Y, (r Y)) (-. (Ex X, (r X))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) (All Y, (s Y)) ### Equiv 111 57 % 0.20/0.44 113. (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) (All Y, (p Y)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (s X))) (-. (s T_1)) ### NotEquiv 6 99 % 0.20/0.44 114. (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (s T_8) (-. (s T_1)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (p T_7)) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) ### NotEquiv 101 40 % 0.20/0.44 115. (-. (All Y, (p Y))) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (s T_1)) (s T_8) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) ### NotAllEx 114 % 0.20/0.44 116. (Ex X, (s X)) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (-. (s T_1)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) (-. (All Y, (p Y))) ### Exists 115 % 0.20/0.44 117. (-. ((Ex X, (s X)) <=> (All Y, (p Y)))) (-. (s T_1)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) ### NotEquiv 113 116 % 0.20/0.44 118. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (p T_7)) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) (-. (Ex X, (s X))) (-. (s T_1)) ### Equiv 6 101 % 0.20/0.44 119. (-. (All Y, (p Y))) (-. (s T_1)) (-. (Ex X, (s X))) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) ### NotAllEx 118 % 0.20/0.44 120. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (s T_8) (-. (s T_1)) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) (All Y, (p Y)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) ### Equiv 99 40 % 0.20/0.44 121. (Ex X, (s X)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (All Y, (p Y)) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) (-. (s T_1)) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) ### Exists 120 % 0.20/0.44 122. ((Ex X, (s X)) <=> (All Y, (p Y))) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) (-. (s T_1)) ### Equiv 119 121 % 0.20/0.44 123. (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (s T_1)) ### Equiv 117 122 % 0.20/0.44 124. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (-. (s T_1)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) (r T_13) (All Y, (r Y)) ### Equiv 65 123 % 0.20/0.44 125. (-. (All Y, (s Y))) (All Y, (r Y)) (r T_13) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) ### NotAllEx 124 % 0.20/0.44 126. (Ex X, (r X)) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) (All Y, (r Y)) (-. (All Y, (s Y))) ### Exists 125 % 0.20/0.44 127. (-. ((Ex X, (r X)) <=> (All Y, (s Y)))) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (All Y, (r Y)) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) ### NotEquiv 112 126 % 0.20/0.44 128. (Ex X, (All Y, ((q X) <=> (q Y)))) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (All Y, (r Y)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (q X))) (-. ((Ex X, (r X)) <=> (All Y, (s Y)))) ### Exists 127 % 0.20/0.44 129. (-. ((Ex X, (All Y, ((q X) <=> (q Y)))) <=> ((Ex X, (r X)) <=> (All Y, (s Y))))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (All Y, (r Y)) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) ### NotEquiv 92 128 % 0.20/0.44 130. (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (All Y, (r Y)) (-. (Ex X, (r X))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) (All Y, (s Y)) ### NotEquiv 89 57 % 0.20/0.44 131. (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (-. (s T_1)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) (r T_13) (All Y, (r Y)) ### NotEquiv 65 50 % 0.20/0.44 132. (-. (All Y, (s Y))) (All Y, (r Y)) (r T_13) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ### NotAllEx 131 % 0.20/0.44 133. (Ex X, (r X)) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) (All Y, (r Y)) (-. (All Y, (s Y))) ### Exists 132 % 0.20/0.44 134. (-. ((Ex X, (r X)) <=> (All Y, (s Y)))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (All Y, (r Y)) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ### NotEquiv 130 133 % 0.20/0.44 135. (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (All Y, (r Y)) (-. (Ex X, (r X))) (-. (s T_1)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) ### NotEquiv 123 57 % 0.20/0.44 136. (-. (All Y, (s Y))) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (r X))) (All Y, (r Y)) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ### NotAllEx 135 % 0.20/0.44 137. (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) (All Y, (s Y)) (r T_13) (All Y, (r Y)) ### NotEquiv 65 111 % 0.20/0.44 138. (Ex X, (r X)) (All Y, (r Y)) (All Y, (s Y)) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ### Exists 137 % 0.20/0.44 139. ((Ex X, (r X)) <=> (All Y, (s Y))) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (All Y, (r Y)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) ### Equiv 136 138 % 0.20/0.44 140. (Ex X, (All Y, ((q X) <=> (q Y)))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (All Y, (r Y)) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ((Ex X, (r X)) <=> (All Y, (s Y))) ### Exists 139 % 0.20/0.44 141. ((Ex X, (All Y, ((q X) <=> (q Y)))) <=> ((Ex X, (r X)) <=> (All Y, (s Y)))) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (All Y, (r Y)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (q X))) ### Equiv 134 140 % 0.20/0.44 142. (-. (((Ex X, (All Y, ((q X) <=> (q Y)))) <=> ((Ex X, (r X)) <=> (All Y, (s Y)))) <=> ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))))) (All Y, (r Y)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (q X))) ### NotEquiv 129 141 % 0.20/0.44 143. (r T_18) (-. (r T_18)) ### Axiom % 0.20/0.44 144. (-. (Ex X, (r X))) (r T_18) ### NotExists 143 % 0.20/0.44 145. (-. (r T_19)) (r T_19) ### Axiom % 0.20/0.44 146. (-. ((r T_19) <=> (r T_18))) (-. (r T_19)) (-. (Ex X, (r X))) ### NotEquiv 144 145 % 0.20/0.44 147. (-. (All Y, ((r T_19) <=> (r Y)))) (-. (Ex X, (r X))) (-. (r T_19)) ### NotAllEx 146 % 0.20/0.44 148. (-. (Ex X, (All Y, ((r X) <=> (r Y))))) (-. (r T_19)) (-. (Ex X, (r X))) ### NotExists 147 % 0.20/0.44 149. (q T_20) (-. (q T_20)) ### Axiom % 0.20/0.44 150. (-. (q T_21)) (q T_21) ### Axiom % 0.20/0.44 151. (All Y, (q Y)) (-. (q T_21)) ### All 150 % 0.20/0.44 152. (-. ((q T_20) <=> (q T_21))) (All Y, (q Y)) (q T_20) ### NotEquiv 149 151 % 0.20/0.44 153. (-. (All Y, ((q T_20) <=> (q Y)))) (q T_20) (All Y, (q Y)) ### NotAllEx 152 % 0.20/0.44 154. (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (All Y, (q Y)) (q T_20) ### NotExists 153 % 0.20/0.44 155. (-. ((Ex X, (p X)) <=> (All Y, (q Y)))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (All Y, (p Y)) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) ### NotEquiv 154 20 % 0.20/0.44 156. (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) (All Y, (p Y)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (s X))) (-. (s T_1)) ### NotEquiv 6 155 % 0.20/0.44 157. ((Ex X, (p X)) <=> (All Y, (q Y))) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (p T_7)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) ### Equiv 28 154 % 0.20/0.44 158. (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (s T_8) (-. (s T_1)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (p T_7)) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) ### NotEquiv 157 40 % 0.20/0.44 159. (-. (All Y, (p Y))) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (s T_1)) (s T_8) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) ### NotAllEx 158 % 0.20/0.44 160. (Ex X, (s X)) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (-. (s T_1)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) (-. (All Y, (p Y))) ### Exists 159 % 0.20/0.44 161. (-. ((Ex X, (s X)) <=> (All Y, (p Y)))) (-. (s T_1)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) ### NotEquiv 156 160 % 0.20/0.44 162. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (p T_7)) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) (-. (Ex X, (s X))) (-. (s T_1)) ### Equiv 6 157 % 0.20/0.44 163. (-. (All Y, (p Y))) (-. (s T_1)) (-. (Ex X, (s X))) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) ### NotAllEx 162 % 0.20/0.44 164. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (s T_8) (-. (s T_1)) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) (All Y, (p Y)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) ### Equiv 155 40 % 0.20/0.44 165. (Ex X, (s X)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (All Y, (p Y)) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (s T_1)) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) ### Exists 164 % 0.20/0.44 166. ((Ex X, (s X)) <=> (All Y, (p Y))) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) (-. (s T_1)) ### Equiv 163 165 % 0.20/0.44 167. (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (s T_1)) ### Equiv 161 166 % 0.20/0.44 168. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (-. (s T_1)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (r X))) (-. (r T_19)) ### Equiv 148 167 % 0.20/0.44 169. (-. (All Y, (s Y))) (-. (r T_19)) (-. (Ex X, (r X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) ### NotAllEx 168 % 0.20/0.44 170. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (All Y, (s Y)) (-. (Ex X, (s X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) (All Y, (p Y)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) ### Equiv 155 72 % 0.20/0.44 171. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (p T_7)) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) (s T_8) (All Y, (s Y)) ### Equiv 79 157 % 0.20/0.44 172. (-. (All Y, (p Y))) (All Y, (s Y)) (s T_8) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) ### NotAllEx 171 % 0.20/0.44 173. (Ex X, (s X)) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) (All Y, (s Y)) (-. (All Y, (p Y))) ### Exists 172 % 0.20/0.44 174. (-. ((Ex X, (s X)) <=> (All Y, (p Y)))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (All Y, (s Y)) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) ### NotEquiv 170 173 % 0.20/0.44 175. (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (All Y, (s Y)) (-. (Ex X, (s X))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (p T_7)) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) ### NotEquiv 157 72 % 0.20/0.44 176. (-. (All Y, (p Y))) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (s X))) (All Y, (s Y)) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) ### NotAllEx 175 % 0.20/0.44 177. (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) (All Y, (p Y)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (s T_8) (All Y, (s Y)) ### NotEquiv 79 155 % 0.20/0.44 178. (Ex X, (s X)) (All Y, (s Y)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (All Y, (p Y)) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) ### Exists 177 % 0.20/0.44 179. ((Ex X, (s X)) <=> (All Y, (p Y))) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (All Y, (s Y)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) ### Equiv 176 178 % 0.20/0.44 180. (-. (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (All Y, (s Y)) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) ### NotEquiv 174 179 % 0.20/0.44 181. (r T_13) (-. (r T_13)) ### Axiom % 0.20/0.44 182. (-. (r T_11)) (r T_11) ### Axiom % 0.20/0.44 183. ((r T_11) <=> (r T_13)) (-. (r T_11)) (r T_13) ### Equiv 181 182 % 0.20/0.44 184. (All Y, ((r T_11) <=> (r Y))) (r T_13) (-. (r T_11)) ### All 183 % 0.20/0.44 185. (r T_11) (-. (r T_11)) ### Axiom % 0.20/0.44 186. (-. (r T_19)) (r T_19) ### Axiom % 0.20/0.44 187. ((r T_11) <=> (r T_19)) (-. (r T_19)) (r T_11) ### Equiv 185 186 % 0.20/0.44 188. (All Y, ((r T_11) <=> (r Y))) (r T_11) (-. (r T_19)) ### All 187 % 0.20/0.44 189. ((r T_11) <=> (r zenon_X12)) (-. (r T_19)) (r T_13) (All Y, ((r T_11) <=> (r Y))) ### Equiv 184 188 % 0.20/0.44 190. (All Y, ((r T_11) <=> (r Y))) (r T_13) (-. (r T_19)) ### All 189 % 0.20/0.44 191. (Ex X, (All Y, ((r X) <=> (r Y)))) (-. (r T_19)) (r T_13) ### Exists 190 % 0.20/0.44 192. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (r T_13) (-. (r T_19)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (All Y, (s Y)) ### Equiv 180 191 % 0.20/0.44 193. (Ex X, (r X)) (All Y, (s Y)) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (r T_19)) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) ### Exists 192 % 0.20/0.44 194. ((Ex X, (r X)) <=> (All Y, (s Y))) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (r T_19)) ### Equiv 169 193 % 0.20/0.44 195. (q T_20) (-. (q T_20)) ### Axiom % 0.20/0.44 196. (-. (q T_16)) (q T_16) ### Axiom % 0.20/0.44 197. ((q T_16) <=> (q T_20)) (-. (q T_16)) (q T_20) ### Equiv 195 196 % 0.20/0.44 198. (All Y, ((q T_16) <=> (q Y))) (q T_20) (-. (q T_16)) ### All 197 % 0.20/0.45 199. (q T_16) (-. (q T_16)) ### Axiom % 0.20/0.45 200. (-. (q T_3)) (q T_3) ### Axiom % 0.20/0.45 201. ((q T_16) <=> (q T_3)) (-. (q T_3)) (q T_16) ### Equiv 199 200 % 0.20/0.45 202. (All Y, ((q T_16) <=> (q Y))) (q T_16) (-. (q T_3)) ### All 201 % 0.20/0.45 203. ((q T_16) <=> (q zenon_X17)) (-. (q T_3)) (q T_20) (All Y, ((q T_16) <=> (q Y))) ### Equiv 198 202 % 0.20/0.45 204. (All Y, ((q T_16) <=> (q Y))) (q T_20) (-. (q T_3)) ### All 203 % 0.20/0.45 205. (-. (All Y, (q Y))) (q T_20) (All Y, ((q T_16) <=> (q Y))) ### NotAllEx 204 % 0.20/0.45 206. ((Ex X, (p X)) <=> (All Y, (q Y))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (All Y, (p Y)) (All Y, ((q T_16) <=> (q Y))) (q T_20) ### Equiv 205 20 % 0.20/0.45 207. (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (All Y, (s Y)) (-. (Ex X, (s X))) (q T_20) (All Y, ((q T_16) <=> (q Y))) (All Y, (p Y)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) ### NotEquiv 206 72 % 0.20/0.45 208. (-. ((Ex X, (p X)) <=> (All Y, (q Y)))) (All Y, ((q T_16) <=> (q Y))) (q T_20) (-. (p T_7)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) ### NotEquiv 28 205 % 0.20/0.45 209. (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (p T_7)) (q T_20) (All Y, ((q T_16) <=> (q Y))) (s T_8) (All Y, (s Y)) ### NotEquiv 79 208 % 0.20/0.45 210. (-. (All Y, (p Y))) (All Y, (s Y)) (s T_8) (All Y, ((q T_16) <=> (q Y))) (q T_20) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) ### NotAllEx 209 % 0.20/0.45 211. (Ex X, (s X)) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (q T_20) (All Y, ((q T_16) <=> (q Y))) (All Y, (s Y)) (-. (All Y, (p Y))) ### Exists 210 % 0.20/0.45 212. (-. ((Ex X, (s X)) <=> (All Y, (p Y)))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (All Y, ((q T_16) <=> (q Y))) (q T_20) (All Y, (s Y)) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) ### NotEquiv 207 211 % 0.20/0.45 213. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (All Y, (s Y)) (-. (Ex X, (s X))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (p T_7)) (q T_20) (All Y, ((q T_16) <=> (q Y))) ### Equiv 208 72 % 0.20/0.45 214. (-. (All Y, (p Y))) (All Y, ((q T_16) <=> (q Y))) (q T_20) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (s X))) (All Y, (s Y)) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) ### NotAllEx 213 % 0.20/0.45 215. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (q T_20) (All Y, ((q T_16) <=> (q Y))) (All Y, (p Y)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (s T_8) (All Y, (s Y)) ### Equiv 79 206 % 0.20/0.45 216. (Ex X, (s X)) (All Y, (s Y)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (All Y, (p Y)) (All Y, ((q T_16) <=> (q Y))) (q T_20) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) ### Exists 215 % 0.20/0.45 217. ((Ex X, (s X)) <=> (All Y, (p Y))) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (All Y, (s Y)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (q T_20) (All Y, ((q T_16) <=> (q Y))) ### Equiv 214 216 % 0.20/0.45 218. (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (All Y, (s Y)) (q T_20) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) ### Equiv 212 217 % 0.20/0.45 219. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (All Y, ((q T_16) <=> (q Y))) (q T_20) (All Y, (s Y)) (-. (Ex X, (r X))) (-. (r T_19)) ### Equiv 148 218 % 0.20/0.45 220. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (q T_20) (All Y, ((q T_16) <=> (q Y))) (All Y, (p Y)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (s X))) (-. (s T_1)) ### Equiv 6 206 % 0.20/0.45 221. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (s T_8) (-. (s T_1)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (p T_7)) (q T_20) (All Y, ((q T_16) <=> (q Y))) ### Equiv 208 40 % 0.20/0.45 222. (-. (All Y, (p Y))) (All Y, ((q T_16) <=> (q Y))) (q T_20) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (s T_1)) (s T_8) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) ### NotAllEx 221 % 0.20/0.45 223. (Ex X, (s X)) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (-. (s T_1)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (q T_20) (All Y, ((q T_16) <=> (q Y))) (-. (All Y, (p Y))) ### Exists 222 % 0.20/0.45 224. (-. ((Ex X, (s X)) <=> (All Y, (p Y)))) (-. (s T_1)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (All Y, ((q T_16) <=> (q Y))) (q T_20) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) ### NotEquiv 220 223 % 0.20/0.45 225. (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (p T_7)) (q T_20) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (s X))) (-. (s T_1)) ### NotEquiv 6 208 % 0.20/0.45 226. (-. (All Y, (p Y))) (-. (s T_1)) (-. (Ex X, (s X))) (All Y, ((q T_16) <=> (q Y))) (q T_20) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) ### NotAllEx 225 % 0.20/0.45 227. (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (s T_8) (-. (s T_1)) (q T_20) (All Y, ((q T_16) <=> (q Y))) (All Y, (p Y)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) ### NotEquiv 206 40 % 0.20/0.45 228. (Ex X, (s X)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (All Y, (p Y)) (All Y, ((q T_16) <=> (q Y))) (q T_20) (-. (s T_1)) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) ### Exists 227 % 0.20/0.45 229. ((Ex X, (s X)) <=> (All Y, (p Y))) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (q T_20) (All Y, ((q T_16) <=> (q Y))) (-. (s T_1)) ### Equiv 226 228 % 0.20/0.45 230. (-. (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (q T_20) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (s T_1)) ### NotEquiv 224 229 % 0.20/0.45 231. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (r T_13) (-. (r T_19)) (-. (s T_1)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (All Y, ((q T_16) <=> (q Y))) (q T_20) ### Equiv 230 191 % 0.20/0.45 232. (-. (All Y, (s Y))) (q T_20) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (r T_19)) (r T_13) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) ### NotAllEx 231 % 0.20/0.45 233. (Ex X, (r X)) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (-. (r T_19)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (All Y, ((q T_16) <=> (q Y))) (q T_20) (-. (All Y, (s Y))) ### Exists 232 % 0.20/0.45 234. (-. ((Ex X, (r X)) <=> (All Y, (s Y)))) (-. (r T_19)) (q T_20) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) ### NotEquiv 219 233 % 0.20/0.45 235. (Ex X, (All Y, ((q X) <=> (q Y)))) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (q T_20) (-. (r T_19)) (-. ((Ex X, (r X)) <=> (All Y, (s Y)))) ### Exists 234 % 0.20/0.45 236. (-. ((Ex X, (All Y, ((q X) <=> (q Y)))) <=> ((Ex X, (r X)) <=> (All Y, (s Y))))) (-. (r T_19)) (q T_20) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) ### NotEquiv 194 235 % 0.20/0.45 237. (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (All Y, (s Y)) (-. (Ex X, (r X))) (-. (r T_19)) ### NotEquiv 148 180 % 0.20/0.45 238. (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (r T_13) (-. (r T_19)) (-. (s T_1)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) ### NotEquiv 167 191 % 0.20/0.45 239. (-. (All Y, (s Y))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (r T_19)) (r T_13) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ### NotAllEx 238 % 0.20/0.45 240. (Ex X, (r X)) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (-. (r T_19)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (All Y, (s Y))) ### Exists 239 % 0.20/0.45 241. (-. ((Ex X, (r X)) <=> (All Y, (s Y)))) (-. (r T_19)) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ### NotEquiv 237 240 % 0.20/0.45 242. (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (-. (s T_1)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (All Y, ((q T_16) <=> (q Y))) (q T_20) (-. (Ex X, (r X))) (-. (r T_19)) ### NotEquiv 148 230 % 0.20/0.45 243. (-. (All Y, (s Y))) (-. (r T_19)) (-. (Ex X, (r X))) (q T_20) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ### NotAllEx 242 % 0.20/0.45 244. (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (r T_13) (-. (r T_19)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (All Y, ((q T_16) <=> (q Y))) (q T_20) (All Y, (s Y)) ### NotEquiv 218 191 % 0.20/0.45 245. (Ex X, (r X)) (All Y, (s Y)) (q T_20) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (r T_19)) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ### Exists 244 % 0.20/0.45 246. ((Ex X, (r X)) <=> (All Y, (s Y))) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (All Y, ((q T_16) <=> (q Y))) (q T_20) (-. (r T_19)) ### Equiv 243 245 % 0.20/0.45 247. (Ex X, (All Y, ((q X) <=> (q Y)))) (-. (r T_19)) (q T_20) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ((Ex X, (r X)) <=> (All Y, (s Y))) ### Exists 246 % 0.20/0.45 248. ((Ex X, (All Y, ((q X) <=> (q Y)))) <=> ((Ex X, (r X)) <=> (All Y, (s Y)))) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (q T_20) (-. (r T_19)) ### Equiv 241 247 % 0.20/0.45 249. (-. (((Ex X, (All Y, ((q X) <=> (q Y)))) <=> ((Ex X, (r X)) <=> (All Y, (s Y)))) <=> ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (q T_20) (-. (r T_19)) ### NotEquiv 236 248 % 0.20/0.45 250. (-. (All Y, (r Y))) (q T_20) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (((Ex X, (All Y, ((q X) <=> (q Y)))) <=> ((Ex X, (r X)) <=> (All Y, (s Y)))) <=> ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))))) ### NotAllEx 249 % 0.20/0.45 251. (Ex X, (q X)) (-. (((Ex X, (All Y, ((q X) <=> (q Y)))) <=> ((Ex X, (r X)) <=> (All Y, (s Y)))) <=> ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (All Y, (r Y))) ### Exists 250 % 0.20/0.45 252. (-. ((Ex X, (q X)) <=> (All Y, (r Y)))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (((Ex X, (All Y, ((q X) <=> (q Y)))) <=> ((Ex X, (r X)) <=> (All Y, (s Y)))) <=> ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))))) ### NotEquiv 142 251 % 0.20/0.45 253. (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (-. (s T_1)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) (-. (Ex X, (r X))) (-. (r T_19)) ### NotEquiv 148 50 % 0.20/0.45 254. (-. (All Y, (s Y))) (-. (r T_19)) (-. (Ex X, (r X))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ### NotAllEx 253 % 0.20/0.45 255. (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (r T_13) (-. (r T_19)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) (All Y, (s Y)) ### NotEquiv 89 191 % 0.20/0.45 256. (Ex X, (r X)) (All Y, (s Y)) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (r T_19)) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ### Exists 255 % 0.20/0.45 257. ((Ex X, (r X)) <=> (All Y, (s Y))) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) (-. (r T_19)) ### Equiv 254 256 % 0.20/0.45 258. (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) (All Y, (s Y)) (-. (Ex X, (r X))) (-. (r T_19)) ### NotEquiv 148 111 % 0.20/0.45 259. (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (r T_13) (-. (r T_19)) (-. (s T_1)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) ### NotEquiv 123 191 % 0.20/0.45 260. (-. (All Y, (s Y))) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (r T_19)) (r T_13) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ### NotAllEx 259 % 0.20/0.45 261. (Ex X, (r X)) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (-. (r T_19)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) (-. (All Y, (s Y))) ### Exists 260 % 0.20/0.45 262. (-. ((Ex X, (r X)) <=> (All Y, (s Y)))) (-. (r T_19)) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ### NotEquiv 258 261 % 0.20/0.46 263. (Ex X, (All Y, ((q X) <=> (q Y)))) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (q X))) (-. (r T_19)) (-. ((Ex X, (r X)) <=> (All Y, (s Y)))) ### Exists 262 % 0.20/0.46 264. (-. ((Ex X, (All Y, ((q X) <=> (q Y)))) <=> ((Ex X, (r X)) <=> (All Y, (s Y))))) (-. (r T_19)) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ### NotEquiv 257 263 % 0.20/0.46 265. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) (All Y, (s Y)) (-. (Ex X, (r X))) (-. (r T_19)) ### Equiv 148 89 % 0.20/0.46 266. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (r T_13) (-. (r T_19)) (-. (s T_1)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) ### Equiv 50 191 % 0.20/0.46 267. (-. (All Y, (s Y))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (r T_19)) (r T_13) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) ### NotAllEx 266 % 0.20/0.46 268. (Ex X, (r X)) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (-. (r T_19)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) (-. (All Y, (s Y))) ### Exists 267 % 0.20/0.46 269. (-. ((Ex X, (r X)) <=> (All Y, (s Y)))) (-. (r T_19)) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) ### NotEquiv 265 268 % 0.20/0.46 270. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (-. (s T_1)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (r X))) (-. (r T_19)) ### Equiv 148 123 % 0.20/0.46 271. (-. (All Y, (s Y))) (-. (r T_19)) (-. (Ex X, (r X))) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) ### NotAllEx 270 % 0.20/0.46 272. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (r T_13) (-. (r T_19)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) (All Y, (s Y)) ### Equiv 111 191 % 0.20/0.46 273. (Ex X, (r X)) (All Y, (s Y)) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (r T_19)) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) ### Exists 272 % 0.20/0.46 274. ((Ex X, (r X)) <=> (All Y, (s Y))) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) (-. (r T_19)) ### Equiv 271 273 % 0.20/0.46 275. (Ex X, (All Y, ((q X) <=> (q Y)))) (-. (r T_19)) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) ((Ex X, (r X)) <=> (All Y, (s Y))) ### Exists 274 % 0.20/0.46 276. ((Ex X, (All Y, ((q X) <=> (q Y)))) <=> ((Ex X, (r X)) <=> (All Y, (s Y)))) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (q X))) (-. (r T_19)) ### Equiv 269 275 % 0.20/0.46 277. (((Ex X, (All Y, ((q X) <=> (q Y)))) <=> ((Ex X, (r X)) <=> (All Y, (s Y)))) <=> ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (q X))) (-. (r T_19)) ### Equiv 264 276 % 0.20/0.46 278. (-. (All Y, (r Y))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (((Ex X, (All Y, ((q X) <=> (q Y)))) <=> ((Ex X, (r X)) <=> (All Y, (s Y)))) <=> ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ### NotAllEx 277 % 0.20/0.46 279. (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (All Y, (r Y)) (-. (Ex X, (r X))) (-. (s T_1)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) ### NotEquiv 167 57 % 0.20/0.46 280. (-. (All Y, (s Y))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (r X))) (All Y, (r Y)) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ### NotAllEx 279 % 0.20/0.46 281. (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (All Y, (s Y)) (r T_13) (All Y, (r Y)) ### NotEquiv 65 180 % 0.20/0.46 282. (Ex X, (r X)) (All Y, (r Y)) (All Y, (s Y)) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ### Exists 281 % 0.20/0.46 283. ((Ex X, (r X)) <=> (All Y, (s Y))) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (All Y, (r Y)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) ### Equiv 280 282 % 0.20/0.46 284. (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (All Y, (r Y)) (-. (Ex X, (r X))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (All Y, ((q T_16) <=> (q Y))) (q T_20) (All Y, (s Y)) ### NotEquiv 218 57 % 0.20/0.46 285. (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (-. (s T_1)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (All Y, ((q T_16) <=> (q Y))) (q T_20) (r T_13) (All Y, (r Y)) ### NotEquiv 65 230 % 0.20/0.46 286. (-. (All Y, (s Y))) (All Y, (r Y)) (r T_13) (q T_20) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ### NotAllEx 285 % 0.20/0.46 287. (Ex X, (r X)) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (All Y, ((q T_16) <=> (q Y))) (q T_20) (All Y, (r Y)) (-. (All Y, (s Y))) ### Exists 286 % 0.20/0.46 288. (-. ((Ex X, (r X)) <=> (All Y, (s Y)))) (q T_20) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (All Y, (r Y)) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ### NotEquiv 284 287 % 0.20/0.46 289. (Ex X, (All Y, ((q X) <=> (q Y)))) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (All Y, (r Y)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (q T_20) (-. ((Ex X, (r X)) <=> (All Y, (s Y)))) ### Exists 288 % 0.20/0.46 290. (-. ((Ex X, (All Y, ((q X) <=> (q Y)))) <=> ((Ex X, (r X)) <=> (All Y, (s Y))))) (q T_20) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (All Y, (r Y)) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ### NotEquiv 283 289 % 0.20/0.46 291. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (All Y, (r Y)) (-. (Ex X, (r X))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (All Y, (s Y)) ### Equiv 180 57 % 0.20/0.46 292. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (-. (s T_1)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (r T_13) (All Y, (r Y)) ### Equiv 65 167 % 0.20/0.46 293. (-. (All Y, (s Y))) (All Y, (r Y)) (r T_13) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) ### NotAllEx 292 % 0.20/0.46 294. (Ex X, (r X)) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (All Y, (r Y)) (-. (All Y, (s Y))) ### Exists 293 % 0.20/0.46 295. (-. ((Ex X, (r X)) <=> (All Y, (s Y)))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (All Y, (r Y)) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) ### NotEquiv 291 294 % 0.20/0.46 296. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (All Y, (r Y)) (-. (Ex X, (r X))) (-. (s T_1)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (All Y, ((q T_16) <=> (q Y))) (q T_20) ### Equiv 230 57 % 0.20/0.46 297. (-. (All Y, (s Y))) (q T_20) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (-. (Ex X, (r X))) (All Y, (r Y)) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) ### NotAllEx 296 % 0.20/0.46 298. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (All Y, ((q T_16) <=> (q Y))) (q T_20) (All Y, (s Y)) (r T_13) (All Y, (r Y)) ### Equiv 65 218 % 0.20/0.46 299. (Ex X, (r X)) (All Y, (r Y)) (All Y, (s Y)) (q T_20) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) ### Exists 298 % 0.20/0.46 300. ((Ex X, (r X)) <=> (All Y, (s Y))) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (All Y, (r Y)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (All Y, ((q T_16) <=> (q Y))) (q T_20) ### Equiv 297 299 % 0.20/0.46 301. (Ex X, (All Y, ((q X) <=> (q Y)))) (q T_20) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (All Y, (r Y)) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) ((Ex X, (r X)) <=> (All Y, (s Y))) ### Exists 300 % 0.20/0.46 302. ((Ex X, (All Y, ((q X) <=> (q Y)))) <=> ((Ex X, (r X)) <=> (All Y, (s Y)))) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (All Y, (r Y)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (q T_20) ### Equiv 295 301 % 0.20/0.46 303. (((Ex X, (All Y, ((q X) <=> (q Y)))) <=> ((Ex X, (r X)) <=> (All Y, (s Y)))) <=> ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (All Y, (r Y)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (q T_20) ### Equiv 290 302 % 0.20/0.46 304. (Ex X, (q X)) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) (All Y, (r Y)) (((Ex X, (All Y, ((q X) <=> (q Y)))) <=> ((Ex X, (r X)) <=> (All Y, (s Y)))) <=> ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ### Exists 303 % 0.20/0.46 305. ((Ex X, (q X)) <=> (All Y, (r Y))) (((Ex X, (All Y, ((q X) <=> (q Y)))) <=> ((Ex X, (r X)) <=> (All Y, (s Y)))) <=> ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) ### Equiv 278 304 % 0.20/0.46 306. (((Ex X, (q X)) <=> (All Y, (r Y))) <=> (((Ex X, (All Y, ((q X) <=> (q Y)))) <=> ((Ex X, (r X)) <=> (All Y, (s Y)))) <=> ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))))) (-. (Ex X, (All Y, ((p X) <=> (p Y))))) ### Equiv 252 305 % 0.20/0.46 307. (-. (p T_22)) (p T_22) ### Axiom % 0.20/0.46 308. (All Y, (p Y)) (-. (p T_22)) ### All 307 % 0.20/0.46 309. (p T_22) (-. (p T_22)) ### Axiom % 0.20/0.46 310. (-. (Ex X, (p X))) (p T_22) ### NotExists 309 % 0.20/0.46 311. ((p T_22) <=> (p zenon_X23)) (-. (Ex X, (p X))) (All Y, (p Y)) ### Equiv 308 310 % 0.20/0.46 312. (All Y, ((p T_22) <=> (p Y))) (All Y, (p Y)) (-. (Ex X, (p X))) ### All 311 % 0.20/0.46 313. (-. ((Ex X, (p X)) <=> (All Y, (q Y)))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) (All Y, (p Y)) (All Y, ((p T_22) <=> (p Y))) ### NotEquiv 312 13 % 0.20/0.46 314. (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (All Y, ((p T_22) <=> (p Y))) (All Y, (p Y)) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (s X))) (-. (s T_1)) ### NotEquiv 6 313 % 0.20/0.46 315. (p T_4) (-. (p T_4)) ### Axiom % 0.20/0.46 316. (-. (p T_22)) (p T_22) ### Axiom % 0.20/0.46 317. ((p T_22) <=> (p T_4)) (-. (p T_22)) (p T_4) ### Equiv 315 316 % 0.20/0.46 318. (All Y, ((p T_22) <=> (p Y))) (p T_4) (-. (p T_22)) ### All 317 % 0.20/0.46 319. (p T_22) (-. (p T_22)) ### Axiom % 0.20/0.46 320. (-. (p T_7)) (p T_7) ### Axiom % 0.20/0.46 321. ((p T_22) <=> (p T_7)) (-. (p T_7)) (p T_22) ### Equiv 319 320 % 0.20/0.46 322. (All Y, ((p T_22) <=> (p Y))) (p T_22) (-. (p T_7)) ### All 321 % 0.20/0.46 323. ((p T_22) <=> (p zenon_X23)) (-. (p T_7)) (p T_4) (All Y, ((p T_22) <=> (p Y))) ### Equiv 318 322 % 0.20/0.46 324. (All Y, ((p T_22) <=> (p Y))) (p T_4) (-. (p T_7)) ### All 323 % 0.20/0.46 325. (Ex X, (p X)) (-. (p T_7)) (All Y, ((p T_22) <=> (p Y))) ### Exists 324 % 0.20/0.46 326. ((Ex X, (p X)) <=> (All Y, (q Y))) (All Y, ((p T_22) <=> (p Y))) (-. (p T_7)) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) ### Equiv 13 325 % 0.20/0.46 327. (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (s T_8) (-. (s T_1)) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (p T_7)) (All Y, ((p T_22) <=> (p Y))) ### NotEquiv 326 40 % 0.20/0.46 328. (-. (All Y, (p Y))) (All Y, ((p T_22) <=> (p Y))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) (-. (s T_1)) (s T_8) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) ### NotAllEx 327 % 0.20/0.46 329. (Ex X, (s X)) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (-. (s T_1)) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (All Y, ((p T_22) <=> (p Y))) (-. (All Y, (p Y))) ### Exists 328 % 0.20/0.46 330. (-. ((Ex X, (s X)) <=> (All Y, (p Y)))) (-. (s T_1)) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) (All Y, ((p T_22) <=> (p Y))) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) ### NotEquiv 314 329 % 0.20/0.46 331. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (p T_7)) (All Y, ((p T_22) <=> (p Y))) (-. (Ex X, (s X))) (-. (s T_1)) ### Equiv 6 326 % 0.20/0.46 332. (-. (All Y, (p Y))) (-. (s T_1)) (-. (Ex X, (s X))) (All Y, ((p T_22) <=> (p Y))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) ### NotAllEx 331 % 0.20/0.46 333. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (s T_8) (-. (s T_1)) (All Y, ((p T_22) <=> (p Y))) (All Y, (p Y)) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) ### Equiv 313 40 % 0.20/0.46 334. (Ex X, (s X)) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) (All Y, (p Y)) (All Y, ((p T_22) <=> (p Y))) (-. (s T_1)) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) ### Exists 333 % 0.20/0.46 335. ((Ex X, (s X)) <=> (All Y, (p Y))) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (All Y, ((p T_22) <=> (p Y))) (-. (s T_1)) ### Equiv 332 334 % 0.20/0.46 336. (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (All Y, ((p T_22) <=> (p Y))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (s T_1)) ### Equiv 330 335 % 0.20/0.46 337. (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (All Y, (r Y)) (-. (Ex X, (r X))) (-. (s T_1)) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) (All Y, ((p T_22) <=> (p Y))) ### NotEquiv 336 57 % 0.20/0.46 338. (-. (All Y, (s Y))) (All Y, ((p T_22) <=> (p Y))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (r X))) (All Y, (r Y)) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ### NotAllEx 337 % 0.20/0.46 339. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (All Y, (s Y)) (-. (Ex X, (s X))) (All Y, ((p T_22) <=> (p Y))) (All Y, (p Y)) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) ### Equiv 313 72 % 0.20/0.46 340. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (p T_7)) (All Y, ((p T_22) <=> (p Y))) (s T_8) (All Y, (s Y)) ### Equiv 79 326 % 0.20/0.46 341. (-. (All Y, (p Y))) (All Y, (s Y)) (s T_8) (All Y, ((p T_22) <=> (p Y))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) ### NotAllEx 340 % 0.20/0.46 342. (Ex X, (s X)) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (All Y, ((p T_22) <=> (p Y))) (All Y, (s Y)) (-. (All Y, (p Y))) ### Exists 341 % 0.20/0.46 343. (-. ((Ex X, (s X)) <=> (All Y, (p Y)))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) (All Y, ((p T_22) <=> (p Y))) (All Y, (s Y)) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) ### NotEquiv 339 342 % 0.20/0.46 344. (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (All Y, (s Y)) (-. (Ex X, (s X))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (p T_7)) (All Y, ((p T_22) <=> (p Y))) ### NotEquiv 326 72 % 0.20/0.46 345. (-. (All Y, (p Y))) (All Y, ((p T_22) <=> (p Y))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) (-. (Ex X, (s X))) (All Y, (s Y)) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) ### NotAllEx 344 % 0.20/0.46 346. (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (All Y, ((p T_22) <=> (p Y))) (All Y, (p Y)) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (s T_8) (All Y, (s Y)) ### NotEquiv 79 313 % 0.20/0.46 347. (Ex X, (s X)) (All Y, (s Y)) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) (All Y, (p Y)) (All Y, ((p T_22) <=> (p Y))) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) ### Exists 346 % 0.20/0.46 348. ((Ex X, (s X)) <=> (All Y, (p Y))) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (All Y, (s Y)) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (All Y, ((p T_22) <=> (p Y))) ### Equiv 345 347 % 0.20/0.46 349. (-. (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (All Y, (s Y)) (All Y, ((p T_22) <=> (p Y))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) ### NotEquiv 343 348 % 0.20/0.46 350. (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) (All Y, ((p T_22) <=> (p Y))) (All Y, (s Y)) (r T_13) (All Y, (r Y)) ### NotEquiv 65 349 % 0.20/0.46 351. (Ex X, (r X)) (All Y, (r Y)) (All Y, (s Y)) (All Y, ((p T_22) <=> (p Y))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ### Exists 350 % 0.20/0.46 352. ((Ex X, (r X)) <=> (All Y, (s Y))) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (All Y, (r Y)) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) (All Y, ((p T_22) <=> (p Y))) ### Equiv 338 351 % 0.20/0.46 353. ((Ex X, (p X)) <=> (All Y, (q Y))) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) (All Y, (p Y)) (All Y, ((p T_22) <=> (p Y))) ### Equiv 312 98 % 0.20/0.46 354. (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (All Y, (s Y)) (-. (Ex X, (s X))) (All Y, ((p T_22) <=> (p Y))) (All Y, (p Y)) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) ### NotEquiv 353 72 % 0.20/0.46 355. (-. ((Ex X, (p X)) <=> (All Y, (q Y)))) (All Y, ((p T_22) <=> (p Y))) (-. (p T_7)) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) ### NotEquiv 98 325 % 0.20/0.46 356. (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) (-. (p T_7)) (All Y, ((p T_22) <=> (p Y))) (s T_8) (All Y, (s Y)) ### NotEquiv 79 355 % 0.20/0.46 357. (-. (All Y, (p Y))) (All Y, (s Y)) (s T_8) (All Y, ((p T_22) <=> (p Y))) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) ### NotAllEx 356 % 0.20/0.46 358. (Ex X, (s X)) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) (All Y, ((p T_22) <=> (p Y))) (All Y, (s Y)) (-. (All Y, (p Y))) ### Exists 357 % 0.20/0.46 359. (-. ((Ex X, (s X)) <=> (All Y, (p Y)))) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) (All Y, ((p T_22) <=> (p Y))) (All Y, (s Y)) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) ### NotEquiv 354 358 % 0.20/0.46 360. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (All Y, (s Y)) (-. (Ex X, (s X))) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) (-. (p T_7)) (All Y, ((p T_22) <=> (p Y))) ### Equiv 355 72 % 0.20/0.46 361. (-. (All Y, (p Y))) (All Y, ((p T_22) <=> (p Y))) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (s X))) (All Y, (s Y)) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) ### NotAllEx 360 % 0.20/0.46 362. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (All Y, ((p T_22) <=> (p Y))) (All Y, (p Y)) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) (s T_8) (All Y, (s Y)) ### Equiv 79 353 % 0.20/0.46 363. (Ex X, (s X)) (All Y, (s Y)) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) (All Y, (p Y)) (All Y, ((p T_22) <=> (p Y))) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) ### Exists 362 % 0.20/0.46 364. ((Ex X, (s X)) <=> (All Y, (p Y))) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (All Y, (s Y)) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) (All Y, ((p T_22) <=> (p Y))) ### Equiv 361 363 % 0.20/0.46 365. (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (All Y, (s Y)) (All Y, ((p T_22) <=> (p Y))) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) ### Equiv 359 364 % 0.20/0.46 366. (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (All Y, (r Y)) (-. (Ex X, (r X))) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) (All Y, ((p T_22) <=> (p Y))) (All Y, (s Y)) ### NotEquiv 365 57 % 0.20/0.46 367. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (All Y, ((p T_22) <=> (p Y))) (All Y, (p Y)) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) (-. (Ex X, (s X))) (-. (s T_1)) ### Equiv 6 353 % 0.20/0.46 368. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (s T_8) (-. (s T_1)) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) (-. (p T_7)) (All Y, ((p T_22) <=> (p Y))) ### Equiv 355 40 % 0.20/0.46 369. (-. (All Y, (p Y))) (All Y, ((p T_22) <=> (p Y))) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) (-. (s T_1)) (s T_8) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) ### NotAllEx 368 % 0.20/0.46 370. (Ex X, (s X)) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (-. (s T_1)) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) (All Y, ((p T_22) <=> (p Y))) (-. (All Y, (p Y))) ### Exists 369 % 0.20/0.46 371. (-. ((Ex X, (s X)) <=> (All Y, (p Y)))) (-. (s T_1)) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) (All Y, ((p T_22) <=> (p Y))) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) ### NotEquiv 367 370 % 0.20/0.46 372. (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) (-. (p T_7)) (All Y, ((p T_22) <=> (p Y))) (-. (Ex X, (s X))) (-. (s T_1)) ### NotEquiv 6 355 % 0.20/0.46 373. (-. (All Y, (p Y))) (-. (s T_1)) (-. (Ex X, (s X))) (All Y, ((p T_22) <=> (p Y))) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) ### NotAllEx 372 % 0.20/0.46 374. (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (s T_8) (-. (s T_1)) (All Y, ((p T_22) <=> (p Y))) (All Y, (p Y)) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) ### NotEquiv 353 40 % 0.20/0.46 375. (Ex X, (s X)) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) (All Y, (p Y)) (All Y, ((p T_22) <=> (p Y))) (-. (s T_1)) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) ### Exists 374 % 0.20/0.46 376. ((Ex X, (s X)) <=> (All Y, (p Y))) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) (All Y, ((p T_22) <=> (p Y))) (-. (s T_1)) ### Equiv 373 375 % 0.20/0.46 377. (-. (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (All Y, ((p T_22) <=> (p Y))) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) (-. (s T_1)) ### NotEquiv 371 376 % 0.20/0.46 378. (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (-. (s T_1)) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) (All Y, ((p T_22) <=> (p Y))) (r T_13) (All Y, (r Y)) ### NotEquiv 65 377 % 0.20/0.46 379. (-. (All Y, (s Y))) (All Y, (r Y)) (r T_13) (All Y, ((p T_22) <=> (p Y))) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ### NotAllEx 378 % 0.20/0.46 380. (Ex X, (r X)) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) (All Y, ((p T_22) <=> (p Y))) (All Y, (r Y)) (-. (All Y, (s Y))) ### Exists 379 % 0.20/0.46 381. (-. ((Ex X, (r X)) <=> (All Y, (s Y)))) (All Y, ((p T_22) <=> (p Y))) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) (All Y, (r Y)) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ### NotEquiv 366 380 % 0.20/0.46 382. (Ex X, (All Y, ((q X) <=> (q Y)))) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (All Y, (r Y)) (-. (Ex X, (q X))) (All Y, ((p T_22) <=> (p Y))) (-. ((Ex X, (r X)) <=> (All Y, (s Y)))) ### Exists 381 % 0.20/0.46 383. (-. ((Ex X, (All Y, ((q X) <=> (q Y)))) <=> ((Ex X, (r X)) <=> (All Y, (s Y))))) (All Y, ((p T_22) <=> (p Y))) (-. (Ex X, (q X))) (All Y, (r Y)) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ### NotEquiv 352 382 % 0.20/0.46 384. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (All Y, (r Y)) (-. (Ex X, (r X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) (All Y, ((p T_22) <=> (p Y))) (All Y, (s Y)) ### Equiv 349 57 % 0.20/0.46 385. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (-. (s T_1)) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) (All Y, ((p T_22) <=> (p Y))) (r T_13) (All Y, (r Y)) ### Equiv 65 336 % 0.20/0.46 386. (-. (All Y, (s Y))) (All Y, (r Y)) (r T_13) (All Y, ((p T_22) <=> (p Y))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) ### NotAllEx 385 % 0.20/0.46 387. (Ex X, (r X)) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) (All Y, ((p T_22) <=> (p Y))) (All Y, (r Y)) (-. (All Y, (s Y))) ### Exists 386 % 0.20/0.46 388. (-. ((Ex X, (r X)) <=> (All Y, (s Y)))) (All Y, ((p T_22) <=> (p Y))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (All Y, (r Y)) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) ### NotEquiv 384 387 % 0.20/0.46 389. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (All Y, (r Y)) (-. (Ex X, (r X))) (-. (s T_1)) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) (All Y, ((p T_22) <=> (p Y))) ### Equiv 377 57 % 0.20/0.46 390. (-. (All Y, (s Y))) (All Y, ((p T_22) <=> (p Y))) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) (-. (Ex X, (r X))) (All Y, (r Y)) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) ### NotAllEx 389 % 0.20/0.46 391. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) (All Y, ((p T_22) <=> (p Y))) (All Y, (s Y)) (r T_13) (All Y, (r Y)) ### Equiv 65 365 % 0.20/0.46 392. (Ex X, (r X)) (All Y, (r Y)) (All Y, (s Y)) (All Y, ((p T_22) <=> (p Y))) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) ### Exists 391 % 0.20/0.47 393. ((Ex X, (r X)) <=> (All Y, (s Y))) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (All Y, (r Y)) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) (All Y, ((p T_22) <=> (p Y))) ### Equiv 390 392 % 0.20/0.47 394. (Ex X, (All Y, ((q X) <=> (q Y)))) (All Y, ((p T_22) <=> (p Y))) (-. (Ex X, (q X))) (All Y, (r Y)) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) ((Ex X, (r X)) <=> (All Y, (s Y))) ### Exists 393 % 0.20/0.47 395. ((Ex X, (All Y, ((q X) <=> (q Y)))) <=> ((Ex X, (r X)) <=> (All Y, (s Y)))) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (All Y, (r Y)) (-. (Ex X, (q X))) (All Y, ((p T_22) <=> (p Y))) ### Equiv 388 394 % 0.20/0.47 396. (((Ex X, (All Y, ((q X) <=> (q Y)))) <=> ((Ex X, (r X)) <=> (All Y, (s Y)))) <=> ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (All Y, (r Y)) (-. (Ex X, (q X))) (All Y, ((p T_22) <=> (p Y))) ### Equiv 383 395 % 0.20/0.47 397. ((Ex X, (p X)) <=> (All Y, (q Y))) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (All Y, (p Y)) (All Y, ((p T_22) <=> (p Y))) ### Equiv 312 154 % 0.20/0.47 398. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (All Y, ((p T_22) <=> (p Y))) (All Y, (p Y)) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) (-. (Ex X, (s X))) (-. (s T_1)) ### Equiv 6 397 % 0.20/0.47 399. (-. ((Ex X, (p X)) <=> (All Y, (q Y)))) (All Y, ((p T_22) <=> (p Y))) (-. (p T_7)) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) ### NotEquiv 154 325 % 0.20/0.47 400. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (s T_8) (-. (s T_1)) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) (-. (p T_7)) (All Y, ((p T_22) <=> (p Y))) ### Equiv 399 40 % 0.20/0.47 401. (-. (All Y, (p Y))) (All Y, ((p T_22) <=> (p Y))) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (s T_1)) (s T_8) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) ### NotAllEx 400 % 0.20/0.47 402. (Ex X, (s X)) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (-. (s T_1)) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) (All Y, ((p T_22) <=> (p Y))) (-. (All Y, (p Y))) ### Exists 401 % 0.20/0.47 403. (-. ((Ex X, (s X)) <=> (All Y, (p Y)))) (-. (s T_1)) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (All Y, ((p T_22) <=> (p Y))) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) ### NotEquiv 398 402 % 0.20/0.47 404. (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) (-. (p T_7)) (All Y, ((p T_22) <=> (p Y))) (-. (Ex X, (s X))) (-. (s T_1)) ### NotEquiv 6 399 % 0.20/0.47 405. (-. (All Y, (p Y))) (-. (s T_1)) (-. (Ex X, (s X))) (All Y, ((p T_22) <=> (p Y))) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) ### NotAllEx 404 % 0.20/0.47 406. (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (s T_8) (-. (s T_1)) (All Y, ((p T_22) <=> (p Y))) (All Y, (p Y)) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) ### NotEquiv 397 40 % 0.20/0.47 407. (Ex X, (s X)) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (All Y, (p Y)) (All Y, ((p T_22) <=> (p Y))) (-. (s T_1)) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) ### Exists 406 % 0.20/0.47 408. ((Ex X, (s X)) <=> (All Y, (p Y))) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) (All Y, ((p T_22) <=> (p Y))) (-. (s T_1)) ### Equiv 405 407 % 0.20/0.47 409. (-. (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (All Y, ((p T_22) <=> (p Y))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) (-. (s T_1)) ### NotEquiv 403 408 % 0.20/0.47 410. (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (-. (s T_1)) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (All Y, ((p T_22) <=> (p Y))) (-. (Ex X, (r X))) (-. (r T_19)) ### NotEquiv 148 409 % 0.20/0.47 411. (-. (All Y, (s Y))) (-. (r T_19)) (-. (Ex X, (r X))) (All Y, ((p T_22) <=> (p Y))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ### NotAllEx 410 % 0.20/0.47 412. (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (All Y, (s Y)) (-. (Ex X, (s X))) (All Y, ((p T_22) <=> (p Y))) (All Y, (p Y)) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) ### NotEquiv 397 72 % 0.20/0.47 413. (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) (-. (p T_7)) (All Y, ((p T_22) <=> (p Y))) (s T_8) (All Y, (s Y)) ### NotEquiv 79 399 % 0.20/0.47 414. (-. (All Y, (p Y))) (All Y, (s Y)) (s T_8) (All Y, ((p T_22) <=> (p Y))) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) ### NotAllEx 413 % 0.20/0.47 415. (Ex X, (s X)) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) (All Y, ((p T_22) <=> (p Y))) (All Y, (s Y)) (-. (All Y, (p Y))) ### Exists 414 % 0.20/0.47 416. (-. ((Ex X, (s X)) <=> (All Y, (p Y)))) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (All Y, ((p T_22) <=> (p Y))) (All Y, (s Y)) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) ### NotEquiv 412 415 % 0.20/0.47 417. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (All Y, (s Y)) (-. (Ex X, (s X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) (-. (p T_7)) (All Y, ((p T_22) <=> (p Y))) ### Equiv 399 72 % 0.20/0.47 418. (-. (All Y, (p Y))) (All Y, ((p T_22) <=> (p Y))) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (s X))) (All Y, (s Y)) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) ### NotAllEx 417 % 0.20/0.47 419. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (All Y, ((p T_22) <=> (p Y))) (All Y, (p Y)) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) (s T_8) (All Y, (s Y)) ### Equiv 79 397 % 0.20/0.47 420. (Ex X, (s X)) (All Y, (s Y)) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (All Y, (p Y)) (All Y, ((p T_22) <=> (p Y))) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) ### Exists 419 % 0.20/0.47 421. ((Ex X, (s X)) <=> (All Y, (p Y))) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (All Y, (s Y)) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) (All Y, ((p T_22) <=> (p Y))) ### Equiv 418 420 % 0.20/0.47 422. (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (All Y, (s Y)) (All Y, ((p T_22) <=> (p Y))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) ### Equiv 416 421 % 0.20/0.47 423. (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (r T_13) (-. (r T_19)) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (All Y, ((p T_22) <=> (p Y))) (All Y, (s Y)) ### NotEquiv 422 191 % 0.20/0.47 424. (Ex X, (r X)) (All Y, (s Y)) (All Y, ((p T_22) <=> (p Y))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) (-. (r T_19)) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ### Exists 423 % 0.20/0.47 425. ((Ex X, (r X)) <=> (All Y, (s Y))) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (All Y, ((p T_22) <=> (p Y))) (-. (r T_19)) ### Equiv 411 424 % 0.20/0.48 426. (-. ((Ex X, (p X)) <=> (All Y, (q Y)))) (All Y, ((q T_16) <=> (q Y))) (q T_20) (All Y, (p Y)) (All Y, ((p T_22) <=> (p Y))) ### NotEquiv 312 205 % 0.20/0.48 427. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (All Y, (s Y)) (-. (Ex X, (s X))) (All Y, ((p T_22) <=> (p Y))) (All Y, (p Y)) (q T_20) (All Y, ((q T_16) <=> (q Y))) ### Equiv 426 72 % 0.20/0.48 428. ((Ex X, (p X)) <=> (All Y, (q Y))) (All Y, ((p T_22) <=> (p Y))) (-. (p T_7)) (All Y, ((q T_16) <=> (q Y))) (q T_20) ### Equiv 205 325 % 0.20/0.48 429. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (q T_20) (All Y, ((q T_16) <=> (q Y))) (-. (p T_7)) (All Y, ((p T_22) <=> (p Y))) (s T_8) (All Y, (s Y)) ### Equiv 79 428 % 0.20/0.48 430. (-. (All Y, (p Y))) (All Y, (s Y)) (s T_8) (All Y, ((p T_22) <=> (p Y))) (All Y, ((q T_16) <=> (q Y))) (q T_20) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) ### NotAllEx 429 % 0.20/0.48 431. (Ex X, (s X)) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (q T_20) (All Y, ((q T_16) <=> (q Y))) (All Y, ((p T_22) <=> (p Y))) (All Y, (s Y)) (-. (All Y, (p Y))) ### Exists 430 % 0.20/0.48 432. (-. ((Ex X, (s X)) <=> (All Y, (p Y)))) (All Y, ((q T_16) <=> (q Y))) (q T_20) (All Y, ((p T_22) <=> (p Y))) (All Y, (s Y)) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) ### NotEquiv 427 431 % 0.20/0.48 433. (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (All Y, (s Y)) (-. (Ex X, (s X))) (q T_20) (All Y, ((q T_16) <=> (q Y))) (-. (p T_7)) (All Y, ((p T_22) <=> (p Y))) ### NotEquiv 428 72 % 0.20/0.48 434. (-. (All Y, (p Y))) (All Y, ((p T_22) <=> (p Y))) (All Y, ((q T_16) <=> (q Y))) (q T_20) (-. (Ex X, (s X))) (All Y, (s Y)) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) ### NotAllEx 433 % 0.20/0.48 435. (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (All Y, ((p T_22) <=> (p Y))) (All Y, (p Y)) (q T_20) (All Y, ((q T_16) <=> (q Y))) (s T_8) (All Y, (s Y)) ### NotEquiv 79 426 % 0.20/0.48 436. (Ex X, (s X)) (All Y, (s Y)) (All Y, ((q T_16) <=> (q Y))) (q T_20) (All Y, (p Y)) (All Y, ((p T_22) <=> (p Y))) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) ### Exists 435 % 0.20/0.48 437. ((Ex X, (s X)) <=> (All Y, (p Y))) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (All Y, (s Y)) (q T_20) (All Y, ((q T_16) <=> (q Y))) (All Y, ((p T_22) <=> (p Y))) ### Equiv 434 436 % 0.20/0.48 438. (-. (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (All Y, (s Y)) (All Y, ((p T_22) <=> (p Y))) (q T_20) (All Y, ((q T_16) <=> (q Y))) ### NotEquiv 432 437 % 0.20/0.48 439. (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (All Y, ((q T_16) <=> (q Y))) (q T_20) (All Y, ((p T_22) <=> (p Y))) (All Y, (s Y)) (-. (Ex X, (r X))) (-. (r T_19)) ### NotEquiv 148 438 % 0.20/0.48 440. (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (All Y, ((p T_22) <=> (p Y))) (All Y, (p Y)) (q T_20) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (s X))) (-. (s T_1)) ### NotEquiv 6 426 % 0.20/0.48 441. (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (s T_8) (-. (s T_1)) (q T_20) (All Y, ((q T_16) <=> (q Y))) (-. (p T_7)) (All Y, ((p T_22) <=> (p Y))) ### NotEquiv 428 40 % 0.20/0.48 442. (-. (All Y, (p Y))) (All Y, ((p T_22) <=> (p Y))) (All Y, ((q T_16) <=> (q Y))) (q T_20) (-. (s T_1)) (s T_8) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) ### NotAllEx 441 % 0.20/0.48 443. (Ex X, (s X)) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (-. (s T_1)) (q T_20) (All Y, ((q T_16) <=> (q Y))) (All Y, ((p T_22) <=> (p Y))) (-. (All Y, (p Y))) ### Exists 442 % 0.20/0.48 444. (-. ((Ex X, (s X)) <=> (All Y, (p Y)))) (-. (s T_1)) (All Y, ((q T_16) <=> (q Y))) (q T_20) (All Y, ((p T_22) <=> (p Y))) (-. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) ### NotEquiv 440 443 % 0.20/0.48 445. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (q T_20) (All Y, ((q T_16) <=> (q Y))) (-. (p T_7)) (All Y, ((p T_22) <=> (p Y))) (-. (Ex X, (s X))) (-. (s T_1)) ### Equiv 6 428 % 0.20/0.48 446. (-. (All Y, (p Y))) (-. (s T_1)) (-. (Ex X, (s X))) (All Y, ((p T_22) <=> (p Y))) (All Y, ((q T_16) <=> (q Y))) (q T_20) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) ### NotAllEx 445 % 0.20/0.48 447. ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (s T_8) (-. (s T_1)) (All Y, ((p T_22) <=> (p Y))) (All Y, (p Y)) (q T_20) (All Y, ((q T_16) <=> (q Y))) ### Equiv 426 40 % 0.20/0.48 448. (Ex X, (s X)) (All Y, ((q T_16) <=> (q Y))) (q T_20) (All Y, (p Y)) (All Y, ((p T_22) <=> (p Y))) (-. (s T_1)) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) ### Exists 447 % 0.20/0.48 449. ((Ex X, (s X)) <=> (All Y, (p Y))) ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))) (q T_20) (All Y, ((q T_16) <=> (q Y))) (All Y, ((p T_22) <=> (p Y))) (-. (s T_1)) ### Equiv 446 448 % 0.20/0.48 450. (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))) (All Y, ((p T_22) <=> (p Y))) (q T_20) (All Y, ((q T_16) <=> (q Y))) (-. (s T_1)) ### Equiv 444 449 % 0.20/0.48 451. (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (r T_13) (-. (r T_19)) (-. (s T_1)) (All Y, ((q T_16) <=> (q Y))) (q T_20) (All Y, ((p T_22) <=> (p Y))) ### NotEquiv 450 191 % 0.20/0.48 452. (-. (All Y, (s Y))) (All Y, ((p T_22) <=> (p Y))) (q T_20) (All Y, ((q T_16) <=> (q Y))) (-. (r T_19)) (r T_13) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ### NotAllEx 451 % 0.20/0.48 453. (Ex X, (r X)) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (-. (r T_19)) (All Y, ((q T_16) <=> (q Y))) (q T_20) (All Y, ((p T_22) <=> (p Y))) (-. (All Y, (s Y))) ### Exists 452 % 0.20/0.48 454. (-. ((Ex X, (r X)) <=> (All Y, (s Y)))) (-. (r T_19)) (All Y, ((p T_22) <=> (p Y))) (q T_20) (All Y, ((q T_16) <=> (q Y))) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ### NotEquiv 439 453 % 0.20/0.48 455. (Ex X, (All Y, ((q X) <=> (q Y)))) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (q T_20) (All Y, ((p T_22) <=> (p Y))) (-. (r T_19)) (-. ((Ex X, (r X)) <=> (All Y, (s Y)))) ### Exists 454 % 0.20/0.48 456. (-. ((Ex X, (All Y, ((q X) <=> (q Y)))) <=> ((Ex X, (r X)) <=> (All Y, (s Y))))) (-. (r T_19)) (All Y, ((p T_22) <=> (p Y))) (q T_20) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ### NotEquiv 425 455 % 0.20/0.48 457. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (All Y, ((p T_22) <=> (p Y))) (All Y, (s Y)) (-. (Ex X, (r X))) (-. (r T_19)) ### Equiv 148 422 % 0.20/0.48 458. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (r T_13) (-. (r T_19)) (-. (s T_1)) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (All Y, ((p T_22) <=> (p Y))) ### Equiv 409 191 % 0.20/0.48 459. (-. (All Y, (s Y))) (All Y, ((p T_22) <=> (p Y))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) (-. (r T_19)) (r T_13) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) ### NotAllEx 458 % 0.20/0.48 460. (Ex X, (r X)) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (-. (r T_19)) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (All Y, ((p T_22) <=> (p Y))) (-. (All Y, (s Y))) ### Exists 459 % 0.20/0.48 461. (-. ((Ex X, (r X)) <=> (All Y, (s Y)))) (-. (r T_19)) (All Y, ((p T_22) <=> (p Y))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) ### NotEquiv 457 460 % 0.20/0.48 462. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (-. (s T_1)) (All Y, ((q T_16) <=> (q Y))) (q T_20) (All Y, ((p T_22) <=> (p Y))) (-. (Ex X, (r X))) (-. (r T_19)) ### Equiv 148 450 % 0.20/0.48 463. (-. (All Y, (s Y))) (-. (r T_19)) (-. (Ex X, (r X))) (All Y, ((p T_22) <=> (p Y))) (q T_20) (All Y, ((q T_16) <=> (q Y))) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) ### NotAllEx 462 % 0.20/0.48 464. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (r T_13) (-. (r T_19)) (All Y, ((q T_16) <=> (q Y))) (q T_20) (All Y, ((p T_22) <=> (p Y))) (All Y, (s Y)) ### Equiv 438 191 % 0.20/0.48 465. (Ex X, (r X)) (All Y, (s Y)) (All Y, ((p T_22) <=> (p Y))) (q T_20) (All Y, ((q T_16) <=> (q Y))) (-. (r T_19)) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) ### Exists 464 % 0.20/0.48 466. ((Ex X, (r X)) <=> (All Y, (s Y))) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (All Y, ((q T_16) <=> (q Y))) (q T_20) (All Y, ((p T_22) <=> (p Y))) (-. (r T_19)) ### Equiv 463 465 % 0.20/0.48 467. (Ex X, (All Y, ((q X) <=> (q Y)))) (-. (r T_19)) (All Y, ((p T_22) <=> (p Y))) (q T_20) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) ((Ex X, (r X)) <=> (All Y, (s Y))) ### Exists 466 % 0.20/0.48 468. ((Ex X, (All Y, ((q X) <=> (q Y)))) <=> ((Ex X, (r X)) <=> (All Y, (s Y)))) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (q T_20) (All Y, ((p T_22) <=> (p Y))) (-. (r T_19)) ### Equiv 461 467 % 0.20/0.48 469. (((Ex X, (All Y, ((q X) <=> (q Y)))) <=> ((Ex X, (r X)) <=> (All Y, (s Y)))) <=> ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (q T_20) (All Y, ((p T_22) <=> (p Y))) (-. (r T_19)) ### Equiv 456 468 % 0.20/0.48 470. (-. (All Y, (r Y))) (All Y, ((p T_22) <=> (p Y))) (q T_20) (((Ex X, (All Y, ((q X) <=> (q Y)))) <=> ((Ex X, (r X)) <=> (All Y, (s Y)))) <=> ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ### NotAllEx 469 % 0.20/0.48 471. (Ex X, (q X)) (((Ex X, (All Y, ((q X) <=> (q Y)))) <=> ((Ex X, (r X)) <=> (All Y, (s Y)))) <=> ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (All Y, ((p T_22) <=> (p Y))) (-. (All Y, (r Y))) ### Exists 470 % 0.20/0.48 472. (-. ((Ex X, (q X)) <=> (All Y, (r Y)))) (All Y, ((p T_22) <=> (p Y))) (((Ex X, (All Y, ((q X) <=> (q Y)))) <=> ((Ex X, (r X)) <=> (All Y, (s Y)))) <=> ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ### NotEquiv 396 471 % 0.20/0.48 473. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (-. (s T_1)) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) (All Y, ((p T_22) <=> (p Y))) (-. (Ex X, (r X))) (-. (r T_19)) ### Equiv 148 336 % 0.20/0.48 474. (-. (All Y, (s Y))) (-. (r T_19)) (-. (Ex X, (r X))) (All Y, ((p T_22) <=> (p Y))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) ### NotAllEx 473 % 0.20/0.48 475. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (r T_13) (-. (r T_19)) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) (All Y, ((p T_22) <=> (p Y))) (All Y, (s Y)) ### Equiv 349 191 % 0.20/0.48 476. (Ex X, (r X)) (All Y, (s Y)) (All Y, ((p T_22) <=> (p Y))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (r T_19)) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) ### Exists 475 % 0.20/0.48 477. ((Ex X, (r X)) <=> (All Y, (s Y))) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) (All Y, ((p T_22) <=> (p Y))) (-. (r T_19)) ### Equiv 474 476 % 0.20/0.48 478. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) (All Y, ((p T_22) <=> (p Y))) (All Y, (s Y)) (-. (Ex X, (r X))) (-. (r T_19)) ### Equiv 148 365 % 0.20/0.48 479. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (r T_13) (-. (r T_19)) (-. (s T_1)) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) (All Y, ((p T_22) <=> (p Y))) ### Equiv 377 191 % 0.20/0.48 480. (-. (All Y, (s Y))) (All Y, ((p T_22) <=> (p Y))) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) (-. (r T_19)) (r T_13) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) ### NotAllEx 479 % 0.20/0.48 481. (Ex X, (r X)) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (-. (r T_19)) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) (All Y, ((p T_22) <=> (p Y))) (-. (All Y, (s Y))) ### Exists 480 % 0.20/0.48 482. (-. ((Ex X, (r X)) <=> (All Y, (s Y)))) (-. (r T_19)) (All Y, ((p T_22) <=> (p Y))) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) ### NotEquiv 478 481 % 0.20/0.48 483. (Ex X, (All Y, ((q X) <=> (q Y)))) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (-. (Ex X, (q X))) (All Y, ((p T_22) <=> (p Y))) (-. (r T_19)) (-. ((Ex X, (r X)) <=> (All Y, (s Y)))) ### Exists 482 % 0.20/0.48 484. (-. ((Ex X, (All Y, ((q X) <=> (q Y)))) <=> ((Ex X, (r X)) <=> (All Y, (s Y))))) (-. (r T_19)) (All Y, ((p T_22) <=> (p Y))) (-. (Ex X, (q X))) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) ### NotEquiv 477 483 % 0.20/0.48 485. (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) (All Y, ((p T_22) <=> (p Y))) (All Y, (s Y)) (-. (Ex X, (r X))) (-. (r T_19)) ### NotEquiv 148 349 % 0.20/0.48 486. (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (r T_13) (-. (r T_19)) (-. (s T_1)) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) (All Y, ((p T_22) <=> (p Y))) ### NotEquiv 336 191 % 0.20/0.48 487. (-. (All Y, (s Y))) (All Y, ((p T_22) <=> (p Y))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (r T_19)) (r T_13) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ### NotAllEx 486 % 0.20/0.48 488. (Ex X, (r X)) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (-. (r T_19)) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. (Ex X, (q X))) (All Y, ((p T_22) <=> (p Y))) (-. (All Y, (s Y))) ### Exists 487 % 0.20/0.48 489. (-. ((Ex X, (r X)) <=> (All Y, (s Y)))) (-. (r T_19)) (All Y, ((p T_22) <=> (p Y))) (-. (Ex X, (q X))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ### NotEquiv 485 488 % 0.20/0.48 490. (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (-. (s T_1)) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) (All Y, ((p T_22) <=> (p Y))) (-. (Ex X, (r X))) (-. (r T_19)) ### NotEquiv 148 377 % 0.20/0.48 491. (-. (All Y, (s Y))) (-. (r T_19)) (-. (Ex X, (r X))) (All Y, ((p T_22) <=> (p Y))) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ### NotAllEx 490 % 0.20/0.48 492. (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (r T_13) (-. (r T_19)) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) (All Y, ((p T_22) <=> (p Y))) (All Y, (s Y)) ### NotEquiv 365 191 % 0.20/0.48 493. (Ex X, (r X)) (All Y, (s Y)) (All Y, ((p T_22) <=> (p Y))) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (q X))) (-. (r T_19)) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ### Exists 492 % 0.20/0.48 494. ((Ex X, (r X)) <=> (All Y, (s Y))) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (-. (Ex X, (q X))) (All Y, ((q T_16) <=> (q Y))) (All Y, ((p T_22) <=> (p Y))) (-. (r T_19)) ### Equiv 491 493 % 0.20/0.48 495. (Ex X, (All Y, ((q X) <=> (q Y)))) (-. (r T_19)) (All Y, ((p T_22) <=> (p Y))) (-. (Ex X, (q X))) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ((Ex X, (r X)) <=> (All Y, (s Y))) ### Exists 494 % 0.20/0.48 496. ((Ex X, (All Y, ((q X) <=> (q Y)))) <=> ((Ex X, (r X)) <=> (All Y, (s Y)))) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (-. (Ex X, (q X))) (All Y, ((p T_22) <=> (p Y))) (-. (r T_19)) ### Equiv 489 495 % 0.20/0.48 497. (-. (((Ex X, (All Y, ((q X) <=> (q Y)))) <=> ((Ex X, (r X)) <=> (All Y, (s Y)))) <=> ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))))) (-. (Ex X, (q X))) (All Y, ((p T_22) <=> (p Y))) (-. (r T_19)) ### NotEquiv 484 496 % 0.20/0.48 498. (-. (All Y, (r Y))) (All Y, ((p T_22) <=> (p Y))) (-. (Ex X, (q X))) (-. (((Ex X, (All Y, ((q X) <=> (q Y)))) <=> ((Ex X, (r X)) <=> (All Y, (s Y)))) <=> ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))))) ### NotAllEx 497 % 0.20/0.48 499. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (All Y, (r Y)) (-. (Ex X, (r X))) (-. (s T_1)) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (All Y, ((p T_22) <=> (p Y))) ### Equiv 409 57 % 0.20/0.48 500. (-. (All Y, (s Y))) (All Y, ((p T_22) <=> (p Y))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) (-. (Ex X, (r X))) (All Y, (r Y)) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) ### NotAllEx 499 % 0.20/0.48 501. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (All Y, ((p T_22) <=> (p Y))) (All Y, (s Y)) (r T_13) (All Y, (r Y)) ### Equiv 65 422 % 0.20/0.48 502. (Ex X, (r X)) (All Y, (r Y)) (All Y, (s Y)) (All Y, ((p T_22) <=> (p Y))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) ### Exists 501 % 0.20/0.48 503. ((Ex X, (r X)) <=> (All Y, (s Y))) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (All Y, (r Y)) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (All Y, ((p T_22) <=> (p Y))) ### Equiv 500 502 % 0.20/0.48 504. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (All Y, (r Y)) (-. (Ex X, (r X))) (All Y, ((q T_16) <=> (q Y))) (q T_20) (All Y, ((p T_22) <=> (p Y))) (All Y, (s Y)) ### Equiv 438 57 % 0.20/0.48 505. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (-. (s T_1)) (All Y, ((q T_16) <=> (q Y))) (q T_20) (All Y, ((p T_22) <=> (p Y))) (r T_13) (All Y, (r Y)) ### Equiv 65 450 % 0.20/0.48 506. (-. (All Y, (s Y))) (All Y, (r Y)) (r T_13) (All Y, ((p T_22) <=> (p Y))) (q T_20) (All Y, ((q T_16) <=> (q Y))) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) ### NotAllEx 505 % 0.20/0.48 507. (Ex X, (r X)) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (All Y, ((q T_16) <=> (q Y))) (q T_20) (All Y, ((p T_22) <=> (p Y))) (All Y, (r Y)) (-. (All Y, (s Y))) ### Exists 506 % 0.20/0.48 508. (-. ((Ex X, (r X)) <=> (All Y, (s Y)))) (All Y, ((p T_22) <=> (p Y))) (q T_20) (All Y, ((q T_16) <=> (q Y))) (All Y, (r Y)) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) ### NotEquiv 504 507 % 0.20/0.48 509. (Ex X, (All Y, ((q X) <=> (q Y)))) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) (All Y, (r Y)) (q T_20) (All Y, ((p T_22) <=> (p Y))) (-. ((Ex X, (r X)) <=> (All Y, (s Y)))) ### Exists 508 % 0.20/0.48 510. (-. ((Ex X, (All Y, ((q X) <=> (q Y)))) <=> ((Ex X, (r X)) <=> (All Y, (s Y))))) (All Y, ((p T_22) <=> (p Y))) (q T_20) (All Y, (r Y)) ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))) ### NotEquiv 503 509 % 0.20/0.48 511. (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (All Y, (r Y)) (-. (Ex X, (r X))) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (All Y, ((p T_22) <=> (p Y))) (All Y, (s Y)) ### NotEquiv 422 57 % 0.20/0.48 512. (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (-. (s T_1)) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (All Y, ((p T_22) <=> (p Y))) (r T_13) (All Y, (r Y)) ### NotEquiv 65 409 % 0.20/0.48 513. (-. (All Y, (s Y))) (All Y, (r Y)) (r T_13) (All Y, ((p T_22) <=> (p Y))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ### NotAllEx 512 % 0.20/0.48 514. (Ex X, (r X)) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (q T_20) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (All Y, ((p T_22) <=> (p Y))) (All Y, (r Y)) (-. (All Y, (s Y))) ### Exists 513 % 0.20/0.48 515. (-. ((Ex X, (r X)) <=> (All Y, (s Y)))) (All Y, ((p T_22) <=> (p Y))) (-. (Ex X, (All Y, ((q X) <=> (q Y))))) (q T_20) (All Y, (r Y)) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ### NotEquiv 511 514 % 0.20/0.48 516. (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (All Y, (r Y)) (-. (Ex X, (r X))) (-. (s T_1)) (All Y, ((q T_16) <=> (q Y))) (q T_20) (All Y, ((p T_22) <=> (p Y))) ### NotEquiv 450 57 % 0.20/0.48 517. (-. (All Y, (s Y))) (All Y, ((p T_22) <=> (p Y))) (q T_20) (All Y, ((q T_16) <=> (q Y))) (-. (Ex X, (r X))) (All Y, (r Y)) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ### NotAllEx 516 % 0.20/0.48 518. (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (All Y, ((q T_16) <=> (q Y))) (q T_20) (All Y, ((p T_22) <=> (p Y))) (All Y, (s Y)) (r T_13) (All Y, (r Y)) ### NotEquiv 65 438 % 0.20/0.48 519. (Ex X, (r X)) (All Y, (r Y)) (All Y, (s Y)) (All Y, ((p T_22) <=> (p Y))) (q T_20) (All Y, ((q T_16) <=> (q Y))) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ### Exists 518 % 0.20/0.48 520. ((Ex X, (r X)) <=> (All Y, (s Y))) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (All Y, (r Y)) (All Y, ((q T_16) <=> (q Y))) (q T_20) (All Y, ((p T_22) <=> (p Y))) ### Equiv 517 519 % 0.20/0.48 521. (Ex X, (All Y, ((q X) <=> (q Y)))) (All Y, ((p T_22) <=> (p Y))) (q T_20) (All Y, (r Y)) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) ((Ex X, (r X)) <=> (All Y, (s Y))) ### Exists 520 % 0.20/0.48 522. ((Ex X, (All Y, ((q X) <=> (q Y)))) <=> ((Ex X, (r X)) <=> (All Y, (s Y)))) (-. ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))) (All Y, (r Y)) (q T_20) (All Y, ((p T_22) <=> (p Y))) ### Equiv 515 521 % 0.20/0.48 523. (-. (((Ex X, (All Y, ((q X) <=> (q Y)))) <=> ((Ex X, (r X)) <=> (All Y, (s Y)))) <=> ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))))) (All Y, (r Y)) (q T_20) (All Y, ((p T_22) <=> (p Y))) ### NotEquiv 510 522 % 0.20/0.48 524. (Ex X, (q X)) (All Y, ((p T_22) <=> (p Y))) (All Y, (r Y)) (-. (((Ex X, (All Y, ((q X) <=> (q Y)))) <=> ((Ex X, (r X)) <=> (All Y, (s Y)))) <=> ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))))) ### Exists 523 % 0.20/0.48 525. ((Ex X, (q X)) <=> (All Y, (r Y))) (-. (((Ex X, (All Y, ((q X) <=> (q Y)))) <=> ((Ex X, (r X)) <=> (All Y, (s Y)))) <=> ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))))) (All Y, ((p T_22) <=> (p Y))) ### Equiv 498 524 % 0.20/0.48 526. (-. (((Ex X, (q X)) <=> (All Y, (r Y))) <=> (((Ex X, (All Y, ((q X) <=> (q Y)))) <=> ((Ex X, (r X)) <=> (All Y, (s Y)))) <=> ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))))) (All Y, ((p T_22) <=> (p Y))) ### NotEquiv 472 525 % 0.20/0.48 527. (Ex X, (All Y, ((p X) <=> (p Y)))) (-. (((Ex X, (q X)) <=> (All Y, (r Y))) <=> (((Ex X, (All Y, ((q X) <=> (q Y)))) <=> ((Ex X, (r X)) <=> (All Y, (s Y)))) <=> ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y))))))))) ### Exists 526 % 0.20/0.48 528. (-. ((Ex X, (All Y, ((p X) <=> (p Y)))) <=> (((Ex X, (q X)) <=> (All Y, (r Y))) <=> (((Ex X, (All Y, ((q X) <=> (q Y)))) <=> ((Ex X, (r X)) <=> (All Y, (s Y)))) <=> ((Ex X, (All Y, ((r X) <=> (r Y)))) <=> (((Ex X, (s X)) <=> (All Y, (p Y))) <=> ((Ex X, (All Y, ((s X) <=> (s Y)))) <=> ((Ex X, (p X)) <=> (All Y, (q Y)))))))))) ### NotEquiv 306 527 % 0.20/0.48 % SZS output end Proof % 0.20/0.48 (* END-PROOF *) %------------------------------------------------------------------------------