%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : ALG042+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:51 EDT 2022 % Result : Theorem 27.80s 28.02s % Output : Proof 27.80s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : ALG042+1 : TPTP v8.1.0. Released v2.7.0. % 0.03/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 : Wed Jun 8 14:03:03 EDT 2022 % 0.12/0.34 % CPUTime : % 27.80/28.02 % SZS status Theorem % 27.80/28.02 (* PROOF-FOUND *) % 27.80/28.02 (* BEGIN-PROOF *) % 27.80/28.02 % SZS output start Proof % 27.80/28.02 1. ((h (e11)) = (e20)) ((h (e11)) != (e20)) ### Axiom % 27.80/28.02 2. ((j (h (e11))) != (j (e20))) ((h (e11)) = (e20)) ### NotEqual 1 % 27.80/28.02 3. ((e10) != (e10)) ### NotEqual % 27.80/28.02 4. ((e10) != (j (h (e11)))) ((j (e20)) = (e10)) ((h (e11)) = (e20)) ### Trans-sym 2 3 % 27.80/28.02 5. ((e11) != (e11)) ### NotEqual % 27.80/28.02 6. ((e10) != (e11)) ((j (h (e11))) = (e11)) ((h (e11)) = (e20)) ((j (e20)) = (e10)) ### TransEq 4 5 5 % 27.80/28.02 7. ((op2 (e20) (e20)) = (e20)) ((e20) != (op2 (e20) (e20))) ### Sym(=) % 27.80/28.02 8. ((j (e20)) != (j (op2 (e20) (e20)))) ((op2 (e20) (e20)) = (e20)) ### NotEqual 7 % 27.80/28.02 9. ((j (e20)) = (e11)) ((j (e20)) != (e11)) ### Axiom % 27.80/28.02 10. ((j (e20)) = (e11)) ((j (e20)) != (e11)) ### Axiom % 27.80/28.02 11. ((op1 (j (e20)) (j (e20))) != (op1 (e11) (e11))) ((j (e20)) = (e11)) ### NotEqual 9 10 % 27.80/28.02 12. ((op1 (e13) (e13)) = (e10)) ((e10) != (op1 (e13) (e13))) ### Sym(=) % 27.80/28.02 13. ((op1 (j (e20)) (j (e20))) != (op1 (e13) (e13))) ((op1 (e11) (e11)) = (e10)) ((op1 (e13) (e13)) = (e10)) ((j (e20)) = (e11)) ### Trans 11 12 % 27.80/28.02 14. ((op1 (e13) (e13)) != (j (e20))) ((j (op2 (e20) (e20))) = (op1 (j (e20)) (j (e20)))) ((j (e20)) = (e11)) ((op1 (e13) (e13)) = (e10)) ((op1 (e11) (e11)) = (e10)) ((op2 (e20) (e20)) = (e20)) ### Trans-sym 8 13 % 27.80/28.02 15. ((e11) != (op1 (e13) (e13))) ((op2 (e20) (e20)) = (e20)) ((op1 (e11) (e11)) = (e10)) ((op1 (e13) (e13)) = (e10)) ((j (e20)) = (e11)) ((j (op2 (e20) (e20))) = (op1 (j (e20)) (j (e20)))) ### Trans-sym 14 5 % 27.80/28.02 16. ((e10) != (e11)) ((j (op2 (e20) (e20))) = (op1 (j (e20)) (j (e20)))) ((j (e20)) = (e11)) ((op1 (e13) (e13)) = (e10)) ((op1 (e11) (e11)) = (e10)) ((op2 (e20) (e20)) = (e20)) ### TransEq-sym 15 3 3 % 27.80/28.02 17. ((j (e20)) = (e12)) ((j (e20)) != (e12)) ### Axiom % 27.80/28.02 18. ((j (e20)) = (e12)) ((j (e20)) != (e12)) ### Axiom % 27.80/28.02 19. ((op1 (j (e20)) (j (e20))) != (op1 (e12) (e12))) ((j (e20)) = (e12)) ### NotEqual 17 18 % 27.80/28.02 20. ((op1 (e13) (e13)) = (e10)) ((e10) != (op1 (e13) (e13))) ### Sym(=) % 27.80/28.02 21. ((op1 (j (e20)) (j (e20))) != (op1 (e13) (e13))) ((op1 (e12) (e12)) = (e10)) ((op1 (e13) (e13)) = (e10)) ((j (e20)) = (e12)) ### Trans 19 20 % 27.80/28.02 22. ((op1 (e13) (e13)) != (j (e20))) ((j (op2 (e20) (e20))) = (op1 (j (e20)) (j (e20)))) ((j (e20)) = (e12)) ((op1 (e13) (e13)) = (e10)) ((op1 (e12) (e12)) = (e10)) ((op2 (e20) (e20)) = (e20)) ### Trans-sym 8 21 % 27.80/28.02 23. ((e12) != (e12)) ### NotEqual % 27.80/28.02 24. ((e12) != (op1 (e13) (e13))) ((op2 (e20) (e20)) = (e20)) ((op1 (e12) (e12)) = (e10)) ((op1 (e13) (e13)) = (e10)) ((j (e20)) = (e12)) ((j (op2 (e20) (e20))) = (op1 (j (e20)) (j (e20)))) ### Trans-sym 22 23 % 27.80/28.02 25. ((e10) != (e12)) ((j (op2 (e20) (e20))) = (op1 (j (e20)) (j (e20)))) ((j (e20)) = (e12)) ((op1 (e13) (e13)) = (e10)) ((op1 (e12) (e12)) = (e10)) ((op2 (e20) (e20)) = (e20)) ### TransEq-sym 24 3 3 % 27.80/28.02 26. ((j (e20)) = (e13)) ((j (e20)) != (e13)) ### Axiom % 27.80/28.02 27. ((j (e20)) = (e13)) ((j (e20)) != (e13)) ### Axiom % 27.80/28.02 28. ((op1 (j (e20)) (j (e20))) != (op1 (e13) (e13))) ((j (e20)) = (e13)) ### NotEqual 26 27 % 27.80/28.02 29. ((op1 (e13) (e13)) != (j (e20))) ((j (op2 (e20) (e20))) = (op1 (j (e20)) (j (e20)))) ((j (e20)) = (e13)) ((op2 (e20) (e20)) = (e20)) ### Trans-sym 8 28 % 27.80/28.02 30. ((e13) != (e13)) ### NotEqual % 27.80/28.02 31. ((e13) != (op1 (e13) (e13))) ((op2 (e20) (e20)) = (e20)) ((j (e20)) = (e13)) ((j (op2 (e20) (e20))) = (op1 (j (e20)) (j (e20)))) ### Trans-sym 29 30 % 27.80/28.02 32. ((e10) != (e13)) ((op1 (e13) (e13)) = (e10)) ((j (op2 (e20) (e20))) = (op1 (j (e20)) (j (e20)))) ((j (e20)) = (e13)) ((op2 (e20) (e20)) = (e20)) ### TransEq-sym 31 3 3 % 27.80/28.02 33. (((j (e20)) = (e10)) \/ (((j (e20)) = (e11)) \/ (((j (e20)) = (e12)) \/ ((j (e20)) = (e13))))) ((e10) != (e13)) ((op1 (e12) (e12)) = (e10)) ((e10) != (e12)) ((op2 (e20) (e20)) = (e20)) ((op1 (e11) (e11)) = (e10)) ((op1 (e13) (e13)) = (e10)) ((j (op2 (e20) (e20))) = (op1 (j (e20)) (j (e20)))) ((h (e11)) = (e20)) ((j (h (e11))) = (e11)) ((e10) != (e11)) ### DisjTree 6 16 25 32 % 27.80/28.02 34. ((h (e12)) = (e20)) ((h (e12)) != (e20)) ### Axiom % 27.80/28.02 35. ((j (h (e12))) != (j (e20))) ((h (e12)) = (e20)) ### NotEqual 34 % 27.80/28.02 36. ((e10) != (j (h (e12)))) ((j (e20)) = (e10)) ((h (e12)) = (e20)) ### Trans-sym 35 3 % 27.80/28.02 37. ((e10) != (e12)) ((j (h (e12))) = (e12)) ((h (e12)) = (e20)) ((j (e20)) = (e10)) ### TransEq 36 23 23 % 27.80/28.02 38. ((e11) != (j (h (e12)))) ((j (e20)) = (e11)) ((h (e12)) = (e20)) ### Trans-sym 35 5 % 27.80/28.02 39. ((e11) != (e12)) ((j (h (e12))) = (e12)) ((h (e12)) = (e20)) ((j (e20)) = (e11)) ### TransEq 38 23 23 % 27.80/28.02 40. (((j (e20)) = (e10)) \/ (((j (e20)) = (e11)) \/ (((j (e20)) = (e12)) \/ ((j (e20)) = (e13))))) ((e10) != (e13)) ((op2 (e20) (e20)) = (e20)) ((op1 (e12) (e12)) = (e10)) ((op1 (e13) (e13)) = (e10)) ((j (op2 (e20) (e20))) = (op1 (j (e20)) (j (e20)))) ((e11) != (e12)) ((h (e12)) = (e20)) ((j (h (e12))) = (e12)) ((e10) != (e12)) ### DisjTree 37 39 25 32 % 27.80/28.02 41. ((h (e12)) = (e21)) ((h (e12)) != (e21)) ### Axiom % 27.80/28.02 42. ((j (h (e12))) != (j (e21))) ((h (e12)) = (e21)) ### NotEqual 41 % 27.80/28.02 43. ((e10) != (j (h (e12)))) ((j (e21)) = (e10)) ((h (e12)) = (e21)) ### Trans-sym 42 3 % 27.80/28.02 44. ((e10) != (e12)) ((j (h (e12))) = (e12)) ((h (e12)) = (e21)) ((j (e21)) = (e10)) ### TransEq 43 23 23 % 27.80/28.02 45. ((e11) != (j (h (e12)))) ((j (e21)) = (e11)) ((h (e12)) = (e21)) ### Trans-sym 42 5 % 27.80/28.02 46. ((e11) != (e12)) ((j (h (e12))) = (e12)) ((h (e12)) = (e21)) ((j (e21)) = (e11)) ### TransEq 45 23 23 % 27.80/28.02 47. ((h (e11)) = (e21)) ((h (e11)) != (e21)) ### Axiom % 27.80/28.02 48. ((j (h (e11))) != (j (e21))) ((h (e11)) = (e21)) ### NotEqual 47 % 27.80/28.02 49. ((e12) != (j (h (e11)))) ((j (e21)) = (e12)) ((h (e11)) = (e21)) ### Trans-sym 48 23 % 27.80/28.02 50. ((e11) != (e12)) ((j (h (e11))) = (e11)) ((h (e11)) = (e21)) ((j (e21)) = (e12)) ### TransEq-sym 49 5 5 % 27.80/28.02 51. ((e13) != (j (h (e11)))) ((j (e21)) = (e13)) ((h (e11)) = (e21)) ### Trans-sym 48 30 % 27.80/28.02 52. ((e11) != (e13)) ((j (h (e11))) = (e11)) ((h (e11)) = (e21)) ((j (e21)) = (e13)) ### TransEq-sym 51 5 5 % 27.80/28.02 53. (((j (e21)) = (e10)) \/ (((j (e21)) = (e11)) \/ (((j (e21)) = (e12)) \/ ((j (e21)) = (e13))))) ((e11) != (e13)) ((h (e11)) = (e21)) ((j (h (e11))) = (e11)) ((e11) != (e12)) ((h (e12)) = (e21)) ((j (h (e12))) = (e12)) ((e10) != (e12)) ### DisjTree 44 46 50 52 % 27.80/28.02 54. ((h (e13)) = (e20)) ((h (e13)) != (e20)) ### Axiom % 27.80/28.02 55. ((j (h (e13))) != (j (e20))) ((h (e13)) = (e20)) ### NotEqual 54 % 27.80/28.02 56. ((e10) != (j (h (e13)))) ((j (e20)) = (e10)) ((h (e13)) = (e20)) ### Trans-sym 55 3 % 27.80/28.02 57. ((e10) != (e13)) ((j (h (e13))) = (e13)) ((h (e13)) = (e20)) ((j (e20)) = (e10)) ### TransEq 56 30 30 % 27.80/28.02 58. ((e11) != (j (h (e13)))) ((j (e20)) = (e11)) ((h (e13)) = (e20)) ### Trans-sym 55 5 % 27.80/28.02 59. ((e11) != (e13)) ((j (h (e13))) = (e13)) ((h (e13)) = (e20)) ((j (e20)) = (e11)) ### TransEq 58 30 30 % 27.80/28.02 60. ((e12) != (j (h (e13)))) ((j (e20)) = (e12)) ((h (e13)) = (e20)) ### Trans-sym 55 23 % 27.80/28.02 61. ((e12) != (e13)) ((j (h (e13))) = (e13)) ((h (e13)) = (e20)) ((j (e20)) = (e12)) ### TransEq 60 30 30 % 27.80/28.02 62. (((j (e20)) = (e10)) \/ (((j (e20)) = (e11)) \/ (((j (e20)) = (e12)) \/ ((j (e20)) = (e13))))) ((op2 (e20) (e20)) = (e20)) ((j (op2 (e20) (e20))) = (op1 (j (e20)) (j (e20)))) ((op1 (e13) (e13)) = (e10)) ((e12) != (e13)) ((e11) != (e13)) ((h (e13)) = (e20)) ((j (h (e13))) = (e13)) ((e10) != (e13)) ### DisjTree 57 59 61 32 % 27.80/28.02 63. ((h (e13)) = (e21)) ((h (e13)) != (e21)) ### Axiom % 27.80/28.02 64. ((j (h (e13))) != (j (e21))) ((h (e13)) = (e21)) ### NotEqual 63 % 27.80/28.02 65. ((e10) != (j (h (e13)))) ((j (e21)) = (e10)) ((h (e13)) = (e21)) ### Trans-sym 64 3 % 27.80/28.02 66. ((e10) != (e13)) ((j (h (e13))) = (e13)) ((h (e13)) = (e21)) ((j (e21)) = (e10)) ### TransEq 65 30 30 % 27.80/28.02 67. ((e11) != (j (h (e13)))) ((j (e21)) = (e11)) ((h (e13)) = (e21)) ### Trans-sym 64 5 % 27.80/28.02 68. ((e11) != (e13)) ((j (h (e13))) = (e13)) ((h (e13)) = (e21)) ((j (e21)) = (e11)) ### TransEq 67 30 30 % 27.80/28.02 69. ((e12) != (j (h (e13)))) ((j (e21)) = (e12)) ((h (e13)) = (e21)) ### Trans-sym 64 23 % 27.80/28.02 70. ((e12) != (e13)) ((j (h (e13))) = (e13)) ((h (e13)) = (e21)) ((j (e21)) = (e12)) ### TransEq 69 30 30 % 27.80/28.02 71. (((j (e21)) = (e10)) \/ (((j (e21)) = (e11)) \/ (((j (e21)) = (e12)) \/ ((j (e21)) = (e13))))) ((h (e11)) = (e21)) ((j (h (e11))) = (e11)) ((e12) != (e13)) ((e11) != (e13)) ((h (e13)) = (e21)) ((j (h (e13))) = (e13)) ((e10) != (e13)) ### DisjTree 66 68 70 52 % 27.80/28.02 72. ((h (e13)) = (e22)) ((h (e13)) != (e22)) ### Axiom % 27.80/28.02 73. ((j (h (e13))) != (j (e22))) ((h (e13)) = (e22)) ### NotEqual 72 % 27.80/28.02 74. ((e10) != (j (h (e13)))) ((j (e22)) = (e10)) ((h (e13)) = (e22)) ### Trans-sym 73 3 % 27.80/28.02 75. ((e10) != (e13)) ((j (h (e13))) = (e13)) ((h (e13)) = (e22)) ((j (e22)) = (e10)) ### TransEq 74 30 30 % 27.80/28.02 76. ((e11) != (j (h (e13)))) ((j (e22)) = (e11)) ((h (e13)) = (e22)) ### Trans-sym 73 5 % 27.80/28.02 77. ((e11) != (e13)) ((j (h (e13))) = (e13)) ((h (e13)) = (e22)) ((j (e22)) = (e11)) ### TransEq 76 30 30 % 27.80/28.02 78. ((e12) != (j (h (e13)))) ((j (e22)) = (e12)) ((h (e13)) = (e22)) ### Trans-sym 73 23 % 27.80/28.02 79. ((e12) != (e13)) ((j (h (e13))) = (e13)) ((h (e13)) = (e22)) ((j (e22)) = (e12)) ### TransEq 78 30 30 % 27.80/28.02 80. ((h (e12)) = (e22)) ((h (e12)) != (e22)) ### Axiom % 27.80/28.02 81. ((j (h (e12))) != (j (e22))) ((h (e12)) = (e22)) ### NotEqual 80 % 27.80/28.02 82. ((e13) != (j (h (e12)))) ((j (e22)) = (e13)) ((h (e12)) = (e22)) ### Trans-sym 81 30 % 27.80/28.02 83. ((e12) != (e13)) ((j (h (e12))) = (e12)) ((h (e12)) = (e22)) ((j (e22)) = (e13)) ### TransEq-sym 82 23 23 % 27.80/28.02 84. (((j (e22)) = (e10)) \/ (((j (e22)) = (e11)) \/ (((j (e22)) = (e12)) \/ ((j (e22)) = (e13))))) ((h (e12)) = (e22)) ((j (h (e12))) = (e12)) ((e12) != (e13)) ((e11) != (e13)) ((h (e13)) = (e22)) ((j (h (e13))) = (e13)) ((e10) != (e13)) ### DisjTree 75 77 79 83 % 27.80/28.02 85. ((e10) != (j (h (e11)))) ((j (e21)) = (e10)) ((h (e11)) = (e21)) ### Trans-sym 48 3 % 27.80/28.02 86. ((e10) != (e11)) ((j (h (e11))) = (e11)) ((h (e11)) = (e21)) ((j (e21)) = (e10)) ### TransEq 85 5 5 % 27.80/28.02 87. ((h (e13)) = (e23)) ((h (e13)) != (e23)) ### Axiom % 27.80/28.02 88. ((j (h (e13))) != (j (e23))) ((h (e13)) = (e23)) ### NotEqual 87 % 27.80/28.02 89. ((e10) != (j (h (e13)))) ((j (e23)) = (e10)) ((h (e13)) = (e23)) ### Trans-sym 88 3 % 27.80/28.02 90. ((e10) != (e13)) ((j (h (e13))) = (e13)) ((h (e13)) = (e23)) ((j (e23)) = (e10)) ### TransEq 89 30 30 % 27.80/28.02 91. ((e11) != (j (h (e13)))) ((j (e23)) = (e11)) ((h (e13)) = (e23)) ### Trans-sym 88 5 % 27.80/28.02 92. ((e11) != (e13)) ((j (h (e13))) = (e13)) ((h (e13)) = (e23)) ((j (e23)) = (e11)) ### TransEq 91 30 30 % 27.80/28.02 93. ((op2 (e21) (e21)) = (e23)) ((e23) != (op2 (e21) (e21))) ### Sym(=) % 27.80/28.02 94. ((j (e23)) != (j (op2 (e21) (e21)))) ((op2 (e21) (e21)) = (e23)) ### NotEqual 93 % 27.80/28.02 95. ((j (e21)) = (e11)) ((j (e21)) != (e11)) ### Axiom % 27.80/28.02 96. ((j (e21)) = (e11)) ((j (e21)) != (e11)) ### Axiom % 27.80/28.02 97. ((op1 (j (e21)) (j (e21))) != (op1 (e11) (e11))) ((j (e21)) = (e11)) ### NotEqual 95 96 % 27.80/28.02 98. ((op1 (e13) (e13)) = (e10)) ((e10) != (op1 (e13) (e13))) ### Sym(=) % 27.80/28.02 99. ((op1 (j (e21)) (j (e21))) != (op1 (e13) (e13))) ((op1 (e11) (e11)) = (e10)) ((op1 (e13) (e13)) = (e10)) ((j (e21)) = (e11)) ### Trans 97 98 % 27.80/28.02 100. ((op1 (e13) (e13)) != (j (e23))) ((j (op2 (e21) (e21))) = (op1 (j (e21)) (j (e21)))) ((j (e21)) = (e11)) ((op1 (e13) (e13)) = (e10)) ((op1 (e11) (e11)) = (e10)) ((op2 (e21) (e21)) = (e23)) ### Trans-sym 94 99 % 27.80/28.02 101. ((e12) != (op1 (e13) (e13))) ((j (e23)) = (e12)) ((op2 (e21) (e21)) = (e23)) ((op1 (e11) (e11)) = (e10)) ((op1 (e13) (e13)) = (e10)) ((j (e21)) = (e11)) ((j (op2 (e21) (e21))) = (op1 (j (e21)) (j (e21)))) ### Trans-sym 100 23 % 27.80/28.02 102. ((e10) != (e12)) ((j (op2 (e21) (e21))) = (op1 (j (e21)) (j (e21)))) ((j (e21)) = (e11)) ((op1 (e13) (e13)) = (e10)) ((op1 (e11) (e11)) = (e10)) ((op2 (e21) (e21)) = (e23)) ((j (e23)) = (e12)) ### TransEq-sym 101 3 3 % 27.80/28.02 103. ((e13) != (op1 (e13) (e13))) ((j (e23)) = (e13)) ((op2 (e21) (e21)) = (e23)) ((op1 (e11) (e11)) = (e10)) ((op1 (e13) (e13)) = (e10)) ((j (e21)) = (e11)) ((j (op2 (e21) (e21))) = (op1 (j (e21)) (j (e21)))) ### Trans-sym 100 30 % 27.80/28.02 104. ((e10) != (e13)) ((j (op2 (e21) (e21))) = (op1 (j (e21)) (j (e21)))) ((j (e21)) = (e11)) ((op1 (e13) (e13)) = (e10)) ((op1 (e11) (e11)) = (e10)) ((op2 (e21) (e21)) = (e23)) ((j (e23)) = (e13)) ### TransEq-sym 103 3 3 % 27.80/28.02 105. (((j (e23)) = (e10)) \/ (((j (e23)) = (e11)) \/ (((j (e23)) = (e12)) \/ ((j (e23)) = (e13))))) ((op2 (e21) (e21)) = (e23)) ((op1 (e11) (e11)) = (e10)) ((op1 (e13) (e13)) = (e10)) ((j (e21)) = (e11)) ((j (op2 (e21) (e21))) = (op1 (j (e21)) (j (e21)))) ((e10) != (e12)) ((e11) != (e13)) ((h (e13)) = (e23)) ((j (h (e13))) = (e13)) ((e10) != (e13)) ### DisjTree 90 92 102 104 % 27.80/28.02 106. ((e12) != (j (h (e13)))) ((j (e23)) = (e12)) ((h (e13)) = (e23)) ### Trans-sym 88 23 % 27.80/28.02 107. ((e12) != (e13)) ((j (h (e13))) = (e13)) ((h (e13)) = (e23)) ((j (e23)) = (e12)) ### TransEq 106 30 30 % 27.80/28.02 108. ((j (e21)) = (e12)) ((j (e21)) != (e12)) ### Axiom % 27.80/28.02 109. ((j (e21)) = (e12)) ((j (e21)) != (e12)) ### Axiom % 27.80/28.02 110. ((op1 (j (e21)) (j (e21))) != (op1 (e12) (e12))) ((j (e21)) = (e12)) ### NotEqual 108 109 % 27.80/28.02 111. ((op1 (e13) (e13)) = (e10)) ((e10) != (op1 (e13) (e13))) ### Sym(=) % 27.80/28.02 112. ((op1 (j (e21)) (j (e21))) != (op1 (e13) (e13))) ((op1 (e12) (e12)) = (e10)) ((op1 (e13) (e13)) = (e10)) ((j (e21)) = (e12)) ### Trans 110 111 % 27.80/28.02 113. ((op1 (e13) (e13)) != (j (e23))) ((j (op2 (e21) (e21))) = (op1 (j (e21)) (j (e21)))) ((j (e21)) = (e12)) ((op1 (e13) (e13)) = (e10)) ((op1 (e12) (e12)) = (e10)) ((op2 (e21) (e21)) = (e23)) ### Trans-sym 94 112 % 27.80/28.02 114. ((e13) != (op1 (e13) (e13))) ((j (e23)) = (e13)) ((op2 (e21) (e21)) = (e23)) ((op1 (e12) (e12)) = (e10)) ((op1 (e13) (e13)) = (e10)) ((j (e21)) = (e12)) ((j (op2 (e21) (e21))) = (op1 (j (e21)) (j (e21)))) ### Trans-sym 113 30 % 27.80/28.02 115. ((e10) != (e13)) ((j (op2 (e21) (e21))) = (op1 (j (e21)) (j (e21)))) ((j (e21)) = (e12)) ((op1 (e13) (e13)) = (e10)) ((op1 (e12) (e12)) = (e10)) ((op2 (e21) (e21)) = (e23)) ((j (e23)) = (e13)) ### TransEq-sym 114 3 3 % 27.80/28.02 116. (((j (e23)) = (e10)) \/ (((j (e23)) = (e11)) \/ (((j (e23)) = (e12)) \/ ((j (e23)) = (e13))))) ((op2 (e21) (e21)) = (e23)) ((op1 (e12) (e12)) = (e10)) ((op1 (e13) (e13)) = (e10)) ((j (e21)) = (e12)) ((j (op2 (e21) (e21))) = (op1 (j (e21)) (j (e21)))) ((e12) != (e13)) ((e11) != (e13)) ((h (e13)) = (e23)) ((j (h (e13))) = (e13)) ((e10) != (e13)) ### DisjTree 90 92 107 115 % 27.80/28.02 117. (((j (e21)) = (e10)) \/ (((j (e21)) = (e11)) \/ (((j (e21)) = (e12)) \/ ((j (e21)) = (e13))))) ((e12) != (e13)) ((op1 (e12) (e12)) = (e10)) ((e10) != (e13)) ((j (h (e13))) = (e13)) ((h (e13)) = (e23)) ((e11) != (e13)) ((e10) != (e12)) ((j (op2 (e21) (e21))) = (op1 (j (e21)) (j (e21)))) ((op1 (e13) (e13)) = (e10)) ((op1 (e11) (e11)) = (e10)) ((op2 (e21) (e21)) = (e23)) (((j (e23)) = (e10)) \/ (((j (e23)) = (e11)) \/ (((j (e23)) = (e12)) \/ ((j (e23)) = (e13))))) ((h (e11)) = (e21)) ((j (h (e11))) = (e11)) ((e10) != (e11)) ### DisjTree 86 105 116 52 % 27.80/28.02 118. (((h (e13)) = (e20)) \/ (((h (e13)) = (e21)) \/ (((h (e13)) = (e22)) \/ ((h (e13)) = (e23))))) ((e10) != (e11)) (((j (e23)) = (e10)) \/ (((j (e23)) = (e11)) \/ (((j (e23)) = (e12)) \/ ((j (e23)) = (e13))))) ((op2 (e21) (e21)) = (e23)) ((op1 (e11) (e11)) = (e10)) ((j (op2 (e21) (e21))) = (op1 (j (e21)) (j (e21)))) ((e10) != (e12)) ((op1 (e12) (e12)) = (e10)) ((j (h (e12))) = (e12)) ((h (e12)) = (e22)) (((j (e22)) = (e10)) \/ (((j (e22)) = (e11)) \/ (((j (e22)) = (e12)) \/ ((j (e22)) = (e13))))) ((j (h (e11))) = (e11)) ((h (e11)) = (e21)) (((j (e21)) = (e10)) \/ (((j (e21)) = (e11)) \/ (((j (e21)) = (e12)) \/ ((j (e21)) = (e13))))) ((e10) != (e13)) ((j (h (e13))) = (e13)) ((e11) != (e13)) ((e12) != (e13)) ((op1 (e13) (e13)) = (e10)) ((j (op2 (e20) (e20))) = (op1 (j (e20)) (j (e20)))) ((op2 (e20) (e20)) = (e20)) (((j (e20)) = (e10)) \/ (((j (e20)) = (e11)) \/ (((j (e20)) = (e12)) \/ ((j (e20)) = (e13))))) ### DisjTree 62 71 84 117 % 27.80/28.02 119. ((h (e12)) = (e23)) ((h (e12)) != (e23)) ### Axiom % 27.80/28.02 120. ((j (h (e12))) != (j (e23))) ((h (e12)) = (e23)) ### NotEqual 119 % 27.80/28.02 121. ((e10) != (j (h (e12)))) ((j (e23)) = (e10)) ((h (e12)) = (e23)) ### Trans-sym 120 3 % 27.80/28.02 122. ((e10) != (e12)) ((j (h (e12))) = (e12)) ((h (e12)) = (e23)) ((j (e23)) = (e10)) ### TransEq 121 23 23 % 27.80/28.02 123. ((e11) != (j (h (e12)))) ((j (e23)) = (e11)) ((h (e12)) = (e23)) ### Trans-sym 120 5 % 27.80/28.02 124. ((e11) != (e12)) ((j (h (e12))) = (e12)) ((h (e12)) = (e23)) ((j (e23)) = (e11)) ### TransEq 123 23 23 % 27.80/28.02 125. ((e13) != (j (h (e12)))) ((j (e23)) = (e13)) ((h (e12)) = (e23)) ### Trans-sym 120 30 % 27.80/28.02 126. ((e12) != (e13)) ((j (h (e12))) = (e12)) ((h (e12)) = (e23)) ((j (e23)) = (e13)) ### TransEq-sym 125 23 23 % 27.80/28.02 127. (((j (e23)) = (e10)) \/ (((j (e23)) = (e11)) \/ (((j (e23)) = (e12)) \/ ((j (e23)) = (e13))))) ((e12) != (e13)) ((op2 (e21) (e21)) = (e23)) ((op1 (e11) (e11)) = (e10)) ((op1 (e13) (e13)) = (e10)) ((j (e21)) = (e11)) ((j (op2 (e21) (e21))) = (op1 (j (e21)) (j (e21)))) ((e11) != (e12)) ((h (e12)) = (e23)) ((j (h (e12))) = (e12)) ((e10) != (e12)) ### DisjTree 122 124 102 126 % 27.80/28.02 128. ((j (e21)) = (e13)) ((j (e21)) != (e13)) ### Axiom % 27.80/28.02 129. ((j (e21)) = (e13)) ((j (e21)) != (e13)) ### Axiom % 27.80/28.02 130. ((op1 (j (e21)) (j (e21))) != (op1 (e13) (e13))) ((j (e21)) = (e13)) ### NotEqual 128 129 % 27.80/28.02 131. ((op1 (e13) (e13)) != (j (e23))) ((j (op2 (e21) (e21))) = (op1 (j (e21)) (j (e21)))) ((j (e21)) = (e13)) ((op2 (e21) (e21)) = (e23)) ### Trans-sym 94 130 % 27.80/28.02 132. ((e11) != (op1 (e13) (e13))) ((j (e23)) = (e11)) ((op2 (e21) (e21)) = (e23)) ((j (e21)) = (e13)) ((j (op2 (e21) (e21))) = (op1 (j (e21)) (j (e21)))) ### Trans-sym 131 5 % 27.80/28.02 133. ((e10) != (e11)) ((op1 (e13) (e13)) = (e10)) ((j (op2 (e21) (e21))) = (op1 (j (e21)) (j (e21)))) ((j (e21)) = (e13)) ((op2 (e21) (e21)) = (e23)) ((j (e23)) = (e11)) ### TransEq-sym 132 3 3 % 27.80/28.02 134. ((e12) != (op1 (e13) (e13))) ((j (e23)) = (e12)) ((op2 (e21) (e21)) = (e23)) ((j (e21)) = (e13)) ((j (op2 (e21) (e21))) = (op1 (j (e21)) (j (e21)))) ### Trans-sym 131 23 % 27.80/28.02 135. ((e10) != (e12)) ((op1 (e13) (e13)) = (e10)) ((j (op2 (e21) (e21))) = (op1 (j (e21)) (j (e21)))) ((j (e21)) = (e13)) ((op2 (e21) (e21)) = (e23)) ((j (e23)) = (e12)) ### TransEq-sym 134 3 3 % 27.80/28.02 136. (((j (e23)) = (e10)) \/ (((j (e23)) = (e11)) \/ (((j (e23)) = (e12)) \/ ((j (e23)) = (e13))))) ((e12) != (e13)) ((op2 (e21) (e21)) = (e23)) ((j (e21)) = (e13)) ((j (op2 (e21) (e21))) = (op1 (j (e21)) (j (e21)))) ((op1 (e13) (e13)) = (e10)) ((e10) != (e11)) ((h (e12)) = (e23)) ((j (h (e12))) = (e12)) ((e10) != (e12)) ### DisjTree 122 133 135 126 % 27.80/28.02 137. (((j (e21)) = (e10)) \/ (((j (e21)) = (e11)) \/ (((j (e21)) = (e12)) \/ ((j (e21)) = (e13))))) ((e10) != (e12)) ((j (h (e12))) = (e12)) ((h (e12)) = (e23)) ((e11) != (e12)) ((j (op2 (e21) (e21))) = (op1 (j (e21)) (j (e21)))) ((op1 (e13) (e13)) = (e10)) ((op1 (e11) (e11)) = (e10)) ((op2 (e21) (e21)) = (e23)) ((e12) != (e13)) (((j (e23)) = (e10)) \/ (((j (e23)) = (e11)) \/ (((j (e23)) = (e12)) \/ ((j (e23)) = (e13))))) ((h (e11)) = (e21)) ((j (h (e11))) = (e11)) ((e10) != (e11)) ### DisjTree 86 127 50 136 % 27.80/28.02 138. (((h (e12)) = (e20)) \/ (((h (e12)) = (e21)) \/ (((h (e12)) = (e22)) \/ ((h (e12)) = (e23))))) ((e12) != (e13)) ((j (h (e13))) = (e13)) (((j (e22)) = (e10)) \/ (((j (e22)) = (e11)) \/ (((j (e22)) = (e12)) \/ ((j (e22)) = (e13))))) ((j (op2 (e21) (e21))) = (op1 (j (e21)) (j (e21)))) ((op1 (e11) (e11)) = (e10)) ((op2 (e21) (e21)) = (e23)) (((j (e23)) = (e10)) \/ (((j (e23)) = (e11)) \/ (((j (e23)) = (e12)) \/ ((j (e23)) = (e13))))) ((e10) != (e11)) (((h (e13)) = (e20)) \/ (((h (e13)) = (e21)) \/ (((h (e13)) = (e22)) \/ ((h (e13)) = (e23))))) ((j (h (e11))) = (e11)) ((h (e11)) = (e21)) ((e11) != (e13)) (((j (e21)) = (e10)) \/ (((j (e21)) = (e11)) \/ (((j (e21)) = (e12)) \/ ((j (e21)) = (e13))))) ((e10) != (e12)) ((j (h (e12))) = (e12)) ((e11) != (e12)) ((j (op2 (e20) (e20))) = (op1 (j (e20)) (j (e20)))) ((op1 (e13) (e13)) = (e10)) ((op1 (e12) (e12)) = (e10)) ((op2 (e20) (e20)) = (e20)) ((e10) != (e13)) (((j (e20)) = (e10)) \/ (((j (e20)) = (e11)) \/ (((j (e20)) = (e12)) \/ ((j (e20)) = (e13))))) ### DisjTree 40 53 118 137 % 27.80/28.02 139. ((e13) != (j (h (e12)))) ((j (e21)) = (e13)) ((h (e12)) = (e21)) ### Trans-sym 42 30 % 27.80/28.02 140. ((e12) != (e13)) ((j (h (e12))) = (e12)) ((h (e12)) = (e21)) ((j (e21)) = (e13)) ### TransEq-sym 139 23 23 % 27.80/28.02 141. (((j (e21)) = (e10)) \/ (((j (e21)) = (e11)) \/ (((j (e21)) = (e12)) \/ ((j (e21)) = (e13))))) ((h (e12)) = (e21)) ((j (h (e12))) = (e12)) ((e12) != (e13)) ((e11) != (e13)) ((h (e13)) = (e21)) ((j (h (e13))) = (e13)) ((e10) != (e13)) ### DisjTree 66 68 70 140 % 27.80/28.02 142. ((h (e11)) = (e22)) ((h (e11)) != (e22)) ### Axiom % 27.80/28.02 143. ((j (h (e11))) != (j (e22))) ((h (e11)) = (e22)) ### NotEqual 142 % 27.80/28.02 144. ((e13) != (j (h (e11)))) ((j (e22)) = (e13)) ((h (e11)) = (e22)) ### Trans-sym 143 30 % 27.80/28.02 145. ((e11) != (e13)) ((j (h (e11))) = (e11)) ((h (e11)) = (e22)) ((j (e22)) = (e13)) ### TransEq-sym 144 5 5 % 27.80/28.02 146. (((j (e22)) = (e10)) \/ (((j (e22)) = (e11)) \/ (((j (e22)) = (e12)) \/ ((j (e22)) = (e13))))) ((h (e11)) = (e22)) ((j (h (e11))) = (e11)) ((e12) != (e13)) ((e11) != (e13)) ((h (e13)) = (e22)) ((j (h (e13))) = (e13)) ((e10) != (e13)) ### DisjTree 75 77 79 145 % 27.80/28.02 147. (((j (e21)) = (e10)) \/ (((j (e21)) = (e11)) \/ (((j (e21)) = (e12)) \/ ((j (e21)) = (e13))))) ((e10) != (e13)) ((j (h (e13))) = (e13)) ((h (e13)) = (e23)) ((e11) != (e13)) ((e12) != (e13)) ((j (op2 (e21) (e21))) = (op1 (j (e21)) (j (e21)))) ((op1 (e13) (e13)) = (e10)) ((op1 (e12) (e12)) = (e10)) ((op2 (e21) (e21)) = (e23)) (((j (e23)) = (e10)) \/ (((j (e23)) = (e11)) \/ (((j (e23)) = (e12)) \/ ((j (e23)) = (e13))))) ((e11) != (e12)) ((h (e12)) = (e21)) ((j (h (e12))) = (e12)) ((e10) != (e12)) ### DisjTree 44 46 116 140 % 27.80/28.02 148. (((h (e13)) = (e20)) \/ (((h (e13)) = (e21)) \/ (((h (e13)) = (e22)) \/ ((h (e13)) = (e23))))) ((e10) != (e12)) ((e11) != (e12)) (((j (e23)) = (e10)) \/ (((j (e23)) = (e11)) \/ (((j (e23)) = (e12)) \/ ((j (e23)) = (e13))))) ((op2 (e21) (e21)) = (e23)) ((op1 (e12) (e12)) = (e10)) ((j (op2 (e21) (e21))) = (op1 (j (e21)) (j (e21)))) ((j (h (e11))) = (e11)) ((h (e11)) = (e22)) (((j (e22)) = (e10)) \/ (((j (e22)) = (e11)) \/ (((j (e22)) = (e12)) \/ ((j (e22)) = (e13))))) ((j (h (e12))) = (e12)) ((h (e12)) = (e21)) (((j (e21)) = (e10)) \/ (((j (e21)) = (e11)) \/ (((j (e21)) = (e12)) \/ ((j (e21)) = (e13))))) ((e10) != (e13)) ((j (h (e13))) = (e13)) ((e11) != (e13)) ((e12) != (e13)) ((op1 (e13) (e13)) = (e10)) ((j (op2 (e20) (e20))) = (op1 (j (e20)) (j (e20)))) ((op2 (e20) (e20)) = (e20)) (((j (e20)) = (e10)) \/ (((j (e20)) = (e11)) \/ (((j (e20)) = (e12)) \/ ((j (e20)) = (e13))))) ### DisjTree 62 141 146 147 % 27.80/28.02 149. ((e10) != (j (h (e12)))) ((j (e22)) = (e10)) ((h (e12)) = (e22)) ### Trans-sym 81 3 % 27.80/28.02 150. ((e10) != (e12)) ((j (h (e12))) = (e12)) ((h (e12)) = (e22)) ((j (e22)) = (e10)) ### TransEq 149 23 23 % 27.80/28.02 151. ((e11) != (j (h (e12)))) ((j (e22)) = (e11)) ((h (e12)) = (e22)) ### Trans-sym 81 5 % 27.80/28.02 152. ((e11) != (e12)) ((j (h (e12))) = (e12)) ((h (e12)) = (e22)) ((j (e22)) = (e11)) ### TransEq 151 23 23 % 27.80/28.02 153. ((e12) != (j (h (e11)))) ((j (e22)) = (e12)) ((h (e11)) = (e22)) ### Trans-sym 143 23 % 27.80/28.02 154. ((e11) != (e12)) ((j (h (e11))) = (e11)) ((h (e11)) = (e22)) ((j (e22)) = (e12)) ### TransEq-sym 153 5 5 % 27.80/28.02 155. (((j (e22)) = (e10)) \/ (((j (e22)) = (e11)) \/ (((j (e22)) = (e12)) \/ ((j (e22)) = (e13))))) ((e12) != (e13)) ((h (e11)) = (e22)) ((j (h (e11))) = (e11)) ((e11) != (e12)) ((h (e12)) = (e22)) ((j (h (e12))) = (e12)) ((e10) != (e12)) ### DisjTree 150 152 154 83 % 27.80/28.02 156. (((j (e21)) = (e10)) \/ (((j (e21)) = (e11)) \/ (((j (e21)) = (e12)) \/ ((j (e21)) = (e13))))) ((e10) != (e12)) ((j (h (e12))) = (e12)) ((h (e12)) = (e23)) ((e10) != (e11)) ((op1 (e13) (e13)) = (e10)) ((j (op2 (e21) (e21))) = (op1 (j (e21)) (j (e21)))) ((op2 (e21) (e21)) = (e23)) (((j (e23)) = (e10)) \/ (((j (e23)) = (e11)) \/ (((j (e23)) = (e12)) \/ ((j (e23)) = (e13))))) ((e12) != (e13)) ((e11) != (e13)) ((h (e13)) = (e21)) ((j (h (e13))) = (e13)) ((e10) != (e13)) ### DisjTree 66 68 70 136 % 27.80/28.02 157. (((j (e23)) = (e10)) \/ (((j (e23)) = (e11)) \/ (((j (e23)) = (e12)) \/ ((j (e23)) = (e13))))) ((h (e12)) = (e23)) ((j (h (e12))) = (e12)) ((e12) != (e13)) ((e11) != (e13)) ((h (e13)) = (e23)) ((j (h (e13))) = (e13)) ((e10) != (e13)) ### DisjTree 90 92 107 126 % 27.80/28.02 158. (((h (e13)) = (e20)) \/ (((h (e13)) = (e21)) \/ (((h (e13)) = (e22)) \/ ((h (e13)) = (e23))))) ((j (h (e11))) = (e11)) ((h (e11)) = (e22)) (((j (e22)) = (e10)) \/ (((j (e22)) = (e11)) \/ (((j (e22)) = (e12)) \/ ((j (e22)) = (e13))))) (((j (e23)) = (e10)) \/ (((j (e23)) = (e11)) \/ (((j (e23)) = (e12)) \/ ((j (e23)) = (e13))))) ((op2 (e21) (e21)) = (e23)) ((j (op2 (e21) (e21))) = (op1 (j (e21)) (j (e21)))) ((e10) != (e11)) ((h (e12)) = (e23)) ((j (h (e12))) = (e12)) ((e10) != (e12)) (((j (e21)) = (e10)) \/ (((j (e21)) = (e11)) \/ (((j (e21)) = (e12)) \/ ((j (e21)) = (e13))))) ((e10) != (e13)) ((j (h (e13))) = (e13)) ((e11) != (e13)) ((e12) != (e13)) ((op1 (e13) (e13)) = (e10)) ((j (op2 (e20) (e20))) = (op1 (j (e20)) (j (e20)))) ((op2 (e20) (e20)) = (e20)) (((j (e20)) = (e10)) \/ (((j (e20)) = (e11)) \/ (((j (e20)) = (e12)) \/ ((j (e20)) = (e13))))) ### DisjTree 62 156 146 157 % 27.80/28.02 159. (((h (e12)) = (e20)) \/ (((h (e12)) = (e21)) \/ (((h (e12)) = (e22)) \/ ((h (e12)) = (e23))))) ((e10) != (e11)) ((e12) != (e13)) ((e11) != (e13)) ((j (h (e13))) = (e13)) (((j (e21)) = (e10)) \/ (((j (e21)) = (e11)) \/ (((j (e21)) = (e12)) \/ ((j (e21)) = (e13))))) (((j (e22)) = (e10)) \/ (((j (e22)) = (e11)) \/ (((j (e22)) = (e12)) \/ ((j (e22)) = (e13))))) ((h (e11)) = (e22)) ((j (h (e11))) = (e11)) ((j (op2 (e21) (e21))) = (op1 (j (e21)) (j (e21)))) ((op2 (e21) (e21)) = (e23)) (((j (e23)) = (e10)) \/ (((j (e23)) = (e11)) \/ (((j (e23)) = (e12)) \/ ((j (e23)) = (e13))))) (((h (e13)) = (e20)) \/ (((h (e13)) = (e21)) \/ (((h (e13)) = (e22)) \/ ((h (e13)) = (e23))))) ((e10) != (e12)) ((j (h (e12))) = (e12)) ((e11) != (e12)) ((j (op2 (e20) (e20))) = (op1 (j (e20)) (j (e20)))) ((op1 (e13) (e13)) = (e10)) ((op1 (e12) (e12)) = (e10)) ((op2 (e20) (e20)) = (e20)) ((e10) != (e13)) (((j (e20)) = (e10)) \/ (((j (e20)) = (e11)) \/ (((j (e20)) = (e12)) \/ ((j (e20)) = (e13))))) ### DisjTree 40 148 155 158 % 27.80/28.02 160. ((h (e11)) = (e23)) ((h (e11)) != (e23)) ### Axiom % 27.80/28.02 161. ((j (h (e11))) != (j (e23))) ((h (e11)) = (e23)) ### NotEqual 160 % 27.80/28.02 162. ((e10) != (j (h (e11)))) ((j (e23)) = (e10)) ((h (e11)) = (e23)) ### Trans-sym 161 3 % 27.80/28.02 163. ((e10) != (e11)) ((j (h (e11))) = (e11)) ((h (e11)) = (e23)) ((j (e23)) = (e10)) ### TransEq 162 5 5 % 27.80/28.02 164. ((e11) != (op1 (e13) (e13))) ((j (e23)) = (e11)) ((op2 (e21) (e21)) = (e23)) ((op1 (e12) (e12)) = (e10)) ((op1 (e13) (e13)) = (e10)) ((j (e21)) = (e12)) ((j (op2 (e21) (e21))) = (op1 (j (e21)) (j (e21)))) ### Trans-sym 113 5 % 27.80/28.02 165. ((e10) != (e11)) ((j (op2 (e21) (e21))) = (op1 (j (e21)) (j (e21)))) ((j (e21)) = (e12)) ((op1 (e13) (e13)) = (e10)) ((op1 (e12) (e12)) = (e10)) ((op2 (e21) (e21)) = (e23)) ((j (e23)) = (e11)) ### TransEq-sym 164 3 3 % 27.80/28.02 166. ((e12) != (j (h (e11)))) ((j (e23)) = (e12)) ((h (e11)) = (e23)) ### Trans-sym 161 23 % 27.80/28.02 167. ((e11) != (e12)) ((j (h (e11))) = (e11)) ((h (e11)) = (e23)) ((j (e23)) = (e12)) ### TransEq-sym 166 5 5 % 27.80/28.02 168. ((e13) != (j (h (e11)))) ((j (e23)) = (e13)) ((h (e11)) = (e23)) ### Trans-sym 161 30 % 27.80/28.02 169. ((e11) != (e13)) ((j (h (e11))) = (e11)) ((h (e11)) = (e23)) ((j (e23)) = (e13)) ### TransEq-sym 168 5 5 % 27.80/28.02 170. (((j (e23)) = (e10)) \/ (((j (e23)) = (e11)) \/ (((j (e23)) = (e12)) \/ ((j (e23)) = (e13))))) ((e11) != (e13)) ((e11) != (e12)) ((op2 (e21) (e21)) = (e23)) ((op1 (e12) (e12)) = (e10)) ((op1 (e13) (e13)) = (e10)) ((j (e21)) = (e12)) ((j (op2 (e21) (e21))) = (op1 (j (e21)) (j (e21)))) ((h (e11)) = (e23)) ((j (h (e11))) = (e11)) ((e10) != (e11)) ### DisjTree 163 165 167 169 % 27.80/28.02 171. (((j (e23)) = (e10)) \/ (((j (e23)) = (e11)) \/ (((j (e23)) = (e12)) \/ ((j (e23)) = (e13))))) ((e11) != (e13)) ((e11) != (e12)) ((op2 (e21) (e21)) = (e23)) ((j (e21)) = (e13)) ((j (op2 (e21) (e21))) = (op1 (j (e21)) (j (e21)))) ((op1 (e13) (e13)) = (e10)) ((h (e11)) = (e23)) ((j (h (e11))) = (e11)) ((e10) != (e11)) ### DisjTree 163 133 167 169 % 27.80/28.02 172. (((j (e21)) = (e10)) \/ (((j (e21)) = (e11)) \/ (((j (e21)) = (e12)) \/ ((j (e21)) = (e13))))) ((e10) != (e11)) ((j (h (e11))) = (e11)) ((h (e11)) = (e23)) ((j (op2 (e21) (e21))) = (op1 (j (e21)) (j (e21)))) ((op1 (e13) (e13)) = (e10)) ((op1 (e12) (e12)) = (e10)) ((op2 (e21) (e21)) = (e23)) ((e11) != (e13)) (((j (e23)) = (e10)) \/ (((j (e23)) = (e11)) \/ (((j (e23)) = (e12)) \/ ((j (e23)) = (e13))))) ((e11) != (e12)) ((h (e12)) = (e21)) ((j (h (e12))) = (e12)) ((e10) != (e12)) ### DisjTree 44 46 170 171 % 27.80/28.02 173. (((j (e21)) = (e10)) \/ (((j (e21)) = (e11)) \/ (((j (e21)) = (e12)) \/ ((j (e21)) = (e13))))) ((e10) != (e11)) ((j (h (e11))) = (e11)) ((h (e11)) = (e23)) ((op1 (e13) (e13)) = (e10)) ((j (op2 (e21) (e21))) = (op1 (j (e21)) (j (e21)))) ((op2 (e21) (e21)) = (e23)) ((e11) != (e12)) (((j (e23)) = (e10)) \/ (((j (e23)) = (e11)) \/ (((j (e23)) = (e12)) \/ ((j (e23)) = (e13))))) ((e12) != (e13)) ((e11) != (e13)) ((h (e13)) = (e21)) ((j (h (e13))) = (e13)) ((e10) != (e13)) ### DisjTree 66 68 70 171 % 27.80/28.02 174. (((j (e23)) = (e10)) \/ (((j (e23)) = (e11)) \/ (((j (e23)) = (e12)) \/ ((j (e23)) = (e13))))) ((h (e11)) = (e23)) ((j (h (e11))) = (e11)) ((e12) != (e13)) ((e11) != (e13)) ((h (e13)) = (e23)) ((j (h (e13))) = (e13)) ((e10) != (e13)) ### DisjTree 90 92 107 169 % 27.80/28.02 175. (((h (e13)) = (e20)) \/ (((h (e13)) = (e21)) \/ (((h (e13)) = (e22)) \/ ((h (e13)) = (e23))))) ((j (h (e12))) = (e12)) ((h (e12)) = (e22)) (((j (e22)) = (e10)) \/ (((j (e22)) = (e11)) \/ (((j (e22)) = (e12)) \/ ((j (e22)) = (e13))))) (((j (e23)) = (e10)) \/ (((j (e23)) = (e11)) \/ (((j (e23)) = (e12)) \/ ((j (e23)) = (e13))))) ((e11) != (e12)) ((op2 (e21) (e21)) = (e23)) ((j (op2 (e21) (e21))) = (op1 (j (e21)) (j (e21)))) ((h (e11)) = (e23)) ((j (h (e11))) = (e11)) ((e10) != (e11)) (((j (e21)) = (e10)) \/ (((j (e21)) = (e11)) \/ (((j (e21)) = (e12)) \/ ((j (e21)) = (e13))))) ((e10) != (e13)) ((j (h (e13))) = (e13)) ((e11) != (e13)) ((e12) != (e13)) ((op1 (e13) (e13)) = (e10)) ((j (op2 (e20) (e20))) = (op1 (j (e20)) (j (e20)))) ((op2 (e20) (e20)) = (e20)) (((j (e20)) = (e10)) \/ (((j (e20)) = (e11)) \/ (((j (e20)) = (e12)) \/ ((j (e20)) = (e13))))) ### DisjTree 62 173 84 174 % 27.80/28.02 176. (((j (e23)) = (e10)) \/ (((j (e23)) = (e11)) \/ (((j (e23)) = (e12)) \/ ((j (e23)) = (e13))))) ((e12) != (e13)) ((h (e11)) = (e23)) ((j (h (e11))) = (e11)) ((e11) != (e12)) ((h (e12)) = (e23)) ((j (h (e12))) = (e12)) ((e10) != (e12)) ### DisjTree 122 124 167 126 % 27.80/28.02 177. (((h (e12)) = (e20)) \/ (((h (e12)) = (e21)) \/ (((h (e12)) = (e22)) \/ ((h (e12)) = (e23))))) ((e12) != (e13)) ((j (h (e13))) = (e13)) (((j (e22)) = (e10)) \/ (((j (e22)) = (e11)) \/ (((j (e22)) = (e12)) \/ ((j (e22)) = (e13))))) (((h (e13)) = (e20)) \/ (((h (e13)) = (e21)) \/ (((h (e13)) = (e22)) \/ ((h (e13)) = (e23))))) (((j (e23)) = (e10)) \/ (((j (e23)) = (e11)) \/ (((j (e23)) = (e12)) \/ ((j (e23)) = (e13))))) ((e11) != (e13)) ((op2 (e21) (e21)) = (e23)) ((j (op2 (e21) (e21))) = (op1 (j (e21)) (j (e21)))) ((h (e11)) = (e23)) ((j (h (e11))) = (e11)) ((e10) != (e11)) (((j (e21)) = (e10)) \/ (((j (e21)) = (e11)) \/ (((j (e21)) = (e12)) \/ ((j (e21)) = (e13))))) ((e10) != (e12)) ((j (h (e12))) = (e12)) ((e11) != (e12)) ((j (op2 (e20) (e20))) = (op1 (j (e20)) (j (e20)))) ((op1 (e13) (e13)) = (e10)) ((op1 (e12) (e12)) = (e10)) ((op2 (e20) (e20)) = (e20)) ((e10) != (e13)) (((j (e20)) = (e10)) \/ (((j (e20)) = (e11)) \/ (((j (e20)) = (e12)) \/ ((j (e20)) = (e13))))) ### DisjTree 40 172 175 176 % 27.80/28.02 178. (((h (e11)) = (e20)) \/ (((h (e11)) = (e21)) \/ (((h (e11)) = (e22)) \/ ((h (e11)) = (e23))))) ((e11) != (e12)) ((j (h (e12))) = (e12)) (((j (e21)) = (e10)) \/ (((j (e21)) = (e11)) \/ (((j (e21)) = (e12)) \/ ((j (e21)) = (e13))))) ((e11) != (e13)) (((h (e13)) = (e20)) \/ (((h (e13)) = (e21)) \/ (((h (e13)) = (e22)) \/ ((h (e13)) = (e23))))) (((j (e23)) = (e10)) \/ (((j (e23)) = (e11)) \/ (((j (e23)) = (e12)) \/ ((j (e23)) = (e13))))) ((op2 (e21) (e21)) = (e23)) ((j (op2 (e21) (e21))) = (op1 (j (e21)) (j (e21)))) (((j (e22)) = (e10)) \/ (((j (e22)) = (e11)) \/ (((j (e22)) = (e12)) \/ ((j (e22)) = (e13))))) ((j (h (e13))) = (e13)) ((e12) != (e13)) (((h (e12)) = (e20)) \/ (((h (e12)) = (e21)) \/ (((h (e12)) = (e22)) \/ ((h (e12)) = (e23))))) ((e10) != (e11)) ((j (h (e11))) = (e11)) ((j (op2 (e20) (e20))) = (op1 (j (e20)) (j (e20)))) ((op1 (e13) (e13)) = (e10)) ((op1 (e11) (e11)) = (e10)) ((op2 (e20) (e20)) = (e20)) ((e10) != (e12)) ((op1 (e12) (e12)) = (e10)) ((e10) != (e13)) (((j (e20)) = (e10)) \/ (((j (e20)) = (e11)) \/ (((j (e20)) = (e12)) \/ ((j (e20)) = (e13))))) ### DisjTree 33 138 159 177 % 27.80/28.02 179. (-. (((((h (e10)) = (e20)) \/ (((h (e10)) = (e21)) \/ (((h (e10)) = (e22)) \/ ((h (e10)) = (e23))))) /\ ((((h (e11)) = (e20)) \/ (((h (e11)) = (e21)) \/ (((h (e11)) = (e22)) \/ ((h (e11)) = (e23))))) /\ ((((h (e12)) = (e20)) \/ (((h (e12)) = (e21)) \/ (((h (e12)) = (e22)) \/ ((h (e12)) = (e23))))) /\ ((((h (e13)) = (e20)) \/ (((h (e13)) = (e21)) \/ (((h (e13)) = (e22)) \/ ((h (e13)) = (e23))))) /\ ((((j (e20)) = (e10)) \/ (((j (e20)) = (e11)) \/ (((j (e20)) = (e12)) \/ ((j (e20)) = (e13))))) /\ ((((j (e21)) = (e10)) \/ (((j (e21)) = (e11)) \/ (((j (e21)) = (e12)) \/ ((j (e21)) = (e13))))) /\ ((((j (e22)) = (e10)) \/ (((j (e22)) = (e11)) \/ (((j (e22)) = (e12)) \/ ((j (e22)) = (e13))))) /\ (((j (e23)) = (e10)) \/ (((j (e23)) = (e11)) \/ (((j (e23)) = (e12)) \/ ((j (e23)) = (e13)))))))))))) => (-. (((h (op1 (e10) (e10))) = (op2 (h (e10)) (h (e10)))) /\ (((h (op1 (e10) (e11))) = (op2 (h (e10)) (h (e11)))) /\ (((h (op1 (e10) (e12))) = (op2 (h (e10)) (h (e12)))) /\ (((h (op1 (e10) (e13))) = (op2 (h (e10)) (h (e13)))) /\ (((h (op1 (e11) (e10))) = (op2 (h (e11)) (h (e10)))) /\ (((h (op1 (e11) (e11))) = (op2 (h (e11)) (h (e11)))) /\ (((h (op1 (e11) (e12))) = (op2 (h (e11)) (h (e12)))) /\ (((h (op1 (e11) (e13))) = (op2 (h (e11)) (h (e13)))) /\ (((h (op1 (e12) (e10))) = (op2 (h (e12)) (h (e10)))) /\ (((h (op1 (e12) (e11))) = (op2 (h (e12)) (h (e11)))) /\ (((h (op1 (e12) (e12))) = (op2 (h (e12)) (h (e12)))) /\ (((h (op1 (e12) (e13))) = (op2 (h (e12)) (h (e13)))) /\ (((h (op1 (e13) (e10))) = (op2 (h (e13)) (h (e10)))) /\ (((h (op1 (e13) (e11))) = (op2 (h (e13)) (h (e11)))) /\ (((h (op1 (e13) (e12))) = (op2 (h (e13)) (h (e12)))) /\ (((h (op1 (e13) (e13))) = (op2 (h (e13)) (h (e13)))) /\ (((j (op2 (e20) (e20))) = (op1 (j (e20)) (j (e20)))) /\ (((j (op2 (e20) (e21))) = (op1 (j (e20)) (j (e21)))) /\ (((j (op2 (e20) (e22))) = (op1 (j (e20)) (j (e22)))) /\ (((j (op2 (e20) (e23))) = (op1 (j (e20)) (j (e23)))) /\ (((j (op2 (e21) (e20))) = (op1 (j (e21)) (j (e20)))) /\ (((j (op2 (e21) (e21))) = (op1 (j (e21)) (j (e21)))) /\ (((j (op2 (e21) (e22))) = (op1 (j (e21)) (j (e22)))) /\ (((j (op2 (e21) (e23))) = (op1 (j (e21)) (j (e23)))) /\ (((j (op2 (e22) (e20))) = (op1 (j (e22)) (j (e20)))) /\ (((j (op2 (e22) (e21))) = (op1 (j (e22)) (j (e21)))) /\ (((j (op2 (e22) (e22))) = (op1 (j (e22)) (j (e22)))) /\ (((j (op2 (e22) (e23))) = (op1 (j (e22)) (j (e23)))) /\ (((j (op2 (e23) (e20))) = (op1 (j (e23)) (j (e20)))) /\ (((j (op2 (e23) (e21))) = (op1 (j (e23)) (j (e21)))) /\ (((j (op2 (e23) (e22))) = (op1 (j (e23)) (j (e22)))) /\ (((j (op2 (e23) (e23))) = (op1 (j (e23)) (j (e23)))) /\ (((h (j (e20))) = (e20)) /\ (((h (j (e21))) = (e21)) /\ (((h (j (e22))) = (e22)) /\ (((h (j (e23))) = (e23)) /\ (((j (h (e10))) = (e10)) /\ (((j (h (e11))) = (e11)) /\ (((j (h (e12))) = (e12)) /\ ((j (h (e13))) = (e13)))))))))))))))))))))))))))))))))))))))))))) ((e10) != (e13)) ((op1 (e12) (e12)) = (e10)) ((e10) != (e12)) ((op2 (e20) (e20)) = (e20)) ((op1 (e11) (e11)) = (e10)) ((op1 (e13) (e13)) = (e10)) ((e10) != (e11)) ((e12) != (e13)) ((op2 (e21) (e21)) = (e23)) ((e11) != (e13)) ((e11) != (e12)) ### ConjTree 178 % 27.80/28.02 180. (((op2 (e20) (e20)) = (e20)) /\ (((op2 (e20) (e21)) = (e21)) /\ (((op2 (e20) (e22)) = (e22)) /\ (((op2 (e20) (e23)) = (e23)) /\ (((op2 (e21) (e20)) = (e21)) /\ (((op2 (e21) (e21)) = (e23)) /\ (((op2 (e21) (e22)) = (e20)) /\ (((op2 (e21) (e23)) = (e22)) /\ (((op2 (e22) (e20)) = (e22)) /\ (((op2 (e22) (e21)) = (e20)) /\ (((op2 (e22) (e22)) = (e23)) /\ (((op2 (e22) (e23)) = (e21)) /\ (((op2 (e23) (e20)) = (e23)) /\ (((op2 (e23) (e21)) = (e22)) /\ (((op2 (e23) (e22)) = (e21)) /\ ((op2 (e23) (e23)) = (e20))))))))))))))))) ((e11) != (e12)) ((e11) != (e13)) ((e12) != (e13)) ((e10) != (e11)) ((op1 (e13) (e13)) = (e10)) ((op1 (e11) (e11)) = (e10)) ((e10) != (e12)) ((op1 (e12) (e12)) = (e10)) ((e10) != (e13)) (-. (((((h (e10)) = (e20)) \/ (((h (e10)) = (e21)) \/ (((h (e10)) = (e22)) \/ ((h (e10)) = (e23))))) /\ ((((h (e11)) = (e20)) \/ (((h (e11)) = (e21)) \/ (((h (e11)) = (e22)) \/ ((h (e11)) = (e23))))) /\ ((((h (e12)) = (e20)) \/ (((h (e12)) = (e21)) \/ (((h (e12)) = (e22)) \/ ((h (e12)) = (e23))))) /\ ((((h (e13)) = (e20)) \/ (((h (e13)) = (e21)) \/ (((h (e13)) = (e22)) \/ ((h (e13)) = (e23))))) /\ ((((j (e20)) = (e10)) \/ (((j (e20)) = (e11)) \/ (((j (e20)) = (e12)) \/ ((j (e20)) = (e13))))) /\ ((((j (e21)) = (e10)) \/ (((j (e21)) = (e11)) \/ (((j (e21)) = (e12)) \/ ((j (e21)) = (e13))))) /\ ((((j (e22)) = (e10)) \/ (((j (e22)) = (e11)) \/ (((j (e22)) = (e12)) \/ ((j (e22)) = (e13))))) /\ (((j (e23)) = (e10)) \/ (((j (e23)) = (e11)) \/ (((j (e23)) = (e12)) \/ ((j (e23)) = (e13)))))))))))) => (-. (((h (op1 (e10) (e10))) = (op2 (h (e10)) (h (e10)))) /\ (((h (op1 (e10) (e11))) = (op2 (h (e10)) (h (e11)))) /\ (((h (op1 (e10) (e12))) = (op2 (h (e10)) (h (e12)))) /\ (((h (op1 (e10) (e13))) = (op2 (h (e10)) (h (e13)))) /\ (((h (op1 (e11) (e10))) = (op2 (h (e11)) (h (e10)))) /\ (((h (op1 (e11) (e11))) = (op2 (h (e11)) (h (e11)))) /\ (((h (op1 (e11) (e12))) = (op2 (h (e11)) (h (e12)))) /\ (((h (op1 (e11) (e13))) = (op2 (h (e11)) (h (e13)))) /\ (((h (op1 (e12) (e10))) = (op2 (h (e12)) (h (e10)))) /\ (((h (op1 (e12) (e11))) = (op2 (h (e12)) (h (e11)))) /\ (((h (op1 (e12) (e12))) = (op2 (h (e12)) (h (e12)))) /\ (((h (op1 (e12) (e13))) = (op2 (h (e12)) (h (e13)))) /\ (((h (op1 (e13) (e10))) = (op2 (h (e13)) (h (e10)))) /\ (((h (op1 (e13) (e11))) = (op2 (h (e13)) (h (e11)))) /\ (((h (op1 (e13) (e12))) = (op2 (h (e13)) (h (e12)))) /\ (((h (op1 (e13) (e13))) = (op2 (h (e13)) (h (e13)))) /\ (((j (op2 (e20) (e20))) = (op1 (j (e20)) (j (e20)))) /\ (((j (op2 (e20) (e21))) = (op1 (j (e20)) (j (e21)))) /\ (((j (op2 (e20) (e22))) = (op1 (j (e20)) (j (e22)))) /\ (((j (op2 (e20) (e23))) = (op1 (j (e20)) (j (e23)))) /\ (((j (op2 (e21) (e20))) = (op1 (j (e21)) (j (e20)))) /\ (((j (op2 (e21) (e21))) = (op1 (j (e21)) (j (e21)))) /\ (((j (op2 (e21) (e22))) = (op1 (j (e21)) (j (e22)))) /\ (((j (op2 (e21) (e23))) = (op1 (j (e21)) (j (e23)))) /\ (((j (op2 (e22) (e20))) = (op1 (j (e22)) (j (e20)))) /\ (((j (op2 (e22) (e21))) = (op1 (j (e22)) (j (e21)))) /\ (((j (op2 (e22) (e22))) = (op1 (j (e22)) (j (e22)))) /\ (((j (op2 (e22) (e23))) = (op1 (j (e22)) (j (e23)))) /\ (((j (op2 (e23) (e20))) = (op1 (j (e23)) (j (e20)))) /\ (((j (op2 (e23) (e21))) = (op1 (j (e23)) (j (e21)))) /\ (((j (op2 (e23) (e22))) = (op1 (j (e23)) (j (e22)))) /\ (((j (op2 (e23) (e23))) = (op1 (j (e23)) (j (e23)))) /\ (((h (j (e20))) = (e20)) /\ (((h (j (e21))) = (e21)) /\ (((h (j (e22))) = (e22)) /\ (((h (j (e23))) = (e23)) /\ (((j (h (e10))) = (e10)) /\ (((j (h (e11))) = (e11)) /\ (((j (h (e12))) = (e12)) /\ ((j (h (e13))) = (e13)))))))))))))))))))))))))))))))))))))))))))) ### ConjTree 179 % 27.80/28.02 181. (((op1 (e10) (e10)) = (e10)) /\ (((op1 (e10) (e11)) = (e11)) /\ (((op1 (e10) (e12)) = (e12)) /\ (((op1 (e10) (e13)) = (e13)) /\ (((op1 (e11) (e10)) = (e11)) /\ (((op1 (e11) (e11)) = (e10)) /\ (((op1 (e11) (e12)) = (e13)) /\ (((op1 (e11) (e13)) = (e12)) /\ (((op1 (e12) (e10)) = (e12)) /\ (((op1 (e12) (e11)) = (e13)) /\ (((op1 (e12) (e12)) = (e10)) /\ (((op1 (e12) (e13)) = (e11)) /\ (((op1 (e13) (e10)) = (e13)) /\ (((op1 (e13) (e11)) = (e12)) /\ (((op1 (e13) (e12)) = (e11)) /\ ((op1 (e13) (e13)) = (e10))))))))))))))))) (-. (((((h (e10)) = (e20)) \/ (((h (e10)) = (e21)) \/ (((h (e10)) = (e22)) \/ ((h (e10)) = (e23))))) /\ ((((h (e11)) = (e20)) \/ (((h (e11)) = (e21)) \/ (((h (e11)) = (e22)) \/ ((h (e11)) = (e23))))) /\ ((((h (e12)) = (e20)) \/ (((h (e12)) = (e21)) \/ (((h (e12)) = (e22)) \/ ((h (e12)) = (e23))))) /\ ((((h (e13)) = (e20)) \/ (((h (e13)) = (e21)) \/ (((h (e13)) = (e22)) \/ ((h (e13)) = (e23))))) /\ ((((j (e20)) = (e10)) \/ (((j (e20)) = (e11)) \/ (((j (e20)) = (e12)) \/ ((j (e20)) = (e13))))) /\ ((((j (e21)) = (e10)) \/ (((j (e21)) = (e11)) \/ (((j (e21)) = (e12)) \/ ((j (e21)) = (e13))))) /\ ((((j (e22)) = (e10)) \/ (((j (e22)) = (e11)) \/ (((j (e22)) = (e12)) \/ ((j (e22)) = (e13))))) /\ (((j (e23)) = (e10)) \/ (((j (e23)) = (e11)) \/ (((j (e23)) = (e12)) \/ ((j (e23)) = (e13)))))))))))) => (-. (((h (op1 (e10) (e10))) = (op2 (h (e10)) (h (e10)))) /\ (((h (op1 (e10) (e11))) = (op2 (h (e10)) (h (e11)))) /\ (((h (op1 (e10) (e12))) = (op2 (h (e10)) (h (e12)))) /\ (((h (op1 (e10) (e13))) = (op2 (h (e10)) (h (e13)))) /\ (((h (op1 (e11) (e10))) = (op2 (h (e11)) (h (e10)))) /\ (((h (op1 (e11) (e11))) = (op2 (h (e11)) (h (e11)))) /\ (((h (op1 (e11) (e12))) = (op2 (h (e11)) (h (e12)))) /\ (((h (op1 (e11) (e13))) = (op2 (h (e11)) (h (e13)))) /\ (((h (op1 (e12) (e10))) = (op2 (h (e12)) (h (e10)))) /\ (((h (op1 (e12) (e11))) = (op2 (h (e12)) (h (e11)))) /\ (((h (op1 (e12) (e12))) = (op2 (h (e12)) (h (e12)))) /\ (((h (op1 (e12) (e13))) = (op2 (h (e12)) (h (e13)))) /\ (((h (op1 (e13) (e10))) = (op2 (h (e13)) (h (e10)))) /\ (((h (op1 (e13) (e11))) = (op2 (h (e13)) (h (e11)))) /\ (((h (op1 (e13) (e12))) = (op2 (h (e13)) (h (e12)))) /\ (((h (op1 (e13) (e13))) = (op2 (h (e13)) (h (e13)))) /\ (((j (op2 (e20) (e20))) = (op1 (j (e20)) (j (e20)))) /\ (((j (op2 (e20) (e21))) = (op1 (j (e20)) (j (e21)))) /\ (((j (op2 (e20) (e22))) = (op1 (j (e20)) (j (e22)))) /\ (((j (op2 (e20) (e23))) = (op1 (j (e20)) (j (e23)))) /\ (((j (op2 (e21) (e20))) = (op1 (j (e21)) (j (e20)))) /\ (((j (op2 (e21) (e21))) = (op1 (j (e21)) (j (e21)))) /\ (((j (op2 (e21) (e22))) = (op1 (j (e21)) (j (e22)))) /\ (((j (op2 (e21) (e23))) = (op1 (j (e21)) (j (e23)))) /\ (((j (op2 (e22) (e20))) = (op1 (j (e22)) (j (e20)))) /\ (((j (op2 (e22) (e21))) = (op1 (j (e22)) (j (e21)))) /\ (((j (op2 (e22) (e22))) = (op1 (j (e22)) (j (e22)))) /\ (((j (op2 (e22) (e23))) = (op1 (j (e22)) (j (e23)))) /\ (((j (op2 (e23) (e20))) = (op1 (j (e23)) (j (e20)))) /\ (((j (op2 (e23) (e21))) = (op1 (j (e23)) (j (e21)))) /\ (((j (op2 (e23) (e22))) = (op1 (j (e23)) (j (e22)))) /\ (((j (op2 (e23) (e23))) = (op1 (j (e23)) (j (e23)))) /\ (((h (j (e20))) = (e20)) /\ (((h (j (e21))) = (e21)) /\ (((h (j (e22))) = (e22)) /\ (((h (j (e23))) = (e23)) /\ (((j (h (e10))) = (e10)) /\ (((j (h (e11))) = (e11)) /\ (((j (h (e12))) = (e12)) /\ ((j (h (e13))) = (e13)))))))))))))))))))))))))))))))))))))))))))) ((e10) != (e13)) ((e10) != (e12)) ((e10) != (e11)) ((e12) != (e13)) ((e11) != (e13)) ((e11) != (e12)) (((op2 (e20) (e20)) = (e20)) /\ (((op2 (e20) (e21)) = (e21)) /\ (((op2 (e20) (e22)) = (e22)) /\ (((op2 (e20) (e23)) = (e23)) /\ (((op2 (e21) (e20)) = (e21)) /\ (((op2 (e21) (e21)) = (e23)) /\ (((op2 (e21) (e22)) = (e20)) /\ (((op2 (e21) (e23)) = (e22)) /\ (((op2 (e22) (e20)) = (e22)) /\ (((op2 (e22) (e21)) = (e20)) /\ (((op2 (e22) (e22)) = (e23)) /\ (((op2 (e22) (e23)) = (e21)) /\ (((op2 (e23) (e20)) = (e23)) /\ (((op2 (e23) (e21)) = (e22)) /\ (((op2 (e23) (e22)) = (e21)) /\ ((op2 (e23) (e23)) = (e20))))))))))))))))) ### ConjTree 180 % 27.80/28.02 182. (((e10) != (e11)) /\ (((e10) != (e12)) /\ (((e10) != (e13)) /\ (((e11) != (e12)) /\ (((e11) != (e13)) /\ ((e12) != (e13))))))) (((op2 (e20) (e20)) = (e20)) /\ (((op2 (e20) (e21)) = (e21)) /\ (((op2 (e20) (e22)) = (e22)) /\ (((op2 (e20) (e23)) = (e23)) /\ (((op2 (e21) (e20)) = (e21)) /\ (((op2 (e21) (e21)) = (e23)) /\ (((op2 (e21) (e22)) = (e20)) /\ (((op2 (e21) (e23)) = (e22)) /\ (((op2 (e22) (e20)) = (e22)) /\ (((op2 (e22) (e21)) = (e20)) /\ (((op2 (e22) (e22)) = (e23)) /\ (((op2 (e22) (e23)) = (e21)) /\ (((op2 (e23) (e20)) = (e23)) /\ (((op2 (e23) (e21)) = (e22)) /\ (((op2 (e23) (e22)) = (e21)) /\ ((op2 (e23) (e23)) = (e20))))))))))))))))) (-. (((((h (e10)) = (e20)) \/ (((h (e10)) = (e21)) \/ (((h (e10)) = (e22)) \/ ((h (e10)) = (e23))))) /\ ((((h (e11)) = (e20)) \/ (((h (e11)) = (e21)) \/ (((h (e11)) = (e22)) \/ ((h (e11)) = (e23))))) /\ ((((h (e12)) = (e20)) \/ (((h (e12)) = (e21)) \/ (((h (e12)) = (e22)) \/ ((h (e12)) = (e23))))) /\ ((((h (e13)) = (e20)) \/ (((h (e13)) = (e21)) \/ (((h (e13)) = (e22)) \/ ((h (e13)) = (e23))))) /\ ((((j (e20)) = (e10)) \/ (((j (e20)) = (e11)) \/ (((j (e20)) = (e12)) \/ ((j (e20)) = (e13))))) /\ ((((j (e21)) = (e10)) \/ (((j (e21)) = (e11)) \/ (((j (e21)) = (e12)) \/ ((j (e21)) = (e13))))) /\ ((((j (e22)) = (e10)) \/ (((j (e22)) = (e11)) \/ (((j (e22)) = (e12)) \/ ((j (e22)) = (e13))))) /\ (((j (e23)) = (e10)) \/ (((j (e23)) = (e11)) \/ (((j (e23)) = (e12)) \/ ((j (e23)) = (e13)))))))))))) => (-. (((h (op1 (e10) (e10))) = (op2 (h (e10)) (h (e10)))) /\ (((h (op1 (e10) (e11))) = (op2 (h (e10)) (h (e11)))) /\ (((h (op1 (e10) (e12))) = (op2 (h (e10)) (h (e12)))) /\ (((h (op1 (e10) (e13))) = (op2 (h (e10)) (h (e13)))) /\ (((h (op1 (e11) (e10))) = (op2 (h (e11)) (h (e10)))) /\ (((h (op1 (e11) (e11))) = (op2 (h (e11)) (h (e11)))) /\ (((h (op1 (e11) (e12))) = (op2 (h (e11)) (h (e12)))) /\ (((h (op1 (e11) (e13))) = (op2 (h (e11)) (h (e13)))) /\ (((h (op1 (e12) (e10))) = (op2 (h (e12)) (h (e10)))) /\ (((h (op1 (e12) (e11))) = (op2 (h (e12)) (h (e11)))) /\ (((h (op1 (e12) (e12))) = (op2 (h (e12)) (h (e12)))) /\ (((h (op1 (e12) (e13))) = (op2 (h (e12)) (h (e13)))) /\ (((h (op1 (e13) (e10))) = (op2 (h (e13)) (h (e10)))) /\ (((h (op1 (e13) (e11))) = (op2 (h (e13)) (h (e11)))) /\ (((h (op1 (e13) (e12))) = (op2 (h (e13)) (h (e12)))) /\ (((h (op1 (e13) (e13))) = (op2 (h (e13)) (h (e13)))) /\ (((j (op2 (e20) (e20))) = (op1 (j (e20)) (j (e20)))) /\ (((j (op2 (e20) (e21))) = (op1 (j (e20)) (j (e21)))) /\ (((j (op2 (e20) (e22))) = (op1 (j (e20)) (j (e22)))) /\ (((j (op2 (e20) (e23))) = (op1 (j (e20)) (j (e23)))) /\ (((j (op2 (e21) (e20))) = (op1 (j (e21)) (j (e20)))) /\ (((j (op2 (e21) (e21))) = (op1 (j (e21)) (j (e21)))) /\ (((j (op2 (e21) (e22))) = (op1 (j (e21)) (j (e22)))) /\ (((j (op2 (e21) (e23))) = (op1 (j (e21)) (j (e23)))) /\ (((j (op2 (e22) (e20))) = (op1 (j (e22)) (j (e20)))) /\ (((j (op2 (e22) (e21))) = (op1 (j (e22)) (j (e21)))) /\ (((j (op2 (e22) (e22))) = (op1 (j (e22)) (j (e22)))) /\ (((j (op2 (e22) (e23))) = (op1 (j (e22)) (j (e23)))) /\ (((j (op2 (e23) (e20))) = (op1 (j (e23)) (j (e20)))) /\ (((j (op2 (e23) (e21))) = (op1 (j (e23)) (j (e21)))) /\ (((j (op2 (e23) (e22))) = (op1 (j (e23)) (j (e22)))) /\ (((j (op2 (e23) (e23))) = (op1 (j (e23)) (j (e23)))) /\ (((h (j (e20))) = (e20)) /\ (((h (j (e21))) = (e21)) /\ (((h (j (e22))) = (e22)) /\ (((h (j (e23))) = (e23)) /\ (((j (h (e10))) = (e10)) /\ (((j (h (e11))) = (e11)) /\ (((j (h (e12))) = (e12)) /\ ((j (h (e13))) = (e13)))))))))))))))))))))))))))))))))))))))))))) (((op1 (e10) (e10)) = (e10)) /\ (((op1 (e10) (e11)) = (e11)) /\ (((op1 (e10) (e12)) = (e12)) /\ (((op1 (e10) (e13)) = (e13)) /\ (((op1 (e11) (e10)) = (e11)) /\ (((op1 (e11) (e11)) = (e10)) /\ (((op1 (e11) (e12)) = (e13)) /\ (((op1 (e11) (e13)) = (e12)) /\ (((op1 (e12) (e10)) = (e12)) /\ (((op1 (e12) (e11)) = (e13)) /\ (((op1 (e12) (e12)) = (e10)) /\ (((op1 (e12) (e13)) = (e11)) /\ (((op1 (e13) (e10)) = (e13)) /\ (((op1 (e13) (e11)) = (e12)) /\ (((op1 (e13) (e12)) = (e11)) /\ ((op1 (e13) (e13)) = (e10))))))))))))))))) ### ConjTree 181 % 27.80/28.02 % SZS output end Proof % 27.80/28.02 (* END-PROOF *) %------------------------------------------------------------------------------