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/synthesis-ptl-cmos-circuits/normalized-C432.opb
MD5SUM	6292e63147fb202dc159fbf5a9ff5c77
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	4822
Optimality of the best value was proved	NO
Number of terms in the objective function	771
Biggest coefficient in the objective function	61
Number of bits for the biggest coefficient in the objective function	6
Sum of the numbers in the objective function	33355
Number of bits of the sum of numbers in the objective function	16
Biggest number in a constraint	61
Number of bits of the biggest number in a constraint	6
Biggest sum of numbers in a constraint	33355
Number of bits of the biggest sum of numbers	16
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02584
Number of variables	771
Total number of constraints	1951
Number of constraints which are clauses	1949
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	2
Minimum length of a constraint	1
Maximum length of a constraint	42
Trace number 4999

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc1 THE 2005-04-13 21:11:39 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2228 boxname=wulflinc1 idbench=248 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  6292e63147fb202dc159fbf5a9ff5c77  /oldhome/oroussel/tmp/wulflinc1/normalized-C432.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc1/normalized-C432.opb
IDLAUNCH: 2228
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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.053
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:        863052 kB
Buffers:         40000 kB
Cached:         107560 kB
SwapCached:          0 kB
Active:         106556 kB
Inactive:        44104 kB
HighTotal:      131008 kB
HighFree:        30744 kB
LowTotal:       903652 kB
LowFree:        832308 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           7196 kB
Slab:            15180 kB
Committed_AS:    92808 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 21:31:41 (client local time) WITH STATUS 10 IN 1200.23 SECONDS
stats: 2228 7 1200.23 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1905 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    1905     9279 |     635       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 7184[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:125007     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  296867   697871 |   98955       0        0     nan |  0.000 % |
c |       100 |  295982   695900 |  108850      91     3014    33.1 |  0.231 % |
c |       250 |  295982   695900 |  119735     241     3707    15.4 |  0.231 % |
c |       475 |  295982   695900 |  131709     466    10278    22.1 |  0.231 % |
c |       812 |  294997   693680 |  144880     789    11854    15.0 |  0.481 % |
c |      1320 |  294829   693311 |  159368    1295    20055    15.5 |  0.530 % |
c |      2079 |  294759   693152 |  175304    2050    88175    43.0 |  0.557 % |
c |      3218 |  294736   693103 |  192835    3187   108254    34.0 |  0.568 % |
c |      4926 |  294736   693103 |  212118    4895   153808    31.4 |  0.568 % |
c |      7488 |  294736   693103 |  233330    7457   270645    36.3 |  0.568 % |
c |     11333 |  294418   692379 |  256663   11299   313690    27.8 |  0.658 % |
c |     17100 |  294416   692375 |  282330   17065   662123    38.8 |  0.658 % |
c |     25751 |  294416   692375 |  310563   25716   813498    31.6 |  0.658 % |
c |     38728 |  294416   692375 |  341619   38693  1063269    27.5 |  0.658 % |
c |     58190 |  294408   692357 |  375781   58154  2180279    37.5 |  0.660 % |
c |     87382 |  294408   692357 |  413359   87346  7615229    87.2 |  0.660 % |
c ==============================================================================
c [1mFound solution: 7183[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:113803     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     94656 |  559505  1311181 |  186501   94615  7988355    84.4 |  0.660 % |
c |     94756 |  559505  1311181 |  205151   94715  7989688    84.4 |  0.371 % |
c |     94908 |  559505  1311181 |  225666   94867  7991107    84.2 |  0.371 % |
c |     95133 |  559505  1311181 |  248232   95092  7992665    84.1 |  0.371 % |
c |     95471 |  559505  1311181 |  273056   95430  7995137    83.8 |  0.371 % |
c |     95977 |  559505  1311181 |  300361   95936  8001388    83.4 |  0.371 % |
c |     96737 |  559283  1310683 |  330397   96692  8017970    82.9 |  0.399 % |
c |     97876 |  559283  1310683 |  363437   97831  8185359    83.7 |  0.399 % |
c |     99586 |  559257  1310623 |  399781   99539  8302907    83.4 |  0.403 % |
c |    102149 |  559257  1310623 |  439759  102102  8360519    81.9 |  0.403 % |
c |    105993 |  559257  1310623 |  483735  105946  8633190    81.5 |  0.403 % |
c |    111759 |  559222  1310544 |  532109  111705  8830790    79.1 |  0.409 % |
c ==============================================================================
c [1mFound solution: 7057[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    119088 |  560348  1313511 |  186782  119034  9225789    77.5 |  0.409 % |
c |    119188 |  560306  1313413 |  205460  119125  9227282    77.5 |  0.415 % |
c |    119340 |  560306  1313413 |  226006  119277  9228056    77.4 |  0.415 % |
c |    119566 |  560306  1313413 |  248606  119503  9231202    77.2 |  0.415 % |
c |    119903 |  560306  1313413 |  273467  119840  9234987    77.1 |  0.415 % |
c |    120409 |  560306  1313413 |  300814  120346  9241080    76.8 |  0.415 % |
c |    121168 |  560306  1313413 |  330895  121105  9251183    76.4 |  0.415 % |
c |    122307 |  560306  1313413 |  363985  122244  9271616    75.8 |  0.415 % |
c |    124015 |  560306  1313413 |  400383  123952  9431695    76.1 |  0.415 % |
c |    126577 |  560306  1313413 |  440422  126514  9508990    75.2 |  0.415 % |
c |    130421 |  559913  1312537 |  484464  130355  9685336    74.3 |  0.467 % |
c |    136187 |  559913  1312537 |  532910  136121 10247409    75.3 |  0.467 % |
c ==============================================================================
c [1mFound solution: 6620[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    137914 |  560751  1314600 |  186917  137848 10314918    74.8 |  0.467 % |
c |    138014 |  560751  1314600 |  205608  137948 10315911    74.8 |  0.466 % |
c |    138165 |  560751  1314600 |  226169  138099 10317492    74.7 |  0.466 % |
c |    138390 |  560751  1314600 |  248786  138324 10318668    74.6 |  0.466 % |
c |    138729 |  560751  1314600 |  273665  138663 10323472    74.5 |  0.466 % |
c |    139235 |  560751  1314600 |  301031  139169 10327920    74.2 |  0.466 % |
c |    139997 |  560751  1314600 |  331134  139931 10336052    73.9 |  0.466 % |
c |    141136 |  560751  1314600 |  364248  141070 10360456    73.4 |  0.466 % |
c |    142847 |  560751  1314600 |  400673  142781 10379767    72.7 |  0.466 % |
c |    145409 |  560739  1314573 |  440740  145342 10445617    71.9 |  0.468 % |
c |    149253 |  560739  1314573 |  484814  149186 10511984    70.5 |  0.468 % |
c ==============================================================================
c [1mFound solution: 6488[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    151261 |  560761  1314653 |  186920  151191 10586361    70.0 |  0.468 % |
c |    151362 |  560761  1314653 |  205612  151292 10589236    70.0 |  0.475 % |
c |    151513 |  560761  1314653 |  226173  151443 10593887    70.0 |  0.475 % |
c |    151738 |  560761  1314653 |  248790  151668 10597787    69.9 |  0.475 % |
c |    152075 |  560761  1314653 |  273669  152005 10617281    69.8 |  0.475 % |
c |    152581 |  560761  1314653 |  301036  152511 10626184    69.7 |  0.475 % |
c |    153340 |  560761  1314653 |  331140  153270 10637022    69.4 |  0.475 % |
c |    154479 |  560761  1314653 |  364254  154409 10693941    69.3 |  0.475 % |
c |    156187 |  560740  1314603 |  400679  156108 10909790    69.9 |  0.478 % |
c |    158750 |  560740  1314603 |  440747  158671 11002600    69.3 |  0.478 % |
c |    162596 |  560682  1314473 |  484822  162494 11166367    68.7 |  0.487 % |
c |    168362 |  560631  1314359 |  533304  168259 11376430    67.6 |  0.493 % |
c |    177011 |  560584  1314259 |  586635  176902 11587917    65.5 |  0.502 % |
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 -x534 -x535 -x536 -x537 -x538 x539 -x540 -x541 -x542 -x543 -x544 -x545 -x546 -x547 -x548 -x549 -x550 x551 x552 x553 -x554 -x555 -x556 -x557 -x558 -x559 -x560 -x561 -x562 -x563 -x564 -x565 -x566 -x567 -x568 -x569 -x570 -x571 -x572 x573 x574 -x575 -x576 -x577 x578 -x579 x580 -x581 x582 x583 -x584 x585 x586 x587 x588 x589 -x590 -x591 -x592 -x593 -x594 -x595 x596 -x597 x598 -x599 x600 -x601 x602 -x603 x604 -x605 -x606 -x607 -x608 -x609 -x610 x611 x612 -x613 -x614 x615 x616 x617 -x618 -x619 -x620 -x621 -x622 -x623 -x624 -x625 -x626 x627 x628 -x629 -x630 x631 x632 x633 x634 x635 -x636 x637 -x638 x639 -x640 x641 -x642 -x643 -x644 x645 x646 x647 -x648 -x649 -x650 -x651 -x652 -x653 -x654 x655 x656 x657 -x658 -x659 -x660 -x661 -x662 -x663 -x664 -x665 -x666 -x667 -x668 -x669 -x670 -x671 x672 x673 -x674 -x675 -x676 -x677 -x678 -x679 -x680 x681 -x682 -x683 -x684 -x685 -x686 -x687 -x688 -x689 -x690 -x691 -x692 -x693 -x694 -x695 -x696 x697 x698 -x699 -x700 -x701 -x702 -x703 -x704 -x705 -x706 -x707 -x708 -x709 -x710 -x711 -x712 -x713 -x714 -x715 -x716 -x717 -x71#### 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.85 0.94 0.90 2/56 15368
Raw data (stat): 15368 (runsolver) D 15367 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 364015304 1052672 99 4294967295 134512640 135381576 3221224544 3221219788 135158418 0 2147483391 7 90112 3225161850 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.87 0.94 0.90 2/56 15368
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 9676 0 0 0 977 22 0 0 25 0 1 0 364015304 41803776 9216 4294967295 134512640 134672761 3221224640 3221223840 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10206 9216 603 41 0 10165 0
vsize: 40824
[startup+20.0011 s]
Raw data (loadavg): 0.89 0.94 0.90 2/56 15368
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 9829 0 0 0 1976 23 0 0 25 0 1 0 364015304 42344448 9369 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10338 9369 603 41 0 10297 0
vsize: 41352
[startup+30.0009 s]
Raw data (loadavg): 0.91 0.94 0.90 2/56 15368
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 9935 0 0 0 2975 23 0 0 25 0 1 0 364015304 42803200 9475 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10450 9475 603 41 0 10409 0
vsize: 41800
[startup+40.0021 s]
Raw data (loadavg): 0.92 0.94 0.90 2/56 15368
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 9984 0 0 0 3975 24 0 0 25 0 1 0 364015304 43073536 9524 4294967295 134512640 134672761 3221224640 3221223800 134561238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10516 9524 603 41 0 10475 0
vsize: 42064
[startup+50.0025 s]
Raw data (loadavg): 0.93 0.94 0.90 2/56 15368
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 10084 0 0 0 4975 24 0 0 25 0 1 0 364015304 43474944 9624 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10614 9624 603 41 0 10573 0
vsize: 42456
[startup+60.0022 s]
Raw data (loadavg): 0.94 0.95 0.91 2/56 15368
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 10336 0 0 0 5975 24 0 0 25 0 1 0 364015304 44544000 9876 4294967295 134512640 134672761 3221224640 3221223744 134560248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10875 9876 603 41 0 10834 0
vsize: 43500
[startup+70.003 s]
Raw data (loadavg): 0.95 0.95 0.91 2/56 15368
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 10465 0 0 0 6974 25 0 0 25 0 1 0 364015304 45113344 10005 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11014 10005 603 41 0 10973 0
vsize: 44056
[startup+80.0038 s]
Raw data (loadavg): 0.96 0.95 0.91 2/56 15368
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 10594 0 0 0 7974 26 0 0 25 0 1 0 364015304 45645824 10134 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11144 10134 603 41 0 11103 0
vsize: 44576
[startup+90.0046 s]
Raw data (loadavg): 0.96 0.95 0.91 2/56 15368
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 10741 0 0 0 8973 27 0 0 25 0 1 0 364015304 46174208 10281 4294967295 134512640 134672761 3221224640 3221223808 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11273 10281 603 41 0 11232 0
vsize: 45092
[startup+100.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/56 15368
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 10868 0 0 0 9972 27 0 0 25 0 1 0 364015304 46833664 10408 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11434 10408 603 41 0 11393 0
vsize: 45736
[startup+110.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/56 15368
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 10953 0 0 0 10972 28 0 0 25 0 1 0 364015304 47099904 10493 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11499 10493 603 41 0 11458 0
vsize: 45996
[startup+120.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 15368
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 11064 0 0 0 11971 28 0 0 25 0 1 0 364015304 47624192 10604 4294967295 134512640 134672761 3221224640 3221223788 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11627 10604 603 41 0 11586 0
vsize: 46508
[startup+130.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 15368
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 11136 0 0 0 12971 29 0 0 25 0 1 0 364015304 47890432 10676 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11692 10676 603 41 0 11651 0
vsize: 46768
[startup+140.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 15368
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 11213 0 0 0 13970 30 0 0 25 0 1 0 364015304 48160768 10753 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11758 10753 603 41 0 11717 0
vsize: 47032
[startup+150.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 15368
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 11307 0 0 0 14970 30 0 0 25 0 1 0 364015304 48553984 10847 4294967295 134512640 134672761 3221224640 3221223824 134558839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11854 10847 603 41 0 11813 0
vsize: 47416
[startup+160.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 15368
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 11400 0 0 0 15970 30 0 0 25 0 1 0 364015304 48947200 10940 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11950 10940 603 41 0 11909 0
vsize: 47800
[startup+170.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 15368
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 11518 0 0 0 16970 31 0 0 25 0 1 0 364015304 49348608 11058 4294967295 134512640 134672761 3221224640 3221223744 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12048 11058 603 41 0 12007 0
vsize: 48192
[startup+180.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 15368
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 11627 0 0 0 17970 31 0 0 25 0 1 0 364015304 49876992 11167 4294967295 134512640 134672761 3221224640 3221223776 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12177 11167 603 41 0 12136 0
vsize: 48708
[startup+190.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 15368
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 11700 0 0 0 18970 31 0 0 25 0 1 0 364015304 50139136 11240 4294967295 134512640 134672761 3221224640 3221223776 134560720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12241 11240 603 41 0 12200 0
vsize: 48964
[startup+200.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 15368
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 11747 0 0 0 19970 31 0 0 25 0 1 0 364015304 50270208 11287 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12273 11287 603 41 0 12232 0
vsize: 49092
[startup+210.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 15368
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 11814 0 0 0 20969 32 0 0 25 0 1 0 364015304 50536448 11354 4294967295 134512640 134672761 3221224640 3221223744 134559941 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12338 11354 603 41 0 12297 0
vsize: 49352
[startup+220.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 15368
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 11887 0 0 0 21969 32 0 0 25 0 1 0 364015304 50941952 11427 4294967295 134512640 134672761 3221224640 3221223824 134558638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12437 11427 603 41 0 12396 0
vsize: 49748
[startup+230.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 15368
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 11962 0 0 0 22969 32 0 0 25 0 1 0 364015304 51208192 11502 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12502 11502 603 41 0 12461 0
vsize: 50008
[startup+240.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 15368
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 12032 0 0 0 23969 32 0 0 25 0 1 0 364015304 51474432 11572 4294967295 134512640 134672761 3221224640 3221223808 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12567 11572 603 41 0 12526 0
vsize: 50268
[startup+250.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 15368
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 12124 0 0 0 24969 33 0 0 25 0 1 0 364015304 51875840 11664 4294967295 134512640 134672761 3221224640 3221223744 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12665 11664 603 41 0 12624 0
vsize: 50660
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15368
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 12246 0 0 0 25968 33 0 0 25 0 1 0 364015304 52273152 11786 4294967295 134512640 134672761 3221224640 3221223840 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12762 11786 603 41 0 12721 0
vsize: 51048
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15368
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 12337 0 0 0 26968 34 0 0 25 0 1 0 364015304 52678656 11877 4294967295 134512640 134672761 3221224640 3221223780 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12861 11877 603 41 0 12820 0
vsize: 51444
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15370
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 12466 0 0 0 27967 35 0 0 25 0 1 0 364015304 53211136 12006 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12991 12006 603 41 0 12950 0
vsize: 51964
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15370
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 12819 0 0 0 28966 36 0 0 25 0 1 0 364015304 54685696 12359 4294967295 134512640 134672761 3221224640 3221223744 134560034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13351 12359 603 41 0 13310 0
vsize: 53404
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15370
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 13123 0 0 0 29965 37 0 0 25 0 1 0 364015304 55877632 12663 4294967295 134512640 134672761 3221224640 3221223744 134560008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13642 12663 603 41 0 13601 0
vsize: 54568
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15370
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 13327 0 0 0 30965 37 0 0 25 0 1 0 364015304 56930304 12867 4294967295 134512640 134672761 3221224640 3221223744 134559929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13899 12867 603 41 0 13858 0
vsize: 55596
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15370
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 13578 0 0 0 31964 38 0 0 25 0 1 0 364015304 57999360 13118 4294967295 134512640 134672761 3221224640 3221223744 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14160 13118 603 41 0 14119 0
vsize: 56640
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15370
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 13834 0 0 0 32964 39 0 0 25 0 1 0 364015304 59068416 13374 4294967295 134512640 134672761 3221224640 3221223776 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14421 13374 603 41 0 14380 0
vsize: 57684
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15370
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 14102 0 0 0 33963 39 0 0 25 0 1 0 364015304 60137472 13642 4294967295 134512640 134672761 3221224640 3221223808 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14682 13642 603 41 0 14641 0
vsize: 58728
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15370
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 14347 0 0 0 34963 40 0 0 25 0 1 0 364015304 61071360 13887 4294967295 134512640 134672761 3221224640 3221223840 134557916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14910 13887 603 41 0 14869 0
vsize: 59640
[startup+360.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15370
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 14561 0 0 0 35962 41 0 0 25 0 1 0 364015304 62001152 14101 4294967295 134512640 134672761 3221224640 3221223792 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15137 14101 603 41 0 15096 0
vsize: 60548
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15370
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 14778 0 0 0 36962 41 0 0 25 0 1 0 364015304 62935040 14318 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15365 14318 603 41 0 15324 0
vsize: 61460
[startup+380.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15370
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 14983 0 0 0 37961 42 0 0 25 0 1 0 364015304 63737856 14523 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15561 14523 603 41 0 15520 0
vsize: 62244
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15370
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 15226 0 0 0 38960 43 0 0 25 0 1 0 364015304 64667648 14766 4294967295 134512640 134672761 3221224640 3221223744 134560344 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15788 14766 603 41 0 15747 0
vsize: 63152
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15370
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 15452 0 0 0 39960 43 0 0 25 0 1 0 364015304 65593344 14992 4294967295 134512640 134672761 3221224640 3221223744 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16014 14992 603 41 0 15973 0
vsize: 64056
[startup+410.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15370
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 15652 0 0 0 40960 43 0 0 25 0 1 0 364015304 66400256 15192 4294967295 134512640 134672761 3221224640 3221223744 134560212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16211 15192 603 41 0 16170 0
vsize: 64844
[startup+420.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15370
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 15888 0 0 0 41960 44 0 0 25 0 1 0 364015304 67469312 15428 4294967295 134512640 134672761 3221224640 3221223776 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16472 15428 603 41 0 16431 0
vsize: 65888
[startup+430.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15370
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 16106 0 0 0 42959 45 0 0 25 0 1 0 364015304 68268032 15646 4294967295 134512640 134672761 3221224640 3221223824 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16667 15646 603 41 0 16626 0
vsize: 66668
[startup+440.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15370
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 16290 0 0 0 43959 46 0 0 25 0 1 0 364015304 69070848 15830 4294967295 134512640 134672761 3221224640 3221223744 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16863 15830 603 41 0 16822 0
vsize: 67452
[startup+450.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15370
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 16534 0 0 0 44959 46 0 0 25 0 1 0 364015304 70004736 16074 4294967295 134512640 134672761 3221224640 3221223824 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17091 16074 603 41 0 17050 0
vsize: 68364
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15370
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 16732 0 0 0 45958 46 0 0 25 0 1 0 364015304 70926336 16272 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17316 16272 603 41 0 17275 0
vsize: 69264
[startup+470.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15370
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 16835 0 0 0 46958 46 0 0 25 0 1 0 364015304 71327744 16375 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17414 16376 603 41 0 17373 0
vsize: 69656
[startup+480.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15370
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 17005 0 0 0 47958 47 0 0 25 0 1 0 364015304 71995392 16545 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17577 16545 603 41 0 17536 0
vsize: 70308
[startup+490.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15370
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 17131 0 0 0 48958 47 0 0 25 0 1 0 364015304 72531968 16671 4294967295 134512640 134672761 3221224640 3221223776 134560647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17708 16671 603 41 0 17667 0
vsize: 70832
[startup+500.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15370
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 17316 0 0 0 49957 48 0 0 25 0 1 0 364015304 73203712 16856 4294967295 134512640 134672761 3221224640 3221223840 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17872 16856 603 41 0 17831 0
vsize: 71488
[startup+510.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15370
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 17491 0 0 0 50957 49 0 0 25 0 1 0 364015304 74006528 17031 4294967295 134512640 134672761 3221224640 3221223824 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18068 17031 603 41 0 18027 0
vsize: 72272
[startup+520.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15370
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 17682 0 0 0 51957 49 0 0 25 0 1 0 364015304 74670080 17222 4294967295 134512640 134672761 3221224640 3221223808 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18230 17222 603 41 0 18189 0
vsize: 72920
[startup+530.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15370
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 17810 0 0 0 52957 49 0 0 25 0 1 0 364015304 75206656 17350 4294967295 134512640 134672761 3221224640 3221223744 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18361 17350 603 41 0 18320 0
vsize: 73444
[startup+540.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15370
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 17953 0 0 0 53956 49 0 0 25 0 1 0 364015304 75894784 17493 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18529 17493 603 41 0 18488 0
vsize: 74116
[startup+550.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15370
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 18017 0 0 0 54957 49 0 0 25 0 1 0 364015304 76161024 17557 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18594 17557 603 41 0 18553 0
vsize: 74376
[startup+560.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15370
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 18054 0 0 0 55957 50 0 0 25 0 1 0 364015304 76296192 17594 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18627 17594 603 41 0 18586 0
vsize: 74508
[startup+570.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15370
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 18147 0 0 0 56956 50 0 0 25 0 1 0 364015304 76701696 17687 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18726 17687 603 41 0 18685 0
vsize: 74904
[startup+580.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15372
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 18319 0 0 0 57955 51 0 0 25 0 1 0 364015304 77369344 17859 4294967295 134512640 134672761 3221224640 3221223808 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18889 17859 603 41 0 18848 0
vsize: 75556
[startup+590.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15372
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 26808 0 0 0 58936 70 0 0 25 0 1 0 364015304 114458624 25893 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27944 25893 603 41 0 27903 0
vsize: 111776
[startup+600.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15372
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 26936 0 0 0 59936 70 0 0 25 0 1 0 364015304 114868224 26021 4294967295 134512640 134672761 3221224640 3221223744 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28044 26021 603 41 0 28003 0
vsize: 112176
[startup+610.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15372
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 27035 0 0 0 60936 71 0 0 25 0 1 0 364015304 115273728 26120 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28143 26120 603 41 0 28102 0
vsize: 112572
[startup+620.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15372
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 27074 0 0 0 61936 71 0 0 25 0 1 0 364015304 115408896 26159 4294967295 134512640 134672761 3221224640 3221223776 134560632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28176 26159 603 41 0 28135 0
vsize: 112704
[startup+630.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15372
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 27193 0 0 0 62936 72 0 0 25 0 1 0 364015304 115810304 26278 4294967295 134512640 134672761 3221224640 3221223808 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28274 26278 603 41 0 28233 0
vsize: 113096
[startup+640.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15372
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 27285 0 0 0 63936 72 0 0 25 0 1 0 364015304 116215808 26370 4294967295 134512640 134672761 3221224640 3221223792 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28373 26370 603 41 0 28332 0
vsize: 113492
[startup+650.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15372
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 27405 0 0 0 64935 72 0 0 25 0 1 0 364015304 116617216 26490 4294967295 134512640 134672761 3221224640 3221223808 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28471 26490 603 41 0 28430 0
vsize: 113884
[startup+660.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15372
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 27515 0 0 0 65935 72 0 0 25 0 1 0 364015304 117149696 26600 4294967295 134512640 134672761 3221224640 3221223808 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28601 26600 603 41 0 28560 0
vsize: 114404
[startup+670.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15372
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 27617 0 0 0 66935 73 0 0 25 0 1 0 364015304 117547008 26702 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28698 26702 603 41 0 28657 0
vsize: 114792
[startup+680.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15372
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 27664 0 0 0 67935 73 0 0 25 0 1 0 364015304 117682176 26749 4294967295 134512640 134672761 3221224640 3221223776 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28731 26749 603 41 0 28690 0
vsize: 114924
[startup+690.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15372
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 27743 0 0 0 68935 73 0 0 25 0 1 0 364015304 118087680 26828 4294967295 134512640 134672761 3221224640 3221223776 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28830 26828 603 41 0 28789 0
vsize: 115320
[startup+700.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15372
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 27841 0 0 0 69935 74 0 0 25 0 1 0 364015304 118489088 26926 4294967295 134512640 134672761 3221224640 3221223776 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28928 26926 603 41 0 28887 0
vsize: 115712
[startup+710.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15372
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 27935 0 0 0 70934 74 0 0 25 0 1 0 364015304 118755328 27020 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28993 27020 603 41 0 28952 0
vsize: 115972
[startup+720.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15372
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 28006 0 0 0 71935 74 0 0 25 0 1 0 364015304 119025664 27091 4294967295 134512640 134672761 3221224640 3221223808 134561269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29059 27091 603 41 0 29018 0
vsize: 116236
[startup+730.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15372
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 28091 0 0 0 72935 74 0 0 25 0 1 0 364015304 119431168 27176 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29158 27176 603 41 0 29117 0
vsize: 116632
[startup+740.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15372
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 28785 0 0 0 73933 76 0 0 25 0 1 0 364015304 121733120 27745 4294967295 134512640 134672761 3221224640 3221223940 134556646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29720 27745 603 41 0 29679 0
vsize: 118880
[startup+750.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15372
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 28786 0 0 0 74933 77 0 0 25 0 1 0 364015304 121733120 27746 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29720 27746 603 41 0 29679 0
vsize: 118880
[startup+760.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15372
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 28788 0 0 0 75933 77 0 0 25 0 1 0 364015304 121733120 27748 4294967295 134512640 134672761 3221224640 3221223808 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29720 27748 603 41 0 29679 0
vsize: 118880
[startup+770.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15372
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 28834 0 0 0 76933 77 0 0 25 0 1 0 364015304 122003456 27794 4294967295 134512640 134672761 3221224640 3221223808 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29786 27794 603 41 0 29745 0
vsize: 119144
[startup+780.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15372
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 28929 0 0 0 77933 77 0 0 25 0 1 0 364015304 122400768 27889 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29883 27889 603 41 0 29842 0
vsize: 119532
[startup+790.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15372
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 29005 0 0 0 78932 77 0 0 25 0 1 0 364015304 122671104 27965 4294967295 134512640 134672761 3221224640 3221223808 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29949 27965 603 41 0 29908 0
vsize: 119796
[startup+800.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15372
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 29050 0 0 0 79932 78 0 0 25 0 1 0 364015304 122806272 28010 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29982 28010 603 41 0 29941 0
vsize: 119928
[startup+810.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15372
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 29093 0 0 0 80932 78 0 0 25 0 1 0 364015304 122941440 28053 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30015 28053 603 41 0 29974 0
vsize: 120060
[startup+820.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15372
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 29226 0 0 0 81932 78 0 0 25 0 1 0 364015304 123478016 28186 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30146 28186 603 41 0 30105 0
vsize: 120584
[startup+830.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15372
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 29287 0 0 0 82932 78 0 0 25 0 1 0 364015304 124272640 28247 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30340 28247 603 41 0 30299 0
vsize: 121360
[startup+840.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15372
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 29360 0 0 0 83932 79 0 0 25 0 1 0 364015304 124674048 28320 4294967295 134512640 134672761 3221224640 3221223788 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30438 28320 603 41 0 30397 0
vsize: 121752
[startup+850.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15372
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 29462 0 0 0 84932 79 0 0 25 0 1 0 364015304 125067264 28422 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30534 28422 603 41 0 30493 0
vsize: 122136
[startup+860.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15372
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 29573 0 0 0 85932 79 0 0 25 0 1 0 364015304 125468672 28533 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30632 28533 603 41 0 30591 0
vsize: 122528
[startup+870.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15372
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 29706 0 0 0 86931 80 0 0 25 0 1 0 364015304 126009344 28666 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30764 28666 603 41 0 30723 0
vsize: 123056
[startup+880.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15374
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 29820 0 0 0 87931 80 0 0 25 0 1 0 364015304 126545920 28780 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30895 28780 603 41 0 30854 0
vsize: 123580
[startup+890.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15374
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 29913 0 0 0 88931 80 0 0 25 0 1 0 364015304 126816256 28873 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30961 28873 603 41 0 30920 0
vsize: 123844
[startup+900.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15374
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 30214 0 0 0 89930 81 0 0 25 0 1 0 364015304 127119360 28954 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31035 28954 603 41 0 30994 0
vsize: 124140
[startup+910.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15374
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 30267 0 0 0 90930 81 0 0 25 0 1 0 364015304 127385600 29007 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31100 29007 603 41 0 31059 0
vsize: 124400
[startup+920.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15374
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 30324 0 0 0 91931 81 0 0 25 0 1 0 364015304 127516672 29064 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31132 29064 603 41 0 31091 0
vsize: 124528
[startup+930.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15374
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 30355 0 0 0 92931 81 0 0 25 0 1 0 364015304 127651840 29095 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31165 29095 603 41 0 31124 0
vsize: 124660
[startup+940.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15374
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 30400 0 0 0 93931 81 0 0 25 0 1 0 364015304 127918080 29140 4294967295 134512640 134672761 3221224640 3221223840 134557876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31230 29140 603 41 0 31189 0
vsize: 124920
[startup+950.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15374
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 30460 0 0 0 94931 81 0 0 25 0 1 0 364015304 128049152 29200 4294967295 134512640 134672761 3221224640 3221223840 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31262 29200 603 41 0 31221 0
vsize: 125048
[startup+960.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15374
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 30515 0 0 0 95931 82 0 0 25 0 1 0 364015304 128315392 29255 4294967295 134512640 134672761 3221224640 3221223764 134566018 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31327 29255 603 41 0 31286 0
vsize: 125308
[startup+970.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15374
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 30780 0 0 0 96930 83 0 0 25 0 1 0 364015304 128524288 29323 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31378 29323 603 41 0 31337 0
vsize: 125512
[startup+980.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15374
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 30812 0 0 0 97930 83 0 0 25 0 1 0 364015304 128659456 29355 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31411 29355 603 41 0 31370 0
vsize: 125644
[startup+990.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15374
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 30862 0 0 0 98930 83 0 0 25 0 1 0 364015304 128929792 29405 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31477 29405 603 41 0 31436 0
vsize: 125908
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15374
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 30911 0 0 0 99930 83 0 0 25 0 1 0 364015304 129064960 29454 4294967295 134512640 134672761 3221224640 3221223808 134560785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31510 29454 603 41 0 31469 0
vsize: 126040
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15374
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 31105 0 0 0 100929 84 0 0 25 0 1 0 364015304 129871872 29648 4294967295 134512640 134672761 3221224640 3221223776 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31707 29648 603 41 0 31666 0
vsize: 126828
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15374
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 31185 0 0 0 101929 84 0 0 25 0 1 0 364015304 130277376 29728 4294967295 134512640 134672761 3221224640 3221223808 134561269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31806 29728 603 41 0 31765 0
vsize: 127224
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15374
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 31237 0 0 0 102929 84 0 0 25 0 1 0 364015304 130408448 29780 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31838 29780 603 41 0 31797 0
vsize: 127352
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15374
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 31309 0 0 0 103930 84 0 0 25 0 1 0 364015304 130670592 29852 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31902 29852 603 41 0 31861 0
vsize: 127608
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15374
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 31369 0 0 0 104930 84 0 0 25 0 1 0 364015304 130936832 29912 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31967 29912 603 41 0 31926 0
vsize: 127868
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15374
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 31414 0 0 0 105930 84 0 0 25 0 1 0 364015304 131203072 29957 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32032 29957 603 41 0 31991 0
vsize: 128128
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15374
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 31475 0 0 0 106930 84 0 0 25 0 1 0 364015304 131338240 30018 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32065 30018 603 41 0 32024 0
vsize: 128260
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15374
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 31546 0 0 0 107930 84 0 0 25 0 1 0 364015304 131604480 30089 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32130 30089 603 41 0 32089 0
vsize: 128520
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15374
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 31688 0 0 0 108930 85 0 0 25 0 1 0 364015304 132276224 30231 4294967295 134512640 134672761 3221224640 3221223776 134560611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32294 30231 603 41 0 32253 0
vsize: 129176
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15374
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 31770 0 0 0 109930 85 0 0 25 0 1 0 364015304 132542464 30313 4294967295 134512640 134672761 3221224640 3221223776 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32359 30313 603 41 0 32318 0
vsize: 129436
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15374
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 31880 0 0 0 110929 85 0 0 25 0 1 0 364015304 132943872 30423 4294967295 134512640 134672761 3221224640 3221223812 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32457 30423 603 41 0 32416 0
vsize: 129828
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15374
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 31932 0 0 0 111929 86 0 0 25 0 1 0 364015304 133214208 30475 4294967295 134512640 134672761 3221224640 3221223808 134560849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32523 30475 603 41 0 32482 0
vsize: 130092
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15374
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 31955 0 0 0 112929 86 0 0 25 0 1 0 364015304 133349376 30498 4294967295 134512640 134672761 3221224640 3221223776 134560596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32556 30498 603 41 0 32515 0
vsize: 130224
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15374
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 31998 0 0 0 113929 86 0 0 25 0 1 0 364015304 133480448 30541 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32588 30541 603 41 0 32547 0
vsize: 130352
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15374
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 32037 0 0 0 114929 86 0 0 25 0 1 0 364015304 133615616 30580 4294967295 134512640 134672761 3221224640 3221223776 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32621 30580 603 41 0 32580 0
vsize: 130484
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15374
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 32083 0 0 0 115929 86 0 0 25 0 1 0 364015304 133750784 30626 4294967295 134512640 134672761 3221224640 3221223776 134560667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32654 30626 603 41 0 32613 0
vsize: 130616
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15374
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 32138 0 0 0 116930 86 0 0 25 0 1 0 364015304 134021120 30681 4294967295 134512640 134672761 3221224640 3221223808 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32720 30681 603 41 0 32679 0
vsize: 130880
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15376
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 32177 0 0 0 117929 87 0 0 25 0 1 0 364015304 134156288 30720 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32753 30720 603 41 0 32712 0
vsize: 131012
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15376
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 32212 0 0 0 118930 87 0 0 25 0 1 0 364015304 134291456 30755 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32786 30755 603 41 0 32745 0
vsize: 131144
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15376
Raw data (stat): 15368 (minisat+) R 15367 12452 12451 0 -1 0 32256 0 0 0 119930 87 0 0 25 0 1 0 364015304 134561792 30799 4294967295 134512640 134672761 3221224640 3221223804 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32852 30799 603 41 0 32811 0
vsize: 131408
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.91 1/56 15376
Raw data (stat): 15368 (minisat+) Z 15367 12452 12451 0 -1 12 32259 0 0 0 119930 93 0 0 25 0 1 0 364015304 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.08
CPU time (s): 1200.23
CPU user time (s): 1199.3
CPU system time (s): 0.930858
CPU usage (%): 100.013
Max. virtual memory (Kb): 131408
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####