%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : NUM295+1 : TPTP v8.1.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n014.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:41:33 EDT 2022 % Result : Theorem 95.70s 95.91s % Output : Proof 95.70s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NUM295+1 : TPTP v8.1.0. Released v3.1.0. % 0.03/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n014.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Thu Jul 7 06:09:22 EDT 2022 % 0.12/0.33 % CPUTime : % 95.70/95.91 % SZS status Theorem % 95.70/95.91 (* PROOF-FOUND *) % 95.70/95.91 (* BEGIN-PROOF *) % 95.70/95.91 % SZS output start Proof % 95.70/95.91 1. (less (n0) (rdnn (n1))) (-. (less (n0) (rdnn (n1)))) ### Axiom % 95.70/95.91 2. (-. (Ex Y, (less (n0) Y))) (less (n0) (rdnn (n1))) ### NotExists 1 % 95.70/95.91 3. (-. (-. (less (n0) (rdnn (n1))))) (-. (Ex Y, (less (n0) Y))) ### NotNot 2 % 95.70/95.91 4. (less (n1) (rdnn (n8))) (-. (less (n1) (rdnn (n8)))) ### Axiom % 95.70/95.91 5. (-. (Ex Y, (less (n1) Y))) (less (n1) (rdnn (n8))) ### NotExists 4 % 95.70/95.91 6. (-. (-. (less (n1) (rdnn (n8))))) (-. (Ex Y, (less (n1) Y))) ### NotNot 5 % 95.70/95.91 7. (less (n0) (rdnn (n8))) (-. (less (n0) (rdnn (n8)))) ### Axiom % 95.70/95.91 8. (-. (Ex Y, (less (n0) Y))) (less (n0) (rdnn (n8))) ### NotExists 7 % 95.70/95.91 9. (-. (-. (less (n0) (rdnn (n8))))) (-. (Ex Y, (less (n0) Y))) ### NotNot 8 % 95.70/95.91 10. (-. (less (rdnn (n8)) (n0))) (less (rdnn (n8)) (n0)) ### Axiom % 95.70/95.91 11. (-. (-. (less (rdnn (n8)) (n0)))) (-. (less (rdnn (n8)) (n0))) ### NotNot 10 % 95.70/95.91 12. ((n1) != (n1)) ### NotEqual % 95.70/95.91 13. (-. ((rdnn (n8)) != (n0))) ((rdnn (n8)) != (n0)) ### Axiom % 95.70/95.91 14. ((rdnn (n1)) != (rdnn (n1))) ### Refl(=) % 95.70/95.91 15. ((rdnn (n1)) != (rdnn (n8))) ((n0) = (rdnn (n1))) (-. ((rdnn (n8)) != (n0))) ### Trans-sym 13 14 % 95.70/95.91 16. (-. (less (n1) (rdnn (n8)))) (less (n1) (rdnn (n1))) (-. ((rdnn (n8)) != (n0))) ((n0) = (rdnn (n1))) ### P-NotP 12 15 % 95.70/95.91 17. ((n1) = (rdnn (n8))) ((rdnn (n8)) != (n1)) ### Sym(=) % 95.70/95.91 18. ((-. (less (rdnn (n8)) (n1))) /\ ((rdnn (n8)) != (n1))) ((n1) = (rdnn (n8))) ### And 17 % 95.70/95.91 19. ((less (n1) (rdnn (n8))) <=> ((-. (less (rdnn (n8)) (n1))) /\ ((rdnn (n8)) != (n1)))) ((n1) = (rdnn (n8))) ((n0) = (rdnn (n1))) (-. ((rdnn (n8)) != (n0))) (less (n1) (rdnn (n1))) ### Equiv 16 18 % 95.70/95.91 20. (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (less (n1) (rdnn (n1))) (-. ((rdnn (n8)) != (n0))) ((n0) = (rdnn (n1))) ((n1) = (rdnn (n8))) ### All 19 % 95.70/95.91 21. (-. ((-. (less (rdnn (n8)) (n0))) /\ ((rdnn (n8)) != (n0)))) ((n1) = (rdnn (n8))) ((n0) = (rdnn (n1))) (less (n1) (rdnn (n1))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (-. (less (rdnn (n8)) (n0))) ### NotAnd 11 20 % 95.70/95.91 22. ((n0) = (rdnn (n8))) ((rdnn (n8)) != (n0)) ### Sym(=) % 95.70/95.91 23. ((-. (less (rdnn (n8)) (n0))) /\ ((rdnn (n8)) != (n0))) ((n0) = (rdnn (n8))) ### And 22 % 95.70/95.91 24. ((less (n0) (rdnn (n8))) <=> ((-. (less (rdnn (n8)) (n0))) /\ ((rdnn (n8)) != (n0)))) ((n0) = (rdnn (n8))) (-. (less (rdnn (n8)) (n0))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (less (n1) (rdnn (n1))) ((n0) = (rdnn (n1))) ((n1) = (rdnn (n8))) ### Equiv 21 23 % 95.70/95.91 25. (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) ((n1) = (rdnn (n8))) ((n0) = (rdnn (n1))) (less (n1) (rdnn (n1))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (-. (less (rdnn (n8)) (n0))) ((n0) = (rdnn (n8))) ### All 24 % 95.70/95.91 26. (-. ((n0) != (rdnn (n8)))) (-. (less (rdnn (n8)) (n0))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (less (n1) (rdnn (n1))) ((n0) = (rdnn (n1))) ((n1) = (rdnn (n8))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) ### NotNot 25 % 95.70/95.91 27. (-. ((-. (less (n0) (rdnn (n8)))) /\ ((n0) != (rdnn (n8))))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) ((n1) = (rdnn (n8))) ((n0) = (rdnn (n1))) (less (n1) (rdnn (n1))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (-. (less (rdnn (n8)) (n0))) (-. (Ex Y, (less (n0) Y))) ### NotAnd 9 26 % 95.70/95.91 28. (less (rdnn (n8)) (n0)) (-. (less (rdnn (n8)) (n0))) ### Axiom % 95.70/95.91 29. (-. (Ex Y, (less (rdnn (n8)) Y))) (less (rdnn (n8)) (n0)) ### NotExists 28 % 95.70/95.91 30. (-. (Ex X, (Ex Y, (less X Y)))) (less (rdnn (n8)) (n0)) ### NotExists 29 % 95.70/95.91 31. ((less (rdnn (n8)) (n0)) <=> ((-. (less (n0) (rdnn (n8)))) /\ ((n0) != (rdnn (n8))))) (-. (Ex X, (Ex Y, (less X Y)))) (-. (Ex Y, (less (n0) Y))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (less (n1) (rdnn (n1))) ((n0) = (rdnn (n1))) ((n1) = (rdnn (n8))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) ### Equiv 27 30 % 95.70/95.91 32. (All Y, ((less (rdnn (n8)) Y) <=> ((-. (less Y (rdnn (n8)))) /\ (Y != (rdnn (n8)))))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) ((n1) = (rdnn (n8))) ((n0) = (rdnn (n1))) (less (n1) (rdnn (n1))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (-. (Ex Y, (less (n0) Y))) (-. (Ex X, (Ex Y, (less X Y)))) ### All 31 % 95.70/95.91 33. (-. ((n1) != (rdnn (n8)))) (-. (Ex X, (Ex Y, (less X Y)))) (-. (Ex Y, (less (n0) Y))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (less (n1) (rdnn (n1))) ((n0) = (rdnn (n1))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) (All Y, ((less (rdnn (n8)) Y) <=> ((-. (less Y (rdnn (n8)))) /\ (Y != (rdnn (n8)))))) ### NotNot 32 % 95.70/95.91 34. (-. ((-. (less (n1) (rdnn (n8)))) /\ ((n1) != (rdnn (n8))))) (All Y, ((less (rdnn (n8)) Y) <=> ((-. (less Y (rdnn (n8)))) /\ (Y != (rdnn (n8)))))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) ((n0) = (rdnn (n1))) (less (n1) (rdnn (n1))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (-. (Ex Y, (less (n0) Y))) (-. (Ex X, (Ex Y, (less X Y)))) (-. (Ex Y, (less (n1) Y))) ### NotAnd 6 33 % 95.70/95.91 35. (less (rdnn (n8)) (n1)) (-. (less (rdnn (n8)) (n1))) ### Axiom % 95.70/95.91 36. (-. (Ex Y, (less (rdnn (n8)) Y))) (less (rdnn (n8)) (n1)) ### NotExists 35 % 95.70/95.91 37. (-. (Ex X, (Ex Y, (less X Y)))) (less (rdnn (n8)) (n1)) ### NotExists 36 % 95.70/95.91 38. ((less (rdnn (n8)) (n1)) <=> ((-. (less (n1) (rdnn (n8)))) /\ ((n1) != (rdnn (n8))))) (-. (Ex Y, (less (n1) Y))) (-. (Ex X, (Ex Y, (less X Y)))) (-. (Ex Y, (less (n0) Y))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (less (n1) (rdnn (n1))) ((n0) = (rdnn (n1))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) (All Y, ((less (rdnn (n8)) Y) <=> ((-. (less Y (rdnn (n8)))) /\ (Y != (rdnn (n8)))))) ### Equiv 34 37 % 95.70/95.91 39. (All Y, ((less (rdnn (n8)) Y) <=> ((-. (less Y (rdnn (n8)))) /\ (Y != (rdnn (n8)))))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) ((n0) = (rdnn (n1))) (less (n1) (rdnn (n1))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (-. (Ex Y, (less (n0) Y))) (-. (Ex X, (Ex Y, (less X Y)))) (-. (Ex Y, (less (n1) Y))) ### All 38 % 95.70/95.91 40. (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (-. (Ex Y, (less (n1) Y))) (-. (Ex X, (Ex Y, (less X Y)))) (-. (Ex Y, (less (n0) Y))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (less (n1) (rdnn (n1))) ((n0) = (rdnn (n1))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) ### All 39 % 95.70/95.91 41. (-. (-. (less (n1) (rdnn (n1))))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) ((n0) = (rdnn (n1))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (-. (Ex Y, (less (n0) Y))) (-. (Ex X, (Ex Y, (less X Y)))) (-. (Ex Y, (less (n1) Y))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) ### NotNot 40 % 95.70/95.91 42. (less (n8) (n3)) (-. (less (n8) (n3))) ### Axiom % 95.70/95.91 43. (-. (Ex Y, (less (n8) Y))) (less (n8) (n3)) ### NotExists 42 % 95.70/95.91 44. (-. (-. (less (n8) (n3)))) (-. (Ex Y, (less (n8) Y))) ### NotNot 43 % 95.70/95.91 45. ((n3) != (n8)) ((n8) = (n3)) ### Sym(=) % 95.70/95.91 46. (-. ((n8) != (n3))) ((n3) != (n8)) ### NotNot 45 % 95.70/95.91 47. (-. ((-. (less (n8) (n3))) /\ ((n8) != (n3)))) ((n3) != (n8)) (-. (Ex Y, (less (n8) Y))) ### NotAnd 44 46 % 95.70/95.91 48. (less (n3) (n8)) (-. (less (n3) (n8))) ### Axiom % 95.70/95.91 49. (-. (Ex Y, (less (n3) Y))) (less (n3) (n8)) ### NotExists 48 % 95.70/95.91 50. (-. (Ex X, (Ex Y, (less X Y)))) (less (n3) (n8)) ### NotExists 49 % 95.70/95.91 51. ((less (n3) (n8)) <=> ((-. (less (n8) (n3))) /\ ((n8) != (n3)))) (-. (Ex X, (Ex Y, (less X Y)))) (-. (Ex Y, (less (n8) Y))) ((n3) != (n8)) ### Equiv 47 50 % 95.70/95.91 52. (All Y, ((less (n3) Y) <=> ((-. (less Y (n3))) /\ (Y != (n3))))) ((n3) != (n8)) (-. (Ex Y, (less (n8) Y))) (-. (Ex X, (Ex Y, (less X Y)))) ### All 51 % 95.70/95.91 53. (-. (Ex X, (Ex Y, (less X Y)))) ((n3) != (n8)) (All Y, ((less (n3) Y) <=> ((-. (less Y (n3))) /\ (Y != (n3))))) ### NotExists 52 % 95.70/95.91 54. (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) ((n3) != (n8)) (-. (Ex X, (Ex Y, (less X Y)))) ### All 53 % 95.70/95.91 55. ((rdnn (n3)) != (rdnn (n8))) (-. (Ex X, (Ex Y, (less X Y)))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) ### NotEqual 54 % 95.70/95.91 56. (-. ((-. (less (rdnn (n8)) (n0))) /\ ((rdnn (n8)) != (n0)))) ((n0) = (rdnn (n1))) ((rdnn (n1)) != (rdnn (n8))) (-. (less (rdnn (n8)) (n0))) ### NotAnd 11 15 % 95.70/95.91 57. ((less (n0) (rdnn (n8))) <=> ((-. (less (rdnn (n8)) (n0))) /\ ((rdnn (n8)) != (n0)))) ((n0) = (rdnn (n8))) (-. (less (rdnn (n8)) (n0))) ((rdnn (n1)) != (rdnn (n8))) ((n0) = (rdnn (n1))) ### Equiv 56 23 % 95.70/95.91 58. (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) ((n0) = (rdnn (n1))) ((rdnn (n1)) != (rdnn (n8))) (-. (less (rdnn (n8)) (n0))) ((n0) = (rdnn (n8))) ### All 57 % 95.70/95.91 59. (-. ((n0) != (rdnn (n8)))) (-. (less (rdnn (n8)) (n0))) ((rdnn (n1)) != (rdnn (n8))) ((n0) = (rdnn (n1))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) ### NotNot 58 % 95.70/95.91 60. (-. ((-. (less (n0) (rdnn (n8)))) /\ ((n0) != (rdnn (n8))))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) ((n0) = (rdnn (n1))) ((rdnn (n1)) != (rdnn (n8))) (-. (less (rdnn (n8)) (n0))) (-. (Ex Y, (less (n0) Y))) ### NotAnd 9 59 % 95.70/95.91 61. ((less (rdnn (n8)) (n0)) <=> ((-. (less (n0) (rdnn (n8)))) /\ ((n0) != (rdnn (n8))))) (-. (Ex X, (Ex Y, (less X Y)))) (-. (Ex Y, (less (n0) Y))) ((rdnn (n1)) != (rdnn (n8))) ((n0) = (rdnn (n1))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) ### Equiv 60 30 % 95.70/95.91 62. (All Y, ((less (rdnn (n8)) Y) <=> ((-. (less Y (rdnn (n8)))) /\ (Y != (rdnn (n8)))))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) ((n0) = (rdnn (n1))) ((rdnn (n1)) != (rdnn (n8))) (-. (Ex Y, (less (n0) Y))) (-. (Ex X, (Ex Y, (less X Y)))) ### All 61 % 95.70/95.91 63. (-. (less (rdnn (n8)) (rdnn (n8)))) (less (rdnn (n3)) (rdnn (n1))) (-. (Ex Y, (less (n0) Y))) ((n0) = (rdnn (n1))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) (All Y, ((less (rdnn (n8)) Y) <=> ((-. (less Y (rdnn (n8)))) /\ (Y != (rdnn (n8)))))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (-. (Ex X, (Ex Y, (less X Y)))) ### P-NotP 55 62 % 95.70/95.91 64. (less (rdnn (n8)) (rdnn (n8))) (-. (less (rdnn (n8)) (rdnn (n8)))) ### Axiom % 95.70/95.91 65. ((-. (less (rdnn (n8)) (rdnn (n8)))) /\ ((rdnn (n8)) != (rdnn (n8)))) (less (rdnn (n8)) (rdnn (n8))) ### And 64 % 95.70/95.91 66. ((less (rdnn (n8)) (rdnn (n8))) <=> ((-. (less (rdnn (n8)) (rdnn (n8)))) /\ ((rdnn (n8)) != (rdnn (n8))))) (-. (Ex X, (Ex Y, (less X Y)))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (All Y, ((less (rdnn (n8)) Y) <=> ((-. (less Y (rdnn (n8)))) /\ (Y != (rdnn (n8)))))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) ((n0) = (rdnn (n1))) (-. (Ex Y, (less (n0) Y))) (less (rdnn (n3)) (rdnn (n1))) ### Equiv 63 65 % 95.70/95.91 67. (less (rdnn (n3)) (rdnn (n1))) (-. (Ex Y, (less (n0) Y))) ((n0) = (rdnn (n1))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) (All Y, ((less (rdnn (n8)) Y) <=> ((-. (less Y (rdnn (n8)))) /\ (Y != (rdnn (n8)))))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (-. (Ex X, (Ex Y, (less X Y)))) ### All 66 % 95.70/95.91 68. (-. (-. (less (rdnn (n3)) (rdnn (n1))))) (-. (Ex X, (Ex Y, (less X Y)))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (All Y, ((less (rdnn (n8)) Y) <=> ((-. (less Y (rdnn (n8)))) /\ (Y != (rdnn (n8)))))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) ((n0) = (rdnn (n1))) (-. (Ex Y, (less (n0) Y))) ### NotNot 67 % 95.70/95.91 69. ((rdnn (n3)) = (rdnn (n1))) ((rdnn (n3)) != (rdnn (n1))) ### Axiom % 95.70/95.91 70. (-. (less (n1) (rdnn (n1)))) (less (n1) (rdnn (n3))) ((rdnn (n3)) = (rdnn (n1))) ### P-NotP 12 69 % 95.70/95.91 71. ((n1) = (rdnn (n1))) ((rdnn (n1)) != (n1)) ### Sym(=) % 95.70/95.91 72. ((-. (less (rdnn (n1)) (n1))) /\ ((rdnn (n1)) != (n1))) ((n1) = (rdnn (n1))) ### And 71 % 95.70/95.91 73. ((less (n1) (rdnn (n1))) <=> ((-. (less (rdnn (n1)) (n1))) /\ ((rdnn (n1)) != (n1)))) ((n1) = (rdnn (n1))) ((rdnn (n3)) = (rdnn (n1))) (less (n1) (rdnn (n3))) ### Equiv 70 72 % 95.70/95.91 74. (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (less (n1) (rdnn (n3))) ((rdnn (n3)) = (rdnn (n1))) ((n1) = (rdnn (n1))) ### All 73 % 95.70/95.91 75. (-. ((rdnn (n3)) != (rdnn (n1)))) ((n1) = (rdnn (n1))) (less (n1) (rdnn (n3))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) ### NotNot 74 % 95.70/95.91 76. (-. ((-. (less (rdnn (n3)) (rdnn (n1)))) /\ ((rdnn (n3)) != (rdnn (n1))))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (less (n1) (rdnn (n3))) ((n1) = (rdnn (n1))) (-. (Ex Y, (less (n0) Y))) ((n0) = (rdnn (n1))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) (All Y, ((less (rdnn (n8)) Y) <=> ((-. (less Y (rdnn (n8)))) /\ (Y != (rdnn (n8)))))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (-. (Ex X, (Ex Y, (less X Y)))) ### NotAnd 68 75 % 95.70/95.91 77. (less (n3) (n1)) (-. (less (n3) (n1))) ### Axiom % 95.70/95.91 78. (-. (Ex Y, (less (n3) Y))) (less (n3) (n1)) ### NotExists 77 % 95.70/95.91 79. (-. (-. (less (n3) (n1)))) (-. (Ex Y, (less (n3) Y))) ### NotNot 78 % 95.70/95.91 80. ((n3) != (n1)) ((n3) = (n1)) ### Axiom % 95.70/95.91 81. (-. ((n3) != (n1))) ((n3) != (n1)) ### NotNot 80 % 95.70/95.91 82. (-. ((-. (less (n3) (n1))) /\ ((n3) != (n1)))) ((n3) != (n1)) (-. (Ex Y, (less (n3) Y))) ### NotAnd 79 81 % 95.70/95.91 83. (less (n1) (n3)) (-. (less (n1) (n3))) ### Axiom % 95.70/95.91 84. (-. (Ex Y, (less (n1) Y))) (less (n1) (n3)) ### NotExists 83 % 95.70/95.91 85. ((less (n1) (n3)) <=> ((-. (less (n3) (n1))) /\ ((n3) != (n1)))) (-. (Ex Y, (less (n1) Y))) (-. (Ex Y, (less (n3) Y))) ((n3) != (n1)) ### Equiv 82 84 % 95.70/95.91 86. (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) ((n3) != (n1)) (-. (Ex Y, (less (n3) Y))) (-. (Ex Y, (less (n1) Y))) ### All 85 % 95.70/95.91 87. (-. (Ex X, (Ex Y, (less X Y)))) (-. (Ex Y, (less (n1) Y))) ((n3) != (n1)) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) ### NotExists 86 % 95.70/95.91 88. ((rdnn (n3)) != (rdnn (n1))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (-. (Ex Y, (less (n1) Y))) (-. (Ex X, (Ex Y, (less X Y)))) ### NotEqual 87 % 95.70/95.91 89. ((-. (less (rdnn (n3)) (rdnn (n1)))) /\ ((rdnn (n3)) != (rdnn (n1)))) (-. (Ex X, (Ex Y, (less X Y)))) (-. (Ex Y, (less (n1) Y))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) ### And 88 % 95.70/95.91 90. ((less (rdnn (n1)) (rdnn (n3))) <=> ((-. (less (rdnn (n3)) (rdnn (n1)))) /\ ((rdnn (n3)) != (rdnn (n1))))) (-. (Ex Y, (less (n1) Y))) (-. (Ex X, (Ex Y, (less X Y)))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (All Y, ((less (rdnn (n8)) Y) <=> ((-. (less Y (rdnn (n8)))) /\ (Y != (rdnn (n8)))))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) ((n0) = (rdnn (n1))) (-. (Ex Y, (less (n0) Y))) ((n1) = (rdnn (n1))) (less (n1) (rdnn (n3))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) ### Equiv 76 89 % 95.70/95.91 91. (All Y, ((less (rdnn (n1)) Y) <=> ((-. (less Y (rdnn (n1)))) /\ (Y != (rdnn (n1)))))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (less (n1) (rdnn (n3))) ((n1) = (rdnn (n1))) (-. (Ex Y, (less (n0) Y))) ((n0) = (rdnn (n1))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) (All Y, ((less (rdnn (n8)) Y) <=> ((-. (less Y (rdnn (n8)))) /\ (Y != (rdnn (n8)))))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (-. (Ex X, (Ex Y, (less X Y)))) (-. (Ex Y, (less (n1) Y))) ### All 90 % 95.70/95.91 92. (-. (Ex Y, (less (n1) Y))) (-. (Ex X, (Ex Y, (less X Y)))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) ((n0) = (rdnn (n1))) (-. (Ex Y, (less (n0) Y))) ((n1) = (rdnn (n1))) (less (n1) (rdnn (n3))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (All Y, ((less (rdnn (n1)) Y) <=> ((-. (less Y (rdnn (n1)))) /\ (Y != (rdnn (n1)))))) ### All 91 % 95.70/95.91 93. (-. (-. (less (n1) (rdnn (n3))))) (All Y, ((less (rdnn (n1)) Y) <=> ((-. (less Y (rdnn (n1)))) /\ (Y != (rdnn (n1)))))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) ((n1) = (rdnn (n1))) (-. (Ex Y, (less (n0) Y))) ((n0) = (rdnn (n1))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (-. (Ex X, (Ex Y, (less X Y)))) (-. (Ex Y, (less (n1) Y))) ### NotNot 92 % 95.70/95.91 94. (less (n7) (n1)) (-. (less (n7) (n1))) ### Axiom % 95.70/95.91 95. (-. (Ex Y, (less (n7) Y))) (less (n7) (n1)) ### NotExists 94 % 95.70/95.91 96. (-. (-. (less (n7) (n1)))) (-. (Ex Y, (less (n7) Y))) ### NotNot 95 % 95.70/95.91 97. ((n7) != (n1)) ((n7) = (n1)) ### Axiom % 95.70/95.91 98. (-. ((n7) != (n1))) ((n7) != (n1)) ### NotNot 97 % 95.70/95.91 99. (-. ((-. (less (n7) (n1))) /\ ((n7) != (n1)))) ((n7) != (n1)) (-. (Ex Y, (less (n7) Y))) ### NotAnd 96 98 % 95.70/95.91 100. (less (n1) (n7)) (-. (less (n1) (n7))) ### Axiom % 95.70/95.91 101. (-. (Ex Y, (less (n1) Y))) (less (n1) (n7)) ### NotExists 100 % 95.70/95.91 102. ((less (n1) (n7)) <=> ((-. (less (n7) (n1))) /\ ((n7) != (n1)))) (-. (Ex Y, (less (n1) Y))) (-. (Ex Y, (less (n7) Y))) ((n7) != (n1)) ### Equiv 99 101 % 95.70/95.91 103. (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) ((n7) != (n1)) (-. (Ex Y, (less (n7) Y))) (-. (Ex Y, (less (n1) Y))) ### All 102 % 95.70/95.91 104. (-. (Ex X, (Ex Y, (less X Y)))) (-. (Ex Y, (less (n1) Y))) ((n7) != (n1)) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) ### NotExists 103 % 95.70/95.91 105. ((rdnn (n7)) != (rdnn (n1))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (-. (Ex Y, (less (n1) Y))) (-. (Ex X, (Ex Y, (less X Y)))) ### NotEqual 104 % 95.70/95.91 106. ((rdnn (n3)) != (rdnn (n3))) ### Refl(=) % 95.70/95.91 107. (-. (less (rdnn (n1)) (rdnn (n3)))) (less (rdnn (n7)) (rdnn (n3))) (-. (Ex X, (Ex Y, (less X Y)))) (-. (Ex Y, (less (n1) Y))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) ### P-NotP 105 106 % 95.70/95.91 108. ((less (rdnn (n1)) (rdnn (n3))) <=> ((-. (less (rdnn (n3)) (rdnn (n1)))) /\ ((rdnn (n3)) != (rdnn (n1))))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (-. (Ex Y, (less (n1) Y))) (-. (Ex X, (Ex Y, (less X Y)))) (less (rdnn (n7)) (rdnn (n3))) ### Equiv 107 89 % 95.70/95.91 109. (All Y, ((less (rdnn (n1)) Y) <=> ((-. (less Y (rdnn (n1)))) /\ (Y != (rdnn (n1)))))) (less (rdnn (n7)) (rdnn (n3))) (-. (Ex X, (Ex Y, (less X Y)))) (-. (Ex Y, (less (n1) Y))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) ### All 108 % 95.70/95.91 110. (-. (-. (less (rdnn (n7)) (rdnn (n3))))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (-. (Ex Y, (less (n1) Y))) (-. (Ex X, (Ex Y, (less X Y)))) (All Y, ((less (rdnn (n1)) Y) <=> ((-. (less Y (rdnn (n1)))) /\ (Y != (rdnn (n1)))))) ### NotNot 109 % 95.70/95.91 111. ((nn7) != (nn7)) ### NotEqual % 95.70/95.91 112. ((rdnn (n7)) != (rdnn (n3))) ((rdnn (n7)) = (rdnn (n3))) ### Axiom % 95.70/95.91 113. (-. ((rdnn (n7)) != (rdnn (n3)))) ((rdnn (n7)) != (rdnn (n3))) ### NotNot 112 % 95.70/95.91 114. (-. ((-. (less (rdnn (n7)) (rdnn (n3)))) /\ ((rdnn (n7)) != (rdnn (n3))))) ((rdnn (n7)) != (rdnn (n3))) (All Y, ((less (rdnn (n1)) Y) <=> ((-. (less Y (rdnn (n1)))) /\ (Y != (rdnn (n1)))))) (-. (Ex X, (Ex Y, (less X Y)))) (-. (Ex Y, (less (n1) Y))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) ### NotAnd 110 113 % 95.70/95.91 115. (less (n8) (n7)) (-. (less (n8) (n7))) ### Axiom % 95.70/95.91 116. (-. (Ex Y, (less (n8) Y))) (less (n8) (n7)) ### NotExists 115 % 95.70/95.91 117. (-. (-. (less (n8) (n7)))) (-. (Ex Y, (less (n8) Y))) ### NotNot 116 % 95.70/95.91 118. ((n7) != (n8)) ((n8) = (n7)) ### Sym(=) % 95.70/95.91 119. (-. ((n8) != (n7))) ((n7) != (n8)) ### NotNot 118 % 95.70/95.91 120. (-. ((-. (less (n8) (n7))) /\ ((n8) != (n7)))) ((n7) != (n8)) (-. (Ex Y, (less (n8) Y))) ### NotAnd 117 119 % 95.70/95.91 121. (less (n7) (n8)) (-. (less (n7) (n8))) ### Axiom % 95.70/95.91 122. (-. (Ex Y, (less (n7) Y))) (less (n7) (n8)) ### NotExists 121 % 95.70/95.91 123. ((less (n7) (n8)) <=> ((-. (less (n8) (n7))) /\ ((n8) != (n7)))) (-. (Ex Y, (less (n7) Y))) (-. (Ex Y, (less (n8) Y))) ((n7) != (n8)) ### Equiv 120 122 % 95.70/95.91 124. (All Y, ((less (n7) Y) <=> ((-. (less Y (n7))) /\ (Y != (n7))))) ((n7) != (n8)) (-. (Ex Y, (less (n8) Y))) (-. (Ex Y, (less (n7) Y))) ### All 123 % 95.70/95.91 125. (-. (Ex X, (Ex Y, (less X Y)))) (-. (Ex Y, (less (n7) Y))) ((n7) != (n8)) (All Y, ((less (n7) Y) <=> ((-. (less Y (n7))) /\ (Y != (n7))))) ### NotExists 124 % 95.70/95.91 126. (All Y, ((less (n7) Y) <=> ((-. (less Y (n7))) /\ (Y != (n7))))) ((n7) != (n8)) (-. (Ex X, (Ex Y, (less X Y)))) ### NotExists 125 % 95.70/95.91 127. (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (-. (Ex X, (Ex Y, (less X Y)))) ((n7) != (n8)) ### All 126 % 95.70/95.91 128. ((rdnn (n7)) != (rdnn (n8))) (-. (Ex X, (Ex Y, (less X Y)))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) ### NotEqual 127 % 95.70/95.91 129. (-. (less (rdnn (n1)) (rdnn (n8)))) (less (rdnn (n3)) (rdnn (n7))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (-. (Ex X, (Ex Y, (less X Y)))) (-. (Ex Y, (less (n1) Y))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) ### P-NotP 88 128 % 95.70/95.91 130. ((less (rdnn (n3)) (rdnn (n7))) <=> ((-. (less (rdnn (n7)) (rdnn (n3)))) /\ ((rdnn (n7)) != (rdnn (n3))))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (-. (less (rdnn (n1)) (rdnn (n8)))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (-. (Ex Y, (less (n1) Y))) (-. (Ex X, (Ex Y, (less X Y)))) (All Y, ((less (rdnn (n1)) Y) <=> ((-. (less Y (rdnn (n1)))) /\ (Y != (rdnn (n1)))))) ((rdnn (n7)) != (rdnn (n3))) ### Equiv 114 129 % 95.70/95.91 131. (All Y, ((less (rdnn (n3)) Y) <=> ((-. (less Y (rdnn (n3)))) /\ (Y != (rdnn (n3)))))) ((rdnn (n7)) != (rdnn (n3))) (All Y, ((less (rdnn (n1)) Y) <=> ((-. (less Y (rdnn (n1)))) /\ (Y != (rdnn (n1)))))) (-. (Ex X, (Ex Y, (less X Y)))) (-. (Ex Y, (less (n1) Y))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (-. (less (rdnn (n1)) (rdnn (n8)))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) ### All 130 % 95.70/95.91 132. ((rdn_neg (rdnn (n7))) != (rdn_neg (rdnn (n3)))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (-. (less (rdnn (n1)) (rdnn (n8)))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (-. (Ex Y, (less (n1) Y))) (-. (Ex X, (Ex Y, (less X Y)))) (All Y, ((less (rdnn (n1)) Y) <=> ((-. (less Y (rdnn (n1)))) /\ (Y != (rdnn (n1)))))) (All Y, ((less (rdnn (n3)) Y) <=> ((-. (less Y (rdnn (n3)))) /\ (Y != (rdnn (n3)))))) ### NotEqual 131 % 95.70/95.91 133. (-. (rdn_translate (nn7) (rdn_neg (rdnn (n3))))) (rdn_translate (nn7) (rdn_neg (rdnn (n7)))) (All Y, ((less (rdnn (n3)) Y) <=> ((-. (less Y (rdnn (n3)))) /\ (Y != (rdnn (n3)))))) (All Y, ((less (rdnn (n1)) Y) <=> ((-. (less Y (rdnn (n1)))) /\ (Y != (rdnn (n1)))))) (-. (Ex X, (Ex Y, (less X Y)))) (-. (Ex Y, (less (n1) Y))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (-. (less (rdnn (n1)) (rdnn (n8)))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) ### P-NotP 111 132 % 95.70/95.91 134. ((nn3) != (nn3)) ### NotEqual % 95.70/95.91 135. ((rdnn (n7)) = (rdnn (n3))) ((rdnn (n3)) != (rdnn (n7))) ### Sym(=) % 95.70/95.91 136. ((rdn_neg (rdnn (n3))) != (rdn_neg (rdnn (n7)))) ((rdnn (n7)) = (rdnn (n3))) ### NotEqual 135 % 95.70/95.91 137. (-. (rdn_translate (nn3) (rdn_neg (rdnn (n7))))) (rdn_translate (nn3) (rdn_neg (rdnn (n3)))) ((rdnn (n7)) = (rdnn (n3))) ### P-NotP 134 136 % 95.70/95.91 138. (less (n7) (n0)) (-. (less (n7) (n0))) ### Axiom % 95.70/95.91 139. (-. (Ex Y, (less (n7) Y))) (less (n7) (n0)) ### NotExists 138 % 95.70/95.91 140. (-. (-. (less (n7) (n0)))) (-. (Ex Y, (less (n7) Y))) ### NotNot 139 % 95.70/95.91 141. ((n0) != (n7)) ((n7) = (n0)) ### Sym(=) % 95.70/95.91 142. (-. ((n7) != (n0))) ((n0) != (n7)) ### NotNot 141 % 95.70/95.91 143. (-. ((-. (less (n7) (n0))) /\ ((n7) != (n0)))) ((n0) != (n7)) (-. (Ex Y, (less (n7) Y))) ### NotAnd 140 142 % 95.70/95.91 144. (less (n0) (n7)) (-. (less (n0) (n7))) ### Axiom % 95.70/95.91 145. (-. (Ex Y, (less (n0) Y))) (less (n0) (n7)) ### NotExists 144 % 95.70/95.91 146. ((less (n0) (n7)) <=> ((-. (less (n7) (n0))) /\ ((n7) != (n0)))) (-. (Ex Y, (less (n0) Y))) (-. (Ex Y, (less (n7) Y))) ((n0) != (n7)) ### Equiv 143 145 % 95.70/95.91 147. (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) ((n0) != (n7)) (-. (Ex Y, (less (n7) Y))) (-. (Ex Y, (less (n0) Y))) ### All 146 % 95.70/95.91 148. (-. (Ex X, (Ex Y, (less X Y)))) (-. (Ex Y, (less (n0) Y))) ((n0) != (n7)) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) ### NotExists 147 % 95.70/95.91 149. ((rdnn (n0)) != (rdnn (n7))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) (-. (Ex Y, (less (n0) Y))) (-. (Ex X, (Ex Y, (less X Y)))) ### NotEqual 148 % 95.70/95.91 150. (-. (less (rdnn (n3)) (n1))) (less (rdnn (n3)) (n1)) ### Axiom % 95.70/95.91 151. (-. (-. (less (rdnn (n3)) (n1)))) (-. (less (rdnn (n3)) (n1))) ### NotNot 150 % 95.70/95.91 152. (-. ((rdnn (n3)) != (n1))) ((rdnn (n3)) != (n1)) ### Axiom % 95.70/95.91 153. ((rdnn (n1)) != (rdnn (n1))) ### Refl(=) % 95.70/95.91 154. ((rdnn (n1)) != (rdnn (n3))) ((n1) = (rdnn (n1))) (-. ((rdnn (n3)) != (n1))) ### Trans-sym 152 153 % 95.70/95.91 155. (-. ((-. (less (rdnn (n3)) (n1))) /\ ((rdnn (n3)) != (n1)))) ((n1) = (rdnn (n1))) ((rdnn (n1)) != (rdnn (n3))) (-. (less (rdnn (n3)) (n1))) ### NotAnd 151 154 % 95.70/95.91 156. ((n1) = (rdnn (n3))) ((rdnn (n3)) != (n1)) ### Sym(=) % 95.70/95.91 157. ((-. (less (rdnn (n3)) (n1))) /\ ((rdnn (n3)) != (n1))) ((n1) = (rdnn (n3))) ### And 156 % 95.70/95.91 158. ((less (n1) (rdnn (n3))) <=> ((-. (less (rdnn (n3)) (n1))) /\ ((rdnn (n3)) != (n1)))) ((n1) = (rdnn (n3))) (-. (less (rdnn (n3)) (n1))) ((rdnn (n1)) != (rdnn (n3))) ((n1) = (rdnn (n1))) ### Equiv 155 157 % 95.70/95.91 159. (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) ((n1) = (rdnn (n1))) ((rdnn (n1)) != (rdnn (n3))) (-. (less (rdnn (n3)) (n1))) ((n1) = (rdnn (n3))) ### All 158 % 95.70/95.91 160. (-. (rdn_positive_less (rdnn (n7)) (rdnn (n3)))) (rdn_positive_less (rdnn (n0)) (rdnn (n1))) ((n1) = (rdnn (n3))) (-. (less (rdnn (n3)) (n1))) ((n1) = (rdnn (n1))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (-. (Ex X, (Ex Y, (less X Y)))) (-. (Ex Y, (less (n0) Y))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) ### P-NotP 149 159 % 95.70/95.91 161. (less (nn7) (nn3)) (-. (less (nn7) (nn3))) ### Axiom % 95.70/95.91 162. (-. (Ex Y, (less (nn7) Y))) (less (nn7) (nn3)) ### NotExists 161 % 95.70/95.91 163. (-. (Ex X, (Ex Y, (less X Y)))) (less (nn7) (nn3)) ### NotExists 162 % 95.70/95.91 164. (((rdn_translate (nn7) (rdn_neg (rdnn (n3)))) /\ ((rdn_translate (nn3) (rdn_neg (rdnn (n7)))) /\ (rdn_positive_less (rdnn (n7)) (rdnn (n3))))) => (less (nn7) (nn3))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) (-. (Ex Y, (less (n0) Y))) ((n1) = (rdnn (n1))) (-. (less (rdnn (n3)) (n1))) ((n1) = (rdnn (n3))) (rdn_positive_less (rdnn (n0)) (rdnn (n1))) ((rdnn (n7)) = (rdnn (n3))) (rdn_translate (nn3) (rdn_neg (rdnn (n3)))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (-. (less (rdnn (n1)) (rdnn (n8)))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (-. (Ex Y, (less (n1) Y))) (-. (Ex X, (Ex Y, (less X Y)))) (All Y, ((less (rdnn (n1)) Y) <=> ((-. (less Y (rdnn (n1)))) /\ (Y != (rdnn (n1)))))) (All Y, ((less (rdnn (n3)) Y) <=> ((-. (less Y (rdnn (n3)))) /\ (Y != (rdnn (n3)))))) (rdn_translate (nn7) (rdn_neg (rdnn (n7)))) ### DisjTree 133 137 160 163 % 95.70/95.91 165. (All RDN_Y, (((rdn_translate (nn7) (rdn_neg (rdnn (n3)))) /\ ((rdn_translate (nn3) (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y (rdnn (n3))))) => (less (nn7) (nn3)))) (rdn_translate (nn7) (rdn_neg (rdnn (n7)))) (All Y, ((less (rdnn (n3)) Y) <=> ((-. (less Y (rdnn (n3)))) /\ (Y != (rdnn (n3)))))) (All Y, ((less (rdnn (n1)) Y) <=> ((-. (less Y (rdnn (n1)))) /\ (Y != (rdnn (n1)))))) (-. (Ex X, (Ex Y, (less X Y)))) (-. (Ex Y, (less (n1) Y))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (-. (less (rdnn (n1)) (rdnn (n8)))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (rdn_translate (nn3) (rdn_neg (rdnn (n3)))) ((rdnn (n7)) = (rdnn (n3))) (rdn_positive_less (rdnn (n0)) (rdnn (n1))) ((n1) = (rdnn (n3))) (-. (less (rdnn (n3)) (n1))) ((n1) = (rdnn (n1))) (-. (Ex Y, (less (n0) Y))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) ### All 164 % 95.70/95.91 166. (All RDN_X, (All RDN_Y, (((rdn_translate (nn7) (rdn_neg RDN_X)) /\ ((rdn_translate (nn3) (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y RDN_X))) => (less (nn7) (nn3))))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) (-. (Ex Y, (less (n0) Y))) ((n1) = (rdnn (n1))) (-. (less (rdnn (n3)) (n1))) ((n1) = (rdnn (n3))) (rdn_positive_less (rdnn (n0)) (rdnn (n1))) ((rdnn (n7)) = (rdnn (n3))) (rdn_translate (nn3) (rdn_neg (rdnn (n3)))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (-. (less (rdnn (n1)) (rdnn (n8)))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (-. (Ex Y, (less (n1) Y))) (-. (Ex X, (Ex Y, (less X Y)))) (All Y, ((less (rdnn (n1)) Y) <=> ((-. (less Y (rdnn (n1)))) /\ (Y != (rdnn (n1)))))) (All Y, ((less (rdnn (n3)) Y) <=> ((-. (less Y (rdnn (n3)))) /\ (Y != (rdnn (n3)))))) (rdn_translate (nn7) (rdn_neg (rdnn (n7)))) ### All 165 % 95.70/95.91 167. (-. ((rdnn (n7)) != (rdnn (n3)))) (rdn_translate (nn7) (rdn_neg (rdnn (n7)))) (All Y, ((less (rdnn (n3)) Y) <=> ((-. (less Y (rdnn (n3)))) /\ (Y != (rdnn (n3)))))) (All Y, ((less (rdnn (n1)) Y) <=> ((-. (less Y (rdnn (n1)))) /\ (Y != (rdnn (n1)))))) (-. (Ex X, (Ex Y, (less X Y)))) (-. (Ex Y, (less (n1) Y))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (-. (less (rdnn (n1)) (rdnn (n8)))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (rdn_translate (nn3) (rdn_neg (rdnn (n3)))) (rdn_positive_less (rdnn (n0)) (rdnn (n1))) ((n1) = (rdnn (n3))) (-. (less (rdnn (n3)) (n1))) ((n1) = (rdnn (n1))) (-. (Ex Y, (less (n0) Y))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) (All RDN_X, (All RDN_Y, (((rdn_translate (nn7) (rdn_neg RDN_X)) /\ ((rdn_translate (nn3) (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y RDN_X))) => (less (nn7) (nn3))))) ### NotNot 166 % 95.70/95.91 168. (-. ((-. (less (rdnn (n7)) (rdnn (n3)))) /\ ((rdnn (n7)) != (rdnn (n3))))) (All RDN_X, (All RDN_Y, (((rdn_translate (nn7) (rdn_neg RDN_X)) /\ ((rdn_translate (nn3) (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y RDN_X))) => (less (nn7) (nn3))))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) (-. (Ex Y, (less (n0) Y))) ((n1) = (rdnn (n1))) (-. (less (rdnn (n3)) (n1))) ((n1) = (rdnn (n3))) (rdn_positive_less (rdnn (n0)) (rdnn (n1))) (rdn_translate (nn3) (rdn_neg (rdnn (n3)))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (-. (less (rdnn (n1)) (rdnn (n8)))) (All Y, ((less (rdnn (n3)) Y) <=> ((-. (less Y (rdnn (n3)))) /\ (Y != (rdnn (n3)))))) (rdn_translate (nn7) (rdn_neg (rdnn (n7)))) (All Y, ((less (rdnn (n1)) Y) <=> ((-. (less Y (rdnn (n1)))) /\ (Y != (rdnn (n1)))))) (-. (Ex X, (Ex Y, (less X Y)))) (-. (Ex Y, (less (n1) Y))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) ### NotAnd 110 167 % 95.70/95.91 169. ((less (rdnn (n3)) (rdnn (n7))) <=> ((-. (less (rdnn (n7)) (rdnn (n3)))) /\ ((rdnn (n7)) != (rdnn (n3))))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (-. (Ex Y, (less (n1) Y))) (-. (Ex X, (Ex Y, (less X Y)))) (All Y, ((less (rdnn (n1)) Y) <=> ((-. (less Y (rdnn (n1)))) /\ (Y != (rdnn (n1)))))) (rdn_translate (nn7) (rdn_neg (rdnn (n7)))) (All Y, ((less (rdnn (n3)) Y) <=> ((-. (less Y (rdnn (n3)))) /\ (Y != (rdnn (n3)))))) (-. (less (rdnn (n1)) (rdnn (n8)))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (rdn_translate (nn3) (rdn_neg (rdnn (n3)))) (rdn_positive_less (rdnn (n0)) (rdnn (n1))) ((n1) = (rdnn (n3))) (-. (less (rdnn (n3)) (n1))) ((n1) = (rdnn (n1))) (-. (Ex Y, (less (n0) Y))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) (All RDN_X, (All RDN_Y, (((rdn_translate (nn7) (rdn_neg RDN_X)) /\ ((rdn_translate (nn3) (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y RDN_X))) => (less (nn7) (nn3))))) ### Equiv 168 129 % 95.70/95.91 170. (All RDN_X, (All RDN_Y, (((rdn_translate (nn7) (rdn_neg RDN_X)) /\ ((rdn_translate (nn3) (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y RDN_X))) => (less (nn7) (nn3))))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) (-. (Ex Y, (less (n0) Y))) ((n1) = (rdnn (n1))) (-. (less (rdnn (n3)) (n1))) ((n1) = (rdnn (n3))) (rdn_positive_less (rdnn (n0)) (rdnn (n1))) (rdn_translate (nn3) (rdn_neg (rdnn (n3)))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (-. (less (rdnn (n1)) (rdnn (n8)))) (All Y, ((less (rdnn (n3)) Y) <=> ((-. (less Y (rdnn (n3)))) /\ (Y != (rdnn (n3)))))) (rdn_translate (nn7) (rdn_neg (rdnn (n7)))) (All Y, ((less (rdnn (n1)) Y) <=> ((-. (less Y (rdnn (n1)))) /\ (Y != (rdnn (n1)))))) (-. (Ex X, (Ex Y, (less X Y)))) (-. (Ex Y, (less (n1) Y))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) ### All 169 % 95.70/95.91 171. (All Y, (All RDN_X, (All RDN_Y, (((rdn_translate (nn7) (rdn_neg RDN_X)) /\ ((rdn_translate Y (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y RDN_X))) => (less (nn7) Y))))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (-. (Ex Y, (less (n1) Y))) (-. (Ex X, (Ex Y, (less X Y)))) (All Y, ((less (rdnn (n1)) Y) <=> ((-. (less Y (rdnn (n1)))) /\ (Y != (rdnn (n1)))))) (rdn_translate (nn7) (rdn_neg (rdnn (n7)))) (All Y, ((less (rdnn (n3)) Y) <=> ((-. (less Y (rdnn (n3)))) /\ (Y != (rdnn (n3)))))) (-. (less (rdnn (n1)) (rdnn (n8)))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (rdn_translate (nn3) (rdn_neg (rdnn (n3)))) (rdn_positive_less (rdnn (n0)) (rdnn (n1))) ((n1) = (rdnn (n3))) (-. (less (rdnn (n3)) (n1))) ((n1) = (rdnn (n1))) (-. (Ex Y, (less (n0) Y))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) ### All 170 % 95.70/95.91 172. (less (n8) (n1)) (-. (less (n8) (n1))) ### Axiom % 95.70/95.91 173. (-. (Ex Y, (less (n8) Y))) (less (n8) (n1)) ### NotExists 172 % 95.70/95.91 174. (-. (-. (less (n8) (n1)))) (-. (Ex Y, (less (n8) Y))) ### NotNot 173 % 95.70/95.91 175. ((n8) != (n1)) ((n8) = (n1)) ### Axiom % 95.70/95.91 176. (-. ((n8) != (n1))) ((n8) != (n1)) ### NotNot 175 % 95.70/95.91 177. (-. ((-. (less (n8) (n1))) /\ ((n8) != (n1)))) ((n8) != (n1)) (-. (Ex Y, (less (n8) Y))) ### NotAnd 174 176 % 95.70/95.91 178. (less (n1) (n8)) (-. (less (n1) (n8))) ### Axiom % 95.70/95.91 179. (-. (Ex Y, (less (n1) Y))) (less (n1) (n8)) ### NotExists 178 % 95.70/95.91 180. ((less (n1) (n8)) <=> ((-. (less (n8) (n1))) /\ ((n8) != (n1)))) (-. (Ex Y, (less (n1) Y))) (-. (Ex Y, (less (n8) Y))) ((n8) != (n1)) ### Equiv 177 179 % 95.70/95.91 181. (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) ((n8) != (n1)) (-. (Ex Y, (less (n8) Y))) (-. (Ex Y, (less (n1) Y))) ### All 180 % 95.70/95.91 182. (-. (Ex X, (Ex Y, (less X Y)))) (-. (Ex Y, (less (n1) Y))) ((n8) != (n1)) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) ### NotExists 181 % 95.70/95.91 183. ((rdnn (n8)) != (rdnn (n1))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (-. (Ex Y, (less (n1) Y))) (-. (Ex X, (Ex Y, (less X Y)))) ### NotEqual 182 % 95.70/95.91 184. ((-. (less (rdnn (n8)) (rdnn (n1)))) /\ ((rdnn (n8)) != (rdnn (n1)))) (-. (Ex X, (Ex Y, (less X Y)))) (-. (Ex Y, (less (n1) Y))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) ### And 183 % 95.70/95.91 185. ((less (rdnn (n1)) (rdnn (n8))) <=> ((-. (less (rdnn (n8)) (rdnn (n1)))) /\ ((rdnn (n8)) != (rdnn (n1))))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) (-. (Ex Y, (less (n0) Y))) ((n1) = (rdnn (n1))) (-. (less (rdnn (n3)) (n1))) ((n1) = (rdnn (n3))) (rdn_positive_less (rdnn (n0)) (rdnn (n1))) (rdn_translate (nn3) (rdn_neg (rdnn (n3)))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (All Y, ((less (rdnn (n3)) Y) <=> ((-. (less Y (rdnn (n3)))) /\ (Y != (rdnn (n3)))))) (rdn_translate (nn7) (rdn_neg (rdnn (n7)))) (All Y, ((less (rdnn (n1)) Y) <=> ((-. (less Y (rdnn (n1)))) /\ (Y != (rdnn (n1)))))) (-. (Ex X, (Ex Y, (less X Y)))) (-. (Ex Y, (less (n1) Y))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (All Y, (All RDN_X, (All RDN_Y, (((rdn_translate (nn7) (rdn_neg RDN_X)) /\ ((rdn_translate Y (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y RDN_X))) => (less (nn7) Y))))) ### Equiv 171 184 % 95.70/95.91 186. (All Y, (All RDN_X, (All RDN_Y, (((rdn_translate (nn7) (rdn_neg RDN_X)) /\ ((rdn_translate Y (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y RDN_X))) => (less (nn7) Y))))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (-. (Ex Y, (less (n1) Y))) (-. (Ex X, (Ex Y, (less X Y)))) (All Y, ((less (rdnn (n1)) Y) <=> ((-. (less Y (rdnn (n1)))) /\ (Y != (rdnn (n1)))))) (rdn_translate (nn7) (rdn_neg (rdnn (n7)))) (All Y, ((less (rdnn (n3)) Y) <=> ((-. (less Y (rdnn (n3)))) /\ (Y != (rdnn (n3)))))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (rdn_translate (nn3) (rdn_neg (rdnn (n3)))) (rdn_positive_less (rdnn (n0)) (rdnn (n1))) ((n1) = (rdnn (n3))) (-. (less (rdnn (n3)) (n1))) ((n1) = (rdnn (n1))) (-. (Ex Y, (less (n0) Y))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) ### All 185 % 95.70/95.91 187. (All X, (All Y, (All RDN_X, (All RDN_Y, (((rdn_translate X (rdn_neg RDN_X)) /\ ((rdn_translate Y (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y RDN_X))) => (less X Y)))))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) (-. (Ex Y, (less (n0) Y))) ((n1) = (rdnn (n1))) (-. (less (rdnn (n3)) (n1))) ((n1) = (rdnn (n3))) (rdn_positive_less (rdnn (n0)) (rdnn (n1))) (rdn_translate (nn3) (rdn_neg (rdnn (n3)))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (All Y, ((less (rdnn (n3)) Y) <=> ((-. (less Y (rdnn (n3)))) /\ (Y != (rdnn (n3)))))) (rdn_translate (nn7) (rdn_neg (rdnn (n7)))) (All Y, ((less (rdnn (n1)) Y) <=> ((-. (less Y (rdnn (n1)))) /\ (Y != (rdnn (n1)))))) (-. (Ex X, (Ex Y, (less X Y)))) (-. (Ex Y, (less (n1) Y))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) ### All 186 % 95.70/95.91 188. (-. ((n1) != (rdnn (n3)))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (-. (Ex Y, (less (n1) Y))) (-. (Ex X, (Ex Y, (less X Y)))) (All Y, ((less (rdnn (n1)) Y) <=> ((-. (less Y (rdnn (n1)))) /\ (Y != (rdnn (n1)))))) (rdn_translate (nn7) (rdn_neg (rdnn (n7)))) (All Y, ((less (rdnn (n3)) Y) <=> ((-. (less Y (rdnn (n3)))) /\ (Y != (rdnn (n3)))))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (rdn_translate (nn3) (rdn_neg (rdnn (n3)))) (rdn_positive_less (rdnn (n0)) (rdnn (n1))) (-. (less (rdnn (n3)) (n1))) ((n1) = (rdnn (n1))) (-. (Ex Y, (less (n0) Y))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) (All X, (All Y, (All RDN_X, (All RDN_Y, (((rdn_translate X (rdn_neg RDN_X)) /\ ((rdn_translate Y (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y RDN_X))) => (less X Y)))))) ### NotNot 187 % 95.70/95.91 189. (-. ((-. (less (n1) (rdnn (n3)))) /\ ((n1) != (rdnn (n3))))) (All X, (All Y, (All RDN_X, (All RDN_Y, (((rdn_translate X (rdn_neg RDN_X)) /\ ((rdn_translate Y (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y RDN_X))) => (less X Y)))))) (-. (less (rdnn (n3)) (n1))) (rdn_positive_less (rdnn (n0)) (rdnn (n1))) (rdn_translate (nn3) (rdn_neg (rdnn (n3)))) (All Y, ((less (rdnn (n3)) Y) <=> ((-. (less Y (rdnn (n3)))) /\ (Y != (rdnn (n3)))))) (rdn_translate (nn7) (rdn_neg (rdnn (n7)))) (-. (Ex Y, (less (n1) Y))) (-. (Ex X, (Ex Y, (less X Y)))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) ((n0) = (rdnn (n1))) (-. (Ex Y, (less (n0) Y))) ((n1) = (rdnn (n1))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (All Y, ((less (rdnn (n1)) Y) <=> ((-. (less Y (rdnn (n1)))) /\ (Y != (rdnn (n1)))))) ### NotAnd 93 188 % 95.70/95.91 190. (-. (less (rdnn (n1)) (n1))) (less (rdnn (n3)) (n1)) (-. (Ex X, (Ex Y, (less X Y)))) (-. (Ex Y, (less (n1) Y))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) ### P-NotP 88 12 % 95.70/95.91 191. ((less (rdnn (n3)) (n1)) <=> ((-. (less (n1) (rdnn (n3)))) /\ ((n1) != (rdnn (n3))))) (-. (less (rdnn (n1)) (n1))) (All Y, ((less (rdnn (n1)) Y) <=> ((-. (less Y (rdnn (n1)))) /\ (Y != (rdnn (n1)))))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) ((n1) = (rdnn (n1))) (-. (Ex Y, (less (n0) Y))) ((n0) = (rdnn (n1))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (-. (Ex X, (Ex Y, (less X Y)))) (-. (Ex Y, (less (n1) Y))) (rdn_translate (nn7) (rdn_neg (rdnn (n7)))) (All Y, ((less (rdnn (n3)) Y) <=> ((-. (less Y (rdnn (n3)))) /\ (Y != (rdnn (n3)))))) (rdn_translate (nn3) (rdn_neg (rdnn (n3)))) (rdn_positive_less (rdnn (n0)) (rdnn (n1))) (All X, (All Y, (All RDN_X, (All RDN_Y, (((rdn_translate X (rdn_neg RDN_X)) /\ ((rdn_translate Y (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y RDN_X))) => (less X Y)))))) ### Equiv 189 190 % 95.70/95.91 192. (All X, (All Y, (All RDN_X, (All RDN_Y, (((rdn_translate X (rdn_neg RDN_X)) /\ ((rdn_translate Y (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y RDN_X))) => (less X Y)))))) (rdn_positive_less (rdnn (n0)) (rdnn (n1))) (rdn_translate (nn3) (rdn_neg (rdnn (n3)))) (All Y, ((less (rdnn (n3)) Y) <=> ((-. (less Y (rdnn (n3)))) /\ (Y != (rdnn (n3)))))) (rdn_translate (nn7) (rdn_neg (rdnn (n7)))) (-. (Ex Y, (less (n1) Y))) (-. (Ex X, (Ex Y, (less X Y)))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) ((n0) = (rdnn (n1))) (-. (Ex Y, (less (n0) Y))) ((n1) = (rdnn (n1))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (All Y, ((less (rdnn (n1)) Y) <=> ((-. (less Y (rdnn (n1)))) /\ (Y != (rdnn (n1)))))) (-. (less (rdnn (n1)) (n1))) ### All 191 % 95.70/95.91 193. (-. (less (rdnn (n1)) (n1))) (All Y, ((less (rdnn (n1)) Y) <=> ((-. (less Y (rdnn (n1)))) /\ (Y != (rdnn (n1)))))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) ((n1) = (rdnn (n1))) (-. (Ex Y, (less (n0) Y))) ((n0) = (rdnn (n1))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (-. (Ex X, (Ex Y, (less X Y)))) (-. (Ex Y, (less (n1) Y))) (rdn_translate (nn7) (rdn_neg (rdnn (n7)))) (rdn_translate (nn3) (rdn_neg (rdnn (n3)))) (rdn_positive_less (rdnn (n0)) (rdnn (n1))) (All X, (All Y, (All RDN_X, (All RDN_Y, (((rdn_translate X (rdn_neg RDN_X)) /\ ((rdn_translate Y (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y RDN_X))) => (less X Y)))))) ### All 192 % 95.70/95.91 194. (-. ((n1) != (rdnn (n1)))) (All X, (All Y, (All RDN_X, (All RDN_Y, (((rdn_translate X (rdn_neg RDN_X)) /\ ((rdn_translate Y (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y RDN_X))) => (less X Y)))))) (rdn_positive_less (rdnn (n0)) (rdnn (n1))) (rdn_translate (nn3) (rdn_neg (rdnn (n3)))) (rdn_translate (nn7) (rdn_neg (rdnn (n7)))) (-. (Ex Y, (less (n1) Y))) (-. (Ex X, (Ex Y, (less X Y)))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) ((n0) = (rdnn (n1))) (-. (Ex Y, (less (n0) Y))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (All Y, ((less (rdnn (n1)) Y) <=> ((-. (less Y (rdnn (n1)))) /\ (Y != (rdnn (n1)))))) (-. (less (rdnn (n1)) (n1))) ### NotNot 193 % 95.70/95.91 195. (-. ((-. (less (n1) (rdnn (n1)))) /\ ((n1) != (rdnn (n1))))) (-. (less (rdnn (n1)) (n1))) (All Y, ((less (rdnn (n1)) Y) <=> ((-. (less Y (rdnn (n1)))) /\ (Y != (rdnn (n1)))))) (rdn_translate (nn7) (rdn_neg (rdnn (n7)))) (rdn_translate (nn3) (rdn_neg (rdnn (n3)))) (rdn_positive_less (rdnn (n0)) (rdnn (n1))) (All X, (All Y, (All RDN_X, (All RDN_Y, (((rdn_translate X (rdn_neg RDN_X)) /\ ((rdn_translate Y (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y RDN_X))) => (less X Y)))))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (-. (Ex Y, (less (n1) Y))) (-. (Ex X, (Ex Y, (less X Y)))) (-. (Ex Y, (less (n0) Y))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) ((n0) = (rdnn (n1))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) ### NotAnd 41 194 % 95.70/95.91 196. (less (rdnn (n1)) (n1)) (-. (less (rdnn (n1)) (n1))) ### Axiom % 95.70/95.91 197. (-. (Ex Y, (less (rdnn (n1)) Y))) (less (rdnn (n1)) (n1)) ### NotExists 196 % 95.70/95.91 198. (-. (Ex X, (Ex Y, (less X Y)))) (less (rdnn (n1)) (n1)) ### NotExists 197 % 95.70/95.91 199. ((less (rdnn (n1)) (n1)) <=> ((-. (less (n1) (rdnn (n1)))) /\ ((n1) != (rdnn (n1))))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) ((n0) = (rdnn (n1))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (-. (Ex Y, (less (n0) Y))) (-. (Ex X, (Ex Y, (less X Y)))) (-. (Ex Y, (less (n1) Y))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (All X, (All Y, (All RDN_X, (All RDN_Y, (((rdn_translate X (rdn_neg RDN_X)) /\ ((rdn_translate Y (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y RDN_X))) => (less X Y)))))) (rdn_positive_less (rdnn (n0)) (rdnn (n1))) (rdn_translate (nn3) (rdn_neg (rdnn (n3)))) (rdn_translate (nn7) (rdn_neg (rdnn (n7)))) (All Y, ((less (rdnn (n1)) Y) <=> ((-. (less Y (rdnn (n1)))) /\ (Y != (rdnn (n1)))))) ### Equiv 195 198 % 95.70/95.91 200. (All Y, ((less (rdnn (n1)) Y) <=> ((-. (less Y (rdnn (n1)))) /\ (Y != (rdnn (n1)))))) (rdn_translate (nn7) (rdn_neg (rdnn (n7)))) (rdn_translate (nn3) (rdn_neg (rdnn (n3)))) (rdn_positive_less (rdnn (n0)) (rdnn (n1))) (All X, (All Y, (All RDN_X, (All RDN_Y, (((rdn_translate X (rdn_neg RDN_X)) /\ ((rdn_translate Y (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y RDN_X))) => (less X Y)))))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (-. (Ex Y, (less (n1) Y))) (-. (Ex X, (Ex Y, (less X Y)))) (-. (Ex Y, (less (n0) Y))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) ((n0) = (rdnn (n1))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) ### All 199 % 95.70/95.91 201. (-. ((n0) != (rdnn (n1)))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (-. (Ex Y, (less (n0) Y))) (-. (Ex X, (Ex Y, (less X Y)))) (-. (Ex Y, (less (n1) Y))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (All X, (All Y, (All RDN_X, (All RDN_Y, (((rdn_translate X (rdn_neg RDN_X)) /\ ((rdn_translate Y (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y RDN_X))) => (less X Y)))))) (rdn_positive_less (rdnn (n0)) (rdnn (n1))) (rdn_translate (nn3) (rdn_neg (rdnn (n3)))) (rdn_translate (nn7) (rdn_neg (rdnn (n7)))) (All Y, ((less (rdnn (n1)) Y) <=> ((-. (less Y (rdnn (n1)))) /\ (Y != (rdnn (n1)))))) ### NotNot 200 % 95.70/95.91 202. (-. ((-. (less (n0) (rdnn (n1)))) /\ ((n0) != (rdnn (n1))))) (All Y, ((less (rdnn (n1)) Y) <=> ((-. (less Y (rdnn (n1)))) /\ (Y != (rdnn (n1)))))) (rdn_translate (nn7) (rdn_neg (rdnn (n7)))) (rdn_translate (nn3) (rdn_neg (rdnn (n3)))) (rdn_positive_less (rdnn (n0)) (rdnn (n1))) (All X, (All Y, (All RDN_X, (All RDN_Y, (((rdn_translate X (rdn_neg RDN_X)) /\ ((rdn_translate Y (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y RDN_X))) => (less X Y)))))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (-. (Ex Y, (less (n1) Y))) (-. (Ex X, (Ex Y, (less X Y)))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) (-. (Ex Y, (less (n0) Y))) ### NotAnd 3 201 % 95.70/95.91 203. (less (rdnn (n1)) (n0)) (-. (less (rdnn (n1)) (n0))) ### Axiom % 95.70/95.91 204. (-. (Ex Y, (less (rdnn (n1)) Y))) (less (rdnn (n1)) (n0)) ### NotExists 203 % 95.70/95.91 205. (-. (Ex X, (Ex Y, (less X Y)))) (less (rdnn (n1)) (n0)) ### NotExists 204 % 95.70/95.91 206. ((less (rdnn (n1)) (n0)) <=> ((-. (less (n0) (rdnn (n1)))) /\ ((n0) != (rdnn (n1))))) (-. (Ex Y, (less (n0) Y))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (-. (Ex X, (Ex Y, (less X Y)))) (-. (Ex Y, (less (n1) Y))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (All X, (All Y, (All RDN_X, (All RDN_Y, (((rdn_translate X (rdn_neg RDN_X)) /\ ((rdn_translate Y (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y RDN_X))) => (less X Y)))))) (rdn_positive_less (rdnn (n0)) (rdnn (n1))) (rdn_translate (nn3) (rdn_neg (rdnn (n3)))) (rdn_translate (nn7) (rdn_neg (rdnn (n7)))) (All Y, ((less (rdnn (n1)) Y) <=> ((-. (less Y (rdnn (n1)))) /\ (Y != (rdnn (n1)))))) ### Equiv 202 205 % 95.70/95.91 207. (All Y, ((less (rdnn (n1)) Y) <=> ((-. (less Y (rdnn (n1)))) /\ (Y != (rdnn (n1)))))) (rdn_translate (nn7) (rdn_neg (rdnn (n7)))) (rdn_translate (nn3) (rdn_neg (rdnn (n3)))) (rdn_positive_less (rdnn (n0)) (rdnn (n1))) (All X, (All Y, (All RDN_X, (All RDN_Y, (((rdn_translate X (rdn_neg RDN_X)) /\ ((rdn_translate Y (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y RDN_X))) => (less X Y)))))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (-. (Ex Y, (less (n1) Y))) (-. (Ex X, (Ex Y, (less X Y)))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) (-. (Ex Y, (less (n0) Y))) ### All 206 % 95.70/95.91 208. (-. (Ex Y, (less (n0) Y))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (-. (Ex X, (Ex Y, (less X Y)))) (-. (Ex Y, (less (n1) Y))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (All X, (All Y, (All RDN_X, (All RDN_Y, (((rdn_translate X (rdn_neg RDN_X)) /\ ((rdn_translate Y (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y RDN_X))) => (less X Y)))))) (rdn_positive_less (rdnn (n0)) (rdnn (n1))) (rdn_translate (nn3) (rdn_neg (rdnn (n3)))) (rdn_translate (nn7) (rdn_neg (rdnn (n7)))) ### All 207 % 95.70/95.91 209. (rdn_translate (nn7) (rdn_neg (rdnn (n7)))) (rdn_translate (nn3) (rdn_neg (rdnn (n3)))) (rdn_positive_less (rdnn (n0)) (rdnn (n1))) (All X, (All Y, (All RDN_X, (All RDN_Y, (((rdn_translate X (rdn_neg RDN_X)) /\ ((rdn_translate Y (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y RDN_X))) => (less X Y)))))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (-. (Ex X, (Ex Y, (less X Y)))) (All Y, ((less (n1) Y) <=> ((-. (less Y (n1))) /\ (Y != (n1))))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) (-. (Ex Y, (less (n0) Y))) ### NotExists 208 % 95.70/95.91 210. (-. (Ex Y, (less (n0) Y))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) (-. (Ex X, (Ex Y, (less X Y)))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (All X, (All Y, (All RDN_X, (All RDN_Y, (((rdn_translate X (rdn_neg RDN_X)) /\ ((rdn_translate Y (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y RDN_X))) => (less X Y)))))) (rdn_positive_less (rdnn (n0)) (rdnn (n1))) (rdn_translate (nn3) (rdn_neg (rdnn (n3)))) (rdn_translate (nn7) (rdn_neg (rdnn (n7)))) ### All 209 % 95.70/95.91 211. (rdn_translate (nn7) (rdn_neg (rdnn (n7)))) (rdn_translate (nn3) (rdn_neg (rdnn (n3)))) (rdn_positive_less (rdnn (n0)) (rdnn (n1))) (All X, (All Y, (All RDN_X, (All RDN_Y, (((rdn_translate X (rdn_neg RDN_X)) /\ ((rdn_translate Y (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y RDN_X))) => (less X Y)))))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (-. (Ex X, (Ex Y, (less X Y)))) (All Y, ((less (n0) Y) <=> ((-. (less Y (n0))) /\ (Y != (n0))))) ### NotExists 210 % 95.70/95.91 212. (-. (Ex X, (Ex Y, (less X Y)))) (All X, (All Y, ((less X Y) <=> ((-. (less Y X)) /\ (Y != X))))) (All X, (All Y, (All RDN_X, (All RDN_Y, (((rdn_translate X (rdn_neg RDN_X)) /\ ((rdn_translate Y (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y RDN_X))) => (less X Y)))))) (rdn_positive_less (rdnn (n0)) (rdnn (n1))) (rdn_translate (nn3) (rdn_neg (rdnn (n3)))) (rdn_translate (nn7) (rdn_neg (rdnn (n7)))) ### All 211 % 95.70/95.91 % SZS output end Proof % 95.70/95.91 (* END-PROOF *) %------------------------------------------------------------------------------