c SATISFIABLE: No goal function specified. s SATISFIABLE c CPU time : 1.02284 s c decisions : 4384 (4286 /sec)