PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

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

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-04-13 20:52:15 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=1544 boxname=wulflinc20 idbench=172 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  966ceb4249ada81e9b52daecca845c09  /oldhome/oroussel/tmp/wulflinc20/normalized-ii8c2.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc20/normalized-ii8c2.opb
IDLAUNCH: 1544
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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	: 3
cpu MHz		: 451.215
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        895552 kB
Buffers:         33196 kB
Cached:          70520 kB
SwapCached:       2636 kB
Active:          44432 kB
Inactive:        64756 kB
HighTotal:      131008 kB
HighFree:        56756 kB
LowTotal:       903652 kB
LowFree:        838796 kB
SwapTotal:     2097892 kB
SwapFree:      2095256 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            24428 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 21:12:17 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 1544 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 7639 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 |    7639    17170 |    2546       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 846[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:108112     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        20 |  142004   331152 |   47334      20      433    21.6 |  0.000 % |
c |       120 |  141879   330895 |   52067     116     2334    20.1 |  0.087 % |
c |       270 |  141843   330819 |   57274     265     4364    16.5 |  0.109 % |
c |       495 |  141742   330606 |   63001     488     9937    20.4 |  0.171 % |
c |       832 |  141699   330513 |   69301     824    13932    16.9 |  0.198 % |
c ==============================================================================
c [1mFound solution: 675[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 |      1299 |  142059   331764 |   47353    1277    22673    17.8 |  0.198 % |
c |      1400 |  142059   331764 |   52088    1378    27677    20.1 |  0.652 % |
c |      1550 |  142059   331764 |   57297    1528    37170    24.3 |  0.652 % |
c |      1775 |  141706   331023 |   63026    1739    47276    27.2 |  0.864 % |
c |      2112 |  141706   331023 |   69329    2076    61030    29.4 |  0.864 % |
c |      2618 |  141706   331023 |   76262    2582    76846    29.8 |  0.864 % |
c ==============================================================================
c [1mFound solution: 572[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 |      3178 |  142358   332633 |   47452    3142   102366    32.6 |  0.864 % |
c |      3279 |  142358   332633 |   52197    3243   107591    33.2 |  0.905 % |
c |      3429 |  141631   331042 |   57416    3372   113663    33.7 |  1.375 % |
c |      3661 |  141592   330959 |   63158    3551   129449    36.5 |  1.399 % |
c |      3999 |  141410   330555 |   69474    3879   133761    34.5 |  1.519 % |
c |      4506 |  140434   328383 |   76421    3911   134845    34.5 |  2.170 % |
c |      5268 |  139398   326077 |   84064    4642   166116    35.8 |  2.860 % |
c |      6407 |  139398   326077 |   92470    5781   325625    56.3 |  2.860 % |
c |      8115 |  138919   325014 |  101717    7476   375562    50.2 |  3.178 % |
c ==============================================================================
c [1mFound solution: 549[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 |      8848 |  139152   325650 |   46384    8209   395099    48.1 |  3.178 % |
c |      8948 |  139152   325650 |   51022    8309   397658    47.9 |  3.174 % |
c |      9099 |  139152   325650 |   56124    8460   400787    47.4 |  3.174 % |
c |      9325 |  139105   325551 |   61737    8661   409960    47.3 |  3.202 % |
c |      9668 |  139060   325458 |   67910    9003   427664    47.5 |  3.228 % |
c |     10175 |  139060   325458 |   74701    9510   447056    47.0 |  3.228 % |
c |     10935 |  138086   323286 |   82172   10192   466087    45.7 |  3.879 % |
c |     12074 |  138086   323286 |   90389   11331   551902    48.7 |  3.879 % |
c ==============================================================================
c [1mFound solution: 537[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 |     12642 |  138215   323657 |   46071   11899   579529    48.7 |  3.879 % |
c |     12743 |  138152   323526 |   50678   11999   584184    48.7 |  3.917 % |
c |     12894 |  138152   323526 |   55745   12150   586918    48.3 |  3.917 % |
c |     13121 |  138152   323526 |   61320   12377   591056    47.8 |  3.917 % |
c |     13458 |  138152   323526 |   67452   12714   605389    47.6 |  3.917 % |
c |     13965 |  138152   323526 |   74197   13221   618996    46.8 |  3.917 % |
c |     14724 |  138152   323526 |   81617   13980   631125    45.1 |  3.917 % |
c |     15863 |  138152   323526 |   89779   15119   648428    42.9 |  3.917 % |
c |     17571 |  138114   323444 |   98757   14113   634473    45.0 |  3.940 % |
c |     20136 |  137695   322535 |  108633   16548   863131    52.2 |  4.206 % |
c |     23980 |  137171   321403 |  119496   20340  1244053    61.2 |  4.536 % |
c |     29747 |  137015   321054 |  131445   26075  1746694    67.0 |  4.641 % |
c |     38397 |  136889   320784 |  144590   34606  3825916   110.6 |  4.719 % |
c |     51371 |  136651   320246 |  159049   47551  5308624   111.6 |  4.882 % |
c |     70832 |  136610   320157 |  174954   67011  8429007   125.8 |  4.908 % |
c ==============================================================================
c [1mFound solution: 525[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 |     72243 |  136598   320212 |   45532   68407  8531576   124.7 |  4.908 % |
c |     72344 |  136598   320212 |   50085   19774  1322493    66.9 |  4.997 % |
c |     72494 |  136598   320212 |   55093   19924  1331546    66.8 |  4.997 % |
c |     72721 |  136598   320212 |   60603   20151  1334825    66.2 |  4.997 % |
c |     73058 |  136598   320212 |   66663   20488  1348960    65.8 |  4.997 % |
c |     73565 |  136545   320095 |   73329   20864  1366784    65.5 |  5.032 % |
c |     74330 |  136545   320095 |   80662   21629  1397067    64.6 |  5.032 % |
c |     75469 |  136545   320095 |   88728   22768  1532087    67.3 |  5.032 % |
c |     77178 |  136451   319893 |   97601   24475  1717505    70.2 |  5.090 % |
c |     79740 |  136308   319578 |  107362   27008  1884332    69.8 |  5.183 % |
c |     83584 |  136308   319578 |  118098   30852  2620553    84.9 |  5.183 % |
c |     89354 |  136262   319474 |  129908   36616  2932225    80.1 |  5.215 % |
c |     98004 |  136165   319257 |  142898   45258  3743800    82.7 |  5.280 % |
c |    110978 |  136108   319122 |  157188   58204  4594747    78.9 |  5.322 % |
c |    130439 |  136108   319122 |  172907   77665  7808742   100.5 |  5.322 % |
c |    159633 |  136108   319122 |  190198  106859 11719000   109.7 |  5.322 % |
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 -#### 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.91 0.95 0.90 2/54 30639
Raw data (stat): 30639 (runsolver) R 30638 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478974141 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0011 s]
Raw data (loadavg): 0.92 0.95 0.90 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 7525 0 0 0 981 18 0 0 25 0 1 0 478974141 34439168 7229 4294967295 134512640 134672761 3221224640 3221222840 134523049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8408 7229 603 41 0 8367 0
vsize: 33632
[startup+20.0015 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 7591 0 0 0 1980 19 0 0 25 0 1 0 478974141 35139584 7295 4294967295 134512640 134672761 3221224640 3221223840 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8579 7295 603 41 0 8538 0
vsize: 34316
[startup+30.0017 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 7694 0 0 0 2979 19 0 0 25 0 1 0 478974141 35549184 7398 4294967295 134512640 134672761 3221224640 3221223776 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8679 7398 603 41 0 8638 0
vsize: 34716
[startup+40.0023 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 7866 0 0 0 3978 21 0 0 25 0 1 0 478974141 36216832 7570 4294967295 134512640 134672761 3221224640 3221223744 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8842 7570 603 41 0 8801 0
vsize: 35368
[startup+50.0027 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 7955 0 0 0 4977 22 0 0 25 0 1 0 478974141 36618240 7659 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8940 7659 603 41 0 8899 0
vsize: 35760
[startup+60.0038 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 8041 0 0 0 5977 22 0 0 25 0 1 0 478974141 36892672 7745 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9007 7745 603 41 0 8966 0
vsize: 36028
[startup+70.0046 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 8158 0 0 0 6976 23 0 0 25 0 1 0 478974141 37433344 7862 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9139 7862 603 41 0 9098 0
vsize: 36556
[startup+80.0049 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 8333 0 0 0 7975 23 0 0 25 0 1 0 478974141 38023168 8001 4294967295 134512640 134672761 3221224640 3221223744 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9283 8001 603 41 0 9242 0
vsize: 37132
[startup+90.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 8437 0 0 0 8975 24 0 0 25 0 1 0 478974141 38424576 8105 4294967295 134512640 134672761 3221224640 3221223776 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9381 8105 603 41 0 9340 0
vsize: 37524
[startup+100.007 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 8625 0 0 0 9974 25 0 0 25 0 1 0 478974141 39256064 8293 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9584 8293 603 41 0 9543 0
vsize: 38336
[startup+110.008 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 8880 0 0 0 10974 25 0 0 25 0 1 0 478974141 40198144 8548 4294967295 134512640 134672761 3221224640 3221223808 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9814 8548 603 41 0 9773 0
vsize: 39256
[startup+120.009 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 9034 0 0 0 11973 26 0 0 25 0 1 0 478974141 40857600 8702 4294967295 134512640 134672761 3221224640 3221223824 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9975 8702 603 41 0 9934 0
vsize: 39900
[startup+130.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 9242 0 0 0 12972 27 0 0 25 0 1 0 478974141 41697280 8910 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10180 8910 603 41 0 10139 0
vsize: 40720
[startup+140.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 9399 0 0 0 13971 28 0 0 25 0 1 0 478974141 42360832 9067 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10342 9067 603 41 0 10301 0
vsize: 41368
[startup+150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 9564 0 0 0 14970 29 0 0 25 0 1 0 478974141 43036672 9232 4294967295 134512640 134672761 3221224640 3221223840 134557922 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10507 9232 603 41 0 10466 0
vsize: 42028
[startup+160.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 9701 0 0 0 15970 30 0 0 25 0 1 0 478974141 43569152 9369 4294967295 134512640 134672761 3221224640 3221223824 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10637 9369 603 41 0 10596 0
vsize: 42548
[startup+170.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 9890 0 0 0 16968 31 0 0 25 0 1 0 478974141 44376064 9558 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10834 9558 603 41 0 10793 0
vsize: 43336
[startup+180.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 10067 0 0 0 17968 32 0 0 25 0 1 0 478974141 45051904 9735 4294967295 134512640 134672761 3221224640 3221223744 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10999 9735 603 41 0 10958 0
vsize: 43996
[startup+190.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 10523 0 0 0 18966 34 0 0 25 0 1 0 478974141 46911488 10191 4294967295 134512640 134672761 3221224640 3221223744 134560326 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11453 10191 603 41 0 11412 0
vsize: 45812
[startup+200.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 11003 0 0 0 19965 35 0 0 25 0 1 0 478974141 48922624 10671 4294967295 134512640 134672761 3221224640 3221223808 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11944 10671 603 41 0 11903 0
vsize: 47776
[startup+210.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 11413 0 0 0 20963 37 0 0 25 0 1 0 478974141 50753536 11081 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12391 11081 603 41 0 12350 0
vsize: 49564
[startup+220.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 11723 0 0 0 21962 38 0 0 25 0 1 0 478974141 51957760 11391 4294967295 134512640 134672761 3221224640 3221223808 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12685 11391 603 41 0 12644 0
vsize: 50740
[startup+230.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 11853 0 0 0 22961 39 0 0 25 0 1 0 478974141 52482048 11521 4294967295 134512640 134672761 3221224640 3221223808 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12813 11521 603 41 0 12772 0
vsize: 51252
[startup+240.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 12024 0 0 0 23961 40 0 0 25 0 1 0 478974141 53153792 11692 4294967295 134512640 134672761 3221224640 3221223776 134560622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12977 11692 603 41 0 12936 0
vsize: 51908
[startup+250.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 12237 0 0 0 24960 41 0 0 25 0 1 0 478974141 54071296 11905 4294967295 134512640 134672761 3221224640 3221223776 134565076 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13201 11905 603 41 0 13160 0
vsize: 52804
[startup+260.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 12459 0 0 0 25959 41 0 0 25 0 1 0 478974141 55009280 12127 4294967295 134512640 134672761 3221224640 3221223744 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13430 12127 603 41 0 13389 0
vsize: 53720
[startup+270.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 12680 0 0 0 26958 42 0 0 25 0 1 0 478974141 55808000 12348 4294967295 134512640 134672761 3221224640 3221223744 134560344 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13625 12348 603 41 0 13584 0
vsize: 54500
[startup+280.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 12859 0 0 0 27957 43 0 0 25 0 1 0 478974141 56602624 12527 4294967295 134512640 134672761 3221224640 3221223808 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13819 12527 603 41 0 13778 0
vsize: 55276
[startup+290.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 12987 0 0 0 28956 44 0 0 25 0 1 0 478974141 57139200 12655 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13950 12655 603 41 0 13909 0
vsize: 55800
[startup+300.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 13108 0 0 0 29956 44 0 0 25 0 1 0 478974141 57540608 12776 4294967295 134512640 134672761 3221224640 3221223824 134559383 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14048 12776 603 41 0 14007 0
vsize: 56192
[startup+310.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 13288 0 0 0 30955 45 0 0 25 0 1 0 478974141 58343424 12956 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14244 12956 603 41 0 14203 0
vsize: 56976
[startup+320.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 13591 0 0 0 31954 47 0 0 25 0 1 0 478974141 59559936 13259 4294967295 134512640 134672761 3221224640 3221223744 134560212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14541 13259 603 41 0 14500 0
vsize: 58164
[startup+330.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 13942 0 0 0 32952 48 0 0 25 0 1 0 478974141 61014016 13610 4294967295 134512640 134672761 3221224640 3221223744 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14896 13610 603 41 0 14855 0
vsize: 59584
[startup+340.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 14253 0 0 0 33951 50 0 0 25 0 1 0 478974141 62214144 13921 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15189 13921 603 41 0 15148 0
vsize: 60756
[startup+350.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 14535 0 0 0 34950 51 0 0 25 0 1 0 478974141 63418368 14203 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15483 14203 603 41 0 15442 0
vsize: 61932
[startup+360.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 14803 0 0 0 35949 52 0 0 25 0 1 0 478974141 64479232 14471 4294967295 134512640 134672761 3221224640 3221223696 134565080 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15742 14471 603 41 0 15701 0
vsize: 62968
[startup+370.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 15023 0 0 0 36949 53 0 0 25 0 1 0 478974141 65413120 14691 4294967295 134512640 134672761 3221224640 3221223744 134560361 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15970 14691 603 41 0 15929 0
vsize: 63880
[startup+380.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 15192 0 0 0 37948 53 0 0 25 0 1 0 478974141 66068480 14860 4294967295 134512640 134672761 3221224640 3221223744 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16130 14860 603 41 0 16089 0
vsize: 64520
[startup+390.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 15323 0 0 0 38948 54 0 0 25 0 1 0 478974141 66600960 14991 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16260 14991 603 41 0 16219 0
vsize: 65040
[startup+400.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 15488 0 0 0 39947 54 0 0 25 0 1 0 478974141 67268608 15156 4294967295 134512640 134672761 3221224640 3221223792 134561040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16423 15156 603 41 0 16382 0
vsize: 65692
[startup+410.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 15681 0 0 0 40946 55 0 0 25 0 1 0 478974141 68075520 15349 4294967295 134512640 134672761 3221224640 3221223824 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16620 15349 603 41 0 16579 0
vsize: 66480
[startup+420.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 15847 0 0 0 41946 56 0 0 25 0 1 0 478974141 68747264 15515 4294967295 134512640 134672761 3221224640 3221223776 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16784 15515 603 41 0 16743 0
vsize: 67136
[startup+430.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16012 0 0 0 42945 57 0 0 25 0 1 0 478974141 69406720 15680 4294967295 134512640 134672761 3221224640 3221223744 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16945 15680 603 41 0 16904 0
vsize: 67780
[startup+440.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16183 0 0 0 43944 58 0 0 25 0 1 0 478974141 70078464 15851 4294967295 134512640 134672761 3221224640 3221223804 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17109 15851 603 41 0 17068 0
vsize: 68436
[startup+450.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16343 0 0 0 44943 59 0 0 25 0 1 0 478974141 71016448 16011 4294967295 134512640 134672761 3221224640 3221223808 134561121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17338 16011 603 41 0 17297 0
vsize: 69352
[startup+460.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30639
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16537 0 0 0 45943 59 0 0 25 0 1 0 478974141 71823360 16205 4294967295 134512640 134672761 3221224640 3221223808 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17535 16205 603 41 0 17494 0
vsize: 70140
[startup+470.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30642
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16724 0 0 0 46943 60 0 0 25 0 1 0 478974141 72507392 16392 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17702 16392 603 41 0 17661 0
vsize: 70808
[startup+480.03 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 30692
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16724 0 0 0 47943 60 0 0 25 0 1 0 478974141 72507392 16392 4294967295 134512640 134672761 3221224640 3221223792 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17702 16392 603 41 0 17661 0
vsize: 70808
[startup+490.03 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 30692
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16724 0 0 0 48943 60 0 0 25 0 1 0 478974141 72507392 16392 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17702 16392 603 41 0 17661 0
vsize: 70808
[startup+500.03 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 30692
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16724 0 0 0 49943 60 0 0 25 0 1 0 478974141 72507392 16392 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17702 16392 603 41 0 17661 0
vsize: 70808
[startup+510.031 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 30692
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16724 0 0 0 50943 60 0 0 25 0 1 0 478974141 72507392 16392 4294967295 134512640 134672761 3221224640 3221223808 134561264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17702 16392 603 41 0 17661 0
vsize: 70808
[startup+520.03 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 30692
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16724 0 0 0 51943 60 0 0 25 0 1 0 478974141 72507392 16392 4294967295 134512640 134672761 3221224640 3221223824 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17702 16392 603 41 0 17661 0
vsize: 70808
[startup+530.03 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 30692
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16724 0 0 0 52943 60 0 0 25 0 1 0 478974141 72507392 16392 4294967295 134512640 134672761 3221224640 3221223744 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17702 16392 603 41 0 17661 0
vsize: 70808
[startup+540.031 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16724 0 0 0 53943 60 0 0 25 0 1 0 478974141 72507392 16392 4294967295 134512640 134672761 3221224640 3221223792 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17702 16392 603 41 0 17661 0
vsize: 70808
[startup+550.031 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16724 0 0 0 54944 60 0 0 25 0 1 0 478974141 72507392 16392 4294967295 134512640 134672761 3221224640 3221223808 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17702 16392 603 41 0 17661 0
vsize: 70808
[startup+560.031 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16724 0 0 0 55944 60 0 0 25 0 1 0 478974141 72507392 16392 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17702 16392 603 41 0 17661 0
vsize: 70808
[startup+570.032 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16724 0 0 0 56944 60 0 0 25 0 1 0 478974141 72507392 16392 4294967295 134512640 134672761 3221224640 3221223808 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17702 16392 603 41 0 17661 0
vsize: 70808
[startup+580.032 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16724 0 0 0 57944 60 0 0 25 0 1 0 478974141 72507392 16392 4294967295 134512640 134672761 3221224640 3221223776 134565119 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17702 16392 603 41 0 17661 0
vsize: 70808
[startup+590.033 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16724 0 0 0 58944 60 0 0 25 0 1 0 478974141 72507392 16392 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17702 16392 603 41 0 17661 0
vsize: 70808
[startup+600.033 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16724 0 0 0 59945 60 0 0 25 0 1 0 478974141 72507392 16392 4294967295 134512640 134672761 3221224640 3221223840 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17702 16392 603 41 0 17661 0
vsize: 70808
[startup+610.034 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16724 0 0 0 60945 60 0 0 25 0 1 0 478974141 72507392 16392 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17702 16392 603 41 0 17661 0
vsize: 70808
[startup+620.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16724 0 0 0 61945 60 0 0 25 0 1 0 478974141 72507392 16392 4294967295 134512640 134672761 3221224640 3221223804 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17702 16392 603 41 0 17661 0
vsize: 70808
[startup+630.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16724 0 0 0 62945 60 0 0 25 0 1 0 478974141 72507392 16392 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17702 16392 603 41 0 17661 0
vsize: 70808
[startup+640.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16724 0 0 0 63945 60 0 0 25 0 1 0 478974141 72507392 16392 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17702 16392 603 41 0 17661 0
vsize: 70808
[startup+650.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16724 0 0 0 64946 60 0 0 25 0 1 0 478974141 72507392 16392 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17702 16392 603 41 0 17661 0
vsize: 70808
[startup+660.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16724 0 0 0 65946 60 0 0 25 0 1 0 478974141 72507392 16392 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17702 16392 603 41 0 17661 0
vsize: 70808
[startup+670.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16724 0 0 0 66946 60 0 0 25 0 1 0 478974141 72507392 16392 4294967295 134512640 134672761 3221224640 3221223744 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17702 16392 603 41 0 17661 0
vsize: 70808
[startup+680.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16724 0 0 0 67946 60 0 0 25 0 1 0 478974141 72507392 16392 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17702 16392 603 41 0 17661 0
vsize: 70808
[startup+690.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16724 0 0 0 68946 60 0 0 25 0 1 0 478974141 72507392 16392 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17702 16392 603 41 0 17661 0
vsize: 70808
[startup+700.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16724 0 0 0 69946 60 0 0 25 0 1 0 478974141 72507392 16392 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17702 16392 603 41 0 17661 0
vsize: 70808
[startup+710.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16724 0 0 0 70947 61 0 0 25 0 1 0 478974141 72507392 16392 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17702 16392 603 41 0 17661 0
vsize: 70808
[startup+720.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16724 0 0 0 71947 61 0 0 25 0 1 0 478974141 72507392 16392 4294967295 134512640 134672761 3221224640 3221223744 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17702 16392 603 41 0 17661 0
vsize: 70808
[startup+730.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16724 0 0 0 72947 61 0 0 25 0 1 0 478974141 72507392 16392 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17702 16392 603 41 0 17661 0
vsize: 70808
[startup+740.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16724 0 0 0 73947 61 0 0 25 0 1 0 478974141 72507392 16392 4294967295 134512640 134672761 3221224640 3221223808 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17702 16392 603 41 0 17661 0
vsize: 70808
[startup+750.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16724 0 0 0 74947 61 0 0 25 0 1 0 478974141 72507392 16392 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17702 16392 603 41 0 17661 0
vsize: 70808
[startup+760.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16725 0 0 0 75948 61 0 0 25 0 1 0 478974141 72507392 16393 4294967295 134512640 134672761 3221224640 3221223808 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17702 16393 603 41 0 17661 0
vsize: 70808
[startup+770.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16726 0 0 0 76948 61 0 0 25 0 1 0 478974141 72507392 16394 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17702 16394 603 41 0 17661 0
vsize: 70808
[startup+780.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16727 0 0 0 77948 61 0 0 25 0 1 0 478974141 72507392 16395 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17702 16395 603 41 0 17661 0
vsize: 70808
[startup+790.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16728 0 0 0 78948 61 0 0 25 0 1 0 478974141 72507392 16396 4294967295 134512640 134672761 3221224640 3221223776 134560683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17702 16396 603 41 0 17661 0
vsize: 70808
[startup+800.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30694
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16729 0 0 0 79948 61 0 0 25 0 1 0 478974141 72507392 16397 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17702 16397 603 41 0 17661 0
vsize: 70808
[startup+810.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16730 0 0 0 80948 61 0 0 25 0 1 0 478974141 72507392 16398 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17702 16398 603 41 0 17661 0
vsize: 70808
[startup+820.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16731 0 0 0 81948 61 0 0 25 0 1 0 478974141 72507392 16399 4294967295 134512640 134672761 3221224640 3221223824 134558513 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17702 16399 603 41 0 17661 0
vsize: 70808
[startup+830.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16732 0 0 0 82948 61 0 0 25 0 1 0 478974141 72507392 16400 4294967295 134512640 134672761 3221224640 3221223744 134559966 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17702 16400 603 41 0 17661 0
vsize: 70808
[startup+840.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16733 0 0 0 83948 61 0 0 25 0 1 0 478974141 72507392 16401 4294967295 134512640 134672761 3221224640 3221223808 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17702 16401 603 41 0 17661 0
vsize: 70808
[startup+850.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16735 0 0 0 84948 61 0 0 25 0 1 0 478974141 72507392 16403 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17702 16403 603 41 0 17661 0
vsize: 70808
[startup+860.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16736 0 0 0 85949 61 0 0 25 0 1 0 478974141 72507392 16404 4294967295 134512640 134672761 3221224640 3221223744 134560051 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17702 16404 603 41 0 17661 0
vsize: 70808
[startup+870.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16737 0 0 0 86949 61 0 0 25 0 1 0 478974141 72507392 16405 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17702 16405 603 41 0 17661 0
vsize: 70808
[startup+880.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16820 0 0 0 87949 61 0 0 25 0 1 0 478974141 72912896 16488 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17801 16488 603 41 0 17760 0
vsize: 71204
[startup+890.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 16951 0 0 0 88948 62 0 0 25 0 1 0 478974141 73428992 16619 4294967295 134512640 134672761 3221224640 3221223640 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17927 16619 603 41 0 17886 0
vsize: 71708
[startup+900.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 17126 0 0 0 89948 62 0 0 25 0 1 0 478974141 74092544 16794 4294967295 134512640 134672761 3221224640 3221223808 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18089 16794 603 41 0 18048 0
vsize: 72356
[startup+910.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 17290 0 0 0 90948 63 0 0 25 0 1 0 478974141 74764288 16958 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18253 16958 603 41 0 18212 0
vsize: 73012
[startup+920.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 17424 0 0 0 91947 64 0 0 25 0 1 0 478974141 75292672 17092 4294967295 134512640 134672761 3221224640 3221223744 134559969 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18382 17092 603 41 0 18341 0
vsize: 73528
[startup+930.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 17605 0 0 0 92947 64 0 0 25 0 1 0 478974141 76083200 17273 4294967295 134512640 134672761 3221224640 3221223776 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18575 17273 603 41 0 18534 0
vsize: 74300
[startup+940.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 17752 0 0 0 93946 65 0 0 25 0 1 0 478974141 76734464 17420 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18734 17420 603 41 0 18693 0
vsize: 74936
[startup+950.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 17979 0 0 0 94946 66 0 0 25 0 1 0 478974141 77668352 17647 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18962 17647 603 41 0 18921 0
vsize: 75848
[startup+960.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 18145 0 0 0 95946 66 0 0 25 0 1 0 478974141 78323712 17813 4294967295 134512640 134672761 3221224640 3221223744 134560408 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19122 17813 603 41 0 19081 0
vsize: 76488
[startup+970.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 18315 0 0 0 96945 66 0 0 25 0 1 0 478974141 78991360 17983 4294967295 134512640 134672761 3221224640 3221223744 134559974 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19285 17983 603 41 0 19244 0
vsize: 77140
[startup+980.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 18463 0 0 0 97945 67 0 0 25 0 1 0 478974141 79519744 18131 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19414 18131 603 41 0 19373 0
vsize: 77656
[startup+990.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 18633 0 0 0 98944 68 0 0 25 0 1 0 478974141 80322560 18301 4294967295 134512640 134672761 3221224640 3221223808 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19610 18301 603 41 0 19569 0
vsize: 78440
[startup+1000.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 18805 0 0 0 99944 68 0 0 25 0 1 0 478974141 80994304 18473 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19774 18473 603 41 0 19733 0
vsize: 79096
[startup+1010.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 18965 0 0 0 100944 69 0 0 25 0 1 0 478974141 81666048 18633 4294967295 134512640 134672761 3221224640 3221223840 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19938 18633 603 41 0 19897 0
vsize: 79752
[startup+1020.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 19129 0 0 0 101944 69 0 0 25 0 1 0 478974141 82341888 18797 4294967295 134512640 134672761 3221224640 3221223808 134561234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20103 18797 603 41 0 20062 0
vsize: 80412
[startup+1030.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 19283 0 0 0 102943 69 0 0 25 0 1 0 478974141 82866176 18951 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20231 18951 603 41 0 20190 0
vsize: 80924
[startup+1040.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 19462 0 0 0 103943 70 0 0 25 0 1 0 478974141 83644416 19130 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20421 19130 603 41 0 20380 0
vsize: 81684
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 19641 0 0 0 104942 71 0 0 25 0 1 0 478974141 84439040 19309 4294967295 134512640 134672761 3221224640 3221223744 134560194 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20615 19309 603 41 0 20574 0
vsize: 82460
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 19824 0 0 0 105941 72 0 0 25 0 1 0 478974141 85098496 19492 4294967295 134512640 134672761 3221224640 3221223744 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20776 19492 603 41 0 20735 0
vsize: 83104
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 20014 0 0 0 106941 72 0 0 25 0 1 0 478974141 85880832 19682 4294967295 134512640 134672761 3221224640 3221223744 134559953 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20967 19682 603 41 0 20926 0
vsize: 83868
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 20174 0 0 0 107940 73 0 0 25 0 1 0 478974141 86536192 19842 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21127 19842 603 41 0 21086 0
vsize: 84508
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 20329 0 0 0 108940 74 0 0 25 0 1 0 478974141 87195648 19997 4294967295 134512640 134672761 3221224640 3221223776 134560716 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21288 19997 603 41 0 21247 0
vsize: 85152
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 20434 0 0 0 109938 74 0 0 25 0 1 0 478974141 87601152 20102 4294967295 134512640 134672761 3221224640 3221223804 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21387 20102 603 41 0 21346 0
vsize: 85548
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 20614 0 0 0 110938 75 0 0 25 0 1 0 478974141 88276992 20282 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21552 20282 603 41 0 21511 0
vsize: 86208
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 20782 0 0 0 111938 75 0 0 25 0 1 0 478974141 89075712 20450 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21747 20450 603 41 0 21706 0
vsize: 86988
[startup+1130.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 20950 0 0 0 112937 76 0 0 25 0 1 0 478974141 89747456 20618 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21911 20618 603 41 0 21870 0
vsize: 87644
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 21147 0 0 0 113937 76 0 0 25 0 1 0 478974141 90546176 20815 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22106 20815 603 41 0 22065 0
vsize: 88424
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 21238 0 0 0 114937 77 0 0 25 0 1 0 478974141 90808320 20906 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22170 20906 603 41 0 22129 0
vsize: 88680
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 21304 0 0 0 115937 77 0 0 25 0 1 0 478974141 91078656 20972 4294967295 134512640 134672761 3221224640 3221223824 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22236 20972 603 41 0 22195 0
vsize: 88944
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 21404 0 0 0 116936 78 0 0 25 0 1 0 478974141 91615232 21072 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22367 21072 603 41 0 22326 0
vsize: 89468
[startup+1180.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 21526 0 0 0 117936 78 0 0 25 0 1 0 478974141 92020736 21194 4294967295 134512640 134672761 3221224640 3221223776 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22466 21194 603 41 0 22425 0
vsize: 89864
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 21685 0 0 0 118935 79 0 0 25 0 1 0 478974141 92688384 21353 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22629 21353 603 41 0 22588 0
vsize: 90516
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30696
Raw data (stat): 30639 (minisat+) R 30638 27565 27564 0 -1 0 21862 0 0 0 119935 79 0 0 25 0 1 0 478974141 93364224 21530 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22794 21530 603 41 0 22753 0
vsize: 91176
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 30696
Raw data (stat): 30639 (minisat+) Z 30638 27565 27564 0 -1 12 21865 0 0 0 119935 83 0 0 25 0 1 0 478974141 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.2
CPU user time (s): 1199.36
CPU system time (s): 0.839872
CPU usage (%): 100.01
Max. virtual memory (Kb): 91176
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####