%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : ALG022+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:04:48 EDT 2022 % Result : Theorem 1.82s 2.02s % Output : Proof 1.82s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : ALG022+1 : TPTP v8.1.0. Released v2.7.0. % 0.06/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.13/0.34 % Computer : n020.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Wed Jun 8 06:59:21 EDT 2022 % 0.13/0.34 % CPUTime : % 1.82/2.02 % SZS status Theorem % 1.82/2.02 (* PROOF-FOUND *) % 1.82/2.02 (* BEGIN-PROOF *) % 1.82/2.02 % SZS output start Proof % 1.82/2.02 1. ((op (e2) (e2)) = (e0)) ((e0) != (op (e2) (e2))) ### Sym(=) % 1.82/2.02 2. ((op (e2) (e2)) = (e0)) ((e0) != (op (e2) (e2))) ### Sym(=) % 1.82/2.02 3. ((e3) != (e3)) ### NotEqual % 1.82/2.02 4. ((e0) != (e3)) ((op (e2) (e2)) = (e3)) ((op (e2) (e2)) = (e0)) ### TransEq 1 2 3 % 1.82/2.02 5. (((op (e0) (e0)) = (e0)) /\ (((op (e1) (e1)) = (e0)) /\ (((op (e2) (e2)) = (e0)) /\ ((op (e3) (e3)) = (e0))))) ((op (e2) (e2)) = (e3)) ((e0) != (e3)) ### ConjTree 4 % 1.82/2.02 6. ((op (e3) (e3)) = (e1)) ((e1) != (op (e3) (e3))) ### Sym(=) % 1.82/2.02 7. ((op (e3) (e3)) = (e1)) ((e1) != (op (e3) (e3))) ### Sym(=) % 1.82/2.02 8. ((e0) != (e0)) ### NotEqual % 1.82/2.02 9. ((e0) != (e1)) ((op (e3) (e3)) = (e0)) ((op (e3) (e3)) = (e1)) ### TransEq-sym 6 7 8 % 1.82/2.02 10. (((op (e0) (e0)) = (e1)) /\ (((op (e1) (e1)) = (e1)) /\ (((op (e2) (e2)) = (e1)) /\ ((op (e3) (e3)) = (e1))))) ((op (e3) (e3)) = (e0)) ((e0) != (e1)) ### ConjTree 9 % 1.82/2.02 11. ((op (e3) (e3)) = (e2)) ((e2) != (op (e3) (e3))) ### Sym(=) % 1.82/2.02 12. ((op (e3) (e3)) = (e2)) ((e2) != (op (e3) (e3))) ### Sym(=) % 1.82/2.02 13. ((e0) != (e2)) ((op (e3) (e3)) = (e0)) ((op (e3) (e3)) = (e2)) ### TransEq-sym 11 12 8 % 1.82/2.02 14. (((op (e0) (e0)) = (e2)) /\ (((op (e1) (e1)) = (e2)) /\ (((op (e2) (e2)) = (e2)) /\ ((op (e3) (e3)) = (e2))))) ((op (e3) (e3)) = (e0)) ((e0) != (e2)) ### ConjTree 13 % 1.82/2.02 15. ((op (e3) (e3)) = (e3)) ((e3) != (op (e3) (e3))) ### Sym(=) % 1.82/2.02 16. ((op (e3) (e3)) = (e3)) ((e3) != (op (e3) (e3))) ### Sym(=) % 1.82/2.02 17. ((e0) != (e3)) ((op (e3) (e3)) = (e0)) ((op (e3) (e3)) = (e3)) ### TransEq-sym 15 16 8 % 1.82/2.02 18. (((op (e0) (e0)) = (e3)) /\ (((op (e1) (e1)) = (e3)) /\ (((op (e2) (e2)) = (e3)) /\ ((op (e3) (e3)) = (e3))))) ((op (e3) (e3)) = (e0)) ((e0) != (e3)) ### ConjTree 17 % 1.82/2.02 19. ((op (e0) (e0)) = (e0)) ((op (e0) (e0)) != (e0)) ### Axiom % 1.82/2.02 20. (-. (((op (e0) (e0)) = (e0)) \/ (((op (e0) (e0)) = (e1)) \/ (((op (e0) (e0)) = (e2)) \/ ((op (e0) (e0)) = (e3)))))) ((op (e0) (e0)) = (e0)) ### ConjTree 19 % 1.82/2.02 21. ((op (e0) (e1)) = (e1)) ((op (e0) (e1)) != (e1)) ### Axiom % 1.82/2.02 22. (-. (((op (e0) (e1)) = (e0)) \/ (((op (e0) (e1)) = (e1)) \/ (((op (e0) (e1)) = (e2)) \/ ((op (e0) (e1)) = (e3)))))) ((op (e0) (e1)) = (e1)) ### ConjTree 21 % 1.82/2.02 23. ((op (e0) (e2)) = (e2)) ((op (e0) (e2)) != (e2)) ### Axiom % 1.82/2.02 24. (-. (((op (e0) (e2)) = (e0)) \/ (((op (e0) (e2)) = (e1)) \/ (((op (e0) (e2)) = (e2)) \/ ((op (e0) (e2)) = (e3)))))) ((op (e0) (e2)) = (e2)) ### ConjTree 23 % 1.82/2.02 25. ((op (e0) (e3)) = (e3)) ((op (e0) (e3)) != (e3)) ### Axiom % 1.82/2.02 26. (-. (((op (e0) (e3)) = (e0)) \/ (((op (e0) (e3)) = (e1)) \/ (((op (e0) (e3)) = (e2)) \/ ((op (e0) (e3)) = (e3)))))) ((op (e0) (e3)) = (e3)) ### ConjTree 25 % 1.82/2.02 27. ((op (e1) (e0)) = (e1)) ((op (e1) (e0)) != (e1)) ### Axiom % 1.82/2.02 28. (-. (((op (e1) (e0)) = (e0)) \/ (((op (e1) (e0)) = (e1)) \/ (((op (e1) (e0)) = (e2)) \/ ((op (e1) (e0)) = (e3)))))) ((op (e1) (e0)) = (e1)) ### ConjTree 27 % 1.82/2.02 29. ((op (e1) (e1)) = (e3)) ((op (e1) (e1)) != (e3)) ### Axiom % 1.82/2.02 30. (-. (((op (e1) (e1)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e1) (e1)) = (e2)) \/ ((op (e1) (e1)) = (e3)))))) ((op (e1) (e1)) = (e3)) ### ConjTree 29 % 1.82/2.02 31. ((op (e1) (e2)) = (e0)) ((op (e1) (e2)) != (e0)) ### Axiom % 1.82/2.02 32. (-. (((op (e1) (e2)) = (e0)) \/ (((op (e1) (e2)) = (e1)) \/ (((op (e1) (e2)) = (e2)) \/ ((op (e1) (e2)) = (e3)))))) ((op (e1) (e2)) = (e0)) ### ConjTree 31 % 1.82/2.02 33. ((op (e1) (e3)) = (e2)) ((op (e1) (e3)) != (e2)) ### Axiom % 1.82/2.02 34. (-. (((op (e1) (e3)) = (e0)) \/ (((op (e1) (e3)) = (e1)) \/ (((op (e1) (e3)) = (e2)) \/ ((op (e1) (e3)) = (e3)))))) ((op (e1) (e3)) = (e2)) ### ConjTree 33 % 1.82/2.02 35. ((op (e2) (e0)) = (e2)) ((op (e2) (e0)) != (e2)) ### Axiom % 1.82/2.02 36. (-. (((op (e2) (e0)) = (e0)) \/ (((op (e2) (e0)) = (e1)) \/ (((op (e2) (e0)) = (e2)) \/ ((op (e2) (e0)) = (e3)))))) ((op (e2) (e0)) = (e2)) ### ConjTree 35 % 1.82/2.02 37. ((op (e2) (e1)) = (e0)) ((op (e2) (e1)) != (e0)) ### Axiom % 1.82/2.02 38. (-. (((op (e2) (e1)) = (e0)) \/ (((op (e2) (e1)) = (e1)) \/ (((op (e2) (e1)) = (e2)) \/ ((op (e2) (e1)) = (e3)))))) ((op (e2) (e1)) = (e0)) ### ConjTree 37 % 1.82/2.02 39. ((op (e2) (e2)) = (e3)) ((op (e2) (e2)) != (e3)) ### Axiom % 1.82/2.02 40. (-. (((op (e2) (e2)) = (e0)) \/ (((op (e2) (e2)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ ((op (e2) (e2)) = (e3)))))) ((op (e2) (e2)) = (e3)) ### ConjTree 39 % 1.82/2.02 41. ((op (e2) (e3)) = (e1)) ((op (e2) (e3)) != (e1)) ### Axiom % 1.82/2.02 42. (-. (((op (e2) (e3)) = (e0)) \/ (((op (e2) (e3)) = (e1)) \/ (((op (e2) (e3)) = (e2)) \/ ((op (e2) (e3)) = (e3)))))) ((op (e2) (e3)) = (e1)) ### ConjTree 41 % 1.82/2.02 43. ((op (e3) (e0)) = (e3)) ((op (e3) (e0)) != (e3)) ### Axiom % 1.82/2.02 44. (-. (((op (e3) (e0)) = (e0)) \/ (((op (e3) (e0)) = (e1)) \/ (((op (e3) (e0)) = (e2)) \/ ((op (e3) (e0)) = (e3)))))) ((op (e3) (e0)) = (e3)) ### ConjTree 43 % 1.82/2.02 45. ((op (e3) (e1)) = (e2)) ((op (e3) (e1)) != (e2)) ### Axiom % 1.82/2.02 46. (-. (((op (e3) (e1)) = (e0)) \/ (((op (e3) (e1)) = (e1)) \/ (((op (e3) (e1)) = (e2)) \/ ((op (e3) (e1)) = (e3)))))) ((op (e3) (e1)) = (e2)) ### ConjTree 45 % 1.82/2.02 47. ((op (e3) (e2)) = (e1)) ((op (e3) (e2)) != (e1)) ### Axiom % 1.82/2.02 48. (-. (((op (e3) (e2)) = (e0)) \/ (((op (e3) (e2)) = (e1)) \/ (((op (e3) (e2)) = (e2)) \/ ((op (e3) (e2)) = (e3)))))) ((op (e3) (e2)) = (e1)) ### ConjTree 47 % 1.82/2.02 49. ((op (e3) (e3)) = (e0)) ((op (e3) (e3)) != (e0)) ### Axiom % 1.82/2.02 50. (-. (((op (e3) (e3)) = (e0)) \/ (((op (e3) (e3)) = (e1)) \/ (((op (e3) (e3)) = (e2)) \/ ((op (e3) (e3)) = (e3)))))) ((op (e3) (e3)) = (e0)) ### ConjTree 49 % 1.82/2.02 51. ((op (e0) (e0)) = (e0)) ((op (e0) (e0)) != (e0)) ### Axiom % 1.82/2.02 52. ((op (e0) (e0)) = (e0)) ((e0) != (op (e0) (e0))) ### Sym(=) % 1.82/2.02 53. ((op (op (e0) (e0)) (e0)) != (op (e0) (op (e0) (e0)))) ((op (e0) (e0)) = (e0)) ### NotEqual 51 52 % 1.82/2.02 54. ((op (e0) (e0)) = (e0)) ((op (e0) (e0)) != (e0)) ### Axiom % 1.82/2.02 55. ((op (e0) (e1)) = (e1)) ((e1) != (op (e0) (e1))) ### Sym(=) % 1.82/2.02 56. ((op (op (e0) (e0)) (e1)) != (op (e0) (op (e0) (e1)))) ((op (e0) (e1)) = (e1)) ((op (e0) (e0)) = (e0)) ### NotEqual 54 55 % 1.82/2.02 57. ((op (e0) (e0)) = (e0)) ((op (e0) (e0)) != (e0)) ### Axiom % 1.82/2.02 58. ((op (e0) (e2)) = (e2)) ((e2) != (op (e0) (e2))) ### Sym(=) % 1.82/2.02 59. ((op (op (e0) (e0)) (e2)) != (op (e0) (op (e0) (e2)))) ((op (e0) (e2)) = (e2)) ((op (e0) (e0)) = (e0)) ### NotEqual 57 58 % 1.82/2.02 60. ((op (e0) (e0)) = (e0)) ((op (e0) (e0)) != (e0)) ### Axiom % 1.82/2.02 61. ((op (e0) (e3)) = (e3)) ((e3) != (op (e0) (e3))) ### Sym(=) % 1.82/2.02 62. ((op (op (e0) (e0)) (e3)) != (op (e0) (op (e0) (e3)))) ((op (e0) (e3)) = (e3)) ((op (e0) (e0)) = (e0)) ### NotEqual 60 61 % 1.82/2.02 63. ((op (e0) (e1)) = (e1)) ((op (e0) (e1)) != (e1)) ### Axiom % 1.82/2.02 64. ((op (op (e0) (e1)) (e0)) != (op (e1) (e0))) ((op (e0) (e1)) = (e1)) ### NotEqual 63 8 % 1.82/2.02 65. ((op (e1) (e0)) = (e1)) ((op (e1) (e0)) != (e1)) ### Axiom % 1.82/2.02 66. ((op (e0) (op (e1) (e0))) != (op (e0) (e1))) ((op (e1) (e0)) = (e1)) ### NotEqual 8 65 % 1.82/2.02 67. ((e1) != (e1)) ### NotEqual % 1.82/2.02 68. ((e1) != (op (e0) (op (e1) (e0)))) ((op (e0) (e1)) = (e1)) ((op (e1) (e0)) = (e1)) ### Trans-sym 66 67 % 1.82/2.02 69. ((op (op (e0) (e1)) (e0)) != (op (e0) (op (e1) (e0)))) ((op (e1) (e0)) = (e1)) ((op (e0) (e1)) = (e1)) ### Trans 64 68 % 1.82/2.02 70. ((op (e0) (e1)) = (e1)) ((op (e0) (e1)) != (e1)) ### Axiom % 1.82/2.02 71. ((op (op (e0) (e1)) (e1)) != (op (e1) (e1))) ((op (e0) (e1)) = (e1)) ### NotEqual 70 67 % 1.82/2.02 72. ((op (e1) (e1)) = (e3)) ((op (e1) (e1)) != (e3)) ### Axiom % 1.82/2.02 73. ((op (e0) (op (e1) (e1))) != (op (e0) (e3))) ((op (e1) (e1)) = (e3)) ### NotEqual 8 72 % 1.82/2.02 74. ((e3) != (op (e0) (op (e1) (e1)))) ((op (e0) (e3)) = (e3)) ((op (e1) (e1)) = (e3)) ### Trans-sym 73 3 % 1.82/2.02 75. ((op (op (e0) (e1)) (e1)) != (op (e0) (op (e1) (e1)))) ((op (e1) (e1)) = (e3)) ((op (e0) (e3)) = (e3)) ((op (e0) (e1)) = (e1)) ### Trans 71 74 % 1.82/2.02 76. ((op (e0) (e1)) = (e1)) ((op (e0) (e1)) != (e1)) ### Axiom % 1.82/2.02 77. ((e2) != (e2)) ### NotEqual % 1.82/2.02 78. ((op (op (e0) (e1)) (e2)) != (op (e1) (e2))) ((op (e0) (e1)) = (e1)) ### NotEqual 76 77 % 1.82/2.02 79. ((op (e1) (e2)) = (e0)) ((op (e1) (e2)) != (e0)) ### Axiom % 1.82/2.02 80. ((op (e0) (op (e1) (e2))) != (op (e0) (e0))) ((op (e1) (e2)) = (e0)) ### NotEqual 8 79 % 1.82/2.02 81. ((e0) != (op (e0) (op (e1) (e2)))) ((op (e0) (e0)) = (e0)) ((op (e1) (e2)) = (e0)) ### Trans-sym 80 8 % 1.82/2.02 82. ((op (op (e0) (e1)) (e2)) != (op (e0) (op (e1) (e2)))) ((op (e1) (e2)) = (e0)) ((op (e0) (e0)) = (e0)) ((op (e0) (e1)) = (e1)) ### Trans 78 81 % 1.82/2.02 83. ((op (e0) (e1)) = (e1)) ((op (e0) (e1)) != (e1)) ### Axiom % 1.82/2.02 84. ((op (op (e0) (e1)) (e3)) != (op (e1) (e3))) ((op (e0) (e1)) = (e1)) ### NotEqual 83 3 % 1.82/2.02 85. ((op (e1) (e3)) = (e2)) ((op (e1) (e3)) != (e2)) ### Axiom % 1.82/2.02 86. ((op (e0) (op (e1) (e3))) != (op (e0) (e2))) ((op (e1) (e3)) = (e2)) ### NotEqual 8 85 % 1.82/2.02 87. ((e2) != (op (e0) (op (e1) (e3)))) ((op (e0) (e2)) = (e2)) ((op (e1) (e3)) = (e2)) ### Trans-sym 86 77 % 1.82/2.02 88. ((op (op (e0) (e1)) (e3)) != (op (e0) (op (e1) (e3)))) ((op (e1) (e3)) = (e2)) ((op (e0) (e2)) = (e2)) ((op (e0) (e1)) = (e1)) ### Trans 84 87 % 1.82/2.02 89. ((op (e0) (e2)) = (e2)) ((op (e0) (e2)) != (e2)) ### Axiom % 1.82/2.02 90. ((op (op (e0) (e2)) (e0)) != (op (e2) (e0))) ((op (e0) (e2)) = (e2)) ### NotEqual 89 8 % 1.82/2.02 91. ((op (e2) (e0)) = (e2)) ((op (e2) (e0)) != (e2)) ### Axiom % 1.82/2.02 92. ((op (e0) (op (e2) (e0))) != (op (e0) (e2))) ((op (e2) (e0)) = (e2)) ### NotEqual 8 91 % 1.82/2.02 93. ((e2) != (op (e0) (op (e2) (e0)))) ((op (e0) (e2)) = (e2)) ((op (e2) (e0)) = (e2)) ### Trans-sym 92 77 % 1.82/2.02 94. ((op (op (e0) (e2)) (e0)) != (op (e0) (op (e2) (e0)))) ((op (e2) (e0)) = (e2)) ((op (e0) (e2)) = (e2)) ### Trans 90 93 % 1.82/2.02 95. ((op (e0) (e2)) = (e2)) ((op (e0) (e2)) != (e2)) ### Axiom % 1.82/2.02 96. ((op (op (e0) (e2)) (e1)) != (op (e2) (e1))) ((op (e0) (e2)) = (e2)) ### NotEqual 95 67 % 1.82/2.02 97. ((op (e2) (e1)) = (e0)) ((op (e2) (e1)) != (e0)) ### Axiom % 1.82/2.02 98. ((op (e0) (op (e2) (e1))) != (op (e0) (e0))) ((op (e2) (e1)) = (e0)) ### NotEqual 8 97 % 1.82/2.02 99. ((e0) != (op (e0) (op (e2) (e1)))) ((op (e0) (e0)) = (e0)) ((op (e2) (e1)) = (e0)) ### Trans-sym 98 8 % 1.82/2.02 100. ((op (op (e0) (e2)) (e1)) != (op (e0) (op (e2) (e1)))) ((op (e2) (e1)) = (e0)) ((op (e0) (e0)) = (e0)) ((op (e0) (e2)) = (e2)) ### Trans 96 99 % 1.82/2.02 101. ((op (e0) (e2)) = (e2)) ((op (e0) (e2)) != (e2)) ### Axiom % 1.82/2.02 102. ((op (op (e0) (e2)) (e2)) != (op (e2) (e2))) ((op (e0) (e2)) = (e2)) ### NotEqual 101 77 % 1.82/2.02 103. ((op (e2) (e2)) = (e3)) ((op (e2) (e2)) != (e3)) ### Axiom % 1.82/2.02 104. ((op (e0) (op (e2) (e2))) != (op (e0) (e3))) ((op (e2) (e2)) = (e3)) ### NotEqual 8 103 % 1.82/2.02 105. ((e3) != (op (e0) (op (e2) (e2)))) ((op (e0) (e3)) = (e3)) ((op (e2) (e2)) = (e3)) ### Trans-sym 104 3 % 1.82/2.02 106. ((op (op (e0) (e2)) (e2)) != (op (e0) (op (e2) (e2)))) ((op (e2) (e2)) = (e3)) ((op (e0) (e3)) = (e3)) ((op (e0) (e2)) = (e2)) ### Trans 102 105 % 1.82/2.02 107. ((op (e0) (e2)) = (e2)) ((op (e0) (e2)) != (e2)) ### Axiom % 1.82/2.02 108. ((op (op (e0) (e2)) (e3)) != (op (e2) (e3))) ((op (e0) (e2)) = (e2)) ### NotEqual 107 3 % 1.82/2.02 109. ((op (e2) (e3)) = (e1)) ((op (e2) (e3)) != (e1)) ### Axiom % 1.82/2.02 110. ((op (e0) (op (e2) (e3))) != (op (e0) (e1))) ((op (e2) (e3)) = (e1)) ### NotEqual 8 109 % 1.82/2.02 111. ((e1) != (op (e0) (op (e2) (e3)))) ((op (e0) (e1)) = (e1)) ((op (e2) (e3)) = (e1)) ### Trans-sym 110 67 % 1.82/2.02 112. ((op (op (e0) (e2)) (e3)) != (op (e0) (op (e2) (e3)))) ((op (e2) (e3)) = (e1)) ((op (e0) (e1)) = (e1)) ((op (e0) (e2)) = (e2)) ### Trans 108 111 % 1.82/2.02 113. ((op (e0) (e3)) = (e3)) ((op (e0) (e3)) != (e3)) ### Axiom % 1.82/2.02 114. ((op (op (e0) (e3)) (e0)) != (op (e3) (e0))) ((op (e0) (e3)) = (e3)) ### NotEqual 113 8 % 1.82/2.02 115. ((op (e3) (e0)) = (e3)) ((op (e3) (e0)) != (e3)) ### Axiom % 1.82/2.02 116. ((op (e0) (op (e3) (e0))) != (op (e0) (e3))) ((op (e3) (e0)) = (e3)) ### NotEqual 8 115 % 1.82/2.02 117. ((e3) != (op (e0) (op (e3) (e0)))) ((op (e0) (e3)) = (e3)) ((op (e3) (e0)) = (e3)) ### Trans-sym 116 3 % 1.82/2.02 118. ((op (op (e0) (e3)) (e0)) != (op (e0) (op (e3) (e0)))) ((op (e3) (e0)) = (e3)) ((op (e0) (e3)) = (e3)) ### Trans 114 117 % 1.82/2.02 119. ((op (e0) (e3)) = (e3)) ((op (e0) (e3)) != (e3)) ### Axiom % 1.82/2.02 120. ((op (op (e0) (e3)) (e1)) != (op (e3) (e1))) ((op (e0) (e3)) = (e3)) ### NotEqual 119 67 % 1.82/2.02 121. ((op (e3) (e1)) = (e2)) ((op (e3) (e1)) != (e2)) ### Axiom % 1.82/2.02 122. ((op (e0) (op (e3) (e1))) != (op (e0) (e2))) ((op (e3) (e1)) = (e2)) ### NotEqual 8 121 % 1.82/2.02 123. ((e2) != (op (e0) (op (e3) (e1)))) ((op (e0) (e2)) = (e2)) ((op (e3) (e1)) = (e2)) ### Trans-sym 122 77 % 1.82/2.02 124. ((op (op (e0) (e3)) (e1)) != (op (e0) (op (e3) (e1)))) ((op (e3) (e1)) = (e2)) ((op (e0) (e2)) = (e2)) ((op (e0) (e3)) = (e3)) ### Trans 120 123 % 1.82/2.02 125. ((op (e0) (e3)) = (e3)) ((op (e0) (e3)) != (e3)) ### Axiom % 1.82/2.02 126. ((op (op (e0) (e3)) (e2)) != (op (e3) (e2))) ((op (e0) (e3)) = (e3)) ### NotEqual 125 77 % 1.82/2.02 127. ((op (e3) (e2)) = (e1)) ((op (e3) (e2)) != (e1)) ### Axiom % 1.82/2.02 128. ((op (e0) (op (e3) (e2))) != (op (e0) (e1))) ((op (e3) (e2)) = (e1)) ### NotEqual 8 127 % 1.82/2.02 129. ((e1) != (op (e0) (op (e3) (e2)))) ((op (e0) (e1)) = (e1)) ((op (e3) (e2)) = (e1)) ### Trans-sym 128 67 % 1.82/2.02 130. ((op (op (e0) (e3)) (e2)) != (op (e0) (op (e3) (e2)))) ((op (e3) (e2)) = (e1)) ((op (e0) (e1)) = (e1)) ((op (e0) (e3)) = (e3)) ### Trans 126 129 % 1.82/2.02 131. ((op (e0) (e3)) = (e3)) ((op (e0) (e3)) != (e3)) ### Axiom % 1.82/2.02 132. ((op (op (e0) (e3)) (e3)) != (op (e3) (e3))) ((op (e0) (e3)) = (e3)) ### NotEqual 131 3 % 1.82/2.02 133. ((op (e3) (e3)) = (e0)) ((op (e3) (e3)) != (e0)) ### Axiom % 1.82/2.02 134. ((op (e0) (op (e3) (e3))) != (op (e0) (e0))) ((op (e3) (e3)) = (e0)) ### NotEqual 8 133 % 1.82/2.02 135. ((e0) != (op (e0) (op (e3) (e3)))) ((op (e0) (e0)) = (e0)) ((op (e3) (e3)) = (e0)) ### Trans-sym 134 8 % 1.82/2.02 136. ((op (op (e0) (e3)) (e3)) != (op (e0) (op (e3) (e3)))) ((op (e3) (e3)) = (e0)) ((op (e0) (e0)) = (e0)) ((op (e0) (e3)) = (e3)) ### Trans 132 135 % 1.82/2.02 137. ((op (e1) (e0)) = (e1)) ((op (e1) (e0)) != (e1)) ### Axiom % 1.82/2.02 138. ((op (e0) (e0)) = (e0)) ((e0) != (op (e0) (e0))) ### Sym(=) % 1.82/2.02 139. ((op (op (e1) (e0)) (e0)) != (op (e1) (op (e0) (e0)))) ((op (e0) (e0)) = (e0)) ((op (e1) (e0)) = (e1)) ### NotEqual 137 138 % 1.82/2.02 140. ((op (e1) (e0)) = (e1)) ((op (e1) (e0)) != (e1)) ### Axiom % 1.82/2.02 141. ((op (e0) (e1)) = (e1)) ((e1) != (op (e0) (e1))) ### Sym(=) % 1.82/2.02 142. ((op (op (e1) (e0)) (e1)) != (op (e1) (op (e0) (e1)))) ((op (e0) (e1)) = (e1)) ((op (e1) (e0)) = (e1)) ### NotEqual 140 141 % 1.82/2.02 143. ((op (e1) (e0)) = (e1)) ((op (e1) (e0)) != (e1)) ### Axiom % 1.82/2.02 144. ((op (e0) (e2)) = (e2)) ((e2) != (op (e0) (e2))) ### Sym(=) % 1.82/2.02 145. ((op (op (e1) (e0)) (e2)) != (op (e1) (op (e0) (e2)))) ((op (e0) (e2)) = (e2)) ((op (e1) (e0)) = (e1)) ### NotEqual 143 144 % 1.82/2.02 146. ((op (e1) (e0)) = (e1)) ((op (e1) (e0)) != (e1)) ### Axiom % 1.82/2.02 147. ((op (e0) (e3)) = (e3)) ((e3) != (op (e0) (e3))) ### Sym(=) % 1.82/2.02 148. ((op (op (e1) (e0)) (e3)) != (op (e1) (op (e0) (e3)))) ((op (e0) (e3)) = (e3)) ((op (e1) (e0)) = (e1)) ### NotEqual 146 147 % 1.82/2.02 149. ((op (e1) (e1)) = (e3)) ((op (e1) (e1)) != (e3)) ### Axiom % 1.82/2.02 150. ((op (op (e1) (e1)) (e0)) != (op (e3) (e0))) ((op (e1) (e1)) = (e3)) ### NotEqual 149 8 % 1.82/2.02 151. ((op (e1) (e0)) = (e1)) ((op (e1) (e0)) != (e1)) ### Axiom % 1.82/2.02 152. ((op (e1) (op (e1) (e0))) != (op (e1) (e1))) ((op (e1) (e0)) = (e1)) ### NotEqual 67 151 % 1.82/2.02 153. ((e3) != (op (e1) (op (e1) (e0)))) ((op (e1) (e1)) = (e3)) ((op (e1) (e0)) = (e1)) ### Trans-sym 152 3 % 1.82/2.02 154. ((op (op (e1) (e1)) (e0)) != (op (e1) (op (e1) (e0)))) ((op (e3) (e0)) = (e3)) ((op (e1) (e0)) = (e1)) ((op (e1) (e1)) = (e3)) ### Trans 150 153 % 1.82/2.02 155. ((op (e1) (e1)) = (e3)) ((op (e1) (e1)) != (e3)) ### Axiom % 1.82/2.02 156. ((op (op (e1) (e1)) (e1)) != (op (e3) (e1))) ((op (e1) (e1)) = (e3)) ### NotEqual 155 67 % 1.82/2.02 157. ((op (e1) (e1)) = (e3)) ((op (e1) (e1)) != (e3)) ### Axiom % 1.82/2.02 158. ((op (e1) (op (e1) (e1))) != (op (e1) (e3))) ((op (e1) (e1)) = (e3)) ### NotEqual 67 157 % 1.82/2.02 159. ((e2) != (op (e1) (op (e1) (e1)))) ((op (e1) (e3)) = (e2)) ((op (e1) (e1)) = (e3)) ### Trans-sym 158 77 % 1.82/2.02 160. ((op (op (e1) (e1)) (e1)) != (op (e1) (op (e1) (e1)))) ((op (e3) (e1)) = (e2)) ((op (e1) (e3)) = (e2)) ((op (e1) (e1)) = (e3)) ### Trans 156 159 % 1.82/2.02 161. ((op (e1) (e1)) = (e3)) ((op (e1) (e1)) != (e3)) ### Axiom % 1.82/2.02 162. ((op (op (e1) (e1)) (e2)) != (op (e3) (e2))) ((op (e1) (e1)) = (e3)) ### NotEqual 161 77 % 1.82/2.02 163. ((op (e1) (e2)) = (e0)) ((op (e1) (e2)) != (e0)) ### Axiom % 1.82/2.02 164. ((op (e1) (op (e1) (e2))) != (op (e1) (e0))) ((op (e1) (e2)) = (e0)) ### NotEqual 67 163 % 1.82/2.02 165. ((e1) != (op (e1) (op (e1) (e2)))) ((op (e1) (e0)) = (e1)) ((op (e1) (e2)) = (e0)) ### Trans-sym 164 67 % 1.82/2.02 166. ((op (op (e1) (e1)) (e2)) != (op (e1) (op (e1) (e2)))) ((op (e3) (e2)) = (e1)) ((op (e1) (e2)) = (e0)) ((op (e1) (e0)) = (e1)) ((op (e1) (e1)) = (e3)) ### Trans 162 165 % 1.82/2.02 167. ((op (e1) (e1)) = (e3)) ((op (e1) (e1)) != (e3)) ### Axiom % 1.82/2.02 168. ((op (op (e1) (e1)) (e3)) != (op (e3) (e3))) ((op (e1) (e1)) = (e3)) ### NotEqual 167 3 % 1.82/2.02 169. ((op (e1) (e3)) = (e2)) ((op (e1) (e3)) != (e2)) ### Axiom % 1.82/2.02 170. ((op (e1) (op (e1) (e3))) != (op (e1) (e2))) ((op (e1) (e3)) = (e2)) ### NotEqual 67 169 % 1.82/2.02 171. ((e0) != (op (e1) (op (e1) (e3)))) ((op (e1) (e2)) = (e0)) ((op (e1) (e3)) = (e2)) ### Trans-sym 170 8 % 1.82/2.02 172. ((op (op (e1) (e1)) (e3)) != (op (e1) (op (e1) (e3)))) ((op (e3) (e3)) = (e0)) ((op (e1) (e3)) = (e2)) ((op (e1) (e2)) = (e0)) ((op (e1) (e1)) = (e3)) ### Trans 168 171 % 1.82/2.02 173. ((op (e1) (e2)) = (e0)) ((op (e1) (e2)) != (e0)) ### Axiom % 1.82/2.02 174. ((op (op (e1) (e2)) (e0)) != (op (e0) (e0))) ((op (e1) (e2)) = (e0)) ### NotEqual 173 8 % 1.82/2.02 175. ((op (e2) (e0)) = (e2)) ((op (e2) (e0)) != (e2)) ### Axiom % 1.82/2.02 176. ((op (e1) (op (e2) (e0))) != (op (e1) (e2))) ((op (e2) (e0)) = (e2)) ### NotEqual 67 175 % 1.82/2.02 177. ((e0) != (op (e1) (op (e2) (e0)))) ((op (e1) (e2)) = (e0)) ((op (e2) (e0)) = (e2)) ### Trans-sym 176 8 % 1.82/2.02 178. ((op (op (e1) (e2)) (e0)) != (op (e1) (op (e2) (e0)))) ((op (e0) (e0)) = (e0)) ((op (e2) (e0)) = (e2)) ((op (e1) (e2)) = (e0)) ### Trans 174 177 % 1.82/2.02 179. ((op (e1) (e2)) = (e0)) ((op (e1) (e2)) != (e0)) ### Axiom % 1.82/2.02 180. ((op (op (e1) (e2)) (e1)) != (op (e0) (e1))) ((op (e1) (e2)) = (e0)) ### NotEqual 179 67 % 1.82/2.02 181. ((op (e2) (e1)) = (e0)) ((op (e2) (e1)) != (e0)) ### Axiom % 1.82/2.02 182. ((op (e1) (op (e2) (e1))) != (op (e1) (e0))) ((op (e2) (e1)) = (e0)) ### NotEqual 67 181 % 1.82/2.02 183. ((e1) != (op (e1) (op (e2) (e1)))) ((op (e1) (e0)) = (e1)) ((op (e2) (e1)) = (e0)) ### Trans-sym 182 67 % 1.82/2.02 184. ((op (op (e1) (e2)) (e1)) != (op (e1) (op (e2) (e1)))) ((op (e0) (e1)) = (e1)) ((op (e2) (e1)) = (e0)) ((op (e1) (e0)) = (e1)) ((op (e1) (e2)) = (e0)) ### Trans 180 183 % 1.82/2.02 185. ((op (e1) (e2)) = (e0)) ((op (e1) (e2)) != (e0)) ### Axiom % 1.82/2.02 186. ((op (op (e1) (e2)) (e2)) != (op (e0) (e2))) ((op (e1) (e2)) = (e0)) ### NotEqual 185 77 % 1.82/2.02 187. ((op (e2) (e2)) = (e3)) ((op (e2) (e2)) != (e3)) ### Axiom % 1.82/2.02 188. ((op (e1) (op (e2) (e2))) != (op (e1) (e3))) ((op (e2) (e2)) = (e3)) ### NotEqual 67 187 % 1.82/2.02 189. ((e2) != (op (e1) (op (e2) (e2)))) ((op (e1) (e3)) = (e2)) ((op (e2) (e2)) = (e3)) ### Trans-sym 188 77 % 1.82/2.02 190. ((op (op (e1) (e2)) (e2)) != (op (e1) (op (e2) (e2)))) ((op (e0) (e2)) = (e2)) ((op (e2) (e2)) = (e3)) ((op (e1) (e3)) = (e2)) ((op (e1) (e2)) = (e0)) ### Trans 186 189 % 1.82/2.02 191. ((op (e1) (e2)) = (e0)) ((op (e1) (e2)) != (e0)) ### Axiom % 1.82/2.02 192. ((op (op (e1) (e2)) (e3)) != (op (e0) (e3))) ((op (e1) (e2)) = (e0)) ### NotEqual 191 3 % 1.82/2.02 193. ((op (e2) (e3)) = (e1)) ((op (e2) (e3)) != (e1)) ### Axiom % 1.82/2.02 194. ((op (e1) (op (e2) (e3))) != (op (e1) (e1))) ((op (e2) (e3)) = (e1)) ### NotEqual 67 193 % 1.82/2.02 195. ((e3) != (op (e1) (op (e2) (e3)))) ((op (e1) (e1)) = (e3)) ((op (e2) (e3)) = (e1)) ### Trans-sym 194 3 % 1.82/2.02 196. ((op (op (e1) (e2)) (e3)) != (op (e1) (op (e2) (e3)))) ((op (e0) (e3)) = (e3)) ((op (e2) (e3)) = (e1)) ((op (e1) (e1)) = (e3)) ((op (e1) (e2)) = (e0)) ### Trans 192 195 % 1.82/2.02 197. ((op (e1) (e3)) = (e2)) ((op (e1) (e3)) != (e2)) ### Axiom % 1.82/2.02 198. ((op (op (e1) (e3)) (e0)) != (op (e2) (e0))) ((op (e1) (e3)) = (e2)) ### NotEqual 197 8 % 1.82/2.02 199. ((op (e3) (e0)) = (e3)) ((op (e3) (e0)) != (e3)) ### Axiom % 1.82/2.02 200. ((op (e1) (op (e3) (e0))) != (op (e1) (e3))) ((op (e3) (e0)) = (e3)) ### NotEqual 67 199 % 1.82/2.02 201. ((e2) != (op (e1) (op (e3) (e0)))) ((op (e1) (e3)) = (e2)) ((op (e3) (e0)) = (e3)) ### Trans-sym 200 77 % 1.82/2.02 202. ((op (op (e1) (e3)) (e0)) != (op (e1) (op (e3) (e0)))) ((op (e2) (e0)) = (e2)) ((op (e3) (e0)) = (e3)) ((op (e1) (e3)) = (e2)) ### Trans 198 201 % 1.82/2.02 203. ((op (e1) (e3)) = (e2)) ((op (e1) (e3)) != (e2)) ### Axiom % 1.82/2.02 204. ((op (op (e1) (e3)) (e1)) != (op (e2) (e1))) ((op (e1) (e3)) = (e2)) ### NotEqual 203 67 % 1.82/2.02 205. ((op (e3) (e1)) = (e2)) ((op (e3) (e1)) != (e2)) ### Axiom % 1.82/2.02 206. ((op (e1) (op (e3) (e1))) != (op (e1) (e2))) ((op (e3) (e1)) = (e2)) ### NotEqual 67 205 % 1.82/2.02 207. ((e0) != (op (e1) (op (e3) (e1)))) ((op (e1) (e2)) = (e0)) ((op (e3) (e1)) = (e2)) ### Trans-sym 206 8 % 1.82/2.02 208. ((op (op (e1) (e3)) (e1)) != (op (e1) (op (e3) (e1)))) ((op (e2) (e1)) = (e0)) ((op (e3) (e1)) = (e2)) ((op (e1) (e2)) = (e0)) ((op (e1) (e3)) = (e2)) ### Trans 204 207 % 1.82/2.02 209. ((op (e1) (e3)) = (e2)) ((op (e1) (e3)) != (e2)) ### Axiom % 1.82/2.02 210. ((op (op (e1) (e3)) (e2)) != (op (e2) (e2))) ((op (e1) (e3)) = (e2)) ### NotEqual 209 77 % 1.82/2.02 211. ((op (e3) (e2)) = (e1)) ((op (e3) (e2)) != (e1)) ### Axiom % 1.82/2.02 212. ((op (e1) (op (e3) (e2))) != (op (e1) (e1))) ((op (e3) (e2)) = (e1)) ### NotEqual 67 211 % 1.82/2.02 213. ((e3) != (op (e1) (op (e3) (e2)))) ((op (e1) (e1)) = (e3)) ((op (e3) (e2)) = (e1)) ### Trans-sym 212 3 % 1.82/2.02 214. ((op (op (e1) (e3)) (e2)) != (op (e1) (op (e3) (e2)))) ((op (e2) (e2)) = (e3)) ((op (e3) (e2)) = (e1)) ((op (e1) (e1)) = (e3)) ((op (e1) (e3)) = (e2)) ### Trans 210 213 % 1.82/2.02 215. ((op (e1) (e3)) = (e2)) ((op (e1) (e3)) != (e2)) ### Axiom % 1.82/2.02 216. ((op (op (e1) (e3)) (e3)) != (op (e2) (e3))) ((op (e1) (e3)) = (e2)) ### NotEqual 215 3 % 1.82/2.02 217. ((op (e3) (e3)) = (e0)) ((op (e3) (e3)) != (e0)) ### Axiom % 1.82/2.02 218. ((op (e1) (op (e3) (e3))) != (op (e1) (e0))) ((op (e3) (e3)) = (e0)) ### NotEqual 67 217 % 1.82/2.02 219. ((e1) != (op (e1) (op (e3) (e3)))) ((op (e1) (e0)) = (e1)) ((op (e3) (e3)) = (e0)) ### Trans-sym 218 67 % 1.82/2.02 220. ((op (op (e1) (e3)) (e3)) != (op (e1) (op (e3) (e3)))) ((op (e2) (e3)) = (e1)) ((op (e3) (e3)) = (e0)) ((op (e1) (e0)) = (e1)) ((op (e1) (e3)) = (e2)) ### Trans 216 219 % 1.82/2.02 221. ((op (e2) (e0)) = (e2)) ((op (e2) (e0)) != (e2)) ### Axiom % 1.82/2.02 222. ((op (e0) (e0)) = (e0)) ((e0) != (op (e0) (e0))) ### Sym(=) % 1.82/2.02 223. ((op (op (e2) (e0)) (e0)) != (op (e2) (op (e0) (e0)))) ((op (e0) (e0)) = (e0)) ((op (e2) (e0)) = (e2)) ### NotEqual 221 222 % 1.82/2.02 224. ((op (e2) (e0)) = (e2)) ((op (e2) (e0)) != (e2)) ### Axiom % 1.82/2.02 225. ((op (e0) (e1)) = (e1)) ((e1) != (op (e0) (e1))) ### Sym(=) % 1.82/2.02 226. ((op (op (e2) (e0)) (e1)) != (op (e2) (op (e0) (e1)))) ((op (e0) (e1)) = (e1)) ((op (e2) (e0)) = (e2)) ### NotEqual 224 225 % 1.82/2.02 227. ((op (e2) (e0)) = (e2)) ((op (e2) (e0)) != (e2)) ### Axiom % 1.82/2.02 228. ((op (e0) (e2)) = (e2)) ((e2) != (op (e0) (e2))) ### Sym(=) % 1.82/2.02 229. ((op (op (e2) (e0)) (e2)) != (op (e2) (op (e0) (e2)))) ((op (e0) (e2)) = (e2)) ((op (e2) (e0)) = (e2)) ### NotEqual 227 228 % 1.82/2.02 230. ((op (e2) (e0)) = (e2)) ((op (e2) (e0)) != (e2)) ### Axiom % 1.82/2.02 231. ((op (e0) (e3)) = (e3)) ((e3) != (op (e0) (e3))) ### Sym(=) % 1.82/2.02 232. ((op (op (e2) (e0)) (e3)) != (op (e2) (op (e0) (e3)))) ((op (e0) (e3)) = (e3)) ((op (e2) (e0)) = (e2)) ### NotEqual 230 231 % 1.82/2.02 233. ((op (e2) (e1)) = (e0)) ((op (e2) (e1)) != (e0)) ### Axiom % 1.82/2.02 234. ((op (op (e2) (e1)) (e0)) != (op (e0) (e0))) ((op (e2) (e1)) = (e0)) ### NotEqual 233 8 % 1.82/2.02 235. ((op (e1) (e0)) = (e1)) ((op (e1) (e0)) != (e1)) ### Axiom % 1.82/2.02 236. ((op (e2) (op (e1) (e0))) != (op (e2) (e1))) ((op (e1) (e0)) = (e1)) ### NotEqual 77 235 % 1.82/2.02 237. ((e0) != (op (e2) (op (e1) (e0)))) ((op (e2) (e1)) = (e0)) ((op (e1) (e0)) = (e1)) ### Trans-sym 236 8 % 1.82/2.02 238. ((op (op (e2) (e1)) (e0)) != (op (e2) (op (e1) (e0)))) ((op (e0) (e0)) = (e0)) ((op (e1) (e0)) = (e1)) ((op (e2) (e1)) = (e0)) ### Trans 234 237 % 1.82/2.02 239. ((op (e2) (e1)) = (e0)) ((op (e2) (e1)) != (e0)) ### Axiom % 1.82/2.02 240. ((op (op (e2) (e1)) (e1)) != (op (e0) (e1))) ((op (e2) (e1)) = (e0)) ### NotEqual 239 67 % 1.82/2.02 241. ((op (e1) (e1)) = (e3)) ((op (e1) (e1)) != (e3)) ### Axiom % 1.82/2.02 242. ((op (e2) (op (e1) (e1))) != (op (e2) (e3))) ((op (e1) (e1)) = (e3)) ### NotEqual 77 241 % 1.82/2.02 243. ((e1) != (op (e2) (op (e1) (e1)))) ((op (e2) (e3)) = (e1)) ((op (e1) (e1)) = (e3)) ### Trans-sym 242 67 % 1.82/2.02 244. ((op (op (e2) (e1)) (e1)) != (op (e2) (op (e1) (e1)))) ((op (e0) (e1)) = (e1)) ((op (e1) (e1)) = (e3)) ((op (e2) (e3)) = (e1)) ((op (e2) (e1)) = (e0)) ### Trans 240 243 % 1.82/2.02 245. ((op (e2) (e1)) = (e0)) ((op (e2) (e1)) != (e0)) ### Axiom % 1.82/2.02 246. ((op (op (e2) (e1)) (e2)) != (op (e0) (e2))) ((op (e2) (e1)) = (e0)) ### NotEqual 245 77 % 1.82/2.02 247. ((op (e1) (e2)) = (e0)) ((op (e1) (e2)) != (e0)) ### Axiom % 1.82/2.02 248. ((op (e2) (op (e1) (e2))) != (op (e2) (e0))) ((op (e1) (e2)) = (e0)) ### NotEqual 77 247 % 1.82/2.02 249. ((e2) != (op (e2) (op (e1) (e2)))) ((op (e2) (e0)) = (e2)) ((op (e1) (e2)) = (e0)) ### Trans-sym 248 77 % 1.82/2.02 250. ((op (op (e2) (e1)) (e2)) != (op (e2) (op (e1) (e2)))) ((op (e0) (e2)) = (e2)) ((op (e1) (e2)) = (e0)) ((op (e2) (e0)) = (e2)) ((op (e2) (e1)) = (e0)) ### Trans 246 249 % 1.82/2.02 251. ((op (e2) (e1)) = (e0)) ((op (e2) (e1)) != (e0)) ### Axiom % 1.82/2.02 252. ((op (op (e2) (e1)) (e3)) != (op (e0) (e3))) ((op (e2) (e1)) = (e0)) ### NotEqual 251 3 % 1.82/2.02 253. ((op (e1) (e3)) = (e2)) ((op (e1) (e3)) != (e2)) ### Axiom % 1.82/2.02 254. ((op (e2) (op (e1) (e3))) != (op (e2) (e2))) ((op (e1) (e3)) = (e2)) ### NotEqual 77 253 % 1.82/2.02 255. ((e3) != (op (e2) (op (e1) (e3)))) ((op (e2) (e2)) = (e3)) ((op (e1) (e3)) = (e2)) ### Trans-sym 254 3 % 1.82/2.02 256. ((op (op (e2) (e1)) (e3)) != (op (e2) (op (e1) (e3)))) ((op (e0) (e3)) = (e3)) ((op (e1) (e3)) = (e2)) ((op (e2) (e2)) = (e3)) ((op (e2) (e1)) = (e0)) ### Trans 252 255 % 1.82/2.02 257. ((op (e2) (e2)) = (e3)) ((op (e2) (e2)) != (e3)) ### Axiom % 1.82/2.02 258. ((op (op (e2) (e2)) (e0)) != (op (e3) (e0))) ((op (e2) (e2)) = (e3)) ### NotEqual 257 8 % 1.82/2.02 259. ((op (e2) (e0)) = (e2)) ((op (e2) (e0)) != (e2)) ### Axiom % 1.82/2.02 260. ((op (e2) (op (e2) (e0))) != (op (e2) (e2))) ((op (e2) (e0)) = (e2)) ### NotEqual 77 259 % 1.82/2.02 261. ((e3) != (op (e2) (op (e2) (e0)))) ((op (e2) (e2)) = (e3)) ((op (e2) (e0)) = (e2)) ### Trans-sym 260 3 % 1.82/2.02 262. ((op (op (e2) (e2)) (e0)) != (op (e2) (op (e2) (e0)))) ((op (e3) (e0)) = (e3)) ((op (e2) (e0)) = (e2)) ((op (e2) (e2)) = (e3)) ### Trans 258 261 % 1.82/2.02 263. ((op (e2) (e2)) = (e3)) ((op (e2) (e2)) != (e3)) ### Axiom % 1.82/2.02 264. ((op (op (e2) (e2)) (e1)) != (op (e3) (e1))) ((op (e2) (e2)) = (e3)) ### NotEqual 263 67 % 1.82/2.02 265. ((op (e2) (e1)) = (e0)) ((op (e2) (e1)) != (e0)) ### Axiom % 1.82/2.02 266. ((op (e2) (op (e2) (e1))) != (op (e2) (e0))) ((op (e2) (e1)) = (e0)) ### NotEqual 77 265 % 1.82/2.02 267. ((e2) != (op (e2) (op (e2) (e1)))) ((op (e2) (e0)) = (e2)) ((op (e2) (e1)) = (e0)) ### Trans-sym 266 77 % 1.82/2.02 268. ((op (op (e2) (e2)) (e1)) != (op (e2) (op (e2) (e1)))) ((op (e3) (e1)) = (e2)) ((op (e2) (e1)) = (e0)) ((op (e2) (e0)) = (e2)) ((op (e2) (e2)) = (e3)) ### Trans 264 267 % 1.82/2.02 269. ((op (e2) (e2)) = (e3)) ((op (e2) (e2)) != (e3)) ### Axiom % 1.82/2.02 270. ((op (op (e2) (e2)) (e2)) != (op (e3) (e2))) ((op (e2) (e2)) = (e3)) ### NotEqual 269 77 % 1.82/2.02 271. ((op (e2) (e2)) = (e3)) ((op (e2) (e2)) != (e3)) ### Axiom % 1.82/2.02 272. ((op (e2) (op (e2) (e2))) != (op (e2) (e3))) ((op (e2) (e2)) = (e3)) ### NotEqual 77 271 % 1.82/2.02 273. ((e1) != (op (e2) (op (e2) (e2)))) ((op (e2) (e3)) = (e1)) ((op (e2) (e2)) = (e3)) ### Trans-sym 272 67 % 1.82/2.02 274. ((op (op (e2) (e2)) (e2)) != (op (e2) (op (e2) (e2)))) ((op (e3) (e2)) = (e1)) ((op (e2) (e3)) = (e1)) ((op (e2) (e2)) = (e3)) ### Trans 270 273 % 1.82/2.02 275. ((op (e2) (e2)) = (e3)) ((op (e2) (e2)) != (e3)) ### Axiom % 1.82/2.02 276. ((op (op (e2) (e2)) (e3)) != (op (e3) (e3))) ((op (e2) (e2)) = (e3)) ### NotEqual 275 3 % 1.82/2.02 277. ((op (e2) (e3)) = (e1)) ((op (e2) (e3)) != (e1)) ### Axiom % 1.82/2.02 278. ((op (e2) (op (e2) (e3))) != (op (e2) (e1))) ((op (e2) (e3)) = (e1)) ### NotEqual 77 277 % 1.82/2.02 279. ((e0) != (op (e2) (op (e2) (e3)))) ((op (e2) (e1)) = (e0)) ((op (e2) (e3)) = (e1)) ### Trans-sym 278 8 % 1.82/2.02 280. ((op (op (e2) (e2)) (e3)) != (op (e2) (op (e2) (e3)))) ((op (e3) (e3)) = (e0)) ((op (e2) (e3)) = (e1)) ((op (e2) (e1)) = (e0)) ((op (e2) (e2)) = (e3)) ### Trans 276 279 % 1.82/2.02 281. ((op (e2) (e3)) = (e1)) ((op (e2) (e3)) != (e1)) ### Axiom % 1.82/2.02 282. ((op (op (e2) (e3)) (e0)) != (op (e1) (e0))) ((op (e2) (e3)) = (e1)) ### NotEqual 281 8 % 1.82/2.02 283. ((op (e3) (e0)) = (e3)) ((op (e3) (e0)) != (e3)) ### Axiom % 1.82/2.02 284. ((op (e2) (op (e3) (e0))) != (op (e2) (e3))) ((op (e3) (e0)) = (e3)) ### NotEqual 77 283 % 1.82/2.02 285. ((e1) != (op (e2) (op (e3) (e0)))) ((op (e2) (e3)) = (e1)) ((op (e3) (e0)) = (e3)) ### Trans-sym 284 67 % 1.82/2.02 286. ((op (op (e2) (e3)) (e0)) != (op (e2) (op (e3) (e0)))) ((op (e1) (e0)) = (e1)) ((op (e3) (e0)) = (e3)) ((op (e2) (e3)) = (e1)) ### Trans 282 285 % 1.82/2.02 287. ((op (e2) (e3)) = (e1)) ((op (e2) (e3)) != (e1)) ### Axiom % 1.82/2.02 288. ((op (op (e2) (e3)) (e1)) != (op (e1) (e1))) ((op (e2) (e3)) = (e1)) ### NotEqual 287 67 % 1.82/2.02 289. ((op (e3) (e1)) = (e2)) ((op (e3) (e1)) != (e2)) ### Axiom % 1.82/2.02 290. ((op (e2) (op (e3) (e1))) != (op (e2) (e2))) ((op (e3) (e1)) = (e2)) ### NotEqual 77 289 % 1.82/2.02 291. ((e3) != (op (e2) (op (e3) (e1)))) ((op (e2) (e2)) = (e3)) ((op (e3) (e1)) = (e2)) ### Trans-sym 290 3 % 1.82/2.02 292. ((op (op (e2) (e3)) (e1)) != (op (e2) (op (e3) (e1)))) ((op (e1) (e1)) = (e3)) ((op (e3) (e1)) = (e2)) ((op (e2) (e2)) = (e3)) ((op (e2) (e3)) = (e1)) ### Trans 288 291 % 1.82/2.02 293. ((op (e2) (e3)) = (e1)) ((op (e2) (e3)) != (e1)) ### Axiom % 1.82/2.02 294. ((op (op (e2) (e3)) (e2)) != (op (e1) (e2))) ((op (e2) (e3)) = (e1)) ### NotEqual 293 77 % 1.82/2.02 295. ((op (e3) (e2)) = (e1)) ((op (e3) (e2)) != (e1)) ### Axiom % 1.82/2.02 296. ((op (e2) (op (e3) (e2))) != (op (e2) (e1))) ((op (e3) (e2)) = (e1)) ### NotEqual 77 295 % 1.82/2.02 297. ((e0) != (op (e2) (op (e3) (e2)))) ((op (e2) (e1)) = (e0)) ((op (e3) (e2)) = (e1)) ### Trans-sym 296 8 % 1.82/2.02 298. ((op (op (e2) (e3)) (e2)) != (op (e2) (op (e3) (e2)))) ((op (e1) (e2)) = (e0)) ((op (e3) (e2)) = (e1)) ((op (e2) (e1)) = (e0)) ((op (e2) (e3)) = (e1)) ### Trans 294 297 % 1.82/2.02 299. ((op (e2) (e3)) = (e1)) ((op (e2) (e3)) != (e1)) ### Axiom % 1.82/2.02 300. ((op (op (e2) (e3)) (e3)) != (op (e1) (e3))) ((op (e2) (e3)) = (e1)) ### NotEqual 299 3 % 1.82/2.02 301. ((op (e3) (e3)) = (e0)) ((op (e3) (e3)) != (e0)) ### Axiom % 1.82/2.02 302. ((op (e2) (op (e3) (e3))) != (op (e2) (e0))) ((op (e3) (e3)) = (e0)) ### NotEqual 77 301 % 1.82/2.02 303. ((e2) != (op (e2) (op (e3) (e3)))) ((op (e2) (e0)) = (e2)) ((op (e3) (e3)) = (e0)) ### Trans-sym 302 77 % 1.82/2.02 304. ((op (op (e2) (e3)) (e3)) != (op (e2) (op (e3) (e3)))) ((op (e1) (e3)) = (e2)) ((op (e3) (e3)) = (e0)) ((op (e2) (e0)) = (e2)) ((op (e2) (e3)) = (e1)) ### Trans 300 303 % 1.82/2.02 305. ((op (e3) (e0)) = (e3)) ((op (e3) (e0)) != (e3)) ### Axiom % 1.82/2.02 306. ((op (e0) (e0)) = (e0)) ((e0) != (op (e0) (e0))) ### Sym(=) % 1.82/2.02 307. ((op (op (e3) (e0)) (e0)) != (op (e3) (op (e0) (e0)))) ((op (e0) (e0)) = (e0)) ((op (e3) (e0)) = (e3)) ### NotEqual 305 306 % 1.82/2.02 308. ((op (e3) (e0)) = (e3)) ((op (e3) (e0)) != (e3)) ### Axiom % 1.82/2.02 309. ((op (e0) (e1)) = (e1)) ((e1) != (op (e0) (e1))) ### Sym(=) % 1.82/2.02 310. ((op (op (e3) (e0)) (e1)) != (op (e3) (op (e0) (e1)))) ((op (e0) (e1)) = (e1)) ((op (e3) (e0)) = (e3)) ### NotEqual 308 309 % 1.82/2.02 311. ((op (e3) (e0)) = (e3)) ((op (e3) (e0)) != (e3)) ### Axiom % 1.82/2.02 312. ((op (e0) (e2)) = (e2)) ((e2) != (op (e0) (e2))) ### Sym(=) % 1.82/2.02 313. ((op (op (e3) (e0)) (e2)) != (op (e3) (op (e0) (e2)))) ((op (e0) (e2)) = (e2)) ((op (e3) (e0)) = (e3)) ### NotEqual 311 312 % 1.82/2.02 314. ((op (e3) (e0)) = (e3)) ((op (e3) (e0)) != (e3)) ### Axiom % 1.82/2.02 315. ((op (e0) (e3)) = (e3)) ((e3) != (op (e0) (e3))) ### Sym(=) % 1.82/2.02 316. ((op (op (e3) (e0)) (e3)) != (op (e3) (op (e0) (e3)))) ((op (e0) (e3)) = (e3)) ((op (e3) (e0)) = (e3)) ### NotEqual 314 315 % 1.82/2.02 317. ((op (e3) (e1)) = (e2)) ((op (e3) (e1)) != (e2)) ### Axiom % 1.82/2.02 318. ((op (op (e3) (e1)) (e0)) != (op (e2) (e0))) ((op (e3) (e1)) = (e2)) ### NotEqual 317 8 % 1.82/2.02 319. ((op (e1) (e0)) = (e1)) ((op (e1) (e0)) != (e1)) ### Axiom % 1.82/2.02 320. ((op (e3) (op (e1) (e0))) != (op (e3) (e1))) ((op (e1) (e0)) = (e1)) ### NotEqual 3 319 % 1.82/2.02 321. ((e2) != (op (e3) (op (e1) (e0)))) ((op (e3) (e1)) = (e2)) ((op (e1) (e0)) = (e1)) ### Trans-sym 320 77 % 1.82/2.02 322. ((op (op (e3) (e1)) (e0)) != (op (e3) (op (e1) (e0)))) ((op (e2) (e0)) = (e2)) ((op (e1) (e0)) = (e1)) ((op (e3) (e1)) = (e2)) ### Trans 318 321 % 1.82/2.02 323. ((op (e3) (e1)) = (e2)) ((op (e3) (e1)) != (e2)) ### Axiom % 1.82/2.02 324. ((op (op (e3) (e1)) (e1)) != (op (e2) (e1))) ((op (e3) (e1)) = (e2)) ### NotEqual 323 67 % 1.82/2.02 325. ((op (e1) (e1)) = (e3)) ((op (e1) (e1)) != (e3)) ### Axiom % 1.82/2.02 326. ((op (e3) (op (e1) (e1))) != (op (e3) (e3))) ((op (e1) (e1)) = (e3)) ### NotEqual 3 325 % 1.82/2.02 327. ((e0) != (op (e3) (op (e1) (e1)))) ((op (e3) (e3)) = (e0)) ((op (e1) (e1)) = (e3)) ### Trans-sym 326 8 % 1.82/2.02 328. ((op (op (e3) (e1)) (e1)) != (op (e3) (op (e1) (e1)))) ((op (e2) (e1)) = (e0)) ((op (e1) (e1)) = (e3)) ((op (e3) (e3)) = (e0)) ((op (e3) (e1)) = (e2)) ### Trans 324 327 % 1.82/2.02 329. ((op (e3) (e1)) = (e2)) ((op (e3) (e1)) != (e2)) ### Axiom % 1.82/2.02 330. ((op (op (e3) (e1)) (e2)) != (op (e2) (e2))) ((op (e3) (e1)) = (e2)) ### NotEqual 329 77 % 1.82/2.02 331. ((op (e1) (e2)) = (e0)) ((op (e1) (e2)) != (e0)) ### Axiom % 1.82/2.02 332. ((op (e3) (op (e1) (e2))) != (op (e3) (e0))) ((op (e1) (e2)) = (e0)) ### NotEqual 3 331 % 1.82/2.02 333. ((e3) != (op (e3) (op (e1) (e2)))) ((op (e3) (e0)) = (e3)) ((op (e1) (e2)) = (e0)) ### Trans-sym 332 3 % 1.82/2.02 334. ((op (op (e3) (e1)) (e2)) != (op (e3) (op (e1) (e2)))) ((op (e2) (e2)) = (e3)) ((op (e1) (e2)) = (e0)) ((op (e3) (e0)) = (e3)) ((op (e3) (e1)) = (e2)) ### Trans 330 333 % 1.82/2.02 335. ((op (e3) (e1)) = (e2)) ((op (e3) (e1)) != (e2)) ### Axiom % 1.82/2.02 336. ((op (op (e3) (e1)) (e3)) != (op (e2) (e3))) ((op (e3) (e1)) = (e2)) ### NotEqual 335 3 % 1.82/2.02 337. ((op (e1) (e3)) = (e2)) ((op (e1) (e3)) != (e2)) ### Axiom % 1.82/2.02 338. ((op (e3) (op (e1) (e3))) != (op (e3) (e2))) ((op (e1) (e3)) = (e2)) ### NotEqual 3 337 % 1.82/2.02 339. ((e1) != (op (e3) (op (e1) (e3)))) ((op (e3) (e2)) = (e1)) ((op (e1) (e3)) = (e2)) ### Trans-sym 338 67 % 1.82/2.02 340. ((op (op (e3) (e1)) (e3)) != (op (e3) (op (e1) (e3)))) ((op (e2) (e3)) = (e1)) ((op (e1) (e3)) = (e2)) ((op (e3) (e2)) = (e1)) ((op (e3) (e1)) = (e2)) ### Trans 336 339 % 1.82/2.02 341. ((op (e3) (e2)) = (e1)) ((op (e3) (e2)) != (e1)) ### Axiom % 1.82/2.02 342. ((op (op (e3) (e2)) (e0)) != (op (e1) (e0))) ((op (e3) (e2)) = (e1)) ### NotEqual 341 8 % 1.82/2.02 343. ((op (e2) (e0)) = (e2)) ((op (e2) (e0)) != (e2)) ### Axiom % 1.82/2.02 344. ((op (e3) (op (e2) (e0))) != (op (e3) (e2))) ((op (e2) (e0)) = (e2)) ### NotEqual 3 343 % 1.82/2.02 345. ((e1) != (op (e3) (op (e2) (e0)))) ((op (e3) (e2)) = (e1)) ((op (e2) (e0)) = (e2)) ### Trans-sym 344 67 % 1.82/2.02 346. ((op (op (e3) (e2)) (e0)) != (op (e3) (op (e2) (e0)))) ((op (e1) (e0)) = (e1)) ((op (e2) (e0)) = (e2)) ((op (e3) (e2)) = (e1)) ### Trans 342 345 % 1.82/2.02 347. ((op (e3) (e2)) = (e1)) ((op (e3) (e2)) != (e1)) ### Axiom % 1.82/2.02 348. ((op (op (e3) (e2)) (e1)) != (op (e1) (e1))) ((op (e3) (e2)) = (e1)) ### NotEqual 347 67 % 1.82/2.02 349. ((op (e2) (e1)) = (e0)) ((op (e2) (e1)) != (e0)) ### Axiom % 1.82/2.02 350. ((op (e3) (op (e2) (e1))) != (op (e3) (e0))) ((op (e2) (e1)) = (e0)) ### NotEqual 3 349 % 1.82/2.02 351. ((e3) != (op (e3) (op (e2) (e1)))) ((op (e3) (e0)) = (e3)) ((op (e2) (e1)) = (e0)) ### Trans-sym 350 3 % 1.82/2.02 352. ((op (op (e3) (e2)) (e1)) != (op (e3) (op (e2) (e1)))) ((op (e1) (e1)) = (e3)) ((op (e2) (e1)) = (e0)) ((op (e3) (e0)) = (e3)) ((op (e3) (e2)) = (e1)) ### Trans 348 351 % 1.82/2.02 353. ((op (e3) (e2)) = (e1)) ((op (e3) (e2)) != (e1)) ### Axiom % 1.82/2.02 354. ((op (op (e3) (e2)) (e2)) != (op (e1) (e2))) ((op (e3) (e2)) = (e1)) ### NotEqual 353 77 % 1.82/2.02 355. ((op (e2) (e2)) = (e3)) ((op (e2) (e2)) != (e3)) ### Axiom % 1.82/2.02 356. ((op (e3) (op (e2) (e2))) != (op (e3) (e3))) ((op (e2) (e2)) = (e3)) ### NotEqual 3 355 % 1.82/2.02 357. ((e0) != (op (e3) (op (e2) (e2)))) ((op (e3) (e3)) = (e0)) ((op (e2) (e2)) = (e3)) ### Trans-sym 356 8 % 1.82/2.02 358. ((op (op (e3) (e2)) (e2)) != (op (e3) (op (e2) (e2)))) ((op (e1) (e2)) = (e0)) ((op (e2) (e2)) = (e3)) ((op (e3) (e3)) = (e0)) ((op (e3) (e2)) = (e1)) ### Trans 354 357 % 1.82/2.02 359. ((op (e3) (e2)) = (e1)) ((op (e3) (e2)) != (e1)) ### Axiom % 1.82/2.02 360. ((op (op (e3) (e2)) (e3)) != (op (e1) (e3))) ((op (e3) (e2)) = (e1)) ### NotEqual 359 3 % 1.82/2.02 361. ((op (e2) (e3)) = (e1)) ((op (e2) (e3)) != (e1)) ### Axiom % 1.82/2.02 362. ((op (e3) (op (e2) (e3))) != (op (e3) (e1))) ((op (e2) (e3)) = (e1)) ### NotEqual 3 361 % 1.82/2.02 363. ((e2) != (op (e3) (op (e2) (e3)))) ((op (e3) (e1)) = (e2)) ((op (e2) (e3)) = (e1)) ### Trans-sym 362 77 % 1.82/2.02 364. ((op (op (e3) (e2)) (e3)) != (op (e3) (op (e2) (e3)))) ((op (e1) (e3)) = (e2)) ((op (e2) (e3)) = (e1)) ((op (e3) (e1)) = (e2)) ((op (e3) (e2)) = (e1)) ### Trans 360 363 % 1.82/2.02 365. ((op (e3) (e3)) = (e0)) ((op (e3) (e3)) != (e0)) ### Axiom % 1.82/2.02 366. ((op (op (e3) (e3)) (e0)) != (op (e0) (e0))) ((op (e3) (e3)) = (e0)) ### NotEqual 365 8 % 1.82/2.02 367. ((op (e3) (e0)) = (e3)) ((op (e3) (e0)) != (e3)) ### Axiom % 1.82/2.02 368. ((op (e3) (op (e3) (e0))) != (op (e3) (e3))) ((op (e3) (e0)) = (e3)) ### NotEqual 3 367 % 1.82/2.02 369. ((e0) != (op (e3) (op (e3) (e0)))) ((op (e3) (e3)) = (e0)) ((op (e3) (e0)) = (e3)) ### Trans-sym 368 8 % 1.82/2.02 370. ((op (op (e3) (e3)) (e0)) != (op (e3) (op (e3) (e0)))) ((op (e0) (e0)) = (e0)) ((op (e3) (e0)) = (e3)) ((op (e3) (e3)) = (e0)) ### Trans 366 369 % 1.82/2.02 371. ((op (e3) (e3)) = (e0)) ((op (e3) (e3)) != (e0)) ### Axiom % 1.82/2.02 372. ((op (op (e3) (e3)) (e1)) != (op (e0) (e1))) ((op (e3) (e3)) = (e0)) ### NotEqual 371 67 % 1.82/2.02 373. ((op (e3) (e1)) = (e2)) ((op (e3) (e1)) != (e2)) ### Axiom % 1.82/2.02 374. ((op (e3) (op (e3) (e1))) != (op (e3) (e2))) ((op (e3) (e1)) = (e2)) ### NotEqual 3 373 % 1.82/2.02 375. ((e1) != (op (e3) (op (e3) (e1)))) ((op (e3) (e2)) = (e1)) ((op (e3) (e1)) = (e2)) ### Trans-sym 374 67 % 1.82/2.02 376. ((op (op (e3) (e3)) (e1)) != (op (e3) (op (e3) (e1)))) ((op (e0) (e1)) = (e1)) ((op (e3) (e1)) = (e2)) ((op (e3) (e2)) = (e1)) ((op (e3) (e3)) = (e0)) ### Trans 372 375 % 1.82/2.02 377. ((op (e3) (e3)) = (e0)) ((op (e3) (e3)) != (e0)) ### Axiom % 1.82/2.02 378. ((op (op (e3) (e3)) (e2)) != (op (e0) (e2))) ((op (e3) (e3)) = (e0)) ### NotEqual 377 77 % 1.82/2.02 379. ((op (e3) (e2)) = (e1)) ((op (e3) (e2)) != (e1)) ### Axiom % 1.82/2.02 380. ((op (e3) (op (e3) (e2))) != (op (e3) (e1))) ((op (e3) (e2)) = (e1)) ### NotEqual 3 379 % 1.82/2.02 381. ((e2) != (op (e3) (op (e3) (e2)))) ((op (e3) (e1)) = (e2)) ((op (e3) (e2)) = (e1)) ### Trans-sym 380 77 % 1.82/2.02 382. ((op (op (e3) (e3)) (e2)) != (op (e3) (op (e3) (e2)))) ((op (e0) (e2)) = (e2)) ((op (e3) (e2)) = (e1)) ((op (e3) (e1)) = (e2)) ((op (e3) (e3)) = (e0)) ### Trans 378 381 % 1.82/2.02 383. ((op (e3) (e3)) = (e0)) ((op (e3) (e3)) != (e0)) ### Axiom % 1.82/2.02 384. ((op (op (e3) (e3)) (e3)) != (op (e0) (e3))) ((op (e3) (e3)) = (e0)) ### NotEqual 383 3 % 1.82/2.02 385. ((op (e3) (e3)) = (e0)) ((op (e3) (e3)) != (e0)) ### Axiom % 1.82/2.02 386. ((op (e3) (op (e3) (e3))) != (op (e3) (e0))) ((op (e3) (e3)) = (e0)) ### NotEqual 3 385 % 1.82/2.02 387. ((e3) != (op (e3) (op (e3) (e3)))) ((op (e3) (e0)) = (e3)) ((op (e3) (e3)) = (e0)) ### Trans-sym 386 3 % 1.82/2.02 388. ((op (op (e3) (e3)) (e3)) != (op (e3) (op (e3) (e3)))) ((op (e0) (e3)) = (e3)) ((op (e3) (e0)) = (e3)) ((op (e3) (e3)) = (e0)) ### Trans 384 387 % 1.82/2.02 389. ((unit) = (e0)) ((unit) != (e0)) ### Axiom % 1.82/2.02 390. ((op (unit) (e0)) != (op (e0) (e0))) ((unit) = (e0)) ### NotEqual 389 8 % 1.82/2.02 391. ((op (unit) (e0)) != (e0)) ((op (e0) (e0)) = (e0)) ((unit) = (e0)) ### Trans 390 8 % 1.82/2.02 392. ((unit) = (e0)) ((unit) != (e0)) ### Axiom % 1.82/2.02 393. ((op (e0) (unit)) != (op (e0) (e0))) ((unit) = (e0)) ### NotEqual 8 392 % 1.82/2.02 394. ((op (e0) (unit)) != (e0)) ((op (e0) (e0)) = (e0)) ((unit) = (e0)) ### Trans 393 8 % 1.82/2.02 395. ((unit) = (e0)) ((unit) != (e0)) ### Axiom % 1.82/2.02 396. ((op (unit) (e1)) != (op (e0) (e1))) ((unit) = (e0)) ### NotEqual 395 67 % 1.82/2.02 397. ((op (unit) (e1)) != (e1)) ((op (e0) (e1)) = (e1)) ((unit) = (e0)) ### Trans 396 67 % 1.82/2.02 398. ((unit) = (e0)) ((unit) != (e0)) ### Axiom % 1.82/2.02 399. ((op (e1) (unit)) != (op (e1) (e0))) ((unit) = (e0)) ### NotEqual 67 398 % 1.82/2.02 400. ((op (e1) (unit)) != (e1)) ((op (e1) (e0)) = (e1)) ((unit) = (e0)) ### Trans 399 67 % 1.82/2.02 401. ((unit) = (e0)) ((unit) != (e0)) ### Axiom % 1.82/2.02 402. ((op (unit) (e2)) != (op (e0) (e2))) ((unit) = (e0)) ### NotEqual 401 77 % 1.82/2.02 403. ((op (unit) (e2)) != (e2)) ((op (e0) (e2)) = (e2)) ((unit) = (e0)) ### Trans 402 77 % 1.82/2.02 404. ((unit) = (e0)) ((unit) != (e0)) ### Axiom % 1.82/2.02 405. ((op (e2) (unit)) != (op (e2) (e0))) ((unit) = (e0)) ### NotEqual 77 404 % 1.82/2.02 406. ((op (e2) (unit)) != (e2)) ((op (e2) (e0)) = (e2)) ((unit) = (e0)) ### Trans 405 77 % 1.82/2.02 407. ((unit) = (e0)) ((unit) != (e0)) ### Axiom % 1.82/2.02 408. ((op (unit) (e3)) != (op (e0) (e3))) ((unit) = (e0)) ### NotEqual 407 3 % 1.82/2.02 409. ((op (unit) (e3)) != (e3)) ((op (e0) (e3)) = (e3)) ((unit) = (e0)) ### Trans 408 3 % 1.82/2.02 410. ((unit) = (e0)) ((unit) != (e0)) ### Axiom % 1.82/2.02 411. ((op (e3) (unit)) != (op (e3) (e0))) ((unit) = (e0)) ### NotEqual 3 410 % 1.82/2.02 412. ((op (e3) (unit)) != (e3)) ((op (e3) (e0)) = (e3)) ((unit) = (e0)) ### Trans 411 3 % 1.82/2.02 413. ((unit) = (e0)) ((unit) != (e0)) ### Axiom % 1.82/2.02 414. (-. (((unit) = (e0)) \/ (((unit) = (e1)) \/ (((unit) = (e2)) \/ ((unit) = (e3)))))) ((unit) = (e0)) ### ConjTree 413 % 1.82/2.02 415. ((inv (e0)) = (e0)) ((inv (e0)) != (e0)) ### Axiom % 1.82/2.02 416. ((op (e0) (inv (e0))) != (op (e0) (e0))) ((inv (e0)) = (e0)) ### NotEqual 8 415 % 1.82/2.02 417. ((unit) = (e0)) ((e0) != (unit)) ### Sym(=) % 1.82/2.02 418. ((op (e0) (inv (e0))) != (unit)) ((op (e0) (e0)) = (e0)) ((unit) = (e0)) ((inv (e0)) = (e0)) ### Trans 416 417 % 1.82/2.02 419. ((inv (e0)) = (e0)) ((inv (e0)) != (e0)) ### Axiom % 1.82/2.02 420. ((op (inv (e0)) (e0)) != (op (e0) (e0))) ((inv (e0)) = (e0)) ### NotEqual 419 8 % 1.82/2.02 421. ((unit) = (e0)) ((e0) != (unit)) ### Sym(=) % 1.82/2.02 422. ((op (inv (e0)) (e0)) != (unit)) ((op (e0) (e0)) = (e0)) ((unit) = (e0)) ((inv (e0)) = (e0)) ### Trans 420 421 % 1.82/2.02 423. ((inv (e1)) = (e2)) ((inv (e1)) != (e2)) ### Axiom % 1.82/2.02 424. ((op (e1) (inv (e1))) != (op (e1) (e2))) ((inv (e1)) = (e2)) ### NotEqual 67 423 % 1.82/2.02 425. ((unit) = (e0)) ((e0) != (unit)) ### Sym(=) % 1.82/2.02 426. ((op (e1) (inv (e1))) != (unit)) ((op (e1) (e2)) = (e0)) ((unit) = (e0)) ((inv (e1)) = (e2)) ### Trans 424 425 % 1.82/2.02 427. ((inv (e1)) = (e2)) ((inv (e1)) != (e2)) ### Axiom % 1.82/2.02 428. ((op (inv (e1)) (e1)) != (op (e2) (e1))) ((inv (e1)) = (e2)) ### NotEqual 427 67 % 1.82/2.02 429. ((unit) = (e0)) ((e0) != (unit)) ### Sym(=) % 1.82/2.02 430. ((op (inv (e1)) (e1)) != (unit)) ((op (e2) (e1)) = (e0)) ((unit) = (e0)) ((inv (e1)) = (e2)) ### Trans 428 429 % 1.82/2.02 431. ((inv (e2)) = (e1)) ((inv (e2)) != (e1)) ### Axiom % 1.82/2.02 432. ((op (e2) (inv (e2))) != (op (e2) (e1))) ((inv (e2)) = (e1)) ### NotEqual 77 431 % 1.82/2.02 433. ((unit) = (e0)) ((e0) != (unit)) ### Sym(=) % 1.82/2.02 434. ((op (e2) (inv (e2))) != (unit)) ((op (e2) (e1)) = (e0)) ((unit) = (e0)) ((inv (e2)) = (e1)) ### Trans 432 433 % 1.82/2.02 435. ((inv (e2)) = (e1)) ((inv (e2)) != (e1)) ### Axiom % 1.82/2.02 436. ((op (inv (e2)) (e2)) != (op (e1) (e2))) ((inv (e2)) = (e1)) ### NotEqual 435 77 % 1.82/2.02 437. ((unit) = (e0)) ((e0) != (unit)) ### Sym(=) % 1.82/2.02 438. ((op (inv (e2)) (e2)) != (unit)) ((op (e1) (e2)) = (e0)) ((unit) = (e0)) ((inv (e2)) = (e1)) ### Trans 436 437 % 1.82/2.02 439. ((inv (e3)) = (e3)) ((inv (e3)) != (e3)) ### Axiom % 1.82/2.02 440. ((op (e3) (inv (e3))) != (op (e3) (e3))) ((inv (e3)) = (e3)) ### NotEqual 3 439 % 1.82/2.02 441. ((unit) = (e0)) ((e0) != (unit)) ### Sym(=) % 1.82/2.02 442. ((op (e3) (inv (e3))) != (unit)) ((op (e3) (e3)) = (e0)) ((unit) = (e0)) ((inv (e3)) = (e3)) ### Trans 440 441 % 1.82/2.02 443. ((inv (e3)) = (e3)) ((inv (e3)) != (e3)) ### Axiom % 1.82/2.02 444. ((op (inv (e3)) (e3)) != (op (e3) (e3))) ((inv (e3)) = (e3)) ### NotEqual 443 3 % 1.82/2.02 445. ((unit) = (e0)) ((e0) != (unit)) ### Sym(=) % 1.82/2.02 446. ((op (inv (e3)) (e3)) != (unit)) ((op (e3) (e3)) = (e0)) ((unit) = (e0)) ((inv (e3)) = (e3)) ### Trans 444 445 % 1.82/2.02 447. ((inv (e0)) = (e0)) ((inv (e0)) != (e0)) ### Axiom % 1.82/2.02 448. (-. (((inv (e0)) = (e0)) \/ (((inv (e0)) = (e1)) \/ (((inv (e0)) = (e2)) \/ ((inv (e0)) = (e3)))))) ((inv (e0)) = (e0)) ### ConjTree 447 % 1.82/2.02 449. ((inv (e1)) = (e2)) ((inv (e1)) != (e2)) ### Axiom % 1.82/2.02 450. (-. (((inv (e1)) = (e0)) \/ (((inv (e1)) = (e1)) \/ (((inv (e1)) = (e2)) \/ ((inv (e1)) = (e3)))))) ((inv (e1)) = (e2)) ### ConjTree 449 % 1.82/2.02 451. ((inv (e2)) = (e1)) ((inv (e2)) != (e1)) ### Axiom % 1.82/2.02 452. (-. (((inv (e2)) = (e0)) \/ (((inv (e2)) = (e1)) \/ (((inv (e2)) = (e2)) \/ ((inv (e2)) = (e3)))))) ((inv (e2)) = (e1)) ### ConjTree 451 % 1.82/2.02 453. ((inv (e3)) = (e3)) ((inv (e3)) != (e3)) ### Axiom % 1.82/2.02 454. (-. (((inv (e3)) = (e0)) \/ (((inv (e3)) = (e1)) \/ (((inv (e3)) = (e2)) \/ ((inv (e3)) = (e3)))))) ((inv (e3)) = (e3)) ### ConjTree 453 % 1.82/2.02 455. (-. ((-. ((((op (e0) (e0)) = (e0)) /\ (((op (e1) (e1)) = (e0)) /\ (((op (e2) (e2)) = (e0)) /\ ((op (e3) (e3)) = (e0))))) \/ ((((op (e0) (e0)) = (e1)) /\ (((op (e1) (e1)) = (e1)) /\ (((op (e2) (e2)) = (e1)) /\ ((op (e3) (e3)) = (e1))))) \/ ((((op (e0) (e0)) = (e2)) /\ (((op (e1) (e1)) = (e2)) /\ (((op (e2) (e2)) = (e2)) /\ ((op (e3) (e3)) = (e2))))) \/ (((op (e0) (e0)) = (e3)) /\ (((op (e1) (e1)) = (e3)) /\ (((op (e2) (e2)) = (e3)) /\ ((op (e3) (e3)) = (e3))))))))) /\ ((((op (e0) (e0)) = (e0)) \/ (((op (e0) (e0)) = (e1)) \/ (((op (e0) (e0)) = (e2)) \/ ((op (e0) (e0)) = (e3))))) /\ ((((op (e0) (e1)) = (e0)) \/ (((op (e0) (e1)) = (e1)) \/ (((op (e0) (e1)) = (e2)) \/ ((op (e0) (e1)) = (e3))))) /\ ((((op (e0) (e2)) = (e0)) \/ (((op (e0) (e2)) = (e1)) \/ (((op (e0) (e2)) = (e2)) \/ ((op (e0) (e2)) = (e3))))) /\ ((((op (e0) (e3)) = (e0)) \/ (((op (e0) (e3)) = (e1)) \/ (((op (e0) (e3)) = (e2)) \/ ((op (e0) (e3)) = (e3))))) /\ ((((op (e1) (e0)) = (e0)) \/ (((op (e1) (e0)) = (e1)) \/ (((op (e1) (e0)) = (e2)) \/ ((op (e1) (e0)) = (e3))))) /\ ((((op (e1) (e1)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e1) (e1)) = (e2)) \/ ((op (e1) (e1)) = (e3))))) /\ ((((op (e1) (e2)) = (e0)) \/ (((op (e1) (e2)) = (e1)) \/ (((op (e1) (e2)) = (e2)) \/ ((op (e1) (e2)) = (e3))))) /\ ((((op (e1) (e3)) = (e0)) \/ (((op (e1) (e3)) = (e1)) \/ (((op (e1) (e3)) = (e2)) \/ ((op (e1) (e3)) = (e3))))) /\ ((((op (e2) (e0)) = (e0)) \/ (((op (e2) (e0)) = (e1)) \/ (((op (e2) (e0)) = (e2)) \/ ((op (e2) (e0)) = (e3))))) /\ ((((op (e2) (e1)) = (e0)) \/ (((op (e2) (e1)) = (e1)) \/ (((op (e2) (e1)) = (e2)) \/ ((op (e2) (e1)) = (e3))))) /\ ((((op (e2) (e2)) = (e0)) \/ (((op (e2) (e2)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ ((op (e2) (e2)) = (e3))))) /\ ((((op (e2) (e3)) = (e0)) \/ (((op (e2) (e3)) = (e1)) \/ (((op (e2) (e3)) = (e2)) \/ ((op (e2) (e3)) = (e3))))) /\ ((((op (e3) (e0)) = (e0)) \/ (((op (e3) (e0)) = (e1)) \/ (((op (e3) (e0)) = (e2)) \/ ((op (e3) (e0)) = (e3))))) /\ ((((op (e3) (e1)) = (e0)) \/ (((op (e3) (e1)) = (e1)) \/ (((op (e3) (e1)) = (e2)) \/ ((op (e3) (e1)) = (e3))))) /\ ((((op (e3) (e2)) = (e0)) \/ (((op (e3) (e2)) = (e1)) \/ (((op (e3) (e2)) = (e2)) \/ ((op (e3) (e2)) = (e3))))) /\ ((((op (e3) (e3)) = (e0)) \/ (((op (e3) (e3)) = (e1)) \/ (((op (e3) (e3)) = (e2)) \/ ((op (e3) (e3)) = (e3))))) /\ (((op (op (e0) (e0)) (e0)) = (op (e0) (op (e0) (e0)))) /\ (((op (op (e0) (e0)) (e1)) = (op (e0) (op (e0) (e1)))) /\ (((op (op (e0) (e0)) (e2)) = (op (e0) (op (e0) (e2)))) /\ (((op (op (e0) (e0)) (e3)) = (op (e0) (op (e0) (e3)))) /\ (((op (op (e0) (e1)) (e0)) = (op (e0) (op (e1) (e0)))) /\ (((op (op (e0) (e1)) (e1)) = (op (e0) (op (e1) (e1)))) /\ (((op (op (e0) (e1)) (e2)) = (op (e0) (op (e1) (e2)))) /\ (((op (op (e0) (e1)) (e3)) = (op (e0) (op (e1) (e3)))) /\ (((op (op (e0) (e2)) (e0)) = (op (e0) (op (e2) (e0)))) /\ (((op (op (e0) (e2)) (e1)) = (op (e0) (op (e2) (e1)))) /\ (((op (op (e0) (e2)) (e2)) = (op (e0) (op (e2) (e2)))) /\ (((op (op (e0) (e2)) (e3)) = (op (e0) (op (e2) (e3)))) /\ (((op (op (e0) (e3)) (e0)) = (op (e0) (op (e3) (e0)))) /\ (((op (op (e0) (e3)) (e1)) = (op (e0) (op (e3) (e1)))) /\ (((op (op (e0) (e3)) (e2)) = (op (e0) (op (e3) (e2)))) /\ (((op (op (e0) (e3)) (e3)) = (op (e0) (op (e3) (e3)))) /\ (((op (op (e1) (e0)) (e0)) = (op (e1) (op (e0) (e0)))) /\ (((op (op (e1) (e0)) (e1)) = (op (e1) (op (e0) (e1)))) /\ (((op (op (e1) (e0)) (e2)) = (op (e1) (op (e0) (e2)))) /\ (((op (op (e1) (e0)) (e3)) = (op (e1) (op (e0) (e3)))) /\ (((op (op (e1) (e1)) (e0)) = (op (e1) (op (e1) (e0)))) /\ (((op (op (e1) (e1)) (e1)) = (op (e1) (op (e1) (e1)))) /\ (((op (op (e1) (e1)) (e2)) = (op (e1) (op (e1) (e2)))) /\ (((op (op (e1) (e1)) (e3)) = (op (e1) (op (e1) (e3)))) /\ (((op (op (e1) (e2)) (e0)) = (op (e1) (op (e2) (e0)))) /\ (((op (op (e1) (e2)) (e1)) = (op (e1) (op (e2) (e1)))) /\ (((op (op (e1) (e2)) (e2)) = (op (e1) (op (e2) (e2)))) /\ (((op (op (e1) (e2)) (e3)) = (op (e1) (op (e2) (e3)))) /\ (((op (op (e1) (e3)) (e0)) = (op (e1) (op (e3) (e0)))) /\ (((op (op (e1) (e3)) (e1)) = (op (e1) (op (e3) (e1)))) /\ (((op (op (e1) (e3)) (e2)) = (op (e1) (op (e3) (e2)))) /\ (((op (op (e1) (e3)) (e3)) = (op (e1) (op (e3) (e3)))) /\ (((op (op (e2) (e0)) (e0)) = (op (e2) (op (e0) (e0)))) /\ (((op (op (e2) (e0)) (e1)) = (op (e2) (op (e0) (e1)))) /\ (((op (op (e2) (e0)) (e2)) = (op (e2) (op (e0) (e2)))) /\ (((op (op (e2) (e0)) (e3)) = (op (e2) (op (e0) (e3)))) /\ (((op (op (e2) (e1)) (e0)) = (op (e2) (op (e1) (e0)))) /\ (((op (op (e2) (e1)) (e1)) = (op (e2) (op (e1) (e1)))) /\ (((op (op (e2) (e1)) (e2)) = (op (e2) (op (e1) (e2)))) /\ (((op (op (e2) (e1)) (e3)) = (op (e2) (op (e1) (e3)))) /\ (((op (op (e2) (e2)) (e0)) = (op (e2) (op (e2) (e0)))) /\ (((op (op (e2) (e2)) (e1)) = (op (e2) (op (e2) (e1)))) /\ (((op (op (e2) (e2)) (e2)) = (op (e2) (op (e2) (e2)))) /\ (((op (op (e2) (e2)) (e3)) = (op (e2) (op (e2) (e3)))) /\ (((op (op (e2) (e3)) (e0)) = (op (e2) (op (e3) (e0)))) /\ (((op (op (e2) (e3)) (e1)) = (op (e2) (op (e3) (e1)))) /\ (((op (op (e2) (e3)) (e2)) = (op (e2) (op (e3) (e2)))) /\ (((op (op (e2) (e3)) (e3)) = (op (e2) (op (e3) (e3)))) /\ (((op (op (e3) (e0)) (e0)) = (op (e3) (op (e0) (e0)))) /\ (((op (op (e3) (e0)) (e1)) = (op (e3) (op (e0) (e1)))) /\ (((op (op (e3) (e0)) (e2)) = (op (e3) (op (e0) (e2)))) /\ (((op (op (e3) (e0)) (e3)) = (op (e3) (op (e0) (e3)))) /\ (((op (op (e3) (e1)) (e0)) = (op (e3) (op (e1) (e0)))) /\ (((op (op (e3) (e1)) (e1)) = (op (e3) (op (e1) (e1)))) /\ (((op (op (e3) (e1)) (e2)) = (op (e3) (op (e1) (e2)))) /\ (((op (op (e3) (e1)) (e3)) = (op (e3) (op (e1) (e3)))) /\ (((op (op (e3) (e2)) (e0)) = (op (e3) (op (e2) (e0)))) /\ (((op (op (e3) (e2)) (e1)) = (op (e3) (op (e2) (e1)))) /\ (((op (op (e3) (e2)) (e2)) = (op (e3) (op (e2) (e2)))) /\ (((op (op (e3) (e2)) (e3)) = (op (e3) (op (e2) (e3)))) /\ (((op (op (e3) (e3)) (e0)) = (op (e3) (op (e3) (e0)))) /\ (((op (op (e3) (e3)) (e1)) = (op (e3) (op (e3) (e1)))) /\ (((op (op (e3) (e3)) (e2)) = (op (e3) (op (e3) (e2)))) /\ (((op (op (e3) (e3)) (e3)) = (op (e3) (op (e3) (e3)))) /\ (((op (unit) (e0)) = (e0)) /\ (((op (e0) (unit)) = (e0)) /\ (((op (unit) (e1)) = (e1)) /\ (((op (e1) (unit)) = (e1)) /\ (((op (unit) (e2)) = (e2)) /\ (((op (e2) (unit)) = (e2)) /\ (((op (unit) (e3)) = (e3)) /\ (((op (e3) (unit)) = (e3)) /\ ((((unit) = (e0)) \/ (((unit) = (e1)) \/ (((unit) = (e2)) \/ ((unit) = (e3))))) /\ (((op (e0) (inv (e0))) = (unit)) /\ (((op (inv (e0)) (e0)) = (unit)) /\ (((op (e1) (inv (e1))) = (unit)) /\ (((op (inv (e1)) (e1)) = (unit)) /\ (((op (e2) (inv (e2))) = (unit)) /\ (((op (inv (e2)) (e2)) = (unit)) /\ (((op (e3) (inv (e3))) = (unit)) /\ (((op (inv (e3)) (e3)) = (unit)) /\ ((((inv (e0)) = (e0)) \/ (((inv (e0)) = (e1)) \/ (((inv (e0)) = (e2)) \/ ((inv (e0)) = (e3))))) /\ ((((inv (e1)) = (e0)) \/ (((inv (e1)) = (e1)) \/ (((inv (e1)) = (e2)) \/ ((inv (e1)) = (e3))))) /\ ((((inv (e2)) = (e0)) \/ (((inv (e2)) = (e1)) \/ (((inv (e2)) = (e2)) \/ ((inv (e2)) = (e3))))) /\ (((inv (e3)) = (e0)) \/ (((inv (e3)) = (e1)) \/ (((inv (e3)) = (e2)) \/ ((inv (e3)) = (e3))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ((inv (e3)) = (e3)) ((inv (e2)) = (e1)) ((inv (e1)) = (e2)) ((inv (e0)) = (e0)) ((unit) = (e0)) ((op (e3) (e2)) = (e1)) ((op (e3) (e1)) = (e2)) ((op (e3) (e0)) = (e3)) ((op (e2) (e3)) = (e1)) ((op (e2) (e1)) = (e0)) ((op (e2) (e0)) = (e2)) ((op (e1) (e3)) = (e2)) ((op (e1) (e2)) = (e0)) ((op (e1) (e1)) = (e3)) ((op (e1) (e0)) = (e1)) ((op (e0) (e3)) = (e3)) ((op (e0) (e2)) = (e2)) ((op (e0) (e1)) = (e1)) ((op (e0) (e0)) = (e0)) ((e0) != (e2)) ((e0) != (e1)) ((op (e3) (e3)) = (e0)) ((e0) != (e3)) ((op (e2) (e2)) = (e3)) ### DisjTree 5 10 14 18 20 22 24 26 28 30 32 34 36 38 40 42 44 46 48 50 53 56 59 62 69 75 82 88 94 100 106 112 118 124 130 136 139 142 145 148 154 160 166 172 178 184 190 196 202 208 214 220 223 226 229 232 238 244 250 256 262 268 274 280 286 292 298 304 307 310 313 316 322 328 334 340 346 352 358 364 370 376 382 388 391 394 397 400 403 406 409 412 414 418 422 426 430 434 438 442 446 448 450 452 454 % 1.82/2.02 456. (((inv (e0)) = (e0)) /\ (((inv (e1)) = (e2)) /\ (((inv (e2)) = (e1)) /\ ((inv (e3)) = (e3))))) ((op (e2) (e2)) = (e3)) ((e0) != (e3)) ((op (e3) (e3)) = (e0)) ((e0) != (e1)) ((e0) != (e2)) ((op (e0) (e0)) = (e0)) ((op (e0) (e1)) = (e1)) ((op (e0) (e2)) = (e2)) ((op (e0) (e3)) = (e3)) ((op (e1) (e0)) = (e1)) ((op (e1) (e1)) = (e3)) ((op (e1) (e2)) = (e0)) ((op (e1) (e3)) = (e2)) ((op (e2) (e0)) = (e2)) ((op (e2) (e1)) = (e0)) ((op (e2) (e3)) = (e1)) ((op (e3) (e0)) = (e3)) ((op (e3) (e1)) = (e2)) ((op (e3) (e2)) = (e1)) ((unit) = (e0)) (-. ((-. ((((op (e0) (e0)) = (e0)) /\ (((op (e1) (e1)) = (e0)) /\ (((op (e2) (e2)) = (e0)) /\ ((op (e3) (e3)) = (e0))))) \/ ((((op (e0) (e0)) = (e1)) /\ (((op (e1) (e1)) = (e1)) /\ (((op (e2) (e2)) = (e1)) /\ ((op (e3) (e3)) = (e1))))) \/ ((((op (e0) (e0)) = (e2)) /\ (((op (e1) (e1)) = (e2)) /\ (((op (e2) (e2)) = (e2)) /\ ((op (e3) (e3)) = (e2))))) \/ (((op (e0) (e0)) = (e3)) /\ (((op (e1) (e1)) = (e3)) /\ (((op (e2) (e2)) = (e3)) /\ ((op (e3) (e3)) = (e3))))))))) /\ ((((op (e0) (e0)) = (e0)) \/ (((op (e0) (e0)) = (e1)) \/ (((op (e0) (e0)) = (e2)) \/ ((op (e0) (e0)) = (e3))))) /\ ((((op (e0) (e1)) = (e0)) \/ (((op (e0) (e1)) = (e1)) \/ (((op (e0) (e1)) = (e2)) \/ ((op (e0) (e1)) = (e3))))) /\ ((((op (e0) (e2)) = (e0)) \/ (((op (e0) (e2)) = (e1)) \/ (((op (e0) (e2)) = (e2)) \/ ((op (e0) (e2)) = (e3))))) /\ ((((op (e0) (e3)) = (e0)) \/ (((op (e0) (e3)) = (e1)) \/ (((op (e0) (e3)) = (e2)) \/ ((op (e0) (e3)) = (e3))))) /\ ((((op (e1) (e0)) = (e0)) \/ (((op (e1) (e0)) = (e1)) \/ (((op (e1) (e0)) = (e2)) \/ ((op (e1) (e0)) = (e3))))) /\ ((((op (e1) (e1)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e1) (e1)) = (e2)) \/ ((op (e1) (e1)) = (e3))))) /\ ((((op (e1) (e2)) = (e0)) \/ (((op (e1) (e2)) = (e1)) \/ (((op (e1) (e2)) = (e2)) \/ ((op (e1) (e2)) = (e3))))) /\ ((((op (e1) (e3)) = (e0)) \/ (((op (e1) (e3)) = (e1)) \/ (((op (e1) (e3)) = (e2)) \/ ((op (e1) (e3)) = (e3))))) /\ ((((op (e2) (e0)) = (e0)) \/ (((op (e2) (e0)) = (e1)) \/ (((op (e2) (e0)) = (e2)) \/ ((op (e2) (e0)) = (e3))))) /\ ((((op (e2) (e1)) = (e0)) \/ (((op (e2) (e1)) = (e1)) \/ (((op (e2) (e1)) = (e2)) \/ ((op (e2) (e1)) = (e3))))) /\ ((((op (e2) (e2)) = (e0)) \/ (((op (e2) (e2)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ ((op (e2) (e2)) = (e3))))) /\ ((((op (e2) (e3)) = (e0)) \/ (((op (e2) (e3)) = (e1)) \/ (((op (e2) (e3)) = (e2)) \/ ((op (e2) (e3)) = (e3))))) /\ ((((op (e3) (e0)) = (e0)) \/ (((op (e3) (e0)) = (e1)) \/ (((op (e3) (e0)) = (e2)) \/ ((op (e3) (e0)) = (e3))))) /\ ((((op (e3) (e1)) = (e0)) \/ (((op (e3) (e1)) = (e1)) \/ (((op (e3) (e1)) = (e2)) \/ ((op (e3) (e1)) = (e3))))) /\ ((((op (e3) (e2)) = (e0)) \/ (((op (e3) (e2)) = (e1)) \/ (((op (e3) (e2)) = (e2)) \/ ((op (e3) (e2)) = (e3))))) /\ ((((op (e3) (e3)) = (e0)) \/ (((op (e3) (e3)) = (e1)) \/ (((op (e3) (e3)) = (e2)) \/ ((op (e3) (e3)) = (e3))))) /\ (((op (op (e0) (e0)) (e0)) = (op (e0) (op (e0) (e0)))) /\ (((op (op (e0) (e0)) (e1)) = (op (e0) (op (e0) (e1)))) /\ (((op (op (e0) (e0)) (e2)) = (op (e0) (op (e0) (e2)))) /\ (((op (op (e0) (e0)) (e3)) = (op (e0) (op (e0) (e3)))) /\ (((op (op (e0) (e1)) (e0)) = (op (e0) (op (e1) (e0)))) /\ (((op (op (e0) (e1)) (e1)) = (op (e0) (op (e1) (e1)))) /\ (((op (op (e0) (e1)) (e2)) = (op (e0) (op (e1) (e2)))) /\ (((op (op (e0) (e1)) (e3)) = (op (e0) (op (e1) (e3)))) /\ (((op (op (e0) (e2)) (e0)) = (op (e0) (op (e2) (e0)))) /\ (((op (op (e0) (e2)) (e1)) = (op (e0) (op (e2) (e1)))) /\ (((op (op (e0) (e2)) (e2)) = (op (e0) (op (e2) (e2)))) /\ (((op (op (e0) (e2)) (e3)) = (op (e0) (op (e2) (e3)))) /\ (((op (op (e0) (e3)) (e0)) = (op (e0) (op (e3) (e0)))) /\ (((op (op (e0) (e3)) (e1)) = (op (e0) (op (e3) (e1)))) /\ (((op (op (e0) (e3)) (e2)) = (op (e0) (op (e3) (e2)))) /\ (((op (op (e0) (e3)) (e3)) = (op (e0) (op (e3) (e3)))) /\ (((op (op (e1) (e0)) (e0)) = (op (e1) (op (e0) (e0)))) /\ (((op (op (e1) (e0)) (e1)) = (op (e1) (op (e0) (e1)))) /\ (((op (op (e1) (e0)) (e2)) = (op (e1) (op (e0) (e2)))) /\ (((op (op (e1) (e0)) (e3)) = (op (e1) (op (e0) (e3)))) /\ (((op (op (e1) (e1)) (e0)) = (op (e1) (op (e1) (e0)))) /\ (((op (op (e1) (e1)) (e1)) = (op (e1) (op (e1) (e1)))) /\ (((op (op (e1) (e1)) (e2)) = (op (e1) (op (e1) (e2)))) /\ (((op (op (e1) (e1)) (e3)) = (op (e1) (op (e1) (e3)))) /\ (((op (op (e1) (e2)) (e0)) = (op (e1) (op (e2) (e0)))) /\ (((op (op (e1) (e2)) (e1)) = (op (e1) (op (e2) (e1)))) /\ (((op (op (e1) (e2)) (e2)) = (op (e1) (op (e2) (e2)))) /\ (((op (op (e1) (e2)) (e3)) = (op (e1) (op (e2) (e3)))) /\ (((op (op (e1) (e3)) (e0)) = (op (e1) (op (e3) (e0)))) /\ (((op (op (e1) (e3)) (e1)) = (op (e1) (op (e3) (e1)))) /\ (((op (op (e1) (e3)) (e2)) = (op (e1) (op (e3) (e2)))) /\ (((op (op (e1) (e3)) (e3)) = (op (e1) (op (e3) (e3)))) /\ (((op (op (e2) (e0)) (e0)) = (op (e2) (op (e0) (e0)))) /\ (((op (op (e2) (e0)) (e1)) = (op (e2) (op (e0) (e1)))) /\ (((op (op (e2) (e0)) (e2)) = (op (e2) (op (e0) (e2)))) /\ (((op (op (e2) (e0)) (e3)) = (op (e2) (op (e0) (e3)))) /\ (((op (op (e2) (e1)) (e0)) = (op (e2) (op (e1) (e0)))) /\ (((op (op (e2) (e1)) (e1)) = (op (e2) (op (e1) (e1)))) /\ (((op (op (e2) (e1)) (e2)) = (op (e2) (op (e1) (e2)))) /\ (((op (op (e2) (e1)) (e3)) = (op (e2) (op (e1) (e3)))) /\ (((op (op (e2) (e2)) (e0)) = (op (e2) (op (e2) (e0)))) /\ (((op (op (e2) (e2)) (e1)) = (op (e2) (op (e2) (e1)))) /\ (((op (op (e2) (e2)) (e2)) = (op (e2) (op (e2) (e2)))) /\ (((op (op (e2) (e2)) (e3)) = (op (e2) (op (e2) (e3)))) /\ (((op (op (e2) (e3)) (e0)) = (op (e2) (op (e3) (e0)))) /\ (((op (op (e2) (e3)) (e1)) = (op (e2) (op (e3) (e1)))) /\ (((op (op (e2) (e3)) (e2)) = (op (e2) (op (e3) (e2)))) /\ (((op (op (e2) (e3)) (e3)) = (op (e2) (op (e3) (e3)))) /\ (((op (op (e3) (e0)) (e0)) = (op (e3) (op (e0) (e0)))) /\ (((op (op (e3) (e0)) (e1)) = (op (e3) (op (e0) (e1)))) /\ (((op (op (e3) (e0)) (e2)) = (op (e3) (op (e0) (e2)))) /\ (((op (op (e3) (e0)) (e3)) = (op (e3) (op (e0) (e3)))) /\ (((op (op (e3) (e1)) (e0)) = (op (e3) (op (e1) (e0)))) /\ (((op (op (e3) (e1)) (e1)) = (op (e3) (op (e1) (e1)))) /\ (((op (op (e3) (e1)) (e2)) = (op (e3) (op (e1) (e2)))) /\ (((op (op (e3) (e1)) (e3)) = (op (e3) (op (e1) (e3)))) /\ (((op (op (e3) (e2)) (e0)) = (op (e3) (op (e2) (e0)))) /\ (((op (op (e3) (e2)) (e1)) = (op (e3) (op (e2) (e1)))) /\ (((op (op (e3) (e2)) (e2)) = (op (e3) (op (e2) (e2)))) /\ (((op (op (e3) (e2)) (e3)) = (op (e3) (op (e2) (e3)))) /\ (((op (op (e3) (e3)) (e0)) = (op (e3) (op (e3) (e0)))) /\ (((op (op (e3) (e3)) (e1)) = (op (e3) (op (e3) (e1)))) /\ (((op (op (e3) (e3)) (e2)) = (op (e3) (op (e3) (e2)))) /\ (((op (op (e3) (e3)) (e3)) = (op (e3) (op (e3) (e3)))) /\ (((op (unit) (e0)) = (e0)) /\ (((op (e0) (unit)) = (e0)) /\ (((op (unit) (e1)) = (e1)) /\ (((op (e1) (unit)) = (e1)) /\ (((op (unit) (e2)) = (e2)) /\ (((op (e2) (unit)) = (e2)) /\ (((op (unit) (e3)) = (e3)) /\ (((op (e3) (unit)) = (e3)) /\ ((((unit) = (e0)) \/ (((unit) = (e1)) \/ (((unit) = (e2)) \/ ((unit) = (e3))))) /\ (((op (e0) (inv (e0))) = (unit)) /\ (((op (inv (e0)) (e0)) = (unit)) /\ (((op (e1) (inv (e1))) = (unit)) /\ (((op (inv (e1)) (e1)) = (unit)) /\ (((op (e2) (inv (e2))) = (unit)) /\ (((op (inv (e2)) (e2)) = (unit)) /\ (((op (e3) (inv (e3))) = (unit)) /\ (((op (inv (e3)) (e3)) = (unit)) /\ ((((inv (e0)) = (e0)) \/ (((inv (e0)) = (e1)) \/ (((inv (e0)) = (e2)) \/ ((inv (e0)) = (e3))))) /\ ((((inv (e1)) = (e0)) \/ (((inv (e1)) = (e1)) \/ (((inv (e1)) = (e2)) \/ ((inv (e1)) = (e3))))) /\ ((((inv (e2)) = (e0)) \/ (((inv (e2)) = (e1)) \/ (((inv (e2)) = (e2)) \/ ((inv (e2)) = (e3))))) /\ (((inv (e3)) = (e0)) \/ (((inv (e3)) = (e1)) \/ (((inv (e3)) = (e2)) \/ ((inv (e3)) = (e3))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ### ConjTree 455 % 1.82/2.02 457. (((op (e0) (e0)) = (e0)) /\ (((op (e0) (e1)) = (e1)) /\ (((op (e0) (e2)) = (e2)) /\ (((op (e0) (e3)) = (e3)) /\ (((op (e1) (e0)) = (e1)) /\ (((op (e1) (e1)) = (e3)) /\ (((op (e1) (e2)) = (e0)) /\ (((op (e1) (e3)) = (e2)) /\ (((op (e2) (e0)) = (e2)) /\ (((op (e2) (e1)) = (e0)) /\ (((op (e2) (e2)) = (e3)) /\ (((op (e2) (e3)) = (e1)) /\ (((op (e3) (e0)) = (e3)) /\ (((op (e3) (e1)) = (e2)) /\ (((op (e3) (e2)) = (e1)) /\ ((op (e3) (e3)) = (e0))))))))))))))))) (-. ((-. ((((op (e0) (e0)) = (e0)) /\ (((op (e1) (e1)) = (e0)) /\ (((op (e2) (e2)) = (e0)) /\ ((op (e3) (e3)) = (e0))))) \/ ((((op (e0) (e0)) = (e1)) /\ (((op (e1) (e1)) = (e1)) /\ (((op (e2) (e2)) = (e1)) /\ ((op (e3) (e3)) = (e1))))) \/ ((((op (e0) (e0)) = (e2)) /\ (((op (e1) (e1)) = (e2)) /\ (((op (e2) (e2)) = (e2)) /\ ((op (e3) (e3)) = (e2))))) \/ (((op (e0) (e0)) = (e3)) /\ (((op (e1) (e1)) = (e3)) /\ (((op (e2) (e2)) = (e3)) /\ ((op (e3) (e3)) = (e3))))))))) /\ ((((op (e0) (e0)) = (e0)) \/ (((op (e0) (e0)) = (e1)) \/ (((op (e0) (e0)) = (e2)) \/ ((op (e0) (e0)) = (e3))))) /\ ((((op (e0) (e1)) = (e0)) \/ (((op (e0) (e1)) = (e1)) \/ (((op (e0) (e1)) = (e2)) \/ ((op (e0) (e1)) = (e3))))) /\ ((((op (e0) (e2)) = (e0)) \/ (((op (e0) (e2)) = (e1)) \/ (((op (e0) (e2)) = (e2)) \/ ((op (e0) (e2)) = (e3))))) /\ ((((op (e0) (e3)) = (e0)) \/ (((op (e0) (e3)) = (e1)) \/ (((op (e0) (e3)) = (e2)) \/ ((op (e0) (e3)) = (e3))))) /\ ((((op (e1) (e0)) = (e0)) \/ (((op (e1) (e0)) = (e1)) \/ (((op (e1) (e0)) = (e2)) \/ ((op (e1) (e0)) = (e3))))) /\ ((((op (e1) (e1)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e1) (e1)) = (e2)) \/ ((op (e1) (e1)) = (e3))))) /\ ((((op (e1) (e2)) = (e0)) \/ (((op (e1) (e2)) = (e1)) \/ (((op (e1) (e2)) = (e2)) \/ ((op (e1) (e2)) = (e3))))) /\ ((((op (e1) (e3)) = (e0)) \/ (((op (e1) (e3)) = (e1)) \/ (((op (e1) (e3)) = (e2)) \/ ((op (e1) (e3)) = (e3))))) /\ ((((op (e2) (e0)) = (e0)) \/ (((op (e2) (e0)) = (e1)) \/ (((op (e2) (e0)) = (e2)) \/ ((op (e2) (e0)) = (e3))))) /\ ((((op (e2) (e1)) = (e0)) \/ (((op (e2) (e1)) = (e1)) \/ (((op (e2) (e1)) = (e2)) \/ ((op (e2) (e1)) = (e3))))) /\ ((((op (e2) (e2)) = (e0)) \/ (((op (e2) (e2)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ ((op (e2) (e2)) = (e3))))) /\ ((((op (e2) (e3)) = (e0)) \/ (((op (e2) (e3)) = (e1)) \/ (((op (e2) (e3)) = (e2)) \/ ((op (e2) (e3)) = (e3))))) /\ ((((op (e3) (e0)) = (e0)) \/ (((op (e3) (e0)) = (e1)) \/ (((op (e3) (e0)) = (e2)) \/ ((op (e3) (e0)) = (e3))))) /\ ((((op (e3) (e1)) = (e0)) \/ (((op (e3) (e1)) = (e1)) \/ (((op (e3) (e1)) = (e2)) \/ ((op (e3) (e1)) = (e3))))) /\ ((((op (e3) (e2)) = (e0)) \/ (((op (e3) (e2)) = (e1)) \/ (((op (e3) (e2)) = (e2)) \/ ((op (e3) (e2)) = (e3))))) /\ ((((op (e3) (e3)) = (e0)) \/ (((op (e3) (e3)) = (e1)) \/ (((op (e3) (e3)) = (e2)) \/ ((op (e3) (e3)) = (e3))))) /\ (((op (op (e0) (e0)) (e0)) = (op (e0) (op (e0) (e0)))) /\ (((op (op (e0) (e0)) (e1)) = (op (e0) (op (e0) (e1)))) /\ (((op (op (e0) (e0)) (e2)) = (op (e0) (op (e0) (e2)))) /\ (((op (op (e0) (e0)) (e3)) = (op (e0) (op (e0) (e3)))) /\ (((op (op (e0) (e1)) (e0)) = (op (e0) (op (e1) (e0)))) /\ (((op (op (e0) (e1)) (e1)) = (op (e0) (op (e1) (e1)))) /\ (((op (op (e0) (e1)) (e2)) = (op (e0) (op (e1) (e2)))) /\ (((op (op (e0) (e1)) (e3)) = (op (e0) (op (e1) (e3)))) /\ (((op (op (e0) (e2)) (e0)) = (op (e0) (op (e2) (e0)))) /\ (((op (op (e0) (e2)) (e1)) = (op (e0) (op (e2) (e1)))) /\ (((op (op (e0) (e2)) (e2)) = (op (e0) (op (e2) (e2)))) /\ (((op (op (e0) (e2)) (e3)) = (op (e0) (op (e2) (e3)))) /\ (((op (op (e0) (e3)) (e0)) = (op (e0) (op (e3) (e0)))) /\ (((op (op (e0) (e3)) (e1)) = (op (e0) (op (e3) (e1)))) /\ (((op (op (e0) (e3)) (e2)) = (op (e0) (op (e3) (e2)))) /\ (((op (op (e0) (e3)) (e3)) = (op (e0) (op (e3) (e3)))) /\ (((op (op (e1) (e0)) (e0)) = (op (e1) (op (e0) (e0)))) /\ (((op (op (e1) (e0)) (e1)) = (op (e1) (op (e0) (e1)))) /\ (((op (op (e1) (e0)) (e2)) = (op (e1) (op (e0) (e2)))) /\ (((op (op (e1) (e0)) (e3)) = (op (e1) (op (e0) (e3)))) /\ (((op (op (e1) (e1)) (e0)) = (op (e1) (op (e1) (e0)))) /\ (((op (op (e1) (e1)) (e1)) = (op (e1) (op (e1) (e1)))) /\ (((op (op (e1) (e1)) (e2)) = (op (e1) (op (e1) (e2)))) /\ (((op (op (e1) (e1)) (e3)) = (op (e1) (op (e1) (e3)))) /\ (((op (op (e1) (e2)) (e0)) = (op (e1) (op (e2) (e0)))) /\ (((op (op (e1) (e2)) (e1)) = (op (e1) (op (e2) (e1)))) /\ (((op (op (e1) (e2)) (e2)) = (op (e1) (op (e2) (e2)))) /\ (((op (op (e1) (e2)) (e3)) = (op (e1) (op (e2) (e3)))) /\ (((op (op (e1) (e3)) (e0)) = (op (e1) (op (e3) (e0)))) /\ (((op (op (e1) (e3)) (e1)) = (op (e1) (op (e3) (e1)))) /\ (((op (op (e1) (e3)) (e2)) = (op (e1) (op (e3) (e2)))) /\ (((op (op (e1) (e3)) (e3)) = (op (e1) (op (e3) (e3)))) /\ (((op (op (e2) (e0)) (e0)) = (op (e2) (op (e0) (e0)))) /\ (((op (op (e2) (e0)) (e1)) = (op (e2) (op (e0) (e1)))) /\ (((op (op (e2) (e0)) (e2)) = (op (e2) (op (e0) (e2)))) /\ (((op (op (e2) (e0)) (e3)) = (op (e2) (op (e0) (e3)))) /\ (((op (op (e2) (e1)) (e0)) = (op (e2) (op (e1) (e0)))) /\ (((op (op (e2) (e1)) (e1)) = (op (e2) (op (e1) (e1)))) /\ (((op (op (e2) (e1)) (e2)) = (op (e2) (op (e1) (e2)))) /\ (((op (op (e2) (e1)) (e3)) = (op (e2) (op (e1) (e3)))) /\ (((op (op (e2) (e2)) (e0)) = (op (e2) (op (e2) (e0)))) /\ (((op (op (e2) (e2)) (e1)) = (op (e2) (op (e2) (e1)))) /\ (((op (op (e2) (e2)) (e2)) = (op (e2) (op (e2) (e2)))) /\ (((op (op (e2) (e2)) (e3)) = (op (e2) (op (e2) (e3)))) /\ (((op (op (e2) (e3)) (e0)) = (op (e2) (op (e3) (e0)))) /\ (((op (op (e2) (e3)) (e1)) = (op (e2) (op (e3) (e1)))) /\ (((op (op (e2) (e3)) (e2)) = (op (e2) (op (e3) (e2)))) /\ (((op (op (e2) (e3)) (e3)) = (op (e2) (op (e3) (e3)))) /\ (((op (op (e3) (e0)) (e0)) = (op (e3) (op (e0) (e0)))) /\ (((op (op (e3) (e0)) (e1)) = (op (e3) (op (e0) (e1)))) /\ (((op (op (e3) (e0)) (e2)) = (op (e3) (op (e0) (e2)))) /\ (((op (op (e3) (e0)) (e3)) = (op (e3) (op (e0) (e3)))) /\ (((op (op (e3) (e1)) (e0)) = (op (e3) (op (e1) (e0)))) /\ (((op (op (e3) (e1)) (e1)) = (op (e3) (op (e1) (e1)))) /\ (((op (op (e3) (e1)) (e2)) = (op (e3) (op (e1) (e2)))) /\ (((op (op (e3) (e1)) (e3)) = (op (e3) (op (e1) (e3)))) /\ (((op (op (e3) (e2)) (e0)) = (op (e3) (op (e2) (e0)))) /\ (((op (op (e3) (e2)) (e1)) = (op (e3) (op (e2) (e1)))) /\ (((op (op (e3) (e2)) (e2)) = (op (e3) (op (e2) (e2)))) /\ (((op (op (e3) (e2)) (e3)) = (op (e3) (op (e2) (e3)))) /\ (((op (op (e3) (e3)) (e0)) = (op (e3) (op (e3) (e0)))) /\ (((op (op (e3) (e3)) (e1)) = (op (e3) (op (e3) (e1)))) /\ (((op (op (e3) (e3)) (e2)) = (op (e3) (op (e3) (e2)))) /\ (((op (op (e3) (e3)) (e3)) = (op (e3) (op (e3) (e3)))) /\ (((op (unit) (e0)) = (e0)) /\ (((op (e0) (unit)) = (e0)) /\ (((op (unit) (e1)) = (e1)) /\ (((op (e1) (unit)) = (e1)) /\ (((op (unit) (e2)) = (e2)) /\ (((op (e2) (unit)) = (e2)) /\ (((op (unit) (e3)) = (e3)) /\ (((op (e3) (unit)) = (e3)) /\ ((((unit) = (e0)) \/ (((unit) = (e1)) \/ (((unit) = (e2)) \/ ((unit) = (e3))))) /\ (((op (e0) (inv (e0))) = (unit)) /\ (((op (inv (e0)) (e0)) = (unit)) /\ (((op (e1) (inv (e1))) = (unit)) /\ (((op (inv (e1)) (e1)) = (unit)) /\ (((op (e2) (inv (e2))) = (unit)) /\ (((op (inv (e2)) (e2)) = (unit)) /\ (((op (e3) (inv (e3))) = (unit)) /\ (((op (inv (e3)) (e3)) = (unit)) /\ ((((inv (e0)) = (e0)) \/ (((inv (e0)) = (e1)) \/ (((inv (e0)) = (e2)) \/ ((inv (e0)) = (e3))))) /\ ((((inv (e1)) = (e0)) \/ (((inv (e1)) = (e1)) \/ (((inv (e1)) = (e2)) \/ ((inv (e1)) = (e3))))) /\ ((((inv (e2)) = (e0)) \/ (((inv (e2)) = (e1)) \/ (((inv (e2)) = (e2)) \/ ((inv (e2)) = (e3))))) /\ (((inv (e3)) = (e0)) \/ (((inv (e3)) = (e1)) \/ (((inv (e3)) = (e2)) \/ ((inv (e3)) = (e3))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ((unit) = (e0)) ((e0) != (e2)) ((e0) != (e1)) ((e0) != (e3)) (((inv (e0)) = (e0)) /\ (((inv (e1)) = (e2)) /\ (((inv (e2)) = (e1)) /\ ((inv (e3)) = (e3))))) ### ConjTree 456 % 1.82/2.02 458. (((e0) != (e1)) /\ (((e0) != (e2)) /\ (((e0) != (e3)) /\ (((e1) != (e2)) /\ (((e1) != (e3)) /\ ((e2) != (e3))))))) (((inv (e0)) = (e0)) /\ (((inv (e1)) = (e2)) /\ (((inv (e2)) = (e1)) /\ ((inv (e3)) = (e3))))) ((unit) = (e0)) (-. ((-. ((((op (e0) (e0)) = (e0)) /\ (((op (e1) (e1)) = (e0)) /\ (((op (e2) (e2)) = (e0)) /\ ((op (e3) (e3)) = (e0))))) \/ ((((op (e0) (e0)) = (e1)) /\ (((op (e1) (e1)) = (e1)) /\ (((op (e2) (e2)) = (e1)) /\ ((op (e3) (e3)) = (e1))))) \/ ((((op (e0) (e0)) = (e2)) /\ (((op (e1) (e1)) = (e2)) /\ (((op (e2) (e2)) = (e2)) /\ ((op (e3) (e3)) = (e2))))) \/ (((op (e0) (e0)) = (e3)) /\ (((op (e1) (e1)) = (e3)) /\ (((op (e2) (e2)) = (e3)) /\ ((op (e3) (e3)) = (e3))))))))) /\ ((((op (e0) (e0)) = (e0)) \/ (((op (e0) (e0)) = (e1)) \/ (((op (e0) (e0)) = (e2)) \/ ((op (e0) (e0)) = (e3))))) /\ ((((op (e0) (e1)) = (e0)) \/ (((op (e0) (e1)) = (e1)) \/ (((op (e0) (e1)) = (e2)) \/ ((op (e0) (e1)) = (e3))))) /\ ((((op (e0) (e2)) = (e0)) \/ (((op (e0) (e2)) = (e1)) \/ (((op (e0) (e2)) = (e2)) \/ ((op (e0) (e2)) = (e3))))) /\ ((((op (e0) (e3)) = (e0)) \/ (((op (e0) (e3)) = (e1)) \/ (((op (e0) (e3)) = (e2)) \/ ((op (e0) (e3)) = (e3))))) /\ ((((op (e1) (e0)) = (e0)) \/ (((op (e1) (e0)) = (e1)) \/ (((op (e1) (e0)) = (e2)) \/ ((op (e1) (e0)) = (e3))))) /\ ((((op (e1) (e1)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e1) (e1)) = (e2)) \/ ((op (e1) (e1)) = (e3))))) /\ ((((op (e1) (e2)) = (e0)) \/ (((op (e1) (e2)) = (e1)) \/ (((op (e1) (e2)) = (e2)) \/ ((op (e1) (e2)) = (e3))))) /\ ((((op (e1) (e3)) = (e0)) \/ (((op (e1) (e3)) = (e1)) \/ (((op (e1) (e3)) = (e2)) \/ ((op (e1) (e3)) = (e3))))) /\ ((((op (e2) (e0)) = (e0)) \/ (((op (e2) (e0)) = (e1)) \/ (((op (e2) (e0)) = (e2)) \/ ((op (e2) (e0)) = (e3))))) /\ ((((op (e2) (e1)) = (e0)) \/ (((op (e2) (e1)) = (e1)) \/ (((op (e2) (e1)) = (e2)) \/ ((op (e2) (e1)) = (e3))))) /\ ((((op (e2) (e2)) = (e0)) \/ (((op (e2) (e2)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ ((op (e2) (e2)) = (e3))))) /\ ((((op (e2) (e3)) = (e0)) \/ (((op (e2) (e3)) = (e1)) \/ (((op (e2) (e3)) = (e2)) \/ ((op (e2) (e3)) = (e3))))) /\ ((((op (e3) (e0)) = (e0)) \/ (((op (e3) (e0)) = (e1)) \/ (((op (e3) (e0)) = (e2)) \/ ((op (e3) (e0)) = (e3))))) /\ ((((op (e3) (e1)) = (e0)) \/ (((op (e3) (e1)) = (e1)) \/ (((op (e3) (e1)) = (e2)) \/ ((op (e3) (e1)) = (e3))))) /\ ((((op (e3) (e2)) = (e0)) \/ (((op (e3) (e2)) = (e1)) \/ (((op (e3) (e2)) = (e2)) \/ ((op (e3) (e2)) = (e3))))) /\ ((((op (e3) (e3)) = (e0)) \/ (((op (e3) (e3)) = (e1)) \/ (((op (e3) (e3)) = (e2)) \/ ((op (e3) (e3)) = (e3))))) /\ (((op (op (e0) (e0)) (e0)) = (op (e0) (op (e0) (e0)))) /\ (((op (op (e0) (e0)) (e1)) = (op (e0) (op (e0) (e1)))) /\ (((op (op (e0) (e0)) (e2)) = (op (e0) (op (e0) (e2)))) /\ (((op (op (e0) (e0)) (e3)) = (op (e0) (op (e0) (e3)))) /\ (((op (op (e0) (e1)) (e0)) = (op (e0) (op (e1) (e0)))) /\ (((op (op (e0) (e1)) (e1)) = (op (e0) (op (e1) (e1)))) /\ (((op (op (e0) (e1)) (e2)) = (op (e0) (op (e1) (e2)))) /\ (((op (op (e0) (e1)) (e3)) = (op (e0) (op (e1) (e3)))) /\ (((op (op (e0) (e2)) (e0)) = (op (e0) (op (e2) (e0)))) /\ (((op (op (e0) (e2)) (e1)) = (op (e0) (op (e2) (e1)))) /\ (((op (op (e0) (e2)) (e2)) = (op (e0) (op (e2) (e2)))) /\ (((op (op (e0) (e2)) (e3)) = (op (e0) (op (e2) (e3)))) /\ (((op (op (e0) (e3)) (e0)) = (op (e0) (op (e3) (e0)))) /\ (((op (op (e0) (e3)) (e1)) = (op (e0) (op (e3) (e1)))) /\ (((op (op (e0) (e3)) (e2)) = (op (e0) (op (e3) (e2)))) /\ (((op (op (e0) (e3)) (e3)) = (op (e0) (op (e3) (e3)))) /\ (((op (op (e1) (e0)) (e0)) = (op (e1) (op (e0) (e0)))) /\ (((op (op (e1) (e0)) (e1)) = (op (e1) (op (e0) (e1)))) /\ (((op (op (e1) (e0)) (e2)) = (op (e1) (op (e0) (e2)))) /\ (((op (op (e1) (e0)) (e3)) = (op (e1) (op (e0) (e3)))) /\ (((op (op (e1) (e1)) (e0)) = (op (e1) (op (e1) (e0)))) /\ (((op (op (e1) (e1)) (e1)) = (op (e1) (op (e1) (e1)))) /\ (((op (op (e1) (e1)) (e2)) = (op (e1) (op (e1) (e2)))) /\ (((op (op (e1) (e1)) (e3)) = (op (e1) (op (e1) (e3)))) /\ (((op (op (e1) (e2)) (e0)) = (op (e1) (op (e2) (e0)))) /\ (((op (op (e1) (e2)) (e1)) = (op (e1) (op (e2) (e1)))) /\ (((op (op (e1) (e2)) (e2)) = (op (e1) (op (e2) (e2)))) /\ (((op (op (e1) (e2)) (e3)) = (op (e1) (op (e2) (e3)))) /\ (((op (op (e1) (e3)) (e0)) = (op (e1) (op (e3) (e0)))) /\ (((op (op (e1) (e3)) (e1)) = (op (e1) (op (e3) (e1)))) /\ (((op (op (e1) (e3)) (e2)) = (op (e1) (op (e3) (e2)))) /\ (((op (op (e1) (e3)) (e3)) = (op (e1) (op (e3) (e3)))) /\ (((op (op (e2) (e0)) (e0)) = (op (e2) (op (e0) (e0)))) /\ (((op (op (e2) (e0)) (e1)) = (op (e2) (op (e0) (e1)))) /\ (((op (op (e2) (e0)) (e2)) = (op (e2) (op (e0) (e2)))) /\ (((op (op (e2) (e0)) (e3)) = (op (e2) (op (e0) (e3)))) /\ (((op (op (e2) (e1)) (e0)) = (op (e2) (op (e1) (e0)))) /\ (((op (op (e2) (e1)) (e1)) = (op (e2) (op (e1) (e1)))) /\ (((op (op (e2) (e1)) (e2)) = (op (e2) (op (e1) (e2)))) /\ (((op (op (e2) (e1)) (e3)) = (op (e2) (op (e1) (e3)))) /\ (((op (op (e2) (e2)) (e0)) = (op (e2) (op (e2) (e0)))) /\ (((op (op (e2) (e2)) (e1)) = (op (e2) (op (e2) (e1)))) /\ (((op (op (e2) (e2)) (e2)) = (op (e2) (op (e2) (e2)))) /\ (((op (op (e2) (e2)) (e3)) = (op (e2) (op (e2) (e3)))) /\ (((op (op (e2) (e3)) (e0)) = (op (e2) (op (e3) (e0)))) /\ (((op (op (e2) (e3)) (e1)) = (op (e2) (op (e3) (e1)))) /\ (((op (op (e2) (e3)) (e2)) = (op (e2) (op (e3) (e2)))) /\ (((op (op (e2) (e3)) (e3)) = (op (e2) (op (e3) (e3)))) /\ (((op (op (e3) (e0)) (e0)) = (op (e3) (op (e0) (e0)))) /\ (((op (op (e3) (e0)) (e1)) = (op (e3) (op (e0) (e1)))) /\ (((op (op (e3) (e0)) (e2)) = (op (e3) (op (e0) (e2)))) /\ (((op (op (e3) (e0)) (e3)) = (op (e3) (op (e0) (e3)))) /\ (((op (op (e3) (e1)) (e0)) = (op (e3) (op (e1) (e0)))) /\ (((op (op (e3) (e1)) (e1)) = (op (e3) (op (e1) (e1)))) /\ (((op (op (e3) (e1)) (e2)) = (op (e3) (op (e1) (e2)))) /\ (((op (op (e3) (e1)) (e3)) = (op (e3) (op (e1) (e3)))) /\ (((op (op (e3) (e2)) (e0)) = (op (e3) (op (e2) (e0)))) /\ (((op (op (e3) (e2)) (e1)) = (op (e3) (op (e2) (e1)))) /\ (((op (op (e3) (e2)) (e2)) = (op (e3) (op (e2) (e2)))) /\ (((op (op (e3) (e2)) (e3)) = (op (e3) (op (e2) (e3)))) /\ (((op (op (e3) (e3)) (e0)) = (op (e3) (op (e3) (e0)))) /\ (((op (op (e3) (e3)) (e1)) = (op (e3) (op (e3) (e1)))) /\ (((op (op (e3) (e3)) (e2)) = (op (e3) (op (e3) (e2)))) /\ (((op (op (e3) (e3)) (e3)) = (op (e3) (op (e3) (e3)))) /\ (((op (unit) (e0)) = (e0)) /\ (((op (e0) (unit)) = (e0)) /\ (((op (unit) (e1)) = (e1)) /\ (((op (e1) (unit)) = (e1)) /\ (((op (unit) (e2)) = (e2)) /\ (((op (e2) (unit)) = (e2)) /\ (((op (unit) (e3)) = (e3)) /\ (((op (e3) (unit)) = (e3)) /\ ((((unit) = (e0)) \/ (((unit) = (e1)) \/ (((unit) = (e2)) \/ ((unit) = (e3))))) /\ (((op (e0) (inv (e0))) = (unit)) /\ (((op (inv (e0)) (e0)) = (unit)) /\ (((op (e1) (inv (e1))) = (unit)) /\ (((op (inv (e1)) (e1)) = (unit)) /\ (((op (e2) (inv (e2))) = (unit)) /\ (((op (inv (e2)) (e2)) = (unit)) /\ (((op (e3) (inv (e3))) = (unit)) /\ (((op (inv (e3)) (e3)) = (unit)) /\ ((((inv (e0)) = (e0)) \/ (((inv (e0)) = (e1)) \/ (((inv (e0)) = (e2)) \/ ((inv (e0)) = (e3))))) /\ ((((inv (e1)) = (e0)) \/ (((inv (e1)) = (e1)) \/ (((inv (e1)) = (e2)) \/ ((inv (e1)) = (e3))))) /\ ((((inv (e2)) = (e0)) \/ (((inv (e2)) = (e1)) \/ (((inv (e2)) = (e2)) \/ ((inv (e2)) = (e3))))) /\ (((inv (e3)) = (e0)) \/ (((inv (e3)) = (e1)) \/ (((inv (e3)) = (e2)) \/ ((inv (e3)) = (e3))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (((op (e0) (e0)) = (e0)) /\ (((op (e0) (e1)) = (e1)) /\ (((op (e0) (e2)) = (e2)) /\ (((op (e0) (e3)) = (e3)) /\ (((op (e1) (e0)) = (e1)) /\ (((op (e1) (e1)) = (e3)) /\ (((op (e1) (e2)) = (e0)) /\ (((op (e1) (e3)) = (e2)) /\ (((op (e2) (e0)) = (e2)) /\ (((op (e2) (e1)) = (e0)) /\ (((op (e2) (e2)) = (e3)) /\ (((op (e2) (e3)) = (e1)) /\ (((op (e3) (e0)) = (e3)) /\ (((op (e3) (e1)) = (e2)) /\ (((op (e3) (e2)) = (e1)) /\ ((op (e3) (e3)) = (e0))))))))))))))))) ### ConjTree 457 % 1.82/2.02 % SZS output end Proof % 1.82/2.02 (* END-PROOF *) %------------------------------------------------------------------------------