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

as obj
-

as prop
814ab..

theory
HotG

stx
1dd49..

address
TMbtE..