%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SEU234+1 : TPTP v8.1.0. Released v3.3.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 : Tue Jul 19 14:49:30 EDT 2022 % Result : Theorem 16.66s 16.90s % Output : Proof 16.66s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.14 % Problem : SEU234+1 : TPTP v8.1.0. Released v3.3.0. % 0.08/0.15 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.14/0.36 % Computer : n013.cluster.edu % 0.14/0.36 % Model : x86_64 x86_64 % 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.36 % Memory : 8042.1875MB % 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.37 % CPULimit : 300 % 0.14/0.37 % WCLimit : 600 % 0.14/0.37 % DateTime : Sun Jun 19 19:16:29 EDT 2022 % 0.14/0.37 % CPUTime : % 16.66/16.90 % SZS status Theorem % 16.66/16.90 (* PROOF-FOUND *) % 16.66/16.90 (* BEGIN-PROOF *) % 16.66/16.90 % SZS output start Proof % 16.66/16.90 1. (in T_0 T_1) (-. (in T_0 T_1)) ### Axiom % 16.66/16.90 2. (-. (subset T_0 T_1)) (subset T_0 T_1) ### Axiom % 16.66/16.90 3. ((ordinal T_0) /\ (subset T_0 T_1)) (-. (subset T_0 T_1)) ### And 2 % 16.66/16.90 4. ((in T_0 T_1) => ((ordinal T_0) /\ (subset T_0 T_1))) (-. (subset T_0 T_1)) (in T_0 T_1) ### Imply 1 3 % 16.66/16.90 5. (All B, ((in B T_1) => ((ordinal B) /\ (subset B T_1)))) (in T_0 T_1) (-. (subset T_0 T_1)) ### All 4 % 16.66/16.90 6. (-. ((in T_0 T_1) => (subset T_0 T_1))) (All B, ((in B T_1) => ((ordinal B) /\ (subset B T_1)))) ### NotImply 5 % 16.66/16.90 7. (-. (All B, ((in B T_1) => (subset B T_1)))) (All B, ((in B T_1) => ((ordinal B) /\ (subset B T_1)))) ### NotAllEx 6 % 16.66/16.90 8. (-. (epsilon_transitive T_1)) (All B, ((in B T_1) => ((ordinal B) /\ (subset B T_1)))) ### Definition-Pseudo(epsilon_transitive) 7 % 16.66/16.90 9. (in T_2 T_1) (-. (in T_2 T_1)) ### Axiom % 16.66/16.90 10. (-. (All B, ((in B T_2) => (subset B T_2)))) (All B, ((in B T_2) => (subset B T_2))) ### Axiom % 16.66/16.90 11. (epsilon_transitive T_2) (-. (All B, ((in B T_2) => (subset B T_2)))) ### Definition-Pseudo(epsilon_transitive) 10 % 16.66/16.90 12. ((epsilon_transitive T_2) /\ (epsilon_connected T_2)) (-. (All B, ((in B T_2) => (subset B T_2)))) ### And 11 % 16.66/16.90 13. (ordinal T_2) (-. (All B, ((in B T_2) => (subset B T_2)))) ### Definition-Pseudo(ordinal) 12 % 16.66/16.90 14. ((ordinal T_2) /\ (subset T_2 T_1)) (-. (All B, ((in B T_2) => (subset B T_2)))) ### And 13 % 16.66/16.90 15. ((in T_2 T_1) => ((ordinal T_2) /\ (subset T_2 T_1))) (-. (All B, ((in B T_2) => (subset B T_2)))) (in T_2 T_1) ### Imply 9 14 % 16.66/16.90 16. (All B, ((in B T_1) => ((ordinal B) /\ (subset B T_1)))) (in T_2 T_1) (-. (All B, ((in B T_2) => (subset B T_2)))) ### All 15 % 16.66/16.90 17. (-. (epsilon_transitive T_2)) (in T_2 T_1) (All B, ((in B T_1) => ((ordinal B) /\ (subset B T_1)))) ### Definition-Pseudo(epsilon_transitive) 16 % 16.66/16.90 18. (in T_2 T_1) (-. (in T_2 T_1)) ### Axiom % 16.66/16.90 19. (-. (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 % 16.66/16.90 20. (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) 19 % 16.66/16.90 21. ((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 20 % 16.66/16.90 22. (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) 21 % 16.66/16.90 23. ((ordinal T_2) /\ (subset T_2 T_1)) (-. (All B, (All C, (-. ((in B T_2) /\ ((in C T_2) /\ ((-. (in B C)) /\ ((B != C) /\ (-. (in C B)))))))))) ### And 22 % 16.66/16.90 24. ((in T_2 T_1) => ((ordinal T_2) /\ (subset T_2 T_1))) (-. (All B, (All C, (-. ((in B T_2) /\ ((in C T_2) /\ ((-. (in B C)) /\ ((B != C) /\ (-. (in C B)))))))))) (in T_2 T_1) ### Imply 18 23 % 16.66/16.90 25. (All B, ((in B T_1) => ((ordinal B) /\ (subset B T_1)))) (in T_2 T_1) (-. (All B, (All C, (-. ((in B T_2) /\ ((in C T_2) /\ ((-. (in B C)) /\ ((B != C) /\ (-. (in C B)))))))))) ### All 24 % 16.66/16.90 26. (-. (epsilon_connected T_2)) (in T_2 T_1) (All B, ((in B T_1) => ((ordinal B) /\ (subset B T_1)))) ### Definition-Pseudo(epsilon_connected) 25 % 16.66/16.90 27. (-. ((epsilon_transitive T_2) /\ (epsilon_connected T_2))) (All B, ((in B T_1) => ((ordinal B) /\ (subset B T_1)))) (in T_2 T_1) ### NotAnd 17 26 % 16.66/16.90 28. (-. (ordinal T_2)) (in T_2 T_1) (All B, ((in B T_1) => ((ordinal B) /\ (subset B T_1)))) ### Definition-Pseudo(ordinal) 27 % 16.66/16.90 29. (in T_3 T_1) (-. (in T_3 T_1)) ### Axiom % 16.66/16.90 30. (-. (All B, ((in B T_3) => (subset B T_3)))) (All B, ((in B T_3) => (subset B T_3))) ### Axiom % 16.66/16.90 31. (epsilon_transitive T_3) (-. (All B, ((in B T_3) => (subset B T_3)))) ### Definition-Pseudo(epsilon_transitive) 30 % 16.66/16.90 32. ((epsilon_transitive T_3) /\ (epsilon_connected T_3)) (-. (All B, ((in B T_3) => (subset B T_3)))) ### And 31 % 16.66/16.90 33. (ordinal T_3) (-. (All B, ((in B T_3) => (subset B T_3)))) ### Definition-Pseudo(ordinal) 32 % 16.66/16.90 34. ((ordinal T_3) /\ (subset T_3 T_1)) (-. (All B, ((in B T_3) => (subset B T_3)))) ### And 33 % 16.66/16.90 35. ((in T_3 T_1) => ((ordinal T_3) /\ (subset T_3 T_1))) (-. (All B, ((in B T_3) => (subset B T_3)))) (in T_3 T_1) ### Imply 29 34 % 16.66/16.90 36. (All B, ((in B T_1) => ((ordinal B) /\ (subset B T_1)))) (in T_3 T_1) (-. (All B, ((in B T_3) => (subset B T_3)))) ### All 35 % 16.66/16.90 37. (-. (epsilon_transitive T_3)) (in T_3 T_1) (All B, ((in B T_1) => ((ordinal B) /\ (subset B T_1)))) ### Definition-Pseudo(epsilon_transitive) 36 % 16.66/16.90 38. (in T_3 T_1) (-. (in T_3 T_1)) ### Axiom % 16.66/16.90 39. (-. (All B, (All C, (-. ((in B T_3) /\ ((in C T_3) /\ ((-. (in B C)) /\ ((B != C) /\ (-. (in C B)))))))))) (All B, (All C, (-. ((in B T_3) /\ ((in C T_3) /\ ((-. (in B C)) /\ ((B != C) /\ (-. (in C B))))))))) ### Axiom % 16.66/16.90 40. (epsilon_connected T_3) (-. (All B, (All C, (-. ((in B T_3) /\ ((in C T_3) /\ ((-. (in B C)) /\ ((B != C) /\ (-. (in C B)))))))))) ### Definition-Pseudo(epsilon_connected) 39 % 16.66/16.90 41. ((epsilon_transitive T_3) /\ (epsilon_connected T_3)) (-. (All B, (All C, (-. ((in B T_3) /\ ((in C T_3) /\ ((-. (in B C)) /\ ((B != C) /\ (-. (in C B)))))))))) ### And 40 % 16.66/16.90 42. (ordinal T_3) (-. (All B, (All C, (-. ((in B T_3) /\ ((in C T_3) /\ ((-. (in B C)) /\ ((B != C) /\ (-. (in C B)))))))))) ### Definition-Pseudo(ordinal) 41 % 16.66/16.90 43. ((ordinal T_3) /\ (subset T_3 T_1)) (-. (All B, (All C, (-. ((in B T_3) /\ ((in C T_3) /\ ((-. (in B C)) /\ ((B != C) /\ (-. (in C B)))))))))) ### And 42 % 16.66/16.90 44. ((in T_3 T_1) => ((ordinal T_3) /\ (subset T_3 T_1))) (-. (All B, (All C, (-. ((in B T_3) /\ ((in C T_3) /\ ((-. (in B C)) /\ ((B != C) /\ (-. (in C B)))))))))) (in T_3 T_1) ### Imply 38 43 % 16.66/16.90 45. (All B, ((in B T_1) => ((ordinal B) /\ (subset B T_1)))) (in T_3 T_1) (-. (All B, (All C, (-. ((in B T_3) /\ ((in C T_3) /\ ((-. (in B C)) /\ ((B != C) /\ (-. (in C B)))))))))) ### All 44 % 16.66/16.90 46. (-. (epsilon_connected T_3)) (in T_3 T_1) (All B, ((in B T_1) => ((ordinal B) /\ (subset B T_1)))) ### Definition-Pseudo(epsilon_connected) 45 % 16.66/16.90 47. (-. ((epsilon_transitive T_3) /\ (epsilon_connected T_3))) (All B, ((in B T_1) => ((ordinal B) /\ (subset B T_1)))) (in T_3 T_1) ### NotAnd 37 46 % 16.66/16.90 48. (-. (ordinal T_3)) (in T_3 T_1) (All B, ((in B T_1) => ((ordinal B) /\ (subset B T_1)))) ### Definition-Pseudo(ordinal) 47 % 16.66/16.90 49. (-. (in T_2 T_3)) (in T_2 T_3) ### Axiom % 16.66/16.90 50. (T_3 != T_2) (T_2 = T_3) ### Sym(=) % 16.66/16.90 51. (-. (in T_3 T_2)) (in T_3 T_2) ### Axiom % 16.66/16.90 52. ((ordinal T_3) => (-. ((-. (in T_2 T_3)) /\ ((T_2 != T_3) /\ (-. (in T_3 T_2)))))) (-. (in T_3 T_2)) (T_3 != T_2) (-. (in T_2 T_3)) (All B, ((in B T_1) => ((ordinal B) /\ (subset B T_1)))) (in T_3 T_1) ### DisjTree 48 49 50 51 % 16.66/16.90 53. (All B, ((ordinal B) => (-. ((-. (in T_2 B)) /\ ((T_2 != B) /\ (-. (in B T_2))))))) (in T_3 T_1) (All B, ((in B T_1) => ((ordinal B) /\ (subset B T_1)))) (-. (in T_2 T_3)) (T_3 != T_2) (-. (in T_3 T_2)) ### All 52 % 16.66/16.90 54. ((ordinal T_2) => (All B, ((ordinal B) => (-. ((-. (in T_2 B)) /\ ((T_2 != B) /\ (-. (in B T_2)))))))) (-. (in T_3 T_2)) (T_3 != T_2) (-. (in T_2 T_3)) (in T_3 T_1) (All B, ((in B T_1) => ((ordinal B) /\ (subset B T_1)))) (in T_2 T_1) ### Imply 28 53 % 16.66/16.90 55. (All A, ((ordinal A) => (All B, ((ordinal B) => (-. ((-. (in A B)) /\ ((A != B) /\ (-. (in B A))))))))) (in T_2 T_1) (All B, ((in B T_1) => ((ordinal B) /\ (subset B T_1)))) (in T_3 T_1) (-. (in T_2 T_3)) (T_3 != T_2) (-. (in T_3 T_2)) ### All 54 % 16.66/16.90 56. ((in T_3 T_1) /\ ((in T_2 T_1) /\ ((-. (in T_3 T_2)) /\ ((T_3 != T_2) /\ (-. (in T_2 T_3)))))) (All B, ((in B T_1) => ((ordinal B) /\ (subset B T_1)))) (All A, ((ordinal A) => (All B, ((ordinal B) => (-. ((-. (in A B)) /\ ((A != B) /\ (-. (in B A))))))))) ### ConjTree 55 % 16.66/16.90 57. (-. (-. ((in T_3 T_1) /\ ((in T_2 T_1) /\ ((-. (in T_3 T_2)) /\ ((T_3 != T_2) /\ (-. (in T_2 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) /\ (subset B T_1)))) ### NotNot 56 % 16.66/16.90 58. (-. (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) /\ (subset B T_1)))) (All A, ((ordinal A) => (All B, ((ordinal B) => (-. ((-. (in A B)) /\ ((A != B) /\ (-. (in B A))))))))) ### NotAllEx 57 % 16.66/16.91 59. (-. (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) /\ (subset B T_1)))) ### NotAllEx 58 % 16.66/16.91 60. (-. (epsilon_connected T_1)) (All B, ((in B T_1) => ((ordinal B) /\ (subset B T_1)))) (All A, ((ordinal A) => (All B, ((ordinal B) => (-. ((-. (in A B)) /\ ((A != B) /\ (-. (in B A))))))))) ### Definition-Pseudo(epsilon_connected) 59 % 16.66/16.91 61. (-. ((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) /\ (subset B T_1)))) ### NotAnd 8 60 % 16.66/16.91 62. (-. (ordinal T_1)) (All B, ((in B T_1) => ((ordinal B) /\ (subset B T_1)))) (All A, ((ordinal A) => (All B, ((ordinal B) => (-. ((-. (in A B)) /\ ((A != B) /\ (-. (in B A))))))))) ### Definition-Pseudo(ordinal) 61 % 16.66/16.91 63. (-. ((All B, ((in B T_1) => ((ordinal B) /\ (subset B T_1)))) => (ordinal T_1))) (All A, ((ordinal A) => (All B, ((ordinal B) => (-. ((-. (in A B)) /\ ((A != B) /\ (-. (in B A))))))))) ### NotImply 62 % 16.66/16.91 64. (-. (All A, ((All B, ((in B A) => ((ordinal B) /\ (subset B A)))) => (ordinal A)))) (All A, ((ordinal A) => (All B, ((ordinal B) => (-. ((-. (in A B)) /\ ((A != B) /\ (-. (in B A))))))))) ### NotAllEx 63 % 16.66/16.91 % SZS output end Proof % 16.66/16.91 (* END-PROOF *) %------------------------------------------------------------------------------