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

as obj
-

as prop
0bb13..

theory
HotG

stx
1b586..

address
TMPzo..