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 5961

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc19 THE 2005-04-14 02:30:41 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4384 boxname=wulflinc19 idbench=248 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6292e63147fb202dc159fbf5a9ff5c77  /oldhome/oroussel/tmp/wulflinc19/normalized-C432.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc19/normalized-C432.opb /oldhome/oroussel/tmp/wulflinc19/normalized-C432.opb
IDLAUNCH: 4384
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        879824 kB
Buffers:         35404 kB
Cached:          85716 kB
SwapCached:         56 kB
Active:          49608 kB
Inactive:        74484 kB
HighTotal:      131008 kB
HighFree:        41300 kB
LowTotal:       903652 kB
LowFree:        838524 kB
SwapTotal:     2097892 kB
SwapFree:      2097836 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7028 kB
Slab:            25200 kB
Committed_AS:    63708 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 02:50:43 (client local time) WITH STATUS 10 IN 1200.25 SECONDS
stats: 4384 7 1200.25 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.91 2/55 28770
Raw data (stat): 28770 (runsolver) R 28769 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481001076 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.87 0.94 0.91 2/55 28770
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 9548 0 0 0 975 23 0 0 25 0 1 0 481001076 41779200 9210 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10200 9210 603 41 0 10159 0
vsize: 40800
[startup+20.0011 s]
Raw data (loadavg): 0.89 0.94 0.91 2/55 28770
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 9704 0 0 0 1974 23 0 0 25 0 1 0 481001076 42319872 9366 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10332 9366 603 41 0 10291 0
vsize: 41328
[startup+30.0016 s]
Raw data (loadavg): 0.91 0.94 0.91 2/55 28772
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 9810 0 0 0 2974 24 0 0 25 0 1 0 481001076 42778624 9472 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10444 9472 603 41 0 10403 0
vsize: 41776
[startup+40.0017 s]
Raw data (loadavg): 0.92 0.94 0.91 2/55 28772
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 9857 0 0 0 3974 24 0 0 25 0 1 0 481001076 43048960 9519 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10510 9519 603 41 0 10469 0
vsize: 42040
[startup+50.0015 s]
Raw data (loadavg): 0.93 0.94 0.91 2/55 28772
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 9963 0 0 0 4974 24 0 0 25 0 1 0 481001076 43450368 9625 4294967295 134512640 134672761 3221224560 3221223728 134561256 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10608 9625 603 41 0 10567 0
vsize: 42432
[startup+60.002 s]
Raw data (loadavg): 0.94 0.95 0.91 2/55 28772
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 10220 0 0 0 5973 25 0 0 25 0 1 0 481001076 44519424 9882 4294967295 134512640 134672761 3221224560 3221223744 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10869 9882 603 41 0 10828 0
vsize: 43476
[startup+70.002 s]
Raw data (loadavg): 0.95 0.95 0.91 2/55 28772
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 10344 0 0 0 6973 25 0 0 25 0 1 0 481001076 45088768 10006 4294967295 134512640 134672761 3221224560 3221223728 134560808 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11008 10006 603 41 0 10967 0
vsize: 44032
[startup+80.0029 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 28772
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 10484 0 0 0 7971 27 0 0 25 0 1 0 481001076 45625344 10146 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11139 10146 603 41 0 11098 0
vsize: 44556
[startup+90.0024 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 28772
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 10622 0 0 0 8971 27 0 0 25 0 1 0 481001076 46161920 10284 4294967295 134512640 134672761 3221224560 3221223728 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11270 10284 603 41 0 11229 0
vsize: 45080
[startup+100.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 28772
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 10741 0 0 0 9971 27 0 0 25 0 1 0 481001076 46825472 10403 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11432 10403 603 41 0 11391 0
vsize: 45728
[startup+110.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 28772
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 10838 0 0 0 10971 28 0 0 25 0 1 0 481001076 47091712 10500 4294967295 134512640 134672761 3221224560 3221223696 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11497 10500 603 41 0 11456 0
vsize: 45988
[startup+120.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 28772
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 10948 0 0 0 11970 29 0 0 25 0 1 0 481001076 47632384 10610 4294967295 134512640 134672761 3221224560 3221223696 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11629 10610 603 41 0 11588 0
vsize: 46516
[startup+130.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 28772
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 11015 0 0 0 12970 29 0 0 25 0 1 0 481001076 47902720 10677 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11695 10677 603 41 0 11654 0
vsize: 46780
[startup+140.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 28772
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 11108 0 0 0 13970 29 0 0 25 0 1 0 481001076 48300032 10770 4294967295 134512640 134672761 3221224560 3221223760 134557922 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11792 10770 603 41 0 11751 0
vsize: 47168
[startup+150.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 28772
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 11197 0 0 0 14970 29 0 0 25 0 1 0 481001076 48562176 10859 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11856 10859 603 41 0 11815 0
vsize: 47424
[startup+160.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28772
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 11296 0 0 0 15970 30 0 0 25 0 1 0 481001076 48955392 10958 4294967295 134512640 134672761 3221224560 3221223664 134560347 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11952 10958 603 41 0 11911 0
vsize: 47808
[startup+170.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28772
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 11410 0 0 0 16970 30 0 0 25 0 1 0 481001076 49491968 11072 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12083 11072 603 41 0 12042 0
vsize: 48332
[startup+180.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28772
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 11517 0 0 0 17970 30 0 0 25 0 1 0 481001076 49885184 11179 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12179 11179 603 41 0 12138 0
vsize: 48716
[startup+190.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28772
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 11580 0 0 0 18970 30 0 0 25 0 1 0 481001076 50155520 11242 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12245 11242 603 41 0 12204 0
vsize: 48980
[startup+200.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28772
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 11639 0 0 0 19970 31 0 0 25 0 1 0 481001076 50417664 11301 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12309 11301 603 41 0 12268 0
vsize: 49236
[startup+210.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28772
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 11703 0 0 0 20970 31 0 0 25 0 1 0 481001076 50679808 11365 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12373 11365 603 41 0 12332 0
vsize: 49492
[startup+220.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28772
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 11770 0 0 0 21970 31 0 0 25 0 1 0 481001076 50946048 11432 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12438 11432 603 41 0 12397 0
vsize: 49752
[startup+230.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28772
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 11858 0 0 0 22970 31 0 0 25 0 1 0 481001076 51216384 11520 4294967295 134512640 134672761 3221224560 3221223696 134560640 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12504 11520 603 41 0 12463 0
vsize: 50016
[startup+240.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28772
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 11930 0 0 0 23970 31 0 0 25 0 1 0 481001076 51482624 11592 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12569 11592 603 41 0 12528 0
vsize: 50276
[startup+250.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28772
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 12043 0 0 0 24969 32 0 0 25 0 1 0 481001076 52023296 11705 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12701 11705 603 41 0 12660 0
vsize: 50804
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28772
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 12155 0 0 0 25969 32 0 0 25 0 1 0 481001076 52420608 11817 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12798 11817 603 41 0 12757 0
vsize: 51192
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28772
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 12238 0 0 0 26968 33 0 0 25 0 1 0 481001076 52826112 11900 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12897 11900 603 41 0 12856 0
vsize: 51588
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28772
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 12447 0 0 0 27967 34 0 0 25 0 1 0 481001076 53624832 12109 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13092 12109 603 41 0 13051 0
vsize: 52368
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28772
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 12796 0 0 0 28967 35 0 0 25 0 1 0 481001076 55111680 12458 4294967295 134512640 134672761 3221224560 3221223616 134565080 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13455 12458 603 41 0 13414 0
vsize: 53820
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28772
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 13080 0 0 0 29966 36 0 0 25 0 1 0 481001076 56430592 12742 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13777 12742 603 41 0 13736 0
vsize: 55108
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28772
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 13307 0 0 0 30965 36 0 0 25 0 1 0 481001076 57368576 12969 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14006 12969 603 41 0 13965 0
vsize: 56024
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28772
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 13557 0 0 0 31965 37 0 0 25 0 1 0 481001076 58429440 13219 4294967295 134512640 134672761 3221224560 3221223760 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14265 13219 603 41 0 14224 0
vsize: 57060
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28774
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 13816 0 0 0 32964 38 0 0 25 0 1 0 481001076 59490304 13478 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14524 13478 603 41 0 14483 0
vsize: 58096
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28774
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 14086 0 0 0 33963 39 0 0 25 0 1 0 481001076 60559360 13748 4294967295 134512640 134672761 3221224560 3221223560 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14785 13748 603 41 0 14744 0
vsize: 59140
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28774
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 14314 0 0 0 34963 40 0 0 25 0 1 0 481001076 61472768 13976 4294967295 134512640 134672761 3221224560 3221223696 134560566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15008 13976 603 41 0 14967 0
vsize: 60032
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28774
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 14533 0 0 0 35962 40 0 0 25 0 1 0 481001076 62390272 14195 4294967295 134512640 134672761 3221224560 3221223664 134560361 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15232 14195 603 41 0 15191 0
vsize: 60928
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28774
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 14746 0 0 0 36962 41 0 0 25 0 1 0 481001076 63201280 14408 4294967295 134512640 134672761 3221224560 3221223664 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15430 14408 603 41 0 15389 0
vsize: 61720
[startup+380.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28774
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 14974 0 0 0 37962 41 0 0 25 0 1 0 481001076 64245760 14636 4294967295 134512640 134672761 3221224560 3221223664 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15685 14636 603 41 0 15644 0
vsize: 62740
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28774
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 15224 0 0 0 38961 42 0 0 25 0 1 0 481001076 65167360 14886 4294967295 134512640 134672761 3221224560 3221223576 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15910 14886 603 41 0 15869 0
vsize: 63640
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28774
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 15412 0 0 0 39961 43 0 0 25 0 1 0 481001076 65974272 15074 4294967295 134512640 134672761 3221224560 3221223664 134560252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16107 15074 603 41 0 16066 0
vsize: 64428
[startup+410.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28774
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 15640 0 0 0 40960 43 0 0 25 0 1 0 481001076 66912256 15302 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16336 15302 603 41 0 16295 0
vsize: 65344
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28774
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 15863 0 0 0 41960 44 0 0 25 0 1 0 481001076 67846144 15525 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16564 15525 603 41 0 16523 0
vsize: 66256
[startup+430.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28774
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 16069 0 0 0 42960 44 0 0 25 0 1 0 481001076 68640768 15731 4294967295 134512640 134672761 3221224560 3221223664 134559979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16758 15731 603 41 0 16717 0
vsize: 67032
[startup+440.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28774
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 16271 0 0 0 43959 45 0 0 25 0 1 0 481001076 69443584 15933 4294967295 134512640 134672761 3221224560 3221223664 134559941 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16954 15933 603 41 0 16913 0
vsize: 67816
[startup+450.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28774
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 16492 0 0 0 44959 46 0 0 25 0 1 0 481001076 70385664 16154 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17184 16154 603 41 0 17143 0
vsize: 68736
[startup+460.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28774
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 16642 0 0 0 45959 46 0 0 25 0 1 0 481001076 71045120 16304 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17345 16304 603 41 0 17304 0
vsize: 69380
[startup+470.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28774
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 16790 0 0 0 46958 47 0 0 25 0 1 0 481001076 71577600 16452 4294967295 134512640 134672761 3221224560 3221223728 134560849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17475 16452 603 41 0 17434 0
vsize: 69900
[startup+480.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28774
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 16934 0 0 0 47958 47 0 0 25 0 1 0 481001076 72241152 16596 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17637 16596 603 41 0 17596 0
vsize: 70548
[startup+490.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28774
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 17118 0 0 0 48958 47 0 0 25 0 1 0 481001076 72912896 16780 4294967295 134512640 134672761 3221224560 3221223744 134558836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17801 16780 603 41 0 17760 0
vsize: 71204
[startup+500.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28774
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 17285 0 0 0 49957 48 0 0 25 0 1 0 481001076 73584640 16947 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17965 16947 603 41 0 17924 0
vsize: 71860
[startup+510.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28774
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 17483 0 0 0 50957 49 0 0 25 0 1 0 481001076 74375168 17145 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18158 17145 603 41 0 18117 0
vsize: 72632
[startup+520.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28774
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 17617 0 0 0 51957 49 0 0 25 0 1 0 481001076 74911744 17279 4294967295 134512640 134672761 3221224560 3221223664 134560350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18289 17279 603 41 0 18248 0
vsize: 73156
[startup+530.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28774
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 17760 0 0 0 52957 49 0 0 25 0 1 0 481001076 75603968 17422 4294967295 134512640 134672761 3221224560 3221223696 134560606 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18458 17422 603 41 0 18417 0
vsize: 73832
[startup+540.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28774
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 17861 0 0 0 53956 50 0 0 25 0 1 0 481001076 76005376 17523 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18556 17523 603 41 0 18515 0
vsize: 74224
[startup+550.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28774
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 17898 0 0 0 54956 50 0 0 25 0 1 0 481001076 76136448 17560 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18588 17560 603 41 0 18547 0
vsize: 74352
[startup+560.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28774
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 17956 0 0 0 55956 50 0 0 25 0 1 0 481001076 76406784 17618 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18654 17618 603 41 0 18613 0
vsize: 74616
[startup+570.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28774
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 18081 0 0 0 56956 51 0 0 25 0 1 0 481001076 76808192 17743 4294967295 134512640 134672761 3221224560 3221223696 134565089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18752 17743 603 41 0 18711 0
vsize: 75008
[startup+580.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28774
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 26499 0 0 0 57939 68 0 0 25 0 1 0 481001076 114151424 25831 4294967295 134512640 134672761 3221224560 3221223684 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27869 25831 603 41 0 27828 0
vsize: 111476
[startup+590.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28774
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 26592 0 0 0 58939 68 0 0 25 0 1 0 481001076 114556928 25924 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27968 25924 603 41 0 27927 0
vsize: 111872
[startup+600.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28774
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 26756 0 0 0 59939 68 0 0 25 0 1 0 481001076 115093504 26088 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28099 26088 603 41 0 28058 0
vsize: 112396
[startup+610.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28774
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 26815 0 0 0 60939 68 0 0 25 0 1 0 481001076 115363840 26147 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28165 26147 603 41 0 28124 0
vsize: 112660
[startup+620.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28774
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 26875 0 0 0 61939 68 0 0 25 0 1 0 481001076 115499008 26207 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28198 26207 603 41 0 28157 0
vsize: 112792
[startup+630.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28776
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 26985 0 0 0 62939 69 0 0 25 0 1 0 481001076 116035584 26317 4294967295 134512640 134672761 3221224560 3221223760 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28329 26317 603 41 0 28288 0
vsize: 113316
[startup+640.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28776
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 27065 0 0 0 63939 69 0 0 25 0 1 0 481001076 116305920 26397 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28395 26397 603 41 0 28354 0
vsize: 113580
[startup+650.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28776
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 27201 0 0 0 64939 69 0 0 25 0 1 0 481001076 116846592 26533 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28527 26533 603 41 0 28486 0
vsize: 114108
[startup+660.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28776
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 27339 0 0 0 65939 70 0 0 25 0 1 0 481001076 117387264 26671 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28659 26671 603 41 0 28618 0
vsize: 114636
[startup+670.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28776
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 27391 0 0 0 66939 70 0 0 25 0 1 0 481001076 117649408 26723 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28723 26723 603 41 0 28682 0
vsize: 114892
[startup+680.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28776
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 27451 0 0 0 67939 70 0 0 25 0 1 0 481001076 117915648 26783 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28788 26783 603 41 0 28747 0
vsize: 115152
[startup+690.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28776
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 27568 0 0 0 68938 71 0 0 25 0 1 0 481001076 118321152 26900 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28887 26901 603 41 0 28846 0
vsize: 115548
[startup+700.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28776
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 27640 0 0 0 69938 71 0 0 25 0 1 0 481001076 118583296 26972 4294967295 134512640 134672761 3221224560 3221223664 134560279 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28951 26972 603 41 0 28910 0
vsize: 115804
[startup+710.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28776
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 27722 0 0 0 70938 71 0 0 25 0 1 0 481001076 118988800 27054 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29050 27054 603 41 0 29009 0
vsize: 116200
[startup+720.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28776
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 27795 0 0 0 71938 71 0 0 25 0 1 0 481001076 119255040 27127 4294967295 134512640 134672761 3221224560 3221223664 134560520 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29115 27127 603 41 0 29074 0
vsize: 116460
[startup+730.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28776
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 27923 0 0 0 72938 71 0 0 25 0 1 0 481001076 119660544 27255 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29214 27255 603 41 0 29173 0
vsize: 116856
[startup+740.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28776
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 28249 0 0 0 73938 72 0 0 25 0 1 0 481001076 121167872 27581 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29582 27581 603 41 0 29541 0
vsize: 118328
[startup+750.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28776
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 28303 0 0 0 74938 72 0 0 25 0 1 0 481001076 121438208 27635 4294967295 134512640 134672761 3221224560 3221223696 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29648 27635 603 41 0 29607 0
vsize: 118592
[startup+760.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28776
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 28355 0 0 0 75938 72 0 0 25 0 1 0 481001076 121573376 27687 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29681 27687 603 41 0 29640 0
vsize: 118724
[startup+770.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28776
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 28480 0 0 0 76938 72 0 0 25 0 1 0 481001076 122105856 27812 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29811 27812 603 41 0 29770 0
vsize: 119244
[startup+780.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28776
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 28548 0 0 0 77938 73 0 0 25 0 1 0 481001076 122372096 27880 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29876 27880 603 41 0 29835 0
vsize: 119504
[startup+790.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28776
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 28602 0 0 0 78938 73 0 0 25 0 1 0 481001076 122642432 27934 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29942 27934 603 41 0 29901 0
vsize: 119768
[startup+800.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28776
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 28635 0 0 0 79938 73 0 0 25 0 1 0 481001076 122773504 27967 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29974 27967 603 41 0 29933 0
vsize: 119896
[startup+810.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28776
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 28735 0 0 0 80938 73 0 0 25 0 1 0 481001076 123179008 28067 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30073 28067 603 41 0 30032 0
vsize: 120292
[startup+820.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28776
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 28821 0 0 0 81937 74 0 0 25 0 1 0 481001076 123445248 28153 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30138 28153 603 41 0 30097 0
vsize: 120552
[startup+830.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28776
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 28896 0 0 0 82938 74 0 0 25 0 1 0 481001076 124375040 28228 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30365 28228 603 41 0 30324 0
vsize: 121460
[startup+840.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28776
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 28986 0 0 0 83937 74 0 0 25 0 1 0 481001076 124637184 28318 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30429 28318 603 41 0 30388 0
vsize: 121716
[startup+850.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28776
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 29094 0 0 0 84937 75 0 0 25 0 1 0 481001076 125165568 28426 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30558 28426 603 41 0 30517 0
vsize: 122232
[startup+860.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28776
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 29223 0 0 0 85937 75 0 0 25 0 1 0 481001076 125698048 28555 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30688 28555 603 41 0 30647 0
vsize: 122752
[startup+870.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28776
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 29348 0 0 0 86937 75 0 0 25 0 1 0 481001076 126103552 28680 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30787 28680 603 41 0 30746 0
vsize: 123148
[startup+880.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28776
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 29441 0 0 0 87937 76 0 0 25 0 1 0 481001076 126509056 28773 4294967295 134512640 134672761 3221224560 3221223760 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30886 28773 603 41 0 30845 0
vsize: 123544
[startup+890.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28776
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 29536 0 0 0 88936 76 0 0 25 0 1 0 481001076 126816256 28868 4294967295 134512640 134672761 3221224560 3221223728 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30961 28868 603 41 0 30920 0
vsize: 123844
[startup+900.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28776
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 29587 0 0 0 89936 76 0 0 25 0 1 0 481001076 127082496 28919 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31026 28919 603 41 0 30985 0
vsize: 124104
[startup+910.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28776
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 29639 0 0 0 90936 76 0 0 25 0 1 0 481001076 127213568 28971 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31058 28971 603 41 0 31017 0
vsize: 124232
[startup+920.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28776
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 29695 0 0 0 91936 76 0 0 25 0 1 0 481001076 127483904 29027 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31124 29027 603 41 0 31083 0
vsize: 124496
[startup+930.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28778
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 29724 0 0 0 92936 77 0 0 25 0 1 0 481001076 127619072 29056 4294967295 134512640 134672761 3221224560 3221223696 134560625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31157 29056 603 41 0 31116 0
vsize: 124628
[startup+940.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28778
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 29787 0 0 0 93936 77 0 0 25 0 1 0 481001076 127889408 29119 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31223 29119 603 41 0 31182 0
vsize: 124892
[startup+950.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28778
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 29830 0 0 0 94936 77 0 0 25 0 1 0 481001076 128024576 29162 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31256 29162 603 41 0 31215 0
vsize: 125024
[startup+960.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28778
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 29920 0 0 0 95936 77 0 0 25 0 1 0 481001076 128425984 29252 4294967295 134512640 134672761 3221224560 3221222448 134522954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31354 29252 603 41 0 31313 0
vsize: 125416
[startup+970.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28778
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 29946 0 0 0 96936 78 0 0 25 0 1 0 481001076 128495616 29278 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31371 29278 603 41 0 31330 0
vsize: 125484
[startup+980.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28778
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 29984 0 0 0 97936 78 0 0 25 0 1 0 481001076 128626688 29316 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31403 29316 603 41 0 31362 0
vsize: 125612
[startup+990.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28778
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 30036 0 0 0 98936 78 0 0 25 0 1 0 481001076 128897024 29368 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31469 29368 603 41 0 31428 0
vsize: 125876
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28778
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 30205 0 0 0 99936 78 0 0 25 0 1 0 481001076 129572864 29537 4294967295 134512640 134672761 3221224560 3221223664 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31634 29537 603 41 0 31593 0
vsize: 126536
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28778
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 30301 0 0 0 100936 78 0 0 25 0 1 0 481001076 129974272 29633 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31732 29633 603 41 0 31691 0
vsize: 126928
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28778
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 30367 0 0 0 101936 78 0 0 25 0 1 0 481001076 130236416 29699 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31796 29699 603 41 0 31755 0
vsize: 127184
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28778
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 30433 0 0 0 102936 78 0 0 25 0 1 0 481001076 130498560 29765 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31860 29765 603 41 0 31819 0
vsize: 127440
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28778
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 30489 0 0 0 103936 78 0 0 25 0 1 0 481001076 130633728 29821 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31893 29821 603 41 0 31852 0
vsize: 127572
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28778
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 30546 0 0 0 104937 78 0 0 25 0 1 0 481001076 130899968 29878 4294967295 134512640 134672761 3221224560 3221223728 134560825 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31958 29878 603 41 0 31917 0
vsize: 127832
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28778
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 30597 0 0 0 105937 79 0 0 25 0 1 0 481001076 131035136 29929 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31991 29929 603 41 0 31950 0
vsize: 127964
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28778
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 30672 0 0 0 106937 79 0 0 25 0 1 0 481001076 131436544 30004 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32089 30004 603 41 0 32048 0
vsize: 128356
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28778
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 30780 0 0 0 107936 79 0 0 25 0 1 0 481001076 131842048 30112 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32188 30112 603 41 0 32147 0
vsize: 128752
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28778
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 30887 0 0 0 108936 79 0 0 25 0 1 0 481001076 132247552 30219 4294967295 134512640 134672761 3221224560 3221223728 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32287 30219 603 41 0 32246 0
vsize: 129148
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28778
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 30988 0 0 0 109936 80 0 0 25 0 1 0 481001076 132648960 30320 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32385 30320 603 41 0 32344 0
vsize: 129540
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28778
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 31068 0 0 0 110936 80 0 0 25 0 1 0 481001076 132919296 30400 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32451 30400 603 41 0 32410 0
vsize: 129804
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28778
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 31093 0 0 0 111936 80 0 0 25 0 1 0 481001076 133054464 30425 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32484 30425 603 41 0 32443 0
vsize: 129936
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28778
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 31128 0 0 0 112936 80 0 0 25 0 1 0 481001076 133185536 30460 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32516 30460 603 41 0 32475 0
vsize: 130064
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28778
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 31168 0 0 0 113936 80 0 0 25 0 1 0 481001076 133320704 30500 4294967295 134512640 134672761 3221224560 3221223728 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32549 30500 603 41 0 32508 0
vsize: 130196
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28778
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 31218 0 0 0 114936 81 0 0 25 0 1 0 481001076 133591040 30550 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32615 30550 603 41 0 32574 0
vsize: 130460
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28778
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 31258 0 0 0 115936 81 0 0 25 0 1 0 481001076 133726208 30590 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32648 30590 603 41 0 32607 0
vsize: 130592
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28778
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 31314 0 0 0 116936 81 0 0 25 0 1 0 481001076 133996544 30646 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32714 30646 603 41 0 32673 0
vsize: 130856
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28778
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 31345 0 0 0 117936 81 0 0 25 0 1 0 481001076 134131712 30677 4294967295 134512640 134672761 3221224560 3221223728 134560822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32747 30677 603 41 0 32706 0
vsize: 130988
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28778
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 31385 0 0 0 118936 82 0 0 25 0 1 0 481001076 134262784 30717 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32779 30717 603 41 0 32738 0
vsize: 131116
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28778
Raw data (stat): 28770 (minisat+) R 28769 22929 22928 0 -1 0 31433 0 0 0 119936 82 0 0 25 0 1 0 481001076 134397952 30765 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32812 30765 603 41 0 32771 0
vsize: 131248
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 28778
Raw data (stat): 28770 (minisat+) Z 28769 22929 22928 0 -1 12 31436 0 0 0 119936 88 0 0 25 0 1 0 481001076 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.09
CPU time (s): 1200.25
CPU user time (s): 1199.37
CPU system time (s): 0.882865
CPU usage (%): 100.013
Max. virtual memory (Kb): 131248
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####