Search for blocks/addresses/...
Proofgold Asset
asset id
cf46402f96ea7f9c3e7f211b7c4248c153eba9983788b9564bc1f4af55eae65b
asset hash
e5a1658df293fad8d138f4429d6dd965648248559e28f136741fc8bc9aa089e4
bday / block
35129
tx
041b4..
preasset
doc published by
PrPhD..
Definition
False
False
:=
∀ x0 : ο .
x0
Definition
not
not
:=
λ x0 : ο .
x0
⟶
False
Theorem
a5502..
:
∀ 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 .
x73
x75
⟶
(
x75
=
x74
⟶
False
)
⟶
x73
x74
⟶
False
)
⟶
(
∀ x74 x75 .
x0
x74
x75
⟶
x73
x75
⟶
False
)
⟶
(
∀ x74 .
x73
x74
⟶
(
x74
=
x72
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 x76 .
x0
x74
x75
⟶
x2
x75
(
x1
x76
)
⟶
x73
x76
⟶
False
)
⟶
(
∀ x74 x75 x76 .
x0
x75
x76
⟶
x2
x76
(
x1
x74
)
⟶
(
x2
x75
x74
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 .
x3
x75
x74
⟶
(
x2
x75
(
x1
x74
)
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 .
x2
x75
(
x1
x74
)
⟶
(
x3
x75
x74
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 x76 .
x0
x75
x76
⟶
x0
x74
x76
⟶
x0
x74
(
x4
x76
x75
)
⟶
False
)
⟶
(
∀ x74 x75 .
x0
x75
x74
⟶
(
x0
(
x4
x74
x75
)
x74
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 .
x2
x74
x75
⟶
(
x73
x75
⟶
False
)
⟶
(
x0
x74
x75
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 .
x0
x75
x74
⟶
(
x2
x75
x74
⟶
False
)
⟶
False
)
⟶
(
x73
x5
⟶
False
)
⟶
(
∀ x74 .
(
x3
x74
x74
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 x76 x77 .
(
x6
x77
⟶
False
)
⟶
(
x15
x77
⟶
False
)
⟶
x7
x77
⟶
x14
x77
⟶
x8
x77
⟶
x13
x77
⟶
x9
x77
⟶
x12
x77
⟶
(
x6
x76
⟶
False
)
⟶
(
x15
x76
⟶
False
)
⟶
x7
x76
⟶
x14
x76
⟶
x8
x76
⟶
x13
x76
⟶
x9
x76
⟶
x12
x76
⟶
x10
x75
x77
x76
⟶
x10
x74
x77
x76
⟶
(
x11
x77
x76
x75
x75
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 .
(
x6
x75
⟶
False
)
⟶
(
x15
x75
⟶
False
)
⟶
x71
x75
⟶
x2
x74
(
x70
x75
)
⟶
(
x68
x75
x74
=
x69
x75
x74
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 .
(
x6
x75
⟶
False
)
⟶
(
x15
x75
⟶
False
)
⟶
x71
x75
⟶
x2
x74
(
x70
x75
)
⟶
(
x17
x75
x74
=
x16
x75
x74
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 x76 x77 .
(
x73
x77
⟶
False
)
⟶
x63
x74
⟶
x67
x74
x77
x76
⟶
x2
x74
(
x1
(
x66
x77
x76
)
)
⟶
x2
x75
x77
⟶
(
x65
x77
x76
x74
x75
=
x64
x74
x75
⟶
False
)
⟶
False
)
⟶
(
∀ x74 .
(
x6
x74
⟶
False
)
⟶
x19
x74
⟶
x73
(
x18
x74
)
⟶
False
)
⟶
(
∀ x74 .
(
x6
x74
⟶
False
)
⟶
x19
x74
⟶
(
x2
(
x18
x74
)
(
x1
(
x62
x74
)
)
⟶
False
)
⟶
False
)
⟶
(
x15
x20
⟶
False
)
⟶
(
x6
x20
⟶
False
)
⟶
(
(
x12
x20
⟶
False
)
⟶
False
)
⟶
(
x61
x60
⟶
False
)
⟶
(
(
x21
x60
⟶
False
)
⟶
False
)
⟶
(
∀ x74 .
(
x59
x74
⟶
False
)
⟶
x19
x74
⟶
x58
(
x57
x74
)
⟶
False
)
⟶
(
∀ x74 .
(
x59
x74
⟶
False
)
⟶
x19
x74
⟶
(
x2
(
x57
x74
)
(
x1
(
x62
x74
)
)
⟶
False
)
⟶
False
)
⟶
(
∀ x74 .
(
x6
x74
⟶
False
)
⟶
x19
x74
⟶
(
x58
(
x56
x74
)
⟶
False
)
⟶
False
)
⟶
(
∀ x74 .
(
x6
x74
⟶
False
)
⟶
x19
x74
⟶
x73
(
x56
x74
)
⟶
False
)
⟶
(
∀ x74 .
(
x6
x74
⟶
False
)
⟶
x19
x74
⟶
(
x2
(
x56
x74
)
(
x1
(
x62
x74
)
)
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 .
(
x22
(
x23
x74
x75
)
x74
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 .
(
x55
(
x23
x75
x74
)
x74
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 .
(
x24
(
x23
x74
x75
)
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 .
(
x73
(
x23
x74
x75
)
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 .
(
x2
(
x23
x74
x75
)
(
x1
(
x66
x75
x74
)
)
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 .
(
x67
(
x54
x74
x75
)
x75
x74
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 .
(
x63
(
x54
x74
x75
)
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 .
(
x22
(
x54
x74
x75
)
x74
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 .
(
x55
(
x54
x75
x74
)
x74
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 .
(
x24
(
x54
x74
x75
)
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 .
(
x2
(
x54
x74
x75
)
(
x1
(
x66
x75
x74
)
)
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 x76 x77 x78 .
(
x6
x78
⟶
False
)
⟶
(
x15
x78
⟶
False
)
⟶
x12
x78
⟶
x2
x74
(
x62
x78
)
⟶
x2
x77
(
x62
x78
)
⟶
x2
x75
(
x70
x78
)
⟶
x76
=
x75
⟶
x17
x78
x75
=
x74
⟶
x68
x78
x75
=
x77
⟶
(
x0
x76
(
x53
x78
x74
x77
)
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 x76 x77 .
(
x6
x77
⟶
False
)
⟶
(
x15
x77
⟶
False
)
⟶
x12
x77
⟶
x2
x74
(
x62
x77
)
⟶
x2
x76
(
x62
x77
)
⟶
x0
x75
(
x53
x77
x74
x76
)
⟶
(
x68
x77
(
x25
x76
x74
x77
x75
)
=
x76
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 x76 x77 .
(
x6
x77
⟶
False
)
⟶
(
x15
x77
⟶
False
)
⟶
x12
x77
⟶
x2
x74
(
x62
x77
)
⟶
x2
x76
(
x62
x77
)
⟶
x0
x75
(
x53
x77
x74
x76
)
⟶
(
x17
x77
(
x25
x76
x74
x77
x75
)
=
x74
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 x76 x77 .
(
x6
x77
⟶
False
)
⟶
(
x15
x77
⟶
False
)
⟶
x12
x77
⟶
x2
x74
(
x62
x77
)
⟶
x2
x76
(
x62
x77
)
⟶
x0
x75
(
x53
x77
x74
x76
)
⟶
(
x75
=
x25
x76
x74
x77
x75
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 x76 x77 .
(
x6
x77
⟶
False
)
⟶
(
x15
x77
⟶
False
)
⟶
x12
x77
⟶
x2
x74
(
x62
x77
)
⟶
x2
x76
(
x62
x77
)
⟶
x0
x75
(
x53
x77
x74
x76
)
⟶
(
x2
(
x25
x76
x74
x77
x75
)
(
x70
x77
)
⟶
False
)
⟶
False
)
⟶
(
∀ x74 .
(
x26
x74
⟶
False
)
⟶
x19
x74
⟶
x27
(
x62
x74
)
⟶
False
)
⟶
(
∀ x74 .
x26
x74
⟶
x19
x74
⟶
(
x27
(
x62
x74
)
⟶
False
)
⟶
False
)
⟶
(
∀ x74 .
x59
x74
⟶
x19
x74
⟶
(
x58
(
x62
x74
)
⟶
False
)
⟶
False
)
⟶
(
∀ x74 .
(
x59
x74
⟶
False
)
⟶
x19
x74
⟶
x58
(
x62
x74
)
⟶
False
)
⟶
(
∀ x74 x75 .
(
x6
x75
⟶
False
)
⟶
(
x15
x75
⟶
False
)
⟶
x13
x75
⟶
x12
x75
⟶
x2
x74
(
x62
x75
)
⟶
x73
(
x28
x75
x74
x74
)
⟶
False
)
⟶
(
∀ x74 .
(
x6
x74
⟶
False
)
⟶
x19
x74
⟶
x73
(
x62
x74
)
⟶
False
)
⟶
(
∀ x74 .
(
x61
x74
⟶
False
)
⟶
x21
x74
⟶
x58
(
x70
x74
)
⟶
False
)
⟶
(
∀ x74 .
x61
x74
⟶
x21
x74
⟶
(
x58
(
x70
x74
)
⟶
False
)
⟶
False
)
⟶
(
∀ x74 .
x6
x74
⟶
x19
x74
⟶
(
x73
(
x62
x74
)
⟶
False
)
⟶
False
)
⟶
(
∀ x74 .
(
x15
x74
⟶
False
)
⟶
x21
x74
⟶
x73
(
x70
x74
)
⟶
False
)
⟶
(
∀ x74 .
x15
x74
⟶
x21
x74
⟶
(
x73
(
x70
x74
)
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 .
(
x6
x75
⟶
False
)
⟶
(
x15
x75
⟶
False
)
⟶
x7
x75
⟶
x14
x75
⟶
x8
x75
⟶
x13
x75
⟶
x9
x75
⟶
x12
x75
⟶
(
x6
x74
⟶
False
)
⟶
(
x15
x74
⟶
False
)
⟶
x7
x74
⟶
x14
x74
⟶
x8
x74
⟶
x13
x74
⟶
x9
x74
⟶
x12
x74
⟶
(
x10
(
x52
x74
x75
)
x75
x74
⟶
False
)
⟶
False
)
⟶
(
∀ x74 .
(
x2
(
x29
x74
)
x74
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 x76 x77 .
(
x6
x77
⟶
False
)
⟶
(
x15
x77
⟶
False
)
⟶
x7
x77
⟶
x14
x77
⟶
x8
x77
⟶
x13
x77
⟶
x9
x77
⟶
x12
x77
⟶
(
x6
x76
⟶
False
)
⟶
(
x15
x76
⟶
False
)
⟶
x7
x76
⟶
x14
x76
⟶
x8
x76
⟶
x13
x76
⟶
x9
x76
⟶
x12
x76
⟶
x10
x75
x77
x76
⟶
x10
x74
x77
x76
⟶
(
x51
(
x50
x74
x75
x76
x77
)
x77
x76
x75
x74
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 x76 .
(
x6
x76
⟶
False
)
⟶
(
x15
x76
⟶
False
)
⟶
x12
x76
⟶
x2
x74
(
x62
x76
)
⟶
x2
x75
(
x62
x76
)
⟶
(
x30
(
x31
x75
x74
x76
)
x76
x74
x75
⟶
False
)
⟶
False
)
⟶
(
(
x21
x49
⟶
False
)
⟶
False
)
⟶
(
(
x19
x32
⟶
False
)
⟶
False
)
⟶
(
(
x71
x48
⟶
False
)
⟶
False
)
⟶
(
(
x12
x33
⟶
False
)
⟶
False
)
⟶
(
(
x73
x47
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 x76 .
(
x6
x76
⟶
False
)
⟶
(
x15
x76
⟶
False
)
⟶
x7
x76
⟶
x14
x76
⟶
x8
x76
⟶
x13
x76
⟶
x9
x76
⟶
x12
x76
⟶
(
x6
x75
⟶
False
)
⟶
(
x15
x75
⟶
False
)
⟶
x7
x75
⟶
x14
x75
⟶
x8
x75
⟶
x13
x75
⟶
x9
x75
⟶
x12
x75
⟶
x10
x74
x76
x75
⟶
(
x2
x74
(
x1
(
x66
(
x70
x76
)
(
x70
x75
)
)
)
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 x76 .
(
x6
x76
⟶
False
)
⟶
(
x15
x76
⟶
False
)
⟶
x7
x76
⟶
x14
x76
⟶
x8
x76
⟶
x13
x76
⟶
x9
x76
⟶
x12
x76
⟶
(
x6
x75
⟶
False
)
⟶
(
x15
x75
⟶
False
)
⟶
x7
x75
⟶
x14
x75
⟶
x8
x75
⟶
x13
x75
⟶
x9
x75
⟶
x12
x75
⟶
x10
x74
x76
x75
⟶
(
x67
x74
(
x70
x76
)
(
x70
x75
)
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 x76 .
(
x6
x76
⟶
False
)
⟶
(
x15
x76
⟶
False
)
⟶
x7
x76
⟶
x14
x76
⟶
x8
x76
⟶
x13
x76
⟶
x9
x76
⟶
x12
x76
⟶
(
x6
x75
⟶
False
)
⟶
(
x15
x75
⟶
False
)
⟶
x7
x75
⟶
x14
x75
⟶
x8
x75
⟶
x13
x75
⟶
x9
x75
⟶
x12
x75
⟶
x10
x74
x76
x75
⟶
(
x63
x74
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 x76 x77 x78 .
(
x6
x78
⟶
False
)
⟶
(
x15
x78
⟶
False
)
⟶
x7
x78
⟶
x14
x78
⟶
x8
x78
⟶
x13
x78
⟶
x9
x78
⟶
x12
x78
⟶
(
x6
x77
⟶
False
)
⟶
(
x15
x77
⟶
False
)
⟶
x7
x77
⟶
x14
x77
⟶
x8
x77
⟶
x13
x77
⟶
x9
x77
⟶
x12
x77
⟶
x10
x76
x78
x77
⟶
x10
x74
x78
x77
⟶
x51
x75
x78
x77
x76
x74
⟶
(
x2
x75
(
x1
(
x66
(
x62
x78
)
(
x70
x77
)
)
)
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 x76 x77 x78 .
(
x6
x78
⟶
False
)
⟶
(
x15
x78
⟶
False
)
⟶
x7
x78
⟶
x14
x78
⟶
x8
x78
⟶
x13
x78
⟶
x9
x78
⟶
x12
x78
⟶
(
x6
x77
⟶
False
)
⟶
(
x15
x77
⟶
False
)
⟶
x7
x77
⟶
x14
x77
⟶
x8
x77
⟶
x13
x77
⟶
x9
x77
⟶
x12
x77
⟶
x10
x76
x78
x77
⟶
x10
x74
x78
x77
⟶
x51
x75
x78
x77
x76
x74
⟶
(
x67
x75
(
x62
x78
)
(
x70
x77
)
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 x76 x77 x78 .
(
x6
x78
⟶
False
)
⟶
(
x15
x78
⟶
False
)
⟶
x7
x78
⟶
x14
x78
⟶
x8
x78
⟶
x13
x78
⟶
x9
x78
⟶
x12
x78
⟶
(
x6
x77
⟶
False
)
⟶
(
x15
x77
⟶
False
)
⟶
x7
x77
⟶
x14
x77
⟶
x8
x77
⟶
x13
x77
⟶
x9
x77
⟶
x12
x77
⟶
x10
x76
x78
x77
⟶
x10
x74
x78
x77
⟶
x51
x75
x78
x77
x76
x74
⟶
(
x63
x75
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 x76 x77 .
(
x6
x77
⟶
False
)
⟶
(
x15
x77
⟶
False
)
⟶
x12
x77
⟶
x2
x74
(
x62
x77
)
⟶
x2
x76
(
x62
x77
)
⟶
x30
x75
x77
x74
x76
⟶
(
x2
x75
(
x70
x77
)
⟶
False
)
⟶
False
)
⟶
(
∀ x74 .
x21
x74
⟶
(
x19
x74
⟶
False
)
⟶
False
)
⟶
(
∀ x74 .
x71
x74
⟶
(
x21
x74
⟶
False
)
⟶
False
)
⟶
(
∀ x74 .
x12
x74
⟶
(
x71
x74
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 x76 x77 .
(
x6
x77
⟶
False
)
⟶
(
x15
x77
⟶
False
)
⟶
x7
x77
⟶
x14
x77
⟶
x8
x77
⟶
x13
x77
⟶
x9
x77
⟶
x12
x77
⟶
(
x6
x76
⟶
False
)
⟶
(
x15
x76
⟶
False
)
⟶
x7
x76
⟶
x14
x76
⟶
x8
x76
⟶
x13
x76
⟶
x9
x76
⟶
x12
x76
⟶
x10
x75
x77
x76
⟶
x2
x74
(
x62
x77
)
⟶
(
x2
(
x34
x77
x76
x75
x74
)
(
x62
x76
)
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 x76 .
(
x6
x76
⟶
False
)
⟶
(
x15
x76
⟶
False
)
⟶
x7
x76
⟶
x14
x76
⟶
x8
x76
⟶
x13
x76
⟶
x9
x76
⟶
x12
x76
⟶
(
x6
x75
⟶
False
)
⟶
(
x15
x75
⟶
False
)
⟶
x7
x75
⟶
x14
x75
⟶
x8
x75
⟶
x13
x75
⟶
x9
x75
⟶
x12
x75
⟶
x63
x74
⟶
x67
x74
(
x70
x76
)
(
x70
x75
)
⟶
x2
x74
(
x1
(
x66
(
x70
x76
)
(
x70
x75
)
)
)
⟶
(
x2
(
x46
x76
x75
x74
)
(
x1
(
x66
(
x62
x76
)
(
x62
x75
)
)
)
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 x76 .
(
x6
x76
⟶
False
)
⟶
(
x15
x76
⟶
False
)
⟶
x7
x76
⟶
x14
x76
⟶
x8
x76
⟶
x13
x76
⟶
x9
x76
⟶
x12
x76
⟶
(
x6
x75
⟶
False
)
⟶
(
x15
x75
⟶
False
)
⟶
x7
x75
⟶
x14
x75
⟶
x8
x75
⟶
x13
x75
⟶
x9
x75
⟶
x12
x75
⟶
x63
x74
⟶
x67
x74
(
x70
x76
)
(
x70
x75
)
⟶
x2
x74
(
x1
(
x66
(
x70
x76
)
(
x70
x75
)
)
)
⟶
(
x67
(
x46
x76
x75
x74
)
(
x62
x76
)
(
x62
x75
)
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 x76 .
(
x6
x76
⟶
False
)
⟶
(
x15
x76
⟶
False
)
⟶
x7
x76
⟶
x14
x76
⟶
x8
x76
⟶
x13
x76
⟶
x9
x76
⟶
x12
x76
⟶
(
x6
x75
⟶
False
)
⟶
(
x15
x75
⟶
False
)
⟶
x7
x75
⟶
x14
x75
⟶
x8
x75
⟶
x13
x75
⟶
x9
x75
⟶
x12
x75
⟶
x63
x74
⟶
x67
x74
(
x70
x76
)
(
x70
x75
)
⟶
x2
x74
(
x1
(
x66
(
x70
x76
)
(
x70
x75
)
)
)
⟶
(
x63
(
x46
x76
x75
x74
)
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 x76 x77 x78 x79 .
(
x6
x79
⟶
False
)
⟶
(
x15
x79
⟶
False
)
⟶
x7
x79
⟶
x14
x79
⟶
x8
x79
⟶
x13
x79
⟶
x9
x79
⟶
x12
x79
⟶
(
x6
x78
⟶
False
)
⟶
(
x15
x78
⟶
False
)
⟶
x7
x78
⟶
x14
x78
⟶
x8
x78
⟶
x13
x78
⟶
x9
x78
⟶
x12
x78
⟶
x10
x77
x79
x78
⟶
x10
x74
x79
x78
⟶
x51
x76
x79
x78
x77
x74
⟶
x2
x75
(
x62
x79
)
⟶
(
x30
(
x35
x79
x78
x77
x74
x76
x75
)
x78
(
x34
x79
x78
x77
x75
)
(
x34
x79
x78
x74
x75
)
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 .
(
x6
x75
⟶
False
)
⟶
(
x15
x75
⟶
False
)
⟶
x71
x75
⟶
x2
x74
(
x70
x75
)
⟶
(
x2
(
x68
x75
x74
)
(
x62
x75
)
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 .
(
x6
x75
⟶
False
)
⟶
(
x15
x75
⟶
False
)
⟶
x71
x75
⟶
x2
x74
(
x70
x75
)
⟶
(
x2
(
x17
x75
x74
)
(
x62
x75
)
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 x76 x77 .
(
x73
x77
⟶
False
)
⟶
x63
x74
⟶
x67
x74
x77
x76
⟶
x2
x74
(
x1
(
x66
x77
x76
)
)
⟶
x2
x75
x77
⟶
(
x2
(
x65
x77
x76
x74
x75
)
x76
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 .
x71
x75
⟶
x2
x74
(
x70
x75
)
⟶
(
x2
(
x69
x75
x74
)
(
x62
x75
)
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 x76 .
(
x6
x76
⟶
False
)
⟶
(
x15
x76
⟶
False
)
⟶
x12
x76
⟶
x2
x74
(
x62
x76
)
⟶
x2
x75
(
x62
x76
)
⟶
(
x2
(
x28
x76
x74
x75
)
(
x1
(
x70
x76
)
)
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 .
x71
x75
⟶
x2
x74
(
x70
x75
)
⟶
(
x2
(
x16
x75
x74
)
(
x62
x75
)
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 x76 x77 .
(
x6
x77
⟶
False
)
⟶
(
x15
x77
⟶
False
)
⟶
x12
x77
⟶
x2
x74
(
x62
x77
)
⟶
x2
x76
(
x62
x77
)
⟶
(
x28
x77
x74
x76
=
x72
⟶
False
)
⟶
x2
x75
(
x70
x77
)
⟶
x0
x75
(
x28
x77
x74
x76
)
⟶
(
x30
x75
x77
x74
x76
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 x76 x77 .
(
x6
x77
⟶
False
)
⟶
(
x15
x77
⟶
False
)
⟶
x12
x77
⟶
x2
x74
(
x62
x77
)
⟶
x2
x76
(
x62
x77
)
⟶
(
x28
x77
x74
x76
=
x72
⟶
False
)
⟶
x2
x75
(
x70
x77
)
⟶
x30
x75
x77
x74
x76
⟶
(
x0
x75
(
x28
x77
x74
x76
)
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 x76 .
(
x6
x76
⟶
False
)
⟶
(
x15
x76
⟶
False
)
⟶
x12
x76
⟶
x2
x74
(
x62
x76
)
⟶
x2
x75
(
x62
x76
)
⟶
(
x28
x76
x74
x75
=
x53
x76
x74
x75
⟶
False
)
⟶
False
)
⟶
(
(
x72
=
x47
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 x76 x77 .
(
x6
x77
⟶
False
)
⟶
(
x15
x77
⟶
False
)
⟶
x7
x77
⟶
x14
x77
⟶
x8
x77
⟶
x13
x77
⟶
x9
x77
⟶
x12
x77
⟶
(
x6
x76
⟶
False
)
⟶
(
x15
x76
⟶
False
)
⟶
x7
x76
⟶
x14
x76
⟶
x8
x76
⟶
x13
x76
⟶
x9
x76
⟶
x12
x76
⟶
x10
x75
x77
x76
⟶
x10
x74
x77
x76
⟶
(
x28
x76
(
x34
x77
x76
x75
(
x45
x74
x75
x76
x77
)
)
(
x34
x77
x76
x74
(
x45
x74
x75
x76
x77
)
)
=
x72
⟶
False
)
⟶
(
x11
x77
x76
x75
x74
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 x76 x77 .
(
x6
x77
⟶
False
)
⟶
(
x15
x77
⟶
False
)
⟶
x7
x77
⟶
x14
x77
⟶
x8
x77
⟶
x13
x77
⟶
x9
x77
⟶
x12
x77
⟶
(
x6
x76
⟶
False
)
⟶
(
x15
x76
⟶
False
)
⟶
x7
x76
⟶
x14
x76
⟶
x8
x76
⟶
x13
x76
⟶
x9
x76
⟶
x12
x76
⟶
x10
x75
x77
x76
⟶
x10
x74
x77
x76
⟶
(
x2
(
x45
x74
x75
x76
x77
)
(
x62
x77
)
⟶
False
)
⟶
(
x11
x77
x76
x75
x74
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 x76 x77 x78 .
(
x6
x78
⟶
False
)
⟶
(
x15
x78
⟶
False
)
⟶
x7
x78
⟶
x14
x78
⟶
x8
x78
⟶
x13
x78
⟶
x9
x78
⟶
x12
x78
⟶
(
x6
x77
⟶
False
)
⟶
(
x15
x77
⟶
False
)
⟶
x7
x77
⟶
x14
x77
⟶
x8
x77
⟶
x13
x77
⟶
x9
x77
⟶
x12
x77
⟶
x10
x76
x78
x77
⟶
x10
x74
x78
x77
⟶
x11
x78
x77
x76
x74
⟶
x2
x75
(
x62
x78
)
⟶
x28
x77
(
x34
x78
x77
x76
x75
)
(
x34
x78
x77
x74
x75
)
=
x72
⟶
False
)
⟶
(
∀ x74 x75 x76 x77 .
(
x6
x77
⟶
False
)
⟶
(
x15
x77
⟶
False
)
⟶
x7
x77
⟶
x14
x77
⟶
x8
x77
⟶
x13
x77
⟶
x9
x77
⟶
x12
x77
⟶
(
x6
x76
⟶
False
)
⟶
(
x15
x76
⟶
False
)
⟶
x7
x76
⟶
x14
x76
⟶
x8
x76
⟶
x13
x76
⟶
x9
x76
⟶
x12
x76
⟶
x10
x75
x77
x76
⟶
x2
x74
(
x62
x77
)
⟶
(
x34
x77
x76
x75
x74
=
x65
(
x62
x77
)
(
x62
x76
)
(
x46
x77
x76
x75
)
x74
⟶
False
)
⟶
False
)
⟶
(
∀ x74 .
x19
x74
⟶
x44
x74
x72
⟶
(
x6
x74
⟶
False
)
⟶
False
)
⟶
(
∀ x74 .
x19
x74
⟶
x6
x74
⟶
(
x44
x74
x72
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 x76 .
(
x73
x76
⟶
False
)
⟶
(
x73
x74
⟶
False
)
⟶
x2
x75
(
x1
(
x66
x76
x74
)
)
⟶
x63
x75
⟶
x67
x75
x76
x74
⟶
(
x67
x75
x76
x74
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 x76 .
(
x73
x76
⟶
False
)
⟶
(
x73
x74
⟶
False
)
⟶
x2
x75
(
x1
(
x66
x76
x74
)
)
⟶
x63
x75
⟶
x67
x75
x76
x74
⟶
x73
x75
⟶
False
)
⟶
(
∀ x74 x75 x76 .
(
x73
x76
⟶
False
)
⟶
(
x73
x74
⟶
False
)
⟶
x2
x75
(
x1
(
x66
x76
x74
)
)
⟶
x63
x75
⟶
x67
x75
x76
x74
⟶
(
x63
x75
⟶
False
)
⟶
False
)
⟶
(
∀ x74 .
x19
x74
⟶
(
x26
x74
⟶
False
)
⟶
x59
x74
⟶
False
)
⟶
(
∀ x74 .
x19
x74
⟶
x59
x74
⟶
(
x26
x74
⟶
False
)
⟶
False
)
⟶
(
∀ x74 .
x19
x74
⟶
(
x26
x74
⟶
False
)
⟶
x26
x74
⟶
False
)
⟶
(
∀ x74 .
x19
x74
⟶
(
x26
x74
⟶
False
)
⟶
x6
x74
⟶
False
)
⟶
(
∀ x74 .
x19
x74
⟶
x6
x74
⟶
(
x26
x74
⟶
False
)
⟶
False
)
⟶
(
∀ x74 .
x19
x74
⟶
x6
x74
⟶
(
x6
x74
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 x76 .
x73
x76
⟶
x2
x74
(
x1
(
x66
x75
x76
)
)
⟶
(
x73
x74
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 .
x2
x75
(
x1
(
x66
x74
x74
)
)
⟶
x67
x75
x74
x74
⟶
(
x43
x75
x74
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 x76 .
x73
x76
⟶
x2
x74
(
x1
(
x66
x76
x75
)
)
⟶
(
x73
x74
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 x76 .
(
x73
x76
⟶
False
)
⟶
x2
x74
(
x1
(
x66
x75
x76
)
)
⟶
x67
x74
x75
x76
⟶
(
x43
x74
x75
⟶
False
)
⟶
False
)
⟶
(
∀ x74 .
x19
x74
⟶
(
x59
x74
⟶
False
)
⟶
x6
x74
⟶
False
)
⟶
(
∀ x74 x75 x76 .
x2
x76
(
x1
(
x66
x74
x75
)
)
⟶
(
x22
x76
x75
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 x76 .
x2
x76
(
x1
(
x66
x75
x74
)
)
⟶
(
x55
x76
x75
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 x76 .
x73
x76
⟶
x2
x74
(
x1
(
x66
x76
x75
)
)
⟶
x67
x74
x76
x75
⟶
(
x43
x74
x76
⟶
False
)
⟶
False
)
⟶
(
∀ x74 .
x12
x74
⟶
(
x6
x74
⟶
False
)
⟶
(
x15
x74
⟶
False
)
⟶
x61
x74
⟶
(
x9
x74
⟶
False
)
⟶
False
)
⟶
(
∀ x74 .
x12
x74
⟶
(
x6
x74
⟶
False
)
⟶
(
x15
x74
⟶
False
)
⟶
x61
x74
⟶
(
x8
x74
⟶
False
)
⟶
False
)
⟶
(
∀ x74 .
x12
x74
⟶
(
x6
x74
⟶
False
)
⟶
(
x15
x74
⟶
False
)
⟶
x61
x74
⟶
x15
x74
⟶
False
)
⟶
(
∀ x74 .
x12
x74
⟶
(
x6
x74
⟶
False
)
⟶
(
x15
x74
⟶
False
)
⟶
x61
x74
⟶
x6
x74
⟶
False
)
⟶
(
∀ x74 .
x19
x74
⟶
x6
x74
⟶
(
x59
x74
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 x76 .
x2
x76
(
x1
(
x66
x74
x75
)
)
⟶
(
x24
x76
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 x76 .
x2
x75
(
x1
(
x66
x76
x74
)
)
⟶
x43
x75
x76
⟶
(
x67
x75
x76
x74
⟶
False
)
⟶
False
)
⟶
(
∀ x74 .
x12
x74
⟶
(
x6
x74
⟶
False
)
⟶
x59
x74
⟶
(
x15
x74
⟶
False
)
⟶
(
x13
x74
⟶
False
)
⟶
False
)
⟶
(
∀ x74 .
x12
x74
⟶
(
x6
x74
⟶
False
)
⟶
x59
x74
⟶
(
x15
x74
⟶
False
)
⟶
(
x14
x74
⟶
False
)
⟶
False
)
⟶
(
∀ x74 .
x12
x74
⟶
(
x6
x74
⟶
False
)
⟶
x59
x74
⟶
(
x15
x74
⟶
False
)
⟶
x15
x74
⟶
False
)
⟶
(
∀ x74 .
x12
x74
⟶
(
x6
x74
⟶
False
)
⟶
x59
x74
⟶
(
x15
x74
⟶
False
)
⟶
x6
x74
⟶
False
)
⟶
(
∀ x74 .
x19
x74
⟶
(
x59
x74
⟶
False
)
⟶
x6
x74
⟶
False
)
⟶
(
∀ x74 .
x21
x74
⟶
x15
x74
⟶
(
x61
x74
⟶
False
)
⟶
False
)
⟶
(
∀ x74 .
x21
x74
⟶
(
x15
x74
⟶
False
)
⟶
x42
x74
⟶
x6
x74
⟶
False
)
⟶
(
∀ x74 .
x21
x74
⟶
x6
x74
⟶
x42
x74
⟶
(
x15
x74
⟶
False
)
⟶
False
)
⟶
(
∀ x74 .
x21
x74
⟶
x15
x74
⟶
(
x42
x74
⟶
False
)
⟶
False
)
⟶
(
∀ x74 .
x21
x74
⟶
(
x6
x74
⟶
False
)
⟶
(
x42
x74
⟶
False
)
⟶
False
)
⟶
(
∀ x74 .
x19
x74
⟶
x44
x74
x5
⟶
(
x59
x74
⟶
False
)
⟶
False
)
⟶
(
∀ x74 .
x19
x74
⟶
x44
x74
x5
⟶
x6
x74
⟶
False
)
⟶
(
∀ x74 .
x19
x74
⟶
(
x6
x74
⟶
False
)
⟶
x59
x74
⟶
(
x44
x74
x5
⟶
False
)
⟶
False
)
⟶
(
∀ x74 x75 .
x0
x74
x75
⟶
x0
x75
x74
⟶
False
)
⟶
(
x0
(
x35
x37
x41
x40
x39
x36
x38
)
(
x28
x41
(
x34
x37
x41
x40
x38
)
(
x34
x37
x41
x39
x38
)
)
⟶
False
)
⟶
(
(
x2
x38
(
x62
x37
)
⟶
False
)
⟶
False
)
⟶
(
(
x51
x36
x37
x41
x40
x39
⟶
False
)
⟶
False
)
⟶
(
(
x11
x37
x41
x40
x39
⟶
False
)
⟶
False
)
⟶
(
(
x10
x39
x37
x41
⟶
False
)
⟶
False
)
⟶
(
(
x10
x40
x37
x41
⟶
False
)
⟶
False
)
⟶
(
(
x12
x41
⟶
False
)
⟶
False
)
⟶
(
(
x9
x41
⟶
False
)
⟶
False
)
⟶
(
(
x13
x41
⟶
False
)
⟶
False
)
⟶
(
(
x8
x41
⟶
False
)
⟶
False
)
⟶
(
(
x14
x41
⟶
False
)
⟶
False
)
⟶
(
(
x7
x41
⟶
False
)
⟶
False
)
⟶
(
x15
x41
⟶
False
)
⟶
(
x6
x41
⟶
False
)
⟶
(
(
x12
x37
⟶
False
)
⟶
False
)
⟶
(
(
x9
x37
⟶
False
)
⟶
False
)
⟶
(
(
x13
x37
⟶
False
)
⟶
False
)
⟶
(
(
x8
x37
⟶
False
)
⟶
False
)
⟶
(
(
x14
x37
⟶
False
)
⟶
False
)
⟶
(
(
x7
x37
⟶
False
)
⟶
False
)
⟶
(
x15
x37
⟶
False
)
⟶
(
x6
x37
⟶
False
)
⟶
False
(proof)