Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrNUD../ee55f..
PUK8b../f629d..
vout
PrNUD../0cd44.. 0.00 bars
TMGE2../ba7d0.. ownership of 9d36d.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMY49../1e8e3.. ownership of d6baf.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUZrh../f6cf4.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 9d36d.. : ∀ 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 x56 . x54 x56 ⟶ x54 x55 ⟶ (x53 x56 x55 ⟶ False) ⟶ (x52 x55 ⟶ False) ⟶ (x51 x56 ⟶ False) ⟶ False) ⟶ (∀ x55 x56 . x0 x56 ⟶ (x56 = x55 ⟶ False) ⟶ x0 x55 ⟶ False) ⟶ (∀ x55 x56 . x54 x56 ⟶ x54 x55 ⟶ (x53 x56 x55 ⟶ False) ⟶ (x51 x56 ⟶ False) ⟶ (x52 x55 ⟶ False) ⟶ False) ⟶ (∀ x55 x56 . x1 x55 x56 ⟶ x0 x56 ⟶ False) ⟶ (∀ x55 x56 . x54 x56 ⟶ x54 x55 ⟶ x53 x56 x55 ⟶ (x0 x56 ⟶ False) ⟶ (x51 x55 ⟶ False) ⟶ (x52 x56 ⟶ False) ⟶ False) ⟶ (∀ x55 . x0 x55 ⟶ (x55 = x2 ⟶ False) ⟶ False) ⟶ (∀ x55 . x50 x55 ⟶ (x49 x55 x48 = x55 ⟶ False) ⟶ False) ⟶ (∀ x55 x56 x57 . x1 x55 x56 ⟶ x4 x56 (x3 x57) ⟶ x0 x57 ⟶ False) ⟶ (∀ x55 x56 . x54 x56 ⟶ x54 x55 ⟶ x53 x56 x55 ⟶ (x0 x55 ⟶ False) ⟶ (x52 x56 ⟶ False) ⟶ (x51 x55 ⟶ False) ⟶ False) ⟶ (∀ x55 . x50 x55 ⟶ (x49 x5 x55 = x5 ⟶ False) ⟶ False) ⟶ (∀ x55 x56 x57 . x1 x56 x57 ⟶ x4 x57 (x3 x55) ⟶ (x4 x56 x55 ⟶ False) ⟶ False) ⟶ (∀ x55 x56 . x54 x56 ⟶ x54 x55 ⟶ x53 x56 x55 ⟶ (x51 x55 ⟶ False) ⟶ x51 x56 ⟶ False) ⟶ (∀ x55 . x50 x55 ⟶ (x47 x55 x5 = x55 ⟶ False) ⟶ False) ⟶ (∀ x55 x56 . x6 x56 x55 ⟶ (x4 x56 (x3 x55) ⟶ False) ⟶ False) ⟶ (∀ x55 x56 . x4 x56 (x3 x55) ⟶ (x6 x56 x55 ⟶ False) ⟶ False) ⟶ (∀ x55 x56 . x54 x56 ⟶ x54 x55 ⟶ x53 x56 x55 ⟶ (x52 x56 ⟶ False) ⟶ x52 x55 ⟶ False) ⟶ (∀ x55 . x50 x55 ⟶ (x46 x48 x55 = x55 ⟶ False) ⟶ False) ⟶ (∀ x55 x56 . x4 x55 x56 ⟶ (x0 x56 ⟶ False) ⟶ (x1 x55 x56 ⟶ False) ⟶ False) ⟶ (∀ x55 x56 . x54 x56 ⟶ x54 x55 ⟶ x53 x56 x55 ⟶ x52 x55 ⟶ (x52 x56 ⟶ False) ⟶ False) ⟶ (∀ x55 . x50 x55 ⟶ (x46 x55 x5 = x5 ⟶ False) ⟶ False) ⟶ (∀ x55 x56 . x54 x56 ⟶ x54 x55 ⟶ x53 (x45 x55) (x45 x56) ⟶ (x53 x56 x55 ⟶ False) ⟶ False) ⟶ (∀ x55 x56 . x54 x56 ⟶ x54 x55 ⟶ x53 x56 x55 ⟶ (x53 (x45 x55) (x45 x56) ⟶ False) ⟶ False) ⟶ (∀ x55 x56 . x1 x56 x55 ⟶ (x4 x56 x55 ⟶ False) ⟶ False) ⟶ (∀ x55 x56 . x54 x56 ⟶ x54 x55 ⟶ x53 x56 x55 ⟶ x51 x56 ⟶ (x51 x55 ⟶ False) ⟶ False) ⟶ ((x4 x2 x44 ⟶ False) ⟶ False) ⟶ (∀ x55 . x50 x55 ⟶ (x7 x55 x5 = x55 ⟶ False) ⟶ False) ⟶ (∀ x55 x56 . x54 x56 ⟶ x54 x55 ⟶ x53 x5 x56 ⟶ (x53 x55 x56 ⟶ False) ⟶ x53 (x43 x55) (x43 x56) ⟶ False) ⟶ (∀ x55 x56 . x50 x56 ⟶ x50 x55 ⟶ (x47 (x45 x56) (x45 x55) = x47 x55 x56 ⟶ False) ⟶ False) ⟶ (∀ x55 x56 . x50 x56 ⟶ x50 x55 ⟶ (x7 (x45 x56) (x45 x55) = x45 (x7 x56 x55) ⟶ False) ⟶ False) ⟶ (∀ x55 x56 x57 . x50 x57 ⟶ x50 x55 ⟶ x50 x56 ⟶ (x46 (x46 x57 x55) x56 = x46 x57 (x46 x55 x56) ⟶ False) ⟶ False) ⟶ (∀ x55 x56 x57 . x50 x57 ⟶ x50 x55 ⟶ x50 x56 ⟶ (x7 (x7 x57 x55) x56 = x7 x57 (x7 x55 x56) ⟶ False) ⟶ False) ⟶ (∀ x55 x56 x57 . x50 x57 ⟶ x50 x55 ⟶ x50 x56 ⟶ (x46 (x7 x57 x55) x56 = x7 (x46 x57 x56) (x46 x55 x56) ⟶ False) ⟶ False) ⟶ (∀ x55 x56 x57 . x50 x57 ⟶ x50 x55 ⟶ x50 x56 ⟶ (x46 x57 (x49 x55 x56) = x49 (x46 x57 x55) x56 ⟶ False) ⟶ False) ⟶ (∀ x55 . x50 x55 ⟶ (x49 x48 x55 = x8 x55 ⟶ False) ⟶ False) ⟶ ((x4 x41 x42 ⟶ False) ⟶ False) ⟶ ((x4 x41 x9 ⟶ False) ⟶ False) ⟶ ((x40 x41 x42 x9 ⟶ False) ⟶ False) ⟶ ((x51 x41 ⟶ False) ⟶ False) ⟶ (x0 x41 ⟶ False) ⟶ (∀ x55 . x50 x55 ⟶ (x46 x55 (x45 x48) = x45 x55 ⟶ False) ⟶ False) ⟶ ((x4 x48 x42 ⟶ False) ⟶ False) ⟶ ((x4 x48 x9 ⟶ False) ⟶ False) ⟶ ((x40 x48 x42 x9 ⟶ False) ⟶ False) ⟶ ((x51 x48 ⟶ False) ⟶ False) ⟶ (x0 x48 ⟶ False) ⟶ (∀ x55 x56 . x50 x56 ⟶ x50 x55 ⟶ (x7 x56 (x45 x55) = x47 x56 x55 ⟶ False) ⟶ False) ⟶ (∀ x55 x56 . x50 x56 ⟶ x50 x55 ⟶ (x46 x56 (x8 x55) = x49 x56 x55 ⟶ False) ⟶ False) ⟶ (∀ x55 x56 . x50 x56 ⟶ x50 x55 ⟶ (x49 (x8 x56) (x8 x55) = x49 x55 x56 ⟶ False) ⟶ False) ⟶ (∀ x55 x56 . x50 x56 ⟶ x50 x55 ⟶ (x46 (x8 x56) (x8 x55) = x8 (x46 x56 x55) ⟶ False) ⟶ False) ⟶ ((x4 x10 x42 ⟶ False) ⟶ False) ⟶ ((x4 x10 x9 ⟶ False) ⟶ False) ⟶ ((x40 x10 x42 x9 ⟶ False) ⟶ False) ⟶ ((x0 x10 ⟶ False) ⟶ False) ⟶ ((x45 (x49 (x45 x48) x41) = x49 x48 x41 ⟶ False) ⟶ False) ⟶ ((x45 (x49 x48 x41) = x49 (x45 x48) x41 ⟶ False) ⟶ False) ⟶ ((x45 (x45 x41) = x41 ⟶ False) ⟶ False) ⟶ ((x45 (x45 x48) = x48 ⟶ False) ⟶ False) ⟶ ((x45 x41 = x45 x41 ⟶ False) ⟶ False) ⟶ ((x45 x48 = x45 x48 ⟶ False) ⟶ False) ⟶ ((x45 x10 = x10 ⟶ False) ⟶ False) ⟶ ((x46 (x49 (x45 x48) x41) (x45 x41) = x48 ⟶ False) ⟶ False) ⟶ ((x46 (x49 (x45 x48) x41) x41 = x45 x48 ⟶ False) ⟶ False) ⟶ ((x46 (x49 (x45 x48) x41) x48 = x49 (x45 x48) x41 ⟶ False) ⟶ False) ⟶ ((x46 (x49 x48 x41) (x45 x41) = x45 x48 ⟶ False) ⟶ False) ⟶ ((x46 (x49 x48 x41) x41 = x48 ⟶ False) ⟶ False) ⟶ ((x46 (x49 x48 x41) x48 = x49 x48 x41 ⟶ False) ⟶ False) ⟶ ((x46 (x49 x48 x41) x10 = x10 ⟶ False) ⟶ False) ⟶ ((x46 (x45 x41) (x49 (x45 x48) x41) = x48 ⟶ False) ⟶ False) ⟶ ((x46 (x45 x41) (x49 x48 x41) = x45 x48 ⟶ False) ⟶ False) ⟶ ((x46 (x45 x41) x48 = x45 x41 ⟶ False) ⟶ False) ⟶ ((x46 (x45 x41) x10 = x10 ⟶ False) ⟶ False) ⟶ ((x46 x41 (x49 (x45 x48) x41) = x45 x48 ⟶ False) ⟶ False) ⟶ ((x46 x41 (x49 x48 x41) = x48 ⟶ False) ⟶ False) ⟶ ((x46 x41 x48 = x41 ⟶ False) ⟶ False) ⟶ ((x46 x41 x10 = x10 ⟶ False) ⟶ False) ⟶ ((x46 x48 (x49 (x45 x48) x41) = x49 (x45 x48) x41 ⟶ False) ⟶ False) ⟶ ((x46 x48 (x49 x48 x41) = x49 x48 x41 ⟶ False) ⟶ False) ⟶ ((x46 x48 (x45 x41) = x45 x41 ⟶ False) ⟶ False) ⟶ ((x46 x48 x41 = x41 ⟶ False) ⟶ False) ⟶ ((x46 x48 x48 = x48 ⟶ False) ⟶ False) ⟶ ((x46 x48 x10 = x10 ⟶ False) ⟶ False) ⟶ ((x46 x10 (x49 x48 x41) = x10 ⟶ False) ⟶ False) ⟶ ((x46 x10 (x45 x41) = x10 ⟶ False) ⟶ False) ⟶ ((x46 x10 x41 = x10 ⟶ False) ⟶ False) ⟶ ((x46 x10 x48 = x10 ⟶ False) ⟶ False) ⟶ ((x46 x10 x10 = x10 ⟶ False) ⟶ False) ⟶ ((x49 (x45 x41) x41 = x45 x48 ⟶ False) ⟶ False) ⟶ ((x49 (x45 x48) x41 = x49 (x45 x48) x41 ⟶ False) ⟶ False) ⟶ ((x49 (x45 x48) x48 = x45 x48 ⟶ False) ⟶ False) ⟶ ((x49 x41 x41 = x48 ⟶ False) ⟶ False) ⟶ ((x49 x41 x48 = x41 ⟶ False) ⟶ False) ⟶ ((x49 x48 (x49 (x45 x48) x41) = x45 x41 ⟶ False) ⟶ False) ⟶ ((x49 x48 (x49 x48 x41) = x41 ⟶ False) ⟶ False) ⟶ ((x49 x48 (x45 x41) = x49 (x45 x48) x41 ⟶ False) ⟶ False) ⟶ ((x49 x48 (x45 x48) = x45 x48 ⟶ False) ⟶ False) ⟶ ((x49 x48 x41 = x49 x48 x41 ⟶ False) ⟶ False) ⟶ ((x49 x48 x48 = x48 ⟶ False) ⟶ False) ⟶ ((x47 (x49 (x45 x48) x41) (x49 (x45 x48) x41) = x10 ⟶ False) ⟶ False) ⟶ ((x47 (x49 (x45 x48) x41) (x49 x48 x41) = x45 x48 ⟶ False) ⟶ False) ⟶ ((x47 (x49 (x45 x48) x41) (x45 x48) = x49 x48 x41 ⟶ False) ⟶ False) ⟶ ((x47 (x49 (x45 x48) x41) x10 = x49 (x45 x48) x41 ⟶ False) ⟶ False) ⟶ ((x47 (x49 x48 x41) (x49 (x45 x48) x41) = x48 ⟶ False) ⟶ False) ⟶ ((x47 (x49 x48 x41) (x49 x48 x41) = x10 ⟶ False) ⟶ False) ⟶ ((x47 (x49 x48 x41) x48 = x49 (x45 x48) x41 ⟶ False) ⟶ False) ⟶ ((x47 (x49 x48 x41) x10 = x49 x48 x41 ⟶ False) ⟶ False) ⟶ ((x47 (x45 x41) (x45 x41) = x10 ⟶ False) ⟶ False) ⟶ ((x47 (x45 x41) (x45 x48) = x45 x48 ⟶ False) ⟶ False) ⟶ ((x47 (x45 x41) x10 = x45 x41 ⟶ False) ⟶ False) ⟶ ((x47 (x45 x48) (x49 (x45 x48) x41) = x49 (x45 x48) x41 ⟶ False) ⟶ False) ⟶ ((x47 (x45 x48) (x45 x41) = x48 ⟶ False) ⟶ False) ⟶ ((x47 (x45 x48) (x45 x48) = x10 ⟶ False) ⟶ False) ⟶ ((x47 (x45 x48) x48 = x45 x41 ⟶ False) ⟶ False) ⟶ ((x47 (x45 x48) x10 = x45 x48 ⟶ False) ⟶ False) ⟶ ((x47 x41 x41 = x10 ⟶ False) ⟶ False) ⟶ ((x47 x41 x48 = x48 ⟶ False) ⟶ False) ⟶ ((x47 x41 x10 = x41 ⟶ False) ⟶ False) ⟶ ((x47 x48 (x49 x48 x41) = x49 x48 x41 ⟶ False) ⟶ False) ⟶ ((x47 x48 (x45 x48) = x41 ⟶ False) ⟶ False) ⟶ ((x47 x48 x41 = x45 x48 ⟶ False) ⟶ False) ⟶ ((x47 x48 x48 = x10 ⟶ False) ⟶ False) ⟶ ((x47 x48 x10 = x48 ⟶ False) ⟶ False) ⟶ ((x47 x10 (x49 (x45 x48) x41) = x49 x48 x41 ⟶ False) ⟶ False) ⟶ ((x47 x10 (x49 x48 x41) = x49 (x45 x48) x41 ⟶ False) ⟶ False) ⟶ ((x47 x10 (x45 x41) = x41 ⟶ False) ⟶ False) ⟶ ((x47 x10 (x45 x48) = x48 ⟶ False) ⟶ False) ⟶ ((x47 x10 x41 = x45 x41 ⟶ False) ⟶ False) ⟶ ((x47 x10 x48 = x45 x48 ⟶ False) ⟶ False) ⟶ ((x47 x10 x10 = x10 ⟶ False) ⟶ False) ⟶ ((x7 (x49 (x45 x48) x41) (x49 (x45 x48) x41) = x45 x48 ⟶ False) ⟶ False) ⟶ ((x7 (x49 (x45 x48) x41) (x49 x48 x41) = x10 ⟶ False) ⟶ False) ⟶ ((x7 (x49 (x45 x48) x41) x48 = x49 x48 x41 ⟶ False) ⟶ False) ⟶ ((x7 (x49 x48 x41) (x49 (x45 x48) x41) = x10 ⟶ False) ⟶ False) ⟶ ((x7 (x49 x48 x41) (x49 x48 x41) = x48 ⟶ False) ⟶ False) ⟶ ((x7 (x49 x48 x41) (x45 x48) = x49 (x45 x48) x41 ⟶ False) ⟶ False) ⟶ ((x7 (x49 x48 x41) x10 = x49 x48 x41 ⟶ False) ⟶ False) ⟶ ((x7 (x45 x41) x41 = x10 ⟶ False) ⟶ False) ⟶ ((x7 (x45 x41) x48 = x45 x48 ⟶ False) ⟶ False) ⟶ ((x7 (x45 x48) (x49 x48 x41) = x49 (x45 x48) x41 ⟶ False) ⟶ False) ⟶ ((x7 (x45 x48) (x45 x48) = x45 x41 ⟶ False) ⟶ False) ⟶ ((x7 (x45 x48) x41 = x48 ⟶ False) ⟶ False) ⟶ ((x7 (x45 x48) x48 = x10 ⟶ False) ⟶ False) ⟶ ((x7 (x45 x48) x10 = x45 x48 ⟶ False) ⟶ False) ⟶ ((x7 x41 (x45 x41) = x10 ⟶ False) ⟶ False) ⟶ ((x7 x41 (x45 x48) = x48 ⟶ False) ⟶ False) ⟶ ((x7 x41 x10 = x41 ⟶ False) ⟶ False) ⟶ ((x7 x48 (x49 (x45 x48) x41) = x49 x48 x41 ⟶ False) ⟶ False) ⟶ ((x7 x48 (x45 x41) = x45 x48 ⟶ False) ⟶ False) ⟶ ((x7 x48 (x45 x48) = x10 ⟶ False) ⟶ False) ⟶ ((x7 x48 x48 = x41 ⟶ False) ⟶ False) ⟶ ((x7 x48 x10 = x48 ⟶ False) ⟶ False) ⟶ ((x7 x10 (x49 (x45 x48) x41) = x49 (x45 x48) x41 ⟶ False) ⟶ False) ⟶ ((x7 x10 (x49 x48 x41) = x49 x48 x41 ⟶ False) ⟶ False) ⟶ ((x7 x10 (x45 x41) = x45 x41 ⟶ False) ⟶ False) ⟶ ((x7 x10 (x45 x48) = x45 x48 ⟶ False) ⟶ False) ⟶ ((x7 x10 x41 = x41 ⟶ False) ⟶ False) ⟶ ((x7 x10 x48 = x48 ⟶ False) ⟶ False) ⟶ ((x7 x10 x10 = x10 ⟶ False) ⟶ False) ⟶ ((x53 (x49 (x45 x48) x41) (x49 (x45 x48) x41) ⟶ False) ⟶ False) ⟶ ((x53 (x49 (x45 x48) x41) (x49 x48 x41) ⟶ False) ⟶ False) ⟶ (x53 (x49 (x45 x48) x41) (x45 x48) ⟶ False) ⟶ ((x53 (x49 (x45 x48) x41) x41 ⟶ False) ⟶ False) ⟶ ((x53 (x49 (x45 x48) x41) x48 ⟶ False) ⟶ False) ⟶ ((x53 (x49 (x45 x48) x41) x10 ⟶ False) ⟶ False) ⟶ (x53 (x49 x48 x41) (x49 (x45 x48) x41) ⟶ False) ⟶ ((x53 (x49 x48 x41) (x49 x48 x41) ⟶ False) ⟶ False) ⟶ (x53 (x49 x48 x41) (x45 x41) ⟶ False) ⟶ (x53 (x49 x48 x41) (x45 x48) ⟶ False) ⟶ ((x53 (x49 x48 x41) x41 ⟶ False) ⟶ False) ⟶ ((x53 (x49 x48 x41) x48 ⟶ False) ⟶ False) ⟶ (x53 (x49 x48 x41) x10 ⟶ False) ⟶ ((x53 (x45 x41) (x49 x48 x41) ⟶ False) ⟶ False) ⟶ ((x53 (x45 x41) (x45 x41) ⟶ False) ⟶ False) ⟶ ((x53 (x45 x41) (x45 x48) ⟶ False) ⟶ False) ⟶ ((x53 (x45 x41) x41 ⟶ False) ⟶ False) ⟶ ((x53 (x45 x41) x48 ⟶ False) ⟶ False) ⟶ ((x53 (x45 x41) x10 ⟶ False) ⟶ False) ⟶ ((x53 (x45 x48) (x49 (x45 x48) x41) ⟶ False) ⟶ False) ⟶ ((x53 (x45 x48) (x49 x48 x41) ⟶ False) ⟶ False) ⟶ (x53 (x45 x48) (x45 x41) ⟶ False) ⟶ ((x53 (x45 x48) (x45 x48) ⟶ False) ⟶ False) ⟶ ((x53 (x45 x48) x41 ⟶ False) ⟶ False) ⟶ ((x53 (x45 x48) x48 ⟶ False) ⟶ False) ⟶ ((x53 (x45 x48) x10 ⟶ False) ⟶ False) ⟶ (x53 x41 (x49 (x45 x48) x41) ⟶ False) ⟶ (x53 x41 (x49 x48 x41) ⟶ False) ⟶ (x53 x41 (x45 x41) ⟶ False) ⟶ (x53 x41 (x45 x48) ⟶ False) ⟶ ((x53 x41 x41 ⟶ False) ⟶ False) ⟶ (x53 x41 x48 ⟶ False) ⟶ (x53 x41 x10 ⟶ False) ⟶ (x53 x48 (x49 (x45 x48) x41) ⟶ False) ⟶ (x53 x48 (x49 x48 x41) ⟶ False) ⟶ (x53 x48 (x45 x41) ⟶ False) ⟶ (x53 x48 (x45 x48) ⟶ False) ⟶ ((x53 x48 x41 ⟶ False) ⟶ False) ⟶ ((x53 x48 x48 ⟶ False) ⟶ False) ⟶ (x53 x48 x10 ⟶ False) ⟶ (x53 x10 (x49 (x45 x48) x41) ⟶ False) ⟶ ((x53 x10 (x49 x48 x41) ⟶ False) ⟶ False) ⟶ (x53 x10 (x45 x41) ⟶ False) ⟶ (x53 x10 (x45 x48) ⟶ False) ⟶ ((x53 x10 x41 ⟶ False) ⟶ False) ⟶ ((x53 x10 x48 ⟶ False) ⟶ False) ⟶ ((x53 x10 x10 ⟶ False) ⟶ False) ⟶ (∀ x55 x56 . x39 x56 ⟶ x39 x55 ⟶ (x53 x56 x56 ⟶ False) ⟶ False) ⟶ (∀ x55 . (x6 x55 x55 ⟶ False) ⟶ False) ⟶ (∀ x55 x56 x57 . (x0 x57 ⟶ False) ⟶ (x0 x55 ⟶ False) ⟶ x4 x55 (x3 x57) ⟶ x4 x56 x55 ⟶ (x40 x56 x57 x55 ⟶ False) ⟶ False) ⟶ (∀ x55 x56 x57 . (x0 x57 ⟶ False) ⟶ (x0 x55 ⟶ False) ⟶ x4 x55 (x3 x57) ⟶ x40 x56 x57 x55 ⟶ (x4 x56 x55 ⟶ False) ⟶ False) ⟶ ((x5 = x2 ⟶ False) ⟶ False) ⟶ ((x9 = x44 ⟶ False) ⟶ False) ⟶ ((x38 x37 ⟶ False) ⟶ False) ⟶ (x0 x37 ⟶ False) ⟶ ((x39 x36 ⟶ False) ⟶ False) ⟶ ((x0 x36 ⟶ False) ⟶ False) ⟶ ((x54 x35 ⟶ False) ⟶ False) ⟶ ((x39 x35 ⟶ False) ⟶ False) ⟶ ((x50 x35 ⟶ False) ⟶ False) ⟶ ((x0 x35 ⟶ False) ⟶ False) ⟶ ((x38 x34 ⟶ False) ⟶ False) ⟶ ((x52 x11 ⟶ False) ⟶ False) ⟶ ((x39 x11 ⟶ False) ⟶ False) ⟶ ((x54 x12 ⟶ False) ⟶ False) ⟶ ((x52 x12 ⟶ False) ⟶ False) ⟶ ((x39 x12 ⟶ False) ⟶ False) ⟶ ((x50 x12 ⟶ False) ⟶ False) ⟶ ((x51 x13 ⟶ False) ⟶ False) ⟶ ((x39 x13 ⟶ False) ⟶ False) ⟶ ((x54 x14 ⟶ False) ⟶ False) ⟶ ((x51 x14 ⟶ False) ⟶ False) ⟶ ((x39 x14 ⟶ False) ⟶ False) ⟶ ((x50 x14 ⟶ False) ⟶ False) ⟶ ((x50 x15 ⟶ False) ⟶ False) ⟶ (x0 x15 ⟶ False) ⟶ (x0 x16 ⟶ False) ⟶ ((x33 x32 ⟶ False) ⟶ False) ⟶ ((x17 x32 ⟶ False) ⟶ False) ⟶ ((x31 x32 ⟶ False) ⟶ False) ⟶ (x0 x32 ⟶ False) ⟶ ((x39 x30 ⟶ False) ⟶ False) ⟶ ((x54 x18 ⟶ False) ⟶ False) ⟶ ((x50 x29 ⟶ False) ⟶ False) ⟶ ((x0 x19 ⟶ False) ⟶ False) ⟶ ((x54 x28 ⟶ False) ⟶ False) ⟶ ((x51 x28 ⟶ False) ⟶ False) ⟶ ((x39 x28 ⟶ False) ⟶ False) ⟶ ((x50 x28 ⟶ False) ⟶ False) ⟶ ((x4 x28 x42 ⟶ False) ⟶ False) ⟶ ((x33 x20 ⟶ False) ⟶ False) ⟶ (∀ x55 . x50 x55 ⟶ (x8 (x8 x55) = x55 ⟶ False) ⟶ False) ⟶ (∀ x55 . x50 x55 ⟶ (x45 (x45 x55) = x55 ⟶ False) ⟶ False) ⟶ (∀ x55 x56 . (x52 x56 ⟶ False) ⟶ x54 x56 ⟶ (x52 x55 ⟶ False) ⟶ x54 x55 ⟶ x52 (x7 x56 x55) ⟶ False) ⟶ (∀ x55 x56 . (x0 x56 ⟶ False) ⟶ x50 x56 ⟶ (x0 x55 ⟶ False) ⟶ x50 x55 ⟶ x0 (x49 x56 x55) ⟶ False) ⟶ (∀ x55 x56 . x54 x56 ⟶ x54 x55 ⟶ (x54 (x49 x56 x55) ⟶ False) ⟶ False) ⟶ (∀ x55 x56 . (x0 x56 ⟶ False) ⟶ x50 x56 ⟶ (x0 x55 ⟶ False) ⟶ x50 x55 ⟶ x0 (x46 x56 x55) ⟶ False) ⟶ (x27 x42 ⟶ False) ⟶ (∀ x55 x56 . x54 x56 ⟶ x54 x55 ⟶ (x54 (x47 x56 x55) ⟶ False) ⟶ False) ⟶ (∀ x55 . (x0 x55 ⟶ False) ⟶ x50 x55 ⟶ (x50 (x8 x55) ⟶ False) ⟶ False) ⟶ (∀ x55 . (x0 x55 ⟶ False) ⟶ x50 x55 ⟶ x0 (x8 x55) ⟶ False) ⟶ (∀ x55 x56 . x54 x56 ⟶ x54 x55 ⟶ (x54 (x46 x56 x55) ⟶ False) ⟶ False) ⟶ (∀ x55 . (x0 x55 ⟶ False) ⟶ x50 x55 ⟶ (x50 (x45 x55) ⟶ False) ⟶ False) ⟶ (∀ x55 . (x0 x55 ⟶ False) ⟶ x50 x55 ⟶ x0 (x45 x55) ⟶ False) ⟶ ((x33 x44 ⟶ False) ⟶ False) ⟶ (x0 x44 ⟶ False) ⟶ (∀ x55 x56 . x54 x56 ⟶ x54 x55 ⟶ (x54 (x7 x56 x55) ⟶ False) ⟶ False) ⟶ (∀ x55 x56 . x50 x56 ⟶ x50 x55 ⟶ (x50 (x49 x56 x55) ⟶ False) ⟶ False) ⟶ (∀ x55 . x54 x55 ⟶ (x54 (x8 x55) ⟶ False) ⟶ False) ⟶ (∀ x55 . x54 x55 ⟶ (x50 (x8 x55) ⟶ False) ⟶ False) ⟶ (∀ x55 x56 . x50 x56 ⟶ x50 x55 ⟶ (x50 (x47 x56 x55) ⟶ False) ⟶ False) ⟶ (∀ x55 . x54 x55 ⟶ (x54 (x45 x55) ⟶ False) ⟶ False) ⟶ (∀ x55 . x54 x55 ⟶ (x50 (x45 x55) ⟶ False) ⟶ False) ⟶ (∀ x55 x56 . x50 x56 ⟶ x50 x55 ⟶ (x50 (x46 x56 x55) ⟶ False) ⟶ False) ⟶ (∀ x55 x56 . (x51 x56 ⟶ False) ⟶ x54 x56 ⟶ (x51 x55 ⟶ False) ⟶ x54 x55 ⟶ x52 (x49 x56 x55) ⟶ False) ⟶ (∀ x55 x56 . (x52 x56 ⟶ False) ⟶ x54 x56 ⟶ (x52 x55 ⟶ False) ⟶ x54 x55 ⟶ x52 (x49 x56 x55) ⟶ False) ⟶ (∀ x55 x56 . (x52 x56 ⟶ False) ⟶ x54 x56 ⟶ (x51 x55 ⟶ False) ⟶ x54 x55 ⟶ x51 (x49 x55 x56) ⟶ False) ⟶ (∀ x55 x56 . (x52 x56 ⟶ False) ⟶ x54 x56 ⟶ (x51 x55 ⟶ False) ⟶ x54 x55 ⟶ x51 (x49 x56 x55) ⟶ False) ⟶ (∀ x55 . (x52 x55 ⟶ False) ⟶ x54 x55 ⟶ x52 (x8 x55) ⟶ False) ⟶ (∀ x55 . (x52 x55 ⟶ False) ⟶ x54 x55 ⟶ (x50 (x8 x55) ⟶ False) ⟶ False) ⟶ (∀ x55 x56 . x50 x56 ⟶ x50 x55 ⟶ (x50 (x7 x56 x55) ⟶ False) ⟶ False) ⟶ (∀ x55 . x54 x55 ⟶ (x54 (x43 x55) ⟶ False) ⟶ False) ⟶ (∀ x55 . x52 x55 ⟶ x54 x55 ⟶ (x52 (x8 x55) ⟶ False) ⟶ False) ⟶ (∀ x55 . x52 x55 ⟶ x54 x55 ⟶ (x50 (x8 x55) ⟶ False) ⟶ False) ⟶ (∀ x55 . (x51 x55 ⟶ False) ⟶ x54 x55 ⟶ x51 (x8 x55) ⟶ False) ⟶ (∀ x55 . (x51 x55 ⟶ False) ⟶ x54 x55 ⟶ (x50 (x8 x55) ⟶ False) ⟶ False) ⟶ (∀ x55 . x51 x55 ⟶ x54 x55 ⟶ (x51 (x8 x55) ⟶ False) ⟶ False) ⟶ (∀ x55 . x51 x55 ⟶ x54 x55 ⟶ (x50 (x8 x55) ⟶ False) ⟶ False) ⟶ (∀ x55 x56 . (x52 x56 ⟶ False) ⟶ x54 x56 ⟶ (x52 x55 ⟶ False) ⟶ x54 x55 ⟶ x52 (x46 x56 x55) ⟶ False) ⟶ (∀ x55 x56 . (x51 x56 ⟶ False) ⟶ x54 x56 ⟶ (x51 x55 ⟶ False) ⟶ x54 x55 ⟶ x52 (x46 x56 x55) ⟶ False) ⟶ (∀ x55 x56 . (x51 x56 ⟶ False) ⟶ x54 x56 ⟶ (x52 x55 ⟶ False) ⟶ x54 x55 ⟶ x51 (x46 x55 x56) ⟶ False) ⟶ (∀ x55 x56 . (x51 x56 ⟶ False) ⟶ x54 x56 ⟶ (x52 x55 ⟶ False) ⟶ x54 x55 ⟶ x51 (x46 x56 x55) ⟶ False) ⟶ (∀ x55 x56 . x52 x56 ⟶ x54 x56 ⟶ (x52 x55 ⟶ False) ⟶ x54 x55 ⟶ (x51 (x47 x55 x56) ⟶ False) ⟶ False) ⟶ (∀ x55 x56 . x52 x56 ⟶ x54 x56 ⟶ (x52 x55 ⟶ False) ⟶ x54 x55 ⟶ (x52 (x47 x56 x55) ⟶ False) ⟶ False) ⟶ (∀ x55 x56 . x51 x56 ⟶ x54 x56 ⟶ (x51 x55 ⟶ False) ⟶ x54 x55 ⟶ (x52 (x47 x55 x56) ⟶ False) ⟶ False) ⟶ ((x0 x2 ⟶ False) ⟶ False) ⟶ (∀ x55 . x50 x55 ⟶ (x50 (x43 x55) ⟶ False) ⟶ False) ⟶ (x0 x42 ⟶ False) ⟶ (∀ x55 x56 . x51 x56 ⟶ x54 x56 ⟶ (x51 x55 ⟶ False) ⟶ x54 x55 ⟶ (x51 (x47 x56 x55) ⟶ False) ⟶ False) ⟶ (∀ x55 x56 . (x52 x56 ⟶ False) ⟶ x54 x56 ⟶ (x51 x55 ⟶ False) ⟶ x54 x55 ⟶ x51 (x47 x55 x56) ⟶ False) ⟶ (∀ x55 x56 . (x52 x56 ⟶ False) ⟶ x54 x56 ⟶ (x51 x55 ⟶ False) ⟶ x54 x55 ⟶ x52 (x47 x56 x55) ⟶ False) ⟶ (∀ x55 . (x52 x55 ⟶ False) ⟶ x54 x55 ⟶ x51 (x45 x55) ⟶ False) ⟶ (∀ x55 . (x52 x55 ⟶ False) ⟶ x54 x55 ⟶ (x50 (x45 x55) ⟶ False) ⟶ False) ⟶ (∀ x55 . (x51 x55 ⟶ False) ⟶ x54 x55 ⟶ x52 (x45 x55) ⟶ False) ⟶ (∀ x55 . (x51 x55 ⟶ False) ⟶ x54 x55 ⟶ (x50 (x45 x55) ⟶ False) ⟶ False) ⟶ (∀ x55 x56 . x52 x56 ⟶ x54 x56 ⟶ (x51 x55 ⟶ False) ⟶ x54 x55 ⟶ (x52 (x7 x55 x56) ⟶ False) ⟶ False) ⟶ (∀ x55 x56 . x52 x56 ⟶ x54 x56 ⟶ (x51 x55 ⟶ False) ⟶ x54 x55 ⟶ (x52 (x7 x56 x55) ⟶ False) ⟶ False) ⟶ (∀ x55 x56 . x51 x56 ⟶ x54 x56 ⟶ (x52 x55 ⟶ False) ⟶ x54 x55 ⟶ (x51 (x7 x55 x56) ⟶ False) ⟶ False) ⟶ (∀ x55 x56 . x51 x56 ⟶ x54 x56 ⟶ (x52 x55 ⟶ False) ⟶ x54 x55 ⟶ (x51 (x7 x56 x55) ⟶ False) ⟶ False) ⟶ (∀ x55 x56 . (x51 x56 ⟶ False) ⟶ x54 x56 ⟶ (x51 x55 ⟶ False) ⟶ x54 x55 ⟶ x51 (x7 x56 x55) ⟶ False) ⟶ (∀ x55 x56 . (x0 x56 ⟶ False) ⟶ (x0 x55 ⟶ False) ⟶ x4 x55 (x3 x56) ⟶ (x40 (x21 x55 x56) x56 x55 ⟶ False) ⟶ False) ⟶ (∀ x55 . (x4 (x26 x55) x55 ⟶ False) ⟶ False) ⟶ (∀ x55 x56 x57 . (x0 x57 ⟶ False) ⟶ (x0 x55 ⟶ False) ⟶ x4 x55 (x3 x57) ⟶ x40 x56 x57 x55 ⟶ (x4 x56 x57 ⟶ False) ⟶ False) ⟶ ((x40 x5 x42 x9 ⟶ False) ⟶ False) ⟶ (∀ x55 . x50 x55 ⟶ (x50 (x8 x55) ⟶ False) ⟶ False) ⟶ ((x4 x9 (x3 x42) ⟶ False) ⟶ False) ⟶ (∀ x55 . x50 x55 ⟶ (x50 (x45 x55) ⟶ False) ⟶ False) ⟶ (∀ x55 x56 . x50 x56 ⟶ x50 x55 ⟶ (x49 x56 x55 = x46 x56 (x8 x55) ⟶ False) ⟶ False) ⟶ (∀ x55 x56 . x50 x56 ⟶ x50 x55 ⟶ (x47 x56 x55 = x7 x56 (x45 x55) ⟶ False) ⟶ False) ⟶ (∀ x55 . x50 x55 ⟶ (x43 x55 = x46 x55 x55 ⟶ False) ⟶ False) ⟶ (∀ x55 x56 . x39 x56 ⟶ x39 x55 ⟶ (x53 x56 x55 ⟶ False) ⟶ (x53 x55 x56 ⟶ False) ⟶ False) ⟶ (∀ x55 x56 . x50 x56 ⟶ x50 x55 ⟶ (x46 x56 x55 = x46 x55 x56 ⟶ False) ⟶ False) ⟶ (∀ x55 x56 . x50 x56 ⟶ x50 x55 ⟶ (x7 x56 x55 = x7 x55 x56 ⟶ False) ⟶ False) ⟶ (∀ x55 . x0 x55 ⟶ (x25 x55 ⟶ False) ⟶ False) ⟶ (∀ x55 . x39 x55 ⟶ (x51 x55 ⟶ False) ⟶ (x52 x55 ⟶ False) ⟶ (x39 x55 ⟶ False) ⟶ False) ⟶ (∀ x55 . x39 x55 ⟶ (x51 x55 ⟶ False) ⟶ (x52 x55 ⟶ False) ⟶ (x0 x55 ⟶ False) ⟶ False) ⟶ (∀ x55 . x4 x55 x44 ⟶ (x38 x55 ⟶ False) ⟶ False) ⟶ (∀ x55 . x0 x55 ⟶ x39 x55 ⟶ x52 x55 ⟶ False) ⟶ (∀ x55 . x0 x55 ⟶ x39 x55 ⟶ x51 x55 ⟶ False) ⟶ (∀ x55 . x0 x55 ⟶ x39 x55 ⟶ (x39 x55 ⟶ False) ⟶ False) ⟶ (∀ x55 . x0 x55 ⟶ (x38 x55 ⟶ False) ⟶ False) ⟶ (∀ x55 . (x0 x55 ⟶ False) ⟶ x39 x55 ⟶ (x51 x55 ⟶ False) ⟶ (x52 x55 ⟶ False) ⟶ False) ⟶ (∀ x55 . (x0 x55 ⟶ False) ⟶ x39 x55 ⟶ (x51 x55 ⟶ False) ⟶ (x39 x55 ⟶ False) ⟶ False) ⟶ (∀ x55 . x38 x55 ⟶ (x33 x55 ⟶ False) ⟶ False) ⟶ (∀ x55 . x39 x55 ⟶ x52 x55 ⟶ x51 x55 ⟶ False) ⟶ (∀ x55 . x39 x55 ⟶ x52 x55 ⟶ (x39 x55 ⟶ False) ⟶ False) ⟶ (∀ x55 . x39 x55 ⟶ x52 x55 ⟶ x0 x55 ⟶ False) ⟶ (∀ x55 x56 . x33 x56 ⟶ x4 x55 x56 ⟶ (x33 x55 ⟶ False) ⟶ False) ⟶ (∀ x55 . (x0 x55 ⟶ False) ⟶ x39 x55 ⟶ (x52 x55 ⟶ False) ⟶ (x51 x55 ⟶ False) ⟶ False) ⟶ (∀ x55 . (x0 x55 ⟶ False) ⟶ x39 x55 ⟶ (x52 x55 ⟶ False) ⟶ (x39 x55 ⟶ False) ⟶ False) ⟶ (∀ x55 . x54 x55 ⟶ (x39 x55 ⟶ False) ⟶ False) ⟶ (∀ x55 . x0 x55 ⟶ (x24 x55 ⟶ False) ⟶ False) ⟶ (∀ x55 . x39 x55 ⟶ x51 x55 ⟶ x52 x55 ⟶ False) ⟶ (∀ x55 . x39 x55 ⟶ x51 x55 ⟶ (x39 x55 ⟶ False) ⟶ False) ⟶ (∀ x55 . x39 x55 ⟶ x51 x55 ⟶ x0 x55 ⟶ False) ⟶ (∀ x55 . x54 x55 ⟶ (x50 x55 ⟶ False) ⟶ False) ⟶ (∀ x55 . x0 x55 ⟶ (x33 x55 ⟶ False) ⟶ False) ⟶ (∀ x55 . x38 x55 ⟶ (x39 x55 ⟶ False) ⟶ False) ⟶ (∀ x55 . x38 x55 ⟶ (x54 x55 ⟶ False) ⟶ False) ⟶ (∀ x55 . x38 x55 ⟶ (x50 x55 ⟶ False) ⟶ False) ⟶ (∀ x55 . x31 x55 ⟶ x17 x55 ⟶ (x33 x55 ⟶ False) ⟶ False) ⟶ (∀ x55 . x4 x55 x42 ⟶ (x54 x55 ⟶ False) ⟶ False) ⟶ (∀ x55 . x4 x55 x42 ⟶ (x50 x55 ⟶ False) ⟶ False) ⟶ (∀ x55 . x4 x55 x42 ⟶ (x54 x55 ⟶ False) ⟶ False) ⟶ (∀ x55 . x33 x55 ⟶ (x17 x55 ⟶ False) ⟶ False) ⟶ (∀ x55 . x33 x55 ⟶ (x31 x55 ⟶ False) ⟶ False) ⟶ (∀ x55 x56 . x25 x56 ⟶ x4 x55 (x3 x56) ⟶ (x25 x55 ⟶ False) ⟶ False) ⟶ (∀ x55 x56 . x1 x55 x56 ⟶ x1 x56 x55 ⟶ False) ⟶ (x53 (x45 x22) x23 ⟶ x53 x23 x22 ⟶ False) ⟶ ((x53 x5 x22 ⟶ False) ⟶ False) ⟶ ((x53 (x43 x23) (x43 x22) ⟶ False) ⟶ False) ⟶ ((x54 x22 ⟶ False) ⟶ False) ⟶ ((x54 x23 ⟶ False) ⟶ False) ⟶ False (proof)