Search for blocks/addresses/...

Proofgold Proposition

∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . In x2 x0∀ x3 . In x3 x0In (x1 x2 x3) x0)∀ x2 : ι → ι → ι . (∀ x3 . In x3 x0∀ x4 . In x4 x0In (x2 x3 x4) x0)∀ x3 : ι → ι → ι → ι . (∀ x4 . In x4 x0∀ x5 . In x5 x0∀ x6 . In x6 x0In (x3 x4 x5 x6) x0)∀ x4 . In x4 x0∀ x5 . In x5 x0∀ x6 : ι → ι → ι → ι . (∀ x7 . In x7 x0∀ x8 . In x8 x0∀ x9 . In x9 x0In (x6 x7 x8 x9) x0)∀ x7 : ι → ι → ι . (∀ x8 . In x8 x0∀ x9 . In x9 x0In (x7 x8 x9) x0)∀ x8 : ι → ι → ι . (∀ x9 . In x9 x0∀ x10 . In x10 x0In (x8 x9 x10) x0)∀ x9 . In x9 x0∀ x10 : ι → ι → ι . (∀ x11 . In x11 x0∀ x12 . In x12 x0In (x10 x11 x12) x0)(∀ x11 . In x11 x0(x10 x11 x9 = x11False)False)(∀ x11 . In x11 x0∀ x12 . In x12 x0(x1 x11 (x10 x11 x12) = x12False)False)(∀ x11 . In x11 x0∀ x12 . In x12 x0(x10 x11 (x1 x11 x12) = x12False)False)(∀ x11 . In x11 x0∀ x12 . In x12 x0(x10 (x2 x12 x11) x11 = x12False)False)(∀ x11 . In x11 x0∀ x12 . In x12 x0(x8 x11 x12 = x1 x11 (x10 x12 x11)False)False)(∀ x11 . In x11 x0(x1 x9 x11 = x11False)False)(∀ x11 . In x11 x0(x7 x9 x11 = x11False)False)(∀ x11 . In x11 x0∀ x12 . In x12 x0(x3 x11 x9 x12 = x12False)False)(∀ x11 . In x11 x0∀ x12 . In x12 x0(x6 x9 x11 x12 = x12False)False)(∀ x11 . In x11 x0∀ x12 . In x12 x0∀ x13 . In x13 x0(x3 x11 x12 (x8 x11 (x7 x12 (x3 x11 x12 (x8 x11 (x7 x12 (x3 x11 x12 (x8 x11 (x7 x12 (x3 x11 x12 (x8 x11 (x7 x12 (x3 x11 x12 (x8 x11 (x7 x12 x13)))))))))))))) = x13False)False)(∀ x11 . In x11 x0∀ x12 . In x12 x0∀ x13 . In x13 x0∀ x14 . In x14 x0(x6 x11 x13 (x8 x12 (x8 x11 (x6 x13 x12 (x6 x11 x13 (x8 x12 (x8 x11 (x6 x13 x12 (x6 x11 x13 (x8 x12 (x8 x11 (x6 x13 x12 (x6 x11 x13 (x8 x12 (x8 x11 (x6 x13 x12 x14))))))))))))))) = x14False)False)(x10 x5 x4 = x10 x4 x5False)False
type
prop
theory
HF
name
-
proof
PULXW..
Megalodon
-
proofgold address
TMJdA..
creator
11752 PrGVS../81383..
owner
11752 PrGVS../81383..
term root
83b64..