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