Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrQyi../34854..
PUadC../a9c67..
vout
PrQyi../579c5.. 5.81 bars
TMY3r../e46e4.. ownership of f1f7a.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMTAg../0ba1b.. ownership of 63209.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
PURP4../1549d.. doc published by Pr4zB..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Known 0c063.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 : ι → ο . x8 x2x8 x3x8 x4x8 x5x8 x6x8 x7∀ x9 . x0 x9x8 x9)x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2x1 x3x1 x4x1 x5∀ x8 x9 x10 : ι → ι . x8 x2 = x3x8 x3 = x2x8 x4 = x5x8 x5 = x4x9 x2 = x4x9 x3 = x5x9 x4 = x2x9 x5 = x3x10 x2 = x5x10 x3 = x4x10 x4 = x3x10 x5 = x2∀ x11 : ι → ι → ι → ι → ο . (∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x12 x13))(∀ x12 x13 x14 x15 . x11 x12 x13 x14 x15x11 x14 x15 x12 x13)(∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x7 x7))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x8 x13) x14 (x8 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x9 x13) x14 (x9 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x10 x13) x14 (x10 x15)))(∀ x12 . x0 x12not (x11 x4 x6 x5 x12))(∀ x12 . x0 x12not (x11 x4 x7 x5 x12))(∀ x12 . x0 x12not (x11 x5 x6 x6 x12))(∀ x12 . x0 x12not (x11 x6 x7 x2 x12))(∀ x12 . x0 x12not (x11 x2 x3 x12 x6))not (x11 x2 x2 x2 x5)not (x11 x2 x2 x3 x4)not (x11 x2 x2 x3 x5)not (x11 x2 x2 x4 x2)not (x11 x2 x2 x5 x2)not (x11 x2 x2 x5 x5)not (x11 x2 x2 x6 x2)not (x11 x2 x3 x7 x2)not (x11 x2 x4 x2 x6)not (x11 x2 x4 x5 x6)not (x11 x2 x4 x7 x6)not (x11 x2 x5 x5 x2)not (x11 x2 x6 x3 x5)not (x11 x2 x6 x4 x3)not (x11 x2 x6 x4 x4)not (x11 x2 x6 x5 x3)not (x11 x2 x6 x7 x2)not (x11 x2 x6 x7 x3)not (x11 x2 x7 x5 x2)not (x11 x3 x2 x3 x3)not (x11 x3 x2 x3 x5)not (x11 x3 x2 x4 x4)not (x11 x3 x2 x4 x5)not (x11 x3 x2 x5 x2)not (x11 x3 x2 x6 x2)not (x11 x3 x2 x6 x5)not (x11 x3 x2 x7 x2)not (x11 x3 x2 x7 x4)not (x11 x3 x2 x7 x5)not (x11 x3 x3 x5 x6)not (x11 x3 x3 x7 x6)not (x11 x3 x4 x4 x2)not (x11 x3 x4 x5 x6)not (x11 x3 x4 x7 x2)not (x11 x3 x4 x7 x6)not (x11 x3 x5 x4 x2)not (x11 x3 x5 x6 x2)not (x11 x3 x5 x7 x2)not (x11 x3 x6 x5 x2)not (x11 x3 x7 x5 x2)not (x11 x4 x2 x5 x2)not (x11 x4 x2 x6 x2)not (x11 x4 x2 x7 x2)not (x11 x4 x2 x7 x5)not (x11 x4 x3 x7 x2)not (x11 x4 x5 x5 x2)not (x11 x4 x5 x7 x2)not (x11 x5 x2 x5 x4)not (x11 x5 x2 x5 x5)not (x11 x5 x2 x5 x7)not (x11 x5 x2 x6 x2)not (x11 x5 x2 x6 x3)not (x11 x5 x2 x6 x5)not (x11 x5 x2 x6 x6)not (x11 x5 x2 x7 x4)not (x11 x5 x2 x7 x5)not (x11 x5 x6 x7 x6)not (x11 x6 x2 x7 x5)not (x11 x6 x4 x7 x6)not (x11 x6 x5 x7 x2)not (x11 x7 x2 x7 x3)∀ x12 . x0 x12∀ x13 . x0 x13∀ x14 . x0 x14∀ x15 . x0 x15∀ x16 . x0 x16x11 x5 x2 x2 x12x11 x5 x2 x13 x14x11 x5 x2 x15 x16x11 x2 x12 x13 x14x11 x2 x12 x15 x16x11 x13 x14 x15 x16False
Known 0d27e.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 : ι → ο . x8 x2x8 x3x8 x4x8 x5x8 x6x8 x7∀ x9 . x0 x9x8 x9)x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2x1 x3x1 x4x1 x5∀ x8 x9 x10 : ι → ι . x8 x2 = x3x8 x3 = x2x8 x4 = x5x8 x5 = x4x9 x2 = x4x9 x3 = x5x9 x4 = x2x9 x5 = x3x10 x2 = x5x10 x3 = x4x10 x4 = x3x10 x5 = x2∀ x11 : ι → ι → ι → ι → ο . (∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x12 x13))(∀ x12 x13 x14 x15 . x11 x12 x13 x14 x15x11 x14 x15 x12 x13)(∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x7 x7))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x8 x13) x14 (x8 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x9 x13) x14 (x9 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x10 x13) x14 (x10 x15)))(∀ x12 . x0 x12not (x11 x4 x6 x5 x12))(∀ x12 . x0 x12not (x11 x4 x7 x5 x12))(∀ x12 . x0 x12not (x11 x5 x6 x6 x12))(∀ x12 . x0 x12not (x11 x6 x7 x2 x12))(∀ x12 . x0 x12not (x11 x6 x7 x4 x12))(∀ x12 . x0 x12not (x11 x2 x3 x12 x6))not (x11 x2 x2 x3 x4)not (x11 x2 x2 x3 x5)not (x11 x2 x2 x4 x2)not (x11 x2 x2 x5 x2)not (x11 x2 x2 x5 x5)not (x11 x2 x2 x6 x2)not (x11 x2 x3 x7 x2)not (x11 x2 x4 x2 x6)not (x11 x2 x4 x3 x2)not (x11 x2 x4 x5 x6)not (x11 x2 x5 x3 x2)not (x11 x2 x5 x5 x2)not (x11 x2 x6 x3 x5)not (x11 x2 x6 x4 x3)not (x11 x2 x6 x4 x4)not (x11 x2 x6 x5 x3)not (x11 x2 x6 x7 x2)not (x11 x2 x7 x5 x2)not (x11 x3 x2 x3 x3)not (x11 x3 x2 x3 x5)not (x11 x3 x2 x4 x3)not (x11 x3 x2 x4 x4)not (x11 x3 x2 x4 x5)not (x11 x3 x2 x5 x2)not (x11 x3 x2 x6 x2)not (x11 x3 x2 x6 x5)not (x11 x3 x2 x7 x2)not (x11 x3 x2 x7 x4)not (x11 x3 x2 x7 x5)not (x11 x3 x3 x5 x6)not (x11 x3 x3 x6 x7)not (x11 x3 x3 x7 x6)not (x11 x3 x4 x4 x2)not (x11 x3 x4 x5 x6)not (x11 x3 x4 x7 x2)not (x11 x3 x4 x7 x6)not (x11 x3 x5 x6 x2)not (x11 x3 x5 x6 x7)not (x11 x3 x5 x7 x2)not (x11 x3 x5 x7 x6)not (x11 x3 x6 x5 x2)not (x11 x3 x7 x5 x2)not (x11 x4 x2 x5 x2)not (x11 x4 x2 x5 x5)not (x11 x4 x3 x7 x2)not (x11 x4 x5 x5 x2)not (x11 x5 x2 x5 x4)not (x11 x5 x2 x5 x5)not (x11 x5 x2 x5 x7)not (x11 x5 x2 x6 x2)not (x11 x5 x2 x6 x3)not (x11 x5 x2 x6 x5)not (x11 x5 x2 x6 x6)not (x11 x5 x2 x7 x4)not (x11 x5 x2 x7 x5)not (x11 x5 x3 x5 x6)not (x11 x5 x3 x6 x7)not (x11 x5 x5 x6 x2)∀ x12 . x0 x12∀ x13 . x0 x13∀ x14 . x0 x14∀ x15 . x0 x15∀ x16 . x0 x16x11 x5 x2 x3 x12x11 x5 x2 x13 x14x11 x5 x2 x15 x16x11 x3 x12 x13 x14x11 x3 x12 x15 x16x11 x13 x14 x15 x16False
Known 9dabc.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 : ι → ο . x8 x2x8 x3x8 x4x8 x5x8 x6x8 x7∀ x9 . x0 x9x8 x9)x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2x1 x3x1 x4x1 x5∀ x8 x9 x10 : ι → ι . x8 x2 = x3x8 x3 = x2x8 x4 = x5x8 x5 = x4x9 x2 = x4x9 x3 = x5x9 x4 = x2x9 x5 = x3x10 x2 = x5x10 x3 = x4x10 x4 = x3x10 x5 = x2∀ x11 : ι → ι → ι → ι → ο . (∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x12 x13))(∀ x12 x13 x14 x15 . x11 x12 x13 x14 x15x11 x14 x15 x12 x13)(∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x7 x7))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x8 x13) x14 (x8 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x9 x13) x14 (x9 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x10 x13) x14 (x10 x15)))(∀ x12 . x0 x12not (x11 x4 x6 x5 x12))(∀ x12 . x0 x12not (x11 x4 x7 x5 x12))(∀ x12 . x0 x12not (x11 x5 x6 x6 x12))(∀ x12 . x0 x12not (x11 x6 x7 x4 x12))(∀ x12 . x0 x12not (x11 x7 x6 x7 x12))(∀ x12 . x0 x12not (x11 x2 x3 x12 x6))not (x11 x2 x2 x3 x5)not (x11 x2 x2 x4 x2)not (x11 x2 x2 x5 x2)not (x11 x2 x2 x6 x2)not (x11 x2 x3 x7 x2)not (x11 x2 x4 x5 x6)not (x11 x2 x4 x7 x6)not (x11 x2 x5 x3 x2)not (x11 x2 x5 x5 x2)not (x11 x2 x6 x4 x3)not (x11 x2 x6 x4 x4)not (x11 x2 x7 x5 x2)not (x11 x3 x2 x5 x2)not (x11 x3 x2 x6 x5)not (x11 x3 x3 x4 x2)not (x11 x3 x3 x5 x6)not (x11 x3 x3 x7 x6)not (x11 x3 x4 x4 x2)not (x11 x3 x4 x5 x6)not (x11 x3 x4 x7 x2)not (x11 x3 x4 x7 x6)not (x11 x3 x5 x4 x2)not (x11 x3 x5 x6 x2)not (x11 x3 x6 x5 x2)not (x11 x3 x7 x5 x2)not (x11 x4 x2 x4 x5)not (x11 x4 x2 x5 x2)not (x11 x4 x2 x5 x5)not (x11 x4 x2 x6 x2)not (x11 x4 x2 x7 x2)not (x11 x4 x2 x7 x5)not (x11 x4 x3 x7 x2)not (x11 x4 x5 x5 x2)not (x11 x5 x2 x5 x4)not (x11 x5 x2 x5 x5)not (x11 x5 x2 x5 x7)not (x11 x5 x2 x6 x2)not (x11 x5 x2 x6 x3)not (x11 x5 x2 x6 x5)not (x11 x5 x2 x6 x6)not (x11 x5 x2 x7 x4)not (x11 x5 x2 x7 x5)not (x11 x5 x6 x7 x2)not (x11 x5 x6 x7 x6)not (x11 x6 x4 x7 x6)∀ x12 . x0 x12∀ x13 . x0 x13∀ x14 . x0 x14∀ x15 . x0 x15∀ x16 . x0 x16x11 x5 x2 x4 x12x11 x5 x2 x13 x14x11 x5 x2 x15 x16x11 x4 x12 x13 x14x11 x4 x12 x15 x16x11 x13 x14 x15 x16False
Known df7f7.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 : ι → ο . x8 x2x8 x3x8 x4x8 x5x8 x6x8 x7∀ x9 . x0 x9x8 x9)x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2x1 x3x1 x4x1 x5∀ x8 x9 x10 : ι → ι . x8 x2 = x3x8 x3 = x2x8 x4 = x5x8 x5 = x4x9 x2 = x4x9 x3 = x5x9 x4 = x2x9 x5 = x3x10 x2 = x5x10 x3 = x4x10 x4 = x3x10 x5 = x2∀ x11 : ι → ι → ι → ι → ο . (∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x12 x13))(∀ x12 x13 x14 x15 . x11 x12 x13 x14 x15x11 x14 x15 x12 x13)(∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x7 x7))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x8 x13) x14 (x8 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x9 x13) x14 (x9 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x10 x13) x14 (x10 x15)))(∀ x12 . x0 x12not (x11 x4 x6 x5 x12))(∀ x12 . x0 x12not (x11 x4 x7 x5 x12))(∀ x12 . x0 x12not (x11 x5 x6 x6 x12))(∀ x12 . x0 x12not (x11 x7 x6 x7 x12))(∀ x12 . x0 x12not (x11 x2 x3 x12 x6))not (x11 x2 x2 x5 x2)not (x11 x2 x4 x5 x6)not (x11 x2 x5 x5 x2)not (x11 x2 x6 x3 x5)not (x11 x2 x6 x4 x3)not (x11 x2 x6 x4 x4)not (x11 x2 x6 x5 x3)not (x11 x2 x6 x7 x3)not (x11 x2 x7 x5 x2)not (x11 x3 x2 x3 x3)not (x11 x3 x2 x4 x3)not (x11 x3 x2 x4 x4)not (x11 x3 x2 x5 x2)not (x11 x3 x2 x7 x4)not (x11 x3 x2 x7 x5)not (x11 x3 x3 x4 x2)not (x11 x3 x3 x5 x6)not (x11 x3 x4 x4 x2)not (x11 x3 x4 x5 x6)not (x11 x3 x4 x7 x2)not (x11 x3 x4 x7 x6)not (x11 x3 x5 x7 x2)not (x11 x3 x5 x7 x6)not (x11 x3 x6 x5 x2)not (x11 x3 x7 x5 x2)not (x11 x4 x2 x4 x5)not (x11 x4 x2 x5 x2)not (x11 x4 x2 x7 x2)not (x11 x4 x2 x7 x5)not (x11 x4 x5 x5 x2)not (x11 x4 x5 x7 x2)not (x11 x5 x2 x5 x4)not (x11 x5 x2 x5 x5)not (x11 x5 x2 x5 x7)not (x11 x5 x2 x6 x2)not (x11 x5 x2 x6 x3)not (x11 x5 x2 x6 x5)not (x11 x5 x2 x6 x6)not (x11 x5 x2 x7 x4)not (x11 x5 x2 x7 x5)not (x11 x5 x3 x5 x6)not (x11 x5 x3 x6 x7)not (x11 x5 x6 x7 x2)not (x11 x5 x6 x7 x6)not (x11 x7 x2 x7 x3)∀ x12 . x0 x12∀ x13 . x0 x13∀ x14 . x0 x14∀ x15 . x0 x15∀ x16 . x0 x16x11 x5 x2 x5 x12x11 x5 x2 x13 x14x11 x5 x2 x15 x16x11 x5 x12 x13 x14x11 x5 x12 x15 x16x11 x13 x14 x15 x16False
Known dcd72.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 : ι → ο . x8 x2x8 x3x8 x4x8 x5x8 x6x8 x7∀ x9 . x0 x9x8 x9)x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2x1 x3x1 x4x1 x5∀ x8 x9 x10 : ι → ι . x8 x2 = x3x8 x3 = x2x8 x4 = x5x8 x5 = x4x9 x2 = x4x9 x3 = x5x9 x4 = x2x9 x5 = x3x10 x2 = x5x10 x3 = x4x10 x4 = x3x10 x5 = x2∀ x11 : ι → ι → ι → ι → ο . (∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x12 x13))(∀ x12 x13 x14 x15 . x11 x12 x13 x14 x15x11 x14 x15 x12 x13)(∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x7 x7))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x8 x13) x14 (x8 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x9 x13) x14 (x9 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x10 x13) x14 (x10 x15)))(∀ x12 . x0 x12not (x11 x4 x6 x5 x12))(∀ x12 . x0 x12not (x11 x4 x7 x5 x12))(∀ x12 . x0 x12not (x11 x5 x6 x6 x12))(∀ x12 . x0 x12not (x11 x6 x7 x2 x12))(∀ x12 . x0 x12not (x11 x6 x7 x4 x12))(∀ x12 . x0 x12not (x11 x7 x6 x7 x12))(∀ x12 . x0 x12not (x11 x2 x3 x12 x6))not (x11 x2 x2 x3 x4)not (x11 x2 x2 x4 x2)not (x11 x2 x2 x5 x2)not (x11 x2 x2 x6 x2)not (x11 x2 x4 x3 x2)not (x11 x2 x5 x5 x2)not (x11 x2 x6 x3 x5)not (x11 x2 x6 x4 x3)not (x11 x2 x7 x5 x2)not (x11 x3 x2 x4 x4)not (x11 x3 x2 x5 x2)not (x11 x3 x2 x6 x2)not (x11 x3 x2 x7 x5)not (x11 x3 x3 x6 x7)not (x11 x3 x4 x4 x2)not (x11 x3 x4 x7 x2)not (x11 x3 x4 x7 x6)not (x11 x3 x5 x6 x2)not (x11 x3 x5 x6 x7)not (x11 x3 x5 x7 x2)not (x11 x3 x6 x5 x2)not (x11 x3 x7 x5 x2)not (x11 x4 x2 x5 x2)not (x11 x4 x2 x6 x2)not (x11 x4 x5 x5 x2)not (x11 x5 x2 x5 x4)not (x11 x5 x2 x5 x5)not (x11 x5 x2 x5 x7)not (x11 x5 x2 x6 x2)not (x11 x5 x2 x6 x3)not (x11 x5 x2 x6 x5)not (x11 x5 x2 x6 x6)not (x11 x5 x2 x7 x4)not (x11 x5 x2 x7 x5)not (x11 x5 x3 x6 x7)not (x11 x5 x5 x6 x2)not (x11 x6 x2 x7 x5)not (x11 x6 x4 x7 x2)not (x11 x6 x4 x7 x6)not (x11 x6 x5 x7 x2)not (x11 x7 x2 x7 x3)∀ x12 . x0 x12∀ x13 . x0 x13∀ x14 . x0 x14∀ x15 . x0 x15∀ x16 . x0 x16x11 x5 x2 x6 x12x11 x5 x2 x13 x14x11 x5 x2 x15 x16x11 x6 x12 x13 x14x11 x6 x12 x15 x16x11 x13 x14 x15 x16False
Known 4adeb.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 : ι → ο . x8 x2x8 x3x8 x4x8 x5x8 x6x8 x7∀ x9 . x0 x9x8 x9)x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2x1 x3x1 x4x1 x5∀ x8 x9 x10 : ι → ι . x8 x2 = x3x8 x3 = x2x8 x4 = x5x8 x5 = x4x9 x2 = x4x9 x3 = x5x9 x4 = x2x9 x5 = x3x10 x2 = x5x10 x3 = x4x10 x4 = x3x10 x5 = x2∀ x11 : ι → ι → ι → ι → ο . (∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x12 x13))(∀ x12 x13 x14 x15 . x11 x12 x13 x14 x15x11 x14 x15 x12 x13)(∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x7 x7))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x8 x13) x14 (x8 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x9 x13) x14 (x9 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x10 x13) x14 (x10 x15)))(∀ x12 . x0 x12not (x11 x4 x6 x5 x12))(∀ x12 . x0 x12not (x11 x4 x7 x5 x12))(∀ x12 . x0 x12not (x11 x5 x6 x6 x12))(∀ x12 . x0 x12not (x11 x6 x7 x2 x12))(∀ x12 . x0 x12not (x11 x6 x7 x4 x12))(∀ x12 . x0 x12not (x11 x7 x6 x7 x12))(∀ x12 . x0 x12not (x11 x2 x3 x12 x6))not (x11 x2 x2 x2 x5)not (x11 x2 x2 x3 x5)not (x11 x2 x2 x4 x2)not (x11 x2 x2 x5 x2)not (x11 x2 x2 x5 x5)not (x11 x2 x3 x7 x2)not (x11 x2 x4 x5 x6)not (x11 x2 x4 x7 x6)not (x11 x2 x5 x3 x2)not (x11 x2 x5 x5 x2)not (x11 x2 x6 x4 x3)not (x11 x2 x6 x4 x4)not (x11 x2 x6 x5 x3)not (x11 x2 x6 x7 x2)not (x11 x2 x6 x7 x3)not (x11 x2 x7 x5 x2)not (x11 x3 x2 x4 x5)not (x11 x3 x2 x5 x2)not (x11 x3 x2 x7 x2)not (x11 x3 x3 x6 x7)not (x11 x3 x3 x7 x6)not (x11 x3 x4 x7 x2)not (x11 x3 x4 x7 x6)not (x11 x3 x5 x4 x2)not (x11 x3 x5 x7 x2)not (x11 x3 x5 x7 x6)not (x11 x3 x6 x5 x2)not (x11 x3 x7 x5 x2)not (x11 x4 x2 x4 x5)not (x11 x4 x2 x5 x2)not (x11 x4 x2 x5 x5)not (x11 x4 x2 x7 x2)not (x11 x4 x3 x7 x2)not (x11 x4 x5 x5 x2)not (x11 x4 x5 x7 x2)not (x11 x5 x2 x5 x4)not (x11 x5 x2 x5 x5)not (x11 x5 x2 x5 x7)not (x11 x5 x2 x6 x2)not (x11 x5 x2 x6 x3)not (x11 x5 x2 x6 x5)not (x11 x5 x2 x6 x6)not (x11 x5 x2 x7 x4)not (x11 x5 x2 x7 x5)not (x11 x5 x3 x5 x6)not (x11 x5 x3 x6 x7)not (x11 x5 x6 x7 x2)not (x11 x5 x6 x7 x6)not (x11 x6 x4 x7 x2)not (x11 x6 x4 x7 x6)not (x11 x6 x5 x7 x2)not (x11 x7 x2 x7 x3)∀ x12 . x0 x12∀ x13 . x0 x13∀ x14 . x0 x14∀ x15 . x0 x15∀ x16 . x0 x16x11 x5 x2 x7 x12x11 x5 x2 x13 x14x11 x5 x2 x15 x16x11 x7 x12 x13 x14x11 x7 x12 x15 x16x11 x13 x14 x15 x16False
Known a8686.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 : ι → ο . x8 x2x8 x3x8 x4x8 x5x8 x6x8 x7∀ x9 . x0 x9x8 x9)x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2x1 x3x1 x4x1 x5∀ x8 x9 x10 : ι → ι . x8 x2 = x3x8 x3 = x2x8 x4 = x5x8 x5 = x4x9 x2 = x4x9 x3 = x5x9 x4 = x2x9 x5 = x3x10 x2 = x5x10 x3 = x4x10 x4 = x3x10 x5 = x2∀ x11 : ι → ι → ι → ι → ο . (∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x12 x13))(∀ x12 x13 x14 x15 . x11 x12 x13 x14 x15x11 x14 x15 x12 x13)(∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x7 x7))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x8 x13) x14 (x8 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x9 x13) x14 (x9 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x10 x13) x14 (x10 x15)))(∀ x12 . x0 x12not (x11 x4 x6 x5 x12))(∀ x12 . x0 x12not (x11 x4 x7 x5 x12))(∀ x12 . x0 x12not (x11 x5 x7 x6 x12))(∀ x12 . x0 x12not (x11 x6 x6 x2 x12))(∀ x12 . x0 x12not (x11 x2 x2 x12 x7))not (x11 x2 x2 x2 x5)not (x11 x2 x2 x3 x4)not (x11 x2 x2 x3 x5)not (x11 x2 x2 x4 x2)not (x11 x2 x2 x5 x2)not (x11 x2 x2 x6 x2)not (x11 x2 x2 x7 x3)not (x11 x2 x2 x7 x6)not (x11 x2 x5 x2 x7)not (x11 x2 x5 x3 x2)not (x11 x2 x5 x5 x2)not (x11 x2 x5 x5 x7)not (x11 x2 x5 x7 x6)not (x11 x2 x6 x5 x3)not (x11 x2 x7 x3 x4)not (x11 x2 x7 x4 x2)not (x11 x2 x7 x4 x5)not (x11 x2 x7 x5 x2)not (x11 x2 x7 x7 x2)not (x11 x2 x7 x7 x3)not (x11 x3 x2 x3 x3)not (x11 x3 x2 x3 x5)not (x11 x3 x2 x4 x5)not (x11 x3 x2 x5 x2)not (x11 x3 x2 x5 x7)not (x11 x3 x2 x6 x2)not (x11 x3 x2 x6 x5)not (x11 x3 x2 x7 x2)not (x11 x3 x2 x7 x4)not (x11 x3 x2 x7 x5)not (x11 x3 x2 x7 x6)not (x11 x3 x4 x4 x2)not (x11 x3 x4 x7 x2)not (x11 x3 x5 x4 x2)not (x11 x3 x5 x5 x7)not (x11 x3 x5 x7 x2)not (x11 x3 x5 x7 x6)not (x11 x3 x6 x5 x3)not (x11 x3 x7 x5 x3)not (x11 x4 x2 x5 x2)not (x11 x4 x2 x6 x2)not (x11 x4 x2 x7 x2)not (x11 x4 x2 x7 x3)not (x11 x4 x5 x5 x2)not (x11 x4 x5 x7 x2)not (x11 x5 x2 x5 x4)not (x11 x5 x2 x5 x5)not (x11 x5 x2 x6 x2)not (x11 x5 x2 x6 x5)not (x11 x5 x2 x7 x4)not (x11 x5 x2 x7 x5)not (x11 x5 x3 x5 x6)not (x11 x5 x3 x6 x2)not (x11 x5 x3 x6 x7)not (x11 x5 x7 x7 x6)not (x11 x6 x5 x7 x2)not (x11 x6 x5 x7 x6)not (x11 x7 x2 x7 x3)∀ x12 . x0 x12∀ x13 . x0 x13∀ x14 . x0 x14∀ x15 . x0 x15∀ x16 . x0 x16x11 x5 x3 x2 x12x11 x5 x3 x13 x14x11 x5 x3 x15 x16x11 x2 x12 x13 x14x11 x2 x12 x15 x16x11 x13 x14 x15 x16False
Known cdbef.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 : ι → ο . x8 x2x8 x3x8 x4x8 x5x8 x6x8 x7∀ x9 . x0 x9x8 x9)x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2x1 x3x1 x4x1 x5∀ x8 x9 x10 : ι → ι . x8 x2 = x3x8 x3 = x2x8 x4 = x5x8 x5 = x4x9 x2 = x4x9 x3 = x5x9 x4 = x2x9 x5 = x3x10 x2 = x5x10 x3 = x4x10 x4 = x3x10 x5 = x2∀ x11 : ι → ι → ι → ι → ο . (∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x12 x13))(∀ x12 x13 x14 x15 . x11 x12 x13 x14 x15x11 x14 x15 x12 x13)(∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x7 x7))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x8 x13) x14 (x8 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x9 x13) x14 (x9 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x10 x13) x14 (x10 x15)))(∀ x12 . x0 x12not (x11 x4 x6 x5 x12))(∀ x12 . x0 x12not (x11 x4 x7 x5 x12))(∀ x12 . x0 x12not (x11 x5 x7 x6 x12))(∀ x12 . x0 x12not (x11 x6 x6 x2 x12))(∀ x12 . x0 x12not (x11 x6 x6 x4 x12))(∀ x12 . x0 x12not (x11 x2 x2 x12 x7))not (x11 x2 x2 x3 x4)not (x11 x2 x2 x3 x5)not (x11 x2 x2 x4 x2)not (x11 x2 x2 x5 x2)not (x11 x2 x2 x6 x2)not (x11 x2 x2 x7 x3)not (x11 x2 x5 x2 x7)not (x11 x2 x5 x3 x2)not (x11 x2 x5 x5 x2)not (x11 x2 x5 x5 x7)not (x11 x2 x6 x5 x3)not (x11 x2 x7 x3 x4)not (x11 x2 x7 x4 x2)not (x11 x2 x7 x4 x5)not (x11 x2 x7 x5 x2)not (x11 x2 x7 x7 x3)not (x11 x3 x2 x3 x3)not (x11 x3 x2 x3 x5)not (x11 x3 x2 x4 x3)not (x11 x3 x2 x4 x5)not (x11 x3 x2 x5 x2)not (x11 x3 x2 x5 x7)not (x11 x3 x2 x6 x2)not (x11 x3 x2 x6 x5)not (x11 x3 x2 x6 x6)not (x11 x3 x2 x7 x2)not (x11 x3 x2 x7 x4)not (x11 x3 x2 x7 x5)not (x11 x3 x2 x7 x6)not (x11 x3 x4 x4 x2)not (x11 x3 x4 x6 x6)not (x11 x3 x4 x7 x2)not (x11 x3 x4 x7 x6)not (x11 x3 x5 x4 x2)not (x11 x3 x5 x5 x7)not (x11 x3 x5 x7 x2)not (x11 x3 x5 x7 x6)not (x11 x3 x6 x5 x3)not (x11 x3 x7 x5 x3)not (x11 x4 x2 x5 x2)not (x11 x4 x2 x7 x3)not (x11 x4 x5 x5 x2)not (x11 x5 x2 x5 x4)not (x11 x5 x2 x5 x5)not (x11 x5 x2 x5 x7)not (x11 x5 x2 x6 x2)not (x11 x5 x2 x6 x5)not (x11 x5 x2 x6 x6)not (x11 x5 x2 x7 x4)not (x11 x5 x2 x7 x5)not (x11 x5 x3 x5 x6)not (x11 x5 x3 x6 x2)not (x11 x5 x3 x6 x7)∀ x12 . x0 x12∀ x13 . x0 x13∀ x14 . x0 x14∀ x15 . x0 x15∀ x16 . x0 x16x11 x5 x3 x3 x12x11 x5 x3 x13 x14x11 x5 x3 x15 x16x11 x3 x12 x13 x14x11 x3 x12 x15 x16x11 x13 x14 x15 x16False
Known f59d4.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 : ι → ο . x8 x2x8 x3x8 x4x8 x5x8 x6x8 x7∀ x9 . x0 x9x8 x9)x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2x1 x3x1 x4x1 x5∀ x8 x9 x10 : ι → ι . x8 x2 = x3x8 x3 = x2x8 x4 = x5x8 x5 = x4x9 x2 = x4x9 x3 = x5x9 x4 = x2x9 x5 = x3x10 x2 = x5x10 x3 = x4x10 x4 = x3x10 x5 = x2∀ x11 : ι → ι → ι → ι → ο . (∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x12 x13))(∀ x12 x13 x14 x15 . x11 x12 x13 x14 x15x11 x14 x15 x12 x13)(∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x7 x7))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x8 x13) x14 (x8 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x9 x13) x14 (x9 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x10 x13) x14 (x10 x15)))(∀ x12 . x0 x12not (x11 x4 x6 x5 x12))(∀ x12 . x0 x12not (x11 x4 x7 x5 x12))(∀ x12 . x0 x12not (x11 x5 x7 x6 x12))(∀ x12 . x0 x12not (x11 x6 x6 x4 x12))(∀ x12 . x0 x12not (x11 x7 x6 x7 x12))(∀ x12 . x0 x12not (x11 x2 x2 x12 x7))not (x11 x2 x2 x3 x5)not (x11 x2 x2 x4 x2)not (x11 x2 x2 x5 x2)not (x11 x2 x2 x6 x2)not (x11 x2 x2 x7 x3)not (x11 x2 x2 x7 x6)not (x11 x2 x5 x3 x2)not (x11 x2 x5 x5 x2)not (x11 x2 x5 x5 x7)not (x11 x2 x5 x7 x6)not (x11 x2 x6 x5 x3)not (x11 x2 x7 x4 x2)not (x11 x2 x7 x4 x5)not (x11 x3 x2 x4 x5)not (x11 x3 x2 x5 x2)not (x11 x3 x2 x5 x7)not (x11 x3 x2 x6 x5)not (x11 x3 x2 x7 x4)not (x11 x3 x2 x7 x6)not (x11 x3 x3 x4 x2)not (x11 x3 x4 x4 x2)not (x11 x3 x4 x7 x2)not (x11 x3 x5 x4 x2)not (x11 x3 x5 x5 x7)not (x11 x3 x5 x7 x6)not (x11 x3 x6 x5 x3)not (x11 x3 x7 x5 x3)not (x11 x4 x2 x4 x5)not (x11 x4 x2 x5 x2)not (x11 x4 x2 x6 x2)not (x11 x4 x2 x7 x2)not (x11 x4 x2 x7 x3)not (x11 x4 x5 x5 x2)not (x11 x4 x5 x7 x2)not (x11 x5 x2 x5 x4)not (x11 x5 x2 x5 x5)not (x11 x5 x2 x6 x2)not (x11 x5 x2 x6 x5)not (x11 x5 x2 x7 x4)not (x11 x5 x2 x7 x5)not (x11 x5 x3 x5 x6)not (x11 x5 x3 x6 x2)not (x11 x5 x3 x6 x7)not (x11 x5 x7 x7 x3)not (x11 x5 x7 x7 x6)not (x11 x6 x5 x7 x6)∀ x12 . x0 x12∀ x13 . x0 x13∀ x14 . x0 x14∀ x15 . x0 x15∀ x16 . x0 x16x11 x5 x3 x4 x12x11 x5 x3 x13 x14x11 x5 x3 x15 x16x11 x4 x12 x13 x14x11 x4 x12 x15 x16x11 x13 x14 x15 x16False
Known 6d753.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 : ι → ο . x8 x2x8 x3x8 x4x8 x5x8 x6x8 x7∀ x9 . x0 x9x8 x9)x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2x1 x3x1 x4x1 x5∀ x8 x9 x10 : ι → ι . x8 x2 = x3x8 x3 = x2x8 x4 = x5x8 x5 = x4x9 x2 = x4x9 x3 = x5x9 x4 = x2x9 x5 = x3x10 x2 = x5x10 x3 = x4x10 x4 = x3x10 x5 = x2∀ x11 : ι → ι → ι → ι → ο . (∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x12 x13))(∀ x12 x13 x14 x15 . x11 x12 x13 x14 x15x11 x14 x15 x12 x13)(∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x7 x7))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x8 x13) x14 (x8 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x9 x13) x14 (x9 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x10 x13) x14 (x10 x15)))(∀ x12 . x0 x12not (x11 x4 x6 x5 x12))(∀ x12 . x0 x12not (x11 x4 x7 x5 x12))(∀ x12 . x0 x12not (x11 x5 x7 x6 x12))(∀ x12 . x0 x12not (x11 x7 x6 x7 x12))(∀ x12 . x0 x12not (x11 x2 x2 x12 x7))not (x11 x2 x2 x5 x2)not (x11 x2 x5 x5 x2)not (x11 x2 x5 x5 x7)not (x11 x2 x6 x5 x3)not (x11 x2 x7 x3 x4)not (x11 x2 x7 x4 x2)not (x11 x2 x7 x4 x5)not (x11 x2 x7 x5 x2)not (x11 x2 x7 x7 x2)not (x11 x3 x2 x3 x3)not (x11 x3 x2 x4 x3)not (x11 x3 x2 x5 x2)not (x11 x3 x2 x5 x7)not (x11 x3 x2 x7 x4)not (x11 x3 x2 x7 x5)not (x11 x3 x3 x4 x2)not (x11 x3 x4 x4 x2)not (x11 x3 x4 x7 x2)not (x11 x3 x4 x7 x6)not (x11 x3 x5 x5 x7)not (x11 x3 x5 x7 x2)not (x11 x3 x5 x7 x6)not (x11 x3 x6 x5 x3)not (x11 x3 x7 x5 x3)not (x11 x4 x2 x4 x5)not (x11 x4 x2 x5 x2)not (x11 x4 x2 x7 x2)not (x11 x4 x5 x5 x2)not (x11 x4 x5 x7 x2)not (x11 x5 x2 x5 x4)not (x11 x5 x2 x5 x5)not (x11 x5 x2 x5 x7)not (x11 x5 x2 x6 x2)not (x11 x5 x2 x6 x5)not (x11 x5 x2 x6 x6)not (x11 x5 x2 x7 x4)not (x11 x5 x2 x7 x5)not (x11 x5 x3 x5 x6)not (x11 x5 x3 x6 x2)not (x11 x5 x3 x6 x7)not (x11 x5 x7 x7 x3)not (x11 x5 x7 x7 x6)not (x11 x7 x2 x7 x3)∀ x12 . x0 x12∀ x13 . x0 x13∀ x14 . x0 x14∀ x15 . x0 x15∀ x16 . x0 x16x11 x5 x3 x5 x12x11 x5 x3 x13 x14x11 x5 x3 x15 x16x11 x5 x12 x13 x14x11 x5 x12 x15 x16x11 x13 x14 x15 x16False
Known 1cd99.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 : ι → ο . x8 x2x8 x3x8 x4x8 x5x8 x6x8 x7∀ x9 . x0 x9x8 x9)x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2x1 x3x1 x4x1 x5∀ x8 x9 x10 : ι → ι . x8 x2 = x3x8 x3 = x2x8 x4 = x5x8 x5 = x4x9 x2 = x4x9 x3 = x5x9 x4 = x2x9 x5 = x3x10 x2 = x5x10 x3 = x4x10 x4 = x3x10 x5 = x2∀ x11 : ι → ι → ι → ι → ο . (∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x12 x13))(∀ x12 x13 x14 x15 . x11 x12 x13 x14 x15x11 x14 x15 x12 x13)(∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x7 x7))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x8 x13) x14 (x8 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x9 x13) x14 (x9 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x10 x13) x14 (x10 x15)))(∀ x12 . x0 x12not (x11 x4 x6 x5 x12))(∀ x12 . x0 x12not (x11 x4 x7 x5 x12))(∀ x12 . x0 x12not (x11 x5 x7 x6 x12))(∀ x12 . x0 x12not (x11 x6 x6 x2 x12))(∀ x12 . x0 x12not (x11 x6 x6 x4 x12))(∀ x12 . x0 x12not (x11 x7 x6 x7 x12))(∀ x12 . x0 x12not (x11 x2 x2 x12 x7))not (x11 x2 x2 x3 x4)not (x11 x2 x2 x4 x2)not (x11 x2 x2 x5 x2)not (x11 x2 x2 x6 x2)not (x11 x2 x5 x5 x2)not (x11 x2 x6 x5 x3)not (x11 x2 x7 x3 x4)not (x11 x2 x7 x4 x2)not (x11 x3 x2 x5 x2)not (x11 x3 x2 x6 x2)not (x11 x3 x2 x6 x5)not (x11 x3 x2 x6 x6)not (x11 x3 x2 x7 x4)not (x11 x3 x4 x4 x2)not (x11 x3 x4 x6 x6)not (x11 x3 x4 x7 x2)not (x11 x3 x5 x7 x2)not (x11 x3 x5 x7 x6)not (x11 x3 x6 x5 x3)not (x11 x3 x7 x5 x3)not (x11 x4 x2 x5 x2)not (x11 x4 x2 x6 x2)not (x11 x4 x5 x5 x2)not (x11 x5 x2 x5 x4)not (x11 x5 x2 x5 x5)not (x11 x5 x2 x6 x2)not (x11 x5 x2 x6 x5)not (x11 x5 x2 x6 x6)not (x11 x5 x2 x7 x4)not (x11 x5 x2 x7 x5)not (x11 x5 x3 x5 x6)not (x11 x5 x3 x6 x2)not (x11 x5 x3 x6 x7)not (x11 x6 x2 x7 x4)not (x11 x6 x4 x7 x2)not (x11 x6 x5 x7 x2)not (x11 x6 x5 x7 x6)not (x11 x7 x2 x7 x3)∀ x12 . x0 x12∀ x13 . x0 x13∀ x14 . x0 x14∀ x15 . x0 x15∀ x16 . x0 x16x11 x5 x3 x6 x12x11 x5 x3 x13 x14x11 x5 x3 x15 x16x11 x6 x12 x13 x14x11 x6 x12 x15 x16x11 x13 x14 x15 x16False
Known 3eb6f.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 : ι → ο . x8 x2x8 x3x8 x4x8 x5x8 x6x8 x7∀ x9 . x0 x9x8 x9)x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2x1 x3x1 x4x1 x5∀ x8 x9 x10 : ι → ι . x8 x2 = x3x8 x3 = x2x8 x4 = x5x8 x5 = x4x9 x2 = x4x9 x3 = x5x9 x4 = x2x9 x5 = x3x10 x2 = x5x10 x3 = x4x10 x4 = x3x10 x5 = x2∀ x11 : ι → ι → ι → ι → ο . (∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x12 x13))(∀ x12 x13 x14 x15 . x11 x12 x13 x14 x15x11 x14 x15 x12 x13)(∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x7 x7))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x8 x13) x14 (x8 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x9 x13) x14 (x9 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x10 x13) x14 (x10 x15)))(∀ x12 . x0 x12not (x11 x4 x6 x5 x12))(∀ x12 . x0 x12not (x11 x4 x7 x5 x12))(∀ x12 . x0 x12not (x11 x5 x7 x6 x12))(∀ x12 . x0 x12not (x11 x6 x6 x2 x12))(∀ x12 . x0 x12not (x11 x6 x6 x4 x12))(∀ x12 . x0 x12not (x11 x7 x6 x7 x12))(∀ x12 . x0 x12not (x11 x2 x2 x12 x7))not (x11 x2 x2 x2 x5)not (x11 x2 x2 x4 x2)not (x11 x2 x2 x5 x2)not (x11 x2 x2 x7 x3)not (x11 x2 x2 x7 x6)not (x11 x2 x5 x3 x2)not (x11 x2 x5 x5 x2)not (x11 x2 x5 x5 x7)not (x11 x2 x5 x7 x6)not (x11 x2 x6 x5 x3)not (x11 x2 x7 x4 x2)not (x11 x2 x7 x4 x5)not (x11 x2 x7 x5 x2)not (x11 x2 x7 x7 x2)not (x11 x2 x7 x7 x3)not (x11 x3 x2 x4 x5)not (x11 x3 x2 x5 x2)not (x11 x3 x2 x6 x6)not (x11 x3 x2 x7 x2)not (x11 x3 x2 x7 x6)not (x11 x3 x4 x7 x2)not (x11 x3 x4 x7 x6)not (x11 x3 x5 x7 x2)not (x11 x3 x5 x7 x6)not (x11 x3 x6 x5 x3)not (x11 x3 x7 x5 x3)not (x11 x4 x2 x4 x5)not (x11 x4 x2 x5 x2)not (x11 x4 x2 x7 x2)not (x11 x4 x2 x7 x3)not (x11 x4 x5 x5 x2)not (x11 x4 x5 x7 x2)not (x11 x5 x2 x5 x4)not (x11 x5 x2 x5 x5)not (x11 x5 x2 x5 x7)not (x11 x5 x2 x6 x2)not (x11 x5 x2 x6 x5)not (x11 x5 x2 x6 x6)not (x11 x5 x2 x7 x4)not (x11 x5 x2 x7 x5)not (x11 x5 x3 x5 x6)not (x11 x5 x3 x6 x2)not (x11 x5 x3 x6 x7)not (x11 x5 x7 x7 x3)not (x11 x5 x7 x7 x6)not (x11 x6 x4 x7 x2)not (x11 x6 x5 x7 x2)not (x11 x6 x5 x7 x6)not (x11 x7 x2 x7 x3)∀ x12 . x0 x12∀ x13 . x0 x13∀ x14 . x0 x14∀ x15 . x0 x15∀ x16 . x0 x16x11 x5 x3 x7 x12x11 x5 x3 x13 x14x11 x5 x3 x15 x16x11 x7 x12 x13 x14x11 x7 x12 x15 x16x11 x13 x14 x15 x16False
Known 842b1.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 : ι → ο . x8 x2x8 x3x8 x4x8 x5x8 x6x8 x7∀ x9 . x0 x9x8 x9)x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2x1 x3x1 x4x1 x5∀ x8 x9 x10 : ι → ι . x8 x2 = x3x8 x3 = x2x8 x4 = x5x8 x5 = x4x9 x2 = x4x9 x3 = x5x9 x4 = x2x9 x5 = x3x10 x2 = x5x10 x3 = x4x10 x4 = x3x10 x5 = x2∀ x11 : ι → ι → ι → ι → ο . (∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x12 x13))(∀ x12 x13 x14 x15 . x11 x12 x13 x14 x15x11 x14 x15 x12 x13)(∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x7 x7))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x8 x13) x14 (x8 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x9 x13) x14 (x9 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x10 x13) x14 (x10 x15)))(∀ x12 . x0 x12not (x11 x4 x6 x5 x12))(∀ x12 . x0 x12not (x11 x4 x7 x5 x12))(∀ x12 . x0 x12not (x11 x5 x7 x6 x12))(∀ x12 . x0 x12not (x11 x6 x7 x2 x12))(∀ x12 . x0 x12not (x11 x2 x2 x12 x7))(∀ x12 . x0 x12not (x11 x5 x5 x12 x7))(∀ x12 . x0 x12not (x11 x6 x2 x12 x6))not (x11 x2 x2 x2 x5)not (x11 x2 x2 x3 x4)not (x11 x2 x2 x3 x5)not (x11 x2 x2 x4 x2)not (x11 x2 x2 x5 x2)not (x11 x2 x2 x5 x5)not (x11 x2 x2 x6 x2)not (x11 x2 x2 x7 x3)not (x11 x2 x2 x7 x6)not (x11 x2 x5 x2 x7)not (x11 x2 x5 x3 x2)not (x11 x2 x5 x5 x2)not (x11 x2 x5 x5 x7)not (x11 x2 x5 x7 x6)not (x11 x2 x6 x5 x4)not (x11 x2 x7 x3 x3)not (x11 x2 x7 x4 x2)not (x11 x2 x7 x4 x5)not (x11 x2 x7 x7 x4)not (x11 x2 x7 x7 x5)not (x11 x3 x2 x3 x3)not (x11 x3 x2 x3 x5)not (x11 x3 x2 x4 x4)not (x11 x3 x2 x4 x5)not (x11 x3 x2 x5 x2)not (x11 x3 x2 x5 x7)not (x11 x3 x2 x6 x2)not (x11 x3 x2 x7 x2)not (x11 x3 x2 x7 x4)not (x11 x3 x2 x7 x5)not (x11 x3 x2 x7 x6)not (x11 x3 x4 x4 x2)not (x11 x3 x4 x7 x2)not (x11 x3 x5 x4 x2)not (x11 x3 x5 x5 x7)not (x11 x3 x5 x6 x2)not (x11 x3 x5 x7 x2)not (x11 x3 x5 x7 x6)not (x11 x3 x6 x5 x4)not (x11 x3 x7 x5 x4)not (x11 x4 x2 x5 x2)not (x11 x4 x2 x6 x2)not (x11 x4 x2 x7 x2)not (x11 x4 x2 x7 x3)not (x11 x4 x2 x7 x5)not (x11 x4 x3 x7 x2)not (x11 x4 x5 x5 x2)not (x11 x5 x2 x5 x4)not (x11 x5 x2 x5 x5)not (x11 x5 x2 x6 x2)not (x11 x5 x2 x6 x3)not (x11 x5 x2 x6 x5)not (x11 x5 x2 x7 x5)not (x11 x5 x4 x5 x6)not (x11 x5 x4 x6 x6)not (x11 x5 x4 x7 x2)not (x11 x5 x7 x7 x6)not (x11 x6 x2 x7 x5)not (x11 x7 x2 x7 x3)∀ x12 . x0 x12∀ x13 . x0 x13∀ x14 . x0 x14∀ x15 . x0 x15∀ x16 . x0 x16x11 x5 x4 x2 x12x11 x5 x4 x13 x14x11 x5 x4 x15 x16x11 x2 x12 x13 x14x11 x2 x12 x15 x16x11 x13 x14 x15 x16False
Known 0da89.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 : ι → ο . x8 x2x8 x3x8 x4x8 x5x8 x6x8 x7∀ x9 . x0 x9x8 x9)x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2x1 x3x1 x4x1 x5∀ x8 x9 x10 : ι → ι . x8 x2 = x3x8 x3 = x2x8 x4 = x5x8 x5 = x4x9 x2 = x4x9 x3 = x5x9 x4 = x2x9 x5 = x3x10 x2 = x5x10 x3 = x4x10 x4 = x3x10 x5 = x2∀ x11 : ι → ι → ι → ι → ο . (∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x12 x13))(∀ x12 x13 x14 x15 . x11 x12 x13 x14 x15x11 x14 x15 x12 x13)(∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x7 x7))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x8 x13) x14 (x8 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x9 x13) x14 (x9 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x10 x13) x14 (x10 x15)))(∀ x12 . x0 x12not (x11 x4 x6 x5 x12))(∀ x12 . x0 x12not (x11 x4 x7 x5 x12))(∀ x12 . x0 x12not (x11 x5 x7 x6 x12))(∀ x12 . x0 x12not (x11 x6 x7 x2 x12))(∀ x12 . x0 x12not (x11 x6 x7 x4 x12))(∀ x12 . x0 x12not (x11 x2 x2 x12 x7))(∀ x12 . x0 x12not (x11 x5 x5 x12 x7))not (x11 x2 x2 x3 x4)not (x11 x2 x2 x3 x5)not (x11 x2 x2 x4 x2)not (x11 x2 x2 x5 x2)not (x11 x2 x2 x5 x5)not (x11 x2 x2 x6 x2)not (x11 x2 x2 x7 x3)not (x11 x2 x3 x7 x2)not (x11 x2 x4 x3 x2)not (x11 x2 x5 x2 x7)not (x11 x2 x5 x3 x2)not (x11 x2 x5 x5 x2)not (x11 x2 x6 x5 x4)not (x11 x2 x7 x3 x3)not (x11 x2 x7 x4 x2)not (x11 x2 x7 x4 x5)not (x11 x2 x7 x7 x4)not (x11 x3 x2 x3 x3)not (x11 x3 x2 x3 x5)not (x11 x3 x2 x4 x4)not (x11 x3 x2 x4 x5)not (x11 x3 x2 x5 x2)not (x11 x3 x2 x5 x7)not (x11 x3 x2 x6 x2)not (x11 x3 x2 x7 x2)not (x11 x3 x2 x7 x4)not (x11 x3 x2 x7 x5)not (x11 x3 x2 x7 x6)not (x11 x3 x3 x4 x2)not (x11 x3 x3 x6 x7)not (x11 x3 x3 x7 x6)not (x11 x3 x4 x4 x2)not (x11 x3 x5 x4 x2)not (x11 x3 x5 x5 x7)not (x11 x3 x5 x6 x2)not (x11 x3 x5 x6 x7)not (x11 x3 x5 x7 x2)not (x11 x3 x5 x7 x6)not (x11 x3 x6 x5 x4)not (x11 x3 x7 x5 x4)not (x11 x4 x2 x5 x2)not (x11 x4 x2 x5 x5)not (x11 x4 x2 x7 x3)not (x11 x4 x3 x7 x2)not (x11 x4 x5 x5 x2)not (x11 x5 x2 x5 x4)not (x11 x5 x2 x5 x5)not (x11 x5 x2 x6 x2)not (x11 x5 x2 x6 x3)not (x11 x5 x2 x6 x5)not (x11 x5 x2 x7 x5)not (x11 x5 x4 x5 x6)not (x11 x5 x4 x6 x6)not (x11 x5 x4 x7 x2)not (x11 x5 x5 x6 x2)∀ x12 . x0 x12∀ x13 . x0 x13∀ x14 . x0 x14∀ x15 . x0 x15∀ x16 . x0 x16x11 x5 x4 x3 x12x11 x5 x4 x13 x14x11 x5 x4 x15 x16x11 x3 x12 x13 x14x11 x3 x12 x15 x16x11 x13 x14 x15 x16False
Known d66b4.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 : ι → ο . x8 x2x8 x3x8 x4x8 x5x8 x6x8 x7∀ x9 . x0 x9x8 x9)x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2x1 x3x1 x4x1 x5∀ x8 x9 x10 : ι → ι . x8 x2 = x3x8 x3 = x2x8 x4 = x5x8 x5 = x4x9 x2 = x4x9 x3 = x5x9 x4 = x2x9 x5 = x3x10 x2 = x5x10 x3 = x4x10 x4 = x3x10 x5 = x2∀ x11 : ι → ι → ι → ι → ο . (∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x12 x13))(∀ x12 x13 x14 x15 . x11 x12 x13 x14 x15x11 x14 x15 x12 x13)(∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x7 x7))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x8 x13) x14 (x8 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x9 x13) x14 (x9 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x10 x13) x14 (x10 x15)))(∀ x12 . x0 x12not (x11 x4 x6 x5 x12))(∀ x12 . x0 x12not (x11 x4 x7 x5 x12))(∀ x12 . x0 x12not (x11 x5 x7 x6 x12))(∀ x12 . x0 x12not (x11 x6 x7 x4 x12))(∀ x12 . x0 x12not (x11 x7 x6 x7 x12))(∀ x12 . x0 x12not (x11 x2 x2 x12 x7))(∀ x12 . x0 x12not (x11 x6 x2 x12 x6))not (x11 x2 x2 x3 x5)not (x11 x2 x2 x4 x2)not (x11 x2 x2 x5 x2)not (x11 x2 x2 x6 x2)not (x11 x2 x2 x7 x3)not (x11 x2 x2 x7 x6)not (x11 x2 x3 x7 x2)not (x11 x2 x5 x3 x2)not (x11 x2 x5 x5 x2)not (x11 x2 x5 x5 x7)not (x11 x2 x5 x7 x6)not (x11 x2 x6 x5 x4)not (x11 x2 x7 x4 x2)not (x11 x2 x7 x4 x5)not (x11 x3 x2 x4 x5)not (x11 x3 x2 x5 x2)not (x11 x3 x2 x5 x7)not (x11 x3 x2 x7 x4)not (x11 x3 x2 x7 x6)not (x11 x3 x3 x4 x2)not (x11 x3 x4 x4 x2)not (x11 x3 x5 x4 x2)not (x11 x3 x5 x5 x7)not (x11 x3 x5 x6 x2)not (x11 x3 x5 x7 x6)not (x11 x3 x6 x5 x4)not (x11 x3 x7 x5 x4)not (x11 x4 x2 x4 x5)not (x11 x4 x2 x5 x2)not (x11 x4 x2 x5 x5)not (x11 x4 x2 x6 x2)not (x11 x4 x2 x7 x2)not (x11 x4 x2 x7 x3)not (x11 x4 x2 x7 x5)not (x11 x4 x5 x5 x2)not (x11 x5 x2 x5 x4)not (x11 x5 x2 x5 x5)not (x11 x5 x2 x6 x2)not (x11 x5 x2 x6 x3)not (x11 x5 x2 x6 x5)not (x11 x5 x2 x7 x5)not (x11 x5 x4 x5 x6)not (x11 x5 x4 x6 x6)not (x11 x5 x4 x7 x2)not (x11 x5 x7 x7 x4)not (x11 x5 x7 x7 x6)∀ x12 . x0 x12∀ x13 . x0 x13∀ x14 . x0 x14∀ x15 . x0 x15∀ x16 . x0 x16x11 x5 x4 x4 x12x11 x5 x4 x13 x14x11 x5 x4 x15 x16x11 x4 x12 x13 x14x11 x4 x12 x15 x16x11 x13 x14 x15 x16False
Known 23c75.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 : ι → ο . x8 x2x8 x3x8 x4x8 x5x8 x6x8 x7∀ x9 . x0 x9x8 x9)x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2x1 x3x1 x4x1 x5∀ x8 x9 x10 : ι → ι . x8 x2 = x3x8 x3 = x2x8 x4 = x5x8 x5 = x4x9 x2 = x4x9 x3 = x5x9 x4 = x2x9 x5 = x3x10 x2 = x5x10 x3 = x4x10 x4 = x3x10 x5 = x2∀ x11 : ι → ι → ι → ι → ο . (∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x12 x13))(∀ x12 x13 x14 x15 . x11 x12 x13 x14 x15x11 x14 x15 x12 x13)(∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x7 x7))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x8 x13) x14 (x8 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x9 x13) x14 (x9 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x10 x13) x14 (x10 x15)))(∀ x12 . x0 x12not (x11 x4 x6 x5 x12))(∀ x12 . x0 x12not (x11 x4 x7 x5 x12))(∀ x12 . x0 x12not (x11 x5 x7 x6 x12))(∀ x12 . x0 x12not (x11 x7 x6 x7 x12))(∀ x12 . x0 x12not (x11 x2 x2 x12 x7))(∀ x12 . x0 x12not (x11 x5 x5 x12 x7))not (x11 x2 x2 x5 x2)not (x11 x2 x2 x5 x5)not (x11 x2 x5 x5 x2)not (x11 x2 x5 x5 x7)not (x11 x2 x6 x5 x4)not (x11 x2 x7 x3 x3)not (x11 x2 x7 x4 x2)not (x11 x2 x7 x4 x5)not (x11 x2 x7 x7 x5)not (x11 x3 x2 x3 x3)not (x11 x3 x2 x4 x4)not (x11 x3 x2 x5 x2)not (x11 x3 x2 x5 x7)not (x11 x3 x2 x7 x4)not (x11 x3 x2 x7 x5)not (x11 x3 x2 x7 x6)not (x11 x3 x3 x4 x2)not (x11 x3 x3 x7 x6)not (x11 x3 x4 x4 x2)not (x11 x3 x4 x7 x2)not (x11 x3 x5 x5 x7)not (x11 x3 x5 x7 x2)not (x11 x3 x6 x5 x4)not (x11 x3 x7 x5 x4)not (x11 x4 x2 x4 x5)not (x11 x4 x2 x5 x2)not (x11 x4 x2 x5 x5)not (x11 x4 x2 x7 x2)not (x11 x4 x2 x7 x5)not (x11 x4 x5 x5 x2)not (x11 x5 x2 x5 x4)not (x11 x5 x2 x5 x5)not (x11 x5 x2 x6 x2)not (x11 x5 x2 x6 x3)not (x11 x5 x2 x6 x5)not (x11 x5 x2 x7 x5)not (x11 x5 x4 x5 x6)not (x11 x5 x4 x6 x6)not (x11 x5 x4 x7 x2)not (x11 x5 x5 x6 x2)not (x11 x5 x7 x7 x4)not (x11 x5 x7 x7 x6)not (x11 x7 x2 x7 x3)∀ x12 . x0 x12∀ x13 . x0 x13∀ x14 . x0 x14∀ x15 . x0 x15∀ x16 . x0 x16x11 x5 x4 x5 x12x11 x5 x4 x13 x14x11 x5 x4 x15 x16x11 x5 x12 x13 x14x11 x5 x12 x15 x16x11 x13 x14 x15 x16False
Known eff90.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 : ι → ο . x8 x2x8 x3x8 x4x8 x5x8 x6x8 x7∀ x9 . x0 x9x8 x9)x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2x1 x3x1 x4x1 x5∀ x8 x9 x10 : ι → ι . x8 x2 = x3x8 x3 = x2x8 x4 = x5x8 x5 = x4x9 x2 = x4x9 x3 = x5x9 x4 = x2x9 x5 = x3x10 x2 = x5x10 x3 = x4x10 x4 = x3x10 x5 = x2∀ x11 : ι → ι → ι → ι → ο . (∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x12 x13))(∀ x12 x13 x14 x15 . x11 x12 x13 x14 x15x11 x14 x15 x12 x13)(∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x7 x7))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x8 x13) x14 (x8 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x9 x13) x14 (x9 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x10 x13) x14 (x10 x15)))(∀ x12 . x0 x12not (x11 x4 x6 x5 x12))(∀ x12 . x0 x12not (x11 x4 x7 x5 x12))(∀ x12 . x0 x12not (x11 x5 x7 x6 x12))(∀ x12 . x0 x12not (x11 x6 x7 x2 x12))(∀ x12 . x0 x12not (x11 x6 x7 x4 x12))(∀ x12 . x0 x12not (x11 x7 x6 x7 x12))(∀ x12 . x0 x12not (x11 x5 x5 x12 x7))(∀ x12 . x0 x12not (x11 x6 x2 x12 x6))(∀ x12 . x0 x12not (x11 x6 x7 x12 x7))not (x11 x2 x2 x3 x4)not (x11 x2 x2 x4 x2)not (x11 x2 x2 x5 x2)not (x11 x2 x2 x6 x2)not (x11 x2 x4 x3 x2)not (x11 x2 x5 x2 x7)not (x11 x2 x5 x5 x2)not (x11 x2 x6 x5 x4)not (x11 x2 x7 x3 x3)not (x11 x2 x7 x4 x5)not (x11 x3 x2 x4 x4)not (x11 x3 x2 x5 x2)not (x11 x3 x2 x6 x2)not (x11 x3 x2 x7 x4)not (x11 x3 x2 x7 x5)not (x11 x3 x2 x7 x6)not (x11 x3 x3 x6 x7)not (x11 x3 x4 x4 x2)not (x11 x3 x5 x6 x2)not (x11 x3 x5 x6 x7)not (x11 x3 x6 x5 x4)not (x11 x3 x7 x5 x4)not (x11 x4 x2 x5 x2)not (x11 x4 x2 x6 x2)not (x11 x4 x5 x5 x2)not (x11 x5 x2 x5 x4)not (x11 x5 x2 x5 x5)not (x11 x5 x2 x6 x2)not (x11 x5 x2 x6 x3)not (x11 x5 x2 x6 x5)not (x11 x5 x2 x7 x5)not (x11 x5 x4 x5 x6)not (x11 x5 x4 x6 x6)not (x11 x5 x4 x7 x2)not (x11 x5 x5 x6 x2)not (x11 x6 x2 x7 x4)not (x11 x6 x2 x7 x5)not (x11 x7 x2 x7 x3)∀ x12 . x0 x12∀ x13 . x0 x13∀ x14 . x0 x14∀ x15 . x0 x15∀ x16 . x0 x16x11 x5 x4 x6 x12x11 x5 x4 x13 x14x11 x5 x4 x15 x16x11 x6 x12 x13 x14x11 x6 x12 x15 x16x11 x13 x14 x15 x16False
Known 61123.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 : ι → ο . x8 x2x8 x3x8 x4x8 x5x8 x6x8 x7∀ x9 . x0 x9x8 x9)x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2x1 x3x1 x4x1 x5∀ x8 x9 x10 : ι → ι . x8 x2 = x3x8 x3 = x2x8 x4 = x5x8 x5 = x4x9 x2 = x4x9 x3 = x5x9 x4 = x2x9 x5 = x3x10 x2 = x5x10 x3 = x4x10 x4 = x3x10 x5 = x2∀ x11 : ι → ι → ι → ι → ο . (∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x12 x13))(∀ x12 x13 x14 x15 . x11 x12 x13 x14 x15x11 x14 x15 x12 x13)(∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x7 x7))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x8 x13) x14 (x8 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x9 x13) x14 (x9 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x10 x13) x14 (x10 x15)))(∀ x12 . x0 x12not (x11 x4 x6 x5 x12))(∀ x12 . x0 x12not (x11 x4 x7 x5 x12))(∀ x12 . x0 x12not (x11 x5 x7 x6 x12))(∀ x12 . x0 x12not (x11 x6 x7 x2 x12))(∀ x12 . x0 x12not (x11 x6 x7 x4 x12))(∀ x12 . x0 x12not (x11 x7 x6 x7 x12))(∀ x12 . x0 x12not (x11 x2 x2 x12 x7))(∀ x12 . x0 x12not (x11 x5 x5 x12 x7))(∀ x12 . x0 x12not (x11 x6 x2 x12 x6))(∀ x12 . x0 x12not (x11 x6 x7 x12 x7))not (x11 x2 x2 x2 x5)not (x11 x2 x2 x3 x5)not (x11 x2 x2 x4 x2)not (x11 x2 x2 x5 x2)not (x11 x2 x2 x5 x5)not (x11 x2 x2 x7 x6)not (x11 x2 x3 x7 x2)not (x11 x2 x5 x5 x2)not (x11 x2 x5 x5 x7)not (x11 x2 x5 x7 x6)not (x11 x2 x6 x5 x4)not (x11 x2 x7 x4 x2)not (x11 x2 x7 x4 x5)not (x11 x2 x7 x7 x4)not (x11 x2 x7 x7 x5)not (x11 x3 x2 x5 x2)not (x11 x3 x2 x7 x2)not (x11 x3 x2 x7 x4)not (x11 x3 x2 x7 x5)not (x11 x3 x2 x7 x6)not (x11 x3 x3 x7 x6)not (x11 x3 x4 x7 x2)not (x11 x3 x5 x4 x2)not (x11 x3 x5 x6 x7)not (x11 x3 x5 x7 x2)not (x11 x3 x5 x7 x6)not (x11 x3 x6 x5 x4)not (x11 x3 x7 x5 x4)not (x11 x4 x2 x4 x5)not (x11 x4 x2 x5 x2)not (x11 x4 x2 x5 x5)not (x11 x4 x2 x7 x2)not (x11 x4 x2 x7 x5)not (x11 x4 x3 x7 x2)not (x11 x4 x5 x5 x2)not (x11 x5 x2 x5 x4)not (x11 x5 x2 x5 x5)not (x11 x5 x2 x6 x2)not (x11 x5 x2 x6 x3)not (x11 x5 x2 x6 x5)not (x11 x5 x2 x7 x5)not (x11 x5 x4 x5 x6)not (x11 x5 x4 x6 x6)not (x11 x5 x4 x7 x2)not (x11 x5 x7 x7 x4)not (x11 x5 x7 x7 x6)not (x11 x6 x2 x7 x4)not (x11 x6 x2 x7 x5)not (x11 x7 x2 x7 x3)∀ x12 . x0 x12∀ x13 . x0 x13∀ x14 . x0 x14∀ x15 . x0 x15∀ x16 . x0 x16x11 x5 x4 x7 x12x11 x5 x4 x13 x14x11 x5 x4 x15 x16x11 x7 x12 x13 x14x11 x7 x12 x15 x16x11 x13 x14 x15 x16False
Known bb807.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 : ι → ο . x8 x2x8 x3x8 x4x8 x5x8 x6x8 x7∀ x9 . x0 x9x8 x9)x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2x1 x3x1 x4x1 x5∀ x8 x9 x10 : ι → ι . x8 x2 = x3x8 x3 = x2x8 x4 = x5x8 x5 = x4x9 x2 = x4x9 x3 = x5x9 x4 = x2x9 x5 = x3x10 x2 = x5x10 x3 = x4x10 x4 = x3x10 x5 = x2∀ x11 : ι → ι → ι → ι → ο . (∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x12 x13))(∀ x12 x13 x14 x15 . x11 x12 x13 x14 x15x11 x14 x15 x12 x13)(∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x7 x7))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x8 x13) x14 (x8 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x9 x13) x14 (x9 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x10 x13) x14 (x10 x15)))(∀ x12 . x0 x12not (x11 x4 x6 x5 x12))(∀ x12 . x0 x12not (x11 x5 x6 x6 x12))(∀ x12 . x0 x12not (x11 x6 x6 x2 x12))(∀ x12 . x0 x12not (x11 x2 x3 x12 x6))(∀ x12 . x0 x12not (x11 x5 x5 x12 x7))not (x11 x2 x2 x2 x5)not (x11 x2 x2 x3 x5)not (x11 x2 x2 x4 x2)not (x11 x2 x2 x5 x2)not (x11 x2 x2 x5 x5)not (x11 x2 x2 x6 x2)not (x11 x2 x2 x7 x3)not (x11 x2 x4 x2 x6)not (x11 x2 x4 x3 x2)not (x11 x2 x4 x5 x6)not (x11 x2 x4 x7 x6)not (x11 x2 x6 x3 x2)not (x11 x2 x6 x4 x3)not (x11 x2 x6 x4 x4)not (x11 x2 x6 x5 x4)not (x11 x2 x6 x7 x4)not (x11 x2 x6 x7 x5)not (x11 x3 x2 x3 x3)not (x11 x3 x2 x3 x5)not (x11 x3 x2 x4 x4)not (x11 x3 x2 x4 x5)not (x11 x3 x2 x5 x2)not (x11 x3 x2 x6 x2)not (x11 x3 x2 x6 x5)not (x11 x3 x2 x7 x2)not (x11 x3 x2 x7 x4)not (x11 x3 x2 x7 x5)not (x11 x3 x3 x5 x6)not (x11 x3 x3 x7 x6)not (x11 x3 x4 x5 x6)not (x11 x3 x4 x7 x2)not (x11 x3 x4 x7 x6)not (x11 x3 x5 x4 x2)not (x11 x3 x5 x6 x2)not (x11 x3 x5 x7 x2)not (x11 x3 x6 x5 x5)not (x11 x4 x2 x5 x2)not (x11 x4 x2 x5 x5)not (x11 x4 x2 x6 x2)not (x11 x4 x2 x7 x2)not (x11 x4 x2 x7 x3)not (x11 x4 x2 x7 x5)not (x11 x4 x3 x7 x2)not (x11 x4 x5 x7 x2)not (x11 x5 x2 x5 x4)not (x11 x5 x2 x5 x5)not (x11 x5 x2 x6 x2)not (x11 x5 x2 x6 x3)not (x11 x5 x2 x7 x4)not (x11 x5 x5 x6 x2)not (x11 x5 x5 x7 x2)not (x11 x5 x6 x7 x6)not (x11 x6 x2 x7 x5)not (x11 x6 x3 x7 x6)not (x11 x6 x5 x7 x2)not (x11 x7 x2 x7 x3)∀ x12 . x0 x12∀ x13 . x0 x13∀ x14 . x0 x14∀ x15 . x0 x15∀ x16 . x0 x16x11 x5 x5 x2 x12x11 x5 x5 x13 x14x11 x5 x5 x15 x16x11 x2 x12 x13 x14x11 x2 x12 x15 x16x11 x13 x14 x15 x16False
Known c496b.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 : ι → ο . x8 x2x8 x3x8 x4x8 x5x8 x6x8 x7∀ x9 . x0 x9x8 x9)x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2x1 x3x1 x4x1 x5∀ x8 x9 x10 : ι → ι . x8 x2 = x3x8 x3 = x2x8 x4 = x5x8 x5 = x4x9 x2 = x4x9 x3 = x5x9 x4 = x2x9 x5 = x3x10 x2 = x5x10 x3 = x4x10 x4 = x3x10 x5 = x2∀ x11 : ι → ι → ι → ι → ο . (∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x12 x13))(∀ x12 x13 x14 x15 . x11 x12 x13 x14 x15x11 x14 x15 x12 x13)(∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x7 x7))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x8 x13) x14 (x8 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x9 x13) x14 (x9 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x10 x13) x14 (x10 x15)))(∀ x12 . x0 x12not (x11 x4 x6 x5 x12))(∀ x12 . x0 x12not (x11 x5 x6 x6 x12))(∀ x12 . x0 x12not (x11 x6 x6 x2 x12))(∀ x12 . x0 x12not (x11 x6 x6 x4 x12))(∀ x12 . x0 x12not (x11 x2 x3 x12 x6))(∀ x12 . x0 x12not (x11 x5 x5 x12 x7))not (x11 x2 x2 x3 x5)not (x11 x2 x2 x4 x2)not (x11 x2 x2 x5 x2)not (x11 x2 x2 x5 x5)not (x11 x2 x2 x6 x2)not (x11 x2 x2 x7 x3)not (x11 x2 x3 x7 x2)not (x11 x2 x4 x2 x6)not (x11 x2 x4 x3 x2)not (x11 x2 x5 x3 x2)not (x11 x2 x5 x5 x2)not (x11 x2 x6 x3 x2)not (x11 x2 x6 x4 x3)not (x11 x2 x6 x4 x4)not (x11 x2 x6 x5 x4)not (x11 x2 x6 x7 x5)not (x11 x3 x2 x3 x3)not (x11 x3 x2 x3 x5)not (x11 x3 x2 x4 x3)not (x11 x3 x2 x4 x4)not (x11 x3 x2 x4 x5)not (x11 x3 x2 x5 x2)not (x11 x3 x2 x6 x2)not (x11 x3 x2 x6 x5)not (x11 x3 x2 x6 x6)not (x11 x3 x2 x7 x2)not (x11 x3 x2 x7 x4)not (x11 x3 x2 x7 x5)not (x11 x3 x2 x7 x6)not (x11 x3 x3 x5 x6)not (x11 x3 x3 x7 x6)not (x11 x3 x4 x5 x6)not (x11 x3 x4 x6 x6)not (x11 x3 x4 x7 x6)not (x11 x3 x5 x6 x2)not (x11 x3 x6 x5 x5)not (x11 x4 x2 x5 x2)not (x11 x4 x2 x5 x5)not (x11 x4 x2 x7 x3)not (x11 x4 x3 x7 x2)not (x11 x4 x5 x5 x2)not (x11 x5 x2 x5 x4)not (x11 x5 x2 x5 x5)not (x11 x5 x2 x6 x2)not (x11 x5 x2 x6 x3)not (x11 x5 x2 x6 x5)not (x11 x5 x2 x7 x4)not (x11 x5 x4 x5 x6)not (x11 x5 x4 x6 x6)not (x11 x5 x5 x6 x2)not (x11 x5 x5 x7 x2)∀ x12 . x0 x12∀ x13 . x0 x13∀ x14 . x0 x14∀ x15 . x0 x15∀ x16 . x0 x16x11 x5 x5 x3 x12x11 x5 x5 x13 x14x11 x5 x5 x15 x16x11 x3 x12 x13 x14x11 x3 x12 x15 x16x11 x13 x14 x15 x16False
Known ba172.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 : ι → ο . x8 x2x8 x3x8 x4x8 x5x8 x6x8 x7∀ x9 . x0 x9x8 x9)x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2x1 x3x1 x4x1 x5∀ x8 x9 x10 : ι → ι . x8 x2 = x3x8 x3 = x2x8 x4 = x5x8 x5 = x4x9 x2 = x4x9 x3 = x5x9 x4 = x2x9 x5 = x3x10 x2 = x5x10 x3 = x4x10 x4 = x3x10 x5 = x2∀ x11 : ι → ι → ι → ι → ο . (∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x12 x13))(∀ x12 x13 x14 x15 . x11 x12 x13 x14 x15x11 x14 x15 x12 x13)(∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x7 x7))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x8 x13) x14 (x8 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x9 x13) x14 (x9 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x10 x13) x14 (x10 x15)))(∀ x12 . x0 x12not (x11 x4 x6 x5 x12))(∀ x12 . x0 x12not (x11 x5 x6 x6 x12))(∀ x12 . x0 x12not (x11 x6 x6 x4 x12))(∀ x12 . x0 x12not (x11 x7 x6 x7 x12))(∀ x12 . x0 x12not (x11 x2 x3 x12 x6))(∀ x12 . x0 x12not (x11 x5 x5 x12 x7))not (x11 x2 x2 x3 x5)not (x11 x2 x2 x4 x2)not (x11 x2 x2 x5 x2)not (x11 x2 x2 x5 x5)not (x11 x2 x2 x6 x2)not (x11 x2 x2 x7 x3)not (x11 x2 x3 x7 x2)not (x11 x2 x4 x5 x6)not (x11 x2 x4 x7 x6)not (x11 x2 x5 x3 x2)not (x11 x2 x6 x4 x3)not (x11 x2 x6 x4 x4)not (x11 x3 x2 x4 x3)not (x11 x3 x2 x4 x4)not (x11 x3 x2 x5 x2)not (x11 x3 x2 x6 x5)not (x11 x3 x2 x7 x4)not (x11 x3 x3 x5 x6)not (x11 x3 x3 x7 x6)not (x11 x3 x4 x5 x6)not (x11 x3 x4 x7 x2)not (x11 x3 x4 x7 x6)not (x11 x3 x5 x4 x2)not (x11 x3 x5 x6 x2)not (x11 x3 x6 x5 x5)not (x11 x4 x2 x4 x5)not (x11 x4 x2 x5 x2)not (x11 x4 x2 x5 x5)not (x11 x4 x2 x6 x2)not (x11 x4 x2 x7 x2)not (x11 x4 x2 x7 x3)not (x11 x4 x2 x7 x5)not (x11 x5 x2 x5 x4)not (x11 x5 x2 x5 x5)not (x11 x5 x2 x6 x2)not (x11 x5 x2 x6 x3)not (x11 x5 x2 x7 x4)not (x11 x5 x5 x6 x2)not (x11 x5 x5 x7 x2)not (x11 x5 x6 x7 x5)not (x11 x5 x6 x7 x6)not (x11 x6 x3 x7 x6)∀ x12 . x0 x12∀ x13 . x0 x13∀ x14 . x0 x14∀ x15 . x0 x15∀ x16 . x0 x16x11 x5 x5 x4 x12x11 x5 x5 x13 x14x11 x5 x5 x15 x16x11 x4 x12 x13 x14x11 x4 x12 x15 x16x11 x13 x14 x15 x16False
Known 7fbee.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 : ι → ο . x8 x2x8 x3x8 x4x8 x5x8 x6x8 x7∀ x9 . x0 x9x8 x9)x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2x1 x3x1 x4x1 x5∀ x8 x9 x10 : ι → ι . x8 x2 = x3x8 x3 = x2x8 x4 = x5x8 x5 = x4x9 x2 = x4x9 x3 = x5x9 x4 = x2x9 x5 = x3x10 x2 = x5x10 x3 = x4x10 x4 = x3x10 x5 = x2∀ x11 : ι → ι → ι → ι → ο . (∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x12 x13))(∀ x12 x13 x14 x15 . x11 x12 x13 x14 x15x11 x14 x15 x12 x13)(∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x7 x7))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x8 x13) x14 (x8 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x9 x13) x14 (x9 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x10 x13) x14 (x10 x15)))(∀ x12 . x0 x12not (x11 x4 x6 x5 x12))(∀ x12 . x0 x12not (x11 x5 x6 x6 x12))(∀ x12 . x0 x12not (x11 x7 x6 x7 x12))(∀ x12 . x0 x12not (x11 x2 x3 x12 x6))(∀ x12 . x0 x12not (x11 x5 x5 x12 x7))not (x11 x2 x2 x5 x2)not (x11 x2 x2 x5 x5)not (x11 x2 x4 x5 x6)not (x11 x2 x5 x5 x2)not (x11 x2 x6 x3 x2)not (x11 x2 x6 x4 x3)not (x11 x2 x6 x4 x4)not (x11 x2 x6 x5 x4)not (x11 x2 x6 x7 x4)not (x11 x3 x2 x3 x3)not (x11 x3 x2 x4 x3)not (x11 x3 x2 x4 x4)not (x11 x3 x2 x5 x2)not (x11 x3 x2 x7 x4)not (x11 x3 x2 x7 x5)not (x11 x3 x2 x7 x6)not (x11 x3 x3 x5 x6)not (x11 x3 x3 x7 x6)not (x11 x3 x4 x5 x6)not (x11 x3 x4 x7 x2)not (x11 x3 x5 x7 x2)not (x11 x3 x6 x5 x5)not (x11 x4 x2 x4 x5)not (x11 x4 x2 x5 x2)not (x11 x4 x2 x5 x5)not (x11 x4 x2 x7 x2)not (x11 x4 x2 x7 x5)not (x11 x4 x5 x5 x2)not (x11 x4 x5 x7 x2)not (x11 x5 x2 x5 x4)not (x11 x5 x2 x5 x5)not (x11 x5 x2 x6 x2)not (x11 x5 x2 x6 x3)not (x11 x5 x2 x6 x5)not (x11 x5 x2 x7 x4)not (x11 x5 x4 x5 x6)not (x11 x5 x4 x6 x6)not (x11 x5 x5 x6 x2)not (x11 x5 x5 x7 x2)not (x11 x5 x6 x7 x5)not (x11 x5 x6 x7 x6)not (x11 x7 x2 x7 x3)∀ x12 . x0 x12∀ x13 . x0 x13∀ x14 . x0 x14∀ x15 . x0 x15∀ x16 . x0 x16x11 x5 x5 x5 x12x11 x5 x5 x13 x14x11 x5 x5 x15 x16x11 x5 x12 x13 x14x11 x5 x12 x15 x16x11 x13 x14 x15 x16False
Known d1ded.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 : ι → ο . x8 x2x8 x3x8 x4x8 x5x8 x6x8 x7∀ x9 . x0 x9x8 x9)x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2x1 x3x1 x4x1 x5∀ x8 x9 x10 : ι → ι . x8 x2 = x3x8 x3 = x2x8 x4 = x5x8 x5 = x4x9 x2 = x4x9 x3 = x5x9 x4 = x2x9 x5 = x3x10 x2 = x5x10 x3 = x4x10 x4 = x3x10 x5 = x2∀ x11 : ι → ι → ι → ι → ο . (∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x12 x13))(∀ x12 x13 x14 x15 . x11 x12 x13 x14 x15x11 x14 x15 x12 x13)(∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x7 x7))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x8 x13) x14 (x8 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x9 x13) x14 (x9 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x10 x13) x14 (x10 x15)))(∀ x12 . x0 x12not (x11 x4 x6 x5 x12))(∀ x12 . x0 x12not (x11 x5 x6 x6 x12))(∀ x12 . x0 x12not (x11 x6 x6 x2 x12))(∀ x12 . x0 x12not (x11 x6 x6 x4 x12))(∀ x12 . x0 x12not (x11 x7 x6 x7 x12))(∀ x12 . x0 x12not (x11 x5 x5 x12 x7))not (x11 x2 x2 x4 x2)not (x11 x2 x2 x5 x2)not (x11 x2 x2 x5 x5)not (x11 x2 x2 x6 x2)not (x11 x2 x4 x2 x6)not (x11 x2 x4 x3 x2)not (x11 x2 x6 x3 x2)not (x11 x2 x6 x4 x4)not (x11 x3 x2 x4 x4)not (x11 x3 x2 x5 x2)not (x11 x3 x2 x6 x2)not (x11 x3 x2 x6 x6)not (x11 x3 x2 x7 x4)not (x11 x3 x2 x7 x5)not (x11 x3 x3 x7 x6)not (x11 x3 x4 x6 x6)not (x11 x3 x4 x7 x2)not (x11 x3 x5 x6 x2)not (x11 x3 x5 x7 x2)not (x11 x3 x6 x5 x5)not (x11 x4 x2 x5 x2)not (x11 x4 x2 x5 x5)not (x11 x4 x2 x6 x2)not (x11 x5 x2 x5 x4)not (x11 x5 x2 x5 x5)not (x11 x5 x2 x6 x2)not (x11 x5 x2 x6 x3)not (x11 x5 x2 x7 x4)not (x11 x5 x4 x6 x6)not (x11 x5 x5 x6 x2)not (x11 x5 x5 x7 x2)not (x11 x6 x2 x7 x4)not (x11 x6 x2 x7 x5)not (x11 x6 x3 x7 x6)not (x11 x6 x4 x7 x2)not (x11 x6 x5 x7 x2)not (x11 x7 x2 x7 x3)∀ x12 . x0 x12∀ x13 . x0 x13∀ x14 . x0 x14∀ x15 . x0 x15∀ x16 . x0 x16x11 x5 x5 x6 x12x11 x5 x5 x13 x14x11 x5 x5 x15 x16x11 x6 x12 x13 x14x11 x6 x12 x15 x16x11 x13 x14 x15 x16False
Known 33323.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 : ι → ο . x8 x2x8 x3x8 x4x8 x5x8 x6x8 x7∀ x9 . x0 x9x8 x9)x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2x1 x3x1 x4x1 x5∀ x8 x9 x10 : ι → ι . x8 x2 = x3x8 x3 = x2x8 x4 = x5x8 x5 = x4x9 x2 = x4x9 x3 = x5x9 x4 = x2x9 x5 = x3x10 x2 = x5x10 x3 = x4x10 x4 = x3x10 x5 = x2∀ x11 : ι → ι → ι → ι → ο . (∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x12 x13))(∀ x12 x13 x14 x15 . x11 x12 x13 x14 x15x11 x14 x15 x12 x13)(∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x7 x7))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x8 x13) x14 (x8 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x9 x13) x14 (x9 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x10 x13) x14 (x10 x15)))(∀ x12 . x0 x12not (x11 x4 x6 x5 x12))(∀ x12 . x0 x12not (x11 x5 x6 x6 x12))(∀ x12 . x0 x12not (x11 x6 x6 x2 x12))(∀ x12 . x0 x12not (x11 x6 x6 x4 x12))(∀ x12 . x0 x12not (x11 x7 x6 x7 x12))(∀ x12 . x0 x12not (x11 x2 x3 x12 x6))(∀ x12 . x0 x12not (x11 x5 x5 x12 x7))not (x11 x2 x2 x2 x5)not (x11 x2 x2 x3 x5)not (x11 x2 x2 x4 x2)not (x11 x2 x2 x5 x2)not (x11 x2 x2 x5 x5)not (x11 x2 x3 x7 x2)not (x11 x2 x4 x5 x6)not (x11 x2 x4 x7 x6)not (x11 x2 x5 x3 x2)not (x11 x2 x5 x5 x2)not (x11 x2 x6 x4 x3)not (x11 x2 x6 x4 x4)not (x11 x2 x6 x5 x4)not (x11 x2 x6 x7 x4)not (x11 x2 x6 x7 x5)not (x11 x3 x2 x4 x5)not (x11 x3 x2 x5 x2)not (x11 x3 x2 x7 x2)not (x11 x3 x2 x7 x4)not (x11 x3 x2 x7 x5)not (x11 x3 x2 x7 x6)not (x11 x3 x3 x7 x6)not (x11 x3 x4 x6 x6)not (x11 x3 x4 x7 x2)not (x11 x3 x4 x7 x6)not (x11 x3 x5 x4 x2)not (x11 x3 x5 x7 x2)not (x11 x3 x6 x5 x5)not (x11 x4 x2 x4 x5)not (x11 x4 x2 x5 x2)not (x11 x4 x2 x5 x5)not (x11 x4 x2 x7 x2)not (x11 x4 x3 x7 x2)not (x11 x4 x5 x5 x2)not (x11 x4 x5 x7 x2)not (x11 x5 x2 x5 x4)not (x11 x5 x2 x5 x5)not (x11 x5 x2 x6 x2)not (x11 x5 x2 x6 x3)not (x11 x5 x2 x7 x4)not (x11 x5 x4 x5 x6)not (x11 x5 x4 x6 x6)not (x11 x5 x5 x6 x2)not (x11 x5 x5 x7 x2)not (x11 x5 x6 x7 x5)not (x11 x5 x6 x7 x6)not (x11 x6 x3 x7 x6)not (x11 x6 x4 x7 x2)not (x11 x6 x5 x7 x2)not (x11 x7 x2 x7 x3)∀ x12 . x0 x12∀ x13 . x0 x13∀ x14 . x0 x14∀ x15 . x0 x15∀ x16 . x0 x16x11 x5 x5 x7 x12x11 x5 x5 x13 x14x11 x5 x5 x15 x16x11 x7 x12 x13 x14x11 x7 x12 x15 x16x11 x13 x14 x15 x16False
Known 79aac.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 : ι → ο . x8 x2x8 x3x8 x4x8 x5x8 x6x8 x7∀ x9 . x0 x9x8 x9)x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2x1 x3x1 x4x1 x5∀ x8 x9 x10 : ι → ι . x8 x2 = x3x8 x3 = x2x8 x4 = x5x8 x5 = x4x9 x2 = x4x9 x3 = x5x9 x4 = x2x9 x5 = x3x10 x2 = x5x10 x3 = x4x10 x4 = x3x10 x5 = x2∀ x11 : ι → ι → ι → ι → ο . (∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x12 x13))(∀ x12 x13 x14 x15 . x11 x12 x13 x14 x15x11 x14 x15 x12 x13)(∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x7 x7))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x8 x13) x14 (x8 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x9 x13) x14 (x9 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x10 x13) x14 (x10 x15)))(∀ x12 . x0 x12not (x11 x4 x6 x5 x12))(∀ x12 . x0 x12not (x11 x4 x7 x5 x12))(∀ x12 . x0 x12not (x11 x5 x6 x6 x12))(∀ x12 . x0 x12not (x11 x2 x2 x12 x7))(∀ x12 . x0 x12not (x11 x2 x3 x12 x6))(∀ x12 . x0 x12not (x11 x5 x5 x12 x7))not (x11 x2 x2 x2 x5)not (x11 x2 x2 x3 x5)not (x11 x2 x2 x4 x3)not (x11 x2 x2 x5 x2)not (x11 x2 x2 x5 x5)not (x11 x2 x2 x7 x3)not (x11 x2 x4 x5 x6)not (x11 x2 x5 x2 x7)not (x11 x2 x5 x3 x2)not (x11 x2 x5 x3 x6)not (x11 x2 x5 x5 x2)not (x11 x2 x6 x2 x7)not (x11 x2 x6 x3 x2)not (x11 x2 x6 x3 x5)not (x11 x2 x6 x3 x6)not (x11 x2 x6 x3 x7)not (x11 x2 x6 x4 x3)not (x11 x2 x6 x4 x4)not (x11 x2 x6 x7 x3)not (x11 x2 x6 x7 x4)not (x11 x2 x7 x3 x6)not (x11 x2 x7 x3 x7)not (x11 x2 x7 x5 x2)not (x11 x2 x7 x7 x3)not (x11 x2 x7 x7 x4)not (x11 x3 x2 x3 x5)not (x11 x3 x2 x3 x6)not (x11 x3 x2 x4 x3)not (x11 x3 x2 x4 x4)not (x11 x3 x2 x7 x4)not (x11 x3 x3 x4 x2)not (x11 x3 x3 x5 x6)not (x11 x3 x4 x4 x2)not (x11 x3 x4 x5 x6)not (x11 x3 x4 x7 x2)not (x11 x3 x5 x3 x7)not (x11 x3 x6 x4 x4)not (x11 x3 x6 x7 x4)not (x11 x3 x7 x4 x3)not (x11 x3 x7 x7 x3)not (x11 x4 x2 x4 x5)not (x11 x4 x2 x5 x6)not (x11 x4 x2 x7 x2)not (x11 x4 x5 x5 x6)not (x11 x5 x2 x5 x5)not (x11 x5 x3 x5 x6)not (x11 x5 x4 x5 x6)not (x11 x5 x6 x5 x7)not (x11 x5 x6 x7 x2)not (x11 x5 x6 x7 x5)not (x11 x5 x6 x7 x6)∀ x12 . x0 x12∀ x13 . x0 x13∀ x14 . x0 x14∀ x15 . x0 x15∀ x16 . x0 x16x11 x5 x6 x2 x12x11 x5 x6 x13 x14x11 x5 x6 x15 x16x11 x2 x12 x13 x14x11 x2 x12 x15 x16x11 x13 x14 x15 x16False
Known caaab.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 : ι → ο . x8 x2x8 x3x8 x4x8 x5x8 x6x8 x7∀ x9 . x0 x9x8 x9)x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2x1 x3x1 x4x1 x5∀ x8 x9 x10 : ι → ι . x8 x2 = x3x8 x3 = x2x8 x4 = x5x8 x5 = x4x9 x2 = x4x9 x3 = x5x9 x4 = x2x9 x5 = x3x10 x2 = x5x10 x3 = x4x10 x4 = x3x10 x5 = x2∀ x11 : ι → ι → ι → ι → ο . (∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x12 x13))(∀ x12 x13 x14 x15 . x11 x12 x13 x14 x15x11 x14 x15 x12 x13)(∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x7 x7))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x8 x13) x14 (x8 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x9 x13) x14 (x9 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x10 x13) x14 (x10 x15)))(∀ x12 . x0 x12not (x11 x4 x6 x5 x12))(∀ x12 . x0 x12not (x11 x4 x7 x5 x12))(∀ x12 . x0 x12not (x11 x5 x6 x6 x12))(∀ x12 . x0 x12not (x11 x2 x2 x12 x7))(∀ x12 . x0 x12not (x11 x2 x3 x12 x6))(∀ x12 . x0 x12not (x11 x5 x5 x12 x7))not (x11 x2 x2 x3 x5)not (x11 x2 x2 x4 x3)not (x11 x2 x2 x5 x5)not (x11 x2 x2 x7 x3)not (x11 x2 x3 x4 x2)not (x11 x2 x3 x7 x2)not (x11 x2 x4 x5 x6)not (x11 x2 x5 x2 x7)not (x11 x2 x5 x3 x2)not (x11 x2 x5 x3 x6)not (x11 x2 x5 x5 x2)not (x11 x2 x6 x3 x2)not (x11 x2 x6 x3 x5)not (x11 x2 x6 x3 x6)not (x11 x2 x6 x3 x7)not (x11 x2 x7 x3 x6)not (x11 x2 x7 x3 x7)not (x11 x2 x7 x5 x2)not (x11 x2 x7 x7 x3)not (x11 x2 x7 x7 x4)not (x11 x3 x2 x3 x5)not (x11 x3 x2 x3 x6)not (x11 x3 x2 x4 x3)not (x11 x3 x2 x4 x4)not (x11 x3 x2 x5 x2)not (x11 x3 x2 x7 x4)not (x11 x3 x3 x5 x6)not (x11 x3 x4 x4 x2)not (x11 x3 x4 x5 x6)not (x11 x3 x4 x7 x2)not (x11 x3 x5 x3 x7)not (x11 x3 x6 x4 x4)not (x11 x3 x6 x5 x2)not (x11 x3 x6 x5 x5)not (x11 x3 x6 x7 x4)not (x11 x3 x7 x4 x3)not (x11 x3 x7 x5 x2)not (x11 x3 x7 x7 x3)not (x11 x4 x2 x5 x6)not (x11 x4 x2 x7 x2)not (x11 x4 x5 x5 x6)not (x11 x5 x2 x7 x4)not (x11 x5 x3 x5 x6)not (x11 x5 x4 x5 x6)not (x11 x5 x4 x7 x2)not (x11 x5 x6 x5 x7)not (x11 x5 x6 x7 x2)not (x11 x5 x6 x7 x5)not (x11 x5 x6 x7 x6)∀ x12 . x0 x12∀ x13 . x0 x13∀ x14 . x0 x14∀ x15 . x0 x15∀ x16 . x0 x16x11 x5 x6 x3 x12x11 x5 x6 x13 x14x11 x5 x6 x15 x16x11 x3 x12 x13 x14x11 x3 x12 x15 x16x11 x13 x14 x15 x16False
Known fbdde.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 : ι → ο . x8 x2x8 x3x8 x4x8 x5x8 x6x8 x7∀ x9 . x0 x9x8 x9)x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2x1 x3x1 x4x1 x5∀ x8 x9 x10 : ι → ι . x8 x2 = x3x8 x3 = x2x8 x4 = x5x8 x5 = x4x9 x2 = x4x9 x3 = x5x9 x4 = x2x9 x5 = x3x10 x2 = x5x10 x3 = x4x10 x4 = x3x10 x5 = x2∀ x11 : ι → ι → ι → ι → ο . (∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x12 x13))(∀ x12 x13 x14 x15 . x11 x12 x13 x14 x15x11 x14 x15 x12 x13)(∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x7 x7))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x8 x13) x14 (x8 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x9 x13) x14 (x9 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x10 x13) x14 (x10 x15)))(∀ x12 . x0 x12not (x11 x4 x6 x5 x12))(∀ x12 . x0 x12not (x11 x4 x7 x5 x12))(∀ x12 . x0 x12not (x11 x5 x6 x6 x12))(∀ x12 . x0 x12not (x11 x2 x2 x12 x7))(∀ x12 . x0 x12not (x11 x2 x3 x12 x6))(∀ x12 . x0 x12not (x11 x5 x5 x12 x7))not (x11 x2 x2 x4 x3)not (x11 x2 x2 x5 x2)not (x11 x2 x2 x5 x5)not (x11 x2 x3 x4 x2)not (x11 x2 x4 x5 x6)not (x11 x2 x5 x2 x7)not (x11 x2 x5 x3 x6)not (x11 x2 x5 x5 x2)not (x11 x2 x6 x4 x3)not (x11 x2 x6 x4 x4)not (x11 x2 x7 x3 x6)not (x11 x2 x7 x3 x7)not (x11 x2 x7 x5 x2)not (x11 x3 x2 x4 x3)not (x11 x3 x2 x4 x4)not (x11 x3 x3 x4 x2)not (x11 x3 x3 x5 x6)not (x11 x3 x4 x4 x2)not (x11 x3 x4 x5 x6)not (x11 x3 x6 x4 x4)not (x11 x3 x6 x5 x2)not (x11 x3 x6 x5 x5)not (x11 x3 x7 x4 x3)not (x11 x3 x7 x5 x2)not (x11 x4 x2 x4 x5)not (x11 x4 x2 x5 x6)not (x11 x4 x2 x7 x2)not (x11 x4 x2 x7 x5)not (x11 x4 x5 x5 x6)not (x11 x5 x2 x5 x5)not (x11 x5 x3 x5 x6)not (x11 x5 x4 x5 x6)not (x11 x5 x6 x5 x7)not (x11 x5 x6 x7 x2)not (x11 x5 x6 x7 x5)not (x11 x5 x6 x7 x6)∀ x12 . x0 x12∀ x13 . x0 x13∀ x14 . x0 x14∀ x15 . x0 x15∀ x16 . x0 x16x11 x5 x6 x4 x12x11 x5 x6 x13 x14x11 x5 x6 x15 x16x11 x4 x12 x13 x14x11 x4 x12 x15 x16x11 x13 x14 x15 x16False
Known 5c797.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 : ι → ο . x8 x2x8 x3x8 x4x8 x5x8 x6x8 x7∀ x9 . x0 x9x8 x9)x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2x1 x3x1 x4x1 x5∀ x8 x9 x10 : ι → ι . x8 x2 = x3x8 x3 = x2x8 x4 = x5x8 x5 = x4x9 x2 = x4x9 x3 = x5x9 x4 = x2x9 x5 = x3x10 x2 = x5x10 x3 = x4x10 x4 = x3x10 x5 = x2∀ x11 : ι → ι → ι → ι → ο . (∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x12 x13))(∀ x12 x13 x14 x15 . x11 x12 x13 x14 x15x11 x14 x15 x12 x13)(∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x7 x7))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x8 x13) x14 (x8 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x9 x13) x14 (x9 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x10 x13) x14 (x10 x15)))(∀ x12 . x0 x12not (x11 x4 x6 x5 x12))(∀ x12 . x0 x12not (x11 x4 x7 x5 x12))(∀ x12 . x0 x12not (x11 x5 x6 x6 x12))(∀ x12 . x0 x12not (x11 x2 x3 x12 x6))(∀ x12 . x0 x12not (x11 x5 x5 x12 x7))not (x11 x2 x2 x5 x2)not (x11 x2 x2 x5 x5)not (x11 x2 x4 x5 x6)not (x11 x2 x5 x5 x2)not (x11 x2 x6 x3 x2)not (x11 x2 x6 x3 x5)not (x11 x2 x6 x4 x3)not (x11 x2 x6 x4 x4)not (x11 x2 x6 x7 x3)not (x11 x2 x6 x7 x4)not (x11 x2 x7 x5 x2)not (x11 x3 x2 x4 x3)not (x11 x3 x2 x4 x4)not (x11 x3 x2 x5 x2)not (x11 x3 x2 x7 x4)not (x11 x3 x3 x4 x2)not (x11 x3 x3 x5 x6)not (x11 x3 x4 x4 x2)not (x11 x3 x4 x5 x6)not (x11 x3 x4 x7 x2)not (x11 x3 x6 x5 x2)not (x11 x3 x6 x5 x5)not (x11 x3 x7 x5 x2)not (x11 x4 x2 x4 x5)not (x11 x4 x2 x5 x6)not (x11 x4 x2 x7 x2)not (x11 x4 x2 x7 x5)not (x11 x4 x5 x5 x6)not (x11 x4 x5 x7 x2)not (x11 x5 x2 x5 x5)not (x11 x5 x2 x7 x4)not (x11 x5 x3 x5 x6)not (x11 x5 x4 x5 x6)not (x11 x5 x6 x5 x7)not (x11 x5 x6 x7 x2)not (x11 x5 x6 x7 x5)not (x11 x5 x6 x7 x6)∀ x12 . x0 x12∀ x13 . x0 x13∀ x14 . x0 x14∀ x15 . x0 x15∀ x16 . x0 x16x11 x5 x6 x5 x12x11 x5 x6 x13 x14x11 x5 x6 x15 x16x11 x5 x12 x13 x14x11 x5 x12 x15 x16x11 x13 x14 x15 x16False
Known dde6c.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 : ι → ο . x8 x2x8 x3x8 x4x8 x5x8 x6x8 x7∀ x9 . x0 x9x8 x9)x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2x1 x3x1 x4x1 x5∀ x8 x9 x10 : ι → ι . x8 x2 = x3x8 x3 = x2x8 x4 = x5x8 x5 = x4x9 x2 = x4x9 x3 = x5x9 x4 = x2x9 x5 = x3x10 x2 = x5x10 x3 = x4x10 x4 = x3x10 x5 = x2∀ x11 : ι → ι → ι → ι → ο . (∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x12 x13))(∀ x12 x13 x14 x15 . x11 x12 x13 x14 x15x11 x14 x15 x12 x13)(∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x7 x7))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x8 x13) x14 (x8 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x9 x13) x14 (x9 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x10 x13) x14 (x10 x15)))(∀ x12 . x0 x12not (x11 x4 x6 x5 x12))(∀ x12 . x0 x12not (x11 x4 x7 x5 x12))(∀ x12 . x0 x12not (x11 x5 x6 x6 x12))(∀ x12 . x0 x12not (x11 x2 x2 x12 x7))(∀ x12 . x0 x12not (x11 x2 x3 x12 x6))(∀ x12 . x0 x12not (x11 x5 x5 x12 x7))not (x11 x2 x2 x3 x5)not (x11 x2 x2 x5 x5)not (x11 x2 x2 x7 x3)not (x11 x2 x3 x7 x2)not (x11 x2 x4 x5 x6)not (x11 x2 x5 x3 x2)not (x11 x2 x5 x3 x6)not (x11 x2 x5 x5 x2)not (x11 x2 x6 x7 x3)not (x11 x2 x6 x7 x4)not (x11 x2 x7 x7 x3)not (x11 x2 x7 x7 x4)not (x11 x3 x2 x3 x6)not (x11 x3 x2 x5 x2)not (x11 x3 x2 x7 x4)not (x11 x3 x3 x5 x6)not (x11 x3 x4 x5 x6)not (x11 x3 x4 x7 x2)not (x11 x3 x5 x3 x7)not (x11 x3 x6 x5 x2)not (x11 x3 x6 x7 x4)not (x11 x3 x7 x7 x3)not (x11 x4 x2 x5 x6)not (x11 x4 x2 x7 x2)not (x11 x4 x5 x5 x6)not (x11 x4 x5 x7 x2)not (x11 x5 x2 x7 x4)not (x11 x5 x3 x5 x6)not (x11 x5 x4 x5 x6)not (x11 x5 x4 x7 x2)not (x11 x5 x6 x5 x7)not (x11 x5 x6 x7 x2)not (x11 x5 x6 x7 x5)not (x11 x5 x6 x7 x6)∀ x12 . x0 x12∀ x13 . x0 x13∀ x14 . x0 x14∀ x15 . x0 x15∀ x16 . x0 x16x11 x5 x6 x7 x12x11 x5 x6 x13 x14x11 x5 x6 x15 x16x11 x7 x12 x13 x14x11 x7 x12 x15 x16x11 x13 x14 x15 x16False
Known e973f.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 : ι → ο . x8 x2x8 x3x8 x4x8 x5x8 x6x8 x7∀ x9 . x0 x9x8 x9)x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2x1 x3x1 x4x1 x5∀ x8 x9 x10 : ι → ι . x8 x2 = x3x8 x3 = x2x8 x4 = x5x8 x5 = x4x9 x2 = x4x9 x3 = x5x9 x4 = x2x9 x5 = x3x10 x2 = x5x10 x3 = x4x10 x4 = x3x10 x5 = x2∀ x11 : ι → ι → ι → ι → ο . (∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x12 x13))(∀ x12 x13 x14 x15 . x11 x12 x13 x14 x15x11 x14 x15 x12 x13)(∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x7 x7))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x8 x13) x14 (x8 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x9 x13) x14 (x9 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x10 x13) x14 (x10 x15)))(∀ x12 . x0 x12not (x11 x4 x6 x5 x12))(∀ x12 . x0 x12not (x11 x4 x7 x5 x12))(∀ x12 . x0 x12not (x11 x5 x7 x6 x12))(∀ x12 . x0 x12not (x11 x2 x2 x12 x7))(∀ x12 . x0 x12not (x11 x2 x3 x12 x6))(∀ x12 . x0 x12not (x11 x5 x5 x12 x7))not (x11 x2 x2 x2 x5)not (x11 x2 x2 x3 x5)not (x11 x2 x2 x4 x3)not (x11 x2 x2 x5 x2)not (x11 x2 x2 x5 x5)not (x11 x2 x2 x7 x3)not (x11 x2 x3 x4 x2)not (x11 x2 x3 x7 x2)not (x11 x2 x4 x2 x6)not (x11 x2 x4 x3 x7)not (x11 x2 x5 x5 x2)not (x11 x2 x5 x5 x7)not (x11 x2 x6 x2 x7)not (x11 x2 x6 x3 x6)not (x11 x2 x6 x3 x7)not (x11 x2 x6 x5 x3)not (x11 x2 x6 x5 x4)not (x11 x2 x6 x7 x2)not (x11 x2 x6 x7 x5)not (x11 x2 x7 x3 x3)not (x11 x2 x7 x3 x4)not (x11 x2 x7 x3 x6)not (x11 x2 x7 x3 x7)not (x11 x2 x7 x4 x2)not (x11 x2 x7 x4 x5)not (x11 x2 x7 x7 x2)not (x11 x2 x7 x7 x5)not (x11 x3 x2 x3 x5)not (x11 x3 x2 x4 x3)not (x11 x3 x2 x4 x4)not (x11 x3 x2 x5 x7)not (x11 x3 x2 x7 x4)not (x11 x3 x3 x3 x7)not (x11 x3 x3 x4 x2)not (x11 x3 x4 x3 x6)not (x11 x3 x4 x4 x2)not (x11 x3 x4 x7 x2)not (x11 x3 x5 x5 x7)not (x11 x3 x6 x4 x2)not (x11 x3 x6 x7 x2)not (x11 x3 x7 x4 x5)not (x11 x3 x7 x7 x5)not (x11 x4 x2 x4 x5)not (x11 x4 x2 x7 x2)not (x11 x4 x3 x5 x7)not (x11 x4 x4 x5 x7)not (x11 x5 x2 x5 x5)not (x11 x5 x2 x5 x7)not (x11 x5 x6 x5 x7)not (x11 x5 x7 x7 x3)not (x11 x5 x7 x7 x4)not (x11 x5 x7 x7 x6)∀ x12 . x0 x12∀ x13 . x0 x13∀ x14 . x0 x14∀ x15 . x0 x15∀ x16 . x0 x16x11 x5 x7 x2 x12x11 x5 x7 x13 x14x11 x5 x7 x15 x16x11 x2 x12 x13 x14x11 x2 x12 x15 x16x11 x13 x14 x15 x16False
Known b0910.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 : ι → ο . x8 x2x8 x3x8 x4x8 x5x8 x6x8 x7∀ x9 . x0 x9x8 x9)x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2x1 x3x1 x4x1 x5∀ x8 x9 x10 : ι → ι . x8 x2 = x3x8 x3 = x2x8 x4 = x5x8 x5 = x4x9 x2 = x4x9 x3 = x5x9 x4 = x2x9 x5 = x3x10 x2 = x5x10 x3 = x4x10 x4 = x3x10 x5 = x2∀ x11 : ι → ι → ι → ι → ο . (∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x12 x13))(∀ x12 x13 x14 x15 . x11 x12 x13 x14 x15x11 x14 x15 x12 x13)(∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x7 x7))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x8 x13) x14 (x8 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x9 x13) x14 (x9 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x10 x13) x14 (x10 x15)))(∀ x12 . x0 x12not (x11 x4 x6 x5 x12))(∀ x12 . x0 x12not (x11 x4 x7 x5 x12))(∀ x12 . x0 x12not (x11 x5 x7 x6 x12))(∀ x12 . x0 x12not (x11 x2 x2 x12 x7))(∀ x12 . x0 x12not (x11 x2 x3 x12 x6))(∀ x12 . x0 x12not (x11 x5 x5 x12 x7))not (x11 x2 x2 x3 x5)not (x11 x2 x2 x4 x3)not (x11 x2 x2 x5 x5)not (x11 x2 x2 x7 x3)not (x11 x2 x3 x4 x2)not (x11 x2 x3 x7 x2)not (x11 x2 x4 x2 x6)not (x11 x2 x4 x3 x7)not (x11 x2 x5 x3 x2)not (x11 x2 x5 x5 x2)not (x11 x2 x5 x5 x7)not (x11 x2 x6 x3 x6)not (x11 x2 x6 x3 x7)not (x11 x2 x6 x5 x3)not (x11 x2 x6 x5 x4)not (x11 x2 x6 x7 x2)not (x11 x2 x6 x7 x5)not (x11 x2 x7 x3 x3)not (x11 x2 x7 x3 x4)not (x11 x2 x7 x3 x6)not (x11 x2 x7 x3 x7)not (x11 x3 x2 x3 x5)not (x11 x3 x2 x4 x3)not (x11 x3 x2 x4 x4)not (x11 x3 x2 x5 x2)not (x11 x3 x2 x5 x7)not (x11 x3 x2 x7 x4)not (x11 x3 x3 x3 x7)not (x11 x3 x3 x4 x2)not (x11 x3 x4 x3 x6)not (x11 x3 x4 x4 x2)not (x11 x3 x4 x7 x2)not (x11 x3 x5 x5 x7)not (x11 x3 x6 x4 x2)not (x11 x3 x6 x5 x3)not (x11 x3 x6 x5 x4)not (x11 x3 x6 x7 x2)not (x11 x3 x7 x4 x5)not (x11 x3 x7 x5 x3)not (x11 x3 x7 x5 x4)not (x11 x3 x7 x7 x5)not (x11 x4 x2 x7 x2)not (x11 x4 x3 x5 x7)not (x11 x4 x4 x5 x7)not (x11 x5 x2 x5 x7)not (x11 x5 x2 x7 x4)not (x11 x5 x4 x7 x2)not (x11 x5 x6 x5 x7)not (x11 x5 x7 x7 x3)not (x11 x5 x7 x7 x4)not (x11 x5 x7 x7 x6)∀ x12 . x0 x12∀ x13 . x0 x13∀ x14 . x0 x14∀ x15 . x0 x15∀ x16 . x0 x16x11 x5 x7 x3 x12x11 x5 x7 x13 x14x11 x5 x7 x15 x16x11 x3 x12 x13 x14x11 x3 x12 x15 x16x11 x13 x14 x15 x16False
Known 4e4c6.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 : ι → ο . x8 x2x8 x3x8 x4x8 x5x8 x6x8 x7∀ x9 . x0 x9x8 x9)x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2x1 x3x1 x4x1 x5∀ x8 x9 x10 : ι → ι . x8 x2 = x3x8 x3 = x2x8 x4 = x5x8 x5 = x4x9 x2 = x4x9 x3 = x5x9 x4 = x2x9 x5 = x3x10 x2 = x5x10 x3 = x4x10 x4 = x3x10 x5 = x2∀ x11 : ι → ι → ι → ι → ο . (∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x12 x13))(∀ x12 x13 x14 x15 . x11 x12 x13 x14 x15x11 x14 x15 x12 x13)(∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x7 x7))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x8 x13) x14 (x8 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x9 x13) x14 (x9 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x10 x13) x14 (x10 x15)))(∀ x12 . x0 x12not (x11 x4 x6 x5 x12))(∀ x12 . x0 x12not (x11 x4 x7 x5 x12))(∀ x12 . x0 x12not (x11 x5 x7 x6 x12))(∀ x12 . x0 x12not (x11 x2 x2 x12 x7))(∀ x12 . x0 x12not (x11 x2 x3 x12 x6))(∀ x12 . x0 x12not (x11 x5 x5 x12 x7))not (x11 x2 x2 x5 x2)not (x11 x2 x2 x5 x5)not (x11 x2 x3 x4 x2)not (x11 x2 x4 x2 x6)not (x11 x2 x4 x3 x7)not (x11 x2 x5 x5 x2)not (x11 x2 x5 x5 x7)not (x11 x2 x6 x3 x6)not (x11 x2 x6 x3 x7)not (x11 x2 x6 x5 x3)not (x11 x2 x6 x5 x4)not (x11 x2 x7 x4 x2)not (x11 x2 x7 x4 x5)not (x11 x3 x2 x5 x7)not (x11 x3 x3 x4 x2)not (x11 x3 x4 x4 x2)not (x11 x3 x5 x5 x7)not (x11 x3 x6 x4 x2)not (x11 x3 x6 x5 x3)not (x11 x3 x6 x5 x4)not (x11 x3 x7 x4 x5)not (x11 x3 x7 x5 x3)not (x11 x3 x7 x5 x4)not (x11 x4 x2 x4 x5)not (x11 x4 x2 x7 x2)not (x11 x4 x2 x7 x5)not (x11 x4 x3 x5 x7)not (x11 x4 x4 x5 x7)not (x11 x4 x5 x7 x2)not (x11 x5 x2 x5 x5)not (x11 x5 x2 x5 x7)not (x11 x5 x6 x5 x7)not (x11 x5 x7 x7 x3)not (x11 x5 x7 x7 x4)not (x11 x5 x7 x7 x6)∀ x12 . x0 x12∀ x13 . x0 x13∀ x14 . x0 x14∀ x15 . x0 x15∀ x16 . x0 x16x11 x5 x7 x4 x12x11 x5 x7 x13 x14x11 x5 x7 x15 x16x11 x4 x12 x13 x14x11 x4 x12 x15 x16x11 x13 x14 x15 x16False
Known 694fc.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 : ι → ο . x8 x2x8 x3x8 x4x8 x5x8 x6x8 x7∀ x9 . x0 x9x8 x9)x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2x1 x3x1 x4x1 x5∀ x8 x9 x10 : ι → ι . x8 x2 = x3x8 x3 = x2x8 x4 = x5x8 x5 = x4x9 x2 = x4x9 x3 = x5x9 x4 = x2x9 x5 = x3x10 x2 = x5x10 x3 = x4x10 x4 = x3x10 x5 = x2∀ x11 : ι → ι → ι → ι → ο . (∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x12 x13))(∀ x12 x13 x14 x15 . x11 x12 x13 x14 x15x11 x14 x15 x12 x13)(∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x7 x7))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x8 x13) x14 (x8 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x9 x13) x14 (x9 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x10 x13) x14 (x10 x15)))(∀ x12 . x0 x12not (x11 x4 x6 x5 x12))(∀ x12 . x0 x12not (x11 x4 x7 x5 x12))(∀ x12 . x0 x12not (x11 x5 x7 x6 x12))(∀ x12 . x0 x12not (x11 x2 x2 x12 x7))(∀ x12 . x0 x12not (x11 x5 x5 x12 x7))not (x11 x2 x2 x5 x2)not (x11 x2 x5 x5 x2)not (x11 x2 x5 x5 x7)not (x11 x2 x6 x5 x3)not (x11 x2 x6 x5 x4)not (x11 x2 x7 x3 x3)not (x11 x2 x7 x3 x4)not (x11 x2 x7 x4 x2)not (x11 x2 x7 x4 x5)not (x11 x2 x7 x7 x2)not (x11 x2 x7 x7 x5)not (x11 x3 x2 x4 x3)not (x11 x3 x2 x4 x4)not (x11 x3 x2 x5 x2)not (x11 x3 x2 x5 x7)not (x11 x3 x2 x7 x4)not (x11 x3 x3 x4 x2)not (x11 x3 x4 x4 x2)not (x11 x3 x4 x7 x2)not (x11 x3 x5 x5 x7)not (x11 x3 x6 x5 x3)not (x11 x3 x6 x5 x4)not (x11 x3 x7 x5 x3)not (x11 x3 x7 x5 x4)not (x11 x4 x2 x4 x5)not (x11 x4 x2 x7 x2)not (x11 x4 x2 x7 x5)not (x11 x4 x3 x5 x7)not (x11 x4 x4 x5 x7)not (x11 x4 x5 x7 x2)not (x11 x5 x2 x5 x5)not (x11 x5 x2 x5 x7)not (x11 x5 x2 x7 x4)not (x11 x5 x4 x7 x2)not (x11 x5 x6 x5 x7)not (x11 x5 x7 x7 x3)not (x11 x5 x7 x7 x4)not (x11 x5 x7 x7 x6)∀ x12 . x0 x12∀ x13 . x0 x13∀ x14 . x0 x14∀ x15 . x0 x15∀ x16 . x0 x16x11 x5 x7 x5 x12x11 x5 x7 x13 x14x11 x5 x7 x15 x16x11 x5 x12 x13 x14x11 x5 x12 x15 x16x11 x13 x14 x15 x16False
Known 59e95.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 : ι → ο . x8 x2x8 x3x8 x4x8 x5x8 x6x8 x7∀ x9 . x0 x9x8 x9)x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2x1 x3x1 x4x1 x5∀ x8 x9 x10 : ι → ι . x8 x2 = x3x8 x3 = x2x8 x4 = x5x8 x5 = x4x9 x2 = x4x9 x3 = x5x9 x4 = x2x9 x5 = x3x10 x2 = x5x10 x3 = x4x10 x4 = x3x10 x5 = x2∀ x11 : ι → ι → ι → ι → ο . (∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x12 x13))(∀ x12 x13 x14 x15 . x11 x12 x13 x14 x15x11 x14 x15 x12 x13)(∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x7 x7))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x8 x13) x14 (x8 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x9 x13) x14 (x9 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x10 x13) x14 (x10 x15)))(∀ x12 . x0 x12not (x11 x4 x6 x5 x12))(∀ x12 . x0 x12not (x11 x4 x7 x5 x12))(∀ x12 . x0 x12not (x11 x5 x7 x6 x12))(∀ x12 . x0 x12not (x11 x2 x2 x12 x7))(∀ x12 . x0 x12not (x11 x2 x3 x12 x6))(∀ x12 . x0 x12not (x11 x5 x5 x12 x7))not (x11 x2 x2 x3 x5)not (x11 x2 x2 x5 x5)not (x11 x2 x2 x7 x3)not (x11 x2 x3 x7 x2)not (x11 x2 x4 x3 x7)not (x11 x2 x5 x3 x2)not (x11 x2 x5 x5 x2)not (x11 x2 x5 x5 x7)not (x11 x2 x6 x7 x2)not (x11 x2 x6 x7 x5)not (x11 x2 x7 x7 x2)not (x11 x2 x7 x7 x5)not (x11 x3 x2 x5 x2)not (x11 x3 x2 x5 x7)not (x11 x3 x2 x7 x4)not (x11 x3 x3 x3 x7)not (x11 x3 x4 x3 x6)not (x11 x3 x4 x7 x2)not (x11 x3 x5 x5 x7)not (x11 x3 x6 x5 x4)not (x11 x3 x6 x7 x2)not (x11 x3 x7 x5 x3)not (x11 x3 x7 x7 x5)not (x11 x4 x2 x7 x2)not (x11 x4 x2 x7 x5)not (x11 x4 x3 x5 x7)not (x11 x4 x4 x5 x7)not (x11 x4 x5 x7 x2)not (x11 x5 x2 x5 x7)not (x11 x5 x2 x7 x4)not (x11 x5 x4 x7 x2)not (x11 x5 x6 x5 x7)not (x11 x5 x7 x7 x3)not (x11 x5 x7 x7 x4)not (x11 x5 x7 x7 x6)∀ x12 . x0 x12∀ x13 . x0 x13∀ x14 . x0 x14∀ x15 . x0 x15∀ x16 . x0 x16x11 x5 x7 x7 x12x11 x5 x7 x13 x14x11 x5 x7 x15 x16x11 x7 x12 x13 x14x11 x7 x12 x15 x16x11 x13 x14 x15 x16False
Known FalseEFalseE : False∀ x0 : ο . x0
Theorem f1f7a.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 : ι → ο . x8 x2x8 x3x8 x4x8 x5x8 x6x8 x7∀ x9 . x0 x9x8 x9)x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2x1 x3x1 x4x1 x5∀ x8 x9 x10 : ι → ι . x8 x2 = x3x8 x3 = x2x8 x4 = x5x8 x5 = x4x9 x2 = x4x9 x3 = x5x9 x4 = x2x9 x5 = x3x10 x2 = x5x10 x3 = x4x10 x4 = x3x10 x5 = x2∀ x11 : ι → ι → ι → ι → ο . (∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x12 x13))(∀ x12 x13 x14 x15 . x11 x12 x13 x14 x15x11 x14 x15 x12 x13)(∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x7 x7))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x8 x13) x14 (x8 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x9 x13) x14 (x9 x15)))(∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x10 x13) x14 (x10 x15)))(∀ x12 . x0 x12not (x11 x4 x6 x5 x12))(∀ x12 . x0 x12not (x11 x4 x7 x5 x12))(∀ x12 . x0 x12not (x11 x5 x6 x6 x12))(∀ x12 . x0 x12not (x11 x5 x7 x6 x12))(∀ x12 . x0 x12not (x11 x6 x6 x2 x12))(∀ x12 . x0 x12not (x11 x6 x6 x4 x12))(∀ x12 . x0 x12not (x11 x6 x7 x2 x12))(∀ x12 . x0 x12not (x11 x6 x7 x4 x12))(∀ x12 . x0 x12not (x11 x7 x6 x7 x12))(∀ x12 . x0 x12not (x11 x2 x2 x12 x7))(∀ x12 . x0 x12not (x11 x2 x3 x12 x6))(∀ x12 . x0 x12not (x11 x5 x5 x12 x7))(∀ x12 . x0 x12not (x11 x6 x2 x12 x6))(∀ x12 . x0 x12not (x11 x6 x7 x12 x7))not (x11 x2 x2 x2 x5)not (x11 x2 x2 x3 x4)not (x11 x2 x2 x3 x5)not (x11 x2 x2 x4 x2)not (x11 x2 x2 x4 x3)not (x11 x2 x2 x5 x2)not (x11 x2 x2 x5 x5)not (x11 x2 x2 x6 x2)not (x11 x2 x2 x7 x3)not (x11 x2 x2 x7 x6)not (x11 x2 x3 x4 x2)not (x11 x2 x3 x7 x2)not (x11 x2 x4 x2 x6)not (x11 x2 x4 x3 x2)not (x11 x2 x4 x3 x7)not (x11 x2 x4 x5 x6)not (x11 x2 x4 x7 x6)not (x11 x2 x5 x2 x7)not (x11 x2 x5 x3 x2)not (x11 x2 x5 x3 x6)not (x11 x2 x5 x5 x2)not (x11 x2 x5 x5 x7)not (x11 x2 x5 x7 x6)not (x11 x2 x6 x2 x7)not (x11 x2 x6 x3 x2)not (x11 x2 x6 x3 x5)not (x11 x2 x6 x3 x6)not (x11 x2 x6 x3 x7)not (x11 x2 x6 x4 x3)not (x11 x2 x6 x4 x4)not (x11 x2 x6 x5 x3)not (x11 x2 x6 x5 x4)not (x11 x2 x6 x7 x2)not (x11 x2 x6 x7 x3)not (x11 x2 x6 x7 x4)not (x11 x2 x6 x7 x5)not (x11 x2 x7 x3 x3)not (x11 x2 x7 x3 x4)not (x11 x2 x7 x3 x6)not (x11 x2 x7 x3 x7)not (x11 x2 x7 x4 x2)not (x11 x2 x7 x4 x5)not (x11 x2 x7 x5 x2)not (x11 x2 x7 x7 x2)not (x11 x2 x7 x7 x3)not (x11 x2 x7 x7 x4)not (x11 x2 x7 x7 x5)not (x11 x3 x2 x3 x3)not (x11 x3 x2 x3 x5)not (x11 x3 x2 x3 x6)not (x11 x3 x2 x4 x3)not (x11 x3 x2 x4 x4)not (x11 x3 x2 x4 x5)not (x11 x3 x2 x5 x2)not (x11 x3 x2 x5 x7)not (x11 x3 x2 x6 x2)not (x11 x3 x2 x6 x5)not (x11 x3 x2 x6 x6)not (x11 x3 x2 x7 x2)not (x11 x3 x2 x7 x4)not (x11 x3 x2 x7 x5)not (x11 x3 x2 x7 x6)not (x11 x3 x3 x3 x7)not (x11 x3 x3 x4 x2)not (x11 x3 x3 x5 x6)not (x11 x3 x3 x6 x7)not (x11 x3 x3 x7 x6)not (x11 x3 x4 x3 x6)not (x11 x3 x4 x4 x2)not (x11 x3 x4 x5 x6)not (x11 x3 x4 x6 x6)not (x11 x3 x4 x7 x2)not (x11 x3 x4 x7 x6)not (x11 x3 x5 x3 x7)not (x11 x3 x5 x4 x2)not (x11 x3 x5 x5 x7)not (x11 x3 x5 x6 x2)not (x11 x3 x5 x6 x7)not (x11 x3 x5 x7 x2)not (x11 x3 x5 x7 x6)not (x11 x3 x6 x4 x2)not (x11 x3 x6 x4 x4)not (x11 x3 x6 x5 x2)not (x11 x3 x6 x5 x3)not (x11 x3 x6 x5 x4)not (x11 x3 x6 x5 x5)not (x11 x3 x6 x7 x2)not (x11 x3 x6 x7 x4)not (x11 x3 x7 x4 x3)not (x11 x3 x7 x4 x5)not (x11 x3 x7 x5 x2)not (x11 x3 x7 x5 x3)not (x11 x3 x7 x5 x4)not (x11 x3 x7 x7 x3)not (x11 x3 x7 x7 x5)not (x11 x4 x2 x4 x5)not (x11 x4 x2 x5 x2)not (x11 x4 x2 x5 x5)not (x11 x4 x2 x5 x6)not (x11 x4 x2 x6 x2)not (x11 x4 x2 x7 x2)not (x11 x4 x2 x7 x3)not (x11 x4 x2 x7 x5)not (x11 x4 x3 x5 x7)not (x11 x4 x3 x7 x2)not (x11 x4 x4 x5 x7)not (x11 x4 x5 x5 x2)not (x11 x4 x5 x5 x6)not (x11 x4 x5 x7 x2)not (x11 x5 x2 x5 x4)not (x11 x5 x2 x5 x5)not (x11 x5 x2 x5 x7)not (x11 x5 x2 x6 x2)not (x11 x5 x2 x6 x3)not (x11 x5 x2 x6 x5)not (x11 x5 x2 x6 x6)not (x11 x5 x2 x7 x4)not (x11 x5 x2 x7 x5)not (x11 x5 x3 x5 x6)not (x11 x5 x3 x6 x2)not (x11 x5 x3 x6 x7)not (x11 x5 x4 x5 x6)not (x11 x5 x4 x6 x6)not (x11 x5 x4 x7 x2)not (x11 x5 x5 x6 x2)not (x11 x5 x5 x7 x2)not (x11 x5 x6 x5 x7)not (x11 x5 x6 x7 x2)not (x11 x5 x6 x7 x5)not (x11 x5 x6 x7 x6)not (x11 x5 x7 x7 x3)not (x11 x5 x7 x7 x4)not (x11 x5 x7 x7 x6)not (x11 x6 x2 x7 x4)not (x11 x6 x2 x7 x5)not (x11 x6 x3 x7 x6)not (x11 x6 x4 x7 x2)not (x11 x6 x4 x7 x6)not (x11 x6 x5 x7 x2)not (x11 x6 x5 x7 x6)not (x11 x7 x2 x7 x3)∀ x12 . x0 x12∀ x13 . x0 x13∀ x14 . x0 x14∀ x15 . x0 x15∀ x16 . x0 x16∀ x17 . x0 x17∀ x18 . x0 x18x11 x5 x12 x13 x14x11 x5 x12 x15 x16x11 x5 x12 x17 x18x11 x13 x14 x15 x16x11 x13 x14 x17 x18x11 x15 x16 x17 x18False (proof)