%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : MSC012+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 : 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 : Sun Jul 17 23:00:22 EDT 2022 % Result : Theorem 0.91s 1.15s % Output : Proof 0.91s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : MSC012+1 : TPTP v8.1.0. Released v3.2.0. % 0.11/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.13/0.34 % Computer : n015.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Fri Jul 1 16:53:58 EDT 2022 % 0.13/0.34 % CPUTime : % 0.91/1.15 % SZS status Theorem % 0.91/1.15 (* PROOF-FOUND *) % 0.91/1.15 (* BEGIN-PROOF *) % 0.91/1.15 % SZS output start Proof % 0.91/1.15 1. (p zenon_X0) (-. (p zenon_X0)) ### Axiom % 0.91/1.15 2. (less zenon_X0 T_1) (-. (less zenon_X0 T_1)) ### Axiom % 0.91/1.15 3. (-. (p T_1)) (p T_1) ### Axiom % 0.91/1.15 4. (less zenon_X0 T_1) (-. (less zenon_X0 T_1)) ### Axiom % 0.91/1.15 5. (less T_1 T_2) (-. (less T_1 T_2)) ### Axiom % 0.91/1.15 6. (p zenon_X0) (-. (p zenon_X0)) ### Axiom % 0.91/1.15 7. (less zenon_X0 T_2) (-. (less zenon_X0 T_2)) ### Axiom % 0.91/1.15 8. (p T_2) (-. (p T_2)) ### Axiom % 0.91/1.15 9. (-. (goal)) (goal) ### P-NotP % 0.91/1.15 10. (((p zenon_X0) /\ ((less zenon_X0 T_2) /\ (p T_2))) => (goal)) (-. (goal)) (p T_2) (less zenon_X0 T_2) (p zenon_X0) ### DisjTree 6 7 8 9 % 0.91/1.15 11. (All B, (((p zenon_X0) /\ ((less zenon_X0 B) /\ (p B))) => (goal))) (p zenon_X0) (less zenon_X0 T_2) (p T_2) (-. (goal)) ### All 10 % 0.91/1.15 12. (((less zenon_X0 T_1) /\ (less T_1 T_2)) => (less zenon_X0 T_2)) (-. (goal)) (p T_2) (p zenon_X0) (All B, (((p zenon_X0) /\ ((less zenon_X0 B) /\ (p B))) => (goal))) (less T_1 T_2) (less zenon_X0 T_1) ### DisjTree 4 5 11 % 0.91/1.15 13. (All C, (((less zenon_X0 T_1) /\ (less T_1 C)) => (less zenon_X0 C))) (less zenon_X0 T_1) (less T_1 T_2) (All B, (((p zenon_X0) /\ ((less zenon_X0 B) /\ (p B))) => (goal))) (p zenon_X0) (p T_2) (-. (goal)) ### All 12 % 0.91/1.15 14. (All B, (All C, (((less zenon_X0 B) /\ (less B C)) => (less zenon_X0 C)))) (-. (goal)) (p T_2) (p zenon_X0) (All B, (((p zenon_X0) /\ ((less zenon_X0 B) /\ (p B))) => (goal))) (less T_1 T_2) (less zenon_X0 T_1) ### All 13 % 0.91/1.15 15. ((less T_1 T_2) /\ (p T_2)) (less zenon_X0 T_1) (All B, (((p zenon_X0) /\ ((less zenon_X0 B) /\ (p B))) => (goal))) (p zenon_X0) (-. (goal)) (All B, (All C, (((less zenon_X0 B) /\ (less B C)) => (less zenon_X0 C)))) ### And 14 % 0.91/1.15 16. (Ex B, ((less T_1 B) /\ (p B))) (All B, (All C, (((less zenon_X0 B) /\ (less B C)) => (less zenon_X0 C)))) (-. (goal)) (p zenon_X0) (All B, (((p zenon_X0) /\ ((less zenon_X0 B) /\ (p B))) => (goal))) (less zenon_X0 T_1) ### Exists 15 % 0.91/1.15 17. ((p T_1) \/ (Ex B, ((less T_1 B) /\ (p B)))) (less zenon_X0 T_1) (All B, (((p zenon_X0) /\ ((less zenon_X0 B) /\ (p B))) => (goal))) (p zenon_X0) (-. (goal)) (All B, (All C, (((less zenon_X0 B) /\ (less B C)) => (less zenon_X0 C)))) (-. (p T_1)) ### Or 3 16 % 0.91/1.15 18. (All A, ((p A) \/ (Ex B, ((less A B) /\ (p B))))) (-. (p T_1)) (All B, (All C, (((less zenon_X0 B) /\ (less B C)) => (less zenon_X0 C)))) (-. (goal)) (p zenon_X0) (All B, (((p zenon_X0) /\ ((less zenon_X0 B) /\ (p B))) => (goal))) (less zenon_X0 T_1) ### All 17 % 0.91/1.15 19. (All A, (All B, (All C, (((less A B) /\ (less B C)) => (less A C))))) (less zenon_X0 T_1) (All B, (((p zenon_X0) /\ ((less zenon_X0 B) /\ (p B))) => (goal))) (p zenon_X0) (-. (goal)) (-. (p T_1)) (All A, ((p A) \/ (Ex B, ((less A B) /\ (p B))))) ### All 18 % 0.91/1.15 20. (((p zenon_X0) /\ ((less zenon_X0 T_1) /\ (p T_1))) => (goal)) (All A, ((p A) \/ (Ex B, ((less A B) /\ (p B))))) (-. (goal)) (All B, (((p zenon_X0) /\ ((less zenon_X0 B) /\ (p B))) => (goal))) (All A, (All B, (All C, (((less A B) /\ (less B C)) => (less A C))))) (less zenon_X0 T_1) (p zenon_X0) ### DisjTree 1 2 19 9 % 0.91/1.15 21. (p zenon_X0) (less zenon_X0 T_1) (All A, (All B, (All C, (((less A B) /\ (less B C)) => (less A C))))) (All B, (((p zenon_X0) /\ ((less zenon_X0 B) /\ (p B))) => (goal))) (-. (goal)) (All A, ((p A) \/ (Ex B, ((less A B) /\ (p B))))) ### All 20 % 0.91/1.15 22. (Ex B, (less zenon_X0 B)) (All A, ((p A) \/ (Ex B, ((less A B) /\ (p B))))) (-. (goal)) (All B, (((p zenon_X0) /\ ((less zenon_X0 B) /\ (p B))) => (goal))) (All A, (All B, (All C, (((less A B) /\ (less B C)) => (less A C))))) (p zenon_X0) ### Exists 21 % 0.91/1.15 23. (All A, (Ex B, (less A B))) (p zenon_X0) (All A, (All B, (All C, (((less A B) /\ (less B C)) => (less A C))))) (All B, (((p zenon_X0) /\ ((less zenon_X0 B) /\ (p B))) => (goal))) (-. (goal)) (All A, ((p A) \/ (Ex B, ((less A B) /\ (p B))))) ### All 22 % 0.91/1.15 24. (All A, (All B, (((p A) /\ ((less A B) /\ (p B))) => (goal)))) (All A, ((p A) \/ (Ex B, ((less A B) /\ (p B))))) (-. (goal)) (All A, (All B, (All C, (((less A B) /\ (less B C)) => (less A C))))) (p zenon_X0) (All A, (Ex B, (less A B))) ### All 23 % 0.91/1.15 25. (p T_3) (-. (p T_3)) ### Axiom % 0.91/1.15 26. (less T_3 T_4) (-. (less T_3 T_4)) ### Axiom % 0.91/1.15 27. (-. (p T_4)) (p T_4) ### Axiom % 0.91/1.15 28. (less T_3 T_4) (-. (less T_3 T_4)) ### Axiom % 0.91/1.15 29. (less T_4 T_5) (-. (less T_4 T_5)) ### Axiom % 0.91/1.15 30. (p T_3) (-. (p T_3)) ### Axiom % 0.91/1.15 31. (less T_3 T_5) (-. (less T_3 T_5)) ### Axiom % 0.91/1.15 32. (p T_5) (-. (p T_5)) ### Axiom % 0.91/1.15 33. (((p T_3) /\ ((less T_3 T_5) /\ (p T_5))) => (goal)) (-. (goal)) (p T_5) (less T_3 T_5) (p T_3) ### DisjTree 30 31 32 9 % 0.91/1.15 34. (All B, (((p T_3) /\ ((less T_3 B) /\ (p B))) => (goal))) (p T_3) (less T_3 T_5) (p T_5) (-. (goal)) ### All 33 % 0.91/1.15 35. (((less T_3 T_4) /\ (less T_4 T_5)) => (less T_3 T_5)) (-. (goal)) (p T_5) (p T_3) (All B, (((p T_3) /\ ((less T_3 B) /\ (p B))) => (goal))) (less T_4 T_5) (less T_3 T_4) ### DisjTree 28 29 34 % 0.91/1.15 36. (All C, (((less T_3 T_4) /\ (less T_4 C)) => (less T_3 C))) (less T_3 T_4) (less T_4 T_5) (All B, (((p T_3) /\ ((less T_3 B) /\ (p B))) => (goal))) (p T_3) (p T_5) (-. (goal)) ### All 35 % 0.91/1.15 37. ((less T_4 T_5) /\ (p T_5)) (-. (goal)) (p T_3) (All B, (((p T_3) /\ ((less T_3 B) /\ (p B))) => (goal))) (less T_3 T_4) (All C, (((less T_3 T_4) /\ (less T_4 C)) => (less T_3 C))) ### And 36 % 0.91/1.15 38. (Ex B, ((less T_4 B) /\ (p B))) (All C, (((less T_3 T_4) /\ (less T_4 C)) => (less T_3 C))) (less T_3 T_4) (All B, (((p T_3) /\ ((less T_3 B) /\ (p B))) => (goal))) (p T_3) (-. (goal)) ### Exists 37 % 0.91/1.15 39. ((p T_4) \/ (Ex B, ((less T_4 B) /\ (p B)))) (-. (goal)) (p T_3) (All B, (((p T_3) /\ ((less T_3 B) /\ (p B))) => (goal))) (less T_3 T_4) (All C, (((less T_3 T_4) /\ (less T_4 C)) => (less T_3 C))) (-. (p T_4)) ### Or 27 38 % 0.91/1.15 40. (All A, ((p A) \/ (Ex B, ((less A B) /\ (p B))))) (-. (p T_4)) (All C, (((less T_3 T_4) /\ (less T_4 C)) => (less T_3 C))) (less T_3 T_4) (All B, (((p T_3) /\ ((less T_3 B) /\ (p B))) => (goal))) (p T_3) (-. (goal)) ### All 39 % 0.91/1.15 41. (All B, (All C, (((less T_3 B) /\ (less B C)) => (less T_3 C)))) (-. (goal)) (p T_3) (All B, (((p T_3) /\ ((less T_3 B) /\ (p B))) => (goal))) (less T_3 T_4) (-. (p T_4)) (All A, ((p A) \/ (Ex B, ((less A B) /\ (p B))))) ### All 40 % 0.91/1.15 42. (All A, (All B, (All C, (((less A B) /\ (less B C)) => (less A C))))) (All A, ((p A) \/ (Ex B, ((less A B) /\ (p B))))) (-. (p T_4)) (less T_3 T_4) (All B, (((p T_3) /\ ((less T_3 B) /\ (p B))) => (goal))) (p T_3) (-. (goal)) ### All 41 % 0.91/1.15 43. (((p T_3) /\ ((less T_3 T_4) /\ (p T_4))) => (goal)) (-. (goal)) (All B, (((p T_3) /\ ((less T_3 B) /\ (p B))) => (goal))) (All A, ((p A) \/ (Ex B, ((less A B) /\ (p B))))) (All A, (All B, (All C, (((less A B) /\ (less B C)) => (less A C))))) (less T_3 T_4) (p T_3) ### DisjTree 25 26 42 9 % 0.91/1.15 44. (p T_3) (less T_3 T_4) (All A, (All B, (All C, (((less A B) /\ (less B C)) => (less A C))))) (All A, ((p A) \/ (Ex B, ((less A B) /\ (p B))))) (All B, (((p T_3) /\ ((less T_3 B) /\ (p B))) => (goal))) (-. (goal)) ### All 43 % 0.91/1.15 45. (Ex B, (less T_3 B)) (-. (goal)) (All B, (((p T_3) /\ ((less T_3 B) /\ (p B))) => (goal))) (All A, ((p A) \/ (Ex B, ((less A B) /\ (p B))))) (All A, (All B, (All C, (((less A B) /\ (less B C)) => (less A C))))) (p T_3) ### Exists 44 % 0.91/1.15 46. (All A, (Ex B, (less A B))) (p T_3) (All A, (All B, (All C, (((less A B) /\ (less B C)) => (less A C))))) (All A, ((p A) \/ (Ex B, ((less A B) /\ (p B))))) (All B, (((p T_3) /\ ((less T_3 B) /\ (p B))) => (goal))) (-. (goal)) ### All 45 % 0.91/1.15 47. (All A, (All B, (((p A) /\ ((less A B) /\ (p B))) => (goal)))) (-. (goal)) (All A, ((p A) \/ (Ex B, ((less A B) /\ (p B))))) (All A, (All B, (All C, (((less A B) /\ (less B C)) => (less A C))))) (p T_3) (All A, (Ex B, (less A B))) ### All 46 % 0.91/1.15 48. ((less zenon_X0 T_3) /\ (p T_3)) (All A, (Ex B, (less A B))) (All A, (All B, (All C, (((less A B) /\ (less B C)) => (less A C))))) (All A, ((p A) \/ (Ex B, ((less A B) /\ (p B))))) (-. (goal)) (All A, (All B, (((p A) /\ ((less A B) /\ (p B))) => (goal)))) ### And 47 % 0.91/1.15 49. (Ex B, ((less zenon_X0 B) /\ (p B))) (All A, (All B, (((p A) /\ ((less A B) /\ (p B))) => (goal)))) (-. (goal)) (All A, ((p A) \/ (Ex B, ((less A B) /\ (p B))))) (All A, (All B, (All C, (((less A B) /\ (less B C)) => (less A C))))) (All A, (Ex B, (less A B))) ### Exists 48 % 0.91/1.15 50. ((p zenon_X0) \/ (Ex B, ((less zenon_X0 B) /\ (p B)))) (All A, (Ex B, (less A B))) (All A, (All B, (All C, (((less A B) /\ (less B C)) => (less A C))))) (-. (goal)) (All A, ((p A) \/ (Ex B, ((less A B) /\ (p B))))) (All A, (All B, (((p A) /\ ((less A B) /\ (p B))) => (goal)))) ### Or 24 49 % 0.91/1.15 51. (All A, (All B, (((p A) /\ ((less A B) /\ (p B))) => (goal)))) (All A, ((p A) \/ (Ex B, ((less A B) /\ (p B))))) (-. (goal)) (All A, (All B, (All C, (((less A B) /\ (less B C)) => (less A C))))) (All A, (Ex B, (less A B))) ### All 50 % 0.91/1.15 % SZS output end Proof % 0.91/1.15 (* END-PROOF *) %------------------------------------------------------------------------------