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