Search for blocks/addresses/...
Proofgold Proposition
(
∀ x0 x1 x2 .
equip_mod
(
setsum
(
setsum
(
setprod
(
Power
(
binrep
(
Power
(
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
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
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
(
Power
0
)
)
)
(
Power
0
)
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
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
(
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
(
binrep
(
Power
(
Power
0
)
)
0
)
)
0
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setprod
(
setexp
x1
(
Power
(
Power
0
)
)
)
x2
)
)
)
(
setsum
(
setprod
(
Power
(
Power
0
)
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setexp
x1
(
Power
(
Power
0
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
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
(
Power
(
Power
0
)
)
)
0
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setprod
x1
x2
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
0
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
x1
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
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
(
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
(
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
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setprod
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
(
setsum
(
setprod
(
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
)
)
0
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
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
(
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
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
0
)
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setprod
(
setexp
x1
(
Power
(
Power
0
)
)
)
x2
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
0
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setexp
x1
(
Power
(
Power
0
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setprod
x1
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
0
)
)
0
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setprod
x1
x2
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
0
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
x1
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
0
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
(
setsum
(
setprod
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
x2
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
0
)
)
(
setexp
x0
(
Power
(
Power
0
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
(
setprod
x0
(
setprod
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
0
)
(
setprod
x0
(
setprod
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
0
)
(
setprod
x0
(
setprod
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
x2
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
0
)
(
setprod
x0
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
0
)
(
setprod
x0
(
setprod
(
setexp
x1
(
Power
(
Power
0
)
)
)
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
(
setprod
x0
(
setprod
(
setexp
x1
(
Power
(
Power
0
)
)
)
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
0
)
(
setprod
x0
(
setprod
(
setexp
x1
(
Power
(
Power
0
)
)
)
x2
)
)
)
(
setsum
(
setprod
x0
(
setexp
x1
(
Power
(
Power
0
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
(
setprod
x0
(
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
x0
(
setprod
x1
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
(
setprod
x0
(
setprod
x1
x2
)
)
)
(
setsum
(
setprod
(
Power
(
Power
0
)
)
(
setprod
x0
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
(
setsum
(
setprod
x0
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
0
)
(
setprod
x0
x2
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
0
)
x0
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
0
)
(
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
)
)
)
0
)
(
setprod
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
(
setsum
(
setprod
(
Power
(
Power
0
)
)
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
(
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
x1
(
Power
(
Power
0
)
)
)
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
0
)
(
setprod
(
setexp
x1
(
Power
(
Power
0
)
)
)
x2
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
0
)
)
0
)
(
setexp
x1
(
Power
(
Power
0
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
0
)
(
setprod
x1
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
0
)
(
setprod
x1
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
(
setsum
(
setprod
(
Power
(
Power
0
)
)
x1
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
0
)
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
(
setsum
(
setprod
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
(
setsum
x2
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(
Power
(
Power
(
Power
(
Power
0
)
)
)
)
)
(
setsum
(
setprod
(
Power
(
Power
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
(
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
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
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
)
)
0
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
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
(
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
(
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
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
0
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setexp
x1
(
Power
(
Power
0
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
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
x2
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
x1
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
(
setprod
(
setexp
x0
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
(
setsum
(
setprod
(
Power
(
Power
(
Power
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
(
Power
(
binrep
(
Power
(
Power
0
)
)
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
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setprod
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
0
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setprod
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
x2
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
0
)
)
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
(
Power
(
Power
0
)
)
)
)
)
)
(
setsum
(
setprod
(
Power
(
Power
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
(
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
)
)
0
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
x1
)
)
(
setsum
(
setprod
(
Power
(
Power
(
Power
0
)
)
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
0
)
(
setprod
(
setexp
x0
(
Power
(
Power
0
)
)
)
x2
)
)
(
setsum
(
setexp
x0
(
Power
(
Power
0
)
)
)
(
setsum
(
setprod
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setprod
x0
(
setprod
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
)
(
setsum
(
setprod
(
Power
(
Power
(
Power
0
)
)
)
(
setprod
x0
(
setprod
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
0
)
)
(
setprod
x0
(
setprod
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
x2
)
)
)
(
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
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
(
setprod
x0
(
setprod
(
setexp
x1
(
Power
(
Power
0
)
)
)
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
0
)
(
setprod
x0
(
setprod
(
setexp
x1
(
Power
(
Power
0
)
)
)
x2
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
0
)
)
(
setprod
x0
(
setexp
x1
(
Power
(
Power
0
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
0
)
)
0
)
(
setprod
x0
(
setprod
x1
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
)
(
setsum
(
setprod
(
Power
(
binrep
(
Power
(
Power
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
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
0
)
(
setprod
x0
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
0
)
)
x0
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
(
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
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
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
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
x2
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
0
)
)
(
setexp
x1
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
0
)
)
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
x1
(
Power
(
Power
0
)
)
)
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
0
)
(
setprod
(
setexp
x1
(
Power
(
Power
0
)
)
)
x2
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
0
)
)
0
)
(
setexp
x1
(
Power
(
Power
0
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
0
)
)
(
setprod
x1
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
(
setsum
(
setprod
(
Power
(
Power
(
Power
0
)
)
)
(
setprod
x1
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
)
(
setsum
(
setprod
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setprod
x1
x2
)
)
(
setsum
(
setprod
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
x1
)
(
setsum
(
setprod
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setexp
x2
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
(
setsum
(
setprod
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
setexp
x2
(
Power
(
Power
0
)
)
)
)
(
setsum
(
setprod
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
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
(
Power
(
binrep
(
binrep
(
Power
(
Power
(
Power
(
Power
0
)
)
)
)
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
)
(
binrep
(
binrep
(
binrep
(
Power
(
Power
(
Power
(
Power
0
)
)
)
)
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
0
)
)
0
)
)
(
binrep
(
Power
(
Power
(
Power
(
Power
0
)
)
)
)
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
(
binrep
(
binrep
(
Power
(
Power
(
Power
(
Power
0
)
)
)
)
(
Power
(
Power
0
)
)
)
0
)
)
(
binrep
(
binrep
(
Power
(
Power
(
Power
(
Power
0
)
)
)
)
(
Power
0
)
)
0
)
)
(
Power
(
Power
(
Power
(
Power
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
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
0
)
)
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
0
)
)
⟶
False
)
⟶
∀ x0 : ο .
x0
type
prop
theory
HF
name
-
proof
PUgLs..
Megalodon
-
proofgold address
TMSoX..
creator
35068
PrAFa..
/
e4f1d..
owner
35068
PrAFa..
/
e4f1d..
term root
34878..