c SATISFIABLE: No goal function specified. s SATISFIABLE c CPU time : 0.747886 s c decisions : 84470 (112945 /sec)