%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : ALG054+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 : n017.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:54 EDT 2022 % Result : Theorem 16.80s 16.98s % Output : Proof 16.80s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : ALG054+1 : TPTP v8.1.0. Released v2.7.0. % 0.06/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n017.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Thu Jun 9 02:31:48 EDT 2022 % 0.12/0.33 % CPUTime : % 16.80/16.98 % SZS status Theorem % 16.80/16.98 (* PROOF-FOUND *) % 16.80/16.98 (* BEGIN-PROOF *) % 16.80/16.98 % SZS output start Proof % 16.80/16.98 1. ((op (e0) (e0)) = (e3)) ((op (e0) (e0)) != (e3)) ### Axiom % 16.80/16.98 2. ((e4) = (op (e1) (e1))) ((op (e1) (e1)) != (e4)) ### Sym(=) % 16.80/16.98 3. ((e1) != (e1)) ### NotEqual % 16.80/16.98 4. ((unit) = (e0)) ((e0) != (unit)) ### Sym(=) % 16.80/16.98 5. ((op (e1) (e0)) != (op (e1) (unit))) ((unit) = (e0)) ### NotEqual 3 4 % 16.80/16.98 6. ((op (e1) (e4)) = (e1)) ((e1) != (op (e1) (e4))) ### Sym(=) % 16.80/16.98 7. ((op (e1) (e0)) != (op (e1) (e4))) ((op (e1) (unit)) = (e1)) ((op (e1) (e4)) = (e1)) ((unit) = (e0)) ### Trans 5 6 % 16.80/16.98 8. ((unit) = (e1)) ((e1) != (unit)) ### Sym(=) % 16.80/16.98 9. ((op (e1) (e1)) != (op (unit) (e1))) ((unit) = (e1)) ### NotEqual 8 3 % 16.80/16.98 10. ((op (e1) (e4)) = (e1)) ((e1) != (op (e1) (e4))) ### Sym(=) % 16.80/16.98 11. ((op (e1) (e1)) != (op (e1) (e4))) ((op (unit) (e1)) = (e1)) ((op (e1) (e4)) = (e1)) ((unit) = (e1)) ### Trans 9 10 % 16.80/16.98 12. ((unit) = (e2)) ((e2) != (unit)) ### Sym(=) % 16.80/16.98 13. ((op (e1) (e2)) != (op (e1) (unit))) ((unit) = (e2)) ### NotEqual 3 12 % 16.80/16.98 14. ((op (e1) (e4)) = (e1)) ((e1) != (op (e1) (e4))) ### Sym(=) % 16.80/16.98 15. ((op (e1) (e2)) != (op (e1) (e4))) ((op (e1) (unit)) = (e1)) ((op (e1) (e4)) = (e1)) ((unit) = (e2)) ### Trans 13 14 % 16.80/16.98 16. ((unit) = (e3)) ((e3) != (unit)) ### Sym(=) % 16.80/16.98 17. ((op (e1) (e3)) != (op (e1) (unit))) ((unit) = (e3)) ### NotEqual 3 16 % 16.80/16.98 18. ((op (e1) (e4)) = (e1)) ((e1) != (op (e1) (e4))) ### Sym(=) % 16.80/16.98 19. ((op (e1) (e3)) != (op (e1) (e4))) ((op (e1) (unit)) = (e1)) ((op (e1) (e4)) = (e1)) ((unit) = (e3)) ### Trans 17 18 % 16.80/16.98 20. ((e0) != (e0)) ### NotEqual % 16.80/16.98 21. ((unit) = (e4)) ((e4) != (unit)) ### Sym(=) % 16.80/16.98 22. ((op (e0) (e4)) != (op (e0) (unit))) ((unit) = (e4)) ### NotEqual 20 21 % 16.80/16.98 23. ((op (e0) (e3)) = (e0)) ((e0) != (op (e0) (e3))) ### Sym(=) % 16.80/16.98 24. ((op (e0) (e3)) != (op (e0) (e4))) ((op (e0) (unit)) = (e0)) ((op (e0) (e3)) = (e0)) ((unit) = (e4)) ### Trans-sym 22 23 % 16.80/16.98 25. (((unit) = (e0)) \/ (((unit) = (e1)) \/ (((unit) = (e2)) \/ (((unit) = (e3)) \/ ((unit) = (e4)))))) ((op (e0) (e3)) = (e0)) ((op (e0) (unit)) = (e0)) ((op (e0) (e3)) != (op (e0) (e4))) ((op (e1) (e3)) != (op (e1) (e4))) ((op (e1) (e2)) != (op (e1) (e4))) ((op (unit) (e1)) = (e1)) ((op (e1) (e1)) != (op (e1) (e4))) ((op (e1) (e4)) = (e1)) ((op (e1) (unit)) = (e1)) ((op (e1) (e0)) != (op (e1) (e4))) ### DisjTree 7 11 15 19 24 % 16.80/16.98 26. (((op (e1) (e1)) != (e4)) \/ ((op (e1) (e4)) = (e1))) ((op (e1) (e0)) != (op (e1) (e4))) ((op (e1) (unit)) = (e1)) ((op (e1) (e1)) != (op (e1) (e4))) ((op (unit) (e1)) = (e1)) ((op (e1) (e2)) != (op (e1) (e4))) ((op (e1) (e3)) != (op (e1) (e4))) ((op (e0) (e3)) != (op (e0) (e4))) ((op (e0) (unit)) = (e0)) ((op (e0) (e3)) = (e0)) (((unit) = (e0)) \/ (((unit) = (e1)) \/ (((unit) = (e2)) \/ (((unit) = (e3)) \/ ((unit) = (e4)))))) ((e4) = (op (e1) (e1))) ### Or 2 25 % 16.80/16.98 27. (((op (e0) (e0)) != (e3)) \/ ((op (e0) (e3)) = (e0))) ((e4) = (op (e1) (e1))) (((unit) = (e0)) \/ (((unit) = (e1)) \/ (((unit) = (e2)) \/ (((unit) = (e3)) \/ ((unit) = (e4)))))) ((op (e0) (unit)) = (e0)) ((op (e0) (e3)) != (op (e0) (e4))) ((op (e1) (e3)) != (op (e1) (e4))) ((op (e1) (e2)) != (op (e1) (e4))) ((op (unit) (e1)) = (e1)) ((op (e1) (e1)) != (op (e1) (e4))) ((op (e1) (unit)) = (e1)) ((op (e1) (e0)) != (op (e1) (e4))) (((op (e1) (e1)) != (e4)) \/ ((op (e1) (e4)) = (e1))) ((op (e0) (e0)) = (e3)) ### Or 1 26 % 16.80/16.98 28. ((op (e1) (e1)) = (e3)) ((op (e1) (e1)) != (e3)) ### Axiom % 16.80/16.98 29. ((e4) = (op (e1) (e1))) ((op (e1) (e1)) != (e4)) ### Sym(=) % 16.80/16.98 30. ((unit) = (e4)) ((e4) != (unit)) ### Sym(=) % 16.80/16.98 31. ((op (e1) (e4)) != (op (e1) (unit))) ((unit) = (e4)) ### NotEqual 3 30 % 16.80/16.98 32. ((op (e1) (e3)) = (e1)) ((e1) != (op (e1) (e3))) ### Sym(=) % 16.80/16.98 33. ((op (e1) (e3)) != (op (e1) (e4))) ((op (e1) (unit)) = (e1)) ((op (e1) (e3)) = (e1)) ((unit) = (e4)) ### Trans-sym 31 32 % 16.80/16.98 34. (((unit) = (e0)) \/ (((unit) = (e1)) \/ (((unit) = (e2)) \/ (((unit) = (e3)) \/ ((unit) = (e4)))))) ((op (e1) (e3)) = (e1)) ((op (e1) (e3)) != (op (e1) (e4))) ((op (e1) (e2)) != (op (e1) (e4))) ((op (unit) (e1)) = (e1)) ((op (e1) (e1)) != (op (e1) (e4))) ((op (e1) (e4)) = (e1)) ((op (e1) (unit)) = (e1)) ((op (e1) (e0)) != (op (e1) (e4))) ### DisjTree 7 11 15 19 33 % 16.80/16.98 35. (((op (e1) (e1)) != (e4)) \/ ((op (e1) (e4)) = (e1))) ((op (e1) (e0)) != (op (e1) (e4))) ((op (e1) (unit)) = (e1)) ((op (e1) (e1)) != (op (e1) (e4))) ((op (unit) (e1)) = (e1)) ((op (e1) (e2)) != (op (e1) (e4))) ((op (e1) (e3)) != (op (e1) (e4))) ((op (e1) (e3)) = (e1)) (((unit) = (e0)) \/ (((unit) = (e1)) \/ (((unit) = (e2)) \/ (((unit) = (e3)) \/ ((unit) = (e4)))))) ((e4) = (op (e1) (e1))) ### Or 29 34 % 16.80/16.98 36. (((op (e1) (e1)) != (e3)) \/ ((op (e1) (e3)) = (e1))) ((e4) = (op (e1) (e1))) (((unit) = (e0)) \/ (((unit) = (e1)) \/ (((unit) = (e2)) \/ (((unit) = (e3)) \/ ((unit) = (e4)))))) ((op (e1) (e3)) != (op (e1) (e4))) ((op (e1) (e2)) != (op (e1) (e4))) ((op (unit) (e1)) = (e1)) ((op (e1) (e1)) != (op (e1) (e4))) ((op (e1) (unit)) = (e1)) ((op (e1) (e0)) != (op (e1) (e4))) (((op (e1) (e1)) != (e4)) \/ ((op (e1) (e4)) = (e1))) ((op (e1) (e1)) = (e3)) ### Or 28 35 % 16.80/16.98 37. ((e4) = (op (e1) (e1))) ((op (e1) (e1)) != (e4)) ### Sym(=) % 16.80/16.98 38. ((op (e2) (e2)) = (e3)) ((op (e2) (e2)) != (e3)) ### Axiom % 16.80/16.98 39. ((e2) != (e2)) ### NotEqual % 16.80/16.98 40. ((unit) = (e4)) ((e4) != (unit)) ### Sym(=) % 16.80/16.98 41. ((op (e2) (e4)) != (op (e2) (unit))) ((unit) = (e4)) ### NotEqual 39 40 % 16.80/16.98 42. ((op (e2) (e3)) = (e2)) ((e2) != (op (e2) (e3))) ### Sym(=) % 16.80/16.98 43. ((op (e2) (e3)) != (op (e2) (e4))) ((op (e2) (unit)) = (e2)) ((op (e2) (e3)) = (e2)) ((unit) = (e4)) ### Trans-sym 41 42 % 16.80/16.98 44. (((unit) = (e0)) \/ (((unit) = (e1)) \/ (((unit) = (e2)) \/ (((unit) = (e3)) \/ ((unit) = (e4)))))) ((op (e2) (e3)) = (e2)) ((op (e2) (unit)) = (e2)) ((op (e2) (e3)) != (op (e2) (e4))) ((op (e1) (e3)) != (op (e1) (e4))) ((op (e1) (e2)) != (op (e1) (e4))) ((op (unit) (e1)) = (e1)) ((op (e1) (e1)) != (op (e1) (e4))) ((op (e1) (e4)) = (e1)) ((op (e1) (unit)) = (e1)) ((op (e1) (e0)) != (op (e1) (e4))) ### DisjTree 7 11 15 19 43 % 16.80/16.98 45. (((op (e2) (e2)) != (e3)) \/ ((op (e2) (e3)) = (e2))) ((op (e1) (e0)) != (op (e1) (e4))) ((op (e1) (unit)) = (e1)) ((op (e1) (e4)) = (e1)) ((op (e1) (e1)) != (op (e1) (e4))) ((op (unit) (e1)) = (e1)) ((op (e1) (e2)) != (op (e1) (e4))) ((op (e1) (e3)) != (op (e1) (e4))) ((op (e2) (e3)) != (op (e2) (e4))) ((op (e2) (unit)) = (e2)) (((unit) = (e0)) \/ (((unit) = (e1)) \/ (((unit) = (e2)) \/ (((unit) = (e3)) \/ ((unit) = (e4)))))) ((op (e2) (e2)) = (e3)) ### Or 38 44 % 16.80/16.98 46. (((op (e1) (e1)) != (e4)) \/ ((op (e1) (e4)) = (e1))) ((op (e2) (e2)) = (e3)) (((unit) = (e0)) \/ (((unit) = (e1)) \/ (((unit) = (e2)) \/ (((unit) = (e3)) \/ ((unit) = (e4)))))) ((op (e2) (unit)) = (e2)) ((op (e2) (e3)) != (op (e2) (e4))) ((op (e1) (e3)) != (op (e1) (e4))) ((op (e1) (e2)) != (op (e1) (e4))) ((op (unit) (e1)) = (e1)) ((op (e1) (e1)) != (op (e1) (e4))) ((op (e1) (unit)) = (e1)) ((op (e1) (e0)) != (op (e1) (e4))) (((op (e2) (e2)) != (e3)) \/ ((op (e2) (e3)) = (e2))) ((e4) = (op (e1) (e1))) ### Or 37 45 % 16.80/16.98 47. ((e4) = (op (e1) (e1))) ((op (e1) (e1)) != (e4)) ### Sym(=) % 16.80/16.98 48. ((e3) != (e3)) ### NotEqual % 16.80/16.98 49. ((unit) = (e0)) ((e0) != (unit)) ### Sym(=) % 16.80/16.98 50. ((op (e3) (e0)) != (op (e3) (unit))) ((unit) = (e0)) ### NotEqual 48 49 % 16.80/16.98 51. ((op (e3) (e3)) = (e3)) ((e3) != (op (e3) (e3))) ### Sym(=) % 16.80/16.98 52. ((op (e3) (e0)) != (op (e3) (e3))) ((op (e3) (unit)) = (e3)) ((op (e3) (e3)) = (e3)) ((unit) = (e0)) ### Trans 50 51 % 16.80/16.98 53. ((unit) = (e1)) ((e1) != (unit)) ### Sym(=) % 16.80/16.98 54. ((op (e3) (e1)) != (op (e3) (unit))) ((unit) = (e1)) ### NotEqual 48 53 % 16.80/16.98 55. ((op (e3) (e3)) = (e3)) ((e3) != (op (e3) (e3))) ### Sym(=) % 16.80/16.98 56. ((op (e3) (e1)) != (op (e3) (e3))) ((op (e3) (unit)) = (e3)) ((op (e3) (e3)) = (e3)) ((unit) = (e1)) ### Trans 54 55 % 16.80/16.98 57. ((unit) = (e2)) ((e2) != (unit)) ### Sym(=) % 16.80/16.98 58. ((op (e3) (e2)) != (op (e3) (unit))) ((unit) = (e2)) ### NotEqual 48 57 % 16.80/16.98 59. ((op (e3) (e3)) = (e3)) ((e3) != (op (e3) (e3))) ### Sym(=) % 16.80/16.98 60. ((op (e3) (e2)) != (op (e3) (e3))) ((op (e3) (unit)) = (e3)) ((op (e3) (e3)) = (e3)) ((unit) = (e2)) ### Trans 58 59 % 16.80/16.98 61. ((unit) = (e4)) ((e4) != (unit)) ### Sym(=) % 16.80/16.98 62. ((op (e3) (e4)) != (op (e3) (unit))) ((unit) = (e4)) ### NotEqual 48 61 % 16.80/16.98 63. ((op (e3) (e3)) = (e3)) ((e3) != (op (e3) (e3))) ### Sym(=) % 16.80/16.98 64. ((op (e3) (e3)) != (op (e3) (e4))) ((op (e3) (unit)) = (e3)) ((op (e3) (e3)) = (e3)) ((unit) = (e4)) ### Trans-sym 62 63 % 16.80/16.98 65. (((unit) = (e0)) \/ (((unit) = (e1)) \/ (((unit) = (e2)) \/ (((unit) = (e3)) \/ ((unit) = (e4)))))) ((op (e3) (e3)) != (op (e3) (e4))) ((op (e1) (e4)) = (e1)) ((op (e1) (unit)) = (e1)) ((op (e1) (e3)) != (op (e1) (e4))) ((op (e3) (e2)) != (op (e3) (e3))) ((op (e3) (e1)) != (op (e3) (e3))) ((op (e3) (e3)) = (e3)) ((op (e3) (unit)) = (e3)) ((op (e3) (e0)) != (op (e3) (e3))) ### DisjTree 52 56 60 19 64 % 16.80/16.98 66. (((op (e1) (e1)) != (e4)) \/ ((op (e1) (e4)) = (e1))) ((op (e3) (e0)) != (op (e3) (e3))) ((op (e3) (unit)) = (e3)) ((op (e3) (e3)) = (e3)) ((op (e3) (e1)) != (op (e3) (e3))) ((op (e3) (e2)) != (op (e3) (e3))) ((op (e1) (e3)) != (op (e1) (e4))) ((op (e1) (unit)) = (e1)) ((op (e3) (e3)) != (op (e3) (e4))) (((unit) = (e0)) \/ (((unit) = (e1)) \/ (((unit) = (e2)) \/ (((unit) = (e3)) \/ ((unit) = (e4)))))) ((e4) = (op (e1) (e1))) ### Or 47 65 % 16.80/16.98 67. ((e4) = (op (e1) (e1))) ((op (e1) (e1)) != (e4)) ### Sym(=) % 16.80/16.98 68. ((unit) = (e4)) ((e4) != (unit)) ### Sym(=) % 16.80/16.98 69. ((op (e4) (e3)) != (op (unit) (e3))) ((unit) = (e4)) ### NotEqual 68 48 % 16.80/16.98 70. ((op (e4) (e4)) = (e3)) ((e3) != (op (e4) (e4))) ### Sym(=) % 16.80/16.98 71. ((op (e4) (e3)) != (op (e4) (e4))) ((op (unit) (e3)) = (e3)) ((op (e4) (e4)) = (e3)) ((unit) = (e4)) ### Trans 69 70 % 16.80/16.98 72. (((unit) = (e0)) \/ (((unit) = (e1)) \/ (((unit) = (e2)) \/ (((unit) = (e3)) \/ ((unit) = (e4)))))) ((op (e4) (e4)) = (e3)) ((op (unit) (e3)) = (e3)) ((op (e4) (e3)) != (op (e4) (e4))) ((op (e1) (e3)) != (op (e1) (e4))) ((op (e1) (e2)) != (op (e1) (e4))) ((op (unit) (e1)) = (e1)) ((op (e1) (e1)) != (op (e1) (e4))) ((op (e1) (e4)) = (e1)) ((op (e1) (unit)) = (e1)) ((op (e1) (e0)) != (op (e1) (e4))) ### DisjTree 7 11 15 19 71 % 16.80/16.98 73. (((op (e1) (e1)) != (e4)) \/ ((op (e1) (e4)) = (e1))) ((op (e1) (e0)) != (op (e1) (e4))) ((op (e1) (unit)) = (e1)) ((op (e1) (e1)) != (op (e1) (e4))) ((op (unit) (e1)) = (e1)) ((op (e1) (e2)) != (op (e1) (e4))) ((op (e1) (e3)) != (op (e1) (e4))) ((op (e4) (e3)) != (op (e4) (e4))) ((op (unit) (e3)) = (e3)) ((op (e4) (e4)) = (e3)) (((unit) = (e0)) \/ (((unit) = (e1)) \/ (((unit) = (e2)) \/ (((unit) = (e3)) \/ ((unit) = (e4)))))) ((e4) = (op (e1) (e1))) ### Or 67 72 % 16.80/16.98 74. (((op (e0) (e0)) = (e3)) \/ (((op (e1) (e1)) = (e3)) \/ (((op (e2) (e2)) = (e3)) \/ (((op (e3) (e3)) = (e3)) \/ ((op (e4) (e4)) = (e3)))))) ((op (unit) (e3)) = (e3)) ((op (e4) (e3)) != (op (e4) (e4))) ((op (e3) (e3)) != (op (e3) (e4))) ((op (e3) (e2)) != (op (e3) (e3))) ((op (e3) (e1)) != (op (e3) (e3))) ((op (e3) (unit)) = (e3)) ((op (e3) (e0)) != (op (e3) (e3))) (((op (e2) (e2)) != (e3)) \/ ((op (e2) (e3)) = (e2))) ((op (e2) (e3)) != (op (e2) (e4))) ((op (e2) (unit)) = (e2)) (((op (e1) (e1)) != (e3)) \/ ((op (e1) (e3)) = (e1))) (((op (e1) (e1)) != (e4)) \/ ((op (e1) (e4)) = (e1))) ((op (e1) (e0)) != (op (e1) (e4))) ((op (e1) (unit)) = (e1)) ((op (e1) (e1)) != (op (e1) (e4))) ((op (unit) (e1)) = (e1)) ((op (e1) (e2)) != (op (e1) (e4))) ((op (e1) (e3)) != (op (e1) (e4))) ((op (e0) (e3)) != (op (e0) (e4))) ((op (e0) (unit)) = (e0)) (((unit) = (e0)) \/ (((unit) = (e1)) \/ (((unit) = (e2)) \/ (((unit) = (e3)) \/ ((unit) = (e4)))))) ((e4) = (op (e1) (e1))) (((op (e0) (e0)) != (e3)) \/ ((op (e0) (e3)) = (e0))) ### DisjTree 27 36 46 66 73 % 16.80/16.98 75. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e0)) \/ (((op (e2) (e2)) = (e0)) \/ (((op (e3) (e3)) = (e0)) \/ ((op (e4) (e4)) = (e0)))))) /\ ((((op (e0) (e0)) = (e1)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e1)) \/ (((op (e3) (e3)) = (e1)) \/ ((op (e4) (e4)) = (e1)))))) /\ ((((op (e0) (e0)) = (e2)) \/ (((op (e1) (e1)) = (e2)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e2)) \/ ((op (e4) (e4)) = (e2)))))) /\ ((((op (e0) (e0)) = (e3)) \/ (((op (e1) (e1)) = (e3)) \/ (((op (e2) (e2)) = (e3)) \/ (((op (e3) (e3)) = (e3)) \/ ((op (e4) (e4)) = (e3)))))) /\ ((((op (e0) (e0)) = (e4)) \/ (((op (e1) (e1)) = (e4)) \/ (((op (e2) (e2)) = (e4)) \/ (((op (e3) (e3)) = (e4)) \/ ((op (e4) (e4)) = (e4)))))) /\ ((((op (e0) (e0)) != (e0)) \/ ((op (e0) (e0)) = (e0))) /\ ((((op (e0) (e0)) != (e1)) \/ ((op (e0) (e1)) = (e0))) /\ ((((op (e0) (e0)) != (e2)) \/ ((op (e0) (e2)) = (e0))) /\ ((((op (e0) (e0)) != (e3)) \/ ((op (e0) (e3)) = (e0))) /\ ((((op (e0) (e0)) != (e4)) \/ ((op (e0) (e4)) = (e0))) /\ ((((op (e1) (e1)) != (e0)) \/ ((op (e1) (e0)) = (e1))) /\ ((((op (e1) (e1)) != (e1)) \/ ((op (e1) (e1)) = (e1))) /\ ((((op (e1) (e1)) != (e2)) \/ ((op (e1) (e2)) = (e1))) /\ ((((op (e1) (e1)) != (e3)) \/ ((op (e1) (e3)) = (e1))) /\ ((((op (e1) (e1)) != (e4)) \/ ((op (e1) (e4)) = (e1))) /\ ((((op (e2) (e2)) != (e0)) \/ ((op (e2) (e0)) = (e2))) /\ ((((op (e2) (e2)) != (e1)) \/ ((op (e2) (e1)) = (e2))) /\ ((((op (e2) (e2)) != (e2)) \/ ((op (e2) (e2)) = (e2))) /\ ((((op (e2) (e2)) != (e3)) \/ ((op (e2) (e3)) = (e2))) /\ ((((op (e2) (e2)) != (e4)) \/ ((op (e2) (e4)) = (e2))) /\ ((((op (e3) (e3)) != (e0)) \/ ((op (e3) (e0)) = (e3))) /\ ((((op (e3) (e3)) != (e1)) \/ ((op (e3) (e1)) = (e3))) /\ ((((op (e3) (e3)) != (e2)) \/ ((op (e3) (e2)) = (e3))) /\ ((((op (e3) (e3)) != (e3)) \/ ((op (e3) (e3)) = (e3))) /\ ((((op (e3) (e3)) != (e4)) \/ ((op (e3) (e4)) = (e3))) /\ ((((op (e4) (e4)) != (e0)) \/ ((op (e4) (e0)) = (e4))) /\ ((((op (e4) (e4)) != (e1)) \/ ((op (e4) (e1)) = (e4))) /\ ((((op (e4) (e4)) != (e2)) \/ ((op (e4) (e2)) = (e4))) /\ ((((op (e4) (e4)) != (e3)) \/ ((op (e4) (e3)) = (e4))) /\ (((op (e4) (e4)) != (e4)) \/ ((op (e4) (e4)) = (e4)))))))))))))))))))))))))))))))) ((e4) = (op (e1) (e1))) (((unit) = (e0)) \/ (((unit) = (e1)) \/ (((unit) = (e2)) \/ (((unit) = (e3)) \/ ((unit) = (e4)))))) ((op (e0) (unit)) = (e0)) ((op (e0) (e3)) != (op (e0) (e4))) ((op (e1) (e3)) != (op (e1) (e4))) ((op (e1) (e2)) != (op (e1) (e4))) ((op (unit) (e1)) = (e1)) ((op (e1) (e1)) != (op (e1) (e4))) ((op (e1) (unit)) = (e1)) ((op (e1) (e0)) != (op (e1) (e4))) ((op (e2) (unit)) = (e2)) ((op (e2) (e3)) != (op (e2) (e4))) ((op (e3) (e0)) != (op (e3) (e3))) ((op (e3) (unit)) = (e3)) ((op (e3) (e1)) != (op (e3) (e3))) ((op (e3) (e2)) != (op (e3) (e3))) ((op (e3) (e3)) != (op (e3) (e4))) ((op (e4) (e3)) != (op (e4) (e4))) ((op (unit) (e3)) = (e3)) ### ConjTree 74 % 16.80/16.98 76. (-. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e0)) \/ (((op (e2) (e2)) = (e0)) \/ (((op (e3) (e3)) = (e0)) \/ ((op (e4) (e4)) = (e0)))))) /\ ((((op (e0) (e0)) = (e1)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e1)) \/ (((op (e3) (e3)) = (e1)) \/ ((op (e4) (e4)) = (e1)))))) /\ ((((op (e0) (e0)) = (e2)) \/ (((op (e1) (e1)) = (e2)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e2)) \/ ((op (e4) (e4)) = (e2)))))) /\ ((((op (e0) (e0)) = (e3)) \/ (((op (e1) (e1)) = (e3)) \/ (((op (e2) (e2)) = (e3)) \/ (((op (e3) (e3)) = (e3)) \/ ((op (e4) (e4)) = (e3)))))) /\ ((((op (e0) (e0)) = (e4)) \/ (((op (e1) (e1)) = (e4)) \/ (((op (e2) (e2)) = (e4)) \/ (((op (e3) (e3)) = (e4)) \/ ((op (e4) (e4)) = (e4)))))) /\ ((((op (e0) (e0)) != (e0)) \/ ((op (e0) (e0)) = (e0))) /\ ((((op (e0) (e0)) != (e1)) \/ ((op (e0) (e1)) = (e0))) /\ ((((op (e0) (e0)) != (e2)) \/ ((op (e0) (e2)) = (e0))) /\ ((((op (e0) (e0)) != (e3)) \/ ((op (e0) (e3)) = (e0))) /\ ((((op (e0) (e0)) != (e4)) \/ ((op (e0) (e4)) = (e0))) /\ ((((op (e1) (e1)) != (e0)) \/ ((op (e1) (e0)) = (e1))) /\ ((((op (e1) (e1)) != (e1)) \/ ((op (e1) (e1)) = (e1))) /\ ((((op (e1) (e1)) != (e2)) \/ ((op (e1) (e2)) = (e1))) /\ ((((op (e1) (e1)) != (e3)) \/ ((op (e1) (e3)) = (e1))) /\ ((((op (e1) (e1)) != (e4)) \/ ((op (e1) (e4)) = (e1))) /\ ((((op (e2) (e2)) != (e0)) \/ ((op (e2) (e0)) = (e2))) /\ ((((op (e2) (e2)) != (e1)) \/ ((op (e2) (e1)) = (e2))) /\ ((((op (e2) (e2)) != (e2)) \/ ((op (e2) (e2)) = (e2))) /\ ((((op (e2) (e2)) != (e3)) \/ ((op (e2) (e3)) = (e2))) /\ ((((op (e2) (e2)) != (e4)) \/ ((op (e2) (e4)) = (e2))) /\ ((((op (e3) (e3)) != (e0)) \/ ((op (e3) (e0)) = (e3))) /\ ((((op (e3) (e3)) != (e1)) \/ ((op (e3) (e1)) = (e3))) /\ ((((op (e3) (e3)) != (e2)) \/ ((op (e3) (e2)) = (e3))) /\ ((((op (e3) (e3)) != (e3)) \/ ((op (e3) (e3)) = (e3))) /\ ((((op (e3) (e3)) != (e4)) \/ ((op (e3) (e4)) = (e3))) /\ ((((op (e4) (e4)) != (e0)) \/ ((op (e4) (e0)) = (e4))) /\ ((((op (e4) (e4)) != (e1)) \/ ((op (e4) (e1)) = (e4))) /\ ((((op (e4) (e4)) != (e2)) \/ ((op (e4) (e2)) = (e4))) /\ ((((op (e4) (e4)) != (e3)) \/ ((op (e4) (e3)) = (e4))) /\ (((op (e4) (e4)) != (e4)) \/ ((op (e4) (e4)) = (e4)))))))))))))))))))))))))))))))))) ((op (unit) (e3)) = (e3)) ((op (e4) (e3)) != (op (e4) (e4))) ((op (e3) (e3)) != (op (e3) (e4))) ((op (e3) (e2)) != (op (e3) (e3))) ((op (e3) (e1)) != (op (e3) (e3))) ((op (e3) (unit)) = (e3)) ((op (e3) (e0)) != (op (e3) (e3))) ((op (e2) (e3)) != (op (e2) (e4))) ((op (e2) (unit)) = (e2)) ((op (e1) (e0)) != (op (e1) (e4))) ((op (e1) (unit)) = (e1)) ((op (e1) (e1)) != (op (e1) (e4))) ((op (unit) (e1)) = (e1)) ((op (e1) (e2)) != (op (e1) (e4))) ((op (e1) (e3)) != (op (e1) (e4))) ((op (e0) (e3)) != (op (e0) (e4))) ((op (e0) (unit)) = (e0)) (((unit) = (e0)) \/ (((unit) = (e1)) \/ (((unit) = (e2)) \/ (((unit) = (e3)) \/ ((unit) = (e4)))))) ((e4) = (op (e1) (e1))) ### NotNot 75 % 16.80/16.98 77. (((e0) = (op (e1) (op (op (e1) (e1)) (op (e1) (e1))))) /\ (((e2) = (op (op (e1) (e1)) (op (e1) (e1)))) /\ (((e3) = (op (op (op (e1) (e1)) (op (e1) (e1))) (op (op (e1) (e1)) (op (e1) (e1))))) /\ ((e4) = (op (e1) (e1)))))) (((unit) = (e0)) \/ (((unit) = (e1)) \/ (((unit) = (e2)) \/ (((unit) = (e3)) \/ ((unit) = (e4)))))) ((op (e0) (unit)) = (e0)) ((op (e0) (e3)) != (op (e0) (e4))) ((op (e1) (e3)) != (op (e1) (e4))) ((op (e1) (e2)) != (op (e1) (e4))) ((op (unit) (e1)) = (e1)) ((op (e1) (e1)) != (op (e1) (e4))) ((op (e1) (unit)) = (e1)) ((op (e1) (e0)) != (op (e1) (e4))) ((op (e2) (unit)) = (e2)) ((op (e2) (e3)) != (op (e2) (e4))) ((op (e3) (e0)) != (op (e3) (e3))) ((op (e3) (unit)) = (e3)) ((op (e3) (e1)) != (op (e3) (e3))) ((op (e3) (e2)) != (op (e3) (e3))) ((op (e3) (e3)) != (op (e3) (e4))) ((op (e4) (e3)) != (op (e4) (e4))) ((op (unit) (e3)) = (e3)) (-. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e0)) \/ (((op (e2) (e2)) = (e0)) \/ (((op (e3) (e3)) = (e0)) \/ ((op (e4) (e4)) = (e0)))))) /\ ((((op (e0) (e0)) = (e1)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e1)) \/ (((op (e3) (e3)) = (e1)) \/ ((op (e4) (e4)) = (e1)))))) /\ ((((op (e0) (e0)) = (e2)) \/ (((op (e1) (e1)) = (e2)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e2)) \/ ((op (e4) (e4)) = (e2)))))) /\ ((((op (e0) (e0)) = (e3)) \/ (((op (e1) (e1)) = (e3)) \/ (((op (e2) (e2)) = (e3)) \/ (((op (e3) (e3)) = (e3)) \/ ((op (e4) (e4)) = (e3)))))) /\ ((((op (e0) (e0)) = (e4)) \/ (((op (e1) (e1)) = (e4)) \/ (((op (e2) (e2)) = (e4)) \/ (((op (e3) (e3)) = (e4)) \/ ((op (e4) (e4)) = (e4)))))) /\ ((((op (e0) (e0)) != (e0)) \/ ((op (e0) (e0)) = (e0))) /\ ((((op (e0) (e0)) != (e1)) \/ ((op (e0) (e1)) = (e0))) /\ ((((op (e0) (e0)) != (e2)) \/ ((op (e0) (e2)) = (e0))) /\ ((((op (e0) (e0)) != (e3)) \/ ((op (e0) (e3)) = (e0))) /\ ((((op (e0) (e0)) != (e4)) \/ ((op (e0) (e4)) = (e0))) /\ ((((op (e1) (e1)) != (e0)) \/ ((op (e1) (e0)) = (e1))) /\ ((((op (e1) (e1)) != (e1)) \/ ((op (e1) (e1)) = (e1))) /\ ((((op (e1) (e1)) != (e2)) \/ ((op (e1) (e2)) = (e1))) /\ ((((op (e1) (e1)) != (e3)) \/ ((op (e1) (e3)) = (e1))) /\ ((((op (e1) (e1)) != (e4)) \/ ((op (e1) (e4)) = (e1))) /\ ((((op (e2) (e2)) != (e0)) \/ ((op (e2) (e0)) = (e2))) /\ ((((op (e2) (e2)) != (e1)) \/ ((op (e2) (e1)) = (e2))) /\ ((((op (e2) (e2)) != (e2)) \/ ((op (e2) (e2)) = (e2))) /\ ((((op (e2) (e2)) != (e3)) \/ ((op (e2) (e3)) = (e2))) /\ ((((op (e2) (e2)) != (e4)) \/ ((op (e2) (e4)) = (e2))) /\ ((((op (e3) (e3)) != (e0)) \/ ((op (e3) (e0)) = (e3))) /\ ((((op (e3) (e3)) != (e1)) \/ ((op (e3) (e1)) = (e3))) /\ ((((op (e3) (e3)) != (e2)) \/ ((op (e3) (e2)) = (e3))) /\ ((((op (e3) (e3)) != (e3)) \/ ((op (e3) (e3)) = (e3))) /\ ((((op (e3) (e3)) != (e4)) \/ ((op (e3) (e4)) = (e3))) /\ ((((op (e4) (e4)) != (e0)) \/ ((op (e4) (e0)) = (e4))) /\ ((((op (e4) (e4)) != (e1)) \/ ((op (e4) (e1)) = (e4))) /\ ((((op (e4) (e4)) != (e2)) \/ ((op (e4) (e2)) = (e4))) /\ ((((op (e4) (e4)) != (e3)) \/ ((op (e4) (e3)) = (e4))) /\ (((op (e4) (e4)) != (e4)) \/ ((op (e4) (e4)) = (e4)))))))))))))))))))))))))))))))))) ### ConjTree 76 % 16.80/16.98 78. (((op (e0) (e0)) != (op (e1) (e0))) /\ (((op (e0) (e0)) != (op (e2) (e0))) /\ (((op (e0) (e0)) != (op (e3) (e0))) /\ (((op (e0) (e0)) != (op (e4) (e0))) /\ (((op (e1) (e0)) != (op (e2) (e0))) /\ (((op (e1) (e0)) != (op (e3) (e0))) /\ (((op (e1) (e0)) != (op (e4) (e0))) /\ (((op (e2) (e0)) != (op (e3) (e0))) /\ (((op (e2) (e0)) != (op (e4) (e0))) /\ (((op (e3) (e0)) != (op (e4) (e0))) /\ (((op (e0) (e1)) != (op (e1) (e1))) /\ (((op (e0) (e1)) != (op (e2) (e1))) /\ (((op (e0) (e1)) != (op (e3) (e1))) /\ (((op (e0) (e1)) != (op (e4) (e1))) /\ (((op (e1) (e1)) != (op (e2) (e1))) /\ (((op (e1) (e1)) != (op (e3) (e1))) /\ (((op (e1) (e1)) != (op (e4) (e1))) /\ (((op (e2) (e1)) != (op (e3) (e1))) /\ (((op (e2) (e1)) != (op (e4) (e1))) /\ (((op (e3) (e1)) != (op (e4) (e1))) /\ (((op (e0) (e2)) != (op (e1) (e2))) /\ (((op (e0) (e2)) != (op (e2) (e2))) /\ (((op (e0) (e2)) != (op (e3) (e2))) /\ (((op (e0) (e2)) != (op (e4) (e2))) /\ (((op (e1) (e2)) != (op (e2) (e2))) /\ (((op (e1) (e2)) != (op (e3) (e2))) /\ (((op (e1) (e2)) != (op (e4) (e2))) /\ (((op (e2) (e2)) != (op (e3) (e2))) /\ (((op (e2) (e2)) != (op (e4) (e2))) /\ (((op (e3) (e2)) != (op (e4) (e2))) /\ (((op (e0) (e3)) != (op (e1) (e3))) /\ (((op (e0) (e3)) != (op (e2) (e3))) /\ (((op (e0) (e3)) != (op (e3) (e3))) /\ (((op (e0) (e3)) != (op (e4) (e3))) /\ (((op (e1) (e3)) != (op (e2) (e3))) /\ (((op (e1) (e3)) != (op (e3) (e3))) /\ (((op (e1) (e3)) != (op (e4) (e3))) /\ (((op (e2) (e3)) != (op (e3) (e3))) /\ (((op (e2) (e3)) != (op (e4) (e3))) /\ (((op (e3) (e3)) != (op (e4) (e3))) /\ (((op (e0) (e4)) != (op (e1) (e4))) /\ (((op (e0) (e4)) != (op (e2) (e4))) /\ (((op (e0) (e4)) != (op (e3) (e4))) /\ (((op (e0) (e4)) != (op (e4) (e4))) /\ (((op (e1) (e4)) != (op (e2) (e4))) /\ (((op (e1) (e4)) != (op (e3) (e4))) /\ (((op (e1) (e4)) != (op (e4) (e4))) /\ (((op (e2) (e4)) != (op (e3) (e4))) /\ (((op (e2) (e4)) != (op (e4) (e4))) /\ (((op (e3) (e4)) != (op (e4) (e4))) /\ (((op (e0) (e0)) != (op (e0) (e1))) /\ (((op (e0) (e0)) != (op (e0) (e2))) /\ (((op (e0) (e0)) != (op (e0) (e3))) /\ (((op (e0) (e0)) != (op (e0) (e4))) /\ (((op (e0) (e1)) != (op (e0) (e2))) /\ (((op (e0) (e1)) != (op (e0) (e3))) /\ (((op (e0) (e1)) != (op (e0) (e4))) /\ (((op (e0) (e2)) != (op (e0) (e3))) /\ (((op (e0) (e2)) != (op (e0) (e4))) /\ (((op (e0) (e3)) != (op (e0) (e4))) /\ (((op (e1) (e0)) != (op (e1) (e1))) /\ (((op (e1) (e0)) != (op (e1) (e2))) /\ (((op (e1) (e0)) != (op (e1) (e3))) /\ (((op (e1) (e0)) != (op (e1) (e4))) /\ (((op (e1) (e1)) != (op (e1) (e2))) /\ (((op (e1) (e1)) != (op (e1) (e3))) /\ (((op (e1) (e1)) != (op (e1) (e4))) /\ (((op (e1) (e2)) != (op (e1) (e3))) /\ (((op (e1) (e2)) != (op (e1) (e4))) /\ (((op (e1) (e3)) != (op (e1) (e4))) /\ (((op (e2) (e0)) != (op (e2) (e1))) /\ (((op (e2) (e0)) != (op (e2) (e2))) /\ (((op (e2) (e0)) != (op (e2) (e3))) /\ (((op (e2) (e0)) != (op (e2) (e4))) /\ (((op (e2) (e1)) != (op (e2) (e2))) /\ (((op (e2) (e1)) != (op (e2) (e3))) /\ (((op (e2) (e1)) != (op (e2) (e4))) /\ (((op (e2) (e2)) != (op (e2) (e3))) /\ (((op (e2) (e2)) != (op (e2) (e4))) /\ (((op (e2) (e3)) != (op (e2) (e4))) /\ (((op (e3) (e0)) != (op (e3) (e1))) /\ (((op (e3) (e0)) != (op (e3) (e2))) /\ (((op (e3) (e0)) != (op (e3) (e3))) /\ (((op (e3) (e0)) != (op (e3) (e4))) /\ (((op (e3) (e1)) != (op (e3) (e2))) /\ (((op (e3) (e1)) != (op (e3) (e3))) /\ (((op (e3) (e1)) != (op (e3) (e4))) /\ (((op (e3) (e2)) != (op (e3) (e3))) /\ (((op (e3) (e2)) != (op (e3) (e4))) /\ (((op (e3) (e3)) != (op (e3) (e4))) /\ (((op (e4) (e0)) != (op (e4) (e1))) /\ (((op (e4) (e0)) != (op (e4) (e2))) /\ (((op (e4) (e0)) != (op (e4) (e3))) /\ (((op (e4) (e0)) != (op (e4) (e4))) /\ (((op (e4) (e1)) != (op (e4) (e2))) /\ (((op (e4) (e1)) != (op (e4) (e3))) /\ (((op (e4) (e1)) != (op (e4) (e4))) /\ (((op (e4) (e2)) != (op (e4) (e3))) /\ (((op (e4) (e2)) != (op (e4) (e4))) /\ ((op (e4) (e3)) != (op (e4) (e4)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (-. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e0)) \/ (((op (e2) (e2)) = (e0)) \/ (((op (e3) (e3)) = (e0)) \/ ((op (e4) (e4)) = (e0)))))) /\ ((((op (e0) (e0)) = (e1)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e1)) \/ (((op (e3) (e3)) = (e1)) \/ ((op (e4) (e4)) = (e1)))))) /\ ((((op (e0) (e0)) = (e2)) \/ (((op (e1) (e1)) = (e2)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e2)) \/ ((op (e4) (e4)) = (e2)))))) /\ ((((op (e0) (e0)) = (e3)) \/ (((op (e1) (e1)) = (e3)) \/ (((op (e2) (e2)) = (e3)) \/ (((op (e3) (e3)) = (e3)) \/ ((op (e4) (e4)) = (e3)))))) /\ ((((op (e0) (e0)) = (e4)) \/ (((op (e1) (e1)) = (e4)) \/ (((op (e2) (e2)) = (e4)) \/ (((op (e3) (e3)) = (e4)) \/ ((op (e4) (e4)) = (e4)))))) /\ ((((op (e0) (e0)) != (e0)) \/ ((op (e0) (e0)) = (e0))) /\ ((((op (e0) (e0)) != (e1)) \/ ((op (e0) (e1)) = (e0))) /\ ((((op (e0) (e0)) != (e2)) \/ ((op (e0) (e2)) = (e0))) /\ ((((op (e0) (e0)) != (e3)) \/ ((op (e0) (e3)) = (e0))) /\ ((((op (e0) (e0)) != (e4)) \/ ((op (e0) (e4)) = (e0))) /\ ((((op (e1) (e1)) != (e0)) \/ ((op (e1) (e0)) = (e1))) /\ ((((op (e1) (e1)) != (e1)) \/ ((op (e1) (e1)) = (e1))) /\ ((((op (e1) (e1)) != (e2)) \/ ((op (e1) (e2)) = (e1))) /\ ((((op (e1) (e1)) != (e3)) \/ ((op (e1) (e3)) = (e1))) /\ ((((op (e1) (e1)) != (e4)) \/ ((op (e1) (e4)) = (e1))) /\ ((((op (e2) (e2)) != (e0)) \/ ((op (e2) (e0)) = (e2))) /\ ((((op (e2) (e2)) != (e1)) \/ ((op (e2) (e1)) = (e2))) /\ ((((op (e2) (e2)) != (e2)) \/ ((op (e2) (e2)) = (e2))) /\ ((((op (e2) (e2)) != (e3)) \/ ((op (e2) (e3)) = (e2))) /\ ((((op (e2) (e2)) != (e4)) \/ ((op (e2) (e4)) = (e2))) /\ ((((op (e3) (e3)) != (e0)) \/ ((op (e3) (e0)) = (e3))) /\ ((((op (e3) (e3)) != (e1)) \/ ((op (e3) (e1)) = (e3))) /\ ((((op (e3) (e3)) != (e2)) \/ ((op (e3) (e2)) = (e3))) /\ ((((op (e3) (e3)) != (e3)) \/ ((op (e3) (e3)) = (e3))) /\ ((((op (e3) (e3)) != (e4)) \/ ((op (e3) (e4)) = (e3))) /\ ((((op (e4) (e4)) != (e0)) \/ ((op (e4) (e0)) = (e4))) /\ ((((op (e4) (e4)) != (e1)) \/ ((op (e4) (e1)) = (e4))) /\ ((((op (e4) (e4)) != (e2)) \/ ((op (e4) (e2)) = (e4))) /\ ((((op (e4) (e4)) != (e3)) \/ ((op (e4) (e3)) = (e4))) /\ (((op (e4) (e4)) != (e4)) \/ ((op (e4) (e4)) = (e4)))))))))))))))))))))))))))))))))) ((op (unit) (e3)) = (e3)) ((op (e3) (unit)) = (e3)) ((op (e2) (unit)) = (e2)) ((op (e1) (unit)) = (e1)) ((op (unit) (e1)) = (e1)) ((op (e0) (unit)) = (e0)) (((unit) = (e0)) \/ (((unit) = (e1)) \/ (((unit) = (e2)) \/ (((unit) = (e3)) \/ ((unit) = (e4)))))) (((e0) = (op (e1) (op (op (e1) (e1)) (op (e1) (e1))))) /\ (((e2) = (op (op (e1) (e1)) (op (e1) (e1)))) /\ (((e3) = (op (op (op (e1) (e1)) (op (e1) (e1))) (op (op (e1) (e1)) (op (e1) (e1))))) /\ ((e4) = (op (e1) (e1)))))) ### ConjTree 77 % 16.80/16.98 79. (((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)) /\ (((op (unit) (e4)) = (e4)) /\ (((op (e4) (unit)) = (e4)) /\ (((unit) = (e0)) \/ (((unit) = (e1)) \/ (((unit) = (e2)) \/ (((unit) = (e3)) \/ ((unit) = (e4)))))))))))))))) (((e0) = (op (e1) (op (op (e1) (e1)) (op (e1) (e1))))) /\ (((e2) = (op (op (e1) (e1)) (op (e1) (e1)))) /\ (((e3) = (op (op (op (e1) (e1)) (op (e1) (e1))) (op (op (e1) (e1)) (op (e1) (e1))))) /\ ((e4) = (op (e1) (e1)))))) (-. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e0)) \/ (((op (e2) (e2)) = (e0)) \/ (((op (e3) (e3)) = (e0)) \/ ((op (e4) (e4)) = (e0)))))) /\ ((((op (e0) (e0)) = (e1)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e1)) \/ (((op (e3) (e3)) = (e1)) \/ ((op (e4) (e4)) = (e1)))))) /\ ((((op (e0) (e0)) = (e2)) \/ (((op (e1) (e1)) = (e2)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e2)) \/ ((op (e4) (e4)) = (e2)))))) /\ ((((op (e0) (e0)) = (e3)) \/ (((op (e1) (e1)) = (e3)) \/ (((op (e2) (e2)) = (e3)) \/ (((op (e3) (e3)) = (e3)) \/ ((op (e4) (e4)) = (e3)))))) /\ ((((op (e0) (e0)) = (e4)) \/ (((op (e1) (e1)) = (e4)) \/ (((op (e2) (e2)) = (e4)) \/ (((op (e3) (e3)) = (e4)) \/ ((op (e4) (e4)) = (e4)))))) /\ ((((op (e0) (e0)) != (e0)) \/ ((op (e0) (e0)) = (e0))) /\ ((((op (e0) (e0)) != (e1)) \/ ((op (e0) (e1)) = (e0))) /\ ((((op (e0) (e0)) != (e2)) \/ ((op (e0) (e2)) = (e0))) /\ ((((op (e0) (e0)) != (e3)) \/ ((op (e0) (e3)) = (e0))) /\ ((((op (e0) (e0)) != (e4)) \/ ((op (e0) (e4)) = (e0))) /\ ((((op (e1) (e1)) != (e0)) \/ ((op (e1) (e0)) = (e1))) /\ ((((op (e1) (e1)) != (e1)) \/ ((op (e1) (e1)) = (e1))) /\ ((((op (e1) (e1)) != (e2)) \/ ((op (e1) (e2)) = (e1))) /\ ((((op (e1) (e1)) != (e3)) \/ ((op (e1) (e3)) = (e1))) /\ ((((op (e1) (e1)) != (e4)) \/ ((op (e1) (e4)) = (e1))) /\ ((((op (e2) (e2)) != (e0)) \/ ((op (e2) (e0)) = (e2))) /\ ((((op (e2) (e2)) != (e1)) \/ ((op (e2) (e1)) = (e2))) /\ ((((op (e2) (e2)) != (e2)) \/ ((op (e2) (e2)) = (e2))) /\ ((((op (e2) (e2)) != (e3)) \/ ((op (e2) (e3)) = (e2))) /\ ((((op (e2) (e2)) != (e4)) \/ ((op (e2) (e4)) = (e2))) /\ ((((op (e3) (e3)) != (e0)) \/ ((op (e3) (e0)) = (e3))) /\ ((((op (e3) (e3)) != (e1)) \/ ((op (e3) (e1)) = (e3))) /\ ((((op (e3) (e3)) != (e2)) \/ ((op (e3) (e2)) = (e3))) /\ ((((op (e3) (e3)) != (e3)) \/ ((op (e3) (e3)) = (e3))) /\ ((((op (e3) (e3)) != (e4)) \/ ((op (e3) (e4)) = (e3))) /\ ((((op (e4) (e4)) != (e0)) \/ ((op (e4) (e0)) = (e4))) /\ ((((op (e4) (e4)) != (e1)) \/ ((op (e4) (e1)) = (e4))) /\ ((((op (e4) (e4)) != (e2)) \/ ((op (e4) (e2)) = (e4))) /\ ((((op (e4) (e4)) != (e3)) \/ ((op (e4) (e3)) = (e4))) /\ (((op (e4) (e4)) != (e4)) \/ ((op (e4) (e4)) = (e4)))))))))))))))))))))))))))))))))) (((op (e0) (e0)) != (op (e1) (e0))) /\ (((op (e0) (e0)) != (op (e2) (e0))) /\ (((op (e0) (e0)) != (op (e3) (e0))) /\ (((op (e0) (e0)) != (op (e4) (e0))) /\ (((op (e1) (e0)) != (op (e2) (e0))) /\ (((op (e1) (e0)) != (op (e3) (e0))) /\ (((op (e1) (e0)) != (op (e4) (e0))) /\ (((op (e2) (e0)) != (op (e3) (e0))) /\ (((op (e2) (e0)) != (op (e4) (e0))) /\ (((op (e3) (e0)) != (op (e4) (e0))) /\ (((op (e0) (e1)) != (op (e1) (e1))) /\ (((op (e0) (e1)) != (op (e2) (e1))) /\ (((op (e0) (e1)) != (op (e3) (e1))) /\ (((op (e0) (e1)) != (op (e4) (e1))) /\ (((op (e1) (e1)) != (op (e2) (e1))) /\ (((op (e1) (e1)) != (op (e3) (e1))) /\ (((op (e1) (e1)) != (op (e4) (e1))) /\ (((op (e2) (e1)) != (op (e3) (e1))) /\ (((op (e2) (e1)) != (op (e4) (e1))) /\ (((op (e3) (e1)) != (op (e4) (e1))) /\ (((op (e0) (e2)) != (op (e1) (e2))) /\ (((op (e0) (e2)) != (op (e2) (e2))) /\ (((op (e0) (e2)) != (op (e3) (e2))) /\ (((op (e0) (e2)) != (op (e4) (e2))) /\ (((op (e1) (e2)) != (op (e2) (e2))) /\ (((op (e1) (e2)) != (op (e3) (e2))) /\ (((op (e1) (e2)) != (op (e4) (e2))) /\ (((op (e2) (e2)) != (op (e3) (e2))) /\ (((op (e2) (e2)) != (op (e4) (e2))) /\ (((op (e3) (e2)) != (op (e4) (e2))) /\ (((op (e0) (e3)) != (op (e1) (e3))) /\ (((op (e0) (e3)) != (op (e2) (e3))) /\ (((op (e0) (e3)) != (op (e3) (e3))) /\ (((op (e0) (e3)) != (op (e4) (e3))) /\ (((op (e1) (e3)) != (op (e2) (e3))) /\ (((op (e1) (e3)) != (op (e3) (e3))) /\ (((op (e1) (e3)) != (op (e4) (e3))) /\ (((op (e2) (e3)) != (op (e3) (e3))) /\ (((op (e2) (e3)) != (op (e4) (e3))) /\ (((op (e3) (e3)) != (op (e4) (e3))) /\ (((op (e0) (e4)) != (op (e1) (e4))) /\ (((op (e0) (e4)) != (op (e2) (e4))) /\ (((op (e0) (e4)) != (op (e3) (e4))) /\ (((op (e0) (e4)) != (op (e4) (e4))) /\ (((op (e1) (e4)) != (op (e2) (e4))) /\ (((op (e1) (e4)) != (op (e3) (e4))) /\ (((op (e1) (e4)) != (op (e4) (e4))) /\ (((op (e2) (e4)) != (op (e3) (e4))) /\ (((op (e2) (e4)) != (op (e4) (e4))) /\ (((op (e3) (e4)) != (op (e4) (e4))) /\ (((op (e0) (e0)) != (op (e0) (e1))) /\ (((op (e0) (e0)) != (op (e0) (e2))) /\ (((op (e0) (e0)) != (op (e0) (e3))) /\ (((op (e0) (e0)) != (op (e0) (e4))) /\ (((op (e0) (e1)) != (op (e0) (e2))) /\ (((op (e0) (e1)) != (op (e0) (e3))) /\ (((op (e0) (e1)) != (op (e0) (e4))) /\ (((op (e0) (e2)) != (op (e0) (e3))) /\ (((op (e0) (e2)) != (op (e0) (e4))) /\ (((op (e0) (e3)) != (op (e0) (e4))) /\ (((op (e1) (e0)) != (op (e1) (e1))) /\ (((op (e1) (e0)) != (op (e1) (e2))) /\ (((op (e1) (e0)) != (op (e1) (e3))) /\ (((op (e1) (e0)) != (op (e1) (e4))) /\ (((op (e1) (e1)) != (op (e1) (e2))) /\ (((op (e1) (e1)) != (op (e1) (e3))) /\ (((op (e1) (e1)) != (op (e1) (e4))) /\ (((op (e1) (e2)) != (op (e1) (e3))) /\ (((op (e1) (e2)) != (op (e1) (e4))) /\ (((op (e1) (e3)) != (op (e1) (e4))) /\ (((op (e2) (e0)) != (op (e2) (e1))) /\ (((op (e2) (e0)) != (op (e2) (e2))) /\ (((op (e2) (e0)) != (op (e2) (e3))) /\ (((op (e2) (e0)) != (op (e2) (e4))) /\ (((op (e2) (e1)) != (op (e2) (e2))) /\ (((op (e2) (e1)) != (op (e2) (e3))) /\ (((op (e2) (e1)) != (op (e2) (e4))) /\ (((op (e2) (e2)) != (op (e2) (e3))) /\ (((op (e2) (e2)) != (op (e2) (e4))) /\ (((op (e2) (e3)) != (op (e2) (e4))) /\ (((op (e3) (e0)) != (op (e3) (e1))) /\ (((op (e3) (e0)) != (op (e3) (e2))) /\ (((op (e3) (e0)) != (op (e3) (e3))) /\ (((op (e3) (e0)) != (op (e3) (e4))) /\ (((op (e3) (e1)) != (op (e3) (e2))) /\ (((op (e3) (e1)) != (op (e3) (e3))) /\ (((op (e3) (e1)) != (op (e3) (e4))) /\ (((op (e3) (e2)) != (op (e3) (e3))) /\ (((op (e3) (e2)) != (op (e3) (e4))) /\ (((op (e3) (e3)) != (op (e3) (e4))) /\ (((op (e4) (e0)) != (op (e4) (e1))) /\ (((op (e4) (e0)) != (op (e4) (e2))) /\ (((op (e4) (e0)) != (op (e4) (e3))) /\ (((op (e4) (e0)) != (op (e4) (e4))) /\ (((op (e4) (e1)) != (op (e4) (e2))) /\ (((op (e4) (e1)) != (op (e4) (e3))) /\ (((op (e4) (e1)) != (op (e4) (e4))) /\ (((op (e4) (e2)) != (op (e4) (e3))) /\ (((op (e4) (e2)) != (op (e4) (e4))) /\ ((op (e4) (e3)) != (op (e4) (e4)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ### ConjTree 78 % 16.80/16.98 % SZS output end Proof % 16.80/16.98 (* END-PROOF *) %------------------------------------------------------------------------------