(!x2 v !x3 v !x4 v !x7)<-(!x1 v !x2 v !x3)+(x1 v !x4 v !x7)
(!x2 v !x3 v x5 v x6 v !x7)<-(!x2 v !x3 v !x4 v !x7)+(x4 v x5 v x6)
(!x2 v !x3 v x5 v x6 v x8 v x9)<-(!x2 v !x3 v x5 v x6 v !x7)+(x7 v x8 v x9)
(!x3 v x5 v x6 v x8 v x9)<-(!x2 v !x3 v x5 v x6 v x8 v x9)+(x2 v x5 v x8)
(x5 v x6 v x8 v x9)<-(!x3 v x5 v x6 v x8 v x9)+(x3 v x6 v x9)
(x2 v !x3 v x4 v !x7)<-(x1 v x2 v !x3)+(!x1 v x4 v !x7)
(x2 v !x3 v !x5 v x6 v !x7)<-(x2 v !x3 v x4 v !x7)+(!x4 v !x5 v x6)
(x2 v !x3 v !x5 v x6 v x8 v x9)<-(x2 v !x3 v !x5 v x6 v !x7)+(x7 v x8 v x9)
(!x3 v !x5 v x6 v x8 v x9)<-(x2 v !x3 v !x5 v x6 v x8 v x9)+(!x2 v !x5 v x8)
(!x5 v x6 v x8 v x9)<-(!x3 v !x5 v x6 v x8 v x9)+(x3 v x6 v x9)
(x6 v x8 v x9)<-(x5 v x6 v x8 v x9)+(!x5 v x6 v x8 v x9)
(!x2 v x3 v x4 v !x7)<-(x1 v !x2 v x3)+(!x1 v x4 v !x7)
(!x2 v x3 v x5 v !x6 v !x7)<-(!x2 v x3 v x4 v !x7)+(!x4 v x5 v !x6)
(!x2 v x3 v x5 v !x6 v x8 v x9)<-(!x2 v x3 v x5 v !x6 v !x7)+(x7 v x8 v x9)
(x3 v x5 v !x6 v x8 v x9)<-(!x2 v x3 v x5 v !x6 v x8 v x9)+(x2 v x5 v x8)
(x5 v !x6 v x8 v x9)<-(x3 v x5 v !x6 v x8 v x9)+(!x3 v !x6 v x9)
(x2 v x3 v !x4 v !x7)<-(!x1 v x2 v x3)+(x1 v !x4 v !x7)
(x2 v x3 v !x5 v !x6 v !x7)<-(x2 v x3 v !x4 v !x7)+(x4 v !x5 v !x6)
(x2 v x3 v !x5 v !x6 v x8 v x9)<-(x2 v x3 v !x5 v !x6 v !x7)+(x7 v x8 v x9)
(x3 v !x5 v !x6 v x8 v x9)<-(x2 v x3 v !x5 v !x6 v x8 v x9)+(!x2 v !x5 v x8)
(!x5 v !x6 v x8 v x9)<-(x3 v !x5 v !x6 v x8 v x9)+(!x3 v !x6 v x9)
(!x6 v x8 v x9)<-(x5 v !x6 v x8 v x9)+(!x5 v !x6 v x8 v x9)
(x8 v x9)<-(x6 v x8 v x9)+(!x6 v x8 v x9)
(x2 v !x3 v !x4 v x7)<-(x1 v x2 v !x3)+(!x1 v !x4 v x7)
(x2 v !x3 v x5 v x6 v x7)<-(x2 v !x3 v !x4 v x7)+(x4 v x5 v x6)
(x2 v !x3 v x5 v x6 v !x8 v x9)<-(x2 v !x3 v x5 v x6 v x7)+(!x7 v !x8 v x9)
(!x3 v x5 v x6 v !x8 v x9)<-(x2 v !x3 v x5 v x6 v !x8 v x9)+(!x2 v x5 v !x8)
(x5 v x6 v !x8 v x9)<-(!x3 v x5 v x6 v !x8 v x9)+(x3 v x6 v x9)
(!x2 v !x3 v x4 v x7)<-(!x1 v !x2 v !x3)+(x1 v x4 v x7)
(!x2 v !x3 v !x5 v x6 v x7)<-(!x2 v !x3 v x4 v x7)+(!x4 v !x5 v x6)
(!x2 v !x3 v !x5 v x6 v !x8 v x9)<-(!x2 v !x3 v !x5 v x6 v x7)+(!x7 v !x8 v x9)
(!x3 v !x5 v x6 v !x8 v x9)<-(!x2 v !x3 v !x5 v x6 v !x8 v x9)+(x2 v !x5 v !x8)
(!x5 v x6 v !x8 v x9)<-(!x3 v !x5 v x6 v !x8 v x9)+(x3 v x6 v x9)
(x6 v !x8 v x9)<-(x5 v x6 v !x8 v x9)+(!x5 v x6 v !x8 v x9)
(x2 v x3 v x4 v x7)<-(!x1 v x2 v x3)+(x1 v x4 v x7)
(x2 v x3 v x5 v !x6 v x7)<-(x2 v x3 v x4 v x7)+(!x4 v x5 v !x6)
(x2 v x3 v x5 v !x6 v !x8 v x9)<-(x2 v x3 v x5 v !x6 v x7)+(!x7 v !x8 v x9)
(x3 v x5 v !x6 v !x8 v x9)<-(x2 v x3 v x5 v !x6 v !x8 v x9)+(!x2 v x5 v !x8)
(x5 v !x6 v !x8 v x9)<-(x3 v x5 v !x6 v !x8 v x9)+(!x3 v !x6 v x9)
(!x2 v x3 v !x4 v x7)<-(x1 v !x2 v x3)+(!x1 v !x4 v x7)
(!x2 v x3 v !x5 v !x6 v x7)<-(!x2 v x3 v !x4 v x7)+(x4 v !x5 v !x6)
(!x2 v x3 v !x5 v !x6 v !x8 v x9)<-(!x2 v x3 v !x5 v !x6 v x7)+(!x7 v !x8 v x9)
(x3 v !x5 v !x6 v !x8 v x9)<-(!x2 v x3 v !x5 v !x6 v !x8 v x9)+(x2 v !x5 v !x8)
(!x5 v !x6 v !x8 v x9)<-(x3 v !x5 v !x6 v !x8 v x9)+(!x3 v !x6 v x9)
(!x6 v !x8 v x9)<-(x5 v !x6 v !x8 v x9)+(!x5 v !x6 v !x8 v x9)
(!x8 v x9)<-(x6 v !x8 v x9)+(!x6 v !x8 v x9)
(x9)<-(x8 v x9)+(!x8 v x9)
(!x2 v x3 v x5 v x6 v x7)<-(!x2 v x3 v !x4 v x7)+(x4 v x5 v x6)
(!x2 v x3 v x5 v x6 v x8 v !x9)<-(!x2 v x3 v x5 v x6 v x7)+(!x7 v x8 v !x9)
(x3 v x5 v x6 v x8 v !x9)<-(!x2 v x3 v x5 v x6 v x8 v !x9)+(x2 v x5 v x8)
(x5 v x6 v x8 v !x9)<-(x3 v x5 v x6 v x8 v !x9)+(!x3 v x6 v !x9)
(x2 v x3 v !x5 v x6 v x7)<-(x2 v x3 v x4 v x7)+(!x4 v !x5 v x6)
(x2 v x3 v !x5 v x6 v x8 v !x9)<-(x2 v x3 v !x5 v x6 v x7)+(!x7 v x8 v !x9)
(x3 v !x5 v x6 v x8 v !x9)<-(x2 v x3 v !x5 v x6 v x8 v !x9)+(!x2 v !x5 v x8)
(!x5 v x6 v x8 v !x9)<-(x3 v !x5 v x6 v x8 v !x9)+(!x3 v x6 v !x9)
(x6 v x8 v !x9)<-(x5 v x6 v x8 v !x9)+(!x5 v x6 v x8 v !x9)
(!x2 v !x3 v x5 v !x6 v x7)<-(!x2 v !x3 v x4 v x7)+(!x4 v x5 v !x6)
(!x2 v !x3 v x5 v !x6 v x8 v !x9)<-(!x2 v !x3 v x5 v !x6 v x7)+(!x7 v x8 v !x9)
(!x3 v x5 v !x6 v x8 v !x9)<-(!x2 v !x3 v x5 v !x6 v x8 v !x9)+(x2 v x5 v x8)
(x5 v !x6 v x8 v !x9)<-(!x3 v x5 v !x6 v x8 v !x9)+(x3 v !x6 v !x9)
(x2 v !x3 v !x5 v !x6 v x7)<-(x2 v !x3 v !x4 v x7)+(x4 v !x5 v !x6)
(x2 v !x3 v !x5 v !x6 v x8 v !x9)<-(x2 v !x3 v !x5 v !x6 v x7)+(!x7 v x8 v !x9)
(!x3 v !x5 v !x6 v x8 v !x9)<-(x2 v !x3 v !x5 v !x6 v x8 v !x9)+(!x2 v !x5 v x8)
(!x5 v !x6 v x8 v !x9)<-(!x3 v !x5 v !x6 v x8 v !x9)+(x3 v !x6 v !x9)
(!x6 v x8 v !x9)<-(x5 v !x6 v x8 v !x9)+(!x5 v !x6 v x8 v !x9)
(x8 v !x9)<-(x6 v x8 v !x9)+(!x6 v x8 v !x9)
(x2 v x3 v x5 v x6 v !x7)<-(x2 v x3 v !x4 v !x7)+(x4 v x5 v x6)
(x2 v x3 v x5 v x6 v !x8 v !x9)<-(x2 v x3 v x5 v x6 v !x7)+(x7 v !x8 v !x9)
(x3 v x5 v x6 v !x8 v !x9)<-(x2 v x3 v x5 v x6 v !x8 v !x9)+(!x2 v x5 v !x8)
(x5 v x6 v !x8 v !x9)<-(x3 v x5 v x6 v !x8 v !x9)+(!x3 v x6 v !x9)
(!x2 v x3 v !x5 v x6 v !x7)<-(!x2 v x3 v x4 v !x7)+(!x4 v !x5 v x6)
(!x2 v x3 v !x5 v x6 v !x8 v !x9)<-(!x2 v x3 v !x5 v x6 v !x7)+(x7 v !x8 v !x9)
(x3 v !x5 v x6 v !x8 v !x9)<-(!x2 v x3 v !x5 v x6 v !x8 v !x9)+(x2 v !x5 v !x8)
(!x5 v x6 v !x8 v !x9)<-(x3 v !x5 v x6 v !x8 v !x9)+(!x3 v x6 v !x9)
(x6 v !x8 v !x9)<-(x5 v x6 v !x8 v !x9)+(!x5 v x6 v !x8 v !x9)
(x2 v !x3 v x5 v !x6 v !x7)<-(x2 v !x3 v x4 v !x7)+(!x4 v x5 v !x6)
(x2 v !x3 v x5 v !x6 v !x8 v !x9)<-(x2 v !x3 v x5 v !x6 v !x7)+(x7 v !x8 v !x9)
(!x3 v x5 v !x6 v !x8 v !x9)<-(x2 v !x3 v x5 v !x6 v !x8 v !x9)+(!x2 v x5 v !x8)
(x5 v !x6 v !x8 v !x9)<-(!x3 v x5 v !x6 v !x8 v !x9)+(x3 v !x6 v !x9)
(!x2 v !x3 v !x5 v !x6 v !x7)<-(!x2 v !x3 v !x4 v !x7)+(x4 v !x5 v !x6)
(!x2 v !x3 v !x5 v !x6 v !x8 v !x9)<-(!x2 v !x3 v !x5 v !x6 v !x7)+(x7 v !x8 v !x9)
(!x3 v !x5 v !x6 v !x8 v !x9)<-(!x2 v !x3 v !x5 v !x6 v !x8 v !x9)+(x2 v !x5 v !x8)
(!x5 v !x6 v !x8 v !x9)<-(!x3 v !x5 v !x6 v !x8 v !x9)+(x3 v !x6 v !x9)
(!x6 v !x8 v !x9)<-(x5 v !x6 v !x8 v !x9)+(!x5 v !x6 v !x8 v !x9)
(!x8 v !x9)<-(x6 v !x8 v !x9)+(!x6 v !x8 v !x9)
(!x9)<-(x8 v !x9)+(!x8 v !x9)
()<-(x9)+(!x9)