Search for blocks/addresses/...

Proofgold Asset

asset id
484320ea69deb850aa19c747e55a2cfcd82fda6c8b0c6daf27a115e6a1254a57
asset hash
65f794bc9cb51a89209d9766d0226138fadf18e3f8ee8bab9fad44bb15cadc40
bday / block
35132
tx
c3f71..
preasset
doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 2883e.. : ∀ 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 x56 x57 . x49 x57 ⟶ x49 x54 ⟶ x49 x56 ⟶ x49 x55 ⟶ (x48 (x47 x57 x54) (x47 x56 x55) = x47 (x48 x57 x56) (x48 x54 x55) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 x56 . x53 x56 ⟶ x53 x54 ⟶ x53 x55 ⟶ (x52 x56 x2 ⟶ False) ⟶ (x52 x55 x54 ⟶ False) ⟶ x52 (x47 x55 x56) (x47 x54 x56) ⟶ False) ⟶ (∀ x54 x55 . x53 x55 ⟶ x53 x54 ⟶ x52 x55 x54 ⟶ (x0 x55 ⟶ False) ⟶ (x50 x54 ⟶ False) ⟶ (x51 x55 ⟶ False) ⟶ False) ⟶ (∀ x54 . x0 x54 ⟶ (x54 = x3 ⟶ False) ⟶ False) ⟶ (∀ x54 . x49 x54 ⟶ (x47 x54 x46 = x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x49 x54 ⟶ (x54 = x2 ⟶ False) ⟶ (x47 x54 x54 = x46 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 x56 . x1 x54 x55 ⟶ x44 x55 (x45 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 ⟶ (x47 x2 x54 = x2 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 x56 . x1 x55 x56 ⟶ x44 x56 (x45 x54) ⟶ (x44 x55 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x53 x55 ⟶ x53 x54 ⟶ x52 x55 x54 ⟶ (x50 x54 ⟶ False) ⟶ x50 x55 ⟶ False) ⟶ (∀ x54 . x49 x54 ⟶ (x4 x54 x2 = x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x43 x55 x54 ⟶ (x44 x55 (x45 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x44 x55 (x45 x54) ⟶ (x43 x55 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x53 x55 ⟶ x53 x54 ⟶ x52 x55 x54 ⟶ (x51 x55 ⟶ False) ⟶ x51 x54 ⟶ False) ⟶ (∀ x54 . x49 x54 ⟶ (x48 x46 x54 = x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x44 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 ⟶ (x48 x54 x2 = x2 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x1 x55 x54 ⟶ (x44 x55 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x53 x55 ⟶ x53 x54 ⟶ x52 x55 x54 ⟶ x50 x55 ⟶ (x50 x54 ⟶ False) ⟶ False) ⟶ ((x44 x3 x5 ⟶ False) ⟶ False) ⟶ (∀ x54 . x49 x54 ⟶ (x42 x54 x2 = x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x49 x55 ⟶ x49 x54 ⟶ (x4 (x6 x55) (x6 x54) = x4 x54 x55 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x49 x55 ⟶ x49 x54 ⟶ (x42 (x6 x55) (x6 x54) = x6 (x42 x55 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 x56 . x49 x56 ⟶ x49 x54 ⟶ x49 x55 ⟶ (x48 (x48 x56 x54) x55 = x48 x56 (x48 x54 x55) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 x56 . x49 x56 ⟶ x49 x54 ⟶ x49 x55 ⟶ (x42 (x42 x56 x54) x55 = x42 x56 (x42 x54 x55) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 x56 . x49 x56 ⟶ x49 x54 ⟶ x49 x55 ⟶ (x48 (x42 x56 x54) x55 = x42 (x48 x56 x55) (x48 x54 x55) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 x56 . x49 x56 ⟶ x49 x54 ⟶ x49 x55 ⟶ (x48 x56 (x47 x54 x55) = x47 (x48 x56 x54) x55 ⟶ False) ⟶ False) ⟶ (∀ x54 . x49 x54 ⟶ (x47 x46 x54 = x7 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x49 x54 ⟶ (x48 x54 (x6 x46) = x6 x54 ⟶ False) ⟶ False) ⟶ ((x44 x46 x8 ⟶ False) ⟶ False) ⟶ ((x44 x46 x41 ⟶ False) ⟶ False) ⟶ ((x9 x46 x8 x41 ⟶ False) ⟶ False) ⟶ ((x50 x46 ⟶ False) ⟶ False) ⟶ (x0 x46 ⟶ False) ⟶ (∀ x54 x55 . x49 x55 ⟶ x49 x54 ⟶ (x42 x55 (x6 x54) = x4 x55 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x49 x55 ⟶ x49 x54 ⟶ (x48 x55 (x7 x54) = x47 x55 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x49 x55 ⟶ x49 x54 ⟶ (x47 (x7 x55) (x7 x54) = x47 x54 x55 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x49 x55 ⟶ x49 x54 ⟶ (x48 (x7 x55) (x7 x54) = x7 (x48 x55 x54) ⟶ False) ⟶ False) ⟶ ((x44 x40 x8 ⟶ False) ⟶ False) ⟶ ((x44 x40 x41 ⟶ False) ⟶ False) ⟶ ((x9 x40 x8 x41 ⟶ False) ⟶ False) ⟶ ((x0 x40 ⟶ False) ⟶ False) ⟶ ((x6 (x6 x46) = x46 ⟶ False) ⟶ False) ⟶ ((x6 x46 = x6 x46 ⟶ False) ⟶ False) ⟶ ((x6 x40 = x40 ⟶ False) ⟶ False) ⟶ ((x48 x46 x46 = x46 ⟶ False) ⟶ False) ⟶ ((x48 x46 x40 = x40 ⟶ False) ⟶ False) ⟶ ((x48 x40 x46 = x40 ⟶ False) ⟶ False) ⟶ ((x48 x40 x40 = x40 ⟶ False) ⟶ False) ⟶ ((x47 (x6 x46) x46 = x6 x46 ⟶ False) ⟶ False) ⟶ ((x47 x46 (x6 x46) = x6 x46 ⟶ False) ⟶ False) ⟶ ((x47 x46 x46 = x46 ⟶ False) ⟶ False) ⟶ ((x4 (x6 x46) (x6 x46) = x40 ⟶ False) ⟶ False) ⟶ ((x4 (x6 x46) x40 = x6 x46 ⟶ False) ⟶ False) ⟶ ((x4 x46 x46 = x40 ⟶ False) ⟶ False) ⟶ ((x4 x46 x40 = x46 ⟶ False) ⟶ False) ⟶ ((x4 x40 (x6 x46) = x46 ⟶ False) ⟶ False) ⟶ ((x4 x40 x46 = x6 x46 ⟶ False) ⟶ False) ⟶ ((x4 x40 x40 = x40 ⟶ False) ⟶ False) ⟶ ((x42 (x6 x46) x46 = x40 ⟶ False) ⟶ False) ⟶ ((x42 (x6 x46) x40 = x6 x46 ⟶ False) ⟶ False) ⟶ ((x42 x46 (x6 x46) = x40 ⟶ False) ⟶ False) ⟶ ((x42 x46 x40 = x46 ⟶ False) ⟶ False) ⟶ ((x42 x40 (x6 x46) = x6 x46 ⟶ False) ⟶ False) ⟶ ((x42 x40 x46 = x46 ⟶ False) ⟶ False) ⟶ ((x42 x40 x40 = x40 ⟶ False) ⟶ False) ⟶ ((x52 (x6 x46) (x6 x46) ⟶ False) ⟶ False) ⟶ ((x52 (x6 x46) x46 ⟶ False) ⟶ False) ⟶ ((x52 (x6 x46) x40 ⟶ False) ⟶ False) ⟶ (x52 x46 (x6 x46) ⟶ False) ⟶ ((x52 x46 x46 ⟶ False) ⟶ False) ⟶ (x52 x46 x40 ⟶ False) ⟶ (x52 x40 (x6 x46) ⟶ False) ⟶ ((x52 x40 x46 ⟶ False) ⟶ False) ⟶ ((x52 x40 x40 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x10 x55 ⟶ x10 x54 ⟶ (x52 x55 x55 ⟶ False) ⟶ False) ⟶ (∀ x54 . (x43 x54 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 x56 . (x0 x56 ⟶ False) ⟶ (x0 x54 ⟶ False) ⟶ x44 x54 (x45 x56) ⟶ x44 x55 x54 ⟶ (x9 x55 x56 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 x56 . (x0 x56 ⟶ False) ⟶ (x0 x54 ⟶ False) ⟶ x44 x54 (x45 x56) ⟶ x9 x55 x56 x54 ⟶ (x44 x55 x54 ⟶ False) ⟶ False) ⟶ ((x2 = x3 ⟶ False) ⟶ False) ⟶ (∀ x54 . x44 x54 x8 ⟶ (x39 x54 = x38 x54 ⟶ False) ⟶ False) ⟶ ((x41 = x5 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x53 x55 ⟶ x53 x54 ⟶ (x37 x55 x54 = x47 x55 x54 ⟶ False) ⟶ False) ⟶ ((x10 x11 ⟶ False) ⟶ False) ⟶ ((x0 x11 ⟶ False) ⟶ False) ⟶ ((x53 x12 ⟶ False) ⟶ False) ⟶ ((x10 x12 ⟶ False) ⟶ False) ⟶ ((x49 x12 ⟶ False) ⟶ False) ⟶ ((x0 x12 ⟶ False) ⟶ False) ⟶ ((x51 x13 ⟶ False) ⟶ False) ⟶ ((x10 x13 ⟶ False) ⟶ False) ⟶ ((x53 x14 ⟶ False) ⟶ False) ⟶ ((x51 x14 ⟶ False) ⟶ False) ⟶ ((x10 x14 ⟶ False) ⟶ False) ⟶ ((x49 x14 ⟶ False) ⟶ False) ⟶ ((x15 x16 ⟶ False) ⟶ False) ⟶ ((x36 x16 ⟶ False) ⟶ False) ⟶ (x0 x16 ⟶ False) ⟶ ((x50 x35 ⟶ False) ⟶ False) ⟶ ((x10 x35 ⟶ False) ⟶ False) ⟶ ((x53 x34 ⟶ False) ⟶ False) ⟶ ((x50 x34 ⟶ False) ⟶ False) ⟶ ((x10 x34 ⟶ False) ⟶ False) ⟶ ((x49 x34 ⟶ False) ⟶ False) ⟶ (x0 x33 ⟶ False) ⟶ ((x36 x17 ⟶ False) ⟶ False) ⟶ (x0 x17 ⟶ False) ⟶ ((x10 x18 ⟶ False) ⟶ False) ⟶ ((x53 x32 ⟶ False) ⟶ False) ⟶ ((x0 x19 ⟶ False) ⟶ False) ⟶ ((x36 x31 ⟶ False) ⟶ False) ⟶ (x0 x31 ⟶ False) ⟶ (∀ x54 . x49 x54 ⟶ (x7 (x7 x54) = x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x49 x54 ⟶ (x6 (x6 x54) = x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . (x51 x55 ⟶ False) ⟶ x53 x55 ⟶ (x51 x54 ⟶ False) ⟶ x53 x54 ⟶ x51 (x42 x55 x54) ⟶ False) ⟶ (∀ x54 x55 . x53 x55 ⟶ x53 x54 ⟶ (x53 (x47 x55 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x53 x55 ⟶ x53 x54 ⟶ (x53 (x4 x55 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x53 x55 ⟶ x53 x54 ⟶ (x53 (x48 x55 x54) ⟶ False) ⟶ False) ⟶ ((x36 x5 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x53 x55 ⟶ x53 x54 ⟶ (x53 (x42 x55 x54) ⟶ False) ⟶ False) ⟶ ((x15 x5 ⟶ False) ⟶ False) ⟶ ((x15 x8 ⟶ False) ⟶ False) ⟶ (∀ x54 . x53 x54 ⟶ (x53 (x7 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 . x53 x54 ⟶ (x49 (x7 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 . x53 x54 ⟶ (x53 (x6 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 . x53 x54 ⟶ (x49 (x6 x54) ⟶ False) ⟶ False) ⟶ ((x30 x8 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . (x50 x55 ⟶ False) ⟶ x53 x55 ⟶ (x50 x54 ⟶ False) ⟶ x53 x54 ⟶ x51 (x47 x55 x54) ⟶ False) ⟶ (∀ x54 x55 . (x51 x55 ⟶ False) ⟶ x53 x55 ⟶ (x51 x54 ⟶ False) ⟶ x53 x54 ⟶ x51 (x47 x55 x54) ⟶ False) ⟶ (∀ x54 x55 . (x51 x55 ⟶ False) ⟶ x53 x55 ⟶ (x50 x54 ⟶ False) ⟶ x53 x54 ⟶ x50 (x47 x54 x55) ⟶ False) ⟶ (∀ x54 x55 . (x51 x55 ⟶ False) ⟶ x53 x55 ⟶ (x50 x54 ⟶ False) ⟶ x53 x54 ⟶ x50 (x47 x55 x54) ⟶ False) ⟶ (∀ x54 . (x51 x54 ⟶ False) ⟶ x53 x54 ⟶ x51 (x7 x54) ⟶ False) ⟶ (∀ x54 . (x51 x54 ⟶ False) ⟶ x53 x54 ⟶ (x49 (x7 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 . x53 x54 ⟶ (x53 (x38 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 . x51 x54 ⟶ x53 x54 ⟶ (x51 (x7 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 . x51 x54 ⟶ x53 x54 ⟶ (x49 (x7 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 . (x50 x54 ⟶ False) ⟶ x53 x54 ⟶ x50 (x7 x54) ⟶ False) ⟶ (∀ x54 . (x50 x54 ⟶ False) ⟶ x53 x54 ⟶ (x49 (x7 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 . x50 x54 ⟶ x53 x54 ⟶ (x50 (x7 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 . x50 x54 ⟶ x53 x54 ⟶ (x49 (x7 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . (x51 x55 ⟶ False) ⟶ x53 x55 ⟶ (x51 x54 ⟶ False) ⟶ x53 x54 ⟶ x51 (x48 x55 x54) ⟶ False) ⟶ (∀ x54 x55 . (x50 x55 ⟶ False) ⟶ x53 x55 ⟶ (x50 x54 ⟶ False) ⟶ x53 x54 ⟶ x51 (x48 x55 x54) ⟶ False) ⟶ (∀ x54 x55 . (x50 x55 ⟶ False) ⟶ x53 x55 ⟶ (x51 x54 ⟶ False) ⟶ x53 x54 ⟶ x50 (x48 x54 x55) ⟶ False) ⟶ (∀ x54 x55 . (x50 x55 ⟶ False) ⟶ x53 x55 ⟶ (x51 x54 ⟶ False) ⟶ x53 x54 ⟶ x50 (x48 x55 x54) ⟶ False) ⟶ (∀ x54 x55 . x51 x55 ⟶ x53 x55 ⟶ (x51 x54 ⟶ False) ⟶ x53 x54 ⟶ (x50 (x4 x54 x55) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x51 x55 ⟶ x53 x55 ⟶ (x51 x54 ⟶ False) ⟶ x53 x54 ⟶ (x51 (x4 x55 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x50 x55 ⟶ x53 x55 ⟶ (x50 x54 ⟶ False) ⟶ x53 x54 ⟶ (x51 (x4 x54 x55) ⟶ False) ⟶ False) ⟶ ((x0 x3 ⟶ False) ⟶ False) ⟶ (∀ x54 . x49 x54 ⟶ (x49 (x38 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x50 x55 ⟶ x53 x55 ⟶ (x50 x54 ⟶ False) ⟶ x53 x54 ⟶ (x50 (x4 x55 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . (x51 x55 ⟶ False) ⟶ x53 x55 ⟶ (x50 x54 ⟶ False) ⟶ x53 x54 ⟶ x50 (x4 x54 x55) ⟶ False) ⟶ (∀ x54 x55 . (x51 x55 ⟶ False) ⟶ x53 x55 ⟶ (x50 x54 ⟶ False) ⟶ x53 x54 ⟶ x51 (x4 x55 x54) ⟶ False) ⟶ (∀ x54 . (x51 x54 ⟶ False) ⟶ x53 x54 ⟶ x50 (x6 x54) ⟶ False) ⟶ (∀ x54 . (x51 x54 ⟶ False) ⟶ x53 x54 ⟶ (x49 (x6 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 . (x50 x54 ⟶ False) ⟶ x53 x54 ⟶ x51 (x6 x54) ⟶ False) ⟶ (∀ x54 . (x50 x54 ⟶ False) ⟶ x53 x54 ⟶ (x49 (x6 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x51 x55 ⟶ x53 x55 ⟶ (x50 x54 ⟶ False) ⟶ x53 x54 ⟶ (x51 (x42 x54 x55) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x51 x55 ⟶ x53 x55 ⟶ (x50 x54 ⟶ False) ⟶ x53 x54 ⟶ (x51 (x42 x55 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x50 x55 ⟶ x53 x55 ⟶ (x51 x54 ⟶ False) ⟶ x53 x54 ⟶ (x50 (x42 x54 x55) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x50 x55 ⟶ x53 x55 ⟶ (x51 x54 ⟶ False) ⟶ x53 x54 ⟶ (x50 (x42 x55 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . (x50 x55 ⟶ False) ⟶ x53 x55 ⟶ (x50 x54 ⟶ False) ⟶ x53 x54 ⟶ x50 (x42 x55 x54) ⟶ False) ⟶ (∀ x54 x55 . (x0 x55 ⟶ False) ⟶ (x0 x54 ⟶ False) ⟶ x44 x54 (x45 x55) ⟶ (x9 (x20 x54 x55) x55 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . (x44 (x29 x54) x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 x56 . (x0 x56 ⟶ False) ⟶ (x0 x54 ⟶ False) ⟶ x44 x54 (x45 x56) ⟶ x9 x55 x56 x54 ⟶ (x44 x55 x56 ⟶ False) ⟶ False) ⟶ ((x9 x2 x8 x41 ⟶ False) ⟶ False) ⟶ (∀ x54 . x49 x54 ⟶ (x49 (x7 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 . x44 x54 x8 ⟶ (x44 (x39 x54) x8 ⟶ False) ⟶ False) ⟶ ((x44 x41 (x45 x8) ⟶ False) ⟶ False) ⟶ (∀ x54 . x49 x54 ⟶ (x49 (x6 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x53 x55 ⟶ x53 x54 ⟶ (x44 (x37 x55 x54) x8 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x49 x55 ⟶ x49 x54 ⟶ (x47 x55 x54 = x48 x55 (x7 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x49 x55 ⟶ x49 x54 ⟶ (x4 x55 x54 = x42 x55 (x6 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 . x49 x54 ⟶ (x38 x54 = x48 x54 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x10 x55 ⟶ x10 x54 ⟶ (x52 x55 x54 ⟶ False) ⟶ (x52 x54 x55 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x49 x55 ⟶ x49 x54 ⟶ (x48 x55 x54 = x48 x54 x55 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x49 x55 ⟶ x49 x54 ⟶ (x42 x55 x54 = x42 x54 x55 ⟶ False) ⟶ False) ⟶ (∀ x54 . x10 x54 ⟶ (x50 x54 ⟶ False) ⟶ (x51 x54 ⟶ False) ⟶ (x10 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x10 x54 ⟶ (x50 x54 ⟶ False) ⟶ (x51 x54 ⟶ False) ⟶ (x0 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x44 x54 (x45 x8) ⟶ (x30 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x0 x54 ⟶ x10 x54 ⟶ x51 x54 ⟶ False) ⟶ (∀ x54 . x0 x54 ⟶ x10 x54 ⟶ x50 x54 ⟶ False) ⟶ (∀ x54 . x0 x54 ⟶ x10 x54 ⟶ (x10 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . (x0 x54 ⟶ False) ⟶ x10 x54 ⟶ (x50 x54 ⟶ False) ⟶ (x51 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . (x0 x54 ⟶ False) ⟶ x10 x54 ⟶ (x50 x54 ⟶ False) ⟶ (x10 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x10 x54 ⟶ x51 x54 ⟶ x50 x54 ⟶ False) ⟶ (∀ x54 . x10 x54 ⟶ x51 x54 ⟶ (x10 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x10 x54 ⟶ x51 x54 ⟶ x0 x54 ⟶ False) ⟶ (∀ x54 . x30 x54 ⟶ (x21 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . (x0 x54 ⟶ False) ⟶ x10 x54 ⟶ (x51 x54 ⟶ False) ⟶ (x50 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . (x0 x54 ⟶ False) ⟶ x10 x54 ⟶ (x51 x54 ⟶ False) ⟶ (x10 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x53 x54 ⟶ (x10 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x30 x54 ⟶ (x22 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x10 x54 ⟶ x50 x54 ⟶ x51 x54 ⟶ False) ⟶ (∀ x54 . x10 x54 ⟶ x50 x54 ⟶ (x10 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x10 x54 ⟶ x50 x54 ⟶ x0 x54 ⟶ False) ⟶ (∀ x54 . x53 x54 ⟶ (x49 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x28 x54 ⟶ (x30 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x23 x54 ⟶ (x10 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x23 x54 ⟶ (x53 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x24 x54 ⟶ (x28 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x0 x54 ⟶ (x15 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x44 x54 x41 ⟶ (x36 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x36 x55 ⟶ x44 x54 (x45 x55) ⟶ (x36 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x24 x55 ⟶ x44 x54 (x45 x55) ⟶ (x24 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x28 x55 ⟶ x44 x54 (x45 x55) ⟶ (x28 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x30 x55 ⟶ x44 x54 (x45 x55) ⟶ (x30 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x22 x55 ⟶ x44 x54 (x45 x55) ⟶ (x22 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x44 x54 x8 ⟶ (x53 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x36 x54 ⟶ (x24 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x21 x55 ⟶ x44 x54 (x45 x55) ⟶ (x21 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x0 x54 ⟶ (x36 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x36 x55 ⟶ x44 x54 x55 ⟶ (x23 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x24 x55 ⟶ x44 x54 x55 ⟶ (x27 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x28 x55 ⟶ x44 x54 x55 ⟶ (x25 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x30 x55 ⟶ x44 x54 x55 ⟶ (x53 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x22 x55 ⟶ x44 x54 x55 ⟶ (x10 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x21 x55 ⟶ x44 x54 x55 ⟶ (x49 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x44 x54 (x45 x41) ⟶ (x36 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x1 x54 x55 ⟶ x1 x55 x54 ⟶ False) ⟶ ((x52 x46 (x39 (x37 x46 x26)) ⟶ False) ⟶ False) ⟶ (x52 (x38 x26) x46 ⟶ False) ⟶ ((x53 x26 ⟶ False) ⟶ False) ⟶ False (proof)