%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : NUM860+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 : n024.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:53 EDT 2022 % Result : Theorem 27.71s 27.93s % Output : Proof 27.86s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : NUM860+1 : TPTP v8.1.0. Released v4.1.0. % 0.06/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.34 % Computer : n024.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % 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 : Thu Jul 7 02:23:44 EDT 2022 % 0.12/0.34 % CPUTime : % 27.71/27.93 % SZS status Theorem % 27.71/27.93 (* PROOF-FOUND *) % 27.71/27.93 (* BEGIN-PROOF *) % 27.71/27.93 % SZS output start Proof % 27.71/27.93 1. (-. (lesseq T_0 T_0)) ### Refl(lesseq) % 27.71/27.93 2. (lesseq T_1 T_0) (-. (lesseq T_1 T_0)) ### Axiom % 27.71/27.93 3. (-. ((lesseq T_0 T_0) /\ (lesseq T_1 T_0))) (lesseq T_1 T_0) ### NotAnd 1 2 % 27.71/27.93 4. (-. (ub T_0 T_1 T_0)) (lesseq T_1 T_0) ### Definition-Pseudo(ub) 3 % 27.71/27.93 5. ((max T_0 T_1) = T_0) ((max T_0 T_1) != T_0) ### Axiom % 27.71/27.93 6. ((summation (max T_0 T_1)) != (summation T_0)) ((max T_0 T_1) = T_0) ### NotEqual 5 % 27.71/27.93 7. (T_2 != T_2) ### Refl(=) % 27.71/27.93 8. (-. (lesseq (summation T_0) T_2)) (lesseq (summation (max T_0 T_1)) T_2) ((max T_0 T_1) = T_0) ### P-NotP 6 7 % 27.71/27.93 9. (-. ((ub T_0 T_1 T_0) /\ (lesseq (summation T_0) T_2))) ((max T_0 T_1) = T_0) (lesseq (summation (max T_0 T_1)) T_2) (lesseq T_1 T_0) ### NotAnd 4 8 % 27.71/27.93 10. (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_2)))) (lesseq T_1 T_0) (lesseq (summation (max T_0 T_1)) T_2) ((max T_0 T_1) = T_0) ### NotExists 9 % 27.71/27.93 11. (lesseq T_1 T_0) (-. (lesseq T_1 T_0)) ### Axiom % 27.71/27.93 12. (((max T_0 T_1) = T_0) \/ (-. (lesseq T_1 T_0))) (lesseq (summation (max T_0 T_1)) T_2) (lesseq T_1 T_0) (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_2)))) ### Or 10 11 % 27.71/27.93 13. (All Y, (((max T_0 Y) = T_0) \/ (-. (lesseq Y T_0)))) (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_2)))) (lesseq T_1 T_0) (lesseq (summation (max T_0 T_1)) T_2) ### All 12 % 27.71/27.93 14. (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (lesseq (summation (max T_0 T_1)) T_2) (lesseq T_1 T_0) (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_2)))) ### All 13 % 27.71/27.93 15. (-. (lesseq T_0 T_1)) (lesseq T_0 T_1) ### Axiom % 27.71/27.93 16. ((lesseq T_1 T_0) \/ (lesseq T_0 T_1)) (-. (lesseq T_0 T_1)) (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_2)))) (lesseq (summation (max T_0 T_1)) T_2) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) ### Or 14 15 % 27.71/27.93 17. (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (lesseq (summation (max T_0 T_1)) T_2) (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_2)))) (-. (lesseq T_0 T_1)) ### All 16 % 27.71/27.93 18. (-. (lesseq T_1 T_1)) ### Refl(lesseq) % 27.71/27.93 19. (-. ((lesseq T_0 T_1) /\ (lesseq T_1 T_1))) (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_2)))) (lesseq (summation (max T_0 T_1)) T_2) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) ### NotAnd 17 18 % 27.71/27.93 20. (-. (ub T_0 T_1 T_1)) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (lesseq (summation (max T_0 T_1)) T_2) (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_2)))) ### Definition-Pseudo(ub) 19 % 27.71/27.93 21. (-. (lesseq T_1 T_0)) (lesseq T_1 T_0) ### Axiom % 27.71/27.93 22. ((max T_0 T_1) != T_1) ((max T_0 T_1) = T_1) ### Axiom % 27.71/27.93 23. (lesseq T_0 T_1) (-. (lesseq T_0 T_1)) ### Axiom % 27.71/27.93 24. (((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 22 23 % 27.71/27.93 25. (All Y, (((max T_0 Y) = Y) \/ (-. (lesseq T_0 Y)))) ((max T_0 T_1) != T_1) (lesseq T_0 T_1) ### All 24 % 27.71/27.93 26. (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (lesseq T_0 T_1) ((max T_0 T_1) != T_1) ### All 25 % 27.71/27.93 27. ((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))))) (-. (lesseq T_1 T_0)) ### Or 21 26 % 27.71/27.93 28. (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (-. (lesseq T_1 T_0)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) ((max T_0 T_1) != T_1) ### All 27 % 27.71/27.93 29. ((lesseq T_1 T_0) <=> (lesseq (sum zenon_X3 T_1) (sum zenon_X3 T_0))) (lesseq (summation (max T_0 T_1)) T_2) (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_2)))) (All Y, (((max T_0 Y) = T_0) \/ (-. (lesseq Y T_0)))) ((max T_0 T_1) != T_1) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) ### Equiv 28 13 % 27.71/27.93 30. (All Z, ((lesseq T_1 T_0) <=> (lesseq (sum Z T_1) (sum Z T_0)))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) ((max T_0 T_1) != T_1) (All Y, (((max T_0 Y) = T_0) \/ (-. (lesseq Y T_0)))) (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_2)))) (lesseq (summation (max T_0 T_1)) T_2) ### All 29 % 27.71/27.93 31. (All Y, (All Z, ((lesseq T_1 Y) <=> (lesseq (sum Z T_1) (sum Z Y))))) (lesseq (summation (max T_0 T_1)) T_2) (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_2)))) (All Y, (((max T_0 Y) = T_0) \/ (-. (lesseq Y T_0)))) ((max T_0 T_1) != T_1) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) ### All 30 % 27.71/27.93 32. (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) ((max T_0 T_1) != T_1) (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_2)))) (lesseq (summation (max T_0 T_1)) T_2) (All Y, (All Z, ((lesseq T_1 Y) <=> (lesseq (sum Z T_1) (sum Z Y))))) ### All 31 % 27.71/27.93 33. ((summation (max T_0 T_1)) != (summation T_1)) (All Y, (All Z, ((lesseq T_1 Y) <=> (lesseq (sum Z T_1) (sum Z Y))))) (lesseq (summation (max T_0 T_1)) T_2) (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_2)))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) ### NotEqual 32 % 27.71/27.93 34. (T_2 != T_2) ### Refl(=) % 27.71/27.93 35. (-. (lesseq (summation T_1) T_2)) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_2)))) (lesseq (summation (max T_0 T_1)) T_2) (All Y, (All Z, ((lesseq T_1 Y) <=> (lesseq (sum Z T_1) (sum Z Y))))) ### P-NotP 33 34 % 27.71/27.93 36. (-. ((ub T_0 T_1 T_1) /\ (lesseq (summation T_1) T_2))) (All Y, (All Z, ((lesseq T_1 Y) <=> (lesseq (sum Z T_1) (sum Z Y))))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_2)))) (lesseq (summation (max T_0 T_1)) T_2) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) ### NotAnd 20 35 % 27.71/27.93 37. (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (lesseq (summation (max T_0 T_1)) T_2) (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_2)))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All Y, (All Z, ((lesseq T_1 Y) <=> (lesseq (sum Z T_1) (sum Z Y))))) ### NotExists 36 % 27.71/27.93 38. (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_2)))) (lesseq (summation (max T_0 T_1)) T_2) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) ### All 37 % 27.71/27.93 39. (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (lesseq (summation (max T_0 T_1)) T_2) (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_2)))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) ### All 38 % 27.71/27.93 40. (-. (model_ub T_0 T_1 T_2)) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (lesseq (summation (max 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)))) ### Definition-Pseudo(model_ub) 39 % 27.71/27.93 41. (-. (lesseq (summation (max T_0 T_1)) (summation (max T_0 T_1)))) ### Refl(lesseq) % 27.71/27.93 42. (-. (model_max T_0 T_1 (summation (max T_0 T_1)))) ### Definition-Pseudo(model_max) 41 % 27.71/27.93 43. ((summation T_4) != (summation T_4)) ### Refl(=) % 27.71/27.93 44. (-. (lesseq T_2 T_5)) (lesseq T_2 T_5) ### Axiom % 27.71/27.93 45. (T_5 != T_5) ### Refl(=) % 27.71/27.93 46. (-. (lesseq T_2 (summation (max T_0 T_1)))) (lesseq T_2 (summation (max T_0 T_1))) ### Axiom % 27.71/27.93 47. ((model_max T_0 T_1 (summation (max T_0 T_1))) => (lesseq T_2 (summation (max T_0 T_1)))) (-. (lesseq T_2 (summation (max T_0 T_1)))) ### Imply 42 46 % 27.71/27.93 48. (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (-. (lesseq T_2 (summation (max T_0 T_1)))) ### All 47 % 27.71/27.95 49. (-. (lesseq T_5 (summation (max T_0 T_1)))) (lesseq T_5 T_2) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) ### Trans 45 48 % 27.71/27.95 50. ((lesseq T_2 T_5) \/ (lesseq T_5 T_2)) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (-. (lesseq T_5 (summation (max T_0 T_1)))) (-. (lesseq T_2 T_5)) ### Or 44 49 % 27.71/27.95 51. (All Y, ((lesseq T_2 Y) \/ (lesseq Y T_2))) (-. (lesseq T_2 T_5)) (-. (lesseq T_5 (summation (max T_0 T_1)))) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) ### All 50 % 27.71/27.95 52. (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (-. (lesseq T_5 (summation (max T_0 T_1)))) (-. (lesseq T_2 T_5)) ### All 51 % 27.71/27.95 53. (-. (lesseq (summation T_4) (summation (max T_0 T_1)))) (lesseq (summation T_4) T_5) (-. (lesseq T_2 T_5)) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) ### Trans 43 52 % 27.71/27.95 54. (T_2 != T_2) ### Refl(=) % 27.71/27.95 55. (-. (lesseq (summation T_4) T_2)) (lesseq (summation (max T_0 T_1)) T_2) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (-. (lesseq T_2 T_5)) (lesseq (summation T_4) T_5) ### Trans 53 54 % 27.71/27.95 56. ((max T_0 T_1) != T_0) ((max T_0 T_1) = T_0) ### Axiom % 27.71/27.95 57. (lesseq T_1 T_0) (-. (lesseq T_1 T_0)) ### Axiom % 27.71/27.95 58. (((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 56 57 % 27.71/27.95 59. (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 58 % 27.71/27.95 60. (-. (lesseq T_0 T_1)) (lesseq T_0 T_1) ### Axiom % 27.71/27.95 61. ((lesseq T_1 T_0) \/ (lesseq T_0 T_1)) (-. (lesseq T_0 T_1)) ((max T_0 T_1) != T_0) (All Y, (((max T_0 Y) = T_0) \/ (-. (lesseq Y T_0)))) ### Or 59 60 % 27.71/27.95 62. (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All Y, (((max T_0 Y) = T_0) \/ (-. (lesseq Y T_0)))) ((max T_0 T_1) != T_0) (-. (lesseq T_0 T_1)) ### All 61 % 27.71/27.95 63. ((summation (max T_0 T_1)) != (summation T_0)) (-. (lesseq T_0 T_1)) (All Y, (((max T_0 Y) = T_0) \/ (-. (lesseq Y T_0)))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) ### NotEqual 62 % 27.71/27.95 64. (-. (lesseq (summation T_4) (summation T_0))) (lesseq T_2 (summation (max T_0 T_1))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All Y, (((max T_0 Y) = T_0) \/ (-. (lesseq Y T_0)))) (-. (lesseq T_0 T_1)) (lesseq (summation T_4) T_5) (-. (lesseq T_2 T_5)) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (lesseq (summation (max T_0 T_1)) T_2) ### Trans 55 63 % 27.71/27.95 65. (-. (lesseq T_4 T_0)) (lesseq T_4 T_0) ### Axiom % 27.71/27.95 66. ((lesseq T_4 T_0) <=> (lesseq (summation T_4) (summation T_0))) (-. (lesseq T_4 T_0)) (lesseq (summation (max T_0 T_1)) T_2) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (-. (lesseq T_2 T_5)) (lesseq (summation T_4) T_5) (-. (lesseq T_0 T_1)) (All Y, (((max T_0 Y) = T_0) \/ (-. (lesseq Y T_0)))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (lesseq T_2 (summation (max T_0 T_1))) ### Equiv 64 65 % 27.71/27.95 67. (All Y, ((lesseq T_4 Y) <=> (lesseq (summation T_4) (summation Y)))) (lesseq T_2 (summation (max T_0 T_1))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All Y, (((max T_0 Y) = T_0) \/ (-. (lesseq Y T_0)))) (-. (lesseq T_0 T_1)) (lesseq (summation T_4) T_5) (-. (lesseq T_2 T_5)) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (lesseq (summation (max T_0 T_1)) T_2) (-. (lesseq T_4 T_0)) ### All 66 % 27.71/27.95 68. (lesseq T_1 T_4) (-. (lesseq T_1 T_4)) ### Axiom % 27.71/27.95 69. (T_1 != (max T_0 T_1)) ((max T_0 T_1) = T_1) ### Sym(=) % 27.71/27.95 70. (lesseq T_0 T_1) (-. (lesseq T_0 T_1)) ### Axiom % 27.71/27.95 71. (((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 69 70 % 27.71/27.95 72. (All Y, (((max T_0 Y) = Y) \/ (-. (lesseq T_0 Y)))) (T_1 != (max T_0 T_1)) (lesseq T_0 T_1) ### All 71 % 27.71/27.95 73. ((summation T_1) != (summation (max T_0 T_1))) (lesseq T_0 T_1) (All Y, (((max T_0 Y) = Y) \/ (-. (lesseq T_0 Y)))) ### NotEqual 72 % 27.71/27.95 74. ((summation T_4) != (summation T_4)) ### Refl(=) % 27.71/27.95 75. (-. (lesseq (summation (max T_0 T_1)) (summation T_4))) (lesseq (summation T_1) (summation T_4)) (All Y, (((max T_0 Y) = Y) \/ (-. (lesseq T_0 Y)))) (lesseq T_0 T_1) ### P-NotP 73 74 % 27.71/27.95 76. ((lesseq T_1 T_4) <=> (lesseq (summation T_1) (summation T_4))) (lesseq T_0 T_1) (All Y, (((max T_0 Y) = Y) \/ (-. (lesseq T_0 Y)))) (-. (lesseq (summation (max T_0 T_1)) (summation T_4))) (lesseq T_1 T_4) ### Equiv 68 75 % 27.71/27.95 77. (All Y, ((lesseq T_1 Y) <=> (lesseq (summation T_1) (summation Y)))) (lesseq T_1 T_4) (-. (lesseq (summation (max T_0 T_1)) (summation T_4))) (All Y, (((max T_0 Y) = Y) \/ (-. (lesseq T_0 Y)))) (lesseq T_0 T_1) ### All 76 % 27.71/27.95 78. ((lesseq T_0 T_1) <=> (lesseq (sum zenon_X6 T_0) (sum zenon_X6 T_1))) (All Y, (((max T_0 Y) = Y) \/ (-. (lesseq T_0 Y)))) (-. (lesseq (summation (max T_0 T_1)) (summation T_4))) (lesseq T_1 T_4) (All Y, ((lesseq T_1 Y) <=> (lesseq (summation T_1) (summation Y)))) (-. (lesseq T_4 T_0)) (lesseq (summation (max T_0 T_1)) T_2) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (-. (lesseq T_2 T_5)) (lesseq (summation T_4) T_5) (All Y, (((max T_0 Y) = T_0) \/ (-. (lesseq Y T_0)))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (lesseq T_2 (summation (max T_0 T_1))) (All Y, ((lesseq T_4 Y) <=> (lesseq (summation T_4) (summation Y)))) ### Equiv 67 77 % 27.71/27.95 79. (All Z, ((lesseq T_0 T_1) <=> (lesseq (sum Z T_0) (sum Z T_1)))) (All Y, ((lesseq T_4 Y) <=> (lesseq (summation T_4) (summation Y)))) (lesseq T_2 (summation (max T_0 T_1))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All Y, (((max T_0 Y) = T_0) \/ (-. (lesseq Y T_0)))) (lesseq (summation T_4) T_5) (-. (lesseq T_2 T_5)) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (lesseq (summation (max T_0 T_1)) T_2) (-. (lesseq T_4 T_0)) (All Y, ((lesseq T_1 Y) <=> (lesseq (summation T_1) (summation Y)))) (lesseq T_1 T_4) (-. (lesseq (summation (max T_0 T_1)) (summation T_4))) (All Y, (((max T_0 Y) = Y) \/ (-. (lesseq T_0 Y)))) ### All 78 % 27.71/27.95 80. (All Y, (All Z, ((lesseq T_0 Y) <=> (lesseq (sum Z T_0) (sum Z Y))))) (All Y, (((max T_0 Y) = Y) \/ (-. (lesseq T_0 Y)))) (-. (lesseq (summation (max T_0 T_1)) (summation T_4))) (lesseq T_1 T_4) (All Y, ((lesseq T_1 Y) <=> (lesseq (summation T_1) (summation Y)))) (-. (lesseq T_4 T_0)) (lesseq (summation (max T_0 T_1)) T_2) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (-. (lesseq T_2 T_5)) (lesseq (summation T_4) T_5) (All Y, (((max T_0 Y) = T_0) \/ (-. (lesseq Y T_0)))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (lesseq T_2 (summation (max T_0 T_1))) (All Y, ((lesseq T_4 Y) <=> (lesseq (summation T_4) (summation Y)))) ### All 79 % 27.71/27.95 81. ((model_max T_0 T_1 (summation (max T_0 T_1))) => (lesseq T_2 (summation (max T_0 T_1)))) (All Y, ((lesseq T_4 Y) <=> (lesseq (summation T_4) (summation Y)))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All Y, (((max T_0 Y) = T_0) \/ (-. (lesseq Y T_0)))) (lesseq (summation T_4) T_5) (-. (lesseq T_2 T_5)) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (lesseq (summation (max T_0 T_1)) T_2) (-. (lesseq T_4 T_0)) (All Y, ((lesseq T_1 Y) <=> (lesseq (summation T_1) (summation Y)))) (lesseq T_1 T_4) (-. (lesseq (summation (max T_0 T_1)) (summation T_4))) (All Y, (((max T_0 Y) = Y) \/ (-. (lesseq T_0 Y)))) (All Y, (All Z, ((lesseq T_0 Y) <=> (lesseq (sum Z T_0) (sum Z Y))))) ### Imply 42 80 % 27.71/27.95 82. (All Y, (All Z, ((lesseq T_0 Y) <=> (lesseq (sum Z T_0) (sum Z Y))))) (All Y, (((max T_0 Y) = Y) \/ (-. (lesseq T_0 Y)))) (-. (lesseq (summation (max T_0 T_1)) (summation T_4))) (lesseq T_1 T_4) (All Y, ((lesseq T_1 Y) <=> (lesseq (summation T_1) (summation Y)))) (-. (lesseq T_4 T_0)) (lesseq (summation (max T_0 T_1)) T_2) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (-. (lesseq T_2 T_5)) (lesseq (summation T_4) T_5) (All Y, (((max T_0 Y) = T_0) \/ (-. (lesseq Y T_0)))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All Y, ((lesseq T_4 Y) <=> (lesseq (summation T_4) (summation Y)))) ### All 81 % 27.79/27.97 83. (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All Y, ((lesseq T_4 Y) <=> (lesseq (summation T_4) (summation Y)))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All Y, (((max T_0 Y) = T_0) \/ (-. (lesseq Y T_0)))) (lesseq (summation T_4) T_5) (-. (lesseq T_2 T_5)) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (lesseq (summation (max T_0 T_1)) T_2) (-. (lesseq T_4 T_0)) (lesseq T_1 T_4) (-. (lesseq (summation (max T_0 T_1)) (summation T_4))) (All Y, (((max T_0 Y) = Y) \/ (-. (lesseq T_0 Y)))) (All Y, (All Z, ((lesseq T_0 Y) <=> (lesseq (sum Z T_0) (sum Z Y))))) ### All 82 % 27.79/27.97 84. (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (All Y, (((max T_0 Y) = Y) \/ (-. (lesseq T_0 Y)))) (-. (lesseq (summation (max T_0 T_1)) (summation T_4))) (lesseq T_1 T_4) (-. (lesseq T_4 T_0)) (lesseq (summation (max T_0 T_1)) T_2) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (-. (lesseq T_2 T_5)) (lesseq (summation T_4) T_5) (All Y, (((max T_0 Y) = T_0) \/ (-. (lesseq Y T_0)))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All Y, ((lesseq T_4 Y) <=> (lesseq (summation T_4) (summation Y)))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) ### All 83 % 27.79/27.97 85. (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All Y, ((lesseq T_4 Y) <=> (lesseq (summation T_4) (summation Y)))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (lesseq (summation T_4) T_5) (-. (lesseq T_2 T_5)) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (lesseq (summation (max T_0 T_1)) T_2) (-. (lesseq T_4 T_0)) (lesseq T_1 T_4) (-. (lesseq (summation (max T_0 T_1)) (summation T_4))) (All Y, (((max T_0 Y) = Y) \/ (-. (lesseq T_0 Y)))) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) ### All 84 % 27.79/27.97 86. (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (All Y, (((max T_0 Y) = Y) \/ (-. (lesseq T_0 Y)))) (-. (lesseq (summation (max T_0 T_1)) (summation T_4))) (lesseq T_1 T_4) (-. (lesseq T_4 T_0)) (lesseq (summation (max T_0 T_1)) T_2) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (-. (lesseq T_2 T_5)) (lesseq (summation T_4) T_5) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) ### All 85 % 27.79/27.97 87. (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (lesseq (summation T_4) T_5) (-. (lesseq T_2 T_5)) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (lesseq (summation (max T_0 T_1)) T_2) (-. (lesseq T_4 T_0)) (lesseq T_1 T_4) (-. (lesseq (summation (max T_0 T_1)) (summation T_4))) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) ### All 86 % 27.79/27.97 88. (lesseq T_0 T_4) (-. (lesseq T_0 T_4)) ### Axiom % 27.79/27.97 89. (T_4 != T_4) ### Refl(=) % 27.79/27.97 90. (-. (lesseq T_4 T_4)) ### Refl(lesseq) % 27.79/27.97 91. (T_4 != T_4) ### Refl(=) % 27.79/27.97 92. (T_4 != T_4) ### Refl(=) % 27.79/27.97 93. (T_0 != (max T_0 T_1)) ((max T_0 T_1) = T_0) ### Sym(=) % 27.79/27.97 94. (lesseq T_1 T_0) (-. (lesseq T_1 T_0)) ### Axiom % 27.79/27.97 95. (((max T_0 T_1) = T_0) \/ (-. (lesseq T_1 T_0))) (lesseq T_1 T_0) (T_0 != (max T_0 T_1)) ### Or 93 94 % 27.79/27.97 96. (All Y, (((max T_0 Y) = T_0) \/ (-. (lesseq Y T_0)))) (T_0 != (max T_0 T_1)) (lesseq T_1 T_0) ### All 95 % 27.79/27.97 97. (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (lesseq T_1 T_0) (T_0 != (max T_0 T_1)) ### All 96 % 27.79/27.97 98. (-. (lesseq T_0 T_1)) (lesseq T_0 T_1) ### Axiom % 27.79/27.97 99. ((lesseq T_1 T_0) \/ (lesseq T_0 T_1)) (-. (lesseq T_0 T_1)) (T_0 != (max T_0 T_1)) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) ### Or 97 98 % 27.79/27.97 100. (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (T_0 != (max T_0 T_1)) (-. (lesseq T_0 T_1)) ### All 99 % 27.79/27.97 101. (T_4 != (max T_0 T_1)) (T_4 = T_0) (-. (lesseq T_0 T_1)) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) ### TransEq 91 92 100 % 27.79/27.97 102. (-. (lesseq T_4 T_1)) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (T_4 = T_0) (T_4 != (max T_0 T_1)) ### TransEq 89 90 101 % 27.79/27.97 103. (lesseq T_1 T_4) (-. (lesseq T_1 T_4)) ### Axiom % 27.79/27.97 104. (T_4 != T_4) ### Refl(=) % 27.79/27.97 105. (T_4 != T_4) ### Refl(=) % 27.79/27.97 106. (T_4 != T_4) ### Refl(=) % 27.79/27.97 107. (T_4 != T_4) ### Refl(=) % 27.79/27.97 108. ((lesseq T_1 T_0) \/ (lesseq T_0 T_1)) (T_1 != (max T_0 T_1)) (All Y, (((max T_0 Y) = Y) \/ (-. (lesseq T_0 Y)))) (T_0 != (max T_0 T_1)) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) ### Or 97 72 % 27.79/27.97 109. (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (T_0 != (max T_0 T_1)) (All Y, (((max T_0 Y) = Y) \/ (-. (lesseq T_0 Y)))) (T_1 != (max T_0 T_1)) ### All 108 % 27.79/27.97 110. (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (T_1 != (max T_0 T_1)) (T_0 != (max T_0 T_1)) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) ### All 109 % 27.79/27.97 111. (T_4 != (max T_0 T_1)) (T_4 = T_1) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (T_0 != (max T_0 T_1)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) ### TransEq 106 107 110 % 27.79/27.97 112. (T_4 = T_0) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (T_4 = T_1) (T_4 != (max T_0 T_1)) ### TransEq 104 105 111 % 27.79/27.97 113. (((lesseq T_4 T_1) /\ (lesseq T_1 T_4)) => (T_4 = T_1)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (lesseq T_1 T_4) (T_4 != (max T_0 T_1)) (T_4 = T_0) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) ### DisjTree 102 103 112 % 27.79/27.97 114. (All Y, (((lesseq T_4 Y) /\ (lesseq Y T_4)) => (T_4 = Y))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (T_4 = T_0) (T_4 != (max T_0 T_1)) (lesseq T_1 T_4) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) ### All 113 % 27.79/27.97 115. (((lesseq T_4 T_0) /\ (lesseq T_0 T_4)) => (T_4 = T_0)) (T_4 != (max T_0 T_1)) (All Y, (((lesseq T_4 Y) /\ (lesseq Y T_4)) => (T_4 = Y))) (lesseq T_0 T_4) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (-. (lesseq (summation (max T_0 T_1)) (summation T_4))) (lesseq T_1 T_4) (lesseq (summation (max T_0 T_1)) T_2) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (-. (lesseq T_2 T_5)) (lesseq (summation T_4) T_5) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) ### DisjTree 87 88 114 % 27.79/27.97 116. (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (lesseq (summation T_4) T_5) (-. (lesseq T_2 T_5)) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (lesseq (summation (max T_0 T_1)) T_2) (lesseq T_1 T_4) (-. (lesseq (summation (max T_0 T_1)) (summation T_4))) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (lesseq T_0 T_4) (All Y, (((lesseq T_4 Y) /\ (lesseq Y T_4)) => (T_4 = Y))) (T_4 != (max T_0 T_1)) ### All 115 % 27.79/27.97 117. (T_4 != (max T_0 T_1)) (All Y, (((lesseq T_4 Y) /\ (lesseq Y T_4)) => (T_4 = Y))) (lesseq T_0 T_4) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (-. (lesseq (summation (max T_0 T_1)) (summation T_4))) (lesseq T_1 T_4) (lesseq (summation (max T_0 T_1)) T_2) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (-. (lesseq T_2 T_5)) (lesseq (summation T_4) T_5) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) ### All 116 % 27.79/27.98 118. (T_5 != T_5) ### Refl(=) % 27.79/27.98 119. (-. (lesseq (summation (max T_0 T_1)) T_5)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (lesseq (summation T_4) T_5) (-. (lesseq T_2 T_5)) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (lesseq (summation (max T_0 T_1)) T_2) (lesseq T_1 T_4) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (lesseq T_0 T_4) (All Y, (((lesseq T_4 Y) /\ (lesseq Y T_4)) => (T_4 = Y))) (T_4 != (max T_0 T_1)) ### Trans 117 118 % 27.79/27.98 120. ((summation T_4) != (summation (max T_0 T_1))) (All Y, (((lesseq T_4 Y) /\ (lesseq Y T_4)) => (T_4 = Y))) (lesseq T_0 T_4) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (lesseq T_1 T_4) (lesseq (summation (max T_0 T_1)) T_2) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (-. (lesseq T_2 T_5)) (lesseq (summation T_4) T_5) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (-. (lesseq (summation (max T_0 T_1)) T_5)) ### NotEqual 119 % 27.79/27.98 121. (T_5 != T_5) ### Refl(=) % 27.79/27.98 122. (-. (lesseq (summation (max T_0 T_1)) T_5)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (lesseq (summation T_4) T_5) (-. (lesseq T_2 T_5)) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (lesseq (summation (max T_0 T_1)) T_2) (lesseq T_1 T_4) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (lesseq T_0 T_4) (All Y, (((lesseq T_4 Y) /\ (lesseq Y T_4)) => (T_4 = Y))) ### P-NotP 120 121 % 27.79/27.98 123. (-. (model_max T_0 T_1 T_5)) (All Y, (((lesseq T_4 Y) /\ (lesseq Y T_4)) => (T_4 = Y))) (lesseq T_0 T_4) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (lesseq T_1 T_4) (lesseq (summation (max T_0 T_1)) T_2) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (-. (lesseq T_2 T_5)) (lesseq (summation T_4) T_5) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) ### Definition-Pseudo(model_max) 122 % 27.79/27.98 124. (-. (lesseq T_2 T_5)) (lesseq T_2 T_5) ### Axiom % 27.79/27.98 125. ((model_max T_0 T_1 T_5) => (lesseq T_2 T_5)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (lesseq (summation T_4) T_5) (-. (lesseq T_2 T_5)) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (lesseq (summation (max T_0 T_1)) T_2) (lesseq T_1 T_4) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (lesseq T_0 T_4) (All Y, (((lesseq T_4 Y) /\ (lesseq Y T_4)) => (T_4 = Y))) ### Imply 123 124 % 27.79/27.98 126. (All Y, (((lesseq T_4 Y) /\ (lesseq Y T_4)) => (T_4 = Y))) (lesseq T_0 T_4) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (lesseq T_1 T_4) (lesseq (summation (max T_0 T_1)) T_2) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (-. (lesseq T_2 T_5)) (lesseq (summation T_4) T_5) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) ### All 125 % 27.79/27.98 127. (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (lesseq (summation T_4) T_5) (-. (lesseq T_2 T_5)) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (lesseq (summation (max T_0 T_1)) T_2) (lesseq T_1 T_4) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (lesseq T_0 T_4) ### All 126 % 27.79/27.98 128. ((lesseq T_0 T_4) /\ (lesseq T_1 T_4)) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (lesseq (summation (max T_0 T_1)) T_2) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (-. (lesseq T_2 T_5)) (lesseq (summation T_4) T_5) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (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)) => (X = Y)))) ### And 127 % 27.79/27.98 129. (ub T_0 T_1 T_4) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (lesseq (summation T_4) T_5) (-. (lesseq T_2 T_5)) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (lesseq (summation (max T_0 T_1)) T_2) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) ### Definition-Pseudo(ub) 128 % 27.79/27.98 130. ((ub T_0 T_1 T_4) /\ (lesseq (summation T_4) T_5)) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (lesseq (summation (max T_0 T_1)) T_2) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (-. (lesseq T_2 T_5)) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (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)) => (X = Y)))) ### And 129 % 27.79/27.98 131. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_5))) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (-. (lesseq T_2 T_5)) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (lesseq (summation (max T_0 T_1)) T_2) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) ### Exists 130 % 27.79/27.98 132. (model_ub T_0 T_1 T_5) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (lesseq (summation (max T_0 T_1)) T_2) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (-. (lesseq T_2 T_5)) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (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)) => (X = Y)))) ### Definition-Pseudo(model_ub) 131 % 27.79/27.98 133. (-. ((model_ub T_0 T_1 T_5) => (lesseq T_2 T_5))) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (lesseq (summation (max T_0 T_1)) T_2) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) ### NotImply 132 % 27.79/27.99 134. (-. (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z)))) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (lesseq (summation (max T_0 T_1)) T_2) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (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)) => (X = Y)))) ### NotAllEx 133 % 27.79/27.99 135. (-. ((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, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (lesseq (summation (max T_0 T_1)) T_2) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) ### NotAnd 40 134 % 27.79/27.99 136. (model_max T_0 T_1 T_2) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All Z, ((model_max T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (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) 135 % 27.79/27.99 137. ((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, ((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, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) ### And 136 % 27.79/27.99 138. (minsol_model_max T_0 T_1 T_2) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq 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, (((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) 137 % 27.79/27.99 139. (-. (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, ((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, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (minsol_model_max T_0 T_1 T_2) ### Definition-Pseudo(minsol_model_ub) 138 % 27.79/27.99 140. (lesseq T_0 T_7) (-. (lesseq T_0 T_7)) ### Axiom % 27.79/27.99 141. ((summation T_7) != (summation T_7)) ### Refl(=) % 27.79/27.99 142. (lesseq T_0 T_1) (-. (lesseq T_0 T_1)) ### Axiom % 27.79/27.99 143. (-. (lesseq T_1 T_1)) ### Refl(lesseq) % 27.79/27.99 144. (-. ((lesseq T_0 T_1) /\ (lesseq T_1 T_1))) (lesseq T_0 T_1) ### NotAnd 142 143 % 27.79/27.99 145. (-. (ub T_0 T_1 T_1)) (lesseq T_0 T_1) ### Definition-Pseudo(ub) 144 % 27.79/27.99 146. (-. (lesseq (summation T_1) (summation T_1))) ### Refl(lesseq) % 27.79/27.99 147. (-. ((ub T_0 T_1 T_1) /\ (lesseq (summation T_1) (summation T_1)))) (lesseq T_0 T_1) ### NotAnd 145 146 % 27.79/27.99 148. (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) (summation T_1))))) (lesseq T_0 T_1) ### NotExists 147 % 27.79/27.99 149. (-. (model_ub T_0 T_1 (summation T_1))) (lesseq T_0 T_1) ### Definition-Pseudo(model_ub) 148 % 27.79/27.99 150. (-. (lesseq T_2 (summation T_1))) (lesseq T_2 (summation T_1)) ### Axiom % 27.79/27.99 151. ((model_ub T_0 T_1 (summation T_1)) => (lesseq T_2 (summation T_1))) (-. (lesseq T_2 (summation T_1))) (lesseq T_0 T_1) ### Imply 149 150 % 27.79/27.99 152. (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (lesseq T_0 T_1) (-. (lesseq T_2 (summation T_1))) ### All 151 % 27.79/27.99 153. (-. (lesseq (summation T_7) (summation T_1))) (lesseq (summation T_7) T_2) (lesseq T_0 T_1) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) ### Trans 141 152 % 27.79/27.99 154. (-. (lesseq T_7 T_1)) (lesseq T_7 T_1) ### Axiom % 27.79/27.99 155. ((lesseq T_7 T_1) <=> (lesseq (summation T_7) (summation T_1))) (-. (lesseq T_7 T_1)) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (lesseq T_0 T_1) (lesseq (summation T_7) T_2) ### Equiv 153 154 % 27.79/27.99 156. (All Y, ((lesseq T_7 Y) <=> (lesseq (summation T_7) (summation Y)))) (lesseq (summation T_7) T_2) (lesseq T_0 T_1) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (-. (lesseq T_7 T_1)) ### All 155 % 27.79/27.99 157. ((lesseq T_0 T_1) <=> (lesseq (summation T_0) (summation T_1))) (-. (lesseq T_7 T_1)) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (lesseq (summation T_7) T_2) (All Y, ((lesseq T_7 Y) <=> (lesseq (summation T_7) (summation Y)))) (T_0 != (max T_0 T_1)) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) ### Equiv 100 156 % 27.79/28.00 158. (All Y, ((lesseq T_0 Y) <=> (lesseq (summation T_0) (summation Y)))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (T_0 != (max T_0 T_1)) (All Y, ((lesseq T_7 Y) <=> (lesseq (summation T_7) (summation Y)))) (lesseq (summation T_7) T_2) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (-. (lesseq T_7 T_1)) ### All 157 % 27.79/28.00 159. (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (-. (lesseq T_7 T_1)) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (lesseq (summation T_7) T_2) (All Y, ((lesseq T_7 Y) <=> (lesseq (summation T_7) (summation Y)))) (T_0 != (max T_0 T_1)) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) ### All 158 % 27.79/28.00 160. (lesseq T_1 T_7) (-. (lesseq T_1 T_7)) ### Axiom % 27.79/28.00 161. (T_7 != T_7) ### Refl(=) % 27.79/28.00 162. (T_7 != T_7) ### Refl(=) % 27.79/28.00 163. (T_1 != (max T_0 T_1)) ((max T_0 T_1) = T_1) ### Sym(=) % 27.79/28.00 164. (T_0 != T_0) ### Refl(=) % 27.79/28.00 165. (T_7 = T_1) (T_7 != T_1) ### Axiom % 27.79/28.00 166. (-. (lesseq T_0 T_1)) (lesseq T_0 T_7) (T_7 = T_1) ### Trans 164 165 % 27.79/28.00 167. (((max T_0 T_1) = T_1) \/ (-. (lesseq T_0 T_1))) (T_7 = T_1) (lesseq T_0 T_7) (T_1 != (max T_0 T_1)) ### Or 163 166 % 27.79/28.00 168. (All Y, (((max T_0 Y) = Y) \/ (-. (lesseq T_0 Y)))) (T_1 != (max T_0 T_1)) (lesseq T_0 T_7) (T_7 = T_1) ### All 167 % 27.79/28.00 169. (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (T_7 = T_1) (lesseq T_0 T_7) (T_1 != (max T_0 T_1)) ### All 168 % 27.79/28.00 170. (T_7 != (max T_0 T_1)) (lesseq T_0 T_7) (T_7 = T_1) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) ### TransEq 161 162 169 % 27.79/28.00 171. (((lesseq T_7 T_1) /\ (lesseq T_1 T_7)) => (T_7 = T_1)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (lesseq T_0 T_7) (T_7 != (max T_0 T_1)) (lesseq T_1 T_7) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (T_0 != (max T_0 T_1)) (All Y, ((lesseq T_7 Y) <=> (lesseq (summation T_7) (summation Y)))) (lesseq (summation T_7) T_2) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) ### DisjTree 159 160 170 % 27.79/28.00 172. (All Y, (((lesseq T_7 Y) /\ (lesseq Y T_7)) => (T_7 = Y))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (lesseq (summation T_7) T_2) (All Y, ((lesseq T_7 Y) <=> (lesseq (summation T_7) (summation Y)))) (T_0 != (max T_0 T_1)) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (lesseq T_1 T_7) (T_7 != (max T_0 T_1)) (lesseq T_0 T_7) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) ### All 171 % 27.79/28.00 173. (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (lesseq T_0 T_7) (T_7 != (max T_0 T_1)) (lesseq T_1 T_7) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (T_0 != (max T_0 T_1)) (lesseq (summation T_7) T_2) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All Y, (((lesseq T_7 Y) /\ (lesseq Y T_7)) => (T_7 = Y))) ### All 172 % 27.83/28.01 174. ((summation T_0) != (summation (max T_0 T_1))) (All Y, (((lesseq T_7 Y) /\ (lesseq Y T_7)) => (T_7 = Y))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (lesseq (summation T_7) T_2) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (lesseq T_1 T_7) (T_7 != (max T_0 T_1)) (lesseq T_0 T_7) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) ### NotEqual 173 % 27.83/28.01 175. ((summation T_7) != (summation T_7)) ### Refl(=) % 27.83/28.01 176. (-. (lesseq (summation (max T_0 T_1)) (summation T_7))) (lesseq (summation T_0) (summation T_7)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (lesseq T_0 T_7) (T_7 != (max T_0 T_1)) (lesseq T_1 T_7) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (lesseq (summation T_7) T_2) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All Y, (((lesseq T_7 Y) /\ (lesseq Y T_7)) => (T_7 = Y))) ### P-NotP 174 175 % 27.83/28.01 177. ((lesseq T_0 T_7) <=> (lesseq (summation T_0) (summation T_7))) (All Y, (((lesseq T_7 Y) /\ (lesseq Y T_7)) => (T_7 = Y))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (lesseq (summation T_7) T_2) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (lesseq T_1 T_7) (T_7 != (max T_0 T_1)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (-. (lesseq (summation (max T_0 T_1)) (summation T_7))) (lesseq T_0 T_7) ### Equiv 140 176 % 27.83/28.01 178. (All Y, ((lesseq T_0 Y) <=> (lesseq (summation T_0) (summation Y)))) (lesseq T_0 T_7) (-. (lesseq (summation (max T_0 T_1)) (summation T_7))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (T_7 != (max T_0 T_1)) (lesseq T_1 T_7) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (lesseq (summation T_7) T_2) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All Y, (((lesseq T_7 Y) /\ (lesseq Y T_7)) => (T_7 = Y))) ### All 177 % 27.83/28.01 179. (All Y, (((lesseq T_7 Y) /\ (lesseq Y T_7)) => (T_7 = Y))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (lesseq (summation T_7) T_2) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (lesseq T_1 T_7) (T_7 != (max T_0 T_1)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (-. (lesseq (summation (max T_0 T_1)) (summation T_7))) (lesseq T_0 T_7) ### All 178 % 27.83/28.01 180. (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (lesseq T_0 T_7) (-. (lesseq (summation (max T_0 T_1)) (summation T_7))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (T_7 != (max T_0 T_1)) (lesseq T_1 T_7) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (lesseq (summation T_7) T_2) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All Y, (((lesseq T_7 Y) /\ (lesseq Y T_7)) => (T_7 = Y))) ### All 179 % 27.83/28.01 181. (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (lesseq (summation T_7) T_2) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (lesseq T_1 T_7) (T_7 != (max T_0 T_1)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (-. (lesseq (summation (max T_0 T_1)) (summation T_7))) (lesseq T_0 T_7) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) ### All 180 % 27.83/28.01 182. (T_2 != T_2) ### Refl(=) % 27.83/28.01 183. (-. (lesseq (summation (max T_0 T_1)) T_2)) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (lesseq T_0 T_7) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (T_7 != (max T_0 T_1)) (lesseq T_1 T_7) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (lesseq (summation T_7) T_2) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) ### Trans 181 182 % 27.83/28.01 184. ((summation T_7) != (summation (max T_0 T_1))) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (lesseq (summation T_7) T_2) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (lesseq T_1 T_7) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (lesseq T_0 T_7) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (-. (lesseq (summation (max T_0 T_1)) T_2)) ### NotEqual 183 % 27.83/28.01 185. (T_2 != T_2) ### Refl(=) % 27.83/28.01 186. (-. (lesseq (summation (max T_0 T_1)) T_2)) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (lesseq T_0 T_7) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (lesseq T_1 T_7) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (lesseq (summation T_7) T_2) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) ### P-NotP 184 185 % 27.83/28.01 187. (-. (model_max T_0 T_1 T_2)) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (lesseq (summation T_7) T_2) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (lesseq T_1 T_7) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (lesseq T_0 T_7) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) ### Definition-Pseudo(model_max) 186 % 27.83/28.01 188. (lesseq T_1 T_7) (-. (lesseq T_1 T_7)) ### Axiom % 27.83/28.01 189. (T_8 != T_8) ### Refl(=) % 27.83/28.01 190. (-. (lesseq (summation T_0) T_8)) (lesseq (summation (max T_0 T_1)) T_8) ((max T_0 T_1) = T_0) ### P-NotP 6 189 % 27.83/28.01 191. (lesseq (summation T_0) T_8) (-. (lesseq (summation T_0) T_8)) ### Axiom % 27.83/28.01 192. (-. ((ub T_0 T_1 T_0) /\ (lesseq (summation T_0) T_8))) (lesseq (summation T_0) T_8) (lesseq T_1 T_0) ### NotAnd 4 191 % 27.83/28.01 193. (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_8)))) (lesseq T_1 T_0) (lesseq (summation T_0) T_8) ### NotExists 192 % 27.83/28.01 194. ((lesseq (summation T_0) T_8) <=> (lesseq (sum zenon_X9 (summation T_0)) (sum zenon_X9 T_8))) (lesseq T_1 T_0) (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_8)))) ((max T_0 T_1) = T_0) (lesseq (summation (max T_0 T_1)) T_8) ### Equiv 190 193 % 27.83/28.01 195. (All Z, ((lesseq (summation T_0) T_8) <=> (lesseq (sum Z (summation T_0)) (sum Z T_8)))) (lesseq (summation (max T_0 T_1)) T_8) ((max T_0 T_1) = T_0) (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_8)))) (lesseq T_1 T_0) ### All 194 % 27.83/28.01 196. (All Y, (All Z, ((lesseq (summation T_0) Y) <=> (lesseq (sum Z (summation T_0)) (sum Z Y))))) (lesseq T_1 T_0) (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_8)))) ((max T_0 T_1) = T_0) (lesseq (summation (max T_0 T_1)) T_8) ### All 195 % 27.83/28.01 197. (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (lesseq (summation (max T_0 T_1)) T_8) ((max T_0 T_1) = T_0) (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_8)))) (lesseq T_1 T_0) ### All 196 % 27.83/28.01 198. (lesseq T_1 T_0) (-. (lesseq T_1 T_0)) ### Axiom % 27.83/28.01 199. (((max T_0 T_1) = T_0) \/ (-. (lesseq T_1 T_0))) (lesseq T_1 T_0) (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_8)))) (lesseq (summation (max T_0 T_1)) T_8) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) ### Or 197 198 % 27.83/28.01 200. (All Y, (((max T_0 Y) = T_0) \/ (-. (lesseq Y T_0)))) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (lesseq (summation (max T_0 T_1)) T_8) (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_8)))) (lesseq T_1 T_0) ### All 199 % 27.83/28.03 201. ((lesseq T_1 T_0) \/ (lesseq T_0 T_1)) (-. (lesseq T_2 (summation T_1))) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_8)))) (lesseq (summation (max T_0 T_1)) T_8) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (All Y, (((max T_0 Y) = T_0) \/ (-. (lesseq Y T_0)))) ### Or 200 152 % 27.83/28.03 202. (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All Y, (((max T_0 Y) = T_0) \/ (-. (lesseq Y T_0)))) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (lesseq (summation (max T_0 T_1)) T_8) (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_8)))) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (-. (lesseq T_2 (summation T_1))) ### All 201 % 27.83/28.03 203. (-. (lesseq T_1 T_0)) (lesseq T_1 T_0) ### Axiom % 27.83/28.03 204. (-. (lesseq T_0 T_1)) (lesseq T_0 T_1) ### Axiom % 27.83/28.03 205. ((lesseq T_1 T_0) \/ (lesseq T_0 T_1)) (-. (lesseq T_0 T_1)) (-. (lesseq T_1 T_0)) ### Or 203 204 % 27.83/28.03 206. (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (-. (lesseq T_1 T_0)) (-. (lesseq T_0 T_1)) ### All 205 % 27.83/28.03 207. ((lesseq T_0 T_1) <=> (lesseq (summation T_0) (summation T_1))) (-. (lesseq T_7 T_1)) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (lesseq (summation T_7) T_2) (All Y, ((lesseq T_7 Y) <=> (lesseq (summation T_7) (summation Y)))) (-. (lesseq T_1 T_0)) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) ### Equiv 206 156 % 27.83/28.03 208. (All Y, ((lesseq T_0 Y) <=> (lesseq (summation T_0) (summation Y)))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (-. (lesseq T_1 T_0)) (All Y, ((lesseq T_7 Y) <=> (lesseq (summation T_7) (summation Y)))) (lesseq (summation T_7) T_2) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (-. (lesseq T_7 T_1)) ### All 207 % 27.83/28.03 209. ((lesseq T_1 T_0) <=> (lesseq (sum zenon_X3 T_1) (sum zenon_X3 T_0))) (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_8)))) (lesseq (summation (max T_0 T_1)) T_8) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (All Y, (((max T_0 Y) = T_0) \/ (-. (lesseq Y T_0)))) (-. (lesseq T_7 T_1)) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (lesseq (summation T_7) T_2) (All Y, ((lesseq T_7 Y) <=> (lesseq (summation T_7) (summation Y)))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All Y, ((lesseq T_0 Y) <=> (lesseq (summation T_0) (summation Y)))) ### Equiv 208 200 % 27.83/28.03 210. (All Z, ((lesseq T_1 T_0) <=> (lesseq (sum Z T_1) (sum Z T_0)))) (All Y, ((lesseq T_0 Y) <=> (lesseq (summation T_0) (summation Y)))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All Y, ((lesseq T_7 Y) <=> (lesseq (summation T_7) (summation Y)))) (lesseq (summation T_7) T_2) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (-. (lesseq T_7 T_1)) (All Y, (((max T_0 Y) = T_0) \/ (-. (lesseq Y T_0)))) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (lesseq (summation (max T_0 T_1)) T_8) (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_8)))) ### All 209 % 27.83/28.03 211. (All Y, (All Z, ((lesseq T_1 Y) <=> (lesseq (sum Z T_1) (sum Z Y))))) (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_8)))) (lesseq (summation (max T_0 T_1)) T_8) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (All Y, (((max T_0 Y) = T_0) \/ (-. (lesseq Y T_0)))) (-. (lesseq T_7 T_1)) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (lesseq (summation T_7) T_2) (All Y, ((lesseq T_7 Y) <=> (lesseq (summation T_7) (summation Y)))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All Y, ((lesseq T_0 Y) <=> (lesseq (summation T_0) (summation Y)))) ### All 210 % 27.83/28.03 212. (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All Y, ((lesseq T_0 Y) <=> (lesseq (summation T_0) (summation Y)))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All Y, ((lesseq T_7 Y) <=> (lesseq (summation T_7) (summation Y)))) (lesseq (summation T_7) T_2) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (-. (lesseq T_7 T_1)) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (lesseq (summation (max T_0 T_1)) T_8) (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_8)))) (All Y, (All Z, ((lesseq T_1 Y) <=> (lesseq (sum Z T_1) (sum Z Y))))) ### All 211 % 27.83/28.03 213. (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All Y, (All Z, ((lesseq T_1 Y) <=> (lesseq (sum Z T_1) (sum Z Y))))) (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_8)))) (lesseq (summation (max T_0 T_1)) T_8) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (-. (lesseq T_7 T_1)) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (lesseq (summation T_7) T_2) (All Y, ((lesseq T_7 Y) <=> (lesseq (summation T_7) (summation Y)))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) ### All 212 % 27.83/28.03 214. (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All Y, ((lesseq T_7 Y) <=> (lesseq (summation T_7) (summation Y)))) (lesseq (summation T_7) T_2) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (-. (lesseq T_7 T_1)) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (lesseq (summation (max T_0 T_1)) T_8) (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_8)))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) ### All 213 % 27.83/28.03 215. (lesseq T_1 T_7) (-. (lesseq T_1 T_7)) ### Axiom % 27.83/28.03 216. (((lesseq T_7 T_1) /\ (lesseq T_1 T_7)) => (T_7 = T_1)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (lesseq T_0 T_7) (T_7 != (max T_0 T_1)) (lesseq T_1 T_7) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_8)))) (lesseq (summation (max T_0 T_1)) T_8) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (lesseq (summation T_7) T_2) (All Y, ((lesseq T_7 Y) <=> (lesseq (summation T_7) (summation Y)))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) ### DisjTree 214 215 170 % 27.83/28.03 217. (All Y, (((lesseq T_7 Y) /\ (lesseq Y T_7)) => (T_7 = Y))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All Y, ((lesseq T_7 Y) <=> (lesseq (summation T_7) (summation Y)))) (lesseq (summation T_7) T_2) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (lesseq (summation (max T_0 T_1)) T_8) (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_8)))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (lesseq T_1 T_7) (T_7 != (max T_0 T_1)) (lesseq T_0 T_7) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) ### All 216 % 27.83/28.03 218. (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (lesseq T_0 T_7) (T_7 != (max T_0 T_1)) (lesseq T_1 T_7) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_8)))) (lesseq (summation (max T_0 T_1)) T_8) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (lesseq (summation T_7) T_2) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All Y, (((lesseq T_7 Y) /\ (lesseq Y T_7)) => (T_7 = Y))) ### All 217 % 27.83/28.03 219. ((summation T_7) != (summation (max T_0 T_1))) (All Y, (((lesseq T_7 Y) /\ (lesseq Y T_7)) => (T_7 = Y))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (lesseq (summation T_7) T_2) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (lesseq (summation (max T_0 T_1)) T_8) (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_8)))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (lesseq T_1 T_7) (lesseq T_0 T_7) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) ### NotEqual 218 % 27.83/28.03 220. (-. (lesseq T_2 (summation (max T_0 T_1)))) (lesseq (summation T_1) (summation T_7)) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (lesseq T_0 T_7) (lesseq T_1 T_7) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (lesseq (summation T_7) T_2) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All Y, (((lesseq T_7 Y) /\ (lesseq Y T_7)) => (T_7 = Y))) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_8)))) (lesseq (summation (max T_0 T_1)) T_8) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (All Y, (((max T_0 Y) = T_0) \/ (-. (lesseq Y T_0)))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) ### Trans 202 219 % 27.86/28.04 221. ((lesseq T_1 T_7) <=> (lesseq (summation T_1) (summation T_7))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All Y, (((max T_0 Y) = T_0) \/ (-. (lesseq Y T_0)))) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (lesseq (summation (max T_0 T_1)) T_8) (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_8)))) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (All Y, (((lesseq T_7 Y) /\ (lesseq Y T_7)) => (T_7 = Y))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (lesseq (summation T_7) T_2) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (lesseq T_0 T_7) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (-. (lesseq T_2 (summation (max T_0 T_1)))) (lesseq T_1 T_7) ### Equiv 188 220 % 27.86/28.04 222. (All Y, ((lesseq T_1 Y) <=> (lesseq (summation T_1) (summation Y)))) (lesseq T_1 T_7) (-. (lesseq T_2 (summation (max T_0 T_1)))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (lesseq T_0 T_7) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (lesseq (summation T_7) T_2) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All Y, (((lesseq T_7 Y) /\ (lesseq Y T_7)) => (T_7 = Y))) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_8)))) (lesseq (summation (max T_0 T_1)) T_8) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (All Y, (((max T_0 Y) = T_0) \/ (-. (lesseq Y T_0)))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) ### All 221 % 27.86/28.04 223. (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (lesseq (summation (max T_0 T_1)) T_8) (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_8)))) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (All Y, (((lesseq T_7 Y) /\ (lesseq Y T_7)) => (T_7 = Y))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (lesseq (summation T_7) T_2) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (lesseq T_0 T_7) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (-. (lesseq T_2 (summation (max T_0 T_1)))) (lesseq T_1 T_7) (All Y, ((lesseq T_1 Y) <=> (lesseq (summation T_1) (summation Y)))) ### All 222 % 27.86/28.04 224. (lesseq T_1 T_7) (-. (lesseq T_2 (summation (max T_0 T_1)))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (lesseq T_0 T_7) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (lesseq (summation T_7) T_2) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All Y, (((lesseq T_7 Y) /\ (lesseq Y T_7)) => (T_7 = Y))) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_8)))) (lesseq (summation (max T_0 T_1)) T_8) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (All Y, ((lesseq T_1 Y) \/ (lesseq Y T_1))) ### All 223 % 27.86/28.04 225. (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (lesseq (summation (max T_0 T_1)) T_8) (-. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_8)))) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (All Y, (((lesseq T_7 Y) /\ (lesseq Y T_7)) => (T_7 = Y))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (lesseq (summation T_7) T_2) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (lesseq T_0 T_7) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (-. (lesseq T_2 (summation (max T_0 T_1)))) (lesseq T_1 T_7) ### All 224 % 27.86/28.04 226. (-. (model_ub T_0 T_1 T_8)) (lesseq T_1 T_7) (-. (lesseq T_2 (summation (max T_0 T_1)))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (lesseq T_0 T_7) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (lesseq (summation T_7) T_2) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All Y, (((lesseq T_7 Y) /\ (lesseq Y T_7)) => (T_7 = Y))) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (lesseq (summation (max T_0 T_1)) T_8) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) ### Definition-Pseudo(model_ub) 225 % 27.86/28.04 227. (-. (lesseq T_2 T_8)) (lesseq T_2 T_8) ### Axiom % 27.86/28.04 228. ((model_ub T_0 T_1 T_8) => (lesseq T_2 T_8)) (-. (lesseq T_2 T_8)) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (lesseq (summation (max T_0 T_1)) T_8) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (All Y, (((lesseq T_7 Y) /\ (lesseq Y T_7)) => (T_7 = Y))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (lesseq (summation T_7) T_2) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (lesseq T_0 T_7) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (-. (lesseq T_2 (summation (max T_0 T_1)))) (lesseq T_1 T_7) ### Imply 226 227 % 27.86/28.04 229. (lesseq T_1 T_7) (-. (lesseq T_2 (summation (max T_0 T_1)))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (lesseq T_0 T_7) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (lesseq (summation T_7) T_2) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (All Y, (((lesseq T_7 Y) /\ (lesseq Y T_7)) => (T_7 = Y))) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (lesseq (summation (max T_0 T_1)) T_8) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (-. (lesseq T_2 T_8)) ### All 228 % 27.86/28.04 230. (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (-. (lesseq T_2 T_8)) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (lesseq (summation (max T_0 T_1)) T_8) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (lesseq (summation T_7) T_2) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (lesseq T_0 T_7) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (-. (lesseq T_2 (summation (max T_0 T_1)))) (lesseq T_1 T_7) ### All 229 % 27.86/28.04 231. (T_8 != T_8) ### Refl(=) % 27.86/28.04 232. (lesseq T_1 T_7) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (lesseq T_0 T_7) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (lesseq (summation T_7) 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))) (lesseq (summation (max T_0 T_1)) T_8) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (-. (lesseq T_2 T_8)) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) ### Trans 230 231 % 27.86/28.04 233. (model_max T_0 T_1 T_8) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (-. (lesseq T_2 T_8)) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (lesseq (summation T_7) T_2) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (lesseq T_0 T_7) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (lesseq T_1 T_7) ### Definition-Pseudo(model_max) 232 % 27.86/28.04 234. (-. ((model_max T_0 T_1 T_8) => (lesseq T_2 T_8))) (lesseq T_1 T_7) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (lesseq T_0 T_7) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (lesseq (summation T_7) 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, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) ### NotImply 233 % 27.86/28.05 235. (-. (All Z, ((model_max 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, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (lesseq (summation T_7) T_2) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (lesseq T_0 T_7) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (lesseq T_1 T_7) ### NotAllEx 234 % 27.86/28.05 236. (-. ((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, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (lesseq T_0 T_7) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (lesseq T_1 T_7) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (lesseq (summation T_7) T_2) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) ### NotAnd 187 235 % 27.86/28.05 237. (-. (minsol_model_max T_0 T_1 T_2)) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (lesseq (summation T_7) T_2) (All X, (All Y, (((max X Y) = X) \/ (-. (lesseq Y X))))) (lesseq T_1 T_7) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (lesseq T_0 T_7) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) ### Definition-Pseudo(minsol_model_max) 236 % 27.86/28.05 238. ((lesseq T_0 T_7) /\ (lesseq T_1 T_7)) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (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 (summation T_7) T_2) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (-. (minsol_model_max T_0 T_1 T_2)) ### And 237 % 27.86/28.05 239. (ub T_0 T_1 T_7) (-. (minsol_model_max T_0 T_1 T_2)) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (lesseq (summation T_7) T_2) (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)))) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) ### Definition-Pseudo(ub) 238 % 27.86/28.05 240. ((ub T_0 T_1 T_7) /\ (lesseq (summation T_7) T_2)) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (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))))) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (-. (minsol_model_max T_0 T_1 T_2)) ### And 239 % 27.86/28.05 241. (Ex Z, ((ub T_0 T_1 Z) /\ (lesseq (summation Z) T_2))) (-. (minsol_model_max T_0 T_1 T_2)) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (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 X, (All Y, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, ((lesseq X Y) \/ (lesseq Y X)))) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) ### Exists 240 % 27.86/28.05 242. (model_ub T_0 T_1 T_2) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (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))))) (All Z, ((model_ub T_0 T_1 Z) => (lesseq T_2 Z))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (-. (minsol_model_max T_0 T_1 T_2)) ### Definition-Pseudo(model_ub) 241 % 27.86/28.05 243. ((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, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (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)))) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) ### And 242 % 27.86/28.05 244. (minsol_model_ub T_0 T_1 T_2) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (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))))) (All X, (All Y, ((lesseq X Y) <=> (lesseq (summation X) (summation Y))))) (All X, (All Y, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) (-. (minsol_model_max T_0 T_1 T_2)) ### Definition-Pseudo(minsol_model_ub) 243 % 27.86/28.05 245. (-. ((minsol_model_ub T_0 T_1 T_2) <=> (minsol_model_max T_0 T_1 T_2))) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq 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, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) ### NotEquiv 139 244 % 27.86/28.05 246. (-. (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, ((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, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) ### NotAllEx 245 % 27.86/28.05 247. (-. (All Y, (All Z, ((minsol_model_ub T_0 Y Z) <=> (minsol_model_max T_0 Y Z))))) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) (All X, (All Y, (((max X Y) = Y) \/ (-. (lesseq 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, (((lesseq X Y) /\ (lesseq Y X)) => (X = Y)))) ### NotAllEx 246 % 27.86/28.05 248. (-. (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, ((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, (((max X Y) = Y) \/ (-. (lesseq X Y))))) (All X, (All Y, (All Z, ((lesseq X Y) <=> (lesseq (sum Z X) (sum Z Y)))))) ### NotAllEx 247 % 27.86/28.05 % SZS output end Proof % 27.86/28.05 (* END-PROOF *) %------------------------------------------------------------------------------