Search for blocks/addresses/...

Proofgold Asset

asset id
5f68a0d009005be8e5df534703ac0886f9e8dd0687692b96b22f555ad029cc42
asset hash
1ff20583806722aa9444d5cef2d95fb5fef3ae71b18828d313b45a54b0843bcb
bday / block
35127
tx
56168..
preasset
doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Theorem d58dd.. : ∀ 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 . x78 x80(x80 = x79False)x78 x79False)(∀ x79 x80 . x0 x79 x80x78 x80False)(∀ x79 x80 . (x77 x80False)x62 x80x76 x80x63 x79x74 x79 (x75 x80) (x75 x80)x64 x79 (x75 x80) (x75 x80)x73 x79 (x71 (x72 (x75 x80) (x75 x80)))x65 x79 x80x66 x80 (x67 x79 x80) (x68 (x75 x80) (x75 x80) x79 (x67 x79 x80)) (x69 x79 x80) (x68 (x75 x80) (x75 x80) x79 (x69 x79 x80))(x70 x79 x80False)False)(∀ x79 x80 . (x77 x80False)x62 x80x76 x80x63 x79x74 x79 (x75 x80) (x75 x80)x64 x79 (x75 x80) (x75 x80)x73 x79 (x71 (x72 (x75 x80) (x75 x80)))x65 x79 x80(x73 (x69 x79 x80) (x75 x80)False)(x70 x79 x80False)False)(∀ x79 x80 . (x77 x80False)x62 x80x76 x80x63 x79x74 x79 (x75 x80) (x75 x80)x64 x79 (x75 x80) (x75 x80)x73 x79 (x71 (x72 (x75 x80) (x75 x80)))x65 x79 x80(x73 (x67 x79 x80) (x75 x80)False)(x70 x79 x80False)False)(∀ x79 x80 x81 x82 . (x77 x82False)x62 x82x76 x82x63 x79x74 x79 (x75 x82) (x75 x82)x64 x79 (x75 x82) (x75 x82)x73 x79 (x71 (x72 (x75 x82) (x75 x82)))x65 x79 x82x70 x79 x82x73 x80 (x75 x82)x73 x81 (x75 x82)(x66 x82 x80 (x68 (x75 x82) (x75 x82) x79 x80) x81 (x68 (x75 x82) (x75 x82) x79 x81)False)False)(∀ x79 x80 x81 x82 x83 x84 . (x77 x84False)x62 x84x76 x84x73 x79 (x75 x84)x73 x83 (x75 x84)x73 x80 (x75 x84)x73 x82 (x75 x84)x73 x81 (x75 x84)x66 x84 x79 x83 x80 x82x66 x84 x79 x83 x80 x81x66 x84 x79 x80 x83 x82x66 x84 x79 x80 x83 x81(x61 x84 x79 x83 x80False)(x82 = x81False)False)(∀ x79 . x78 x79(x79 = x1False)False)(∀ x79 x80 . (x77 x80False)x62 x80x76 x80x63 x79x74 x79 (x75 x80) (x75 x80)x64 x79 (x75 x80) (x75 x80)x73 x79 (x71 (x72 (x75 x80) (x75 x80)))x66 x80 (x60 x79 x80) (x59 x79 x80) (x68 (x75 x80) (x75 x80) x79 (x60 x79 x80)) (x68 (x75 x80) (x75 x80) x79 (x59 x79 x80))(x65 x79 x80False)False)(∀ x79 x80 . (x77 x80False)x62 x80x76 x80x63 x79x74 x79 (x75 x80) (x75 x80)x64 x79 (x75 x80) (x75 x80)x73 x79 (x71 (x72 (x75 x80) (x75 x80)))(x73 (x59 x79 x80) (x75 x80)False)(x65 x79 x80False)False)(∀ x79 x80 . (x77 x80False)x62 x80x76 x80x63 x79x74 x79 (x75 x80) (x75 x80)x64 x79 (x75 x80) (x75 x80)x73 x79 (x71 (x72 (x75 x80) (x75 x80)))(x73 (x60 x79 x80) (x75 x80)False)(x65 x79 x80False)False)(∀ x79 x80 x81 x82 . (x77 x82False)x62 x82x76 x82x63 x79x74 x79 (x75 x82) (x75 x82)x64 x79 (x75 x82) (x75 x82)x73 x79 (x71 (x72 (x75 x82) (x75 x82)))x65 x79 x82x73 x81 (x75 x82)x73 x80 (x75 x82)(x66 x82 x81 x80 (x68 (x75 x82) (x75 x82) x79 x81) (x68 (x75 x82) (x75 x82) x79 x80)False)False)(∀ x79 x80 x81 . x0 x79 x80x73 x80 (x71 x81)x78 x81False)(∀ x79 x80 x81 . x0 x80 x81x73 x81 (x71 x79)(x73 x80 x79False)False)(∀ x79 x80 . x58 x80 x79(x73 x80 (x71 x79)False)False)(∀ x79 x80 . x73 x80 (x71 x79)(x58 x80 x79False)False)(∀ x79 x80 . x73 x79 x80(x78 x80False)(x0 x79 x80False)False)(∀ x79 x80 . x0 x80 x79(x73 x80 x79False)False)(∀ x79 x80 x81 x82 . x63 x82x74 x82 x79 x80x73 x82 (x71 (x72 x79 x80))x63 x81x74 x81 x79 x80x73 x81 (x71 (x72 x79 x80))x57 x79 x80 x82 x81(x57 x79 x80 x81 x82False)False)(x78 x2False)(∀ x79 x80 x81 x82 . x63 x82x74 x82 x79 x80x73 x82 (x71 (x72 x79 x80))x63 x81x74 x81 x79 x80x73 x81 (x71 (x72 x79 x80))(x57 x79 x80 x82 x82False)False)(∀ x79 . (x58 x79 x79False)False)(∀ x79 x80 x81 x82 . x63 x82x74 x82 x79 x80x73 x82 (x71 (x72 x79 x80))x63 x81x74 x81 x79 x80x73 x81 (x71 (x72 x79 x80))x82 = x81(x57 x79 x80 x82 x81False)False)(∀ x79 x80 x81 x82 . x63 x82x74 x82 x79 x80x73 x82 (x71 (x72 x79 x80))x63 x81x74 x81 x79 x80x73 x81 (x71 (x72 x79 x80))x57 x79 x80 x82 x81(x82 = x81False)False)(∀ x79 . (x56 x79 = x55 x79False)False)(∀ x79 x80 x81 x82 . (x78 x82False)x63 x79x74 x79 x82 x81x73 x79 (x71 (x72 x82 x81))x73 x80 x82(x68 x82 x81 x79 x80 = x3 x79 x80False)False)(∀ x79 . (x63 (x54 x79)False)False)(∀ x79 . (x4 (x54 x79) x79False)False)(∀ x79 . (x53 (x54 x79)False)False)(∀ x79 . (x5 (x54 x79)False)False)((x52 x51False)False)(x78 x51False)(∀ x79 x80 . (x63 (x50 x79 x80)False)False)(∀ x79 x80 . (x6 (x50 x79 x80) x79False)False)(∀ x79 x80 . (x4 (x50 x80 x79) x79False)False)(∀ x79 x80 . (x5 (x50 x79 x80)False)False)(x49 x48False)((x63 x48False)False)((x5 x48False)False)(∀ x79 . (x7 x79False)x9 x79x78 (x8 x79)False)(∀ x79 . (x7 x79False)x9 x79(x73 (x8 x79) (x71 (x75 x79))False)False)((x63 x10False)False)((x53 x10False)False)((x5 x10False)False)(x78 x10False)(∀ x79 x80 . (x6 (x11 x79 x80) x79False)False)(∀ x79 x80 . (x4 (x11 x80 x79) x79False)False)(∀ x79 x80 . (x5 (x11 x79 x80)False)False)(∀ x79 x80 . (x78 x80False)(x78 x79False)x78 (x47 x79 x80)False)(∀ x79 x80 . (x78 x80False)(x78 x79False)(x63 (x47 x79 x80)False)False)(∀ x79 x80 . (x78 x80False)(x78 x79False)(x6 (x47 x79 x80) x79False)False)(∀ x79 x80 . (x78 x80False)(x78 x79False)(x4 (x47 x79 x80) x80False)False)(∀ x79 x80 . (x78 x80False)(x78 x79False)(x5 (x47 x79 x80)False)False)(∀ x79 x80 . (x78 x80False)(x78 x79False)(x73 (x47 x79 x80) (x71 (x72 x80 x79))False)False)((x63 x46False)False)((x53 x46False)False)((x5 x46False)False)(x78 x12False)((x53 x45False)False)((x5 x45False)False)(∀ x79 . (x44 (x43 x79) x79False)False)(∀ x79 . (x13 (x43 x79)False)False)(∀ x79 . (x42 (x43 x79)False)False)(∀ x79 . (x14 (x43 x79)False)False)(∀ x79 . (x41 (x43 x79)False)False)(∀ x79 . (x6 (x43 x79) x79False)False)(∀ x79 . (x4 (x43 x79) x79False)False)(∀ x79 . (x5 (x43 x79)False)False)(∀ x79 . (x73 (x43 x79) (x71 (x72 x79 x79))False)False)(∀ x79 . (x64 (x15 x79) x79 x79False)False)(∀ x79 . (x74 (x15 x79) x79 x79False)False)(∀ x79 . (x44 (x15 x79) x79False)False)(∀ x79 . (x63 (x15 x79)False)False)(∀ x79 . (x6 (x15 x79) x79False)False)(∀ x79 . (x4 (x15 x79) x79False)False)(∀ x79 . (x5 (x15 x79)False)False)(∀ x79 . (x73 (x15 x79) (x71 (x72 x79 x79))False)False)((x16 x17False)False)((x63 x17False)False)((x5 x17False)False)(∀ x79 . (x77 x79False)x9 x79x40 (x39 x79)False)(∀ x79 . (x77 x79False)x9 x79(x73 (x39 x79) (x71 (x75 x79))False)False)(∀ x79 . (x7 x79False)x9 x79(x40 (x38 x79)False)False)(∀ x79 . (x7 x79False)x9 x79x78 (x38 x79)False)(∀ x79 . (x7 x79False)x9 x79(x73 (x38 x79) (x71 (x75 x79))False)False)((x78 x18False)False)((x5 x37False)False)(x78 x37False)(∀ x79 x80 . (x63 (x36 x79 x80)False)False)(∀ x79 x80 . (x6 (x36 x79 x80) x79False)False)(∀ x79 x80 . (x4 (x36 x80 x79) x79False)False)(∀ x79 x80 . (x5 (x36 x79 x80)False)False)(∀ x79 x80 . (x73 (x36 x79 x80) (x71 (x72 x80 x79))False)False)(∀ x79 x80 . (x74 (x19 x79 x80) x80 x79False)False)(∀ x79 x80 . (x63 (x19 x79 x80)False)False)(∀ x79 x80 . (x6 (x19 x79 x80) x79False)False)(∀ x79 x80 . (x4 (x19 x80 x79) x79False)False)(∀ x79 x80 . (x5 (x19 x79 x80)False)False)(∀ x79 x80 . (x73 (x19 x79 x80) (x71 (x72 x80 x79))False)False)((x63 x20False)False)((x5 x20False)False)(∀ x79 . (x21 x79False)x9 x79x22 (x75 x79)False)(∀ x79 . x21 x79x9 x79(x22 (x75 x79)False)False)(∀ x79 . x77 x79x9 x79(x40 (x75 x79)False)False)(∀ x79 . (x77 x79False)x9 x79x40 (x75 x79)False)(∀ x79 x80 . (x5 (x72 x79 x80)False)False)(∀ x79 . (x16 (x55 x79)False)False)(∀ x79 . (x5 (x55 x79)False)False)(∀ x79 . (x13 (x55 x79)False)False)(∀ x79 . (x42 (x55 x79)False)False)(∀ x79 . (x14 (x55 x79)False)False)(∀ x79 . (x5 (x55 x79)False)False)(∀ x79 . (x63 (x55 x79)False)False)(∀ x79 . (x5 (x55 x79)False)False)(∀ x79 . (x7 x79False)x9 x79x78 (x75 x79)False)(∀ x79 . (x6 (x55 x79) x79False)False)(∀ x79 . (x4 (x55 x79) x79False)False)(∀ x79 . (x5 (x55 x79)False)False)((x78 x1False)False)(∀ x79 . x7 x79x9 x79(x78 (x75 x79)False)False)(∀ x79 x80 . x5 x80x35 x80x63 x80(x78 (x3 x80 x79)False)False)(∀ x79 x80 x81 . x52 x81x5 x79x6 x79 x81x63 x79(x63 (x3 x79 x80)False)False)(∀ x79 x80 x81 . x52 x81x5 x79x6 x79 x81x63 x79(x5 (x3 x79 x80)False)False)(∀ x79 . (x44 (x55 x79) x79False)False)(∀ x79 . (x63 (x55 x79)False)False)(∀ x79 . (x4 (x55 x79) x79False)False)(∀ x79 . (x5 (x55 x79)False)False)(∀ x79 . (x73 (x23 x79) x79False)False)((x9 x34False)False)((x76 x24False)False)(∀ x79 . x76 x79(x9 x79False)False)(∀ x79 . (x73 (x56 x79) (x71 (x72 x79 x79))False)False)(∀ x79 . (x44 (x56 x79) x79False)False)(∀ x79 . (x5 (x55 x79)False)False)(∀ x79 x80 x81 x82 . (x78 x82False)x63 x79x74 x79 x82 x81x73 x79 (x71 (x72 x82 x81))x73 x80 x82(x73 (x68 x82 x81 x79 x80) x81False)False)(∀ x79 x80 . (x77 x80False)x62 x80x76 x80x63 x79x74 x79 (x75 x80) (x75 x80)x64 x79 (x75 x80) (x75 x80)x73 x79 (x71 (x72 (x75 x80) (x75 x80)))x65 x79 x80(x25 x79 x80 = x68 (x75 x80) (x75 x80) x79 (x25 x79 x80)False)(x70 x79 x80False)False)(∀ x79 x80 . (x77 x80False)x62 x80x76 x80x63 x79x74 x79 (x75 x80) (x75 x80)x64 x79 (x75 x80) (x75 x80)x73 x79 (x71 (x72 (x75 x80) (x75 x80)))x65 x79 x80(x73 (x25 x79 x80) (x75 x80)False)(x70 x79 x80False)False)(∀ x79 x80 . (x77 x80False)x62 x80x76 x80x63 x79x74 x79 (x75 x80) (x75 x80)x64 x79 (x75 x80) (x75 x80)x73 x79 (x71 (x72 (x75 x80) (x75 x80)))x65 x79 x80x57 (x75 x80) (x75 x80) x79 (x56 (x75 x80))(x70 x79 x80False)False)(∀ x79 x80 x81 . (x77 x81False)x62 x81x76 x81x63 x79x74 x79 (x75 x81) (x75 x81)x64 x79 (x75 x81) (x75 x81)x73 x79 (x71 (x72 (x75 x81) (x75 x81)))x70 x79 x81(x57 (x75 x81) (x75 x81) x79 (x56 (x75 x81))False)x73 x80 (x75 x81)x80 = x68 (x75 x81) (x75 x81) x79 x80False)(∀ x79 x80 . (x77 x80False)x62 x80x76 x80x63 x79x74 x79 (x75 x80) (x75 x80)x64 x79 (x75 x80) (x75 x80)x73 x79 (x71 (x72 (x75 x80) (x75 x80)))x70 x79 x80(x65 x79 x80False)False)(∀ x79 . x9 x79x33 x79 x1(x7 x79False)False)(∀ x79 x80 . x52 x80x73 x79 (x71 x80)(x52 x79False)False)(∀ x79 . x9 x79x7 x79(x33 x79 x1False)False)(∀ x79 x80 . x78 x80x5 x79x6 x79 x80(x6 x79 x80False)False)(∀ x79 x80 . x78 x80x5 x79x6 x79 x80(x5 x79False)False)(∀ x79 x80 . x78 x80x5 x79x6 x79 x80(x78 x79False)False)(∀ x79 x80 x81 . (x78 x81False)(x78 x79False)x73 x80 (x71 (x72 x81 x79))x63 x80x74 x80 x81 x79(x74 x80 x81 x79False)False)(∀ x79 x80 x81 . (x78 x81False)(x78 x79False)x73 x80 (x71 (x72 x81 x79))x63 x80x74 x80 x81 x79x78 x80False)(∀ x79 x80 x81 . (x78 x81False)(x78 x79False)x73 x80 (x71 (x72 x81 x79))x63 x80x74 x80 x81 x79(x63 x80False)False)(∀ x79 x80 . x52 x80x73 x79 x80(x63 x79False)False)(∀ x79 x80 . x52 x80x73 x79 x80(x5 x79False)False)(∀ x79 . x9 x79(x21 x79False)x77 x79False)(∀ x79 x80 . x78 x80x5 x79x4 x79 x80(x4 x79 x80False)False)(∀ x79 x80 . x78 x80x5 x79x4 x79 x80(x5 x79False)False)(∀ x79 x80 . x78 x80x5 x79x4 x79 x80(x78 x79False)False)(∀ x79 x80 . x73 x80 (x71 (x72 x79 x79))x41 x80x63 x80x44 x80 x79x74 x80 x79 x79(x64 x80 x79 x79False)False)(∀ x79 x80 . x73 x80 (x71 (x72 x79 x79))x41 x80x63 x80x44 x80 x79x74 x80 x79 x79(x74 x80 x79 x79False)False)(∀ x79 x80 . x73 x80 (x71 (x72 x79 x79))x41 x80x63 x80x44 x80 x79x74 x80 x79 x79(x63 x80False)False)(∀ x79 . x78 x79(x52 x79False)False)(∀ x79 . x9 x79x77 x79(x21 x79False)False)(∀ x79 x80 x81 . x5 x81x6 x81 x79x73 x80 (x71 x81)(x6 x80 x79False)False)(∀ x79 x80 x81 . x73 x81 (x71 (x72 x79 x80))x63 x81x16 x81x26 x81 x80(x64 x81 x79 x80False)False)(∀ x79 x80 x81 . x73 x81 (x71 (x72 x79 x80))x63 x81x16 x81x26 x81 x80(x63 x81False)False)(∀ x79 . x40 x79x5 x79x63 x79(x49 x79False)False)(∀ x79 . x40 x79x5 x79x63 x79(x63 x79False)False)(∀ x79 . x40 x79x5 x79x63 x79(x5 x79False)False)(∀ x79 . x9 x79(x21 x79False)x21 x79False)(∀ x79 . x9 x79(x21 x79False)x7 x79False)(∀ x79 x80 x81 . x5 x81x4 x81 x79x73 x80 (x71 x81)(x4 x80 x79False)False)(∀ x79 x80 x81 . x73 x81 (x71 (x72 x80 x79))x63 x81x64 x81 x80 x79(x26 x81 x79False)False)(∀ x79 x80 x81 . x73 x81 (x71 (x72 x80 x79))x63 x81x64 x81 x80 x79(x16 x81False)False)(∀ x79 x80 x81 . x73 x81 (x71 (x72 x80 x79))x63 x81x64 x81 x80 x79(x63 x81False)False)(∀ x79 . x5 x79x63 x79(x49 x79False)(x63 x79False)False)(∀ x79 . x5 x79x63 x79(x49 x79False)(x5 x79False)False)(∀ x79 . x5 x79x63 x79(x49 x79False)x40 x79False)(∀ x79 . x9 x79x7 x79(x21 x79False)False)(∀ x79 . x9 x79x7 x79(x7 x79False)False)(∀ x79 . x78 x79x5 x79(x53 x79False)False)(∀ x79 . x78 x79x5 x79(x5 x79False)False)(∀ x79 x80 . x73 x80 (x71 (x72 x79 x79))x74 x80 x79 x79(x44 x80 x79False)False)(∀ x79 . x78 x79x5 x79x63 x79(x49 x79False)False)(∀ x79 . x78 x79x5 x79x63 x79(x63 x79False)False)(∀ x79 . x78 x79x5 x79x63 x79(x5 x79False)False)(∀ x79 . x78 x79x5 x79(x35 x79False)False)(∀ x79 . x78 x79x5 x79(x5 x79False)False)(∀ x79 . x5 x79x14 x79x13 x79(x41 x79False)False)(∀ x79 . x5 x79x14 x79x13 x79(x5 x79False)False)(∀ x79 x80 x81 . (x78 x81False)x73 x79 (x71 (x72 x80 x81))x74 x79 x80 x81(x44 x79 x80False)False)(∀ x79 x80 . x5 x80x63 x80x73 x79 (x71 x80)(x63 x79False)False)(∀ x79 . x9 x79(x77 x79False)x7 x79False)(∀ x79 x80 . x5 x80x73 x79 (x71 x80)(x5 x79False)False)(∀ x79 x80 x81 . (x78 x81False)x78 x79x73 x80 (x71 (x72 x81 x79))x44 x80 x81False)(∀ x79 x80 x81 . x78 x81x73 x79 (x71 (x72 x81 x80))x74 x79 x81 x80(x44 x79 x81False)False)(∀ x79 . x78 x79x5 x79x63 x79(x16 x79False)False)(∀ x79 . x78 x79x5 x79x63 x79(x63 x79False)False)(∀ x79 . x78 x79x5 x79x63 x79(x5 x79False)False)(∀ x79 . x9 x79x7 x79(x77 x79False)False)(∀ x79 . x78 x79(x5 x79False)False)(∀ x79 x80 x81 . x78 x81x73 x79 (x71 (x72 x81 x80))(x44 x79 x81False)False)(∀ x79 x80 x81 . x73 x80 (x71 (x72 x81 x79))x44 x80 x81(x74 x80 x81 x79False)False)(∀ x79 . x78 x79(x63 x79False)False)(∀ x79 . x9 x79(x77 x79False)x7 x79False)(∀ x79 . x9 x79x33 x79 x2(x77 x79False)False)(∀ x79 . x9 x79x33 x79 x2x7 x79False)(∀ x79 . x9 x79(x7 x79False)x77 x79(x33 x79 x2False)False)(∀ x79 x80 . x0 x79 x80x0 x80 x79False)(x29 = x68 (x75 x32) (x75 x32) x31 x30False)(x61 x32 x27 (x68 (x75 x32) (x75 x32) x31 x27) x30False)((x66 x32 x27 x30 (x68 (x75 x32) (x75 x32) x31 x27) x29False)False)((x66 x32 x27 (x68 (x75 x32) (x75 x32) x31 x27) x30 x29False)False)((x70 x31 x32False)False)((x73 x31 (x71 (x72 (x75 x32) (x75 x32)))False)False)((x64 x31 (x75 x32) (x75 x32)False)False)((x74 x31 (x75 x32) (x75 x32)False)False)((x63 x31False)False)((x73 x29 (x75 x32)False)False)((x73 x30 (x75 x32)False)False)((x73 x27 (x75 x32)False)False)((x76 x32False)False)((x28 x32False)False)((x62 x32False)False)(x77 x32False)False (proof)