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

as obj
-

as prop
73a98..

theory
HotG

stx
0d075..

address
TMGpe..