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

as obj
-

as prop
8f193..

theory
HotG

stx
3b00e..

address
TMMiW..