%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SYN036+1 : 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 : n020.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:22 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.03/0.12 % Problem : SYN036+1 : TPTP v8.1.0. Released v2.0.0. % 0.03/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n020.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 11:40:27 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_q T_0) (-. (big_q T_0)) ### Axiom % 0.18/0.40 2. (-. (Ex U, (big_q U))) (big_q T_0) ### NotExists 1 % 0.18/0.40 3. (-. (big_q T_1)) (big_q T_1) ### Axiom % 0.18/0.40 4. (-. ((big_q T_1) <=> (big_q T_0))) (-. (big_q T_1)) (-. (Ex U, (big_q U))) ### NotEquiv 2 3 % 0.18/0.40 5. (-. (All Y1, ((big_q T_1) <=> (big_q Y1)))) (-. (Ex U, (big_q U))) (-. (big_q T_1)) ### NotAllEx 4 % 0.18/0.40 6. (-. (Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1))))) (-. (big_q T_1)) (-. (Ex U, (big_q U))) ### NotExists 5 % 0.18/0.40 7. (big_p T_2) (-. (big_p T_2)) ### Axiom % 0.18/0.40 8. (-. (Ex U1, (big_p U1))) (big_p T_2) ### NotExists 7 % 0.18/0.40 9. (-. (big_p T_3)) (big_p T_3) ### Axiom % 0.18/0.40 10. (-. ((big_p T_3) <=> (big_p T_2))) (-. (big_p T_3)) (-. (Ex U1, (big_p U1))) ### NotEquiv 8 9 % 0.18/0.40 11. (-. (All Y, ((big_p T_3) <=> (big_p Y)))) (-. (Ex U1, (big_p U1))) (-. (big_p T_3)) ### NotAllEx 10 % 0.18/0.40 12. (-. (Ex X, (All Y, ((big_p X) <=> (big_p Y))))) (-. (big_p T_3)) (-. (Ex U1, (big_p U1))) ### NotExists 11 % 0.18/0.40 13. (-. (All W1, (big_p W1))) (-. (Ex U1, (big_p U1))) (-. (Ex X, (All Y, ((big_p X) <=> (big_p Y))))) ### NotAllEx 12 % 0.18/0.40 14. (big_p T_4) (-. (big_p T_4)) ### Axiom % 0.18/0.40 15. (-. (big_p T_5)) (big_p T_5) ### Axiom % 0.18/0.40 16. (All W1, (big_p W1)) (-. (big_p T_5)) ### All 15 % 0.18/0.40 17. (-. ((big_p T_4) <=> (big_p T_5))) (All W1, (big_p W1)) (big_p T_4) ### NotEquiv 14 16 % 0.18/0.40 18. (-. (All Y, ((big_p T_4) <=> (big_p Y)))) (big_p T_4) (All W1, (big_p W1)) ### NotAllEx 17 % 0.18/0.40 19. (-. (Ex X, (All Y, ((big_p X) <=> (big_p Y))))) (All W1, (big_p W1)) (big_p T_4) ### NotExists 18 % 0.18/0.40 20. (Ex U1, (big_p U1)) (All W1, (big_p W1)) (-. (Ex X, (All Y, ((big_p X) <=> (big_p Y))))) ### Exists 19 % 0.18/0.40 21. ((Ex U1, (big_p U1)) <=> (All W1, (big_p W1))) (-. (Ex X, (All Y, ((big_p X) <=> (big_p Y))))) ### Equiv 13 20 % 0.18/0.40 22. ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_p W1)))) (-. (Ex X, (All Y, ((big_p X) <=> (big_p Y))))) (-. (Ex U, (big_q U))) (-. (big_q T_1)) ### Equiv 6 21 % 0.18/0.40 23. (-. (All W, (big_q 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_p W1)))) ### NotAllEx 22 % 0.18/0.40 24. (big_q T_6) (-. (big_q T_6)) ### Axiom % 0.18/0.40 25. (-. (big_q T_7)) (big_q T_7) ### Axiom % 0.18/0.40 26. (All W, (big_q W)) (-. (big_q T_7)) ### All 25 % 0.18/0.40 27. (-. ((big_q T_6) <=> (big_q T_7))) (All W, (big_q W)) (big_q T_6) ### NotEquiv 24 26 % 0.18/0.40 28. (-. (All Y1, ((big_q T_6) <=> (big_q Y1)))) (big_q T_6) (All W, (big_q W)) ### NotAllEx 27 % 0.18/0.40 29. (-. (Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1))))) (All W, (big_q W)) (big_q T_6) ### NotExists 28 % 0.18/0.40 30. ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_p W1)))) (-. (Ex X, (All Y, ((big_p X) <=> (big_p Y))))) (big_q T_6) (All W, (big_q W)) ### Equiv 29 21 % 0.18/0.40 31. (Ex U, (big_q U)) (All W, (big_q 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_p W1)))) ### Exists 30 % 0.18/0.40 32. ((Ex U, (big_q U)) <=> (All W, (big_q W))) ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_p W1)))) (-. (Ex X, (All Y, ((big_p X) <=> (big_p Y))))) ### Equiv 23 31 % 0.18/0.40 33. (-. (big_p T_8)) (big_p T_8) ### Axiom % 0.18/0.40 34. (All W1, (big_p W1)) (-. (big_p T_8)) ### All 33 % 0.18/0.40 35. (big_p T_8) (-. (big_p T_8)) ### Axiom % 0.18/0.40 36. (-. (Ex U1, (big_p U1))) (big_p T_8) ### NotExists 35 % 0.18/0.40 37. ((big_p T_8) <=> (big_p zenon_X9)) (-. (Ex U1, (big_p U1))) (All W1, (big_p W1)) ### Equiv 34 36 % 0.18/0.40 38. (All Y, ((big_p T_8) <=> (big_p Y))) (All W1, (big_p W1)) (-. (Ex U1, (big_p U1))) ### All 37 % 0.18/0.40 39. (big_p T_4) (-. (big_p T_4)) ### Axiom % 0.18/0.40 40. (-. (big_p T_8)) (big_p T_8) ### Axiom % 0.18/0.40 41. ((big_p T_8) <=> (big_p T_4)) (-. (big_p T_8)) (big_p T_4) ### Equiv 39 40 % 0.18/0.40 42. (All Y, ((big_p T_8) <=> (big_p Y))) (big_p T_4) (-. (big_p T_8)) ### All 41 % 0.18/0.40 43. (big_p T_8) (-. (big_p T_8)) ### Axiom % 0.18/0.40 44. (-. (big_p T_3)) (big_p T_3) ### Axiom % 0.18/0.40 45. ((big_p T_8) <=> (big_p T_3)) (-. (big_p T_3)) (big_p T_8) ### Equiv 43 44 % 0.18/0.40 46. (All Y, ((big_p T_8) <=> (big_p Y))) (big_p T_8) (-. (big_p T_3)) ### All 45 % 0.18/0.40 47. ((big_p T_8) <=> (big_p zenon_X9)) (-. (big_p T_3)) (big_p T_4) (All Y, ((big_p T_8) <=> (big_p Y))) ### Equiv 42 46 % 0.18/0.40 48. (All Y, ((big_p T_8) <=> (big_p Y))) (big_p T_4) (-. (big_p T_3)) ### All 47 % 0.18/0.40 49. (-. (All W1, (big_p W1))) (big_p T_4) (All Y, ((big_p T_8) <=> (big_p Y))) ### NotAllEx 48 % 0.18/0.40 50. (Ex U1, (big_p U1)) (All Y, ((big_p T_8) <=> (big_p Y))) (-. (All W1, (big_p W1))) ### Exists 49 % 0.18/0.40 51. (-. ((Ex U1, (big_p U1)) <=> (All W1, (big_p W1)))) (All Y, ((big_p T_8) <=> (big_p Y))) ### NotEquiv 38 50 % 0.18/0.40 52. (-. (big_q T_10)) (big_q T_10) ### Axiom % 0.18/0.40 53. (All W, (big_q W)) (-. (big_q T_10)) ### All 52 % 0.18/0.40 54. (big_q T_10) (-. (big_q T_10)) ### Axiom % 0.18/0.40 55. (-. (Ex U, (big_q U))) (big_q T_10) ### NotExists 54 % 0.18/0.40 56. ((big_q T_10) <=> (big_q zenon_X11)) (-. (Ex U, (big_q U))) (All W, (big_q W)) ### Equiv 53 55 % 0.18/0.40 57. (All Y1, ((big_q T_10) <=> (big_q Y1))) (All W, (big_q W)) (-. (Ex U, (big_q U))) ### All 56 % 0.18/0.40 58. (Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) (-. (Ex U, (big_q U))) (All W, (big_q W)) ### Exists 57 % 0.18/0.40 59. ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_p W1)))) (All W, (big_q W)) (-. (Ex U, (big_q U))) (All Y, ((big_p T_8) <=> (big_p Y))) ### Equiv 51 58 % 0.18/0.40 60. (big_q T_6) (-. (big_q T_6)) ### Axiom % 0.18/0.40 61. (-. (big_q T_10)) (big_q T_10) ### Axiom % 0.18/0.40 62. ((big_q T_10) <=> (big_q T_6)) (-. (big_q T_10)) (big_q T_6) ### Equiv 60 61 % 0.18/0.40 63. (All Y1, ((big_q T_10) <=> (big_q Y1))) (big_q T_6) (-. (big_q T_10)) ### All 62 % 0.18/0.40 64. (big_q T_10) (-. (big_q T_10)) ### Axiom % 0.18/0.40 65. (-. (big_q T_1)) (big_q T_1) ### Axiom % 0.18/0.40 66. ((big_q T_10) <=> (big_q T_1)) (-. (big_q T_1)) (big_q T_10) ### Equiv 64 65 % 0.18/0.40 67. (All Y1, ((big_q T_10) <=> (big_q Y1))) (big_q T_10) (-. (big_q T_1)) ### All 66 % 0.18/0.40 68. ((big_q T_10) <=> (big_q zenon_X11)) (-. (big_q T_1)) (big_q T_6) (All Y1, ((big_q T_10) <=> (big_q Y1))) ### Equiv 63 67 % 0.18/0.40 69. (All Y1, ((big_q T_10) <=> (big_q Y1))) (big_q T_6) (-. (big_q T_1)) ### All 68 % 0.18/0.40 70. (Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) (-. (big_q T_1)) (big_q T_6) ### Exists 69 % 0.18/0.40 71. ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_p W1)))) (big_q T_6) (-. (big_q T_1)) (All Y, ((big_p T_8) <=> (big_p Y))) ### Equiv 51 70 % 0.18/0.40 72. (-. (All W, (big_q W))) (All Y, ((big_p T_8) <=> (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_p W1)))) ### NotAllEx 71 % 0.18/0.40 73. (Ex U, (big_q U)) ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_p W1)))) (All Y, ((big_p T_8) <=> (big_p Y))) (-. (All W, (big_q W))) ### Exists 72 % 0.18/0.40 74. (-. ((Ex U, (big_q U)) <=> (All W, (big_q W)))) (All Y, ((big_p T_8) <=> (big_p Y))) ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_p W1)))) ### NotEquiv 59 73 % 0.18/0.40 75. (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_p W1)))) (-. ((Ex U, (big_q U)) <=> (All W, (big_q W)))) ### Exists 74 % 0.18/0.40 76. (-. ((Ex X, (All Y, ((big_p X) <=> (big_p Y)))) <=> ((Ex U, (big_q U)) <=> (All W, (big_q W))))) ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_p W1)))) ### NotEquiv 32 75 % 0.18/0.40 77. (-. ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_p W1))))) (All W, (big_q W)) (-. (Ex U, (big_q U))) (-. (Ex X, (All Y, ((big_p X) <=> (big_p Y))))) ### NotEquiv 21 58 % 0.18/0.40 78. (-. ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_p W1))))) (big_q T_6) (-. (big_q T_1)) (-. (Ex X, (All Y, ((big_p X) <=> (big_p Y))))) ### NotEquiv 21 70 % 0.18/0.40 79. (-. (All W, (big_q W))) (-. (Ex X, (All Y, ((big_p X) <=> (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_p W1))))) ### NotAllEx 78 % 0.18/0.40 80. (Ex U, (big_q U)) (-. ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_p W1))))) (-. (Ex X, (All Y, ((big_p X) <=> (big_p Y))))) (-. (All W, (big_q W))) ### Exists 79 % 0.18/0.40 81. (-. ((Ex U, (big_q U)) <=> (All W, (big_q 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_p W1))))) ### NotEquiv 77 80 % 0.18/0.40 82. (-. ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_p W1))))) (All Y, ((big_p T_8) <=> (big_p Y))) (-. (Ex U, (big_q U))) (-. (big_q T_1)) ### NotEquiv 6 51 % 0.18/0.40 83. (-. (All W, (big_q W))) (-. (Ex U, (big_q U))) (All Y, ((big_p T_8) <=> (big_p Y))) (-. ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_p W1))))) ### NotAllEx 82 % 0.18/0.40 84. (-. ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_p W1))))) (All Y, ((big_p T_8) <=> (big_p Y))) (big_q T_6) (All W, (big_q W)) ### NotEquiv 29 51 % 0.18/0.40 85. (Ex U, (big_q U)) (All W, (big_q W)) (All Y, ((big_p T_8) <=> (big_p Y))) (-. ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_p W1))))) ### Exists 84 % 0.18/0.40 86. ((Ex U, (big_q U)) <=> (All W, (big_q W))) (-. ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_p W1))))) (All Y, ((big_p T_8) <=> (big_p Y))) ### Equiv 83 85 % 0.18/0.40 87. (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_p W1))))) ((Ex U, (big_q U)) <=> (All W, (big_q W))) ### Exists 86 % 0.18/0.40 88. ((Ex X, (All Y, ((big_p X) <=> (big_p Y)))) <=> ((Ex U, (big_q U)) <=> (All W, (big_q W)))) (-. ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_p W1))))) ### Equiv 81 87 % 0.18/0.40 89. (-. (((Ex X, (All Y, ((big_p X) <=> (big_p Y)))) <=> ((Ex U, (big_q U)) <=> (All W, (big_q W)))) <=> ((Ex X1, (All Y1, ((big_q X1) <=> (big_q Y1)))) <=> ((Ex U1, (big_p U1)) <=> (All W1, (big_p W1)))))) ### NotEquiv 76 88 % 0.18/0.40 % SZS output end Proof % 0.18/0.40 (* END-PROOF *) %------------------------------------------------------------------------------