%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SEU234+3 : 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 : n012.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 15.48s 15.72s % Output : Proof 15.58s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.11 % Problem : SEU234+3 : TPTP v8.1.0. Released v3.2.0. % 0.10/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.13/0.33 % Computer : n012.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Sun Jun 19 12:47:23 EDT 2022 % 0.13/0.33 % CPUTime : % 15.48/15.72 % SZS status Theorem % 15.48/15.72 (* PROOF-FOUND *) % 15.48/15.72 (* BEGIN-PROOF *) % 15.48/15.72 % SZS output start Proof % 15.48/15.72 1. (in T_0 T_1) (-. (in T_0 T_1)) ### Axiom % 15.48/15.72 2. (-. (subset T_0 T_1)) (subset T_0 T_1) ### Axiom % 15.48/15.72 3. ((ordinal T_0) /\ (subset T_0 T_1)) (-. (subset T_0 T_1)) ### And 2 % 15.48/15.72 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 % 15.48/15.72 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 % 15.48/15.72 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 % 15.48/15.72 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 % 15.48/15.72 8. (-. (epsilon_transitive T_1)) (All B, ((in B T_1) => ((ordinal B) /\ (subset B T_1)))) ### Definition-Pseudo(epsilon_transitive) 7 % 15.48/15.72 9. (in T_2 T_1) (-. (in T_2 T_1)) ### Axiom % 15.48/15.72 10. (-. (All B, ((in B T_2) => (subset B T_2)))) (All B, ((in B T_2) => (subset B T_2))) ### Axiom % 15.48/15.72 11. (epsilon_transitive T_2) (-. (All B, ((in B T_2) => (subset B T_2)))) ### Definition-Pseudo(epsilon_transitive) 10 % 15.48/15.72 12. ((epsilon_transitive T_2) /\ (epsilon_connected T_2)) (-. (All B, ((in B T_2) => (subset B T_2)))) ### And 11 % 15.48/15.72 13. (ordinal T_2) (-. (All B, ((in B T_2) => (subset B T_2)))) ### Definition-Pseudo(ordinal) 12 % 15.48/15.72 14. ((ordinal T_2) /\ (subset T_2 T_1)) (-. (All B, ((in B T_2) => (subset B T_2)))) ### And 13 % 15.48/15.72 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 % 15.48/15.72 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 % 15.48/15.72 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 % 15.48/15.72 18. (in T_2 T_1) (-. (in T_2 T_1)) ### Axiom % 15.48/15.72 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 % 15.48/15.72 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 % 15.48/15.72 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 % 15.48/15.72 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 % 15.48/15.72 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 % 15.48/15.72 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 % 15.48/15.72 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 % 15.48/15.72 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 % 15.48/15.72 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 % 15.48/15.72 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 % 15.48/15.72 29. (in T_3 T_1) (-. (in T_3 T_1)) ### Axiom % 15.48/15.72 30. (-. (All B, ((in B T_3) => (subset B T_3)))) (All B, ((in B T_3) => (subset B T_3))) ### Axiom % 15.48/15.72 31. (epsilon_transitive T_3) (-. (All B, ((in B T_3) => (subset B T_3)))) ### Definition-Pseudo(epsilon_transitive) 30 % 15.48/15.72 32. ((epsilon_transitive T_3) /\ (epsilon_connected T_3)) (-. (All B, ((in B T_3) => (subset B T_3)))) ### And 31 % 15.48/15.72 33. (ordinal T_3) (-. (All B, ((in B T_3) => (subset B T_3)))) ### Definition-Pseudo(ordinal) 32 % 15.48/15.72 34. ((ordinal T_3) /\ (subset T_3 T_1)) (-. (All B, ((in B T_3) => (subset B T_3)))) ### And 33 % 15.48/15.72 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 % 15.48/15.72 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 % 15.48/15.72 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 % 15.48/15.72 38. (in T_3 T_1) (-. (in T_3 T_1)) ### Axiom % 15.48/15.72 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 % 15.48/15.72 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 % 15.48/15.72 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 % 15.48/15.72 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 % 15.48/15.72 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 % 15.48/15.72 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 % 15.48/15.72 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 % 15.48/15.72 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 % 15.48/15.72 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 % 15.48/15.72 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 % 15.48/15.72 49. (-. (in T_2 T_3)) (in T_2 T_3) ### Axiom % 15.48/15.72 50. (T_3 != T_2) (T_2 = T_3) ### Sym(=) % 15.48/15.72 51. (-. (in T_3 T_2)) (in T_3 T_2) ### Axiom % 15.48/15.72 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 % 15.48/15.72 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 % 15.48/15.72 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 % 15.48/15.72 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 % 15.48/15.72 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 % 15.48/15.72 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 % 15.48/15.72 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 % 15.58/15.73 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 % 15.58/15.73 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 % 15.58/15.73 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 % 15.58/15.73 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 % 15.58/15.73 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 % 15.58/15.73 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 % 15.58/15.73 % SZS output end Proof % 15.58/15.73 (* END-PROOF *) %------------------------------------------------------------------------------