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