%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : NUM404+1 : TPTP v8.1.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n013.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 : Mon Jul 18 14:42:11 EDT 2022 % Result : Theorem 10.41s 10.64s % Output : Proof 10.50s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NUM404+1 : TPTP v8.1.0. Released v3.2.0. % 0.03/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n013.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 : Wed Jul 6 08:16:14 EDT 2022 % 0.12/0.34 % CPUTime : % 10.41/10.64 % SZS status Theorem % 10.41/10.64 (* PROOF-FOUND *) % 10.41/10.64 (* BEGIN-PROOF *) % 10.41/10.64 % SZS output start Proof % 10.41/10.64 1. (in T_0 T_1) (-. (in T_0 T_1)) ### Axiom % 10.41/10.64 2. ((epsilon_transitive T_0) /\ (epsilon_connected T_0)) (-. ((epsilon_transitive T_0) /\ (epsilon_connected T_0))) ### Axiom % 10.41/10.64 3. (-. (ordinal T_0)) ((epsilon_transitive T_0) /\ (epsilon_connected T_0)) ### Definition-Pseudo(ordinal) 2 % 10.41/10.64 4. (in T_2 T_0) (-. (in T_2 T_0)) ### Axiom % 10.41/10.64 5. (-. (All B, ((in B T_2) => (subset B T_2)))) (All B, ((in B T_2) => (subset B T_2))) ### Axiom % 10.41/10.64 6. (epsilon_transitive T_2) (-. (All B, ((in B T_2) => (subset B T_2)))) ### Definition-Pseudo(epsilon_transitive) 5 % 10.41/10.64 7. ((epsilon_transitive T_2) /\ (epsilon_connected T_2)) (-. (All B, ((in B T_2) => (subset B T_2)))) ### And 6 % 10.41/10.64 8. (ordinal T_2) (-. (All B, ((in B T_2) => (subset B T_2)))) ### Definition-Pseudo(ordinal) 7 % 10.41/10.64 9. ((ordinal T_0) => ((in T_2 T_0) => (ordinal T_2))) (-. (All B, ((in B T_2) => (subset B T_2)))) (in T_2 T_0) ((epsilon_transitive T_0) /\ (epsilon_connected T_0)) ### DisjTree 3 4 8 % 10.41/10.64 10. (All B, ((ordinal B) => ((in T_2 B) => (ordinal T_2)))) ((epsilon_transitive T_0) /\ (epsilon_connected T_0)) (in T_2 T_0) (-. (All B, ((in B T_2) => (subset B T_2)))) ### All 9 % 10.41/10.64 11. (All A, (All B, ((ordinal B) => ((in A B) => (ordinal A))))) (-. (All B, ((in B T_2) => (subset B T_2)))) (in T_2 T_0) ((epsilon_transitive T_0) /\ (epsilon_connected T_0)) ### All 10 % 10.41/10.64 12. (-. (epsilon_transitive T_2)) ((epsilon_transitive T_0) /\ (epsilon_connected T_0)) (in T_2 T_0) (All A, (All B, ((ordinal B) => ((in A B) => (ordinal A))))) ### Definition-Pseudo(epsilon_transitive) 11 % 10.41/10.64 13. (in T_2 T_0) (-. (in T_2 T_0)) ### Axiom % 10.41/10.64 14. (-. (All B, (All C, (-. ((in B T_2) /\ ((in C T_2) /\ ((-. (in B C)) /\ ((B != C) /\ (-. (in C B)))))))))) (All B, (All C, (-. ((in B T_2) /\ ((in C T_2) /\ ((-. (in B C)) /\ ((B != C) /\ (-. (in C B))))))))) ### Axiom % 10.41/10.64 15. (epsilon_connected T_2) (-. (All B, (All C, (-. ((in B T_2) /\ ((in C T_2) /\ ((-. (in B C)) /\ ((B != C) /\ (-. (in C B)))))))))) ### Definition-Pseudo(epsilon_connected) 14 % 10.41/10.64 16. ((epsilon_transitive T_2) /\ (epsilon_connected T_2)) (-. (All B, (All C, (-. ((in B T_2) /\ ((in C T_2) /\ ((-. (in B C)) /\ ((B != C) /\ (-. (in C B)))))))))) ### And 15 % 10.41/10.64 17. (ordinal T_2) (-. (All B, (All C, (-. ((in B T_2) /\ ((in C T_2) /\ ((-. (in B C)) /\ ((B != C) /\ (-. (in C B)))))))))) ### Definition-Pseudo(ordinal) 16 % 10.41/10.64 18. ((ordinal T_0) => ((in T_2 T_0) => (ordinal T_2))) (-. (All B, (All C, (-. ((in B T_2) /\ ((in C T_2) /\ ((-. (in B C)) /\ ((B != C) /\ (-. (in C B)))))))))) (in T_2 T_0) ((epsilon_transitive T_0) /\ (epsilon_connected T_0)) ### DisjTree 3 13 17 % 10.41/10.64 19. (All B, ((ordinal B) => ((in T_2 B) => (ordinal T_2)))) ((epsilon_transitive T_0) /\ (epsilon_connected T_0)) (in T_2 T_0) (-. (All B, (All C, (-. ((in B T_2) /\ ((in C T_2) /\ ((-. (in B C)) /\ ((B != C) /\ (-. (in C B)))))))))) ### All 18 % 10.41/10.64 20. (All A, (All B, ((ordinal B) => ((in A B) => (ordinal A))))) (-. (All B, (All C, (-. ((in B T_2) /\ ((in C T_2) /\ ((-. (in B C)) /\ ((B != C) /\ (-. (in C B)))))))))) (in T_2 T_0) ((epsilon_transitive T_0) /\ (epsilon_connected T_0)) ### All 19 % 10.41/10.64 21. (-. (epsilon_connected T_2)) ((epsilon_transitive T_0) /\ (epsilon_connected T_0)) (in T_2 T_0) (All A, (All B, ((ordinal B) => ((in A B) => (ordinal A))))) ### Definition-Pseudo(epsilon_connected) 20 % 10.41/10.64 22. (-. ((epsilon_transitive T_2) /\ (epsilon_connected T_2))) (All A, (All B, ((ordinal B) => ((in A B) => (ordinal A))))) (in T_2 T_0) ((epsilon_transitive T_0) /\ (epsilon_connected T_0)) ### NotAnd 12 21 % 10.41/10.64 23. (-. (ordinal T_2)) ((epsilon_transitive T_0) /\ (epsilon_connected T_0)) (in T_2 T_0) (All A, (All B, ((ordinal B) => ((in A B) => (ordinal A))))) ### Definition-Pseudo(ordinal) 22 % 10.41/10.64 24. (-. (in T_2 T_1)) (in T_2 T_1) ### Axiom % 10.41/10.64 25. ((in T_2 T_1) <=> (ordinal T_2)) (-. (in T_2 T_1)) (All A, (All B, ((ordinal B) => ((in A B) => (ordinal A))))) (in T_2 T_0) ((epsilon_transitive T_0) /\ (epsilon_connected T_0)) ### Equiv 23 24 % 10.41/10.64 26. (All B, ((in B T_1) <=> (ordinal B))) ((epsilon_transitive T_0) /\ (epsilon_connected T_0)) (in T_2 T_0) (All A, (All B, ((ordinal B) => ((in A B) => (ordinal A))))) (-. (in T_2 T_1)) ### All 25 % 10.41/10.64 27. (ordinal T_0) (-. (in T_2 T_1)) (All A, (All B, ((ordinal B) => ((in A B) => (ordinal A))))) (in T_2 T_0) (All B, ((in B T_1) <=> (ordinal B))) ### Definition-Pseudo(ordinal) 26 % 10.41/10.64 28. ((in T_0 T_1) <=> (ordinal T_0)) (All B, ((in B T_1) <=> (ordinal B))) (in T_2 T_0) (All A, (All B, ((ordinal B) => ((in A B) => (ordinal A))))) (-. (in T_2 T_1)) (in T_0 T_1) ### Equiv 1 27 % 10.41/10.64 29. (in T_0 T_1) (-. (in T_2 T_1)) (All A, (All B, ((ordinal B) => ((in A B) => (ordinal A))))) (in T_2 T_0) (All B, ((in B T_1) <=> (ordinal B))) ### All 28 % 10.41/10.64 30. (-. ((in T_2 T_0) => (in T_2 T_1))) (All B, ((in B T_1) <=> (ordinal B))) (All A, (All B, ((ordinal B) => ((in A B) => (ordinal A))))) (in T_0 T_1) ### NotImply 29 % 10.41/10.64 31. (-. (All C, ((in C T_0) => (in C T_1)))) (in T_0 T_1) (All A, (All B, ((ordinal B) => ((in A B) => (ordinal A))))) (All B, ((in B T_1) <=> (ordinal B))) ### NotAllEx 30 % 10.41/10.64 32. (-. (subset T_0 T_1)) (All B, ((in B T_1) <=> (ordinal B))) (All A, (All B, ((ordinal B) => ((in A B) => (ordinal A))))) (in T_0 T_1) ### Definition-Pseudo(subset) 31 % 10.41/10.64 33. (-. ((in T_0 T_1) => (subset T_0 T_1))) (All A, (All B, ((ordinal B) => ((in A B) => (ordinal A))))) (All B, ((in B T_1) <=> (ordinal B))) ### NotImply 32 % 10.41/10.64 34. (-. (All B, ((in B T_1) => (subset B T_1)))) (All B, ((in B T_1) <=> (ordinal B))) (All A, (All B, ((ordinal B) => ((in A B) => (ordinal A))))) ### NotAllEx 33 % 10.41/10.64 35. (-. (epsilon_transitive T_1)) (All A, (All B, ((ordinal B) => ((in A B) => (ordinal A))))) (All B, ((in B T_1) <=> (ordinal B))) ### Definition-Pseudo(epsilon_transitive) 34 % 10.41/10.64 36. (in T_3 T_1) (-. (in T_3 T_1)) ### Axiom % 10.41/10.64 37. ((epsilon_transitive T_3) /\ (epsilon_connected T_3)) (-. ((epsilon_transitive T_3) /\ (epsilon_connected T_3))) ### Axiom % 10.41/10.64 38. (-. (ordinal T_3)) ((epsilon_transitive T_3) /\ (epsilon_connected T_3)) ### Definition-Pseudo(ordinal) 37 % 10.41/10.64 39. (ordinal T_3) (-. (ordinal T_3)) ### Definition-Pseudo(ordinal) 38 % 10.41/10.64 40. ((in T_3 T_1) <=> (ordinal T_3)) (-. (ordinal T_3)) (in T_3 T_1) ### Equiv 36 39 % 10.41/10.64 41. (All B, ((in B T_1) <=> (ordinal B))) (in T_3 T_1) (-. (ordinal T_3)) ### All 40 % 10.41/10.64 42. (in T_4 T_1) (-. (in T_4 T_1)) ### Axiom % 10.41/10.64 43. (-. (All B, ((in B T_4) => (subset B T_4)))) (All B, ((in B T_4) => (subset B T_4))) ### Axiom % 10.41/10.64 44. (epsilon_transitive T_4) (-. (All B, ((in B T_4) => (subset B T_4)))) ### Definition-Pseudo(epsilon_transitive) 43 % 10.41/10.64 45. ((epsilon_transitive T_4) /\ (epsilon_connected T_4)) (-. (All B, ((in B T_4) => (subset B T_4)))) ### And 44 % 10.41/10.64 46. (ordinal T_4) (-. (All B, ((in B T_4) => (subset B T_4)))) ### Definition-Pseudo(ordinal) 45 % 10.41/10.64 47. ((in T_4 T_1) <=> (ordinal T_4)) (-. (All B, ((in B T_4) => (subset B T_4)))) (in T_4 T_1) ### Equiv 42 46 % 10.41/10.64 48. (All B, ((in B T_1) <=> (ordinal B))) (in T_4 T_1) (-. (All B, ((in B T_4) => (subset B T_4)))) ### All 47 % 10.41/10.64 49. (-. (epsilon_transitive T_4)) (in T_4 T_1) (All B, ((in B T_1) <=> (ordinal B))) ### Definition-Pseudo(epsilon_transitive) 48 % 10.41/10.64 50. (in T_4 T_1) (-. (in T_4 T_1)) ### Axiom % 10.41/10.64 51. (-. (All B, (All C, (-. ((in B T_4) /\ ((in C T_4) /\ ((-. (in B C)) /\ ((B != C) /\ (-. (in C B)))))))))) (All B, (All C, (-. ((in B T_4) /\ ((in C T_4) /\ ((-. (in B C)) /\ ((B != C) /\ (-. (in C B))))))))) ### Axiom % 10.41/10.64 52. (epsilon_connected T_4) (-. (All B, (All C, (-. ((in B T_4) /\ ((in C T_4) /\ ((-. (in B C)) /\ ((B != C) /\ (-. (in C B)))))))))) ### Definition-Pseudo(epsilon_connected) 51 % 10.41/10.64 53. ((epsilon_transitive T_4) /\ (epsilon_connected T_4)) (-. (All B, (All C, (-. ((in B T_4) /\ ((in C T_4) /\ ((-. (in B C)) /\ ((B != C) /\ (-. (in C B)))))))))) ### And 52 % 10.41/10.64 54. (ordinal T_4) (-. (All B, (All C, (-. ((in B T_4) /\ ((in C T_4) /\ ((-. (in B C)) /\ ((B != C) /\ (-. (in C B)))))))))) ### Definition-Pseudo(ordinal) 53 % 10.41/10.64 55. ((in T_4 T_1) <=> (ordinal T_4)) (-. (All B, (All C, (-. ((in B T_4) /\ ((in C T_4) /\ ((-. (in B C)) /\ ((B != C) /\ (-. (in C B)))))))))) (in T_4 T_1) ### Equiv 50 54 % 10.41/10.64 56. (All B, ((in B T_1) <=> (ordinal B))) (in T_4 T_1) (-. (All B, (All C, (-. ((in B T_4) /\ ((in C T_4) /\ ((-. (in B C)) /\ ((B != C) /\ (-. (in C B)))))))))) ### All 55 % 10.50/10.67 57. (-. (epsilon_connected T_4)) (in T_4 T_1) (All B, ((in B T_1) <=> (ordinal B))) ### Definition-Pseudo(epsilon_connected) 56 % 10.50/10.67 58. (-. ((epsilon_transitive T_4) /\ (epsilon_connected T_4))) (All B, ((in B T_1) <=> (ordinal B))) (in T_4 T_1) ### NotAnd 49 57 % 10.50/10.67 59. (-. (ordinal T_4)) (in T_4 T_1) (All B, ((in B T_1) <=> (ordinal B))) ### Definition-Pseudo(ordinal) 58 % 10.50/10.67 60. (-. (in T_3 T_4)) (in T_3 T_4) ### Axiom % 10.50/10.67 61. (T_3 != T_4) (T_3 = T_4) ### Axiom % 10.50/10.67 62. (-. (in T_4 T_3)) (in T_4 T_3) ### Axiom % 10.50/10.67 63. ((ordinal T_4) => (-. ((-. (in T_3 T_4)) /\ ((T_3 != T_4) /\ (-. (in T_4 T_3)))))) (-. (in T_4 T_3)) (T_3 != T_4) (-. (in T_3 T_4)) (All B, ((in B T_1) <=> (ordinal B))) (in T_4 T_1) ### DisjTree 59 60 61 62 % 10.50/10.67 64. (All B, ((ordinal B) => (-. ((-. (in T_3 B)) /\ ((T_3 != B) /\ (-. (in B T_3))))))) (in T_4 T_1) (All B, ((in B T_1) <=> (ordinal B))) (-. (in T_3 T_4)) (T_3 != T_4) (-. (in T_4 T_3)) ### All 63 % 10.50/10.67 65. ((ordinal T_3) => (All B, ((ordinal B) => (-. ((-. (in T_3 B)) /\ ((T_3 != B) /\ (-. (in B T_3)))))))) (-. (in T_4 T_3)) (T_3 != T_4) (-. (in T_3 T_4)) (in T_4 T_1) (in T_3 T_1) (All B, ((in B T_1) <=> (ordinal B))) ### Imply 41 64 % 10.50/10.67 66. (All A, ((ordinal A) => (All B, ((ordinal B) => (-. ((-. (in A B)) /\ ((A != B) /\ (-. (in B A))))))))) (All B, ((in B T_1) <=> (ordinal B))) (in T_3 T_1) (in T_4 T_1) (-. (in T_3 T_4)) (T_3 != T_4) (-. (in T_4 T_3)) ### All 65 % 10.50/10.67 67. ((in T_3 T_1) /\ ((in T_4 T_1) /\ ((-. (in T_3 T_4)) /\ ((T_3 != T_4) /\ (-. (in T_4 T_3)))))) (All B, ((in B T_1) <=> (ordinal B))) (All A, ((ordinal A) => (All B, ((ordinal B) => (-. ((-. (in A B)) /\ ((A != B) /\ (-. (in B A))))))))) ### ConjTree 66 % 10.50/10.67 68. (-. (-. ((in T_3 T_1) /\ ((in T_4 T_1) /\ ((-. (in T_3 T_4)) /\ ((T_3 != T_4) /\ (-. (in T_4 T_3)))))))) (All A, ((ordinal A) => (All B, ((ordinal B) => (-. ((-. (in A B)) /\ ((A != B) /\ (-. (in B A))))))))) (All B, ((in B T_1) <=> (ordinal B))) ### NotNot 67 % 10.50/10.67 69. (-. (All C, (-. ((in T_3 T_1) /\ ((in C T_1) /\ ((-. (in T_3 C)) /\ ((T_3 != C) /\ (-. (in C T_3))))))))) (All B, ((in B T_1) <=> (ordinal B))) (All A, ((ordinal A) => (All B, ((ordinal B) => (-. ((-. (in A B)) /\ ((A != B) /\ (-. (in B A))))))))) ### NotAllEx 68 % 10.50/10.67 70. (-. (All B, (All C, (-. ((in B T_1) /\ ((in C T_1) /\ ((-. (in B C)) /\ ((B != C) /\ (-. (in C B)))))))))) (All A, ((ordinal A) => (All B, ((ordinal B) => (-. ((-. (in A B)) /\ ((A != B) /\ (-. (in B A))))))))) (All B, ((in B T_1) <=> (ordinal B))) ### NotAllEx 69 % 10.50/10.67 71. (-. (epsilon_connected T_1)) (All B, ((in B T_1) <=> (ordinal B))) (All A, ((ordinal A) => (All B, ((ordinal B) => (-. ((-. (in A B)) /\ ((A != B) /\ (-. (in B A))))))))) ### Definition-Pseudo(epsilon_connected) 70 % 10.50/10.67 72. (-. ((epsilon_transitive T_1) /\ (epsilon_connected T_1))) (All A, ((ordinal A) => (All B, ((ordinal B) => (-. ((-. (in A B)) /\ ((A != B) /\ (-. (in B A))))))))) (All B, ((in B T_1) <=> (ordinal B))) (All A, (All B, ((ordinal B) => ((in A B) => (ordinal A))))) ### NotAnd 35 71 % 10.50/10.67 73. (-. (ordinal T_1)) (All A, (All B, ((ordinal B) => ((in A B) => (ordinal A))))) (All B, ((in B T_1) <=> (ordinal B))) (All A, ((ordinal A) => (All B, ((ordinal B) => (-. ((-. (in A B)) /\ ((A != B) /\ (-. (in B A))))))))) ### Definition-Pseudo(ordinal) 72 % 10.50/10.67 74. ((epsilon_transitive T_1) /\ (epsilon_connected T_1)) (-. ((epsilon_transitive T_1) /\ (epsilon_connected T_1))) ### Axiom % 10.50/10.67 75. (-. (ordinal T_1)) ((epsilon_transitive T_1) /\ (epsilon_connected T_1)) ### Definition-Pseudo(ordinal) 74 % 10.50/10.67 76. (in T_1 T_1) (-. (in T_1 T_1)) ### Axiom % 10.50/10.67 77. (in T_1 T_1) (-. (in T_1 T_1)) ### Axiom % 10.50/10.67 78. ((in T_1 T_1) => (-. (in T_1 T_1))) (in T_1 T_1) ### Imply 76 77 % 10.50/10.67 79. (All B, ((in T_1 B) => (-. (in B T_1)))) (in T_1 T_1) ### All 78 % 10.50/10.67 80. ((in T_1 T_1) <=> (ordinal T_1)) (All B, ((in T_1 B) => (-. (in B T_1)))) ((epsilon_transitive T_1) /\ (epsilon_connected T_1)) ### Equiv 75 79 % 10.50/10.67 81. (All B, ((in B T_1) <=> (ordinal B))) ((epsilon_transitive T_1) /\ (epsilon_connected T_1)) (All B, ((in T_1 B) => (-. (in B T_1)))) ### All 80 % 10.50/10.67 82. ((ordinal T_1) => ((epsilon_transitive T_1) /\ (epsilon_connected T_1))) (All B, ((in T_1 B) => (-. (in B T_1)))) (All A, ((ordinal A) => (All B, ((ordinal B) => (-. ((-. (in A B)) /\ ((A != B) /\ (-. (in B A))))))))) (All B, ((in B T_1) <=> (ordinal B))) (All A, (All B, ((ordinal B) => ((in A B) => (ordinal A))))) ### Imply 73 81 % 10.50/10.67 83. (All A, ((ordinal A) => ((epsilon_transitive A) /\ (epsilon_connected A)))) (All A, (All B, ((ordinal B) => ((in A B) => (ordinal A))))) (All B, ((in B T_1) <=> (ordinal B))) (All A, ((ordinal A) => (All B, ((ordinal B) => (-. ((-. (in A B)) /\ ((A != B) /\ (-. (in B A))))))))) (All B, ((in T_1 B) => (-. (in B T_1)))) ### All 82 % 10.50/10.67 84. (All A, (All B, ((in A B) => (-. (in B A))))) (All A, ((ordinal A) => (All B, ((ordinal B) => (-. ((-. (in A B)) /\ ((A != B) /\ (-. (in B A))))))))) (All B, ((in B T_1) <=> (ordinal B))) (All A, (All B, ((ordinal B) => ((in A B) => (ordinal A))))) (All A, ((ordinal A) => ((epsilon_transitive A) /\ (epsilon_connected A)))) ### All 83 % 10.50/10.67 85. (-. (-. (All B, ((in B T_1) <=> (ordinal B))))) (All A, ((ordinal A) => ((epsilon_transitive A) /\ (epsilon_connected A)))) (All A, (All B, ((ordinal B) => ((in A B) => (ordinal A))))) (All A, ((ordinal A) => (All B, ((ordinal B) => (-. ((-. (in A B)) /\ ((A != B) /\ (-. (in B A))))))))) (All A, (All B, ((in A B) => (-. (in B A))))) ### NotNot 84 % 10.50/10.67 86. (-. (All A, (-. (All B, ((in B A) <=> (ordinal B)))))) (All A, (All B, ((in A B) => (-. (in B A))))) (All A, ((ordinal A) => (All B, ((ordinal B) => (-. ((-. (in A B)) /\ ((A != B) /\ (-. (in B A))))))))) (All A, (All B, ((ordinal B) => ((in A B) => (ordinal A))))) (All A, ((ordinal A) => ((epsilon_transitive A) /\ (epsilon_connected A)))) ### NotAllEx 85 % 10.50/10.67 % SZS output end Proof % 10.50/10.67 (* END-PROOF *) %------------------------------------------------------------------------------