c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 1846.9 s
c decisions             : 29099396       (15756 /sec)