Search for blocks/addresses/...

Proofgold Address

address
PUdGQv5xXSgGZz1UHZRAuYNVLh45DyySTfQ
total
0
mg
-
conjpub
-
current assets
a25e4../7913b.. bday: 38738 doc published by PrCmT..
Conjecture 42fc4..aK1 : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . ∀ x5 : ι → ι → ι . ∀ x6 : ι → ι → ι → ι . ∀ x7 : ι → ι → ι . ∀ x8 x9 : ι → ι → ι → ι . x4x0(∀ x10 . x10x0∀ x11 . x11x0x1 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0x3 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0x2 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0x5 x10 x11 = x2 (x1 x11 x10) (x1 x10 x11))(∀ x10 . x10x0∀ x11 . x11x0x5 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x6 x10 x11 x12 = x2 (x1 x10 (x1 x11 x12)) (x1 (x1 x10 x11) x12))(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x6 x10 x11 x12x0)(∀ x10 . x10x0∀ x11 . x11x0x7 x10 x11 = x2 x11 (x1 x10 x11))(∀ x10 . x10x0∀ x11 . x11x0x7 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x8 x10 x11 x12 = x2 (x1 x12 x11) (x1 x12 (x1 x11 x10)))(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x8 x10 x11 x12x0)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x9 x10 x11 x12 = x3 (x1 (x1 x10 x11) x12) (x1 x11 x12))(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x9 x10 x11 x12x0)(∀ x10 . x10x0x1 x4 x10 = x10)(∀ x10 . x10x0x1 x10 x4 = x10)(∀ x10 . x10x0∀ x11 . x11x0x2 x10 (x1 x10 x11) = x11)(∀ x10 . x10x0∀ x11 . x11x0x1 x10 (x2 x10 x11) = x11)(∀ x10 . x10x0∀ x11 . x11x0x3 (x1 x10 x11) x11 = x10)(∀ x10 . x10x0∀ x11 . x11x0x1 (x3 x10 x11) x11 = x10)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x7 (x7 x10 x11) x12 = x7 (x7 x10 x12) x11)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0x7 (x8 x10 x11 x12) x13 = x8 (x7 x10 x13) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0x7 (x9 x10 x11 x12) x13 = x9 (x7 x10 x13) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0x8 (x9 x10 x11 x12) x13 x14 = x9 (x8 x10 x13 x14) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0x8 (x8 x10 x11 x12) x13 x14 = x8 (x8 x10 x13 x14) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0x9 (x9 x10 x11 x12) x13 x14 = x9 (x9 x10 x13 x14) x11 x12)∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0x6 (x5 x10 x11) x12 x13 = x4
Conjecture eac1e..aa1 : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . ∀ x5 : ι → ι → ι . ∀ x6 : ι → ι → ι → ι . ∀ x7 : ι → ι → ι . ∀ x8 x9 : ι → ι → ι → ι . x4x0(∀ x10 . x10x0∀ x11 . x11x0x1 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0x3 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0x2 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0x5 x10 x11 = x2 (x1 x11 x10) (x1 x10 x11))(∀ x10 . x10x0∀ x11 . x11x0x5 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x6 x10 x11 x12 = x2 (x1 x10 (x1 x11 x12)) (x1 (x1 x10 x11) x12))(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x6 x10 x11 x12x0)(∀ x10 . x10x0∀ x11 . x11x0x7 x10 x11 = x2 x11 (x1 x10 x11))(∀ x10 . x10x0∀ x11 . x11x0x7 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x8 x10 x11 x12 = x2 (x1 x12 x11) (x1 x12 (x1 x11 x10)))(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x8 x10 x11 x12x0)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x9 x10 x11 x12 = x3 (x1 (x1 x10 x11) x12) (x1 x11 x12))(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x9 x10 x11 x12x0)(∀ x10 . x10x0x1 x4 x10 = x10)(∀ x10 . x10x0x1 x10 x4 = x10)(∀ x10 . x10x0∀ x11 . x11x0x2 x10 (x1 x10 x11) = x11)(∀ x10 . x10x0∀ x11 . x11x0x1 x10 (x2 x10 x11) = x11)(∀ x10 . x10x0∀ x11 . x11x0x3 (x1 x10 x11) x11 = x10)(∀ x10 . x10x0∀ x11 . x11x0x1 (x3 x10 x11) x11 = x10)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x7 (x7 x10 x11) x12 = x7 (x7 x10 x12) x11)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0x7 (x8 x10 x11 x12) x13 = x8 (x7 x10 x13) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0x7 (x9 x10 x11 x12) x13 = x9 (x7 x10 x13) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0x8 (x9 x10 x11 x12) x13 x14 = x9 (x8 x10 x13 x14) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0x8 (x8 x10 x11 x12) x13 x14 = x8 (x8 x10 x13 x14) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0x9 (x9 x10 x11 x12) x13 x14 = x9 (x9 x10 x13 x14) x11 x12)∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0x6 (x6 x10 x11 x12) x13 x14 = x4
Conjecture 975e1..com__aa1 : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . ∀ x5 : ι → ι → ι . ∀ x6 : ι → ι → ι → ι . ∀ x7 : ι → ι → ι . ∀ x8 x9 : ι → ι → ι → ι . x4x0(∀ x10 . x10x0∀ x11 . x11x0x1 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0x3 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0x2 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0x5 x10 x11 = x2 (x1 x11 x10) (x1 x10 x11))(∀ x10 . x10x0∀ x11 . x11x0x5 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x6 x10 x11 x12 = x2 (x1 x10 (x1 x11 x12)) (x1 (x1 x10 x11) x12))(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x6 x10 x11 x12x0)(∀ x10 . x10x0∀ x11 . x11x0x7 x10 x11 = x2 x11 (x1 x10 x11))(∀ x10 . x10x0∀ x11 . x11x0x7 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x8 x10 x11 x12 = x2 (x1 x12 x11) (x1 x12 (x1 x11 x10)))(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x8 x10 x11 x12x0)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x9 x10 x11 x12 = x3 (x1 (x1 x10 x11) x12) (x1 x11 x12))(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x9 x10 x11 x12x0)(∀ x10 . x10x0x1 x4 x10 = x10)(∀ x10 . x10x0x1 x10 x4 = x10)(∀ x10 . x10x0∀ x11 . x11x0x2 x10 (x1 x10 x11) = x11)(∀ x10 . x10x0∀ x11 . x11x0x1 x10 (x2 x10 x11) = x11)(∀ x10 . x10x0∀ x11 . x11x0x3 (x1 x10 x11) x11 = x10)(∀ x10 . x10x0∀ x11 . x11x0x1 (x3 x10 x11) x11 = x10)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x7 (x7 x10 x11) x12 = x7 (x7 x10 x12) x11)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0x7 (x8 x10 x11 x12) x13 = x8 (x7 x10 x13) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0x7 (x9 x10 x11 x12) x13 = x9 (x7 x10 x13) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0x8 (x9 x10 x11 x12) x13 x14 = x9 (x8 x10 x13 x14) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0x8 (x8 x10 x11 x12) x13 x14 = x8 (x8 x10 x13 x14) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0x9 (x9 x10 x11 x12) x13 x14 = x9 (x9 x10 x13 x14) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0x1 x10 x11 = x1 x11 x10)∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0x6 (x6 x10 x11 x12) x13 x14 = x4
Conjecture 79b0e..middle_Bol__aa1 : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . ∀ x5 : ι → ι → ι . ∀ x6 : ι → ι → ι → ι . ∀ x7 : ι → ι → ι . ∀ x8 x9 : ι → ι → ι → ι . x4x0(∀ x10 . x10x0∀ x11 . x11x0x1 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0x3 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0x2 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0x5 x10 x11 = x2 (x1 x11 x10) (x1 x10 x11))(∀ x10 . x10x0∀ x11 . x11x0x5 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x6 x10 x11 x12 = x2 (x1 x10 (x1 x11 x12)) (x1 (x1 x10 x11) x12))(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x6 x10 x11 x12x0)(∀ x10 . x10x0∀ x11 . x11x0x7 x10 x11 = x2 x11 (x1 x10 x11))(∀ x10 . x10x0∀ x11 . x11x0x7 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x8 x10 x11 x12 = x2 (x1 x12 x11) (x1 x12 (x1 x11 x10)))(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x8 x10 x11 x12x0)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x9 x10 x11 x12 = x3 (x1 (x1 x10 x11) x12) (x1 x11 x12))(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x9 x10 x11 x12x0)(∀ x10 . x10x0x1 x4 x10 = x10)(∀ x10 . x10x0x1 x10 x4 = x10)(∀ x10 . x10x0∀ x11 . x11x0x2 x10 (x1 x10 x11) = x11)(∀ x10 . x10x0∀ x11 . x11x0x1 x10 (x2 x10 x11) = x11)(∀ x10 . x10x0∀ x11 . x11x0x3 (x1 x10 x11) x11 = x10)(∀ x10 . x10x0∀ x11 . x11x0x1 (x3 x10 x11) x11 = x10)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x7 (x7 x10 x11) x12 = x7 (x7 x10 x12) x11)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0x7 (x8 x10 x11 x12) x13 = x8 (x7 x10 x13) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0x7 (x9 x10 x11 x12) x13 = x9 (x7 x10 x13) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0x8 (x9 x10 x11 x12) x13 x14 = x9 (x8 x10 x13 x14) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0x8 (x8 x10 x11 x12) x13 x14 = x8 (x8 x10 x13 x14) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0x9 (x9 x10 x11 x12) x13 x14 = x9 (x9 x10 x13 x14) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x1 x10 (x2 (x1 x11 x12) x10) = x1 (x3 x10 x12) (x2 x11 x10))∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0x6 (x6 x10 x11 x12) x13 x14 = x4
Conjecture edea9..KK_Kcom__aa1 : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . ∀ x5 : ι → ι → ι . ∀ x6 : ι → ι → ι → ι . ∀ x7 : ι → ι → ι . ∀ x8 x9 : ι → ι → ι → ι . x4x0(∀ x10 . x10x0∀ x11 . x11x0x1 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0x3 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0x2 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0x5 x10 x11 = x2 (x1 x11 x10) (x1 x10 x11))(∀ x10 . x10x0∀ x11 . x11x0x5 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x6 x10 x11 x12 = x2 (x1 x10 (x1 x11 x12)) (x1 (x1 x10 x11) x12))(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x6 x10 x11 x12x0)(∀ x10 . x10x0∀ x11 . x11x0x7 x10 x11 = x2 x11 (x1 x10 x11))(∀ x10 . x10x0∀ x11 . x11x0x7 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x8 x10 x11 x12 = x2 (x1 x12 x11) (x1 x12 (x1 x11 x10)))(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x8 x10 x11 x12x0)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x9 x10 x11 x12 = x3 (x1 (x1 x10 x11) x12) (x1 x11 x12))(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x9 x10 x11 x12x0)(∀ x10 . x10x0x1 x4 x10 = x10)(∀ x10 . x10x0x1 x10 x4 = x10)(∀ x10 . x10x0∀ x11 . x11x0x2 x10 (x1 x10 x11) = x11)(∀ x10 . x10x0∀ x11 . x11x0x1 x10 (x2 x10 x11) = x11)(∀ x10 . x10x0∀ x11 . x11x0x3 (x1 x10 x11) x11 = x10)(∀ x10 . x10x0∀ x11 . x11x0x1 (x3 x10 x11) x11 = x10)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x7 (x7 x10 x11) x12 = x7 (x7 x10 x12) x11)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0x7 (x8 x10 x11 x12) x13 = x8 (x7 x10 x13) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0x7 (x9 x10 x11 x12) x13 = x9 (x7 x10 x13) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0x8 (x9 x10 x11 x12) x13 x14 = x9 (x8 x10 x13 x14) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0x8 (x8 x10 x11 x12) x13 x14 = x8 (x8 x10 x13 x14) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0x9 (x9 x10 x11 x12) x13 x14 = x9 (x9 x10 x13 x14) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x5 (x5 x10 x11) x12 = x4)(∀ x10 . x10x0∀ x11 . x11x0x5 x10 x11 = x5 x11 x10)∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0x6 (x6 x10 x11 x12) x13 x14 = x4
Conjecture 6fb88..T1dist__aa1 : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . ∀ x5 : ι → ι → ι . ∀ x6 : ι → ι → ι → ι . ∀ x7 : ι → ι → ι . ∀ x8 x9 : ι → ι → ι → ι . x4x0(∀ x10 . x10x0∀ x11 . x11x0x1 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0x3 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0x2 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0x5 x10 x11 = x2 (x1 x11 x10) (x1 x10 x11))(∀ x10 . x10x0∀ x11 . x11x0x5 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x6 x10 x11 x12 = x2 (x1 x10 (x1 x11 x12)) (x1 (x1 x10 x11) x12))(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x6 x10 x11 x12x0)(∀ x10 . x10x0∀ x11 . x11x0x7 x10 x11 = x2 x11 (x1 x10 x11))(∀ x10 . x10x0∀ x11 . x11x0x7 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x8 x10 x11 x12 = x2 (x1 x12 x11) (x1 x12 (x1 x11 x10)))(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x8 x10 x11 x12x0)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x9 x10 x11 x12 = x3 (x1 (x1 x10 x11) x12) (x1 x11 x12))(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x9 x10 x11 x12x0)(∀ x10 . x10x0x1 x4 x10 = x10)(∀ x10 . x10x0x1 x10 x4 = x10)(∀ x10 . x10x0∀ x11 . x11x0x2 x10 (x1 x10 x11) = x11)(∀ x10 . x10x0∀ x11 . x11x0x1 x10 (x2 x10 x11) = x11)(∀ x10 . x10x0∀ x11 . x11x0x3 (x1 x10 x11) x11 = x10)(∀ x10 . x10x0∀ x11 . x11x0x1 (x3 x10 x11) x11 = x10)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x7 (x7 x10 x11) x12 = x7 (x7 x10 x12) x11)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0x7 (x8 x10 x11 x12) x13 = x8 (x7 x10 x13) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0x7 (x9 x10 x11 x12) x13 = x9 (x7 x10 x13) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0x8 (x9 x10 x11 x12) x13 x14 = x9 (x8 x10 x13 x14) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0x8 (x8 x10 x11 x12) x13 x14 = x8 (x8 x10 x13 x14) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0x9 (x9 x10 x11 x12) x13 x14 = x9 (x9 x10 x13 x14) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x1 (x7 x10 x11) (x7 x12 x11) = x7 (x1 x10 x12) x11)∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0x6 (x6 x10 x11 x12) x13 x14 = x4
Conjecture 76b60..nil3_24 : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . ∀ x5 : ι → ι → ι . ∀ x6 : ι → ι → ι → ι . ∀ x7 : ι → ι → ι . ∀ x8 x9 : ι → ι → ι → ι . x4x0(∀ x10 . x10x0∀ x11 . x11x0x1 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0x3 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0x2 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0x5 x10 x11 = x2 (x1 x11 x10) (x1 x10 x11))(∀ x10 . x10x0∀ x11 . x11x0x5 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x6 x10 x11 x12 = x2 (x1 x10 (x1 x11 x12)) (x1 (x1 x10 x11) x12))(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x6 x10 x11 x12x0)(∀ x10 . x10x0∀ x11 . x11x0x7 x10 x11 = x2 x11 (x1 x10 x11))(∀ x10 . x10x0∀ x11 . x11x0x7 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x8 x10 x11 x12 = x2 (x1 x12 x11) (x1 x12 (x1 x11 x10)))(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x8 x10 x11 x12x0)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x9 x10 x11 x12 = x3 (x1 (x1 x10 x11) x12) (x1 x11 x12))(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x9 x10 x11 x12x0)(∀ x10 . x10x0x1 x4 x10 = x10)(∀ x10 . x10x0x1 x10 x4 = x10)(∀ x10 . x10x0∀ x11 . x11x0x2 x10 (x1 x10 x11) = x11)(∀ x10 . x10x0∀ x11 . x11x0x1 x10 (x2 x10 x11) = x11)(∀ x10 . x10x0∀ x11 . x11x0x3 (x1 x10 x11) x11 = x10)(∀ x10 . x10x0∀ x11 . x11x0x1 (x3 x10 x11) x11 = x10)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x7 (x7 x10 x11) x12 = x7 (x7 x10 x12) x11)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0x7 (x8 x10 x11 x12) x13 = x8 (x7 x10 x13) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0x7 (x9 x10 x11 x12) x13 = x9 (x7 x10 x13) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0x8 (x9 x10 x11 x12) x13 x14 = x9 (x8 x10 x13 x14) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0x8 (x8 x10 x11 x12) x13 x14 = x8 (x8 x10 x13 x14) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0x9 (x9 x10 x11 x12) x13 x14 = x9 (x9 x10 x13 x14) x11 x12)∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0x6 (x6 (x6 x10 x11 x12) x13 x14) x15 x16 = x4
Conjecture 6793d..com__nil3_24 : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . ∀ x5 : ι → ι → ι . ∀ x6 : ι → ι → ι → ι . ∀ x7 : ι → ι → ι . ∀ x8 x9 : ι → ι → ι → ι . x4x0(∀ x10 . x10x0∀ x11 . x11x0x1 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0x3 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0x2 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0x5 x10 x11 = x2 (x1 x11 x10) (x1 x10 x11))(∀ x10 . x10x0∀ x11 . x11x0x5 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x6 x10 x11 x12 = x2 (x1 x10 (x1 x11 x12)) (x1 (x1 x10 x11) x12))(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x6 x10 x11 x12x0)(∀ x10 . x10x0∀ x11 . x11x0x7 x10 x11 = x2 x11 (x1 x10 x11))(∀ x10 . x10x0∀ x11 . x11x0x7 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x8 x10 x11 x12 = x2 (x1 x12 x11) (x1 x12 (x1 x11 x10)))(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x8 x10 x11 x12x0)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x9 x10 x11 x12 = x3 (x1 (x1 x10 x11) x12) (x1 x11 x12))(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x9 x10 x11 x12x0)(∀ x10 . x10x0x1 x4 x10 = x10)(∀ x10 . x10x0x1 x10 x4 = x10)(∀ x10 . x10x0∀ x11 . x11x0x2 x10 (x1 x10 x11) = x11)(∀ x10 . x10x0∀ x11 . x11x0x1 x10 (x2 x10 x11) = x11)(∀ x10 . x10x0∀ x11 . x11x0x3 (x1 x10 x11) x11 = x10)(∀ x10 . x10x0∀ x11 . x11x0x1 (x3 x10 x11) x11 = x10)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x7 (x7 x10 x11) x12 = x7 (x7 x10 x12) x11)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0x7 (x8 x10 x11 x12) x13 = x8 (x7 x10 x13) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0x7 (x9 x10 x11 x12) x13 = x9 (x7 x10 x13) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0x8 (x9 x10 x11 x12) x13 x14 = x9 (x8 x10 x13 x14) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0x8 (x8 x10 x11 x12) x13 x14 = x8 (x8 x10 x13 x14) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0x9 (x9 x10 x11 x12) x13 x14 = x9 (x9 x10 x13 x14) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0x1 x10 x11 = x1 x11 x10)∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0x6 (x6 (x6 x10 x11 x12) x13 x14) x15 x16 = x4
Conjecture 203c2..aa1_45 : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . ∀ x5 : ι → ι → ι . ∀ x6 : ι → ι → ι → ι . ∀ x7 : ι → ι → ι . ∀ x8 x9 : ι → ι → ι → ι . x4x0(∀ x10 . x10x0∀ x11 . x11x0x1 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0x3 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0x2 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0x5 x10 x11 = x2 (x1 x11 x10) (x1 x10 x11))(∀ x10 . x10x0∀ x11 . x11x0x5 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x6 x10 x11 x12 = x2 (x1 x10 (x1 x11 x12)) (x1 (x1 x10 x11) x12))(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x6 x10 x11 x12x0)(∀ x10 . x10x0∀ x11 . x11x0x7 x10 x11 = x2 x11 (x1 x10 x11))(∀ x10 . x10x0∀ x11 . x11x0x7 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x8 x10 x11 x12 = x2 (x1 x12 x11) (x1 x12 (x1 x11 x10)))(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x8 x10 x11 x12x0)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x9 x10 x11 x12 = x3 (x1 (x1 x10 x11) x12) (x1 x11 x12))(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x9 x10 x11 x12x0)(∀ x10 . x10x0x1 x4 x10 = x10)(∀ x10 . x10x0x1 x10 x4 = x10)(∀ x10 . x10x0∀ x11 . x11x0x2 x10 (x1 x10 x11) = x11)(∀ x10 . x10x0∀ x11 . x11x0x1 x10 (x2 x10 x11) = x11)(∀ x10 . x10x0∀ x11 . x11x0x3 (x1 x10 x11) x11 = x10)(∀ x10 . x10x0∀ x11 . x11x0x1 (x3 x10 x11) x11 = x10)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x7 (x7 x10 x11) x12 = x7 (x7 x10 x12) x11)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0x7 (x8 x10 x11 x12) x13 = x8 (x7 x10 x13) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0x7 (x9 x10 x11 x12) x13 = x9 (x7 x10 x13) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0x8 (x9 x10 x11 x12) x13 x14 = x9 (x8 x10 x13 x14) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0x8 (x8 x10 x11 x12) x13 x14 = x8 (x8 x10 x13 x14) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0x9 (x9 x10 x11 x12) x13 x14 = x9 (x9 x10 x13 x14) x11 x12)∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0x6 (x6 x10 x11 x12) x13 x14 = x6 (x6 x10 x11 x12) x14 x13
Conjecture bd861..nil3_24__aa1 : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . ∀ x5 : ι → ι → ι . ∀ x6 : ι → ι → ι → ι . ∀ x7 : ι → ι → ι . ∀ x8 x9 : ι → ι → ι → ι . x4x0(∀ x10 . x10x0∀ x11 . x11x0x1 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0x3 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0x2 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0x5 x10 x11 = x2 (x1 x11 x10) (x1 x10 x11))(∀ x10 . x10x0∀ x11 . x11x0x5 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x6 x10 x11 x12 = x2 (x1 x10 (x1 x11 x12)) (x1 (x1 x10 x11) x12))(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x6 x10 x11 x12x0)(∀ x10 . x10x0∀ x11 . x11x0x7 x10 x11 = x2 x11 (x1 x10 x11))(∀ x10 . x10x0∀ x11 . x11x0x7 x10 x11x0)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x8 x10 x11 x12 = x2 (x1 x12 x11) (x1 x12 (x1 x11 x10)))(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x8 x10 x11 x12x0)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x9 x10 x11 x12 = x3 (x1 (x1 x10 x11) x12) (x1 x11 x12))(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x9 x10 x11 x12x0)(∀ x10 . x10x0x1 x4 x10 = x10)(∀ x10 . x10x0x1 x10 x4 = x10)(∀ x10 . x10x0∀ x11 . x11x0x2 x10 (x1 x10 x11) = x11)(∀ x10 . x10x0∀ x11 . x11x0x1 x10 (x2 x10 x11) = x11)(∀ x10 . x10x0∀ x11 . x11x0x3 (x1 x10 x11) x11 = x10)(∀ x10 . x10x0∀ x11 . x11x0x1 (x3 x10 x11) x11 = x10)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0x7 (x7 x10 x11) x12 = x7 (x7 x10 x12) x11)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0x7 (x8 x10 x11 x12) x13 = x8 (x7 x10 x13) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0x7 (x9 x10 x11 x12) x13 = x9 (x7 x10 x13) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0x8 (x9 x10 x11 x12) x13 x14 = x9 (x8 x10 x13 x14) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0x8 (x8 x10 x11 x12) x13 x14 = x8 (x8 x10 x13 x14) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0x9 (x9 x10 x11 x12) x13 x14 = x9 (x9 x10 x13 x14) x11 x12)(∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0x6 (x6 (x6 x10 x11 x12) x13 x14) x15 x16 = x4)∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0x6 (x6 x10 x11 x12) x13 x14 = x4

previous assets