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/logic-synthesis/normalized-prom2.pi.opb
MD5SUM	4a63080ba3e63c3b77e35782a700d569
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	330
Optimality of the best value was proved	NO
Number of terms in the objective function	2618
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	2618
Number of bits of the sum of numbers in the objective function	12
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	2618
Number of bits of the biggest sum of numbers	12
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.71974
Number of variables	2617
Total number of constraints	1988
Number of constraints which are clauses	1988
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	30
Trace number 5811

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc6 THE 2005-04-14 01:56:21 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4207 boxname=wulflinc6 idbench=71 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4a63080ba3e63c3b77e35782a700d569  /oldhome/oroussel/tmp/wulflinc6/normalized-prom2.pi.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc6/normalized-prom2.pi.opb /oldhome/oroussel/tmp/wulflinc6/normalized-prom2.pi.opb
IDLAUNCH: 4207
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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:        890404 kB
Buffers:         36056 kB
Cached:          86216 kB
SwapCached:       2644 kB
Active:          52760 kB
Inactive:        75012 kB
HighTotal:      131008 kB
HighFree:        40908 kB
LowTotal:       903652 kB
LowFree:        849496 kB
SwapTotal:     2097136 kB
SwapFree:      2094492 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            10872 kB
Committed_AS:    63472 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 02:16:24 (client local time) WITH STATUS 10 IN 1200.42 SECONDS
stats: 4207 7 1200.42 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1966 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ================
c   -- Clauses(.)/Splits(s): ........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    1944    15270 |     648       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 438[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:173028     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  213956   510135 |   71318       0        0     nan |  0.000 % |
c |       100 |  211045   503945 |   78449      39      229     5.9 |  1.180 % |
c |       250 |  208839   499197 |   86294     148     1116     7.5 |  2.066 % |
c |       475 |  207944   497228 |   94924     357     2725     7.6 |  2.443 % |
c |       812 |  207008   495163 |  104416     672     5926     8.8 |  2.834 % |
c |      1318 |  206464   493970 |  114858    1160    11078     9.6 |  3.060 % |
c |      2077 |  205360   491537 |  126344    1885    17253     9.2 |  3.523 % |
c |      3216 |  205144   491048 |  138978    3013    43555    14.5 |  3.618 % |
c |      4924 |  204057   488637 |  152876    4673    61214    13.1 |  4.077 % |
c |      7487 |  203673   487787 |  168164    7198    99047    13.8 |  4.239 % |
c |     11331 |  203303   486968 |  184980   11020   148770    13.5 |  4.393 % |
c |     17097 |  202804   485861 |  203478   16729   230769    13.8 |  4.603 % |
c |     25747 |  202434   485027 |  223826   25347   385130    15.2 |  4.762 % |
c |     38722 |  202393   484931 |  246209   38314   743803    19.4 |  4.781 % |
c ==============================================================================
c [1mFound solution: 384[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     55429 |  202712   485691 |   67570   55017  1170088    21.3 |  4.781 % |
c |     55530 |  202712   485691 |   74327   55118  1171692    21.3 |  4.802 % |
c |     55681 |  202712   485691 |   81759   55269  1173037    21.2 |  4.802 % |
c |     55906 |  202712   485691 |   89935   55494  1175747    21.2 |  4.802 % |
c |     56245 |  202712   485691 |   98929   55833  1182500    21.2 |  4.802 % |
c |     56751 |  202670   485601 |  108822   56335  1190446    21.1 |  4.819 % |
c |     57510 |  202670   485601 |  119704   57094  1206218    21.1 |  4.819 % |
c |     58650 |  202609   485454 |  131674   58227  1234697    21.2 |  4.849 % |
c |     60358 |  202609   485454 |  144842   59935  1266362    21.1 |  4.849 % |
c |     62921 |  202607   485450 |  159326   62485  1316403    21.1 |  4.850 % |
c |     66766 |  202535   485298 |  175259   66324  1407295    21.2 |  4.878 % |
c |     72532 |  202532   485291 |  192785   72088  1549682    21.5 |  4.879 % |
c |     81183 |  202532   485291 |  212063   80739  1802391    22.3 |  4.879 % |
c |     94157 |  202380   484941 |  233269   93661  2154388    23.0 |  4.947 % |
c |    113618 |  202380   484941 |  256596  113122  2718404    24.0 |  4.947 % |
c ==============================================================================
c [1mFound solution: 357[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    132357 |  202616   485526 |   67538  131861  3547880    26.9 |  4.947 % |
c |    132457 |  202616   485526 |   74291   22469   715651    31.9 |  4.942 % |
c |    132607 |  202567   485415 |   81720   22618   717190    31.7 |  4.964 % |
c |    132833 |  202519   485302 |   89893   22841   721278    31.6 |  4.986 % |
c |    133172 |  202417   485070 |   98882   23175   726511    31.3 |  5.032 % |
c |    133678 |  202417   485070 |  108770   23681   734153    31.0 |  5.032 % |
c |    134438 |  202417   485070 |  119647   24441   745381    30.5 |  5.032 % |
c |    135577 |  202417   485070 |  131612   25580   770437    30.1 |  5.032 % |
c |    137288 |  202417   485070 |  144773   27291   796432    29.2 |  5.032 % |
c |    139850 |  202417   485070 |  159251   29853   883336    29.6 |  5.032 % |
c |    143694 |  202191   484566 |  175176   33669   945458    28.1 |  5.128 % |
c |    149461 |  202191   484566 |  192693   39436  1113693    28.2 |  5.128 % |
c |    158110 |  202104   484366 |  211963   48082  1277192    26.6 |  5.167 % |
c |    171084 |  202104   484366 |  233159   61056  1595166    26.1 |  5.167 % |
c |    190546 |  202104   484366 |  256475   80518  2225541    27.6 |  5.167 % |
c ==============================================================================
c [1mFound solution: 334[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    200645 |  202073   484317 |   67357   90596  2672519    29.5 |  5.167 % |
c |    200745 |  202073   484317 |   74092   20503   544611    26.6 |  5.269 % |
c |    200895 |  202073   484317 |   81501   20653   546522    26.5 |  5.269 % |
c |    201121 |  202073   484317 |   89652   20879   549353    26.3 |  5.269 % |
c |    201460 |  201914   483946 |   98617   21210   553386    26.1 |  5.342 % |
c |    201967 |  201872   483858 |  108479   21716   559698    25.8 |  5.358 % |
c |    202729 |  201872   483858 |  119327   22478   568831    25.3 |  5.358 % |
c |    203868 |  201872   483858 |  131259   23617   607621    25.7 |  5.358 % |
c |    205576 |  201872   483858 |  144385   25325   630272    24.9 |  5.358 % |
c |    208139 |  201831   483763 |  158824   27885   673085    24.1 |  5.377 % |
c |    211983 |  201831   483763 |  174706   31729   763066    24.0 |  5.377 % |
c |    217750 |  201831   483763 |  192177   37496  1015541    27.1 |  5.377 % |
c |    226402 |  201785   483662 |  211395   46144  1269354    27.5 |  5.397 % |
c |    239376 |  201785   483662 |  232534   59118  1608337    27.2 |  5.397 % |
c |    258837 |  201785   483662 |  255788   78579  2179490    27.7 |  5.397 % |
c |    288029 |  201785   483662 |  281366  107771  3567695    33.1 |  5.397 % |
c |    331818 |  201748   483573 |  309503  151559  6590227    43.5 |  5.415 % |
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 -x720 -x721 x722 -x723 -x724 -x725 x726 -x727 -x728 -x729 -x730 -x731 -x732 -x733 x734 -x735 -x736 -x737 -x738 -x739 -x740 -x741 -x742 x743 -x744 -x745 -x746 -x747 -x748 x749 -x750 -x751 -x752 -x753 -x754 -x755 -x756 -x757 -x758 x759 -x760 -x761 x762 -x763 -x764 -x765 -x766 -x767 x768 -x769 -x770 -x771 -x772 -x773 -x774 -x775 -x776 x777 -x778 -x779 -x780 -x781 x782 -x783 -x784 -x785 -x786 -x787 -x788 -x789 -x790 -x791 -x792 x793 -x794 -x795 -x796 -x797 -x798 -x799 -x800 -x801 -x802 -x803 -x804 -x805 -x806 -x807 x808 -x809 -x810 -x811 -x812 -x813 -x814 -x815 -x816 -x817 -x818 -x819 -x820 -x821 -x822 x823 -x824 -x825 -x826 -x827 -x828 -x829 -x830 -x831 -x832 -x833 -x834 -x835 -x836 -x837 -x838 -x839 -x840 x841 -x842 -x843 -x844 -x845 -x846 -x847 -x848 -x849 -x850 -x851 -x852 -x853 -x854 -x855 x856 -x857 -x858 -x859 -x860 -x861 -x862 -x863 x864 -x865 -x866 -x867 -x868 -x869 -x870 -x871 -x872 -x873 -x874 -x875 x876 x877 -x878 -x879 -x880 -x881 -x882 -x883 -x884 -x885 -x886 x887 -x888 -x889 -x890 -x891 -x892 x893 -x894 x895 -x896 -x897 -x898 x899 x900 -x901 -x902 -x903 -x904 -x905 -x906 -x907 -x908 x909 -x910 -x911 -x912 -x913 -x914 -x915 -x916 -x917 -x918 -x919 -x920 -x921 -x922 -x923 x924 -x925 x926 -x927 -x928 -x929 -x930 -x931 -x932 -x933 -x934 x935 -x936 -x937 -x938 -x939 -x940 -x941 x942 -x943 -x944 x945 -x946 -x947 -x948 -x949 -x950 -x951 -x952 -x953 -x954 -x955 x956 -x957 -x958 -x959 -x960 -x961 x962 -x963 -x964 -x965 x966 -x967 -x968 -x969 -x970 -x971 -x972 -x973 -x974 -x975 -x976 -x977 -x978 -x979 x980 -x981 -x982 -x983 x984 -x985 -x986 -x987 -x988 -x989 -x990 -x991 -x992 -x993 -x994 -x995 -x996 -x997 -x998 x999 -x1000 -x1001 -x1002 -x1003 -x1004 -x1005 -x1006 -x1007 -x1008 -x1009 -x1010 -x1011 -x1012 x1013 -x1014 -x1015 -x1016 -x1017 -x1018 -x1019 -x1020 -x1021 -x1022 -x1023 x1024 -x1025 -x1026 -x1027 -x1028 -x1029 -x1030 -x1031 -x1032 -x1033 -x1034 -x1035 -x1036 -x1037 -x1038 x1039 -x1040 -x1041 -x1042 -x1043 x1044 -x1045 -x1046 -x1047 -x1048 -x1049 -x1050 -x1051 -x1052 x1053 x1054 -x1055 -x1056 -x1057 -x1058 -x1059 -x1060 -x1061 -x1062 -x1063 -x1064 -x1065 x1066 -x1067 -x1068 -x1069 -x1070 -x1071 -x1072 -x1073 x1074 -x1075 -x1076 -x1077 -x1078 -x1079 -x1080 x1081 x1082 x1083 -x1084 -x1085 -x1086 -x1087 x1088 -x1089 -x1090 -x1091 -x1092 -x1093 -x1094 x1095 -x1096 x1097 -x1098 -x1099 -x1100 -x1101 -x1102 -x1103 -x1104 x1105 -x1106 -x1107 -x1108 x1109 -x1110 x1111 -x1112 -x1113 -x1114 -x1115 -x1116 -x1117 -x1118 -x1119 -x1120 -x1121 x1122 x1123 -x1124 -x1125 -x1126 -x1127 x1128 -x1129 -x1130 -x1131 -x1132 -x1133 -x1134 -x1135 -x1136 -x1137 -x1138 -x1139 -x1140 -x1141 -x1142 -x1143 -x1144 -x1145 -x1146 -x1147 x1148 -x1149 -x1150 -x1151 -x1152 -x1153 -x1154 -x1155 -x1156 -x1157 x1158 -x1159 x1160 -x1161 -x1162 -x1163 -x1164 x1165 x1166 -x1167 x1168 -x1169 -x1170 -x1171 -x1172 x1173 -x1174 -x1175 -x1176 -x1177 -x1178 -x1179 x1180 -x1181 x1182 -x1183 x1184 -x1185 -x1186 -x1187 -x1188 -x1189 -x1190 -x1191 x1192 -x1193 x1194 -x1195 x1196 -x1197 -x1198 -x1199 -x1200 -x1201 x1202 -x1203 -x1204 x1205 -x1206 x1207 -x1208 -x1209 x1210 -x1211 -x1212 -x1213 -x1214 x1215 -x1216 -x1217 x1218 -x1219 x1220 -x1221 -x1222 -x1223 -x1224 -x1225 -x1226 -x1227 -x1228 -x1229 -x1230 -x1231 -x1232 x1233 -x1234 -x1235 -x1236 -x1237 x1238 -x1239 -x1240 -x1241 x1242 -x1243 -x1244 x1245 -x1246 -x1247 -x1248 -x1249 -x1250 -x1251 -x1252 -x1253 -x1254 -x1255 -x1256 -x1257 -x1258 -x1259 -x1260 -x1261 -x1262 -x1263 -x1264 -x1265 x1266 -x1267 -x1268 x1269 -x1270 -x1271 -x1272 -x1273 -x1274 -x1275 -x1276 x1277 -x1278 -x1279 -x1280 -x1281 x1282 -x1283 -x1284 -x1285 -x1286 -x1287 -x1288 -x1289 -x1290 -x1291 -x1292 -x1293 -x1294 -x1295 -x1296 x1297 -x1298 -x1299 -x1300 -x1301 -x1302 -x1303 -x1304 -x1305 -x1306 -x1307 -x1308 -x1309 -x1310 -x1311 -x1312 -x1313 -x1314 -x1315 -x1316 -x1317 -x1318 -x1319 -x1320 x1321 -x1322 -x1323 -x1324 -x1325 -x1326 x1327 -x1328 -x1329 -x1330 -x1331 -x1332 -x1333 -x1334 -x1335 -x1336 x1337 -x1338 -x1339 -x1340 -x1341 -x1342 -x1343 x1344 -x1345 -x1346 -x1347 -x1348 -x1349 -x1350 -x1351 -x1352 -x1353 -x1354 -x1355 x1356 -x1357 x1358 -x1359 -x1360 -x1361 -x1362 -x1363 -x1364 -x1365 -x1366 -x1367 -x1368 -x1369 -x1370 -x1371 -x1372 -x1373 -x1374 -x1375 -x1376 -x1377 -x1378 -x1379 -x1380 -x1381 -x1382 x1383 -x1384 -x1385 -x1386 -x1387 -x1388 -x1389 -x1390 -x1391 -x1392 -x1393 -x1394 -x1395 -x1396 -x1397 -x1398 -x1399 -x1400 -x1401 -x1402 -x1403 -x1404 -x1405 -x1406 -x1407 x1408 -x1409 -x1410 -x1411 -x1412 -x1413 -x1414 -x1415 -x1416 -x1417 -x1418 -x1419 -x1420 -x1421 x1422 -x1423 -x1424 -x1425 -x1426 -x1427 -x1428 -x1429 -x1430 -x1431 -x1432 -x1433 -x1434 -x1435 -x1436 -x1437 -x1438 x1439 -x1440 -x1441 -x1442 -x1443 -x1444 -x1445 -x1446 -x1447 -x1448 -x1449 -x1450 x1451 -x1452 -x1453 -x1454 -x1455 -x1456 -x1457 -x1458 -x1459 -x1460 -x1461 -x1462 -x1463 -x1464 -x1465 -x1466 x1467 -x1468 -x1469 -x1470 -x1471 -x1472 -x1473 -x1474 x1475 -x1476 -x1477 -x1478 -x1479 -x1480 -x1481 -x1482 -x1483 -x1484 -x1485 -x1486 -x1487 -x1488 -x1489 -x1490 -x1491 -x1492 -x1493 x1494 x1495 -x1496 -x1497 x1498 x1499 -x1500 -x1501 -x1502 -x1503 -x1504 -x1505 -x1506 -x1507 -x1508 -x1509 -x1510 -x1511 -x1512 -x1513 -x1514 -x1515 -x1516 -x1517 -x1518 -x1519 -x1520 x1521 -x1522 -x1523 -x1524 -x1525 -x1526 -x1527 -x1528 x1529 -x1530 -x1531 -x1532 -x1533 -x1534 -x1535 -x1536 -x1537 -x1538 -x1539 -x1540 -x1541 -x1542 -x1543 -x1544 x1545 -x1546 -x1547 -x1548 x1549 -x1550 -x1551 -x1552 -x1553 -x1554 -x1555 x1556 x1557 -x1558 -x1559 -x1560 -x1561 -x1562 -x1563 -x1564 -x1565 -x1566 -x1567 -x1568 -x1569 x1570 -x1571 -x1572 -x1573 -x1574 -x1575 -x1576 -x1577 -x1578 -x1579 -x1580 -x1581 -x1582 -x1583 x1584 -x1585 -x1586 -x1587 -x1588 -x1589 -x1590 -x1591 -x1592 -x1593 -x1594 -x1595 x1596 -x1597 -x1598 -x1599 -x1600 -x1601 -x1602 -x1603 -x1604 -x1605 -x1606 x1607 x1608 x1609 -x1610 x1611 -x1612 -x1613 -x1614 -x1615 -x1616 -x1617 -x1618 -x1619 -x1620 -x1621 x1622 -x1623 -x1624 -x1625 x1626 -x1627 -x1628 -x1629 -x1630 -x1631 -x1632 -x1633 x1634 -x1635 -x1636 -x1637 -x1638 -x1639 -x1640 -x1641 -x1642 -x1643 -x1644 -x1645 -x1646 -x1647 -x1648 -x1649 x1650 x1651 -x1652 -x1653 -x1654 x1655 -x1656 -x1657 -x1658 -x1659 -x1660 -x1661 -x1662 -x1663 -x1664 -x1665 -x1666 -x1667 -x1668 -x1669 -x1670 -x1671 -x1672 x1673 -x1674 -x1675 -x1676 x1677 -x1678 -x1679 -x1680 -x1681 -x1682 -x1683 x1684 -x1685 -x1686 -x1687 -x1688 -x1689 -x1690 -x1691 -x1692 -x1693 -x1694 x1695 -x1696 -x1697 -x1698 -x1699 -x1700 -x1701 x1702 -x1703 -x1704 -x1705 -x1706 x1707 -x1708 -x1709 -x1710 -x1711 -x1712 -x1713 x1714 -x1715 -x1716 -x1717 x1718 x1719 x1720 -x1721 -x1722 -x1723 -x1724 x1725 -x1726 x1727 -x1728 -x1729 -x1730 -x1731 -x1732 -x1733 -x1734 -x1735 -x1736 -x1737 -x1738 -x1739 -x1740 -x1741 -x1742 x1743 -x1744 -x1745 -x1746 -x1747 -x1748 -x1749 -x1750 -x1751 -x1752 -x1753 -x1754 -x1755 -x1756 -x1757 -x1758 -x1759 -x1760 -x1761 -x1762 -x1763 -x1764 -x1765 x1766 -x1767 -x1768 -x1769 -x1770 -x1771 -x1772 -x1773 -x1774 -x1775 -x1776 -x1777 -x1778 -x1779 -x1780 -x1781 -x1782 -x1783 -x1784 -x1785 -x1786 -x1787 -x1788 -x1789 -x1790 -x1791 -x1792 -x1793 -x1794 x1795 -x1796 -x1797 -x1798 -x1799 -x1800 x1801 -x1802 -x1803 x1804 -x1805 -x1806 -x1807 -x1808 -x1809 -x1810 x1811 -x1812 -x1813 -x1814 -x1815 -x1816 -x1817 -x1818 -x1819 x1820 -x1821 -x1822 -x1823 -x1824 -x1825 -x1826 x1827 -x1828 -x1829 -x1830 -x1831 -x1832 -x1833 -x1834 -x1835 -x1836 x1837 -x1838 -x1839 x1840 -x1841 -x1842 -x1843 -x1844 -x1845 -x1846 -x1847 -x1848 -x1849 x1850 -x1851 -x1852 -x1853 -x1854 -x1855 -x1856 x1857 -x1858 -x1859 -x1860 -x1861 -x1862 -x1863 -x1864 -x1865 -x1866 x1867 -x1868 -x1869 -x1870 -x1871 -x1872 -x1873 -x1874 -x1875 x1876 -x1877 -x1878 -x1879 -x1880 -x1881 x1882 -x1883 -x1884 -x1885 -x1886 -x1887 -x1888 -x1889 x1890 -x1891 -x1892 -x1893 -x1894 -x1895 x1896 -x1897 -x1898 -x1899 -x1900 -x1901 -x1902 -x1903 -x1904 -x1905 -x1906 -x1907 -x1908 -x1909 -x1910 -x1911 -x1912 -x1913 x1914 -x1915 -x1916 -x1917 -x1918 -x1919 x1920 -x1921 -x1922 -x1923 -x1924 -x1925 x1926 -x1927 -x1928 -x1929 -x1930 -x1931 -x1932 -x1933 -x1934 -x1935 -x1936 -x1937 -x1938 -x1939 -x1940 -x1941 -x1942 x1943 -x1944 -x1945 -x1946 -x1947 x1948 -x1949 -x1950 -x1951 x1952 -x1953 -x1954 -x1955 -x1956 -x1957 -x1958 -x1959 -x1960 -x1961 x1962 -x1963 -x1964 -x1965 -x1966 -x1967 x1968 -x1969 -x1970 -x1971 -x1972 -x1973 -x1974 x1975 -x1976 -x1977 -x1978 -x1979 -x1980 -x1981 -x1982 x1983 -x1984 -x1985 -x1986 x1987 -x1988 -x1989 -x1990 -x1991 -x1992 -x1993 -x1994 x1995 -x1996 -x1997 -x1998 -x1999 -x2000 -x2001 -x2002 x2003 -x2004 -x2005 -x2006 -x2007 -x2008 -x2009 x2010 -x2011 -x2012 -x2013 -x2014 -x2015 -x2016 x2017 -x2018 x2019 -x2020 x2021 -x2022 -x2023 -x2024 -x2025 -x2026 -x2027 -x2028 -x2029 -x2030 -x2031 -x2032 -x2033 -x2034 -x2035 -x2036 -x2037 -x2038 x2039 -x2040 -x2041 -x2042 -x2043 -x2044 -x2045 -x2046 -x2047 x2048 -x2049 -x2050 -x2051 x2052 x2053 x2054 -x2055 -x2056 -x2057 -x2058 -x2059 -x2060 -x2061 -x2062 -x2063 -x2064 -x2065 -x2066 -x2067 -x2068 -x2069 -x2070 -x2071 -x2072 -x2073 -x2074 -x2075 x2076 -x2077 -x2078 -x2079 -x2080 -x2081 -x2082 -x2083 -x2084 x2085 -x2086 -x2087 -x2088 -x2089 -x2090 -x2091 x2092 -x2093 -x2094 -x2095 -x2096 -x2097 -x2098 -x2099 -x2100 -x2101 -x2102 -x2103 -x2104 -x2105 -x2106 -x2107 -x2108 -x2109 -x2110 -x2111 -x2112 -x2113 -x2114 -x2115 x2116 -x2117 -x2118 x2119 -x2120 -x2121 -x2122 -x2123 -x2124 -x2125 -x2126 -x2127 x2128 -x2129 -x2130 -x2131 -x2132 -x2133 -x2134 -x2135 -x2136 x2137 -x2138 -x2139 -x2140 -x2141 -x2142 -x2143 -x2144 -x2145 -x2146 x2147 -x2148 -x2149 -x2150 -x2151 -x2152 -x2153 -x2154 x2155 -x2156 -x2157 -x2158 x2159 -x2160 -x2161 -x2162 -x2163 x2164 x2165 -x2166 -x2167 -x2168 -x2169 -x2170 -x2171 -x2172 -x2173 -x2174 -x2175 -x2176 -x2177 -x2178 -x2179 -x2180 -x2181 -x2182 -x2183 -x2184 x2185 -x2186 x2187 -x2188 -x2189 -x2190 -x2191 -x2192 x2193 -x2194 -x2195 -x2196 x2197 x2198 -x2199 -x2200 -x2201 -x2202 -x2203 -x2204 -x2205 -x2206 -x2207 -x2208 -x2209 -x2210 -x2211 x2212 -x2213 -x2214 -x2215 -x2216 -x2217 x2218 -x2219 -x2220 -x2221 -x2222 x2223 -x2224 -x2225 -x2226 -x2227 -x2228 -x2229 -x2230 -x2231 -x2232 x2233 -x2234 -x2235 -x2236 x2237 -x2238 -x2239 -x2240 -x2241 x2242 -x2243 x2244 -x2245 -x2246 -x2247 -x2248 x2249 -x2250 -x2251 -x2252 x2253 -x2254 -x2255 -x2256 -x2257 x2258 -x2259 -x2260 -x2261 -x2262 -x2263 x2264 -x2265 -x2266 x2267 -x2268 x2269 -x2270 -x2271 -x2272 -x2273 x2274 -x2275 -x2276 -x2277 -x2278 -x2279 -x2280 -x2281 x2282 -x2283 -x2284 -x2285 -x2286 -x2287 -x2288 -x2289 -x2290 -x2291 -x2292 x2293 -x2294 x2295 -x2296 -x2297 -x2298 -x2299 -x2300 -x2301 -x2302 -x2303 -x2304 x2305 -x2306 -x2307 -x2308 -x2309 -x2310 -x2311 -x2312 -x2313 -x2314 -x2315 -x2316 x2317 -x2318 x2319 -x2320 -x2321 -x2322 -x2323 -x2324 x2325 -x2326 -x2327 -x2328 x2329 -x2330 -x2331 -x2332 -x2333 x2334 -x2335 -x2336 x2337 -x2338 -x2339 -x2340 -x2341 x2342 -x2343 -x2344 -x2345 -x2346 -x2347 -x2348 x2349 x2350 -x2351 x2352 -x2353 -x2354 -x2355 -x2356 x2357 -x2358 -x2359 -x2360 -x2361 -x2362 x2363 -x2364 -x2365 x2366 -x2367 -x2368 -x2369 -x2370 -x2371 -x2372 -x2373 x2374 -x2375 x2376 x2377 -x2378 x2379 -x2380 -x2381 x2382 -x2383 -x2384 -x2385 -x2386 -x2387 -x2388 -x2389 -x2390 -x2391 x2392 -x2393 -x2394 -x2395 -x2396 -x2397 -x2398 -x2399 -x2400 x2401 -x2402 -x2403 -x2404 -x2405 -x2406 -x2407 -x2408 x2409 -x2410 -x2411 x2412 x2413 x2414 -x2415 -x2416 x2417 -x2418 -x2419 -x2420 -x2421 x2422 -x2423 -x2424 -x2425 -x2426 -x2427 x2428 -x2429 -x2430 -x2431 x2432 -x2433 -x2434 x2435 -x2436 -x2437 x2438 -x2439 -x2440 x2441 -x2442 -x2443 x2444 x2445 -x2446 x2447 -x2448 -x2449 -x2450 -x2451 -x2452 -x2453 -x2454 -x2455 -x2456 x2457 -x2458 -x2459 -x2460 -x2461 x2462 -x2463 -x2464 -x2465 -x2466 -x2467 -x2468 -x2469 -x2470 -x2471 -x2472 -x2473 x2474 -x2475 -x2476 -x2477 -x2478 -x2479 -x2480 -x2481 -x2482 x2483 -x2484 -x2485 -x2486 -x2487 -x2488 x2489 -x2490 -x2491 -x2492 x2493 -x2494 -x2495 -x2496 -x2497 -x2498 x2499 -x2500 -x2501 -x2502 -x2503 -x2504 x2505 -x2506 -x2507 -x2508 -x2509 x2510 -x2511 -x2512 -x2513 -x2514 -x2515 -x2516 -x2517 -x2518 x2519 -x2520 -x2521 -x2522 -x2523 -x2524 -x2525 -x2526 -x2527 x2528 -x2529 -x2530 -x2531 x2532 -x2533 -x2534 -x2535 x2536 -x2537 -x2538 #### 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.84 0.94 0.91 2/54 1583
Raw data (stat): 1583 (runsolver) R 1582 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422577994 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/54 1583
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 11132 0 0 0 968 30 0 0 25 0 1 0 422577994 53743616 10465 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13121 10465 603 41 0 13080 0
vsize: 52484
[startup+20.0001 s]
Raw data (loadavg): 0.89 0.94 0.91 2/54 1583
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 11255 0 0 0 1967 30 0 0 25 0 1 0 422577994 54276096 10588 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13251 10588 603 41 0 13210 0
vsize: 53004
[startup+30.0006 s]
Raw data (loadavg): 0.90 0.94 0.91 2/54 1583
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 11359 0 0 0 2967 30 0 0 25 0 1 0 422577994 54681600 10692 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13350 10692 603 41 0 13309 0
vsize: 53400
[startup+40.0005 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 1583
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 11423 0 0 0 3967 31 0 0 25 0 1 0 422577994 54951936 10756 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13416 10756 603 41 0 13375 0
vsize: 53664
[startup+50.0003 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 1583
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 11500 0 0 0 4967 31 0 0 25 0 1 0 422577994 55222272 10833 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13482 10833 603 41 0 13441 0
vsize: 53928
[startup+60.0008 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 1583
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 11568 0 0 0 5967 31 0 0 25 0 1 0 422577994 55533568 10901 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13558 10901 603 41 0 13517 0
vsize: 54232
[startup+70.0012 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 1583
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 11641 0 0 0 6967 31 0 0 25 0 1 0 422577994 55799808 10974 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13623 10974 603 41 0 13582 0
vsize: 54492
[startup+80.0018 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 1583
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 11707 0 0 0 7966 32 0 0 25 0 1 0 422577994 56070144 11040 4294967295 134512640 134672761 3221224560 3221223704 134560555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13689 11040 603 41 0 13648 0
vsize: 54756
[startup+90.0022 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 1583
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 11773 0 0 0 8966 32 0 0 25 0 1 0 422577994 56360960 11106 4294967295 134512640 134672761 3221224560 3221223684 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13760 11106 603 41 0 13719 0
vsize: 55040
[startup+100.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 1583
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 11844 0 0 0 9966 32 0 0 25 0 1 0 422577994 56631296 11177 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13826 11177 603 41 0 13785 0
vsize: 55304
[startup+110.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 1583
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 11925 0 0 0 10967 32 0 0 25 0 1 0 422577994 56901632 11258 4294967295 134512640 134672761 3221224560 3221223704 134560630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13892 11258 603 41 0 13851 0
vsize: 55568
[startup+120.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 1583
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 12111 0 0 0 11967 33 0 0 25 0 1 0 422577994 57708544 11444 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14089 11444 603 41 0 14048 0
vsize: 56356
[startup+130.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 1583
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 12192 0 0 0 12967 33 0 0 25 0 1 0 422577994 57978880 11525 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14155 11525 603 41 0 14114 0
vsize: 56620
[startup+140.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 1583
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 12276 0 0 0 13967 33 0 0 25 0 1 0 422577994 58384384 11609 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14254 11609 603 41 0 14213 0
vsize: 57016
[startup+150.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 1583
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 12344 0 0 0 14967 34 0 0 25 0 1 0 422577994 58781696 11677 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14351 11677 603 41 0 14310 0
vsize: 57404
[startup+160.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1583
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 12424 0 0 0 15967 34 0 0 25 0 1 0 422577994 59052032 11757 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14417 11757 603 41 0 14376 0
vsize: 57668
[startup+170.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1583
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 12506 0 0 0 16967 34 0 0 25 0 1 0 422577994 59457536 11839 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14516 11839 603 41 0 14475 0
vsize: 58064
[startup+180.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1583
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 12588 0 0 0 17968 34 0 0 25 0 1 0 422577994 59723776 11921 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14581 11921 603 41 0 14540 0
vsize: 58324
[startup+190.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1583
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 12889 0 0 0 18967 35 0 0 25 0 1 0 422577994 60936192 12222 4294967295 134512640 134672761 3221224560 3221223760 134557822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14877 12222 603 41 0 14836 0
vsize: 59508
[startup+200.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1583
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 13004 0 0 0 19967 35 0 0 25 0 1 0 422577994 61337600 12337 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14975 12337 603 41 0 14934 0
vsize: 59900
[startup+210.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1583
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 13073 0 0 0 20967 35 0 0 25 0 1 0 422577994 61607936 12406 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15041 12406 603 41 0 15000 0
vsize: 60164
[startup+220.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1583
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 13386 0 0 0 21966 37 0 0 25 0 1 0 422577994 63426560 12705 4294967295 134512640 134672761 3221224560 3221223696 134565076 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15485 12705 603 41 0 15444 0
vsize: 61940
[startup+230.004 s]
Raw data (loadavg): 1.07 0.98 0.91 2/54 1636
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 13440 0 0 0 22966 37 0 0 25 0 1 0 422577994 63696896 12759 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15551 12759 603 41 0 15510 0
vsize: 62204
[startup+240.005 s]
Raw data (loadavg): 1.06 0.98 0.91 2/54 1636
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 13546 0 0 0 23965 38 0 0 25 0 1 0 422577994 64102400 12865 4294967295 134512640 134672761 3221224560 3221223684 134566077 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15650 12865 603 41 0 15609 0
vsize: 62600
[startup+250.005 s]
Raw data (loadavg): 1.05 0.98 0.91 2/54 1636
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 13627 0 0 0 24966 38 0 0 25 0 1 0 422577994 64507904 12946 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15749 12946 603 41 0 15708 0
vsize: 62996
[startup+260.006 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 1636
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 13766 0 0 0 25966 38 0 0 25 0 1 0 422577994 65306624 13085 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15944 13085 603 41 0 15903 0
vsize: 63776
[startup+270.006 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 1636
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 13838 0 0 0 26966 38 0 0 25 0 1 0 422577994 65576960 13157 4294967295 134512640 134672761 3221224560 3221223824 134562262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16010 13157 603 41 0 15969 0
vsize: 64040
[startup+280.006 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 1636
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 13961 0 0 0 27965 39 0 0 25 0 1 0 422577994 65982464 13280 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16109 13280 603 41 0 16068 0
vsize: 64436
[startup+290.006 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 1636
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 14118 0 0 0 28965 40 0 0 25 0 1 0 422577994 66641920 13437 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16270 13437 603 41 0 16229 0
vsize: 65080
[startup+300.006 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 1638
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 14294 0 0 0 29964 41 0 0 25 0 1 0 422577994 67313664 13613 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16434 13613 603 41 0 16393 0
vsize: 65736
[startup+310.007 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 1638
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 14397 0 0 0 30964 41 0 0 25 0 1 0 422577994 67719168 13716 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16533 13716 603 41 0 16492 0
vsize: 66132
[startup+320.007 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 1638
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 14466 0 0 0 31964 41 0 0 25 0 1 0 422577994 67989504 13785 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16599 13785 603 41 0 16558 0
vsize: 66396
[startup+330.007 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 1638
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 14564 0 0 0 32964 42 0 0 25 0 1 0 422577994 68390912 13883 4294967295 134512640 134672761 3221224560 3221223728 134560845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16697 13883 603 41 0 16656 0
vsize: 66788
[startup+340.007 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 1638
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 14668 0 0 0 33964 42 0 0 25 0 1 0 422577994 68792320 13987 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16795 13987 603 41 0 16754 0
vsize: 67180
[startup+350.007 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 1638
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 14797 0 0 0 34964 42 0 0 25 0 1 0 422577994 69324800 14116 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16925 14116 603 41 0 16884 0
vsize: 67700
[startup+360.007 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 1638
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 14877 0 0 0 35965 43 0 0 25 0 1 0 422577994 69726208 14196 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17023 14196 603 41 0 16982 0
vsize: 68092
[startup+370.008 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1638
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 14941 0 0 0 36965 43 0 0 25 0 1 0 422577994 69996544 14260 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17089 14260 603 41 0 17048 0
vsize: 68356
[startup+380.008 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1638
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 15013 0 0 0 37965 43 0 0 25 0 1 0 422577994 70266880 14332 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17155 14332 603 41 0 17114 0
vsize: 68620
[startup+390.007 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1638
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 15088 0 0 0 38965 43 0 0 25 0 1 0 422577994 70533120 14407 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17220 14407 603 41 0 17179 0
vsize: 68880
[startup+400.008 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1638
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 15172 0 0 0 39965 44 0 0 25 0 1 0 422577994 70934528 14491 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17318 14491 603 41 0 17277 0
vsize: 69272
[startup+410.008 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1638
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 15314 0 0 0 40965 44 0 0 25 0 1 0 422577994 71475200 14633 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17450 14633 603 41 0 17409 0
vsize: 69800
[startup+420.008 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1638
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 15468 0 0 0 41965 45 0 0 25 0 1 0 422577994 72007680 14787 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17580 14787 603 41 0 17539 0
vsize: 70320
[startup+430.009 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1638
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 15551 0 0 0 42965 45 0 0 25 0 1 0 422577994 72409088 14870 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17678 14870 603 41 0 17637 0
vsize: 70712
[startup+440.008 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1638
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 15624 0 0 0 43965 45 0 0 25 0 1 0 422577994 72679424 14943 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17744 14943 603 41 0 17703 0
vsize: 70976
[startup+450.008 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1638
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 15703 0 0 0 44965 45 0 0 25 0 1 0 422577994 72945664 15022 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17809 15022 603 41 0 17768 0
vsize: 71236
[startup+460.009 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1638
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 15843 0 0 0 45965 46 0 0 25 0 1 0 422577994 73613312 15162 4294967295 134512640 134672761 3221224560 3221223728 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17972 15162 603 41 0 17931 0
vsize: 71888
[startup+470.009 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1638
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16028 0 0 0 46965 46 0 0 25 0 1 0 422577994 74285056 15347 4294967295 134512640 134672761 3221224560 3221223728 134560797 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18136 15347 603 41 0 18095 0
vsize: 72544
[startup+480.009 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1638
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16146 0 0 0 47965 46 0 0 25 0 1 0 422577994 74821632 15465 4294967295 134512640 134672761 3221224560 3221223728 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18267 15465 603 41 0 18226 0
vsize: 73068
[startup+490.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1638
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16283 0 0 0 48964 47 0 0 25 0 1 0 422577994 75358208 15602 4294967295 134512640 134672761 3221224560 3221223728 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18398 15602 603 41 0 18357 0
vsize: 73592
[startup+500.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1638
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16409 0 0 0 49965 48 0 0 25 0 1 0 422577994 75898880 15728 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18530 15728 603 41 0 18489 0
vsize: 74120
[startup+510.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1638
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16610 0 0 0 50964 48 0 0 25 0 1 0 422577994 77037568 15910 4294967295 134512640 134672761 3221224560 3221223392 134565852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15910 603 41 0 18767 0
vsize: 75232
[startup+520.011 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1638
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16610 0 0 0 51965 48 0 0 25 0 1 0 422577994 77037568 15910 4294967295 134512640 134672761 3221224560 3221223728 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15910 603 41 0 18767 0
vsize: 75232
[startup+530.011 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1638
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16610 0 0 0 52965 48 0 0 25 0 1 0 422577994 77037568 15910 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15910 603 41 0 18767 0
vsize: 75232
[startup+540.011 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16610 0 0 0 53965 48 0 0 25 0 1 0 422577994 77037568 15910 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15910 603 41 0 18767 0
vsize: 75232
[startup+550.011 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16610 0 0 0 54965 48 0 0 25 0 1 0 422577994 77037568 15910 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15910 603 41 0 18767 0
vsize: 75232
[startup+560.011 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16610 0 0 0 55966 48 0 0 25 0 1 0 422577994 77037568 15910 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15910 603 41 0 18767 0
vsize: 75232
[startup+570.011 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16610 0 0 0 56966 48 0 0 25 0 1 0 422577994 77037568 15910 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15910 603 41 0 18767 0
vsize: 75232
[startup+580.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16610 0 0 0 57966 49 0 0 25 0 1 0 422577994 77037568 15910 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15910 603 41 0 18767 0
vsize: 75232
[startup+590.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16610 0 0 0 58967 49 0 0 25 0 1 0 422577994 77037568 15910 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15910 603 41 0 18767 0
vsize: 75232
[startup+600.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16610 0 0 0 59967 49 0 0 25 0 1 0 422577994 77037568 15910 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15910 603 41 0 18767 0
vsize: 75232
[startup+610.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16610 0 0 0 60967 49 0 0 25 0 1 0 422577994 77037568 15910 4294967295 134512640 134672761 3221224560 3221223728 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15910 603 41 0 18767 0
vsize: 75232
[startup+620.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16610 0 0 0 61968 49 0 0 25 0 1 0 422577994 77037568 15910 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15910 603 41 0 18767 0
vsize: 75232
[startup+630.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16610 0 0 0 62968 49 0 0 25 0 1 0 422577994 77037568 15910 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15910 603 41 0 18767 0
vsize: 75232
[startup+640.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16610 0 0 0 63968 49 0 0 25 0 1 0 422577994 77037568 15910 4294967295 134512640 134672761 3221224560 3221223728 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15910 603 41 0 18767 0
vsize: 75232
[startup+650.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16610 0 0 0 64969 49 0 0 25 0 1 0 422577994 77037568 15910 4294967295 134512640 134672761 3221224560 3221223728 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15910 603 41 0 18767 0
vsize: 75232
[startup+660.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16610 0 0 0 65969 49 0 0 25 0 1 0 422577994 77037568 15910 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15910 603 41 0 18767 0
vsize: 75232
[startup+670.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16610 0 0 0 66970 49 0 0 25 0 1 0 422577994 77037568 15910 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15910 603 41 0 18767 0
vsize: 75232
[startup+680.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16610 0 0 0 67970 49 0 0 25 0 1 0 422577994 77037568 15910 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15910 603 41 0 18767 0
vsize: 75232
[startup+690.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16612 0 0 0 68970 49 0 0 25 0 1 0 422577994 77037568 15912 4294967295 134512640 134672761 3221224560 3221223728 134561018 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15912 603 41 0 18767 0
vsize: 75232
[startup+700.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16612 0 0 0 69970 49 0 0 25 0 1 0 422577994 77037568 15912 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15912 603 41 0 18767 0
vsize: 75232
[startup+710.015 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16612 0 0 0 70971 49 0 0 25 0 1 0 422577994 77037568 15912 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15912 603 41 0 18767 0
vsize: 75232
[startup+720.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16612 0 0 0 71971 49 0 0 25 0 1 0 422577994 77037568 15912 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15912 603 41 0 18767 0
vsize: 75232
[startup+730.015 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16612 0 0 0 72972 49 0 0 25 0 1 0 422577994 77037568 15912 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15912 603 41 0 18767 0
vsize: 75232
[startup+740.015 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16612 0 0 0 73972 49 0 0 25 0 1 0 422577994 77037568 15912 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15912 603 41 0 18767 0
vsize: 75232
[startup+750.015 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16612 0 0 0 74972 49 0 0 25 0 1 0 422577994 77037568 15912 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15912 603 41 0 18767 0
vsize: 75232
[startup+760.015 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16612 0 0 0 75972 49 0 0 25 0 1 0 422577994 77037568 15912 4294967295 134512640 134672761 3221224560 3221223696 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15912 603 41 0 18767 0
vsize: 75232
[startup+770.015 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16612 0 0 0 76972 49 0 0 25 0 1 0 422577994 77037568 15912 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15912 603 41 0 18767 0
vsize: 75232
[startup+780.015 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16612 0 0 0 77973 49 0 0 25 0 1 0 422577994 77037568 15912 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15912 603 41 0 18767 0
vsize: 75232
[startup+790.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16612 0 0 0 78973 49 0 0 25 0 1 0 422577994 77037568 15912 4294967295 134512640 134672761 3221224560 3221223696 134560667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15912 603 41 0 18767 0
vsize: 75232
[startup+800.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16612 0 0 0 79973 49 0 0 25 0 1 0 422577994 77037568 15912 4294967295 134512640 134672761 3221224560 3221223616 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15912 603 41 0 18767 0
vsize: 75232
[startup+810.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16612 0 0 0 80974 49 0 0 25 0 1 0 422577994 77037568 15912 4294967295 134512640 134672761 3221224560 3221223728 134560797 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15912 603 41 0 18767 0
vsize: 75232
[startup+820.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16612 0 0 0 81974 49 0 0 25 0 1 0 422577994 77037568 15912 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15912 603 41 0 18767 0
vsize: 75232
[startup+830.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16612 0 0 0 82974 49 0 0 25 0 1 0 422577994 77037568 15912 4294967295 134512640 134672761 3221224560 3221223664 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15912 603 41 0 18767 0
vsize: 75232
[startup+840.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16612 0 0 0 83975 49 0 0 25 0 1 0 422577994 77037568 15912 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15912 603 41 0 18767 0
vsize: 75232
[startup+850.017 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16612 0 0 0 84975 49 0 0 25 0 1 0 422577994 77037568 15912 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15912 603 41 0 18767 0
vsize: 75232
[startup+860.017 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16612 0 0 0 85975 49 0 0 25 0 1 0 422577994 77037568 15912 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15912 603 41 0 18767 0
vsize: 75232
[startup+870.017 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16612 0 0 0 86976 49 0 0 25 0 1 0 422577994 77037568 15912 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15912 603 41 0 18767 0
vsize: 75232
[startup+880.017 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16612 0 0 0 87976 49 0 0 25 0 1 0 422577994 77037568 15912 4294967295 134512640 134672761 3221224560 3221223664 134554926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15912 603 41 0 18767 0
vsize: 75232
[startup+890.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16612 0 0 0 88976 49 0 0 25 0 1 0 422577994 77037568 15912 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15912 603 41 0 18767 0
vsize: 75232
[startup+900.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16612 0 0 0 89977 49 0 0 25 0 1 0 422577994 77037568 15912 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15912 603 41 0 18767 0
vsize: 75232
[startup+910.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16612 0 0 0 90977 49 0 0 25 0 1 0 422577994 77037568 15912 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15912 603 41 0 18767 0
vsize: 75232
[startup+920.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16612 0 0 0 91978 49 0 0 25 0 1 0 422577994 77037568 15912 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15912 603 41 0 18767 0
vsize: 75232
[startup+930.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16612 0 0 0 92978 49 0 0 25 0 1 0 422577994 77037568 15912 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15912 603 41 0 18767 0
vsize: 75232
[startup+940.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16612 0 0 0 93978 49 0 0 25 0 1 0 422577994 77037568 15912 4294967295 134512640 134672761 3221224560 3221223728 134560970 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15912 603 41 0 18767 0
vsize: 75232
[startup+950.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16612 0 0 0 94979 49 0 0 25 0 1 0 422577994 77037568 15912 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 15912 603 41 0 18767 0
vsize: 75232
[startup+960.021 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16641 0 0 0 95979 49 0 0 25 0 1 0 422577994 77168640 15941 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18840 15941 603 41 0 18799 0
vsize: 75360
[startup+970.022 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16895 0 0 0 96979 50 0 0 25 0 1 0 422577994 78274560 16195 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19110 16195 603 41 0 19069 0
vsize: 76440
[startup+980.023 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 16998 0 0 0 97979 50 0 0 25 0 1 0 422577994 78684160 16298 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19210 16298 603 41 0 19169 0
vsize: 76840
[startup+990.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 17068 0 0 0 98979 50 0 0 25 0 1 0 422577994 78954496 16368 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19276 16368 603 41 0 19235 0
vsize: 77104
[startup+1000.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 17146 0 0 0 99979 51 0 0 25 0 1 0 422577994 79364096 16446 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19376 16446 603 41 0 19335 0
vsize: 77504
[startup+1010.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 17223 0 0 0 100979 51 0 0 25 0 1 0 422577994 79634432 16523 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19442 16523 603 41 0 19401 0
vsize: 77768
[startup+1020.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 17321 0 0 0 101979 51 0 0 25 0 1 0 422577994 80035840 16621 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19540 16621 603 41 0 19499 0
vsize: 78160
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 17463 0 0 0 102979 52 0 0 25 0 1 0 422577994 80572416 16763 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19671 16763 603 41 0 19630 0
vsize: 78684
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 17623 0 0 0 103979 52 0 0 25 0 1 0 422577994 81244160 16923 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19835 16923 603 41 0 19794 0
vsize: 79340
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 17773 0 0 0 104979 53 0 0 25 0 1 0 422577994 81911808 17073 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19998 17073 603 41 0 19957 0
vsize: 79992
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 17847 0 0 0 105979 53 0 0 25 0 1 0 422577994 82182144 17147 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20064 17147 603 41 0 20023 0
vsize: 80256
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 17921 0 0 0 106979 53 0 0 25 0 1 0 422577994 82452480 17221 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20130 17221 603 41 0 20089 0
vsize: 80520
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 18071 0 0 0 107979 53 0 0 25 0 1 0 422577994 83111936 17371 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20291 17371 603 41 0 20250 0
vsize: 81164
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 18226 0 0 0 108979 54 0 0 25 0 1 0 422577994 83783680 17526 4294967295 134512640 134672761 3221224560 3221223760 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20455 17526 603 41 0 20414 0
vsize: 81820
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 18360 0 0 0 109979 54 0 0 25 0 1 0 422577994 84320256 17660 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20586 17660 603 41 0 20545 0
vsize: 82344
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 18517 0 0 0 110979 55 0 0 25 0 1 0 422577994 84852736 17817 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20716 17817 603 41 0 20675 0
vsize: 82864
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 18718 0 0 0 111979 55 0 0 25 0 1 0 422577994 85655552 18018 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20912 18018 603 41 0 20871 0
vsize: 83648
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 18909 0 0 0 112979 56 0 0 25 0 1 0 422577994 86466560 18209 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21110 18209 603 41 0 21069 0
vsize: 84440
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 19151 0 0 0 113978 56 0 0 25 0 1 0 422577994 87535616 18451 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21371 18451 603 41 0 21330 0
vsize: 85484
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 19326 0 0 0 114978 57 0 0 25 0 1 0 422577994 88207360 18626 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21535 18626 603 41 0 21494 0
vsize: 86140
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 19551 0 0 0 115978 58 0 0 25 0 1 0 422577994 89149440 18851 4294967295 134512640 134672761 3221224560 3221223664 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21765 18851 603 41 0 21724 0
vsize: 87060
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 19796 0 0 0 116977 59 0 0 25 0 1 0 422577994 90083328 19096 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21993 19096 603 41 0 21952 0
vsize: 87972
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 20003 0 0 0 117977 59 0 0 25 0 1 0 422577994 90873856 19303 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22186 19303 603 41 0 22145 0
vsize: 88744
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 20246 0 0 0 118977 60 0 0 25 0 1 0 422577994 91938816 19546 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22446 19546 603 41 0 22405 0
vsize: 89784
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 1640
Raw data (stat): 1583 (minisat+) R 1582 29653 29652 0 -1 0 20374 0 0 0 119976 61 0 0 25 0 1 0 422577994 92504064 19674 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22584 19674 603 41 0 22543 0
vsize: 90336
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.00 0.98 0.91 1/54 1640
Raw data (stat): 1583 (minisat+) Z 1582 29653 29652 0 -1 12 20377 0 0 0 119976 65 0 0 25 0 1 0 422577994 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.08
CPU time (s): 1200.42
CPU user time (s): 1199.77
CPU system time (s): 0.6539
CPU usage (%): 100.028
Max. virtual memory (Kb): 90336
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####