(and
  (or P10 (not P8) (not P2))
  (or P2 P10 P8)
  (or P35 P23 (not P38))
  (or P33 (not P30) P37)
  (or (not P12) P53 P50)
  (or (not P22) P51 P19)
  (or (not P49) P5 P27)
  (or P12 P53 (not P50))
  (or (not P3) (not P27) P41)
  (or P7 (not P42) (not P18))
  (or P21 (not P32) (not P42))
  (or P31 (not P13) P39)
  (or P3 (not P27) (not P41))
  (or (not P23) (not P32) P50)
  (or (not P45) P37 (not P14))
  (or P38 (not P23) P35)
  (or P32 (not P21) (not P42))
  (or (not P46) P20 P57)
  (or P26 P22 P30)
  (or P37 P30 (not P33))
  (or P20 (not P56) P29)
  (or (not P49) (not P27) (not P5))
  (or (not P40) P25 (not P54))
  (or (not P22) P26 (not P30))
  (or (not P60) (not P58) P52)
  (or (not P43) (not P11) (not P21))
  (or P58 (not P17) (not P44))
  (or (not P47) P3 P46)
  (or P14 P45 P37)
  (or (not P60) (not P52) P58)
  (or P49 (not P5) P27)
  (or P21 (not P43) P11)
  (or (not P45) P25 P10)
  (or (not P57) P16 P49)
  (or (not P54) (not P25) P40)
  (or P40 (not P12) P59)
  (or P56 P18 (not P9))
  (or P27 P3 P41)
  (or P39 (not P31) P13)
  (or (not P17) P44 (not P58))
  (or P44 P58 P17)
  (or P52 P60 P58)
  (or (not P39) (not P36) (not P55))
  (or (not P4) (not P51) P7)
  (or P5 P17 (not P26))
  (or P4 P7 P51)
  (or (not P24) (not P14) P52)
  (or (not P38) (not P35) (not P23))
  (or (not P44) P28 (not P19))
  (or P47 P46 (not P3))
  (or (not P53) (not P1) P6)
  (or (not P30) P22 (not P26))
  (or (not P8) P28 (not P13))
  (or P33 (not P37) P30)
  (or P23 (not P35) P38)
  (or P23 (not P50) (not P32))
  (or (not P59) (not P12) (not P40))
  (or (not P39) (not P13) (not P31))
  (or P21 P43 (not P11))
  (or P2 (not P10) (not P8))
  (or P20 P56 (not P29))
  (or P19 (not P51) P22)
  (or P50 P32 P23)
  (or (not P51) (not P22) (not P19))
  (or P12 P40 (not P59))
  (or (not P57) (not P16) (not P49))
  (or P29 (not P20) P56)
  (or P36 (not P55) P39)
  (or P48 (not P38) P2)
  (or P38 P2 (not P48))
  (or (not P52) P60 (not P58))
  (or (not P5) (not P26) (not P17))
  (or P8 P28 P13)
  (or (not P36) P24 (not P9))
  (or (not P51) P4 (not P7))
  (or (not P28) P19 (not P44))
  (or P1 (not P4) (not P29))
  (or P18 (not P7) (not P42))
  (or P47 P60 P55)
  (or P43 P16 (not P35))
  (or P18 P7 P42)
  (or P34 (not P6) (not P15))
  (or P60 (not P47) (not P55))
  (or (not P47) (not P46) (not P3))
  (or P29 P1 P4)
  (or (not P9) (not P24) P36)
  (or P55 (not P60) (not P47))
  (or (not P16) (not P43) (not P35))
  (or P39 (not P36) P55)
  (or P17 (not P44) (not P58))
  (or P15 (not P6) (not P34))
  (or (not P2) P8 (not P10))
  (or P13 (not P8) (not P28))
  (or P14 (not P52) (not P24))
  (or (not P21) P43 P11)
  (or (not P4) P29 (not P1))
  (or P4 (not P1) (not P29))
  (or (not P46) P47 P3)
  (or P26 P5 (not P17))
  (or P16 P57 (not P49))
  (or (not P56) (not P9) (not P18))
  (or (not P15) (not P34) P6)
  (or P26 (not P5) P17)
  (or P57 (not P20) P46)
  (or P25 (not P10) P45)
  (or P48 (not P34) P31)
  (or P9 (not P56) P18)
  (or P11 (not P33) (not P54))
  (or (not P26) P30 (not P22))
  (or (not P25) P10 P45)
  (or P49 P57 (not P16))
  (or P59 P41 P15)
  (or (not P41) (not P59) P15)
  (or P14 (not P45) (not P37))
  (or (not P1) P53 (not P6))
  (or (not P6) (not P53) P1)
  (or (not P28) P8 (not P13))
  (or (not P31) (not P48) (not P34))
  (or P49 P5 (not P27))
  (or P31 (not P48) P34)
  (or (not P7) (not P4) P51)
  (or (not P31) P34 P48)
  (or (not P24) (not P36) P9)
  (or (not P14) (not P52) P24)
  (or P46 (not P57) P20)
  (or P38 (not P2) P48)
  (or P19 P44 P28)
  (or (not P57) (not P20) (not P46))
  (or P31 (not P39) P13)
  (or (not P33) (not P11) P54)
  (or P54 (not P40) (not P25))
  (or (not P19) (not P28) P44)
  (or (not P60) (not P55) P47)
  (or P6 P53 P1)
  (or P25 P40 P54)
  (or P14 P52 P24)
  (or (not P20) (not P56) (not P29))
  (or P55 (not P39) P36)
  (or P21 P42 P32)
  (or P16 (not P43) P35)
  (or P9 P36 P24)
  (or P6 P15 P34)
  (or (not P50) P32 (not P23))
  (or (not P41) (not P3) P27)
  (or P59 (not P41) (not P15))
  (or P56 P9 (not P18))
  (or (not P45) (not P25) (not P10))
  (or P22 (not P19) P51)
  (or (not P30) (not P33) (not P37))
  (or (not P38) (not P48) (not P2))
  (or P59 (not P40) P12)
  (or (not P50) (not P53) (not P12))
  (or P11 P33 P54)
  (or (not P54) (not P11) P33)
  (or P41 (not P59) (not P15))
  (or (not P7) (not P18) P42)
  (or (not P14) P45 (not P37))
  (or P42 (not P32) (not P21))
  (or P43 (not P16) P35)
  (or P12 P50 (not P53)))