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

as obj
-

as prop
091fd..

theory
HotG

stx
01f7c..

address
TMRKK..