Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrNUD../b5a90..
PUQdw../e600d..
vout
PrNUD../92fba.. 0.00 bars
TMNtB../0b8f0.. ownership of 06930.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMP9s../53f73.. ownership of 16140.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUbjb../af7f2.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 06930.. : ∀ x0 : ι → ι → ο . ∀ x1 . ∀ x2 : ι → ο . ∀ x3 : ι → ι → ι . ∀ x4 . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ο . ∀ x7 . ∀ x8 : ι → ο . ∀ x9 . ∀ x10 : ι → ο . ∀ x11 x12 . ∀ x13 : ι → ο . ∀ x14 x15 x16 x17 . ∀ x18 : ι → ο . ∀ x19 x20 x21 x22 . ∀ x23 x24 : ι → ι → ι . ∀ x25 x26 : ι → ι → ι → ι . ∀ x27 x28 : ι → ο . ∀ x29 . ∀ x30 : ι → ι . ∀ x31 : ι → ι → ι . ∀ x32 x33 x34 x35 . ∀ x36 : ι → ο . ∀ x37 . ∀ x38 : ι → ο . ∀ x39 x40 x41 . ∀ x42 : ι → ο . ∀ x43 . ∀ x44 : ι → ι . ∀ x45 . ∀ x46 x47 : ι → ι → ο . ∀ x48 : ι → ι . ∀ x49 . ∀ x50 : ι → ι . ∀ x51 . ∀ x52 : ι → ο . (∀ x53 x54 . x52 x54 ⟶ (x54 = x53 ⟶ False) ⟶ x52 x53 ⟶ False) ⟶ (∀ x53 x54 . x0 x53 x54 ⟶ x52 x54 ⟶ False) ⟶ ((x50 x51 = x49 ⟶ False) ⟶ False) ⟶ (∀ x53 . x52 x53 ⟶ (x53 = x1 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x0 x53 x54 ⟶ x47 x54 (x48 x55) ⟶ x52 x55 ⟶ False) ⟶ (∀ x53 x54 x55 . x0 x54 x55 ⟶ x47 x55 (x48 x53) ⟶ (x47 x54 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x46 x54 x53 ⟶ (x47 x54 (x48 x53) ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x47 x54 (x48 x53) ⟶ (x46 x54 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x47 x53 x54 ⟶ (x52 x54 ⟶ False) ⟶ (x0 x53 x54 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x0 x54 x53 ⟶ (x47 x54 x53 ⟶ False) ⟶ False) ⟶ ((x47 x1 x45 ⟶ False) ⟶ False) ⟶ (∀ x53 . x2 x53 ⟶ (x3 x53 x4 = x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x2 x54 ⟶ x2 x53 ⟶ (x3 (x44 x54) (x44 x53) = x44 (x3 x54 x53) ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x2 x55 ⟶ x2 x53 ⟶ x2 x54 ⟶ (x3 (x3 x55 x53) x54 = x3 x55 (x3 x53 x54) ⟶ False) ⟶ False) ⟶ (∀ x53 . (x46 x53 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . (x52 x55 ⟶ False) ⟶ (x52 x53 ⟶ False) ⟶ x47 x53 (x48 x55) ⟶ x47 x54 x53 ⟶ (x5 x54 x55 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . (x52 x55 ⟶ False) ⟶ (x52 x53 ⟶ False) ⟶ x47 x53 (x48 x55) ⟶ x5 x54 x55 x53 ⟶ (x47 x54 x53 ⟶ False) ⟶ False) ⟶ ((x4 = x1 ⟶ False) ⟶ False) ⟶ ((x43 = x45 ⟶ False) ⟶ False) ⟶ ((x6 x7 ⟶ False) ⟶ False) ⟶ (x52 x7 ⟶ False) ⟶ ((x8 x9 ⟶ False) ⟶ False) ⟶ ((x52 x9 ⟶ False) ⟶ False) ⟶ ((x10 x11 ⟶ False) ⟶ False) ⟶ ((x8 x11 ⟶ False) ⟶ False) ⟶ ((x2 x11 ⟶ False) ⟶ False) ⟶ ((x52 x11 ⟶ False) ⟶ False) ⟶ ((x6 x12 ⟶ False) ⟶ False) ⟶ ((x42 x41 ⟶ False) ⟶ False) ⟶ ((x8 x41 ⟶ False) ⟶ False) ⟶ ((x10 x40 ⟶ False) ⟶ False) ⟶ ((x42 x40 ⟶ False) ⟶ False) ⟶ ((x8 x40 ⟶ False) ⟶ False) ⟶ ((x2 x40 ⟶ False) ⟶ False) ⟶ (x10 x39 ⟶ False) ⟶ ((x42 x39 ⟶ False) ⟶ False) ⟶ ((x8 x39 ⟶ False) ⟶ False) ⟶ ((x13 x14 ⟶ False) ⟶ False) ⟶ ((x8 x14 ⟶ False) ⟶ False) ⟶ ((x10 x15 ⟶ False) ⟶ False) ⟶ ((x13 x15 ⟶ False) ⟶ False) ⟶ ((x8 x15 ⟶ False) ⟶ False) ⟶ ((x2 x15 ⟶ False) ⟶ False) ⟶ ((x2 x16 ⟶ False) ⟶ False) ⟶ (x52 x16 ⟶ False) ⟶ (x52 x17 ⟶ False) ⟶ ((x38 x37 ⟶ False) ⟶ False) ⟶ ((x18 x37 ⟶ False) ⟶ False) ⟶ ((x36 x37 ⟶ False) ⟶ False) ⟶ (x52 x37 ⟶ False) ⟶ (x10 x35 ⟶ False) ⟶ ((x13 x35 ⟶ False) ⟶ False) ⟶ ((x8 x35 ⟶ False) ⟶ False) ⟶ ((x8 x19 ⟶ False) ⟶ False) ⟶ ((x10 x34 ⟶ False) ⟶ False) ⟶ ((x2 x20 ⟶ False) ⟶ False) ⟶ ((x52 x33 ⟶ False) ⟶ False) ⟶ ((x10 x21 ⟶ False) ⟶ False) ⟶ ((x13 x21 ⟶ False) ⟶ False) ⟶ ((x8 x21 ⟶ False) ⟶ False) ⟶ ((x2 x21 ⟶ False) ⟶ False) ⟶ ((x47 x21 x22 ⟶ False) ⟶ False) ⟶ ((x38 x32 ⟶ False) ⟶ False) ⟶ (∀ x53 . x2 x53 ⟶ (x44 (x44 x53) = x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x8 x53 ⟶ (x50 (x50 x53) = x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x10 x54 ⟶ x2 x53 ⟶ x54 = x53 ⟶ (x50 x54 = x44 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 x56 . x10 x56 ⟶ x10 x53 ⟶ x2 x55 ⟶ x2 x54 ⟶ x56 = x55 ⟶ x53 = x54 ⟶ (x31 x56 x53 = x3 x55 x54 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . (x42 x54 ⟶ False) ⟶ x10 x54 ⟶ (x42 x53 ⟶ False) ⟶ x10 x53 ⟶ x42 (x3 x54 x53) ⟶ False) ⟶ (∀ x53 x54 . x8 x54 ⟶ x42 x54 ⟶ (x10 x54 ⟶ False) ⟶ x8 x53 ⟶ x13 x53 ⟶ (x10 x53 ⟶ False) ⟶ (x8 (x31 x54 x53) ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x8 x54 ⟶ x42 x54 ⟶ (x10 x54 ⟶ False) ⟶ x8 x53 ⟶ x13 x53 ⟶ (x10 x53 ⟶ False) ⟶ (x52 (x31 x54 x53) ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x8 x54 ⟶ x42 x54 ⟶ (x10 x54 ⟶ False) ⟶ x8 x53 ⟶ x42 x53 ⟶ (x10 x53 ⟶ False) ⟶ x10 (x31 x54 x53) ⟶ False) ⟶ (∀ x53 x54 . x8 x54 ⟶ x42 x54 ⟶ (x10 x54 ⟶ False) ⟶ x8 x53 ⟶ x42 x53 ⟶ (x10 x53 ⟶ False) ⟶ (x8 (x31 x54 x53) ⟶ False) ⟶ False) ⟶ (∀ x53 . (x52 x53 ⟶ False) ⟶ x2 x53 ⟶ (x2 (x44 x53) ⟶ False) ⟶ False) ⟶ (∀ x53 . (x52 x53 ⟶ False) ⟶ x2 x53 ⟶ x52 (x44 x53) ⟶ False) ⟶ ((x38 x45 ⟶ False) ⟶ False) ⟶ (x52 x45 ⟶ False) ⟶ (∀ x53 x54 . x8 x54 ⟶ x13 x54 ⟶ (x10 x54 ⟶ False) ⟶ x8 x53 ⟶ x13 x53 ⟶ (x10 x53 ⟶ False) ⟶ x10 (x31 x54 x53) ⟶ False) ⟶ (∀ x53 x54 . x8 x54 ⟶ x13 x54 ⟶ (x10 x54 ⟶ False) ⟶ x8 x53 ⟶ x13 x53 ⟶ (x10 x53 ⟶ False) ⟶ (x8 (x31 x54 x53) ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x10 x54 ⟶ x10 x53 ⟶ (x10 (x3 x54 x53) ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x10 x54 ⟶ x8 x53 ⟶ (x10 x53 ⟶ False) ⟶ x10 (x31 x54 x53) ⟶ False) ⟶ ((x42 x49 ⟶ False) ⟶ False) ⟶ ((x13 x51 ⟶ False) ⟶ False) ⟶ (∀ x53 . x10 x53 ⟶ (x10 (x44 x53) ⟶ False) ⟶ False) ⟶ (∀ x53 . x10 x53 ⟶ (x2 (x44 x53) ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x10 x54 ⟶ x10 x53 ⟶ (x10 (x31 x54 x53) ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x10 x54 ⟶ x10 x53 ⟶ (x8 (x31 x54 x53) ⟶ False) ⟶ False) ⟶ ((x8 x49 ⟶ False) ⟶ False) ⟶ (x10 x51 ⟶ False) ⟶ (∀ x53 x54 . x2 x54 ⟶ x2 x53 ⟶ (x2 (x3 x54 x53) ⟶ False) ⟶ False) ⟶ (∀ x53 . x10 x53 ⟶ (x10 (x50 x53) ⟶ False) ⟶ False) ⟶ (∀ x53 . x10 x53 ⟶ (x8 (x50 x53) ⟶ False) ⟶ False) ⟶ ((x8 x51 ⟶ False) ⟶ False) ⟶ (x10 x49 ⟶ False) ⟶ ((x52 x1 ⟶ False) ⟶ False) ⟶ (∀ x53 . (x42 x53 ⟶ False) ⟶ x10 x53 ⟶ x13 (x44 x53) ⟶ False) ⟶ (∀ x53 . (x42 x53 ⟶ False) ⟶ x10 x53 ⟶ (x2 (x44 x53) ⟶ False) ⟶ False) ⟶ (∀ x53 . (x13 x53 ⟶ False) ⟶ x10 x53 ⟶ x42 (x44 x53) ⟶ False) ⟶ (∀ x53 . (x13 x53 ⟶ False) ⟶ x10 x53 ⟶ (x2 (x44 x53) ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x42 x54 ⟶ x10 x54 ⟶ (x13 x53 ⟶ False) ⟶ x10 x53 ⟶ (x42 (x3 x53 x54) ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x42 x54 ⟶ x10 x54 ⟶ (x13 x53 ⟶ False) ⟶ x10 x53 ⟶ (x42 (x3 x54 x53) ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x13 x54 ⟶ x10 x54 ⟶ (x42 x53 ⟶ False) ⟶ x10 x53 ⟶ (x13 (x3 x53 x54) ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x13 x54 ⟶ x10 x54 ⟶ (x42 x53 ⟶ False) ⟶ x10 x53 ⟶ (x13 (x3 x54 x53) ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . (x13 x54 ⟶ False) ⟶ x10 x54 ⟶ (x13 x53 ⟶ False) ⟶ x10 x53 ⟶ x13 (x3 x54 x53) ⟶ False) ⟶ (∀ x53 x54 . (x52 x54 ⟶ False) ⟶ (x52 x53 ⟶ False) ⟶ x47 x53 (x48 x54) ⟶ (x5 (x23 x53 x54) x54 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . (x47 (x30 x53) x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . (x52 x55 ⟶ False) ⟶ (x52 x53 ⟶ False) ⟶ x47 x53 (x48 x55) ⟶ x5 x54 x55 x53 ⟶ (x47 x54 x55 ⟶ False) ⟶ False) ⟶ ((x5 x4 x22 x43 ⟶ False) ⟶ False) ⟶ ((x47 x43 (x48 x22) ⟶ False) ⟶ False) ⟶ (∀ x53 . x2 x53 ⟶ (x2 (x44 x53) ⟶ False) ⟶ False) ⟶ (∀ x53 . x8 x53 ⟶ (x8 (x50 x53) ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x8 x54 ⟶ x8 x53 ⟶ (x8 (x31 x54 x53) ⟶ False) ⟶ False) ⟶ ((x49 = x24 x4 x22 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x53 ⟶ False) ⟶ x53 = x49 ⟶ x55 = x49 ⟶ x53 = x51 ⟶ x55 = x51 ⟶ x54 = x4 ⟶ (x54 = x31 x55 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x53 ⟶ False) ⟶ x53 = x49 ⟶ x55 = x49 ⟶ x53 = x51 ⟶ x55 = x51 ⟶ x54 = x31 x55 x53 ⟶ (x54 = x4 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x53 ⟶ False) ⟶ x53 = x49 ⟶ x55 = x49 ⟶ x53 = x51 ⟶ (x53 = x49 ⟶ False) ⟶ x54 = x4 ⟶ (x54 = x31 x55 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x53 ⟶ False) ⟶ x53 = x49 ⟶ x55 = x49 ⟶ x53 = x51 ⟶ (x53 = x49 ⟶ False) ⟶ x54 = x31 x55 x53 ⟶ (x54 = x4 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x53 ⟶ False) ⟶ x53 = x49 ⟶ x55 = x49 ⟶ (x55 = x49 ⟶ False) ⟶ x55 = x51 ⟶ x54 = x4 ⟶ (x54 = x31 x55 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x53 ⟶ False) ⟶ x53 = x49 ⟶ x55 = x49 ⟶ (x55 = x49 ⟶ False) ⟶ x55 = x51 ⟶ x54 = x31 x55 x53 ⟶ (x54 = x4 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x53 ⟶ False) ⟶ x53 = x49 ⟶ x55 = x49 ⟶ (x55 = x49 ⟶ False) ⟶ (x53 = x49 ⟶ False) ⟶ x54 = x4 ⟶ (x54 = x31 x55 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x53 ⟶ False) ⟶ x53 = x49 ⟶ x55 = x49 ⟶ (x55 = x49 ⟶ False) ⟶ (x53 = x49 ⟶ False) ⟶ x54 = x31 x55 x53 ⟶ (x54 = x4 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x53 ⟶ False) ⟶ x53 = x49 ⟶ (x53 = x51 ⟶ False) ⟶ x53 = x51 ⟶ x55 = x51 ⟶ x54 = x4 ⟶ (x54 = x31 x55 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x53 ⟶ False) ⟶ x53 = x49 ⟶ (x53 = x51 ⟶ False) ⟶ x53 = x51 ⟶ x55 = x51 ⟶ x54 = x31 x55 x53 ⟶ (x54 = x4 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x53 ⟶ False) ⟶ x53 = x49 ⟶ (x53 = x51 ⟶ False) ⟶ x53 = x51 ⟶ (x53 = x49 ⟶ False) ⟶ x54 = x4 ⟶ (x54 = x31 x55 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x53 ⟶ False) ⟶ x53 = x49 ⟶ (x53 = x51 ⟶ False) ⟶ x53 = x51 ⟶ (x53 = x49 ⟶ False) ⟶ x54 = x31 x55 x53 ⟶ (x54 = x4 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x53 ⟶ False) ⟶ x53 = x49 ⟶ (x53 = x51 ⟶ False) ⟶ (x55 = x49 ⟶ False) ⟶ x55 = x51 ⟶ x54 = x4 ⟶ (x54 = x31 x55 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x53 ⟶ False) ⟶ x53 = x49 ⟶ (x53 = x51 ⟶ False) ⟶ (x55 = x49 ⟶ False) ⟶ x55 = x51 ⟶ x54 = x31 x55 x53 ⟶ (x54 = x4 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x53 ⟶ False) ⟶ x53 = x49 ⟶ (x53 = x51 ⟶ False) ⟶ (x55 = x49 ⟶ False) ⟶ (x53 = x49 ⟶ False) ⟶ x54 = x4 ⟶ (x54 = x31 x55 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x53 ⟶ False) ⟶ x53 = x49 ⟶ (x53 = x51 ⟶ False) ⟶ (x55 = x49 ⟶ False) ⟶ (x53 = x49 ⟶ False) ⟶ x54 = x31 x55 x53 ⟶ (x54 = x4 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x53 ⟶ False) ⟶ (x55 = x51 ⟶ False) ⟶ x55 = x49 ⟶ x53 = x51 ⟶ x55 = x51 ⟶ x54 = x4 ⟶ (x54 = x31 x55 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x53 ⟶ False) ⟶ (x55 = x51 ⟶ False) ⟶ x55 = x49 ⟶ x53 = x51 ⟶ x55 = x51 ⟶ x54 = x31 x55 x53 ⟶ (x54 = x4 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x53 ⟶ False) ⟶ (x55 = x51 ⟶ False) ⟶ x55 = x49 ⟶ x53 = x51 ⟶ (x53 = x49 ⟶ False) ⟶ x54 = x4 ⟶ (x54 = x31 x55 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x53 ⟶ False) ⟶ (x55 = x51 ⟶ False) ⟶ x55 = x49 ⟶ x53 = x51 ⟶ (x53 = x49 ⟶ False) ⟶ x54 = x31 x55 x53 ⟶ (x54 = x4 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x53 ⟶ False) ⟶ (x55 = x51 ⟶ False) ⟶ x55 = x49 ⟶ (x55 = x49 ⟶ False) ⟶ x55 = x51 ⟶ x54 = x4 ⟶ (x54 = x31 x55 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x53 ⟶ False) ⟶ (x55 = x51 ⟶ False) ⟶ x55 = x49 ⟶ (x55 = x49 ⟶ False) ⟶ x55 = x51 ⟶ x54 = x31 x55 x53 ⟶ (x54 = x4 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x53 ⟶ False) ⟶ (x55 = x51 ⟶ False) ⟶ x55 = x49 ⟶ (x55 = x49 ⟶ False) ⟶ (x53 = x49 ⟶ False) ⟶ x54 = x4 ⟶ (x54 = x31 x55 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x53 ⟶ False) ⟶ (x55 = x51 ⟶ False) ⟶ x55 = x49 ⟶ (x55 = x49 ⟶ False) ⟶ (x53 = x49 ⟶ False) ⟶ x54 = x31 x55 x53 ⟶ (x54 = x4 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x53 ⟶ False) ⟶ (x55 = x51 ⟶ False) ⟶ (x53 = x51 ⟶ False) ⟶ x53 = x51 ⟶ x55 = x51 ⟶ x54 = x4 ⟶ (x54 = x31 x55 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x53 ⟶ False) ⟶ (x55 = x51 ⟶ False) ⟶ (x53 = x51 ⟶ False) ⟶ x53 = x51 ⟶ x55 = x51 ⟶ x54 = x31 x55 x53 ⟶ (x54 = x4 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x53 ⟶ False) ⟶ (x55 = x51 ⟶ False) ⟶ (x53 = x51 ⟶ False) ⟶ x53 = x51 ⟶ (x53 = x49 ⟶ False) ⟶ x54 = x4 ⟶ (x54 = x31 x55 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x53 ⟶ False) ⟶ (x55 = x51 ⟶ False) ⟶ (x53 = x51 ⟶ False) ⟶ x53 = x51 ⟶ (x53 = x49 ⟶ False) ⟶ x54 = x31 x55 x53 ⟶ (x54 = x4 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x53 ⟶ False) ⟶ (x55 = x51 ⟶ False) ⟶ (x53 = x51 ⟶ False) ⟶ (x55 = x49 ⟶ False) ⟶ x55 = x51 ⟶ x54 = x4 ⟶ (x54 = x31 x55 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x53 ⟶ False) ⟶ (x55 = x51 ⟶ False) ⟶ (x53 = x51 ⟶ False) ⟶ (x55 = x49 ⟶ False) ⟶ x55 = x51 ⟶ x54 = x31 x55 x53 ⟶ (x54 = x4 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x53 ⟶ False) ⟶ (x55 = x51 ⟶ False) ⟶ (x53 = x51 ⟶ False) ⟶ (x55 = x49 ⟶ False) ⟶ (x53 = x49 ⟶ False) ⟶ x54 = x4 ⟶ (x54 = x31 x55 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x53 ⟶ False) ⟶ (x55 = x51 ⟶ False) ⟶ (x53 = x51 ⟶ False) ⟶ (x55 = x49 ⟶ False) ⟶ (x53 = x49 ⟶ False) ⟶ x54 = x31 x55 x53 ⟶ (x54 = x4 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x55 ⟶ False) ⟶ x53 = x49 ⟶ x55 = x49 ⟶ x53 = x51 ⟶ x55 = x51 ⟶ x54 = x4 ⟶ (x54 = x31 x55 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x55 ⟶ False) ⟶ x53 = x49 ⟶ x55 = x49 ⟶ x53 = x51 ⟶ x55 = x51 ⟶ x54 = x31 x55 x53 ⟶ (x54 = x4 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x55 ⟶ False) ⟶ x53 = x49 ⟶ x55 = x49 ⟶ x53 = x51 ⟶ (x53 = x49 ⟶ False) ⟶ x54 = x4 ⟶ (x54 = x31 x55 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x55 ⟶ False) ⟶ x53 = x49 ⟶ x55 = x49 ⟶ x53 = x51 ⟶ (x53 = x49 ⟶ False) ⟶ x54 = x31 x55 x53 ⟶ (x54 = x4 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x55 ⟶ False) ⟶ x53 = x49 ⟶ x55 = x49 ⟶ (x55 = x49 ⟶ False) ⟶ x55 = x51 ⟶ x54 = x4 ⟶ (x54 = x31 x55 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x55 ⟶ False) ⟶ x53 = x49 ⟶ x55 = x49 ⟶ (x55 = x49 ⟶ False) ⟶ x55 = x51 ⟶ x54 = x31 x55 x53 ⟶ (x54 = x4 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x55 ⟶ False) ⟶ x53 = x49 ⟶ x55 = x49 ⟶ (x55 = x49 ⟶ False) ⟶ (x53 = x49 ⟶ False) ⟶ x54 = x4 ⟶ (x54 = x31 x55 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x55 ⟶ False) ⟶ x53 = x49 ⟶ x55 = x49 ⟶ (x55 = x49 ⟶ False) ⟶ (x53 = x49 ⟶ False) ⟶ x54 = x31 x55 x53 ⟶ (x54 = x4 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x55 ⟶ False) ⟶ x53 = x49 ⟶ (x53 = x51 ⟶ False) ⟶ x53 = x51 ⟶ x55 = x51 ⟶ x54 = x4 ⟶ (x54 = x31 x55 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x55 ⟶ False) ⟶ x53 = x49 ⟶ (x53 = x51 ⟶ False) ⟶ x53 = x51 ⟶ x55 = x51 ⟶ x54 = x31 x55 x53 ⟶ (x54 = x4 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x55 ⟶ False) ⟶ x53 = x49 ⟶ (x53 = x51 ⟶ False) ⟶ x53 = x51 ⟶ (x53 = x49 ⟶ False) ⟶ x54 = x4 ⟶ (x54 = x31 x55 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x55 ⟶ False) ⟶ x53 = x49 ⟶ (x53 = x51 ⟶ False) ⟶ x53 = x51 ⟶ (x53 = x49 ⟶ False) ⟶ x54 = x31 x55 x53 ⟶ (x54 = x4 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x55 ⟶ False) ⟶ x53 = x49 ⟶ (x53 = x51 ⟶ False) ⟶ (x55 = x49 ⟶ False) ⟶ x55 = x51 ⟶ x54 = x4 ⟶ (x54 = x31 x55 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x55 ⟶ False) ⟶ x53 = x49 ⟶ (x53 = x51 ⟶ False) ⟶ (x55 = x49 ⟶ False) ⟶ x55 = x51 ⟶ x54 = x31 x55 x53 ⟶ (x54 = x4 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x55 ⟶ False) ⟶ x53 = x49 ⟶ (x53 = x51 ⟶ False) ⟶ (x55 = x49 ⟶ False) ⟶ (x53 = x49 ⟶ False) ⟶ x54 = x4 ⟶ (x54 = x31 x55 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x55 ⟶ False) ⟶ x53 = x49 ⟶ (x53 = x51 ⟶ False) ⟶ (x55 = x49 ⟶ False) ⟶ (x53 = x49 ⟶ False) ⟶ x54 = x31 x55 x53 ⟶ (x54 = x4 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x55 ⟶ False) ⟶ (x55 = x51 ⟶ False) ⟶ x55 = x49 ⟶ x53 = x51 ⟶ x55 = x51 ⟶ x54 = x4 ⟶ (x54 = x31 x55 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x55 ⟶ False) ⟶ (x55 = x51 ⟶ False) ⟶ x55 = x49 ⟶ x53 = x51 ⟶ x55 = x51 ⟶ x54 = x31 x55 x53 ⟶ (x54 = x4 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x55 ⟶ False) ⟶ (x55 = x51 ⟶ False) ⟶ x55 = x49 ⟶ x53 = x51 ⟶ (x53 = x49 ⟶ False) ⟶ x54 = x4 ⟶ (x54 = x31 x55 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x55 ⟶ False) ⟶ (x55 = x51 ⟶ False) ⟶ x55 = x49 ⟶ x53 = x51 ⟶ (x53 = x49 ⟶ False) ⟶ x54 = x31 x55 x53 ⟶ (x54 = x4 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x55 ⟶ False) ⟶ (x55 = x51 ⟶ False) ⟶ x55 = x49 ⟶ (x55 = x49 ⟶ False) ⟶ x55 = x51 ⟶ x54 = x4 ⟶ (x54 = x31 x55 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x55 ⟶ False) ⟶ (x55 = x51 ⟶ False) ⟶ x55 = x49 ⟶ (x55 = x49 ⟶ False) ⟶ x55 = x51 ⟶ x54 = x31 x55 x53 ⟶ (x54 = x4 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x55 ⟶ False) ⟶ (x55 = x51 ⟶ False) ⟶ x55 = x49 ⟶ (x55 = x49 ⟶ False) ⟶ (x53 = x49 ⟶ False) ⟶ x54 = x4 ⟶ (x54 = x31 x55 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x55 ⟶ False) ⟶ (x55 = x51 ⟶ False) ⟶ x55 = x49 ⟶ (x55 = x49 ⟶ False) ⟶ (x53 = x49 ⟶ False) ⟶ x54 = x31 x55 x53 ⟶ (x54 = x4 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x55 ⟶ False) ⟶ (x55 = x51 ⟶ False) ⟶ (x53 = x51 ⟶ False) ⟶ x53 = x51 ⟶ x55 = x51 ⟶ x54 = x4 ⟶ (x54 = x31 x55 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x55 ⟶ False) ⟶ (x55 = x51 ⟶ False) ⟶ (x53 = x51 ⟶ False) ⟶ x53 = x51 ⟶ x55 = x51 ⟶ x54 = x31 x55 x53 ⟶ (x54 = x4 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x55 ⟶ False) ⟶ (x55 = x51 ⟶ False) ⟶ (x53 = x51 ⟶ False) ⟶ x53 = x51 ⟶ (x53 = x49 ⟶ False) ⟶ x54 = x4 ⟶ (x54 = x31 x55 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x55 ⟶ False) ⟶ (x55 = x51 ⟶ False) ⟶ (x53 = x51 ⟶ False) ⟶ x53 = x51 ⟶ (x53 = x49 ⟶ False) ⟶ x54 = x31 x55 x53 ⟶ (x54 = x4 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x55 ⟶ False) ⟶ (x55 = x51 ⟶ False) ⟶ (x53 = x51 ⟶ False) ⟶ (x55 = x49 ⟶ False) ⟶ x55 = x51 ⟶ x54 = x4 ⟶ (x54 = x31 x55 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x55 ⟶ False) ⟶ (x55 = x51 ⟶ False) ⟶ (x53 = x51 ⟶ False) ⟶ (x55 = x49 ⟶ False) ⟶ x55 = x51 ⟶ x54 = x31 x55 x53 ⟶ (x54 = x4 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x55 ⟶ False) ⟶ (x55 = x51 ⟶ False) ⟶ (x53 = x51 ⟶ False) ⟶ (x55 = x49 ⟶ False) ⟶ (x53 = x49 ⟶ False) ⟶ x54 = x4 ⟶ (x54 = x31 x55 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ (x10 x55 ⟶ False) ⟶ (x55 = x51 ⟶ False) ⟶ (x53 = x51 ⟶ False) ⟶ (x55 = x49 ⟶ False) ⟶ (x53 = x49 ⟶ False) ⟶ x54 = x31 x55 x53 ⟶ (x54 = x4 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ x53 = x49 ⟶ (x55 = x51 ⟶ False) ⟶ x54 = x49 ⟶ (x54 = x31 x55 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ x53 = x49 ⟶ (x55 = x51 ⟶ False) ⟶ x54 = x31 x55 x53 ⟶ (x54 = x49 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ x55 = x49 ⟶ (x53 = x51 ⟶ False) ⟶ x54 = x49 ⟶ (x54 = x31 x55 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ x55 = x49 ⟶ (x53 = x51 ⟶ False) ⟶ x54 = x31 x55 x53 ⟶ (x54 = x49 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ x53 = x51 ⟶ (x55 = x49 ⟶ False) ⟶ x54 = x51 ⟶ (x54 = x31 x55 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ x53 = x51 ⟶ (x55 = x49 ⟶ False) ⟶ x54 = x31 x55 x53 ⟶ (x54 = x51 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ x55 = x51 ⟶ (x53 = x49 ⟶ False) ⟶ x54 = x51 ⟶ (x54 = x31 x55 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ x55 = x51 ⟶ (x53 = x49 ⟶ False) ⟶ x54 = x31 x55 x53 ⟶ (x54 = x51 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 x56 x57 . x8 x57 ⟶ x8 x53 ⟶ x8 x56 ⟶ x10 x57 ⟶ x10 x53 ⟶ x2 x54 ⟶ x2 x55 ⟶ x57 = x54 ⟶ x53 = x55 ⟶ x56 = x3 x54 x55 ⟶ (x56 = x31 x57 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ x10 x55 ⟶ x10 x53 ⟶ x54 = x31 x55 x53 ⟶ (x54 = x3 (x26 x54 x53 x55) (x25 x54 x53 x55) ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ x10 x55 ⟶ x10 x53 ⟶ x54 = x31 x55 x53 ⟶ (x53 = x25 x54 x53 x55 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ x10 x55 ⟶ x10 x53 ⟶ x54 = x31 x55 x53 ⟶ (x55 = x26 x54 x53 x55 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ x10 x55 ⟶ x10 x53 ⟶ x54 = x31 x55 x53 ⟶ (x2 (x25 x54 x53 x55) ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x8 x55 ⟶ x8 x53 ⟶ x8 x54 ⟶ x10 x55 ⟶ x10 x53 ⟶ x54 = x31 x55 x53 ⟶ (x2 (x26 x54 x53 x55) ⟶ False) ⟶ False) ⟶ ((x51 = x22 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x2 x54 ⟶ x2 x53 ⟶ (x3 x54 x53 = x3 x53 x54 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x8 x54 ⟶ x8 x53 ⟶ (x31 x54 x53 = x31 x53 x54 ⟶ False) ⟶ False) ⟶ (∀ x53 . x52 x53 ⟶ (x27 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x8 x53 ⟶ (x13 x53 ⟶ False) ⟶ (x42 x53 ⟶ False) ⟶ (x8 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x8 x53 ⟶ (x13 x53 ⟶ False) ⟶ (x42 x53 ⟶ False) ⟶ (x52 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x47 x53 x45 ⟶ (x6 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x52 x53 ⟶ x8 x53 ⟶ x42 x53 ⟶ False) ⟶ (∀ x53 . x52 x53 ⟶ x8 x53 ⟶ x13 x53 ⟶ False) ⟶ (∀ x53 . x52 x53 ⟶ x8 x53 ⟶ (x8 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x52 x53 ⟶ (x6 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . (x52 x53 ⟶ False) ⟶ x8 x53 ⟶ (x13 x53 ⟶ False) ⟶ (x42 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . (x52 x53 ⟶ False) ⟶ x8 x53 ⟶ (x13 x53 ⟶ False) ⟶ (x8 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x6 x53 ⟶ (x38 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x8 x53 ⟶ x42 x53 ⟶ x13 x53 ⟶ False) ⟶ (∀ x53 . x8 x53 ⟶ x42 x53 ⟶ (x8 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x8 x53 ⟶ x42 x53 ⟶ x52 x53 ⟶ False) ⟶ (∀ x53 x54 . x38 x54 ⟶ x47 x53 x54 ⟶ (x38 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . (x52 x53 ⟶ False) ⟶ x8 x53 ⟶ (x42 x53 ⟶ False) ⟶ (x13 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . (x52 x53 ⟶ False) ⟶ x8 x53 ⟶ (x42 x53 ⟶ False) ⟶ (x8 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x10 x53 ⟶ (x8 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x52 x53 ⟶ (x28 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x8 x53 ⟶ x13 x53 ⟶ x42 x53 ⟶ False) ⟶ (∀ x53 . x8 x53 ⟶ x13 x53 ⟶ (x8 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x8 x53 ⟶ x13 x53 ⟶ x52 x53 ⟶ False) ⟶ (∀ x53 . x10 x53 ⟶ (x2 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x52 x53 ⟶ (x38 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x8 x53 ⟶ (x13 x53 ⟶ False) ⟶ (x10 x53 ⟶ False) ⟶ (x42 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x8 x53 ⟶ (x13 x53 ⟶ False) ⟶ (x10 x53 ⟶ False) ⟶ (x8 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x6 x53 ⟶ (x8 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x6 x53 ⟶ (x10 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x6 x53 ⟶ (x2 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x36 x53 ⟶ x18 x53 ⟶ (x38 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x8 x53 ⟶ (x42 x53 ⟶ False) ⟶ (x10 x53 ⟶ False) ⟶ (x13 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x8 x53 ⟶ (x42 x53 ⟶ False) ⟶ (x10 x53 ⟶ False) ⟶ (x8 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x47 x53 x22 ⟶ (x10 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x47 x53 x22 ⟶ (x2 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x47 x53 x22 ⟶ (x10 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x38 x53 ⟶ (x18 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x38 x53 ⟶ (x36 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x27 x54 ⟶ x47 x53 (x48 x54) ⟶ (x27 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x0 x53 x54 ⟶ x0 x54 x53 ⟶ False) ⟶ (x50 (x31 x29 x51) = x31 (x50 x51) (x50 x29) ⟶ False) ⟶ ((x0 x29 x22 ⟶ False) ⟶ False) ⟶ ((x8 x29 ⟶ False) ⟶ False) ⟶ False (proof)