# Pastebin B6jfU8Vn
Solving problem with 1233925 variables and 3262769 clauses..
Interrupted SAT solver: TIMEOUT!

        _____  _  _      _____ ____  _     _____
       /__ __\/ \/ \__/|/  __//  _ \/ \ /\/__ __\
         / \  | || |\/|||  \  | / \|| | ||  / \
         | |  | || |  |||  /_ | \_/|| \_/|  | |
         \_/  \_/\_/  \|\____\\____/\____/  \_/