// maximum expected number of steps (first round)
multi
(
Rmax
=? [
F
pc1
=
3
&
pc2
=
3
],
P
>=
0
[
F
true
])