Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Theorem 47f84.. : ∀ 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 x55 x56 . x1 x54 x55 ⟶ x48 x55 (x49 x56) ⟶ x0 x56 ⟶ False) ⟶ (∀ x54 x55 . x53 x55 ⟶ x53 x54 ⟶ x52 x55 x54 ⟶ (x0 x54 ⟶ False) ⟶ (x51 x55 ⟶ False) ⟶ (x50 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 x56 . x1 x55 x56 ⟶ x48 x56 (x49 x54) ⟶ (x48 x55 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x53 x55 ⟶ x53 x54 ⟶ x52 x55 x54 ⟶ (x50 x54 ⟶ False) ⟶ x50 x55 ⟶ False) ⟶ (∀ x54 x55 . x47 x55 x54 ⟶ (x48 x55 (x49 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x48 x55 (x49 x54) ⟶ (x47 x55 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x53 x55 ⟶ x53 x54 ⟶ x52 x55 x54 ⟶ (x51 x55 ⟶ False) ⟶ x51 x54 ⟶ False) ⟶ (∀ x54 . x3 x54 ⟶ (x4 x5 x54 = x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x48 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 x55 . x1 x55 x54 ⟶ (x48 x55 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x53 x55 ⟶ x53 x54 ⟶ x52 x55 x54 ⟶ x50 x55 ⟶ (x50 x54 ⟶ False) ⟶ False) ⟶ ((x48 x2 x46 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x3 x55 ⟶ x3 x54 ⟶ (x7 (x6 x55) (x6 x54) = x7 x54 x55 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x3 x55 ⟶ x3 x54 ⟶ (x45 (x6 x55) (x6 x54) = x6 (x45 x55 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 x56 . x3 x56 ⟶ x3 x54 ⟶ x3 x55 ⟶ (x4 (x4 x56 x54) x55 = x4 x56 (x4 x54 x55) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 x56 . x3 x56 ⟶ x3 x54 ⟶ x3 x55 ⟶ (x45 (x45 x56 x54) x55 = x45 x56 (x45 x54 x55) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 x56 . x3 x56 ⟶ x3 x54 ⟶ x3 x55 ⟶ (x4 (x45 x56 x54) x55 = x45 (x4 x56 x55) (x4 x54 x55) ⟶ False) ⟶ False) ⟶ ((x48 x43 x44 ⟶ False) ⟶ False) ⟶ ((x48 x43 x8 ⟶ False) ⟶ False) ⟶ ((x42 x43 x44 x8 ⟶ False) ⟶ False) ⟶ ((x50 x43 ⟶ False) ⟶ False) ⟶ (x0 x43 ⟶ False) ⟶ (∀ x54 . x3 x54 ⟶ (x4 x54 (x6 x5) = x6 x54 ⟶ False) ⟶ False) ⟶ ((x48 x5 x44 ⟶ False) ⟶ False) ⟶ ((x48 x5 x8 ⟶ False) ⟶ False) ⟶ ((x42 x5 x44 x8 ⟶ False) ⟶ False) ⟶ ((x50 x5 ⟶ False) ⟶ False) ⟶ (x0 x5 ⟶ False) ⟶ (∀ x54 x55 . x3 x55 ⟶ x3 x54 ⟶ (x45 x55 (x6 x54) = x7 x55 x54 ⟶ False) ⟶ False) ⟶ ((x48 x41 x44 ⟶ False) ⟶ False) ⟶ ((x48 x41 x8 ⟶ False) ⟶ False) ⟶ ((x42 x41 x44 x8 ⟶ False) ⟶ False) ⟶ ((x0 x41 ⟶ False) ⟶ False) ⟶ ((x6 (x6 x43) = x43 ⟶ False) ⟶ False) ⟶ ((x6 (x6 x5) = x5 ⟶ False) ⟶ False) ⟶ ((x6 x43 = x6 x43 ⟶ False) ⟶ False) ⟶ ((x6 x5 = x6 x5 ⟶ False) ⟶ False) ⟶ ((x6 x41 = x41 ⟶ False) ⟶ False) ⟶ ((x4 (x6 x43) x5 = x6 x43 ⟶ False) ⟶ False) ⟶ ((x4 (x6 x43) x41 = x41 ⟶ False) ⟶ False) ⟶ ((x4 x43 x5 = x43 ⟶ False) ⟶ False) ⟶ ((x4 x43 x41 = x41 ⟶ False) ⟶ False) ⟶ ((x4 x5 (x6 x43) = x6 x43 ⟶ False) ⟶ False) ⟶ ((x4 x5 x43 = x43 ⟶ False) ⟶ False) ⟶ ((x4 x5 x5 = x5 ⟶ False) ⟶ False) ⟶ ((x4 x5 x41 = x41 ⟶ False) ⟶ False) ⟶ ((x4 x41 (x6 x43) = x41 ⟶ False) ⟶ False) ⟶ ((x4 x41 x43 = x41 ⟶ False) ⟶ False) ⟶ ((x4 x41 x5 = x41 ⟶ False) ⟶ False) ⟶ ((x4 x41 x41 = x41 ⟶ False) ⟶ False) ⟶ ((x7 (x6 x43) (x6 x43) = x41 ⟶ False) ⟶ False) ⟶ ((x7 (x6 x43) (x6 x5) = x6 x5 ⟶ False) ⟶ False) ⟶ ((x7 (x6 x43) x41 = x6 x43 ⟶ False) ⟶ False) ⟶ ((x7 (x6 x5) (x6 x43) = x5 ⟶ False) ⟶ False) ⟶ ((x7 (x6 x5) (x6 x5) = x41 ⟶ False) ⟶ False) ⟶ ((x7 (x6 x5) x5 = x6 x43 ⟶ False) ⟶ False) ⟶ ((x7 (x6 x5) x41 = x6 x5 ⟶ False) ⟶ False) ⟶ ((x7 x43 x43 = x41 ⟶ False) ⟶ False) ⟶ ((x7 x43 x5 = x5 ⟶ False) ⟶ False) ⟶ ((x7 x43 x41 = x43 ⟶ False) ⟶ False) ⟶ ((x7 x5 (x6 x5) = x43 ⟶ False) ⟶ False) ⟶ ((x7 x5 x43 = x6 x5 ⟶ False) ⟶ False) ⟶ ((x7 x5 x5 = x41 ⟶ False) ⟶ False) ⟶ ((x7 x5 x41 = x5 ⟶ False) ⟶ False) ⟶ ((x7 x41 (x6 x43) = x43 ⟶ False) ⟶ False) ⟶ ((x7 x41 (x6 x5) = x5 ⟶ False) ⟶ False) ⟶ ((x7 x41 x43 = x6 x43 ⟶ False) ⟶ False) ⟶ ((x7 x41 x5 = x6 x5 ⟶ False) ⟶ False) ⟶ ((x7 x41 x41 = x41 ⟶ False) ⟶ False) ⟶ ((x45 (x6 x43) x43 = x41 ⟶ False) ⟶ False) ⟶ ((x45 (x6 x43) x5 = x6 x5 ⟶ False) ⟶ False) ⟶ ((x45 (x6 x5) (x6 x5) = x6 x43 ⟶ False) ⟶ False) ⟶ ((x45 (x6 x5) x43 = x5 ⟶ False) ⟶ False) ⟶ ((x45 (x6 x5) x5 = x41 ⟶ False) ⟶ False) ⟶ ((x45 (x6 x5) x41 = x6 x5 ⟶ False) ⟶ False) ⟶ ((x45 x43 (x6 x43) = x41 ⟶ False) ⟶ False) ⟶ ((x45 x43 (x6 x5) = x5 ⟶ False) ⟶ False) ⟶ ((x45 x43 x41 = x43 ⟶ False) ⟶ False) ⟶ ((x45 x5 (x6 x43) = x6 x5 ⟶ False) ⟶ False) ⟶ ((x45 x5 (x6 x5) = x41 ⟶ False) ⟶ False) ⟶ ((x45 x5 x5 = x43 ⟶ False) ⟶ False) ⟶ ((x45 x5 x41 = x5 ⟶ False) ⟶ False) ⟶ ((x45 x41 (x6 x43) = x6 x43 ⟶ False) ⟶ False) ⟶ ((x45 x41 (x6 x5) = x6 x5 ⟶ False) ⟶ False) ⟶ ((x45 x41 x43 = x43 ⟶ False) ⟶ False) ⟶ ((x45 x41 x5 = x5 ⟶ False) ⟶ False) ⟶ ((x45 x41 x41 = x41 ⟶ False) ⟶ False) ⟶ ((x52 (x6 x43) (x6 x43) ⟶ False) ⟶ False) ⟶ ((x52 (x6 x43) (x6 x5) ⟶ False) ⟶ False) ⟶ ((x52 (x6 x43) x43 ⟶ False) ⟶ False) ⟶ ((x52 (x6 x43) x5 ⟶ False) ⟶ False) ⟶ ((x52 (x6 x43) x41 ⟶ False) ⟶ False) ⟶ (x52 (x6 x5) (x6 x43) ⟶ False) ⟶ ((x52 (x6 x5) (x6 x5) ⟶ False) ⟶ False) ⟶ ((x52 (x6 x5) x43 ⟶ False) ⟶ False) ⟶ ((x52 (x6 x5) x5 ⟶ False) ⟶ False) ⟶ ((x52 (x6 x5) x41 ⟶ False) ⟶ False) ⟶ (x52 x43 (x6 x43) ⟶ False) ⟶ (x52 x43 (x6 x5) ⟶ False) ⟶ ((x52 x43 x43 ⟶ False) ⟶ False) ⟶ (x52 x43 x5 ⟶ False) ⟶ (x52 x43 x41 ⟶ False) ⟶ (x52 x5 (x6 x43) ⟶ False) ⟶ (x52 x5 (x6 x5) ⟶ False) ⟶ ((x52 x5 x43 ⟶ False) ⟶ False) ⟶ ((x52 x5 x5 ⟶ False) ⟶ False) ⟶ (x52 x5 x41 ⟶ False) ⟶ (x52 x41 (x6 x43) ⟶ False) ⟶ (x52 x41 (x6 x5) ⟶ False) ⟶ ((x52 x41 x43 ⟶ False) ⟶ False) ⟶ ((x52 x41 x5 ⟶ False) ⟶ False) ⟶ ((x52 x41 x41 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x9 x55 ⟶ x9 x54 ⟶ (x52 x55 x55 ⟶ False) ⟶ False) ⟶ (∀ x54 . (x47 x54 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 x56 . (x0 x56 ⟶ False) ⟶ (x0 x54 ⟶ False) ⟶ x48 x54 (x49 x56) ⟶ x48 x55 x54 ⟶ (x42 x55 x56 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 x56 . (x0 x56 ⟶ False) ⟶ (x0 x54 ⟶ False) ⟶ x48 x54 (x49 x56) ⟶ x42 x55 x56 x54 ⟶ (x48 x55 x54 ⟶ False) ⟶ False) ⟶ ((x8 = x46 ⟶ False) ⟶ False) ⟶ (∀ x54 . x40 x54 ⟶ (x39 x54 = x6 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x53 x55 ⟶ x53 x54 ⟶ (x10 x55 x54 = x4 x55 x54 ⟶ False) ⟶ False) ⟶ ((x9 x38 ⟶ False) ⟶ False) ⟶ ((x0 x38 ⟶ False) ⟶ False) ⟶ ((x53 x37 ⟶ False) ⟶ False) ⟶ ((x9 x37 ⟶ False) ⟶ False) ⟶ ((x3 x37 ⟶ False) ⟶ False) ⟶ ((x0 x37 ⟶ False) ⟶ False) ⟶ ((x51 x36 ⟶ False) ⟶ False) ⟶ ((x9 x36 ⟶ False) ⟶ False) ⟶ ((x53 x35 ⟶ False) ⟶ False) ⟶ ((x51 x35 ⟶ False) ⟶ False) ⟶ ((x9 x35 ⟶ False) ⟶ False) ⟶ ((x3 x35 ⟶ False) ⟶ False) ⟶ ((x34 x33 ⟶ False) ⟶ False) ⟶ ((x11 x33 ⟶ False) ⟶ False) ⟶ (x0 x33 ⟶ False) ⟶ ((x50 x12 ⟶ False) ⟶ False) ⟶ ((x9 x12 ⟶ False) ⟶ False) ⟶ ((x53 x13 ⟶ False) ⟶ False) ⟶ ((x50 x13 ⟶ False) ⟶ False) ⟶ ((x9 x13 ⟶ False) ⟶ False) ⟶ ((x3 x13 ⟶ False) ⟶ False) ⟶ (x0 x14 ⟶ False) ⟶ ((x11 x32 ⟶ False) ⟶ False) ⟶ (x0 x32 ⟶ False) ⟶ ((x9 x31 ⟶ False) ⟶ False) ⟶ ((x53 x15 ⟶ False) ⟶ False) ⟶ ((x0 x30 ⟶ False) ⟶ False) ⟶ ((x11 x16 ⟶ False) ⟶ False) ⟶ (x0 x16 ⟶ False) ⟶ (∀ x54 x55 . x53 x55 ⟶ x53 x54 ⟶ (x52 x5 (x17 x55) ⟶ False) ⟶ (x52 x5 x54 ⟶ False) ⟶ x52 x5 (x10 (x17 x55) x54) ⟶ False) ⟶ (∀ x54 . x3 x54 ⟶ (x6 (x6 x54) = x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x40 x54 ⟶ (x39 (x39 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 (x7 x55 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x53 x55 ⟶ x53 x54 ⟶ (x53 (x4 x55 x54) ⟶ False) ⟶ False) ⟶ ((x11 x46 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x53 x55 ⟶ x53 x54 ⟶ (x53 (x45 x55 x54) ⟶ False) ⟶ False) ⟶ ((x18 x19 ⟶ False) ⟶ False) ⟶ ((x34 x46 ⟶ False) ⟶ False) ⟶ ((x34 x19 ⟶ False) ⟶ False) ⟶ ((x34 x44 ⟶ False) ⟶ False) ⟶ (∀ x54 . x53 x54 ⟶ (x53 (x6 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 . x53 x54 ⟶ (x3 (x6 x54) ⟶ False) ⟶ False) ⟶ ((x20 x44 ⟶ False) ⟶ False) ⟶ (∀ x54 . x53 x54 ⟶ (x53 (x17 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 (x7 x54 x55) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x51 x55 ⟶ x53 x55 ⟶ (x51 x54 ⟶ False) ⟶ x53 x54 ⟶ (x51 (x7 x55 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x50 x55 ⟶ x53 x55 ⟶ (x50 x54 ⟶ False) ⟶ x53 x54 ⟶ (x51 (x7 x54 x55) ⟶ False) ⟶ False) ⟶ ((x0 x2 ⟶ False) ⟶ False) ⟶ (∀ x54 . x3 x54 ⟶ (x3 (x17 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x50 x55 ⟶ x53 x55 ⟶ (x50 x54 ⟶ False) ⟶ x53 x54 ⟶ (x50 (x7 x55 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . (x51 x55 ⟶ False) ⟶ x53 x55 ⟶ (x50 x54 ⟶ False) ⟶ x53 x54 ⟶ x50 (x7 x54 x55) ⟶ False) ⟶ (∀ x54 x55 . (x51 x55 ⟶ False) ⟶ x53 x55 ⟶ (x50 x54 ⟶ False) ⟶ x53 x54 ⟶ x51 (x7 x55 x54) ⟶ False) ⟶ (∀ x54 . (x51 x54 ⟶ False) ⟶ x53 x54 ⟶ x50 (x6 x54) ⟶ False) ⟶ (∀ x54 . (x51 x54 ⟶ False) ⟶ x53 x54 ⟶ (x3 (x6 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 . (x50 x54 ⟶ False) ⟶ x53 x54 ⟶ x51 (x6 x54) ⟶ False) ⟶ (∀ x54 . (x50 x54 ⟶ False) ⟶ x53 x54 ⟶ (x3 (x6 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) ⟶ x48 x54 (x49 x55) ⟶ (x42 (x29 x54 x55) x55 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . (x48 (x21 x54) x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 x56 . (x0 x56 ⟶ False) ⟶ (x0 x54 ⟶ False) ⟶ x48 x54 (x49 x56) ⟶ x42 x55 x56 x54 ⟶ (x48 x55 x56 ⟶ False) ⟶ False) ⟶ ((x48 x8 (x49 x44) ⟶ False) ⟶ False) ⟶ (∀ x54 . x3 x54 ⟶ (x3 (x6 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 . x40 x54 ⟶ (x48 (x39 x54) x19 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x53 x55 ⟶ x53 x54 ⟶ (x48 (x10 x55 x54) x44 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x3 x55 ⟶ x3 x54 ⟶ (x7 x55 x54 = x45 x55 (x6 x54) ⟶ False) ⟶ False) ⟶ (∀ x54 . x3 x54 ⟶ (x17 x54 = x4 x54 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x9 x55 ⟶ x9 x54 ⟶ (x52 x55 x54 ⟶ False) ⟶ (x52 x54 x55 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x3 x55 ⟶ x3 x54 ⟶ (x4 x55 x54 = x4 x54 x55 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x3 x55 ⟶ x3 x54 ⟶ (x45 x55 x54 = x45 x54 x55 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x53 x55 ⟶ x53 x54 ⟶ (x10 x55 x54 = x10 x54 x55 ⟶ False) ⟶ False) ⟶ (∀ x54 . x9 x54 ⟶ (x50 x54 ⟶ False) ⟶ (x51 x54 ⟶ False) ⟶ (x9 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x9 x54 ⟶ (x50 x54 ⟶ False) ⟶ (x51 x54 ⟶ False) ⟶ (x0 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x48 x54 (x49 x44) ⟶ (x20 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x0 x54 ⟶ x9 x54 ⟶ x51 x54 ⟶ False) ⟶ (∀ x54 . x0 x54 ⟶ x9 x54 ⟶ x50 x54 ⟶ False) ⟶ (∀ x54 . x0 x54 ⟶ x9 x54 ⟶ (x9 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . (x0 x54 ⟶ False) ⟶ x9 x54 ⟶ (x50 x54 ⟶ False) ⟶ (x51 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . (x0 x54 ⟶ False) ⟶ x9 x54 ⟶ (x50 x54 ⟶ False) ⟶ (x9 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x9 x54 ⟶ x51 x54 ⟶ x50 x54 ⟶ False) ⟶ (∀ x54 . x9 x54 ⟶ x51 x54 ⟶ (x9 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x9 x54 ⟶ x51 x54 ⟶ x0 x54 ⟶ False) ⟶ (∀ x54 . x20 x54 ⟶ (x28 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . (x0 x54 ⟶ False) ⟶ x9 x54 ⟶ (x51 x54 ⟶ False) ⟶ (x50 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . (x0 x54 ⟶ False) ⟶ x9 x54 ⟶ (x51 x54 ⟶ False) ⟶ (x9 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x53 x54 ⟶ (x9 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x20 x54 ⟶ (x27 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x9 x54 ⟶ x50 x54 ⟶ x51 x54 ⟶ False) ⟶ (∀ x54 . x9 x54 ⟶ x50 x54 ⟶ (x9 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x9 x54 ⟶ x50 x54 ⟶ x0 x54 ⟶ False) ⟶ (∀ x54 . x53 x54 ⟶ (x3 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x22 x54 ⟶ (x20 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x26 x54 ⟶ (x9 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x26 x54 ⟶ (x53 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x18 x54 ⟶ (x22 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x0 x54 ⟶ (x34 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x48 x54 x8 ⟶ (x11 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x11 x55 ⟶ x48 x54 (x49 x55) ⟶ (x11 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x18 x55 ⟶ x48 x54 (x49 x55) ⟶ (x18 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x22 x55 ⟶ x48 x54 (x49 x55) ⟶ (x22 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x20 x55 ⟶ x48 x54 (x49 x55) ⟶ (x20 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x27 x55 ⟶ x48 x54 (x49 x55) ⟶ (x27 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x48 x54 x44 ⟶ (x53 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x11 x54 ⟶ (x18 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x28 x55 ⟶ x48 x54 (x49 x55) ⟶ (x28 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x0 x54 ⟶ (x11 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x11 x55 ⟶ x48 x54 x55 ⟶ (x26 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x18 x55 ⟶ x48 x54 x55 ⟶ (x40 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x22 x55 ⟶ x48 x54 x55 ⟶ (x25 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x20 x55 ⟶ x48 x54 x55 ⟶ (x53 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x27 x55 ⟶ x48 x54 x55 ⟶ (x9 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x28 x55 ⟶ x48 x54 x55 ⟶ (x3 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x48 x54 (x49 x8) ⟶ (x11 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 . x48 x54 (x49 x19) ⟶ (x18 x54 ⟶ False) ⟶ False) ⟶ (∀ x54 x55 . x1 x54 x55 ⟶ x1 x55 x54 ⟶ False) ⟶ ((x10 x23 x24 = x39 x5 ⟶ False) ⟶ False) ⟶ (x52 x5 (x17 x24) ⟶ False) ⟶ (x52 x5 (x17 x23) ⟶ False) ⟶ ((x53 x24 ⟶ False) ⟶ False) ⟶ ((x53 x23 ⟶ False) ⟶ False) ⟶ False (proof)

Proofgold Address