Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../96df6..
PUcC8../1994f..
vout
PrPhD../35d67.. 3.40 bars
TMbT7../00b70.. ownership of 73cf8.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMHZn../9848e.. ownership of ca8ef.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUWKb../27237.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 73cf8.. : ∀ 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 x54 ⟶ x0 x53 ⟶ (x2 x54 = x1 ⟶ False) ⟶ (x2 x53 = x1 ⟶ False) ⟶ (x7 (x8 x54 x53) = x6 (x8 (x7 x54) (x7 x53)) (x3 x5 (x4 (x7 x54) (x7 x53))) ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x51 x53 x54 ⟶ x52 x54 ⟶ False) ⟶ (∀ x53 . x52 x53 ⟶ (x53 = x9 ⟶ False) ⟶ False) ⟶ (∀ x53 . x50 x53 ⟶ (x6 x53 x5 = x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x51 x53 x54 ⟶ x11 x54 (x10 x55) ⟶ x52 x55 ⟶ False) ⟶ (∀ x53 . x50 x53 ⟶ (x6 x1 x53 = x1 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x51 x54 x55 ⟶ x11 x55 (x10 x53) ⟶ (x11 x54 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x50 x53 ⟶ (x3 x53 x1 = x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x12 x54 x53 ⟶ (x11 x54 (x10 x53) ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x11 x54 (x10 x53) ⟶ (x12 x54 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x50 x53 ⟶ (x4 x5 x53 = x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x11 x53 x54 ⟶ (x52 x54 ⟶ False) ⟶ (x51 x53 x54 ⟶ False) ⟶ False) ⟶ (∀ x53 . x50 x53 ⟶ (x4 x53 x1 = x1 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x51 x54 x53 ⟶ (x11 x54 x53 ⟶ False) ⟶ False) ⟶ ((x11 x9 x13 ⟶ False) ⟶ False) ⟶ (∀ x53 . x50 x53 ⟶ (x8 x53 x1 = x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x50 x54 ⟶ x50 x53 ⟶ (x3 (x14 x54) (x14 x53) = x3 x53 x54 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x50 x54 ⟶ x50 x53 ⟶ (x8 (x14 x54) (x14 x53) = x14 (x8 x54 x53) ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x50 x55 ⟶ x50 x53 ⟶ x50 x54 ⟶ (x4 (x4 x55 x53) x54 = x4 x55 (x4 x53 x54) ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x50 x55 ⟶ x50 x53 ⟶ x50 x54 ⟶ (x8 (x8 x55 x53) x54 = x8 x55 (x8 x53 x54) ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x50 x55 ⟶ x50 x53 ⟶ x50 x54 ⟶ (x4 (x8 x55 x53) x54 = x8 (x4 x55 x54) (x4 x53 x54) ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . x50 x55 ⟶ x50 x53 ⟶ x50 x54 ⟶ (x4 x55 (x6 x53 x54) = x6 (x4 x55 x53) x54 ⟶ False) ⟶ False) ⟶ ((x11 x16 x15 ⟶ False) ⟶ False) ⟶ ((x11 x16 x49 ⟶ False) ⟶ False) ⟶ ((x17 x16 x15 x49 ⟶ False) ⟶ False) ⟶ ((x48 x16 ⟶ False) ⟶ False) ⟶ (x52 x16 ⟶ False) ⟶ (∀ x53 . x50 x53 ⟶ (x4 x53 (x14 x5) = x14 x53 ⟶ False) ⟶ False) ⟶ ((x11 x5 x15 ⟶ False) ⟶ False) ⟶ ((x11 x5 x49 ⟶ False) ⟶ False) ⟶ ((x17 x5 x15 x49 ⟶ False) ⟶ False) ⟶ ((x48 x5 ⟶ False) ⟶ False) ⟶ (x52 x5 ⟶ False) ⟶ (∀ x53 x54 . x50 x54 ⟶ x50 x53 ⟶ (x8 x54 (x14 x53) = x3 x54 x53 ⟶ False) ⟶ False) ⟶ ((x11 x18 x15 ⟶ False) ⟶ False) ⟶ ((x11 x18 x49 ⟶ False) ⟶ False) ⟶ ((x17 x18 x15 x49 ⟶ False) ⟶ False) ⟶ ((x52 x18 ⟶ False) ⟶ False) ⟶ ((x14 (x6 (x14 x5) x16) = x6 x5 x16 ⟶ False) ⟶ False) ⟶ ((x14 (x6 x5 x16) = x6 (x14 x5) x16 ⟶ False) ⟶ False) ⟶ ((x14 (x14 x16) = x16 ⟶ False) ⟶ False) ⟶ ((x14 (x14 x5) = x5 ⟶ False) ⟶ False) ⟶ ((x14 x16 = x14 x16 ⟶ False) ⟶ False) ⟶ ((x14 x5 = x14 x5 ⟶ False) ⟶ False) ⟶ ((x14 x18 = x18 ⟶ False) ⟶ False) ⟶ ((x4 (x6 (x14 x5) x16) (x14 x16) = x5 ⟶ False) ⟶ False) ⟶ ((x4 (x6 (x14 x5) x16) x16 = x14 x5 ⟶ False) ⟶ False) ⟶ ((x4 (x6 (x14 x5) x16) x5 = x6 (x14 x5) x16 ⟶ False) ⟶ False) ⟶ ((x4 (x6 x5 x16) (x14 x16) = x14 x5 ⟶ False) ⟶ False) ⟶ ((x4 (x6 x5 x16) x16 = x5 ⟶ False) ⟶ False) ⟶ ((x4 (x6 x5 x16) x5 = x6 x5 x16 ⟶ False) ⟶ False) ⟶ ((x4 (x6 x5 x16) x18 = x18 ⟶ False) ⟶ False) ⟶ ((x4 (x14 x16) (x6 (x14 x5) x16) = x5 ⟶ False) ⟶ False) ⟶ ((x4 (x14 x16) (x6 x5 x16) = x14 x5 ⟶ False) ⟶ False) ⟶ ((x4 (x14 x16) x5 = x14 x16 ⟶ False) ⟶ False) ⟶ ((x4 (x14 x16) x18 = x18 ⟶ False) ⟶ False) ⟶ ((x4 x16 (x6 (x14 x5) x16) = x14 x5 ⟶ False) ⟶ False) ⟶ ((x4 x16 (x6 x5 x16) = x5 ⟶ False) ⟶ False) ⟶ ((x4 x16 x5 = x16 ⟶ False) ⟶ False) ⟶ ((x4 x16 x18 = x18 ⟶ False) ⟶ False) ⟶ ((x4 x5 (x6 (x14 x5) x16) = x6 (x14 x5) x16 ⟶ False) ⟶ False) ⟶ ((x4 x5 (x6 x5 x16) = x6 x5 x16 ⟶ False) ⟶ False) ⟶ ((x4 x5 (x14 x16) = x14 x16 ⟶ False) ⟶ False) ⟶ ((x4 x5 x16 = x16 ⟶ False) ⟶ False) ⟶ ((x4 x5 x5 = x5 ⟶ False) ⟶ False) ⟶ ((x4 x5 x18 = x18 ⟶ False) ⟶ False) ⟶ ((x4 x18 (x6 x5 x16) = x18 ⟶ False) ⟶ False) ⟶ ((x4 x18 (x14 x16) = x18 ⟶ False) ⟶ False) ⟶ ((x4 x18 x16 = x18 ⟶ False) ⟶ False) ⟶ ((x4 x18 x5 = x18 ⟶ False) ⟶ False) ⟶ ((x4 x18 x18 = x18 ⟶ False) ⟶ False) ⟶ ((x6 (x14 x16) x16 = x14 x5 ⟶ False) ⟶ False) ⟶ ((x6 (x14 x5) x16 = x6 (x14 x5) x16 ⟶ False) ⟶ False) ⟶ ((x6 (x14 x5) x5 = x14 x5 ⟶ False) ⟶ False) ⟶ ((x6 x16 x16 = x5 ⟶ False) ⟶ False) ⟶ ((x6 x16 x5 = x16 ⟶ False) ⟶ False) ⟶ ((x6 x5 (x6 (x14 x5) x16) = x14 x16 ⟶ False) ⟶ False) ⟶ ((x6 x5 (x6 x5 x16) = x16 ⟶ False) ⟶ False) ⟶ ((x6 x5 (x14 x16) = x6 (x14 x5) x16 ⟶ False) ⟶ False) ⟶ ((x6 x5 (x14 x5) = x14 x5 ⟶ False) ⟶ False) ⟶ ((x6 x5 x16 = x6 x5 x16 ⟶ False) ⟶ False) ⟶ ((x6 x5 x5 = x5 ⟶ False) ⟶ False) ⟶ ((x3 (x6 (x14 x5) x16) (x6 (x14 x5) x16) = x18 ⟶ False) ⟶ False) ⟶ ((x3 (x6 (x14 x5) x16) (x6 x5 x16) = x14 x5 ⟶ False) ⟶ False) ⟶ ((x3 (x6 (x14 x5) x16) (x14 x5) = x6 x5 x16 ⟶ False) ⟶ False) ⟶ ((x3 (x6 (x14 x5) x16) x18 = x6 (x14 x5) x16 ⟶ False) ⟶ False) ⟶ ((x3 (x6 x5 x16) (x6 (x14 x5) x16) = x5 ⟶ False) ⟶ False) ⟶ ((x3 (x6 x5 x16) (x6 x5 x16) = x18 ⟶ False) ⟶ False) ⟶ ((x3 (x6 x5 x16) x5 = x6 (x14 x5) x16 ⟶ False) ⟶ False) ⟶ ((x3 (x6 x5 x16) x18 = x6 x5 x16 ⟶ False) ⟶ False) ⟶ ((x3 (x14 x16) (x14 x16) = x18 ⟶ False) ⟶ False) ⟶ ((x3 (x14 x16) (x14 x5) = x14 x5 ⟶ False) ⟶ False) ⟶ ((x3 (x14 x16) x18 = x14 x16 ⟶ False) ⟶ False) ⟶ ((x3 (x14 x5) (x6 (x14 x5) x16) = x6 (x14 x5) x16 ⟶ False) ⟶ False) ⟶ ((x3 (x14 x5) (x14 x16) = x5 ⟶ False) ⟶ False) ⟶ ((x3 (x14 x5) (x14 x5) = x18 ⟶ False) ⟶ False) ⟶ ((x3 (x14 x5) x5 = x14 x16 ⟶ False) ⟶ False) ⟶ ((x3 (x14 x5) x18 = x14 x5 ⟶ False) ⟶ False) ⟶ ((x3 x16 x16 = x18 ⟶ False) ⟶ False) ⟶ ((x3 x16 x5 = x5 ⟶ False) ⟶ False) ⟶ ((x3 x16 x18 = x16 ⟶ False) ⟶ False) ⟶ ((x3 x5 (x6 x5 x16) = x6 x5 x16 ⟶ False) ⟶ False) ⟶ ((x3 x5 (x14 x5) = x16 ⟶ False) ⟶ False) ⟶ ((x3 x5 x16 = x14 x5 ⟶ False) ⟶ False) ⟶ ((x3 x5 x5 = x18 ⟶ False) ⟶ False) ⟶ ((x3 x5 x18 = x5 ⟶ False) ⟶ False) ⟶ ((x3 x18 (x6 (x14 x5) x16) = x6 x5 x16 ⟶ False) ⟶ False) ⟶ ((x3 x18 (x6 x5 x16) = x6 (x14 x5) x16 ⟶ False) ⟶ False) ⟶ ((x3 x18 (x14 x16) = x16 ⟶ False) ⟶ False) ⟶ ((x3 x18 (x14 x5) = x5 ⟶ False) ⟶ False) ⟶ ((x3 x18 x16 = x14 x16 ⟶ False) ⟶ False) ⟶ ((x3 x18 x5 = x14 x5 ⟶ False) ⟶ False) ⟶ ((x3 x18 x18 = x18 ⟶ False) ⟶ False) ⟶ ((x8 (x6 (x14 x5) x16) (x6 (x14 x5) x16) = x14 x5 ⟶ False) ⟶ False) ⟶ ((x8 (x6 (x14 x5) x16) (x6 x5 x16) = x18 ⟶ False) ⟶ False) ⟶ ((x8 (x6 (x14 x5) x16) x5 = x6 x5 x16 ⟶ False) ⟶ False) ⟶ ((x8 (x6 x5 x16) (x6 (x14 x5) x16) = x18 ⟶ False) ⟶ False) ⟶ ((x8 (x6 x5 x16) (x6 x5 x16) = x5 ⟶ False) ⟶ False) ⟶ ((x8 (x6 x5 x16) (x14 x5) = x6 (x14 x5) x16 ⟶ False) ⟶ False) ⟶ ((x8 (x6 x5 x16) x18 = x6 x5 x16 ⟶ False) ⟶ False) ⟶ ((x8 (x14 x16) x16 = x18 ⟶ False) ⟶ False) ⟶ ((x8 (x14 x16) x5 = x14 x5 ⟶ False) ⟶ False) ⟶ ((x8 (x14 x5) (x6 x5 x16) = x6 (x14 x5) x16 ⟶ False) ⟶ False) ⟶ ((x8 (x14 x5) (x14 x5) = x14 x16 ⟶ False) ⟶ False) ⟶ ((x8 (x14 x5) x16 = x5 ⟶ False) ⟶ False) ⟶ ((x8 (x14 x5) x5 = x18 ⟶ False) ⟶ False) ⟶ ((x8 (x14 x5) x18 = x14 x5 ⟶ False) ⟶ False) ⟶ ((x8 x16 (x14 x16) = x18 ⟶ False) ⟶ False) ⟶ ((x8 x16 (x14 x5) = x5 ⟶ False) ⟶ False) ⟶ ((x8 x16 x18 = x16 ⟶ False) ⟶ False) ⟶ ((x8 x5 (x6 (x14 x5) x16) = x6 x5 x16 ⟶ False) ⟶ False) ⟶ ((x8 x5 (x14 x16) = x14 x5 ⟶ False) ⟶ False) ⟶ ((x8 x5 (x14 x5) = x18 ⟶ False) ⟶ False) ⟶ ((x8 x5 x5 = x16 ⟶ False) ⟶ False) ⟶ ((x8 x5 x18 = x5 ⟶ False) ⟶ False) ⟶ ((x8 x18 (x6 (x14 x5) x16) = x6 (x14 x5) x16 ⟶ False) ⟶ False) ⟶ ((x8 x18 (x6 x5 x16) = x6 x5 x16 ⟶ False) ⟶ False) ⟶ ((x8 x18 (x14 x16) = x14 x16 ⟶ False) ⟶ False) ⟶ ((x8 x18 (x14 x5) = x14 x5 ⟶ False) ⟶ False) ⟶ ((x8 x18 x16 = x16 ⟶ False) ⟶ False) ⟶ ((x8 x18 x5 = x5 ⟶ False) ⟶ False) ⟶ ((x8 x18 x18 = x18 ⟶ False) ⟶ False) ⟶ (∀ x53 . (x12 x53 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . (x52 x55 ⟶ False) ⟶ (x52 x53 ⟶ False) ⟶ x11 x53 (x10 x55) ⟶ x11 x54 x53 ⟶ (x17 x54 x55 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . (x52 x55 ⟶ False) ⟶ (x52 x53 ⟶ False) ⟶ x11 x53 (x10 x55) ⟶ x17 x54 x55 x53 ⟶ (x11 x54 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x11 x54 x15 ⟶ x0 x53 ⟶ (x47 x54 x53 = x3 x54 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x11 x54 x15 ⟶ x0 x53 ⟶ (x19 x54 x53 = x4 x54 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x11 x54 x15 ⟶ x0 x53 ⟶ (x46 x54 x53 = x8 x54 x53 ⟶ False) ⟶ False) ⟶ ((x1 = x9 ⟶ False) ⟶ False) ⟶ (∀ x53 . x11 x53 x15 ⟶ (x45 x53 = x44 x53 ⟶ False) ⟶ False) ⟶ ((x49 = x13 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x11 x54 x15 ⟶ x0 x53 ⟶ (x43 x54 x53 = x6 x54 x53 ⟶ False) ⟶ False) ⟶ ((x0 x20 ⟶ False) ⟶ False) ⟶ ((x42 x20 ⟶ False) ⟶ False) ⟶ ((x50 x20 ⟶ False) ⟶ False) ⟶ ((x52 x20 ⟶ False) ⟶ False) ⟶ ((x0 x21 ⟶ False) ⟶ False) ⟶ ((x41 x21 ⟶ False) ⟶ False) ⟶ ((x42 x21 ⟶ False) ⟶ False) ⟶ ((x50 x21 ⟶ False) ⟶ False) ⟶ ((x22 x23 ⟶ False) ⟶ False) ⟶ ((x40 x23 ⟶ False) ⟶ False) ⟶ (x52 x23 ⟶ False) ⟶ ((x0 x39 ⟶ False) ⟶ False) ⟶ ((x48 x39 ⟶ False) ⟶ False) ⟶ ((x42 x39 ⟶ False) ⟶ False) ⟶ ((x50 x39 ⟶ False) ⟶ False) ⟶ ((x40 x38 ⟶ False) ⟶ False) ⟶ (x52 x38 ⟶ False) ⟶ ((x0 x37 ⟶ False) ⟶ False) ⟶ ((x40 x24 ⟶ False) ⟶ False) ⟶ (x52 x24 ⟶ False) ⟶ (∀ x53 . x50 x53 ⟶ (x14 (x14 x53) = x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . (x41 x54 ⟶ False) ⟶ x0 x54 ⟶ (x41 x53 ⟶ False) ⟶ x0 x53 ⟶ x41 (x8 x54 x53) ⟶ False) ⟶ (∀ x53 x54 . x0 x54 ⟶ x0 x53 ⟶ (x0 (x6 x54 x53) ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x0 x54 ⟶ x0 x53 ⟶ (x0 (x3 x54 x53) ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x0 x54 ⟶ x0 x53 ⟶ (x0 (x4 x54 x53) ⟶ False) ⟶ False) ⟶ ((x40 x13 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x0 x54 ⟶ x0 x53 ⟶ (x0 (x8 x54 x53) ⟶ False) ⟶ False) ⟶ ((x22 x13 ⟶ False) ⟶ False) ⟶ ((x22 x15 ⟶ False) ⟶ False) ⟶ (∀ x53 . x0 x53 ⟶ (x0 (x2 x53) ⟶ False) ⟶ False) ⟶ (∀ x53 . x0 x53 ⟶ (x0 (x14 x53) ⟶ False) ⟶ False) ⟶ (∀ x53 . x0 x53 ⟶ (x50 (x14 x53) ⟶ False) ⟶ False) ⟶ (∀ x53 . x0 x53 ⟶ (x0 (x25 x53) ⟶ False) ⟶ False) ⟶ ((x36 x15 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . (x48 x54 ⟶ False) ⟶ x0 x54 ⟶ (x48 x53 ⟶ False) ⟶ x0 x53 ⟶ x41 (x6 x54 x53) ⟶ False) ⟶ (∀ x53 x54 . (x41 x54 ⟶ False) ⟶ x0 x54 ⟶ (x41 x53 ⟶ False) ⟶ x0 x53 ⟶ x41 (x6 x54 x53) ⟶ False) ⟶ (∀ x53 x54 . (x41 x54 ⟶ False) ⟶ x0 x54 ⟶ (x48 x53 ⟶ False) ⟶ x0 x53 ⟶ x48 (x6 x53 x54) ⟶ False) ⟶ (∀ x53 x54 . (x41 x54 ⟶ False) ⟶ x0 x54 ⟶ (x48 x53 ⟶ False) ⟶ x0 x53 ⟶ x48 (x6 x54 x53) ⟶ False) ⟶ (∀ x53 . x0 x53 ⟶ (x0 (x44 x53) ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . (x41 x54 ⟶ False) ⟶ x0 x54 ⟶ (x41 x53 ⟶ False) ⟶ x0 x53 ⟶ x41 (x4 x54 x53) ⟶ False) ⟶ (∀ x53 x54 . (x48 x54 ⟶ False) ⟶ x0 x54 ⟶ (x48 x53 ⟶ False) ⟶ x0 x53 ⟶ x41 (x4 x54 x53) ⟶ False) ⟶ (∀ x53 x54 . (x48 x54 ⟶ False) ⟶ x0 x54 ⟶ (x41 x53 ⟶ False) ⟶ x0 x53 ⟶ x48 (x4 x53 x54) ⟶ False) ⟶ (∀ x53 x54 . (x48 x54 ⟶ False) ⟶ x0 x54 ⟶ (x41 x53 ⟶ False) ⟶ x0 x53 ⟶ x48 (x4 x54 x53) ⟶ False) ⟶ (∀ x53 x54 . x41 x54 ⟶ x0 x54 ⟶ (x41 x53 ⟶ False) ⟶ x0 x53 ⟶ (x48 (x3 x53 x54) ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x41 x54 ⟶ x0 x54 ⟶ (x41 x53 ⟶ False) ⟶ x0 x53 ⟶ (x41 (x3 x54 x53) ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x48 x54 ⟶ x0 x54 ⟶ (x48 x53 ⟶ False) ⟶ x0 x53 ⟶ (x41 (x3 x53 x54) ⟶ False) ⟶ False) ⟶ (∀ x53 . x50 x53 ⟶ (x50 (x44 x53) ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x48 x54 ⟶ x0 x54 ⟶ (x48 x53 ⟶ False) ⟶ x0 x53 ⟶ (x48 (x3 x54 x53) ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . (x41 x54 ⟶ False) ⟶ x0 x54 ⟶ (x48 x53 ⟶ False) ⟶ x0 x53 ⟶ x48 (x3 x53 x54) ⟶ False) ⟶ (∀ x53 x54 . (x41 x54 ⟶ False) ⟶ x0 x54 ⟶ (x48 x53 ⟶ False) ⟶ x0 x53 ⟶ x41 (x3 x54 x53) ⟶ False) ⟶ (∀ x53 . (x41 x53 ⟶ False) ⟶ x0 x53 ⟶ x48 (x14 x53) ⟶ False) ⟶ (∀ x53 . (x41 x53 ⟶ False) ⟶ x0 x53 ⟶ (x50 (x14 x53) ⟶ False) ⟶ False) ⟶ (∀ x53 . (x48 x53 ⟶ False) ⟶ x0 x53 ⟶ x41 (x14 x53) ⟶ False) ⟶ (∀ x53 . (x48 x53 ⟶ False) ⟶ x0 x53 ⟶ (x50 (x14 x53) ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x41 x54 ⟶ x0 x54 ⟶ (x48 x53 ⟶ False) ⟶ x0 x53 ⟶ (x41 (x8 x53 x54) ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x41 x54 ⟶ x0 x54 ⟶ (x48 x53 ⟶ False) ⟶ x0 x53 ⟶ (x41 (x8 x54 x53) ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x48 x54 ⟶ x0 x54 ⟶ (x41 x53 ⟶ False) ⟶ x0 x53 ⟶ (x48 (x8 x53 x54) ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x48 x54 ⟶ x0 x54 ⟶ (x41 x53 ⟶ False) ⟶ x0 x53 ⟶ (x48 (x8 x54 x53) ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . (x48 x54 ⟶ False) ⟶ x0 x54 ⟶ (x48 x53 ⟶ False) ⟶ x0 x53 ⟶ x48 (x8 x54 x53) ⟶ False) ⟶ (∀ x53 x54 . (x52 x54 ⟶ False) ⟶ (x52 x53 ⟶ False) ⟶ x11 x53 (x10 x54) ⟶ (x17 (x35 x53 x54) x54 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . (x11 (x26 x53) x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 x55 . (x52 x55 ⟶ False) ⟶ (x52 x53 ⟶ False) ⟶ x11 x53 (x10 x55) ⟶ x17 x54 x55 x53 ⟶ (x11 x54 x55 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x11 x54 x15 ⟶ x0 x53 ⟶ (x11 (x47 x54 x53) x15 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x11 x54 x15 ⟶ x0 x53 ⟶ (x11 (x19 x54 x53) x15 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x11 x54 x15 ⟶ x0 x53 ⟶ (x11 (x46 x54 x53) x15 ⟶ False) ⟶ False) ⟶ ((x17 x1 x15 x49 ⟶ False) ⟶ False) ⟶ (∀ x53 . x11 x53 x15 ⟶ (x11 (x45 x53) x15 ⟶ False) ⟶ False) ⟶ ((x11 x49 (x10 x15) ⟶ False) ⟶ False) ⟶ (∀ x53 . x50 x53 ⟶ (x50 (x14 x53) ⟶ False) ⟶ False) ⟶ (∀ x53 . x0 x53 ⟶ (x11 (x7 x53) x15 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x11 x54 x15 ⟶ x0 x53 ⟶ (x11 (x43 x54 x53) x15 ⟶ False) ⟶ False) ⟶ (∀ x53 . x50 x53 ⟶ (x44 x53 = x4 x53 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x0 x53 ⟶ (x7 x53 = x6 (x25 x53) (x2 x53) ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x11 x54 x15 ⟶ x0 x53 ⟶ (x19 x54 x53 = x19 x53 x54 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x11 x54 x15 ⟶ x0 x53 ⟶ (x46 x54 x53 = x46 x53 x54 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x50 x54 ⟶ x50 x53 ⟶ (x4 x54 x53 = x4 x53 x54 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x50 x54 ⟶ x50 x53 ⟶ (x8 x54 x53 = x8 x53 x54 ⟶ False) ⟶ False) ⟶ (∀ x53 . x11 x53 (x10 x15) ⟶ (x36 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x36 x53 ⟶ (x27 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x0 x53 ⟶ (x42 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x36 x53 ⟶ (x28 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x0 x53 ⟶ (x50 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x29 x53 ⟶ (x36 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x34 x53 ⟶ (x0 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x30 x53 ⟶ (x29 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x52 x53 ⟶ (x22 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x11 x53 x49 ⟶ (x40 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x40 x54 ⟶ x11 x53 (x10 x54) ⟶ (x40 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x30 x54 ⟶ x11 x53 (x10 x54) ⟶ (x30 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x29 x54 ⟶ x11 x53 (x10 x54) ⟶ (x29 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x36 x54 ⟶ x11 x53 (x10 x54) ⟶ (x36 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x28 x54 ⟶ x11 x53 (x10 x54) ⟶ (x28 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x11 x53 x15 ⟶ (x0 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x40 x53 ⟶ (x30 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x27 x54 ⟶ x11 x53 (x10 x54) ⟶ (x27 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x52 x53 ⟶ (x40 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x40 x54 ⟶ x11 x53 x54 ⟶ (x34 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x30 x54 ⟶ x11 x53 x54 ⟶ (x33 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x29 x54 ⟶ x11 x53 x54 ⟶ (x31 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x36 x54 ⟶ x11 x53 x54 ⟶ (x0 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x28 x54 ⟶ x11 x53 x54 ⟶ (x42 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x27 x54 ⟶ x11 x53 x54 ⟶ (x50 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 . x11 x53 (x10 x49) ⟶ (x40 x53 ⟶ False) ⟶ False) ⟶ (∀ x53 x54 . x51 x53 x54 ⟶ x51 x54 x53 ⟶ False) ⟶ (x7 (x19 x16 x32) = x43 (x19 x16 (x7 x32)) (x47 x5 (x45 (x7 x32))) ⟶ False) ⟶ (x2 x32 = x1 ⟶ False) ⟶ ((x0 x32 ⟶ False) ⟶ False) ⟶ False (proof)