((s1=10 | s2=10 | s3=10 | s4=10 | s5=10 | s6=10 | s7=10 | s8=10 | s9=10 | s10=10 | s11=10 | s12=10) | (s1=11 | s2=11 | s3=11 | s4=11 | s5=11 | s6=11 | s7=11 | s8=11 | s9=11 | s10=11 | s11=11 | s12=11) | (s1=12 | s2=12 | s3=12 | s4=12 | s5=12 | s6=12 | s7=12 | s8=12 | s9=12 | s10=12 | s11=12 | s12=12) | (s1=13 | s2=13 | s3=13 | s4=13 | s5=13 | s6=13 | s7=13 | s8=13 | s9=13 | s10=13 | s11=13 | s12=13) | (s1=14 | s2=14 | s3=14 | s4=14 | s5=14 | s6=14 | s7=14 | s8=14 | s9=14 | s10=14 | s11=14 | s12=14) | (s1=15 | s2=15 | s3=15 | s4=15 | s5=15 | s6=15 | s7=15 | s8=15 | s9=15 | s10=15 | s11=15 | s12=15)) => P<=0.999999 [ true U ((s1!=10 & s2!=10 & s3!=10 & s4!=10 & s5!=10 & s6!=10 & s7!=10 & s8!=10 & s9!=10 & s10!=10 & s11!=10 & s12!=10) & (s1!=11 & s2!=11 & s3!=11 & s4!=11 & s5!=11 & s6!=11 & s7!=11 & s8!=11 & s9!=11 & s10!=11 & s11!=11 & s12!=11) & (s1!=12 & s2!=12 & s3!=12 & s4!=12 & s5!=12 & s6!=12 & s7!=12 & s8!=12 & s9!=12 & s10!=12 & s11!=12 & s12!=12) & (s1!=13 & s2!=13 & s3!=13 & s4!=13 & s5!=13 & s6!=13 & s7!=13 & s8!=13 & s9!=13 & s10!=13 & s11!=13 & s12!=13) & (s1!=14 & s2!=14 & s3!=14 & s4!=14 & s5!=14 & s6!=14 & s7!=14 & s8!=14 & s9!=14 & s10!=14 & s11!=14 & s12!=14) & (s1!=15 & s2!=15 & s3!=15 & s4!=15 & s5!=15 & s6!=15 & s7!=15 & s8!=15 & s9!=15 & s10!=15 & s11!=15 & s12!=15)) ]