Search for blocks/addresses/...

Proofgold Proposition

∀ 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 : ι → ι → ο . ∀ x53 : ι → ι . ∀ x54 : ι → ο . ∀ x55 x56 . ∀ x57 : ι → ο . ∀ x58 : ι → ι . ∀ x59 : ι → ο . ∀ x60 : ι → ι → ι → ι → ι → ι . ∀ x61 : ι → ι → ι → ι . ∀ x62 : ι → ι → ι . ∀ x63 : ι → ο . ∀ x64 : ι → ι → ι . ∀ x65 : ι → ο . ∀ x66 : ι → ι → ι → ο . ∀ x67 x68 . ∀ x69 : ι → ι . ∀ x70 . ∀ x71 x72 : ι → ι → ι . ∀ x73 . ∀ x74 : ι → ι → ι . ∀ x75 x76 x77 : ι → ο . ∀ x78 : ι → ι → ο . ∀ x79 : ι → ο . (∀ x80 x81 . x79 x81x79 x80(x78 x81 x80False)(x77 x80False)(x76 x81False)False)(∀ x80 x81 . x0 x81(x81 = x80False)x0 x80False)(∀ x80 x81 . x79 x81x79 x80(x78 x81 x80False)(x76 x81False)(x77 x80False)False)(∀ x80 x81 . x1 x80 x81x0 x81False)(∀ x80 x81 . x79 x81x79 x80x78 x81 x80(x0 x81False)(x76 x80False)(x77 x81False)False)(∀ x80 . x0 x80(x80 = x2False)False)(∀ x80 . x75 x80(x74 x80 x73 = x80False)False)(∀ x80 x81 x82 . x1 x80 x81x4 x81 (x3 x82)x0 x82False)(∀ x80 x81 . x79 x81x79 x80x78 x81 x80(x0 x80False)(x77 x81False)(x76 x80False)False)(∀ x80 . x75 x80(x74 x5 x80 = x5False)False)(∀ x80 x81 x82 . x1 x81 x82x4 x82 (x3 x80)(x4 x81 x80False)False)(∀ x80 x81 . x79 x81x79 x80x78 x81 x80(x76 x80False)x76 x81False)(∀ x80 . x75 x80(x72 x80 x5 = x80False)False)(∀ x80 x81 . x6 x81 x80(x4 x81 (x3 x80)False)False)(∀ x80 x81 . x4 x81 (x3 x80)(x6 x81 x80False)False)(∀ x80 x81 . x79 x81x79 x80x78 x81 x80(x77 x81False)x77 x80False)(∀ x80 . x75 x80(x71 x73 x80 = x80False)False)(∀ x80 x81 . x4 x80 x81(x0 x81False)(x1 x80 x81False)False)(∀ x80 x81 . x79 x81x79 x80x78 x81 x80x77 x80(x77 x81False)False)(∀ x80 . x75 x80(x71 x80 x5 = x5False)False)(∀ x80 x81 . x1 x81 x80(x4 x81 x80False)False)(∀ x80 x81 . x79 x81x79 x80x78 x81 x80x76 x81(x76 x80False)False)((x4 x2 x70False)False)(∀ x80 . x75 x80(x7 x80 x5 = x80False)False)(∀ x80 x81 . x75 x81x75 x80(x72 (x69 x81) (x69 x80) = x72 x80 x81False)False)(∀ x80 x81 . x75 x81x75 x80(x7 (x69 x81) (x69 x80) = x69 (x7 x81 x80)False)False)(∀ x80 x81 x82 . x75 x82x75 x80x75 x81(x71 (x71 x82 x80) x81 = x71 x82 (x71 x80 x81)False)False)(∀ x80 x81 x82 . x75 x82x75 x80x75 x81(x7 (x7 x82 x80) x81 = x7 x82 (x7 x80 x81)False)False)(∀ x80 x81 x82 . x75 x82x75 x80x75 x81(x71 (x7 x82 x80) x81 = x7 (x71 x82 x81) (x71 x80 x81)False)False)(∀ x80 x81 x82 . x75 x82x75 x80x75 x81(x71 x82 (x74 x80 x81) = x74 (x71 x82 x80) x81False)False)((x4 x67 x68False)False)((x4 x67 x8False)False)((x66 x67 x68 x8False)False)((x76 x67False)False)(x0 x67False)((x4 x9 x68False)False)((x4 x9 x8False)False)((x66 x9 x68 x8False)False)((x76 x9False)False)(x0 x9False)(∀ x80 . x75 x80(x71 x80 (x69 x73) = x69 x80False)False)((x4 x73 x68False)False)((x4 x73 x8False)False)((x66 x73 x68 x8False)False)((x76 x73False)False)(x0 x73False)(∀ x80 x81 . x75 x81x75 x80(x7 x81 (x69 x80) = x72 x81 x80False)False)((x4 x10 x68False)False)((x4 x10 x8False)False)((x66 x10 x68 x8False)False)((x0 x10False)False)((x69 (x74 (x69 x67) x9) = x74 x67 x9False)False)((x69 (x74 (x69 x9) x67) = x74 x9 x67False)False)((x69 (x74 (x69 x73) x67) = x74 x73 x67False)False)((x69 (x74 (x69 x73) x9) = x74 x73 x9False)False)((x69 (x74 x67 x9) = x74 (x69 x67) x9False)False)((x69 (x74 x9 x67) = x74 (x69 x9) x67False)False)((x69 (x74 x73 x67) = x74 (x69 x73) x67False)False)((x69 (x74 x73 x9) = x74 (x69 x73) x9False)False)((x69 (x69 x67) = x67False)False)((x69 (x69 x9) = x9False)False)((x69 (x69 x73) = x73False)False)((x69 x67 = x69 x67False)False)((x69 x9 = x69 x9False)False)((x69 x73 = x69 x73False)False)((x69 x10 = x10False)False)((x71 (x74 (x69 x67) x9) (x74 (x69 x9) x67) = x73False)False)((x71 (x74 (x69 x67) x9) (x74 (x69 x73) x67) = x74 x73 x9False)False)((x71 (x74 (x69 x67) x9) (x74 x9 x67) = x69 x73False)False)((x71 (x74 (x69 x67) x9) (x74 x73 x67) = x74 (x69 x73) x9False)False)((x71 (x74 (x69 x67) x9) (x69 x9) = x67False)False)((x71 (x74 (x69 x67) x9) x9 = x69 x67False)False)((x71 (x74 (x69 x67) x9) x73 = x74 (x69 x67) x9False)False)((x71 (x74 (x69 x9) x67) (x74 (x69 x67) x9) = x73False)False)((x71 (x74 (x69 x9) x67) (x74 (x69 x73) x9) = x74 x73 x67False)False)((x71 (x74 (x69 x9) x67) (x74 x67 x9) = x69 x73False)False)((x71 (x74 (x69 x9) x67) (x74 x73 x9) = x74 (x69 x73) x67False)False)((x71 (x74 (x69 x9) x67) (x69 x67) = x9False)False)((x71 (x74 (x69 x9) x67) x67 = x69 x9False)False)((x71 (x74 (x69 x9) x67) x73 = x74 (x69 x9) x67False)False)((x71 (x74 (x69 x73) x67) (x74 (x69 x67) x9) = x74 x73 x9False)False)((x71 (x74 (x69 x73) x67) (x74 x67 x9) = x74 (x69 x73) x9False)False)((x71 (x74 (x69 x73) x67) (x69 x67) = x73False)False)((x71 (x74 (x69 x73) x67) (x69 x9) = x74 x9 x67False)False)((x71 (x74 (x69 x73) x67) x67 = x69 x73False)False)((x71 (x74 (x69 x73) x67) x9 = x74 (x69 x9) x67False)False)((x71 (x74 (x69 x73) x67) x73 = x74 (x69 x73) x67False)False)((x71 (x74 (x69 x73) x9) (x74 x9 x67) = x74 (x69 x73) x67False)False)((x71 (x74 (x69 x73) x9) (x69 x67) = x74 x67 x9False)False)((x71 (x74 (x69 x73) x9) (x69 x9) = x73False)False)((x71 (x74 (x69 x73) x9) x67 = x74 (x69 x67) x9False)False)((x71 (x74 (x69 x73) x9) x9 = x69 x73False)False)((x71 (x74 (x69 x73) x9) x73 = x74 (x69 x73) x9False)False)((x71 (x74 x67 x9) (x74 (x69 x9) x67) = x69 x73False)False)((x71 (x74 x67 x9) (x74 (x69 x73) x67) = x74 (x69 x73) x9False)False)((x71 (x74 x67 x9) (x74 x9 x67) = x73False)False)((x71 (x74 x67 x9) (x74 x73 x67) = x74 x73 x9False)False)((x71 (x74 x67 x9) (x69 x9) = x69 x67False)False)((x71 (x74 x67 x9) x9 = x67False)False)((x71 (x74 x67 x9) x73 = x74 x67 x9False)False)((x71 (x74 x9 x67) (x74 (x69 x67) x9) = x69 x73False)False)((x71 (x74 x9 x67) (x74 (x69 x73) x9) = x74 (x69 x73) x67False)False)((x71 (x74 x9 x67) (x74 x67 x9) = x73False)False)((x71 (x74 x9 x67) (x74 x73 x9) = x74 x73 x67False)False)((x71 (x74 x9 x67) (x69 x67) = x69 x9False)False)((x71 (x74 x9 x67) x67 = x9False)False)((x71 (x74 x9 x67) x73 = x74 x9 x67False)False)((x71 (x74 x9 x67) x10 = x10False)False)((x71 (x74 x73 x67) (x74 (x69 x67) x9) = x74 (x69 x73) x9False)False)((x71 (x74 x73 x67) (x74 x67 x9) = x74 x73 x9False)False)((x71 (x74 x73 x67) (x69 x67) = x69 x73False)False)((x71 (x74 x73 x67) (x69 x9) = x74 (x69 x9) x67False)False)((x71 (x74 x73 x67) x67 = x73False)False)((x71 (x74 x73 x67) x9 = x74 x9 x67False)False)((x71 (x74 x73 x67) x73 = x74 x73 x67False)False)((x71 (x74 x73 x9) (x74 (x69 x9) x67) = x74 (x69 x73) x67False)False)((x71 (x74 x73 x9) (x74 x9 x67) = x74 x73 x67False)False)((x71 (x74 x73 x9) (x69 x67) = x74 (x69 x67) x9False)False)((x71 (x74 x73 x9) (x69 x9) = x69 x73False)False)((x71 (x74 x73 x9) x67 = x74 x67 x9False)False)((x71 (x74 x73 x9) x9 = x73False)False)((x71 (x74 x73 x9) x73 = x74 x73 x9False)False)((x71 (x74 x73 x9) x10 = x10False)False)((x71 (x69 x67) (x74 (x69 x9) x67) = x9False)False)((x71 (x69 x67) (x74 (x69 x73) x67) = x73False)False)((x71 (x69 x67) (x74 (x69 x73) x9) = x74 x67 x9False)False)((x71 (x69 x67) (x74 x9 x67) = x69 x9False)False)((x71 (x69 x67) (x74 x73 x67) = x69 x73False)False)((x71 (x69 x67) (x74 x73 x9) = x74 (x69 x67) x9False)False)((x71 (x69 x67) x73 = x69 x67False)False)((x71 (x69 x67) x10 = x10False)False)((x71 (x69 x9) (x74 (x69 x67) x9) = x67False)False)((x71 (x69 x9) (x74 (x69 x73) x67) = x74 x9 x67False)False)((x71 (x69 x9) (x74 (x69 x73) x9) = x73False)False)((x71 (x69 x9) (x74 x67 x9) = x69 x67False)False)((x71 (x69 x9) (x74 x73 x67) = x74 (x69 x9) x67False)False)((x71 (x69 x9) (x74 x73 x9) = x69 x73False)False)((x71 (x69 x9) x73 = x69 x9False)False)((x71 (x69 x9) x10 = x10False)False)((x71 x67 (x74 (x69 x9) x67) = x69 x9False)False)((x71 x67 (x74 (x69 x73) x67) = x69 x73False)False)((x71 x67 (x74 (x69 x73) x9) = x74 (x69 x67) x9False)False)((x71 x67 (x74 x9 x67) = x9False)False)((x71 x67 (x74 x73 x67) = x73False)False)((x71 x67 (x74 x73 x9) = x74 x67 x9False)False)((x71 x67 x73 = x67False)False)((x71 x67 x10 = x10False)False)((x71 x9 (x74 (x69 x67) x9) = x69 x67False)False)((x71 x9 (x74 (x69 x73) x67) = x74 (x69 x9) x67False)False)((x71 x9 (x74 (x69 x73) x9) = x69 x73False)False)((x71 x9 (x74 x67 x9) = x67False)False)((x71 x9 (x74 x73 x67) = x74 x9 x67False)False)((x71 x9 (x74 x73 x9) = x73False)False)((x71 x9 x73 = x9False)False)((x71 x9 x10 = x10False)False)((x71 x73 (x74 (x69 x67) x9) = x74 (x69 x67) x9False)False)((x71 x73 (x74 (x69 x9) x67) = x74 (x69 x9) x67False)False)((x71 x73 (x74 (x69 x73) x67) = x74 (x69 x73) x67False)False)((x71 x73 (x74 (x69 x73) x9) = x74 (x69 x73) x9False)False)((x71 x73 (x74 x67 x9) = x74 x67 x9False)False)((x71 x73 (x74 x9 x67) = x74 x9 x67False)False)((x71 x73 (x74 x73 x67) = x74 x73 x67False)False)((x71 x73 (x74 x73 x9) = x74 x73 x9False)False)((x71 x73 (x69 x67) = x69 x67False)False)((x71 x73 (x69 x9) = x69 x9False)False)((x71 x73 x67 = x67False)False)((x71 x73 x9 = x9False)False)((x71 x73 x73 = x73False)False)((x71 x73 x10 = x10False)False)((x71 x10 (x74 x9 x67) = x10False)False)((x71 x10 (x74 x73 x67) = x10False)False)((x71 x10 (x74 x73 x9) = x10False)False)((x71 x10 (x69 x67) = x10False)False)((x71 x10 (x69 x9) = x10False)False)((x71 x10 x67 = x10False)False)((x71 x10 x9 = x10False)False)((x71 x10 x73 = x10False)False)((x71 x10 x10 = x10False)False)((x74 (x69 x9) x9 = x69 x73False)False)((x74 (x69 x73) x9 = x74 (x69 x73) x9False)False)((x74 (x69 x73) x73 = x69 x73False)False)((x74 x67 x67 = x73False)False)((x74 x67 x9 = x74 x67 x9False)False)((x74 x9 x67 = x74 x9 x67False)False)((x74 x9 x9 = x73False)False)((x74 x9 x73 = x9False)False)((x74 x73 (x74 (x69 x67) x9) = x74 (x69 x9) x67False)False)((x74 x73 (x74 (x69 x73) x67) = x69 x67False)False)((x74 x73 (x74 (x69 x73) x9) = x69 x9False)False)((x74 x73 (x74 x67 x9) = x74 x9 x67False)False)((x74 x73 (x74 x9 x67) = x74 x67 x9False)False)((x74 x73 (x74 x73 x67) = x67False)False)((x74 x73 (x74 x73 x9) = x9False)False)((x74 x73 (x69 x67) = x74 (x69 x73) x67False)False)((x74 x73 (x69 x9) = x74 (x69 x73) x9False)False)((x74 x73 (x69 x73) = x69 x73False)False)((x74 x73 x67 = x74 x73 x67False)False)((x74 x73 x9 = x74 x73 x9False)False)((x74 x73 x73 = x73False)False)((x72 (x74 (x69 x67) x9) (x74 (x69 x67) x9) = x10False)False)((x72 (x74 (x69 x67) x9) (x74 (x69 x73) x9) = x69 x73False)False)((x72 (x74 (x69 x67) x9) (x74 x67 x9) = x69 x67False)False)((x72 (x74 (x69 x67) x9) (x74 x73 x9) = x69 x9False)False)((x72 (x74 (x69 x67) x9) (x69 x67) = x74 x67 x9False)False)((x72 (x74 (x69 x67) x9) (x69 x9) = x74 x73 x9False)False)((x72 (x74 (x69 x67) x9) (x69 x73) = x74 (x69 x73) x9False)False)((x72 (x74 (x69 x67) x9) x10 = x74 (x69 x67) x9False)False)((x72 (x74 (x69 x9) x67) (x74 (x69 x9) x67) = x10False)False)((x72 (x74 (x69 x9) x67) (x74 (x69 x73) x67) = x74 (x69 x73) x67False)False)((x72 (x74 (x69 x9) x67) (x74 x73 x67) = x69 x73False)False)((x72 (x74 (x69 x9) x67) (x69 x73) = x74 x73 x67False)False)((x72 (x74 (x69 x73) x67) (x74 (x69 x9) x67) = x74 x73 x67False)False)((x72 (x74 (x69 x73) x67) (x74 (x69 x73) x67) = x10False)False)((x72 (x74 (x69 x73) x67) (x74 x9 x67) = x69 x73False)False)((x72 (x74 (x69 x73) x67) (x74 x73 x67) = x74 (x69 x9) x67False)False)((x72 (x74 (x69 x73) x67) (x69 x73) = x74 x9 x67False)False)((x72 (x74 (x69 x73) x67) x10 = x74 (x69 x73) x67False)False)((x72 (x74 (x69 x73) x9) (x74 (x69 x67) x9) = x73False)False)((x72 (x74 (x69 x73) x9) (x74 (x69 x73) x9) = x10False)False)((x72 (x74 (x69 x73) x9) (x74 x67 x9) = x69 x9False)False)((x72 (x74 (x69 x73) x9) (x74 x73 x9) = x69 x73False)False)((x72 (x74 (x69 x73) x9) (x69 x9) = x74 x67 x9False)False)((x72 (x74 (x69 x73) x9) (x69 x73) = x74 x73 x9False)False)((x72 (x74 (x69 x73) x9) x73 = x74 (x69 x67) x9False)False)((x72 (x74 (x69 x73) x9) x10 = x74 (x69 x73) x9False)False)((x72 (x74 x67 x9) (x74 (x69 x67) x9) = x67False)False)((x72 (x74 x67 x9) (x74 (x69 x73) x9) = x9False)False)((x72 (x74 x67 x9) (x74 x67 x9) = x10False)False)((x72 (x74 x67 x9) (x74 x73 x9) = x73False)False)((x72 (x74 x67 x9) x67 = x74 (x69 x67) x9False)False)((x72 (x74 x67 x9) x9 = x74 (x69 x73) x9False)False)((x72 (x74 x67 x9) x73 = x74 x73 x9False)False)((x72 (x74 x67 x9) x10 = x74 x67 x9False)False)((x72 (x74 x9 x67) (x74 (x69 x73) x67) = x73False)False)((x72 (x74 x9 x67) (x74 x9 x67) = x10False)False)((x72 (x74 x9 x67) (x74 x73 x67) = x74 x73 x67False)False)((x72 (x74 x9 x67) x73 = x74 (x69 x73) x67False)False)((x72 (x74 x9 x67) x10 = x74 x9 x67False)False)((x72 (x74 x73 x67) (x74 (x69 x9) x67) = x73False)False)((x72 (x74 x73 x67) (x74 (x69 x73) x67) = x74 x9 x67False)False)((x72 (x74 x73 x67) (x74 x9 x67) = x74 (x69 x73) x67False)False)((x72 (x74 x73 x67) (x74 x73 x67) = x10False)False)((x72 (x74 x73 x67) x73 = x74 (x69 x9) x67False)False)((x72 (x74 x73 x67) x10 = x74 x73 x67False)False)((x72 (x74 x73 x9) (x74 (x69 x67) x9) = x9False)False)((x72 (x74 x73 x9) (x74 (x69 x73) x9) = x73False)False)((x72 (x74 x73 x9) (x74 x67 x9) = x69 x73False)False)((x72 (x74 x73 x9) (x74 x73 x9) = x10False)False)((x72 (x74 x73 x9) (x69 x73) = x74 x67 x9False)False)((x72 (x74 x73 x9) x9 = x74 (x69 x67) x9False)False)((x72 (x74 x73 x9) x73 = x74 (x69 x73) x9False)False)((x72 (x74 x73 x9) x10 = x74 x73 x9False)False)((x72 (x69 x67) (x74 (x69 x67) x9) = x74 (x69 x67) x9False)False)((x72 (x69 x67) (x69 x67) = x10False)False)((x72 (x69 x67) (x69 x9) = x69 x73False)False)((x72 (x69 x67) (x69 x73) = x69 x9False)False)((x72 (x69 x67) x10 = x69 x67False)False)((x72 (x69 x9) (x74 (x69 x67) x9) = x74 (x69 x73) x9False)False)((x72 (x69 x9) (x74 (x69 x73) x9) = x74 (x69 x67) x9False)False)((x72 (x69 x9) (x69 x67) = x73False)False)((x72 (x69 x9) (x69 x9) = x10False)False)((x72 (x69 x9) (x69 x73) = x69 x73False)False)((x72 (x69 x9) x73 = x69 x67False)False)((x72 (x69 x9) x10 = x69 x9False)False)((x72 (x69 x73) (x74 (x69 x67) x9) = x74 x73 x9False)False)((x72 (x69 x73) (x74 (x69 x9) x67) = x74 (x69 x73) x67False)False)((x72 (x69 x73) (x74 (x69 x73) x67) = x74 (x69 x9) x67False)False)((x72 (x69 x73) (x74 (x69 x73) x9) = x74 (x69 x73) x9False)False)((x72 (x69 x73) (x74 x73 x9) = x74 (x69 x67) x9False)False)((x72 (x69 x73) (x69 x67) = x9False)False)((x72 (x69 x73) (x69 x9) = x73False)False)((x72 (x69 x73) (x69 x73) = x10False)False)((x72 (x69 x73) x9 = x69 x67False)False)((x72 (x69 x73) x73 = x69 x9False)False)((x72 (x69 x73) x10 = x69 x73False)False)((x72 x67 (x74 x67 x9) = x74 x67 x9False)False)((x72 x67 x67 = x10False)False)((x72 x67 x9 = x73False)False)((x72 x67 x73 = x9False)False)((x72 x67 x10 = x67False)False)((x72 x9 (x74 x67 x9) = x74 x73 x9False)False)((x72 x9 (x74 x73 x9) = x74 x67 x9False)False)((x72 x9 (x69 x73) = x67False)False)((x72 x9 x67 = x69 x73False)False)((x72 x9 x9 = x10False)False)((x72 x9 x73 = x73False)False)((x72 x9 x10 = x9False)False)((x72 x73 (x74 (x69 x73) x9) = x74 x67 x9False)False)((x72 x73 (x74 x67 x9) = x74 (x69 x73) x9False)False)((x72 x73 (x74 x9 x67) = x74 x73 x67False)False)((x72 x73 (x74 x73 x67) = x74 x9 x67False)False)((x72 x73 (x74 x73 x9) = x74 x73 x9False)False)((x72 x73 (x69 x9) = x67False)False)((x72 x73 (x69 x73) = x9False)False)((x72 x73 x67 = x69 x9False)False)((x72 x73 x9 = x69 x73False)False)((x72 x73 x73 = x10False)False)((x72 x73 x10 = x73False)False)((x72 x10 (x74 (x69 x67) x9) = x74 x67 x9False)False)((x72 x10 (x74 (x69 x73) x9) = x74 x73 x9False)False)((x72 x10 (x74 x67 x9) = x74 (x69 x67) x9False)False)((x72 x10 (x74 x9 x67) = x74 (x69 x9) x67False)False)((x72 x10 (x74 x73 x67) = x74 (x69 x73) x67False)False)((x72 x10 (x74 x73 x9) = x74 (x69 x73) x9False)False)((x72 x10 (x69 x67) = x67False)False)((x72 x10 (x69 x9) = x9False)False)((x72 x10 (x69 x73) = x73False)False)((x72 x10 x67 = x69 x67False)False)((x72 x10 x9 = x69 x9False)False)((x72 x10 x73 = x69 x73False)False)((x72 x10 x10 = x10False)False)((x7 (x74 (x69 x67) x9) (x74 (x69 x67) x9) = x69 x67False)False)((x7 (x74 (x69 x67) x9) (x74 x67 x9) = x10False)False)((x7 (x74 (x69 x67) x9) (x74 x73 x9) = x69 x73False)False)((x7 (x74 (x69 x67) x9) x9 = x74 x73 x9False)False)((x7 (x74 (x69 x67) x9) x73 = x74 (x69 x73) x9False)False)((x7 (x74 (x69 x9) x67) (x74 (x69 x73) x67) = x69 x73False)False)((x7 (x74 (x69 x9) x67) (x74 x9 x67) = x10False)False)((x7 (x74 (x69 x9) x67) x73 = x74 x73 x67False)False)((x7 (x74 (x69 x73) x67) (x74 (x69 x9) x67) = x69 x73False)False)((x7 (x74 (x69 x73) x67) (x74 (x69 x73) x67) = x74 (x69 x9) x67False)False)((x7 (x74 (x69 x73) x67) (x74 x9 x67) = x74 x73 x67False)False)((x7 (x74 (x69 x73) x67) (x74 x73 x67) = x10False)False)((x7 (x74 (x69 x73) x67) x73 = x74 x9 x67False)False)((x7 (x74 (x69 x73) x9) (x74 (x69 x67) x9) = x69 x9False)False)((x7 (x74 (x69 x73) x9) (x74 (x69 x73) x9) = x69 x73False)False)((x7 (x74 (x69 x73) x9) (x74 x67 x9) = x73False)False)((x7 (x74 (x69 x73) x9) (x74 x73 x9) = x10False)False)((x7 (x74 (x69 x73) x9) (x69 x73) = x74 (x69 x67) x9False)False)((x7 (x74 (x69 x73) x9) x9 = x74 x67 x9False)False)((x7 (x74 (x69 x73) x9) x73 = x74 x73 x9False)False)((x7 (x74 x67 x9) (x74 (x69 x67) x9) = x10False)False)((x7 (x74 x67 x9) (x74 (x69 x73) x9) = x73False)False)((x7 (x74 x67 x9) (x74 x67 x9) = x67False)False)((x7 (x74 x67 x9) (x74 x73 x9) = x9False)False)((x7 (x74 x67 x9) (x69 x9) = x74 (x69 x73) x9False)False)((x7 (x74 x67 x9) (x69 x73) = x74 x73 x9False)False)((x7 (x74 x67 x9) x10 = x74 x67 x9False)False)((x7 (x74 x9 x67) (x74 (x69 x9) x67) = x10False)False)((x7 (x74 x9 x67) (x74 (x69 x73) x67) = x74 x73 x67False)False)((x7 (x74 x9 x67) (x74 x73 x67) = x73False)False)((x7 (x74 x9 x67) x10 = x74 x9 x67False)False)((x7 (x74 x73 x67) (x74 (x69 x9) x67) = x74 (x69 x73) x67False)False)((x7 (x74 x73 x67) (x74 (x69 x73) x67) = x10False)False)((x7 (x74 x73 x67) (x74 x9 x67) = x73False)False)((x7 (x74 x73 x67) (x74 x73 x67) = x74 x9 x67False)False)((x7 (x74 x73 x9) (x74 (x69 x67) x9) = x69 x73False)False)((x7 (x74 x73 x9) (x74 (x69 x73) x9) = x10False)False)((x7 (x74 x73 x9) (x74 x67 x9) = x9False)False)((x7 (x74 x73 x9) (x74 x73 x9) = x73False)False)((x7 (x74 x73 x9) (x69 x9) = x74 (x69 x67) x9False)False)((x7 (x74 x73 x9) (x69 x73) = x74 (x69 x73) x9False)False)((x7 (x74 x73 x9) x73 = x74 x67 x9False)False)((x7 (x74 x73 x9) x10 = x74 x73 x9False)False)((x7 (x69 x67) (x74 x67 x9) = x74 (x69 x67) x9False)False)((x7 (x69 x67) x67 = x10False)False)((x7 (x69 x67) x9 = x69 x73False)False)((x7 (x69 x67) x73 = x69 x9False)False)((x7 (x69 x9) (x74 x67 x9) = x74 (x69 x73) x9False)False)((x7 (x69 x9) (x69 x73) = x69 x67False)False)((x7 (x69 x9) x67 = x73False)False)((x7 (x69 x9) x9 = x10False)False)((x7 (x69 x9) x73 = x69 x73False)False)((x7 (x69 x73) (x74 (x69 x73) x9) = x74 (x69 x67) x9False)False)((x7 (x69 x73) (x74 x67 x9) = x74 x73 x9False)False)((x7 (x69 x73) (x74 x9 x67) = x74 (x69 x73) x67False)False)((x7 (x69 x73) (x74 x73 x9) = x74 (x69 x73) x9False)False)((x7 (x69 x73) (x69 x9) = x69 x67False)False)((x7 (x69 x73) (x69 x73) = x69 x9False)False)((x7 (x69 x73) x67 = x9False)False)((x7 (x69 x73) x9 = x73False)False)((x7 (x69 x73) x73 = x10False)False)((x7 (x69 x73) x10 = x69 x73False)False)((x7 x67 (x69 x67) = x10False)False)((x7 x67 (x69 x9) = x73False)False)((x7 x67 (x69 x73) = x9False)False)((x7 x67 x10 = x67False)False)((x7 x9 (x74 (x69 x67) x9) = x74 x73 x9False)False)((x7 x9 (x74 (x69 x73) x9) = x74 x67 x9False)False)((x7 x9 (x69 x67) = x69 x73False)False)((x7 x9 (x69 x9) = x10False)False)((x7 x9 (x69 x73) = x73False)False)((x7 x9 x73 = x67False)False)((x7 x9 x10 = x9False)False)((x7 x73 (x74 (x69 x9) x67) = x74 x73 x67False)False)((x7 x73 (x74 (x69 x73) x67) = x74 x9 x67False)False)((x7 x73 (x74 (x69 x73) x9) = x74 x73 x9False)False)((x7 x73 (x74 x73 x9) = x74 x67 x9False)False)((x7 x73 (x69 x67) = x69 x9False)False)((x7 x73 (x69 x9) = x69 x73False)False)((x7 x73 (x69 x73) = x10False)False)((x7 x73 x9 = x67False)False)((x7 x73 x73 = x9False)False)((x7 x73 x10 = x73False)False)((x7 x10 (x74 (x69 x73) x9) = x74 (x69 x73) x9False)False)((x7 x10 (x74 x67 x9) = x74 x67 x9False)False)((x7 x10 (x74 x9 x67) = x74 x9 x67False)False)((x7 x10 (x74 x73 x9) = x74 x73 x9False)False)((x7 x10 (x69 x67) = x69 x67False)False)((x7 x10 (x69 x9) = x69 x9False)False)((x7 x10 (x69 x73) = x69 x73False)False)((x7 x10 x67 = x67False)False)((x7 x10 x9 = x9False)False)((x7 x10 x73 = x73False)False)((x7 x10 x10 = x10False)False)((x78 (x74 (x69 x73) x67) (x74 (x69 x73) x67)False)False)((x78 (x74 (x69 x73) x67) (x74 x9 x67)False)False)((x78 (x74 (x69 x73) x67) (x74 x73 x67)False)False)(x78 (x74 (x69 x73) x67) (x69 x73)False)((x78 (x74 (x69 x73) x67) x67False)False)((x78 (x74 (x69 x73) x67) x9False)False)((x78 (x74 (x69 x73) x67) x73False)False)((x78 (x74 (x69 x73) x67) x10False)False)((x78 (x74 (x69 x73) x9) (x74 (x69 x73) x9)False)False)((x78 (x74 (x69 x73) x9) (x74 x67 x9)False)False)((x78 (x74 (x69 x73) x9) (x74 x73 x9)False)False)(x78 (x74 (x69 x73) x9) (x69 x73)False)((x78 (x74 (x69 x73) x9) x67False)False)((x78 (x74 (x69 x73) x9) x9False)False)((x78 (x74 (x69 x73) x9) x73False)False)((x78 (x74 (x69 x73) x9) x10False)False)(x78 (x74 x67 x9) (x74 (x69 x73) x9)False)((x78 (x74 x67 x9) (x74 x67 x9)False)False)(x78 (x74 x67 x9) (x74 x73 x9)False)(x78 (x74 x67 x9) (x69 x73)False)((x78 (x74 x67 x9) x67False)False)((x78 (x74 x67 x9) x9False)False)(x78 (x74 x67 x9) x73False)(x78 (x74 x67 x9) x10False)(x78 (x74 x9 x67) (x74 (x69 x73) x67)False)((x78 (x74 x9 x67) (x74 x9 x67)False)False)(x78 (x74 x9 x67) (x74 x73 x67)False)(x78 (x74 x9 x67) (x74 x73 x9)False)(x78 (x74 x9 x67) (x69 x73)False)((x78 (x74 x9 x67) x67False)False)((x78 (x74 x9 x67) x9False)False)((x78 (x74 x9 x67) x73False)False)(x78 (x74 x9 x67) x10False)(x78 (x74 x73 x67) (x74 (x69 x73) x67)False)((x78 (x74 x73 x67) (x74 x9 x67)False)False)((x78 (x74 x73 x67) (x74 x73 x67)False)False)(x78 (x74 x73 x67) (x69 x73)False)((x78 (x74 x73 x67) x67False)False)((x78 (x74 x73 x67) x9False)False)((x78 (x74 x73 x67) x73False)False)(x78 (x74 x73 x67) x10False)(x78 (x74 x73 x9) (x74 (x69 x73) x9)False)((x78 (x74 x73 x9) (x74 x67 x9)False)False)((x78 (x74 x73 x9) (x74 x9 x67)False)False)((x78 (x74 x73 x9) (x74 x73 x9)False)False)(x78 (x74 x73 x9) (x69 x67)False)(x78 (x74 x73 x9) (x69 x9)False)(x78 (x74 x73 x9) (x69 x73)False)((x78 (x74 x73 x9) x67False)False)((x78 (x74 x73 x9) x9False)False)((x78 (x74 x73 x9) x73False)False)(x78 (x74 x73 x9) x10False)((x78 (x69 x67) (x74 x73 x9)False)False)((x78 (x69 x67) (x69 x67)False)False)((x78 (x69 x67) (x69 x9)False)False)((x78 (x69 x67) (x69 x73)False)False)((x78 (x69 x67) x67False)False)((x78 (x69 x67) x9False)False)((x78 (x69 x67) x73False)False)((x78 (x69 x67) x10False)False)((x78 (x69 x9) (x74 x73 x9)False)False)(x78 (x69 x9) (x69 x67)False)((x78 (x69 x9) (x69 x9)False)False)((x78 (x69 x9) (x69 x73)False)False)((x78 (x69 x9) x67False)False)((x78 (x69 x9) x9False)False)((x78 (x69 x9) x73False)False)((x78 (x69 x9) x10False)False)((x78 (x69 x73) (x74 (x69 x73) x67)False)False)((x78 (x69 x73) (x74 (x69 x73) x9)False)False)((x78 (x69 x73) (x74 x67 x9)False)False)((x78 (x69 x73) (x74 x9 x67)False)False)((x78 (x69 x73) (x74 x73 x67)False)False)((x78 (x69 x73) (x74 x73 x9)False)False)(x78 (x69 x73) (x69 x67)False)(x78 (x69 x73) (x69 x9)False)((x78 (x69 x73) (x69 x73)False)False)((x78 (x69 x73) x67False)False)((x78 (x69 x73) x9False)False)((x78 (x69 x73) x73False)False)((x78 (x69 x73) x10False)False)(x78 x67 (x74 (x69 x73) x67)False)(x78 x67 (x74 (x69 x73) x9)False)(x78 x67 (x74 x67 x9)False)(x78 x67 (x74 x9 x67)False)(x78 x67 (x74 x73 x67)False)(x78 x67 (x74 x73 x9)False)(x78 x67 (x69 x67)False)(x78 x67 (x69 x9)False)(x78 x67 (x69 x73)False)((x78 x67 x67False)False)(x78 x67 x9False)(x78 x67 x73False)(x78 x67 x10False)(x78 x9 (x74 (x69 x73) x67)False)(x78 x9 (x74 (x69 x73) x9)False)(x78 x9 (x74 x67 x9)False)(x78 x9 (x74 x9 x67)False)(x78 x9 (x74 x73 x67)False)(x78 x9 (x74 x73 x9)False)(x78 x9 (x69 x67)False)(x78 x9 (x69 x9)False)(x78 x9 (x69 x73)False)((x78 x9 x67False)False)((x78 x9 x9False)False)(x78 x9 x73False)(x78 x9 x10False)(x78 x73 (x74 (x69 x73) x67)False)(x78 x73 (x74 (x69 x73) x9)False)((x78 x73 (x74 x67 x9)False)False)(x78 x73 (x74 x9 x67)False)(x78 x73 (x74 x73 x67)False)(x78 x73 (x74 x73 x9)False)(x78 x73 (x69 x67)False)(x78 x73 (x69 x9)False)(x78 x73 (x69 x73)False)((x78 x73 x67False)False)((x78 x73 x9False)False)((x78 x73 x73False)False)(x78 x73 x10False)(x78 x10 (x74 (x69 x73) x67)False)(x78 x10 (x74 (x69 x73) x9)False)((x78 x10 (x74 x67 x9)False)False)((x78 x10 (x74 x9 x67)False)False)((x78 x10 (x74 x73 x67)False)False)((x78 x10 (x74 x73 x9)False)False)(x78 x10 (x69 x67)False)(x78 x10 (x69 x9)False)(x78 x10 (x69 x73)False)((x78 x10 x67False)False)((x78 x10 x9False)False)((x78 x10 x73False)False)((x78 x10 x10False)False)(∀ x80 x81 . x65 x81x65 x80(x78 x81 x81False)False)(∀ x80 . (x6 x80 x80False)False)(∀ x80 x81 x82 . (x0 x82False)(x0 x80False)x4 x80 (x3 x82)x4 x81 x80(x66 x81 x82 x80False)False)(∀ x80 x81 x82 . (x0 x82False)(x0 x80False)x4 x80 (x3 x82)x66 x81 x82 x80(x4 x81 x80False)False)(∀ x80 x81 . x4 x81 x68x79 x80(x64 x81 x80 = x71 x81 x80False)False)(∀ x80 x81 . x4 x81 x68x79 x80(x11 x81 x80 = x7 x81 x80False)False)((x5 = x2False)False)((x8 = x70False)False)(∀ x80 x81 x82 x83 x84 . x63 x84x4 x84 (x3 (x62 (x62 x81 x80) x68))x4 x83 x81x4 x82 x80(x60 x81 x80 x84 x83 x82 = x61 x84 x83 x82False)False)(∀ x80 x81 . x4 x81 x68x79 x80(x12 x81 x80 = x74 x81 x80False)False)(∀ x80 . (x59 (x58 x80)False)False)(∀ x80 . (x13 (x58 x80) x80False)False)(∀ x80 . (x63 (x58 x80)False)False)(∀ x80 . (x14 (x58 x80) x80False)False)(∀ x80 . (x57 (x58 x80)False)False)((x15 x16False)False)(x0 x16False)((x65 x17False)False)((x0 x17False)False)((x79 x18False)False)((x65 x18False)False)((x75 x18False)False)((x0 x18False)False)((x15 x19False)False)((x77 x56False)False)((x65 x56False)False)((x79 x55False)False)((x77 x55False)False)((x65 x55False)False)((x75 x55False)False)(∀ x80 . (x54 (x53 x80)False)False)(∀ x80 . (x63 (x53 x80)False)False)(∀ x80 . (x52 (x53 x80) x80False)False)(∀ x80 . (x57 (x53 x80)False)False)((x76 x51False)False)((x65 x51False)False)((x79 x50False)False)((x76 x50False)False)((x65 x50False)False)((x75 x50False)False)(x0 x49False)((x20 x21False)False)((x48 x21False)False)((x22 x21False)False)(x0 x21False)((x65 x23False)False)((x79 x47False)False)((x0 x24False)False)((x59 x46False)False)((x63 x46False)False)((x57 x46False)False)(∀ x80 x81 . (x52 (x25 x80 x81) x80False)False)(∀ x80 x81 . (x14 (x25 x81 x80) x80False)False)(∀ x80 x81 . (x57 (x25 x80 x81)False)False)(∀ x80 x81 . (x0 (x25 x80 x81)False)False)(∀ x80 x81 . (x4 (x25 x80 x81) (x3 (x62 x81 x80))False)False)((x20 x45False)False)(∀ x80 x81 . (x26 (x27 x80 x81) x81 x80False)False)(∀ x80 x81 . (x63 (x27 x80 x81)False)False)(∀ x80 x81 . (x52 (x27 x80 x81) x80False)False)(∀ x80 x81 . (x14 (x27 x81 x80) x80False)False)(∀ x80 x81 . (x57 (x27 x80 x81)False)False)(∀ x80 x81 . (x4 (x27 x80 x81) (x3 (x62 x81 x80))False)False)(∀ x80 . x75 x80(x69 (x69 x80) = x80False)False)(∀ x80 x81 . (x77 x81False)x79 x81(x77 x80False)x79 x80x77 (x7 x81 x80)False)(∀ x80 x81 . x79 x81x79 x80(x79 (x74 x81 x80)False)False)(x44 x68False)(∀ x80 x81 . x79 x81x79 x80(x79 (x72 x81 x80)False)False)(x44 x43False)(∀ x80 x81 . x79 x81x79 x80(x79 (x71 x81 x80)False)False)((x20 x70False)False)(x0 x70False)(x44 x42False)(∀ x80 x81 . x79 x81x79 x80(x79 (x7 x81 x80)False)False)(x0 x42False)(∀ x80 . x79 x80(x79 (x69 x80)False)False)(∀ x80 . x79 x80(x75 (x69 x80)False)False)(x0 x43False)(∀ x80 x81 . (x76 x81False)x79 x81(x76 x80False)x79 x80x77 (x74 x81 x80)False)(∀ x80 x81 . (x77 x81False)x79 x81(x77 x80False)x79 x80x77 (x74 x81 x80)False)(∀ x80 x81 . (x77 x81False)x79 x81(x76 x80False)x79 x80x76 (x74 x80 x81)False)(∀ x80 x81 . (x77 x81False)x79 x81(x76 x80False)x79 x80x76 (x74 x81 x80)False)(∀ x80 x81 x82 . x57 x82x63 x82x59 x82(x15 (x61 x82 x80 x81)False)False)(∀ x80 x81 . (x77 x81False)x79 x81(x77 x80False)x79 x80x77 (x71 x81 x80)False)(∀ x80 x81 . (x76 x81False)x79 x81(x76 x80False)x79 x80x77 (x71 x81 x80)False)(∀ x80 x81 . (x76 x81False)x79 x81(x77 x80False)x79 x80x76 (x71 x80 x81)False)(∀ x80 x81 . (x76 x81False)x79 x81(x77 x80False)x79 x80x76 (x71 x81 x80)False)(∀ x80 x81 . x77 x81x79 x81(x77 x80False)x79 x80(x76 (x72 x80 x81)False)False)(∀ x80 x81 . x77 x81x79 x81(x77 x80False)x79 x80(x77 (x72 x81 x80)False)False)(∀ x80 x81 . x76 x81x79 x81(x76 x80False)x79 x80(x77 (x72 x80 x81)False)False)((x0 x2False)False)(x0 x68False)(∀ x80 x81 . x76 x81x79 x81(x76 x80False)x79 x80(x76 (x72 x81 x80)False)False)(∀ x80 x81 . (x77 x81False)x79 x81(x76 x80False)x79 x80x76 (x72 x80 x81)False)(∀ x80 x81 . (x77 x81False)x79 x81(x76 x80False)x79 x80x77 (x72 x81 x80)False)(∀ x80 . (x77 x80False)x79 x80x76 (x69 x80)False)(∀ x80 . (x77 x80False)x79 x80(x75 (x69 x80)False)False)(∀ x80 . (x76 x80False)x79 x80x77 (x69 x80)False)(∀ x80 . (x76 x80False)x79 x80(x75 (x69 x80)False)False)(∀ x80 x81 . x77 x81x79 x81(x76 x80False)x79 x80(x77 (x7 x80 x81)False)False)(∀ x80 x81 . x77 x81x79 x81(x76 x80False)x79 x80(x77 (x7 x81 x80)False)False)(∀ x80 x81 . x76 x81x79 x81(x77 x80False)x79 x80(x76 (x7 x80 x81)False)False)(∀ x80 x81 . x76 x81x79 x81(x77 x80False)x79 x80(x76 (x7 x81 x80)False)False)(∀ x80 x81 . (x76 x81False)x79 x81(x76 x80False)x79 x80x76 (x7 x81 x80)False)(∀ x80 x81 . (x0 x81False)(x0 x80False)x4 x80 (x3 x81)(x66 (x41 x80 x81) x81 x80False)False)(∀ x80 . (x4 (x28 x80) x80False)False)(∀ x80 x81 x82 . (x0 x82False)(x0 x80False)x4 x80 (x3 x82)x66 x81 x82 x80(x4 x81 x82False)False)(∀ x80 x81 . x4 x81 x68x79 x80(x4 (x64 x81 x80) x68False)False)(∀ x80 x81 . x4 x81 x68x79 x80(x4 (x11 x81 x80) x68False)False)((x66 x5 x68 x8False)False)((x4 x8 (x3 x68)False)False)(∀ x80 . x75 x80(x75 (x69 x80)False)False)(∀ x80 x81 x82 x83 x84 . x63 x84x4 x84 (x3 (x62 (x62 x81 x80) x68))x4 x83 x81x4 x82 x80(x4 (x60 x81 x80 x84 x83 x82) x68False)False)(∀ x80 x81 . x4 x81 x68x79 x80(x4 (x12 x81 x80) x68False)False)(∀ x80 x81 . x63 x81x26 x81 (x62 x80 x80) x68x4 x81 (x3 (x62 (x62 x80 x80) x68))x38 x81 x80 = x37 x81 x80x60 x80 x80 x81 (x38 x81 x80) (x37 x81 x80) = x5x60 x80 x80 x81 (x38 x81 x80) (x37 x81 x80) = x60 x80 x80 x81 (x37 x81 x80) (x38 x81 x80)x78 (x60 x80 x80 x81 (x38 x81 x80) (x39 x81 x80)) (x11 (x60 x80 x80 x81 (x38 x81 x80) (x37 x81 x80)) (x60 x80 x80 x81 (x37 x81 x80) (x39 x81 x80)))(x40 x80 x81False)False)(∀ x80 x81 . x63 x81x26 x81 (x62 x80 x80) x68x4 x81 (x3 (x62 (x62 x80 x80) x68))x38 x81 x80 = x37 x81 x80(x38 x81 x80 = x37 x81 x80False)x60 x80 x80 x81 (x38 x81 x80) (x37 x81 x80) = x60 x80 x80 x81 (x37 x81 x80) (x38 x81 x80)x78 (x60 x80 x80 x81 (x38 x81 x80) (x39 x81 x80)) (x11 (x60 x80 x80 x81 (x38 x81 x80) (x37 x81 x80)) (x60 x80 x80 x81 (x37 x81 x80) (x39 x81 x80)))(x40 x80 x81False)False)(∀ x80 x81 . x63 x81x26 x81 (x62 x80 x80) x68x4 x81 (x3 (x62 (x62 x80 x80) x68))(x60 x80 x80 x81 (x38 x81 x80) (x37 x81 x80) = x5False)x60 x80 x80 x81 (x38 x81 x80) (x37 x81 x80) = x5x60 x80 x80 x81 (x38 x81 x80) (x37 x81 x80) = x60 x80 x80 x81 (x37 x81 x80) (x38 x81 x80)x78 (x60 x80 x80 x81 (x38 x81 x80) (x39 x81 x80)) (x11 (x60 x80 x80 x81 (x38 x81 x80) (x37 x81 x80)) (x60 x80 x80 x81 (x37 x81 x80) (x39 x81 x80)))(x40 x80 x81False)False)(∀ x80 x81 . x63 x81x26 x81 (x62 x80 x80) x68x4 x81 (x3 (x62 (x62 x80 x80) x68))(x60 x80 x80 x81 (x38 x81 x80) (x37 x81 x80) = x5False)(x38 x81 x80 = x37 x81 x80False)x60 x80 x80 x81 (x38 x81 x80) (x37 x81 x80) = x60 x80 x80 x81 (x37 x81 x80) (x38 x81 x80)x78 (x60 x80 x80 x81 (x38 x81 x80) (x39 x81 x80)) (x11 (x60 x80 x80 x81 (x38 x81 x80) (x37 x81 x80)) (x60 x80 x80 x81 (x37 x81 x80) (x39 x81 x80)))(x40 x80 x81False)False)(∀ x80 x81 . x63 x81x26 x81 (x62 x80 x80) x68x4 x81 (x3 (x62 (x62 x80 x80) x68))(x4 (x39 x81 x80) x80False)(x40 x80 x81False)False)(∀ x80 x81 . x63 x81x26 x81 (x62 x80 x80) x68x4 x81 (x3 (x62 (x62 x80 x80) x68))(x4 (x37 x81 x80) x80False)(x40 x80 x81False)False)(∀ x80 x81 . x63 x81x26 x81 (x62 x80 x80) x68x4 x81 (x3 (x62 (x62 x80 x80) x68))(x4 (x38 x81 x80) x80False)(x40 x80 x81False)False)(∀ x80 x81 x82 x83 x84 . x63 x84x26 x84 (x62 x80 x80) x68x4 x84 (x3 (x62 (x62 x80 x80) x68))x40 x80 x84x4 x83 x80x4 x81 x80x4 x82 x80(x78 (x60 x80 x80 x84 x83 x82) (x11 (x60 x80 x80 x84 x83 x81) (x60 x80 x80 x84 x81 x82))False)False)(∀ x80 x81 x82 x83 x84 . x63 x84x26 x84 (x62 x80 x80) x68x4 x84 (x3 (x62 (x62 x80 x80) x68))x40 x80 x84x4 x83 x80x4 x81 x80x4 x82 x80(x60 x80 x80 x84 x83 x81 = x60 x80 x80 x84 x81 x83False)False)(∀ x80 x81 x82 x83 x84 . x63 x84x26 x84 (x62 x80 x80) x68x4 x84 (x3 (x62 (x62 x80 x80) x68))x40 x80 x84x4 x83 x80x4 x81 x80x4 x82 x80x83 = x81(x60 x80 x80 x84 x83 x81 = x5False)False)(∀ x80 x81 x82 x83 x84 . x63 x84x26 x84 (x62 x80 x80) x68x4 x84 (x3 (x62 (x62 x80 x80) x68))x40 x80 x84x4 x83 x80x4 x81 x80x4 x82 x80x60 x80 x80 x84 x83 x81 = x5(x83 = x81False)False)(∀ x80 x81 . x65 x81x65 x80(x78 x81 x80False)(x78 x80 x81False)False)(∀ x80 x81 . x4 x81 x68x79 x80(x64 x81 x80 = x64 x80 x81False)False)(∀ x80 x81 . x4 x81 x68x79 x80(x11 x81 x80 = x11 x80 x81False)False)(∀ x80 x81 . x75 x81x75 x80(x71 x81 x80 = x71 x80 x81False)False)(∀ x80 x81 . x75 x81x75 x80(x7 x81 x80 = x7 x80 x81False)False)(∀ x80 . x0 x80x57 x80(x59 x80False)False)(∀ x80 . x0 x80x57 x80(x57 x80False)False)(∀ x80 . x0 x80(x36 x80False)False)(∀ x80 . x65 x80(x76 x80False)(x77 x80False)(x65 x80False)False)(∀ x80 . x65 x80(x76 x80False)(x77 x80False)(x0 x80False)False)(∀ x80 . x57 x80x59 x80(x29 x80False)False)(∀ x80 . x57 x80x59 x80(x57 x80False)False)(∀ x80 . x4 x80 x70(x15 x80False)False)(∀ x80 x81 x82 . (x0 x82False)(x0 x80False)x4 x81 (x3 (x62 x82 x80))x63 x81x26 x81 x82 x80(x26 x81 x82 x80False)False)(∀ x80 x81 x82 . (x0 x82False)(x0 x80False)x4 x81 (x3 (x62 x82 x80))x63 x81x26 x81 x82 x80x0 x81False)(∀ x80 x81 x82 . (x0 x82False)(x0 x80False)x4 x81 (x3 (x62 x82 x80))x63 x81x26 x81 x82 x80(x63 x81False)False)(∀ x80 . x0 x80x65 x80x77 x80False)(∀ x80 . x0 x80x65 x80x76 x80False)(∀ x80 . x0 x80x65 x80(x65 x80False)False)(∀ x80 . x57 x80x59 x80(x52 x80 x43False)False)(∀ x80 . x57 x80x59 x80(x57 x80False)False)(∀ x80 . x0 x80(x15 x80False)False)(∀ x80 . (x0 x80False)x65 x80(x76 x80False)(x77 x80False)False)(∀ x80 . (x0 x80False)x65 x80(x76 x80False)(x65 x80False)False)(∀ x80 . x57 x80x29 x80(x30 x80False)False)(∀ x80 . x57 x80x29 x80(x57 x80False)False)(∀ x80 . x15 x80(x20 x80False)False)(∀ x80 . x65 x80x77 x80x76 x80False)(∀ x80 . x65 x80x77 x80(x65 x80False)False)(∀ x80 . x65 x80x77 x80x0 x80False)(∀ x80 . x57 x80x29 x80(x31 x80False)False)(∀ x80 . x57 x80x29 x80(x57 x80False)False)(∀ x80 x81 . x20 x81x4 x80 x81(x20 x80False)False)(∀ x80 . (x0 x80False)x65 x80(x77 x80False)(x76 x80False)False)(∀ x80 . (x0 x80False)x65 x80(x77 x80False)(x65 x80False)False)(∀ x80 . x79 x80(x65 x80False)False)(∀ x80 . x57 x80x52 x80 x43(x29 x80False)False)(∀ x80 . x57 x80x52 x80 x43(x57 x80False)False)(∀ x80 x81 x82 . x0 x82x4 x80 (x3 (x62 x81 x82))(x0 x80False)False)(∀ x80 . x0 x80(x54 x80False)False)(∀ x80 x81 . x4 x81 (x3 (x62 x80 x80))x26 x81 x80 x80(x13 x81 x80False)False)(∀ x80 . x65 x80x76 x80x77 x80False)(∀ x80 . x65 x80x76 x80(x65 x80False)False)(∀ x80 . x65 x80x76 x80x0 x80False)(∀ x80 . x79 x80(x75 x80False)False)(∀ x80 . x57 x80x52 x80 x42(x29 x80False)False)(∀ x80 . x57 x80x52 x80 x42(x57 x80False)False)(∀ x80 x81 x82 . x0 x82x4 x80 (x3 (x62 x82 x81))(x0 x80False)False)(∀ x80 . x0 x80(x20 x80False)False)(∀ x80 x81 x82 . (x0 x82False)x4 x80 (x3 (x62 x81 x82))x26 x80 x81 x82(x13 x80 x81False)False)(∀ x80 . x57 x80x52 x80 x8(x59 x80False)False)(∀ x80 . x57 x80x52 x80 x8(x57 x80False)False)(∀ x80 . x57 x80x52 x80 x68(x29 x80False)False)(∀ x80 . x57 x80x52 x80 x68(x57 x80False)False)(∀ x80 . x15 x80(x65 x80False)False)(∀ x80 . x15 x80(x79 x80False)False)(∀ x80 . x57 x80x52 x80 x42(x52 x80 x43False)False)(∀ x80 . x57 x80x52 x80 x42(x57 x80False)False)(∀ x80 x81 x82 . x4 x82 (x3 (x62 x80 x81))(x52 x82 x81False)False)(∀ x80 x81 x82 . x4 x82 (x3 (x62 x81 x80))(x14 x82 x81False)False)(∀ x80 . x22 x80x48 x80(x20 x80False)False)(∀ x80 x81 x82 . x0 x82x4 x80 (x3 (x62 x82 x81))x26 x80 x82 x81(x13 x80 x82False)False)(∀ x80 . x4 x80 x68(x79 x80False)False)(∀ x80 . x57 x80x59 x80(x52 x80 x42False)False)(∀ x80 . x57 x80x59 x80(x57 x80False)False)(∀ x80 x81 x82 . x4 x82 (x3 (x62 x80 x81))(x57 x82False)False)(∀ x80 . x20 x80(x48 x80False)False)(∀ x80 . x20 x80(x22 x80False)False)(∀ x80 x81 x82 . x4 x81 (x3 (x62 x82 x80))x13 x81 x82(x26 x81 x82 x80False)False)(∀ x80 x81 . x57 x81x59 x81x4 x80 (x3 x81)(x59 x80False)False)(∀ x80 x81 . x57 x81x52 x81 x42x4 x80 (x3 x81)(x52 x80 x42False)False)(∀ x80 x81 . x57 x81x52 x81 x43x4 x80 (x3 x81)(x52 x80 x43False)False)(∀ x80 x81 . x57 x81x29 x81x4 x80 (x3 x81)(x29 x80False)False)(∀ x80 x81 . x57 x81x31 x81x4 x80 (x3 x81)(x31 x80False)False)(∀ x80 x81 . x57 x81x30 x81x4 x80 (x3 x81)(x30 x80False)False)(∀ x80 x81 . x36 x81x4 x80 (x3 x81)(x36 x80False)False)(∀ x80 x81 . x1 x80 x81x1 x81 x80False)(x78 x5 (x60 x32 x32 x33 x34 x35)False)((x4 x35 x32False)False)((x4 x34 x32False)False)((x40 x32 x33False)False)((x4 x33 (x3 (x62 (x62 x32 x32) x68))False)False)((x26 x33 (x62 x32 x32) x68False)False)((x63 x33False)False)(x0 x32False)False
type
prop
theory
HotG
name
-
proof
PUVMo..
Megalodon
-
proofgold address
TMKnH..
creator
35127 PrPhD../d855f..
owner
35131 PrPhD../32a78..
term root
5950b..