Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrNUD../5b7a2..
PUh24../2310d..
vout
PrNUD../2856e.. 0.04 bars
TMaBC../2b7ff.. ownership of 4af6e.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMPTB../f2f02.. ownership of 8609a.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PURG6../4d98d.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 4af6e.. : ∀ 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 x55 . x53 x55 ⟶ x53 x54 ⟶ (x52 x55 x54 ⟶ False) ⟶ (x51 x54 ⟶ False) ⟶ (x50 x55 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x0 x55 ⟶ (x55 = x54 ⟶ False) ⟶ x0 x54 ⟶ False) ⟶ (∀ x54 x55 . x53 x55 ⟶ x53 x54 ⟶ (x52 x55 x54 ⟶ False) ⟶ (x50 x55 ⟶ False) ⟶ (x51 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x1 x54 x55 ⟶ x0 x55 ⟶ False) ⟶ (∀ x54 x55 . x53 x55 ⟶ x53 x54 ⟶ x52 x55 x54 ⟶ (x0 x55 ⟶ False) ⟶ (x50 x54 ⟶ False) ⟶ (x51 x55 ⟶ False) ⟶ False) ⟶ (∀ x54 . x0 x54 ⟶ (x54 = x2 ⟶ False) ⟶ False) ⟶ (∀ x54 . x49 x54 ⟶ (x48 x54 x47 = x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 x56 . x53 x56 ⟶ x53 x54 ⟶ x53 x55 ⟶ (x52 x56 x3 ⟶ False) ⟶ (x52 x55 x54 ⟶ False) ⟶ x52 (x4 x55 x56) (x4 x54 x56) ⟶ False) ⟶ (∀ x54 . x53 x54 ⟶ (x52 x3 (x4 x54 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 x56 . x1 x54 x55 ⟶ x6 x55 (x5 x56) ⟶ x0 x56 ⟶ False) ⟶ (∀ x54 x55 . x53 x55 ⟶ x53 x54 ⟶ x52 x55 x54 ⟶ (x0 x54 ⟶ False) ⟶ (x51 x55 ⟶ False) ⟶ (x50 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x49 x54 ⟶ (x48 x3 x54 = x3 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 x56 . x1 x55 x56 ⟶ x6 x56 (x5 x54) ⟶ (x6 x55 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x53 x55 ⟶ x53 x54 ⟶ x52 x55 x54 ⟶ (x50 x54 ⟶ False) ⟶ x50 x55 ⟶ False) ⟶ (∀ x54 . x49 x54 ⟶ (x46 x54 x3 = x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x7 x55 x54 ⟶ (x6 x55 (x5 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x6 x55 (x5 x54) ⟶ (x7 x55 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x53 x55 ⟶ x53 x54 ⟶ x52 x55 x54 ⟶ (x51 x55 ⟶ False) ⟶ x51 x54 ⟶ False) ⟶ (∀ x54 . x49 x54 ⟶ (x4 x47 x54 = x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 x56 . x8 x56 ⟶ x8 x54 ⟶ x8 x55 ⟶ x52 x56 x54 ⟶ x52 x54 x55 ⟶ (x52 x56 x55 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x6 x54 x55 ⟶ (x0 x55 ⟶ False) ⟶ (x1 x54 x55 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x53 x55 ⟶ x53 x54 ⟶ x52 x55 x54 ⟶ x51 x54 ⟶ (x51 x55 ⟶ False) ⟶ False) ⟶ (∀ x54 . x49 x54 ⟶ (x4 x54 x3 = x3 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x1 x55 x54 ⟶ (x6 x55 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x53 x55 ⟶ x53 x54 ⟶ x52 x55 x54 ⟶ x50 x55 ⟶ (x50 x54 ⟶ False) ⟶ False) ⟶ ((x6 x2 x9 ⟶ False) ⟶ False) ⟶ (∀ x54 . x49 x54 ⟶ (x45 x54 x3 = x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x49 x55 ⟶ x49 x54 ⟶ (x46 (x10 x55) (x10 x54) = x46 x54 x55 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x49 x55 ⟶ x49 x54 ⟶ (x45 (x10 x55) (x10 x54) = x10 (x45 x55 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 x56 . x49 x56 ⟶ x49 x54 ⟶ x49 x55 ⟶ (x4 (x4 x56 x54) x55 = x4 x56 (x4 x54 x55) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 x56 . x49 x56 ⟶ x49 x54 ⟶ x49 x55 ⟶ (x45 (x45 x56 x54) x55 = x45 x56 (x45 x54 x55) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 x56 . x49 x56 ⟶ x49 x54 ⟶ x49 x55 ⟶ (x4 (x45 x56 x54) x55 = x45 (x4 x56 x55) (x4 x54 x55) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 x56 . x49 x56 ⟶ x49 x54 ⟶ x49 x55 ⟶ (x4 x56 (x48 x54 x55) = x48 (x4 x56 x54) x55 ⟶ False) ⟶ False) ⟶ (∀ x54 . x49 x54 ⟶ (x48 x47 x54 = x11 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x49 x54 ⟶ (x4 x54 (x10 x47) = x10 x54 ⟶ False) ⟶ False) ⟶ ((x6 x47 x12 ⟶ False) ⟶ False) ⟶ ((x6 x47 x44 ⟶ False) ⟶ False) ⟶ ((x13 x47 x12 x44 ⟶ False) ⟶ False) ⟶ ((x50 x47 ⟶ False) ⟶ False) ⟶ (x0 x47 ⟶ False) ⟶ (∀ x54 x55 . x49 x55 ⟶ x49 x54 ⟶ (x45 x55 (x10 x54) = x46 x55 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x49 x55 ⟶ x49 x54 ⟶ (x4 x55 (x11 x54) = x48 x55 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x49 x55 ⟶ x49 x54 ⟶ (x48 (x11 x55) (x11 x54) = x48 x54 x55 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x49 x55 ⟶ x49 x54 ⟶ (x4 (x11 x55) (x11 x54) = x11 (x4 x55 x54) ⟶ False) ⟶ False) ⟶ ((x6 x43 x12 ⟶ False) ⟶ False) ⟶ ((x6 x43 x44 ⟶ False) ⟶ False) ⟶ ((x13 x43 x12 x44 ⟶ False) ⟶ False) ⟶ ((x0 x43 ⟶ False) ⟶ False) ⟶ ((x10 (x10 x47) = x47 ⟶ False) ⟶ False) ⟶ ((x10 x47 = x10 x47 ⟶ False) ⟶ False) ⟶ ((x10 x43 = x43 ⟶ False) ⟶ False) ⟶ ((x4 x47 x47 = x47 ⟶ False) ⟶ False) ⟶ ((x4 x47 x43 = x43 ⟶ False) ⟶ False) ⟶ ((x4 x43 x47 = x43 ⟶ False) ⟶ False) ⟶ ((x4 x43 x43 = x43 ⟶ False) ⟶ False) ⟶ ((x48 (x10 x47) x47 = x10 x47 ⟶ False) ⟶ False) ⟶ ((x48 x47 (x10 x47) = x10 x47 ⟶ False) ⟶ False) ⟶ ((x48 x47 x47 = x47 ⟶ False) ⟶ False) ⟶ ((x46 (x10 x47) (x10 x47) = x43 ⟶ False) ⟶ False) ⟶ ((x46 (x10 x47) x43 = x10 x47 ⟶ False) ⟶ False) ⟶ ((x46 x47 x47 = x43 ⟶ False) ⟶ False) ⟶ ((x46 x47 x43 = x47 ⟶ False) ⟶ False) ⟶ ((x46 x43 (x10 x47) = x47 ⟶ False) ⟶ False) ⟶ ((x46 x43 x47 = x10 x47 ⟶ False) ⟶ False) ⟶ ((x46 x43 x43 = x43 ⟶ False) ⟶ False) ⟶ ((x45 (x10 x47) x47 = x43 ⟶ False) ⟶ False) ⟶ ((x45 (x10 x47) x43 = x10 x47 ⟶ False) ⟶ False) ⟶ ((x45 x47 (x10 x47) = x43 ⟶ False) ⟶ False) ⟶ ((x45 x47 x43 = x47 ⟶ False) ⟶ False) ⟶ ((x45 x43 (x10 x47) = x10 x47 ⟶ False) ⟶ False) ⟶ ((x45 x43 x47 = x47 ⟶ False) ⟶ False) ⟶ ((x45 x43 x43 = x43 ⟶ False) ⟶ False) ⟶ ((x52 (x10 x47) (x10 x47) ⟶ False) ⟶ False) ⟶ ((x52 (x10 x47) x47 ⟶ False) ⟶ False) ⟶ ((x52 (x10 x47) x43 ⟶ False) ⟶ False) ⟶ (x52 x47 (x10 x47) ⟶ False) ⟶ ((x52 x47 x47 ⟶ False) ⟶ False) ⟶ (x52 x47 x43 ⟶ False) ⟶ (x52 x43 (x10 x47) ⟶ False) ⟶ ((x52 x43 x47 ⟶ False) ⟶ False) ⟶ ((x52 x43 x43 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x8 x55 ⟶ x8 x54 ⟶ (x52 x55 x55 ⟶ False) ⟶ False) ⟶ (∀ x54 . (x7 x54 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 x56 . (x0 x56 ⟶ False) ⟶ (x0 x54 ⟶ False) ⟶ x6 x54 (x5 x56) ⟶ x6 x55 x54 ⟶ (x13 x55 x56 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 x56 . (x0 x56 ⟶ False) ⟶ (x0 x54 ⟶ False) ⟶ x6 x54 (x5 x56) ⟶ x13 x55 x56 x54 ⟶ (x6 x55 x54 ⟶ False) ⟶ False) ⟶ ((x3 = x2 ⟶ False) ⟶ False) ⟶ ((x44 = x9 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x53 x55 ⟶ x53 x54 ⟶ (x14 x55 x54 = x4 x55 x54 ⟶ False) ⟶ False) ⟶ ((x8 x42 ⟶ False) ⟶ False) ⟶ ((x0 x42 ⟶ False) ⟶ False) ⟶ ((x53 x41 ⟶ False) ⟶ False) ⟶ ((x8 x41 ⟶ False) ⟶ False) ⟶ ((x49 x41 ⟶ False) ⟶ False) ⟶ ((x0 x41 ⟶ False) ⟶ False) ⟶ ((x51 x40 ⟶ False) ⟶ False) ⟶ ((x8 x40 ⟶ False) ⟶ False) ⟶ ((x53 x39 ⟶ False) ⟶ False) ⟶ ((x51 x39 ⟶ False) ⟶ False) ⟶ ((x8 x39 ⟶ False) ⟶ False) ⟶ ((x49 x39 ⟶ False) ⟶ False) ⟶ ((x38 x37 ⟶ False) ⟶ False) ⟶ ((x15 x37 ⟶ False) ⟶ False) ⟶ (x0 x37 ⟶ False) ⟶ ((x50 x16 ⟶ False) ⟶ False) ⟶ ((x8 x16 ⟶ False) ⟶ False) ⟶ ((x53 x17 ⟶ False) ⟶ False) ⟶ ((x50 x17 ⟶ False) ⟶ False) ⟶ ((x8 x17 ⟶ False) ⟶ False) ⟶ ((x49 x17 ⟶ False) ⟶ False) ⟶ (x0 x18 ⟶ False) ⟶ ((x15 x36 ⟶ False) ⟶ False) ⟶ (x0 x36 ⟶ False) ⟶ ((x8 x35 ⟶ False) ⟶ False) ⟶ ((x53 x19 ⟶ False) ⟶ False) ⟶ ((x0 x34 ⟶ False) ⟶ False) ⟶ ((x15 x20 ⟶ False) ⟶ False) ⟶ (x0 x20 ⟶ False) ⟶ (∀ x54 . x49 x54 ⟶ (x11 (x11 x54) = x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x49 x54 ⟶ (x10 (x10 x54) = x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . (x51 x55 ⟶ False) ⟶ x53 x55 ⟶ (x51 x54 ⟶ False) ⟶ x53 x54 ⟶ x51 (x45 x55 x54) ⟶ False) ⟶ (∀ x54 x55 . x53 x55 ⟶ x53 x54 ⟶ (x53 (x48 x55 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x53 x55 ⟶ x53 x54 ⟶ (x53 (x46 x55 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x53 x55 ⟶ x53 x54 ⟶ (x53 (x4 x55 x54) ⟶ False) ⟶ False) ⟶ ((x15 x9 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x53 x55 ⟶ x53 x54 ⟶ (x53 (x45 x55 x54) ⟶ False) ⟶ False) ⟶ ((x38 x9 ⟶ False) ⟶ False) ⟶ ((x38 x12 ⟶ False) ⟶ False) ⟶ (∀ x54 . x53 x54 ⟶ (x53 (x11 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 . x53 x54 ⟶ (x49 (x11 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 . x53 x54 ⟶ (x53 (x10 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 . x53 x54 ⟶ (x49 (x10 x54) ⟶ False) ⟶ False) ⟶ ((x21 x12 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . (x50 x55 ⟶ False) ⟶ x53 x55 ⟶ (x50 x54 ⟶ False) ⟶ x53 x54 ⟶ x51 (x48 x55 x54) ⟶ False) ⟶ (∀ x54 x55 . (x51 x55 ⟶ False) ⟶ x53 x55 ⟶ (x51 x54 ⟶ False) ⟶ x53 x54 ⟶ x51 (x48 x55 x54) ⟶ False) ⟶ (∀ x54 x55 . (x51 x55 ⟶ False) ⟶ x53 x55 ⟶ (x50 x54 ⟶ False) ⟶ x53 x54 ⟶ x50 (x48 x54 x55) ⟶ False) ⟶ (∀ x54 x55 . (x51 x55 ⟶ False) ⟶ x53 x55 ⟶ (x50 x54 ⟶ False) ⟶ x53 x54 ⟶ x50 (x48 x55 x54) ⟶ False) ⟶ (∀ x54 . (x51 x54 ⟶ False) ⟶ x53 x54 ⟶ x51 (x11 x54) ⟶ False) ⟶ (∀ x54 . (x51 x54 ⟶ False) ⟶ x53 x54 ⟶ (x49 (x11 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 . x53 x54 ⟶ (x53 (x33 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 . x51 x54 ⟶ x53 x54 ⟶ (x51 (x11 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 . x51 x54 ⟶ x53 x54 ⟶ (x49 (x11 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 . (x50 x54 ⟶ False) ⟶ x53 x54 ⟶ x50 (x11 x54) ⟶ False) ⟶ (∀ x54 . (x50 x54 ⟶ False) ⟶ x53 x54 ⟶ (x49 (x11 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 . x50 x54 ⟶ x53 x54 ⟶ (x50 (x11 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 . x50 x54 ⟶ x53 x54 ⟶ (x49 (x11 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . (x51 x55 ⟶ False) ⟶ x53 x55 ⟶ (x51 x54 ⟶ False) ⟶ x53 x54 ⟶ x51 (x4 x55 x54) ⟶ False) ⟶ (∀ x54 x55 . (x50 x55 ⟶ False) ⟶ x53 x55 ⟶ (x50 x54 ⟶ False) ⟶ x53 x54 ⟶ x51 (x4 x55 x54) ⟶ False) ⟶ (∀ x54 x55 . (x50 x55 ⟶ False) ⟶ x53 x55 ⟶ (x51 x54 ⟶ False) ⟶ x53 x54 ⟶ x50 (x4 x54 x55) ⟶ False) ⟶ (∀ x54 x55 . (x50 x55 ⟶ False) ⟶ x53 x55 ⟶ (x51 x54 ⟶ False) ⟶ x53 x54 ⟶ x50 (x4 x55 x54) ⟶ False) ⟶ (∀ x54 x55 . x51 x55 ⟶ x53 x55 ⟶ (x51 x54 ⟶ False) ⟶ x53 x54 ⟶ (x50 (x46 x54 x55) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x51 x55 ⟶ x53 x55 ⟶ (x51 x54 ⟶ False) ⟶ x53 x54 ⟶ (x51 (x46 x55 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x50 x55 ⟶ x53 x55 ⟶ (x50 x54 ⟶ False) ⟶ x53 x54 ⟶ (x51 (x46 x54 x55) ⟶ False) ⟶ False) ⟶ ((x0 x2 ⟶ False) ⟶ False) ⟶ (∀ x54 . x49 x54 ⟶ (x49 (x33 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x50 x55 ⟶ x53 x55 ⟶ (x50 x54 ⟶ False) ⟶ x53 x54 ⟶ (x50 (x46 x55 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . (x51 x55 ⟶ False) ⟶ x53 x55 ⟶ (x50 x54 ⟶ False) ⟶ x53 x54 ⟶ x50 (x46 x54 x55) ⟶ False) ⟶ (∀ x54 x55 . (x51 x55 ⟶ False) ⟶ x53 x55 ⟶ (x50 x54 ⟶ False) ⟶ x53 x54 ⟶ x51 (x46 x55 x54) ⟶ False) ⟶ (∀ x54 . (x51 x54 ⟶ False) ⟶ x53 x54 ⟶ x50 (x10 x54) ⟶ False) ⟶ (∀ x54 . (x51 x54 ⟶ False) ⟶ x53 x54 ⟶ (x49 (x10 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 . (x50 x54 ⟶ False) ⟶ x53 x54 ⟶ x51 (x10 x54) ⟶ False) ⟶ (∀ x54 . (x50 x54 ⟶ False) ⟶ x53 x54 ⟶ (x49 (x10 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x51 x55 ⟶ x53 x55 ⟶ (x50 x54 ⟶ False) ⟶ x53 x54 ⟶ (x51 (x45 x54 x55) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x51 x55 ⟶ x53 x55 ⟶ (x50 x54 ⟶ False) ⟶ x53 x54 ⟶ (x51 (x45 x55 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x50 x55 ⟶ x53 x55 ⟶ (x51 x54 ⟶ False) ⟶ x53 x54 ⟶ (x50 (x45 x54 x55) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x50 x55 ⟶ x53 x55 ⟶ (x51 x54 ⟶ False) ⟶ x53 x54 ⟶ (x50 (x45 x55 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . (x50 x55 ⟶ False) ⟶ x53 x55 ⟶ (x50 x54 ⟶ False) ⟶ x53 x54 ⟶ x50 (x45 x55 x54) ⟶ False) ⟶ (∀ x54 x55 . (x0 x55 ⟶ False) ⟶ (x0 x54 ⟶ False) ⟶ x6 x54 (x5 x55) ⟶ (x13 (x32 x54 x55) x55 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . (x6 (x22 x54) x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 x56 . (x0 x56 ⟶ False) ⟶ (x0 x54 ⟶ False) ⟶ x6 x54 (x5 x56) ⟶ x13 x55 x56 x54 ⟶ (x6 x55 x56 ⟶ False) ⟶ False) ⟶ ((x13 x3 x12 x44 ⟶ False) ⟶ False) ⟶ (∀ x54 . x49 x54 ⟶ (x49 (x11 x54) ⟶ False) ⟶ False) ⟶ ((x6 x44 (x5 x12) ⟶ False) ⟶ False) ⟶ (∀ x54 . x49 x54 ⟶ (x49 (x10 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x53 x55 ⟶ x53 x54 ⟶ (x6 (x14 x55 x54) x12 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x49 x55 ⟶ x49 x54 ⟶ (x48 x55 x54 = x4 x55 (x11 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x49 x55 ⟶ x49 x54 ⟶ (x46 x55 x54 = x45 x55 (x10 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 . x49 x54 ⟶ (x33 x54 = x4 x54 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x8 x55 ⟶ x8 x54 ⟶ (x52 x55 x54 ⟶ False) ⟶ (x52 x54 x55 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x49 x55 ⟶ x49 x54 ⟶ (x4 x55 x54 = x4 x54 x55 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x49 x55 ⟶ x49 x54 ⟶ (x45 x55 x54 = x45 x54 x55 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x53 x55 ⟶ x53 x54 ⟶ (x14 x55 x54 = x14 x54 x55 ⟶ False) ⟶ False) ⟶ (∀ x54 . x8 x54 ⟶ (x50 x54 ⟶ False) ⟶ (x51 x54 ⟶ False) ⟶ (x8 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x8 x54 ⟶ (x50 x54 ⟶ False) ⟶ (x51 x54 ⟶ False) ⟶ (x0 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x6 x54 (x5 x12) ⟶ (x21 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x0 x54 ⟶ x8 x54 ⟶ x51 x54 ⟶ False) ⟶ (∀ x54 . x0 x54 ⟶ x8 x54 ⟶ x50 x54 ⟶ False) ⟶ (∀ x54 . x0 x54 ⟶ x8 x54 ⟶ (x8 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . (x0 x54 ⟶ False) ⟶ x8 x54 ⟶ (x50 x54 ⟶ False) ⟶ (x51 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . (x0 x54 ⟶ False) ⟶ x8 x54 ⟶ (x50 x54 ⟶ False) ⟶ (x8 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x8 x54 ⟶ x51 x54 ⟶ x50 x54 ⟶ False) ⟶ (∀ x54 . x8 x54 ⟶ x51 x54 ⟶ (x8 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x8 x54 ⟶ x51 x54 ⟶ x0 x54 ⟶ False) ⟶ (∀ x54 . x21 x54 ⟶ (x31 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . (x0 x54 ⟶ False) ⟶ x8 x54 ⟶ (x51 x54 ⟶ False) ⟶ (x50 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . (x0 x54 ⟶ False) ⟶ x8 x54 ⟶ (x51 x54 ⟶ False) ⟶ (x8 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x53 x54 ⟶ (x8 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x21 x54 ⟶ (x30 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x8 x54 ⟶ x50 x54 ⟶ x51 x54 ⟶ False) ⟶ (∀ x54 . x8 x54 ⟶ x50 x54 ⟶ (x8 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x8 x54 ⟶ x50 x54 ⟶ x0 x54 ⟶ False) ⟶ (∀ x54 . x53 x54 ⟶ (x49 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x23 x54 ⟶ (x21 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x29 x54 ⟶ (x8 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x29 x54 ⟶ (x53 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x28 x54 ⟶ (x23 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x0 x54 ⟶ (x38 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x6 x54 x44 ⟶ (x15 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x15 x55 ⟶ x6 x54 (x5 x55) ⟶ (x15 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x28 x55 ⟶ x6 x54 (x5 x55) ⟶ (x28 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x23 x55 ⟶ x6 x54 (x5 x55) ⟶ (x23 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x21 x55 ⟶ x6 x54 (x5 x55) ⟶ (x21 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x30 x55 ⟶ x6 x54 (x5 x55) ⟶ (x30 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x6 x54 x12 ⟶ (x53 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x15 x54 ⟶ (x28 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x31 x55 ⟶ x6 x54 (x5 x55) ⟶ (x31 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x0 x54 ⟶ (x15 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x15 x55 ⟶ x6 x54 x55 ⟶ (x29 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x28 x55 ⟶ x6 x54 x55 ⟶ (x24 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x23 x55 ⟶ x6 x54 x55 ⟶ (x27 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x21 x55 ⟶ x6 x54 x55 ⟶ (x53 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x30 x55 ⟶ x6 x54 x55 ⟶ (x8 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x31 x55 ⟶ x6 x54 x55 ⟶ (x49 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x6 x54 (x5 x44) ⟶ (x15 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x1 x54 x55 ⟶ x1 x55 x54 ⟶ False) ⟶ ((x52 x47 (x14 (x33 x25) x26) ⟶ False) ⟶ False) ⟶ (x52 x47 x26 ⟶ False) ⟶ (x52 x47 (x33 x25) ⟶ False) ⟶ ((x53 x26 ⟶ False) ⟶ False) ⟶ ((x53 x25 ⟶ False) ⟶ False) ⟶ False (proof)