%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SYN036+2 : TPTP v8.1.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n015.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:40:23 EDT 2022 % Result : Theorem 0.18s 0.40s % Output : Proof 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.01/0.12 % Problem : SYN036+2 : TPTP v8.1.0. Released v2.0.0. % 0.01/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n015.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Mon Jul 11 20:39:24 EDT 2022 % 0.12/0.33 % CPUTime : % 0.18/0.40 % SZS status Theorem % 0.18/0.40 (* PROOF-FOUND *) % 0.18/0.40 (* BEGIN-PROOF *) % 0.18/0.40 % SZS output start Proof % 0.18/0.40 1. (big_p T_0) (-. (big_p T_0)) ### Axiom % 0.18/0.40 2. (-. (Ex U1, (big_p U1))) (big_p T_0) ### NotExists 1 % 0.18/0.40 3. (-. (big_p T_1)) (big_p T_1) ### Axiom % 0.18/0.40 4. (-. ((big_p T_1) <=> (big_p T_0))) (-. (big_p T_1)) (-. (Ex U1, (big_p U1))) ### NotEquiv 2 3 % 0.18/0.40 5. (-. (All Y, ((big_p T_1) <=> (big_p Y)))) (-. (Ex U1, (big_p U1))) (-. (big_p T_1)) ### NotAllEx 4 % 0.18/0.40 6. (-. (Ex X, (All Y, ((big_p X) <=> (big_p Y))))) (-. (big_p T_1)) (-. (Ex U1, (big_p U1))) ### NotExists 5 % 0.18/0.40 7. (big_q T_2) (-. (big_q T_2)) ### Axiom % 0.18/0.40 8. (-. (Ex U, (big_q U))) (big_q T_2) ### NotExists 7 % 0.18/0.40 9. (-. (big_q T_3)) (big_q T_3) ### Axiom % 0.18/0.40 10. (-. ((big_q T_3) <=> (big_q T_2))) (-. (big_q T_3)) (-. (Ex U, (big_q U))) ### NotEquiv 8 9 % 0.18/0.40 11. (-. (All Y1, ((big_q T_3) <=> (big_q Y1)))) (-. (Ex U, (big_q U))) (-. (big_q T_3)) ### NotAllEx 10 % 0.18/0.40 12. (-. (Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1))))) (-. (big_q T_3)) (-. (Ex U, (big_q U))) ### NotExists 11 % 0.18/0.40 13. (-. (All W1, (big_q W1))) (-. (Ex U, (big_q U))) (-. (Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1))))) ### NotAllEx 12 % 0.18/0.40 14. (-. ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1)))) (-. (Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1))))) (-. (Ex U, (big_q U))) (-. (big_p T_1)) (-. (Ex X, (All Y, ((big_p X) <=> (big_p Y))))) ### NotEquiv 6 13 % 0.18/0.40 15. (-. (big_q T_4)) (big_q T_4) ### Axiom % 0.18/0.40 16. (All W1, (big_q W1)) (-. (big_q T_4)) ### All 15 % 0.18/0.40 17. (big_q T_4) (-. (big_q T_4)) ### Axiom % 0.18/0.40 18. (-. (Ex U, (big_q U))) (big_q T_4) ### NotExists 17 % 0.18/0.40 19. ((big_q T_4) <=> (big_q zenon_X5)) (-. (Ex U, (big_q U))) (All W1, (big_q W1)) ### Equiv 16 18 % 0.18/0.40 20. (All Y1, ((big_q T_4) <=> (big_q Y1))) (All W1, (big_q W1)) (-. (Ex U, (big_q U))) ### All 19 % 0.18/0.40 21. ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1))) (-. (Ex U, (big_q U))) (All Y1, ((big_q T_4) <=> (big_q Y1))) (-. (big_p T_1)) (-. (Ex X, (All Y, ((big_p X) <=> (big_p Y))))) ### Equiv 6 20 % 0.18/0.40 22. (Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) (-. (Ex X, (All Y, ((big_p X) <=> (big_p Y))))) (-. (big_p T_1)) (-. (Ex U, (big_q U))) ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1))) ### Exists 21 % 0.18/0.40 23. ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1)))) (-. (Ex X, (All Y, ((big_p X) <=> (big_p Y))))) (-. (big_p T_1)) (-. (Ex U, (big_q U))) ### Equiv 14 22 % 0.18/0.40 24. (-. (All W, (big_p W))) (-. (Ex U, (big_q U))) (-. (Ex X, (All Y, ((big_p X) <=> (big_p Y))))) ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1)))) ### NotAllEx 23 % 0.18/0.40 25. (big_q T_6) (-. (big_q T_6)) ### Axiom % 0.18/0.40 26. (-. (big_q T_7)) (big_q T_7) ### Axiom % 0.18/0.40 27. (All W1, (big_q W1)) (-. (big_q T_7)) ### All 26 % 0.18/0.40 28. (-. ((big_q T_6) <=> (big_q T_7))) (All W1, (big_q W1)) (big_q T_6) ### NotEquiv 25 27 % 0.18/0.40 29. (-. (All Y1, ((big_q T_6) <=> (big_q Y1)))) (big_q T_6) (All W1, (big_q W1)) ### NotAllEx 28 % 0.18/0.40 30. (-. (Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1))))) (All W1, (big_q W1)) (big_q T_6) ### NotExists 29 % 0.18/0.40 31. (big_p T_8) (-. (big_p T_8)) ### Axiom % 0.18/0.40 32. (-. (big_p T_9)) (big_p T_9) ### Axiom % 0.18/0.40 33. (All W, (big_p W)) (-. (big_p T_9)) ### All 32 % 0.18/0.40 34. (-. ((big_p T_8) <=> (big_p T_9))) (All W, (big_p W)) (big_p T_8) ### NotEquiv 31 33 % 0.18/0.40 35. (-. (All Y, ((big_p T_8) <=> (big_p Y)))) (big_p T_8) (All W, (big_p W)) ### NotAllEx 34 % 0.18/0.40 36. (-. (Ex X, (All Y, ((big_p X) <=> (big_p Y))))) (All W, (big_p W)) (big_p T_8) ### NotExists 35 % 0.18/0.40 37. (Ex U1, (big_p U1)) (All W, (big_p W)) (-. (Ex X, (All Y, ((big_p X) <=> (big_p Y))))) ### Exists 36 % 0.18/0.40 38. (-. ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1)))) (-. (Ex X, (All Y, ((big_p X) <=> (big_p Y))))) (All W, (big_p W)) (big_q T_6) (-. (Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1))))) ### NotEquiv 30 37 % 0.18/0.40 39. (big_q T_6) (-. (big_q T_6)) ### Axiom % 0.18/0.40 40. (-. (big_q T_4)) (big_q T_4) ### Axiom % 0.18/0.40 41. ((big_q T_4) <=> (big_q T_6)) (-. (big_q T_4)) (big_q T_6) ### Equiv 39 40 % 0.18/0.40 42. (All Y1, ((big_q T_4) <=> (big_q Y1))) (big_q T_6) (-. (big_q T_4)) ### All 41 % 0.18/0.40 43. (big_q T_4) (-. (big_q T_4)) ### Axiom % 0.18/0.40 44. (-. (big_q T_3)) (big_q T_3) ### Axiom % 0.18/0.40 45. ((big_q T_4) <=> (big_q T_3)) (-. (big_q T_3)) (big_q T_4) ### Equiv 43 44 % 0.18/0.40 46. (All Y1, ((big_q T_4) <=> (big_q Y1))) (big_q T_4) (-. (big_q T_3)) ### All 45 % 0.18/0.40 47. ((big_q T_4) <=> (big_q zenon_X5)) (-. (big_q T_3)) (big_q T_6) (All Y1, ((big_q T_4) <=> (big_q Y1))) ### Equiv 42 46 % 0.18/0.40 48. (All Y1, ((big_q T_4) <=> (big_q Y1))) (big_q T_6) (-. (big_q T_3)) ### All 47 % 0.18/0.40 49. (-. (All W1, (big_q W1))) (big_q T_6) (All Y1, ((big_q T_4) <=> (big_q Y1))) ### NotAllEx 48 % 0.18/0.40 50. ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1))) (-. (Ex X, (All Y, ((big_p X) <=> (big_p Y))))) (All W, (big_p W)) (All Y1, ((big_q T_4) <=> (big_q Y1))) (big_q T_6) ### Equiv 49 37 % 0.18/0.40 51. (Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) (big_q T_6) (All W, (big_p W)) (-. (Ex X, (All Y, ((big_p X) <=> (big_p Y))))) ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1))) ### Exists 50 % 0.18/0.40 52. ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1)))) (big_q T_6) (All W, (big_p W)) (-. (Ex X, (All Y, ((big_p X) <=> (big_p Y))))) ### Equiv 38 51 % 0.18/0.40 53. (Ex U, (big_q U)) (-. (Ex X, (All Y, ((big_p X) <=> (big_p Y))))) (All W, (big_p W)) ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1)))) ### Exists 52 % 0.18/0.40 54. ((Ex U, (big_q U)) <=> (All W, (big_p W))) ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1)))) (-. (Ex X, (All Y, ((big_p X) <=> (big_p Y))))) ### Equiv 24 53 % 0.18/0.40 55. (-. (big_p T_10)) (big_p T_10) ### Axiom % 0.18/0.40 56. (All W, (big_p W)) (-. (big_p T_10)) ### All 55 % 0.18/0.40 57. (big_p T_10) (-. (big_p T_10)) ### Axiom % 0.18/0.40 58. (-. (Ex U1, (big_p U1))) (big_p T_10) ### NotExists 57 % 0.18/0.40 59. ((big_p T_10) <=> (big_p zenon_X11)) (-. (Ex U1, (big_p U1))) (All W, (big_p W)) ### Equiv 56 58 % 0.18/0.40 60. (All Y, ((big_p T_10) <=> (big_p Y))) (All W, (big_p W)) (-. (Ex U1, (big_p U1))) ### All 59 % 0.18/0.40 61. (-. ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1)))) (-. (Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1))))) (-. (Ex U, (big_q U))) (All W, (big_p W)) (All Y, ((big_p T_10) <=> (big_p Y))) ### NotEquiv 60 13 % 0.18/0.40 62. ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1))) (-. (Ex U, (big_q U))) (All Y1, ((big_q T_4) <=> (big_q Y1))) (All W, (big_p W)) (All Y, ((big_p T_10) <=> (big_p Y))) ### Equiv 60 20 % 0.18/0.40 63. (Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) (All Y, ((big_p T_10) <=> (big_p Y))) (All W, (big_p W)) (-. (Ex U, (big_q U))) ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1))) ### Exists 62 % 0.18/0.40 64. ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1)))) (All Y, ((big_p T_10) <=> (big_p Y))) (All W, (big_p W)) (-. (Ex U, (big_q U))) ### Equiv 61 63 % 0.18/0.40 65. (big_p T_8) (-. (big_p T_8)) ### Axiom % 0.18/0.40 66. (-. (big_p T_10)) (big_p T_10) ### Axiom % 0.18/0.40 67. ((big_p T_10) <=> (big_p T_8)) (-. (big_p T_10)) (big_p T_8) ### Equiv 65 66 % 0.18/0.40 68. (All Y, ((big_p T_10) <=> (big_p Y))) (big_p T_8) (-. (big_p T_10)) ### All 67 % 0.18/0.40 69. (big_p T_10) (-. (big_p T_10)) ### Axiom % 0.18/0.40 70. (-. (big_p T_1)) (big_p T_1) ### Axiom % 0.18/0.40 71. ((big_p T_10) <=> (big_p T_1)) (-. (big_p T_1)) (big_p T_10) ### Equiv 69 70 % 0.18/0.40 72. (All Y, ((big_p T_10) <=> (big_p Y))) (big_p T_10) (-. (big_p T_1)) ### All 71 % 0.18/0.40 73. ((big_p T_10) <=> (big_p zenon_X11)) (-. (big_p T_1)) (big_p T_8) (All Y, ((big_p T_10) <=> (big_p Y))) ### Equiv 68 72 % 0.18/0.40 74. (All Y, ((big_p T_10) <=> (big_p Y))) (big_p T_8) (-. (big_p T_1)) ### All 73 % 0.18/0.40 75. (Ex U1, (big_p U1)) (-. (big_p T_1)) (All Y, ((big_p T_10) <=> (big_p Y))) ### Exists 74 % 0.18/0.40 76. (-. ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1)))) (All Y, ((big_p T_10) <=> (big_p Y))) (-. (big_p T_1)) (big_q T_6) (-. (Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1))))) ### NotEquiv 30 75 % 0.18/0.40 77. ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1))) (All Y, ((big_p T_10) <=> (big_p Y))) (-. (big_p T_1)) (All Y1, ((big_q T_4) <=> (big_q Y1))) (big_q T_6) ### Equiv 49 75 % 0.18/0.40 78. (Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) (big_q T_6) (-. (big_p T_1)) (All Y, ((big_p T_10) <=> (big_p Y))) ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1))) ### Exists 77 % 0.18/0.40 79. ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1)))) (big_q T_6) (-. (big_p T_1)) (All Y, ((big_p T_10) <=> (big_p Y))) ### Equiv 76 78 % 0.18/0.41 80. (-. (All W, (big_p W))) (All Y, ((big_p T_10) <=> (big_p Y))) (big_q T_6) ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1)))) ### NotAllEx 79 % 0.18/0.41 81. (Ex U, (big_q U)) ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1)))) (All Y, ((big_p T_10) <=> (big_p Y))) (-. (All W, (big_p W))) ### Exists 80 % 0.18/0.41 82. (-. ((Ex U, (big_q U)) <=> (All W, (big_p W)))) (All Y, ((big_p T_10) <=> (big_p Y))) ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1)))) ### NotEquiv 64 81 % 0.18/0.41 83. (Ex X, (All Y, ((big_p X) <=> (big_p Y)))) ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1)))) (-. ((Ex U, (big_q U)) <=> (All W, (big_p W)))) ### Exists 82 % 0.18/0.41 84. (-. ((Ex X, (All Y, ((big_p X) <=> (big_p Y)))) <=> ((Ex U, (big_q U)) <=> (All W, (big_p W))))) ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1)))) ### NotEquiv 54 83 % 0.18/0.41 85. ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1))) (-. (Ex X, (All Y, ((big_p X) <=> (big_p Y))))) (All W, (big_p W)) (-. (Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1))))) (-. (Ex U, (big_q U))) ### Equiv 13 37 % 0.18/0.41 86. (-. ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1)))) (-. (Ex X, (All Y, ((big_p X) <=> (big_p Y))))) (All W, (big_p W)) (-. (Ex U, (big_q U))) (All Y1, ((big_q T_4) <=> (big_q Y1))) ### NotEquiv 20 37 % 0.18/0.41 87. (Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) (-. (Ex U, (big_q U))) (All W, (big_p W)) (-. (Ex X, (All Y, ((big_p X) <=> (big_p Y))))) (-. ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1)))) ### Exists 86 % 0.18/0.41 88. (-. ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1))))) (-. (Ex U, (big_q U))) (All W, (big_p W)) (-. (Ex X, (All Y, ((big_p X) <=> (big_p Y))))) ### NotEquiv 85 87 % 0.18/0.41 89. ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1))) (big_q T_6) (-. (Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1))))) (-. (big_p T_1)) (-. (Ex X, (All Y, ((big_p X) <=> (big_p Y))))) ### Equiv 6 30 % 0.18/0.41 90. (-. ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1)))) (All Y1, ((big_q T_4) <=> (big_q Y1))) (big_q T_6) (-. (big_p T_1)) (-. (Ex X, (All Y, ((big_p X) <=> (big_p Y))))) ### NotEquiv 6 49 % 0.18/0.41 91. (Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) (-. (Ex X, (All Y, ((big_p X) <=> (big_p Y))))) (-. (big_p T_1)) (big_q T_6) (-. ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1)))) ### Exists 90 % 0.18/0.41 92. (-. ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1))))) (-. (Ex X, (All Y, ((big_p X) <=> (big_p Y))))) (-. (big_p T_1)) (big_q T_6) ### NotEquiv 89 91 % 0.18/0.41 93. (-. (All W, (big_p W))) (big_q T_6) (-. (Ex X, (All Y, ((big_p X) <=> (big_p Y))))) (-. ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1))))) ### NotAllEx 92 % 0.18/0.41 94. (Ex U, (big_q U)) (-. ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1))))) (-. (Ex X, (All Y, ((big_p X) <=> (big_p Y))))) (-. (All W, (big_p W))) ### Exists 93 % 0.18/0.41 95. (-. ((Ex U, (big_q U)) <=> (All W, (big_p W)))) (-. (Ex X, (All Y, ((big_p X) <=> (big_p Y))))) (-. ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1))))) ### NotEquiv 88 94 % 0.18/0.41 96. ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1))) (All Y, ((big_p T_10) <=> (big_p Y))) (-. (big_p T_1)) (-. (Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1))))) (-. (Ex U, (big_q U))) ### Equiv 13 75 % 0.18/0.41 97. (-. ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1)))) (All Y, ((big_p T_10) <=> (big_p Y))) (-. (big_p T_1)) (-. (Ex U, (big_q U))) (All Y1, ((big_q T_4) <=> (big_q Y1))) ### NotEquiv 20 75 % 0.18/0.41 98. (Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) (-. (Ex U, (big_q U))) (-. (big_p T_1)) (All Y, ((big_p T_10) <=> (big_p Y))) (-. ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1)))) ### Exists 97 % 0.18/0.41 99. (-. ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1))))) (-. (Ex U, (big_q U))) (-. (big_p T_1)) (All Y, ((big_p T_10) <=> (big_p Y))) ### NotEquiv 96 98 % 0.18/0.41 100. (-. (All W, (big_p W))) (All Y, ((big_p T_10) <=> (big_p Y))) (-. (Ex U, (big_q U))) (-. ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1))))) ### NotAllEx 99 % 0.18/0.41 101. ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1))) (big_q T_6) (-. (Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1))))) (All W, (big_p W)) (All Y, ((big_p T_10) <=> (big_p Y))) ### Equiv 60 30 % 0.18/0.41 102. (-. ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1)))) (All Y1, ((big_q T_4) <=> (big_q Y1))) (big_q T_6) (All W, (big_p W)) (All Y, ((big_p T_10) <=> (big_p Y))) ### NotEquiv 60 49 % 0.18/0.41 103. (Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) (All Y, ((big_p T_10) <=> (big_p Y))) (All W, (big_p W)) (big_q T_6) (-. ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1)))) ### Exists 102 % 0.18/0.41 104. (-. ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1))))) (All Y, ((big_p T_10) <=> (big_p Y))) (All W, (big_p W)) (big_q T_6) ### NotEquiv 101 103 % 0.18/0.41 105. (Ex U, (big_q U)) (All W, (big_p W)) (All Y, ((big_p T_10) <=> (big_p Y))) (-. ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1))))) ### Exists 104 % 0.18/0.41 106. ((Ex U, (big_q U)) <=> (All W, (big_p W))) (-. ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1))))) (All Y, ((big_p T_10) <=> (big_p Y))) ### Equiv 100 105 % 0.18/0.41 107. (Ex X, (All Y, ((big_p X) <=> (big_p Y)))) (-. ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1))))) ((Ex U, (big_q U)) <=> (All W, (big_p W))) ### Exists 106 % 0.18/0.41 108. ((Ex X, (All Y, ((big_p X) <=> (big_p Y)))) <=> ((Ex U, (big_q U)) <=> (All W, (big_p W)))) (-. ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1))))) ### Equiv 95 107 % 0.18/0.41 109. (-. (((Ex X, (All Y, ((big_p X) <=> (big_p Y)))) <=> ((Ex U, (big_q U)) <=> (All W, (big_p W)))) <=> ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_q W1)))))) ### NotEquiv 84 108 % 0.18/0.41 % SZS output end Proof % 0.18/0.41 (* END-PROOF *) %------------------------------------------------------------------------------