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 5901

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-04-14 02:16:19 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4308 boxname=wulflinc5 idbench=172 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  966ceb4249ada81e9b52daecca845c09  /oldhome/oroussel/tmp/wulflinc5/normalized-ii8c2.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc5/normalized-ii8c2.opb /oldhome/oroussel/tmp/wulflinc5/normalized-ii8c2.opb
IDLAUNCH: 4308
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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.007
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:        898008 kB
Buffers:         34592 kB
Cached:          80504 kB
SwapCached:       2272 kB
Active:          54616 kB
Inactive:        65576 kB
HighTotal:      131008 kB
HighFree:        46620 kB
LowTotal:       903652 kB
LowFree:        851388 kB
SwapTotal:     2097136 kB
SwapFree:      2094864 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            10872 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 02:36:21 (client local time) WITH STATUS 10 IN 1200.23 SECONDS
stats: 4308 7 1200.23 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.96 0.97 0.91 2/54 28770
Raw data (stat): 28770 (runsolver) R 28769 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422698581 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.97 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 7417 0 0 0 979 19 0 0 25 0 1 0 422698581 34443264 7120 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8409 7120 603 41 0 8368 0
vsize: 33636
[startup+20.0011 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 7508 0 0 0 1978 19 0 0 25 0 1 0 422698581 34861056 7211 4294967295 134512640 134672761 3221224560 3221223684 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8511 7211 603 41 0 8470 0
vsize: 34044
[startup+30.0012 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 7602 0 0 0 2978 19 0 0 25 0 1 0 422698581 35246080 7305 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8605 7305 603 41 0 8564 0
vsize: 34420
[startup+40.0013 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 7788 0 0 0 3975 20 0 0 25 0 1 0 422698581 35926016 7491 4294967295 134512640 134672761 3221224560 3221223708 1074754709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8771 7491 603 41 0 8730 0
vsize: 35084
[startup+50.0014 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 7866 0 0 0 4975 21 0 0 25 0 1 0 422698581 36327424 7569 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8869 7569 603 41 0 8828 0
vsize: 35476
[startup+60.0021 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 7951 0 0 0 5975 21 0 0 25 0 1 0 422698581 36601856 7654 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8936 7654 603 41 0 8895 0
vsize: 35744
[startup+70.0025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 8068 0 0 0 6974 22 0 0 25 0 1 0 422698581 37138432 7771 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9067 7771 603 41 0 9026 0
vsize: 36268
[startup+80.0026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 8208 0 0 0 7974 22 0 0 25 0 1 0 422698581 37736448 7911 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9213 7911 603 41 0 9172 0
vsize: 36852
[startup+90.0035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 8311 0 0 0 8974 22 0 0 25 0 1 0 422698581 38137856 8014 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9311 8014 603 41 0 9270 0
vsize: 37244
[startup+100.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 8496 0 0 0 9974 23 0 0 25 0 1 0 422698581 38965248 8199 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9513 8199 603 41 0 9472 0
vsize: 38052
[startup+110.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 8745 0 0 0 10973 24 0 0 25 0 1 0 422698581 39907328 8448 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9743 8448 603 41 0 9702 0
vsize: 38972
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 8901 0 0 0 11973 24 0 0 25 0 1 0 422698581 40566784 8604 4294967295 134512640 134672761 3221224560 3221223696 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9904 8604 603 41 0 9863 0
vsize: 39616
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 9096 0 0 0 12973 25 0 0 25 0 1 0 422698581 41406464 8799 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10109 8799 603 41 0 10068 0
vsize: 40436
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 9260 0 0 0 13972 25 0 0 25 0 1 0 422698581 42065920 8963 4294967295 134512640 134672761 3221224560 3221223696 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10270 8963 603 41 0 10229 0
vsize: 41080
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 9424 0 0 0 14972 25 0 0 25 0 1 0 422698581 42733568 9127 4294967295 134512640 134672761 3221224560 3221223744 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10433 9127 603 41 0 10392 0
vsize: 41732
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 9557 0 0 0 15972 26 0 0 25 0 1 0 422698581 43257856 9260 4294967295 134512640 134672761 3221224560 3221223664 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10561 9260 603 41 0 10520 0
vsize: 42244
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 9750 0 0 0 16972 26 0 0 25 0 1 0 422698581 44060672 9453 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10757 9453 603 41 0 10716 0
vsize: 43028
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 9905 0 0 0 17972 27 0 0 25 0 1 0 422698581 44597248 9608 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10888 9608 603 41 0 10847 0
vsize: 43552
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 10346 0 0 0 18971 27 0 0 25 0 1 0 422698581 46485504 10049 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11349 10049 603 41 0 11308 0
vsize: 45396
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 10802 0 0 0 19970 29 0 0 25 0 1 0 422698581 48365568 10505 4294967295 134512640 134672761 3221224560 3221223664 134559976 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11808 10505 603 41 0 11767 0
vsize: 47232
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 11223 0 0 0 20969 30 0 0 25 0 1 0 422698581 50216960 10926 4294967295 134512640 134672761 3221224560 3221223664 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12260 10926 603 41 0 12219 0
vsize: 49040
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 11558 0 0 0 21968 31 0 0 25 0 1 0 422698581 51552256 11261 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12586 11261 603 41 0 12545 0
vsize: 50344
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 11712 0 0 0 22967 32 0 0 25 0 1 0 422698581 52076544 11415 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12714 11415 603 41 0 12673 0
vsize: 50856
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 11856 0 0 0 23967 32 0 0 25 0 1 0 422698581 52748288 11559 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12878 11559 603 41 0 12837 0
vsize: 51512
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 12071 0 0 0 24967 33 0 0 25 0 1 0 422698581 53657600 11774 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13100 11774 603 41 0 13059 0
vsize: 52400
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 12291 0 0 0 25966 34 0 0 25 0 1 0 422698581 54448128 11994 4294967295 134512640 134672761 3221224560 3221223664 134559853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13293 11994 603 41 0 13252 0
vsize: 53172
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 12516 0 0 0 26965 35 0 0 25 0 1 0 422698581 55386112 12219 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13522 12219 603 41 0 13481 0
vsize: 54088
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 12701 0 0 0 27964 36 0 0 25 0 1 0 422698581 56180736 12404 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 12404 603 41 0 13675 0
vsize: 54864
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 12817 0 0 0 28964 36 0 0 25 0 1 0 422698581 56578048 12520 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13813 12520 603 41 0 13772 0
vsize: 55252
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 12954 0 0 0 29964 37 0 0 25 0 1 0 422698581 57253888 12657 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13978 12657 603 41 0 13937 0
vsize: 55912
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 13124 0 0 0 30964 37 0 0 25 0 1 0 422698581 57921536 12827 4294967295 134512640 134672761 3221224560 3221223728 134560822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14141 12827 603 41 0 14100 0
vsize: 56564
[startup+320.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 13373 0 0 0 31963 38 0 0 25 0 1 0 422698581 58843136 13076 4294967295 134512640 134672761 3221224560 3221223664 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14366 13076 603 41 0 14325 0
vsize: 57464
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 13713 0 0 0 32962 39 0 0 25 0 1 0 422698581 60293120 13416 4294967295 134512640 134672761 3221224560 3221223744 134559383 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14720 13416 603 41 0 14679 0
vsize: 58880
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 14040 0 0 0 33962 40 0 0 25 0 1 0 422698581 61599744 13743 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15039 13743 603 41 0 14998 0
vsize: 60156
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 14328 0 0 0 34960 41 0 0 25 0 1 0 422698581 62799872 14031 4294967295 134512640 134672761 3221224560 3221223664 134560399 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15332 14031 603 41 0 15291 0
vsize: 61328
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 14576 0 0 0 35959 43 0 0 25 0 1 0 422698581 63864832 14279 4294967295 134512640 134672761 3221224560 3221223712 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15592 14279 603 41 0 15551 0
vsize: 62368
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 14832 0 0 0 36959 43 0 0 25 0 1 0 422698581 64798720 14535 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15820 14535 603 41 0 15779 0
vsize: 63280
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 15001 0 0 0 37958 44 0 0 25 0 1 0 422698581 65470464 14704 4294967295 134512640 134672761 3221224560 3221223664 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15984 14704 603 41 0 15943 0
vsize: 63936
[startup+390.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 15173 0 0 0 38958 44 0 0 25 0 1 0 422698581 66269184 14876 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16179 14876 603 41 0 16138 0
vsize: 64716
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 15310 0 0 0 39958 45 0 0 25 0 1 0 422698581 66801664 15013 4294967295 134512640 134672761 3221224560 3221223712 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16309 15013 603 41 0 16268 0
vsize: 65236
[startup+410.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 15474 0 0 0 40958 45 0 0 25 0 1 0 422698581 67473408 15177 4294967295 134512640 134672761 3221224560 3221223664 134560158 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16473 15177 603 41 0 16432 0
vsize: 65892
[startup+420.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 15663 0 0 0 41958 46 0 0 25 0 1 0 422698581 68272128 15366 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16668 15366 603 41 0 16627 0
vsize: 66672
[startup+430.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 15822 0 0 0 42957 46 0 0 25 0 1 0 422698581 68800512 15525 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16797 15525 603 41 0 16756 0
vsize: 67188
[startup+440.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 15995 0 0 0 43957 46 0 0 25 0 1 0 422698581 69607424 15698 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16994 15698 603 41 0 16953 0
vsize: 67976
[startup+450.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16135 0 0 0 44957 47 0 0 25 0 1 0 422698581 70385664 15838 4294967295 134512640 134672761 3221224560 3221223728 134561261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17184 15838 603 41 0 17143 0
vsize: 68736
[startup+460.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16371 0 0 0 45956 48 0 0 25 0 1 0 422698581 71319552 16074 4294967295 134512640 134672761 3221224560 3221223728 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17412 16074 603 41 0 17371 0
vsize: 69648
[startup+470.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16506 0 0 0 46956 48 0 0 25 0 1 0 422698581 71860224 16209 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17544 16209 603 41 0 17503 0
vsize: 70176
[startup+480.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16560 0 0 0 47955 48 0 0 25 0 1 0 422698581 72060928 16263 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17593 16263 603 41 0 17552 0
vsize: 70372
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16560 0 0 0 48956 48 0 0 25 0 1 0 422698581 72060928 16263 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17593 16263 603 41 0 17552 0
vsize: 70372
[startup+500.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16560 0 0 0 49956 48 0 0 25 0 1 0 422698581 72060928 16263 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17593 16263 603 41 0 17552 0
vsize: 70372
[startup+510.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16560 0 0 0 50956 48 0 0 25 0 1 0 422698581 72060928 16263 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17593 16263 603 41 0 17552 0
vsize: 70372
[startup+520.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16560 0 0 0 51956 48 0 0 25 0 1 0 422698581 72060928 16263 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17593 16263 603 41 0 17552 0
vsize: 70372
[startup+530.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16560 0 0 0 52956 48 0 0 25 0 1 0 422698581 72060928 16263 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17593 16263 603 41 0 17552 0
vsize: 70372
[startup+540.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16560 0 0 0 53956 48 0 0 25 0 1 0 422698581 72060928 16263 4294967295 134512640 134672761 3221224560 3221223664 134560379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17593 16263 603 41 0 17552 0
vsize: 70372
[startup+550.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16560 0 0 0 54957 49 0 0 25 0 1 0 422698581 72060928 16263 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17593 16263 603 41 0 17552 0
vsize: 70372
[startup+560.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16560 0 0 0 55957 49 0 0 25 0 1 0 422698581 72060928 16263 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17593 16263 603 41 0 17552 0
vsize: 70372
[startup+570.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16560 0 0 0 56957 49 0 0 25 0 1 0 422698581 72060928 16263 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17593 16263 603 41 0 17552 0
vsize: 70372
[startup+580.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16560 0 0 0 57957 49 0 0 25 0 1 0 422698581 72060928 16263 4294967295 134512640 134672761 3221224560 3221223664 134560226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17593 16263 603 41 0 17552 0
vsize: 70372
[startup+590.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16560 0 0 0 58957 49 0 0 25 0 1 0 422698581 72060928 16263 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17593 16263 603 41 0 17552 0
vsize: 70372
[startup+600.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16560 0 0 0 59958 49 0 0 25 0 1 0 422698581 72060928 16263 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17593 16263 603 41 0 17552 0
vsize: 70372
[startup+610.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16560 0 0 0 60958 49 0 0 25 0 1 0 422698581 72060928 16263 4294967295 134512640 134672761 3221224560 3221223728 134561275 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17593 16263 603 41 0 17552 0
vsize: 70372
[startup+620.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16560 0 0 0 61958 49 0 0 25 0 1 0 422698581 72060928 16263 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17593 16263 603 41 0 17552 0
vsize: 70372
[startup+630.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16560 0 0 0 62958 49 0 0 25 0 1 0 422698581 72060928 16263 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17593 16263 603 41 0 17552 0
vsize: 70372
[startup+640.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16560 0 0 0 63958 49 0 0 25 0 1 0 422698581 72060928 16263 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17593 16263 603 41 0 17552 0
vsize: 70372
[startup+650.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16560 0 0 0 64959 49 0 0 25 0 1 0 422698581 72060928 16263 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17593 16263 603 41 0 17552 0
vsize: 70372
[startup+660.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16560 0 0 0 65959 49 0 0 25 0 1 0 422698581 72060928 16263 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17593 16263 603 41 0 17552 0
vsize: 70372
[startup+670.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16560 0 0 0 66959 49 0 0 25 0 1 0 422698581 72060928 16263 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17593 16263 603 41 0 17552 0
vsize: 70372
[startup+680.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16560 0 0 0 67959 49 0 0 25 0 1 0 422698581 72060928 16263 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17593 16263 603 41 0 17552 0
vsize: 70372
[startup+690.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16560 0 0 0 68959 49 0 0 25 0 1 0 422698581 72060928 16263 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17593 16263 603 41 0 17552 0
vsize: 70372
[startup+700.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16560 0 0 0 69960 49 0 0 25 0 1 0 422698581 72060928 16263 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17593 16263 603 41 0 17552 0
vsize: 70372
[startup+710.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16560 0 0 0 70960 49 0 0 25 0 1 0 422698581 72060928 16263 4294967295 134512640 134672761 3221224560 3221223760 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17593 16263 603 41 0 17552 0
vsize: 70372
[startup+720.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16560 0 0 0 71960 49 0 0 25 0 1 0 422698581 72060928 16263 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17593 16263 603 41 0 17552 0
vsize: 70372
[startup+730.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16560 0 0 0 72960 49 0 0 25 0 1 0 422698581 72060928 16263 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17593 16263 603 41 0 17552 0
vsize: 70372
[startup+740.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16560 0 0 0 73960 49 0 0 25 0 1 0 422698581 72060928 16263 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17593 16263 603 41 0 17552 0
vsize: 70372
[startup+750.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16560 0 0 0 74961 49 0 0 25 0 1 0 422698581 72060928 16263 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17593 16263 603 41 0 17552 0
vsize: 70372
[startup+760.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16560 0 0 0 75961 49 0 0 25 0 1 0 422698581 72060928 16263 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17593 16263 603 41 0 17552 0
vsize: 70372
[startup+770.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16561 0 0 0 76961 49 0 0 25 0 1 0 422698581 72060928 16264 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17593 16264 603 41 0 17552 0
vsize: 70372
[startup+780.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16562 0 0 0 77961 49 0 0 25 0 1 0 422698581 72060928 16265 4294967295 134512640 134672761 3221224560 3221223664 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17593 16265 603 41 0 17552 0
vsize: 70372
[startup+790.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16564 0 0 0 78961 49 0 0 25 0 1 0 422698581 72060928 16267 4294967295 134512640 134672761 3221224560 3221223664 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17593 16267 603 41 0 17552 0
vsize: 70372
[startup+800.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16565 0 0 0 79962 49 0 0 25 0 1 0 422698581 72060928 16268 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17593 16268 603 41 0 17552 0
vsize: 70372
[startup+810.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16566 0 0 0 80962 49 0 0 25 0 1 0 422698581 72060928 16269 4294967295 134512640 134672761 3221224560 3221223664 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17593 16269 603 41 0 17552 0
vsize: 70372
[startup+820.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16567 0 0 0 81962 49 0 0 25 0 1 0 422698581 72060928 16270 4294967295 134512640 134672761 3221224560 3221223728 134560845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17593 16270 603 41 0 17552 0
vsize: 70372
[startup+830.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16568 0 0 0 82962 49 0 0 25 0 1 0 422698581 72060928 16271 4294967295 134512640 134672761 3221224560 3221223664 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17593 16271 603 41 0 17552 0
vsize: 70372
[startup+840.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16569 0 0 0 83962 49 0 0 25 0 1 0 422698581 72060928 16272 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17593 16272 603 41 0 17552 0
vsize: 70372
[startup+850.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16571 0 0 0 84962 49 0 0 25 0 1 0 422698581 72060928 16274 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17593 16274 603 41 0 17552 0
vsize: 70372
[startup+860.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16572 0 0 0 85962 49 0 0 25 0 1 0 422698581 72060928 16275 4294967295 134512640 134672761 3221224560 3221223728 134561226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17593 16275 603 41 0 17552 0
vsize: 70372
[startup+870.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16573 0 0 0 86962 49 0 0 25 0 1 0 422698581 72060928 16276 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17593 16276 603 41 0 17552 0
vsize: 70372
[startup+880.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16650 0 0 0 87962 49 0 0 25 0 1 0 422698581 72454144 16353 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17689 16353 603 41 0 17648 0
vsize: 70756
[startup+890.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16777 0 0 0 88962 50 0 0 25 0 1 0 422698581 72974336 16480 4294967295 134512640 134672761 3221224560 3221223760 134557822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17816 16480 603 41 0 17775 0
vsize: 71264
[startup+900.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 16935 0 0 0 89961 50 0 0 25 0 1 0 422698581 73633792 16638 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17977 16638 603 41 0 17936 0
vsize: 71908
[startup+910.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 17103 0 0 0 90961 51 0 0 25 0 1 0 422698581 74289152 16806 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18137 16806 603 41 0 18096 0
vsize: 72548
[startup+920.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 17246 0 0 0 91961 51 0 0 25 0 1 0 422698581 74813440 16949 4294967295 134512640 134672761 3221224560 3221223760 134557915 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18265 16949 603 41 0 18224 0
vsize: 73060
[startup+930.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 17417 0 0 0 92961 52 0 0 25 0 1 0 422698581 75485184 17120 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18429 17120 603 41 0 18388 0
vsize: 73716
[startup+940.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 17567 0 0 0 93961 52 0 0 25 0 1 0 422698581 76148736 17270 4294967295 134512640 134672761 3221224560 3221223716 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18591 17270 603 41 0 18550 0
vsize: 74364
[startup+950.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 17774 0 0 0 94959 53 0 0 25 0 1 0 422698581 76939264 17477 4294967295 134512640 134672761 3221224560 3221223664 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18784 17477 603 41 0 18743 0
vsize: 75136
[startup+960.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 17948 0 0 0 95959 54 0 0 25 0 1 0 422698581 77742080 17651 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18980 17651 603 41 0 18939 0
vsize: 75920
[startup+970.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 18141 0 0 0 96958 55 0 0 25 0 1 0 422698581 78548992 17844 4294967295 134512640 134672761 3221224560 3221223664 134560158 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19177 17844 603 41 0 19136 0
vsize: 76708
[startup+980.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 18270 0 0 0 97958 55 0 0 25 0 1 0 422698581 79089664 17973 4294967295 134512640 134672761 3221224560 3221223664 134560134 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19309 17973 603 41 0 19268 0
vsize: 77236
[startup+990.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 18440 0 0 0 98958 56 0 0 25 0 1 0 422698581 79745024 18143 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19469 18143 603 41 0 19428 0
vsize: 77876
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 18615 0 0 0 99957 56 0 0 25 0 1 0 422698581 80396288 18318 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19628 18318 603 41 0 19587 0
vsize: 78512
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 18776 0 0 0 100957 57 0 0 25 0 1 0 422698581 81051648 18479 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19788 18479 603 41 0 19747 0
vsize: 79152
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 18942 0 0 0 101957 57 0 0 25 0 1 0 422698581 81715200 18645 4294967295 134512640 134672761 3221224560 3221223664 134559981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19950 18645 603 41 0 19909 0
vsize: 79800
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 19101 0 0 0 102957 57 0 0 25 0 1 0 422698581 82386944 18804 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20114 18804 603 41 0 20073 0
vsize: 80456
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 19274 0 0 0 103956 58 0 0 25 0 1 0 422698581 83050496 18977 4294967295 134512640 134672761 3221224560 3221223728 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20276 18977 603 41 0 20235 0
vsize: 81104
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 19452 0 0 0 104956 59 0 0 25 0 1 0 422698581 83836928 19155 4294967295 134512640 134672761 3221224560 3221223696 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20468 19155 603 41 0 20427 0
vsize: 81872
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 19627 0 0 0 105956 59 0 0 25 0 1 0 422698581 84504576 19330 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20631 19330 603 41 0 20590 0
vsize: 82524
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 19828 0 0 0 106956 59 0 0 25 0 1 0 422698581 85303296 19531 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20826 19531 603 41 0 20785 0
vsize: 83304
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 19992 0 0 0 107955 60 0 0 25 0 1 0 422698581 86093824 19695 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21019 19695 603 41 0 20978 0
vsize: 84076
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 20158 0 0 0 108955 60 0 0 25 0 1 0 422698581 86761472 19861 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21182 19861 603 41 0 21141 0
vsize: 84728
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 20258 0 0 0 109954 61 0 0 25 0 1 0 422698581 87158784 19961 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21279 19961 603 41 0 21238 0
vsize: 85116
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 20410 0 0 0 110955 61 0 0 25 0 1 0 422698581 87699456 20113 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21411 20113 603 41 0 21370 0
vsize: 85644
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 20591 0 0 0 111954 61 0 0 25 0 1 0 422698581 88506368 20294 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21608 20294 603 41 0 21567 0
vsize: 86432
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 20771 0 0 0 112954 62 0 0 25 0 1 0 422698581 89182208 20474 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21773 20474 603 41 0 21732 0
vsize: 87092
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 20965 0 0 0 113954 63 0 0 25 0 1 0 422698581 89980928 20668 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21968 20668 603 41 0 21927 0
vsize: 87872
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 21084 0 0 0 114953 63 0 0 25 0 1 0 422698581 90513408 20787 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22098 20787 603 41 0 22057 0
vsize: 88392
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 21153 0 0 0 115953 63 0 0 25 0 1 0 422698581 90775552 20856 4294967295 134512640 134672761 3221224560 3221223728 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22162 20856 603 41 0 22121 0
vsize: 88648
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 21223 0 0 0 116953 64 0 0 25 0 1 0 422698581 91037696 20926 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22226 20926 603 41 0 22185 0
vsize: 88904
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 21364 0 0 0 117953 64 0 0 25 0 1 0 422698581 91553792 21067 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22352 21067 603 41 0 22311 0
vsize: 89408
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 21490 0 0 0 118953 64 0 0 25 0 1 0 422698581 92094464 21193 4294967295 134512640 134672761 3221224560 3221223664 134559908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22484 21193 603 41 0 22443 0
vsize: 89936
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28770
Raw data (stat): 28770 (minisat+) R 28769 24215 24214 0 -1 0 21676 0 0 0 119952 65 0 0 25 0 1 0 422698581 92901376 21379 4294967295 134512640 134672761 3221224560 3221223664 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22681 21379 603 41 0 22640 0
vsize: 90724
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 28770
Raw data (stat): 28770 (minisat+) Z 28769 24215 24214 0 -1 12 21679 0 0 0 119953 69 0 0 25 0 1 0 422698581 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.23
CPU user time (s): 1199.53
CPU system time (s): 0.695894
CPU usage (%): 100.012
Max. virtual memory (Kb): 90724
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####