Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
  1. LAUNCHER DATA
    These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. WATCHER DATA
    This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
    Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
    When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
  4. VERIFIER DATA
    The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.

General information on the benchmark

Namesubmitted/manquinho/routing/normalized-s4-4-3-3pb.opb
MD5SUMc267b57d74142f6538ad16680277f9bf
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 62
Optimality of the best value was proved YES
Number of terms in the objective function 648
Biggest coefficient in the objective function 1
Number of bits for the biggest coefficient in the objective function 1
Sum of the numbers in the objective function 648
Number of bits of the sum of numbers in the objective function 10
Biggest number in a constraint 3
Number of bits of the biggest number in a constraint 2
Biggest sum of numbers in a constraint 648
Number of bits of the biggest sum of numbers10
Best result obtained on this benchmarkOPTIMUM FOUND
Best CPU time to get the best result obtained on this benchmark24.9102
Number of variables648
Total number of constraints1954
Number of constraints which are clauses1930
Number of constraints which are cardinality constraints (but not clauses)24
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint2
Maximum length of a constraint27

Trace number 2179

Launcher Data

LAUNCH ON wulflinc8 THE 2005-09-18 18:07:20 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2582 boxname=wulflinc8 idbench=238 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c267b57d74142f6538ad16680277f9bf  /oldhome/oroussel/tmp/wulflinc8/normalized-s4-4-3-3pb.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc8/normalized-s4-4-3-3pb.opb
IDLAUNCH: 2582
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        918860 kB
Buffers:         34832 kB
Cached:          56448 kB
SwapCached:        792 kB
Active:          67324 kB
Inactive:        26624 kB
HighTotal:      131008 kB
HighFree:        70728 kB
LowTotal:       903652 kB
LowFree:        848132 kB
SwapTotal:     2097136 kB
SwapFree:      2095876 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5752 kB
Slab:            16244 kB
Committed_AS:    64132 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 18:18:36 (client local time) WITH STATUS 30 IN 675.657 SECONDS
stats: 2582 0 675.657 30

Solver Data

c Parsing PB file...
c Converting 1954 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ############################################################################################################
c   -- Clauses(.)/Splits(s): ..................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[1944]---> BDD-cost:    1
c ---[1934]---> BDD-cost:    1
c ---[1885]---> BDD-cost:    1
c ---[1883]---> BDD-cost:    1
c ---[1869]---> BDD-cost:    1
c ---[1843]---> BDD-cost:    1
c ---[1821]---> BDD-cost:    1
c ---[1811]---> BDD-cost:    1
c ---[1778]---> BDD-cost:    1
c ---[1752]---> BDD-cost:    1
c ---[1750]---> BDD-cost:    1
c ---[1740]---> BDD-cost:    1
c ---[1726]---> BDD-cost:    1
c ---[1700]---> BDD-cost:    1
c ---[1678]---> BDD-cost:    1
c ---[1668]---> BDD-cost:    1
c ---[1654]---> BDD-cost:    1
c ---[1628]---> BDD-cost:    1
c ---[1606]---> BDD-cost:    1
c ---[1596]---> BDD-cost:    1
c ---[1594]---> BDD-cost:    1
c ---[1568]---> BDD-cost:    1
c ---[1550]---> BDD-cost:    1
c ---[1525]---> BDD-cost:    1
c ---[1507]---> BDD-cost:    1
c ---[1485]---> BDD-cost:    1
c ---[1459]---> BDD-cost:    1
c ---[1453]---> BDD-cost:    1
c ---[1435]---> BDD-cost:    1
c ---[1413]---> BDD-cost:    1
c ---[1387]---> BDD-cost:    1
c ---[1381]---> BDD-cost:    1
c ---[1333]---> BDD-cost:    1
c ---[1323]---> BDD-cost:    1
c ---[1313]---> BDD-cost:    1
c ---[1311]---> BDD-cost:    1
c ---[1258]---> BDD-cost:    1
c ---[1248]---> BDD-cost:    1
c ---[1242]---> BDD-cost:    1
c ---[1240]---> BDD-cost:    1
c ---[1203]---> BDD-cost:    1
c ---[1181]---> BDD-cost:    1
c ---[1175]---> BDD-cost:    1
c ---[1169]---> BDD-cost:    1
c ---[1167]---> BDD-cost:    1
c ---[1141]---> BDD-cost:    1
c ---[1123]---> BDD-cost:    1
c ---[1097]---> BDD-cost:    1
c ---[1060]---> BDD-cost:    1
c ---[1038]---> BDD-cost:    1
c ---[1032]---> BDD-cost:    1
c ---[1026]---> BDD-cost:    1
c ---[1024]---> BDD-cost:    1
c ---[ 998]---> BDD-cost:    1
c ---[ 980]---> BDD-cost:    1
c ---[ 954]---> BDD-cost:    1
c ---[ 952]---> BDD-cost:    1
c ---[ 926]---> BDD-cost:    1
c ---[ 908]---> BDD-cost:    1
c ---[ 882]---> BDD-cost:    1
c ---[ 868]---> BDD-cost:    1
c ---[ 842]---> BDD-cost:    1
c ---[ 820]---> BDD-cost:    1
c ---[ 810]---> BDD-cost:    1
c ---[ 792]---> BDD-cost:    1
c ---[ 771]---> BDD-cost:    1
c ---[ 745]---> BDD-cost:    1
c ---[ 739]---> BDD-cost:    1
c ---[ 722]---> BDD-cost:    1
c ---[ 700]---> BDD-cost:    1
c ---[ 674]---> BDD-cost:    1
c ---[ 668]---> BDD-cost:    1
c ---[ 658]---> BDD-cost:    1
c ---[ 648]---> BDD-cost:    1
c ---[ 598]---> BDD-cost:    1
c ---[ 596]---> BDD-cost:    1
c ---[ 586]---> BDD-cost:    1
c ---[ 576]---> BDD-cost:    1
c ---[ 526]---> BDD-cost:    1
c ---[ 524]---> BDD-cost:    1
c ---[ 487]---> BDD-cost:    1
c ---[ 465]---> BDD-cost:    1
c ---[ 459]---> BDD-cost:    1
c ---[ 453]---> BDD-cost:    1
c ---[ 400]---> BDD-cost:    1
c ---[ 390]---> BDD-cost:    1
c ---[ 384]---> BDD-cost:    1
c ---[ 382]---> BDD-cost:    1
c ---[ 372]---> BDD-cost:    1
c ---[ 362]---> BDD-cost:    1
c ---[ 312]---> BDD-cost:    1
c ---[ 310]---> BDD-cost:    1
c ---[ 304]---> BDD-cost:    1
c ---[ 286]---> BDD-cost:    1
c ---[ 248]---> BDD-cost:    1
c ---[ 238]---> BDD-cost:    1
c ---[ 236]---> BDD-cost:    1
c ---[ 210]---> BDD-cost:    1
c ---[ 192]---> BDD-cost:    1
c ---[ 166]---> BDD-cost:    1
c ---[ 129]---> BDD-cost:    1
c ---[ 107]---> BDD-cost:    1
c ---[ 101]---> BDD-cost:    1
c ---[  95]---> BDD-cost:    1
c ---[  62]---> BDD-cost:    1
c ---[  36]---> BDD-cost:    1
c ---[  34]---> BDD-cost:    1
c ---[  24]---> BDD-cost:    1
c ---[  23]---> BDD-cost:   95
c ---[  22]---> BDD-cost:   95
c ---[  21]---> BDD-cost:   95
c ---[  20]---> BDD-cost:   95
c ---[  19]---> BDD-cost:   95
c ---[  18]---> BDD-cost:   95
c ---[  17]---> BDD-cost:   95
c ---[  16]---> BDD-cost:   95
c ---[  15]---> BDD-cost:   95
c ---[  14]---> BDD-cost:   95
c ---[  13]---> BDD-cost:   95
c ---[  12]---> BDD-cost:   95
c ---[  11]---> BDD-cost:   95
c ---[  10]---> BDD-cost:   95
c ---[   9]---> BDD-cost:   95
c ---[   8]---> BDD-cost:   95
c ---[   7]---> BDD-cost:   95
c ---[   6]---> BDD-cost:   95
c ---[   5]---> BDD-cost:   95
c ---[   4]---> BDD-cost:   95
c ---[   3]---> BDD-cost:   95
c ---[   2]---> BDD-cost:   95
c ---[   1]---> BDD-cost:   95
c ---[   0]---> BDD-cost:   95
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    8074    23340 |    2691       0        0     nan |  0.000 % |
c |       102 |    8074    23340 |    2960     102     1442    14.1 |  4.348 % |
c |       252 |    8074    23340 |    3256     252     3799    15.1 |  4.348 % |
c |       480 |    8074    23340 |    3581     480     7765    16.2 |  4.348 % |
c |       817 |    8074    23340 |    3939     817    16005    19.6 |  4.348 % |
c |      1329 |    8074    23340 |    4333    1329    40635    30.6 |  4.348 % |
c |      2090 |    8074    23340 |    4767    2090    66094    31.6 |  4.348 % |
c |      3230 |    8074    23340 |    5243    3230   138206    42.8 |  4.348 % |
c |      4938 |    8074    23340 |    5768    4938   177073    35.9 |  4.348 % |
c |      7502 |    8074    23340 |    6345    4091   151590    37.1 |  4.348 % |
c |     11347 |    8074    23340 |    6979    4497   120713    26.8 |  4.348 % |
c |     17113 |    8074    23340 |    7677    6583   255623    38.8 |  4.348 % |
c |     25763 |    8074    23340 |    8445    6746   282069    41.8 |  4.348 % |
c |     38738 |    8074    23340 |    9290    6392   297596    46.6 |  4.348 % |
c |     58199 |    8074    23340 |   10219    6507   176077    27.1 |  4.348 % |
c |     87395 |    8074    23340 |   11240    9317   321418    34.5 |  4.348 % |
c ==============================================================================
c Found solution: 70
c ---[   0]---> Sorter-cost:29320     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    113284 |   41944   102393 |   13981    6209   195155    31.4 |  4.348 % |
c |    113385 |   41944   102393 |   15379    6310   198132    31.4 |  0.570 % |
c |    113535 |   41944   102393 |   16917    6460   203849    31.6 |  0.570 % |
c |    113760 |   41944   102393 |   18608    6685   211502    31.6 |  0.570 % |
c |    114099 |   41944   102393 |   20469    7024   220570    31.4 |  0.570 % |
c |    114608 |   41944   102393 |   22516    7533   236489    31.4 |  0.570 % |
c |    115367 |   41932   102369 |   24768    8291   259897    31.3 |  0.593 % |
c |    116506 |   41932   102369 |   27245    9430   299512    31.8 |  0.593 % |
c |    118214 |   41932   102369 |   29969   11138   349483    31.4 |  0.593 % |
c |    120778 |   41907   102318 |   32966   13701   452146    33.0 |  0.645 % |
c |    124622 |   41882   102267 |   36263   17544   571773    32.6 |  0.696 % |
c |    130390 |   41882   102267 |   39889   23312   778542    33.4 |  0.696 % |
c ==============================================================================
c Found solution: 68
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    138293 |   41801   102101 |   13933   31214  1065607    34.1 |  0.696 % |
c |    138394 |   41801   102101 |   15326   13484   424371    31.5 |  0.981 % |
c |    138544 |   41801   102101 |   16858   13634   429467    31.5 |  0.981 % |
c |    138769 |   41801   102101 |   18544   13859   433478    31.3 |  0.981 % |
c |    139111 |   41801   102101 |   20399   14201   441685    31.1 |  0.981 % |
c |    139620 |   41801   102101 |   22439   14710   462914    31.5 |  0.981 % |
c |    140381 |   41801   102101 |   24683   15471   490629    31.7 |  0.981 % |
c |    141522 |   41801   102101 |   27151   16612   519133    31.3 |  0.981 % |
c |    143233 |   41801   102101 |   29866   18323   574634    31.4 |  0.981 % |
c |    145801 |   41801   102101 |   32853   20891   660751    31.6 |  0.981 % |
c |    149646 |   41781   102061 |   36138   24735   760512    30.7 |  1.016 % |
c |    155412 |   41781   102061 |   39752   30501   878079    28.8 |  1.016 % |
c |    164061 |   41717   101929 |   43727   39147  1079879    27.6 |  1.143 % |
c |    177036 |   41617   101718 |   48100   22012   483097    21.9 |  1.360 % |
c |    196498 |   41587   101652 |   52910   41473   845150    20.4 |  1.431 % |
c |    225690 |   41542   101559 |   58201   31944   814601    25.5 |  1.518 % |
c |    269481 |   41542   101559 |   64021   32065  1137175    35.5 |  1.518 % |
c |    335165 |   41467   101400 |   70423   49247  1388238    28.2 |  1.684 % |
c |    433692 |   41083   100562 |   77466   38900   776606    20.0 |  2.574 % |
c ==============================================================================
c Found solution: 66
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    525778 |   41062   100523 |   13687   68345  1212971    17.7 |  2.574 % |
c |    525880 |   41062   100523 |   15055    7974   140769    17.7 |  2.691 % |
c |    526032 |   41062   100523 |   16561    8126   143870    17.7 |  2.691 % |
c |    526259 |   41062   100523 |   18217    8353   147844    17.7 |  2.691 % |
c |    526597 |   41062   100523 |   20039    8691   153752    17.7 |  2.691 % |
c |    527103 |   41062   100523 |   22043    9197   162601    17.7 |  2.691 % |
c |    527864 |   41062   100523 |   24247    9958   173677    17.4 |  2.691 % |
c |    529003 |   41062   100523 |   26672   11097   189986    17.1 |  2.691 % |
c |    530712 |   41062   100523 |   29339   12806   217213    17.0 |  2.691 % |
c |    533275 |   41062   100523 |   32273   15369   256491    16.7 |  2.691 % |
c |    537120 |   41062   100523 |   35500   19214   336697    17.5 |  2.691 % |
c |    542888 |   41062   100523 |   39050   24982   429208    17.2 |  2.691 % |
c |    551539 |   41062   100523 |   42955   33633   567257    16.9 |  2.691 % |
c |    564513 |   40100    98410 |   47251   16373   365874    22.3 |  4.936 % |
c ==============================================================================
c Found solution: 64
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    565714 |   37929    93431 |   12643   17486   386189    22.1 |  4.936 % |
c ==============================================================================
c Found solution: 62
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    565806 |   37880    93314 |   12626    8831   186716    21.1 |  4.936 % |
c ==============================================================================
c Optimal solution: 62
s OPTIMUM FOUND
v -v1 -v2 -v3 -v4 -v5 -v6 -v7 -v8 v9 -v10 -v11 -v12 -v13 -v14 -v15 -v16 -v17 -v18 -v19 v20 -v21 -v22 -v23 -v24 -v25 -v26 -v27 -v28 -v29 -v30 -v31 -v32 -v33 v34 v35 -v36 -v37 -v38 v39 -v40 -v41 -v42 v43 -v44 -v45 -v46 v47 -v48 -v49 -v50 -v51 -v52 -v53 -v54 -v55 -v56 -v57 -v58 -v59 -v60 -v61 -v62 v63 -v64 -v65 -v66 v67 -v68 -v69 -v70 -v71 -v72 -v73 -v74 -v75 -v76 -v77 -v78 -v79 -v80 -v81 -v82 -v83 v84 -v85 -v86 -v87 -v88 -v89 -v90 -v91 v92 -v93 -v94 -v95 v96 -v97 -v98 -v99 -v100 v101 -v102 -v103 -v104 -v105 -v106 -v107 -v108 -v109 v110 -v111 -v112 -v113 -v114 v115 -v116 -v117 -v118 v119 -v120 v121 -v122 -v123 -v124 -v125 -v126 -v127 v128 -v129 -v130 -v131 -v132 -v133 v134 -v135 -v136 -v137 v138 -v139 -v140 -v141 -v142 -v143 -v144 -v145 -v146 -v147 -v148 -v149 -v150 -v151 -v152 -v153 v154 -v155 -v156 -v157 -v158 -v159 -v160 -v161 -v162 -v163 -v164 -v165 -v166 -v167 -v168 -v169 -v170 -v171 -v172 -v173 -v174 -v175 -v176 -v177 v178 -v179 -v180 -v181 -v182 -v183 -v184 v185 -v186 -v187 -v188 v189 -v190 -v191 -v192 -v193 -v194 -v195 -v196 v197 -v198 -v199 -v200 -v201 -v202 -v203 -v204 -v205 -v206 -v207 -v208 -v209 v210 -v211 -v212 -v213 -v214 -v215 -v216 -v217 -v218 -v219 -v220 -v221 -v222 -v223 -v224 -v225 -v226 -v227 -v228 -v229 -v230 -v231 -v232 -v233 v234 -v235 -v236 -v237 v238 -v239 -v240 -v241 -v242 -v243 -v244 -v245 -v246 v247 -v248 -v249 -v250 -v251 -v252 -v253 -v254 -v255 -v256 v257 -v258 -v259 -v260 -v261 -v262 -v263 -v264 -v265 -v266 -v267 -v268 -v269 -v270 -v271 -v272 -v273 -v274 -v275 -v276 -v277 -v278 -v279 -v280 -v281 -v282 -v283 -v284 v285 -v286 -v287 -v288 -v289 -v290 -v291 -v292 -v293 -v294 v295 -v296 -v297 -v298 -v299 -v300 -v301 -v302 -v303 -v304 -v305 -v306 -v307 -v308 -v309 -v310 -v311 -v312 -v313 -v314 -v315 -v316 -v317 -v318 -v319 -v320 -v321 -v322 -v323 -v324 -v325 -v326 -v327 v328 -v329 -v330 -v331 v332 -v333 -v334 -v335 v336 -v337 -v338 -v339 -v340 -v341 -v342 v343 v344 v345 -v346 -v347 -v348 v349 -v350 -v351 -v352 v353 -v354 -v355 -v356 -v357 -v358 -v359 v360 v361 v362 -v363 -v364 -v365 -v366 -v367 -v368 -v369 -v370 -v371 -v372 -v373 -v374 -v375 -v376 -v377 -v378 -v379 -v380 -v381 -v382 -v383 -v384 -v385 v386 -v387 -v388 -v389 -v390 -v391 -v392 -v393 -v394 -v395 -v396 -v397 -v398 v399 -v400 -v401 -v402 -v403 -v404 -v405 -v406 -v407 -v408 -v409 -v410 -v411 -v412 -v413 -v414 -v415 -v416 -v417 -v418 -v419 -v420 -v421 -v422 -v423 -v424 -v425 -v426 -v427 -v428 -v429 v430 -v431 -v432 -v433 -v434 -v435 v436 v437 v438 -v439 -v440 -v441 -v442 -v443 -v444 -v445 -v446 -v447 -v448 -v449 -v450 -v451 -v452 -v453 -v454 -v455 -v456 v457 v458 v459 -v460 -v461 -v462 -v463 -v464 -v465 -v466 -v467 -v468 -v469 -v470 -v471 v472 -v473 -v474 -v475 -v476 -v477 -v478 -v479 -v480 -v481 -v482 -v483 -v484 -v485 -v486 -v487 v488 -v489 -v490 -v491 -v492 -v493 -v494 -v495 -v496 -v497 -v498 -v499 -v500 -v501 -v502 v503 -v504 -v505 -v506 -v507 -v508 -v509 -v510 -v511 -v512 -v513 -v514 -v515 -v516 -v517 v518 -v519 -v520 -v521 -v522 -v523 -v524 -v525 -v526 -v527 -v528 -v529 -v530 v531 -v532 -v533 -v534 -v535 -v536 -v537 -v538 -v539 -v540 -v541 -v542 -v543 v544 -v545 -v546 -v547 -v548 -v549 -v550 -v551 -v552 -v553 -v554 -v555 -v556 -v557 -v558 -v559 -v560 -v561 -v562 -v563 -v564 -v565 -v566 -v567 -v568 -v569 -v570 -v571 -v572 v573 -v574 -v575 -v576 -v577 -v578 v579 -v580 -v581 -v582 -v583 -v584 -v585 -v586 -v587 -v588 -v589 -v590 -v591 -v592 -v593 -v594 -v595 -v596 -v597 -v598 -v599 -v600 -v601 -v602 -v603 -v604 -v605 -v606 -v607 -v608 -v609 -v610 -v611 -v612 -v613 -v614 -v615 -v616 -v617 -v618 -v619 -v620 -v621 v622 -v623 -v624 -v625 -v626 -v627 -v628 -v629 -v630 -v631 -v632 v633 -v634 -v635 -v636 -v637 -v638 -v639 -v640 -v641 -v642 -v643 -v644 -v645 -v646 -v647 -v648
c _______________________________________________________________________________
c 
c restarts              : 63
c conflicts             : 565816         (838 /sec)
c decisions             : 846030         (1253 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 675.25 s
c _______________________________________________________________________________

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/6782/stat): 6782 (minisat+_script) R 6781 6782 27660 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1771496986 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/6782/statm): 174 3 169 147 0 27 0
[pid=6782] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libtermcap.so.2
open syscall for file tls/i686/libtermcap.so.2
open syscall for file tls/mmx/libtermcap.so.2
open syscall for file tls/libtermcap.so.2
open syscall for file i686/mmx/libtermcap.so.2
open syscall for file i686/libtermcap.so.2
open syscall for file mmx/libtermcap.so.2
open syscall for file libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/libtermcap.so.2
open syscall for file /etc/ld.so.cache
open syscall for file /lib/libtermcap.so.2
open syscall for file tls/i686/mmx/libdl.so.2
open syscall for file tls/i686/libdl.so.2
open syscall for file tls/mmx/libdl.so.2
open syscall for file tls/libdl.so.2
open syscall for file i686/mmx/libdl.so.2
open syscall for file i686/libdl.so.2
open syscall for file mmx/libdl.so.2
open syscall for file libdl.so.2
open syscall for file /oldhome/oroussel/lib/libdl.so.2
open syscall for file /lib/libdl.so.2
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /lib/tls/libc.so.6
open syscall for file /dev/tty
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
New process pid=6783
New process pid=6784
New process pid=6785
execve syscall for /bin/sed executable
One traced child (pid=6784) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=6785) exited with status: 0
One traced child (pid=6783) exited with status: 0
New process pid=6786
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc8/normalized-s4-4-3-3pb.opb

[startup+10.0045 s]
Raw data (loadavg): 0.93 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 962 0 0 0 986 4 0 0 25 0 1 0 1771496991 4251648 949 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 1038 949 145 145 0 893 0
[pid=6786] vsize: 4152
Current children cumulated CPU time (s) 9.91
Current children cumulated vsize (Kb) 6276

[startup+20.0053 s]
Raw data (loadavg): 0.94 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 1108 0 0 0 1983 5 0 0 25 0 1 0 1771496991 4849664 1095 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 1184 1095 145 145 0 1039 0
[pid=6786] vsize: 4736
Current children cumulated CPU time (s) 19.89
Current children cumulated vsize (Kb) 6860

[startup+30.0061 s]
Raw data (loadavg): 0.95 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 1129 0 0 0 2983 5 0 0 25 0 1 0 1771496991 4939776 1116 4294967295 134512640 135094434 3221224448 3221223104 134558574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 1206 1116 145 145 0 1061 0
[pid=6786] vsize: 4824
Current children cumulated CPU time (s) 29.89
Current children cumulated vsize (Kb) 6948

[startup+40.0069 s]
Raw data (loadavg): 0.96 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 1302 0 0 0 3980 6 0 0 25 0 1 0 1771496991 5640192 1289 4294967295 134512640 135094434 3221224448 3221223116 134555968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6786/statm): 1377 1289 145 145 0 1232 0
[pid=6786] vsize: 5508
Current children cumulated CPU time (s) 39.87
Current children cumulated vsize (Kb) 7632

[startup+50.0077 s]
Raw data (loadavg): 0.96 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 2813 0 0 0 4970 10 0 0 25 0 1 0 1771496991 11849728 2693 4294967295 134512640 135094434 3221224448 3221223072 134557669 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6786/statm): 2893 2693 145 145 0 2748 0
[pid=6786] vsize: 11572
Current children cumulated CPU time (s) 49.81
Current children cumulated vsize (Kb) 13696

[startup+60.0085 s]
Raw data (loadavg): 0.97 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 3493 0 0 0 5958 16 0 0 25 0 1 0 1771496991 14655488 3373 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6786/statm): 3578 3373 145 145 0 3433 0
[pid=6786] vsize: 14312
Current children cumulated CPU time (s) 59.75
Current children cumulated vsize (Kb) 16436

[startup+70.0102 s]
Raw data (loadavg): 0.97 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 3890 0 0 0 6950 19 0 0 25 0 1 0 1771496991 16691200 3770 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 4075 3770 145 145 0 3930 0
[pid=6786] vsize: 16300
Current children cumulated CPU time (s) 69.7
Current children cumulated vsize (Kb) 18424

[startup+80.011 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 3965 0 0 0 7950 20 0 0 25 0 1 0 1771496991 17125376 3845 4294967295 134512640 135094434 3221224448 3221223104 134558240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 4181 3845 145 145 0 4036 0
[pid=6786] vsize: 16724
Current children cumulated CPU time (s) 79.71
Current children cumulated vsize (Kb) 18848

[startup+90.0118 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 4212 0 0 0 8946 22 0 0 25 0 1 0 1771496991 18157568 4092 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 4433 4092 145 145 0 4288 0
[pid=6786] vsize: 17732
Current children cumulated CPU time (s) 89.69
Current children cumulated vsize (Kb) 19856

[startup+100.013 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 4251 0 0 0 9946 22 0 0 25 0 1 0 1771496991 18341888 4131 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 4478 4131 145 145 0 4333 0
[pid=6786] vsize: 17912
Current children cumulated CPU time (s) 99.69
Current children cumulated vsize (Kb) 20036

[startup+110.014 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 4283 0 0 0 10946 22 0 0 25 0 1 0 1771496991 18472960 4163 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 4510 4163 145 145 0 4365 0
[pid=6786] vsize: 18040
Current children cumulated CPU time (s) 109.69
Current children cumulated vsize (Kb) 20164

[startup+120.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 4323 0 0 0 11946 22 0 0 25 0 1 0 1771496991 18669568 4203 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 4558 4203 145 145 0 4413 0
[pid=6786] vsize: 18232
Current children cumulated CPU time (s) 119.69
Current children cumulated vsize (Kb) 20356

[startup+130.016 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 4376 0 0 0 12946 23 0 0 25 0 1 0 1771496991 18931712 4256 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 4622 4256 145 145 0 4477 0
[pid=6786] vsize: 18488
Current children cumulated CPU time (s) 129.7
Current children cumulated vsize (Kb) 20612

[startup+140.017 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 4376 0 0 0 13946 23 0 0 25 0 1 0 1771496991 18931712 4256 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 4622 4256 145 145 0 4477 0
[pid=6786] vsize: 18488
Current children cumulated CPU time (s) 139.7
Current children cumulated vsize (Kb) 20612

[startup+150.018 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 4388 0 0 0 14946 23 0 0 25 0 1 0 1771496991 18931712 4268 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 4622 4268 145 145 0 4477 0
[pid=6786] vsize: 18488
Current children cumulated CPU time (s) 149.7
Current children cumulated vsize (Kb) 20612

[startup+160.018 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 4407 0 0 0 15946 23 0 0 25 0 1 0 1771496991 19128320 4287 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 4670 4287 145 145 0 4525 0
[pid=6786] vsize: 18680
Current children cumulated CPU time (s) 159.7
Current children cumulated vsize (Kb) 20804

[startup+170.019 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) T 6782 6782 27660 0 -1 0 4653 0 0 0 16943 24 0 0 25 0 1 0 1771496991 20103168 4533 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/6786/statm): 4908 4533 145 145 0 4763 0
[pid=6786] vsize: 19632
Current children cumulated CPU time (s) 169.68
Current children cumulated vsize (Kb) 21756

[startup+180.019 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 5052 0 0 0 17936 27 0 0 25 0 1 0 1771496991 21712896 4932 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 5301 4932 145 145 0 5156 0
[pid=6786] vsize: 21204
Current children cumulated CPU time (s) 179.64
Current children cumulated vsize (Kb) 23328

[startup+190.021 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 5086 0 0 0 18936 27 0 0 25 0 1 0 1771496991 21852160 4966 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 5335 4966 145 145 0 5190 0
[pid=6786] vsize: 21340
Current children cumulated CPU time (s) 189.64
Current children cumulated vsize (Kb) 23464

[startup+200.021 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 5104 0 0 0 19936 27 0 0 25 0 1 0 1771496991 21934080 4984 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 5355 4984 145 145 0 5210 0
[pid=6786] vsize: 21420
Current children cumulated CPU time (s) 199.64
Current children cumulated vsize (Kb) 23544

[startup+210.022 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 5128 0 0 0 20936 27 0 0 25 0 1 0 1771496991 22065152 5008 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 5387 5008 145 145 0 5242 0
[pid=6786] vsize: 21548
Current children cumulated CPU time (s) 209.64
Current children cumulated vsize (Kb) 23672

[startup+220.024 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 5161 0 0 0 21936 27 0 0 25 0 1 0 1771496991 22245376 5041 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 5431 5041 145 145 0 5286 0
[pid=6786] vsize: 21724
Current children cumulated CPU time (s) 219.64
Current children cumulated vsize (Kb) 23848

[startup+230.025 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 5164 0 0 0 22937 27 0 0 25 0 1 0 1771496991 22245376 5044 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 5431 5044 145 145 0 5286 0
[pid=6786] vsize: 21724
Current children cumulated CPU time (s) 229.65
Current children cumulated vsize (Kb) 23848

[startup+240.026 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 5284 0 0 0 23936 28 0 0 25 0 1 0 1771496991 22740992 5164 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 5552 5164 145 145 0 5407 0
[pid=6786] vsize: 22208
Current children cumulated CPU time (s) 239.65
Current children cumulated vsize (Kb) 24332

[startup+250.026 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 5417 0 0 0 24934 29 0 0 25 0 1 0 1771496991 23326720 5297 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 5695 5297 145 145 0 5550 0
[pid=6786] vsize: 22780
Current children cumulated CPU time (s) 249.64
Current children cumulated vsize (Kb) 24904

[startup+260.028 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 5535 0 0 0 25932 30 0 0 25 0 1 0 1771496991 23822336 5415 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 5816 5415 145 145 0 5671 0
[pid=6786] vsize: 23264
Current children cumulated CPU time (s) 259.63
Current children cumulated vsize (Kb) 25388

[startup+270.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 5654 0 0 0 26932 30 0 0 25 0 1 0 1771496991 24305664 5534 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 5934 5534 145 145 0 5789 0
[pid=6786] vsize: 23736
Current children cumulated CPU time (s) 269.63
Current children cumulated vsize (Kb) 25860

[startup+280.03 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 5675 0 0 0 27932 30 0 0 25 0 1 0 1771496991 24395776 5555 4294967295 134512640 135094434 3221224448 3221223120 134556507 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 5956 5555 145 145 0 5811 0
[pid=6786] vsize: 23824
Current children cumulated CPU time (s) 279.63
Current children cumulated vsize (Kb) 25948

[startup+290.031 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 5676 0 0 0 28932 30 0 0 25 0 1 0 1771496991 24395776 5556 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 5956 5556 145 145 0 5811 0
[pid=6786] vsize: 23824
Current children cumulated CPU time (s) 289.63
Current children cumulated vsize (Kb) 25948

[startup+300.03 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 5676 0 0 0 29932 30 0 0 25 0 1 0 1771496991 24395776 5556 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 5956 5556 145 145 0 5811 0
[pid=6786] vsize: 23824
Current children cumulated CPU time (s) 299.63
Current children cumulated vsize (Kb) 25948

[startup+310.031 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 5677 0 0 0 30931 31 0 0 25 0 1 0 1771496991 24395776 5557 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6786/statm): 5956 5557 145 145 0 5811 0
[pid=6786] vsize: 23824
Current children cumulated CPU time (s) 309.63
Current children cumulated vsize (Kb) 25948

[startup+320.033 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 5691 0 0 0 31931 31 0 0 25 0 1 0 1771496991 24461312 5571 4294967295 134512640 135094434 3221224448 3221223104 134558227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 5972 5571 145 145 0 5827 0
[pid=6786] vsize: 23888
Current children cumulated CPU time (s) 319.63
Current children cumulated vsize (Kb) 26012

[startup+330.033 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 5711 0 0 0 32931 31 0 0 25 0 1 0 1771496991 24526848 5591 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 5988 5591 145 145 0 5843 0
[pid=6786] vsize: 23952
Current children cumulated CPU time (s) 329.63
Current children cumulated vsize (Kb) 26076

[startup+340.033 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 5793 0 0 0 33930 31 0 0 25 0 1 0 1771496991 25096192 5673 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 6127 5673 145 145 0 5982 0
[pid=6786] vsize: 24508
Current children cumulated CPU time (s) 339.62
Current children cumulated vsize (Kb) 26632

[startup+350.034 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 5817 0 0 0 34930 31 0 0 25 0 1 0 1771496991 25210880 5697 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 6155 5697 145 145 0 6010 0
[pid=6786] vsize: 24620
Current children cumulated CPU time (s) 349.62
Current children cumulated vsize (Kb) 26744

[startup+360.035 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 5840 0 0 0 35931 31 0 0 25 0 1 0 1771496991 25341952 5720 4294967295 134512640 135094434 3221224448 3221223104 134558022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 6187 5720 145 145 0 6042 0
[pid=6786] vsize: 24748
Current children cumulated CPU time (s) 359.63
Current children cumulated vsize (Kb) 26872

[startup+370.036 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 5857 0 0 0 36931 31 0 0 25 0 1 0 1771496991 25473024 5737 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 6219 5737 145 145 0 6074 0
[pid=6786] vsize: 24876
Current children cumulated CPU time (s) 369.63
Current children cumulated vsize (Kb) 27000

[startup+380.037 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 5858 0 0 0 37931 31 0 0 25 0 1 0 1771496991 25473024 5738 4294967295 134512640 135094434 3221224448 3221223136 134554705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 6219 5738 145 145 0 6074 0
[pid=6786] vsize: 24876
Current children cumulated CPU time (s) 379.63
Current children cumulated vsize (Kb) 27000

[startup+390.037 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 5862 0 0 0 38931 31 0 0 25 0 1 0 1771496991 25473024 5742 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 6219 5742 145 145 0 6074 0
[pid=6786] vsize: 24876
Current children cumulated CPU time (s) 389.63
Current children cumulated vsize (Kb) 27000

[startup+400.038 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 5864 0 0 0 39931 31 0 0 25 0 1 0 1771496991 25473024 5744 4294967295 134512640 135094434 3221224448 3221223104 134558181 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 6219 5744 145 145 0 6074 0
[pid=6786] vsize: 24876
Current children cumulated CPU time (s) 399.63
Current children cumulated vsize (Kb) 27000

[startup+410.039 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 5888 0 0 0 40932 31 0 0 25 0 1 0 1771496991 25604096 5768 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 6251 5768 145 145 0 6106 0
[pid=6786] vsize: 25004
Current children cumulated CPU time (s) 409.64
Current children cumulated vsize (Kb) 27128

[startup+420.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 5942 0 0 0 41932 31 0 0 25 0 1 0 1771496991 25931776 5822 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 6331 5822 145 145 0 6186 0
[pid=6786] vsize: 25324
Current children cumulated CPU time (s) 419.64
Current children cumulated vsize (Kb) 27448

[startup+430.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 5969 0 0 0 42932 32 0 0 25 0 1 0 1771496991 25997312 5849 4294967295 134512640 135094434 3221224448 3221223120 134555563 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 6347 5849 145 145 0 6202 0
[pid=6786] vsize: 25388
Current children cumulated CPU time (s) 429.65
Current children cumulated vsize (Kb) 27512

[startup+440.041 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 5969 0 0 0 43932 32 0 0 25 0 1 0 1771496991 25997312 5849 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 6347 5849 145 145 0 6202 0
[pid=6786] vsize: 25388
Current children cumulated CPU time (s) 439.65
Current children cumulated vsize (Kb) 27512

[startup+450.042 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 5969 0 0 0 44932 32 0 0 25 0 1 0 1771496991 25997312 5849 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 6347 5849 145 145 0 6202 0
[pid=6786] vsize: 25388
Current children cumulated CPU time (s) 449.65
Current children cumulated vsize (Kb) 27512

[startup+460.043 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 5984 0 0 0 45932 32 0 0 25 0 1 0 1771496991 26062848 5864 4294967295 134512640 135094434 3221224448 3221223104 134558246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 6363 5864 145 145 0 6218 0
[pid=6786] vsize: 25452
Current children cumulated CPU time (s) 459.65
Current children cumulated vsize (Kb) 27576

[startup+470.044 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 6042 0 0 0 46932 32 0 0 25 0 1 0 1771496991 26390528 5922 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 6443 5922 145 145 0 6298 0
[pid=6786] vsize: 25772
Current children cumulated CPU time (s) 469.65
Current children cumulated vsize (Kb) 27896

[startup+480.043 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 6049 0 0 0 47933 32 0 0 25 0 1 0 1771496991 26390528 5929 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 6443 5929 145 145 0 6298 0
[pid=6786] vsize: 25772
Current children cumulated CPU time (s) 479.66
Current children cumulated vsize (Kb) 27896

[startup+490.045 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 6074 0 0 0 48933 32 0 0 25 0 1 0 1771496991 26521600 5954 4294967295 134512640 135094434 3221224448 3221223072 134557705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 6475 5954 145 145 0 6330 0
[pid=6786] vsize: 25900
Current children cumulated CPU time (s) 489.66
Current children cumulated vsize (Kb) 28024

[startup+500.046 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 6077 0 0 0 49933 32 0 0 25 0 1 0 1771496991 26521600 5957 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 6475 5957 145 145 0 6330 0
[pid=6786] vsize: 25900
Current children cumulated CPU time (s) 499.66
Current children cumulated vsize (Kb) 28024

[startup+510.047 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 6081 0 0 0 50933 32 0 0 25 0 1 0 1771496991 26521600 5961 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 6475 5961 145 145 0 6330 0
[pid=6786] vsize: 25900
Current children cumulated CPU time (s) 509.66
Current children cumulated vsize (Kb) 28024

[startup+520.048 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 6117 0 0 0 51934 32 0 0 25 0 1 0 1771496991 26652672 5997 4294967295 134512640 135094434 3221224448 3221223040 134551454 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 6507 5997 145 145 0 6362 0
[pid=6786] vsize: 26028
Current children cumulated CPU time (s) 519.67
Current children cumulated vsize (Kb) 28152

[startup+530.048 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 6117 0 0 0 52934 32 0 0 25 0 1 0 1771496991 26652672 5997 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 6507 5997 145 145 0 6362 0
[pid=6786] vsize: 26028
Current children cumulated CPU time (s) 529.67
Current children cumulated vsize (Kb) 28152

[startup+540.049 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 6117 0 0 0 53934 32 0 0 25 0 1 0 1771496991 26652672 5997 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 6507 5997 145 145 0 6362 0
[pid=6786] vsize: 26028
Current children cumulated CPU time (s) 539.67
Current children cumulated vsize (Kb) 28152

[startup+550.05 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 6136 0 0 0 54933 32 0 0 25 0 1 0 1771496991 26783744 6016 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6786/statm): 6539 6016 145 145 0 6394 0
[pid=6786] vsize: 26156
Current children cumulated CPU time (s) 549.66
Current children cumulated vsize (Kb) 28280

[startup+560.052 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 6140 0 0 0 55933 32 0 0 25 0 1 0 1771496991 26783744 6020 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 6539 6020 145 145 0 6394 0
[pid=6786] vsize: 26156
Current children cumulated CPU time (s) 559.66
Current children cumulated vsize (Kb) 28280

[startup+570.052 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 6160 0 0 0 56933 32 0 0 25 0 1 0 1771496991 26914816 6040 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 6571 6040 145 145 0 6426 0
[pid=6786] vsize: 26284
Current children cumulated CPU time (s) 569.66
Current children cumulated vsize (Kb) 28408

[startup+580.053 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 6186 0 0 0 57933 33 0 0 25 0 1 0 1771496991 27045888 6066 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 6603 6066 145 145 0 6458 0
[pid=6786] vsize: 26412
Current children cumulated CPU time (s) 579.67
Current children cumulated vsize (Kb) 28536

[startup+590.055 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 6187 0 0 0 58934 33 0 0 25 0 1 0 1771496991 27045888 6067 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 6603 6067 145 145 0 6458 0
[pid=6786] vsize: 26412
Current children cumulated CPU time (s) 589.68
Current children cumulated vsize (Kb) 28536

[startup+600.056 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 6188 0 0 0 59934 33 0 0 25 0 1 0 1771496991 27045888 6068 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 6603 6068 145 145 0 6458 0
[pid=6786] vsize: 26412
Current children cumulated CPU time (s) 599.68
Current children cumulated vsize (Kb) 28536

[startup+610.057 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 6239 0 0 0 60934 33 0 0 25 0 1 0 1771496991 27308032 6119 4294967295 134512640 135094434 3221224448 3221223040 134551428 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6786/statm): 6667 6119 145 145 0 6522 0
[pid=6786] vsize: 26668
Current children cumulated CPU time (s) 609.68
Current children cumulated vsize (Kb) 28792

[startup+620.058 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 6239 0 0 0 61933 33 0 0 25 0 1 0 1771496991 27308032 6119 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6786/statm): 6667 6119 145 145 0 6522 0
[pid=6786] vsize: 26668
Current children cumulated CPU time (s) 619.67
Current children cumulated vsize (Kb) 28792

[startup+630.059 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 6239 0 0 0 62932 33 0 0 25 0 1 0 1771496991 27308032 6119 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 6667 6119 145 145 0 6522 0
[pid=6786] vsize: 26668
Current children cumulated CPU time (s) 629.66
Current children cumulated vsize (Kb) 28792

[startup+640.06 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 6239 0 0 0 63932 33 0 0 25 0 1 0 1771496991 27308032 6119 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 6667 6119 145 145 0 6522 0
[pid=6786] vsize: 26668
Current children cumulated CPU time (s) 639.66
Current children cumulated vsize (Kb) 28792

[startup+650.061 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 6240 0 0 0 64933 33 0 0 25 0 1 0 1771496991 27308032 6120 4294967295 134512640 135094434 3221224448 3221223104 134558029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 6667 6120 145 145 0 6522 0
[pid=6786] vsize: 26668
Current children cumulated CPU time (s) 649.67
Current children cumulated vsize (Kb) 28792

[startup+660.062 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 6240 0 0 0 65933 33 0 0 25 0 1 0 1771496991 27308032 6120 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 6667 6120 145 145 0 6522 0
[pid=6786] vsize: 26668
Current children cumulated CPU time (s) 659.67
Current children cumulated vsize (Kb) 28792

[startup+670.063 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 6786
Raw data (/proc/6782/stat): 6782 (minisat+_script) S 6781 6782 27660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1771496986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6782/statm): 531 226 485 147 0 384 0
[pid=6782] vsize: 2124
Raw data (/proc/6786/stat): 6786 (minisat+_64-bit) R 6782 6782 27660 0 -1 0 6240 0 0 0 66933 33 0 0 25 0 1 0 1771496991 27308032 6120 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6786/statm): 6667 6120 145 145 0 6522 0
[pid=6786] vsize: 26668
Current children cumulated CPU time (s) 669.67
Current children cumulated vsize (Kb) 28792
One traced child (pid=6786) exited with status: 30
One traced child (pid=6782) exited with status: 30
All traced children have exited ! Game is over.

Child status: 30
Real time (s): 676.021
CPU time (s): 675.657
CPU user time (s): 675.286
CPU system time (s): 0.370943
CPU usage (%): 99.9461
Max. virtual memory (cumulated for all children) (Kb): 28792

Verifier Data

Verifier:	OK	62