c SATISFIABLE: No goal function specified. s SATISFIABLE c CPU time : 0.364944 s c decisions : 48926 (134064 /sec)