%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : ALG186+1 : TPTP v8.1.0. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n020.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 : Thu Jul 14 18:06:10 EDT 2022 % Result : Theorem 1.32s 1.49s % Output : Proof 1.32s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : ALG186+1 : TPTP v8.1.0. Released v2.7.0. % 0.04/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.34 % Computer : n020.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.35 % CPULimit : 300 % 0.12/0.35 % WCLimit : 600 % 0.12/0.35 % DateTime : Wed Jun 8 15:37:36 EDT 2022 % 0.12/0.35 % CPUTime : % 1.32/1.49 % SZS status Theorem % 1.32/1.49 (* PROOF-FOUND *) % 1.32/1.49 (* BEGIN-PROOF *) % 1.32/1.49 % SZS output start Proof % 1.32/1.49 1. ((op (e0) (e4)) = (e0)) ((e0) != (op (e0) (e4))) ### Sym(=) % 1.32/1.49 2. ((op (e0) (e4)) = (e0)) ((e0) != (op (e0) (e4))) ### Sym(=) % 1.32/1.49 3. ((e4) != (e4)) ### NotEqual % 1.32/1.49 4. ((e0) != (e4)) ((op (e0) (e4)) = (e4)) ((op (e0) (e4)) = (e0)) ### TransEq 1 2 3 % 1.32/1.49 5. ((op (e1) (e4)) = (e1)) ((e1) != (op (e1) (e4))) ### Sym(=) % 1.32/1.49 6. ((op (e1) (e4)) = (e1)) ((e1) != (op (e1) (e4))) ### Sym(=) % 1.32/1.49 7. ((e3) != (e3)) ### NotEqual % 1.32/1.49 8. ((e1) != (e3)) ((op (e1) (e4)) = (e3)) ((op (e1) (e4)) = (e1)) ### TransEq 5 6 7 % 1.32/1.49 9. ((op (e2) (e4)) = (e2)) ((e2) != (op (e2) (e4))) ### Sym(=) % 1.32/1.49 10. ((op (e2) (e4)) = (e2)) ((e2) != (op (e2) (e4))) ### Sym(=) % 1.32/1.49 11. ((e0) != (e0)) ### NotEqual % 1.32/1.49 12. ((e0) != (e2)) ((op (e2) (e4)) = (e0)) ((op (e2) (e4)) = (e2)) ### TransEq-sym 9 10 11 % 1.32/1.49 13. ((op (e3) (e4)) = (e3)) ((e3) != (op (e3) (e4))) ### Sym(=) % 1.32/1.49 14. ((op (e3) (e4)) = (e3)) ((e3) != (op (e3) (e4))) ### Sym(=) % 1.32/1.49 15. ((e2) != (e2)) ### NotEqual % 1.32/1.49 16. ((e2) != (e3)) ((op (e3) (e4)) = (e2)) ((op (e3) (e4)) = (e3)) ### TransEq-sym 13 14 15 % 1.32/1.49 17. ((op (e4) (e4)) = (e4)) ((e4) != (op (e4) (e4))) ### Sym(=) % 1.32/1.49 18. ((op (e4) (e4)) = (e4)) ((e4) != (op (e4) (e4))) ### Sym(=) % 1.32/1.49 19. ((e1) != (e1)) ### NotEqual % 1.32/1.49 20. ((e1) != (e4)) ((op (e4) (e4)) = (e1)) ((op (e4) (e4)) = (e4)) ### TransEq-sym 17 18 19 % 1.32/1.49 21. (-. (((op (e0) (e4)) != (e0)) /\ (((op (e1) (e4)) != (e1)) /\ (((op (e2) (e4)) != (e2)) /\ (((op (e3) (e4)) != (e3)) /\ ((op (e4) (e4)) != (e4))))))) ((op (e4) (e4)) = (e1)) ((e1) != (e4)) ((op (e3) (e4)) = (e2)) ((e2) != (e3)) ((op (e2) (e4)) = (e0)) ((e0) != (e2)) ((op (e1) (e4)) = (e3)) ((e1) != (e3)) ((op (e0) (e4)) = (e4)) ((e0) != (e4)) ### DisjTree 4 8 12 16 20 % 1.32/1.49 22. (-. ((((op (e0) (e0)) != (e0)) /\ (((op (e1) (e0)) != (e1)) /\ (((op (e2) (e0)) != (e2)) /\ (((op (e3) (e0)) != (e3)) /\ ((op (e4) (e0)) != (e4)))))) \/ ((((op (e0) (e1)) != (e0)) /\ (((op (e1) (e1)) != (e1)) /\ (((op (e2) (e1)) != (e2)) /\ (((op (e3) (e1)) != (e3)) /\ ((op (e4) (e1)) != (e4)))))) \/ ((((op (e0) (e2)) != (e0)) /\ (((op (e1) (e2)) != (e1)) /\ (((op (e2) (e2)) != (e2)) /\ (((op (e3) (e2)) != (e3)) /\ ((op (e4) (e2)) != (e4)))))) \/ ((((op (e0) (e3)) != (e0)) /\ (((op (e1) (e3)) != (e1)) /\ (((op (e2) (e3)) != (e2)) /\ (((op (e3) (e3)) != (e3)) /\ ((op (e4) (e3)) != (e4)))))) \/ (((op (e0) (e4)) != (e0)) /\ (((op (e1) (e4)) != (e1)) /\ (((op (e2) (e4)) != (e2)) /\ (((op (e3) (e4)) != (e3)) /\ ((op (e4) (e4)) != (e4))))))))))) ((e0) != (e4)) ((op (e0) (e4)) = (e4)) ((e1) != (e3)) ((op (e1) (e4)) = (e3)) ((e0) != (e2)) ((op (e2) (e4)) = (e0)) ((e2) != (e3)) ((op (e3) (e4)) = (e2)) ((e1) != (e4)) ((op (e4) (e4)) = (e1)) ### ConjTree 21 % 1.32/1.49 23. ((op (e0) (e0)) = (e3)) ((op (e0) (e0)) != (e3)) ### Axiom % 1.32/1.49 24. (-. (((op (e0) (e0)) = (e0)) \/ (((op (e0) (e0)) = (e1)) \/ (((op (e0) (e0)) = (e2)) \/ (((op (e0) (e0)) = (e3)) \/ ((op (e0) (e0)) = (e4))))))) ((op (e0) (e0)) = (e3)) ### ConjTree 23 % 1.32/1.49 25. ((op (e0) (e1)) = (e2)) ((op (e0) (e1)) != (e2)) ### Axiom % 1.32/1.49 26. (-. (((op (e0) (e1)) = (e0)) \/ (((op (e0) (e1)) = (e1)) \/ (((op (e0) (e1)) = (e2)) \/ (((op (e0) (e1)) = (e3)) \/ ((op (e0) (e1)) = (e4))))))) ((op (e0) (e1)) = (e2)) ### ConjTree 25 % 1.32/1.49 27. ((op (e0) (e2)) = (e0)) ((op (e0) (e2)) != (e0)) ### Axiom % 1.32/1.49 28. (-. (((op (e0) (e2)) = (e0)) \/ (((op (e0) (e2)) = (e1)) \/ (((op (e0) (e2)) = (e2)) \/ (((op (e0) (e2)) = (e3)) \/ ((op (e0) (e2)) = (e4))))))) ((op (e0) (e2)) = (e0)) ### ConjTree 27 % 1.32/1.49 29. ((op (e0) (e3)) = (e1)) ((op (e0) (e3)) != (e1)) ### Axiom % 1.32/1.49 30. (-. (((op (e0) (e3)) = (e0)) \/ (((op (e0) (e3)) = (e1)) \/ (((op (e0) (e3)) = (e2)) \/ (((op (e0) (e3)) = (e3)) \/ ((op (e0) (e3)) = (e4))))))) ((op (e0) (e3)) = (e1)) ### ConjTree 29 % 1.32/1.49 31. ((op (e0) (e4)) = (e4)) ((op (e0) (e4)) != (e4)) ### Axiom % 1.32/1.49 32. (-. (((op (e0) (e4)) = (e0)) \/ (((op (e0) (e4)) = (e1)) \/ (((op (e0) (e4)) = (e2)) \/ (((op (e0) (e4)) = (e3)) \/ ((op (e0) (e4)) = (e4))))))) ((op (e0) (e4)) = (e4)) ### ConjTree 31 % 1.32/1.49 33. ((op (e1) (e0)) = (e0)) ((op (e1) (e0)) != (e0)) ### Axiom % 1.32/1.49 34. (-. (((op (e1) (e0)) = (e0)) \/ (((op (e1) (e0)) = (e1)) \/ (((op (e1) (e0)) = (e2)) \/ (((op (e1) (e0)) = (e3)) \/ ((op (e1) (e0)) = (e4))))))) ((op (e1) (e0)) = (e0)) ### ConjTree 33 % 1.32/1.49 35. ((op (e1) (e1)) = (e4)) ((op (e1) (e1)) != (e4)) ### Axiom % 1.32/1.49 36. (-. (((op (e1) (e1)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e1) (e1)) = (e2)) \/ (((op (e1) (e1)) = (e3)) \/ ((op (e1) (e1)) = (e4))))))) ((op (e1) (e1)) = (e4)) ### ConjTree 35 % 1.32/1.49 37. ((op (e1) (e2)) = (e1)) ((op (e1) (e2)) != (e1)) ### Axiom % 1.32/1.49 38. (-. (((op (e1) (e2)) = (e0)) \/ (((op (e1) (e2)) = (e1)) \/ (((op (e1) (e2)) = (e2)) \/ (((op (e1) (e2)) = (e3)) \/ ((op (e1) (e2)) = (e4))))))) ((op (e1) (e2)) = (e1)) ### ConjTree 37 % 1.32/1.49 39. ((op (e1) (e3)) = (e2)) ((op (e1) (e3)) != (e2)) ### Axiom % 1.32/1.49 40. (-. (((op (e1) (e3)) = (e0)) \/ (((op (e1) (e3)) = (e1)) \/ (((op (e1) (e3)) = (e2)) \/ (((op (e1) (e3)) = (e3)) \/ ((op (e1) (e3)) = (e4))))))) ((op (e1) (e3)) = (e2)) ### ConjTree 39 % 1.32/1.49 41. ((op (e1) (e4)) = (e3)) ((op (e1) (e4)) != (e3)) ### Axiom % 1.32/1.49 42. (-. (((op (e1) (e4)) = (e0)) \/ (((op (e1) (e4)) = (e1)) \/ (((op (e1) (e4)) = (e2)) \/ (((op (e1) (e4)) = (e3)) \/ ((op (e1) (e4)) = (e4))))))) ((op (e1) (e4)) = (e3)) ### ConjTree 41 % 1.32/1.49 43. ((op (e2) (e0)) = (e1)) ((op (e2) (e0)) != (e1)) ### Axiom % 1.32/1.49 44. (-. (((op (e2) (e0)) = (e0)) \/ (((op (e2) (e0)) = (e1)) \/ (((op (e2) (e0)) = (e2)) \/ (((op (e2) (e0)) = (e3)) \/ ((op (e2) (e0)) = (e4))))))) ((op (e2) (e0)) = (e1)) ### ConjTree 43 % 1.32/1.49 45. ((op (e2) (e1)) = (e3)) ((op (e2) (e1)) != (e3)) ### Axiom % 1.32/1.49 46. (-. (((op (e2) (e1)) = (e0)) \/ (((op (e2) (e1)) = (e1)) \/ (((op (e2) (e1)) = (e2)) \/ (((op (e2) (e1)) = (e3)) \/ ((op (e2) (e1)) = (e4))))))) ((op (e2) (e1)) = (e3)) ### ConjTree 45 % 1.32/1.49 47. ((op (e2) (e2)) = (e2)) ((op (e2) (e2)) != (e2)) ### Axiom % 1.32/1.49 48. (-. (((op (e2) (e2)) = (e0)) \/ (((op (e2) (e2)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e2) (e2)) = (e3)) \/ ((op (e2) (e2)) = (e4))))))) ((op (e2) (e2)) = (e2)) ### ConjTree 47 % 1.32/1.49 49. ((op (e2) (e3)) = (e4)) ((op (e2) (e3)) != (e4)) ### Axiom % 1.32/1.49 50. (-. (((op (e2) (e3)) = (e0)) \/ (((op (e2) (e3)) = (e1)) \/ (((op (e2) (e3)) = (e2)) \/ (((op (e2) (e3)) = (e3)) \/ ((op (e2) (e3)) = (e4))))))) ((op (e2) (e3)) = (e4)) ### ConjTree 49 % 1.32/1.49 51. ((op (e2) (e4)) = (e0)) ((op (e2) (e4)) != (e0)) ### Axiom % 1.32/1.49 52. (-. (((op (e2) (e4)) = (e0)) \/ (((op (e2) (e4)) = (e1)) \/ (((op (e2) (e4)) = (e2)) \/ (((op (e2) (e4)) = (e3)) \/ ((op (e2) (e4)) = (e4))))))) ((op (e2) (e4)) = (e0)) ### ConjTree 51 % 1.32/1.49 53. ((op (e3) (e0)) = (e4)) ((op (e3) (e0)) != (e4)) ### Axiom % 1.32/1.49 54. (-. (((op (e3) (e0)) = (e0)) \/ (((op (e3) (e0)) = (e1)) \/ (((op (e3) (e0)) = (e2)) \/ (((op (e3) (e0)) = (e3)) \/ ((op (e3) (e0)) = (e4))))))) ((op (e3) (e0)) = (e4)) ### ConjTree 53 % 1.32/1.49 55. ((op (e3) (e1)) = (e1)) ((op (e3) (e1)) != (e1)) ### Axiom % 1.32/1.49 56. (-. (((op (e3) (e1)) = (e0)) \/ (((op (e3) (e1)) = (e1)) \/ (((op (e3) (e1)) = (e2)) \/ (((op (e3) (e1)) = (e3)) \/ ((op (e3) (e1)) = (e4))))))) ((op (e3) (e1)) = (e1)) ### ConjTree 55 % 1.32/1.49 57. ((op (e3) (e2)) = (e3)) ((op (e3) (e2)) != (e3)) ### Axiom % 1.32/1.49 58. (-. (((op (e3) (e2)) = (e0)) \/ (((op (e3) (e2)) = (e1)) \/ (((op (e3) (e2)) = (e2)) \/ (((op (e3) (e2)) = (e3)) \/ ((op (e3) (e2)) = (e4))))))) ((op (e3) (e2)) = (e3)) ### ConjTree 57 % 1.32/1.49 59. ((op (e3) (e3)) = (e0)) ((op (e3) (e3)) != (e0)) ### Axiom % 1.32/1.49 60. (-. (((op (e3) (e3)) = (e0)) \/ (((op (e3) (e3)) = (e1)) \/ (((op (e3) (e3)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ ((op (e3) (e3)) = (e4))))))) ((op (e3) (e3)) = (e0)) ### ConjTree 59 % 1.32/1.49 61. ((op (e3) (e4)) = (e2)) ((op (e3) (e4)) != (e2)) ### Axiom % 1.32/1.49 62. (-. (((op (e3) (e4)) = (e0)) \/ (((op (e3) (e4)) = (e1)) \/ (((op (e3) (e4)) = (e2)) \/ (((op (e3) (e4)) = (e3)) \/ ((op (e3) (e4)) = (e4))))))) ((op (e3) (e4)) = (e2)) ### ConjTree 61 % 1.32/1.49 63. ((op (e4) (e0)) = (e2)) ((op (e4) (e0)) != (e2)) ### Axiom % 1.32/1.49 64. (-. (((op (e4) (e0)) = (e0)) \/ (((op (e4) (e0)) = (e1)) \/ (((op (e4) (e0)) = (e2)) \/ (((op (e4) (e0)) = (e3)) \/ ((op (e4) (e0)) = (e4))))))) ((op (e4) (e0)) = (e2)) ### ConjTree 63 % 1.32/1.49 65. ((op (e4) (e1)) = (e0)) ((op (e4) (e1)) != (e0)) ### Axiom % 1.32/1.49 66. (-. (((op (e4) (e1)) = (e0)) \/ (((op (e4) (e1)) = (e1)) \/ (((op (e4) (e1)) = (e2)) \/ (((op (e4) (e1)) = (e3)) \/ ((op (e4) (e1)) = (e4))))))) ((op (e4) (e1)) = (e0)) ### ConjTree 65 % 1.32/1.49 67. ((op (e4) (e2)) = (e4)) ((op (e4) (e2)) != (e4)) ### Axiom % 1.32/1.49 68. (-. (((op (e4) (e2)) = (e0)) \/ (((op (e4) (e2)) = (e1)) \/ (((op (e4) (e2)) = (e2)) \/ (((op (e4) (e2)) = (e3)) \/ ((op (e4) (e2)) = (e4))))))) ((op (e4) (e2)) = (e4)) ### ConjTree 67 % 1.32/1.49 69. ((op (e4) (e3)) = (e3)) ((op (e4) (e3)) != (e3)) ### Axiom % 1.32/1.49 70. (-. (((op (e4) (e3)) = (e0)) \/ (((op (e4) (e3)) = (e1)) \/ (((op (e4) (e3)) = (e2)) \/ (((op (e4) (e3)) = (e3)) \/ ((op (e4) (e3)) = (e4))))))) ((op (e4) (e3)) = (e3)) ### ConjTree 69 % 1.32/1.49 71. ((op (e4) (e4)) = (e1)) ((op (e4) (e4)) != (e1)) ### Axiom % 1.32/1.49 72. (-. (((op (e4) (e4)) = (e0)) \/ (((op (e4) (e4)) = (e1)) \/ (((op (e4) (e4)) = (e2)) \/ (((op (e4) (e4)) = (e3)) \/ ((op (e4) (e4)) = (e4))))))) ((op (e4) (e4)) = (e1)) ### ConjTree 71 % 1.32/1.49 73. ((op (e0) (e2)) = (e0)) ((op (e0) (e2)) != (e0)) ### Axiom % 1.32/1.49 74. (-. (((op (e0) (e0)) = (e0)) \/ (((op (e0) (e1)) = (e0)) \/ (((op (e0) (e2)) = (e0)) \/ (((op (e0) (e3)) = (e0)) \/ ((op (e0) (e4)) = (e0))))))) ((op (e0) (e2)) = (e0)) ### ConjTree 73 % 1.32/1.49 75. ((op (e1) (e0)) = (e0)) ((op (e1) (e0)) != (e0)) ### Axiom % 1.32/1.49 76. (-. (((op (e0) (e0)) = (e0)) \/ (((op (e1) (e0)) = (e0)) \/ (((op (e2) (e0)) = (e0)) \/ (((op (e3) (e0)) = (e0)) \/ ((op (e4) (e0)) = (e0))))))) ((op (e1) (e0)) = (e0)) ### ConjTree 75 % 1.32/1.49 77. ((op (e0) (e3)) = (e1)) ((op (e0) (e3)) != (e1)) ### Axiom % 1.32/1.49 78. (-. (((op (e0) (e0)) = (e1)) \/ (((op (e0) (e1)) = (e1)) \/ (((op (e0) (e2)) = (e1)) \/ (((op (e0) (e3)) = (e1)) \/ ((op (e0) (e4)) = (e1))))))) ((op (e0) (e3)) = (e1)) ### ConjTree 77 % 1.32/1.49 79. ((op (e2) (e0)) = (e1)) ((op (e2) (e0)) != (e1)) ### Axiom % 1.32/1.49 80. (-. (((op (e0) (e0)) = (e1)) \/ (((op (e1) (e0)) = (e1)) \/ (((op (e2) (e0)) = (e1)) \/ (((op (e3) (e0)) = (e1)) \/ ((op (e4) (e0)) = (e1))))))) ((op (e2) (e0)) = (e1)) ### ConjTree 79 % 1.32/1.49 81. ((op (e0) (e1)) = (e2)) ((op (e0) (e1)) != (e2)) ### Axiom % 1.32/1.49 82. (-. (((op (e0) (e0)) = (e2)) \/ (((op (e0) (e1)) = (e2)) \/ (((op (e0) (e2)) = (e2)) \/ (((op (e0) (e3)) = (e2)) \/ ((op (e0) (e4)) = (e2))))))) ((op (e0) (e1)) = (e2)) ### ConjTree 81 % 1.32/1.49 83. ((op (e4) (e0)) = (e2)) ((op (e4) (e0)) != (e2)) ### Axiom % 1.32/1.49 84. (-. (((op (e0) (e0)) = (e2)) \/ (((op (e1) (e0)) = (e2)) \/ (((op (e2) (e0)) = (e2)) \/ (((op (e3) (e0)) = (e2)) \/ ((op (e4) (e0)) = (e2))))))) ((op (e4) (e0)) = (e2)) ### ConjTree 83 % 1.32/1.49 85. ((op (e0) (e0)) = (e3)) ((op (e0) (e0)) != (e3)) ### Axiom % 1.32/1.49 86. (-. (((op (e0) (e0)) = (e3)) \/ (((op (e0) (e1)) = (e3)) \/ (((op (e0) (e2)) = (e3)) \/ (((op (e0) (e3)) = (e3)) \/ ((op (e0) (e4)) = (e3))))))) ((op (e0) (e0)) = (e3)) ### ConjTree 85 % 1.32/1.49 87. ((op (e0) (e0)) = (e3)) ((op (e0) (e0)) != (e3)) ### Axiom % 1.32/1.49 88. (-. (((op (e0) (e0)) = (e3)) \/ (((op (e1) (e0)) = (e3)) \/ (((op (e2) (e0)) = (e3)) \/ (((op (e3) (e0)) = (e3)) \/ ((op (e4) (e0)) = (e3))))))) ((op (e0) (e0)) = (e3)) ### ConjTree 87 % 1.32/1.49 89. ((op (e0) (e4)) = (e4)) ((op (e0) (e4)) != (e4)) ### Axiom % 1.32/1.49 90. (-. (((op (e0) (e0)) = (e4)) \/ (((op (e0) (e1)) = (e4)) \/ (((op (e0) (e2)) = (e4)) \/ (((op (e0) (e3)) = (e4)) \/ ((op (e0) (e4)) = (e4))))))) ((op (e0) (e4)) = (e4)) ### ConjTree 89 % 1.32/1.49 91. ((op (e3) (e0)) = (e4)) ((op (e3) (e0)) != (e4)) ### Axiom % 1.32/1.49 92. (-. (((op (e0) (e0)) = (e4)) \/ (((op (e1) (e0)) = (e4)) \/ (((op (e2) (e0)) = (e4)) \/ (((op (e3) (e0)) = (e4)) \/ ((op (e4) (e0)) = (e4))))))) ((op (e3) (e0)) = (e4)) ### ConjTree 91 % 1.32/1.49 93. ((op (e1) (e0)) = (e0)) ((op (e1) (e0)) != (e0)) ### Axiom % 1.32/1.49 94. (-. (((op (e1) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e0)) \/ (((op (e1) (e2)) = (e0)) \/ (((op (e1) (e3)) = (e0)) \/ ((op (e1) (e4)) = (e0))))))) ((op (e1) (e0)) = (e0)) ### ConjTree 93 % 1.32/1.49 95. ((op (e4) (e1)) = (e0)) ((op (e4) (e1)) != (e0)) ### Axiom % 1.32/1.49 96. (-. (((op (e0) (e1)) = (e0)) \/ (((op (e1) (e1)) = (e0)) \/ (((op (e2) (e1)) = (e0)) \/ (((op (e3) (e1)) = (e0)) \/ ((op (e4) (e1)) = (e0))))))) ((op (e4) (e1)) = (e0)) ### ConjTree 95 % 1.32/1.49 97. ((op (e1) (e2)) = (e1)) ((op (e1) (e2)) != (e1)) ### Axiom % 1.32/1.49 98. (-. (((op (e1) (e0)) = (e1)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e1) (e2)) = (e1)) \/ (((op (e1) (e3)) = (e1)) \/ ((op (e1) (e4)) = (e1))))))) ((op (e1) (e2)) = (e1)) ### ConjTree 97 % 1.32/1.49 99. ((op (e3) (e1)) = (e1)) ((op (e3) (e1)) != (e1)) ### Axiom % 1.32/1.49 100. (-. (((op (e0) (e1)) = (e1)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e1)) = (e1)) \/ (((op (e3) (e1)) = (e1)) \/ ((op (e4) (e1)) = (e1))))))) ((op (e3) (e1)) = (e1)) ### ConjTree 99 % 1.32/1.49 101. ((op (e1) (e3)) = (e2)) ((op (e1) (e3)) != (e2)) ### Axiom % 1.32/1.49 102. (-. (((op (e1) (e0)) = (e2)) \/ (((op (e1) (e1)) = (e2)) \/ (((op (e1) (e2)) = (e2)) \/ (((op (e1) (e3)) = (e2)) \/ ((op (e1) (e4)) = (e2))))))) ((op (e1) (e3)) = (e2)) ### ConjTree 101 % 1.32/1.49 103. ((op (e0) (e1)) = (e2)) ((op (e0) (e1)) != (e2)) ### Axiom % 1.32/1.49 104. (-. (((op (e0) (e1)) = (e2)) \/ (((op (e1) (e1)) = (e2)) \/ (((op (e2) (e1)) = (e2)) \/ (((op (e3) (e1)) = (e2)) \/ ((op (e4) (e1)) = (e2))))))) ((op (e0) (e1)) = (e2)) ### ConjTree 103 % 1.32/1.49 105. ((op (e1) (e4)) = (e3)) ((op (e1) (e4)) != (e3)) ### Axiom % 1.32/1.49 106. (-. (((op (e1) (e0)) = (e3)) \/ (((op (e1) (e1)) = (e3)) \/ (((op (e1) (e2)) = (e3)) \/ (((op (e1) (e3)) = (e3)) \/ ((op (e1) (e4)) = (e3))))))) ((op (e1) (e4)) = (e3)) ### ConjTree 105 % 1.32/1.49 107. ((op (e2) (e1)) = (e3)) ((op (e2) (e1)) != (e3)) ### Axiom % 1.32/1.49 108. (-. (((op (e0) (e1)) = (e3)) \/ (((op (e1) (e1)) = (e3)) \/ (((op (e2) (e1)) = (e3)) \/ (((op (e3) (e1)) = (e3)) \/ ((op (e4) (e1)) = (e3))))))) ((op (e2) (e1)) = (e3)) ### ConjTree 107 % 1.32/1.49 109. ((op (e1) (e1)) = (e4)) ((op (e1) (e1)) != (e4)) ### Axiom % 1.32/1.49 110. (-. (((op (e1) (e0)) = (e4)) \/ (((op (e1) (e1)) = (e4)) \/ (((op (e1) (e2)) = (e4)) \/ (((op (e1) (e3)) = (e4)) \/ ((op (e1) (e4)) = (e4))))))) ((op (e1) (e1)) = (e4)) ### ConjTree 109 % 1.32/1.49 111. ((op (e1) (e1)) = (e4)) ((op (e1) (e1)) != (e4)) ### Axiom % 1.32/1.49 112. (-. (((op (e0) (e1)) = (e4)) \/ (((op (e1) (e1)) = (e4)) \/ (((op (e2) (e1)) = (e4)) \/ (((op (e3) (e1)) = (e4)) \/ ((op (e4) (e1)) = (e4))))))) ((op (e1) (e1)) = (e4)) ### ConjTree 111 % 1.32/1.49 113. ((op (e2) (e4)) = (e0)) ((op (e2) (e4)) != (e0)) ### Axiom % 1.32/1.49 114. (-. (((op (e2) (e0)) = (e0)) \/ (((op (e2) (e1)) = (e0)) \/ (((op (e2) (e2)) = (e0)) \/ (((op (e2) (e3)) = (e0)) \/ ((op (e2) (e4)) = (e0))))))) ((op (e2) (e4)) = (e0)) ### ConjTree 113 % 1.32/1.49 115. ((op (e0) (e2)) = (e0)) ((op (e0) (e2)) != (e0)) ### Axiom % 1.32/1.49 116. (-. (((op (e0) (e2)) = (e0)) \/ (((op (e1) (e2)) = (e0)) \/ (((op (e2) (e2)) = (e0)) \/ (((op (e3) (e2)) = (e0)) \/ ((op (e4) (e2)) = (e0))))))) ((op (e0) (e2)) = (e0)) ### ConjTree 115 % 1.32/1.49 117. ((op (e2) (e0)) = (e1)) ((op (e2) (e0)) != (e1)) ### Axiom % 1.32/1.49 118. (-. (((op (e2) (e0)) = (e1)) \/ (((op (e2) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e1)) \/ (((op (e2) (e3)) = (e1)) \/ ((op (e2) (e4)) = (e1))))))) ((op (e2) (e0)) = (e1)) ### ConjTree 117 % 1.32/1.49 119. ((op (e1) (e2)) = (e1)) ((op (e1) (e2)) != (e1)) ### Axiom % 1.32/1.49 120. (-. (((op (e0) (e2)) = (e1)) \/ (((op (e1) (e2)) = (e1)) \/ (((op (e2) (e2)) = (e1)) \/ (((op (e3) (e2)) = (e1)) \/ ((op (e4) (e2)) = (e1))))))) ((op (e1) (e2)) = (e1)) ### ConjTree 119 % 1.32/1.49 121. ((op (e2) (e2)) = (e2)) ((op (e2) (e2)) != (e2)) ### Axiom % 1.32/1.49 122. (-. (((op (e2) (e0)) = (e2)) \/ (((op (e2) (e1)) = (e2)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e2) (e3)) = (e2)) \/ ((op (e2) (e4)) = (e2))))))) ((op (e2) (e2)) = (e2)) ### ConjTree 121 % 1.32/1.49 123. ((op (e2) (e2)) = (e2)) ((op (e2) (e2)) != (e2)) ### Axiom % 1.32/1.49 124. (-. (((op (e0) (e2)) = (e2)) \/ (((op (e1) (e2)) = (e2)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e2)) = (e2)) \/ ((op (e4) (e2)) = (e2))))))) ((op (e2) (e2)) = (e2)) ### ConjTree 123 % 1.32/1.49 125. ((op (e2) (e1)) = (e3)) ((op (e2) (e1)) != (e3)) ### Axiom % 1.32/1.49 126. (-. (((op (e2) (e0)) = (e3)) \/ (((op (e2) (e1)) = (e3)) \/ (((op (e2) (e2)) = (e3)) \/ (((op (e2) (e3)) = (e3)) \/ ((op (e2) (e4)) = (e3))))))) ((op (e2) (e1)) = (e3)) ### ConjTree 125 % 1.32/1.49 127. ((op (e3) (e2)) = (e3)) ((op (e3) (e2)) != (e3)) ### Axiom % 1.32/1.49 128. (-. (((op (e0) (e2)) = (e3)) \/ (((op (e1) (e2)) = (e3)) \/ (((op (e2) (e2)) = (e3)) \/ (((op (e3) (e2)) = (e3)) \/ ((op (e4) (e2)) = (e3))))))) ((op (e3) (e2)) = (e3)) ### ConjTree 127 % 1.32/1.49 129. ((op (e2) (e3)) = (e4)) ((op (e2) (e3)) != (e4)) ### Axiom % 1.32/1.49 130. (-. (((op (e2) (e0)) = (e4)) \/ (((op (e2) (e1)) = (e4)) \/ (((op (e2) (e2)) = (e4)) \/ (((op (e2) (e3)) = (e4)) \/ ((op (e2) (e4)) = (e4))))))) ((op (e2) (e3)) = (e4)) ### ConjTree 129 % 1.32/1.49 131. ((op (e4) (e2)) = (e4)) ((op (e4) (e2)) != (e4)) ### Axiom % 1.32/1.49 132. (-. (((op (e0) (e2)) = (e4)) \/ (((op (e1) (e2)) = (e4)) \/ (((op (e2) (e2)) = (e4)) \/ (((op (e3) (e2)) = (e4)) \/ ((op (e4) (e2)) = (e4))))))) ((op (e4) (e2)) = (e4)) ### ConjTree 131 % 1.32/1.49 133. ((op (e3) (e3)) = (e0)) ((op (e3) (e3)) != (e0)) ### Axiom % 1.32/1.49 134. (-. (((op (e3) (e0)) = (e0)) \/ (((op (e3) (e1)) = (e0)) \/ (((op (e3) (e2)) = (e0)) \/ (((op (e3) (e3)) = (e0)) \/ ((op (e3) (e4)) = (e0))))))) ((op (e3) (e3)) = (e0)) ### ConjTree 133 % 1.32/1.49 135. ((op (e3) (e3)) = (e0)) ((op (e3) (e3)) != (e0)) ### Axiom % 1.32/1.49 136. (-. (((op (e0) (e3)) = (e0)) \/ (((op (e1) (e3)) = (e0)) \/ (((op (e2) (e3)) = (e0)) \/ (((op (e3) (e3)) = (e0)) \/ ((op (e4) (e3)) = (e0))))))) ((op (e3) (e3)) = (e0)) ### ConjTree 135 % 1.32/1.49 137. ((op (e3) (e1)) = (e1)) ((op (e3) (e1)) != (e1)) ### Axiom % 1.32/1.49 138. (-. (((op (e3) (e0)) = (e1)) \/ (((op (e3) (e1)) = (e1)) \/ (((op (e3) (e2)) = (e1)) \/ (((op (e3) (e3)) = (e1)) \/ ((op (e3) (e4)) = (e1))))))) ((op (e3) (e1)) = (e1)) ### ConjTree 137 % 1.32/1.49 139. ((op (e0) (e3)) = (e1)) ((op (e0) (e3)) != (e1)) ### Axiom % 1.32/1.49 140. (-. (((op (e0) (e3)) = (e1)) \/ (((op (e1) (e3)) = (e1)) \/ (((op (e2) (e3)) = (e1)) \/ (((op (e3) (e3)) = (e1)) \/ ((op (e4) (e3)) = (e1))))))) ((op (e0) (e3)) = (e1)) ### ConjTree 139 % 1.32/1.49 141. ((op (e3) (e4)) = (e2)) ((op (e3) (e4)) != (e2)) ### Axiom % 1.32/1.49 142. (-. (((op (e3) (e0)) = (e2)) \/ (((op (e3) (e1)) = (e2)) \/ (((op (e3) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e2)) \/ ((op (e3) (e4)) = (e2))))))) ((op (e3) (e4)) = (e2)) ### ConjTree 141 % 1.32/1.49 143. ((op (e1) (e3)) = (e2)) ((op (e1) (e3)) != (e2)) ### Axiom % 1.32/1.49 144. (-. (((op (e0) (e3)) = (e2)) \/ (((op (e1) (e3)) = (e2)) \/ (((op (e2) (e3)) = (e2)) \/ (((op (e3) (e3)) = (e2)) \/ ((op (e4) (e3)) = (e2))))))) ((op (e1) (e3)) = (e2)) ### ConjTree 143 % 1.32/1.49 145. ((op (e3) (e2)) = (e3)) ((op (e3) (e2)) != (e3)) ### Axiom % 1.32/1.49 146. (-. (((op (e3) (e0)) = (e3)) \/ (((op (e3) (e1)) = (e3)) \/ (((op (e3) (e2)) = (e3)) \/ (((op (e3) (e3)) = (e3)) \/ ((op (e3) (e4)) = (e3))))))) ((op (e3) (e2)) = (e3)) ### ConjTree 145 % 1.32/1.49 147. ((op (e4) (e3)) = (e3)) ((op (e4) (e3)) != (e3)) ### Axiom % 1.32/1.49 148. (-. (((op (e0) (e3)) = (e3)) \/ (((op (e1) (e3)) = (e3)) \/ (((op (e2) (e3)) = (e3)) \/ (((op (e3) (e3)) = (e3)) \/ ((op (e4) (e3)) = (e3))))))) ((op (e4) (e3)) = (e3)) ### ConjTree 147 % 1.32/1.49 149. ((op (e3) (e0)) = (e4)) ((op (e3) (e0)) != (e4)) ### Axiom % 1.32/1.49 150. (-. (((op (e3) (e0)) = (e4)) \/ (((op (e3) (e1)) = (e4)) \/ (((op (e3) (e2)) = (e4)) \/ (((op (e3) (e3)) = (e4)) \/ ((op (e3) (e4)) = (e4))))))) ((op (e3) (e0)) = (e4)) ### ConjTree 149 % 1.32/1.49 151. ((op (e2) (e3)) = (e4)) ((op (e2) (e3)) != (e4)) ### Axiom % 1.32/1.49 152. (-. (((op (e0) (e3)) = (e4)) \/ (((op (e1) (e3)) = (e4)) \/ (((op (e2) (e3)) = (e4)) \/ (((op (e3) (e3)) = (e4)) \/ ((op (e4) (e3)) = (e4))))))) ((op (e2) (e3)) = (e4)) ### ConjTree 151 % 1.32/1.49 153. ((op (e4) (e1)) = (e0)) ((op (e4) (e1)) != (e0)) ### Axiom % 1.32/1.49 154. (-. (((op (e4) (e0)) = (e0)) \/ (((op (e4) (e1)) = (e0)) \/ (((op (e4) (e2)) = (e0)) \/ (((op (e4) (e3)) = (e0)) \/ ((op (e4) (e4)) = (e0))))))) ((op (e4) (e1)) = (e0)) ### ConjTree 153 % 1.32/1.49 155. ((op (e2) (e4)) = (e0)) ((op (e2) (e4)) != (e0)) ### Axiom % 1.32/1.49 156. (-. (((op (e0) (e4)) = (e0)) \/ (((op (e1) (e4)) = (e0)) \/ (((op (e2) (e4)) = (e0)) \/ (((op (e3) (e4)) = (e0)) \/ ((op (e4) (e4)) = (e0))))))) ((op (e2) (e4)) = (e0)) ### ConjTree 155 % 1.32/1.49 157. ((op (e4) (e4)) = (e1)) ((op (e4) (e4)) != (e1)) ### Axiom % 1.32/1.49 158. (-. (((op (e4) (e0)) = (e1)) \/ (((op (e4) (e1)) = (e1)) \/ (((op (e4) (e2)) = (e1)) \/ (((op (e4) (e3)) = (e1)) \/ ((op (e4) (e4)) = (e1))))))) ((op (e4) (e4)) = (e1)) ### ConjTree 157 % 1.32/1.49 159. ((op (e4) (e4)) = (e1)) ((op (e4) (e4)) != (e1)) ### Axiom % 1.32/1.49 160. (-. (((op (e0) (e4)) = (e1)) \/ (((op (e1) (e4)) = (e1)) \/ (((op (e2) (e4)) = (e1)) \/ (((op (e3) (e4)) = (e1)) \/ ((op (e4) (e4)) = (e1))))))) ((op (e4) (e4)) = (e1)) ### ConjTree 159 % 1.32/1.49 161. ((op (e4) (e0)) = (e2)) ((op (e4) (e0)) != (e2)) ### Axiom % 1.32/1.49 162. (-. (((op (e4) (e0)) = (e2)) \/ (((op (e4) (e1)) = (e2)) \/ (((op (e4) (e2)) = (e2)) \/ (((op (e4) (e3)) = (e2)) \/ ((op (e4) (e4)) = (e2))))))) ((op (e4) (e0)) = (e2)) ### ConjTree 161 % 1.32/1.49 163. ((op (e3) (e4)) = (e2)) ((op (e3) (e4)) != (e2)) ### Axiom % 1.32/1.49 164. (-. (((op (e0) (e4)) = (e2)) \/ (((op (e1) (e4)) = (e2)) \/ (((op (e2) (e4)) = (e2)) \/ (((op (e3) (e4)) = (e2)) \/ ((op (e4) (e4)) = (e2))))))) ((op (e3) (e4)) = (e2)) ### ConjTree 163 % 1.32/1.49 165. ((op (e4) (e3)) = (e3)) ((op (e4) (e3)) != (e3)) ### Axiom % 1.32/1.49 166. (-. (((op (e4) (e0)) = (e3)) \/ (((op (e4) (e1)) = (e3)) \/ (((op (e4) (e2)) = (e3)) \/ (((op (e4) (e3)) = (e3)) \/ ((op (e4) (e4)) = (e3))))))) ((op (e4) (e3)) = (e3)) ### ConjTree 165 % 1.32/1.49 167. ((op (e1) (e4)) = (e3)) ((op (e1) (e4)) != (e3)) ### Axiom % 1.32/1.49 168. (-. (((op (e0) (e4)) = (e3)) \/ (((op (e1) (e4)) = (e3)) \/ (((op (e2) (e4)) = (e3)) \/ (((op (e3) (e4)) = (e3)) \/ ((op (e4) (e4)) = (e3))))))) ((op (e1) (e4)) = (e3)) ### ConjTree 167 % 1.32/1.49 169. ((op (e4) (e2)) = (e4)) ((op (e4) (e2)) != (e4)) ### Axiom % 1.32/1.49 170. (-. (((op (e4) (e0)) = (e4)) \/ (((op (e4) (e1)) = (e4)) \/ (((op (e4) (e2)) = (e4)) \/ (((op (e4) (e3)) = (e4)) \/ ((op (e4) (e4)) = (e4))))))) ((op (e4) (e2)) = (e4)) ### ConjTree 169 % 1.32/1.49 171. ((op (e0) (e4)) = (e4)) ((op (e0) (e4)) != (e4)) ### Axiom % 1.32/1.49 172. (-. (((op (e0) (e4)) = (e4)) \/ (((op (e1) (e4)) = (e4)) \/ (((op (e2) (e4)) = (e4)) \/ (((op (e3) (e4)) = (e4)) \/ ((op (e4) (e4)) = (e4))))))) ((op (e0) (e4)) = (e4)) ### ConjTree 171 % 1.32/1.49 173. ((op (e0) (e0)) = (e3)) ((op (e0) (e0)) != (e3)) ### Axiom % 1.32/1.49 174. ((op (e0) (e0)) = (e3)) ((op (e0) (e0)) != (e3)) ### Axiom % 1.32/1.49 175. ((op (op (e0) (e0)) (op (e0) (e0))) != (op (e3) (e3))) ((op (e0) (e0)) = (e3)) ### NotEqual 173 174 % 1.32/1.49 176. ((op (op (e0) (e0)) (op (e0) (e0))) != (e0)) ((op (e3) (e3)) = (e0)) ((op (e0) (e0)) = (e3)) ### Trans 175 11 % 1.32/1.49 177. ((op (e1) (e0)) = (e0)) ((op (e1) (e0)) != (e0)) ### Axiom % 1.32/1.49 178. ((op (e0) (e1)) = (e2)) ((op (e0) (e1)) != (e2)) ### Axiom % 1.32/1.49 179. ((op (op (e1) (e0)) (op (e0) (e1))) != (op (e0) (e2))) ((op (e0) (e1)) = (e2)) ((op (e1) (e0)) = (e0)) ### NotEqual 177 178 % 1.32/1.49 180. ((op (op (e1) (e0)) (op (e0) (e1))) != (e0)) ((op (e0) (e2)) = (e0)) ((op (e1) (e0)) = (e0)) ((op (e0) (e1)) = (e2)) ### Trans 179 11 % 1.32/1.49 181. ((op (e2) (e0)) = (e1)) ((op (e2) (e0)) != (e1)) ### Axiom % 1.32/1.49 182. ((op (e0) (e2)) = (e0)) ((op (e0) (e2)) != (e0)) ### Axiom % 1.32/1.49 183. ((op (op (e2) (e0)) (op (e0) (e2))) != (op (e1) (e0))) ((op (e0) (e2)) = (e0)) ((op (e2) (e0)) = (e1)) ### NotEqual 181 182 % 1.32/1.49 184. ((op (op (e2) (e0)) (op (e0) (e2))) != (e0)) ((op (e1) (e0)) = (e0)) ((op (e2) (e0)) = (e1)) ((op (e0) (e2)) = (e0)) ### Trans 183 11 % 1.32/1.49 185. ((op (e3) (e0)) = (e4)) ((op (e3) (e0)) != (e4)) ### Axiom % 1.32/1.49 186. ((op (e0) (e3)) = (e1)) ((op (e0) (e3)) != (e1)) ### Axiom % 1.32/1.49 187. ((op (op (e3) (e0)) (op (e0) (e3))) != (op (e4) (e1))) ((op (e0) (e3)) = (e1)) ((op (e3) (e0)) = (e4)) ### NotEqual 185 186 % 1.32/1.49 188. ((op (op (e3) (e0)) (op (e0) (e3))) != (e0)) ((op (e4) (e1)) = (e0)) ((op (e3) (e0)) = (e4)) ((op (e0) (e3)) = (e1)) ### Trans 187 11 % 1.32/1.49 189. ((op (e4) (e0)) = (e2)) ((op (e4) (e0)) != (e2)) ### Axiom % 1.32/1.49 190. ((op (e0) (e4)) = (e4)) ((op (e0) (e4)) != (e4)) ### Axiom % 1.32/1.49 191. ((op (op (e4) (e0)) (op (e0) (e4))) != (op (e2) (e4))) ((op (e0) (e4)) = (e4)) ((op (e4) (e0)) = (e2)) ### NotEqual 189 190 % 1.32/1.49 192. ((op (op (e4) (e0)) (op (e0) (e4))) != (e0)) ((op (e2) (e4)) = (e0)) ((op (e4) (e0)) = (e2)) ((op (e0) (e4)) = (e4)) ### Trans 191 11 % 1.32/1.49 193. ((op (e0) (e1)) = (e2)) ((op (e0) (e1)) != (e2)) ### Axiom % 1.32/1.49 194. ((op (e1) (e0)) = (e0)) ((op (e1) (e0)) != (e0)) ### Axiom % 1.32/1.49 195. ((op (op (e0) (e1)) (op (e1) (e0))) != (op (e2) (e0))) ((op (e1) (e0)) = (e0)) ((op (e0) (e1)) = (e2)) ### NotEqual 193 194 % 1.32/1.49 196. ((op (op (e0) (e1)) (op (e1) (e0))) != (e1)) ((op (e2) (e0)) = (e1)) ((op (e0) (e1)) = (e2)) ((op (e1) (e0)) = (e0)) ### Trans 195 19 % 1.32/1.49 197. ((op (e1) (e1)) = (e4)) ((op (e1) (e1)) != (e4)) ### Axiom % 1.32/1.49 198. ((op (e1) (e1)) = (e4)) ((op (e1) (e1)) != (e4)) ### Axiom % 1.32/1.49 199. ((op (op (e1) (e1)) (op (e1) (e1))) != (op (e4) (e4))) ((op (e1) (e1)) = (e4)) ### NotEqual 197 198 % 1.32/1.49 200. ((op (op (e1) (e1)) (op (e1) (e1))) != (e1)) ((op (e4) (e4)) = (e1)) ((op (e1) (e1)) = (e4)) ### Trans 199 19 % 1.32/1.49 201. ((op (e2) (e1)) = (e3)) ((op (e2) (e1)) != (e3)) ### Axiom % 1.32/1.49 202. ((op (e1) (e2)) = (e1)) ((op (e1) (e2)) != (e1)) ### Axiom % 1.32/1.49 203. ((op (op (e2) (e1)) (op (e1) (e2))) != (op (e3) (e1))) ((op (e1) (e2)) = (e1)) ((op (e2) (e1)) = (e3)) ### NotEqual 201 202 % 1.32/1.49 204. ((op (op (e2) (e1)) (op (e1) (e2))) != (e1)) ((op (e3) (e1)) = (e1)) ((op (e2) (e1)) = (e3)) ((op (e1) (e2)) = (e1)) ### Trans 203 19 % 1.32/1.49 205. ((op (e3) (e1)) = (e1)) ((op (e3) (e1)) != (e1)) ### Axiom % 1.32/1.49 206. ((op (e1) (e3)) = (e2)) ((op (e1) (e3)) != (e2)) ### Axiom % 1.32/1.49 207. ((op (op (e3) (e1)) (op (e1) (e3))) != (op (e1) (e2))) ((op (e1) (e3)) = (e2)) ((op (e3) (e1)) = (e1)) ### NotEqual 205 206 % 1.32/1.49 208. ((op (op (e3) (e1)) (op (e1) (e3))) != (e1)) ((op (e1) (e2)) = (e1)) ((op (e3) (e1)) = (e1)) ((op (e1) (e3)) = (e2)) ### Trans 207 19 % 1.32/1.49 209. ((op (e4) (e1)) = (e0)) ((op (e4) (e1)) != (e0)) ### Axiom % 1.32/1.49 210. ((op (e1) (e4)) = (e3)) ((op (e1) (e4)) != (e3)) ### Axiom % 1.32/1.49 211. ((op (op (e4) (e1)) (op (e1) (e4))) != (op (e0) (e3))) ((op (e1) (e4)) = (e3)) ((op (e4) (e1)) = (e0)) ### NotEqual 209 210 % 1.32/1.49 212. ((op (op (e4) (e1)) (op (e1) (e4))) != (e1)) ((op (e0) (e3)) = (e1)) ((op (e4) (e1)) = (e0)) ((op (e1) (e4)) = (e3)) ### Trans 211 19 % 1.32/1.49 213. ((op (e0) (e2)) = (e0)) ((op (e0) (e2)) != (e0)) ### Axiom % 1.32/1.49 214. ((op (e2) (e0)) = (e1)) ((op (e2) (e0)) != (e1)) ### Axiom % 1.32/1.49 215. ((op (op (e0) (e2)) (op (e2) (e0))) != (op (e0) (e1))) ((op (e2) (e0)) = (e1)) ((op (e0) (e2)) = (e0)) ### NotEqual 213 214 % 1.32/1.49 216. ((op (op (e0) (e2)) (op (e2) (e0))) != (e2)) ((op (e0) (e1)) = (e2)) ((op (e0) (e2)) = (e0)) ((op (e2) (e0)) = (e1)) ### Trans 215 15 % 1.32/1.49 217. ((op (e1) (e2)) = (e1)) ((op (e1) (e2)) != (e1)) ### Axiom % 1.32/1.49 218. ((op (e2) (e1)) = (e3)) ((op (e2) (e1)) != (e3)) ### Axiom % 1.32/1.49 219. ((op (op (e1) (e2)) (op (e2) (e1))) != (op (e1) (e3))) ((op (e2) (e1)) = (e3)) ((op (e1) (e2)) = (e1)) ### NotEqual 217 218 % 1.32/1.49 220. ((op (op (e1) (e2)) (op (e2) (e1))) != (e2)) ((op (e1) (e3)) = (e2)) ((op (e1) (e2)) = (e1)) ((op (e2) (e1)) = (e3)) ### Trans 219 15 % 1.32/1.49 221. ((op (e2) (e2)) = (e2)) ((op (e2) (e2)) != (e2)) ### Axiom % 1.32/1.49 222. ((op (e2) (e2)) = (e2)) ((op (e2) (e2)) != (e2)) ### Axiom % 1.32/1.49 223. ((op (op (e2) (e2)) (op (e2) (e2))) != (op (e2) (e2))) ((op (e2) (e2)) = (e2)) ### NotEqual 221 222 % 1.32/1.49 224. ((op (op (e2) (e2)) (op (e2) (e2))) != (e2)) ((op (e2) (e2)) = (e2)) ### Trans 223 15 % 1.32/1.49 225. ((op (e3) (e2)) = (e3)) ((op (e3) (e2)) != (e3)) ### Axiom % 1.32/1.49 226. ((op (e2) (e3)) = (e4)) ((op (e2) (e3)) != (e4)) ### Axiom % 1.32/1.49 227. ((op (op (e3) (e2)) (op (e2) (e3))) != (op (e3) (e4))) ((op (e2) (e3)) = (e4)) ((op (e3) (e2)) = (e3)) ### NotEqual 225 226 % 1.32/1.49 228. ((op (op (e3) (e2)) (op (e2) (e3))) != (e2)) ((op (e3) (e4)) = (e2)) ((op (e3) (e2)) = (e3)) ((op (e2) (e3)) = (e4)) ### Trans 227 15 % 1.32/1.49 229. ((op (e4) (e2)) = (e4)) ((op (e4) (e2)) != (e4)) ### Axiom % 1.32/1.49 230. ((op (e2) (e4)) = (e0)) ((op (e2) (e4)) != (e0)) ### Axiom % 1.32/1.49 231. ((op (op (e4) (e2)) (op (e2) (e4))) != (op (e4) (e0))) ((op (e2) (e4)) = (e0)) ((op (e4) (e2)) = (e4)) ### NotEqual 229 230 % 1.32/1.49 232. ((op (op (e4) (e2)) (op (e2) (e4))) != (e2)) ((op (e4) (e0)) = (e2)) ((op (e4) (e2)) = (e4)) ((op (e2) (e4)) = (e0)) ### Trans 231 15 % 1.32/1.49 233. ((op (e0) (e3)) = (e1)) ((op (e0) (e3)) != (e1)) ### Axiom % 1.32/1.49 234. ((op (e3) (e0)) = (e4)) ((op (e3) (e0)) != (e4)) ### Axiom % 1.32/1.49 235. ((op (op (e0) (e3)) (op (e3) (e0))) != (op (e1) (e4))) ((op (e3) (e0)) = (e4)) ((op (e0) (e3)) = (e1)) ### NotEqual 233 234 % 1.32/1.49 236. ((op (op (e0) (e3)) (op (e3) (e0))) != (e3)) ((op (e1) (e4)) = (e3)) ((op (e0) (e3)) = (e1)) ((op (e3) (e0)) = (e4)) ### Trans 235 7 % 1.32/1.49 237. ((op (e1) (e3)) = (e2)) ((op (e1) (e3)) != (e2)) ### Axiom % 1.32/1.49 238. ((op (e3) (e1)) = (e1)) ((op (e3) (e1)) != (e1)) ### Axiom % 1.32/1.49 239. ((op (op (e1) (e3)) (op (e3) (e1))) != (op (e2) (e1))) ((op (e3) (e1)) = (e1)) ((op (e1) (e3)) = (e2)) ### NotEqual 237 238 % 1.32/1.49 240. ((op (op (e1) (e3)) (op (e3) (e1))) != (e3)) ((op (e2) (e1)) = (e3)) ((op (e1) (e3)) = (e2)) ((op (e3) (e1)) = (e1)) ### Trans 239 7 % 1.32/1.49 241. ((op (e2) (e3)) = (e4)) ((op (e2) (e3)) != (e4)) ### Axiom % 1.32/1.49 242. ((op (e3) (e2)) = (e3)) ((op (e3) (e2)) != (e3)) ### Axiom % 1.32/1.49 243. ((op (op (e2) (e3)) (op (e3) (e2))) != (op (e4) (e3))) ((op (e3) (e2)) = (e3)) ((op (e2) (e3)) = (e4)) ### NotEqual 241 242 % 1.32/1.49 244. ((op (op (e2) (e3)) (op (e3) (e2))) != (e3)) ((op (e4) (e3)) = (e3)) ((op (e2) (e3)) = (e4)) ((op (e3) (e2)) = (e3)) ### Trans 243 7 % 1.32/1.49 245. ((op (e3) (e3)) = (e0)) ((op (e3) (e3)) != (e0)) ### Axiom % 1.32/1.49 246. ((op (e3) (e3)) = (e0)) ((op (e3) (e3)) != (e0)) ### Axiom % 1.32/1.49 247. ((op (op (e3) (e3)) (op (e3) (e3))) != (op (e0) (e0))) ((op (e3) (e3)) = (e0)) ### NotEqual 245 246 % 1.32/1.49 248. ((op (op (e3) (e3)) (op (e3) (e3))) != (e3)) ((op (e0) (e0)) = (e3)) ((op (e3) (e3)) = (e0)) ### Trans 247 7 % 1.32/1.49 249. ((op (e4) (e3)) = (e3)) ((op (e4) (e3)) != (e3)) ### Axiom % 1.32/1.49 250. ((op (e3) (e4)) = (e2)) ((op (e3) (e4)) != (e2)) ### Axiom % 1.32/1.49 251. ((op (op (e4) (e3)) (op (e3) (e4))) != (op (e3) (e2))) ((op (e3) (e4)) = (e2)) ((op (e4) (e3)) = (e3)) ### NotEqual 249 250 % 1.32/1.49 252. ((op (op (e4) (e3)) (op (e3) (e4))) != (e3)) ((op (e3) (e2)) = (e3)) ((op (e4) (e3)) = (e3)) ((op (e3) (e4)) = (e2)) ### Trans 251 7 % 1.32/1.49 253. ((op (e0) (e4)) = (e4)) ((op (e0) (e4)) != (e4)) ### Axiom % 1.32/1.49 254. ((op (e4) (e0)) = (e2)) ((op (e4) (e0)) != (e2)) ### Axiom % 1.32/1.49 255. ((op (op (e0) (e4)) (op (e4) (e0))) != (op (e4) (e2))) ((op (e4) (e0)) = (e2)) ((op (e0) (e4)) = (e4)) ### NotEqual 253 254 % 1.32/1.49 256. ((op (op (e0) (e4)) (op (e4) (e0))) != (e4)) ((op (e4) (e2)) = (e4)) ((op (e0) (e4)) = (e4)) ((op (e4) (e0)) = (e2)) ### Trans 255 3 % 1.32/1.49 257. ((op (e1) (e4)) = (e3)) ((op (e1) (e4)) != (e3)) ### Axiom % 1.32/1.49 258. ((op (e4) (e1)) = (e0)) ((op (e4) (e1)) != (e0)) ### Axiom % 1.32/1.49 259. ((op (op (e1) (e4)) (op (e4) (e1))) != (op (e3) (e0))) ((op (e4) (e1)) = (e0)) ((op (e1) (e4)) = (e3)) ### NotEqual 257 258 % 1.32/1.49 260. ((op (op (e1) (e4)) (op (e4) (e1))) != (e4)) ((op (e3) (e0)) = (e4)) ((op (e1) (e4)) = (e3)) ((op (e4) (e1)) = (e0)) ### Trans 259 3 % 1.32/1.49 261. ((op (e2) (e4)) = (e0)) ((op (e2) (e4)) != (e0)) ### Axiom % 1.32/1.49 262. ((op (e4) (e2)) = (e4)) ((op (e4) (e2)) != (e4)) ### Axiom % 1.32/1.49 263. ((op (op (e2) (e4)) (op (e4) (e2))) != (op (e0) (e4))) ((op (e4) (e2)) = (e4)) ((op (e2) (e4)) = (e0)) ### NotEqual 261 262 % 1.32/1.49 264. ((op (op (e2) (e4)) (op (e4) (e2))) != (e4)) ((op (e0) (e4)) = (e4)) ((op (e2) (e4)) = (e0)) ((op (e4) (e2)) = (e4)) ### Trans 263 3 % 1.32/1.49 265. ((op (e3) (e4)) = (e2)) ((op (e3) (e4)) != (e2)) ### Axiom % 1.32/1.49 266. ((op (e4) (e3)) = (e3)) ((op (e4) (e3)) != (e3)) ### Axiom % 1.32/1.49 267. ((op (op (e3) (e4)) (op (e4) (e3))) != (op (e2) (e3))) ((op (e4) (e3)) = (e3)) ((op (e3) (e4)) = (e2)) ### NotEqual 265 266 % 1.32/1.49 268. ((op (op (e3) (e4)) (op (e4) (e3))) != (e4)) ((op (e2) (e3)) = (e4)) ((op (e3) (e4)) = (e2)) ((op (e4) (e3)) = (e3)) ### Trans 267 3 % 1.32/1.49 269. ((op (e4) (e4)) = (e1)) ((op (e4) (e4)) != (e1)) ### Axiom % 1.32/1.49 270. ((op (e4) (e4)) = (e1)) ((op (e4) (e4)) != (e1)) ### Axiom % 1.32/1.49 271. ((op (op (e4) (e4)) (op (e4) (e4))) != (op (e1) (e1))) ((op (e4) (e4)) = (e1)) ### NotEqual 269 270 % 1.32/1.49 272. ((op (op (e4) (e4)) (op (e4) (e4))) != (e4)) ((op (e1) (e1)) = (e4)) ((op (e4) (e4)) = (e1)) ### Trans 271 3 % 1.32/1.49 273. (-. (((((op (e0) (e0)) != (e0)) /\ (((op (e1) (e0)) != (e1)) /\ (((op (e2) (e0)) != (e2)) /\ (((op (e3) (e0)) != (e3)) /\ ((op (e4) (e0)) != (e4)))))) \/ ((((op (e0) (e1)) != (e0)) /\ (((op (e1) (e1)) != (e1)) /\ (((op (e2) (e1)) != (e2)) /\ (((op (e3) (e1)) != (e3)) /\ ((op (e4) (e1)) != (e4)))))) \/ ((((op (e0) (e2)) != (e0)) /\ (((op (e1) (e2)) != (e1)) /\ (((op (e2) (e2)) != (e2)) /\ (((op (e3) (e2)) != (e3)) /\ ((op (e4) (e2)) != (e4)))))) \/ ((((op (e0) (e3)) != (e0)) /\ (((op (e1) (e3)) != (e1)) /\ (((op (e2) (e3)) != (e2)) /\ (((op (e3) (e3)) != (e3)) /\ ((op (e4) (e3)) != (e4)))))) \/ (((op (e0) (e4)) != (e0)) /\ (((op (e1) (e4)) != (e1)) /\ (((op (e2) (e4)) != (e2)) /\ (((op (e3) (e4)) != (e3)) /\ ((op (e4) (e4)) != (e4)))))))))) /\ ((((op (e0) (e0)) = (e0)) \/ (((op (e0) (e0)) = (e1)) \/ (((op (e0) (e0)) = (e2)) \/ (((op (e0) (e0)) = (e3)) \/ ((op (e0) (e0)) = (e4)))))) /\ ((((op (e0) (e1)) = (e0)) \/ (((op (e0) (e1)) = (e1)) \/ (((op (e0) (e1)) = (e2)) \/ (((op (e0) (e1)) = (e3)) \/ ((op (e0) (e1)) = (e4)))))) /\ ((((op (e0) (e2)) = (e0)) \/ (((op (e0) (e2)) = (e1)) \/ (((op (e0) (e2)) = (e2)) \/ (((op (e0) (e2)) = (e3)) \/ ((op (e0) (e2)) = (e4)))))) /\ ((((op (e0) (e3)) = (e0)) \/ (((op (e0) (e3)) = (e1)) \/ (((op (e0) (e3)) = (e2)) \/ (((op (e0) (e3)) = (e3)) \/ ((op (e0) (e3)) = (e4)))))) /\ ((((op (e0) (e4)) = (e0)) \/ (((op (e0) (e4)) = (e1)) \/ (((op (e0) (e4)) = (e2)) \/ (((op (e0) (e4)) = (e3)) \/ ((op (e0) (e4)) = (e4)))))) /\ ((((op (e1) (e0)) = (e0)) \/ (((op (e1) (e0)) = (e1)) \/ (((op (e1) (e0)) = (e2)) \/ (((op (e1) (e0)) = (e3)) \/ ((op (e1) (e0)) = (e4)))))) /\ ((((op (e1) (e1)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e1) (e1)) = (e2)) \/ (((op (e1) (e1)) = (e3)) \/ ((op (e1) (e1)) = (e4)))))) /\ ((((op (e1) (e2)) = (e0)) \/ (((op (e1) (e2)) = (e1)) \/ (((op (e1) (e2)) = (e2)) \/ (((op (e1) (e2)) = (e3)) \/ ((op (e1) (e2)) = (e4)))))) /\ ((((op (e1) (e3)) = (e0)) \/ (((op (e1) (e3)) = (e1)) \/ (((op (e1) (e3)) = (e2)) \/ (((op (e1) (e3)) = (e3)) \/ ((op (e1) (e3)) = (e4)))))) /\ ((((op (e1) (e4)) = (e0)) \/ (((op (e1) (e4)) = (e1)) \/ (((op (e1) (e4)) = (e2)) \/ (((op (e1) (e4)) = (e3)) \/ ((op (e1) (e4)) = (e4)))))) /\ ((((op (e2) (e0)) = (e0)) \/ (((op (e2) (e0)) = (e1)) \/ (((op (e2) (e0)) = (e2)) \/ (((op (e2) (e0)) = (e3)) \/ ((op (e2) (e0)) = (e4)))))) /\ ((((op (e2) (e1)) = (e0)) \/ (((op (e2) (e1)) = (e1)) \/ (((op (e2) (e1)) = (e2)) \/ (((op (e2) (e1)) = (e3)) \/ ((op (e2) (e1)) = (e4)))))) /\ ((((op (e2) (e2)) = (e0)) \/ (((op (e2) (e2)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e2) (e2)) = (e3)) \/ ((op (e2) (e2)) = (e4)))))) /\ ((((op (e2) (e3)) = (e0)) \/ (((op (e2) (e3)) = (e1)) \/ (((op (e2) (e3)) = (e2)) \/ (((op (e2) (e3)) = (e3)) \/ ((op (e2) (e3)) = (e4)))))) /\ ((((op (e2) (e4)) = (e0)) \/ (((op (e2) (e4)) = (e1)) \/ (((op (e2) (e4)) = (e2)) \/ (((op (e2) (e4)) = (e3)) \/ ((op (e2) (e4)) = (e4)))))) /\ ((((op (e3) (e0)) = (e0)) \/ (((op (e3) (e0)) = (e1)) \/ (((op (e3) (e0)) = (e2)) \/ (((op (e3) (e0)) = (e3)) \/ ((op (e3) (e0)) = (e4)))))) /\ ((((op (e3) (e1)) = (e0)) \/ (((op (e3) (e1)) = (e1)) \/ (((op (e3) (e1)) = (e2)) \/ (((op (e3) (e1)) = (e3)) \/ ((op (e3) (e1)) = (e4)))))) /\ ((((op (e3) (e2)) = (e0)) \/ (((op (e3) (e2)) = (e1)) \/ (((op (e3) (e2)) = (e2)) \/ (((op (e3) (e2)) = (e3)) \/ ((op (e3) (e2)) = (e4)))))) /\ ((((op (e3) (e3)) = (e0)) \/ (((op (e3) (e3)) = (e1)) \/ (((op (e3) (e3)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ ((op (e3) (e3)) = (e4)))))) /\ ((((op (e3) (e4)) = (e0)) \/ (((op (e3) (e4)) = (e1)) \/ (((op (e3) (e4)) = (e2)) \/ (((op (e3) (e4)) = (e3)) \/ ((op (e3) (e4)) = (e4)))))) /\ ((((op (e4) (e0)) = (e0)) \/ (((op (e4) (e0)) = (e1)) \/ (((op (e4) (e0)) = (e2)) \/ (((op (e4) (e0)) = (e3)) \/ ((op (e4) (e0)) = (e4)))))) /\ ((((op (e4) (e1)) = (e0)) \/ (((op (e4) (e1)) = (e1)) \/ (((op (e4) (e1)) = (e2)) \/ (((op (e4) (e1)) = (e3)) \/ ((op (e4) (e1)) = (e4)))))) /\ ((((op (e4) (e2)) = (e0)) \/ (((op (e4) (e2)) = (e1)) \/ (((op (e4) (e2)) = (e2)) \/ (((op (e4) (e2)) = (e3)) \/ ((op (e4) (e2)) = (e4)))))) /\ ((((op (e4) (e3)) = (e0)) \/ (((op (e4) (e3)) = (e1)) \/ (((op (e4) (e3)) = (e2)) \/ (((op (e4) (e3)) = (e3)) \/ ((op (e4) (e3)) = (e4)))))) /\ ((((op (e4) (e4)) = (e0)) \/ (((op (e4) (e4)) = (e1)) \/ (((op (e4) (e4)) = (e2)) \/ (((op (e4) (e4)) = (e3)) \/ ((op (e4) (e4)) = (e4)))))) /\ ((((op (e0) (e0)) = (e0)) \/ (((op (e0) (e1)) = (e0)) \/ (((op (e0) (e2)) = (e0)) \/ (((op (e0) (e3)) = (e0)) \/ ((op (e0) (e4)) = (e0)))))) /\ ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e0)) = (e0)) \/ (((op (e2) (e0)) = (e0)) \/ (((op (e3) (e0)) = (e0)) \/ ((op (e4) (e0)) = (e0)))))) /\ ((((op (e0) (e0)) = (e1)) \/ (((op (e0) (e1)) = (e1)) \/ (((op (e0) (e2)) = (e1)) \/ (((op (e0) (e3)) = (e1)) \/ ((op (e0) (e4)) = (e1)))))) /\ ((((op (e0) (e0)) = (e1)) \/ (((op (e1) (e0)) = (e1)) \/ (((op (e2) (e0)) = (e1)) \/ (((op (e3) (e0)) = (e1)) \/ ((op (e4) (e0)) = (e1)))))) /\ ((((op (e0) (e0)) = (e2)) \/ (((op (e0) (e1)) = (e2)) \/ (((op (e0) (e2)) = (e2)) \/ (((op (e0) (e3)) = (e2)) \/ ((op (e0) (e4)) = (e2)))))) /\ ((((op (e0) (e0)) = (e2)) \/ (((op (e1) (e0)) = (e2)) \/ (((op (e2) (e0)) = (e2)) \/ (((op (e3) (e0)) = (e2)) \/ ((op (e4) (e0)) = (e2)))))) /\ ((((op (e0) (e0)) = (e3)) \/ (((op (e0) (e1)) = (e3)) \/ (((op (e0) (e2)) = (e3)) \/ (((op (e0) (e3)) = (e3)) \/ ((op (e0) (e4)) = (e3)))))) /\ ((((op (e0) (e0)) = (e3)) \/ (((op (e1) (e0)) = (e3)) \/ (((op (e2) (e0)) = (e3)) \/ (((op (e3) (e0)) = (e3)) \/ ((op (e4) (e0)) = (e3)))))) /\ ((((op (e0) (e0)) = (e4)) \/ (((op (e0) (e1)) = (e4)) \/ (((op (e0) (e2)) = (e4)) \/ (((op (e0) (e3)) = (e4)) \/ ((op (e0) (e4)) = (e4)))))) /\ ((((op (e0) (e0)) = (e4)) \/ (((op (e1) (e0)) = (e4)) \/ (((op (e2) (e0)) = (e4)) \/ (((op (e3) (e0)) = (e4)) \/ ((op (e4) (e0)) = (e4)))))) /\ ((((op (e1) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e0)) \/ (((op (e1) (e2)) = (e0)) \/ (((op (e1) (e3)) = (e0)) \/ ((op (e1) (e4)) = (e0)))))) /\ ((((op (e0) (e1)) = (e0)) \/ (((op (e1) (e1)) = (e0)) \/ (((op (e2) (e1)) = (e0)) \/ (((op (e3) (e1)) = (e0)) \/ ((op (e4) (e1)) = (e0)))))) /\ ((((op (e1) (e0)) = (e1)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e1) (e2)) = (e1)) \/ (((op (e1) (e3)) = (e1)) \/ ((op (e1) (e4)) = (e1)))))) /\ ((((op (e0) (e1)) = (e1)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e1)) = (e1)) \/ (((op (e3) (e1)) = (e1)) \/ ((op (e4) (e1)) = (e1)))))) /\ ((((op (e1) (e0)) = (e2)) \/ (((op (e1) (e1)) = (e2)) \/ (((op (e1) (e2)) = (e2)) \/ (((op (e1) (e3)) = (e2)) \/ ((op (e1) (e4)) = (e2)))))) /\ ((((op (e0) (e1)) = (e2)) \/ (((op (e1) (e1)) = (e2)) \/ (((op (e2) (e1)) = (e2)) \/ (((op (e3) (e1)) = (e2)) \/ ((op (e4) (e1)) = (e2)))))) /\ ((((op (e1) (e0)) = (e3)) \/ (((op (e1) (e1)) = (e3)) \/ (((op (e1) (e2)) = (e3)) \/ (((op (e1) (e3)) = (e3)) \/ ((op (e1) (e4)) = (e3)))))) /\ ((((op (e0) (e1)) = (e3)) \/ (((op (e1) (e1)) = (e3)) \/ (((op (e2) (e1)) = (e3)) \/ (((op (e3) (e1)) = (e3)) \/ ((op (e4) (e1)) = (e3)))))) /\ ((((op (e1) (e0)) = (e4)) \/ (((op (e1) (e1)) = (e4)) \/ (((op (e1) (e2)) = (e4)) \/ (((op (e1) (e3)) = (e4)) \/ ((op (e1) (e4)) = (e4)))))) /\ ((((op (e0) (e1)) = (e4)) \/ (((op (e1) (e1)) = (e4)) \/ (((op (e2) (e1)) = (e4)) \/ (((op (e3) (e1)) = (e4)) \/ ((op (e4) (e1)) = (e4)))))) /\ ((((op (e2) (e0)) = (e0)) \/ (((op (e2) (e1)) = (e0)) \/ (((op (e2) (e2)) = (e0)) \/ (((op (e2) (e3)) = (e0)) \/ ((op (e2) (e4)) = (e0)))))) /\ ((((op (e0) (e2)) = (e0)) \/ (((op (e1) (e2)) = (e0)) \/ (((op (e2) (e2)) = (e0)) \/ (((op (e3) (e2)) = (e0)) \/ ((op (e4) (e2)) = (e0)))))) /\ ((((op (e2) (e0)) = (e1)) \/ (((op (e2) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e1)) \/ (((op (e2) (e3)) = (e1)) \/ ((op (e2) (e4)) = (e1)))))) /\ ((((op (e0) (e2)) = (e1)) \/ (((op (e1) (e2)) = (e1)) \/ (((op (e2) (e2)) = (e1)) \/ (((op (e3) (e2)) = (e1)) \/ ((op (e4) (e2)) = (e1)))))) /\ ((((op (e2) (e0)) = (e2)) \/ (((op (e2) (e1)) = (e2)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e2) (e3)) = (e2)) \/ ((op (e2) (e4)) = (e2)))))) /\ ((((op (e0) (e2)) = (e2)) \/ (((op (e1) (e2)) = (e2)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e2)) = (e2)) \/ ((op (e4) (e2)) = (e2)))))) /\ ((((op (e2) (e0)) = (e3)) \/ (((op (e2) (e1)) = (e3)) \/ (((op (e2) (e2)) = (e3)) \/ (((op (e2) (e3)) = (e3)) \/ ((op (e2) (e4)) = (e3)))))) /\ ((((op (e0) (e2)) = (e3)) \/ (((op (e1) (e2)) = (e3)) \/ (((op (e2) (e2)) = (e3)) \/ (((op (e3) (e2)) = (e3)) \/ ((op (e4) (e2)) = (e3)))))) /\ ((((op (e2) (e0)) = (e4)) \/ (((op (e2) (e1)) = (e4)) \/ (((op (e2) (e2)) = (e4)) \/ (((op (e2) (e3)) = (e4)) \/ ((op (e2) (e4)) = (e4)))))) /\ ((((op (e0) (e2)) = (e4)) \/ (((op (e1) (e2)) = (e4)) \/ (((op (e2) (e2)) = (e4)) \/ (((op (e3) (e2)) = (e4)) \/ ((op (e4) (e2)) = (e4)))))) /\ ((((op (e3) (e0)) = (e0)) \/ (((op (e3) (e1)) = (e0)) \/ (((op (e3) (e2)) = (e0)) \/ (((op (e3) (e3)) = (e0)) \/ ((op (e3) (e4)) = (e0)))))) /\ ((((op (e0) (e3)) = (e0)) \/ (((op (e1) (e3)) = (e0)) \/ (((op (e2) (e3)) = (e0)) \/ (((op (e3) (e3)) = (e0)) \/ ((op (e4) (e3)) = (e0)))))) /\ ((((op (e3) (e0)) = (e1)) \/ (((op (e3) (e1)) = (e1)) \/ (((op (e3) (e2)) = (e1)) \/ (((op (e3) (e3)) = (e1)) \/ ((op (e3) (e4)) = (e1)))))) /\ ((((op (e0) (e3)) = (e1)) \/ (((op (e1) (e3)) = (e1)) \/ (((op (e2) (e3)) = (e1)) \/ (((op (e3) (e3)) = (e1)) \/ ((op (e4) (e3)) = (e1)))))) /\ ((((op (e3) (e0)) = (e2)) \/ (((op (e3) (e1)) = (e2)) \/ (((op (e3) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e2)) \/ ((op (e3) (e4)) = (e2)))))) /\ ((((op (e0) (e3)) = (e2)) \/ (((op (e1) (e3)) = (e2)) \/ (((op (e2) (e3)) = (e2)) \/ (((op (e3) (e3)) = (e2)) \/ ((op (e4) (e3)) = (e2)))))) /\ ((((op (e3) (e0)) = (e3)) \/ (((op (e3) (e1)) = (e3)) \/ (((op (e3) (e2)) = (e3)) \/ (((op (e3) (e3)) = (e3)) \/ ((op (e3) (e4)) = (e3)))))) /\ ((((op (e0) (e3)) = (e3)) \/ (((op (e1) (e3)) = (e3)) \/ (((op (e2) (e3)) = (e3)) \/ (((op (e3) (e3)) = (e3)) \/ ((op (e4) (e3)) = (e3)))))) /\ ((((op (e3) (e0)) = (e4)) \/ (((op (e3) (e1)) = (e4)) \/ (((op (e3) (e2)) = (e4)) \/ (((op (e3) (e3)) = (e4)) \/ ((op (e3) (e4)) = (e4)))))) /\ ((((op (e0) (e3)) = (e4)) \/ (((op (e1) (e3)) = (e4)) \/ (((op (e2) (e3)) = (e4)) \/ (((op (e3) (e3)) = (e4)) \/ ((op (e4) (e3)) = (e4)))))) /\ ((((op (e4) (e0)) = (e0)) \/ (((op (e4) (e1)) = (e0)) \/ (((op (e4) (e2)) = (e0)) \/ (((op (e4) (e3)) = (e0)) \/ ((op (e4) (e4)) = (e0)))))) /\ ((((op (e0) (e4)) = (e0)) \/ (((op (e1) (e4)) = (e0)) \/ (((op (e2) (e4)) = (e0)) \/ (((op (e3) (e4)) = (e0)) \/ ((op (e4) (e4)) = (e0)))))) /\ ((((op (e4) (e0)) = (e1)) \/ (((op (e4) (e1)) = (e1)) \/ (((op (e4) (e2)) = (e1)) \/ (((op (e4) (e3)) = (e1)) \/ ((op (e4) (e4)) = (e1)))))) /\ ((((op (e0) (e4)) = (e1)) \/ (((op (e1) (e4)) = (e1)) \/ (((op (e2) (e4)) = (e1)) \/ (((op (e3) (e4)) = (e1)) \/ ((op (e4) (e4)) = (e1)))))) /\ ((((op (e4) (e0)) = (e2)) \/ (((op (e4) (e1)) = (e2)) \/ (((op (e4) (e2)) = (e2)) \/ (((op (e4) (e3)) = (e2)) \/ ((op (e4) (e4)) = (e2)))))) /\ ((((op (e0) (e4)) = (e2)) \/ (((op (e1) (e4)) = (e2)) \/ (((op (e2) (e4)) = (e2)) \/ (((op (e3) (e4)) = (e2)) \/ ((op (e4) (e4)) = (e2)))))) /\ ((((op (e4) (e0)) = (e3)) \/ (((op (e4) (e1)) = (e3)) \/ (((op (e4) (e2)) = (e3)) \/ (((op (e4) (e3)) = (e3)) \/ ((op (e4) (e4)) = (e3)))))) /\ ((((op (e0) (e4)) = (e3)) \/ (((op (e1) (e4)) = (e3)) \/ (((op (e2) (e4)) = (e3)) \/ (((op (e3) (e4)) = (e3)) \/ ((op (e4) (e4)) = (e3)))))) /\ ((((op (e4) (e0)) = (e4)) \/ (((op (e4) (e1)) = (e4)) \/ (((op (e4) (e2)) = (e4)) \/ (((op (e4) (e3)) = (e4)) \/ ((op (e4) (e4)) = (e4)))))) /\ ((((op (e0) (e4)) = (e4)) \/ (((op (e1) (e4)) = (e4)) \/ (((op (e2) (e4)) = (e4)) \/ (((op (e3) (e4)) = (e4)) \/ ((op (e4) (e4)) = (e4)))))) /\ (((op (op (e0) (e0)) (op (e0) (e0))) = (e0)) /\ (((op (op (e1) (e0)) (op (e0) (e1))) = (e0)) /\ (((op (op (e2) (e0)) (op (e0) (e2))) = (e0)) /\ (((op (op (e3) (e0)) (op (e0) (e3))) = (e0)) /\ (((op (op (e4) (e0)) (op (e0) (e4))) = (e0)) /\ (((op (op (e0) (e1)) (op (e1) (e0))) = (e1)) /\ (((op (op (e1) (e1)) (op (e1) (e1))) = (e1)) /\ (((op (op (e2) (e1)) (op (e1) (e2))) = (e1)) /\ (((op (op (e3) (e1)) (op (e1) (e3))) = (e1)) /\ (((op (op (e4) (e1)) (op (e1) (e4))) = (e1)) /\ (((op (op (e0) (e2)) (op (e2) (e0))) = (e2)) /\ (((op (op (e1) (e2)) (op (e2) (e1))) = (e2)) /\ (((op (op (e2) (e2)) (op (e2) (e2))) = (e2)) /\ (((op (op (e3) (e2)) (op (e2) (e3))) = (e2)) /\ (((op (op (e4) (e2)) (op (e2) (e4))) = (e2)) /\ (((op (op (e0) (e3)) (op (e3) (e0))) = (e3)) /\ (((op (op (e1) (e3)) (op (e3) (e1))) = (e3)) /\ (((op (op (e2) (e3)) (op (e3) (e2))) = (e3)) /\ (((op (op (e3) (e3)) (op (e3) (e3))) = (e3)) /\ (((op (op (e4) (e3)) (op (e3) (e4))) = (e3)) /\ (((op (op (e0) (e4)) (op (e4) (e0))) = (e4)) /\ (((op (op (e1) (e4)) (op (e4) (e1))) = (e4)) /\ (((op (op (e2) (e4)) (op (e4) (e2))) = (e4)) /\ (((op (op (e3) (e4)) (op (e4) (e3))) = (e4)) /\ ((op (op (e4) (e4)) (op (e4) (e4))) = (e4))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ((op (e4) (e3)) = (e3)) ((op (e4) (e2)) = (e4)) ((op (e4) (e1)) = (e0)) ((op (e4) (e0)) = (e2)) ((op (e3) (e3)) = (e0)) ((op (e3) (e2)) = (e3)) ((op (e3) (e1)) = (e1)) ((op (e3) (e0)) = (e4)) ((op (e2) (e3)) = (e4)) ((op (e2) (e2)) = (e2)) ((op (e2) (e1)) = (e3)) ((op (e2) (e0)) = (e1)) ((op (e1) (e3)) = (e2)) ((op (e1) (e2)) = (e1)) ((op (e1) (e1)) = (e4)) ((op (e1) (e0)) = (e0)) ((op (e0) (e3)) = (e1)) ((op (e0) (e2)) = (e0)) ((op (e0) (e1)) = (e2)) ((op (e0) (e0)) = (e3)) ((op (e4) (e4)) = (e1)) ((e1) != (e4)) ((op (e3) (e4)) = (e2)) ((e2) != (e3)) ((op (e2) (e4)) = (e0)) ((e0) != (e2)) ((op (e1) (e4)) = (e3)) ((e1) != (e3)) ((op (e0) (e4)) = (e4)) ((e0) != (e4)) ### DisjTree 22 24 26 28 30 32 34 36 38 40 42 44 46 48 50 52 54 56 58 60 62 64 66 68 70 72 74 76 78 80 82 84 86 88 90 92 94 96 98 100 102 104 106 108 110 112 114 116 118 120 122 124 126 128 130 132 134 136 138 140 142 144 146 148 150 152 154 156 158 160 162 164 166 168 170 172 176 180 184 188 192 196 200 204 208 212 216 220 224 228 232 236 240 244 248 252 256 260 264 268 272 % 1.32/1.49 274. (((op (e0) (e0)) = (e3)) /\ (((op (e0) (e1)) = (e2)) /\ (((op (e0) (e2)) = (e0)) /\ (((op (e0) (e3)) = (e1)) /\ (((op (e0) (e4)) = (e4)) /\ (((op (e1) (e0)) = (e0)) /\ (((op (e1) (e1)) = (e4)) /\ (((op (e1) (e2)) = (e1)) /\ (((op (e1) (e3)) = (e2)) /\ (((op (e1) (e4)) = (e3)) /\ (((op (e2) (e0)) = (e1)) /\ (((op (e2) (e1)) = (e3)) /\ (((op (e2) (e2)) = (e2)) /\ (((op (e2) (e3)) = (e4)) /\ (((op (e2) (e4)) = (e0)) /\ (((op (e3) (e0)) = (e4)) /\ (((op (e3) (e1)) = (e1)) /\ (((op (e3) (e2)) = (e3)) /\ (((op (e3) (e3)) = (e0)) /\ (((op (e3) (e4)) = (e2)) /\ (((op (e4) (e0)) = (e2)) /\ (((op (e4) (e1)) = (e0)) /\ (((op (e4) (e2)) = (e4)) /\ (((op (e4) (e3)) = (e3)) /\ ((op (e4) (e4)) = (e1)))))))))))))))))))))))))) ((e0) != (e4)) ((e1) != (e3)) ((e0) != (e2)) ((e2) != (e3)) ((e1) != (e4)) (-. (((((op (e0) (e0)) != (e0)) /\ (((op (e1) (e0)) != (e1)) /\ (((op (e2) (e0)) != (e2)) /\ (((op (e3) (e0)) != (e3)) /\ ((op (e4) (e0)) != (e4)))))) \/ ((((op (e0) (e1)) != (e0)) /\ (((op (e1) (e1)) != (e1)) /\ (((op (e2) (e1)) != (e2)) /\ (((op (e3) (e1)) != (e3)) /\ ((op (e4) (e1)) != (e4)))))) \/ ((((op (e0) (e2)) != (e0)) /\ (((op (e1) (e2)) != (e1)) /\ (((op (e2) (e2)) != (e2)) /\ (((op (e3) (e2)) != (e3)) /\ ((op (e4) (e2)) != (e4)))))) \/ ((((op (e0) (e3)) != (e0)) /\ (((op (e1) (e3)) != (e1)) /\ (((op (e2) (e3)) != (e2)) /\ (((op (e3) (e3)) != (e3)) /\ ((op (e4) (e3)) != (e4)))))) \/ (((op (e0) (e4)) != (e0)) /\ (((op (e1) (e4)) != (e1)) /\ (((op (e2) (e4)) != (e2)) /\ (((op (e3) (e4)) != (e3)) /\ ((op (e4) (e4)) != (e4)))))))))) /\ ((((op (e0) (e0)) = (e0)) \/ (((op (e0) (e0)) = (e1)) \/ (((op (e0) (e0)) = (e2)) \/ (((op (e0) (e0)) = (e3)) \/ ((op (e0) (e0)) = (e4)))))) /\ ((((op (e0) (e1)) = (e0)) \/ (((op (e0) (e1)) = (e1)) \/ (((op (e0) (e1)) = (e2)) \/ (((op (e0) (e1)) = (e3)) \/ ((op (e0) (e1)) = (e4)))))) /\ ((((op (e0) (e2)) = (e0)) \/ (((op (e0) (e2)) = (e1)) \/ (((op (e0) (e2)) = (e2)) \/ (((op (e0) (e2)) = (e3)) \/ ((op (e0) (e2)) = (e4)))))) /\ ((((op (e0) (e3)) = (e0)) \/ (((op (e0) (e3)) = (e1)) \/ (((op (e0) (e3)) = (e2)) \/ (((op (e0) (e3)) = (e3)) \/ ((op (e0) (e3)) = (e4)))))) /\ ((((op (e0) (e4)) = (e0)) \/ (((op (e0) (e4)) = (e1)) \/ (((op (e0) (e4)) = (e2)) \/ (((op (e0) (e4)) = (e3)) \/ ((op (e0) (e4)) = (e4)))))) /\ ((((op (e1) (e0)) = (e0)) \/ (((op (e1) (e0)) = (e1)) \/ (((op (e1) (e0)) = (e2)) \/ (((op (e1) (e0)) = (e3)) \/ ((op (e1) (e0)) = (e4)))))) /\ ((((op (e1) (e1)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e1) (e1)) = (e2)) \/ (((op (e1) (e1)) = (e3)) \/ ((op (e1) (e1)) = (e4)))))) /\ ((((op (e1) (e2)) = (e0)) \/ (((op (e1) (e2)) = (e1)) \/ (((op (e1) (e2)) = (e2)) \/ (((op (e1) (e2)) = (e3)) \/ ((op (e1) (e2)) = (e4)))))) /\ ((((op (e1) (e3)) = (e0)) \/ (((op (e1) (e3)) = (e1)) \/ (((op (e1) (e3)) = (e2)) \/ (((op (e1) (e3)) = (e3)) \/ ((op (e1) (e3)) = (e4)))))) /\ ((((op (e1) (e4)) = (e0)) \/ (((op (e1) (e4)) = (e1)) \/ (((op (e1) (e4)) = (e2)) \/ (((op (e1) (e4)) = (e3)) \/ ((op (e1) (e4)) = (e4)))))) /\ ((((op (e2) (e0)) = (e0)) \/ (((op (e2) (e0)) = (e1)) \/ (((op (e2) (e0)) = (e2)) \/ (((op (e2) (e0)) = (e3)) \/ ((op (e2) (e0)) = (e4)))))) /\ ((((op (e2) (e1)) = (e0)) \/ (((op (e2) (e1)) = (e1)) \/ (((op (e2) (e1)) = (e2)) \/ (((op (e2) (e1)) = (e3)) \/ ((op (e2) (e1)) = (e4)))))) /\ ((((op (e2) (e2)) = (e0)) \/ (((op (e2) (e2)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e2) (e2)) = (e3)) \/ ((op (e2) (e2)) = (e4)))))) /\ ((((op (e2) (e3)) = (e0)) \/ (((op (e2) (e3)) = (e1)) \/ (((op (e2) (e3)) = (e2)) \/ (((op (e2) (e3)) = (e3)) \/ ((op (e2) (e3)) = (e4)))))) /\ ((((op (e2) (e4)) = (e0)) \/ (((op (e2) (e4)) = (e1)) \/ (((op (e2) (e4)) = (e2)) \/ (((op (e2) (e4)) = (e3)) \/ ((op (e2) (e4)) = (e4)))))) /\ ((((op (e3) (e0)) = (e0)) \/ (((op (e3) (e0)) = (e1)) \/ (((op (e3) (e0)) = (e2)) \/ (((op (e3) (e0)) = (e3)) \/ ((op (e3) (e0)) = (e4)))))) /\ ((((op (e3) (e1)) = (e0)) \/ (((op (e3) (e1)) = (e1)) \/ (((op (e3) (e1)) = (e2)) \/ (((op (e3) (e1)) = (e3)) \/ ((op (e3) (e1)) = (e4)))))) /\ ((((op (e3) (e2)) = (e0)) \/ (((op (e3) (e2)) = (e1)) \/ (((op (e3) (e2)) = (e2)) \/ (((op (e3) (e2)) = (e3)) \/ ((op (e3) (e2)) = (e4)))))) /\ ((((op (e3) (e3)) = (e0)) \/ (((op (e3) (e3)) = (e1)) \/ (((op (e3) (e3)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ ((op (e3) (e3)) = (e4)))))) /\ ((((op (e3) (e4)) = (e0)) \/ (((op (e3) (e4)) = (e1)) \/ (((op (e3) (e4)) = (e2)) \/ (((op (e3) (e4)) = (e3)) \/ ((op (e3) (e4)) = (e4)))))) /\ ((((op (e4) (e0)) = (e0)) \/ (((op (e4) (e0)) = (e1)) \/ (((op (e4) (e0)) = (e2)) \/ (((op (e4) (e0)) = (e3)) \/ ((op (e4) (e0)) = (e4)))))) /\ ((((op (e4) (e1)) = (e0)) \/ (((op (e4) (e1)) = (e1)) \/ (((op (e4) (e1)) = (e2)) \/ (((op (e4) (e1)) = (e3)) \/ ((op (e4) (e1)) = (e4)))))) /\ ((((op (e4) (e2)) = (e0)) \/ (((op (e4) (e2)) = (e1)) \/ (((op (e4) (e2)) = (e2)) \/ (((op (e4) (e2)) = (e3)) \/ ((op (e4) (e2)) = (e4)))))) /\ ((((op (e4) (e3)) = (e0)) \/ (((op (e4) (e3)) = (e1)) \/ (((op (e4) (e3)) = (e2)) \/ (((op (e4) (e3)) = (e3)) \/ ((op (e4) (e3)) = (e4)))))) /\ ((((op (e4) (e4)) = (e0)) \/ (((op (e4) (e4)) = (e1)) \/ (((op (e4) (e4)) = (e2)) \/ (((op (e4) (e4)) = (e3)) \/ ((op (e4) (e4)) = (e4)))))) /\ ((((op (e0) (e0)) = (e0)) \/ (((op (e0) (e1)) = (e0)) \/ (((op (e0) (e2)) = (e0)) \/ (((op (e0) (e3)) = (e0)) \/ ((op (e0) (e4)) = (e0)))))) /\ ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e0)) = (e0)) \/ (((op (e2) (e0)) = (e0)) \/ (((op (e3) (e0)) = (e0)) \/ ((op (e4) (e0)) = (e0)))))) /\ ((((op (e0) (e0)) = (e1)) \/ (((op (e0) (e1)) = (e1)) \/ (((op (e0) (e2)) = (e1)) \/ (((op (e0) (e3)) = (e1)) \/ ((op (e0) (e4)) = (e1)))))) /\ ((((op (e0) (e0)) = (e1)) \/ (((op (e1) (e0)) = (e1)) \/ (((op (e2) (e0)) = (e1)) \/ (((op (e3) (e0)) = (e1)) \/ ((op (e4) (e0)) = (e1)))))) /\ ((((op (e0) (e0)) = (e2)) \/ (((op (e0) (e1)) = (e2)) \/ (((op (e0) (e2)) = (e2)) \/ (((op (e0) (e3)) = (e2)) \/ ((op (e0) (e4)) = (e2)))))) /\ ((((op (e0) (e0)) = (e2)) \/ (((op (e1) (e0)) = (e2)) \/ (((op (e2) (e0)) = (e2)) \/ (((op (e3) (e0)) = (e2)) \/ ((op (e4) (e0)) = (e2)))))) /\ ((((op (e0) (e0)) = (e3)) \/ (((op (e0) (e1)) = (e3)) \/ (((op (e0) (e2)) = (e3)) \/ (((op (e0) (e3)) = (e3)) \/ ((op (e0) (e4)) = (e3)))))) /\ ((((op (e0) (e0)) = (e3)) \/ (((op (e1) (e0)) = (e3)) \/ (((op (e2) (e0)) = (e3)) \/ (((op (e3) (e0)) = (e3)) \/ ((op (e4) (e0)) = (e3)))))) /\ ((((op (e0) (e0)) = (e4)) \/ (((op (e0) (e1)) = (e4)) \/ (((op (e0) (e2)) = (e4)) \/ (((op (e0) (e3)) = (e4)) \/ ((op (e0) (e4)) = (e4)))))) /\ ((((op (e0) (e0)) = (e4)) \/ (((op (e1) (e0)) = (e4)) \/ (((op (e2) (e0)) = (e4)) \/ (((op (e3) (e0)) = (e4)) \/ ((op (e4) (e0)) = (e4)))))) /\ ((((op (e1) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e0)) \/ (((op (e1) (e2)) = (e0)) \/ (((op (e1) (e3)) = (e0)) \/ ((op (e1) (e4)) = (e0)))))) /\ ((((op (e0) (e1)) = (e0)) \/ (((op (e1) (e1)) = (e0)) \/ (((op (e2) (e1)) = (e0)) \/ (((op (e3) (e1)) = (e0)) \/ ((op (e4) (e1)) = (e0)))))) /\ ((((op (e1) (e0)) = (e1)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e1) (e2)) = (e1)) \/ (((op (e1) (e3)) = (e1)) \/ ((op (e1) (e4)) = (e1)))))) /\ ((((op (e0) (e1)) = (e1)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e1)) = (e1)) \/ (((op (e3) (e1)) = (e1)) \/ ((op (e4) (e1)) = (e1)))))) /\ ((((op (e1) (e0)) = (e2)) \/ (((op (e1) (e1)) = (e2)) \/ (((op (e1) (e2)) = (e2)) \/ (((op (e1) (e3)) = (e2)) \/ ((op (e1) (e4)) = (e2)))))) /\ ((((op (e0) (e1)) = (e2)) \/ (((op (e1) (e1)) = (e2)) \/ (((op (e2) (e1)) = (e2)) \/ (((op (e3) (e1)) = (e2)) \/ ((op (e4) (e1)) = (e2)))))) /\ ((((op (e1) (e0)) = (e3)) \/ (((op (e1) (e1)) = (e3)) \/ (((op (e1) (e2)) = (e3)) \/ (((op (e1) (e3)) = (e3)) \/ ((op (e1) (e4)) = (e3)))))) /\ ((((op (e0) (e1)) = (e3)) \/ (((op (e1) (e1)) = (e3)) \/ (((op (e2) (e1)) = (e3)) \/ (((op (e3) (e1)) = (e3)) \/ ((op (e4) (e1)) = (e3)))))) /\ ((((op (e1) (e0)) = (e4)) \/ (((op (e1) (e1)) = (e4)) \/ (((op (e1) (e2)) = (e4)) \/ (((op (e1) (e3)) = (e4)) \/ ((op (e1) (e4)) = (e4)))))) /\ ((((op (e0) (e1)) = (e4)) \/ (((op (e1) (e1)) = (e4)) \/ (((op (e2) (e1)) = (e4)) \/ (((op (e3) (e1)) = (e4)) \/ ((op (e4) (e1)) = (e4)))))) /\ ((((op (e2) (e0)) = (e0)) \/ (((op (e2) (e1)) = (e0)) \/ (((op (e2) (e2)) = (e0)) \/ (((op (e2) (e3)) = (e0)) \/ ((op (e2) (e4)) = (e0)))))) /\ ((((op (e0) (e2)) = (e0)) \/ (((op (e1) (e2)) = (e0)) \/ (((op (e2) (e2)) = (e0)) \/ (((op (e3) (e2)) = (e0)) \/ ((op (e4) (e2)) = (e0)))))) /\ ((((op (e2) (e0)) = (e1)) \/ (((op (e2) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e1)) \/ (((op (e2) (e3)) = (e1)) \/ ((op (e2) (e4)) = (e1)))))) /\ ((((op (e0) (e2)) = (e1)) \/ (((op (e1) (e2)) = (e1)) \/ (((op (e2) (e2)) = (e1)) \/ (((op (e3) (e2)) = (e1)) \/ ((op (e4) (e2)) = (e1)))))) /\ ((((op (e2) (e0)) = (e2)) \/ (((op (e2) (e1)) = (e2)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e2) (e3)) = (e2)) \/ ((op (e2) (e4)) = (e2)))))) /\ ((((op (e0) (e2)) = (e2)) \/ (((op (e1) (e2)) = (e2)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e2)) = (e2)) \/ ((op (e4) (e2)) = (e2)))))) /\ ((((op (e2) (e0)) = (e3)) \/ (((op (e2) (e1)) = (e3)) \/ (((op (e2) (e2)) = (e3)) \/ (((op (e2) (e3)) = (e3)) \/ ((op (e2) (e4)) = (e3)))))) /\ ((((op (e0) (e2)) = (e3)) \/ (((op (e1) (e2)) = (e3)) \/ (((op (e2) (e2)) = (e3)) \/ (((op (e3) (e2)) = (e3)) \/ ((op (e4) (e2)) = (e3)))))) /\ ((((op (e2) (e0)) = (e4)) \/ (((op (e2) (e1)) = (e4)) \/ (((op (e2) (e2)) = (e4)) \/ (((op (e2) (e3)) = (e4)) \/ ((op (e2) (e4)) = (e4)))))) /\ ((((op (e0) (e2)) = (e4)) \/ (((op (e1) (e2)) = (e4)) \/ (((op (e2) (e2)) = (e4)) \/ (((op (e3) (e2)) = (e4)) \/ ((op (e4) (e2)) = (e4)))))) /\ ((((op (e3) (e0)) = (e0)) \/ (((op (e3) (e1)) = (e0)) \/ (((op (e3) (e2)) = (e0)) \/ (((op (e3) (e3)) = (e0)) \/ ((op (e3) (e4)) = (e0)))))) /\ ((((op (e0) (e3)) = (e0)) \/ (((op (e1) (e3)) = (e0)) \/ (((op (e2) (e3)) = (e0)) \/ (((op (e3) (e3)) = (e0)) \/ ((op (e4) (e3)) = (e0)))))) /\ ((((op (e3) (e0)) = (e1)) \/ (((op (e3) (e1)) = (e1)) \/ (((op (e3) (e2)) = (e1)) \/ (((op (e3) (e3)) = (e1)) \/ ((op (e3) (e4)) = (e1)))))) /\ ((((op (e0) (e3)) = (e1)) \/ (((op (e1) (e3)) = (e1)) \/ (((op (e2) (e3)) = (e1)) \/ (((op (e3) (e3)) = (e1)) \/ ((op (e4) (e3)) = (e1)))))) /\ ((((op (e3) (e0)) = (e2)) \/ (((op (e3) (e1)) = (e2)) \/ (((op (e3) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e2)) \/ ((op (e3) (e4)) = (e2)))))) /\ ((((op (e0) (e3)) = (e2)) \/ (((op (e1) (e3)) = (e2)) \/ (((op (e2) (e3)) = (e2)) \/ (((op (e3) (e3)) = (e2)) \/ ((op (e4) (e3)) = (e2)))))) /\ ((((op (e3) (e0)) = (e3)) \/ (((op (e3) (e1)) = (e3)) \/ (((op (e3) (e2)) = (e3)) \/ (((op (e3) (e3)) = (e3)) \/ ((op (e3) (e4)) = (e3)))))) /\ ((((op (e0) (e3)) = (e3)) \/ (((op (e1) (e3)) = (e3)) \/ (((op (e2) (e3)) = (e3)) \/ (((op (e3) (e3)) = (e3)) \/ ((op (e4) (e3)) = (e3)))))) /\ ((((op (e3) (e0)) = (e4)) \/ (((op (e3) (e1)) = (e4)) \/ (((op (e3) (e2)) = (e4)) \/ (((op (e3) (e3)) = (e4)) \/ ((op (e3) (e4)) = (e4)))))) /\ ((((op (e0) (e3)) = (e4)) \/ (((op (e1) (e3)) = (e4)) \/ (((op (e2) (e3)) = (e4)) \/ (((op (e3) (e3)) = (e4)) \/ ((op (e4) (e3)) = (e4)))))) /\ ((((op (e4) (e0)) = (e0)) \/ (((op (e4) (e1)) = (e0)) \/ (((op (e4) (e2)) = (e0)) \/ (((op (e4) (e3)) = (e0)) \/ ((op (e4) (e4)) = (e0)))))) /\ ((((op (e0) (e4)) = (e0)) \/ (((op (e1) (e4)) = (e0)) \/ (((op (e2) (e4)) = (e0)) \/ (((op (e3) (e4)) = (e0)) \/ ((op (e4) (e4)) = (e0)))))) /\ ((((op (e4) (e0)) = (e1)) \/ (((op (e4) (e1)) = (e1)) \/ (((op (e4) (e2)) = (e1)) \/ (((op (e4) (e3)) = (e1)) \/ ((op (e4) (e4)) = (e1)))))) /\ ((((op (e0) (e4)) = (e1)) \/ (((op (e1) (e4)) = (e1)) \/ (((op (e2) (e4)) = (e1)) \/ (((op (e3) (e4)) = (e1)) \/ ((op (e4) (e4)) = (e1)))))) /\ ((((op (e4) (e0)) = (e2)) \/ (((op (e4) (e1)) = (e2)) \/ (((op (e4) (e2)) = (e2)) \/ (((op (e4) (e3)) = (e2)) \/ ((op (e4) (e4)) = (e2)))))) /\ ((((op (e0) (e4)) = (e2)) \/ (((op (e1) (e4)) = (e2)) \/ (((op (e2) (e4)) = (e2)) \/ (((op (e3) (e4)) = (e2)) \/ ((op (e4) (e4)) = (e2)))))) /\ ((((op (e4) (e0)) = (e3)) \/ (((op (e4) (e1)) = (e3)) \/ (((op (e4) (e2)) = (e3)) \/ (((op (e4) (e3)) = (e3)) \/ ((op (e4) (e4)) = (e3)))))) /\ ((((op (e0) (e4)) = (e3)) \/ (((op (e1) (e4)) = (e3)) \/ (((op (e2) (e4)) = (e3)) \/ (((op (e3) (e4)) = (e3)) \/ ((op (e4) (e4)) = (e3)))))) /\ ((((op (e4) (e0)) = (e4)) \/ (((op (e4) (e1)) = (e4)) \/ (((op (e4) (e2)) = (e4)) \/ (((op (e4) (e3)) = (e4)) \/ ((op (e4) (e4)) = (e4)))))) /\ ((((op (e0) (e4)) = (e4)) \/ (((op (e1) (e4)) = (e4)) \/ (((op (e2) (e4)) = (e4)) \/ (((op (e3) (e4)) = (e4)) \/ ((op (e4) (e4)) = (e4)))))) /\ (((op (op (e0) (e0)) (op (e0) (e0))) = (e0)) /\ (((op (op (e1) (e0)) (op (e0) (e1))) = (e0)) /\ (((op (op (e2) (e0)) (op (e0) (e2))) = (e0)) /\ (((op (op (e3) (e0)) (op (e0) (e3))) = (e0)) /\ (((op (op (e4) (e0)) (op (e0) (e4))) = (e0)) /\ (((op (op (e0) (e1)) (op (e1) (e0))) = (e1)) /\ (((op (op (e1) (e1)) (op (e1) (e1))) = (e1)) /\ (((op (op (e2) (e1)) (op (e1) (e2))) = (e1)) /\ (((op (op (e3) (e1)) (op (e1) (e3))) = (e1)) /\ (((op (op (e4) (e1)) (op (e1) (e4))) = (e1)) /\ (((op (op (e0) (e2)) (op (e2) (e0))) = (e2)) /\ (((op (op (e1) (e2)) (op (e2) (e1))) = (e2)) /\ (((op (op (e2) (e2)) (op (e2) (e2))) = (e2)) /\ (((op (op (e3) (e2)) (op (e2) (e3))) = (e2)) /\ (((op (op (e4) (e2)) (op (e2) (e4))) = (e2)) /\ (((op (op (e0) (e3)) (op (e3) (e0))) = (e3)) /\ (((op (op (e1) (e3)) (op (e3) (e1))) = (e3)) /\ (((op (op (e2) (e3)) (op (e3) (e2))) = (e3)) /\ (((op (op (e3) (e3)) (op (e3) (e3))) = (e3)) /\ (((op (op (e4) (e3)) (op (e3) (e4))) = (e3)) /\ (((op (op (e0) (e4)) (op (e4) (e0))) = (e4)) /\ (((op (op (e1) (e4)) (op (e4) (e1))) = (e4)) /\ (((op (op (e2) (e4)) (op (e4) (e2))) = (e4)) /\ (((op (op (e3) (e4)) (op (e4) (e3))) = (e4)) /\ ((op (op (e4) (e4)) (op (e4) (e4))) = (e4))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ### ConjTree 273 % 1.32/1.49 275. (((e0) != (e1)) /\ (((e0) != (e2)) /\ (((e0) != (e3)) /\ (((e0) != (e4)) /\ (((e1) != (e2)) /\ (((e1) != (e3)) /\ (((e1) != (e4)) /\ (((e2) != (e3)) /\ (((e2) != (e4)) /\ ((e3) != (e4))))))))))) (-. (((((op (e0) (e0)) != (e0)) /\ (((op (e1) (e0)) != (e1)) /\ (((op (e2) (e0)) != (e2)) /\ (((op (e3) (e0)) != (e3)) /\ ((op (e4) (e0)) != (e4)))))) \/ ((((op (e0) (e1)) != (e0)) /\ (((op (e1) (e1)) != (e1)) /\ (((op (e2) (e1)) != (e2)) /\ (((op (e3) (e1)) != (e3)) /\ ((op (e4) (e1)) != (e4)))))) \/ ((((op (e0) (e2)) != (e0)) /\ (((op (e1) (e2)) != (e1)) /\ (((op (e2) (e2)) != (e2)) /\ (((op (e3) (e2)) != (e3)) /\ ((op (e4) (e2)) != (e4)))))) \/ ((((op (e0) (e3)) != (e0)) /\ (((op (e1) (e3)) != (e1)) /\ (((op (e2) (e3)) != (e2)) /\ (((op (e3) (e3)) != (e3)) /\ ((op (e4) (e3)) != (e4)))))) \/ (((op (e0) (e4)) != (e0)) /\ (((op (e1) (e4)) != (e1)) /\ (((op (e2) (e4)) != (e2)) /\ (((op (e3) (e4)) != (e3)) /\ ((op (e4) (e4)) != (e4)))))))))) /\ ((((op (e0) (e0)) = (e0)) \/ (((op (e0) (e0)) = (e1)) \/ (((op (e0) (e0)) = (e2)) \/ (((op (e0) (e0)) = (e3)) \/ ((op (e0) (e0)) = (e4)))))) /\ ((((op (e0) (e1)) = (e0)) \/ (((op (e0) (e1)) = (e1)) \/ (((op (e0) (e1)) = (e2)) \/ (((op (e0) (e1)) = (e3)) \/ ((op (e0) (e1)) = (e4)))))) /\ ((((op (e0) (e2)) = (e0)) \/ (((op (e0) (e2)) = (e1)) \/ (((op (e0) (e2)) = (e2)) \/ (((op (e0) (e2)) = (e3)) \/ ((op (e0) (e2)) = (e4)))))) /\ ((((op (e0) (e3)) = (e0)) \/ (((op (e0) (e3)) = (e1)) \/ (((op (e0) (e3)) = (e2)) \/ (((op (e0) (e3)) = (e3)) \/ ((op (e0) (e3)) = (e4)))))) /\ ((((op (e0) (e4)) = (e0)) \/ (((op (e0) (e4)) = (e1)) \/ (((op (e0) (e4)) = (e2)) \/ (((op (e0) (e4)) = (e3)) \/ ((op (e0) (e4)) = (e4)))))) /\ ((((op (e1) (e0)) = (e0)) \/ (((op (e1) (e0)) = (e1)) \/ (((op (e1) (e0)) = (e2)) \/ (((op (e1) (e0)) = (e3)) \/ ((op (e1) (e0)) = (e4)))))) /\ ((((op (e1) (e1)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e1) (e1)) = (e2)) \/ (((op (e1) (e1)) = (e3)) \/ ((op (e1) (e1)) = (e4)))))) /\ ((((op (e1) (e2)) = (e0)) \/ (((op (e1) (e2)) = (e1)) \/ (((op (e1) (e2)) = (e2)) \/ (((op (e1) (e2)) = (e3)) \/ ((op (e1) (e2)) = (e4)))))) /\ ((((op (e1) (e3)) = (e0)) \/ (((op (e1) (e3)) = (e1)) \/ (((op (e1) (e3)) = (e2)) \/ (((op (e1) (e3)) = (e3)) \/ ((op (e1) (e3)) = (e4)))))) /\ ((((op (e1) (e4)) = (e0)) \/ (((op (e1) (e4)) = (e1)) \/ (((op (e1) (e4)) = (e2)) \/ (((op (e1) (e4)) = (e3)) \/ ((op (e1) (e4)) = (e4)))))) /\ ((((op (e2) (e0)) = (e0)) \/ (((op (e2) (e0)) = (e1)) \/ (((op (e2) (e0)) = (e2)) \/ (((op (e2) (e0)) = (e3)) \/ ((op (e2) (e0)) = (e4)))))) /\ ((((op (e2) (e1)) = (e0)) \/ (((op (e2) (e1)) = (e1)) \/ (((op (e2) (e1)) = (e2)) \/ (((op (e2) (e1)) = (e3)) \/ ((op (e2) (e1)) = (e4)))))) /\ ((((op (e2) (e2)) = (e0)) \/ (((op (e2) (e2)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e2) (e2)) = (e3)) \/ ((op (e2) (e2)) = (e4)))))) /\ ((((op (e2) (e3)) = (e0)) \/ (((op (e2) (e3)) = (e1)) \/ (((op (e2) (e3)) = (e2)) \/ (((op (e2) (e3)) = (e3)) \/ ((op (e2) (e3)) = (e4)))))) /\ ((((op (e2) (e4)) = (e0)) \/ (((op (e2) (e4)) = (e1)) \/ (((op (e2) (e4)) = (e2)) \/ (((op (e2) (e4)) = (e3)) \/ ((op (e2) (e4)) = (e4)))))) /\ ((((op (e3) (e0)) = (e0)) \/ (((op (e3) (e0)) = (e1)) \/ (((op (e3) (e0)) = (e2)) \/ (((op (e3) (e0)) = (e3)) \/ ((op (e3) (e0)) = (e4)))))) /\ ((((op (e3) (e1)) = (e0)) \/ (((op (e3) (e1)) = (e1)) \/ (((op (e3) (e1)) = (e2)) \/ (((op (e3) (e1)) = (e3)) \/ ((op (e3) (e1)) = (e4)))))) /\ ((((op (e3) (e2)) = (e0)) \/ (((op (e3) (e2)) = (e1)) \/ (((op (e3) (e2)) = (e2)) \/ (((op (e3) (e2)) = (e3)) \/ ((op (e3) (e2)) = (e4)))))) /\ ((((op (e3) (e3)) = (e0)) \/ (((op (e3) (e3)) = (e1)) \/ (((op (e3) (e3)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ ((op (e3) (e3)) = (e4)))))) /\ ((((op (e3) (e4)) = (e0)) \/ (((op (e3) (e4)) = (e1)) \/ (((op (e3) (e4)) = (e2)) \/ (((op (e3) (e4)) = (e3)) \/ ((op (e3) (e4)) = (e4)))))) /\ ((((op (e4) (e0)) = (e0)) \/ (((op (e4) (e0)) = (e1)) \/ (((op (e4) (e0)) = (e2)) \/ (((op (e4) (e0)) = (e3)) \/ ((op (e4) (e0)) = (e4)))))) /\ ((((op (e4) (e1)) = (e0)) \/ (((op (e4) (e1)) = (e1)) \/ (((op (e4) (e1)) = (e2)) \/ (((op (e4) (e1)) = (e3)) \/ ((op (e4) (e1)) = (e4)))))) /\ ((((op (e4) (e2)) = (e0)) \/ (((op (e4) (e2)) = (e1)) \/ (((op (e4) (e2)) = (e2)) \/ (((op (e4) (e2)) = (e3)) \/ ((op (e4) (e2)) = (e4)))))) /\ ((((op (e4) (e3)) = (e0)) \/ (((op (e4) (e3)) = (e1)) \/ (((op (e4) (e3)) = (e2)) \/ (((op (e4) (e3)) = (e3)) \/ ((op (e4) (e3)) = (e4)))))) /\ ((((op (e4) (e4)) = (e0)) \/ (((op (e4) (e4)) = (e1)) \/ (((op (e4) (e4)) = (e2)) \/ (((op (e4) (e4)) = (e3)) \/ ((op (e4) (e4)) = (e4)))))) /\ ((((op (e0) (e0)) = (e0)) \/ (((op (e0) (e1)) = (e0)) \/ (((op (e0) (e2)) = (e0)) \/ (((op (e0) (e3)) = (e0)) \/ ((op (e0) (e4)) = (e0)))))) /\ ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e0)) = (e0)) \/ (((op (e2) (e0)) = (e0)) \/ (((op (e3) (e0)) = (e0)) \/ ((op (e4) (e0)) = (e0)))))) /\ ((((op (e0) (e0)) = (e1)) \/ (((op (e0) (e1)) = (e1)) \/ (((op (e0) (e2)) = (e1)) \/ (((op (e0) (e3)) = (e1)) \/ ((op (e0) (e4)) = (e1)))))) /\ ((((op (e0) (e0)) = (e1)) \/ (((op (e1) (e0)) = (e1)) \/ (((op (e2) (e0)) = (e1)) \/ (((op (e3) (e0)) = (e1)) \/ ((op (e4) (e0)) = (e1)))))) /\ ((((op (e0) (e0)) = (e2)) \/ (((op (e0) (e1)) = (e2)) \/ (((op (e0) (e2)) = (e2)) \/ (((op (e0) (e3)) = (e2)) \/ ((op (e0) (e4)) = (e2)))))) /\ ((((op (e0) (e0)) = (e2)) \/ (((op (e1) (e0)) = (e2)) \/ (((op (e2) (e0)) = (e2)) \/ (((op (e3) (e0)) = (e2)) \/ ((op (e4) (e0)) = (e2)))))) /\ ((((op (e0) (e0)) = (e3)) \/ (((op (e0) (e1)) = (e3)) \/ (((op (e0) (e2)) = (e3)) \/ (((op (e0) (e3)) = (e3)) \/ ((op (e0) (e4)) = (e3)))))) /\ ((((op (e0) (e0)) = (e3)) \/ (((op (e1) (e0)) = (e3)) \/ (((op (e2) (e0)) = (e3)) \/ (((op (e3) (e0)) = (e3)) \/ ((op (e4) (e0)) = (e3)))))) /\ ((((op (e0) (e0)) = (e4)) \/ (((op (e0) (e1)) = (e4)) \/ (((op (e0) (e2)) = (e4)) \/ (((op (e0) (e3)) = (e4)) \/ ((op (e0) (e4)) = (e4)))))) /\ ((((op (e0) (e0)) = (e4)) \/ (((op (e1) (e0)) = (e4)) \/ (((op (e2) (e0)) = (e4)) \/ (((op (e3) (e0)) = (e4)) \/ ((op (e4) (e0)) = (e4)))))) /\ ((((op (e1) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e0)) \/ (((op (e1) (e2)) = (e0)) \/ (((op (e1) (e3)) = (e0)) \/ ((op (e1) (e4)) = (e0)))))) /\ ((((op (e0) (e1)) = (e0)) \/ (((op (e1) (e1)) = (e0)) \/ (((op (e2) (e1)) = (e0)) \/ (((op (e3) (e1)) = (e0)) \/ ((op (e4) (e1)) = (e0)))))) /\ ((((op (e1) (e0)) = (e1)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e1) (e2)) = (e1)) \/ (((op (e1) (e3)) = (e1)) \/ ((op (e1) (e4)) = (e1)))))) /\ ((((op (e0) (e1)) = (e1)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e1)) = (e1)) \/ (((op (e3) (e1)) = (e1)) \/ ((op (e4) (e1)) = (e1)))))) /\ ((((op (e1) (e0)) = (e2)) \/ (((op (e1) (e1)) = (e2)) \/ (((op (e1) (e2)) = (e2)) \/ (((op (e1) (e3)) = (e2)) \/ ((op (e1) (e4)) = (e2)))))) /\ ((((op (e0) (e1)) = (e2)) \/ (((op (e1) (e1)) = (e2)) \/ (((op (e2) (e1)) = (e2)) \/ (((op (e3) (e1)) = (e2)) \/ ((op (e4) (e1)) = (e2)))))) /\ ((((op (e1) (e0)) = (e3)) \/ (((op (e1) (e1)) = (e3)) \/ (((op (e1) (e2)) = (e3)) \/ (((op (e1) (e3)) = (e3)) \/ ((op (e1) (e4)) = (e3)))))) /\ ((((op (e0) (e1)) = (e3)) \/ (((op (e1) (e1)) = (e3)) \/ (((op (e2) (e1)) = (e3)) \/ (((op (e3) (e1)) = (e3)) \/ ((op (e4) (e1)) = (e3)))))) /\ ((((op (e1) (e0)) = (e4)) \/ (((op (e1) (e1)) = (e4)) \/ (((op (e1) (e2)) = (e4)) \/ (((op (e1) (e3)) = (e4)) \/ ((op (e1) (e4)) = (e4)))))) /\ ((((op (e0) (e1)) = (e4)) \/ (((op (e1) (e1)) = (e4)) \/ (((op (e2) (e1)) = (e4)) \/ (((op (e3) (e1)) = (e4)) \/ ((op (e4) (e1)) = (e4)))))) /\ ((((op (e2) (e0)) = (e0)) \/ (((op (e2) (e1)) = (e0)) \/ (((op (e2) (e2)) = (e0)) \/ (((op (e2) (e3)) = (e0)) \/ ((op (e2) (e4)) = (e0)))))) /\ ((((op (e0) (e2)) = (e0)) \/ (((op (e1) (e2)) = (e0)) \/ (((op (e2) (e2)) = (e0)) \/ (((op (e3) (e2)) = (e0)) \/ ((op (e4) (e2)) = (e0)))))) /\ ((((op (e2) (e0)) = (e1)) \/ (((op (e2) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e1)) \/ (((op (e2) (e3)) = (e1)) \/ ((op (e2) (e4)) = (e1)))))) /\ ((((op (e0) (e2)) = (e1)) \/ (((op (e1) (e2)) = (e1)) \/ (((op (e2) (e2)) = (e1)) \/ (((op (e3) (e2)) = (e1)) \/ ((op (e4) (e2)) = (e1)))))) /\ ((((op (e2) (e0)) = (e2)) \/ (((op (e2) (e1)) = (e2)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e2) (e3)) = (e2)) \/ ((op (e2) (e4)) = (e2)))))) /\ ((((op (e0) (e2)) = (e2)) \/ (((op (e1) (e2)) = (e2)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e2)) = (e2)) \/ ((op (e4) (e2)) = (e2)))))) /\ ((((op (e2) (e0)) = (e3)) \/ (((op (e2) (e1)) = (e3)) \/ (((op (e2) (e2)) = (e3)) \/ (((op (e2) (e3)) = (e3)) \/ ((op (e2) (e4)) = (e3)))))) /\ ((((op (e0) (e2)) = (e3)) \/ (((op (e1) (e2)) = (e3)) \/ (((op (e2) (e2)) = (e3)) \/ (((op (e3) (e2)) = (e3)) \/ ((op (e4) (e2)) = (e3)))))) /\ ((((op (e2) (e0)) = (e4)) \/ (((op (e2) (e1)) = (e4)) \/ (((op (e2) (e2)) = (e4)) \/ (((op (e2) (e3)) = (e4)) \/ ((op (e2) (e4)) = (e4)))))) /\ ((((op (e0) (e2)) = (e4)) \/ (((op (e1) (e2)) = (e4)) \/ (((op (e2) (e2)) = (e4)) \/ (((op (e3) (e2)) = (e4)) \/ ((op (e4) (e2)) = (e4)))))) /\ ((((op (e3) (e0)) = (e0)) \/ (((op (e3) (e1)) = (e0)) \/ (((op (e3) (e2)) = (e0)) \/ (((op (e3) (e3)) = (e0)) \/ ((op (e3) (e4)) = (e0)))))) /\ ((((op (e0) (e3)) = (e0)) \/ (((op (e1) (e3)) = (e0)) \/ (((op (e2) (e3)) = (e0)) \/ (((op (e3) (e3)) = (e0)) \/ ((op (e4) (e3)) = (e0)))))) /\ ((((op (e3) (e0)) = (e1)) \/ (((op (e3) (e1)) = (e1)) \/ (((op (e3) (e2)) = (e1)) \/ (((op (e3) (e3)) = (e1)) \/ ((op (e3) (e4)) = (e1)))))) /\ ((((op (e0) (e3)) = (e1)) \/ (((op (e1) (e3)) = (e1)) \/ (((op (e2) (e3)) = (e1)) \/ (((op (e3) (e3)) = (e1)) \/ ((op (e4) (e3)) = (e1)))))) /\ ((((op (e3) (e0)) = (e2)) \/ (((op (e3) (e1)) = (e2)) \/ (((op (e3) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e2)) \/ ((op (e3) (e4)) = (e2)))))) /\ ((((op (e0) (e3)) = (e2)) \/ (((op (e1) (e3)) = (e2)) \/ (((op (e2) (e3)) = (e2)) \/ (((op (e3) (e3)) = (e2)) \/ ((op (e4) (e3)) = (e2)))))) /\ ((((op (e3) (e0)) = (e3)) \/ (((op (e3) (e1)) = (e3)) \/ (((op (e3) (e2)) = (e3)) \/ (((op (e3) (e3)) = (e3)) \/ ((op (e3) (e4)) = (e3)))))) /\ ((((op (e0) (e3)) = (e3)) \/ (((op (e1) (e3)) = (e3)) \/ (((op (e2) (e3)) = (e3)) \/ (((op (e3) (e3)) = (e3)) \/ ((op (e4) (e3)) = (e3)))))) /\ ((((op (e3) (e0)) = (e4)) \/ (((op (e3) (e1)) = (e4)) \/ (((op (e3) (e2)) = (e4)) \/ (((op (e3) (e3)) = (e4)) \/ ((op (e3) (e4)) = (e4)))))) /\ ((((op (e0) (e3)) = (e4)) \/ (((op (e1) (e3)) = (e4)) \/ (((op (e2) (e3)) = (e4)) \/ (((op (e3) (e3)) = (e4)) \/ ((op (e4) (e3)) = (e4)))))) /\ ((((op (e4) (e0)) = (e0)) \/ (((op (e4) (e1)) = (e0)) \/ (((op (e4) (e2)) = (e0)) \/ (((op (e4) (e3)) = (e0)) \/ ((op (e4) (e4)) = (e0)))))) /\ ((((op (e0) (e4)) = (e0)) \/ (((op (e1) (e4)) = (e0)) \/ (((op (e2) (e4)) = (e0)) \/ (((op (e3) (e4)) = (e0)) \/ ((op (e4) (e4)) = (e0)))))) /\ ((((op (e4) (e0)) = (e1)) \/ (((op (e4) (e1)) = (e1)) \/ (((op (e4) (e2)) = (e1)) \/ (((op (e4) (e3)) = (e1)) \/ ((op (e4) (e4)) = (e1)))))) /\ ((((op (e0) (e4)) = (e1)) \/ (((op (e1) (e4)) = (e1)) \/ (((op (e2) (e4)) = (e1)) \/ (((op (e3) (e4)) = (e1)) \/ ((op (e4) (e4)) = (e1)))))) /\ ((((op (e4) (e0)) = (e2)) \/ (((op (e4) (e1)) = (e2)) \/ (((op (e4) (e2)) = (e2)) \/ (((op (e4) (e3)) = (e2)) \/ ((op (e4) (e4)) = (e2)))))) /\ ((((op (e0) (e4)) = (e2)) \/ (((op (e1) (e4)) = (e2)) \/ (((op (e2) (e4)) = (e2)) \/ (((op (e3) (e4)) = (e2)) \/ ((op (e4) (e4)) = (e2)))))) /\ ((((op (e4) (e0)) = (e3)) \/ (((op (e4) (e1)) = (e3)) \/ (((op (e4) (e2)) = (e3)) \/ (((op (e4) (e3)) = (e3)) \/ ((op (e4) (e4)) = (e3)))))) /\ ((((op (e0) (e4)) = (e3)) \/ (((op (e1) (e4)) = (e3)) \/ (((op (e2) (e4)) = (e3)) \/ (((op (e3) (e4)) = (e3)) \/ ((op (e4) (e4)) = (e3)))))) /\ ((((op (e4) (e0)) = (e4)) \/ (((op (e4) (e1)) = (e4)) \/ (((op (e4) (e2)) = (e4)) \/ (((op (e4) (e3)) = (e4)) \/ ((op (e4) (e4)) = (e4)))))) /\ ((((op (e0) (e4)) = (e4)) \/ (((op (e1) (e4)) = (e4)) \/ (((op (e2) (e4)) = (e4)) \/ (((op (e3) (e4)) = (e4)) \/ ((op (e4) (e4)) = (e4)))))) /\ (((op (op (e0) (e0)) (op (e0) (e0))) = (e0)) /\ (((op (op (e1) (e0)) (op (e0) (e1))) = (e0)) /\ (((op (op (e2) (e0)) (op (e0) (e2))) = (e0)) /\ (((op (op (e3) (e0)) (op (e0) (e3))) = (e0)) /\ (((op (op (e4) (e0)) (op (e0) (e4))) = (e0)) /\ (((op (op (e0) (e1)) (op (e1) (e0))) = (e1)) /\ (((op (op (e1) (e1)) (op (e1) (e1))) = (e1)) /\ (((op (op (e2) (e1)) (op (e1) (e2))) = (e1)) /\ (((op (op (e3) (e1)) (op (e1) (e3))) = (e1)) /\ (((op (op (e4) (e1)) (op (e1) (e4))) = (e1)) /\ (((op (op (e0) (e2)) (op (e2) (e0))) = (e2)) /\ (((op (op (e1) (e2)) (op (e2) (e1))) = (e2)) /\ (((op (op (e2) (e2)) (op (e2) (e2))) = (e2)) /\ (((op (op (e3) (e2)) (op (e2) (e3))) = (e2)) /\ (((op (op (e4) (e2)) (op (e2) (e4))) = (e2)) /\ (((op (op (e0) (e3)) (op (e3) (e0))) = (e3)) /\ (((op (op (e1) (e3)) (op (e3) (e1))) = (e3)) /\ (((op (op (e2) (e3)) (op (e3) (e2))) = (e3)) /\ (((op (op (e3) (e3)) (op (e3) (e3))) = (e3)) /\ (((op (op (e4) (e3)) (op (e3) (e4))) = (e3)) /\ (((op (op (e0) (e4)) (op (e4) (e0))) = (e4)) /\ (((op (op (e1) (e4)) (op (e4) (e1))) = (e4)) /\ (((op (op (e2) (e4)) (op (e4) (e2))) = (e4)) /\ (((op (op (e3) (e4)) (op (e4) (e3))) = (e4)) /\ ((op (op (e4) (e4)) (op (e4) (e4))) = (e4))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (((op (e0) (e0)) = (e3)) /\ (((op (e0) (e1)) = (e2)) /\ (((op (e0) (e2)) = (e0)) /\ (((op (e0) (e3)) = (e1)) /\ (((op (e0) (e4)) = (e4)) /\ (((op (e1) (e0)) = (e0)) /\ (((op (e1) (e1)) = (e4)) /\ (((op (e1) (e2)) = (e1)) /\ (((op (e1) (e3)) = (e2)) /\ (((op (e1) (e4)) = (e3)) /\ (((op (e2) (e0)) = (e1)) /\ (((op (e2) (e1)) = (e3)) /\ (((op (e2) (e2)) = (e2)) /\ (((op (e2) (e3)) = (e4)) /\ (((op (e2) (e4)) = (e0)) /\ (((op (e3) (e0)) = (e4)) /\ (((op (e3) (e1)) = (e1)) /\ (((op (e3) (e2)) = (e3)) /\ (((op (e3) (e3)) = (e0)) /\ (((op (e3) (e4)) = (e2)) /\ (((op (e4) (e0)) = (e2)) /\ (((op (e4) (e1)) = (e0)) /\ (((op (e4) (e2)) = (e4)) /\ (((op (e4) (e3)) = (e3)) /\ ((op (e4) (e4)) = (e1)))))))))))))))))))))))))) ### ConjTree 274 % 1.32/1.49 % SZS output end Proof % 1.32/1.49 (* END-PROOF *) %------------------------------------------------------------------------------