Search for blocks/addresses/...
Proofgold Asset
asset id
5e2244c4c3240934754e77549ceaf15e9289c2e76987bb1b62ea27e0d5cb9e52
asset hash
11e9d631df002780231a13887863f05be1364607332fe2ac68cc57ab62e75f87
bday / block
35135
tx
d524a..
preasset
doc published by
PrPhD..
Definition
False
False
:=
∀ x0 : ο .
x0
Definition
not
not
:=
λ x0 : ο .
x0
⟶
False
Theorem
36118..
:
∀ 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 .
x55
x57
⟶
(
x57
=
x56
⟶
False
)
⟶
x55
x56
⟶
False
)
⟶
(
∀ x56 x57 .
x0
x56
x57
⟶
x55
x57
⟶
False
)
⟶
(
∀ x56 .
x55
x56
⟶
(
x56
=
x54
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 x58 .
x0
x56
x57
⟶
x2
x57
(
x1
x58
)
⟶
x55
x58
⟶
False
)
⟶
(
∀ x56 x57 x58 .
x0
x57
x58
⟶
x2
x58
(
x1
x56
)
⟶
(
x2
x57
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x3
x57
x56
⟶
(
x2
x57
(
x1
x56
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x2
x57
(
x1
x56
)
⟶
(
x3
x57
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x2
x56
x57
⟶
(
x55
x57
⟶
False
)
⟶
(
x0
x56
x57
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 x58 x59 .
x53
x59
⟶
x48
x59
⟶
x0
x58
(
x52
x59
)
⟶
x0
x58
x56
⟶
x0
(
x51
x59
x58
)
x57
⟶
(
x0
x58
(
x50
x56
(
x49
x59
x56
x57
)
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 x58 x59 .
x53
x59
⟶
x48
x59
⟶
x0
x58
(
x50
x56
(
x49
x59
x56
x57
)
)
⟶
(
x0
(
x51
x59
x58
)
x57
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 x58 x59 .
x53
x59
⟶
x48
x59
⟶
x0
x58
(
x50
x57
(
x49
x59
x57
x56
)
)
⟶
(
x0
x58
x57
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 x58 x59 .
x53
x59
⟶
x48
x59
⟶
x0
x58
(
x50
x56
(
x49
x59
x56
x57
)
)
⟶
(
x0
x58
(
x52
x59
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x0
x57
x56
⟶
(
x2
x57
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 .
(
x3
x56
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x53
x57
⟶
x47
x57
x56
⟶
(
x50
x56
x57
=
x52
x57
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x53
x57
⟶
x4
x57
x56
⟶
(
x5
x56
x57
=
x57
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x53
x57
⟶
x47
x57
x56
⟶
(
x46
x57
x56
=
x57
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x53
x57
⟶
(
x5
x56
(
x5
x56
x57
)
=
x5
x56
x57
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x53
x57
⟶
(
x46
(
x46
x57
x56
)
x56
=
x46
x57
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 .
x53
x56
⟶
(
x46
x56
(
x52
x56
)
=
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 .
(
x48
(
x45
x56
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 .
(
x47
(
x45
x56
)
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 .
(
x44
(
x45
x56
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 .
(
x53
(
x45
x56
)
⟶
False
)
⟶
False
)
⟶
(
(
x43
x42
⟶
False
)
⟶
False
)
⟶
(
x55
x42
⟶
False
)
⟶
(
∀ x56 .
(
x41
x56
⟶
False
)
⟶
x41
(
x40
x56
)
⟶
False
)
⟶
(
∀ x56 .
(
x41
x56
⟶
False
)
⟶
(
x2
(
x40
x56
)
(
x1
x56
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
(
x48
(
x39
x56
x57
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
(
x4
(
x39
x56
x57
)
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
(
x47
(
x39
x57
x56
)
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
(
x53
(
x39
x56
x57
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 .
(
x55
x56
⟶
False
)
⟶
(
x41
(
x38
x56
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 .
(
x55
x56
⟶
False
)
⟶
x55
(
x38
x56
)
⟶
False
)
⟶
(
∀ x56 .
(
x55
x56
⟶
False
)
⟶
(
x2
(
x38
x56
)
(
x1
x56
)
⟶
False
)
⟶
False
)
⟶
(
x6
x7
⟶
False
)
⟶
(
(
x48
x7
⟶
False
)
⟶
False
)
⟶
(
(
x53
x7
⟶
False
)
⟶
False
)
⟶
(
∀ x56 .
(
x55
x56
⟶
False
)
⟶
(
x36
(
x37
x56
)
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 .
(
x55
x56
⟶
False
)
⟶
(
x2
(
x37
x56
)
(
x1
x56
)
⟶
False
)
⟶
False
)
⟶
(
(
x48
x35
⟶
False
)
⟶
False
)
⟶
(
(
x44
x35
⟶
False
)
⟶
False
)
⟶
(
(
x53
x35
⟶
False
)
⟶
False
)
⟶
(
x55
x35
⟶
False
)
⟶
(
∀ x56 .
x36
(
x34
x56
)
x56
⟶
False
)
⟶
(
∀ x56 .
(
x2
(
x34
x56
)
(
x1
x56
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
(
x4
(
x33
x56
x57
)
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
(
x47
(
x33
x57
x56
)
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
(
x53
(
x33
x56
x57
)
⟶
False
)
⟶
False
)
⟶
(
(
x48
x8
⟶
False
)
⟶
False
)
⟶
(
(
x44
x8
⟶
False
)
⟶
False
)
⟶
(
(
x53
x8
⟶
False
)
⟶
False
)
⟶
(
x55
x32
⟶
False
)
⟶
(
∀ x56 .
(
x55
(
x9
x56
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 .
(
x2
(
x9
x56
)
(
x1
x56
)
⟶
False
)
⟶
False
)
⟶
(
(
x44
x10
⟶
False
)
⟶
False
)
⟶
(
(
x53
x10
⟶
False
)
⟶
False
)
⟶
(
(
x11
x12
⟶
False
)
⟶
False
)
⟶
(
(
x48
x12
⟶
False
)
⟶
False
)
⟶
(
(
x53
x12
⟶
False
)
⟶
False
)
⟶
(
(
x55
x31
⟶
False
)
⟶
False
)
⟶
(
∀ x56 .
(
x55
x56
⟶
False
)
⟶
x55
(
x13
x56
)
⟶
False
)
⟶
(
∀ x56 .
(
x55
x56
⟶
False
)
⟶
(
x2
(
x13
x56
)
(
x1
x56
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
(
x4
(
x14
x56
x57
)
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
(
x47
(
x14
x57
x56
)
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
(
x53
(
x14
x56
x57
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
(
x55
(
x14
x56
x57
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
(
x2
(
x14
x56
x57
)
(
x1
(
x15
x57
x56
)
)
⟶
False
)
⟶
False
)
⟶
(
(
x53
x30
⟶
False
)
⟶
False
)
⟶
(
x55
x30
⟶
False
)
⟶
(
∀ x56 x57 .
(
x48
(
x29
x56
x57
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
(
x4
(
x29
x56
x57
)
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
(
x47
(
x29
x57
x56
)
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
(
x53
(
x29
x56
x57
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
(
x2
(
x29
x56
x57
)
(
x1
(
x15
x57
x56
)
)
⟶
False
)
⟶
False
)
⟶
(
(
x48
x16
⟶
False
)
⟶
False
)
⟶
(
(
x53
x16
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x53
x57
⟶
x48
x57
⟶
(
x48
(
x5
x56
x57
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x53
x57
⟶
x48
x57
⟶
(
x53
(
x5
x56
x57
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 x58 x59 .
x2
x59
(
x1
(
x15
(
x15
x57
x56
)
x58
)
)
⟶
(
x53
(
x52
x59
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 .
(
x55
x56
⟶
False
)
⟶
x53
x56
⟶
x55
(
x52
x56
)
⟶
False
)
⟶
(
∀ x56 x57 .
x53
x57
⟶
x48
x57
⟶
(
x48
(
x46
x57
x56
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x53
x57
⟶
x48
x57
⟶
(
x53
(
x46
x57
x56
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
(
x53
(
x15
x56
x57
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 x58 .
x53
x58
⟶
x4
x58
x56
⟶
(
x4
(
x5
x57
x58
)
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 x58 .
x53
x58
⟶
x4
x58
x57
⟶
(
x4
(
x5
x56
x58
)
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 x58 .
x53
x58
⟶
x4
x58
x57
⟶
(
x53
(
x5
x56
x58
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 x58 .
x53
x58
⟶
x47
x58
x56
⟶
(
x47
(
x5
x57
x58
)
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 x58 .
x53
x58
⟶
x47
x58
x57
⟶
(
x53
(
x5
x56
x58
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 x58 .
x53
x58
⟶
x47
x58
x56
⟶
(
x47
(
x46
x58
x57
)
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 x58 .
x53
x58
⟶
x47
x58
x57
⟶
(
x47
(
x46
x58
x56
)
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 x58 .
x53
x58
⟶
x47
x58
x57
⟶
(
x53
(
x46
x58
x56
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 x58 .
x53
x58
⟶
x4
x58
x56
⟶
(
x4
(
x46
x58
x57
)
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 x58 .
x53
x58
⟶
x4
x58
x57
⟶
(
x53
(
x46
x58
x56
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 .
x41
x56
⟶
x53
x56
⟶
(
x41
(
x52
x56
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x53
x57
⟶
x17
x57
⟶
(
x17
(
x46
x57
x56
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x53
x57
⟶
x17
x57
⟶
(
x53
(
x46
x57
x56
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x55
x57
⟶
x53
x57
⟶
(
x55
(
x18
x57
x56
)
⟶
False
)
⟶
False
)
⟶
(
(
x55
x54
⟶
False
)
⟶
False
)
⟶
(
∀ x56 .
x55
(
x1
x56
)
⟶
False
)
⟶
(
∀ x56 x57 .
x53
x57
⟶
x55
x56
⟶
(
x55
(
x18
x57
x56
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x53
x57
⟶
x17
x57
⟶
x48
x57
⟶
(
x55
(
x51
x57
x56
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x53
x57
⟶
x55
x56
⟶
(
x53
(
x5
x56
x57
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x53
x57
⟶
x55
x56
⟶
(
x55
(
x5
x56
x57
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 .
(
x41
x56
⟶
False
)
⟶
x53
x56
⟶
x48
x56
⟶
x41
(
x52
x56
)
⟶
False
)
⟶
(
∀ x56 x57 .
x55
x57
⟶
x53
x57
⟶
(
x53
(
x46
x57
x56
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x55
x57
⟶
x53
x57
⟶
(
x55
(
x46
x57
x56
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 x58 .
x43
x58
⟶
x53
x56
⟶
x4
x56
x58
⟶
x48
x56
⟶
(
x48
(
x51
x56
x57
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 x58 .
x43
x58
⟶
x53
x56
⟶
x4
x56
x58
⟶
x48
x56
⟶
(
x53
(
x51
x56
x57
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x53
x57
⟶
x55
x56
⟶
(
x53
(
x46
x57
x56
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x53
x57
⟶
x55
x56
⟶
(
x55
(
x46
x57
x56
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
(
x55
x57
⟶
False
)
⟶
x53
x57
⟶
(
x55
x56
⟶
False
)
⟶
x2
x56
(
x1
(
x52
x57
)
)
⟶
x55
(
x18
x57
x56
)
⟶
False
)
⟶
(
∀ x56 x57 .
(
x55
x57
⟶
False
)
⟶
x53
x57
⟶
x44
x57
⟶
x48
x57
⟶
x2
x56
(
x52
x57
)
⟶
x55
(
x51
x57
x56
)
⟶
False
)
⟶
(
∀ x56 x57 .
(
x55
x57
⟶
False
)
⟶
(
x55
x56
⟶
False
)
⟶
x55
(
x15
x57
x56
)
⟶
False
)
⟶
(
∀ x56 x57 .
(
x55
x57
⟶
False
)
⟶
x53
x57
⟶
(
x55
x56
⟶
False
)
⟶
x2
x56
(
x1
(
x52
x57
)
)
⟶
(
x53
(
x46
x57
x56
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
(
x55
x57
⟶
False
)
⟶
x53
x57
⟶
(
x55
x56
⟶
False
)
⟶
x2
x56
(
x1
(
x52
x57
)
)
⟶
x55
(
x46
x57
x56
)
⟶
False
)
⟶
(
∀ x56 .
x55
x56
⟶
(
x55
(
x52
x56
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 .
(
x2
(
x19
x56
)
x56
⟶
False
)
⟶
False
)
⟶
(
(
x55
x28
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x53
x57
⟶
(
x53
(
x5
x56
x57
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x53
x57
⟶
(
x53
(
x46
x57
x56
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 x58 .
x53
x58
⟶
x48
x58
⟶
(
x2
(
x49
x58
x57
x56
)
(
x1
(
x15
x57
x56
)
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 x58 .
x53
x58
⟶
x48
x58
⟶
(
x48
(
x49
x58
x57
x56
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x53
x57
⟶
x47
x57
x56
⟶
(
x2
(
x50
x56
x57
)
(
x1
x56
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 x58 .
x53
x58
⟶
x48
x58
⟶
(
x27
x56
x57
x58
=
x51
x58
(
x26
x56
x57
x58
)
⟶
False
)
⟶
(
x0
(
x27
x56
x57
x58
)
x56
⟶
False
)
⟶
(
x56
=
x18
x58
x57
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 x58 .
x53
x58
⟶
x48
x58
⟶
(
x0
(
x26
x56
x57
x58
)
x57
⟶
False
)
⟶
(
x0
(
x27
x56
x57
x58
)
x56
⟶
False
)
⟶
(
x56
=
x18
x58
x57
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 x58 .
x53
x58
⟶
x48
x58
⟶
(
x0
(
x26
x56
x57
x58
)
(
x52
x58
)
⟶
False
)
⟶
(
x0
(
x27
x56
x57
x58
)
x56
⟶
False
)
⟶
(
x56
=
x18
x58
x57
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 x58 x59 .
x53
x59
⟶
x48
x59
⟶
x0
(
x27
x58
x57
x59
)
x58
⟶
x0
x56
(
x52
x59
)
⟶
x0
x56
x57
⟶
x27
x58
x57
x59
=
x51
x59
x56
⟶
(
x58
=
x18
x59
x57
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 x58 x59 x60 .
x53
x60
⟶
x48
x60
⟶
x59
=
x18
x60
x58
⟶
x0
x56
(
x52
x60
)
⟶
x0
x56
x58
⟶
x57
=
x51
x60
x56
⟶
(
x0
x57
x59
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 x58 x59 .
x53
x59
⟶
x48
x59
⟶
x58
=
x18
x59
x57
⟶
x0
x56
x58
⟶
(
x56
=
x51
x59
(
x20
x56
x58
x57
x59
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 x58 x59 .
x53
x59
⟶
x48
x59
⟶
x58
=
x18
x59
x57
⟶
x0
x56
x58
⟶
(
x0
(
x20
x56
x58
x57
x59
)
x57
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 x58 x59 .
x53
x59
⟶
x48
x59
⟶
x58
=
x18
x59
x57
⟶
x0
x56
x58
⟶
(
x0
(
x20
x56
x58
x57
x59
)
(
x52
x59
)
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x0
(
x25
x56
x57
)
x56
⟶
(
x3
x57
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
(
x0
(
x25
x56
x57
)
x57
⟶
False
)
⟶
(
x3
x57
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 x58 .
x3
x57
x58
⟶
x0
x56
x57
⟶
(
x0
x56
x58
⟶
False
)
⟶
False
)
⟶
(
(
x54
=
x28
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x53
x57
⟶
x47
x57
x56
⟶
x50
x56
x57
=
x56
⟶
(
x24
x57
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x53
x57
⟶
x47
x57
x56
⟶
x24
x57
x56
⟶
(
x50
x56
x57
=
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 x58 .
x53
x58
⟶
x48
x58
⟶
(
x49
x58
x57
x56
=
x46
(
x5
x56
x58
)
x57
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x3
x57
x56
⟶
x3
x56
x57
⟶
(
x57
=
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x56
=
x57
⟶
(
x3
x57
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x57
=
x56
⟶
(
x3
x57
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x43
x57
⟶
x2
x56
(
x1
x57
)
⟶
(
x43
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x55
x57
⟶
x53
x56
⟶
x4
x56
x57
⟶
(
x4
x56
x57
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x55
x57
⟶
x53
x56
⟶
x4
x56
x57
⟶
(
x53
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x55
x57
⟶
x53
x56
⟶
x4
x56
x57
⟶
(
x55
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x43
x57
⟶
x2
x56
x57
⟶
(
x48
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x43
x57
⟶
x2
x56
x57
⟶
(
x53
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x55
x57
⟶
x53
x56
⟶
x47
x56
x57
⟶
(
x47
x56
x57
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x55
x57
⟶
x53
x56
⟶
x47
x56
x57
⟶
(
x53
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x55
x57
⟶
x53
x56
⟶
x47
x56
x57
⟶
(
x55
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 .
x55
x56
⟶
(
x43
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 x58 .
x53
x58
⟶
x4
x58
x56
⟶
x2
x57
(
x1
x58
)
⟶
(
x4
x57
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 .
x41
x56
⟶
x53
x56
⟶
x48
x56
⟶
(
x6
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 .
x41
x56
⟶
x53
x56
⟶
x48
x56
⟶
(
x48
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 .
x41
x56
⟶
x53
x56
⟶
x48
x56
⟶
(
x53
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x41
x57
⟶
x2
x56
(
x1
x57
)
⟶
(
x41
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 x58 .
x53
x58
⟶
x47
x58
x56
⟶
x2
x57
(
x1
x58
)
⟶
(
x47
x57
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 .
x53
x56
⟶
x48
x56
⟶
(
x6
x56
⟶
False
)
⟶
(
x48
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 .
x53
x56
⟶
x48
x56
⟶
(
x6
x56
⟶
False
)
⟶
(
x53
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 .
x53
x56
⟶
x48
x56
⟶
(
x6
x56
⟶
False
)
⟶
x41
x56
⟶
False
)
⟶
(
∀ x56 x57 .
x55
x57
⟶
x2
x56
(
x1
x57
)
⟶
x36
x56
x57
⟶
False
)
⟶
(
∀ x56 x57 x58 .
x55
x58
⟶
x2
x56
(
x1
(
x15
x57
x58
)
)
⟶
(
x55
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 .
x55
x56
⟶
x53
x56
⟶
(
x44
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 .
x55
x56
⟶
x53
x56
⟶
(
x53
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 .
x55
x56
⟶
x53
x56
⟶
x48
x56
⟶
(
x6
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 .
x55
x56
⟶
x53
x56
⟶
x48
x56
⟶
(
x48
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 .
x55
x56
⟶
x53
x56
⟶
x48
x56
⟶
(
x53
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
(
x55
x57
⟶
False
)
⟶
x2
x56
(
x1
x57
)
⟶
x55
x56
⟶
(
x36
x56
x57
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 x58 .
x55
x58
⟶
x2
x56
(
x1
(
x15
x58
x57
)
)
⟶
(
x55
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 .
x55
x56
⟶
x53
x56
⟶
(
x17
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 .
x55
x56
⟶
x53
x56
⟶
(
x53
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x53
x57
⟶
x48
x57
⟶
x2
x56
(
x1
x57
)
⟶
(
x48
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
(
x55
x57
⟶
False
)
⟶
x2
x56
(
x1
x57
)
⟶
(
x36
x56
x57
⟶
False
)
⟶
x55
x56
⟶
False
)
⟶
(
∀ x56 x57 x58 .
x2
x58
(
x1
(
x15
x56
x57
)
)
⟶
(
x4
x58
x57
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 x58 .
x2
x58
(
x1
(
x15
x57
x56
)
)
⟶
(
x47
x58
x57
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x53
x57
⟶
x2
x56
(
x1
x57
)
⟶
(
x53
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 x58 .
(
x55
x58
⟶
False
)
⟶
x55
x56
⟶
x2
x57
(
x1
(
x15
x58
x56
)
)
⟶
x24
x57
x58
⟶
False
)
⟶
(
∀ x56 .
x55
x56
⟶
x53
x56
⟶
x48
x56
⟶
(
x11
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 .
x55
x56
⟶
x53
x56
⟶
x48
x56
⟶
(
x48
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 .
x55
x56
⟶
x53
x56
⟶
x48
x56
⟶
(
x53
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x55
x57
⟶
x2
x56
(
x1
x57
)
⟶
(
x55
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 x58 .
x2
x58
(
x1
(
x15
x56
x57
)
)
⟶
(
x53
x58
⟶
False
)
⟶
False
)
⟶
(
∀ x56 .
x55
x56
⟶
(
x53
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 x58 .
x55
x58
⟶
x2
x56
(
x1
(
x15
x58
x57
)
)
⟶
(
x24
x56
x58
⟶
False
)
⟶
False
)
⟶
(
∀ x56 .
x55
x56
⟶
(
x48
x56
⟶
False
)
⟶
False
)
⟶
(
∀ x56 x57 .
x0
x56
x57
⟶
x0
x57
x56
⟶
False
)
⟶
(
x24
(
x49
x22
x21
x23
)
x21
⟶
False
)
⟶
(
(
x3
(
x18
x22
x21
)
x23
⟶
False
)
⟶
False
)
⟶
(
(
x3
x21
(
x52
x22
)
⟶
False
)
⟶
False
)
⟶
(
(
x48
x22
⟶
False
)
⟶
False
)
⟶
(
(
x53
x22
⟶
False
)
⟶
False
)
⟶
False
(proof)