Query splitting coding challenge example inputs

expressions.in

T
F
v1
w1
(and v1 v2)
(and w1 w2)
(and v1 w2)
(or v1 v2)
(or w1 w2)
(or v1 w2)
(not v1)
(not w2)
(and (and (or (or w3 (not (and w1 (and (or w1 v4) w2)))) (and (or (or (and v1 (or (not v3) v2)) (and (or v2 v5) (not w1))) (not (or (and (and v2 v5) (or w2 v1)) (or (and v2 v4) v5)))) (and (and (and (or (or v1 v3) v4) v3) (or (not (and w1 w1)) w1)) (or (and (or w2 v3) (not v4)) (and (and (or v5 w3) v5) v1))))) (and (and (not (not (and (or (or v1 w2) (not v2)) w3))) (not (not (or (not (and w3 v1)) (or (or v3 v3) v5))))) (and (not (and (not (or w2 (or w1 v2))) (not (and (not v5) (not v1))))) v3))) (and w2 (or (and (and (not (and v1 (or (or v3 w3) (and w3 w3)))) (not v1)) (not (not (not (and (and v4 v3) v4))))) (not (not (and v5 (not (or w2 (and v3 v3)))))))))
(and (and (and (or (or v1 w2) (not v2)) w3) (and (not (and (not (or w2 (or w1 v2))) (not (and (not v5) (not v1))))) v3)) (and w2 (and (not v1) (not v4))))
(or (or (not (or (not v8) (or (or (not (and (and (not (or (and (and (and (not (not (or v15 (not v12)))) (not (not v17))) (and (or (or (or (or w1 v7) v19) (not w6)) (and (and (and w6 (not v20)) (and (and v6 v20) w3)) (and v9 v4))) (and (or (or (not (or v11 w1)) v15) (not (and (not v11) v5))) (not (or v2 (not (or v8 v20))))))) (not (and (or (or v17 v5) (and (or (and w2 v17) (not (and v5 w6))) (not (or (not v14) v14)))) w2))) v2)) (and (or (and (and (or (and (not v13) (not v10)) w8) (and w10 v19)) v9) (or (not (and (and (and (and v12 (and (or v1 v12) w10)) (and (not v9) v14)) w8) (not (and v10 v5)))) (or (or (not v4) (or (or (and v18 w2) (and v1 v2)) (or w9 w9))) (and (or (not (and w7 (not w7))) (or (or (not (or w2 v20)) (or (and w3 v13) w8)) v5)) (or (or (and (and v14 (and v3 v17)) w4) (or (not (not w3)) (not v4))) w3))))) w9)) (and (or (or (or (not (or w2 v13)) (and (or v14 (or (or (and v3 (and w1 (not v16))) v1) (and v14 (and (not (or v3 w1)) w8)))) (and (or (or (and (not v1) (not (or w5 w2))) (or (or v9 v4) v16)) (or (and (and (and v17 w2) v10) v11) (not (not (or v2 w3))))) w10))) (not (or (not (and v1 (or (not v6) (and v3 (or (not v15) (or v9 w10)))))) (not (and (or (not v20) v5) (and (or v9 (or (not v12) (not v14))) (or (and (and v5 w6) v9) (not v15)))))))) (or v8 (and (or (not (or (or (not (and v12 v9)) (and (not (and v18 w1)) (and v11 (or w4 v8)))) (not (or (or v11 (and v20 v2)) (and (not v16) v19))))) (or (not (not (or w9 (or v13 (and w5 w9))))) (and (not (or (not (not v7)) w3)) v2))) v20))) (not (not (and (or (and (not (or v19 w1)) (not (and (not (not v7)) (and (and (not v17) v6) (or (or v10 v5) v9))))) (and (or (and v12 v2) (and v10 (and (not v17) (and v15 (not w5))))) (and (not (and (and (and v18 v17) v3) (or v9 w8))) (not (not (and v3 v8)))))) (and (not v10) (or (or (and (not v10) (not (and w4 (or v19 v7)))) (not (not (not v2)))) (and (and (not (or (not w1) v20)) (or (or (not w7) v9) v14)) v15))))))))) (not (not (not (and (not (and (or (and (or (not (or (not (and v5 w4)) (not (not v2)))) (not (not v2))) (or (or v9 v19) (or (and v18 (not v1)) (and (and (and v12 v3) w8) v15)))) (and (and (or (not (or v4 (not w5))) w5) (and (not v2) (not (and w2 w2)))) v7)) (or (and (not (or (not v16) (and (and v11 w10) (or (or w5 v12) (and v5 v17))))) (and (not v7) v8)) (or (or (not (not (and (not v20) v3))) v14) (or (or (or (not w10) v5) (and (or v17 (not v16)) (and v1 (not w1)))) (not (and (and v3 (or w6 w3)) w2))))))) (not (not (not (not (or (and (not (or v10 w8)) (not v17)) v11)))))))))) (or (or (or (and (or v1 (not (and (not (and (or (not (not v4)) v9) (and (and (or (or (or w4 w10) w10) (not w6)) (and w8 (not w10))) w3))) (not (and v5 (not (not (or (and v2 (and v15 v16)) (or (or v6 w2) (not v8)))))))))) (or v7 (or (or (or v12 (or (not (not (not (and v4 v7)))) v16)) (and (not (and (not (and v16 (not v14))) (or (and v3 (and (not v1) w6)) (not (not w1))))) (or (not (and (or (and (and w9 w10) v4) (and (and v17 v19) (and w5 v9))) (or (not (and v14 v20)) (not (or v7 v5))))) (or (or w9 w4) (and (or (and w6 (or v6 v4)) (and w9 (or v4 v1))) w2))))) (not (or (or (or (and (not v12) (and (and w2 v6) (or (or v19 w10) v11))) (or (not v8) (or v4 (or w10 (not v11))))) (not (not (not w9)))) (or w6 (or (or (or w4 (not (not w4))) (not (not w3))) (not (or v5 (or w5 w4)))))))))) (and v13 (or (not (not (and v20 (or (and (or (and (and v1 (not v6)) (not (or v5 w10))) v15) (and (or (and (not w6) (and w9 v2)) (not v8)) (or v19 (and (and w7 v6) w9)))) (and (not (and (or v20 (and v1 w4)) v19)) (and (or (and v5 (and v18 v4)) w7) v5)))))) (or w1 v19)))) (or (or (not (not (and (not (and (or (not (or (and (not v2) v3) (not v11))) (not (and (or v2 v8) (not w1)))) (not (and (or v15 (or (not v13) (and v5 w9))) (or (not v12) (not w4)))))) (not v10)))) (and (or (and (or v1 (and (or (and w8 w1) v8) (or (not (not (not (and v1 w3)))) v9))) (or (not (not (or v2 v2))) (and v10 (not (and (or (or (or v19 v7) w3) v10) (or w7 (and (and v14 v20) v17))))))) (and (not (or (and (not (not v4)) (or (and (and v10 v2) w4) (not (or v6 v11)))) v18)) (not (and v16 v14)))) (not (or (and (and (and (or (or (or (and w7 v12) (or v6 v2)) (and (and v17 w6) w9)) w3) (not v8)) (or (and (or (or (and v3 v20) (and v13 w8)) w6) (or (or (not v13) (or v6 w5)) (or v8 (and w7 v2)))) (not w4))) (and (not v1) (not (and (or (not v18) (not w2)) (or (and (or w5 v1) v3) (and w7 v18)))))) (or v3 (or v2 (not v13))))))) (and (or (or (or (or (and v19 (or (or (not (or v10 v9)) (and v8 v17)) w6)) (or (not (and (and (or v18 (and v5 v15)) (not v13)) (and (or (and v3 v1) w3) v5))) w4)) (or (or (and w9 (and (not (not v12)) (or (and (and w4 w7) (or v5 v1)) (and v6 (not w5))))) (or (not (and (not (not v3)) (and w7 v20))) w9)) (or (and v10 (and (or w9 (or w9 v15)) (or (or (not v5) (not v18)) (and (and w9 v18) w5)))) (and (or (and w7 v18) w3) (and (not (or w3 v1)) w3))))) (not (not (or (or (or (and v3 w6) (and (or (not v12) (or w4 v10)) (and (or v4 w9) (and v1 w1)))) (or (not (or (or v11 v19) (not w7))) (or (and v6 (or v6 v16)) (not v19)))) (not v16))))) (or (and w4 (not (or (not (not (not (or w5 (not w6))))) (and (not (not (not (and v20 v10)))) (or (not (and (or v8 w9) (and w5 v12))) (or v14 (not (and v14 w4)))))))) (not (not (and (or (not (not w3)) (not (not v10))) (and (or v11 (or (or v7 (not v17)) v2)) (not (and v8 (or v19 w7))))))))) (not v11)))) (or (not (and (not (not (or (and (and v16 (and (and (or v6 w6) (not (not (not v1)))) (or (and (and v15 (not v1)) (not w6)) (not v2)))) (and (or (and v10 w1) (and v7 (not (or (or v4 v17) (not v9))))) (or (or (or (or (and v17 w1) w7) (or (not v16) v4)) v2) (or (and (or w9 v1) v11) v13)))) v11))) (not (not w2)))) (not (or v3 (and (not (or (not (not (not (and (and (or v6 v5) (or (not w2) (or v20 w9))) (not (and v7 v2)))))) v18)) (or (not (not (or (or (not (not (or (and v7 v14) w3))) (not (and (or (or w8 v16) w10) (or v16 (and w4 v15))))) (not (or (not (not (not v15))) (or (and v12 (or v17 v4)) v6)))))) (not (not (and (and v18 (or w2 (not (or v2 v14)))) v5)))))))))))) (and (not (or (or (not (not (and (and (or (not (not v8)) (and v6 (and (or (and (not w6) (or (or w7 v20) (or v13 v9))) (and v19 (or (not (and (or v4 v17) (not v17))) (and (not v14) w3)))) (and (or v7 (and (and (and v7 (and w4 v17)) (or w2 w7)) (and w7 (not (not w6))))) (or (and (and (not v16) (or (and v17 v9) (or w9 v17))) (not (and v17 (not w10)))) (not v7)))))) (and v7 (and v20 (not (and v5 (or (or v13 v6) (not (and (and v14 (not v19)) v12)))))))) (or (or (and (not (or (and w7 (and w6 (or (and (and w8 w10) (and v18 w3)) (not v3)))) (not w8))) (not (not (or v6 w7)))) (not (and v11 (and (not (not (or (or (or v10 w10) (and v19 v18)) v4))) (not (or (or w7 v1) (or v14 v3))))))) (or (not (and (not (or (and (not (and v3 (not w7))) (or (and v13 (not v13)) w3)) (and (and (not (not w4)) (or v11 v7)) w9))) (and (or (or (not (and w8 v13)) (and (and (or w6 v13) w4) (or (and v5 v11) (not v9)))) (or (or (or w1 v1) w1) v15)) w1))) v16))))) (not v15)) (or (not (or (not v13) (and (not (and (or (or (not (not (not v19))) (or (and (or (or v11 (not (not v12))) w8) (and (not (or (not v2) v3)) (or v4 (or (or w2 w10) w7)))) v16)) (or (and (not (or w10 (or (or v18 v10) (and w9 v20)))) (or v6 v5)) (not (or (and v20 (not (not v20))) (and v8 v2))))) v10)) (not (and v11 (and w10 (or v18 v9))))))) (or (or (and v7 (or (and (and (not (not (and v9 v11))) (or v5 (not (not (and w1 (or v4 (not v4))))))) (or (not (and (not (or (or (not (or v5 v5)) (not v11)) v18)) (or w9 (not (or v12 (not v16)))))) (and (or v20 (and (or w7 (or (or (not v9) w5) (and v3 (and v4 v10)))) (not (not (not v5))))) (not (or v4 (not (and (and w4 (not v2)) (and v4 v10)))))))) v11)) (and v15 (or (and (or v7 (not (and (not (or (or (and v12 v5) v7) (or (and w7 (or w8 v4)) (and v10 (or v12 w10))))) w3))) (and (and (not (and (or (or (or w2 (or v2 w4)) (not (and w6 v16))) v8) (and w9 (not (or w5 v8))))) (and (not (and (and (not v8) v18) (and v15 (and (and v3 v7) (or v6 v9))))) (or (or (not (or (and v5 v9) w1)) (or (and w9 (and w1 v11)) (and (and v16 v2) (not w10)))) (or (and (not v20) (and (or w9 w2) (and w3 v13))) (not (and (and v20 v3) v4)))))) (not (or (or (or v10 (and (or w2 (and w7 w1)) (and (or w1 w6) (and v20 v16)))) v18) (not v2))))) (not (not (and (not (and (or (not w10) (and (not (or v4 v13)) (not v20))) (and (and w1 (or (and v7 v9) (and v14 w2))) (and w3 (or v3 w9))))) (or (or (and v6 (not w10)) (not (not (not v3)))) (not (or (and v20 (or (not w7) (not w4))) (not (not w1))))))))))) (or (or (and (or (and (or w3 (or (or (and (and (and (and w1 v7) v6) (not (or v4 w3))) w1) (and v5 (not (not (not w3))))) (and (not (not (or (and v6 w8) w7))) (not (or v16 (and w2 (not v10))))))) (or (and (not w5) (and w4 (and w7 (not v16)))) (not (or (or (or (and (and w1 v12) (and v4 w10)) v14) (or (or (or v16 w4) (and v12 v7)) v1)) (not (and v9 (and w6 w2))))))) (or (and (not (and (not (and (or v13 (and w2 v5)) (or v18 (and v15 w3)))) (or w10 (or (and w1 v17) (not (not v16)))))) (and (not (not v12)) (and (and (not (and (and v19 v15) v11)) v6) (and (not (and v16 v13)) w8)))) (not (and (or (or (or w8 v10) (not (not (and v3 w6)))) w3) (or (or (not (not w1)) (or w3 w10)) (or (or (not v11) (or w9 w10)) (not (not v16)))))))) (or (and (and (and (not (not (and (not v9) w3))) (and (and v9 (and w9 (and v9 w3))) (and (and (not w10) (or (not w8) (or v9 v16))) v17))) (or (not (not v19)) v15)) (and (or v4 (or v16 (not (and (not (not v9)) w5)))) v4)) (or (not (or (or w1 (not (and (and (and v15 v7) w7) (or (and w10 v9) v10)))) (and w4 (not (and (not (and v2 v15)) v18))))) (or (or (not (and (or (or v19 (or w9 v11)) (and w3 v12)) (or (and w7 (not v4)) (not (and w7 v6))))) (not v12)) (and (not (or (not v17) (and (not (not w9)) (or (and v9 v12) (or v15 w8))))) (not (or (not (and (and v11 v17) (or w7 w4))) w4))))))) (not (and (or v5 (not (or (or v4 (not (and v20 (not (or v16 v11))))) (not (and (not v14) v12))))) w6))) (or (and v1 (not v1)) v1)))))) (or (not (not (or (and (or (not (or (or (or (not (or (and (not (and v8 v5)) v7) (and (or (not w8) (not (or w9 w4))) v18))) (or (not (or (or (not (or v1 w4)) w3) v9)) (or (not (not (not (not v2)))) (and (and (and (not v19) (not v18)) w6) (not v10))))) (and (and (or (and (not (not (not w3))) (not (and (not w2) (not v7)))) (not (and w4 v4))) (not (or (and (not (or v4 v3)) v10) (and v2 v15)))) (not (and (and v14 (and v6 v13)) (and (or (and (or w10 v9) w5) v13) (not w5)))))) (not (or (not v17) (or (and w7 (not w4)) (and (or v7 (and (or v20 v12) (not (or v8 v18)))) v5)))))) (or (not (or (and (not (not (not (or (not (and w7 v11)) v6)))) (not (or (and v16 (not (or (or v2 v1) v15))) (and (and (not v15) v6) (not v4))))) (or (and (or v5 w5) (or (and (or (not (not v13)) (or v5 w9)) (and w8 (or (or w3 v6) w4))) (not (or (or (not v11) (not w1)) (and (and w10 v17) (not v16)))))) (not (not (not (and w1 (and (or v17 w2) (and v19 v2))))))))) (or (and (or (and (or w1 (or (not w8) v5)) v4) (not (or (not (and (or v5 (and v14 v1)) w8)) (not v2)))) v20) (and (not (or (not (not v11)) (or (and (not v12) w2) (not (or (or v8 w3) v5))))) (not (not (and (or v8 (or (and v13 (and v20 w5)) w5)) (or (and w3 (not v18)) (not v12))))))))) (or (not (not (and (and (and w5 (not (or (or (or v3 (and w1 w7)) (and w7 (not v7))) (not w8)))) (or w5 v18)) (and w2 (and (or (and w3 (and (or (and w10 v20) w10) (and (not v10) (and w10 v16)))) (or w5 (or (not (or v13 v2)) (not (or v11 w10))))) (or v4 (or (not v19) (not w7)))))))) (not (and (not (not (not (and (not (and (and (and v4 w3) (and w10 v18)) (not (and w7 v12)))) (and (or (not v13) (not (or w5 v18))) (and w3 (or (not w7) (and w8 v14)))))))) (and (or (or (or (not (and w3 (or v12 (not v18)))) (or (and v15 (not v19)) (and (and v1 (and w4 w3)) v1))) (not (or (not (or w1 v3)) (or (and v12 v15) (or v1 (not v2)))))) (or (not (not (not (not (or w7 w3))))) (not w5))) (not (not (and (not (not w1)) (and w1 (or (not w2) w2)))))))))) (or (or (or (not (and (not (not (not (and v7 (not (and (and w6 v13) w10)))))) (or (not (and (not (and (not (not w1)) v6)) (not w8))) w6))) (not (or (not (or v1 (or w6 (or (not w9) (and v5 w10))))) (or (or (and (and (or (or (not w5) (or v8 v3)) v6) (not v14)) (or (and w8 w1) (and (or w2 (not v7)) (not (or v4 w7))))) (or (or v1 (not (not (not v12)))) w10)) (and (and (and (not (and (not v13) (not v19))) v17) (and (not (or (or w7 v18) w9)) (not v8))) (or (and (and (and (not v5) (or v10 v4)) (or w4 v2)) (and w7 v10)) w4)))))) (or (and (or (and (or (not (and (not v5) (not (not (not w9))))) (and w7 (not v18))) (or (and v17 v16) v13)) (and (not v2) (and (not (and (and (not (not w6)) (not (or v19 w6))) (and (and w2 v20) v19))) (or (not v12) (and (and w10 (and v7 (or v14 w2))) (not w1)))))) (and (or (or (or (or (not (not (or w6 v7))) w4) (and (or (and (or w8 v10) (not w7)) (and (or v9 v3) v18)) (not (or w9 (or v15 w3))))) (and v5 (and (or (or v17 v14) w3) w2))) (or (not w10) (and (and w1 (or (and v20 (not v18)) w2)) (not (not (not v12)))))) (and v9 (not v17)))) (and v14 (not (or (or (and (not (or (or w4 (and v17 v1)) (or (or v11 v5) (not w6)))) (and (or (or (and v19 w3) v4) (not w6)) (not (and (and v15 v19) (or v7 v14))))) (or (and (not (not (and w2 v7))) (not v12)) (or v4 v19))) (and (not (and v12 (not v9))) (and (and (not w9) (not (or (not w1) (or v10 v1)))) (and (or (or w1 (not v4)) w1) (not v14))))))))) (or (not (or (and (and (and v1 w8) v4) (not (or (or (and (not v15) (and (and (not w1) (or v4 w10)) (not v10))) v15) (not (and v11 v2))))) (not (or (or (or (and v5 (not (or (and v9 v8) v17))) v8) (or (or (not v5) (and w4 (not (not v4)))) w9)) (or (or (not (not (not w4))) (or (and w3 (and w3 (or v11 v6))) (and w10 v9))) (not v11)))))) (and (not (not (and (not (not (or (or (or v7 v8) w7) v4))) (or (and (and (not v7) (not (or (or v14 w4) (not v6)))) (and (not (and v13 (and v17 w4))) (not v1))) (not v10))))) w10)))))) (and v3 (or (or (not (and (and (not (not (not (or (and (and (and v16 (or (and w8 v15) v6)) (not (not w9))) w7) w7)))) (and (and (and v20 v16) (or (and (and (not (not (or v11 (not v12)))) (not v5)) (or (not v17) (or (or (not v6) (not (not v2))) (or (and (and w5 w6) (not v10)) v13)))) (or (and (or w10 (or (or w4 v10) (not w8))) (or w8 (and (not w2) (and w1 (or w4 v20))))) (and (and (and (or (not v5) w3) (or v2 (not v6))) v18) (not v14))))) (or (not (or (or (or (not (and (or w9 v5) (not v19))) (or w7 (and (or v4 v12) (not w8)))) (or (not v19) w6)) (or v12 (or v18 (or (and (or v9 v14) w8) (and (or v6 v16) v11)))))) (or (or (or v1 (and (or (or (not v13) (not v15)) (or v16 v13)) (and v9 (and (not v14) v9)))) (and (and v8 (not (or (and v8 v8) (and w6 v16)))) (or w4 (or (or w10 (and v3 w3)) (and w10 (not w8)))))) (not (or (or w3 (not v8)) (and (or (and v3 v18) (not (and v13 w4))) (not (and v9 (or w1 v12)))))))))) (and (not (or (or (or (or (and w7 (and (not (and w2 w1)) v16)) (and (and (or (and v4 v3) (not v17)) (and w6 (and v15 w9))) v2)) (and v18 (or (not (and (not v2) w9)) (and (or v8 (not v5)) (not v5))))) (not (or (or (not (or v18 (not v17))) v4) (not v4)))) (and (or (or (and (and (and (or v16 w8) v10) v16) (and (not v9) (or v15 (or v19 w3)))) (not v12)) (and (not (or (or v9 (not w3)) v15)) v14)) (and (or (and (and (not (and v8 v15)) (or v12 (or v19 v1))) (and w7 v18)) (and w2 v7)) (and (not v10) (and (or (and (or v17 v12) (not v2)) (and (not v13) v6)) (and w2 v1))))))) (or (and (not (not (and v20 (and v8 w10)))) (and (or (and v1 w2) (and (or v8 (not w5)) (not v11))) (not (not (or v2 v12))))) (not (or (not (and (not (or (and (and w5 w6) w10) (and (not v15) v15))) (not (not (not v9))))) (and (and (and (and (or v17 v8) v4) (not v8)) (or (and (not v8) (or (not v19) v8)) (not v1))) (or v17 (or (or (or (or w2 w1) (and v14 w5)) (or v5 (not v13))) (and v3 v16)))))))))) (and (not (or (or (and (and (and w6 (or (or (not (and (not w2) (and w9 v18))) v12) (or (or (or (not v13) v11) (or (not v11) (or v4 v17))) (not (or w3 w7))))) v6) (not (and (or (not (and v17 (or (or v4 v10) (not v3)))) v14) (or (and (not (and v3 (or v1 w2))) v3) w5)))) (not (or (and (or (not v15) (or (and w3 (and v19 w7)) (or v16 (not v18)))) (and (and (and w3 (not (not v4))) v19) (or (and (or v18 w5) (not v2)) (and v3 (and (and v6 w5) v13))))) (or v3 (and (or (not v9) (not v2)) (and (or (or v16 w3) (not (and v19 v5))) (not v18))))))) v11)) (not (or (and (and (not w10) (not v6)) (not (and v18 (or (not (not (and (or w9 w6) (not (or v14 v5))))) (and (or (not v16) v14) (not v15)))))) (or (and (or (or (not (not v9)) (or v5 (or (and v7 w3) (not v18)))) (not (or (not (or (or (or v2 v16) w6) (not v13))) w9))) (and v5 (not (or (and (not (not (or v19 v16))) (and (or (and v11 v17) v19) (and (or v4 w5) v2))) (or (not (and (and w2 v18) w3)) w5))))) (or (and v13 (or (not (not (not v10))) v15)) (not (not w4)))))))) (or (or (not (or v9 (and (or (and (not (and (and (not (not w5)) w9) (not (or (not (or w2 v12)) (or (and v8 v10) w4))))) (not (not (or (and (and v16 w8) v4) w2)))) (or (and v15 (or v6 (not (and (and v2 v1) w10)))) (and v8 (or v20 v18)))) (or (and (and v8 (and (and w8 (not v1)) (and (not (and (and v15 v1) (and v11 v1))) (not (or (not w6) (and w10 v7)))))) (and (not (or (not v7) w10)) (not (or v2 (not v10))))) w7)))) (or v10 (not (not (or (or (and (and (not (and (not (and v3 v13)) (not v10))) (or (and (not v1) (not (and v15 v1))) (not (and w5 v12)))) v10) (not v7)) (or v14 (not (or (or (not (and (or w3 w3) w6)) (not (and (or v5 w10) w9))) (or v7 (not (and (not v17) (or v9 w6)))))))))))) w8)))))) (or (not (not (and (or (or (not (or (not (and (not (not (or (or (or v9 (or v19 v19)) (or v18 v19)) (and (not v9) v2)))) (not (or (and (and v19 v12) v1) (not (not (or (not v4) (or (not (and v19 v19)) w3)))))))) (not (not (and (not (and (or (or (not v18) (and (or (and v11 w10) (and v10 v18)) (not w3))) (or (and (or w7 (not v2)) (or v8 w5)) (not (or v20 v4)))) w1)) (or (and (and (or v18 (not (not (not v18)))) (and v6 (or (not w10) v2))) (not (not (not w9)))) (or (or (or (not (and v15 v6)) (not (and w4 (not v12)))) (or (or v3 (not w6)) (or v9 v3))) (not v4)))))))) (and (not (and v20 w6)) (not (not (not (and (and (not (and (not (not (and (and v11 v9) (or v3 w8)))) (or (or (or (and v18 v7) v16) (not (and v15 w1))) v11))) (not (and (not (and v17 (or (not v2) v6))) v13))) (and v16 (not (not (or (not (not v18)) (not w4))))))))))) (or (not (and (and (or (not v11) (and (or (or (or (or (not w8) (not (not v2))) (or v15 (or w3 v4))) w10) (and (or (not v7) (and (and v18 w10) (not (and (and v19 w3) w10)))) (not v10))) (not (not (or (not (not (or (and v19 v6) (not v7)))) (or (or (or (or w1 w1) (not v12)) (or v4 w4)) w4)))))) (or (not (and (not w8) (not (or (and (not w7) v5) (not (and (not (not v13)) (and w5 v7))))))) (not (and (not (not v16)) (or (and (and (or (not v19) v5) v3) (and (or (or v5 (not v2)) (and (and v2 w3) w1)) (and (and v4 v14) w8))) (or (and v9 (not (and v16 v9))) (or (and (or (and v16 w2) (and w3 w6)) (or (not w8) w10)) (not (not (and v2 w2)))))))))) (or (not (not (and (and (or (or v17 (not v11)) (and (not (and v13 v6)) v11)) (not (not v15))) (and (and (and v8 (not (and v3 (not v18)))) (or (not (not (not v5))) (or (and (not v6) (not v2)) (and (or v17 v20) w2)))) (and (and (or (or w1 w1) w6) (not v1)) (not (or w6 v6))))))) (or (not (and (or v15 (not (not (and (not (and v14 v20)) v8)))) (and (and (or (not v3) (not v8)) (or (not (not v7)) (not v4))) (and (or (not (not (or w5 v18))) (or (or (or w4 v13) w5) (or (not v7) v7))) (not (or (not w8) v9)))))) (not (or (and (and v2 (not (or (and (or w2 v9) (or v1 w2)) (and (not w4) (or w4 v13))))) (and (or (or v11 (not w3)) (not w1)) w3)) (or (or (not v8) (and (not (not v14)) (and v15 v17))) (and w2 (not (not (and w9 (and w9 w2)))))))))))) (not (or (not v18) (or (or (or (and (not (or (or (and (and (and w7 v12) w10) (not w4)) (and (not v11) (not (or w7 w10)))) v3)) v10) (not w3)) (and (not (or (or w5 (and (not (or v3 v16)) (and v18 (and v16 (and v16 v18))))) (not (not (and v16 (not v5)))))) (or (and (not v3) (or (and w9 (not (not v12))) (and (or (and w6 (and v5 w9)) (or w6 v12)) v10))) (or w7 (and (and (or (not w3) (not w3)) (or (and v5 (not w1)) (not (and w1 w3)))) (and (or w1 (not (not v7))) (or v9 (not v14)))))))) (or (and (or (not (and v7 v1)) w2) (not (or (or (not (not (or (and v10 w10) w2))) (or (not (or (not v15) (and v1 v19))) v1)) (not (and (or (or (or v5 v14) v8) (or (not v14) v14)) (or v19 (and v9 v10))))))) (not (or (not (or (and v10 (and (or w4 (and w5 v1)) (not (not w4)))) w3)) (not (or (or v3 (not (and (and v10 v20) (and v20 v7)))) (and (not (or (or w8 w3) (and w10 v20))) (or w1 (or v13 (not v1)))))))))))))) (or (or (not (not (and (and (not (or (not (or w3 (and v1 v10))) (and v13 (not (not (and (or v16 (not v11)) v7)))))) (or (or (or (not v12) (not (or (and (not w3) (not w7)) (and v15 (and (or w2 w5) v17))))) (and (not (and (not (and v12 w6)) (not (not v19)))) (and (not v12) (or (or w5 (not w3)) (not (not v9)))))) (and (and (and (not (or (and w10 (or v9 v2)) (not (or v7 v15)))) (not (and (not (or v17 v15)) (or v8 (and v15 v6))))) (not (or (or v2 (not (not v2))) (or (not (or v16 w6)) (not (or v5 w1)))))) (or (or (not (or v14 (not (or v9 v14)))) (or (not (not (or v19 w3))) (and v3 w5))) (not (and (not v2) w9)))))) (or (and (and (or (or w4 (or (not (or (or w7 w4) (or v5 v20))) (not (and w6 w6)))) (and v11 (and (or (and (and v1 v14) v10) (not v17)) (or w5 (or v2 v12))))) v15) (not (or (or (and (or (or (not v4) (not w7)) w5) (or (and v8 v16) (and v15 (and v10 v19)))) (or w2 v17)) (or (and (not w2) (or (and (not v20) (and v1 v17)) (and (and v3 w10) v12))) (not (not (and (or v19 v7) v3))))))) (not (and (not (or v14 (or (or (not (not w9)) (or w3 w3)) (and w3 (and (or v13 v18) v20))))) (and (and (and (not (not (not v5))) (not (or v13 (or w4 w5)))) (not (or (not (not v16)) (not w10)))) v9))))))) (not (and (or (or w3 (not (and (and (not (not w7)) v7) v7))) (and (and w1 v17) (or (not (not (or (and (not (or (not v4) v3)) (not w4)) v3))) (or (not (and (or v19 (or (not (or v8 v15)) v2)) (and (and (or (or w6 v8) (and v4 w4)) (and (not v15) (not w3))) (and (or v20 v12) (not (not v8)))))) (or (and w9 (not (not w6))) (not (not v2))))))) (or (or (not (not (not v20))) (not (and (not (not (and (not (not (not v12))) (not w7)))) (or (and (or (not w9) (not (or v4 (not v17)))) (not (or (not (not v8)) (and v3 (not v14))))) (not (not (or (and (and v18 w3) (not w4)) (or v1 w3)))))))) (not (not (not v15))))))) (not w9))))) (or (and (or (and (not (or (not (not (not (and (and (and (not (and (and (and (not w3) w8) v18) (not v20))) (not (and (and w6 w8) v4))) (and (not (and (not v1) (or (or w4 (and w7 w6)) (not v15)))) (not (or w9 v16)))) (and v17 (and (and (or (and (or (not v1) (not v7)) v2) (and w6 w1)) (not v16)) (or w3 (not (not w10))))))))) (not (and (or (not (not v14)) v17) v3)))) (or (not (not (not (and (or (or (and (and (not (and v9 (not (not v14)))) (not v8)) (or (not v17) (not (or v4 (and v16 v5))))) (or (not (not w9)) (and (and w3 (not v16)) (and (and (not v3) (not w3)) (and (or v3 v6) (or w4 (not w10))))))) (and (not (or (not (or v6 (and (not v18) v1))) (not (or (not v5) (or v15 (not v13)))))) (or (and (or (not (or v10 v1)) (not (or v19 v13))) v11) v17))) (not (or (or v3 (or (not (or (and (not v11) (and w10 v19)) v2)) (and (or v19 (or v10 (not w9))) (not (and v5 v12))))) (or (not (and (or v8 (or v4 (and v7 v20))) (not (or w10 w2)))) (or w6 (and (not v16) (or (and v3 v15) (and (not w10) (and w7 w1)))))))))))) (and (not (and (and (or (or (or (and (or (and w2 (not (not v7))) (not (not (or w8 v5)))) (and w1 v17)) (not (not w5))) (not (and (and w3 (not (and v3 (not v18)))) v2))) (not (or w7 (and v11 (not v15))))) (and (and (or (or (and (and v12 (not (or v16 v10))) v20) v8) (or (or (not (or (not v1) v15)) (not v11)) (not (or (not (or w10 v7)) (not w7))))) (and (not w3) (not v15))) (and (or (not (and (not (and w5 (not v9))) (and (not (or v2 w7)) (and (or w6 v5) v2)))) (and (or (and (and (or w10 w1) (or w8 v20)) v19) w1) (and (or v18 (or (or v3 v1) (or v13 v9))) (and w5 (not w1))))) (or (and v18 v15) (not (and (and (not w9) (not w4)) v13)))))) (not (and w2 v20)))) (or v8 (not (not (or (or (and (not (or v8 (not (or v1 v20)))) v20) (and (and (or (and v13 v7) (and v4 (or v20 (and v1 w2)))) (not (not v19))) (or v10 (and (and (not v9) (not (not v14))) v11)))) v2))))))) (or (and (and (not (not (and (not v18) (or (and (and (and w6 w3) (not (not v3))) (and (or (or (not (not w4)) v2) (not (not (not v11)))) (and (or (or (or v1 v15) v2) v18) (not w2)))) (or (and (or (or (and v13 (not (and w8 v16))) (and (not (or v10 v2)) v7)) (or (and (not (not w1)) (and (and v1 v19) (and v20 v7))) (not (not w3)))) (not w2)) (or (and v1 (not (not (or w5 v1)))) (or (not (not w10)) v3))))))) (and (not (and w10 (not (not (or w5 (or (or (not (not (or v9 v10))) (and (not (and w10 v18)) v13)) (and v8 (and (and v16 v7) (not v6))))))))) w10)) (or (or (or (and (or (or (not (and (not (and (or w3 v15) v11)) (not (and (and w9 v2) w4)))) (or v12 (or (or w6 (or v5 (and w8 w6))) (or (and (and w6 (not v1)) (or w1 (or w6 v10))) (and v17 w9))))) (not (or (not (not (and (not (or v20 v20)) w6))) w6))) (and (or v10 w6) (and (not (or (or (or (not (not w3)) (or v4 w9)) (not (not (and w4 v8)))) w2)) (and (or (and (and (or w8 (and w4 v6)) v4) (and v5 (or (or v11 w3) (not w1)))) (or (not (not v14)) (or w4 w7))) (or (or v15 v6) v17))))) (and (or v2 (or (and (not (not (and (or w5 v12) (or (not v5) w8)))) (and (or w1 (or (or (not w9) (or w1 w10)) w3)) (and (and (not w7) v14) (or w8 v15)))) (or (and (or (not v8) (or (not (or v8 v10)) (or (or w2 v5) v15))) (and (not v2) v17)) v14))) w2)) (or (or (not (not (and (or (not (not v20)) (and (not (not v14)) w4)) (not (or (not v6) (or (or (or v19 w9) w1) (and (not v19) (or v17 v7)))))))) (not (and (or (not (and (and (or (not v14) (or v13 w3)) w9) (or (not (or v2 w8)) w6))) (not (not (and v4 (and (and v1 v11) (or v9 v10)))))) (not (not v7))))) (and (and (and w8 w4) (not (and (not (and (or (or v20 w2) v20) (and v15 (and (and v13 v11) (not v1))))) v11))) (or (not (or (not (and v2 (or v6 (or w1 v12)))) (not (not v6)))) (and (or (or v20 (not (and (and v16 (and v14 w7)) v16))) (or (not (not v3)) v4)) (not v17)))))) (or (and (not (and (or (and (or (or (and (not v13) (or v1 v6)) (not w9)) (not (and (and (or v6 w4) (or v16 v5)) v13))) v10) (not (not (or (not (not v11)) (or (and w2 (not w1)) (and (not w1) v5)))))) (or (or (not (or (and w9 (not (and v14 w3))) (and (and v6 v6) (not (and v6 w8))))) (not (or (not (or v17 w4)) (and (and (not w8) (and w3 v3)) w1)))) (and (and w7 (not (not (and v10 v12)))) v14)))) (and (or (or (not (and (or (not (and (and v14 v7) v8)) (not w2)) (and (or (or v17 w6) (and w6 w1)) v18))) (and (not (not (not (or v7 (and v7 v9))))) (not (or (and (and (or w3 v4) (or v7 v7)) v4) (and (or w8 v2) v19))))) (not (or w8 (and (or (and (not (not v12)) (not v5)) (and (not (or v1 w3)) (and (not w6) (and v20 v9)))) (or (not (or w9 (or v15 v10))) (and (or (not v16) (not v11)) (not v19))))))) (or (not (not w2)) (or (or (not (or (or v15 (and v7 v20)) (or v11 (not (not v2))))) (or (and (and (not (and w6 v8)) v16) (and (not (or v10 w2)) (and (or v17 v10) (or w6 v20)))) (not (and v20 (and w2 w5))))) (or w2 (and w2 (and v20 v6))))))) (or (or (or (or (not (not (and v8 (or (and (and v19 v5) (or v17 v5)) v10)))) (and (and v19 v10) (or (and w8 (and v15 v10)) (not (not (and v9 v2)))))) (or (and w9 (or (or (or (and v11 (not v20)) v17) (and (not (not v9)) (not w5))) (or (and (or (and v6 v15) (and v14 v14)) v16) (not (not v20))))) (not (and (or w10 (and w7 (and w7 (or v9 w1)))) (not (or (and (not w3) w9) (or (or w9 v1) (or v4 v15)))))))) (or (or (and (not (and (not v16) (or (or w1 v4) (not (and v16 v2))))) v3) (or (and v7 (and (and v5 (or (and v11 v20) (and w6 v14))) (and (and (or v2 v5) w10) (not (or w10 w4))))) (or v7 (not (and (and (not v2) v17) (not (and v15 v20))))))) (not (or v6 (or (or v16 (and v5 (and (and w3 v7) (not v6)))) v3))))) w8)))) w7)) (and (or (and (and (and (and (and (and (not w9) (not (and v18 v4))) (or (and (not (and (or (not (not (not w1))) v1) (not (or (not v20) (not w9))))) (not (and v17 v11))) (or v12 (not (not (or (or w9 (not (and w7 w3))) w2)))))) (or (and (not (and (or (and (or (or (or v3 v10) v20) (and v5 w5)) (and v4 (not w8))) (or (or w3 w7) (or (and v8 v3) (and (or w10 v4) v9)))) (and v19 (not (not (and v3 w5)))))) v11) (not v2))) (and (and (and (not v3) (and (or (or (and (not (and (or v3 v14) (not v1))) (or v18 v3)) w10) w2) (and (and (not w8) (not w4)) (not (not w1))))) (and (and (or (or (and (or w7 v1) (or v9 (not v9))) (and (not (not (not v9))) (and v10 w1))) (and (and w6 (or (or v20 (and v13 v14)) (and w5 v9))) (and (not w5) (not (or (and w7 v11) v5))))) v5) (or w10 (or (or w4 (not (or (and w8 w7) (not (or v11 w2))))) (or (or (and (and v9 (not v2)) (and v5 (not w3))) (or w8 v17)) v15))))) (not (not w6)))) v15) (and (or (or (or (or (or (or (and (and (and (not (or w10 v5)) (and (or v10 w9) (and v12 v6))) (or (and (and v13 v17) v1) (or (or v15 v16) v10))) (or v17 (or w8 (not (not v19))))) (not (or (not v13) (not (or (or v5 v19) (and v16 w8)))))) (or (or v18 (or (and (not v9) v17) w10)) w3)) (or (not (and (or (not (not w7)) (or w2 (and (or w6 v15) v8))) (not v16))) (not (and (or (not (or (and w3 v2) v13)) (and w9 v16)) (not (and (or v7 (and w7 v17)) v18)))))) (and (and (not (or (or w1 v14) (not (or (and (or v10 v20) (and v13 v9)) (or w5 (or v12 v19)))))) (or (or (and (or (and (and v20 v1) v19) (or v9 v3)) v8) v9) v9)) (or v1 (and (and (or (and (or (not v11) (or w6 v11)) v18) (not (or (and w3 v4) v16))) w1) v4)))) (or (and (or (not w7) (not (or (and (not (and (and v15 v2) (and w2 v11))) v11) (and (not (not w8)) (and (or v12 (and v12 w6)) v2))))) (not (and (and (or w5 (and v18 (and v20 (not v11)))) (not (and (and (not v3) (or w1 v13)) (and (not v19) v15)))) w6))) (not v18))) (or (not (not (or (not (not (or v8 (and (and v16 (not v1)) (or (not v16) v11))))) v17))) (or (and (and v12 w7) (or (or (and (or (and (and w8 (or v14 v7)) v20) (and (and v15 v14) (not (or w10 v3)))) (or (or v15 w5) (or v17 w4))) (or (and (or (and v6 (not v14)) (and v15 w1)) (or v2 (and (or w8 w9) w2))) (and (and (and (and v7 v7) v17) v15) w2))) (or (not v5) (and (and w1 (and (or (or v8 w4) (or v17 v11)) (or w3 (and v16 v16)))) w10)))) (and (and (not v7) (not (and (and (or (and w1 (not v20)) (or v16 (not v16))) (or (and w5 (and v2 w7)) (or w3 (or w4 v6)))) (and (or (and (not v15) v10) (not v2)) (not (not (not w3))))))) (and (and v7 (not (and (or w4 (and (or v12 v16) v11)) (and v14 (or w10 w2))))) (and (and w8 (or (not v1) (and (or (not w2) v20) (and (not w1) (not v6))))) v7)))))) (not (and (and (or (or (and (and (or v18 w1) (not (and (not (not v18)) v5))) (or (not (or w2 (or (and v9 w8) (or v17 w2)))) v13)) (and (and (and (not (not w5)) (and (and (not w3) (and w8 w9)) v17)) (and w6 (or (or (or w4 v14) (not v20)) (not (or w8 v5))))) (or (or v11 (or (and v1 w4) v19)) (and (or (or (and w9 w2) (not v17)) v20) (and v13 (and (or v1 w9) v9)))))) v16) v5) (not (or (or (or v18 (or v4 v11)) (or (not (not (and (not (not w1)) v5))) (or (not (and (and (not v20) (and w4 v16)) (and w5 (not v3)))) (and v6 v3)))) (not (or (or v15 (or (or w10 (not (and v14 w3))) (and (and w5 (and w3 v4)) (or (not v7) v3)))) (not (not (not v4))))))))))) (or (and (or (or (and (and (and (or (not (and (not (not v7)) v15)) (not (and (or (not v6) (or (or v11 v9) w1)) (or (not (or v10 v1)) (and (or w8 v17) w2))))) (not w8)) (not (or v8 (and (not (not (not (and w9 v7)))) (and (not (not (not w1))) w9))))) (not (not (or (not (not v19)) (not v4))))) (or (and (or v16 (or (not (and (not (or v6 (and v14 v18))) (and (not v11) v18))) (not (not (and (not (not v16)) v7))))) (and (not (and (or (and v2 (not v10)) (not (or (and w1 v16) w6))) (not (and (not w7) w7)))) (and (or (or (and w3 w10) (not (or (and v19 v8) w9))) (or (and w1 (or (and v13 v15) (not w1))) (or (not v3) (and (and v19 v2) v8)))) (not (and w5 (and (or (not v16) (or w8 v12)) (or (and v20 v20) (not w7)))))))) (and (or (and (and (or (or (and (or v5 w4) v2) (and w1 w9)) (or (or (not w5) v20) w10)) w6) (or (not (or (or (or v3 w7) (or v11 w3)) v1)) (not v7))) (and (not (and (or (not (or v17 v3)) (not v4)) v9)) (or (not (or v4 (not (or w5 v9)))) v12))) (and (or w9 (and (or (and (not (not v12)) (not w3)) w5) (or v12 (not (and v6 w3))))) (and (or w1 (or (or w4 (and (or v1 v15) v3)) v8)) (not (and (and w5 (or (or v3 v20) (not w6))) (not (and (not v13) (and v11 v18)))))))))) (not (not v18))) (or (or (not (and (not (or (and (and (and (and v15 (and v15 v1)) (not w9)) w1) (not v4)) (and (or (and (not (and v13 w9)) (not (not w6))) (or w1 (and v19 v16))) (and w10 w10)))) (or w7 (not (or w6 (or (not (and w6 w8)) w1)))))) (and (or (or w10 (not (or (not (or w1 (not (not w1)))) (and w1 v1)))) (not (not (not (not (not (or (or v1 w3) v9))))))) (or (not (not (not (or (and (not v19) w2) (and (and (not w10) w6) (and (not w1) (not v18))))))) (or (and (and (and (and (not (not v18)) (and (not v12) (or w3 v17))) (or w3 (or (and v12 w3) w3))) (and (and (not (or v8 w9)) v3) (not w5))) w3) (or (and (not (not (or (and w2 v18) (and w4 v5)))) v20) v5))))) (not (not (not v6))))) (and w3 (or (and (and (not (and (or (not (and v13 (or w6 v11))) w2) (and (not w9) (and v4 v20)))) (and (not w4) v6)) (not (not (and (or v13 (or (and (not (and (and v6 v14) (or w8 w10))) (not (not v7))) v9)) (not (or (not (not (and w7 v9))) (or v17 (and v20 (and (not w5) w2))))))))) (not (and (and v13 (not (not (or (not (or (and (not v3) v14) v16)) (and (not (and (not v15) (not v18))) v17))))) (not (or v17 (or (not (not (and (or w2 (not v8)) (and (and v18 v13) (and w9 w1))))) (and (not w9) (or (not v16) v16))))))))))) (not (and (not (or (and (or (or (and (not (and (and (and (or v7 (or w4 v8)) (and (not w5) w10)) (or (not (or w2 v1)) (or v6 w3))) (not (and (and (not v13) w5) (or (not v16) (not v10)))))) v18) (not (and (or (or (and (and v2 v9) v3) (and (and (not v10) (not w10)) (not (and v11 v19)))) (or (not v18) (not (not (and w1 w7))))) (or w7 (and (or v15 v20) (and (or v14 v6) (or (and v6 v5) (not v13)))))))) (and v16 (not (not w3)))) (or (and (and v9 (and (and (and w3 (or (or v16 v12) (or (or w2 v10) v15))) (not (and v4 (or (not v13) (not w4))))) v14)) (or (not w3) (or w7 (and (or (and (and v5 (not v1)) (and v6 (or w3 w3))) (and (or v14 v7) w7)) (not (or v2 (and w2 (not v13)))))))) v19)) (not (or (or (not (not (and (and (or (and v5 (not w6)) (or (not v5) v20)) (not v17)) (and (or v13 (and (not w2) (and w6 w4))) (or (and (not v17) (and w10 v11)) w2))))) (and (and (not (not v1)) (or (or w3 (and (not (and v1 v10)) (and (or v8 v16) (not w10)))) (or (not v17) w2))) (or (or (and v5 (or (not (and w4 v20)) (not (or v9 v15)))) (and v9 (not v3))) (not (not v11))))) (not (or v20 (and v8 (not (or (or v9 (and (and w4 v6) (not v11))) (and v1 v6)))))))))) (or (not (or (or w9 (and (or (not (and v19 (and (not (or (and v11 v11) (not v13))) (and (not v1) w9)))) (and (or (or w7 (or (and v18 (not v13)) (or (not v9) (not v19)))) v5) (and (or (and v19 v12) (and w3 (or (not v11) (not v18)))) (and (not w1) v3)))) (and (or w3 (not v2)) (not (and (not (not v6)) w9))))) (or (not (and (or (not (not (not w1))) (not (or (and (not (or v3 v15)) v20) (and v3 v12)))) (or (not (or (not (and v19 (and v19 v12))) (not v4))) (or (or (or (or v19 v2) w10) (and (not w10) (or (and v4 v17) (or v6 v14)))) (not (or (and (and w3 v17) v6) (and w2 v4))))))) (or (or (or (and (and v20 (and (or (and v13 v16) v11) (not v15))) (not v12)) (or (not (and v3 v12)) (and w8 v6))) (and (not v6) (not (or (not v13) v15)))) (not (or (not (and (and (or (and w9 w4) v9) (and v18 (or w7 w7))) (or (not (or v2 v4)) (or v11 (or v9 w7))))) (or (or (or (and v18 v13) (and v18 v3)) (or (and (and v1 v3) (and v10 w5)) (and (and v19 v3) w6))) (not (not (not (not v12))))))))))) (and (not (not (not (and (or (or (or (and (and v18 v18) (not (or v12 v16))) (and (and (or v6 v8) w6) (not (or v20 v4)))) (and (not (not w1)) (not v11))) (not (not (and (and (not v20) v10) (or (and w8 v16) (and v5 v13)))))) (or (not v16) w7))))) (and (not (not v20)) (and (not (or (and v5 (not (not (and (or (or w2 v8) v18) v15)))) (and (and (or (and (or w8 w8) (not w8)) (and (and (not v18) (not v4)) (and v16 v10))) (or v4 (not (not w2)))) (not (and v12 (not (or v6 (and w5 v16)))))))) (or (or (not (and v15 (not v12))) (not v2)) (not (or (or (not (or v9 (and (not v6) v20))) v10) v13))))))))))) (and (and (not v5) (or (and (and (not (not (and (not v5) (and (not (or (and (not (not (or (or v3 w7) (not w1)))) (or (and (and w3 w6) (or (not v10) v5)) (and v5 (and (not v9) v2)))) (or (or v2 (or (and w1 v8) (or w7 v18))) (not v13)))) w6)))) (not (or (or (and (and (and (or (not w6) w10) v14) (and (and v13 (or v11 v17)) (or (and (or (or (not v17) w9) (and v11 v17)) (and v15 w2)) (and w6 (or (not v16) (and w7 (not v15))))))) (or (or (and w3 (not w9)) (and (or v19 v13) w4)) (and (or (or (or (or (not v10) w5) v13) v6) (not (and (or v10 v10) v10))) (and (and (and (and w7 (and v8 v9)) (and v10 v1)) (not (or v10 v20))) (and v8 (or (or (or w2 v19) (or v9 w5)) (or (not v4) (or v10 v6)))))))) (and (or (not (not (not (or v19 v4)))) (or (or (not (or w2 (and v12 (or v9 v11)))) w4) (not (not v16)))) (or (not (not (not w8))) (or (and (and (and (or (or v19 w2) (not v15)) w5) (or w10 (or (not v5) w7))) (or (or (not (or v19 v18)) v16) (or w1 v20))) (and (and (not v18) (and w3 (not (and w9 w4)))) (or (not (and v20 (and v13 v15))) (and (not (or v12 w3)) (not w5)))))))) (and (or (or (and (or (and (or (not (not v3)) (and (not v1) v3)) (not w7)) (not (or (and (or w10 w7) (not v19)) (and (and w1 v13) (and v8 w9))))) (and (or (or w6 v18) (not w5)) (or (not v20) v7))) (or (and (or (or (not (and v9 w4)) (or v8 w7)) v3) (not w1)) (or v9 (not (not (and (and v13 v7) (and v5 v6))))))) (or v20 (and w5 (and (or w5 (and (or (not v12) (not w10)) (and w2 (and v15 w4)))) (not (or (and (or v5 v1) v6) (or v13 (not v14)))))))) (or (not (not (and (not (or (or (and v9 w7) v10) w3)) v7))) (and (not (and (and v18 (not w7)) (not (and (or v2 (and w8 w9)) (and (and w4 v9) (or v8 v19)))))) (and (and (and (not (or v13 (and v2 v14))) (or (or v8 w6) v20)) (not (or v20 (not v20)))) (not v9)))))))) (not v13)) (or (or (not w3) (and (or (and (and (or (not (or (or (or (and v9 w7) w7) v15) (or w2 (not v1)))) (not v14)) w4) (and (not (not (or (and (or (or w9 (and v10 v15)) v19) (not (not (or v10 w2)))) (not (and v9 v17))))) (not (and (or (not (and (not w9) w10)) w7) (and (and v8 v9) (not w3)))))) (or (and w10 (not (and (or (not (not v14)) (not (not (not (not w6))))) (and (or (or (and (not v18) v11) v3) v3) (not (or (not v1) (and w7 (or v15 w4)))))))) (or (or (or (and (or (not (not (or v6 v16))) (and (not (or v2 w8)) (not v16))) (and (not (or v14 (not v18))) (or v9 (or v13 (not w9))))) (and (not (and (not (not v11)) (or (not v17) (and w3 v20)))) (not (and v18 (or v11 (and w5 v19)))))) (not (and (and (not (or v20 v14)) (not v18)) (and (and v18 (or v10 v5)) (and (and w8 w5) (not (not v8))))))) (or (not (and (or (not (or (or v17 v8) w10)) (not v11)) (or (not (or w8 (not v18))) (and (or v19 (not v10)) (or v3 (or v11 w9)))))) (not (and (not v17) v12)))))) v5)) (and (not (or (not (and (and (not (or (and (or (not w8) (and (and v12 v11) (and w4 v5))) (not (or (not w9) v4))) (not v16))) w5) (not (and (not (or (not (not (and v11 w1))) (not (not (and v14 v9))))) w3)))) w7)) (and (or (or w7 v19) (or (and (not (not (and (not (and v15 (and v10 v17))) (or (and (and v17 v7) (or (and v13 v2) (or v2 v13))) (or v3 v5))))) (or (not (not (not w2))) (and w4 (not (and v12 (or w8 (and w2 (or w3 v1)))))))) (or (and (not (or (not (or (or (or v5 v14) v19) (or v13 (or v20 v18)))) (and v2 (not (not (or v6 v2)))))) (not (or (and (or (not (and w4 w8)) v13) (or (and (not v6) w10) w2)) (and (or w5 v6) (not (not v5)))))) (or (not (not (not w10))) (or (not (not v18)) (or (or (and (or (or v11 w9) v10) w4) (not w5)) w3)))))) (or (or (not (or (or (not (not (and w3 (or (and v11 v14) v10)))) (not (or (and (and (and v9 v3) v20) (or w1 (and v9 w6))) (not (not (or v17 w6)))))) (not (or (not (not (and v2 (and v8 w9)))) (or w3 (not (not v7))))))) (not (and v16 (or (or (not w6) v1) (or (and (or (and v14 (or v18 v9)) (or (and w8 w2) (not v12))) (or (not v10) w5)) (or (or v16 (not v8)) (or v6 (or v6 v10)))))))) (and (not (or (or (not (or (and v9 (or w9 (not v2))) (or (not v12) (not (not v3))))) (or w5 (and w7 v12))) (or (and (not (and (not (and v12 w7)) (and w2 v11))) (or (not (or (and v1 v9) (or w2 w4))) (and (and w2 (and w5 v8)) (not (or v6 v7))))) (not v5)))) (and (not (or (not v7) (and (or (or w6 w5) (or (not (and v15 w2)) w6)) (and (not (or (not v17) (not w10))) (not (not (and v9 w2))))))) (not v3))))))))) v12))))
(or (or (not (or (not v8) (or (not (and (and (and (not v2) w9) (not (or (or (or v19 w1) (and v7 (and (and (not v17) v6) (or v5 v9)))) v10))) (not (and (and v5 w4) v9)))) (or (or (or (or v1 (or (and (or v4 v9) (and (and (or w4 (not w6)) (and w8 (not w10))) w3)) (and v5 (or v6 w2)))) (and v13 (and v20 (and (or (and v18 v4) w7) v5)))) (or (or (or v3 (and (or v15 (or (not v13) v5)) (not (and v12 w4)))) (not (or (or v18 (and v16 v14)) (not v13)))) (not v11))) (not (and w2 (and (not (or (not (or v6 v5)) v18)) (or (or (or (and v7 v14) w3) (not (and (or (or w8 v16) w10) (or v16 (and w4 v15))))) (not (or (not v15) (or (and v12 (or v17 v4)) v6))))))))))) (and (not (or (or (and (and (or v8 (and v6 (and (or (not w6) (and v19 (or (not (and v4 (not v17))) (and (not v14) w3)))) (and (and (not v16) (or w9 v17)) (not (and v17 (not w10))))))) (and v7 (and v20 (not (and v5 (or (or v13 v6) (not (and (and v14 (not v19)) v12)))))))) (or (or (and w8 v6) (not (and v11 (and (or (or (or v10 w10) (and v19 v18)) v4) (not (or (or w7 v1) (or v14 v3))))))) (or (not (and (not (or w3 (and w4 w9))) w1)) v16))) (not v15)) (or (and v13 (or (and (or (or (not v19) (or (and (or (or v11 v12) w8) (and (not (or (not v2) v3)) (or v4 (or (or w2 w10) w7)))) v16)) (not (or v20 (and v8 v2)))) v10) (and v11 (and w10 (or v18 v9))))) (or (or (and v7 v11) (or (and (not (and (not (or (or (and v12 v5) v7) (and w7 (or w8 v4)))) w3)) (and (and (not (and w9 (not (or w5 v8)))) (or (or (not (or (and v5 v9) w1)) (or (and w9 (and w1 v11)) (and v16 (not w10)))) (not (and (and v20 v3) v4)))) (not (or (or (or v10 (and (or w2 (and w7 w1)) (and v20 v16))) v18) (not v2))))) (and (not (and (not (and w10 (or (or v4 v13) v20))) (and (and w1 (or (and v7 v9) (and v14 w2))) (and w3 (or v3 w9))))) (or (or (and v6 (not w10)) (not v3)) (not (or (and v20 (not (and w7 w4))) w1)))))) (or (or (and (or (and (or w3 (or (or (and (and (and w1 v7) v6) (not v4)) v5) (and (or (and v6 w8) w7) (not (or v16 (and w2 (not v10))))))) (or (and (not w5) (and w4 (and w7 (not v16)))) (not (or (or (or (and (and w1 v12) (and v4 w10)) v14) (or (or v16 w4) (and v12 v7))) (not (and v9 w2)))))) (or (and (not (and (not (and (or v13 (and w2 v5)) (or v18 w3))) (or w10 (or (and w1 v17) v16)))) (and v12 (and (and (not (and v19 v11)) v6) (and (not (and v16 v13)) w8)))) (not (and (or (or (or w8 v10) v3) w3) (or (or w1 (or w3 w10)) (or (or (not v11) w9) v16)))))) (not (and (or (or w1 (not (and (and v7 w7) (or (and w10 v9) v10)))) (and w4 (not (and (not v2) v18)))) (and (and (and (or (or v19 (or w9 v11)) w3) (not (and v4 (and w7 v6)))) v12) (or (or (not v17) w9) (or (not (and v11 w7)) w4)))))) (not (and (or v5 (not (or (or v4 (not (and v20 (not (or v16 v11))))) (not (and (not v14) v12))))) w6))) v1))))) (or (or (and (or (not (or (or (or (not (or v7 (and (not w8) v18))) (or (not v9) (or v2 (not (or (or v19 v18) v10))))) (not (or (and (not v3) v10) (and (and v14 (and v6 v13)) (not w5))))) (not (or v7 (and (or v20 v12) (not v18)))))) (or (not (or (not (or (not w7) v6)) (or (or w8 (not (and w10 (not v16)))) (not (and w1 (and v19 v2)))))) (and (and w8 v2) v20))) (or (and (and w5 (not (or (or v3 w7) (not w8)))) w2) (not w1))) (or (or (not (and (not (and v7 (not (and v13 w10)))) (or (or (and (and (or (or (not w5) v3) v6) (not v14)) (or (and w8 w1) (and (or w2 (not v7)) (not w7)))) (or (not v12) w10)) (and (or v13 v19) (not (or w7 v18)))))) (and v14 (not (or (and (and w2 v7) (not v12)) v19)))) (or (or (or (or (not v17) v8) (or (or (not v5) v4) w9)) (or (or (not w4) (or w3 (and w10 v9))) (not v11))) (and (and (or v7 w7) (not v10)) w10)))) v3))) (or (and (not (and (and (or (or (and v12 v1) (or (not v4) (or (not v19) w3))) (and (not (and (or (or (not v18) (or (and v11 w10) v10)) (and (or w7 (not v2)) (or v8 w5))) w1)) (or (and (or (not w10) v2) (not w9)) (or (not (and (and v15 v6) (and w4 (not v12)))) (or (or v3 (not w6)) v9))))) (or (and v20 w6) (and (not (or (and (and v11 v9) (or v3 w8)) (and (not (and v17 (or (not v2) v6))) v13))) (and v16 (or v18 (not w4)))))) (and (and (and (or (not v11) (and (or (or (or (or (not w8) v2) (or v15 (or w3 v4))) w10) (not (or v7 v10))) (or (or (and v19 v6) (not v7)) (or (or w1 (not v12)) (or v4 w4))))) (or (or w8 (or (and (not w7) v5) (not (and v13 (and w5 v7))))) (not (and v16 (or w2 (and w3 w6)))))) (or (and v15 (and (and (and v8 (not (and v3 (not v18)))) (or (not v5) (or (not v2) (and (or v17 v20) w2)))) (and (and w1 (not v1)) (not (or w6 v6))))) (not (and (and (or v15 (and (not (and v14 v20)) v8)) (and (and (not (and v3 v8)) (or v7 (not v4))) (not (or (not w8) v9)))) (or (and (and v2 (not (or w2 (and (not w4) v13)))) (and (or v11 (not w1)) w3)) (or (or (not v8) (and v14 (and v15 v17))) (and w9 w2))))))) (or (not v18) (or (or (or (and (not (or (or (and (and (and w7 v12) w10) (not w4)) (not (or v11 (or w7 w10)))) v3)) v10) (not w3)) (and (not (or w5 (and v16 (not v5)))) (or (and (not v3) (or (and w9 v12) (and (or w6 v12) v10))) w7))) (or (not (or (or (or w10 w2) (or v15 v1)) (not (or v19 v9)))) (or v3 (not (and (and v10 v20) v7))))))))) (or (or (and (not (or (not (or w3 (and v1 v10))) (and v13 (and (or v16 (not v11)) v7)))) (or (not (and v12 (or (not (or w3 w7)) (and v15 (and (or w2 w5) v17))))) (and (not (or (or (or (and w10 v9) (not (or v7 v15))) (and (not (or v17 v15)) v8)) (or v2 (not (and (or v16 w6) (or v5 w1)))))) (or (not (or v14 (not v9))) (or (or v19 w3) (and v3 w5)))))) (not (and (or (or w3 (not (and w7 v7))) (and (and w1 v17) (or (or (not (or (not v4) w4)) v3) (or (not (and v19 (and (not v15) (and (or v20 v12) v8)))) (or w6 v2))))) (not (and (and v20 (and (not (or v12 w7)) (or (not (or (or v4 (not v17)) (or v8 (and v3 (not v14))))) (or v1 w3)))) v15))))) (not w9))) (or (and (or (and (and (not (or (or (and (and (and (not w3) w8) v18) (not v20)) (and (and w6 w8) v4)) (or (and (not v1) (or w4 (not v15))) (or w9 v16)))) (and v17 (and (or (and (not (and v1 v7)) v2) (and w6 w1)) (or w3 w10)))) v3) (or (and (and (not v18) (or (and (or (or (and v13 (not (and w8 v16))) (and (not (or v10 v2)) v7)) w3) (not w2)) (or v1 (or w10 v3)))) (and (not (or w5 (or (or (or v9 v10) v13) (and v8 (and (and v16 v7) (not v6)))))) w10)) w7)) (and (or (and (and (and (and (not (or w9 (and v18 v4))) (or (not (and v17 v11)) (or v12 (or (not (and w7 w3)) w2)))) (or v11 (not v2))) (and (and (and (not v3) (and (or (or (and (not (and v14 (not v1))) v18) w10) w2) (and (not (or w8 w4)) w1))) (and (or (or w7 v1) (and (not v9) v10)) v5)) w6)) v15) (or (and (or (or (and (not (or (or (and (and v7 v15) (and (or (not v6) (or (or v11 v9) w1)) (or (not (or v10 v1)) (and v17 w2)))) w8) (or v8 (and (not v7) (and (not w1) w9))))) (or v19 (not v4))) (or (and (not (or (and v2 (not v10)) (not (or (and w1 v16) w6)))) (and (or (or (and w3 w10) (not (or (and v19 v8) w9))) (or (and w1 (and v13 v15)) (or (not v3) (and (and v19 v2) v8)))) (not (and w5 (and (or (not v16) (or w8 v12)) (or v20 (not w7))))))) (and (or (and (and (or (or (and (or v5 w4) v2) (and w1 w9)) (or (or (not w5) v20) w10)) w6) (not (and (or (or (or v3 w7) (or v11 w3)) v1) v7))) (and (not (and (not (and (or v17 v3) v4)) v9)) (or (not (or v4 (not (or w5 v9)))) v12))) (and (or w9 (and (or (and v12 (not w3)) w5) (or v12 (not (and v6 w3))))) (and (or w1 (or (or w4 (and (or v1 v15) v3)) v8)) (not (and w5 (or (or v3 v20) (not w6))))))))) v18) (or (or (not (and (not (or (and (and (and (and v15 v1) (not w9)) w1) (not v4)) (and (or (and (not (and v13 w9)) w6) (or w1 (and v19 v16))) w10))) w7)) (and (or (or w10 (not (or (not w1) v1))) (not (or (or v1 w3) v9))) (or (not (or (and (not v19) w2) (and (and (not w10) w6) (not (or w1 v18))))) (or (and (and (and v18 (not v12)) w3) (and (and (not (or v8 w9)) v3) (not w5))) (or (and (and w2 v18) v20) v5))))) (not v6))) (and w3 (or (and (and (not w4) v6) (not (or (and w7 v9) (and v20 (and (not w5) w2))))) (not (and (and v13 (or (not (or (and (not v3) v14) v16)) (and (or v15 v18) v17))) (not (or v17 (or (and (or w2 (not v8)) (and v18 w1)) (not w9)))))))))) (not (and (not (or (and (or (or (and (not (and (and (or v7 (or w4 v8)) (and (not w5) w10)) (or (not (or w2 v1)) (or v6 w3)))) v18) (not (and (or (or (and (and v2 v9) v3) (not (or (or v10 w10) (and v11 v19)))) (or (not v18) (and w1 w7))) (or w7 (and (or v15 v20) (and (or v14 v6) (or (and v6 v5) (not v13)))))))) (and v16 w3)) (or (and (and v9 (and (and (and w3 (or (or v16 v12) (or (or w2 v10) v15))) (not (and v4 (not (and v13 w4))))) v14)) (or w7 (and (and (and v5 (not v1)) v6) (not (or v2 (and w2 (not v13))))))) v19)) (not (or (or (and (and (or (not w6) (or (not v5) v20)) (not v17)) (and (or v13 (and (not w2) (and w6 w4))) (or (and w10 v11) w2))) (and (and v1 (or (or w3 (and (not v10) (and (or v8 v16) (not w10)))) (or (not v17) w2))) (or (or (and v5 (not (and (and w4 v20) (or v9 v15)))) (and v9 (not v3))) v11))) (not (or v20 (and v8 (not (or (or v9 (and (and w4 v6) (not v11))) (and v1 v6)))))))))) (or (not (or (or w9 (or w3 (not v2))) (or w1 (or (or (not (and v3 v12)) (and w8 v6)) (not (or v6 (or (not v13) v15))))))) (and (not (and (or (and v18 (not (or v12 v16))) (and w1 (not v11))) (or (not v16) w7))) (and v20 (not (or (or (and v5 (and (or (or w2 v8) v18) v15)) (and (and (and (not (or v18 v4)) (and v16 v10)) w2) (not (and v12 (not (or v6 w5)))))) (and (and (and v15 (not v12)) v2) (or (or (not (or v9 (not v6))) v10) v13))))))))))) (and (not (or v5 (and w3 (or (or (not (and (and (and (or w8 (or (not w9) v4)) v16) w5) (or (and v11 w1) (and v14 v9)))) w7) (or (or (and v11 v14) v10) (not (or (and (and (and v9 v3) v20) w1) (or v17 w6)))))))) v12))))