Pmin=? [ true U (s1=9&s2=9&s3=9&s4=9&s5=9&s6=9&s7=9&s8=9) & ((pretwo_zero=1 & pretwo_one=0) | (pretwo_one=1 & pretwo_zero=0)) ]