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

as obj
-

as prop
99b52..

theory
HotG

stx
04bda..

address
TMSdZ..