%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : NUM858+1 : TPTP v8.1.0. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n007.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:46:52 EDT 2022 % Result : Theorem 9.55s 9.76s % Output : Proof 9.73s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : NUM858+1 : TPTP v8.1.0. Released v4.1.0. % 0.11/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n007.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.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Wed Jul 6 14:06:43 EDT 2022 % 0.12/0.34 % CPUTime : % 9.55/9.76 % SZS status Theorem % 9.55/9.76 (* PROOF-FOUND *) % 9.55/9.76 (* BEGIN-PROOF *) % 9.55/9.76 % SZS output start Proof % 9.55/9.76 1. ((max T_0 T_1) != (max T_0 T_1)) ### Refl(=) % 9.55/9.76 2. (-. (model_max T_0 T_1 (max T_0 T_1))) ### Definition-Pseudo(model_max) 1 % 9.55/9.76 3. (T_0 != T_0) ### Refl(=) % 9.55/9.76 4. (-. (lesseq T_0 T_0)) ### Refl(lesseq) % 9.55/9.76 5. (T_0 != T_0) ### Refl(=) % 9.55/9.76 6. (T_2 != T_2) ### Refl(=) % 9.55/9.76 7. (T_0 != (max T_0 T_1)) ((max T_0 T_1) = T_0) ### Sym(=) % 9.55/9.76 8. ((max T_0 T_1) != T_1) ((max T_0 T_1) = T_1) ### Axiom % 9.55/9.76 9. (lesseq T_0 T_1) (-. (lesseq T_0 T_1)) ### Axiom % 9.55/9.76 10. (((max T_0 T_1) = T_1) \/ (-. (lesseq T_0 T_1))) (lesseq T_0 T_1) ((max T_0 T_1) != T_1) ### Or 8 9 % 9.55/9.76 11. (All Y, (((max T_0 Y) = Y) \/ (-. (lesseq T_0 Y)))) ((max T_0 T_1) != T_1) (lesseq T_0 T_1) ### All 10 % 9.55/9.76 12. (-. (lesseq T_1 T_0)) (lesseq T_1 T_0) ### Axiom % 9.55/9.76 13. ((lesseq T_0 T_1) \/ (lesseq T_1 T_0)) (-. (lesseq T_1 T_0)) ((max T_0 T_1) != T_1) (All Y, (((max T_0 Y) = Y) \/ (-. (lesseq T_0 Y)))) ### Or 11 12 % 9.55/9.76 14. (All Y, ((lesseq T_0 Y) \/ (lesseq Y T_0))) (All Y, (((max T_0 Y) = Y) \/ (-. (lesseq T_0 Y)))) ((max T_0 T_1) != T_1) (-. (lesseq T_1 T_0)) ### All 13 % 9.55/9.76 15. (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (-. (lesseq T_1 T_0)) ((max T_0 T_1) != T_1) (All Y, ((lesseq T_0 Y) \/ (lesseq Y T_0))) ### All 14 % 9.55/9.76 16. (((max T_0 T_1) = T_0) \/ (-. (lesseq T_1 T_0))) (All Y, ((lesseq T_0 Y) \/ (lesseq Y T_0))) ((max T_0 T_1) != T_1) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (T_0 != (max T_0 T_1)) ### Or 7 15 % 9.55/9.76 17. (All Y, (((max T_0 Y) = T_0) \/ (-. (lesseq Y T_0)))) (T_0 != (max T_0 T_1)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) ((max T_0 T_1) != T_1) (All Y, ((lesseq T_0 Y) \/ (lesseq Y T_0))) ### All 16 % 9.55/9.76 18. (-. (lesseq T_2 T_1)) (lesseq T_2 (max T_0 T_1)) (All Y, ((lesseq T_0 Y) \/ (lesseq Y T_0))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (T_0 != (max T_0 T_1)) (All Y, (((max T_0 Y) = T_0) \/ (-. (lesseq Y T_0)))) ### Trans 6 17 % 9.55/9.76 19. (T_1 != T_1) ### Refl(=) % 9.55/9.76 20. (-. (lesseq T_1 T_1)) ### Refl(lesseq) % 9.55/9.76 21. (T_2 != T_2) ### Refl(=) % 9.55/9.76 22. (T_1 != (max T_0 T_1)) ((max T_0 T_1) = T_1) ### Sym(=) % 9.55/9.76 23. (lesseq T_0 T_1) (-. (lesseq T_0 T_1)) ### Axiom % 9.55/9.76 24. (((max T_0 T_1) = T_1) \/ (-. (lesseq T_0 T_1))) (lesseq T_0 T_1) (T_1 != (max T_0 T_1)) ### Or 22 23 % 9.55/9.76 25. (All Y, (((max T_0 Y) = Y) \/ (-. (lesseq T_0 Y)))) (T_1 != (max T_0 T_1)) (lesseq T_0 T_1) ### All 24 % 9.55/9.76 26. (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (lesseq T_0 T_1) (T_1 != (max T_0 T_1)) ### All 25 % 9.55/9.76 27. (-. (lesseq T_1 T_0)) (lesseq T_1 T_0) ### Axiom % 9.55/9.76 28. ((lesseq T_0 T_1) \/ (lesseq T_1 T_0)) (-. (lesseq T_1 T_0)) (T_1 != (max T_0 T_1)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) ### Or 26 27 % 9.55/9.76 29. (All Y, ((lesseq T_0 Y) \/ (lesseq Y T_0))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (T_1 != (max T_0 T_1)) (-. (lesseq T_1 T_0)) ### All 28 % 9.55/9.76 30. (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (-. (lesseq T_1 T_0)) (T_1 != (max T_0 T_1)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) ### All 29 % 9.55/9.76 31. ((max T_0 T_1) != T_0) ((max T_0 T_1) = T_0) ### Axiom % 9.55/9.76 32. (lesseq T_1 T_0) (-. (lesseq T_1 T_0)) ### Axiom % 9.55/9.76 33. (((max T_0 T_1) = T_0) \/ (-. (lesseq T_1 T_0))) (lesseq T_1 T_0) ((max T_0 T_1) != T_0) ### Or 31 32 % 9.55/9.76 34. (All Y, (((max T_0 Y) = T_0) \/ (-. (lesseq Y T_0)))) ((max T_0 T_1) != T_0) (lesseq T_1 T_0) ### All 33 % 9.55/9.76 35. ((lesseq T_1 T_0) <=> (lesseq (summation T_1) (summation T_0))) ((max T_0 T_1) != T_0) (All Y, (((max T_0 Y) = T_0) \/ (-. (lesseq Y T_0)))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (T_1 != (max T_0 T_1)) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) ### Equiv 30 34 % 9.55/9.76 36. (All Y, ((lesseq T_1 Y) <=> (lesseq (summation T_1) (summation Y)))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (T_1 != (max T_0 T_1)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All Y, (((max T_0 Y) = T_0) \/ (-. (lesseq Y T_0)))) ((max T_0 T_1) != T_0) ### All 35 % 9.55/9.76 37. (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) ((max T_0 T_1) != T_0) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (T_1 != (max T_0 T_1)) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All Y, ((lesseq T_1 Y) <=> (lesseq (summation T_1) (summation Y)))) ### All 36 % 9.55/9.76 38. (T_2 != T_0) (T_2 = (max T_0 T_1)) (All Y, ((lesseq T_1 Y) <=> (lesseq (summation T_1) (summation Y)))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (T_1 != (max T_0 T_1)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) ### Trans 21 37 % 9.55/9.76 39. (T_1 != T_1) ### Refl(=) % 9.55/9.76 40. ((max T_2 T_1) != (max T_0 T_1)) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (T_1 != (max T_0 T_1)) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All Y, ((lesseq T_1 Y) <=> (lesseq (summation T_1) (summation Y)))) (T_2 = (max T_0 T_1)) ### NotEqual 38 39 % 9.55/9.76 41. (-. (lesseq T_1 (max T_0 T_1))) ((max T_2 T_1) = T_1) (T_2 = (max T_0 T_1)) (All Y, ((lesseq T_1 Y) <=> (lesseq (summation T_1) (summation Y)))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (T_1 != (max T_0 T_1)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) ### TransEq2 19 20 40 % 9.55/9.76 42. (lesseq T_2 T_1) (-. (lesseq T_2 T_1)) ### Axiom % 9.55/9.76 43. (((max T_2 T_1) = T_1) \/ (-. (lesseq T_2 T_1))) (lesseq T_2 T_1) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (T_1 != (max T_0 T_1)) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All Y, ((lesseq T_1 Y) <=> (lesseq (summation T_1) (summation Y)))) (T_2 = (max T_0 T_1)) (-. (lesseq T_1 (max T_0 T_1))) ### Or 41 42 % 9.55/9.76 44. (All Y, (((max T_2 Y) = Y) \/ (-. (lesseq T_2 Y)))) (-. (lesseq T_1 (max T_0 T_1))) (T_2 = (max T_0 T_1)) (All Y, ((lesseq T_1 Y) <=> (lesseq (summation T_1) (summation Y)))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (T_1 != (max T_0 T_1)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (lesseq T_2 T_1) ### All 43 % 9.55/9.76 45. (lesseq T_2 T_1) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (T_1 != (max T_0 T_1)) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All Y, ((lesseq T_1 Y) <=> (lesseq (summation T_1) (summation Y)))) (T_2 = (max T_0 T_1)) (-. (lesseq T_1 (max T_0 T_1))) ### All 44 % 9.55/9.76 46. (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (-. (lesseq T_1 (max T_0 T_1))) (T_2 = (max T_0 T_1)) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (T_1 != (max T_0 T_1)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (lesseq T_2 T_1) ### All 45 % 9.55/9.76 47. (-. (lesseq T_1 T_2)) (lesseq T_1 T_2) ### Axiom % 9.55/9.76 48. ((lesseq T_2 T_1) \/ (lesseq T_1 T_2)) (-. (lesseq T_1 T_2)) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (T_1 != (max T_0 T_1)) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (T_2 = (max T_0 T_1)) (-. (lesseq T_1 (max T_0 T_1))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) ### Or 46 47 % 9.55/9.76 49. (All Y, ((lesseq T_2 Y) \/ (lesseq Y T_2))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (-. (lesseq T_1 (max T_0 T_1))) (T_2 = (max T_0 T_1)) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (T_1 != (max T_0 T_1)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (-. (lesseq T_1 T_2)) ### All 48 % 9.55/9.76 50. (-. (lesseq T_1 T_2)) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (T_1 != (max T_0 T_1)) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (T_2 = (max T_0 T_1)) (-. (lesseq T_1 (max T_0 T_1))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) ### All 49 % 9.55/9.76 51. (-. (lesseq T_2 T_2)) ### Refl(lesseq) % 9.55/9.76 52. (T_2 != T_2) ### Refl(=) % 9.55/9.76 53. (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (T_2 = (max T_0 T_1)) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (-. (lesseq T_1 T_2)) ### TransEq2 50 51 52 % 9.64/9.81 54. (T_2 != T_1) (T_2 = T_1) ### Axiom % 9.64/9.81 55. (((lesseq T_2 T_1) /\ (lesseq T_1 T_2)) => (T_2 = T_1)) (T_2 != T_1) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (T_2 = (max T_0 T_1)) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All Y, (((max T_0 Y) = T_0) \/ (-. (lesseq Y T_0)))) (T_0 != (max T_0 T_1)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All Y, ((lesseq T_0 Y) \/ (lesseq Y T_0))) (lesseq T_2 (max T_0 T_1)) ### DisjTree 18 53 54 % 9.64/9.81 56. (All Y, (((lesseq T_2 Y) /\ (lesseq Y T_2)) => (T_2 = Y))) (lesseq T_2 (max T_0 T_1)) (All Y, ((lesseq T_0 Y) \/ (lesseq Y T_0))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (T_0 != (max T_0 T_1)) (All Y, (((max T_0 Y) = T_0) \/ (-. (lesseq Y T_0)))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (T_2 = (max T_0 T_1)) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (T_2 != T_1) ### All 55 % 9.64/9.81 57. ((max T_0 T_2) != (max T_0 T_1)) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (T_2 = (max T_0 T_1)) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All Y, (((max T_0 Y) = T_0) \/ (-. (lesseq Y T_0)))) (T_0 != (max T_0 T_1)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All Y, ((lesseq T_0 Y) \/ (lesseq Y T_0))) (lesseq T_2 (max T_0 T_1)) (All Y, (((lesseq T_2 Y) /\ (lesseq Y T_2)) => (T_2 = Y))) ### NotEqual 5 56 % 9.64/9.81 58. (-. (lesseq T_0 (max T_0 T_1))) ((max T_0 T_2) = T_0) (All Y, (((lesseq T_2 Y) /\ (lesseq Y T_2)) => (T_2 = Y))) (lesseq T_2 (max T_0 T_1)) (All Y, ((lesseq T_0 Y) \/ (lesseq Y T_0))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (T_0 != (max T_0 T_1)) (All Y, (((max T_0 Y) = T_0) \/ (-. (lesseq Y T_0)))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (T_2 = (max T_0 T_1)) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) ### TransEq2 3 4 57 % 9.64/9.81 59. (lesseq T_2 T_0) (-. (lesseq T_2 T_0)) ### Axiom % 9.64/9.81 60. (((max T_0 T_2) = T_0) \/ (-. (lesseq T_2 T_0))) (lesseq T_2 T_0) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (T_2 = (max T_0 T_1)) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All Y, (((max T_0 Y) = T_0) \/ (-. (lesseq Y T_0)))) (T_0 != (max T_0 T_1)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All Y, ((lesseq T_0 Y) \/ (lesseq Y T_0))) (lesseq T_2 (max T_0 T_1)) (All Y, (((lesseq T_2 Y) /\ (lesseq Y T_2)) => (T_2 = Y))) (-. (lesseq T_0 (max T_0 T_1))) ### Or 58 59 % 9.64/9.81 61. (-. (lesseq T_0 (max T_0 T_1))) (All Y, (((lesseq T_2 Y) /\ (lesseq Y T_2)) => (T_2 = Y))) (lesseq T_2 (max T_0 T_1)) (All Y, ((lesseq T_0 Y) \/ (lesseq Y T_0))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (T_0 != (max T_0 T_1)) (All Y, (((max T_0 Y) = T_0) \/ (-. (lesseq Y T_0)))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (T_2 = (max T_0 T_1)) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (lesseq T_2 T_0) ### All 60 % 9.64/9.81 62. (lesseq T_2 T_0) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (T_2 = (max T_0 T_1)) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All Y, (((max T_0 Y) = T_0) \/ (-. (lesseq Y T_0)))) (T_0 != (max T_0 T_1)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (lesseq T_2 (max T_0 T_1)) (All Y, (((lesseq T_2 Y) /\ (lesseq Y T_2)) => (T_2 = Y))) (-. (lesseq T_0 (max T_0 T_1))) ### All 61 % 9.64/9.81 63. (-. (lesseq T_0 (max T_0 T_1))) (All Y, (((lesseq T_2 Y) /\ (lesseq Y T_2)) => (T_2 = Y))) (lesseq T_2 (max T_0 T_1)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (T_0 != (max T_0 T_1)) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (T_2 = (max T_0 T_1)) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (lesseq T_2 T_0) ### All 62 % 9.64/9.81 64. ((model_max T_0 T_1 (max T_0 T_1)) => (lesseq T_2 (max T_0 T_1))) (lesseq T_2 T_0) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (T_2 = (max T_0 T_1)) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (T_0 != (max T_0 T_1)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All Y, (((lesseq T_2 Y) /\ (lesseq Y T_2)) => (T_2 = Y))) (-. (lesseq T_0 (max T_0 T_1))) ### Imply 2 63 % 9.64/9.81 65. (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (-. (lesseq T_0 (max T_0 T_1))) (All Y, (((lesseq T_2 Y) /\ (lesseq Y T_2)) => (T_2 = Y))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (T_0 != (max T_0 T_1)) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (T_2 = (max T_0 T_1)) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (lesseq T_2 T_0) ### All 64 % 9.64/9.81 66. (-. (lesseq T_0 T_2)) (lesseq T_0 T_2) ### Axiom % 9.64/9.81 67. ((lesseq T_2 T_0) \/ (lesseq T_0 T_2)) (-. (lesseq T_0 T_2)) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (T_2 = (max T_0 T_1)) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (T_0 != (max T_0 T_1)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All Y, (((lesseq T_2 Y) /\ (lesseq Y T_2)) => (T_2 = Y))) (-. (lesseq T_0 (max T_0 T_1))) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) ### Or 65 66 % 9.64/9.81 68. (All Y, ((lesseq T_2 Y) \/ (lesseq Y T_2))) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (-. (lesseq T_0 (max T_0 T_1))) (All Y, (((lesseq T_2 Y) /\ (lesseq Y T_2)) => (T_2 = Y))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (T_0 != (max T_0 T_1)) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (T_2 = (max T_0 T_1)) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (-. (lesseq T_0 T_2)) ### All 67 % 9.64/9.81 69. (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (-. (lesseq T_0 T_2)) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (T_2 = (max T_0 T_1)) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (T_0 != (max T_0 T_1)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (-. (lesseq T_0 (max T_0 T_1))) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (All Y, ((lesseq T_2 Y) \/ (lesseq Y T_2))) ### All 68 % 9.64/9.81 70. (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (-. (lesseq T_0 (max T_0 T_1))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (T_0 != (max T_0 T_1)) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (T_2 = (max T_0 T_1)) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (-. (lesseq T_0 T_2)) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) ### All 69 % 9.64/9.81 71. (-. (lesseq T_2 T_2)) ### Refl(lesseq) % 9.64/9.81 72. (T_2 != T_2) ### Refl(=) % 9.64/9.81 73. (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (-. (lesseq T_0 T_2)) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (T_2 = (max T_0 T_1)) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) ### TransEq2 70 71 72 % 9.64/9.81 74. (-. ((lesseq T_0 T_2) /\ (lesseq T_1 T_2))) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (T_2 = (max T_0 T_1)) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) ### NotAnd 73 53 % 9.73/9.91 75. (-. (ub T_0 T_1 T_2)) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (T_2 = (max T_0 T_1)) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) ### Definition-Pseudo(ub) 74 % 9.73/9.91 76. (-. (model_ub T_0 T_1 T_2)) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (T_2 = (max T_0 T_1)) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) ### Definition-Pseudo(model_ub) 75 % 9.73/9.91 77. (T_2 != T_2) ### Refl(=) % 9.73/9.91 78. (-. (lesseq T_2 T_2)) ### Refl(lesseq) % 9.73/9.91 79. (T_2 != T_2) ### Refl(=) % 9.73/9.91 80. (-. (lesseq T_2 T_2)) ### Refl(lesseq) % 9.73/9.91 81. (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (lesseq T_1 T_0) ((max T_0 T_1) != T_0) ### All 34 % 9.73/9.91 82. (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (lesseq T_0 T_1) ((max T_0 T_1) != T_1) ### All 11 % 9.73/9.91 83. ((lesseq T_1 T_0) \/ (lesseq T_0 T_1)) ((max T_0 T_1) != T_1) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) ((max T_0 T_1) != T_0) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) ### Or 81 82 % 9.73/9.91 84. (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) ((max T_0 T_1) != T_0) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) ((max T_0 T_1) != T_1) ### All 83 % 9.73/9.91 85. (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) ((max T_0 T_1) != T_1) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) ((max T_0 T_1) != T_0) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) ### All 84 % 9.73/9.91 86. (-. (lesseq T_2 T_0)) (T_2 = (max T_0 T_1)) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) ((max T_0 T_1) != T_1) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) ### TransEq 79 80 85 % 9.73/9.91 87. (-. (lesseq T_2 T_1)) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (T_2 = (max T_0 T_1)) (-. (lesseq T_2 T_0)) ### TransEq 77 78 86 % 9.73/9.91 88. (T_3 != T_3) ### Refl(=) % 9.73/9.91 89. (-. (lesseq T_2 T_3)) (lesseq T_1 T_3) (-. (lesseq T_2 T_0)) (T_2 = (max T_0 T_1)) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) ### Trans 87 88 % 9.73/9.91 90. (T_3 != T_3) ### Refl(=) % 9.73/9.91 91. (lesseq T_0 T_3) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (T_2 = (max T_0 T_1)) (lesseq T_1 T_3) (-. (lesseq T_2 T_3)) ### Trans 89 90 % 9.73/9.91 92. ((lesseq T_0 T_3) /\ (lesseq T_1 T_3)) (-. (lesseq T_2 T_3)) (T_2 = (max T_0 T_1)) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) ### And 91 % 9.73/9.91 93. (ub T_0 T_1 T_3) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (T_2 = (max T_0 T_1)) (-. (lesseq T_2 T_3)) ### Definition-Pseudo(ub) 92 % 9.73/9.91 94. (model_ub T_0 T_1 T_3) (-. (lesseq T_2 T_3)) (T_2 = (max T_0 T_1)) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) ### Definition-Pseudo(model_ub) 93 % 9.73/9.91 95. (-. ((model_ub T_0 T_1 T_3) => (lesseq T_2 T_3))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (T_2 = (max T_0 T_1)) ### NotImply 94 % 9.73/9.91 96. (-. (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z)))) (T_2 = (max T_0 T_1)) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) ### NotAllEx 95 % 9.73/9.91 97. (-. ((model_ub T_0 T_1 T_2) /\ (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))))) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (T_2 = (max T_0 T_1)) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) ### NotAnd 76 96 % 9.73/9.91 98. (model_max T_0 T_1 T_2) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (-. ((model_ub T_0 T_1 T_2) /\ (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))))) ### Definition-Pseudo(model_max) 97 % 9.73/9.91 99. ((model_max T_0 T_1 T_2) /\ (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z)))) (-. ((model_ub T_0 T_1 T_2) /\ (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))))) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) ### And 98 % 9.73/9.91 100. (minsol_model_max T_0 T_1 T_2) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (-. ((model_ub T_0 T_1 T_2) /\ (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))))) ### Definition-Pseudo(minsol_model_max) 99 % 9.73/9.91 101. (-. (minsol_model_ub T_0 T_1 T_2)) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (minsol_model_max T_0 T_1 T_2) ### Definition-Pseudo(minsol_model_ub) 100 % 9.73/9.91 102. (-. (lesseq T_0 T_0)) ### Refl(lesseq) % 9.73/9.91 103. (lesseq T_1 T_0) (-. (lesseq T_1 T_0)) ### Axiom % 9.73/9.91 104. (-. ((lesseq T_0 T_0) /\ (lesseq T_1 T_0))) (lesseq T_1 T_0) ### NotAnd 102 103 % 9.73/9.91 105. (-. (ub T_0 T_1 T_0)) (lesseq T_1 T_0) ### Definition-Pseudo(ub) 104 % 9.73/9.91 106. (-. (model_ub T_0 T_1 T_0)) (lesseq T_1 T_0) ### Definition-Pseudo(model_ub) 105 % 9.73/9.91 107. (-. (lesseq T_2 T_0)) (lesseq T_2 T_0) ### Axiom % 9.73/9.91 108. ((model_ub T_0 T_1 T_0) => (lesseq T_2 T_0)) (-. (lesseq T_2 T_0)) (lesseq T_1 T_0) ### Imply 106 107 % 9.73/9.91 109. (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (lesseq T_1 T_0) (-. (lesseq T_2 T_0)) ### All 108 % 9.73/9.91 110. (-. (lesseq T_0 T_1)) (lesseq T_0 T_1) ### Axiom % 9.73/9.91 111. ((lesseq T_1 T_0) \/ (lesseq T_0 T_1)) (-. (lesseq T_0 T_1)) (-. (lesseq T_2 T_0)) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) ### Or 109 110 % 9.73/9.91 112. (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (-. (lesseq T_2 T_0)) (-. (lesseq T_0 T_1)) ### All 111 % 9.73/9.91 113. (lesseq T_0 T_2) (-. (lesseq T_0 T_2)) ### Axiom % 9.73/9.91 114. (T_0 != T_2) (T_2 = T_0) ### Sym(=) % 9.73/9.91 115. (((lesseq T_2 T_0) /\ (lesseq T_0 T_2)) => (T_2 = T_0)) (T_0 != T_2) (lesseq T_0 T_2) (-. (lesseq T_0 T_1)) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) ### DisjTree 112 113 114 % 9.73/9.91 116. (All Y, (((lesseq T_2 Y) /\ (lesseq Y T_2)) => (T_2 = Y))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (-. (lesseq T_0 T_1)) (lesseq T_0 T_2) (T_0 != T_2) ### All 115 % 9.73/9.93 117. (T_1 != T_1) ### Refl(=) % 9.73/9.93 118. ((max T_0 T_1) != (max T_2 T_1)) (lesseq T_0 T_2) (-. (lesseq T_0 T_1)) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All Y, (((lesseq T_2 Y) /\ (lesseq Y T_2)) => (T_2 = Y))) ### NotEqual 116 117 % 9.73/9.93 119. (T_2 != T_2) ### Refl(=) % 9.73/9.93 120. (T_2 != T_2) ### Refl(=) % 9.73/9.93 121. (T_2 != (max T_0 T_1)) ((max T_2 T_1) = T_2) (All Y, (((lesseq T_2 Y) /\ (lesseq Y T_2)) => (T_2 = Y))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (-. (lesseq T_0 T_1)) (lesseq T_0 T_2) ### TransEq-sym 118 119 120 % 9.73/9.93 122. (lesseq T_1 T_2) (-. (lesseq T_1 T_2)) ### Axiom % 9.73/9.93 123. (((max T_2 T_1) = T_2) \/ (-. (lesseq T_1 T_2))) (lesseq T_1 T_2) (lesseq T_0 T_2) (-. (lesseq T_0 T_1)) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All Y, (((lesseq T_2 Y) /\ (lesseq Y T_2)) => (T_2 = Y))) (T_2 != (max T_0 T_1)) ### Or 121 122 % 9.73/9.93 124. (All Y, (((max T_2 Y) = T_2) \/ (-. (lesseq Y T_2)))) (T_2 != (max T_0 T_1)) (All Y, (((lesseq T_2 Y) /\ (lesseq Y T_2)) => (T_2 = Y))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (-. (lesseq T_0 T_1)) (lesseq T_0 T_2) (lesseq T_1 T_2) ### All 123 % 9.73/9.93 125. (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (lesseq T_1 T_2) (lesseq T_0 T_2) (-. (lesseq T_0 T_1)) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (All Y, (((lesseq T_2 Y) /\ (lesseq Y T_2)) => (T_2 = Y))) (T_2 != (max T_0 T_1)) (All Y, (((max T_2 Y) = T_2) \/ (-. (lesseq Y T_2)))) ### All 124 % 9.73/9.93 126. (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (T_2 != (max T_0 T_1)) (All Y, (((lesseq T_2 Y) /\ (lesseq Y T_2)) => (T_2 = Y))) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (-. (lesseq T_0 T_1)) (lesseq T_0 T_2) (lesseq T_1 T_2) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) ### All 125 % 9.73/9.93 127. (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (lesseq T_1 T_2) (lesseq T_0 T_2) (-. (lesseq T_0 T_1)) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (T_2 != (max T_0 T_1)) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) ### All 126 % 9.73/9.93 128. (-. (lesseq T_1 T_1)) ### Refl(lesseq) % 9.73/9.93 129. (-. ((lesseq T_0 T_1) /\ (lesseq T_1 T_1))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (T_2 != (max T_0 T_1)) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (lesseq T_0 T_2) (lesseq T_1 T_2) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) ### NotAnd 127 128 % 9.73/9.93 130. (-. (ub T_0 T_1 T_1)) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (lesseq T_1 T_2) (lesseq T_0 T_2) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (T_2 != (max T_0 T_1)) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) ### Definition-Pseudo(ub) 129 % 9.73/9.93 131. (-. (model_ub T_0 T_1 T_1)) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (T_2 != (max T_0 T_1)) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (lesseq T_0 T_2) (lesseq T_1 T_2) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) ### Definition-Pseudo(model_ub) 130 % 9.73/9.93 132. (lesseq T_2 T_1) (-. (lesseq T_2 T_1)) ### Axiom % 9.73/9.93 133. (lesseq T_1 T_2) (-. (lesseq T_1 T_2)) ### Axiom % 9.73/9.93 134. (T_2 != T_2) ### Refl(=) % 9.73/9.93 135. (T_2 != T_2) ### Refl(=) % 9.73/9.93 136. (T_2 != T_2) ### Refl(=) % 9.73/9.93 137. (-. (lesseq T_2 T_0)) (lesseq T_2 T_1) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (T_1 != (max T_0 T_1)) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) ### Trans 136 30 % 9.73/9.93 138. (lesseq T_0 T_2) (-. (lesseq T_0 T_2)) ### Axiom % 9.73/9.93 139. (T_2 = T_1) (T_1 != T_2) ### Sym(=) % 9.73/9.93 140. (T_0 != T_0) ### Refl(=) % 9.73/9.93 141. (T_0 != T_1) (T_2 = T_0) (T_2 = T_1) ### Trans-sym 139 140 % 9.73/9.93 142. (T_2 = T_0) (T_0 != T_2) ### Sym(=) % 9.73/9.93 143. (T_1 != T_1) ### Refl(=) % 9.73/9.93 144. (T_1 != T_0) (T_2 = T_1) (T_2 = T_0) ### Trans-sym 142 143 % 9.73/9.93 145. ((max T_0 T_1) != (max T_1 T_0)) (T_2 = T_1) (T_2 = T_0) ### NotEqual 141 144 % 9.73/9.93 146. (T_1 != T_1) ### Refl(=) % 9.73/9.93 147. (T_1 != T_1) ### Refl(=) % 9.73/9.93 148. (T_1 != (max T_0 T_1)) ((max T_1 T_0) = T_1) (T_2 = T_0) (T_2 = T_1) ### TransEq-sym 145 146 147 % 9.73/9.93 149. (T_2 = T_0) (T_0 != T_2) ### Sym(=) % 9.73/9.93 150. (T_1 != T_1) ### Refl(=) % 9.73/9.93 151. (-. (lesseq T_0 T_1)) (lesseq T_2 T_1) (T_2 = T_0) ### Trans 149 150 % 9.73/9.93 152. (((max T_1 T_0) = T_1) \/ (-. (lesseq T_0 T_1))) (lesseq T_2 T_1) (T_2 = T_1) (T_2 = T_0) (T_1 != (max T_0 T_1)) ### Or 148 151 % 9.73/9.93 153. (All Y, (((max T_1 Y) = T_1) \/ (-. (lesseq Y T_1)))) (T_1 != (max T_0 T_1)) (T_2 = T_0) (T_2 = T_1) (lesseq T_2 T_1) ### All 152 % 9.73/9.93 154. (((lesseq T_2 T_0) /\ (lesseq T_0 T_2)) => (T_2 = T_0)) (T_2 = T_1) (All Y, (((max T_1 Y) = T_1) \/ (-. (lesseq Y T_1)))) (lesseq T_0 T_2) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (T_1 != (max T_0 T_1)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (lesseq T_2 T_1) ### DisjTree 137 138 153 % 9.73/9.93 155. (All Y, (((lesseq T_2 Y) /\ (lesseq Y T_2)) => (T_2 = Y))) (lesseq T_2 T_1) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (T_1 != (max T_0 T_1)) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (lesseq T_0 T_2) (All Y, (((max T_1 Y) = T_1) \/ (-. (lesseq Y T_1)))) (T_2 = T_1) ### All 154 % 9.73/9.93 156. (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (T_2 = T_1) (lesseq T_0 T_2) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (T_1 != (max T_0 T_1)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (lesseq T_2 T_1) (All Y, (((lesseq T_2 Y) /\ (lesseq Y T_2)) => (T_2 = Y))) ### All 155 % 9.73/9.93 157. (T_2 != (max T_0 T_1)) (All Y, (((lesseq T_2 Y) /\ (lesseq Y T_2)) => (T_2 = Y))) (lesseq T_2 T_1) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (lesseq T_0 T_2) (T_2 = T_1) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) ### TransEq 134 135 156 % 9.73/9.93 158. (((lesseq T_2 T_1) /\ (lesseq T_1 T_2)) => (T_2 = T_1)) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (lesseq T_0 T_2) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All Y, (((lesseq T_2 Y) /\ (lesseq Y T_2)) => (T_2 = Y))) (T_2 != (max T_0 T_1)) (lesseq T_1 T_2) (lesseq T_2 T_1) ### DisjTree 132 133 157 % 9.73/9.93 159. (lesseq T_2 T_1) (lesseq T_1 T_2) (T_2 != (max T_0 T_1)) (All Y, (((lesseq T_2 Y) /\ (lesseq Y T_2)) => (T_2 = Y))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (lesseq T_0 T_2) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) ### All 158 % 9.73/9.93 160. (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (lesseq T_0 T_2) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (T_2 != (max T_0 T_1)) (lesseq T_1 T_2) (lesseq T_2 T_1) ### All 159 % 9.73/9.93 161. ((model_ub T_0 T_1 T_1) => (lesseq T_2 T_1)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (lesseq T_1 T_2) (lesseq T_0 T_2) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (T_2 != (max T_0 T_1)) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) ### Imply 131 160 % 9.73/9.93 162. (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (T_2 != (max T_0 T_1)) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (lesseq T_0 T_2) (lesseq T_1 T_2) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) ### All 161 % 9.73/9.93 163. (-. (model_max T_0 T_1 T_2)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (lesseq T_1 T_2) (lesseq T_0 T_2) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) ### Definition-Pseudo(model_max) 162 % 9.73/9.94 164. (lesseq T_0 T_2) (-. (lesseq T_0 T_2)) ### Axiom % 9.73/9.94 165. (T_2 != T_2) ### Refl(=) % 9.73/9.94 166. (-. (lesseq T_2 T_2)) ### Refl(lesseq) % 9.73/9.94 167. (T_2 = T_0) (T_2 != T_0) ### Axiom % 9.73/9.94 168. (T_1 != T_1) ### Refl(=) % 9.73/9.94 169. ((max T_2 T_1) != (max T_0 T_1)) (T_2 = T_0) ### NotEqual 167 168 % 9.73/9.94 170. (-. (lesseq T_2 (max T_0 T_1))) ((max T_2 T_1) = T_2) (T_2 = T_0) ### TransEq2 165 166 169 % 9.73/9.94 171. (lesseq T_1 T_2) (-. (lesseq T_1 T_2)) ### Axiom % 9.73/9.94 172. (((max T_2 T_1) = T_2) \/ (-. (lesseq T_1 T_2))) (lesseq T_1 T_2) (T_2 = T_0) (-. (lesseq T_2 (max T_0 T_1))) ### Or 170 171 % 9.73/9.94 173. (All Y, (((max T_2 Y) = T_2) \/ (-. (lesseq Y T_2)))) (-. (lesseq T_2 (max T_0 T_1))) (T_2 = T_0) (lesseq T_1 T_2) ### All 172 % 9.73/9.94 174. (((lesseq T_2 T_0) /\ (lesseq T_0 T_2)) => (T_2 = T_0)) (lesseq T_1 T_2) (-. (lesseq T_2 (max T_0 T_1))) (All Y, (((max T_2 Y) = T_2) \/ (-. (lesseq Y T_2)))) (lesseq T_0 T_2) (-. (lesseq T_0 T_1)) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) ### DisjTree 112 164 173 % 9.73/9.94 175. (All Y, (((lesseq T_2 Y) /\ (lesseq Y T_2)) => (T_2 = Y))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (-. (lesseq T_0 T_1)) (lesseq T_0 T_2) (All Y, (((max T_2 Y) = T_2) \/ (-. (lesseq Y T_2)))) (-. (lesseq T_2 (max T_0 T_1))) (lesseq T_1 T_2) ### All 174 % 9.73/9.94 176. (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (lesseq T_1 T_2) (-. (lesseq T_2 (max T_0 T_1))) (All Y, (((max T_2 Y) = T_2) \/ (-. (lesseq Y T_2)))) (lesseq T_0 T_2) (-. (lesseq T_0 T_1)) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (All Y, (((lesseq T_2 Y) /\ (lesseq Y T_2)) => (T_2 = Y))) ### All 175 % 9.73/9.94 177. (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All Y, (((lesseq T_2 Y) /\ (lesseq Y T_2)) => (T_2 = Y))) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (-. (lesseq T_0 T_1)) (lesseq T_0 T_2) (-. (lesseq T_2 (max T_0 T_1))) (lesseq T_1 T_2) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) ### All 176 % 9.73/9.94 178. (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (lesseq T_1 T_2) (-. (lesseq T_2 (max T_0 T_1))) (lesseq T_0 T_2) (-. (lesseq T_0 T_1)) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) ### All 177 % 9.73/9.94 179. (-. (lesseq T_1 T_1)) ### Refl(lesseq) % 9.73/9.94 180. (-. ((lesseq T_0 T_1) /\ (lesseq T_1 T_1))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (lesseq T_0 T_2) (-. (lesseq T_2 (max T_0 T_1))) (lesseq T_1 T_2) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) ### NotAnd 178 179 % 9.73/9.94 181. (-. (ub T_0 T_1 T_1)) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (lesseq T_1 T_2) (-. (lesseq T_2 (max T_0 T_1))) (lesseq T_0 T_2) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) ### Definition-Pseudo(ub) 180 % 9.73/9.94 182. (-. (model_ub T_0 T_1 T_1)) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (lesseq T_0 T_2) (-. (lesseq T_2 (max T_0 T_1))) (lesseq T_1 T_2) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) ### Definition-Pseudo(model_ub) 181 % 9.73/9.94 183. (T_2 != T_2) ### Refl(=) % 9.73/9.94 184. (lesseq T_2 T_1) (-. (lesseq T_2 T_1)) ### Axiom % 9.73/9.94 185. (lesseq T_1 T_2) (-. (lesseq T_1 T_2)) ### Axiom % 9.73/9.94 186. (T_2 != T_2) ### Refl(=) % 9.73/9.94 187. (-. (lesseq T_2 T_0)) (lesseq T_2 T_1) (T_1 != (max T_0 T_1)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All Y, ((lesseq T_0 Y) \/ (lesseq Y T_0))) ### Trans 186 29 % 9.73/9.94 188. (lesseq T_0 T_2) (-. (lesseq T_0 T_2)) ### Axiom % 9.73/9.94 189. (T_2 != T_2) ### Refl(=) % 9.73/9.94 190. (-. (lesseq T_2 T_2)) ### Refl(lesseq) % 9.73/9.94 191. (T_2 = T_0) (T_2 != T_0) ### Axiom % 9.73/9.94 192. (T_2 = T_1) (T_2 != T_1) ### Axiom % 9.73/9.94 193. ((max T_2 T_2) != (max T_0 T_1)) (T_2 = T_1) (T_2 = T_0) ### NotEqual 191 192 % 9.73/9.94 194. (-. (lesseq T_2 (max T_0 T_1))) ((max T_2 T_2) = T_2) (T_2 = T_0) (T_2 = T_1) ### TransEq2 189 190 193 % 9.73/9.94 195. (-. (lesseq T_2 T_2)) ### Refl(lesseq) % 9.73/9.94 196. (((max T_2 T_2) = T_2) \/ (-. (lesseq T_2 T_2))) (T_2 = T_1) (T_2 = T_0) (-. (lesseq T_2 (max T_0 T_1))) ### Or 194 195 % 9.73/9.94 197. (All Y, (((max T_2 Y) = T_2) \/ (-. (lesseq Y T_2)))) (-. (lesseq T_2 (max T_0 T_1))) (T_2 = T_0) (T_2 = T_1) ### All 196 % 9.73/9.94 198. (((lesseq T_2 T_0) /\ (lesseq T_0 T_2)) => (T_2 = T_0)) (T_2 = T_1) (-. (lesseq T_2 (max T_0 T_1))) (All Y, (((max T_2 Y) = T_2) \/ (-. (lesseq Y T_2)))) (lesseq T_0 T_2) (All Y, ((lesseq T_0 Y) \/ (lesseq Y T_0))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (T_1 != (max T_0 T_1)) (lesseq T_2 T_1) ### DisjTree 187 188 197 % 9.73/9.94 199. (All Y, (((lesseq T_2 Y) /\ (lesseq Y T_2)) => (T_2 = Y))) (lesseq T_2 T_1) (T_1 != (max T_0 T_1)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All Y, ((lesseq T_0 Y) \/ (lesseq Y T_0))) (lesseq T_0 T_2) (All Y, (((max T_2 Y) = T_2) \/ (-. (lesseq Y T_2)))) (-. (lesseq T_2 (max T_0 T_1))) (T_2 = T_1) ### All 198 % 9.73/9.94 200. (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (T_2 = T_1) (-. (lesseq T_2 (max T_0 T_1))) (All Y, (((max T_2 Y) = T_2) \/ (-. (lesseq Y T_2)))) (lesseq T_0 T_2) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (T_1 != (max T_0 T_1)) (lesseq T_2 T_1) (All Y, (((lesseq T_2 Y) /\ (lesseq Y T_2)) => (T_2 = Y))) ### All 199 % 9.73/9.94 201. (((lesseq T_2 T_1) /\ (lesseq T_1 T_2)) => (T_2 = T_1)) (All Y, (((lesseq T_2 Y) /\ (lesseq Y T_2)) => (T_2 = Y))) (T_1 != (max T_0 T_1)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (lesseq T_0 T_2) (All Y, (((max T_2 Y) = T_2) \/ (-. (lesseq Y T_2)))) (-. (lesseq T_2 (max T_0 T_1))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (lesseq T_1 T_2) (lesseq T_2 T_1) ### DisjTree 184 185 200 % 9.73/9.94 202. (lesseq T_2 T_1) (lesseq T_1 T_2) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (-. (lesseq T_2 (max T_0 T_1))) (All Y, (((max T_2 Y) = T_2) \/ (-. (lesseq Y T_2)))) (lesseq T_0 T_2) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (T_1 != (max T_0 T_1)) (All Y, (((lesseq T_2 Y) /\ (lesseq Y T_2)) => (T_2 = Y))) ### All 201 % 9.73/9.94 203. (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All Y, (((lesseq T_2 Y) /\ (lesseq Y T_2)) => (T_2 = Y))) (T_1 != (max T_0 T_1)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (lesseq T_0 T_2) (-. (lesseq T_2 (max T_0 T_1))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (lesseq T_1 T_2) (lesseq T_2 T_1) ### All 202 % 9.73/9.94 204. (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (lesseq T_2 T_1) (lesseq T_1 T_2) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (-. (lesseq T_2 (max T_0 T_1))) (lesseq T_0 T_2) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (T_1 != (max T_0 T_1)) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) ### All 203 % 9.73/9.94 205. (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (lesseq T_0 T_2) (-. (lesseq T_2 (max T_0 T_1))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (lesseq T_1 T_2) (lesseq T_2 T_1) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) ### Trans 183 204 % 9.73/9.94 206. ((model_ub T_0 T_1 T_1) => (lesseq T_2 T_1)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (lesseq T_1 T_2) (-. (lesseq T_2 (max T_0 T_1))) (lesseq T_0 T_2) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) ### Imply 182 205 % 9.73/9.94 207. (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (lesseq T_0 T_2) (-. (lesseq T_2 (max T_0 T_1))) (lesseq T_1 T_2) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) ### All 206 % 9.73/9.94 208. (-. (lesseq T_4 T_4)) ### Refl(lesseq) % 9.73/9.95 209. (T_4 != T_4) ### Refl(=) % 9.73/9.95 210. (-. (lesseq T_2 T_4)) (T_4 = (max T_0 T_1)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (lesseq T_1 T_2) (lesseq T_0 T_2) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) ### TransEq2 207 208 209 % 9.73/9.95 211. (model_max T_0 T_1 T_4) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (lesseq T_0 T_2) (lesseq T_1 T_2) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (-. (lesseq T_2 T_4)) ### Definition-Pseudo(model_max) 210 % 9.73/9.95 212. (-. ((model_max T_0 T_1 T_4) => (lesseq T_2 T_4))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (lesseq T_1 T_2) (lesseq T_0 T_2) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) ### NotImply 211 % 9.73/9.95 213. (-. (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z)))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (lesseq T_0 T_2) (lesseq T_1 T_2) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) ### NotAllEx 212 % 9.73/9.95 214. (-. ((model_max T_0 T_1 T_2) /\ (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (lesseq T_0 T_2) (lesseq T_1 T_2) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) ### NotAnd 163 213 % 9.73/9.95 215. (-. (minsol_model_max T_0 T_1 T_2)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (lesseq T_1 T_2) (lesseq T_0 T_2) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) ### Definition-Pseudo(minsol_model_max) 214 % 9.73/9.95 216. ((lesseq T_0 T_2) /\ (lesseq T_1 T_2)) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (-. (minsol_model_max T_0 T_1 T_2)) ### And 215 % 9.73/9.95 217. (ub T_0 T_1 T_2) (-. (minsol_model_max T_0 T_1 T_2)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) ### Definition-Pseudo(ub) 216 % 9.73/9.95 218. (model_ub T_0 T_1 T_2) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (-. (minsol_model_max T_0 T_1 T_2)) ### Definition-Pseudo(model_ub) 217 % 9.73/9.95 219. ((model_ub T_0 T_1 T_2) /\ (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z)))) (-. (minsol_model_max T_0 T_1 T_2)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) ### And 218 % 9.73/9.95 220. (minsol_model_ub T_0 T_1 T_2) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (-. (minsol_model_max T_0 T_1 T_2)) ### Definition-Pseudo(minsol_model_ub) 219 % 9.73/9.95 221. (-. ((minsol_model_ub T_0 T_1 T_2) <=> (minsol_model_max T_0 T_1 T_2))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) ### NotEquiv 101 220 % 9.73/9.95 222. (-. (All Z, ((minsol_model_ub T_0 T_1 Z) <=> (minsol_model_max T_0 T_1 Z)))) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) ### NotAllEx 221 % 9.73/9.95 223. (-. (All Y, (All Z, ((minsol_model_ub T_0 Y Z) <=> (minsol_model_max T_0 Y Z))))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) ### NotAllEx 222 % 9.73/9.95 224. (-. (All X, (All Y, (All Z, ((minsol_model_ub X Y Z) <=> (minsol_model_max X Y Z)))))) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) ### NotAllEx 223 % 9.73/9.95 % SZS output end Proof % 9.73/9.95 (* END-PROOF *) %------------------------------------------------------------------------------