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

as obj
-

as prop
2686c..

theory
HotG

stx
9fb8e..

address
TMNJQ..