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