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

as obj
-

as prop
c9b31..

theory
HotG

stx
cd962..

address
TMPfv..