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

Proofgold Asset