Proofgold Term Root Disambiguation

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

as obj
-

as prop
f819c..

theory
HotG

stx
c6843..

address
TMTnX..