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 6340

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc22 THE 2005-04-14 04:22:08 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4760 boxname=wulflinc22 idbench=248 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6292e63147fb202dc159fbf5a9ff5c77  /oldhome/oroussel/tmp/wulflinc22/normalized-C432.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc22/normalized-C432.opb /oldhome/oroussel/tmp/wulflinc22/normalized-C432.opb
IDLAUNCH: 4760
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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.031
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:        827304 kB
Buffers:         33448 kB
Cached:         130656 kB
SwapCached:        524 kB
Active:          50932 kB
Inactive:       116544 kB
HighTotal:      131008 kB
HighFree:         6552 kB
LowTotal:       903652 kB
LowFree:        820752 kB
SwapTotal:     2097892 kB
SwapFree:      2097368 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            34340 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 04:42:10 (client local time) WITH STATUS 10 IN 1200.12 SECONDS
stats: 4760 7 1200.12 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 |  344517   810525 |  114839       0        0     nan |  0.000 % |
c |       100 |  343497   808227 |  126322      88      715     8.1 |  0.233 % |
c |       252 |  343497   808227 |  138955     240     7901    32.9 |  0.233 % |
c |       477 |  342706   806426 |  152850     453     9788    21.6 |  0.416 % |
c |       815 |  342695   806402 |  168135     790    14840    18.8 |  0.419 % |
c |      1322 |  342695   806402 |  184949    1297    17453    13.5 |  0.419 % |
c |      2082 |  342695   806402 |  203444    2057    23385    11.4 |  0.419 % |
c |      3221 |  342249   805388 |  223788    3192    34448    10.8 |  0.524 % |
c |      4929 |  342138   805135 |  246167    4899    75760    15.5 |  0.552 % |
c |      7491 |  341734   804211 |  270784    7458   124451    16.7 |  0.655 % |
c |     11336 |  341704   804142 |  297862   11302   309559    27.4 |  0.662 % |
c |     17102 |  341696   804124 |  327649   17067   450504    26.4 |  0.664 % |
c |     25751 |  341696   804124 |  360413   25716   789767    30.7 |  0.664 % |
c ==============================================================================
c [1mFound solution: 7061[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 |     30840 |  652077  1530214 |  217359   30805  1506484    48.9 |  0.664 % |
c |     30940 |  652077  1530214 |  239094   30905  1507053    48.8 |  0.353 % |
c |     31090 |  652077  1530214 |  263004   31055  1508165    48.6 |  0.353 % |
c |     31315 |  652077  1530214 |  289304   31280  1511379    48.3 |  0.353 % |
c |     31655 |  652077  1530214 |  318235   31620  1517826    48.0 |  0.353 % |
c |     32163 |  651781  1529549 |  350058   32126  1523547    47.4 |  0.387 % |
c |     32922 |  651781  1529549 |  385064   32885  1539654    46.8 |  0.387 % |
c |     34061 |  651761  1529504 |  423571   34023  1562889    45.9 |  0.389 % |
c ==============================================================================
c [1mFound solution: 7005[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 |     35084 |  653357  1533584 |  217785   35038  1593145    45.5 |  0.389 % |
c |     35184 |  653357  1533584 |  239563   35138  1595105    45.4 |  0.412 % |
c |     35336 |  653357  1533584 |  263519   35290  1595734    45.2 |  0.412 % |
c |     35561 |  653357  1533584 |  289871   35515  1598274    45.0 |  0.412 % |
c |     35898 |  653339  1533543 |  318859   35851  1601385    44.7 |  0.414 % |
c |     36404 |  653339  1533543 |  350744   36357  1606470    44.2 |  0.414 % |
c |     37165 |  653339  1533543 |  385819   37118  1636325    44.1 |  0.414 % |
c |     38304 |  653339  1533543 |  424401   38257  1648562    43.1 |  0.414 % |
c |     40012 |  653339  1533543 |  466841   39965  1675246    41.9 |  0.414 % |
c |     42574 |  653339  1533543 |  513525   42527  1708955    40.2 |  0.414 % |
c |     46419 |  653285  1533422 |  564878   46365  1871810    40.4 |  0.421 % |
c |     52185 |  652704  1532113 |  621366   52104  1999389    38.4 |  0.492 % |
c |     60834 |  652700  1532104 |  683502   60752  2885731    47.5 |  0.492 % |
c |     73808 |  652276  1531144 |  751852   73696  3154386    42.8 |  0.544 % |
c |     93269 |  652225  1531030 |  827038   93153  4444218    47.7 |  0.550 % |
c |    122461 |  651809  1530078 |  909741  122275  5716090    46.7 |  0.604 % |
c |    166250 |  651809  1530078 | 1000716  166064  8198365    49.4 |  0.604 % |
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 -x718 -x719 #### 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.77 0.92 0.89 2/54 32131
Raw data (stat): 32131 (runsolver) R 32130 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481672765 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.0006 s]
Raw data (loadavg): 0.81 0.92 0.89 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 9903 0 0 0 975 23 0 0 25 0 1 0 481672765 42266624 9443 4294967295 134512640 134672761 3221224576 3221223712 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10319 9443 603 41 0 10278 0
vsize: 41276
[startup+20.0007 s]
Raw data (loadavg): 0.84 0.93 0.90 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 9993 0 0 0 1974 23 0 0 25 0 1 0 481672765 42668032 9533 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10417 9533 603 41 0 10376 0
vsize: 41668
[startup+30.0021 s]
Raw data (loadavg): 0.86 0.93 0.90 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 10059 0 0 0 2974 23 0 0 25 0 1 0 481672765 42930176 9599 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10481 9599 603 41 0 10440 0
vsize: 41924
[startup+40.0024 s]
Raw data (loadavg): 0.88 0.93 0.90 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 10284 0 0 0 3973 24 0 0 25 0 1 0 481672765 43864064 9824 4294967295 134512640 134672761 3221224576 3221223724 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10709 9824 603 41 0 10668 0
vsize: 42836
[startup+50.0028 s]
Raw data (loadavg): 0.90 0.93 0.90 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 10349 0 0 0 4973 24 0 0 25 0 1 0 481672765 44130304 9889 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10774 9889 603 41 0 10733 0
vsize: 43096
[startup+60.0028 s]
Raw data (loadavg): 0.91 0.93 0.90 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 10429 0 0 0 5973 25 0 0 25 0 1 0 481672765 44519424 9969 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10869 9969 603 41 0 10828 0
vsize: 43476
[startup+70.0028 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 10571 0 0 0 6972 25 0 0 25 0 1 0 481672765 45060096 10111 4294967295 134512640 134672761 3221224576 3221223776 134557913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11001 10111 603 41 0 10960 0
vsize: 44004
[startup+80.0031 s]
Raw data (loadavg): 0.94 0.94 0.90 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 10661 0 0 0 7972 26 0 0 25 0 1 0 481672765 45330432 10201 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11067 10201 603 41 0 11026 0
vsize: 44268
[startup+90.0032 s]
Raw data (loadavg): 0.95 0.94 0.90 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 10793 0 0 0 8971 27 0 0 25 0 1 0 481672765 45867008 10333 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11198 10333 603 41 0 11157 0
vsize: 44792
[startup+100.004 s]
Raw data (loadavg): 0.95 0.94 0.90 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 10880 0 0 0 9970 28 0 0 25 0 1 0 481672765 46264320 10420 4294967295 134512640 134672761 3221224576 3221223712 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11295 10420 603 41 0 11254 0
vsize: 45180
[startup+110.004 s]
Raw data (loadavg): 0.96 0.94 0.90 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 11224 0 0 0 10969 29 0 0 25 0 1 0 481672765 47607808 10764 4294967295 134512640 134672761 3221224576 3221223760 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11623 10764 603 41 0 11582 0
vsize: 46492
[startup+120.004 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 20285 0 0 0 11949 48 0 0 25 0 1 0 481672765 86687744 19370 4294967295 134512640 134672761 3221224576 3221223724 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21164 19370 603 41 0 21123 0
vsize: 84656
[startup+130.005 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 20360 0 0 0 12949 49 0 0 25 0 1 0 481672765 87080960 19445 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21260 19445 603 41 0 21219 0
vsize: 85040
[startup+140.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 20364 0 0 0 13948 50 0 0 25 0 1 0 481672765 87080960 19449 4294967295 134512640 134672761 3221224576 3221223744 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21260 19449 603 41 0 21219 0
vsize: 85040
[startup+150.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 20371 0 0 0 14948 50 0 0 25 0 1 0 481672765 87212032 19456 4294967295 134512640 134672761 3221224576 3221223776 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21292 19456 603 41 0 21251 0
vsize: 85168
[startup+160.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 20380 0 0 0 15948 50 0 0 25 0 1 0 481672765 87212032 19465 4294967295 134512640 134672761 3221224576 3221223776 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21292 19465 603 41 0 21251 0
vsize: 85168
[startup+170.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 20927 0 0 0 16946 52 0 0 25 0 1 0 481672765 88870912 19887 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21697 19887 603 41 0 21656 0
vsize: 86788
[startup+180.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 20928 0 0 0 17946 52 0 0 25 0 1 0 481672765 88870912 19888 4294967295 134512640 134672761 3221224576 3221223744 134561156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21697 19888 603 41 0 21656 0
vsize: 86788
[startup+190.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 20929 0 0 0 18945 52 0 0 25 0 1 0 481672765 88870912 19889 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21697 19889 603 41 0 21656 0
vsize: 86788
[startup+200.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 20931 0 0 0 19945 53 0 0 25 0 1 0 481672765 88870912 19891 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21697 19891 603 41 0 21656 0
vsize: 86788
[startup+210.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 20999 0 0 0 20944 54 0 0 25 0 1 0 481672765 89141248 19959 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21763 19959 603 41 0 21722 0
vsize: 87052
[startup+220.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 21067 0 0 0 21944 54 0 0 25 0 1 0 481672765 89300992 20027 4294967295 134512640 134672761 3221224576 3221223760 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21802 20027 603 41 0 21761 0
vsize: 87208
[startup+230.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 21201 0 0 0 22943 55 0 0 25 0 1 0 481672765 89837568 20161 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21933 20161 603 41 0 21892 0
vsize: 87732
[startup+240.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 21255 0 0 0 23942 56 0 0 25 0 1 0 481672765 90103808 20215 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21998 20215 603 41 0 21957 0
vsize: 87992
[startup+250.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 21309 0 0 0 24942 56 0 0 25 0 1 0 481672765 90370048 20269 4294967295 134512640 134672761 3221224576 3221223760 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22063 20269 603 41 0 22022 0
vsize: 88252
[startup+260.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 21355 0 0 0 25941 57 0 0 25 0 1 0 481672765 90505216 20315 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22096 20315 603 41 0 22055 0
vsize: 88384
[startup+270.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 21427 0 0 0 26941 57 0 0 25 0 1 0 481672765 90771456 20387 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22161 20387 603 41 0 22120 0
vsize: 88644
[startup+280.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 21508 0 0 0 27940 58 0 0 25 0 1 0 481672765 91168768 20468 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22258 20468 603 41 0 22217 0
vsize: 89032
[startup+290.013 s]
Raw data (loadavg): 1.06 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 21604 0 0 0 28940 58 0 0 25 0 1 0 481672765 91574272 20564 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22357 20564 603 41 0 22316 0
vsize: 89428
[startup+300.014 s]
Raw data (loadavg): 1.05 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 21679 0 0 0 29939 59 0 0 25 0 1 0 481672765 91840512 20639 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22422 20639 603 41 0 22381 0
vsize: 89688
[startup+310.015 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 21773 0 0 0 30939 59 0 0 25 0 1 0 481672765 92246016 20733 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22521 20733 603 41 0 22480 0
vsize: 90084
[startup+320.014 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 21918 0 0 0 31938 60 0 0 25 0 1 0 481672765 92786688 20878 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22653 20878 603 41 0 22612 0
vsize: 90612
[startup+330.015 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 22016 0 0 0 32937 61 0 0 25 0 1 0 481672765 93184000 20976 4294967295 134512640 134672761 3221224576 3221223712 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22750 20976 603 41 0 22709 0
vsize: 91000
[startup+340.016 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 22114 0 0 0 33936 61 0 0 25 0 1 0 481672765 93573120 21074 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22845 21074 603 41 0 22804 0
vsize: 91380
[startup+350.017 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 22264 0 0 0 34935 63 0 0 25 0 1 0 481672765 94236672 21224 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23007 21224 603 41 0 22966 0
vsize: 92028
[startup+360.017 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 22344 0 0 0 35934 63 0 0 25 0 1 0 481672765 94507008 21304 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23073 21304 603 41 0 23032 0
vsize: 92292
[startup+370.017 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 22406 0 0 0 36934 64 0 0 25 0 1 0 481672765 95039488 21366 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23203 21366 603 41 0 23162 0
vsize: 92812
[startup+380.017 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 22463 0 0 0 37933 65 0 0 25 0 1 0 481672765 95309824 21423 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23269 21423 603 41 0 23228 0
vsize: 93076
[startup+390.017 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 22482 0 0 0 38932 65 0 0 25 0 1 0 481672765 95309824 21442 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23269 21442 603 41 0 23228 0
vsize: 93076
[startup+400.019 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 22502 0 0 0 39932 66 0 0 25 0 1 0 481672765 95444992 21462 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23302 21462 603 41 0 23261 0
vsize: 93208
[startup+410.02 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 22524 0 0 0 40932 66 0 0 25 0 1 0 481672765 95444992 21484 4294967295 134512640 134672761 3221224576 3221223712 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23302 21484 603 41 0 23261 0
vsize: 93208
[startup+420.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 22542 0 0 0 41931 66 0 0 25 0 1 0 481672765 95580160 21502 4294967295 134512640 134672761 3221224576 3221223744 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23335 21502 603 41 0 23294 0
vsize: 93340
[startup+430.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 22563 0 0 0 42931 67 0 0 25 0 1 0 481672765 95580160 21523 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23335 21523 603 41 0 23294 0
vsize: 93340
[startup+440.021 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 22580 0 0 0 43931 67 0 0 25 0 1 0 481672765 95711232 21540 4294967295 134512640 134672761 3221224576 3221223744 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23367 21540 603 41 0 23326 0
vsize: 93468
[startup+450.022 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 22593 0 0 0 44930 67 0 0 25 0 1 0 481672765 95711232 21553 4294967295 134512640 134672761 3221224576 3221223744 134561018 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23367 21553 603 41 0 23326 0
vsize: 93468
[startup+460.022 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 22606 0 0 0 45930 68 0 0 25 0 1 0 481672765 95842304 21566 4294967295 134512640 134672761 3221224576 3221223712 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23399 21566 603 41 0 23358 0
vsize: 93596
[startup+470.023 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 22618 0 0 0 46930 68 0 0 25 0 1 0 481672765 95842304 21578 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23399 21578 603 41 0 23358 0
vsize: 93596
[startup+480.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 22629 0 0 0 47929 69 0 0 25 0 1 0 481672765 95842304 21589 4294967295 134512640 134672761 3221224576 3221223776 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23399 21589 603 41 0 23358 0
vsize: 93596
[startup+490.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 22640 0 0 0 48929 69 0 0 25 0 1 0 481672765 95977472 21600 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23432 21600 603 41 0 23391 0
vsize: 93728
[startup+500.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 22654 0 0 0 49928 70 0 0 25 0 1 0 481672765 95977472 21614 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23432 21614 603 41 0 23391 0
vsize: 93728
[startup+510.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 22676 0 0 0 50928 70 0 0 25 0 1 0 481672765 96112640 21636 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23465 21636 603 41 0 23424 0
vsize: 93860
[startup+520.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 22746 0 0 0 51927 71 0 0 25 0 1 0 481672765 96378880 21706 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23530 21706 603 41 0 23489 0
vsize: 94120
[startup+530.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 22783 0 0 0 52927 71 0 0 25 0 1 0 481672765 96514048 21743 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23563 21743 603 41 0 23522 0
vsize: 94252
[startup+540.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 22822 0 0 0 53926 72 0 0 25 0 1 0 481672765 96649216 21782 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23596 21782 603 41 0 23555 0
vsize: 94384
[startup+550.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 22885 0 0 0 54925 72 0 0 25 0 1 0 481672765 96915456 21845 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23661 21845 603 41 0 23620 0
vsize: 94644
[startup+560.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 22949 0 0 0 55924 73 0 0 25 0 1 0 481672765 97185792 21909 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23727 21909 603 41 0 23686 0
vsize: 94908
[startup+570.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 22994 0 0 0 56924 73 0 0 25 0 1 0 481672765 97320960 21954 4294967295 134512640 134672761 3221224576 3221223680 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23760 21954 603 41 0 23719 0
vsize: 95040
[startup+580.028 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 23061 0 0 0 57924 74 0 0 25 0 1 0 481672765 97583104 22021 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23824 22021 603 41 0 23783 0
vsize: 95296
[startup+590.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 23153 0 0 0 58924 74 0 0 25 0 1 0 481672765 98074624 22113 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23944 22113 603 41 0 23903 0
vsize: 95776
[startup+600.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 23228 0 0 0 59924 74 0 0 25 0 1 0 481672765 98349056 22188 4294967295 134512640 134672761 3221224576 3221223700 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24011 22188 603 41 0 23970 0
vsize: 96044
[startup+610.028 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 23328 0 0 0 60924 75 0 0 25 0 1 0 481672765 98746368 22288 4294967295 134512640 134672761 3221224576 3221223744 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24108 22288 603 41 0 24067 0
vsize: 96432
[startup+620.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 23580 0 0 0 61923 76 0 0 25 0 1 0 481672765 99831808 22540 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24373 22540 603 41 0 24332 0
vsize: 97492
[startup+630.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 23758 0 0 0 62922 77 0 0 25 0 1 0 481672765 100499456 22718 4294967295 134512640 134672761 3221224576 3221223712 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24536 22718 603 41 0 24495 0
vsize: 98144
[startup+640.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 23844 0 0 0 63921 77 0 0 25 0 1 0 481672765 100900864 22804 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24634 22804 603 41 0 24593 0
vsize: 98536
[startup+650.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 23919 0 0 0 64921 78 0 0 25 0 1 0 481672765 101171200 22879 4294967295 134512640 134672761 3221224576 3221223712 134560647 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24700 22879 603 41 0 24659 0
vsize: 98800
[startup+660.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 24074 0 0 0 65921 78 0 0 25 0 1 0 481672765 101847040 23034 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24865 23034 603 41 0 24824 0
vsize: 99460
[startup+670.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 24148 0 0 0 66920 79 0 0 25 0 1 0 481672765 102113280 23108 4294967295 134512640 134672761 3221224576 3221223712 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24930 23108 603 41 0 24889 0
vsize: 99720
[startup+680.028 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 24199 0 0 0 67920 79 0 0 25 0 1 0 481672765 102248448 23159 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24963 23159 603 41 0 24922 0
vsize: 99852
[startup+690.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 24279 0 0 0 68920 79 0 0 25 0 1 0 481672765 102641664 23239 4294967295 134512640 134672761 3221224576 3221223776 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25059 23239 603 41 0 25018 0
vsize: 100236
[startup+700.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 24424 0 0 0 69919 79 0 0 25 0 1 0 481672765 103178240 23384 4294967295 134512640 134672761 3221224576 3221223712 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25190 23384 603 41 0 25149 0
vsize: 100760
[startup+710.028 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 24501 0 0 0 70920 79 0 0 25 0 1 0 481672765 103448576 23461 4294967295 134512640 134672761 3221224576 3221223728 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25256 23461 603 41 0 25215 0
vsize: 101024
[startup+720.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 24695 0 0 0 71919 81 0 0 25 0 1 0 481672765 104255488 23655 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25453 23655 603 41 0 25412 0
vsize: 101812
[startup+730.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 24821 0 0 0 72918 81 0 0 25 0 1 0 481672765 104787968 23781 4294967295 134512640 134672761 3221224576 3221223776 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25583 23781 603 41 0 25542 0
vsize: 102332
[startup+740.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 24894 0 0 0 73918 81 0 0 25 0 1 0 481672765 105054208 23854 4294967295 134512640 134672761 3221224576 3221223712 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25648 23854 603 41 0 25607 0
vsize: 102592
[startup+750.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 24974 0 0 0 74918 81 0 0 25 0 1 0 481672765 105459712 23934 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25747 23934 603 41 0 25706 0
vsize: 102988
[startup+760.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 25030 0 0 0 75918 81 0 0 25 0 1 0 481672765 105594880 23990 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25780 23990 603 41 0 25739 0
vsize: 103120
[startup+770.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 25119 0 0 0 76918 82 0 0 25 0 1 0 481672765 106000384 24079 4294967295 134512640 134672761 3221224576 3221223680 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25879 24079 603 41 0 25838 0
vsize: 103516
[startup+780.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 25155 0 0 0 77918 82 0 0 25 0 1 0 481672765 106131456 24115 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25911 24115 603 41 0 25870 0
vsize: 103644
[startup+790.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 25212 0 0 0 78918 82 0 0 25 0 1 0 481672765 106397696 24172 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25976 24172 603 41 0 25935 0
vsize: 103904
[startup+800.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 25248 0 0 0 79918 82 0 0 25 0 1 0 481672765 106532864 24208 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26009 24208 603 41 0 25968 0
vsize: 104036
[startup+810.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 25357 0 0 0 80918 83 0 0 25 0 1 0 481672765 106930176 24317 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26106 24317 603 41 0 26065 0
vsize: 104424
[startup+820.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 25481 0 0 0 81917 84 0 0 25 0 1 0 481672765 107470848 24441 4294967295 134512640 134672761 3221224576 3221223680 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26238 24441 603 41 0 26197 0
vsize: 104952
[startup+830.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 25615 0 0 0 82916 84 0 0 25 0 1 0 481672765 108007424 24575 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26369 24575 603 41 0 26328 0
vsize: 105476
[startup+840.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 25660 0 0 0 83915 85 0 0 25 0 1 0 481672765 108142592 24620 4294967295 134512640 134672761 3221224576 3221223744 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26402 24620 603 41 0 26361 0
vsize: 105608
[startup+850.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 25718 0 0 0 84914 85 0 0 25 0 1 0 481672765 108408832 24678 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26467 24678 603 41 0 26426 0
vsize: 105868
[startup+860.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 25792 0 0 0 85914 86 0 0 25 0 1 0 481672765 108675072 24752 4294967295 134512640 134672761 3221224576 3221223712 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26532 24752 603 41 0 26491 0
vsize: 106128
[startup+870.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 25852 0 0 0 86914 86 0 0 25 0 1 0 481672765 108941312 24812 4294967295 134512640 134672761 3221224576 3221223712 134560596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26597 24812 603 41 0 26556 0
vsize: 106388
[startup+880.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 25935 0 0 0 87914 86 0 0 25 0 1 0 481672765 109207552 24895 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26662 24895 603 41 0 26621 0
vsize: 106648
[startup+890.028 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 26009 0 0 0 88914 87 0 0 25 0 1 0 481672765 109604864 24969 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26759 24969 603 41 0 26718 0
vsize: 107036
[startup+900.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 26092 0 0 0 89914 87 0 0 25 0 1 0 481672765 110391296 25052 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26951 25052 603 41 0 26910 0
vsize: 107804
[startup+910.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 26170 0 0 0 90913 87 0 0 25 0 1 0 481672765 110792704 25130 4294967295 134512640 134672761 3221224576 3221223712 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27049 25130 603 41 0 27008 0
vsize: 108196
[startup+920.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 26244 0 0 0 91913 88 0 0 25 0 1 0 481672765 111058944 25204 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27114 25204 603 41 0 27073 0
vsize: 108456
[startup+930.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 26326 0 0 0 92913 88 0 0 25 0 1 0 481672765 111325184 25286 4294967295 134512640 134672761 3221224576 3221223712 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27179 25286 603 41 0 27138 0
vsize: 108716
[startup+940.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 26408 0 0 0 93913 88 0 0 25 0 1 0 481672765 111722496 25368 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27276 25368 603 41 0 27235 0
vsize: 109104
[startup+950.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 26496 0 0 0 94912 89 0 0 25 0 1 0 481672765 112119808 25456 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27373 25456 603 41 0 27332 0
vsize: 109492
[startup+960.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 26590 0 0 0 95913 89 0 0 25 0 1 0 481672765 112398336 25550 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27441 25550 603 41 0 27400 0
vsize: 109764
[startup+970.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 26671 0 0 0 96912 89 0 0 25 0 1 0 481672765 112795648 25631 4294967295 134512640 134672761 3221224576 3221223712 134560622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27538 25631 603 41 0 27497 0
vsize: 110152
[startup+980.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 26756 0 0 0 97912 89 0 0 25 0 1 0 481672765 113078272 25716 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27607 25716 603 41 0 27566 0
vsize: 110428
[startup+990.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 26839 0 0 0 98912 90 0 0 25 0 1 0 481672765 113479680 25799 4294967295 134512640 134672761 3221224576 3221223712 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27705 25799 603 41 0 27664 0
vsize: 110820
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 26913 0 0 0 99912 90 0 0 25 0 1 0 481672765 113741824 25873 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27769 25873 603 41 0 27728 0
vsize: 111076
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 26997 0 0 0 100912 90 0 0 25 0 1 0 481672765 114139136 25957 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27866 25957 603 41 0 27825 0
vsize: 111464
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 27088 0 0 0 101912 91 0 0 25 0 1 0 481672765 114409472 26048 4294967295 134512640 134672761 3221224576 3221223712 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27932 26048 603 41 0 27891 0
vsize: 111728
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 27188 0 0 0 102912 91 0 0 25 0 1 0 481672765 114950144 26148 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28064 26148 603 41 0 28023 0
vsize: 112256
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 27291 0 0 0 103911 91 0 0 25 0 1 0 481672765 115359744 26251 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28164 26251 603 41 0 28123 0
vsize: 112656
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 27373 0 0 0 104911 92 0 0 25 0 1 0 481672765 115621888 26333 4294967295 134512640 134672761 3221224576 3221223744 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28228 26333 603 41 0 28187 0
vsize: 112912
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 27460 0 0 0 105911 92 0 0 25 0 1 0 481672765 116043776 26420 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28331 26420 603 41 0 28290 0
vsize: 113324
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 27537 0 0 0 106911 92 0 0 25 0 1 0 481672765 116305920 26497 4294967295 134512640 134672761 3221224576 3221223776 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28395 26497 603 41 0 28354 0
vsize: 113580
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 27614 0 0 0 107911 93 0 0 25 0 1 0 481672765 116572160 26574 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28460 26574 603 41 0 28419 0
vsize: 113840
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 27701 0 0 0 108911 93 0 0 25 0 1 0 481672765 116973568 26661 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28558 26661 603 41 0 28517 0
vsize: 114232
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 27786 0 0 0 109910 94 0 0 25 0 1 0 481672765 117374976 26746 4294967295 134512640 134672761 3221224576 3221223760 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28656 26746 603 41 0 28615 0
vsize: 114624
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 27882 0 0 0 110910 94 0 0 25 0 1 0 481672765 117768192 26842 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28752 26842 603 41 0 28711 0
vsize: 115008
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 27984 0 0 0 111909 95 0 0 25 0 1 0 481672765 118169600 26944 4294967295 134512640 134672761 3221224576 3221223776 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28850 26944 603 41 0 28809 0
vsize: 115400
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 28036 0 0 0 112909 95 0 0 25 0 1 0 481672765 118304768 26996 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28883 26996 603 41 0 28842 0
vsize: 115532
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 28141 0 0 0 113909 95 0 0 25 0 1 0 481672765 118710272 27101 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28982 27101 603 41 0 28941 0
vsize: 115928
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 28249 0 0 0 114909 95 0 0 25 0 1 0 481672765 119255040 27209 4294967295 134512640 134672761 3221224576 3221223776 134557822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29115 27209 603 41 0 29074 0
vsize: 116460
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 28273 0 0 0 115909 96 0 0 25 0 1 0 481672765 119255040 27233 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29115 27233 603 41 0 29074 0
vsize: 116460
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 28311 0 0 0 116909 96 0 0 25 0 1 0 481672765 119390208 27271 4294967295 134512640 134672761 3221224576 3221223700 134565980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29148 27271 603 41 0 29107 0
vsize: 116592
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 28399 0 0 0 117909 96 0 0 25 0 1 0 481672765 119791616 27359 4294967295 134512640 134672761 3221224576 3221223776 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29246 27359 603 41 0 29205 0
vsize: 116984
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 28516 0 0 0 118909 96 0 0 25 0 1 0 481672765 120324096 27476 4294967295 134512640 134672761 3221224576 3221223744 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29376 27476 603 41 0 29335 0
vsize: 117504
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 32131
Raw data (stat): 32131 (minisat+) R 32130 26298 26297 0 -1 0 28544 0 0 0 119909 96 0 0 25 0 1 0 481672765 120324096 27504 4294967295 134512640 134672761 3221224576 3221223724 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29376 27504 603 41 0 29335 0
vsize: 117504
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 1.00 0.98 0.91 1/54 32131
Raw data (stat): 32131 (minisat+) Z 32130 26298 26297 0 -1 12 28547 0 0 0 119909 102 0 0 25 0 1 0 481672765 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.12
CPU user time (s): 1199.1
CPU system time (s): 1.02184
CPU usage (%): 100.003
Max. virtual memory (Kb): 117504
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####