Search for blocks/addresses/...

Proofgold Asset

asset id
9759dcf42c5126d431b0035847be5ef661d080b6a50e593f7e0b52620e36bc00
asset hash
3287d0670cb9d8f1f71d9d91cc44963cae72259c95b04f5747d2d231981bdf99
bday / block
27050
tx
7d861..
preasset
doc published by Pr5Zc..
Known 75b00.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))∀ x2 x3 x4 x5 x6 x7 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x2 x7))))
Known 77efa.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x8 (x1 x5 (x1 x2 (x1 x6 (x1 x3 (x1 x7 (x1 x4 x9))))))
Theorem ef3f2.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x7 (x1 x3 (x1 x8 (x1 x5 x4))))))
...

Theorem e78c7.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x7 (x1 x3 (x1 x8 (x1 x5 x4))))))
...

Known 93eac.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))∀ x2 x3 x4 x5 x6 . x0 x2x0 x3x0 x4x0 x5x0 x6x1 x2 (x1 x3 (x1 x4 (x1 x5 x6))) = x1 x3 (x1 x4 (x1 x5 (x1 x2 x6)))
Theorem 1349d.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x7 (x1 x3 (x1 x8 (x1 x4 x5))))))
...

Theorem 6f6aa.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x7 (x1 x3 (x1 x8 (x1 x4 x5))))))
...

Known 75401.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x8 (x1 x5 (x1 x2 (x1 x7 (x1 x6 (x1 x3 (x1 x4 x9))))))
Theorem e23dc.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x7 (x1 x3 (x1 x5 x4))))))
...

Theorem f1770.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x7 (x1 x3 (x1 x5 x4))))))
...

Theorem 40772.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x7 (x1 x3 (x1 x4 x5))))))
...

Theorem d7519.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x7 (x1 x3 (x1 x4 x5))))))
...

Known c0c54.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))∀ x2 x3 x4 x5 x6 x7 x8 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) = x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x2 x8)))))
Theorem f17de.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x7 (x1 x4 (x1 x5 x3))))))
...

Theorem c7f28.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x7 (x1 x4 (x1 x5 x3))))))
...

Known 8ac96.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x8 (x1 x5 (x1 x2 (x1 x7 (x1 x6 (x1 x4 (x1 x3 x9))))))
Theorem 3740a.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x7 (x1 x4 (x1 x3 x5))))))
...

Theorem 7e2fe.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x7 (x1 x4 (x1 x3 x5))))))
...

Theorem 074fd.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x7 (x1 x5 (x1 x4 x3))))))
...

Theorem ae786.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x7 (x1 x5 (x1 x4 x3))))))
...

Theorem bf75a.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x7 (x1 x5 (x1 x3 x4))))))
...

Theorem 28426.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x7 (x1 x5 (x1 x3 x4))))))
...

Known b718f.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x8 (x1 x5 (x1 x2 (x1 x7 (x1 x4 (x1 x3 (x1 x6 x9))))))
Theorem c3ef2.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x5 (x1 x3 (x1 x7 x4))))))
...

Theorem fa3e8.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x5 (x1 x3 (x1 x7 x4))))))
...

Known a16d8.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x8 (x1 x6 (x1 x2 (x1 x7 (x1 x5 (x1 x3 (x1 x4 x9))))))
Theorem 3939b.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x5 (x1 x3 (x1 x4 x7))))))
...

Theorem 05daf.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x5 (x1 x3 (x1 x4 x7))))))
...

Theorem c3fd4.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x5 (x1 x4 (x1 x7 x3))))))
...

Theorem 10ba0.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x5 (x1 x4 (x1 x7 x3))))))
...

Known b597c.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x8 (x1 x6 (x1 x2 (x1 x7 (x1 x5 (x1 x4 (x1 x3 x9))))))
Theorem 4e945.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x5 (x1 x4 (x1 x3 x7))))))
...

Theorem 9061f.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x5 (x1 x4 (x1 x3 x7))))))
...

Known cf3e3.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x8 (x1 x5 (x1 x2 (x1 x7 (x1 x4 (x1 x6 (x1 x3 x9))))))
Theorem e2ed9.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x5 (x1 x7 (x1 x4 x3))))))
...

Theorem a8633.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x5 (x1 x7 (x1 x4 x3))))))
...

Theorem 1e8cc.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x5 (x1 x7 (x1 x3 x4))))))
...

Theorem 4e35f.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x5 (x1 x7 (x1 x3 x4))))))
...

Theorem 5a6e5.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x4 (x1 x3 (x1 x7 x5))))))
...

Theorem a57a9.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x4 (x1 x3 (x1 x7 x5))))))
...

Known ceaa4.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x8 (x1 x6 (x1 x2 (x1 x7 (x1 x4 (x1 x3 (x1 x5 x9))))))
Theorem ee1a3.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x4 (x1 x3 (x1 x5 x7))))))
...

Theorem 32d16.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x4 (x1 x3 (x1 x5 x7))))))
...

Known 27b85.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x8 (x1 x5 (x1 x2 (x1 x7 (x1 x3 (x1 x4 (x1 x6 x9))))))
Theorem e916a.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x4 (x1 x5 (x1 x7 x3))))))
...

Theorem 4195e.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x4 (x1 x5 (x1 x7 x3))))))
...

Known bcba5.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x8 (x1 x6 (x1 x2 (x1 x7 (x1 x4 (x1 x5 (x1 x3 x9))))))
Theorem 8cbea.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x4 (x1 x5 (x1 x3 x7))))))
...

Theorem 36c72.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x4 (x1 x5 (x1 x3 x7))))))
...

Known 0a0bb.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x8 (x1 x5 (x1 x2 (x1 x7 (x1 x3 (x1 x6 (x1 x4 x9))))))
Theorem b2839.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x4 (x1 x7 (x1 x5 x3))))))
...

Theorem 747d5.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x4 (x1 x7 (x1 x5 x3))))))
...

Theorem 3464e.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x4 (x1 x7 (x1 x3 x5))))))
...

Theorem 25c70.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x4 (x1 x7 (x1 x3 x5))))))
...

Theorem b4c5e.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x3 (x1 x4 (x1 x7 x5))))))
...

Theorem 54be7.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x3 (x1 x4 (x1 x7 x5))))))
...

Known d0aa4.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x8 (x1 x6 (x1 x2 (x1 x7 (x1 x3 (x1 x4 (x1 x5 x9))))))
Theorem b17ad.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x3 (x1 x4 (x1 x5 x7))))))
...

Theorem 2b2f5.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x3 (x1 x4 (x1 x5 x7))))))
...

Theorem 9c3ca.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x3 (x1 x5 (x1 x7 x4))))))
...

Theorem bcaf2.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x3 (x1 x5 (x1 x7 x4))))))
...

Known 5fb51.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x8 (x1 x6 (x1 x2 (x1 x7 (x1 x3 (x1 x5 (x1 x4 x9))))))
Theorem 65cd5.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x3 (x1 x5 (x1 x4 x7))))))
...

Theorem 88da2.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x3 (x1 x5 (x1 x4 x7))))))
...

Theorem 1f629.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x3 (x1 x7 (x1 x5 x4))))))
...

Theorem 565ea.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x3 (x1 x7 (x1 x5 x4))))))
...

Theorem 71a24.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x3 (x1 x7 (x1 x4 x5))))))
...

Theorem a53ea.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x6 (x1 x2 (x1 x8 (x1 x3 (x1 x7 (x1 x4 x5))))))
...

Known 6b685.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x8 (x1 x6 (x1 x7 (x1 x2 (x1 x5 (x1 x3 (x1 x4 x9))))))
Theorem 667ab.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x6 (x1 x3 (x1 x5 x4))))))
...

Theorem 9d8e7.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x6 (x1 x3 (x1 x5 x4))))))
...

Theorem 47904.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x6 (x1 x3 (x1 x4 x5))))))
...

Theorem 6f849.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x6 (x1 x3 (x1 x4 x5))))))
...

Theorem 71956.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x6 (x1 x4 (x1 x5 x3))))))
...

Theorem d0c7e.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x6 (x1 x4 (x1 x5 x3))))))
...

Known b2a74.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x8 (x1 x6 (x1 x7 (x1 x2 (x1 x5 (x1 x4 (x1 x3 x9))))))
Theorem ae607.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x6 (x1 x4 (x1 x3 x5))))))
...

Theorem c366e.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x6 (x1 x4 (x1 x3 x5))))))
...

Theorem 84b1c.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x6 (x1 x5 (x1 x4 x3))))))
...

Theorem 14b08.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x6 (x1 x5 (x1 x4 x3))))))
...

Theorem 59b90.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x6 (x1 x5 (x1 x3 x4))))))
...

Theorem 1baad.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x6 (x1 x5 (x1 x3 x4))))))
...

Known d5e60.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x8 (x1 x6 (x1 x7 (x1 x2 (x1 x4 (x1 x3 (x1 x5 x9))))))
Theorem 8187c.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x5 (x1 x3 (x1 x6 x4))))))
...

Theorem 10f90.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x5 (x1 x3 (x1 x6 x4))))))
...

Known 45f87.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))∀ x2 x3 x4 x5 . x0 x2x0 x3x0 x4x0 x5x1 x2 (x1 x3 (x1 x4 x5)) = x1 x3 (x1 x4 (x1 x2 x5))
Theorem 9dbf5.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x5 (x1 x3 (x1 x4 x6))))))
...

Theorem a398b.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x5 (x1 x3 (x1 x4 x6))))))
...

Theorem 64a49.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x5 (x1 x4 (x1 x6 x3))))))
...

Theorem 94328.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x5 (x1 x4 (x1 x6 x3))))))
...

Theorem a4ae3.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x5 (x1 x4 (x1 x3 x6))))))
...

Theorem 70959.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x5 (x1 x4 (x1 x3 x6))))))
...

Known b3efe.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x8 (x1 x6 (x1 x7 (x1 x2 (x1 x4 (x1 x5 (x1 x3 x9))))))
Theorem 3724f.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x5 (x1 x6 (x1 x4 x3))))))
...

Theorem 9da01.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x5 (x1 x6 (x1 x4 x3))))))
...

Theorem 8bd1c.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x5 (x1 x6 (x1 x3 x4))))))
...

Theorem 4afa3.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x5 (x1 x6 (x1 x3 x4))))))
...

Theorem bf44c.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x4 (x1 x3 (x1 x6 x5))))))
...

Theorem bc737.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x4 (x1 x3 (x1 x6 x5))))))
...

Theorem cb6fc.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x4 (x1 x3 (x1 x5 x6))))))
...

Theorem fe8b6.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x4 (x1 x3 (x1 x5 x6))))))
...

Known 54952.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x8 (x1 x6 (x1 x7 (x1 x2 (x1 x3 (x1 x4 (x1 x5 x9))))))
Theorem e588e.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x4 (x1 x5 (x1 x6 x3))))))
...

Theorem 22769.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x4 (x1 x5 (x1 x6 x3))))))
...

Theorem f44ee.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x4 (x1 x5 (x1 x3 x6))))))
...

Theorem 481b9.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x4 (x1 x5 (x1 x3 x6))))))
...

Known 3bc94.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x8 (x1 x6 (x1 x7 (x1 x2 (x1 x3 (x1 x5 (x1 x4 x9))))))
Theorem d4a59.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x4 (x1 x6 (x1 x5 x3))))))
...

Theorem 57592.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x4 (x1 x6 (x1 x5 x3))))))
...

Theorem c2645.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x4 (x1 x6 (x1 x3 x5))))))
...

Theorem fd168.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x4 (x1 x6 (x1 x3 x5))))))
...

Theorem 375b4.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x3 (x1 x4 (x1 x6 x5))))))
...

Theorem d84de.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x3 (x1 x4 (x1 x6 x5))))))
...

Theorem 59b38.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x3 (x1 x4 (x1 x5 x6))))))
...

Theorem 181b8.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x3 (x1 x4 (x1 x5 x6))))))
...

Theorem 24ee3.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x3 (x1 x5 (x1 x6 x4))))))
...

Theorem 3d671.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x3 (x1 x5 (x1 x6 x4))))))
...

Theorem ba9d8.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x3 (x1 x5 (x1 x4 x6))))))
...

Theorem 68c4c.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x3 (x1 x5 (x1 x4 x6))))))
...

Theorem a3cb8.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x3 (x1 x6 (x1 x5 x4))))))
...

Theorem 43401.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x3 (x1 x6 (x1 x5 x4))))))
...

Theorem c00e6.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x3 (x1 x6 (x1 x4 x5))))))
...

Theorem 647c0.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x2 (x1 x3 (x1 x6 (x1 x4 x5))))))
...

Known 2bea3.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x8 (x1 x6 (x1 x7 (x1 x3 (x1 x5 (x1 x2 (x1 x4 x9))))))
Theorem b3ddc.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x3 (x1 x6 (x1 x2 (x1 x5 x4))))))
...

Theorem 5d0a8.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x3 (x1 x6 (x1 x2 (x1 x5 x4))))))
...

Theorem db389.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x3 (x1 x6 (x1 x2 (x1 x4 x5))))))
...

Theorem 856a8.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x3 (x1 x6 (x1 x2 (x1 x4 x5))))))
...

Known 07a54.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x8 (x1 x5 (x1 x7 (x1 x6 (x1 x3 (x1 x4 (x1 x2 x9))))))
Theorem 6e718.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4))(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x3 (x1 x6 (x1 x4 (x1 x2 x5))))))
...

Theorem f0706.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x7 (x1 x8 (x1 x3 (x1 x6 (x1 x4 (x1 x2 x5))))))
...