Search for blocks/addresses/...

Proofgold Asset

asset id
6534985be3432998684dc97e2ed7b017cabdd45a454ce0e6632e55608b12e963
asset hash
21a3e08b11d2ea149b61d7f005770d5e4d9aef75861115a49b189b70141bfb08
bday / block
24878
tx
a5fa5..
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 6775d.. : ∀ 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 x6 (x1 x3 (x1 x5 (x1 x4 (x1 x2 x7))))
Theorem e700f.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x4 (x1 x6 (x1 x5 (x1 x3 x2))))
...

Theorem 1b665.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x4 (x1 x6 (x1 x5 (x1 x3 x2))))
...

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 d1e84.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x4 (x1 x6 (x1 x5 (x1 x2 x3))))
...

Theorem c6e68.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x4 (x1 x6 (x1 x5 (x1 x2 x3))))
...

Known a4b60.. : ∀ 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 x6 (x1 x3 (x1 x4 (x1 x2 (x1 x5 x7))))
Theorem caa8e.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x4 (x1 x5 (x1 x2 (x1 x6 x3))))
...

Theorem 1714a.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x4 (x1 x5 (x1 x2 (x1 x6 x3))))
...

Known 0f4fc.. : ∀ 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 x6 (x1 x4 (x1 x5 (x1 x2 (x1 x3 x7))))
Theorem 6d9a9.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x4 (x1 x5 (x1 x2 (x1 x3 x6))))
...

Theorem 0dbc2.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x4 (x1 x5 (x1 x2 (x1 x3 x6))))
...

Theorem c7094.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x4 (x1 x5 (x1 x3 (x1 x6 x2))))
...

Theorem d4d1e.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x4 (x1 x5 (x1 x3 (x1 x6 x2))))
...

Known 5b962.. : ∀ 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 x6 (x1 x4 (x1 x5 (x1 x3 (x1 x2 x7))))
Theorem b05db.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x4 (x1 x5 (x1 x3 (x1 x2 x6))))
...

Theorem 2bd4b.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x4 (x1 x5 (x1 x3 (x1 x2 x6))))
...

Known c925c.. : ∀ 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 x6 (x1 x3 (x1 x4 (x1 x5 (x1 x2 x7))))
Theorem 80892.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x4 (x1 x5 (x1 x6 (x1 x3 x2))))
...

Theorem 3628c.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x4 (x1 x5 (x1 x6 (x1 x3 x2))))
...

Theorem bd04f.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x4 (x1 x5 (x1 x6 (x1 x2 x3))))
...

Theorem cb604.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x4 (x1 x5 (x1 x6 (x1 x2 x3))))
...

Known 58437.. : ∀ 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 x6 (x1 x4 (x1 x3 (x1 x2 (x1 x5 x7))))
Theorem 24d1f.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x4 (x1 x3 (x1 x2 (x1 x6 x5))))
...

Theorem 90e54.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x4 (x1 x3 (x1 x2 (x1 x6 x5))))
...

Theorem b792e.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x4 (x1 x3 (x1 x2 (x1 x5 x6))))
...

Theorem 6b123.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x4 (x1 x3 (x1 x2 (x1 x5 x6))))
...

Known 303f8.. : ∀ 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 x6 (x1 x3 (x1 x2 (x1 x4 (x1 x5 x7))))
Theorem 0d37b.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x4 (x1 x3 (x1 x5 (x1 x6 x2))))
...

Theorem bfb21.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x4 (x1 x3 (x1 x5 (x1 x6 x2))))
...

Known 6daf3.. : ∀ 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 x6 (x1 x4 (x1 x3 (x1 x5 (x1 x2 x7))))
Theorem 65c0a.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x4 (x1 x3 (x1 x5 (x1 x2 x6))))
...

Theorem de30f.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x4 (x1 x3 (x1 x5 (x1 x2 x6))))
...

Known cbff5.. : ∀ 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 x6 (x1 x3 (x1 x2 (x1 x5 (x1 x4 x7))))
Theorem 00b70.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x4 (x1 x3 (x1 x6 (x1 x5 x2))))
...

Theorem 20bcc.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x4 (x1 x3 (x1 x6 (x1 x5 x2))))
...

Theorem 479ab.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x4 (x1 x3 (x1 x6 (x1 x2 x5))))
...

Theorem 6543d.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x4 (x1 x3 (x1 x6 (x1 x2 x5))))
...

Known 7cae8.. : ∀ 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 x6 (x1 x4 (x1 x2 (x1 x3 (x1 x5 x7))))
Theorem 83da1.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x4 (x1 x2 (x1 x3 (x1 x6 x5))))
...

Theorem 86586.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x4 (x1 x2 (x1 x3 (x1 x6 x5))))
...

Theorem 0bd5b.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x4 (x1 x2 (x1 x3 (x1 x5 x6))))
...

Theorem 11981.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x4 (x1 x2 (x1 x3 (x1 x5 x6))))
...

Theorem 57642.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x4 (x1 x2 (x1 x5 (x1 x6 x3))))
...

Theorem 4dd4a.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x4 (x1 x2 (x1 x5 (x1 x6 x3))))
...

Known a445d.. : ∀ 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 x6 (x1 x4 (x1 x2 (x1 x5 (x1 x3 x7))))
Theorem 411d5.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x4 (x1 x2 (x1 x5 (x1 x3 x6))))
...

Theorem 7822b.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x4 (x1 x2 (x1 x5 (x1 x3 x6))))
...

Theorem ffb3f.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x4 (x1 x2 (x1 x6 (x1 x5 x3))))
...

Theorem fb477.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x4 (x1 x2 (x1 x6 (x1 x5 x3))))
...

Theorem cb3d1.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x4 (x1 x2 (x1 x6 (x1 x3 x5))))
...

Theorem a7091.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x4 (x1 x2 (x1 x6 (x1 x3 x5))))
...

Theorem 868ca.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x6 (x1 x2 (x1 x4 x3))))
...

Theorem dae69.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x6 (x1 x2 (x1 x4 x3))))
...

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 5d5e9.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x6 (x1 x2 (x1 x3 x4))))
...

Theorem 5014f.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x6 (x1 x2 (x1 x3 x4))))
...

Theorem f1f14.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x6 (x1 x3 (x1 x4 x2))))
...

Theorem 16d14.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x6 (x1 x3 (x1 x4 x2))))
...

Theorem 65f28.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x6 (x1 x3 (x1 x2 x4))))
...

Theorem d354f.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x6 (x1 x3 (x1 x2 x4))))
...

Theorem 799b9.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x6 (x1 x4 (x1 x3 x2))))
...

Theorem 97d6b.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x6 (x1 x4 (x1 x3 x2))))
...

Theorem 527a8.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x6 (x1 x4 (x1 x2 x3))))
...

Theorem feb27.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x6 (x1 x4 (x1 x2 x3))))
...

Theorem 147db.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x4 (x1 x2 (x1 x6 x3))))
...

Theorem 5a8bd.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x4 (x1 x2 (x1 x6 x3))))
...

Known 9594a.. : ∀ 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 x6 (x1 x5 (x1 x4 (x1 x2 (x1 x3 x7))))
Theorem 5e2b4.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x4 (x1 x2 (x1 x3 x6))))
...

Theorem 7fc11.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x4 (x1 x2 (x1 x3 x6))))
...

Theorem eee3b.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x4 (x1 x3 (x1 x6 x2))))
...

Theorem 57a28.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x4 (x1 x3 (x1 x6 x2))))
...

Known babbf.. : ∀ 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 x6 (x1 x5 (x1 x4 (x1 x3 (x1 x2 x7))))
Theorem a9e18.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x4 (x1 x3 (x1 x2 x6))))
...

Theorem f56ad.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x4 (x1 x3 (x1 x2 x6))))
...

Theorem c10de.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x4 (x1 x6 (x1 x3 x2))))
...

Theorem ba819.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x4 (x1 x6 (x1 x3 x2))))
...

Theorem 6dbb6.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x4 (x1 x6 (x1 x2 x3))))
...

Theorem 5fa8e.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x4 (x1 x6 (x1 x2 x3))))
...

Theorem 3d75c.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x3 (x1 x2 (x1 x6 x4))))
...

Theorem 6f06a.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x3 (x1 x2 (x1 x6 x4))))
...

Known 8c4b6.. : ∀ 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 x6 (x1 x5 (x1 x3 (x1 x2 (x1 x4 x7))))
Theorem dcfb0.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x3 (x1 x2 (x1 x4 x6))))
...

Theorem edb67.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x3 (x1 x2 (x1 x4 x6))))
...

Theorem 3e530.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x3 (x1 x4 (x1 x2 x6))))
...

Theorem 11543.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x3 (x1 x4 (x1 x2 x6))))
...

Theorem d142c.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x3 (x1 x6 (x1 x2 x4))))
...

Theorem 7365a.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x3 (x1 x6 (x1 x2 x4))))
...

Theorem f471f.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x2 (x1 x3 (x1 x6 x4))))
...

Theorem 8f7e0.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x2 (x1 x3 (x1 x6 x4))))
...

Known 76f9e.. : ∀ 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 x6 (x1 x5 (x1 x2 (x1 x3 (x1 x4 x7))))
Theorem 026fd.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x2 (x1 x3 (x1 x4 x6))))
...

Theorem 27483.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x2 (x1 x3 (x1 x4 x6))))
...

Theorem c8e1e.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x2 (x1 x4 (x1 x6 x3))))
...

Theorem 13968.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x2 (x1 x4 (x1 x6 x3))))
...

Known 4d854.. : ∀ 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 x6 (x1 x5 (x1 x2 (x1 x4 (x1 x3 x7))))
Theorem 52bc2.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x2 (x1 x4 (x1 x3 x6))))
...

Theorem 6f107.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x2 (x1 x4 (x1 x3 x6))))
...

Theorem 2c81b.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x2 (x1 x6 (x1 x4 x3))))
...

Theorem ac6f4.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x2 (x1 x6 (x1 x4 x3))))
...

Theorem 0d065.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x2 (x1 x6 (x1 x3 x4))))
...

Theorem 6e354.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x5 (x1 x2 (x1 x6 (x1 x3 x4))))
...

Theorem 9dd73.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x6 (x1 x5 (x1 x2 (x1 x4 x3))))
...

Theorem 9442b.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x6 (x1 x5 (x1 x2 (x1 x4 x3))))
...

Theorem 85c8e.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x6 (x1 x5 (x1 x2 (x1 x3 x4))))
...

Theorem 06b51.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x6 (x1 x5 (x1 x2 (x1 x3 x4))))
...

Theorem cf676.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x6 (x1 x5 (x1 x3 (x1 x2 x4))))
...

Theorem fb422.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x6 (x1 x5 (x1 x3 (x1 x2 x4))))
...

Theorem 2461d.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x6 (x1 x5 (x1 x4 (x1 x3 x2))))
...

Theorem ed5f6.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x6 (x1 x5 (x1 x4 (x1 x3 x2))))
...

Theorem 640d0.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x6 (x1 x5 (x1 x4 (x1 x2 x3))))
...

Theorem 8b4c8.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x6 (x1 x5 (x1 x4 (x1 x2 x3))))
...

Theorem 35a7f.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x6 (x1 x4 (x1 x2 (x1 x5 x3))))
...

Theorem 6b055.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x6 (x1 x4 (x1 x2 (x1 x5 x3))))
...

Theorem f0bf4.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x6 (x1 x4 (x1 x2 (x1 x3 x5))))
...

Theorem 1b76b.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x6 (x1 x4 (x1 x2 (x1 x3 x5))))
...

Theorem 91586.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x6 (x1 x4 (x1 x3 (x1 x2 x5))))
...

Theorem 2e381.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x6 (x1 x4 (x1 x3 (x1 x2 x5))))
...

Theorem f4654.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x6 (x1 x4 (x1 x5 (x1 x3 x2))))
...

Theorem c31ac.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x6 (x1 x4 (x1 x5 (x1 x3 x2))))
...

Theorem 781bc.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x6 (x1 x4 (x1 x5 (x1 x2 x3))))
...

Theorem e692b.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x6 (x1 x4 (x1 x5 (x1 x2 x3))))
...

Theorem 68f17.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x6 (x1 x3 (x1 x2 (x1 x5 x4))))
...

Theorem 4603c.. : ∀ 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 . x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x7 (x1 x6 (x1 x3 (x1 x2 (x1 x5 x4))))
...