c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 0.419936 s
c decisions             : 26287          (62598 /sec)