Search for blocks/addresses/...
Proofgold Proposition
(
∀ x0 x1 x2 .
equip_mod
(
setsum
(
setsum
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setprod
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
0
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setprod
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
)
(
setsum
(
setprod
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setprod
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
x2
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
0
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
0
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setprod
(
setexp
x1
(
Power
(
Power
0
)
)
)
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
0
)
)
0
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setprod
(
setexp
x1
(
Power
(
Power
0
)
)
)
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
)
(
setsum
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setprod
(
setexp
x1
(
Power
(
Power
0
)
)
)
x2
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setexp
x1
(
Power
(
Power
0
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
0
)
)
0
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setprod
x1
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
0
)
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setprod
x1
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setprod
x1
x2
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
x1
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
0
)
)
0
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
0
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
0
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
x2
)
)
(
setsum
(
setprod
(
Power
(
Power
0
)
)
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
0
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setprod
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
)
(
setsum
(
setprod
(
Power
(
Power
0
)
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setprod
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
)
(
setsum
(
setprod
(
Power
(
Power
(
Power
0
)
)
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setprod
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
x2
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
0
)
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
(
setsum
(
setprod
(
Power
(
Power
(
Power
0
)
)
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setprod
(
setexp
x1
(
Power
(
Power
0
)
)
)
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
0
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setprod
(
setexp
x1
(
Power
(
Power
0
)
)
)
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
0
)
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setprod
(
setexp
x1
(
Power
(
Power
0
)
)
)
x2
)
)
)
(
setsum
(
setprod
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setexp
x1
(
Power
(
Power
0
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
0
)
)
0
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setprod
x1
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
0
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setprod
x1
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
0
)
)
0
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setprod
x1
x2
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
0
)
)
0
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
0
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
x2
)
)
(
setsum
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
0
)
(
setprod
x0
(
setprod
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
)
(
setsum
(
setprod
(
Power
(
Power
0
)
)
(
setprod
x0
(
setprod
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
0
)
(
setprod
x0
(
setprod
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
x2
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
(
setprod
x0
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
0
)
)
0
)
(
setprod
x0
(
setprod
(
setexp
x1
(
Power
(
Power
0
)
)
)
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
0
)
(
setprod
x0
(
setprod
(
setexp
x1
(
Power
(
Power
0
)
)
)
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
)
(
setsum
(
setprod
(
Power
(
Power
(
Power
0
)
)
)
(
setprod
x0
(
setprod
(
setexp
x1
(
Power
(
Power
0
)
)
)
x2
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
0
)
(
setprod
x0
(
setexp
x1
(
Power
(
Power
0
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
0
)
)
0
)
(
setprod
x0
(
setprod
x1
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
0
)
)
0
)
(
setprod
x0
(
setprod
x1
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
0
)
(
setprod
x0
(
setprod
x1
x2
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
0
)
)
0
)
(
setprod
x0
x1
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
(
setprod
x0
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
(
setprod
x0
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
(
setsum
(
setprod
x0
x2
)
(
setsum
x0
(
setsum
(
setprod
(
binrep
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
0
)
(
setprod
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
0
)
)
0
)
(
setprod
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
0
)
(
setprod
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
x2
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
0
)
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
0
)
(
setprod
(
setexp
x1
(
Power
(
Power
0
)
)
)
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
0
)
(
setprod
(
setexp
x1
(
Power
(
Power
0
)
)
)
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
0
)
(
setprod
(
setexp
x1
(
Power
(
Power
0
)
)
)
x2
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
0
)
(
setexp
x1
(
Power
(
Power
0
)
)
)
)
(
setsum
(
setprod
(
Power
(
Power
(
Power
0
)
)
)
(
setprod
x1
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
0
)
)
0
)
(
setprod
x1
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
(
setprod
x1
x2
)
)
(
setsum
x1
(
setsum
(
setprod
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
0
)
)
x2
)
(
Power
0
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(
Power
(
Power
(
Power
(
Power
0
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
0
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setprod
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setprod
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
0
)
)
0
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setprod
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
x2
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
0
)
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
(
setsum
(
setprod
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setprod
(
setexp
x1
(
Power
(
Power
0
)
)
)
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
)
(
setsum
(
setprod
(
Power
(
Power
(
Power
0
)
)
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setprod
(
setexp
x1
(
Power
(
Power
0
)
)
)
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
0
)
)
0
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setprod
(
setexp
x1
(
Power
(
Power
0
)
)
)
x2
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
0
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setexp
x1
(
Power
(
Power
0
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
0
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setprod
x1
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
)
(
setsum
(
setprod
(
Power
(
Power
0
)
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setprod
x1
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
0
)
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setprod
x1
x2
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
0
)
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
x1
)
)
(
setsum
(
setprod
(
Power
(
Power
0
)
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
0
)
)
0
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
x2
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
0
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setprod
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
0
)
)
0
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setprod
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
0
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setprod
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
x2
)
)
)
(
setsum
(
setprod
(
Power
(
Power
0
)
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
0
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setprod
(
setexp
x1
(
Power
(
Power
0
)
)
)
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
0
)
)
0
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setprod
(
setexp
x1
(
Power
(
Power
0
)
)
)
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
0
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setprod
(
setexp
x1
(
Power
(
Power
0
)
)
)
x2
)
)
)
(
setsum
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setexp
x1
(
Power
(
Power
0
)
)
)
)
(
setsum
(
setprod
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setprod
x1
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
)
(
setsum
(
setprod
(
Power
(
Power
(
Power
0
)
)
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setprod
x1
x2
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
0
)
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
x1
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
0
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
0
)
)
0
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
x2
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
0
)
(
setexp
x0
(
Power
(
Power
0
)
)
)
)
(
setsum
(
setprod
x0
(
setprod
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
(
setprod
x0
(
setprod
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
0
)
(
setprod
x0
(
setprod
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
x2
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
0
)
(
setprod
x0
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
(
setprod
x0
(
setprod
(
setexp
x1
(
Power
(
Power
0
)
)
)
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
)
(
setsum
(
setprod
(
Power
(
Power
(
Power
0
)
)
)
(
setprod
x0
(
setprod
(
setexp
x1
(
Power
(
Power
0
)
)
)
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
0
)
(
setprod
x0
(
setprod
(
setexp
x1
(
Power
(
Power
0
)
)
)
x2
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
0
)
(
setprod
x0
(
setexp
x1
(
Power
(
Power
0
)
)
)
)
)
(
setsum
(
setprod
(
Power
(
Power
0
)
)
(
setprod
x0
(
setprod
x1
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
)
(
setsum
(
setprod
(
Power
(
Power
(
Power
0
)
)
)
(
setprod
x0
(
setprod
x1
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
0
)
(
setprod
x0
(
setprod
x1
x2
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
(
setprod
x0
x1
)
)
(
setsum
(
setprod
x0
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
0
)
(
setprod
x0
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
(
setsum
(
setprod
x0
x2
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
(
setprod
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
(
setsum
(
setprod
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
0
)
(
setprod
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
x2
)
)
(
setsum
(
setprod
(
Power
(
Power
(
Power
0
)
)
)
(
setprod
(
setexp
x1
(
Power
(
Power
0
)
)
)
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
(
setsum
(
setprod
(
setexp
x1
(
Power
(
Power
0
)
)
)
x2
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
0
)
)
0
)
(
setexp
x1
(
Power
(
Power
0
)
)
)
)
(
setsum
(
setprod
x1
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
(
setprod
x1
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
0
)
(
setprod
x1
x2
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
0
)
x1
)
(
setsum
(
setprod
(
Power
(
Power
(
Power
0
)
)
)
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
0
)
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
x2
)
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
0
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(
binrep
(
binrep
(
binrep
(
binrep
(
binrep
(
binrep
(
binrep
(
binrep
(
binrep
(
binrep
(
binrep
(
binrep
(
binrep
(
binrep
(
binrep
(
binrep
(
binrep
(
binrep
(
binrep
(
binrep
(
binrep
(
binrep
(
binrep
(
binrep
(
binrep
(
binrep
(
binrep
(
binrep
(
binrep
(
binrep
(
binrep
(
binrep
(
binrep
(
binrep
(
binrep
(
binrep
(
binrep
(
binrep
(
binrep
(
binrep
(
binrep
(
binrep
(
binrep
(
Power
(
binrep
(
binrep
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
0
)
)
(
Power
(
Power
(
Power
0
)
)
)
)
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
0
)
)
0
)
)
(
binrep
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
0
)
)
(
Power
(
Power
(
Power
0
)
)
)
)
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
0
)
)
)
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
0
)
)
(
Power
(
Power
(
Power
0
)
)
)
)
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
(
binrep
(
binrep
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
0
)
)
(
Power
(
Power
(
Power
0
)
)
)
)
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
0
)
)
(
binrep
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
0
)
)
(
Power
(
Power
(
Power
0
)
)
)
)
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
)
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
0
)
)
(
Power
(
Power
(
Power
0
)
)
)
)
(
Power
(
Power
0
)
)
)
)
(
binrep
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
0
)
)
(
Power
(
Power
(
Power
0
)
)
)
)
(
Power
0
)
)
0
)
)
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
0
)
)
(
Power
(
Power
(
Power
0
)
)
)
)
(
Power
0
)
)
)
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
0
)
)
(
Power
(
Power
(
Power
0
)
)
)
)
0
)
)
(
binrep
(
Power
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
0
)
)
(
Power
(
Power
(
Power
0
)
)
)
)
)
(
binrep
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
0
)
)
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
0
)
)
(
binrep
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
0
)
)
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
0
)
)
0
)
)
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
0
)
)
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
0
)
)
)
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
0
)
)
(
binrep
(
Power
(
Power
0
)
)
0
)
)
0
)
)
(
binrep
(
Power
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
0
)
)
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
(
binrep
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
0
)
)
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
0
)
)
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
0
)
)
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
)
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
0
)
)
(
Power
(
Power
0
)
)
)
0
)
)
(
binrep
(
Power
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
0
)
)
(
Power
(
Power
0
)
)
)
)
(
binrep
(
Power
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
0
)
)
(
Power
0
)
)
)
(
binrep
(
Power
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
0
)
)
0
)
)
(
Power
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
0
)
)
)
(
binrep
(
binrep
(
binrep
(
Power
(
Power
(
Power
(
Power
0
)
)
)
)
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
0
)
)
(
binrep
(
binrep
(
Power
(
Power
(
Power
(
Power
0
)
)
)
)
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
)
(
binrep
(
binrep
(
Power
(
Power
(
Power
(
Power
0
)
)
)
)
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
0
)
)
)
(
binrep
(
binrep
(
Power
(
Power
(
Power
(
Power
0
)
)
)
)
(
binrep
(
Power
(
Power
0
)
)
0
)
)
0
)
)
(
binrep
(
Power
(
Power
(
Power
(
Power
0
)
)
)
)
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
(
binrep
(
binrep
(
Power
(
Power
(
Power
(
Power
0
)
)
)
)
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
)
(
binrep
(
binrep
(
Power
(
Power
(
Power
(
Power
0
)
)
)
)
(
Power
(
Power
0
)
)
)
0
)
)
(
binrep
(
Power
(
Power
(
Power
(
Power
0
)
)
)
)
(
Power
(
Power
0
)
)
)
)
(
binrep
(
binrep
(
Power
(
Power
(
Power
(
Power
0
)
)
)
)
(
Power
0
)
)
0
)
)
(
binrep
(
Power
(
Power
(
Power
(
Power
0
)
)
)
)
(
Power
0
)
)
)
(
binrep
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
0
)
)
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
0
)
)
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
)
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
0
)
)
0
)
)
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
0
)
)
)
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
0
)
)
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
(
binrep
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
0
)
)
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
)
(
Power
(
Power
(
Power
0
)
)
)
)
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
⟶
False
)
⟶
∀ x0 : ο .
x0
type
prop
theory
HF
name
-
proof
PUZCS..
Megalodon
-
proofgold address
TMLM2..
creator
22411
PrBTh..
/
b36ed..
owner
22411
PrBTh..
/
b36ed..
term root
2e22d..