Search for blocks/addresses/...

Proofgold Asset

asset id
52e41077f4bff31c4ef9937a96cedfb969a8e0e30afc0e0ef4b99d43abd33dbe
asset hash
80ad6728a5d625f1b66982289ab4d0a3cb003eed4a82310e46a8907eb1e1ad8e
bday / block
24271
tx
6b678..
preasset
doc published by Pr5Zc..
Theorem 547c4.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 . x0 x3x0 x4x0 x5x0 x6x2 (x1 x3 (x1 x4 x5)) x6 = x1 (x2 x3 x6) (x1 (x2 x4 x6) (x2 x5 x6)) (proof)
Known e11b7.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))∀ x2 x3 x4 . x0 x2x0 x3x0 x4x0 (x1 x2 (x1 x3 x4))
Theorem 81c99.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 . x0 x3x0 x4x0 x5x0 x6x0 x7x2 (x1 x3 (x1 x4 (x1 x5 x6))) x7 = x1 (x2 x3 x7) (x1 (x2 x4 x7) (x1 (x2 x5 x7) (x2 x6 x7))) (proof)
Known 25618.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))∀ x2 x3 x4 x5 . x0 x2x0 x3x0 x4x0 x5x0 (x1 x2 (x1 x3 (x1 x4 x5)))
Theorem bc000.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) x8 = x1 (x2 x3 x8) (x1 (x2 x4 x8) (x1 (x2 x5 x8) (x1 (x2 x6 x8) (x2 x7 x8)))) (proof)
Known b9f0e.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))∀ x2 x3 x4 x5 x6 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 (x1 x2 (x1 x3 (x1 x4 (x1 x5 x6))))
Theorem a4026.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) x9 = x1 (x2 x3 x9) (x1 (x2 x4 x9) (x1 (x2 x5 x9) (x1 (x2 x6 x9) (x1 (x2 x7 x9) (x2 x8 x9))))) (proof)
Known 2a50e.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))∀ x2 x3 x4 x5 x6 x7 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 (x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))))
Theorem 6ee59.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) x10 = x1 (x2 x3 x10) (x1 (x2 x4 x10) (x1 (x2 x5 x10) (x1 (x2 x6 x10) (x1 (x2 x7 x10) (x1 (x2 x8 x10) (x2 x9 x10)))))) (proof)
Known 948ae.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))∀ x2 x3 x4 x5 x6 x7 x8 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 (x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))))
Theorem 2fffd.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 x10))))))) x11 = x1 (x2 x3 x11) (x1 (x2 x4 x11) (x1 (x2 x5 x11) (x1 (x2 x6 x11) (x1 (x2 x7 x11) (x1 (x2 x8 x11) (x1 (x2 x9 x11) (x2 x10 x11))))))) (proof)
Known 18faf.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 (x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))))
Theorem de9e9.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 x11)))))))) x12 = x1 (x2 x3 x12) (x1 (x2 x4 x12) (x1 (x2 x5 x12) (x1 (x2 x6 x12) (x1 (x2 x7 x12) (x1 (x2 x8 x12) (x1 (x2 x9 x12) (x1 (x2 x10 x12) (x2 x11 x12)))))))) (proof)
Known 880a1.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 (x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 x10))))))))
Theorem 6c866.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x0 x13x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 x12))))))))) x13 = x1 (x2 x3 x13) (x1 (x2 x4 x13) (x1 (x2 x5 x13) (x1 (x2 x6 x13) (x1 (x2 x7 x13) (x1 (x2 x8 x13) (x1 (x2 x9 x13) (x1 (x2 x10 x13) (x1 (x2 x11 x13) (x2 x12 x13))))))))) (proof)
Known 737fb.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 (x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 x11)))))))))
Theorem 1fe00.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x0 x13x0 x14x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 x13)))))))))) x14 = x1 (x2 x3 x14) (x1 (x2 x4 x14) (x1 (x2 x5 x14) (x1 (x2 x6 x14) (x1 (x2 x7 x14) (x1 (x2 x8 x14) (x1 (x2 x9 x14) (x1 (x2 x10 x14) (x1 (x2 x11 x14) (x1 (x2 x12 x14) (x2 x13 x14)))))))))) (proof)
Known f7821.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x0 (x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 x12))))))))))
Theorem 2555f.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x0 x13x0 x14x0 x15x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 x14))))))))))) x15 = x1 (x2 x3 x15) (x1 (x2 x4 x15) (x1 (x2 x5 x15) (x1 (x2 x6 x15) (x1 (x2 x7 x15) (x1 (x2 x8 x15) (x1 (x2 x9 x15) (x1 (x2 x10 x15) (x1 (x2 x11 x15) (x1 (x2 x12 x15) (x1 (x2 x13 x15) (x2 x14 x15))))))))))) (proof)
Known 2c5ad.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x0 x13x0 (x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 x13)))))))))))
Theorem 3841c.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x0 x13x0 x14x0 x15x0 x16x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 x15)))))))))))) x16 = x1 (x2 x3 x16) (x1 (x2 x4 x16) (x1 (x2 x5 x16) (x1 (x2 x6 x16) (x1 (x2 x7 x16) (x1 (x2 x8 x16) (x1 (x2 x9 x16) (x1 (x2 x10 x16) (x1 (x2 x11 x16) (x1 (x2 x12 x16) (x1 (x2 x13 x16) (x1 (x2 x14 x16) (x2 x15 x16)))))))))))) (proof)
Known ea7b1.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x0 x13x0 x14x0 (x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 x14))))))))))))
Theorem 8454f.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x0 x13x0 x14x0 x15x0 x16x0 x17x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 (x1 x15 x16))))))))))))) x17 = x1 (x2 x3 x17) (x1 (x2 x4 x17) (x1 (x2 x5 x17) (x1 (x2 x6 x17) (x1 (x2 x7 x17) (x1 (x2 x8 x17) (x1 (x2 x9 x17) (x1 (x2 x10 x17) (x1 (x2 x11 x17) (x1 (x2 x12 x17) (x1 (x2 x13 x17) (x1 (x2 x14 x17) (x1 (x2 x15 x17) (x2 x16 x17))))))))))))) (proof)
Known 6cd80.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x0 x13x0 x14x0 x15x0 (x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 x15)))))))))))))
Theorem 1d55a.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x0 x13x0 x14x0 x15x0 x16x0 x17x0 x18x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 (x1 x15 (x1 x16 x17)))))))))))))) x18 = x1 (x2 x3 x18) (x1 (x2 x4 x18) (x1 (x2 x5 x18) (x1 (x2 x6 x18) (x1 (x2 x7 x18) (x1 (x2 x8 x18) (x1 (x2 x9 x18) (x1 (x2 x10 x18) (x1 (x2 x11 x18) (x1 (x2 x12 x18) (x1 (x2 x13 x18) (x1 (x2 x14 x18) (x1 (x2 x15 x18) (x1 (x2 x16 x18) (x2 x17 x18)))))))))))))) (proof)
Known 855a7.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x0 x13x0 x14x0 x15x0 x16x0 (x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 (x1 x15 x16))))))))))))))
Theorem d1d81.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x0 x13x0 x14x0 x15x0 x16x0 x17x0 x18x0 x19x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 (x1 x15 (x1 x16 (x1 x17 x18))))))))))))))) x19 = x1 (x2 x3 x19) (x1 (x2 x4 x19) (x1 (x2 x5 x19) (x1 (x2 x6 x19) (x1 (x2 x7 x19) (x1 (x2 x8 x19) (x1 (x2 x9 x19) (x1 (x2 x10 x19) (x1 (x2 x11 x19) (x1 (x2 x12 x19) (x1 (x2 x13 x19) (x1 (x2 x14 x19) (x1 (x2 x15 x19) (x1 (x2 x16 x19) (x1 (x2 x17 x19) (x2 x18 x19))))))))))))))) (proof)
Theorem cebfe.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))∀ x3 x4 x5 x6 . x0 x3x0 x4x0 x5x0 x6x2 x6 (x1 x3 (x1 x4 x5)) = x1 (x2 x6 x3) (x1 (x2 x6 x4) (x2 x6 x5)) (proof)
Theorem bbdc7.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))∀ x3 x4 x5 x6 x7 . x0 x3x0 x4x0 x5x0 x6x0 x7x2 x7 (x1 x3 (x1 x4 (x1 x5 x6))) = x1 (x2 x7 x3) (x1 (x2 x7 x4) (x1 (x2 x7 x5) (x2 x7 x6))) (proof)
Theorem 6831b.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))∀ x3 x4 x5 x6 x7 x8 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x2 x8 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 (x2 x8 x3) (x1 (x2 x8 x4) (x1 (x2 x8 x5) (x1 (x2 x8 x6) (x2 x8 x7)))) (proof)
Theorem 67024.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))∀ x3 x4 x5 x6 x7 x8 x9 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x2 x9 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) = x1 (x2 x9 x3) (x1 (x2 x9 x4) (x1 (x2 x9 x5) (x1 (x2 x9 x6) (x1 (x2 x9 x7) (x2 x9 x8))))) (proof)
Theorem fc0c5.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x2 x10 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 (x2 x10 x3) (x1 (x2 x10 x4) (x1 (x2 x10 x5) (x1 (x2 x10 x6) (x1 (x2 x10 x7) (x1 (x2 x10 x8) (x2 x10 x9)))))) (proof)
Theorem 128a5.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x2 x11 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 x10))))))) = x1 (x2 x11 x3) (x1 (x2 x11 x4) (x1 (x2 x11 x5) (x1 (x2 x11 x6) (x1 (x2 x11 x7) (x1 (x2 x11 x8) (x1 (x2 x11 x9) (x2 x11 x10))))))) (proof)
Theorem 3eed7.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x2 x12 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 x11)))))))) = x1 (x2 x12 x3) (x1 (x2 x12 x4) (x1 (x2 x12 x5) (x1 (x2 x12 x6) (x1 (x2 x12 x7) (x1 (x2 x12 x8) (x1 (x2 x12 x9) (x1 (x2 x12 x10) (x2 x12 x11)))))))) (proof)
Theorem 83656.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x0 x13x2 x13 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 x12))))))))) = x1 (x2 x13 x3) (x1 (x2 x13 x4) (x1 (x2 x13 x5) (x1 (x2 x13 x6) (x1 (x2 x13 x7) (x1 (x2 x13 x8) (x1 (x2 x13 x9) (x1 (x2 x13 x10) (x1 (x2 x13 x11) (x2 x13 x12))))))))) (proof)
Theorem e214f.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x0 x13x0 x14x2 x14 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 x13)))))))))) = x1 (x2 x14 x3) (x1 (x2 x14 x4) (x1 (x2 x14 x5) (x1 (x2 x14 x6) (x1 (x2 x14 x7) (x1 (x2 x14 x8) (x1 (x2 x14 x9) (x1 (x2 x14 x10) (x1 (x2 x14 x11) (x1 (x2 x14 x12) (x2 x14 x13)))))))))) (proof)
Theorem 3d6c4.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x0 x13x0 x14x0 x15x2 x15 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 x14))))))))))) = x1 (x2 x15 x3) (x1 (x2 x15 x4) (x1 (x2 x15 x5) (x1 (x2 x15 x6) (x1 (x2 x15 x7) (x1 (x2 x15 x8) (x1 (x2 x15 x9) (x1 (x2 x15 x10) (x1 (x2 x15 x11) (x1 (x2 x15 x12) (x1 (x2 x15 x13) (x2 x15 x14))))))))))) (proof)
Theorem 22e9e.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x0 x13x0 x14x0 x15x0 x16x2 x16 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 x15)))))))))))) = x1 (x2 x16 x3) (x1 (x2 x16 x4) (x1 (x2 x16 x5) (x1 (x2 x16 x6) (x1 (x2 x16 x7) (x1 (x2 x16 x8) (x1 (x2 x16 x9) (x1 (x2 x16 x10) (x1 (x2 x16 x11) (x1 (x2 x16 x12) (x1 (x2 x16 x13) (x1 (x2 x16 x14) (x2 x16 x15)))))))))))) (proof)
Theorem 068aa.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x0 x13x0 x14x0 x15x0 x16x0 x17x2 x17 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 (x1 x15 x16))))))))))))) = x1 (x2 x17 x3) (x1 (x2 x17 x4) (x1 (x2 x17 x5) (x1 (x2 x17 x6) (x1 (x2 x17 x7) (x1 (x2 x17 x8) (x1 (x2 x17 x9) (x1 (x2 x17 x10) (x1 (x2 x17 x11) (x1 (x2 x17 x12) (x1 (x2 x17 x13) (x1 (x2 x17 x14) (x1 (x2 x17 x15) (x2 x17 x16))))))))))))) (proof)
Theorem 20ea2.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x0 x13x0 x14x0 x15x0 x16x0 x17x0 x18x2 x18 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 (x1 x15 (x1 x16 x17)))))))))))))) = x1 (x2 x18 x3) (x1 (x2 x18 x4) (x1 (x2 x18 x5) (x1 (x2 x18 x6) (x1 (x2 x18 x7) (x1 (x2 x18 x8) (x1 (x2 x18 x9) (x1 (x2 x18 x10) (x1 (x2 x18 x11) (x1 (x2 x18 x12) (x1 (x2 x18 x13) (x1 (x2 x18 x14) (x1 (x2 x18 x15) (x1 (x2 x18 x16) (x2 x18 x17)))))))))))))) (proof)
Theorem 44d11.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x0 x13x0 x14x0 x15x0 x16x0 x17x0 x18x0 x19x2 x19 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 (x1 x15 (x1 x16 (x1 x17 x18))))))))))))))) = x1 (x2 x19 x3) (x1 (x2 x19 x4) (x1 (x2 x19 x5) (x1 (x2 x19 x6) (x1 (x2 x19 x7) (x1 (x2 x19 x8) (x1 (x2 x19 x9) (x1 (x2 x19 x10) (x1 (x2 x19 x11) (x1 (x2 x19 x12) (x1 (x2 x19 x13) (x1 (x2 x19 x14) (x1 (x2 x19 x15) (x1 (x2 x19 x16) (x1 (x2 x19 x17) (x2 x19 x18))))))))))))))) (proof)
Theorem c50dc.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 . x0 x3x0 x4x0 x5x0 x6x2 (x1 x3 x4) (x1 x5 x6) = x1 (x1 (x2 x3 x5) (x2 x3 x6)) (x1 (x2 x4 x5) (x2 x4 x6)) (proof)
Theorem f7342.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 . x0 x3x0 x4x0 x5x0 x6x0 x7x2 (x1 x3 x4) (x1 x5 (x1 x6 x7)) = x1 (x1 (x2 x3 x5) (x1 (x2 x3 x6) (x2 x3 x7))) (x1 (x2 x4 x5) (x1 (x2 x4 x6) (x2 x4 x7))) (proof)
Theorem 385a8.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x2 (x1 x3 x4) (x1 x5 (x1 x6 (x1 x7 x8))) = x1 (x1 (x2 x3 x5) (x1 (x2 x3 x6) (x1 (x2 x3 x7) (x2 x3 x8)))) (x1 (x2 x4 x5) (x1 (x2 x4 x6) (x1 (x2 x4 x7) (x2 x4 x8)))) (proof)
Theorem 99370.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x2 (x1 x3 x4) (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))) = x1 (x1 (x2 x3 x5) (x1 (x2 x3 x6) (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x2 x3 x9))))) (x1 (x2 x4 x5) (x1 (x2 x4 x6) (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x2 x4 x9))))) (proof)
Theorem 7e8a0.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x2 (x1 x3 x4) (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 x10))))) = x1 (x1 (x2 x3 x5) (x1 (x2 x3 x6) (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x2 x3 x10)))))) (x1 (x2 x4 x5) (x1 (x2 x4 x6) (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x2 x4 x10)))))) (proof)
Theorem 2987b.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x2 (x1 x3 x4) (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 x11)))))) = x1 (x1 (x2 x3 x5) (x1 (x2 x3 x6) (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x2 x3 x11))))))) (x1 (x2 x4 x5) (x1 (x2 x4 x6) (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x2 x4 x11))))))) (proof)
Theorem 65828.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x2 (x1 x3 x4) (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 x12))))))) = x1 (x1 (x2 x3 x5) (x1 (x2 x3 x6) (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x2 x3 x12)))))))) (x1 (x2 x4 x5) (x1 (x2 x4 x6) (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x2 x4 x12)))))))) (proof)
Theorem 7f9d6.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 . x0 x3x0 x4x0 x5x0 x6x0 x7x2 (x1 x3 (x1 x4 x5)) (x1 x6 x7) = x1 (x1 (x2 x3 x6) (x2 x3 x7)) (x1 (x1 (x2 x4 x6) (x2 x4 x7)) (x1 (x2 x5 x6) (x2 x5 x7))) (proof)
Theorem ef027.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x2 (x1 x3 (x1 x4 x5)) (x1 x6 (x1 x7 x8)) = x1 (x1 (x2 x3 x6) (x1 (x2 x3 x7) (x2 x3 x8))) (x1 (x1 (x2 x4 x6) (x1 (x2 x4 x7) (x2 x4 x8))) (x1 (x2 x5 x6) (x1 (x2 x5 x7) (x2 x5 x8)))) (proof)
Theorem 06c4f.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x2 (x1 x3 (x1 x4 x5)) (x1 x6 (x1 x7 (x1 x8 x9))) = x1 (x1 (x2 x3 x6) (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x2 x3 x9)))) (x1 (x1 (x2 x4 x6) (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x2 x4 x9)))) (x1 (x2 x5 x6) (x1 (x2 x5 x7) (x1 (x2 x5 x8) (x2 x5 x9))))) (proof)
Theorem ef15c.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x2 (x1 x3 (x1 x4 x5)) (x1 x6 (x1 x7 (x1 x8 (x1 x9 x10)))) = x1 (x1 (x2 x3 x6) (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x2 x3 x10))))) (x1 (x1 (x2 x4 x6) (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x2 x4 x10))))) (x1 (x2 x5 x6) (x1 (x2 x5 x7) (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x2 x5 x10)))))) (proof)
Theorem 24435.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x2 (x1 x3 (x1 x4 x5)) (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 x11))))) = x1 (x1 (x2 x3 x6) (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x2 x3 x11)))))) (x1 (x1 (x2 x4 x6) (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x2 x4 x11)))))) (x1 (x2 x5 x6) (x1 (x2 x5 x7) (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x2 x5 x11))))))) (proof)
Theorem 6b961.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x2 (x1 x3 (x1 x4 x5)) (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 x12)))))) = x1 (x1 (x2 x3 x6) (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x2 x3 x12))))))) (x1 (x1 (x2 x4 x6) (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x2 x4 x12))))))) (x1 (x2 x5 x6) (x1 (x2 x5 x7) (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x2 x5 x12)))))))) (proof)
Theorem 3ba1a.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x0 x13x2 (x1 x3 (x1 x4 x5)) (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 x13))))))) = x1 (x1 (x2 x3 x6) (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x2 x3 x13)))))))) (x1 (x1 (x2 x4 x6) (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x2 x4 x13)))))))) (x1 (x2 x5 x6) (x1 (x2 x5 x7) (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x2 x5 x13))))))))) (proof)
Theorem bdad1.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x2 (x1 x3 (x1 x4 (x1 x5 x6))) (x1 x7 x8) = x1 (x1 (x2 x3 x7) (x2 x3 x8)) (x1 (x1 (x2 x4 x7) (x2 x4 x8)) (x1 (x1 (x2 x5 x7) (x2 x5 x8)) (x1 (x2 x6 x7) (x2 x6 x8)))) (proof)
Theorem 037b6.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x2 (x1 x3 (x1 x4 (x1 x5 x6))) (x1 x7 (x1 x8 x9)) = x1 (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x2 x3 x9))) (x1 (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x2 x4 x9))) (x1 (x1 (x2 x5 x7) (x1 (x2 x5 x8) (x2 x5 x9))) (x1 (x2 x6 x7) (x1 (x2 x6 x8) (x2 x6 x9))))) (proof)
Theorem 70471.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x2 (x1 x3 (x1 x4 (x1 x5 x6))) (x1 x7 (x1 x8 (x1 x9 x10))) = x1 (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x2 x3 x10)))) (x1 (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x2 x4 x10)))) (x1 (x1 (x2 x5 x7) (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x2 x5 x10)))) (x1 (x2 x6 x7) (x1 (x2 x6 x8) (x1 (x2 x6 x9) (x2 x6 x10)))))) (proof)
Theorem 34a9f.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x2 (x1 x3 (x1 x4 (x1 x5 x6))) (x1 x7 (x1 x8 (x1 x9 (x1 x10 x11)))) = x1 (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x2 x3 x11))))) (x1 (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x2 x4 x11))))) (x1 (x1 (x2 x5 x7) (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x2 x5 x11))))) (x1 (x2 x6 x7) (x1 (x2 x6 x8) (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x2 x6 x11))))))) (proof)
Theorem c5a67.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x2 (x1 x3 (x1 x4 (x1 x5 x6))) (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 x12))))) = x1 (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x2 x3 x12)))))) (x1 (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x2 x4 x12)))))) (x1 (x1 (x2 x5 x7) (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x2 x5 x12)))))) (x1 (x2 x6 x7) (x1 (x2 x6 x8) (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x2 x6 x12)))))))) (proof)
Theorem a4275.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x0 x13x2 (x1 x3 (x1 x4 (x1 x5 x6))) (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 x13)))))) = x1 (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x2 x3 x13))))))) (x1 (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x2 x4 x13))))))) (x1 (x1 (x2 x5 x7) (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x2 x5 x13))))))) (x1 (x2 x6 x7) (x1 (x2 x6 x8) (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x2 x6 x13))))))))) (proof)
Theorem acdf7.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x0 x13x0 x14x2 (x1 x3 (x1 x4 (x1 x5 x6))) (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 x14))))))) = x1 (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x2 x3 x14)))))))) (x1 (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x2 x4 x14)))))))) (x1 (x1 (x2 x5 x7) (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x2 x5 x14)))))))) (x1 (x2 x6 x7) (x1 (x2 x6 x8) (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x2 x6 x14)))))))))) (proof)
Theorem 1634a.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) (x1 x8 x9) = x1 (x1 (x2 x3 x8) (x2 x3 x9)) (x1 (x1 (x2 x4 x8) (x2 x4 x9)) (x1 (x1 (x2 x5 x8) (x2 x5 x9)) (x1 (x1 (x2 x6 x8) (x2 x6 x9)) (x1 (x2 x7 x8) (x2 x7 x9))))) (proof)
Theorem 9d4e1.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) (x1 x8 (x1 x9 x10)) = x1 (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x2 x3 x10))) (x1 (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x2 x4 x10))) (x1 (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x2 x5 x10))) (x1 (x1 (x2 x6 x8) (x1 (x2 x6 x9) (x2 x6 x10))) (x1 (x2 x7 x8) (x1 (x2 x7 x9) (x2 x7 x10)))))) (proof)
Theorem 96e70.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) (x1 x8 (x1 x9 (x1 x10 x11))) = x1 (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x2 x3 x11)))) (x1 (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x2 x4 x11)))) (x1 (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x2 x5 x11)))) (x1 (x1 (x2 x6 x8) (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x2 x6 x11)))) (x1 (x2 x7 x8) (x1 (x2 x7 x9) (x1 (x2 x7 x10) (x2 x7 x11))))))) (proof)
Theorem 8b8a9.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) (x1 x8 (x1 x9 (x1 x10 (x1 x11 x12)))) = x1 (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x2 x3 x12))))) (x1 (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x2 x4 x12))))) (x1 (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x2 x5 x12))))) (x1 (x1 (x2 x6 x8) (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x2 x6 x12))))) (x1 (x2 x7 x8) (x1 (x2 x7 x9) (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x2 x7 x12)))))))) (proof)
Theorem a33b6.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x0 x13x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 x13))))) = x1 (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x2 x3 x13)))))) (x1 (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x2 x4 x13)))))) (x1 (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x2 x5 x13)))))) (x1 (x1 (x2 x6 x8) (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x2 x6 x13)))))) (x1 (x2 x7 x8) (x1 (x2 x7 x9) (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x2 x7 x13))))))))) (proof)
Theorem 6c6f7.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x0 x13x0 x14x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 x14)))))) = x1 (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x2 x3 x14))))))) (x1 (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x2 x4 x14))))))) (x1 (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x2 x5 x14))))))) (x1 (x1 (x2 x6 x8) (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x2 x6 x14))))))) (x1 (x2 x7 x8) (x1 (x2 x7 x9) (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x2 x7 x14)))))))))) (proof)
Theorem a8c31.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x0 x13x0 x14x0 x15x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 x15))))))) = x1 (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x1 (x2 x3 x14) (x2 x3 x15)))))))) (x1 (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x1 (x2 x4 x14) (x2 x4 x15)))))))) (x1 (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x1 (x2 x5 x14) (x2 x5 x15)))))))) (x1 (x1 (x2 x6 x8) (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x1 (x2 x6 x14) (x2 x6 x15)))))))) (x1 (x2 x7 x8) (x1 (x2 x7 x9) (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x1 (x2 x7 x14) (x2 x7 x15))))))))))) (proof)
Theorem c240f.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) (x1 x9 x10) = x1 (x1 (x2 x3 x9) (x2 x3 x10)) (x1 (x1 (x2 x4 x9) (x2 x4 x10)) (x1 (x1 (x2 x5 x9) (x2 x5 x10)) (x1 (x1 (x2 x6 x9) (x2 x6 x10)) (x1 (x1 (x2 x7 x9) (x2 x7 x10)) (x1 (x2 x8 x9) (x2 x8 x10)))))) (proof)
Theorem ab0f3.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) (x1 x9 (x1 x10 x11)) = x1 (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x2 x3 x11))) (x1 (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x2 x4 x11))) (x1 (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x2 x5 x11))) (x1 (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x2 x6 x11))) (x1 (x1 (x2 x7 x9) (x1 (x2 x7 x10) (x2 x7 x11))) (x1 (x2 x8 x9) (x1 (x2 x8 x10) (x2 x8 x11))))))) (proof)
Theorem 1b2e4.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) (x1 x9 (x1 x10 (x1 x11 x12))) = x1 (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x2 x3 x12)))) (x1 (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x2 x4 x12)))) (x1 (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x2 x5 x12)))) (x1 (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x2 x6 x12)))) (x1 (x1 (x2 x7 x9) (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x2 x7 x12)))) (x1 (x2 x8 x9) (x1 (x2 x8 x10) (x1 (x2 x8 x11) (x2 x8 x12)))))))) (proof)
Theorem afa83.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x0 x13x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) (x1 x9 (x1 x10 (x1 x11 (x1 x12 x13)))) = x1 (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x2 x3 x13))))) (x1 (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x2 x4 x13))))) (x1 (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x2 x5 x13))))) (x1 (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x2 x6 x13))))) (x1 (x1 (x2 x7 x9) (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x2 x7 x13))))) (x1 (x2 x8 x9) (x1 (x2 x8 x10) (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x2 x8 x13))))))))) (proof)
Theorem 30e88.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x0 x13x0 x14x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 x14))))) = x1 (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x2 x3 x14)))))) (x1 (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x2 x4 x14)))))) (x1 (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x2 x5 x14)))))) (x1 (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x2 x6 x14)))))) (x1 (x1 (x2 x7 x9) (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x2 x7 x14)))))) (x1 (x2 x8 x9) (x1 (x2 x8 x10) (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x1 (x2 x8 x13) (x2 x8 x14)))))))))) (proof)
Theorem d7b62.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x0 x13x0 x14x0 x15x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 x15)))))) = x1 (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x1 (x2 x3 x14) (x2 x3 x15))))))) (x1 (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x1 (x2 x4 x14) (x2 x4 x15))))))) (x1 (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x1 (x2 x5 x14) (x2 x5 x15))))))) (x1 (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x1 (x2 x6 x14) (x2 x6 x15))))))) (x1 (x1 (x2 x7 x9) (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x1 (x2 x7 x14) (x2 x7 x15))))))) (x1 (x2 x8 x9) (x1 (x2 x8 x10) (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x1 (x2 x8 x13) (x1 (x2 x8 x14) (x2 x8 x15))))))))))) (proof)
Theorem 7be79.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x0 x13x0 x14x0 x15x0 x16x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 (x1 x15 x16))))))) = x1 (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x1 (x2 x3 x14) (x1 (x2 x3 x15) (x2 x3 x16)))))))) (x1 (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x1 (x2 x4 x14) (x1 (x2 x4 x15) (x2 x4 x16)))))))) (x1 (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x1 (x2 x5 x14) (x1 (x2 x5 x15) (x2 x5 x16)))))))) (x1 (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x1 (x2 x6 x14) (x1 (x2 x6 x15) (x2 x6 x16)))))))) (x1 (x1 (x2 x7 x9) (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x1 (x2 x7 x14) (x1 (x2 x7 x15) (x2 x7 x16)))))))) (x1 (x2 x8 x9) (x1 (x2 x8 x10) (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x1 (x2 x8 x13) (x1 (x2 x8 x14) (x1 (x2 x8 x15) (x2 x8 x16)))))))))))) (proof)
Theorem e6d5e.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) (x1 x10 x11) = x1 (x1 (x2 x3 x10) (x2 x3 x11)) (x1 (x1 (x2 x4 x10) (x2 x4 x11)) (x1 (x1 (x2 x5 x10) (x2 x5 x11)) (x1 (x1 (x2 x6 x10) (x2 x6 x11)) (x1 (x1 (x2 x7 x10) (x2 x7 x11)) (x1 (x1 (x2 x8 x10) (x2 x8 x11)) (x1 (x2 x9 x10) (x2 x9 x11))))))) (proof)
Theorem 503ac.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) (x1 x10 (x1 x11 x12)) = x1 (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x2 x3 x12))) (x1 (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x2 x4 x12))) (x1 (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x2 x5 x12))) (x1 (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x2 x6 x12))) (x1 (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x2 x7 x12))) (x1 (x1 (x2 x8 x10) (x1 (x2 x8 x11) (x2 x8 x12))) (x1 (x2 x9 x10) (x1 (x2 x9 x11) (x2 x9 x12)))))))) (proof)
Theorem f7ed5.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x0 x13x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) (x1 x10 (x1 x11 (x1 x12 x13))) = x1 (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x2 x3 x13)))) (x1 (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x2 x4 x13)))) (x1 (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x2 x5 x13)))) (x1 (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x2 x6 x13)))) (x1 (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x2 x7 x13)))) (x1 (x1 (x2 x8 x10) (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x2 x8 x13)))) (x1 (x2 x9 x10) (x1 (x2 x9 x11) (x1 (x2 x9 x12) (x2 x9 x13))))))))) (proof)
Theorem 641ca.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x0 x13x0 x14x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) (x1 x10 (x1 x11 (x1 x12 (x1 x13 x14)))) = x1 (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x2 x3 x14))))) (x1 (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x2 x4 x14))))) (x1 (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x2 x5 x14))))) (x1 (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x2 x6 x14))))) (x1 (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x2 x7 x14))))) (x1 (x1 (x2 x8 x10) (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x1 (x2 x8 x13) (x2 x8 x14))))) (x1 (x2 x9 x10) (x1 (x2 x9 x11) (x1 (x2 x9 x12) (x1 (x2 x9 x13) (x2 x9 x14)))))))))) (proof)
Theorem 7a734.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x0 x13x0 x14x0 x15x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 x15))))) = x1 (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x1 (x2 x3 x14) (x2 x3 x15)))))) (x1 (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x1 (x2 x4 x14) (x2 x4 x15)))))) (x1 (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x1 (x2 x5 x14) (x2 x5 x15)))))) (x1 (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x1 (x2 x6 x14) (x2 x6 x15)))))) (x1 (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x1 (x2 x7 x14) (x2 x7 x15)))))) (x1 (x1 (x2 x8 x10) (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x1 (x2 x8 x13) (x1 (x2 x8 x14) (x2 x8 x15)))))) (x1 (x2 x9 x10) (x1 (x2 x9 x11) (x1 (x2 x9 x12) (x1 (x2 x9 x13) (x1 (x2 x9 x14) (x2 x9 x15))))))))))) (proof)
Theorem 45365.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x0 x13x0 x14x0 x15x0 x16x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 (x1 x15 x16)))))) = x1 (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x1 (x2 x3 x14) (x1 (x2 x3 x15) (x2 x3 x16))))))) (x1 (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x1 (x2 x4 x14) (x1 (x2 x4 x15) (x2 x4 x16))))))) (x1 (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x1 (x2 x5 x14) (x1 (x2 x5 x15) (x2 x5 x16))))))) (x1 (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x1 (x2 x6 x14) (x1 (x2 x6 x15) (x2 x6 x16))))))) (x1 (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x1 (x2 x7 x14) (x1 (x2 x7 x15) (x2 x7 x16))))))) (x1 (x1 (x2 x8 x10) (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x1 (x2 x8 x13) (x1 (x2 x8 x14) (x1 (x2 x8 x15) (x2 x8 x16))))))) (x1 (x2 x9 x10) (x1 (x2 x9 x11) (x1 (x2 x9 x12) (x1 (x2 x9 x13) (x1 (x2 x9 x14) (x1 (x2 x9 x15) (x2 x9 x16)))))))))))) (proof)
Theorem de0dc.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x0 x13x0 x14x0 x15x0 x16x0 x17x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 (x1 x15 (x1 x16 x17))))))) = x1 (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x1 (x2 x3 x14) (x1 (x2 x3 x15) (x1 (x2 x3 x16) (x2 x3 x17)))))))) (x1 (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x1 (x2 x4 x14) (x1 (x2 x4 x15) (x1 (x2 x4 x16) (x2 x4 x17)))))))) (x1 (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x1 (x2 x5 x14) (x1 (x2 x5 x15) (x1 (x2 x5 x16) (x2 x5 x17)))))))) (x1 (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x1 (x2 x6 x14) (x1 (x2 x6 x15) (x1 (x2 x6 x16) (x2 x6 x17)))))))) (x1 (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x1 (x2 x7 x14) (x1 (x2 x7 x15) (x1 (x2 x7 x16) (x2 x7 x17)))))))) (x1 (x1 (x2 x8 x10) (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x1 (x2 x8 x13) (x1 (x2 x8 x14) (x1 (x2 x8 x15) (x1 (x2 x8 x16) (x2 x8 x17)))))))) (x1 (x2 x9 x10) (x1 (x2 x9 x11) (x1 (x2 x9 x12) (x1 (x2 x9 x13) (x1 (x2 x9 x14) (x1 (x2 x9 x15) (x1 (x2 x9 x16) (x2 x9 x17))))))))))))) (proof)
Theorem 74594.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 x10))))))) (x1 x11 x12) = x1 (x1 (x2 x3 x11) (x2 x3 x12)) (x1 (x1 (x2 x4 x11) (x2 x4 x12)) (x1 (x1 (x2 x5 x11) (x2 x5 x12)) (x1 (x1 (x2 x6 x11) (x2 x6 x12)) (x1 (x1 (x2 x7 x11) (x2 x7 x12)) (x1 (x1 (x2 x8 x11) (x2 x8 x12)) (x1 (x1 (x2 x9 x11) (x2 x9 x12)) (x1 (x2 x10 x11) (x2 x10 x12)))))))) (proof)
Theorem 31403.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x0 x13x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 x10))))))) (x1 x11 (x1 x12 x13)) = x1 (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x2 x3 x13))) (x1 (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x2 x4 x13))) (x1 (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x2 x5 x13))) (x1 (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x2 x6 x13))) (x1 (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x2 x7 x13))) (x1 (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x2 x8 x13))) (x1 (x1 (x2 x9 x11) (x1 (x2 x9 x12) (x2 x9 x13))) (x1 (x2 x10 x11) (x1 (x2 x10 x12) (x2 x10 x13))))))))) (proof)
Theorem 24a12.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x0 x13x0 x14x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 x10))))))) (x1 x11 (x1 x12 (x1 x13 x14))) = x1 (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x2 x3 x14)))) (x1 (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x2 x4 x14)))) (x1 (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x2 x5 x14)))) (x1 (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x2 x6 x14)))) (x1 (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x2 x7 x14)))) (x1 (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x1 (x2 x8 x13) (x2 x8 x14)))) (x1 (x1 (x2 x9 x11) (x1 (x2 x9 x12) (x1 (x2 x9 x13) (x2 x9 x14)))) (x1 (x2 x10 x11) (x1 (x2 x10 x12) (x1 (x2 x10 x13) (x2 x10 x14)))))))))) (proof)
Theorem ff328.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x0 x13x0 x14x0 x15x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 x10))))))) (x1 x11 (x1 x12 (x1 x13 (x1 x14 x15)))) = x1 (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x1 (x2 x3 x14) (x2 x3 x15))))) (x1 (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x1 (x2 x4 x14) (x2 x4 x15))))) (x1 (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x1 (x2 x5 x14) (x2 x5 x15))))) (x1 (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x1 (x2 x6 x14) (x2 x6 x15))))) (x1 (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x1 (x2 x7 x14) (x2 x7 x15))))) (x1 (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x1 (x2 x8 x13) (x1 (x2 x8 x14) (x2 x8 x15))))) (x1 (x1 (x2 x9 x11) (x1 (x2 x9 x12) (x1 (x2 x9 x13) (x1 (x2 x9 x14) (x2 x9 x15))))) (x1 (x2 x10 x11) (x1 (x2 x10 x12) (x1 (x2 x10 x13) (x1 (x2 x10 x14) (x2 x10 x15))))))))))) (proof)
Theorem 075c5.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x0 x13x0 x14x0 x15x0 x16x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 x10))))))) (x1 x11 (x1 x12 (x1 x13 (x1 x14 (x1 x15 x16))))) = x1 (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x1 (x2 x3 x14) (x1 (x2 x3 x15) (x2 x3 x16)))))) (x1 (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x1 (x2 x4 x14) (x1 (x2 x4 x15) (x2 x4 x16)))))) (x1 (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x1 (x2 x5 x14) (x1 (x2 x5 x15) (x2 x5 x16)))))) (x1 (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x1 (x2 x6 x14) (x1 (x2 x6 x15) (x2 x6 x16)))))) (x1 (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x1 (x2 x7 x14) (x1 (x2 x7 x15) (x2 x7 x16)))))) (x1 (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x1 (x2 x8 x13) (x1 (x2 x8 x14) (x1 (x2 x8 x15) (x2 x8 x16)))))) (x1 (x1 (x2 x9 x11) (x1 (x2 x9 x12) (x1 (x2 x9 x13) (x1 (x2 x9 x14) (x1 (x2 x9 x15) (x2 x9 x16)))))) (x1 (x2 x10 x11) (x1 (x2 x10 x12) (x1 (x2 x10 x13) (x1 (x2 x10 x14) (x1 (x2 x10 x15) (x2 x10 x16)))))))))))) (proof)
Theorem 5a91e.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x0 x13x0 x14x0 x15x0 x16x0 x17x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 x10))))))) (x1 x11 (x1 x12 (x1 x13 (x1 x14 (x1 x15 (x1 x16 x17)))))) = x1 (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x1 (x2 x3 x14) (x1 (x2 x3 x15) (x1 (x2 x3 x16) (x2 x3 x17))))))) (x1 (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x1 (x2 x4 x14) (x1 (x2 x4 x15) (x1 (x2 x4 x16) (x2 x4 x17))))))) (x1 (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x1 (x2 x5 x14) (x1 (x2 x5 x15) (x1 (x2 x5 x16) (x2 x5 x17))))))) (x1 (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x1 (x2 x6 x14) (x1 (x2 x6 x15) (x1 (x2 x6 x16) (x2 x6 x17))))))) (x1 (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x1 (x2 x7 x14) (x1 (x2 x7 x15) (x1 (x2 x7 x16) (x2 x7 x17))))))) (x1 (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x1 (x2 x8 x13) (x1 (x2 x8 x14) (x1 (x2 x8 x15) (x1 (x2 x8 x16) (x2 x8 x17))))))) (x1 (x1 (x2 x9 x11) (x1 (x2 x9 x12) (x1 (x2 x9 x13) (x1 (x2 x9 x14) (x1 (x2 x9 x15) (x1 (x2 x9 x16) (x2 x9 x17))))))) (x1 (x2 x10 x11) (x1 (x2 x10 x12) (x1 (x2 x10 x13) (x1 (x2 x10 x14) (x1 (x2 x10 x15) (x1 (x2 x10 x16) (x2 x10 x17))))))))))))) (proof)
Theorem 43f21.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x0 x13x0 x14x0 x15x0 x16x0 x17x0 x18x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 x10))))))) (x1 x11 (x1 x12 (x1 x13 (x1 x14 (x1 x15 (x1 x16 (x1 x17 x18))))))) = x1 (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x1 (x2 x3 x14) (x1 (x2 x3 x15) (x1 (x2 x3 x16) (x1 (x2 x3 x17) (x2 x3 x18)))))))) (x1 (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x1 (x2 x4 x14) (x1 (x2 x4 x15) (x1 (x2 x4 x16) (x1 (x2 x4 x17) (x2 x4 x18)))))))) (x1 (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x1 (x2 x5 x14) (x1 (x2 x5 x15) (x1 (x2 x5 x16) (x1 (x2 x5 x17) (x2 x5 x18)))))))) (x1 (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x1 (x2 x6 x14) (x1 (x2 x6 x15) (x1 (x2 x6 x16) (x1 (x2 x6 x17) (x2 x6 x18)))))))) (x1 (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x1 (x2 x7 x14) (x1 (x2 x7 x15) (x1 (x2 x7 x16) (x1 (x2 x7 x17) (x2 x7 x18)))))))) (x1 (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x1 (x2 x8 x13) (x1 (x2 x8 x14) (x1 (x2 x8 x15) (x1 (x2 x8 x16) (x1 (x2 x8 x17) (x2 x8 x18)))))))) (x1 (x1 (x2 x9 x11) (x1 (x2 x9 x12) (x1 (x2 x9 x13) (x1 (x2 x9 x14) (x1 (x2 x9 x15) (x1 (x2 x9 x16) (x1 (x2 x9 x17) (x2 x9 x18)))))))) (x1 (x2 x10 x11) (x1 (x2 x10 x12) (x1 (x2 x10 x13) (x1 (x2 x10 x14) (x1 (x2 x10 x15) (x1 (x2 x10 x16) (x1 (x2 x10 x17) (x2 x10 x18)))))))))))))) (proof)