((ph0.state=READING)+ (ph1.state=READING)+ (ph2.state=READING))
* (!((ph0.state=READING)* (ph1.state=READING)))
* (!((ph1.state=READING)* (ph2.state=READING)))
* (!((ph0.state=READING)* (ph2.state=READING)));