c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 134.452 s
c decisions             : 3758611        (27955 /sec)