%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SWV199+1 : TPTP v8.1.0. Bugfixed v3.3.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n025.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 : Wed Jul 20 21:50:20 EDT 2022 % Result : Theorem 40.75s 40.99s % Output : Proof 41.01s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWV199+1 : TPTP v8.1.0. Bugfixed v3.3.0. % 0.07/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.13/0.34 % Computer : n025.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Wed Jun 15 16:25:10 EDT 2022 % 0.13/0.34 % CPUTime : % 40.75/40.99 % SZS status Theorem % 40.75/40.99 (* PROOF-FOUND *) % 40.75/40.99 (* BEGIN-PROOF *) % 40.75/40.99 % SZS output start Proof % 40.75/40.99 1. (gt (succ T_0) (n0)) (-. (gt (succ T_0) (n0))) ### Axiom % 40.75/40.99 2. (-. (leq (n0) T_0)) (gt (succ T_0) (n0)) ### Definition-Pseudo(leq) 1 % 40.75/40.99 3. ((succ (succ (succ (n0)))) = (n3)) ((n3) != (succ (succ (succ (n0))))) ### Sym(=) % 40.75/40.99 4. ((succ (n3)) != (succ (succ (succ (succ (n0)))))) ((succ (succ (succ (n0)))) = (n3)) ### NotEqual 3 % 40.75/40.99 5. ((n4) != (n4)) ### NotEqual % 40.75/40.99 6. ((succ (succ (succ (succ (n0))))) = (n4)) ((succ (succ (succ (succ (n0))))) != (n4)) ### Axiom % 40.75/40.99 7. ((n3) != (n3)) ### NotEqual % 40.75/40.99 8. (-. (gt (succ (succ (succ (succ (n0))))) (n3))) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) ### Trans 6 7 % 40.75/40.99 9. ((succ (succ (n0))) = (n2)) ((succ (succ (n0))) != (n2)) ### Axiom % 40.75/40.99 10. ((succ (succ (succ (n0)))) != (succ (n2))) ((succ (succ (n0))) = (n2)) ### NotEqual 9 % 40.75/40.99 11. (-. (gt (succ (succ (succ (succ (n0))))) (succ (n2)))) ((succ (succ (succ (n0)))) = (n3)) ((succ (succ (n0))) = (n2)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) ### TransEq2 8 8 10 % 40.75/40.99 12. (-. (gt (n4) (succ (n2)))) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) ((succ (succ (n0))) = (n2)) ((succ (succ (succ (n0)))) = (n3)) ### TransEq2 5 11 11 % 40.75/40.99 13. (-. (gt (succ (n3)) (succ (n2)))) ((succ (succ (n0))) = (n2)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) ((succ (succ (succ (n0)))) = (n3)) ### TransEq 4 12 12 % 40.75/40.99 14. (T_0 != T_0) ### Refl(=) % 40.75/40.99 15. (-. (gt (succ (n3)) T_0)) (gt (succ (n2)) T_0) ((succ (succ (succ (n0)))) = (n3)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) ((succ (succ (n0))) = (n2)) ### Trans 13 14 % 40.75/40.99 16. (-. (leq T_0 (n3))) ((succ (succ (n0))) = (n2)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (n2)) T_0) ### Definition-Pseudo(leq) 15 % 40.75/40.99 17. ((n0) != T_0) (T_0 = (n0)) ### Sym(=) % 40.75/40.99 18. ((n1) != T_0) (T_0 = (n1)) ### Sym(=) % 40.75/40.99 19. ((n2) != T_0) (T_0 = (n2)) ### Sym(=) % 40.75/40.99 20. (T_0 != (n3)) (T_0 = (n3)) ### Axiom % 40.75/40.99 21. (((leq (n0) T_0) /\ (leq T_0 (n3))) => ((T_0 = (n0)) \/ ((T_0 = (n1)) \/ ((T_0 = (n2)) \/ (T_0 = (n3)))))) (T_0 != (n3)) ((n2) != T_0) ((n1) != T_0) ((n0) != T_0) (gt (succ (n2)) T_0) ((succ (succ (succ (n0)))) = (n3)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) ((succ (succ (n0))) = (n2)) (gt (succ T_0) (n0)) ### DisjTree 2 16 17 18 19 20 % 40.75/40.99 22. (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (gt (succ T_0) (n0)) ((succ (succ (n0))) = (n2)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (n2)) T_0) ((n0) != T_0) ((n1) != T_0) ((n2) != T_0) (T_0 != (n3)) ### All 21 % 40.75/40.99 23. ((succ (succ (succ (n0)))) = (n3)) ((succ (succ (succ (n0)))) != (n3)) ### Axiom % 40.75/40.99 24. (-. (gt (succ (succ (succ (n0)))) (n3))) ((n2) != T_0) ((n1) != T_0) ((n0) != T_0) (gt (succ (n2)) T_0) ((succ (succ (succ (n0)))) = (n3)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ T_0) (n0)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((succ (succ (n0))) = (n2)) ### Trans 10 22 % 40.75/40.99 25. ((succ (succ (succ (n0)))) != (succ (succ (succ (n0))))) ### Refl(=) % 40.75/40.99 26. (-. (gt (succ (succ (succ (n0)))) (succ (succ (succ (n0)))))) ((succ (succ (n0))) = (n2)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (gt (succ T_0) (n0)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) (gt (succ (n2)) T_0) ((n0) != T_0) ((n1) != T_0) ((n2) != T_0) ((succ (succ (succ (n0)))) = (n3)) ### TransEq2 23 24 25 % 40.75/40.99 27. ((succ (succ (succ (n0)))) != (succ (succ (succ (n0))))) ### Refl(=) % 40.75/40.99 28. (-. (gt T_0 (succ (succ (succ (n0)))))) ((n2) != T_0) ((n1) != T_0) ((n0) != T_0) (gt (succ (n2)) T_0) ((succ (succ (succ (n0)))) = (n3)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) ((succ (succ (n0))) = (n2)) (gt (succ T_0) (n0)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ### TransEq2 22 26 27 % 40.75/40.99 29. (-. (gt T_0 (n3))) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (gt (succ T_0) (n0)) ((succ (succ (n0))) = (n2)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (n2)) T_0) ((n0) != T_0) ((n1) != T_0) ((n2) != T_0) ### TransEq 28 28 7 % 40.75/40.99 30. (-. (gt T_0 (succ (n2)))) ((n2) != T_0) ((n1) != T_0) ((n0) != T_0) (gt (succ (n2)) T_0) ((succ (succ (succ (n0)))) = (n3)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) ((succ (succ (n0))) = (n2)) (gt (succ T_0) (n0)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ### TransEq2 29 29 10 % 40.75/40.99 31. (T_0 != T_0) ### Refl(=) % 40.75/40.99 32. (-. (gt T_0 T_0)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (gt (succ T_0) (n0)) ((succ (succ (n0))) = (n2)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (n2)) T_0) ((n0) != T_0) ((n1) != T_0) ((n2) != T_0) ### Trans 30 31 % 40.75/40.99 33. (All X, (-. (gt X X))) ((n2) != T_0) ((n1) != T_0) ((n0) != T_0) (gt (succ (n2)) T_0) ((succ (succ (succ (n0)))) = (n3)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) ((succ (succ (n0))) = (n2)) (gt (succ T_0) (n0)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ### All 32 % 40.75/40.99 34. (gt (succ (pv5)) (n0)) (-. (gt (succ (pv5)) (n0))) ### Axiom % 40.75/40.99 35. (-. (leq (n0) (pv5))) (gt (succ (pv5)) (n0)) ### Definition-Pseudo(leq) 34 % 40.75/40.99 36. ((succ (succ (n0))) = (n2)) ((n2) != (succ (succ (n0)))) ### Sym(=) % 40.75/40.99 37. ((succ (n2)) != (succ (succ (succ (n0))))) ((succ (succ (n0))) = (n2)) ### NotEqual 36 % 40.75/40.99 38. ((succ (n0)) = (n1)) ((n1) != (succ (n0))) ### Sym(=) % 40.75/40.99 39. (-. (gt (n3) (succ (n0)))) (gt (n3) (n1)) ((succ (n0)) = (n1)) ### Trans 7 38 % 40.75/40.99 40. (-. (gt (succ (n2)) (succ (n0)))) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) ### TransEq 37 39 39 % 40.75/40.99 41. ((pv5) != (pv5)) ### NotEqual % 40.75/40.99 42. (-. (gt (succ (n2)) (pv5))) (gt (succ (n0)) (pv5)) ((succ (succ (n0))) = (n2)) (gt (n3) (n1)) ((succ (n0)) = (n1)) ((succ (succ (succ (n0)))) = (n3)) ### Trans 40 41 % 40.75/40.99 43. (-. (leq (pv5) (n2))) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) ### Definition-Pseudo(leq) 42 % 40.75/40.99 44. (gt (succ T_1) (n0)) (-. (gt (succ T_1) (n0))) ### Axiom % 40.75/40.99 45. (-. (leq (n0) T_1)) (gt (succ T_1) (n0)) ### Definition-Pseudo(leq) 44 % 40.75/40.99 46. ((succ (succ (succ (n0)))) = (n3)) ((n3) != (succ (succ (succ (n0))))) ### Sym(=) % 40.75/40.99 47. (-. (gt (n4) (succ (succ (succ (n0)))))) (gt (n4) (n3)) ((succ (succ (succ (n0)))) = (n3)) ### Trans 5 46 % 40.75/40.99 48. (-. (gt (succ (n3)) (succ (succ (succ (n0)))))) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) ((succ (succ (succ (n0)))) = (n3)) ### TransEq 4 47 47 % 40.75/40.99 49. ((n2) != (n2)) ### NotEqual % 40.75/40.99 50. ((succ (succ (n0))) = (n2)) ((succ (succ (n0))) != (n2)) ### Axiom % 40.75/40.99 51. ((n1) != (n1)) ### NotEqual % 40.75/40.99 52. (-. (gt (succ (succ (n0))) (n1))) (gt (n2) (n1)) ((succ (succ (n0))) = (n2)) ### Trans 50 51 % 40.75/40.99 53. ((n0) != (pv5)) ((pv5) = (n0)) ### Sym(=) % 40.75/40.99 54. ((pv5) != (n1)) ((pv5) = (n1)) ### Axiom % 40.75/40.99 55. ((pv5) != (n2)) ((pv5) = (n2)) ### Axiom % 40.75/40.99 56. (((leq (n0) (pv5)) /\ (leq (pv5) (n2))) => (((pv5) = (n0)) \/ (((pv5) = (n1)) \/ ((pv5) = (n2))))) ((pv5) != (n2)) ((pv5) != (n1)) ((n0) != (pv5)) (gt (succ (n0)) (pv5)) ((succ (succ (n0))) = (n2)) (gt (n3) (n1)) ((succ (n0)) = (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) ### DisjTree 35 43 53 54 55 % 40.75/40.99 57. (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) ((n0) != (pv5)) ((pv5) != (n1)) ((pv5) != (n2)) ### All 56 % 40.75/40.99 58. ((succ (n0)) != (succ (pv5))) ((pv5) != (n2)) ((pv5) != (n1)) (gt (succ (n0)) (pv5)) ((succ (succ (n0))) = (n2)) (gt (n3) (n1)) ((succ (n0)) = (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) ### NotEqual 57 % 40.75/41.00 59. (-. (gt (succ (succ (n0))) (succ (pv5)))) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) (gt (succ (n0)) (pv5)) ((pv5) != (n1)) ((pv5) != (n2)) ((succ (succ (n0))) = (n2)) (gt (n2) (n1)) ### TransEq2 52 52 58 % 40.75/41.00 60. (-. (gt (n2) (succ (pv5)))) (gt (n2) (n1)) ((succ (succ (n0))) = (n2)) ((pv5) != (n2)) ((pv5) != (n1)) (gt (succ (n0)) (pv5)) (gt (n3) (n1)) ((succ (n0)) = (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) ### TransEq2 49 59 59 % 40.75/41.00 61. (-. (gt (n3) (succ (pv5)))) (gt (n3) (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) (gt (succ (n0)) (pv5)) ((pv5) != (n1)) ((pv5) != (n2)) ((succ (succ (n0))) = (n2)) (gt (n2) (n1)) ### Trans 7 60 % 40.75/41.00 62. (-. (gt (succ (n3)) (succ (pv5)))) (gt (n2) (n1)) ((succ (succ (n0))) = (n2)) ((pv5) != (n2)) ((pv5) != (n1)) (gt (succ (n0)) (pv5)) (gt (n3) (n1)) ((succ (n0)) = (n1)) (gt (succ (pv5)) (n0)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n3) (n2)) ((succ (succ (succ (n0)))) = (n3)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) ### TransEq 48 61 61 % 40.75/41.00 63. (T_1 != T_1) ### Refl(=) % 40.75/41.00 64. (-. (gt (succ (n3)) T_1)) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) ((succ (succ (succ (n0)))) = (n3)) (gt (n3) (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (succ (pv5)) (n0)) ((succ (n0)) = (n1)) (gt (n3) (n1)) (gt (succ (n0)) (pv5)) ((pv5) != (n1)) ((pv5) != (n2)) ((succ (succ (n0))) = (n2)) (gt (n2) (n1)) ### Trans 62 63 % 40.75/41.00 65. (-. (leq T_1 (n3))) (gt (n2) (n1)) ((succ (succ (n0))) = (n2)) ((pv5) != (n2)) ((pv5) != (n1)) (gt (succ (n0)) (pv5)) (gt (n3) (n1)) ((succ (n0)) = (n1)) (gt (succ (pv5)) (n0)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n3) (n2)) ((succ (succ (succ (n0)))) = (n3)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) ### Definition-Pseudo(leq) 64 % 40.75/41.00 66. (T_1 = (n0)) (T_1 != (n0)) ### Axiom % 40.75/41.00 67. ((n0) != T_1) (T_1 = (n0)) ### Sym(=) % 40.75/41.00 68. (T_1 != (n1)) (T_1 = (n1)) ### Axiom % 40.75/41.00 69. (T_1 != (n2)) (T_1 = (n2)) ### Axiom % 40.75/41.00 70. (T_1 != (n3)) (T_1 = (n3)) ### Axiom % 40.75/41.00 71. (((leq (n0) T_1) /\ (leq T_1 (n3))) => ((T_1 = (n0)) \/ ((T_1 = (n1)) \/ ((T_1 = (n2)) \/ (T_1 = (n3)))))) (T_1 != (n3)) (T_1 != (n2)) (T_1 != (n1)) ((n0) != T_1) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) ((succ (succ (succ (n0)))) = (n3)) (gt (n3) (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (succ (pv5)) (n0)) ((succ (n0)) = (n1)) (gt (n3) (n1)) (gt (succ (n0)) (pv5)) ((pv5) != (n1)) ((pv5) != (n2)) ((succ (succ (n0))) = (n2)) (gt (n2) (n1)) (gt (succ T_1) (n0)) ### DisjTree 45 65 67 68 69 70 % 40.75/41.00 72. (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (gt (succ T_1) (n0)) (gt (n2) (n1)) ((succ (succ (n0))) = (n2)) ((pv5) != (n2)) ((pv5) != (n1)) (gt (succ (n0)) (pv5)) (gt (n3) (n1)) ((succ (n0)) = (n1)) (gt (succ (pv5)) (n0)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n3) (n2)) ((succ (succ (succ (n0)))) = (n3)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) ((n0) != T_1) (T_1 != (n1)) (T_1 != (n2)) (T_1 != (n3)) ### All 71 % 40.75/41.00 73. ((succ (n0)) != (succ T_1)) (T_1 != (n3)) (T_1 != (n2)) (T_1 != (n1)) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) ((succ (succ (succ (n0)))) = (n3)) (gt (n3) (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (succ (pv5)) (n0)) ((succ (n0)) = (n1)) (gt (n3) (n1)) (gt (succ (n0)) (pv5)) ((pv5) != (n1)) ((pv5) != (n2)) ((succ (succ (n0))) = (n2)) (gt (n2) (n1)) (gt (succ T_1) (n0)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ### NotEqual 72 % 40.75/41.00 74. (-. (gt (succ T_1) (pv5))) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (gt (succ T_1) (n0)) (gt (n2) (n1)) ((succ (succ (n0))) = (n2)) ((pv5) != (n2)) ((pv5) != (n1)) (gt (succ (n0)) (pv5)) (gt (n3) (n1)) ((succ (n0)) = (n1)) (gt (succ (pv5)) (n0)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n3) (n2)) ((succ (succ (succ (n0)))) = (n3)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (T_1 != (n1)) (T_1 != (n2)) (T_1 != (n3)) ### P-NotP 73 41 % 40.75/41.00 75. (-. (leq (pv5) T_1)) (T_1 != (n3)) (T_1 != (n2)) (T_1 != (n1)) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) ((succ (succ (succ (n0)))) = (n3)) (gt (n3) (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (succ (pv5)) (n0)) ((succ (n0)) = (n1)) (gt (n3) (n1)) (gt (succ (n0)) (pv5)) ((pv5) != (n1)) ((pv5) != (n2)) ((succ (succ (n0))) = (n2)) (gt (n2) (n1)) (gt (succ T_1) (n0)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ### Definition-Pseudo(leq) 74 % 40.75/41.00 76. ((pv5) != T_1) ((pv5) = T_1) ### Axiom % 40.75/41.00 77. (-. (gt T_1 (pv5))) (gt T_1 (pv5)) ### Axiom % 40.75/41.00 78. (((leq (pv5) T_1) /\ ((pv5) != T_1)) => (gt T_1 (pv5))) (-. (gt T_1 (pv5))) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (gt (succ T_1) (n0)) (gt (n2) (n1)) ((succ (succ (n0))) = (n2)) ((pv5) != (n2)) ((pv5) != (n1)) (gt (succ (n0)) (pv5)) (gt (n3) (n1)) ((succ (n0)) = (n1)) (gt (succ (pv5)) (n0)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n3) (n2)) ((succ (succ (succ (n0)))) = (n3)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (T_1 != (n1)) (T_1 != (n2)) (T_1 != (n3)) ### DisjTree 75 76 77 % 40.75/41.00 79. (All Y, (((leq (pv5) Y) /\ ((pv5) != Y)) => (gt Y (pv5)))) (T_1 != (n3)) (T_1 != (n2)) (T_1 != (n1)) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) ((succ (succ (succ (n0)))) = (n3)) (gt (n3) (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (succ (pv5)) (n0)) ((succ (n0)) = (n1)) (gt (n3) (n1)) (gt (succ (n0)) (pv5)) ((pv5) != (n1)) ((pv5) != (n2)) ((succ (succ (n0))) = (n2)) (gt (n2) (n1)) (gt (succ T_1) (n0)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) (-. (gt T_1 (pv5))) ### All 78 % 40.75/41.00 80. ((n0) != (n0)) ### NotEqual % 40.75/41.00 81. (-. (gt T_1 (n0))) ((pv5) = (n0)) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (gt (succ T_1) (n0)) (gt (n2) (n1)) ((succ (succ (n0))) = (n2)) ((pv5) != (n2)) ((pv5) != (n1)) (gt (succ (n0)) (pv5)) (gt (n3) (n1)) ((succ (n0)) = (n1)) (gt (succ (pv5)) (n0)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n3) (n2)) ((succ (succ (succ (n0)))) = (n3)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (T_1 != (n1)) (T_1 != (n2)) (T_1 != (n3)) (All Y, (((leq (pv5) Y) /\ ((pv5) != Y)) => (gt Y (pv5)))) ### TransEq 79 79 80 % 40.75/41.00 82. (T_1 != T_1) ### Refl(=) % 40.75/41.00 83. (-. (gt T_1 T_1)) (All Y, (((leq (pv5) Y) /\ ((pv5) != Y)) => (gt Y (pv5)))) (T_1 != (n3)) (T_1 != (n2)) (T_1 != (n1)) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) ((succ (succ (succ (n0)))) = (n3)) (gt (n3) (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (succ (pv5)) (n0)) ((succ (n0)) = (n1)) (gt (n3) (n1)) (gt (succ (n0)) (pv5)) ((pv5) != (n1)) ((pv5) != (n2)) ((succ (succ (n0))) = (n2)) (gt (n2) (n1)) (gt (succ T_1) (n0)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) ((pv5) = (n0)) (T_1 = (n0)) ### TransEq2 66 81 82 % 41.01/41.20 84. (T_1 != (n1)) (T_1 = (n1)) ### Axiom % 41.01/41.20 85. (T_1 != (n2)) (T_1 = (n2)) ### Axiom % 41.01/41.20 86. (T_1 != (n3)) (T_1 = (n3)) ### Axiom % 41.01/41.20 87. (((leq (n0) T_1) /\ (leq T_1 (n3))) => ((T_1 = (n0)) \/ ((T_1 = (n1)) \/ ((T_1 = (n2)) \/ (T_1 = (n3)))))) ((pv5) = (n0)) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (T_1 != (n1)) (T_1 != (n2)) (T_1 != (n3)) (All Y, (((leq (pv5) Y) /\ ((pv5) != Y)) => (gt Y (pv5)))) (-. (gt T_1 T_1)) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) ((succ (succ (succ (n0)))) = (n3)) (gt (n3) (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (succ (pv5)) (n0)) ((succ (n0)) = (n1)) (gt (n3) (n1)) (gt (succ (n0)) (pv5)) ((pv5) != (n1)) ((pv5) != (n2)) ((succ (succ (n0))) = (n2)) (gt (n2) (n1)) (gt (succ T_1) (n0)) ### DisjTree 45 65 83 84 85 86 % 41.01/41.20 88. (gt (succ T_1) (n0)) (gt (n2) (n1)) ((succ (succ (n0))) = (n2)) ((pv5) != (n2)) ((pv5) != (n1)) (gt (succ (n0)) (pv5)) (gt (n3) (n1)) ((succ (n0)) = (n1)) (gt (succ (pv5)) (n0)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n3) (n2)) ((succ (succ (succ (n0)))) = (n3)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (-. (gt T_1 T_1)) (All Y, (((leq (pv5) Y) /\ ((pv5) != Y)) => (gt Y (pv5)))) (T_1 != (n3)) (T_1 != (n2)) (T_1 != (n1)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) ((pv5) = (n0)) ### All 87 % 41.01/41.20 89. ((pv5) != (n1)) ((pv5) = (n1)) ### Axiom % 41.01/41.20 90. ((pv5) != (n2)) ((pv5) = (n2)) ### Axiom % 41.01/41.20 91. (((leq (n0) (pv5)) /\ (leq (pv5) (n2))) => (((pv5) = (n0)) \/ (((pv5) = (n1)) \/ ((pv5) = (n2))))) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (T_1 != (n1)) (T_1 != (n2)) (T_1 != (n3)) (All Y, (((leq (pv5) Y) /\ ((pv5) != Y)) => (gt Y (pv5)))) (-. (gt T_1 T_1)) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) (gt (n3) (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) ((pv5) != (n1)) ((pv5) != (n2)) (gt (n2) (n1)) (gt (succ T_1) (n0)) (gt (succ (n0)) (pv5)) ((succ (succ (n0))) = (n2)) (gt (n3) (n1)) ((succ (n0)) = (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) ### DisjTree 35 43 88 89 90 % 41.01/41.20 92. (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) (gt (succ T_1) (n0)) (gt (n2) (n1)) ((pv5) != (n2)) ((pv5) != (n1)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n3) (n2)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (-. (gt T_1 T_1)) (All Y, (((leq (pv5) Y) /\ ((pv5) != Y)) => (gt Y (pv5)))) (T_1 != (n3)) (T_1 != (n2)) (T_1 != (n1)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) ### All 91 % 41.01/41.20 93. (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (T_1 != (n1)) (T_1 != (n2)) (T_1 != (n3)) (-. (gt T_1 T_1)) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) (gt (n3) (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) ((pv5) != (n1)) ((pv5) != (n2)) (gt (n2) (n1)) (gt (succ T_1) (n0)) (gt (succ (n0)) (pv5)) ((succ (succ (n0))) = (n2)) (gt (n3) (n1)) ((succ (n0)) = (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) ### All 92 % 41.01/41.20 94. (All X, (-. (gt X X))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) (gt (succ T_1) (n0)) (gt (n2) (n1)) ((pv5) != (n2)) ((pv5) != (n1)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n3) (n2)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (T_1 != (n3)) (T_1 != (n2)) (T_1 != (n1)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ### All 93 % 41.01/41.20 95. ((succ (n0)) = (n1)) ((succ (n0)) != (n1)) ### Axiom % 41.01/41.20 96. (-. (gt (succ (n0)) (n1))) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (T_1 != (n2)) (T_1 != (n3)) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) (gt (n3) (n2)) (gt (n2) (n1)) (gt (succ T_1) (n0)) (All X, (-. (gt X X))) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) ((pv5) != (n1)) ((pv5) != (n2)) ### Trans 58 94 % 41.01/41.20 97. ((succ (n0)) != (succ (n0))) ### Refl(=) % 41.01/41.20 98. (-. (gt (succ (n0)) (succ (n0)))) ((pv5) != (n2)) ((pv5) != (n1)) (gt (succ (n0)) (pv5)) ((succ (succ (n0))) = (n2)) (gt (n3) (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (All X, (-. (gt X X))) (gt (succ T_1) (n0)) (gt (n2) (n1)) (gt (n3) (n2)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (T_1 != (n3)) (T_1 != (n2)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((succ (n0)) = (n1)) ### TransEq2 95 96 97 % 41.01/41.20 99. ((succ (n0)) != (succ (n0))) ### Refl(=) % 41.01/41.20 100. (-. (gt T_1 (succ (n0)))) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (T_1 != (n2)) (T_1 != (n3)) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) (gt (n3) (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) ((pv5) != (n1)) ((pv5) != (n2)) (gt (n2) (n1)) (gt (succ T_1) (n0)) (gt (succ (n0)) (pv5)) ((succ (succ (n0))) = (n2)) (gt (n3) (n1)) ((succ (n0)) = (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) (All X, (-. (gt X X))) ### TransEq2 94 98 99 % 41.01/41.20 101. ((succ (n0)) = (n1)) ((succ (n0)) != (n1)) ### Axiom % 41.01/41.20 102. ((succ (n0)) != (succ (n0))) ### Refl(=) % 41.01/41.20 103. ((pv5) != (n2)) (gt (succ (n0)) (pv5)) ((succ (succ (n0))) = (n2)) (gt (n3) (n1)) ((succ (n0)) = (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (All X, (-. (gt X X))) (gt (succ T_1) (n0)) (gt (n2) (n1)) (gt (n3) (n2)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (T_1 != (n3)) (T_1 != (n2)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) (-. (gt (succ (n0)) (n1))) ### Trans 102 96 % 41.01/41.20 104. ((succ (n0)) != (succ (n0))) ### Refl(=) % 41.01/41.20 105. (-. (gt (succ (n0)) (succ (n0)))) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (T_1 != (n2)) (T_1 != (n3)) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) (gt (n3) (n2)) (gt (n2) (n1)) (gt (succ T_1) (n0)) (All X, (-. (gt X X))) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) ((pv5) != (n2)) ((succ (n0)) = (n1)) ### TransEq2 101 103 104 % 41.01/41.21 106. ((succ (n0)) != (succ (n0))) ### Refl(=) % 41.01/41.21 107. (-. (gt (pv5) (succ (n0)))) (All X, (-. (gt X X))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) (gt (succ T_1) (n0)) (gt (n2) (n1)) ((pv5) != (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n3) (n2)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (T_1 != (n3)) (T_1 != (n2)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) (-. (gt T_1 (succ (n0)))) ### TransEq2 100 105 106 % 41.01/41.21 108. ((succ (n0)) = (n1)) ((succ (n0)) != (n1)) ### Axiom % 41.01/41.21 109. (-. (gt (n1) (n1))) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (T_1 != (n2)) (T_1 != (n3)) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) (gt (n3) (n2)) (gt (n2) (n1)) (gt (succ T_1) (n0)) (All X, (-. (gt X X))) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) ((pv5) != (n2)) ### TransEq2 51 103 108 % 41.01/41.21 110. (-. (gt T_1 (n1))) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (T_1 != (n2)) (T_1 != (n3)) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) (gt (n3) (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) ((pv5) != (n2)) (gt (n2) (n1)) (gt (succ T_1) (n0)) (gt (succ (n0)) (pv5)) ((succ (succ (n0))) = (n2)) (gt (n3) (n1)) ((succ (n0)) = (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) (All X, (-. (gt X X))) (-. (gt (pv5) (succ (n0)))) ### TransEq 107 107 109 % 41.01/41.21 111. ((succ (n0)) != (succ (n0))) ### Refl(=) % 41.01/41.21 112. (-. (gt (pv5) (succ (n0)))) (All X, (-. (gt X X))) (gt (succ T_1) (n0)) (gt (n2) (n1)) (gt (n3) (n2)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (T_1 != (n3)) (T_1 != (n2)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != (n2)) ((n0) != (pv5)) (gt (succ (n0)) (pv5)) ((succ (succ (n0))) = (n2)) (gt (n3) (n1)) ((succ (n0)) = (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) ### TransEq2 57 105 111 % 41.01/41.21 113. ((succ (n0)) != (succ (pv5))) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) ((pv5) != (n2)) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (T_1 != (n2)) (T_1 != (n3)) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) (gt (n3) (n2)) (gt (n2) (n1)) (gt (succ T_1) (n0)) (All X, (-. (gt X X))) (-. (gt (pv5) (succ (n0)))) ### NotEqual 112 % 41.01/41.21 114. (-. (gt T_1 (succ (pv5)))) (-. (gt (pv5) (succ (n0)))) (All X, (-. (gt X X))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) (gt (succ T_1) (n0)) (gt (n2) (n1)) ((pv5) != (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n3) (n2)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (T_1 != (n3)) (T_1 != (n2)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ### TransEq2 110 110 113 % 41.01/41.21 115. ((pv5) != (n1)) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (T_1 != (n3)) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) (gt (n3) (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) ((pv5) != (n2)) (gt (n2) (n1)) (gt (succ T_1) (n0)) (gt (succ (n0)) (pv5)) ((succ (succ (n0))) = (n2)) (gt (n3) (n1)) ((succ (n0)) = (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) (All X, (-. (gt X X))) (-. (gt (pv5) (succ (n0)))) (-. (gt T_1 (succ (pv5)))) ### TransEq2 114 59 59 % 41.01/41.21 116. (T_1 != T_1) ### Refl(=) % 41.01/41.21 117. (-. (gt T_1 T_1)) (-. (gt (pv5) (succ (n0)))) (All X, (-. (gt X X))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) (gt (succ T_1) (n0)) (gt (n2) (n1)) ((pv5) != (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n3) (n2)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (T_1 != (n3)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != (n1)) ### Trans 115 116 % 41.01/41.21 118. ((pv5) != (n1)) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (T_1 != (n3)) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) (gt (n3) (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) ((pv5) != (n2)) (gt (n2) (n1)) (gt (succ T_1) (n0)) (gt (succ (n0)) (pv5)) ((succ (succ (n0))) = (n2)) (gt (n3) (n1)) ((succ (n0)) = (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) (All X, (-. (gt X X))) (-. (gt (pv5) (succ (n0)))) ### All 117 % 41.01/41.21 119. (-. (gt T_1 (n1))) (All X, (-. (gt X X))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) (gt (succ T_1) (n0)) (gt (n2) (n1)) ((pv5) != (n2)) ((pv5) != (n1)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n3) (n2)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (T_1 != (n3)) (T_1 != (n2)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ### TransEq 100 100 51 % 41.01/41.21 120. ((succ (n0)) = (n1)) ((succ (n0)) != (n1)) ### Axiom % 41.01/41.21 121. (-. (gt (succ (n0)) (succ (pv5)))) ((pv5) != (n2)) ((pv5) != (n1)) (gt (succ (n0)) (pv5)) ((succ (succ (n0))) = (n2)) (gt (n3) (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (All X, (-. (gt X X))) (gt (succ T_1) (n0)) (gt (n2) (n1)) (gt (n3) (n2)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (T_1 != (n3)) (T_1 != (n2)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((succ (n0)) = (n1)) ### TransEq2 120 96 58 % 41.01/41.21 122. (-. (gt T_1 (succ (pv5)))) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (T_1 != (n2)) (T_1 != (n3)) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) (gt (n3) (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) ((pv5) != (n1)) ((pv5) != (n2)) (gt (n2) (n1)) (gt (succ T_1) (n0)) (gt (succ (n0)) (pv5)) ((succ (succ (n0))) = (n2)) (gt (n3) (n1)) ((succ (n0)) = (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) (All X, (-. (gt X X))) ### TransEq2 119 119 121 % 41.01/41.23 123. (T_1 != T_1) ### Refl(=) % 41.01/41.23 124. (-. (gt T_1 T_1)) (All X, (-. (gt X X))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) (gt (succ T_1) (n0)) (gt (n2) (n1)) ((pv5) != (n2)) ((pv5) != (n1)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n3) (n2)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (T_1 != (n3)) (T_1 != (n2)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ### Trans 122 123 % 41.01/41.23 125. (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (T_1 != (n2)) (T_1 != (n3)) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) (gt (n3) (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) ((pv5) != (n1)) ((pv5) != (n2)) (gt (n2) (n1)) (gt (succ T_1) (n0)) (gt (succ (n0)) (pv5)) ((succ (succ (n0))) = (n2)) (gt (n3) (n1)) ((succ (n0)) = (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) (All X, (-. (gt X X))) ### All 124 % 41.01/41.23 126. ((succ (n0)) != (succ (n0))) ### Refl(=) % 41.01/41.23 127. (-. (gt (pv5) (succ (n0)))) (All X, (-. (gt X X))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) (gt (succ T_1) (n0)) (gt (n2) (n1)) ((pv5) != (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n3) (n2)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (T_1 != (n3)) (T_1 != (n2)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ### TransEq2 125 105 126 % 41.01/41.23 128. (-. (gt (pv5) (pv5))) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (T_1 != (n2)) (T_1 != (n3)) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) (gt (n3) (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) ((pv5) != (n2)) (gt (n2) (n1)) (gt (succ T_1) (n0)) (gt (succ (n0)) (pv5)) ((succ (succ (n0))) = (n2)) (gt (n3) (n1)) ((succ (n0)) = (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) (All X, (-. (gt X X))) ### Trans 127 41 % 41.01/41.23 129. (All X, (-. (gt X X))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) (gt (succ T_1) (n0)) (gt (n2) (n1)) ((pv5) != (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n3) (n2)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (T_1 != (n3)) (T_1 != (n2)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ### All 128 % 41.01/41.23 130. (-. (gt (succ (n0)) (n2))) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (T_1 != (n3)) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) (gt (n3) (n2)) (gt (n2) (n1)) (gt (succ T_1) (n0)) (All X, (-. (gt X X))) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) ((pv5) != (n1)) ((pv5) != (n2)) ### Trans 58 129 % 41.01/41.23 131. (-. (gt (n1) (n2))) ((pv5) != (n2)) ((pv5) != (n1)) (gt (succ (n0)) (pv5)) ((succ (succ (n0))) = (n2)) (gt (n3) (n1)) ((succ (n0)) = (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (All X, (-. (gt X X))) (gt (succ T_1) (n0)) (gt (n2) (n1)) (gt (n3) (n2)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (T_1 != (n3)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ### TransEq2 51 130 130 % 41.01/41.23 132. (-. (gt (n1) (n1))) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (T_1 != (n3)) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) (gt (n3) (n2)) (gt (n2) (n1)) (gt (succ T_1) (n0)) (All X, (-. (gt X X))) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) ((pv5) != (n1)) ((pv5) != (n2)) ### Trans 131 51 % 41.01/41.23 133. (-. (gt (pv5) (n1))) (All X, (-. (gt X X))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) (gt (succ T_1) (n0)) (gt (n2) (n1)) ((pv5) != (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n3) (n2)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (T_1 != (n3)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != (n1)) ### TransEq 118 118 132 % 41.01/41.23 134. ((succ (n0)) = (n1)) ((succ (n0)) != (n1)) ### Axiom % 41.01/41.23 135. ((succ (n0)) != (succ (n0))) ### Refl(=) % 41.01/41.23 136. ((succ (n0)) != (succ (n0))) ### Refl(=) % 41.01/41.23 137. (-. (gt (succ (n0)) (succ (n0)))) (All X, (-. (gt X X))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) (gt (succ T_1) (n0)) (gt (n2) (n1)) ((pv5) != (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n3) (n2)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (T_1 != (n3)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != (n1)) ### Trans 136 118 % 41.01/41.23 138. (-. (gt (succ (n0)) (n1))) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (T_1 != (n3)) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) (gt (n3) (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) ((pv5) != (n2)) (gt (n2) (n1)) (gt (succ T_1) (n0)) (gt (succ (n0)) (pv5)) ((succ (succ (n0))) = (n2)) (gt (n3) (n1)) ((succ (n0)) = (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) (All X, (-. (gt X X))) (-. (gt (succ (n0)) (succ (n0)))) ### Trans 135 137 % 41.01/41.23 139. ((succ (n0)) != (succ (n0))) ### Refl(=) % 41.01/41.23 140. (-. (gt (succ (n0)) (succ (n0)))) (All X, (-. (gt X X))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) (gt (succ T_1) (n0)) (gt (n2) (n1)) ((pv5) != (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n3) (n2)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (T_1 != (n3)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((succ (n0)) = (n1)) ### TransEq2 134 138 139 % 41.01/41.23 141. ((succ (n0)) != (succ (n0))) ### Refl(=) % 41.01/41.23 142. (-. (gt (pv5) (succ (n0)))) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (T_1 != (n3)) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) (gt (n3) (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) ((pv5) != (n2)) (gt (n2) (n1)) (gt (succ T_1) (n0)) (gt (succ (n0)) (pv5)) ((succ (succ (n0))) = (n2)) (gt (n3) (n1)) ((succ (n0)) = (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) (All X, (-. (gt X X))) ### TransEq2 133 140 141 % 41.01/41.23 143. ((succ (succ (n0))) != (succ (succ (n0)))) ### Refl(=) % 41.01/41.23 144. ((succ (n0)) = (n1)) ((n1) != (succ (n0))) ### Sym(=) % 41.01/41.23 145. (-. (gt (n2) (succ (n0)))) (gt (n2) (n1)) ((succ (n0)) = (n1)) ### Trans 49 144 % 41.01/41.23 146. (-. (gt (succ (succ (n0))) (succ (n0)))) ((succ (succ (n0))) = (n2)) ((succ (n0)) = (n1)) (gt (n2) (n1)) ### TransEq 143 145 145 % 41.01/41.23 147. (All X, (-. (gt X X))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) (gt (succ T_1) (n0)) (gt (n2) (n1)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n3) (n2)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (T_1 != (n3)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) (-. (gt (pv5) (succ (n0)))) ### TransEq2 142 146 146 % 41.01/41.23 148. (-. (gt (pv5) (pv5))) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (T_1 != (n3)) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) (gt (n3) (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n2) (n1)) (gt (succ T_1) (n0)) (gt (succ (n0)) (pv5)) ((succ (succ (n0))) = (n2)) (gt (n3) (n1)) ((succ (n0)) = (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) (All X, (-. (gt X X))) ### Trans 147 41 % 41.01/41.23 149. (All X, (-. (gt X X))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) (gt (succ T_1) (n0)) (gt (n2) (n1)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n3) (n2)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (T_1 != (n3)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ### All 148 % 41.01/41.23 150. ((succ (succ (succ (n0)))) != (succ (succ (succ (n0))))) ### Refl(=) % 41.01/41.23 151. (-. (gt (succ (succ (n0))) (n3))) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) (gt (n3) (n2)) (gt (succ T_1) (n0)) (All X, (-. (gt X X))) (gt (n2) (n1)) ((succ (succ (n0))) = (n2)) ((pv5) != (n2)) ((pv5) != (n1)) (gt (succ (n0)) (pv5)) (gt (n3) (n1)) ((succ (n0)) = (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) ### Trans 59 149 % 41.01/41.23 152. (-. (gt (n2) (n3))) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) (gt (succ (n0)) (pv5)) ((pv5) != (n1)) ((pv5) != (n2)) ((succ (succ (n0))) = (n2)) (gt (n2) (n1)) (All X, (-. (gt X X))) (gt (succ T_1) (n0)) (gt (n3) (n2)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ### TransEq2 49 151 151 % 41.01/41.23 153. (-. (gt (n3) (n3))) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) (gt (n3) (n2)) (gt (succ T_1) (n0)) (All X, (-. (gt X X))) (gt (n2) (n1)) ((succ (succ (n0))) = (n2)) ((pv5) != (n2)) ((pv5) != (n1)) (gt (succ (n0)) (pv5)) (gt (n3) (n1)) ((succ (n0)) = (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) ### Trans 7 152 % 41.01/41.23 154. ((succ (n0)) != (succ (n0))) ### Refl(=) % 41.01/41.23 155. (-. (gt (succ (n0)) (n2))) (All X, (-. (gt X X))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) (gt (succ T_1) (n0)) (gt (n2) (n1)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n3) (n2)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (T_1 != (n3)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) (-. (gt (pv5) (succ (n0)))) ### Trans 154 142 % 41.01/41.23 156. (-. (gt (n1) (n2))) (-. (gt (pv5) (succ (n0)))) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (T_1 != (n3)) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) (gt (n3) (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n2) (n1)) (gt (succ T_1) (n0)) (gt (succ (n0)) (pv5)) ((succ (succ (n0))) = (n2)) (gt (n3) (n1)) ((succ (n0)) = (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) (All X, (-. (gt X X))) ### TransEq2 51 155 155 % 41.01/41.23 157. (-. (gt (succ (n0)) (n3))) (All X, (-. (gt X X))) (gt (succ T_1) (n0)) (gt (n2) (n1)) (gt (n3) (n2)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) (-. (gt (pv5) (succ (n0)))) (-. (gt (n1) (n2))) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) ((pv5) != (n1)) ((pv5) != (n2)) ### Trans 58 156 % 41.01/41.23 158. (-. (gt (n1) (n3))) ((pv5) != (n2)) ((pv5) != (n1)) (gt (succ (n0)) (pv5)) ((succ (succ (n0))) = (n2)) (gt (n3) (n1)) ((succ (n0)) = (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (-. (gt (n1) (n2))) (-. (gt (pv5) (succ (n0)))) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) (gt (n3) (n2)) (gt (n2) (n1)) (gt (succ T_1) (n0)) (All X, (-. (gt X X))) ### TransEq2 51 157 157 % 41.01/41.23 159. (All X, (-. (gt X X))) (gt (succ T_1) (n0)) (gt (n2) (n1)) (gt (n3) (n2)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) (-. (gt (pv5) (succ (n0)))) (-. (gt (n1) (n2))) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) ((pv5) != (n1)) ((pv5) != (n2)) ### Trans 158 49 % 41.01/41.23 160. (-. (gt (n1) (n1))) ((pv5) != (n2)) ((pv5) != (n1)) (gt (succ (n0)) (pv5)) ((succ (succ (n0))) = (n2)) (gt (n3) (n1)) ((succ (n0)) = (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (-. (gt (pv5) (succ (n0)))) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) (gt (n3) (n2)) (gt (n2) (n1)) (gt (succ T_1) (n0)) (All X, (-. (gt X X))) ### Trans 159 51 % 41.01/41.23 161. ((succ (n0)) != (succ (n0))) ### Refl(=) % 41.01/41.23 162. (All X, (-. (gt X X))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) (gt (succ T_1) (n0)) (gt (n2) (n1)) ((pv5) != (n2)) ((pv5) != (n1)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n3) (n2)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (T_1 != (n3)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) (-. (gt T_1 (succ (n0)))) ### TransEq2 100 146 146 % 41.01/41.23 163. ((succ (succ (succ (n0)))) != (succ (succ (succ (n0))))) ### Refl(=) % 41.01/41.23 164. (-. (gt (succ (succ (succ (n0)))) (succ (n0)))) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ### TransEq 163 39 39 % 41.01/41.23 165. (-. (gt T_1 (succ (n0)))) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) (gt (n3) (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) ((pv5) != (n1)) ((pv5) != (n2)) (gt (n2) (n1)) (gt (succ T_1) (n0)) (gt (succ (n0)) (pv5)) ((succ (succ (n0))) = (n2)) (gt (n3) (n1)) ((succ (n0)) = (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) (All X, (-. (gt X X))) ### TransEq2 162 164 164 % 41.01/41.23 166. (-. (gt (succ (n0)) (succ (n0)))) (All X, (-. (gt X X))) (gt (succ T_1) (n0)) (gt (n2) (n1)) (gt (n3) (n2)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) ((pv5) != (n1)) ((pv5) != (n2)) ### Trans 58 165 % 41.01/41.23 167. ((succ (succ (n0))) != (succ (succ (n0)))) ### Refl(=) % 41.01/41.23 168. (-. (gt (succ (n0)) (succ (succ (n0))))) (-. (gt (pv5) (succ (n0)))) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (T_1 != (n3)) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) (gt (n3) (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n2) (n1)) (gt (succ T_1) (n0)) (gt (succ (n0)) (pv5)) ((succ (succ (n0))) = (n2)) (gt (n3) (n1)) ((succ (n0)) = (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) (All X, (-. (gt X X))) ### TransEq2 155 155 167 % 41.01/41.23 169. (-. (gt (succ (n0)) (n3))) (All X, (-. (gt X X))) (gt (succ T_1) (n0)) (gt (n2) (n1)) (gt (n3) (n2)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) (-. (gt (pv5) (succ (n0)))) (-. (gt (succ (n0)) (succ (succ (n0))))) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) ((pv5) != (n1)) ((pv5) != (n2)) ### Trans 58 168 % 41.01/41.23 170. (-. (gt (n1) (n3))) (-. (gt (succ (n0)) (succ (succ (n0))))) (All X, (-. (gt X X))) (gt (succ T_1) (n0)) (gt (n2) (n1)) (gt (n3) (n2)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) (-. (gt (pv5) (succ (n0)))) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) ((pv5) != (n1)) ((pv5) != (n2)) ### TransEq2 160 160 169 % 41.01/41.23 171. ((succ (succ (succ (n0)))) != (succ (succ (succ (n0))))) ### Refl(=) % 41.01/41.23 172. (-. (gt (n1) (succ (succ (succ (n0)))))) ((pv5) != (n2)) ((pv5) != (n1)) (gt (succ (n0)) (pv5)) ((succ (succ (n0))) = (n2)) (gt (n3) (n1)) ((succ (n0)) = (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (-. (gt (pv5) (succ (n0)))) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) (gt (n3) (n2)) (gt (n2) (n1)) (gt (succ T_1) (n0)) (All X, (-. (gt X X))) (-. (gt (succ (n0)) (succ (succ (n0))))) ### TransEq2 170 170 171 % 41.01/41.23 173. (-. (gt (succ (n0)) (succ (succ (succ (n0)))))) (-. (gt (succ (n0)) (succ (succ (n0))))) (-. (gt (pv5) (succ (n0)))) ((pv5) != (n2)) ((pv5) != (n1)) (gt (succ (n0)) (pv5)) ((succ (succ (n0))) = (n2)) (gt (n3) (n1)) ((succ (n0)) = (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) (gt (n3) (n2)) (gt (n2) (n1)) (gt (succ T_1) (n0)) (All X, (-. (gt X X))) ### TransEq 161 166 172 % 41.01/41.23 174. ((succ (succ (succ (n0)))) != (succ (succ (succ (n0))))) ### Refl(=) % 41.01/41.23 175. (-. (gt (n2) (succ (succ (succ (n0)))))) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) (gt (n3) (n2)) (gt (succ T_1) (n0)) (All X, (-. (gt X X))) (gt (n2) (n1)) ((succ (succ (n0))) = (n2)) ((pv5) != (n2)) ((pv5) != (n1)) (gt (succ (n0)) (pv5)) (gt (n3) (n1)) ((succ (n0)) = (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) ### TransEq2 152 152 174 % 41.01/41.23 176. (All X, (-. (gt X X))) (gt (succ T_1) (n0)) (gt (n2) (n1)) (gt (n3) (n2)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) ((pv5) != (n1)) ((pv5) != (n2)) (-. (gt (pv5) (succ (n0)))) (-. (gt (succ (n0)) (succ (succ (succ (n0)))))) ### TransEq 173 173 175 % 41.01/41.24 177. (-. (gt (n1) (succ (succ (succ (n0)))))) (All X, (-. (gt X X))) (gt (succ T_1) (n0)) (gt (n2) (n1)) (gt (n3) (n2)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) (-. (gt (pv5) (succ (n0)))) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) ((pv5) != (n1)) ((pv5) != (n2)) ### TransEq2 160 160 176 % 41.01/41.24 178. (-. (gt (n3) (succ (succ (succ (n0)))))) (-. (gt (pv5) (succ (n0)))) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) (gt (succ (n0)) (pv5)) ((pv5) != (n1)) ((pv5) != (n2)) ((succ (succ (n0))) = (n2)) (gt (n2) (n1)) (All X, (-. (gt X X))) (gt (succ T_1) (n0)) (gt (n3) (n2)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ### Trans 153 177 % 41.01/41.24 179. ((succ (succ (succ (n0)))) = (n3)) ((n3) != (succ (succ (succ (n0))))) ### Sym(=) % 41.01/41.24 180. (-. (gt (succ (succ (succ (n0)))) (succ (succ (succ (n0)))))) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) (gt (n3) (n2)) (gt (succ T_1) (n0)) (All X, (-. (gt X X))) (gt (n2) (n1)) ((succ (succ (n0))) = (n2)) ((pv5) != (n2)) ((pv5) != (n1)) (gt (succ (n0)) (pv5)) (gt (n3) (n1)) ((succ (n0)) = (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (-. (gt (pv5) (succ (n0)))) ### TransEq 150 178 179 % 41.01/41.24 181. ((succ (succ (succ (n0)))) != (succ (succ (succ (n0))))) ### Refl(=) % 41.01/41.24 182. (-. (gt T_1 (succ (succ (succ (n0)))))) (-. (gt (pv5) (succ (n0)))) ((pv5) != (n1)) ((pv5) != (n2)) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) (gt (n3) (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n2) (n1)) (gt (succ T_1) (n0)) (gt (succ (n0)) (pv5)) ((succ (succ (n0))) = (n2)) (gt (n3) (n1)) ((succ (n0)) = (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) (All X, (-. (gt X X))) ### TransEq2 149 180 181 % 41.01/41.24 183. (-. (gt T_1 (n3))) (All X, (-. (gt X X))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) (gt (succ T_1) (n0)) (gt (n2) (n1)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n3) (n2)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != (n2)) ((pv5) != (n1)) (-. (gt (pv5) (succ (n0)))) ### TransEq 182 182 153 % 41.01/41.24 184. ((succ (succ (succ (n0)))) != (succ (succ (succ (n0))))) ### Refl(=) % 41.01/41.24 185. (-. (gt (succ (succ (succ (n0)))) (succ (pv5)))) (gt (n2) (n1)) ((succ (succ (n0))) = (n2)) ((pv5) != (n2)) ((pv5) != (n1)) (gt (succ (n0)) (pv5)) (gt (n3) (n1)) ((succ (n0)) = (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n3) (n2)) ### TransEq 184 61 61 % 41.01/41.24 186. (-. (gt T_1 (succ (pv5)))) (-. (gt (pv5) (succ (n0)))) ((pv5) != (n1)) ((pv5) != (n2)) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) (gt (n3) (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n2) (n1)) (gt (succ T_1) (n0)) (gt (succ (n0)) (pv5)) ((succ (succ (n0))) = (n2)) (gt (n3) (n1)) ((succ (n0)) = (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) (All X, (-. (gt X X))) ### TransEq2 183 183 185 % 41.01/41.24 187. (T_1 != T_1) ### Refl(=) % 41.01/41.24 188. (-. (gt T_1 T_1)) (All X, (-. (gt X X))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) (gt (succ T_1) (n0)) (gt (n2) (n1)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n3) (n2)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != (n2)) ((pv5) != (n1)) (-. (gt (pv5) (succ (n0)))) ### Trans 186 187 % 41.01/41.24 189. (-. (gt (pv5) (succ (n0)))) ((pv5) != (n1)) ((pv5) != (n2)) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) (gt (n3) (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n2) (n1)) (gt (succ T_1) (n0)) (gt (succ (n0)) (pv5)) ((succ (succ (n0))) = (n2)) (gt (n3) (n1)) ((succ (n0)) = (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) (All X, (-. (gt X X))) ### All 188 % 41.01/41.24 190. (-. (gt T_1 (succ (pv5)))) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) (gt (n3) (n2)) (gt (n2) (n1)) (gt (succ T_1) (n0)) (All X, (-. (gt X X))) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) ((pv5) != (n1)) ((pv5) != (n2)) (-. (gt (n1) (n2))) ### TransEq2 131 185 185 % 41.01/41.24 191. (-. (gt (succ (n0)) (succ (pv5)))) (-. (gt (n1) (n2))) (All X, (-. (gt X X))) (gt (succ T_1) (n0)) (gt (n2) (n1)) (gt (n3) (n2)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) ((pv5) != (n1)) ((pv5) != (n2)) ### Trans 58 190 % 41.01/41.24 192. (-. (gt (succ (n0)) (n3))) ((pv5) != (n2)) ((pv5) != (n1)) (gt (succ (n0)) (pv5)) ((succ (succ (n0))) = (n2)) (gt (n3) (n1)) ((succ (n0)) = (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) (gt (n3) (n2)) (gt (n2) (n1)) (gt (succ T_1) (n0)) (All X, (-. (gt X X))) (-. (gt (n1) (n2))) ### Trans 191 131 % 41.01/41.24 193. (-. (gt (n1) (n3))) (-. (gt (n1) (n2))) (All X, (-. (gt X X))) (gt (succ T_1) (n0)) (gt (n2) (n1)) (gt (n3) (n2)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) ((pv5) != (n1)) ((pv5) != (n2)) ### TransEq2 51 192 192 % 41.01/41.24 194. (-. (gt (n2) (n2))) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) (gt (n3) (n2)) (gt (succ T_1) (n0)) (All X, (-. (gt X X))) (gt (n2) (n1)) ((succ (succ (n0))) = (n2)) ((pv5) != (n2)) ((pv5) != (n1)) (gt (succ (n0)) (pv5)) (gt (n3) (n1)) ((succ (n0)) = (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) ### Trans 152 49 % 41.01/41.24 195. ((pv5) != (n2)) ((pv5) != (n1)) (gt (succ (n0)) (pv5)) ((succ (succ (n0))) = (n2)) (gt (n3) (n1)) ((succ (n0)) = (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) (gt (n3) (n2)) (gt (n2) (n1)) (gt (succ T_1) (n0)) (All X, (-. (gt X X))) (-. (gt (n1) (n2))) ### Trans 193 194 % 41.01/41.24 196. (-. (gt (n1) (n1))) (All X, (-. (gt X X))) (gt (succ T_1) (n0)) (gt (n2) (n1)) (gt (n3) (n2)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) ((pv5) != (n1)) ((pv5) != (n2)) ### Trans 195 51 % 41.01/41.24 197. (-. (gt (pv5) (n1))) (All X, (-. (gt X X))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) (gt (succ T_1) (n0)) (gt (n2) (n1)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n3) (n2)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != (n2)) ((pv5) != (n1)) ### TransEq 189 160 196 % 41.01/41.24 198. ((succ (n0)) != (succ (n0))) ### Refl(=) % 41.01/41.24 199. ((succ (n0)) != (succ (n0))) ### Refl(=) % 41.01/41.24 200. (-. (gt (succ (n0)) (n1))) ((pv5) != (n2)) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) (gt (n3) (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n2) (n1)) (gt (succ T_1) (n0)) (gt (succ (n0)) (pv5)) ((succ (succ (n0))) = (n2)) (gt (n3) (n1)) ((succ (n0)) = (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) (All X, (-. (gt X X))) ### Trans 199 197 % 41.01/41.24 201. ((succ (n0)) = (n1)) ((succ (n0)) != (n1)) ### Axiom % 41.01/41.24 202. (-. (gt (n1) (n1))) (All X, (-. (gt X X))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) (gt (succ T_1) (n0)) (gt (n2) (n1)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n3) (n2)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != (n2)) ### TransEq2 51 200 201 % 41.01/41.24 203. ((succ (n0)) != (succ (n0))) ### Refl(=) % 41.01/41.24 204. (-. (gt (n1) (succ (n0)))) ((pv5) != (n2)) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) (gt (n3) (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n2) (n1)) (gt (succ T_1) (n0)) (gt (succ (n0)) (pv5)) ((succ (succ (n0))) = (n2)) (gt (n3) (n1)) ((succ (n0)) = (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) (All X, (-. (gt X X))) ### TransEq2 51 202 203 % 41.01/41.24 205. ((succ (n0)) = (n1)) ((n1) != (succ (n0))) ### Sym(=) % 41.01/41.24 206. (-. (gt (succ (n0)) (succ (n0)))) (All X, (-. (gt X X))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) (gt (succ T_1) (n0)) (gt (n2) (n1)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n3) (n2)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != (n2)) ### TransEq 198 204 205 % 41.01/41.24 207. ((succ (n0)) != (succ (n0))) ### Refl(=) % 41.01/41.24 208. (-. (gt (pv5) (succ (n0)))) ((pv5) != (n2)) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) (gt (n3) (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n2) (n1)) (gt (succ T_1) (n0)) (gt (succ (n0)) (pv5)) ((succ (succ (n0))) = (n2)) (gt (n3) (n1)) ((succ (n0)) = (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) (All X, (-. (gt X X))) ### TransEq2 197 206 207 % 41.01/41.24 209. (All X, (-. (gt X X))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) (gt (succ T_1) (n0)) (gt (n2) (n1)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n3) (n2)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) (-. (gt (pv5) (succ (n0)))) ### TransEq2 208 146 146 % 41.01/41.24 210. (-. (gt (pv5) (pv5))) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ((pv5) != T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (gt (succ (pv5)) T_1) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) (gt (n3) (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n2) (n1)) (gt (succ T_1) (n0)) (gt (succ (n0)) (pv5)) ((succ (succ (n0))) = (n2)) (gt (n3) (n1)) ((succ (n0)) = (n1)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (pv5)) (n0)) (All X, (-. (gt X X))) ### Trans 209 41 % 41.01/41.24 211. (All X, (-. (gt X X))) (gt (succ (pv5)) (n0)) ((succ (succ (succ (n0)))) = (n3)) ((succ (n0)) = (n1)) (gt (n3) (n1)) ((succ (succ (n0))) = (n2)) (gt (succ (n0)) (pv5)) (gt (succ T_1) (n0)) (gt (n2) (n1)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n3) (n2)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (succ (pv5)) T_1) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((pv5) != T_1) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ### All 210 % 41.01/41.25 212. (-. (((n2) = T_0) /\ ((pv5) = T_1))) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) (gt (succ (pv5)) T_1) (gt (n3) (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n2) (n1)) (gt (succ T_1) (n0)) (gt (succ (n0)) (pv5)) (gt (n3) (n1)) ((succ (n0)) = (n1)) (gt (succ (pv5)) (n0)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (gt (succ T_0) (n0)) ((succ (succ (n0))) = (n2)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (n2)) T_0) ((n0) != T_0) ((n1) != T_0) (All X, (-. (gt X X))) ### NotAnd 33 211 % 41.01/41.25 213. (-. (((n1) = T_0) /\ ((pv5) = T_1))) (All X, (-. (gt X X))) ((n0) != T_0) (gt (succ (n2)) T_0) ((succ (succ (succ (n0)))) = (n3)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) ((succ (succ (n0))) = (n2)) (gt (succ T_0) (n0)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (gt (succ (pv5)) (n0)) ((succ (n0)) = (n1)) (gt (n3) (n1)) (gt (succ (n0)) (pv5)) (gt (succ T_1) (n0)) (gt (n2) (n1)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n3) (n2)) (gt (succ (pv5)) T_1) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) (-. (((n2) = T_0) /\ ((pv5) = T_1))) ### NotAnd 212 211 % 41.01/41.25 214. (-. (((n0) = T_0) /\ ((pv5) = T_1))) (-. (((n2) = T_0) /\ ((pv5) = T_1))) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) (gt (succ (pv5)) T_1) (gt (n3) (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n2) (n1)) (gt (succ T_1) (n0)) (gt (succ (n0)) (pv5)) (gt (n3) (n1)) ((succ (n0)) = (n1)) (gt (succ (pv5)) (n0)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (gt (succ T_0) (n0)) ((succ (succ (n0))) = (n2)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) ((succ (succ (succ (n0)))) = (n3)) (gt (succ (n2)) T_0) (All X, (-. (gt X X))) (-. (((n1) = T_0) /\ ((pv5) = T_1))) ### NotAnd 213 211 % 41.01/41.25 215. (leq T_1 (pv5)) (-. (((n1) = T_0) /\ ((pv5) = T_1))) (All X, (-. (gt X X))) (gt (succ (n2)) T_0) ((succ (succ (succ (n0)))) = (n3)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) ((succ (succ (n0))) = (n2)) (gt (succ T_0) (n0)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (gt (succ (pv5)) (n0)) ((succ (n0)) = (n1)) (gt (n3) (n1)) (gt (succ (n0)) (pv5)) (gt (succ T_1) (n0)) (gt (n2) (n1)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n3) (n2)) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) (-. (((n2) = T_0) /\ ((pv5) = T_1))) (-. (((n0) = T_0) /\ ((pv5) = T_1))) ### Definition-Pseudo(leq) 214 % 41.01/41.25 216. (leq T_0 (n2)) (-. (((n0) = T_0) /\ ((pv5) = T_1))) (-. (((n2) = T_0) /\ ((pv5) = T_1))) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) (gt (n3) (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n2) (n1)) (gt (succ T_1) (n0)) (gt (succ (n0)) (pv5)) (gt (n3) (n1)) ((succ (n0)) = (n1)) (gt (succ (pv5)) (n0)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (gt (succ T_0) (n0)) ((succ (succ (n0))) = (n2)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) ((succ (succ (succ (n0)))) = (n3)) (All X, (-. (gt X X))) (-. (((n1) = T_0) /\ ((pv5) = T_1))) (leq T_1 (pv5)) ### Definition-Pseudo(leq) 215 % 41.01/41.25 217. (leq (n0) T_1) (leq T_1 (pv5)) (-. (((n1) = T_0) /\ ((pv5) = T_1))) (All X, (-. (gt X X))) ((succ (succ (succ (n0)))) = (n3)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) ((succ (succ (n0))) = (n2)) (gt (succ T_0) (n0)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (gt (succ (pv5)) (n0)) ((succ (n0)) = (n1)) (gt (n3) (n1)) (gt (succ (n0)) (pv5)) (gt (n2) (n1)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n3) (n2)) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) (-. (((n2) = T_0) /\ ((pv5) = T_1))) (-. (((n0) = T_0) /\ ((pv5) = T_1))) (leq T_0 (n2)) ### Definition-Pseudo(leq) 216 % 41.01/41.25 218. (leq (n0) T_0) (leq T_0 (n2)) (-. (((n0) = T_0) /\ ((pv5) = T_1))) (-. (((n2) = T_0) /\ ((pv5) = T_1))) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) (gt (n3) (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n2) (n1)) (gt (succ (n0)) (pv5)) (gt (n3) (n1)) ((succ (n0)) = (n1)) (gt (succ (pv5)) (n0)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((succ (succ (n0))) = (n2)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) ((succ (succ (succ (n0)))) = (n3)) (All X, (-. (gt X X))) (-. (((n1) = T_0) /\ ((pv5) = T_1))) (leq T_1 (pv5)) (leq (n0) T_1) ### Definition-Pseudo(leq) 217 % 41.01/41.25 219. (-. (((leq (n0) T_0) /\ ((leq (n0) T_1) /\ ((leq T_0 (n2)) /\ (leq T_1 (pv5))))) => (((-. (((n0) = T_0) /\ ((pv5) = T_1))) /\ ((-. (((n1) = T_0) /\ ((pv5) = T_1))) /\ (-. (((n2) = T_0) /\ ((pv5) = T_1))))) => ((a_select3 (z_defuse) T_0 T_1) = (use))))) (All X, (-. (gt X X))) ((succ (succ (succ (n0)))) = (n3)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) ((succ (succ (n0))) = (n2)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (gt (succ (pv5)) (n0)) ((succ (n0)) = (n1)) (gt (n3) (n1)) (gt (succ (n0)) (pv5)) (gt (n2) (n1)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n3) (n2)) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ### ConjTree 218 % 41.01/41.25 220. (-. (All F, (((leq (n0) T_0) /\ ((leq (n0) F) /\ ((leq T_0 (n2)) /\ (leq F (pv5))))) => (((-. (((n0) = T_0) /\ ((pv5) = F))) /\ ((-. (((n1) = T_0) /\ ((pv5) = F))) /\ (-. (((n2) = T_0) /\ ((pv5) = F))))) => ((a_select3 (z_defuse) T_0 F) = (use)))))) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) (gt (n3) (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n2) (n1)) (gt (succ (n0)) (pv5)) (gt (n3) (n1)) ((succ (n0)) = (n1)) (gt (succ (pv5)) (n0)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((succ (succ (n0))) = (n2)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) ((succ (succ (succ (n0)))) = (n3)) (All X, (-. (gt X X))) ### NotAllEx 219 % 41.01/41.25 221. (-. (All E, (All F, (((leq (n0) E) /\ ((leq (n0) F) /\ ((leq E (n2)) /\ (leq F (pv5))))) => (((-. (((n0) = E) /\ ((pv5) = F))) /\ ((-. (((n1) = E) /\ ((pv5) = F))) /\ (-. (((n2) = E) /\ ((pv5) = F))))) => ((a_select3 (z_defuse) E F) = (use))))))) (All X, (-. (gt X X))) ((succ (succ (succ (n0)))) = (n3)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) ((succ (succ (n0))) = (n2)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) (gt (succ (pv5)) (n0)) ((succ (n0)) = (n1)) (gt (n3) (n1)) (gt (succ (n0)) (pv5)) (gt (n2) (n1)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n3) (n2)) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) ### NotAllEx 220 % 41.01/41.25 222. (leq (pv5) (n0)) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) (gt (n3) (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n2) (n1)) (gt (n3) (n1)) ((succ (n0)) = (n1)) (gt (succ (pv5)) (n0)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((succ (succ (n0))) = (n2)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) ((succ (succ (succ (n0)))) = (n3)) (All X, (-. (gt X X))) (-. (All E, (All F, (((leq (n0) E) /\ ((leq (n0) F) /\ ((leq E (n2)) /\ (leq F (pv5))))) => (((-. (((n0) = E) /\ ((pv5) = F))) /\ ((-. (((n1) = E) /\ ((pv5) = F))) /\ (-. (((n2) = E) /\ ((pv5) = F))))) => ((a_select3 (z_defuse) E F) = (use))))))) ### Definition-Pseudo(leq) 221 % 41.01/41.25 223. (leq (n0) (pv5)) (-. (All E, (All F, (((leq (n0) E) /\ ((leq (n0) F) /\ ((leq E (n2)) /\ (leq F (pv5))))) => (((-. (((n0) = E) /\ ((pv5) = F))) /\ ((-. (((n1) = E) /\ ((pv5) = F))) /\ (-. (((n2) = E) /\ ((pv5) = F))))) => ((a_select3 (z_defuse) E F) = (use))))))) (All X, (-. (gt X X))) ((succ (succ (succ (n0)))) = (n3)) (gt (n4) (n3)) ((succ (succ (succ (succ (n0))))) = (n4)) ((succ (succ (n0))) = (n2)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((succ (n0)) = (n1)) (gt (n3) (n1)) (gt (n2) (n1)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n3) (n2)) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) (leq (pv5) (n0)) ### Definition-Pseudo(leq) 222 % 41.01/41.25 224. (-. ((((a_select2 (rho_defuse) (n0)) = (use)) /\ (((a_select2 (rho_defuse) (n1)) = (use)) /\ (((a_select2 (rho_defuse) (n2)) = (use)) /\ (((a_select2 (sigma_defuse) (n0)) = (use)) /\ (((a_select2 (sigma_defuse) (n1)) = (use)) /\ (((a_select2 (sigma_defuse) (n2)) = (use)) /\ (((a_select2 (sigma_defuse) (n3)) = (use)) /\ (((a_select2 (sigma_defuse) (n4)) = (use)) /\ (((a_select2 (sigma_defuse) (n5)) = (use)) /\ (((a_select3 (u_defuse) (n0) (n0)) = (use)) /\ (((a_select3 (u_defuse) (n1) (n0)) = (use)) /\ (((a_select3 (u_defuse) (n2) (n0)) = (use)) /\ (((a_select2 (xinit_defuse) (n3)) = (use)) /\ (((a_select2 (xinit_defuse) (n4)) = (use)) /\ (((a_select2 (xinit_defuse) (n5)) = (use)) /\ (((a_select2 (xinit_mean_defuse) (n0)) = (use)) /\ (((a_select2 (xinit_mean_defuse) (n1)) = (use)) /\ (((a_select2 (xinit_mean_defuse) (n2)) = (use)) /\ (((a_select2 (xinit_mean_defuse) (n3)) = (use)) /\ (((a_select2 (xinit_mean_defuse) (n4)) = (use)) /\ (((a_select2 (xinit_mean_defuse) (n5)) = (use)) /\ (((a_select2 (xinit_noise_defuse) (n0)) = (use)) /\ (((a_select2 (xinit_noise_defuse) (n1)) = (use)) /\ (((a_select2 (xinit_noise_defuse) (n2)) = (use)) /\ (((a_select2 (xinit_noise_defuse) (n3)) = (use)) /\ (((a_select2 (xinit_noise_defuse) (n4)) = (use)) /\ (((a_select2 (xinit_noise_defuse) (n5)) = (use)) /\ ((leq (n0) (pv5)) /\ ((leq (pv5) (n0)) /\ ((leq (pv5) (n998)) /\ ((All A, (All B, (((leq (n0) A) /\ ((leq (n0) B) /\ ((leq A (n2)) /\ (leq B (pred (pv5)))))) => ((a_select3 (u_defuse) A B) = (use))))) /\ (All C, (All D, (((leq (n0) C) /\ ((leq (n0) D) /\ ((leq C (n2)) /\ (leq D (pred (pv5)))))) => ((a_select3 (z_defuse) C D) = (use)))))))))))))))))))))))))))))))))))) => (All E, (All F, (((leq (n0) E) /\ ((leq (n0) F) /\ ((leq E (n2)) /\ (leq F (pv5))))) => (((-. (((n0) = E) /\ ((pv5) = F))) /\ ((-. (((n1) = E) /\ ((pv5) = F))) /\ (-. (((n2) = E) /\ ((pv5) = F))))) => ((a_select3 (z_defuse) E F) = (use)))))))) (All X, (All Y, (((leq X Y) /\ (X != Y)) => (gt Y X)))) (gt (n3) (n2)) (All X, (((leq (n0) X) /\ (leq X (n2))) => ((X = (n0)) \/ ((X = (n1)) \/ (X = (n2)))))) (gt (n2) (n1)) (gt (n3) (n1)) ((succ (n0)) = (n1)) (All X, (((leq (n0) X) /\ (leq X (n3))) => ((X = (n0)) \/ ((X = (n1)) \/ ((X = (n2)) \/ (X = (n3))))))) ((succ (succ (n0))) = (n2)) ((succ (succ (succ (succ (n0))))) = (n4)) (gt (n4) (n3)) ((succ (succ (succ (n0)))) = (n3)) (All X, (-. (gt X X))) ### ConjTree 223 % 41.01/41.25 % SZS output end Proof % 41.01/41.25 (* END-PROOF *) %------------------------------------------------------------------------------