PB'05 competition: run trace

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:
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.
SOLVER DATA
This is the output of the solver (stdout and stderr).
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.
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

Name	normalized-opb/submitted/manquinho/primes-dimacs-cnf/normalized-ii8b2.opb
MD5SUM	bbfcebd70586668574286ad19a1cd5a8
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	379
Optimality of the best value was proved	NO
Number of terms in the objective function	1152
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	1152
Number of bits of the sum of numbers in the objective function	11
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	1152
Number of bits of the biggest sum of numbers	11
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03984
Number of variables	1152
Total number of constraints	4664
Number of constraints which are clauses	4664
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	8
Trace number 5505

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc11 THE 2005-04-14 00:15:07 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3928 boxname=wulflinc11 idbench=168 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  bbfcebd70586668574286ad19a1cd5a8  /oldhome/oroussel/tmp/wulflinc11/normalized-ii8b2.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc11/normalized-ii8b2.opb /oldhome/oroussel/tmp/wulflinc11/normalized-ii8b2.opb
IDLAUNCH: 3928
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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.028
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:        914520 kB
Buffers:         34884 kB
Cached:          61028 kB
SwapCached:       4932 kB
Active:          55836 kB
Inactive:        47872 kB
HighTotal:      131008 kB
HighFree:        66192 kB
LowTotal:       903652 kB
LowFree:        848328 kB
SwapTotal:     2097136 kB
SwapFree:      2092204 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            10844 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 00:35:10 (client local time) WITH STATUS 10 IN 1200.26 SECONDS
stats: 3928 7 1200.26 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 4664 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    4652    10272 |    1395       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1140          
c   -- var.elim.:  1140/1140          
c |         0 |    4652    10272 |    1860       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.133979 s)
c ==============================================================================
c [1mFound solution: 418[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:63108     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         3 |   80340   187201 |   24101       3       43    14.3 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/50611          
c   -- var.elim.:  2000/50611          
c   -- var.elim.:  3000/50611          
c   -- var.elim.:  4000/50611          
c   -- var.elim.:  5000/50611          
c   -- var.elim.:  6000/50611          
c   -- var.elim.:  7000/50611          
c   -- var.elim.:  8000/50611          
c   -- var.elim.:  9000/50611          
c   -- var.elim.:  10000/50611          
c   -- var.elim.:  11000/50611          
c   -- var.elim.:  12000/50611          
c   -- var.elim.:  13000/50611          
c   -- var.elim.:  14000/50611          
c   -- var.elim.:  15000/50611          
c   -- var.elim.:  16000/50611          
c   -- var.elim.:  17000/50611          
c   -- var.elim.:  18000/50611          
c   -- var.elim.:  19000/50611          
c   -- var.elim.:  20000/50611          
c   -- var.elim.:  21000/50611          
c   -- var.elim.:  22000/50611          
c   -- var.elim.:  23000/50611          
c   -- var.elim.:  24000/50611          
c   -- var.elim.:  25000/50611          
c   -- var.elim.:  26000/50611          
c   -- var.elim.:  27000/50611          
c   -- var.elim.:  28000/50611          
c   -- var.elim.:  29000/50611          
c   -- var.elim.:  30000/50611          
c   -- var.elim.:  31000/50611          
c   -- var.elim.:  32000/50611          
c   -- var.elim.:  33000/50611          
c   -- var.elim.:  34000/50611          
c   -- var.elim.:  35000/50611          
c   -- var.elim.:  36000/50611          
c   -- var.elim.:  37000/50611          
c   -- var.elim.:  38000/50611          
c   -- var.elim.:  39000/50611          
c   -- var.elim.:  40000/50611          
c   -- var.elim.:  41000/50611          
c   -- var.elim.:  42000/50611          
c   -- var.elim.:  43000/50611          
c   -- var.elim.:  44000/50611          
c   -- var.elim.:  45000/50611          
c   -- var.elim.:  46000/50611          
c   -- var.elim.:  47000/50611          
c   -- var.elim.:  48000/50611          
c   -- var.elim.:  49000/50611          
c   -- var.elim.:  50000/50611          
c   -- var.elim.:  50611/50611          
c   -- var.elim.:  1000/25049          
c   -- var.elim.:  2000/25049          
c   -- var.elim.:  3000/25049          
c   -- var.elim.:  4000/25049          
c   -- var.elim.:  5000/25049          
c   -- var.elim.:  6000/25049          
c   -- var.elim.:  7000/25049          
c   -- var.elim.:  8000/25049          
c   -- var.elim.:  9000/25049          
c   -- var.elim.:  10000/25049          
c   -- var.elim.:  11000/25049          
c   -- var.elim.:  12000/25049          
c   -- var.elim.:  13000/25049          
c   -- var.elim.:  14000/25049          
c   -- var.elim.:  15000/25049          
c   -- var.elim.:  16000/25049          
c   -- var.elim.:  17000/25049          
c   -- var.elim.:  18000/25049          
c   -- var.elim.:  19000/25049          
c   -- var.elim.:  20000/25049          
c   -- var.elim.:  21000/25049          
c   -- var.elim.:  22000/25049          
c   -- var.elim.:  23000/25049          
c   -- var.elim.:  24000/25049          
c   -- var.elim.:  25000/25049          
c   -- var.elim.:  25049/25049          
c   -- var.elim.:  1000/15219          
c   -- var.elim.:  2000/15219          
c   -- var.elim.:  3000/15219          
c   -- var.elim.:  4000/15219          
c   -- var.elim.:  5000/15219          
c   -- var.elim.:  6000/15219          
c   -- var.elim.:  7000/15219          
c   -- var.elim.:  8000/15219          
c   -- var.elim.:  9000/15219          
c   -- var.elim.:  10000/15219          
c   -- var.elim.:  11000/15219          
c   -- var.elim.:  12000/15219          
c   -- var.elim.:  13000/15219          
c   -- var.elim.:  14000/15219          
c   -- var.elim.:  15000/15219          
c   -- var.elim.:  15219/15219          
c   -- var.elim.:  1000/11078          
c   -- var.elim.:  2000/11078          
c   -- var.elim.:  3000/11078          
c   -- var.elim.:  4000/11078          
c   -- var.elim.:  5000/11078          
c   -- var.elim.:  6000/11078          
c   -- var.elim.:  7000/11078          
c   -- var.elim.:  8000/11078          
c   -- var.elim.:  9000/11078          
c   -- var.elim.:  10000/11078          
c   -- var.elim.:  11000/11078          
c   -- var.elim.:  11078/11078          
c   -- var.elim.:  1000/8089          
c   -- var.elim.:  2000/8089          
c   -- var.elim.:  3000/8089          
c   -- var.elim.:  4000/8089          
c   -- var.elim.:  5000/8089          
c   -- var.elim.:  6000/8089          
c   -- var.elim.:  7000/8089          
c   -- var.elim.:  8000/8089          
c   -- var.elim.:  8089/8089          
c   -- var.elim.:  1000/6754          
c   -- var.elim.:  2000/6754          
c   -- var.elim.:  3000/6754          
c   -- var.elim.:  4000/6754          
c   -- var.elim.:  5000/6754          
c   -- var.elim.:  6000/6754          
c   -- var.elim.:  6754/6754          
c   -- var.elim.:  1000/6575          
c   -- var.elim.:  2000/6575          
c   -- var.elim.:  3000/6575          
c   -- var.elim.:  4000/6575          
c   -- var.elim.:  5000/6575          
c   -- var.elim.:  6000/6575          
c   -- var.elim.:  6575/6575          
c   -- var.elim.:  1000/2191          
c   -- var.elim.:  2000/2191          
c   -- var.elim.:  2191/2191          
c   -- subsuming                       
c   -- var.elim.:  1000/8212          
c   -- var.elim.:  2000/8212          
c   -- var.elim.:  3000/8212          
c   -- var.elim.:  4000/8212          
c   -- var.elim.:  5000/8212          
c   -- var.elim.:  6000/8212          
c   -- var.elim.:  7000/8212          
c   -- var.elim.:  8000/8212          
c   -- var.elim.:  8212/8212          
c   -- var.elim.:  43/43          
c |         3 |   27107   189547 |      --       3       --      -- |     --   | -53223/2376
c |         3 |   27107   189547 |   10842       3       43    14.3 |  0.000 % |
c |       103 |   27107   189547 |   11927     103     7417    72.0 |  0.094 % |
c |       253 |   26950   188167 |   13043     247    39288   159.1 |  0.618 % |
c |       478 |   26712   185938 |   14221     463    73875   159.6 |  1.477 % |
c |       815 |   26409   182949 |   15466     789   184165   233.4 |  2.636 % |
c |      1321 |   26188   180926 |   16870    1286   268858   209.1 |  3.469 % |
c |      2080 |   26023   179301 |   18440    2036   484883   238.2 |  4.095 % |
c |      3221 |   25788   176919 |   20101    3161   776746   245.7 |  4.997 % |
c |      4930 |   25503   174247 |   21867    4850  1214387   250.4 |  6.105 % |
c |      7493 |   25337   172572 |   23897    7403  2304437   311.3 |  6.766 % |
c |     11337 |   25239   171570 |   26185   11240  3919212   348.7 |  7.169 % |
c |     17103 |   25239   171570 |   28803   17006  6592912   387.7 |  7.169 % |
c |     25752 |   25239   171570 |   31684   25655 13486389   525.7 |  7.169 % |
c |     38727 |   25239   171570 |   34852   19851 14090223   709.8 |  7.169 % |
c |     58188 |   25239   171570 |   38338   16779 11414278   680.3 |  7.169 % |
c |     87380 |   25195   171124 |   42098   20163 16200217   803.5 |  7.341 % |
c |    131169 |   25144   170752 |   46214   30792 26205404   851.0 |  7.530 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x1 -x2 x3 -x4 -x5 x6 x7 -x8 x9 -x10 x11 -x12 x13 -x14 x15 -x16 x17 -x18 x19 -x20 x21 -x22 x23 -x24 x25 -x26 x27 -x28 x29 -x30 x31 -x32 x33 -x34 -x35 x36 x37 -x38 x39 -x40 x41 -x42 x43 -x44 x45 -x46 -x47 x48 x49 -x50 -x51 -x52 -x53 x54 x55 -x56 x57 -x58 x59 -x60 x61 -x62 x63 -x64 x65 -x66 x67 -x68 -x69 x70 x71 -x72 x73 -x74 x75 -x76 x77 -x78 x79 -x80 x81 -x82 x83 -x84 x85 -x86 x87 -x88 x89 -x90 x91 -x92 x93 -x94 x95 -x96 x97 -x98 x99 -x100 x101 -x102 x103 -x104 x105 -x106 x107 -x108 x109 -x110 x111 -x112 x113 -x114 x115 -x116 x117 -x118 x119 -x120 x121 -x122 x123 -x124 -x125 x126 x127 -x128 x129 -x130 x131 -x132 x133 -x134 x135 -x136 x137 -x138 x139 -x140 x141 -x142 x143 -x144 x145 -x146 x147 -x148 x149 -x150 x151 -x152 x153 -x154 x155 -x156 -x157 x158 x159 -x160 x161 -x162 x163 -x164 x165 -x166 x167 -x168 x169 -x170 x171 -x172 x173 -x174 x175 -x176 x177 -x178 x179 -x180 x181 -x182 x183 -x184 x185 -x186 x187 -x188 -x189 x190 x191 -x192 -x193 x194 -x195 x196 -x197 x198 x199 -x200 -x201 -x202 -x203 -x204 -x205 x206 x207 -x208 -x209 -x210 -x211 x212 -x213 x214 -x215 x216 x217 -x218 -x219 x220 -x221 -x222 -x223 -x224 -x225 -x226 -x227 -x228 x229 -x230 -x231 x232 -x233 -x234 -x235 -x236 -x237 -x238 -x239 -x240 x241 -x242 -x243 x244 -x245 -x246 -x247 x248 -x249 x250 -x251 x252 x253 -x254 -x255 x256 -x257 -x258 -x259 -x260 -x261 -x262 -x263 -x264 -x265 x266 -x267 x268 x269 -x270 -x271 x272 -x273 x274 -x275 x276 x277 -x278 -x279 x280 -x281 -x282 -x283 -x284 -x285 -x286 -x287 -x288 -x289 x290 -x291 x292 x293 -x294 -x295 x296 -x297 x298 -x299 x300 x301 -x302 -x303 x304 -x305 -x306 -x307 -x308 -x309 -x310 -x311 -x312 -x313 x314 x315 -x316 -x317 -x318 -x319 -x320 -x321 -x322 -x323 -x324 -x325 x326 -x327 x328 -x329 x330 x331 -x332 -x333 -x334 -x335 -x336 x337 -x338 -x339 x340 -x341 -x342 -x343 -x344 -x345 -x346 -x347 -x348 x349 -x350 -x351 x352 -x353 -x354 -x355 -x356 -x357 -x358 -x359 -x360 x361 -x362 -x363 x364 -x365 -x366 -x367 -x368 -x369 -x370 -x371 -x372 -x373 x374 -x375 x376 -x377 x378 x379 -x380 -x381 -x382 -x383 -x384 -x385 x386 -x387 x388 x389 -x390 -x391 -x392 -x393 -x394 -x395 -x396 x397 -x398 -x399 x400 -x401 -x402 -x403 x404 -x405 x406 -x407 x408 x409 -x410 -x411 x412 -x413 -x414 -x415 -x416 -x417 -x418 -x419 -x420 x421 -x422 -x423 x424 -x425 -x426 -x427 -x428 -x429 -x430 -x431 -x432 -x433 x434 -x435 x436 -x437 x438 x439 -x440 -x441 -x442 -x443 -x444 -x445 x446 -x447 x448 x449 -x450 -x451 -x452 -x453 -x454 -x455 -x456 -x457 x458 -x459 x460 x461 -x462 -x463 x464 -x465 x466 -x467 x468 -x469 x470 -x471 x472 x473 -x474 -x475 -x476 -x477 -x478 -x479 -x480 -x481 x482 -x483 x484 x485 -x486 -x487 x488 -x489 x490 -x491 x492 x493 -x494 -x495 x496 -x497 -x498 -x499 -x500 -x501 -x502 -x503 -x504 -x505 x506 -x507 x508 x509 -x510 -x511 x512 -x513 x514 -x515 x516 x517 -x518 -x519 x520 -x521 -x522 -x523 x524 -x525 x526 -x527 x528 -x529 x530 -x531 x532 x533 #### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.93 0.97 0.91 2/54 5768
Raw data (stat): 5768 (runsolver) R 5767 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421968877 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99996 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 7816 0 0 0 971 26 0 0 25 0 1 0 421968877 34672640 7527 4294967295 134512640 134672761 3221224576 3221223024 134643583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8465 7527 603 41 0 8424 0
vsize: 33860
[startup+20.0002 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 7821 0 0 0 1971 26 0 0 25 0 1 0 421968877 34672640 7532 4294967295 134512640 134672761 3221224576 3221223056 134541816 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8465 7532 603 41 0 8424 0
vsize: 33860
[startup+30.0003 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 7821 0 0 0 2971 26 0 0 25 0 1 0 421968877 34672640 7532 4294967295 134512640 134672761 3221224576 3221223024 134643474 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8465 7532 603 41 0 8424 0
vsize: 33860
[startup+40.0013 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 7822 0 0 0 3970 27 0 0 25 0 1 0 421968877 34672640 7533 4294967295 134512640 134672761 3221224576 3221223024 134643493 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8465 7533 603 41 0 8424 0
vsize: 33860
[startup+50.0016 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 7822 0 0 0 4970 27 0 0 25 0 1 0 421968877 34672640 7533 4294967295 134512640 134672761 3221224576 3221223024 134643580 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8465 7533 603 41 0 8424 0
vsize: 33860
[startup+60.0016 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 7822 0 0 0 5970 27 0 0 25 0 1 0 421968877 34672640 7533 4294967295 134512640 134672761 3221224576 3221223024 134643987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8465 7533 603 41 0 8424 0
vsize: 33860
[startup+70.0028 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 7982 0 0 0 6961 36 0 0 25 0 1 0 421968877 35221504 7643 4294967295 134512640 134672761 3221224576 3221222784 1075730206 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8599 7643 603 41 0 8558 0
vsize: 34396
[startup+80.0031 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 7990 0 0 0 7954 41 0 0 25 0 1 0 421968877 35090432 7633 4294967295 134512640 134672761 3221224576 3221223024 134643954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8567 7633 603 41 0 8526 0
vsize: 34268
[startup+90.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 7991 0 0 0 8953 43 0 0 25 0 1 0 421968877 35090432 7634 4294967295 134512640 134672761 3221224576 3221223024 134643574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8567 7634 603 41 0 8526 0
vsize: 34268
[startup+100.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 7991 0 0 0 9951 43 0 0 25 0 1 0 421968877 35090432 7634 4294967295 134512640 134672761 3221224576 3221223024 134643556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8567 7634 603 41 0 8526 0
vsize: 34268
[startup+110.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 7991 0 0 0 10951 44 0 0 25 0 1 0 421968877 35090432 7634 4294967295 134512640 134672761 3221224576 3221223024 134643577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8567 7634 603 41 0 8526 0
vsize: 34268
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 7991 0 0 0 11951 44 0 0 25 0 1 0 421968877 34828288 7584 4294967295 134512640 134672761 3221224576 3221222748 134642831 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8503 7584 603 41 0 8462 0
vsize: 34012
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 7991 0 0 0 12951 44 0 0 25 0 1 0 421968877 34828288 7584 4294967295 134512640 134672761 3221224576 3221223040 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8503 7584 603 41 0 8462 0
vsize: 34012
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 8074 0 0 0 13951 44 0 0 25 0 1 0 421968877 35311616 7664 4294967295 134512640 134672761 3221224576 3221223120 134621065 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8621 7664 603 41 0 8580 0
vsize: 34484
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 8075 0 0 0 14951 44 0 0 25 0 1 0 421968877 34828288 7586 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8503 7586 603 41 0 8462 0
vsize: 34012
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 8230 0 0 0 15950 44 0 0 25 0 1 0 421968877 35475456 7741 4294967295 134512640 134672761 3221224576 3221223720 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8661 7741 603 41 0 8620 0
vsize: 34644
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 8824 0 0 0 16950 45 0 0 25 0 1 0 421968877 37920768 8335 4294967295 134512640 134672761 3221224576 3221223720 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9258 8335 603 41 0 9217 0
vsize: 37032
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 9968 0 0 0 17947 48 0 0 25 0 1 0 421968877 42536960 9479 4294967295 134512640 134672761 3221224576 3221223616 134614254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9479 603 41 0 10344 0
vsize: 41540
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 11243 0 0 0 18943 52 0 0 25 0 1 0 421968877 47824896 10754 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11676 10754 603 41 0 11635 0
vsize: 46704
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 12413 0 0 0 19941 54 0 0 25 0 1 0 421968877 52559872 11924 4294967295 134512640 134672761 3221224576 3221223616 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12832 11924 603 41 0 12791 0
vsize: 51328
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 13951 0 0 0 20938 58 0 0 25 0 1 0 421968877 58953728 13462 4294967295 134512640 134672761 3221224576 3221223616 134603510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14393 13462 603 41 0 14352 0
vsize: 57572
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 15541 0 0 0 21935 61 0 0 25 0 1 0 421968877 65478656 15052 4294967295 134512640 134672761 3221224576 3221223616 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15986 15052 603 41 0 15945 0
vsize: 63944
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 16869 0 0 0 22931 65 0 0 25 0 1 0 421968877 70864896 16380 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17301 16380 603 41 0 17260 0
vsize: 69204
[startup+240.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 18383 0 0 0 23928 68 0 0 25 0 1 0 421968877 77135872 17894 4294967295 134512640 134672761 3221224576 3221223728 134565083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18832 17894 603 41 0 18791 0
vsize: 75328
[startup+250.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 20123 0 0 0 24924 72 0 0 25 0 1 0 421968877 84226048 19634 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20563 19634 603 41 0 20522 0
vsize: 82252
[startup+260.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 21258 0 0 0 25922 75 0 0 25 0 1 0 421968877 88850432 20769 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21692 20769 603 41 0 21651 0
vsize: 86768
[startup+270.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 22837 0 0 0 26918 79 0 0 25 0 1 0 421968877 95322112 22348 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23272 22348 603 41 0 23231 0
vsize: 93088
[startup+280.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 24477 0 0 0 27914 83 0 0 25 0 1 0 421968877 101990400 23988 4294967295 134512640 134672761 3221224576 3221223616 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24900 23988 603 41 0 24859 0
vsize: 99600
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 26209 0 0 0 28912 86 0 0 25 0 1 0 421968877 109203456 25720 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26661 25720 603 41 0 26620 0
vsize: 106644
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 27583 0 0 0 29910 88 0 0 25 0 1 0 421968877 114921472 27094 4294967295 134512640 134672761 3221224576 3221223672 134616299 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28057 27094 603 41 0 28016 0
vsize: 112228
[startup+310.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 27583 0 0 0 30910 88 0 0 25 0 1 0 421968877 114659328 27060 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27993 27060 603 41 0 27952 0
vsize: 111972
[startup+320.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 27583 0 0 0 31910 88 0 0 25 0 1 0 421968877 114659328 27060 4294967295 134512640 134672761 3221224576 3221223616 134603527 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27993 27060 603 41 0 27952 0
vsize: 111972
[startup+330.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 27583 0 0 0 32910 88 0 0 25 0 1 0 421968877 114659328 27060 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27993 27060 603 41 0 27952 0
vsize: 111972
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 27583 0 0 0 33910 88 0 0 25 0 1 0 421968877 114659328 27060 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27993 27060 603 41 0 27952 0
vsize: 111972
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 27583 0 0 0 34911 88 0 0 25 0 1 0 421968877 114659328 27060 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27993 27060 603 41 0 27952 0
vsize: 111972
[startup+360.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 27583 0 0 0 35911 88 0 0 25 0 1 0 421968877 114659328 27060 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27993 27060 603 41 0 27952 0
vsize: 111972
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 28580 0 0 0 36909 90 0 0 25 0 1 0 421968877 118747136 28057 4294967295 134512640 134672761 3221224576 3221223584 134522549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28991 28057 603 41 0 28950 0
vsize: 115964
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 29807 0 0 0 37907 92 0 0 25 0 1 0 421968877 123797504 29284 4294967295 134512640 134672761 3221224576 3221223760 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30224 29284 603 41 0 30183 0
vsize: 120896
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 31464 0 0 0 38903 96 0 0 25 0 1 0 421968877 130617344 30941 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31889 30941 603 41 0 31848 0
vsize: 127556
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 33101 0 0 0 39900 99 0 0 25 0 1 0 421968877 137281536 32578 4294967295 134512640 134672761 3221224576 3221223760 134615581 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33516 32578 603 41 0 33475 0
vsize: 134064
[startup+410.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 34726 0 0 0 40897 103 0 0 25 0 1 0 421968877 143966208 34203 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35148 34203 603 41 0 35107 0
vsize: 140592
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 36235 0 0 0 41894 106 0 0 25 0 1 0 421968877 150138880 35712 4294967295 134512640 134672761 3221224576 3221223760 134615838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36655 35712 603 41 0 36614 0
vsize: 146620
[startup+430.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 37738 0 0 0 42890 109 0 0 25 0 1 0 421968877 156332032 37215 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38167 37215 603 41 0 38126 0
vsize: 152668
[startup+440.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 37881 0 0 0 43890 109 0 0 25 0 1 0 421968877 156672000 37320 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38250 37320 603 41 0 38209 0
vsize: 153000
[startup+450.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 37881 0 0 0 44890 109 0 0 25 0 1 0 421968877 156672000 37320 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38250 37320 603 41 0 38209 0
vsize: 153000
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 37881 0 0 0 45890 109 0 0 25 0 1 0 421968877 156672000 37320 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38250 37320 603 41 0 38209 0
vsize: 153000
[startup+470.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 37881 0 0 0 46891 109 0 0 25 0 1 0 421968877 156672000 37320 4294967295 134512640 134672761 3221224576 3221223760 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38250 37320 603 41 0 38209 0
vsize: 153000
[startup+480.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 37881 0 0 0 47891 109 0 0 25 0 1 0 421968877 156672000 37320 4294967295 134512640 134672761 3221224576 3221223616 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38250 37320 603 41 0 38209 0
vsize: 153000
[startup+490.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 37881 0 0 0 48891 109 0 0 25 0 1 0 421968877 156672000 37320 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38250 37320 603 41 0 38209 0
vsize: 153000
[startup+500.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 37881 0 0 0 49891 109 0 0 25 0 1 0 421968877 156672000 37320 4294967295 134512640 134672761 3221224576 3221223760 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38250 37320 603 41 0 38209 0
vsize: 153000
[startup+510.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 37881 0 0 0 50891 109 0 0 25 0 1 0 421968877 156672000 37320 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38250 37320 603 41 0 38209 0
vsize: 153000
[startup+520.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 37881 0 0 0 51892 109 0 0 25 0 1 0 421968877 156672000 37320 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38250 37320 603 41 0 38209 0
vsize: 153000
[startup+530.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 37881 0 0 0 52892 109 0 0 25 0 1 0 421968877 156672000 37320 4294967295 134512640 134672761 3221224576 3221223616 134613809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38250 37320 603 41 0 38209 0
vsize: 153000
[startup+540.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 37881 0 0 0 53892 109 0 0 25 0 1 0 421968877 156672000 37320 4294967295 134512640 134672761 3221224576 3221223616 134614205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38250 37320 603 41 0 38209 0
vsize: 153000
[startup+550.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 38414 0 0 0 54892 109 0 0 25 0 1 0 421968877 158867456 37853 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38786 37853 603 41 0 38745 0
vsize: 155144
[startup+560.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 39765 0 0 0 55889 112 0 0 25 0 1 0 421968877 164421632 39204 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40142 39204 603 41 0 40101 0
vsize: 160568
[startup+570.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 41504 0 0 0 56884 118 0 0 25 0 1 0 421968877 171618304 40943 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41899 40943 603 41 0 41858 0
vsize: 167596
[startup+580.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 43145 0 0 0 57881 121 0 0 25 0 1 0 421968877 178343936 42584 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43541 42584 603 41 0 43500 0
vsize: 174164
[startup+590.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 43882 0 0 0 58878 123 0 0 25 0 1 0 421968877 181342208 43321 4294967295 134512640 134672761 3221224576 3221223672 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44273 43321 603 41 0 44232 0
vsize: 177092
[startup+600.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 43882 0 0 0 59879 123 0 0 25 0 1 0 421968877 181080064 43281 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44209 43281 603 41 0 44168 0
vsize: 176836
[startup+610.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 43882 0 0 0 60879 123 0 0 25 0 1 0 421968877 181080064 43281 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44209 43281 603 41 0 44168 0
vsize: 176836
[startup+620.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 43882 0 0 0 61879 123 0 0 25 0 1 0 421968877 181080064 43281 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44209 43281 603 41 0 44168 0
vsize: 176836
[startup+630.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 43882 0 0 0 62879 123 0 0 25 0 1 0 421968877 181080064 43281 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44209 43281 603 41 0 44168 0
vsize: 176836
[startup+640.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 43882 0 0 0 63879 123 0 0 25 0 1 0 421968877 181080064 43281 4294967295 134512640 134672761 3221224576 3221223616 134614266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44209 43281 603 41 0 44168 0
vsize: 176836
[startup+650.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 43882 0 0 0 64880 123 0 0 25 0 1 0 421968877 181080064 43281 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44209 43281 603 41 0 44168 0
vsize: 176836
[startup+660.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 43882 0 0 0 65880 123 0 0 25 0 1 0 421968877 181080064 43281 4294967295 134512640 134672761 3221224576 3221223616 134612682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44209 43281 603 41 0 44168 0
vsize: 176836
[startup+670.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 43882 0 0 0 66880 123 0 0 25 0 1 0 421968877 181080064 43281 4294967295 134512640 134672761 3221224576 3221223616 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44209 43281 603 41 0 44168 0
vsize: 176836
[startup+680.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 43882 0 0 0 67880 123 0 0 25 0 1 0 421968877 181080064 43281 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44209 43281 603 41 0 44168 0
vsize: 176836
[startup+690.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 43882 0 0 0 68880 123 0 0 25 0 1 0 421968877 181080064 43281 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44209 43281 603 41 0 44168 0
vsize: 176836
[startup+700.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 43882 0 0 0 69880 123 0 0 25 0 1 0 421968877 181080064 43281 4294967295 134512640 134672761 3221224576 3221223616 134614205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44209 43281 603 41 0 44168 0
vsize: 176836
[startup+710.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 43882 0 0 0 70881 123 0 0 25 0 1 0 421968877 181080064 43281 4294967295 134512640 134672761 3221224576 3221223720 134566157 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44209 43281 603 41 0 44168 0
vsize: 176836
[startup+720.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 43882 0 0 0 71881 123 0 0 25 0 1 0 421968877 181080064 43281 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44209 43281 603 41 0 44168 0
vsize: 176836
[startup+730.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 43882 0 0 0 72881 123 0 0 25 0 1 0 421968877 181080064 43281 4294967295 134512640 134672761 3221224576 3221223616 134612694 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44209 43281 603 41 0 44168 0
vsize: 176836
[startup+740.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 43882 0 0 0 73881 123 0 0 25 0 1 0 421968877 181080064 43281 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44209 43281 603 41 0 44168 0
vsize: 176836
[startup+750.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 43882 0 0 0 74881 123 0 0 25 0 1 0 421968877 181080064 43281 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44209 43281 603 41 0 44168 0
vsize: 176836
[startup+760.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 43882 0 0 0 75881 123 0 0 25 0 1 0 421968877 181080064 43281 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44209 43281 603 41 0 44168 0
vsize: 176836
[startup+770.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 44302 0 0 0 76880 124 0 0 25 0 1 0 421968877 182853632 43701 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44642 43701 603 41 0 44601 0
vsize: 178568
[startup+780.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 45845 0 0 0 77877 128 0 0 25 0 1 0 421968877 189243392 45244 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46202 45244 603 41 0 46161 0
vsize: 184808
[startup+790.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 47412 0 0 0 78874 131 0 0 25 0 1 0 421968877 195551232 46811 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47742 46811 603 41 0 47701 0
vsize: 190968
[startup+800.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 48740 0 0 0 79871 134 0 0 25 0 1 0 421968877 200998912 48139 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49072 48139 603 41 0 49031 0
vsize: 196288
[startup+810.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 50667 0 0 0 80867 138 0 0 25 0 1 0 421968877 208871424 50066 4294967295 134512640 134672761 3221224576 3221223500 1075346603 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50994 50066 603 41 0 50953 0
vsize: 203976
[startup+820.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 52103 0 0 0 81864 141 0 0 25 0 1 0 421968877 214794240 51502 4294967295 134512640 134672761 3221224576 3221223672 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52440 51502 603 41 0 52399 0
vsize: 209760
[startup+830.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 52103 0 0 0 82865 141 0 0 25 0 1 0 421968877 214663168 51485 4294967295 134512640 134672761 3221224576 3221223760 134616011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52408 51485 603 41 0 52367 0
vsize: 209632
[startup+840.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 52103 0 0 0 83865 141 0 0 25 0 1 0 421968877 214663168 51485 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52408 51485 603 41 0 52367 0
vsize: 209632
[startup+850.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 52103 0 0 0 84865 141 0 0 25 0 1 0 421968877 214663168 51485 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52408 51485 603 41 0 52367 0
vsize: 209632
[startup+860.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 52103 0 0 0 85865 141 0 0 25 0 1 0 421968877 214663168 51485 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52408 51485 603 41 0 52367 0
vsize: 209632
[startup+870.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 52103 0 0 0 86865 141 0 0 25 0 1 0 421968877 214663168 51485 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52408 51485 603 41 0 52367 0
vsize: 209632
[startup+880.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 52103 0 0 0 87866 141 0 0 25 0 1 0 421968877 214663168 51485 4294967295 134512640 134672761 3221224576 3221223760 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52408 51485 603 41 0 52367 0
vsize: 209632
[startup+890.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 52103 0 0 0 88866 141 0 0 25 0 1 0 421968877 214663168 51485 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52408 51485 603 41 0 52367 0
vsize: 209632
[startup+900.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 52103 0 0 0 89866 141 0 0 25 0 1 0 421968877 214663168 51485 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52408 51485 603 41 0 52367 0
vsize: 209632
[startup+910.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 52103 0 0 0 90866 141 0 0 25 0 1 0 421968877 214663168 51485 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52408 51485 603 41 0 52367 0
vsize: 209632
[startup+920.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 52103 0 0 0 91867 141 0 0 25 0 1 0 421968877 214663168 51485 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52408 51485 603 41 0 52367 0
vsize: 209632
[startup+930.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 52103 0 0 0 92867 141 0 0 25 0 1 0 421968877 214663168 51485 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52408 51485 603 41 0 52367 0
vsize: 209632
[startup+940.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 52103 0 0 0 93867 141 0 0 25 0 1 0 421968877 214663168 51485 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52408 51485 603 41 0 52367 0
vsize: 209632
[startup+950.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 52103 0 0 0 94867 141 0 0 25 0 1 0 421968877 214663168 51485 4294967295 134512640 134672761 3221224576 3221223616 134614256 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52408 51485 603 41 0 52367 0
vsize: 209632
[startup+960.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 52103 0 0 0 95867 141 0 0 25 0 1 0 421968877 214663168 51485 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52408 51485 603 41 0 52367 0
vsize: 209632
[startup+970.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 52103 0 0 0 96868 141 0 0 25 0 1 0 421968877 214663168 51485 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52408 51485 603 41 0 52367 0
vsize: 209632
[startup+980.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 52103 0 0 0 97868 141 0 0 25 0 1 0 421968877 214663168 51485 4294967295 134512640 134672761 3221224576 3221223616 134603545 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52408 51485 603 41 0 52367 0
vsize: 209632
[startup+990.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 52103 0 0 0 98868 141 0 0 25 0 1 0 421968877 214663168 51485 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52408 51485 603 41 0 52367 0
vsize: 209632
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 52103 0 0 0 99868 141 0 0 25 0 1 0 421968877 214663168 51485 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52408 51485 603 41 0 52367 0
vsize: 209632
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 52103 0 0 0 100868 141 0 0 25 0 1 0 421968877 214663168 51485 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52408 51485 603 41 0 52367 0
vsize: 209632
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 52103 0 0 0 101869 141 0 0 25 0 1 0 421968877 214663168 51485 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52408 51485 603 41 0 52367 0
vsize: 209632
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 52103 0 0 0 102869 141 0 0 25 0 1 0 421968877 214663168 51485 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52408 51485 603 41 0 52367 0
vsize: 209632
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 52104 0 0 0 103869 141 0 0 25 0 1 0 421968877 214663168 51486 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52408 51486 603 41 0 52367 0
vsize: 209632
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 53282 0 0 0 104866 144 0 0 25 0 1 0 421968877 219541504 52664 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53599 52664 603 41 0 53558 0
vsize: 214396
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 53344 0 0 0 105866 144 0 0 25 0 1 0 421968877 219676672 52707 4294967295 134512640 134672761 3221224576 3221223616 134614333 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53632 52707 603 41 0 53591 0
vsize: 214528
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 53344 0 0 0 106866 144 0 0 25 0 1 0 421968877 219676672 52707 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53632 52707 603 41 0 53591 0
vsize: 214528
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 53344 0 0 0 107867 144 0 0 25 0 1 0 421968877 219676672 52707 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53632 52707 603 41 0 53591 0
vsize: 214528
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 53344 0 0 0 108867 144 0 0 25 0 1 0 421968877 219676672 52707 4294967295 134512640 134672761 3221224576 3221223760 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53632 52707 603 41 0 53591 0
vsize: 214528
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 53344 0 0 0 109867 144 0 0 25 0 1 0 421968877 219676672 52707 4294967295 134512640 134672761 3221224576 3221223616 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53632 52707 603 41 0 53591 0
vsize: 214528
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 53344 0 0 0 110867 144 0 0 25 0 1 0 421968877 219676672 52707 4294967295 134512640 134672761 3221224576 3221223616 134614246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53632 52707 603 41 0 53591 0
vsize: 214528
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 53344 0 0 0 111867 144 0 0 25 0 1 0 421968877 219676672 52707 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53632 52707 603 41 0 53591 0
vsize: 214528
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 53344 0 0 0 112868 144 0 0 25 0 1 0 421968877 219676672 52707 4294967295 134512640 134672761 3221224576 3221223568 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53632 52707 603 41 0 53591 0
vsize: 214528
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 53344 0 0 0 113868 144 0 0 25 0 1 0 421968877 219676672 52707 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53632 52707 603 41 0 53591 0
vsize: 214528
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 53344 0 0 0 114868 144 0 0 25 0 1 0 421968877 219676672 52707 4294967295 134512640 134672761 3221224576 3221223680 134603768 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53632 52707 603 41 0 53591 0
vsize: 214528
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 53344 0 0 0 115868 144 0 0 25 0 1 0 421968877 219676672 52707 4294967295 134512640 134672761 3221224576 3221223616 134612650 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53632 52707 603 41 0 53591 0
vsize: 214528
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 53344 0 0 0 116869 144 0 0 25 0 1 0 421968877 219676672 52707 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53632 52707 603 41 0 53591 0
vsize: 214528
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 53344 0 0 0 117869 144 0 0 25 0 1 0 421968877 219676672 52707 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53632 52707 603 41 0 53591 0
vsize: 214528
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 53344 0 0 0 118869 144 0 0 25 0 1 0 421968877 219676672 52707 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53632 52707 603 41 0 53591 0
vsize: 214528
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5768
Raw data (stat): 5768 (minisat+) R 5767 32461 32460 0 -1 0 53344 0 0 0 119869 144 0 0 25 0 1 0 421968877 219676672 52707 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53632 52707 603 41 0 53591 0
vsize: 214528
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.15 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 5768
Raw data (stat): 5768 (minisat+) Z 5767 32461 32460 0 -1 12 53345 0 0 0 119869 156 0 0 25 0 1 0 421968877 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.15
CPU time (s): 1200.26
CPU user time (s): 1198.7
CPU system time (s): 1.56476
CPU usage (%): 100.01
Max. virtual memory (Kb): 214528
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####