%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : KRS080+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 : n032.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Sun Jul 17 03:31:51 EDT 2022 % Result : Unsatisfiable 10.53s 10.73s % Output : Proof 10.93s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.10 % Problem : KRS080+1 : TPTP v8.1.0. Released v3.1.0. % 0.00/0.10 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.10/0.30 % Computer : n032.cluster.edu % 0.10/0.30 % Model : x86_64 x86_64 % 0.10/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.30 % Memory : 8042.1875MB % 0.10/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.30 % CPULimit : 300 % 0.10/0.30 % WCLimit : 600 % 0.10/0.30 % DateTime : Tue Jun 7 20:11:06 EDT 2022 % 0.10/0.30 % CPUTime : % 10.53/10.73 % SZS status Theorem % 10.53/10.73 (* PROOF-FOUND *) % 10.53/10.73 (* BEGIN-PROOF *) % 10.53/10.73 % SZS output start Proof % 10.53/10.73 1. (rr (i2003_11_14_17_19_21224) T_0) (-. (rr (i2003_11_14_17_19_21224) T_0)) ### Axiom % 10.53/10.73 2. (rr (i2003_11_14_17_19_21224) T_1) (-. (rr (i2003_11_14_17_19_21224) T_1)) ### Axiom % 10.53/10.73 3. (rr (i2003_11_14_17_19_21224) T_2) (-. (rr (i2003_11_14_17_19_21224) T_2)) ### Axiom % 10.53/10.73 4. (rr (i2003_11_14_17_19_21224) T_3) (-. (rr (i2003_11_14_17_19_21224) T_3)) ### Axiom % 10.53/10.73 5. (T_0 = T_1) (T_0 != T_1) ### Axiom % 10.53/10.73 6. (cp2 T_0) (-. (cp2 T_0)) ### Axiom % 10.53/10.73 7. (-. (cp2 T_1)) (cp2 T_1) ### Axiom % 10.53/10.73 8. (((T_0 = T_1) /\ (cp2 T_0)) => (cp2 T_1)) (-. (cp2 T_1)) (cp2 T_0) (T_0 = T_1) ### DisjTree 5 6 7 % 10.53/10.73 9. (All B, (((T_0 = B) /\ (cp2 T_0)) => (cp2 B))) (T_0 = T_1) (cp2 T_0) (-. (cp2 T_1)) ### All 8 % 10.53/10.73 10. (T_0 = T_2) (T_2 != T_0) ### Sym(=) % 10.53/10.73 11. (cp1 T_2) (-. (cp1 T_2)) ### Axiom % 10.53/10.73 12. (-. (cp1 T_0)) (cp1 T_0) ### Axiom % 10.53/10.73 13. (((T_2 = T_0) /\ (cp1 T_2)) => (cp1 T_0)) (-. (cp1 T_0)) (cp1 T_2) (T_0 = T_2) ### DisjTree 10 11 12 % 10.53/10.73 14. (All B, (((T_2 = B) /\ (cp1 T_2)) => (cp1 B))) (T_0 = T_2) (cp1 T_2) (-. (cp1 T_0)) ### All 13 % 10.53/10.73 15. (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (-. (cp1 T_0)) (cp1 T_2) (T_0 = T_2) ### All 14 % 10.53/10.73 16. (T_0 = T_3) (T_0 != T_3) ### Axiom % 10.53/10.73 17. (cp2 T_0) (-. (cp2 T_0)) ### Axiom % 10.53/10.73 18. (-. (cp2 T_3)) (cp2 T_3) ### Axiom % 10.53/10.73 19. (((T_0 = T_3) /\ (cp2 T_0)) => (cp2 T_3)) (-. (cp2 T_3)) (cp2 T_0) (T_0 = T_3) ### DisjTree 16 17 18 % 10.53/10.73 20. (All B, (((T_0 = B) /\ (cp2 T_0)) => (cp2 B))) (T_0 = T_3) (cp2 T_0) (-. (cp2 T_3)) ### All 19 % 10.53/10.73 21. (rr (i2003_11_14_17_19_21224) T_1) (-. (rr (i2003_11_14_17_19_21224) T_1)) ### Axiom % 10.53/10.73 22. (rr (i2003_11_14_17_19_21224) T_4) (-. (rr (i2003_11_14_17_19_21224) T_4)) ### Axiom % 10.53/10.73 23. (rr (i2003_11_14_17_19_21224) T_5) (-. (rr (i2003_11_14_17_19_21224) T_5)) ### Axiom % 10.53/10.73 24. (rr (i2003_11_14_17_19_21224) T_6) (-. (rr (i2003_11_14_17_19_21224) T_6)) ### Axiom % 10.53/10.73 25. (T_1 = T_4) (T_4 != T_1) ### Sym(=) % 10.53/10.73 26. (-. (cp1 T_1)) (cp1 T_4) (T_1 = T_4) ### P-NotP 25 % 10.53/10.73 27. (T_1 != T_1) ### Refl(=) % 10.53/10.73 28. (T_1 != T_1) ### Refl(=) % 10.53/10.73 29. (rr (i2003_11_14_17_19_21224) T_2) (-. (rr (i2003_11_14_17_19_21224) T_2)) ### Axiom % 10.53/10.73 30. (rr (i2003_11_14_17_19_21224) T_0) (-. (rr (i2003_11_14_17_19_21224) T_0)) ### Axiom % 10.53/10.73 31. (rr (i2003_11_14_17_19_21224) T_3) (-. (rr (i2003_11_14_17_19_21224) T_3)) ### Axiom % 10.53/10.73 32. (rr (i2003_11_14_17_19_21224) T_5) (-. (rr (i2003_11_14_17_19_21224) T_5)) ### Axiom % 10.53/10.73 33. (T_2 != T_0) (T_2 = T_0) ### Axiom % 10.53/10.73 34. (T_2 = T_3) (T_2 != T_3) ### Axiom % 10.53/10.73 35. (cp1 T_2) (-. (cp1 T_2)) ### Axiom % 10.53/10.73 36. (-. (cp1 T_3)) (cp1 T_3) ### Axiom % 10.53/10.73 37. (((T_2 = T_3) /\ (cp1 T_2)) => (cp1 T_3)) (-. (cp1 T_3)) (cp1 T_2) (T_2 = T_3) ### DisjTree 34 35 36 % 10.53/10.73 38. (All B, (((T_2 = B) /\ (cp1 T_2)) => (cp1 B))) (T_2 = T_3) (cp1 T_2) (-. (cp1 T_3)) ### All 37 % 10.53/10.73 39. (T_2 = T_5) (T_2 != T_5) ### Axiom % 10.53/10.73 40. (cp1 T_2) (-. (cp1 T_2)) ### Axiom % 10.53/10.73 41. (-. (cp1 T_5)) (cp1 T_5) ### Axiom % 10.53/10.73 42. (((T_2 = T_5) /\ (cp1 T_2)) => (cp1 T_5)) (-. (cp1 T_5)) (cp1 T_2) (T_2 = T_5) ### DisjTree 39 40 41 % 10.53/10.73 43. (All B, (((T_2 = B) /\ (cp1 T_2)) => (cp1 B))) (T_2 = T_5) (cp1 T_2) (-. (cp1 T_5)) ### All 42 % 10.53/10.73 44. (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (-. (cp1 T_5)) (cp1 T_2) (T_2 = T_5) ### All 43 % 10.53/10.73 45. (T_0 != T_3) (T_0 = T_3) ### Axiom % 10.53/10.73 46. (T_5 != T_0) (T_0 = T_5) ### Sym(=) % 10.53/10.73 47. (T_3 = T_5) (T_5 != T_3) ### Sym(=) % 10.53/10.73 48. (cp2 T_5) (-. (cp2 T_5)) ### Axiom % 10.53/10.73 49. (-. (cp2 T_3)) (cp2 T_3) ### Axiom % 10.53/10.73 50. (((T_5 = T_3) /\ (cp2 T_5)) => (cp2 T_3)) (-. (cp2 T_3)) (cp2 T_5) (T_3 = T_5) ### DisjTree 47 48 49 % 10.53/10.73 51. (All B, (((T_5 = B) /\ (cp2 T_5)) => (cp2 B))) (T_3 = T_5) (cp2 T_5) (-. (cp2 T_3)) ### All 50 % 10.53/10.73 52. (((rr (i2003_11_14_17_19_21224) T_2) /\ ((rr (i2003_11_14_17_19_21224) T_0) /\ ((rr (i2003_11_14_17_19_21224) T_3) /\ (rr (i2003_11_14_17_19_21224) T_5)))) => ((T_2 = T_0) \/ ((T_2 = T_3) \/ ((T_2 = T_5) \/ ((T_0 = T_3) \/ ((T_0 = T_5) \/ (T_3 = T_5))))))) (-. (cp2 T_3)) (cp2 T_5) (All B, (((T_5 = B) /\ (cp2 T_5)) => (cp2 B))) (T_5 != T_0) (T_0 != T_3) (-. (cp1 T_5)) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (-. (cp1 T_3)) (cp1 T_2) (All B, (((T_2 = B) /\ (cp1 T_2)) => (cp1 B))) (T_2 != T_0) (rr (i2003_11_14_17_19_21224) T_5) (rr (i2003_11_14_17_19_21224) T_3) (rr (i2003_11_14_17_19_21224) T_0) (rr (i2003_11_14_17_19_21224) T_2) ### DisjTree 29 30 31 32 33 38 44 45 46 51 % 10.53/10.73 53. (All Y3, (((rr (i2003_11_14_17_19_21224) T_2) /\ ((rr (i2003_11_14_17_19_21224) T_0) /\ ((rr (i2003_11_14_17_19_21224) T_3) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_2 = T_0) \/ ((T_2 = T_3) \/ ((T_2 = Y3) \/ ((T_0 = T_3) \/ ((T_0 = Y3) \/ (T_3 = Y3)))))))) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_0) (rr (i2003_11_14_17_19_21224) T_3) (rr (i2003_11_14_17_19_21224) T_5) (T_2 != T_0) (All B, (((T_2 = B) /\ (cp1 T_2)) => (cp1 B))) (cp1 T_2) (-. (cp1 T_3)) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (-. (cp1 T_5)) (T_0 != T_3) (T_5 != T_0) (All B, (((T_5 = B) /\ (cp2 T_5)) => (cp2 B))) (cp2 T_5) (-. (cp2 T_3)) ### All 52 % 10.53/10.73 54. (T_0 != T_1) (T_1 = T_5) (-. (cp2 T_3)) (cp2 T_5) (All B, (((T_5 = B) /\ (cp2 T_5)) => (cp2 B))) (T_0 != T_3) (-. (cp1 T_5)) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (-. (cp1 T_3)) (cp1 T_2) (All B, (((T_2 = B) /\ (cp1 T_2)) => (cp1 B))) (T_2 != T_0) (rr (i2003_11_14_17_19_21224) T_5) (rr (i2003_11_14_17_19_21224) T_3) (rr (i2003_11_14_17_19_21224) T_0) (rr (i2003_11_14_17_19_21224) T_2) (All Y3, (((rr (i2003_11_14_17_19_21224) T_2) /\ ((rr (i2003_11_14_17_19_21224) T_0) /\ ((rr (i2003_11_14_17_19_21224) T_3) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_2 = T_0) \/ ((T_2 = T_3) \/ ((T_2 = Y3) \/ ((T_0 = T_3) \/ ((T_0 = Y3) \/ (T_3 = Y3)))))))) ### Trans-sym 28 53 % 10.53/10.73 55. (T_1 = T_2) (All Y3, (((rr (i2003_11_14_17_19_21224) T_2) /\ ((rr (i2003_11_14_17_19_21224) T_0) /\ ((rr (i2003_11_14_17_19_21224) T_3) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_2 = T_0) \/ ((T_2 = T_3) \/ ((T_2 = Y3) \/ ((T_0 = T_3) \/ ((T_0 = Y3) \/ (T_3 = Y3)))))))) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_0) (rr (i2003_11_14_17_19_21224) T_3) (rr (i2003_11_14_17_19_21224) T_5) (All B, (((T_2 = B) /\ (cp1 T_2)) => (cp1 B))) (cp1 T_2) (-. (cp1 T_3)) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (-. (cp1 T_5)) (T_0 != T_3) (All B, (((T_5 = B) /\ (cp2 T_5)) => (cp2 B))) (cp2 T_5) (-. (cp2 T_3)) (T_1 = T_5) (T_0 != T_1) ### Trans-sym 27 54 % 10.53/10.73 56. (cp2 T_0) (-. (cp2 T_0)) ### Axiom % 10.53/10.73 57. (-. (cp2 T_1)) (cp2 T_1) ### Axiom % 10.53/10.73 58. (((T_0 = T_1) /\ (cp2 T_0)) => (cp2 T_1)) (-. (cp2 T_1)) (cp2 T_0) (T_1 = T_5) (-. (cp2 T_3)) (cp2 T_5) (All B, (((T_5 = B) /\ (cp2 T_5)) => (cp2 B))) (T_0 != T_3) (-. (cp1 T_5)) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (-. (cp1 T_3)) (cp1 T_2) (All B, (((T_2 = B) /\ (cp1 T_2)) => (cp1 B))) (rr (i2003_11_14_17_19_21224) T_5) (rr (i2003_11_14_17_19_21224) T_3) (rr (i2003_11_14_17_19_21224) T_0) (rr (i2003_11_14_17_19_21224) T_2) (All Y3, (((rr (i2003_11_14_17_19_21224) T_2) /\ ((rr (i2003_11_14_17_19_21224) T_0) /\ ((rr (i2003_11_14_17_19_21224) T_3) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_2 = T_0) \/ ((T_2 = T_3) \/ ((T_2 = Y3) \/ ((T_0 = T_3) \/ ((T_0 = Y3) \/ (T_3 = Y3)))))))) (T_1 = T_2) ### DisjTree 55 56 57 % 10.53/10.73 59. (All B, (((T_0 = B) /\ (cp2 T_0)) => (cp2 B))) (T_1 = T_2) (All Y3, (((rr (i2003_11_14_17_19_21224) T_2) /\ ((rr (i2003_11_14_17_19_21224) T_0) /\ ((rr (i2003_11_14_17_19_21224) T_3) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_2 = T_0) \/ ((T_2 = T_3) \/ ((T_2 = Y3) \/ ((T_0 = T_3) \/ ((T_0 = Y3) \/ (T_3 = Y3)))))))) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_0) (rr (i2003_11_14_17_19_21224) T_3) (rr (i2003_11_14_17_19_21224) T_5) (All B, (((T_2 = B) /\ (cp1 T_2)) => (cp1 B))) (cp1 T_2) (-. (cp1 T_3)) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (-. (cp1 T_5)) (T_0 != T_3) (All B, (((T_5 = B) /\ (cp2 T_5)) => (cp2 B))) (cp2 T_5) (-. (cp2 T_3)) (T_1 = T_5) (cp2 T_0) (-. (cp2 T_1)) ### All 58 % 10.53/10.73 60. (cp2 T_0) (-. (cp2 T_0)) ### Axiom % 10.53/10.73 61. (-. (cp2 T_3)) (cp2 T_3) ### Axiom % 10.53/10.73 62. (((T_0 = T_3) /\ (cp2 T_0)) => (cp2 T_3)) (-. (cp2 T_1)) (cp2 T_0) (T_1 = T_5) (-. (cp2 T_3)) (cp2 T_5) (All B, (((T_5 = B) /\ (cp2 T_5)) => (cp2 B))) (-. (cp1 T_5)) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (-. (cp1 T_3)) (cp1 T_2) (All B, (((T_2 = B) /\ (cp1 T_2)) => (cp1 B))) (rr (i2003_11_14_17_19_21224) T_5) (rr (i2003_11_14_17_19_21224) T_3) (rr (i2003_11_14_17_19_21224) T_0) (rr (i2003_11_14_17_19_21224) T_2) (All Y3, (((rr (i2003_11_14_17_19_21224) T_2) /\ ((rr (i2003_11_14_17_19_21224) T_0) /\ ((rr (i2003_11_14_17_19_21224) T_3) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_2 = T_0) \/ ((T_2 = T_3) \/ ((T_2 = Y3) \/ ((T_0 = T_3) \/ ((T_0 = Y3) \/ (T_3 = Y3)))))))) (T_1 = T_2) (All B, (((T_0 = B) /\ (cp2 T_0)) => (cp2 B))) ### DisjTree 59 60 61 % 10.73/10.99 63. (All B, (((T_0 = B) /\ (cp2 T_0)) => (cp2 B))) (T_1 = T_2) (All Y3, (((rr (i2003_11_14_17_19_21224) T_2) /\ ((rr (i2003_11_14_17_19_21224) T_0) /\ ((rr (i2003_11_14_17_19_21224) T_3) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_2 = T_0) \/ ((T_2 = T_3) \/ ((T_2 = Y3) \/ ((T_0 = T_3) \/ ((T_0 = Y3) \/ (T_3 = Y3)))))))) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_0) (rr (i2003_11_14_17_19_21224) T_3) (rr (i2003_11_14_17_19_21224) T_5) (All B, (((T_2 = B) /\ (cp1 T_2)) => (cp1 B))) (cp1 T_2) (-. (cp1 T_3)) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (-. (cp1 T_5)) (All B, (((T_5 = B) /\ (cp2 T_5)) => (cp2 B))) (cp2 T_5) (-. (cp2 T_3)) (T_1 = T_5) (cp2 T_0) (-. (cp2 T_1)) ### All 62 % 10.73/10.99 64. (T_1 = T_6) (T_6 != T_1) ### Sym(=) % 10.73/10.99 65. (cp3 T_6) (-. (cp3 T_6)) ### Axiom % 10.73/10.99 66. (-. (cp3 T_1)) (cp3 T_1) ### Axiom % 10.73/10.99 67. (((T_6 = T_1) /\ (cp3 T_6)) => (cp3 T_1)) (-. (cp3 T_1)) (cp3 T_6) (T_1 = T_6) ### DisjTree 64 65 66 % 10.73/10.99 68. (All B, (((T_6 = B) /\ (cp3 T_6)) => (cp3 B))) (T_1 = T_6) (cp3 T_6) (-. (cp3 T_1)) ### All 67 % 10.73/10.99 69. (T_4 = T_5) (T_4 != T_5) ### Axiom % 10.73/10.99 70. (cp1 T_4) (-. (cp1 T_4)) ### Axiom % 10.73/10.99 71. (-. (cp1 T_5)) (cp1 T_5) ### Axiom % 10.73/10.99 72. (((T_4 = T_5) /\ (cp1 T_4)) => (cp1 T_5)) (-. (cp1 T_5)) (cp1 T_4) (T_4 = T_5) ### DisjTree 69 70 71 % 10.73/10.99 73. (All B, (((T_4 = B) /\ (cp1 T_4)) => (cp1 B))) (T_4 = T_5) (cp1 T_4) (-. (cp1 T_5)) ### All 72 % 10.73/10.99 74. (rr (i2003_11_14_17_19_21224) T_1) (-. (rr (i2003_11_14_17_19_21224) T_1)) ### Axiom % 10.73/10.99 75. (rr (i2003_11_14_17_19_21224) T_4) (-. (rr (i2003_11_14_17_19_21224) T_4)) ### Axiom % 10.73/10.99 76. (rr (i2003_11_14_17_19_21224) T_3) (-. (rr (i2003_11_14_17_19_21224) T_3)) ### Axiom % 10.73/10.99 77. (rr (i2003_11_14_17_19_21224) T_0) (-. (rr (i2003_11_14_17_19_21224) T_0)) ### Axiom % 10.73/10.99 78. (T_1 = T_3) (T_3 != T_1) ### Sym(=) % 10.73/10.99 79. (cp3 T_3) (-. (cp3 T_3)) ### Axiom % 10.73/10.99 80. (-. (cp3 T_1)) (cp3 T_1) ### Axiom % 10.73/10.99 81. (((T_3 = T_1) /\ (cp3 T_3)) => (cp3 T_1)) (-. (cp3 T_1)) (cp3 T_3) (T_1 = T_3) ### DisjTree 78 79 80 % 10.73/10.99 82. (All B, (((T_3 = B) /\ (cp3 T_3)) => (cp3 B))) (T_1 = T_3) (cp3 T_3) (-. (cp3 T_1)) ### All 81 % 10.73/10.99 83. (T_0 != T_1) (T_1 = T_0) ### Sym(=) % 10.73/10.99 84. (cp1 T_4) (-. (cp1 T_4)) ### Axiom % 10.73/10.99 85. (T_4 = T_3) (T_3 != T_4) ### Sym(=) % 10.73/10.99 86. (cp3 T_3) (-. (cp3 T_3)) ### Axiom % 10.73/10.99 87. (-. (cp3 T_4)) (cp3 T_4) ### Axiom % 10.73/10.99 88. (((T_3 = T_4) /\ (cp3 T_3)) => (cp3 T_4)) (-. (cp3 T_4)) (cp3 T_3) (T_4 = T_3) ### DisjTree 85 86 87 % 10.73/10.99 89. (All B, (((T_3 = B) /\ (cp3 T_3)) => (cp3 B))) (T_4 = T_3) (cp3 T_3) (-. (cp3 T_4)) ### All 88 % 10.73/10.99 90. (-. ((cp2 T_4) \/ ((cp4 T_4) \/ ((cp5 T_4) \/ (cp3 T_4))))) (cp3 T_3) (T_4 = T_3) (All B, (((T_3 = B) /\ (cp3 T_3)) => (cp3 B))) ### ConjTree 89 % 10.73/10.99 91. ((cp1 T_4) => (-. ((cp2 T_4) \/ ((cp4 T_4) \/ ((cp5 T_4) \/ (cp3 T_4)))))) (All B, (((T_3 = B) /\ (cp3 T_3)) => (cp3 B))) (T_4 = T_3) (cp3 T_3) (cp1 T_4) ### Imply 84 90 % 10.73/10.99 92. (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (cp1 T_4) (cp3 T_3) (T_4 = T_3) (All B, (((T_3 = B) /\ (cp3 T_3)) => (cp3 B))) ### All 91 % 10.73/10.99 93. (T_4 = T_0) (T_0 != T_4) ### Sym(=) % 10.73/10.99 94. (T_6 != T_6) ### Refl(=) % 10.73/10.99 95. (T_0 != T_6) (T_4 = T_6) (T_4 = T_0) ### Trans 93 94 % 10.73/10.99 96. (T_0 != T_3) (T_3 = T_0) ### Sym(=) % 10.73/10.99 97. (((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_4) /\ ((rr (i2003_11_14_17_19_21224) T_3) /\ (rr (i2003_11_14_17_19_21224) T_0)))) => ((T_1 = T_4) \/ ((T_1 = T_3) \/ ((T_1 = T_0) \/ ((T_4 = T_3) \/ ((T_4 = T_0) \/ (T_3 = T_0))))))) (T_0 != T_3) (T_4 = T_6) (T_0 != T_6) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (T_0 != T_1) (-. (cp3 T_1)) (cp3 T_3) (All B, (((T_3 = B) /\ (cp3 T_3)) => (cp3 B))) (cp1 T_4) (-. (cp1 T_1)) (rr (i2003_11_14_17_19_21224) T_0) (rr (i2003_11_14_17_19_21224) T_3) (rr (i2003_11_14_17_19_21224) T_4) (rr (i2003_11_14_17_19_21224) T_1) ### DisjTree 74 75 76 77 26 82 83 92 95 96 % 10.73/10.99 98. (All Y3, (((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_4) /\ ((rr (i2003_11_14_17_19_21224) T_3) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_1 = T_4) \/ ((T_1 = T_3) \/ ((T_1 = Y3) \/ ((T_4 = T_3) \/ ((T_4 = Y3) \/ (T_3 = Y3)))))))) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_4) (rr (i2003_11_14_17_19_21224) T_3) (rr (i2003_11_14_17_19_21224) T_0) (-. (cp1 T_1)) (cp1 T_4) (All B, (((T_3 = B) /\ (cp3 T_3)) => (cp3 B))) (cp3 T_3) (-. (cp3 T_1)) (T_0 != T_1) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (T_0 != T_6) (T_4 = T_6) (T_0 != T_3) ### All 97 % 10.73/10.99 99. (cp2 T_0) (-. (cp2 T_0)) ### Axiom % 10.73/10.99 100. (-. (cp2 T_1)) (cp2 T_1) ### Axiom % 10.73/10.99 101. (((T_0 = T_1) /\ (cp2 T_0)) => (cp2 T_1)) (-. (cp2 T_1)) (cp2 T_0) (T_0 != T_3) (T_4 = T_6) (T_0 != T_6) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (-. (cp3 T_1)) (cp3 T_3) (All B, (((T_3 = B) /\ (cp3 T_3)) => (cp3 B))) (cp1 T_4) (-. (cp1 T_1)) (rr (i2003_11_14_17_19_21224) T_0) (rr (i2003_11_14_17_19_21224) T_3) (rr (i2003_11_14_17_19_21224) T_4) (rr (i2003_11_14_17_19_21224) T_1) (All Y3, (((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_4) /\ ((rr (i2003_11_14_17_19_21224) T_3) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_1 = T_4) \/ ((T_1 = T_3) \/ ((T_1 = Y3) \/ ((T_4 = T_3) \/ ((T_4 = Y3) \/ (T_3 = Y3)))))))) ### DisjTree 98 99 100 % 10.73/10.99 102. (All B, (((T_0 = B) /\ (cp2 T_0)) => (cp2 B))) (All Y3, (((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_4) /\ ((rr (i2003_11_14_17_19_21224) T_3) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_1 = T_4) \/ ((T_1 = T_3) \/ ((T_1 = Y3) \/ ((T_4 = T_3) \/ ((T_4 = Y3) \/ (T_3 = Y3)))))))) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_4) (rr (i2003_11_14_17_19_21224) T_3) (rr (i2003_11_14_17_19_21224) T_0) (-. (cp1 T_1)) (cp1 T_4) (All B, (((T_3 = B) /\ (cp3 T_3)) => (cp3 B))) (cp3 T_3) (-. (cp3 T_1)) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (T_0 != T_6) (T_4 = T_6) (T_0 != T_3) (cp2 T_0) (-. (cp2 T_1)) ### All 101 % 10.73/10.99 103. (cp2 T_0) (-. (cp2 T_0)) ### Axiom % 10.73/10.99 104. (-. (cp2 T_6)) (cp2 T_6) ### Axiom % 10.73/10.99 105. (((T_0 = T_6) /\ (cp2 T_0)) => (cp2 T_6)) (-. (cp2 T_6)) (-. (cp2 T_1)) (cp2 T_0) (T_0 != T_3) (T_4 = T_6) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (-. (cp3 T_1)) (cp3 T_3) (All B, (((T_3 = B) /\ (cp3 T_3)) => (cp3 B))) (cp1 T_4) (-. (cp1 T_1)) (rr (i2003_11_14_17_19_21224) T_0) (rr (i2003_11_14_17_19_21224) T_3) (rr (i2003_11_14_17_19_21224) T_4) (rr (i2003_11_14_17_19_21224) T_1) (All Y3, (((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_4) /\ ((rr (i2003_11_14_17_19_21224) T_3) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_1 = T_4) \/ ((T_1 = T_3) \/ ((T_1 = Y3) \/ ((T_4 = T_3) \/ ((T_4 = Y3) \/ (T_3 = Y3)))))))) (All B, (((T_0 = B) /\ (cp2 T_0)) => (cp2 B))) ### DisjTree 102 103 104 % 10.73/10.99 106. (All B, (((T_0 = B) /\ (cp2 T_0)) => (cp2 B))) (All Y3, (((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_4) /\ ((rr (i2003_11_14_17_19_21224) T_3) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_1 = T_4) \/ ((T_1 = T_3) \/ ((T_1 = Y3) \/ ((T_4 = T_3) \/ ((T_4 = Y3) \/ (T_3 = Y3)))))))) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_4) (rr (i2003_11_14_17_19_21224) T_3) (rr (i2003_11_14_17_19_21224) T_0) (-. (cp1 T_1)) (cp1 T_4) (All B, (((T_3 = B) /\ (cp3 T_3)) => (cp3 B))) (cp3 T_3) (-. (cp3 T_1)) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (T_4 = T_6) (T_0 != T_3) (cp2 T_0) (-. (cp2 T_1)) (-. (cp2 T_6)) ### All 105 % 10.73/10.99 107. (cp2 T_0) (-. (cp2 T_0)) ### Axiom % 10.82/11.01 108. (-. (cp2 T_3)) (cp2 T_3) ### Axiom % 10.82/11.01 109. (((T_0 = T_3) /\ (cp2 T_0)) => (cp2 T_3)) (-. (cp2 T_3)) (-. (cp2 T_6)) (-. (cp2 T_1)) (cp2 T_0) (T_4 = T_6) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (-. (cp3 T_1)) (cp3 T_3) (All B, (((T_3 = B) /\ (cp3 T_3)) => (cp3 B))) (cp1 T_4) (-. (cp1 T_1)) (rr (i2003_11_14_17_19_21224) T_0) (rr (i2003_11_14_17_19_21224) T_3) (rr (i2003_11_14_17_19_21224) T_4) (rr (i2003_11_14_17_19_21224) T_1) (All Y3, (((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_4) /\ ((rr (i2003_11_14_17_19_21224) T_3) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_1 = T_4) \/ ((T_1 = T_3) \/ ((T_1 = Y3) \/ ((T_4 = T_3) \/ ((T_4 = Y3) \/ (T_3 = Y3)))))))) (All B, (((T_0 = B) /\ (cp2 T_0)) => (cp2 B))) ### DisjTree 106 107 108 % 10.82/11.01 110. (All B, (((T_0 = B) /\ (cp2 T_0)) => (cp2 B))) (All Y3, (((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_4) /\ ((rr (i2003_11_14_17_19_21224) T_3) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_1 = T_4) \/ ((T_1 = T_3) \/ ((T_1 = Y3) \/ ((T_4 = T_3) \/ ((T_4 = Y3) \/ (T_3 = Y3)))))))) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_4) (rr (i2003_11_14_17_19_21224) T_3) (rr (i2003_11_14_17_19_21224) T_0) (-. (cp1 T_1)) (cp1 T_4) (All B, (((T_3 = B) /\ (cp3 T_3)) => (cp3 B))) (cp3 T_3) (-. (cp3 T_1)) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (T_4 = T_6) (cp2 T_0) (-. (cp2 T_1)) (-. (cp2 T_6)) (-. (cp2 T_3)) ### All 109 % 10.82/11.01 111. (T_5 = T_6) (T_5 != T_6) ### Axiom % 10.82/11.01 112. (cp2 T_5) (-. (cp2 T_5)) ### Axiom % 10.82/11.01 113. (-. (cp2 T_6)) (cp2 T_6) ### Axiom % 10.82/11.01 114. (((T_5 = T_6) /\ (cp2 T_5)) => (cp2 T_6)) (-. (cp2 T_6)) (cp2 T_5) (T_5 = T_6) ### DisjTree 111 112 113 % 10.82/11.01 115. (All B, (((T_5 = B) /\ (cp2 T_5)) => (cp2 B))) (T_5 = T_6) (cp2 T_5) (-. (cp2 T_6)) ### All 114 % 10.82/11.01 116. (((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_4) /\ ((rr (i2003_11_14_17_19_21224) T_5) /\ (rr (i2003_11_14_17_19_21224) T_6)))) => ((T_1 = T_4) \/ ((T_1 = T_5) \/ ((T_1 = T_6) \/ ((T_4 = T_5) \/ ((T_4 = T_6) \/ (T_5 = T_6))))))) (-. (cp2 T_6)) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (cp3 T_3) (All B, (((T_3 = B) /\ (cp3 T_3)) => (cp3 B))) (All Y3, (((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_4) /\ ((rr (i2003_11_14_17_19_21224) T_3) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_1 = T_4) \/ ((T_1 = T_3) \/ ((T_1 = Y3) \/ ((T_4 = T_3) \/ ((T_4 = Y3) \/ (T_3 = Y3)))))))) (All B, (((T_4 = B) /\ (cp1 T_4)) => (cp1 B))) (-. (cp3 T_1)) (cp3 T_6) (All B, (((T_6 = B) /\ (cp3 T_6)) => (cp3 B))) (-. (cp2 T_1)) (cp2 T_0) (-. (cp2 T_3)) (cp2 T_5) (All B, (((T_5 = B) /\ (cp2 T_5)) => (cp2 B))) (-. (cp1 T_5)) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (-. (cp1 T_3)) (cp1 T_2) (All B, (((T_2 = B) /\ (cp1 T_2)) => (cp1 B))) (rr (i2003_11_14_17_19_21224) T_3) (rr (i2003_11_14_17_19_21224) T_0) (rr (i2003_11_14_17_19_21224) T_2) (All Y3, (((rr (i2003_11_14_17_19_21224) T_2) /\ ((rr (i2003_11_14_17_19_21224) T_0) /\ ((rr (i2003_11_14_17_19_21224) T_3) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_2 = T_0) \/ ((T_2 = T_3) \/ ((T_2 = Y3) \/ ((T_0 = T_3) \/ ((T_0 = Y3) \/ (T_3 = Y3)))))))) (T_1 = T_2) (All B, (((T_0 = B) /\ (cp2 T_0)) => (cp2 B))) (cp1 T_4) (-. (cp1 T_1)) (rr (i2003_11_14_17_19_21224) T_6) (rr (i2003_11_14_17_19_21224) T_5) (rr (i2003_11_14_17_19_21224) T_4) (rr (i2003_11_14_17_19_21224) T_1) ### DisjTree 21 22 23 24 26 63 68 73 110 115 % 10.82/11.02 117. (All Y3, (((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_4) /\ ((rr (i2003_11_14_17_19_21224) T_5) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_1 = T_4) \/ ((T_1 = T_5) \/ ((T_1 = Y3) \/ ((T_4 = T_5) \/ ((T_4 = Y3) \/ (T_5 = Y3)))))))) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_4) (rr (i2003_11_14_17_19_21224) T_5) (rr (i2003_11_14_17_19_21224) T_6) (-. (cp1 T_1)) (cp1 T_4) (All B, (((T_0 = B) /\ (cp2 T_0)) => (cp2 B))) (T_1 = T_2) (All Y3, (((rr (i2003_11_14_17_19_21224) T_2) /\ ((rr (i2003_11_14_17_19_21224) T_0) /\ ((rr (i2003_11_14_17_19_21224) T_3) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_2 = T_0) \/ ((T_2 = T_3) \/ ((T_2 = Y3) \/ ((T_0 = T_3) \/ ((T_0 = Y3) \/ (T_3 = Y3)))))))) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_0) (rr (i2003_11_14_17_19_21224) T_3) (All B, (((T_2 = B) /\ (cp1 T_2)) => (cp1 B))) (cp1 T_2) (-. (cp1 T_3)) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (-. (cp1 T_5)) (All B, (((T_5 = B) /\ (cp2 T_5)) => (cp2 B))) (cp2 T_5) (-. (cp2 T_3)) (cp2 T_0) (-. (cp2 T_1)) (All B, (((T_6 = B) /\ (cp3 T_6)) => (cp3 B))) (cp3 T_6) (-. (cp3 T_1)) (All B, (((T_4 = B) /\ (cp1 T_4)) => (cp1 B))) (All Y3, (((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_4) /\ ((rr (i2003_11_14_17_19_21224) T_3) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_1 = T_4) \/ ((T_1 = T_3) \/ ((T_1 = Y3) \/ ((T_4 = T_3) \/ ((T_4 = Y3) \/ (T_3 = Y3)))))))) (All B, (((T_3 = B) /\ (cp3 T_3)) => (cp3 B))) (cp3 T_3) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (-. (cp2 T_6)) ### All 116 % 10.82/11.02 118. (-. (cp2 T_6)) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (cp3 T_3) (All B, (((T_3 = B) /\ (cp3 T_3)) => (cp3 B))) (All Y3, (((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_4) /\ ((rr (i2003_11_14_17_19_21224) T_3) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_1 = T_4) \/ ((T_1 = T_3) \/ ((T_1 = Y3) \/ ((T_4 = T_3) \/ ((T_4 = Y3) \/ (T_3 = Y3)))))))) (All B, (((T_4 = B) /\ (cp1 T_4)) => (cp1 B))) (-. (cp3 T_1)) (cp3 T_6) (All B, (((T_6 = B) /\ (cp3 T_6)) => (cp3 B))) (-. (cp2 T_1)) (cp2 T_0) (-. (cp2 T_3)) (cp2 T_5) (All B, (((T_5 = B) /\ (cp2 T_5)) => (cp2 B))) (-. (cp1 T_5)) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (-. (cp1 T_3)) (cp1 T_2) (rr (i2003_11_14_17_19_21224) T_3) (rr (i2003_11_14_17_19_21224) T_0) (rr (i2003_11_14_17_19_21224) T_2) (All Y3, (((rr (i2003_11_14_17_19_21224) T_2) /\ ((rr (i2003_11_14_17_19_21224) T_0) /\ ((rr (i2003_11_14_17_19_21224) T_3) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_2 = T_0) \/ ((T_2 = T_3) \/ ((T_2 = Y3) \/ ((T_0 = T_3) \/ ((T_0 = Y3) \/ (T_3 = Y3)))))))) (T_1 = T_2) (All B, (((T_0 = B) /\ (cp2 T_0)) => (cp2 B))) (cp1 T_4) (-. (cp1 T_1)) (rr (i2003_11_14_17_19_21224) T_6) (rr (i2003_11_14_17_19_21224) T_5) (rr (i2003_11_14_17_19_21224) T_4) (rr (i2003_11_14_17_19_21224) T_1) (All Y3, (((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_4) /\ ((rr (i2003_11_14_17_19_21224) T_5) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_1 = T_4) \/ ((T_1 = T_5) \/ ((T_1 = Y3) \/ ((T_4 = T_5) \/ ((T_4 = Y3) \/ (T_5 = Y3)))))))) ### All 117 % 10.82/11.02 119. (All Y3, (((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_4) /\ ((rr (i2003_11_14_17_19_21224) T_5) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_1 = T_4) \/ ((T_1 = T_5) \/ ((T_1 = Y3) \/ ((T_4 = T_5) \/ ((T_4 = Y3) \/ (T_5 = Y3)))))))) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_4) (rr (i2003_11_14_17_19_21224) T_5) (rr (i2003_11_14_17_19_21224) T_6) (-. (cp1 T_1)) (cp1 T_4) (All B, (((T_0 = B) /\ (cp2 T_0)) => (cp2 B))) (T_1 = T_2) (All Y3, (((rr (i2003_11_14_17_19_21224) T_2) /\ ((rr (i2003_11_14_17_19_21224) T_0) /\ ((rr (i2003_11_14_17_19_21224) T_3) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_2 = T_0) \/ ((T_2 = T_3) \/ ((T_2 = Y3) \/ ((T_0 = T_3) \/ ((T_0 = Y3) \/ (T_3 = Y3)))))))) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_0) (rr (i2003_11_14_17_19_21224) T_3) (cp1 T_2) (-. (cp1 T_3)) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (-. (cp1 T_5)) (All B, (((T_5 = B) /\ (cp2 T_5)) => (cp2 B))) (cp2 T_5) (-. (cp2 T_3)) (cp2 T_0) (-. (cp2 T_1)) (All B, (((T_6 = B) /\ (cp3 T_6)) => (cp3 B))) (cp3 T_6) (-. (cp3 T_1)) (All Y3, (((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_4) /\ ((rr (i2003_11_14_17_19_21224) T_3) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_1 = T_4) \/ ((T_1 = T_3) \/ ((T_1 = Y3) \/ ((T_4 = T_3) \/ ((T_4 = Y3) \/ (T_3 = Y3)))))))) (All B, (((T_3 = B) /\ (cp3 T_3)) => (cp3 B))) (cp3 T_3) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (-. (cp2 T_6)) ### All 118 % 10.82/11.05 120. (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (-. (cp1 T_3)) (cp1 T_2) (T_2 = T_3) ### All 38 % 10.82/11.05 121. (((rr (i2003_11_14_17_19_21224) T_0) /\ ((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_2) /\ (rr (i2003_11_14_17_19_21224) T_3)))) => ((T_0 = T_1) \/ ((T_0 = T_2) \/ ((T_0 = T_3) \/ ((T_1 = T_2) \/ ((T_1 = T_3) \/ (T_2 = T_3))))))) (-. (cp2 T_6)) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (cp3 T_3) (All B, (((T_3 = B) /\ (cp3 T_3)) => (cp3 B))) (All Y3, (((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_4) /\ ((rr (i2003_11_14_17_19_21224) T_3) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_1 = T_4) \/ ((T_1 = T_3) \/ ((T_1 = Y3) \/ ((T_4 = T_3) \/ ((T_4 = Y3) \/ (T_3 = Y3)))))))) (-. (cp3 T_1)) (cp3 T_6) (All B, (((T_6 = B) /\ (cp3 T_6)) => (cp3 B))) (cp2 T_5) (All B, (((T_5 = B) /\ (cp2 T_5)) => (cp2 B))) (-. (cp1 T_5)) (-. (cp1 T_3)) (All Y3, (((rr (i2003_11_14_17_19_21224) T_2) /\ ((rr (i2003_11_14_17_19_21224) T_0) /\ ((rr (i2003_11_14_17_19_21224) T_3) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_2 = T_0) \/ ((T_2 = T_3) \/ ((T_2 = Y3) \/ ((T_0 = T_3) \/ ((T_0 = Y3) \/ (T_3 = Y3)))))))) (cp1 T_4) (-. (cp1 T_1)) (rr (i2003_11_14_17_19_21224) T_6) (rr (i2003_11_14_17_19_21224) T_5) (rr (i2003_11_14_17_19_21224) T_4) (All Y3, (((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_4) /\ ((rr (i2003_11_14_17_19_21224) T_5) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_1 = T_4) \/ ((T_1 = T_5) \/ ((T_1 = Y3) \/ ((T_4 = T_5) \/ ((T_4 = Y3) \/ (T_5 = Y3)))))))) (-. (cp2 T_3)) (cp1 T_2) (-. (cp1 T_0)) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (-. (cp2 T_1)) (cp2 T_0) (All B, (((T_0 = B) /\ (cp2 T_0)) => (cp2 B))) (rr (i2003_11_14_17_19_21224) T_3) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_0) ### DisjTree 1 2 3 4 9 15 20 119 82 120 % 10.82/11.05 122. (All Y3, (((rr (i2003_11_14_17_19_21224) T_0) /\ ((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_0 = T_1) \/ ((T_0 = T_2) \/ ((T_0 = Y3) \/ ((T_1 = T_2) \/ ((T_1 = Y3) \/ (T_2 = Y3)))))))) (rr (i2003_11_14_17_19_21224) T_0) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_3) (All B, (((T_0 = B) /\ (cp2 T_0)) => (cp2 B))) (cp2 T_0) (-. (cp2 T_1)) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (-. (cp1 T_0)) (cp1 T_2) (-. (cp2 T_3)) (All Y3, (((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_4) /\ ((rr (i2003_11_14_17_19_21224) T_5) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_1 = T_4) \/ ((T_1 = T_5) \/ ((T_1 = Y3) \/ ((T_4 = T_5) \/ ((T_4 = Y3) \/ (T_5 = Y3)))))))) (rr (i2003_11_14_17_19_21224) T_4) (rr (i2003_11_14_17_19_21224) T_5) (rr (i2003_11_14_17_19_21224) T_6) (-. (cp1 T_1)) (cp1 T_4) (All Y3, (((rr (i2003_11_14_17_19_21224) T_2) /\ ((rr (i2003_11_14_17_19_21224) T_0) /\ ((rr (i2003_11_14_17_19_21224) T_3) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_2 = T_0) \/ ((T_2 = T_3) \/ ((T_2 = Y3) \/ ((T_0 = T_3) \/ ((T_0 = Y3) \/ (T_3 = Y3)))))))) (-. (cp1 T_3)) (-. (cp1 T_5)) (All B, (((T_5 = B) /\ (cp2 T_5)) => (cp2 B))) (cp2 T_5) (All B, (((T_6 = B) /\ (cp3 T_6)) => (cp3 B))) (cp3 T_6) (-. (cp3 T_1)) (All Y3, (((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_4) /\ ((rr (i2003_11_14_17_19_21224) T_3) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_1 = T_4) \/ ((T_1 = T_3) \/ ((T_1 = Y3) \/ ((T_4 = T_3) \/ ((T_4 = Y3) \/ (T_3 = Y3)))))))) (All B, (((T_3 = B) /\ (cp3 T_3)) => (cp3 B))) (cp3 T_3) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (-. (cp2 T_6)) ### All 121 % 10.82/11.05 123. (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (-. (cp2 T_6)) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (cp3 T_3) (All B, (((T_3 = B) /\ (cp3 T_3)) => (cp3 B))) (All Y3, (((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_4) /\ ((rr (i2003_11_14_17_19_21224) T_3) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_1 = T_4) \/ ((T_1 = T_3) \/ ((T_1 = Y3) \/ ((T_4 = T_3) \/ ((T_4 = Y3) \/ (T_3 = Y3)))))))) (-. (cp3 T_1)) (cp3 T_6) (All B, (((T_6 = B) /\ (cp3 T_6)) => (cp3 B))) (cp2 T_5) (-. (cp1 T_5)) (-. (cp1 T_3)) (All Y3, (((rr (i2003_11_14_17_19_21224) T_2) /\ ((rr (i2003_11_14_17_19_21224) T_0) /\ ((rr (i2003_11_14_17_19_21224) T_3) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_2 = T_0) \/ ((T_2 = T_3) \/ ((T_2 = Y3) \/ ((T_0 = T_3) \/ ((T_0 = Y3) \/ (T_3 = Y3)))))))) (cp1 T_4) (-. (cp1 T_1)) (rr (i2003_11_14_17_19_21224) T_6) (rr (i2003_11_14_17_19_21224) T_5) (rr (i2003_11_14_17_19_21224) T_4) (All Y3, (((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_4) /\ ((rr (i2003_11_14_17_19_21224) T_5) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_1 = T_4) \/ ((T_1 = T_5) \/ ((T_1 = Y3) \/ ((T_4 = T_5) \/ ((T_4 = Y3) \/ (T_5 = Y3)))))))) (-. (cp2 T_3)) (cp1 T_2) (-. (cp1 T_0)) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (-. (cp2 T_1)) (cp2 T_0) (All B, (((T_0 = B) /\ (cp2 T_0)) => (cp2 B))) (rr (i2003_11_14_17_19_21224) T_3) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_0) (All Y3, (((rr (i2003_11_14_17_19_21224) T_0) /\ ((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_0 = T_1) \/ ((T_0 = T_2) \/ ((T_0 = Y3) \/ ((T_1 = T_2) \/ ((T_1 = Y3) \/ (T_2 = Y3)))))))) ### All 122 % 10.82/11.05 124. (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_4) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_1 = T_4) \/ ((T_1 = Y2) \/ ((T_1 = Y3) \/ ((T_4 = Y2) \/ ((T_4 = Y3) \/ (Y2 = Y3))))))))) (All Y3, (((rr (i2003_11_14_17_19_21224) T_0) /\ ((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_0 = T_1) \/ ((T_0 = T_2) \/ ((T_0 = Y3) \/ ((T_1 = T_2) \/ ((T_1 = Y3) \/ (T_2 = Y3)))))))) (rr (i2003_11_14_17_19_21224) T_0) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_3) (All B, (((T_0 = B) /\ (cp2 T_0)) => (cp2 B))) (cp2 T_0) (-. (cp2 T_1)) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (-. (cp1 T_0)) (cp1 T_2) (-. (cp2 T_3)) (rr (i2003_11_14_17_19_21224) T_4) (rr (i2003_11_14_17_19_21224) T_5) (rr (i2003_11_14_17_19_21224) T_6) (-. (cp1 T_1)) (cp1 T_4) (All Y3, (((rr (i2003_11_14_17_19_21224) T_2) /\ ((rr (i2003_11_14_17_19_21224) T_0) /\ ((rr (i2003_11_14_17_19_21224) T_3) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_2 = T_0) \/ ((T_2 = T_3) \/ ((T_2 = Y3) \/ ((T_0 = T_3) \/ ((T_0 = Y3) \/ (T_3 = Y3)))))))) (-. (cp1 T_3)) (-. (cp1 T_5)) (cp2 T_5) (All B, (((T_6 = B) /\ (cp3 T_6)) => (cp3 B))) (cp3 T_6) (-. (cp3 T_1)) (All Y3, (((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_4) /\ ((rr (i2003_11_14_17_19_21224) T_3) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_1 = T_4) \/ ((T_1 = T_3) \/ ((T_1 = Y3) \/ ((T_4 = T_3) \/ ((T_4 = Y3) \/ (T_3 = Y3)))))))) (All B, (((T_3 = B) /\ (cp3 T_3)) => (cp3 B))) (cp3 T_3) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (-. (cp2 T_6)) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) ### All 123 % 10.82/11.05 125. (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) T_2) /\ ((rr (i2003_11_14_17_19_21224) T_0) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_2 = T_0) \/ ((T_2 = Y2) \/ ((T_2 = Y3) \/ ((T_0 = Y2) \/ ((T_0 = Y3) \/ (Y2 = Y3))))))))) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (-. (cp2 T_6)) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (cp3 T_3) (All B, (((T_3 = B) /\ (cp3 T_3)) => (cp3 B))) (All Y3, (((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_4) /\ ((rr (i2003_11_14_17_19_21224) T_3) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_1 = T_4) \/ ((T_1 = T_3) \/ ((T_1 = Y3) \/ ((T_4 = T_3) \/ ((T_4 = Y3) \/ (T_3 = Y3)))))))) (-. (cp3 T_1)) (cp3 T_6) (All B, (((T_6 = B) /\ (cp3 T_6)) => (cp3 B))) (cp2 T_5) (-. (cp1 T_5)) (-. (cp1 T_3)) (cp1 T_4) (-. (cp1 T_1)) (rr (i2003_11_14_17_19_21224) T_6) (rr (i2003_11_14_17_19_21224) T_5) (rr (i2003_11_14_17_19_21224) T_4) (-. (cp2 T_3)) (cp1 T_2) (-. (cp1 T_0)) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (-. (cp2 T_1)) (cp2 T_0) (All B, (((T_0 = B) /\ (cp2 T_0)) => (cp2 B))) (rr (i2003_11_14_17_19_21224) T_3) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_0) (All Y3, (((rr (i2003_11_14_17_19_21224) T_0) /\ ((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_0 = T_1) \/ ((T_0 = T_2) \/ ((T_0 = Y3) \/ ((T_1 = T_2) \/ ((T_1 = Y3) \/ (T_2 = Y3)))))))) (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_4) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_1 = T_4) \/ ((T_1 = Y2) \/ ((T_1 = Y3) \/ ((T_4 = Y2) \/ ((T_4 = Y3) \/ (Y2 = Y3))))))))) ### All 124 % 10.92/11.09 126. (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_4) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_1 = T_4) \/ ((T_1 = Y2) \/ ((T_1 = Y3) \/ ((T_4 = Y2) \/ ((T_4 = Y3) \/ (Y2 = Y3))))))))) (All Y3, (((rr (i2003_11_14_17_19_21224) T_0) /\ ((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_0 = T_1) \/ ((T_0 = T_2) \/ ((T_0 = Y3) \/ ((T_1 = T_2) \/ ((T_1 = Y3) \/ (T_2 = Y3)))))))) (rr (i2003_11_14_17_19_21224) T_0) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_3) (All B, (((T_0 = B) /\ (cp2 T_0)) => (cp2 B))) (cp2 T_0) (-. (cp2 T_1)) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (-. (cp1 T_0)) (cp1 T_2) (-. (cp2 T_3)) (rr (i2003_11_14_17_19_21224) T_4) (rr (i2003_11_14_17_19_21224) T_5) (rr (i2003_11_14_17_19_21224) T_6) (-. (cp1 T_1)) (cp1 T_4) (-. (cp1 T_3)) (-. (cp1 T_5)) (cp2 T_5) (cp3 T_6) (-. (cp3 T_1)) (All Y3, (((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_4) /\ ((rr (i2003_11_14_17_19_21224) T_3) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_1 = T_4) \/ ((T_1 = T_3) \/ ((T_1 = Y3) \/ ((T_4 = T_3) \/ ((T_4 = Y3) \/ (T_3 = Y3)))))))) (All B, (((T_3 = B) /\ (cp3 T_3)) => (cp3 B))) (cp3 T_3) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (-. (cp2 T_6)) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) T_2) /\ ((rr (i2003_11_14_17_19_21224) T_0) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_2 = T_0) \/ ((T_2 = Y2) \/ ((T_2 = Y3) \/ ((T_0 = Y2) \/ ((T_0 = Y3) \/ (Y2 = Y3))))))))) ### All 125 % 10.92/11.09 127. (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) T_2) /\ ((rr (i2003_11_14_17_19_21224) T_0) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_2 = T_0) \/ ((T_2 = Y2) \/ ((T_2 = Y3) \/ ((T_0 = Y2) \/ ((T_0 = Y3) \/ (Y2 = Y3))))))))) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (-. (cp2 T_6)) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (cp3 T_3) (All Y3, (((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_4) /\ ((rr (i2003_11_14_17_19_21224) T_3) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_1 = T_4) \/ ((T_1 = T_3) \/ ((T_1 = Y3) \/ ((T_4 = T_3) \/ ((T_4 = Y3) \/ (T_3 = Y3)))))))) (-. (cp3 T_1)) (cp3 T_6) (cp2 T_5) (-. (cp1 T_5)) (-. (cp1 T_3)) (cp1 T_4) (-. (cp1 T_1)) (rr (i2003_11_14_17_19_21224) T_6) (rr (i2003_11_14_17_19_21224) T_5) (rr (i2003_11_14_17_19_21224) T_4) (-. (cp2 T_3)) (cp1 T_2) (-. (cp1 T_0)) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (-. (cp2 T_1)) (cp2 T_0) (All B, (((T_0 = B) /\ (cp2 T_0)) => (cp2 B))) (rr (i2003_11_14_17_19_21224) T_3) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_0) (All Y3, (((rr (i2003_11_14_17_19_21224) T_0) /\ ((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_0 = T_1) \/ ((T_0 = T_2) \/ ((T_0 = Y3) \/ ((T_1 = T_2) \/ ((T_1 = Y3) \/ (T_2 = Y3)))))))) (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_4) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_1 = T_4) \/ ((T_1 = Y2) \/ ((T_1 = Y3) \/ ((T_4 = Y2) \/ ((T_4 = Y3) \/ (Y2 = Y3))))))))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) ### All 126 % 10.92/11.09 128. (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_4) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_1 = T_4) \/ ((T_1 = Y2) \/ ((T_1 = Y3) \/ ((T_4 = Y2) \/ ((T_4 = Y3) \/ (Y2 = Y3))))))))) (All Y3, (((rr (i2003_11_14_17_19_21224) T_0) /\ ((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_0 = T_1) \/ ((T_0 = T_2) \/ ((T_0 = Y3) \/ ((T_1 = T_2) \/ ((T_1 = Y3) \/ (T_2 = Y3)))))))) (rr (i2003_11_14_17_19_21224) T_0) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_3) (All B, (((T_0 = B) /\ (cp2 T_0)) => (cp2 B))) (cp2 T_0) (-. (cp2 T_1)) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (-. (cp1 T_0)) (cp1 T_2) (-. (cp2 T_3)) (rr (i2003_11_14_17_19_21224) T_4) (rr (i2003_11_14_17_19_21224) T_5) (rr (i2003_11_14_17_19_21224) T_6) (-. (cp1 T_1)) (cp1 T_4) (-. (cp1 T_3)) (-. (cp1 T_5)) (cp2 T_5) (cp3 T_6) (-. (cp3 T_1)) (cp3 T_3) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (-. (cp2 T_6)) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) T_2) /\ ((rr (i2003_11_14_17_19_21224) T_0) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_2 = T_0) \/ ((T_2 = Y2) \/ ((T_2 = Y3) \/ ((T_0 = Y2) \/ ((T_0 = Y3) \/ (Y2 = Y3))))))))) ### All 127 % 10.92/11.09 129. (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) T_2) /\ ((rr (i2003_11_14_17_19_21224) T_0) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_2 = T_0) \/ ((T_2 = Y2) \/ ((T_2 = Y3) \/ ((T_0 = Y2) \/ ((T_0 = Y3) \/ (Y2 = Y3))))))))) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (-. (cp2 T_6)) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (cp3 T_3) (-. (cp3 T_1)) (cp3 T_6) (cp2 T_5) (-. (cp1 T_5)) (-. (cp1 T_3)) (cp1 T_4) (-. (cp1 T_1)) (rr (i2003_11_14_17_19_21224) T_6) (rr (i2003_11_14_17_19_21224) T_5) (rr (i2003_11_14_17_19_21224) T_4) (-. (cp2 T_3)) (cp1 T_2) (-. (cp1 T_0)) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (-. (cp2 T_1)) (cp2 T_0) (rr (i2003_11_14_17_19_21224) T_3) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_0) (All Y3, (((rr (i2003_11_14_17_19_21224) T_0) /\ ((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_0 = T_1) \/ ((T_0 = T_2) \/ ((T_0 = Y3) \/ ((T_1 = T_2) \/ ((T_1 = Y3) \/ (T_2 = Y3)))))))) (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_4) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_1 = T_4) \/ ((T_1 = Y2) \/ ((T_1 = Y3) \/ ((T_4 = Y2) \/ ((T_4 = Y3) \/ (Y2 = Y3))))))))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) ### All 128 % 10.92/11.09 130. (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) T_2) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_2 = Y1) \/ ((T_2 = Y2) \/ ((T_2 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3)))))))))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_4) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_1 = T_4) \/ ((T_1 = Y2) \/ ((T_1 = Y3) \/ ((T_4 = Y2) \/ ((T_4 = Y3) \/ (Y2 = Y3))))))))) (All Y3, (((rr (i2003_11_14_17_19_21224) T_0) /\ ((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_0 = T_1) \/ ((T_0 = T_2) \/ ((T_0 = Y3) \/ ((T_1 = T_2) \/ ((T_1 = Y3) \/ (T_2 = Y3)))))))) (rr (i2003_11_14_17_19_21224) T_0) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_3) (cp2 T_0) (-. (cp2 T_1)) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (-. (cp1 T_0)) (cp1 T_2) (-. (cp2 T_3)) (rr (i2003_11_14_17_19_21224) T_4) (rr (i2003_11_14_17_19_21224) T_5) (rr (i2003_11_14_17_19_21224) T_6) (-. (cp1 T_1)) (cp1 T_4) (-. (cp1 T_3)) (-. (cp1 T_5)) (cp2 T_5) (cp3 T_6) (-. (cp3 T_1)) (cp3 T_3) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (-. (cp2 T_6)) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) ### All 129 % 10.92/11.10 131. (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) T_0) /\ ((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_0 = T_1) \/ ((T_0 = Y2) \/ ((T_0 = Y3) \/ ((T_1 = Y2) \/ ((T_1 = Y3) \/ (Y2 = Y3))))))))) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (-. (cp2 T_6)) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (cp3 T_3) (-. (cp3 T_1)) (cp3 T_6) (cp2 T_5) (-. (cp1 T_5)) (-. (cp1 T_3)) (cp1 T_4) (-. (cp1 T_1)) (rr (i2003_11_14_17_19_21224) T_6) (rr (i2003_11_14_17_19_21224) T_5) (rr (i2003_11_14_17_19_21224) T_4) (-. (cp2 T_3)) (cp1 T_2) (-. (cp1 T_0)) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (-. (cp2 T_1)) (cp2 T_0) (rr (i2003_11_14_17_19_21224) T_3) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_0) (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) T_4) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_1 = T_4) \/ ((T_1 = Y2) \/ ((T_1 = Y3) \/ ((T_4 = Y2) \/ ((T_4 = Y3) \/ (Y2 = Y3))))))))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) T_2) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_2 = Y1) \/ ((T_2 = Y2) \/ ((T_2 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3)))))))))) ### All 130 % 10.92/11.10 132. (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_1 = Y1) \/ ((T_1 = Y2) \/ ((T_1 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3)))))))))) (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) T_2) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_2 = Y1) \/ ((T_2 = Y2) \/ ((T_2 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3)))))))))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (rr (i2003_11_14_17_19_21224) T_0) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_3) (cp2 T_0) (-. (cp2 T_1)) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (-. (cp1 T_0)) (cp1 T_2) (-. (cp2 T_3)) (rr (i2003_11_14_17_19_21224) T_4) (rr (i2003_11_14_17_19_21224) T_5) (rr (i2003_11_14_17_19_21224) T_6) (-. (cp1 T_1)) (cp1 T_4) (-. (cp1 T_3)) (-. (cp1 T_5)) (cp2 T_5) (cp3 T_6) (-. (cp3 T_1)) (cp3 T_3) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (-. (cp2 T_6)) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) T_0) /\ ((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_0 = T_1) \/ ((T_0 = Y2) \/ ((T_0 = Y3) \/ ((T_1 = Y2) \/ ((T_1 = Y3) \/ (Y2 = Y3))))))))) ### All 131 % 10.92/11.10 133. (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) T_0) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_0 = Y1) \/ ((T_0 = Y2) \/ ((T_0 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3)))))))))) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (-. (cp2 T_6)) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (cp3 T_3) (-. (cp3 T_1)) (cp3 T_6) (cp2 T_5) (-. (cp1 T_5)) (-. (cp1 T_3)) (cp1 T_4) (-. (cp1 T_1)) (rr (i2003_11_14_17_19_21224) T_6) (rr (i2003_11_14_17_19_21224) T_5) (rr (i2003_11_14_17_19_21224) T_4) (-. (cp2 T_3)) (cp1 T_2) (-. (cp1 T_0)) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (-. (cp2 T_1)) (cp2 T_0) (rr (i2003_11_14_17_19_21224) T_3) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_0) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) T_2) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_2 = Y1) \/ ((T_2 = Y2) \/ ((T_2 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3)))))))))) (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_1 = Y1) \/ ((T_1 = Y2) \/ ((T_1 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3)))))))))) ### All 132 % 10.92/11.10 134. (All Y0, (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) Y0) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3))))))))))) (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) T_1) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_1 = Y1) \/ ((T_1 = Y2) \/ ((T_1 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3)))))))))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (rr (i2003_11_14_17_19_21224) T_0) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_3) (cp2 T_0) (-. (cp2 T_1)) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (-. (cp1 T_0)) (cp1 T_2) (-. (cp2 T_3)) (rr (i2003_11_14_17_19_21224) T_4) (rr (i2003_11_14_17_19_21224) T_5) (rr (i2003_11_14_17_19_21224) T_6) (-. (cp1 T_1)) (cp1 T_4) (-. (cp1 T_3)) (-. (cp1 T_5)) (cp2 T_5) (cp3 T_6) (-. (cp3 T_1)) (cp3 T_3) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (-. (cp2 T_6)) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) T_0) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_0 = Y1) \/ ((T_0 = Y2) \/ ((T_0 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3)))))))))) ### All 133 % 10.92/11.10 135. (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) T_0) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((T_0 = Y1) \/ ((T_0 = Y2) \/ ((T_0 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3)))))))))) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (-. (cp2 T_6)) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (cp3 T_3) (-. (cp3 T_1)) (cp3 T_6) (cp2 T_5) (-. (cp1 T_5)) (-. (cp1 T_3)) (cp1 T_4) (-. (cp1 T_1)) (rr (i2003_11_14_17_19_21224) T_6) (rr (i2003_11_14_17_19_21224) T_5) (rr (i2003_11_14_17_19_21224) T_4) (-. (cp2 T_3)) (cp1 T_2) (-. (cp1 T_0)) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (-. (cp2 T_1)) (cp2 T_0) (rr (i2003_11_14_17_19_21224) T_3) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_0) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All Y0, (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) Y0) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3))))))))))) ### All 134 % 10.93/11.13 136. (All Y0, (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) Y0) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3))))))))))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (rr (i2003_11_14_17_19_21224) T_0) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_3) (cp2 T_0) (-. (cp2 T_1)) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (-. (cp1 T_0)) (cp1 T_2) (-. (cp2 T_3)) (rr (i2003_11_14_17_19_21224) T_4) (rr (i2003_11_14_17_19_21224) T_5) (rr (i2003_11_14_17_19_21224) T_6) (-. (cp1 T_1)) (cp1 T_4) (-. (cp1 T_3)) (-. (cp1 T_5)) (cp2 T_5) (cp3 T_6) (-. (cp3 T_1)) (cp3 T_3) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (-. (cp2 T_6)) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) ### All 135 % 10.93/11.13 137. (cp3 T_3) (-. (cp3 T_3)) ### Axiom % 10.93/11.13 138. (-. ((cp2 T_3) \/ ((cp4 T_3) \/ ((cp5 T_3) \/ (cp3 T_3))))) (cp3 T_3) ### ConjTree 137 % 10.93/11.13 139. ((cp1 T_3) => (-. ((cp2 T_3) \/ ((cp4 T_3) \/ ((cp5 T_3) \/ (cp3 T_3)))))) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (-. (cp2 T_6)) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (cp3 T_3) (-. (cp3 T_1)) (cp3 T_6) (cp2 T_5) (-. (cp1 T_5)) (cp1 T_4) (-. (cp1 T_1)) (rr (i2003_11_14_17_19_21224) T_6) (rr (i2003_11_14_17_19_21224) T_5) (rr (i2003_11_14_17_19_21224) T_4) (-. (cp2 T_3)) (cp1 T_2) (-. (cp1 T_0)) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (-. (cp2 T_1)) (cp2 T_0) (rr (i2003_11_14_17_19_21224) T_3) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_0) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All Y0, (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) Y0) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3))))))))))) ### Imply 136 138 % 10.93/11.13 140. (All Y0, (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) Y0) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3))))))))))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (rr (i2003_11_14_17_19_21224) T_0) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_3) (cp2 T_0) (-. (cp2 T_1)) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (-. (cp1 T_0)) (cp1 T_2) (-. (cp2 T_3)) (rr (i2003_11_14_17_19_21224) T_4) (rr (i2003_11_14_17_19_21224) T_5) (rr (i2003_11_14_17_19_21224) T_6) (-. (cp1 T_1)) (cp1 T_4) (-. (cp1 T_5)) (cp2 T_5) (cp3 T_6) (-. (cp3 T_1)) (cp3 T_3) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (-. (cp2 T_6)) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) ### All 139 % 10.93/11.13 141. (cp2 T_0) (-. (cp2 T_0)) ### Axiom % 10.93/11.13 142. (-. ((cp2 T_0) \/ ((cp4 T_0) \/ ((cp5 T_0) \/ (cp3 T_0))))) (cp2 T_0) ### ConjTree 141 % 10.93/11.13 143. ((cp1 T_0) => (-. ((cp2 T_0) \/ ((cp4 T_0) \/ ((cp5 T_0) \/ (cp3 T_0)))))) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (-. (cp2 T_6)) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (cp3 T_3) (-. (cp3 T_1)) (cp3 T_6) (cp2 T_5) (-. (cp1 T_5)) (cp1 T_4) (-. (cp1 T_1)) (rr (i2003_11_14_17_19_21224) T_6) (rr (i2003_11_14_17_19_21224) T_5) (rr (i2003_11_14_17_19_21224) T_4) (-. (cp2 T_3)) (cp1 T_2) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (-. (cp2 T_1)) (cp2 T_0) (rr (i2003_11_14_17_19_21224) T_3) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_0) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All Y0, (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) Y0) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3))))))))))) ### Imply 140 142 % 10.93/11.13 144. (All Y0, (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) Y0) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3))))))))))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (rr (i2003_11_14_17_19_21224) T_0) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_3) (cp2 T_0) (-. (cp2 T_1)) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (cp1 T_2) (-. (cp2 T_3)) (rr (i2003_11_14_17_19_21224) T_4) (rr (i2003_11_14_17_19_21224) T_5) (rr (i2003_11_14_17_19_21224) T_6) (-. (cp1 T_1)) (cp1 T_4) (-. (cp1 T_5)) (cp2 T_5) (cp3 T_6) (-. (cp3 T_1)) (cp3 T_3) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (-. (cp2 T_6)) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) ### All 143 % 10.93/11.13 145. (cp2 T_5) (-. (cp2 T_5)) ### Axiom % 10.93/11.13 146. (-. ((cp2 T_5) \/ ((cp4 T_5) \/ ((cp5 T_5) \/ (cp3 T_5))))) (cp2 T_5) ### ConjTree 145 % 10.93/11.13 147. ((cp1 T_5) => (-. ((cp2 T_5) \/ ((cp4 T_5) \/ ((cp5 T_5) \/ (cp3 T_5)))))) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (-. (cp2 T_6)) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (cp3 T_3) (-. (cp3 T_1)) (cp3 T_6) (cp2 T_5) (cp1 T_4) (-. (cp1 T_1)) (rr (i2003_11_14_17_19_21224) T_6) (rr (i2003_11_14_17_19_21224) T_5) (rr (i2003_11_14_17_19_21224) T_4) (-. (cp2 T_3)) (cp1 T_2) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (-. (cp2 T_1)) (cp2 T_0) (rr (i2003_11_14_17_19_21224) T_3) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_0) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All Y0, (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) Y0) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3))))))))))) ### Imply 144 146 % 10.93/11.13 148. (All Y0, (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) Y0) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3))))))))))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (rr (i2003_11_14_17_19_21224) T_0) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_3) (cp2 T_0) (-. (cp2 T_1)) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (cp1 T_2) (-. (cp2 T_3)) (rr (i2003_11_14_17_19_21224) T_4) (rr (i2003_11_14_17_19_21224) T_5) (rr (i2003_11_14_17_19_21224) T_6) (-. (cp1 T_1)) (cp1 T_4) (cp2 T_5) (cp3 T_6) (-. (cp3 T_1)) (cp3 T_3) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (-. (cp2 T_6)) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) ### All 147 % 10.93/11.13 149. (cp4 T_1) (-. (cp4 T_1)) ### Axiom % 10.93/11.13 150. (-. ((cp2 T_1) \/ ((cp4 T_1) \/ ((cp5 T_1) \/ (cp3 T_1))))) (cp4 T_1) ### ConjTree 149 % 10.93/11.13 151. ((cp1 T_1) => (-. ((cp2 T_1) \/ ((cp4 T_1) \/ ((cp5 T_1) \/ (cp3 T_1)))))) (cp4 T_1) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (-. (cp2 T_6)) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (cp3 T_3) (-. (cp3 T_1)) (cp3 T_6) (cp2 T_5) (cp1 T_4) (rr (i2003_11_14_17_19_21224) T_6) (rr (i2003_11_14_17_19_21224) T_5) (rr (i2003_11_14_17_19_21224) T_4) (-. (cp2 T_3)) (cp1 T_2) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (-. (cp2 T_1)) (cp2 T_0) (rr (i2003_11_14_17_19_21224) T_3) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_0) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All Y0, (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) Y0) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3))))))))))) ### Imply 148 150 % 10.93/11.14 152. (All Y0, (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) Y0) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3))))))))))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (rr (i2003_11_14_17_19_21224) T_0) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_3) (cp2 T_0) (-. (cp2 T_1)) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (cp1 T_2) (-. (cp2 T_3)) (rr (i2003_11_14_17_19_21224) T_4) (rr (i2003_11_14_17_19_21224) T_5) (rr (i2003_11_14_17_19_21224) T_6) (cp1 T_4) (cp2 T_5) (cp3 T_6) (-. (cp3 T_1)) (cp3 T_3) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (-. (cp2 T_6)) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (cp4 T_1) ### All 151 % 10.93/11.14 153. (cp3 T_3) (-. (cp3 T_3)) ### Axiom % 10.93/11.14 154. (-. ((cp4 T_3) \/ ((cp5 T_3) \/ (cp3 T_3)))) (cp3 T_3) ### ConjTree 153 % 10.93/11.14 155. ((cp2 T_3) => (-. ((cp4 T_3) \/ ((cp5 T_3) \/ (cp3 T_3))))) (cp4 T_1) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (-. (cp2 T_6)) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (cp3 T_3) (-. (cp3 T_1)) (cp3 T_6) (cp2 T_5) (cp1 T_4) (rr (i2003_11_14_17_19_21224) T_6) (rr (i2003_11_14_17_19_21224) T_5) (rr (i2003_11_14_17_19_21224) T_4) (cp1 T_2) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (-. (cp2 T_1)) (cp2 T_0) (rr (i2003_11_14_17_19_21224) T_3) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_0) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All Y0, (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) Y0) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3))))))))))) ### Imply 152 154 % 10.93/11.14 156. (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) (All Y0, (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) Y0) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3))))))))))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (rr (i2003_11_14_17_19_21224) T_0) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_3) (cp2 T_0) (-. (cp2 T_1)) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (cp1 T_2) (rr (i2003_11_14_17_19_21224) T_4) (rr (i2003_11_14_17_19_21224) T_5) (rr (i2003_11_14_17_19_21224) T_6) (cp1 T_4) (cp2 T_5) (cp3 T_6) (-. (cp3 T_1)) (cp3 T_3) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (-. (cp2 T_6)) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (cp4 T_1) ### All 155 % 10.93/11.14 157. (cp3 T_6) (-. (cp3 T_6)) ### Axiom % 10.93/11.14 158. (-. ((cp4 T_6) \/ ((cp5 T_6) \/ (cp3 T_6)))) (cp3 T_6) ### ConjTree 157 % 10.93/11.14 159. ((cp2 T_6) => (-. ((cp4 T_6) \/ ((cp5 T_6) \/ (cp3 T_6))))) (cp4 T_1) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (cp3 T_3) (-. (cp3 T_1)) (cp3 T_6) (cp2 T_5) (cp1 T_4) (rr (i2003_11_14_17_19_21224) T_6) (rr (i2003_11_14_17_19_21224) T_5) (rr (i2003_11_14_17_19_21224) T_4) (cp1 T_2) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (-. (cp2 T_1)) (cp2 T_0) (rr (i2003_11_14_17_19_21224) T_3) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_0) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All Y0, (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) Y0) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3))))))))))) (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) ### Imply 156 158 % 10.93/11.14 160. (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) (All Y0, (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) Y0) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3))))))))))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (rr (i2003_11_14_17_19_21224) T_0) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_3) (cp2 T_0) (-. (cp2 T_1)) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (cp1 T_2) (rr (i2003_11_14_17_19_21224) T_4) (rr (i2003_11_14_17_19_21224) T_5) (rr (i2003_11_14_17_19_21224) T_6) (cp1 T_4) (cp2 T_5) (cp3 T_6) (-. (cp3 T_1)) (cp3 T_3) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (cp4 T_1) ### All 159 % 10.93/11.14 161. (cp4 T_1) (-. (cp4 T_1)) ### Axiom % 10.93/11.14 162. (-. ((cp4 T_1) \/ ((cp5 T_1) \/ (cp3 T_1)))) (cp4 T_1) ### ConjTree 161 % 10.93/11.14 163. ((cp2 T_1) => (-. ((cp4 T_1) \/ ((cp5 T_1) \/ (cp3 T_1))))) (cp4 T_1) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (cp3 T_3) (-. (cp3 T_1)) (cp3 T_6) (cp2 T_5) (cp1 T_4) (rr (i2003_11_14_17_19_21224) T_6) (rr (i2003_11_14_17_19_21224) T_5) (rr (i2003_11_14_17_19_21224) T_4) (cp1 T_2) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (cp2 T_0) (rr (i2003_11_14_17_19_21224) T_3) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_0) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All Y0, (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) Y0) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3))))))))))) (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) ### Imply 160 162 % 10.93/11.14 164. (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) (All Y0, (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) Y0) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3))))))))))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (rr (i2003_11_14_17_19_21224) T_0) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_3) (cp2 T_0) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (cp1 T_2) (rr (i2003_11_14_17_19_21224) T_4) (rr (i2003_11_14_17_19_21224) T_5) (rr (i2003_11_14_17_19_21224) T_6) (cp1 T_4) (cp2 T_5) (cp3 T_6) (-. (cp3 T_1)) (cp3 T_3) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (cp4 T_1) ### All 163 % 10.93/11.14 165. (cp4 T_1) (-. (cp4 T_1)) ### Axiom % 10.93/11.14 166. (-. ((cp4 T_1) \/ (cp5 T_1))) (cp4 T_1) ### NotOr 165 % 10.93/11.14 167. ((cp3 T_1) => (-. ((cp4 T_1) \/ (cp5 T_1)))) (cp4 T_1) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (cp3 T_3) (cp3 T_6) (cp2 T_5) (cp1 T_4) (rr (i2003_11_14_17_19_21224) T_6) (rr (i2003_11_14_17_19_21224) T_5) (rr (i2003_11_14_17_19_21224) T_4) (cp1 T_2) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (cp2 T_0) (rr (i2003_11_14_17_19_21224) T_3) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_0) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All Y0, (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) Y0) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3))))))))))) (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) ### Imply 164 166 % 10.93/11.14 168. (All X, ((cp3 X) => (-. ((cp4 X) \/ (cp5 X))))) (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) (All Y0, (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) Y0) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3))))))))))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (rr (i2003_11_14_17_19_21224) T_0) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_3) (cp2 T_0) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (cp1 T_2) (rr (i2003_11_14_17_19_21224) T_4) (rr (i2003_11_14_17_19_21224) T_5) (rr (i2003_11_14_17_19_21224) T_6) (cp1 T_4) (cp2 T_5) (cp3 T_6) (cp3 T_3) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (cp4 T_1) ### All 167 % 10.93/11.14 169. ((rr (i2003_11_14_17_19_21224) T_5) /\ ((cp2 T_5) /\ (cp T_5))) (cp4 T_1) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (cp3 T_3) (cp3 T_6) (cp1 T_4) (rr (i2003_11_14_17_19_21224) T_6) (rr (i2003_11_14_17_19_21224) T_4) (cp1 T_2) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (cp2 T_0) (rr (i2003_11_14_17_19_21224) T_3) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_0) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All Y0, (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) Y0) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3))))))))))) (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) (All X, ((cp3 X) => (-. ((cp4 X) \/ (cp5 X))))) ### ConjTree 168 % 10.93/11.14 170. (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ ((cp2 Y) /\ (cp Y)))) (All X, ((cp3 X) => (-. ((cp4 X) \/ (cp5 X))))) (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) (All Y0, (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) Y0) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3))))))))))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (rr (i2003_11_14_17_19_21224) T_0) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_3) (cp2 T_0) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (cp1 T_2) (rr (i2003_11_14_17_19_21224) T_4) (rr (i2003_11_14_17_19_21224) T_6) (cp1 T_4) (cp3 T_6) (cp3 T_3) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (cp4 T_1) ### Exists 169 % 10.93/11.14 171. ((rr (i2003_11_14_17_19_21224) T_3) /\ ((cp T_3) /\ (cp3 T_3))) (cp4 T_1) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (cp3 T_6) (cp1 T_4) (rr (i2003_11_14_17_19_21224) T_6) (rr (i2003_11_14_17_19_21224) T_4) (cp1 T_2) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (cp2 T_0) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_0) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All Y0, (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) Y0) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3))))))))))) (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) (All X, ((cp3 X) => (-. ((cp4 X) \/ (cp5 X))))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ ((cp2 Y) /\ (cp Y)))) ### ConjTree 170 % 10.93/11.14 172. (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ ((cp Y) /\ (cp3 Y)))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ ((cp2 Y) /\ (cp Y)))) (All X, ((cp3 X) => (-. ((cp4 X) \/ (cp5 X))))) (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) (All Y0, (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) Y0) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3))))))))))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (rr (i2003_11_14_17_19_21224) T_0) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_2) (cp2 T_0) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (cp1 T_2) (rr (i2003_11_14_17_19_21224) T_4) (rr (i2003_11_14_17_19_21224) T_6) (cp1 T_4) (cp3 T_6) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (cp4 T_1) ### Exists 171 % 10.93/11.14 173. ((rr (i2003_11_14_17_19_21224) T_6) /\ (cp3 T_6)) (cp4 T_1) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (cp1 T_4) (rr (i2003_11_14_17_19_21224) T_4) (cp1 T_2) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (cp2 T_0) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_0) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All Y0, (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) Y0) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3))))))))))) (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) (All X, ((cp3 X) => (-. ((cp4 X) \/ (cp5 X))))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ ((cp2 Y) /\ (cp Y)))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ ((cp Y) /\ (cp3 Y)))) ### And 172 % 10.93/11.14 174. (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ (cp3 Y))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ ((cp Y) /\ (cp3 Y)))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ ((cp2 Y) /\ (cp Y)))) (All X, ((cp3 X) => (-. ((cp4 X) \/ (cp5 X))))) (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) (All Y0, (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) Y0) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3))))))))))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (rr (i2003_11_14_17_19_21224) T_0) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_2) (cp2 T_0) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (cp1 T_2) (rr (i2003_11_14_17_19_21224) T_4) (cp1 T_4) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (cp4 T_1) ### Exists 173 % 10.93/11.14 175. ((rr (i2003_11_14_17_19_21224) T_0) /\ (cp2 T_0)) (cp4 T_1) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (cp1 T_4) (rr (i2003_11_14_17_19_21224) T_4) (cp1 T_2) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (rr (i2003_11_14_17_19_21224) T_2) (rr (i2003_11_14_17_19_21224) T_1) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All Y0, (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) Y0) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3))))))))))) (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) (All X, ((cp3 X) => (-. ((cp4 X) \/ (cp5 X))))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ ((cp2 Y) /\ (cp Y)))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ ((cp Y) /\ (cp3 Y)))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ (cp3 Y))) ### And 174 % 10.93/11.14 176. (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ (cp2 Y))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ (cp3 Y))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ ((cp Y) /\ (cp3 Y)))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ ((cp2 Y) /\ (cp Y)))) (All X, ((cp3 X) => (-. ((cp4 X) \/ (cp5 X))))) (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) (All Y0, (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) Y0) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3))))))))))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (rr (i2003_11_14_17_19_21224) T_1) (rr (i2003_11_14_17_19_21224) T_2) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (cp1 T_2) (rr (i2003_11_14_17_19_21224) T_4) (cp1 T_4) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (cp4 T_1) ### Exists 175 % 10.93/11.15 177. ((rr (i2003_11_14_17_19_21224) T_1) /\ (cp4 T_1)) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (cp1 T_4) (rr (i2003_11_14_17_19_21224) T_4) (cp1 T_2) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (rr (i2003_11_14_17_19_21224) T_2) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All Y0, (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) Y0) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3))))))))))) (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) (All X, ((cp3 X) => (-. ((cp4 X) \/ (cp5 X))))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ ((cp2 Y) /\ (cp Y)))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ ((cp Y) /\ (cp3 Y)))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ (cp3 Y))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ (cp2 Y))) ### And 176 % 10.93/11.15 178. (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ (cp4 Y))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ (cp2 Y))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ (cp3 Y))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ ((cp Y) /\ (cp3 Y)))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ ((cp2 Y) /\ (cp Y)))) (All X, ((cp3 X) => (-. ((cp4 X) \/ (cp5 X))))) (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) (All Y0, (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) Y0) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3))))))))))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (rr (i2003_11_14_17_19_21224) T_2) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (cp1 T_2) (rr (i2003_11_14_17_19_21224) T_4) (cp1 T_4) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) ### Exists 177 % 10.93/11.15 179. ((rr (i2003_11_14_17_19_21224) T_4) /\ (cp1 T_4)) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (cp1 T_2) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (rr (i2003_11_14_17_19_21224) T_2) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All Y0, (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) Y0) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3))))))))))) (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) (All X, ((cp3 X) => (-. ((cp4 X) \/ (cp5 X))))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ ((cp2 Y) /\ (cp Y)))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ ((cp Y) /\ (cp3 Y)))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ (cp3 Y))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ (cp2 Y))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ (cp4 Y))) ### And 178 % 10.93/11.15 180. (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ (cp1 Y))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ (cp4 Y))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ (cp2 Y))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ (cp3 Y))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ ((cp Y) /\ (cp3 Y)))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ ((cp2 Y) /\ (cp Y)))) (All X, ((cp3 X) => (-. ((cp4 X) \/ (cp5 X))))) (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) (All Y0, (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) Y0) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3))))))))))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (rr (i2003_11_14_17_19_21224) T_2) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (cp1 T_2) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) ### Exists 179 % 10.93/11.15 181. ((rr (i2003_11_14_17_19_21224) T_2) /\ ((cp T_2) /\ (cp1 T_2))) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All Y0, (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) Y0) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3))))))))))) (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) (All X, ((cp3 X) => (-. ((cp4 X) \/ (cp5 X))))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ ((cp2 Y) /\ (cp Y)))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ ((cp Y) /\ (cp3 Y)))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ (cp3 Y))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ (cp2 Y))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ (cp4 Y))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ (cp1 Y))) ### ConjTree 180 % 10.93/11.15 182. (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ ((cp Y) /\ (cp1 Y)))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ (cp1 Y))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ (cp4 Y))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ (cp2 Y))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ (cp3 Y))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ ((cp Y) /\ (cp3 Y)))) (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ ((cp2 Y) /\ (cp Y)))) (All X, ((cp3 X) => (-. ((cp4 X) \/ (cp5 X))))) (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) (All Y0, (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) Y0) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3))))))))))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) ### Exists 181 % 10.93/11.15 183. ((Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ ((cp Y) /\ (cp1 Y)))) /\ ((Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ (cp1 Y))) /\ ((Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ (cp4 Y))) /\ ((All Y0, (All Y1, (All Y2, (All Y3, (((rr (i2003_11_14_17_19_21224) Y0) /\ ((rr (i2003_11_14_17_19_21224) Y1) /\ ((rr (i2003_11_14_17_19_21224) Y2) /\ (rr (i2003_11_14_17_19_21224) Y3)))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ (Y2 = Y3))))))))))) /\ ((Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ (cp2 Y))) /\ ((Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ (cp3 Y))) /\ ((Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ ((cp Y) /\ (cp3 Y)))) /\ (Ex Y, ((rr (i2003_11_14_17_19_21224) Y) /\ ((cp2 Y) /\ (cp Y))))))))))) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) (All X, ((cp3 X) => (-. ((cp4 X) \/ (cp5 X))))) ### ConjTree 182 % 10.93/11.15 184. (cUnsatisfiable (i2003_11_14_17_19_21224)) (All X, ((cp3 X) => (-. ((cp4 X) \/ (cp5 X))))) (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All A, (All B, (((A = B) /\ (cp1 A)) => (cp1 B)))) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) ### Definition-Pseudo(cUnsatisfiable) 183 % 10.93/11.15 % SZS output end Proof % 10.93/11.15 (* END-PROOF *) %------------------------------------------------------------------------------