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/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-gt2.opb
MD5SUM	f1382105ee9fb79777762a53cf6a73c1
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	21166
Optimality of the best value was proved	NO
Number of terms in the objective function	304
Biggest coefficient in the objective function	62376
Number of bits for the biggest coefficient in the objective function	16
Sum of the numbers in the objective function	3092598
Number of bits of the sum of numbers in the objective function	22
Biggest number in a constraint	62376
Number of bits of the biggest number in a constraint	16
Biggest sum of numbers in a constraint	3092598
Number of bits of the biggest sum of numbers	22
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.14
Number of variables	556
Total number of constraints	217
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	26
Number of constraints which are nor clauses,nor cardinality constraints	191
Minimum length of a constraint	1
Maximum length of a constraint	48
Trace number 18200

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc21 THE 2005-04-21 13:53:40 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18447 boxname=wulflinc21 idbench=1419 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f1382105ee9fb79777762a53cf6a73c1  /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-gt2.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-gt2.opb /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-gt2.opb
IDLAUNCH: 18447
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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:        868252 kB
Buffers:          2208 kB
Cached:         142088 kB
SwapCached:          0 kB
Active:          23380 kB
Inactive:       123820 kB
HighTotal:      131008 kB
HighFree:        82880 kB
LowTotal:       903652 kB
LowFree:        785372 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           6952 kB
Slab:            13424 kB
Committed_AS:    63796 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 14:13:42 (client local time) WITH STATUS 10 IN 1200.25 SECONDS
stats: 18447 7 1200.25 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 180 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................................................................ssssssssss
c ---[ 189]---> BDD-cost:    2
c ---[ 188]---> BDD-cost:    2
c ---[ 187]---> BDD-cost:    2
c ---[ 186]---> BDD-cost:    2
c ---[ 185]---> BDD-cost:    2
c ---[ 184]---> BDD-cost:    2
c ---[ 183]---> BDD-cost:    2
c ---[ 182]---> BDD-cost:    2
c ---[ 157]---> BDD-cost:    3
c ---[ 156]---> BDD-cost:    3
c ---[ 155]---> BDD-cost:    3
c ---[ 154]---> BDD-cost:    3
c ---[ 153]---> BDD-cost:    3
c ---[ 152]---> BDD-cost:    3
c ---[ 151]---> BDD-cost:    3
c ---[ 150]---> BDD-cost:    3
c ---[ 149]---> BDD-cost:    3
c ---[ 148]---> BDD-cost:    3
c ---[ 147]---> BDD-cost:    3
c ---[ 146]---> BDD-cost:    3
c ---[ 141]---> BDD-cost:    3
c ---[ 140]---> BDD-cost:    3
c ---[ 139]---> BDD-cost:    3
c ---[ 138]---> BDD-cost:    3
c ---[ 137]---> BDD-cost:    3
c ---[ 136]---> BDD-cost:    3
c ---[ 135]---> BDD-cost:    3
c ---[ 134]---> BDD-cost:    3
c ---[ 120]---> BDD-cost:    2
c ---[ 119]---> BDD-cost:    2
c ---[ 117]---> BDD-cost:    2
c ---[ 113]---> BDD-cost:    2
c ---[ 112]---> BDD-cost:    2
c ---[ 110]---> BDD-cost:    2
c ---[ 106]---> BDD-cost:    2
c ---[ 105]---> BDD-cost:    2
c ---[ 103]---> BDD-cost:    2
c ---[  99]---> BDD-cost:    2
c ---[  98]---> BDD-cost:    2
c ---[  96]---> BDD-cost:    2
c ---[  92]---> BDD-cost:    2
c ---[  91]---> BDD-cost:    2
c ---[  89]---> BDD-cost:    2
c ---[  85]---> BDD-cost:    2
c ---[  84]---> BDD-cost:    2
c ---[  82]---> BDD-cost:    2
c ---[  78]---> BDD-cost:    2
c ---[  77]---> BDD-cost:    2
c ---[  75]---> BDD-cost:    2
c ---[  71]---> BDD-cost:    2
c ---[  70]---> BDD-cost:    2
c ---[  68]---> BDD-cost:    2
c ---[  64]---> BDD-cost:    2
c ---[  63]---> BDD-cost:    2
c ---[  61]---> BDD-cost:    2
c ---[  57]---> BDD-cost:    2
c ---[  56]---> BDD-cost:    2
c ---[  54]---> BDD-cost:    2
c ---[  50]---> BDD-cost:    2
c ---[  49]---> BDD-cost:    2
c ---[  47]---> BDD-cost:    2
c ---[  43]---> BDD-cost:    2
c ---[  42]---> BDD-cost:    2
c ---[  40]---> BDD-cost:    2
c ---[  37]---> BDD-cost:  107
c ---[  36]---> Sorter-cost:  778     Base: 2 2 2
c ---[  35]---> Sorter-cost:  777     Base: 2 2 2
c ---[  34]---> BDD-cost:   21
c ---[  33]---> BDD-cost:  128
c ---[  32]---> BDD-cost:  183
c ---[  31]---> BDD-cost:   25
c ---[  30]---> Sorter-cost:  379     Base: 2 2 2
c ---[  29]---> BDD-cost:  111
c ---[  28]---> BDD-cost:  128
c ---[  27]---> BDD-cost:  105
c ---[  26]---> Sorter-cost:  778     Base: 2 2 2
c ---[  25]---> BDD-cost:  111
c ---[  24]---> BDD-cost:  105
c ---[  23]---> BDD-cost:   54
c ---[  22]---> BDD-cost:   54
c ---[  21]---> BDD-cost:   21
c ---[  15]---> Adder-cost: 273   maxlim: 12127   bits: 15/14
c ---[   9]---> Sorter-cost: 2085     Base: 2 5 2 2 2
c ---[   8]---> BDD-cost:   76
c ---[   7]---> Sorter-cost: 2550     Base: 2 5 2 2 2
c ---[   6]---> Adder-cost: 223   maxlim: 249   bits: 9/8
c ---[   5]---> BDD-cost:   48
c ---[   4]---> BDD-cost:  114
c ---[   3]---> BDD-cost:   55
c ---[   2]---> Sorter-cost: 2935     Base: 2 5 2 2 2 2
c ---[   1]---> Adder-cost: 212   maxlim: 230   bits: 9/8
c ---[   0]---> BDD-cost:   92
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   37128    96740 |   12376       0        0     nan |  0.000 % |
c |       100 |   37128    96740 |   13613     100     1068    10.7 |  0.987 % |
c |       250 |   37128    96740 |   14974     250     6753    27.0 |  0.986 % |
c |       475 |   37128    96740 |   16472     475    11658    24.5 |  0.986 % |
c ==============================================================================
c [1mFound solution: 272921[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:92425     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       730 |  301625   715849 |  100541     725    18314    25.3 |  0.986 % |
c |       832 |  301625   715849 |  110595     827    19489    23.6 |  0.112 % |
c |       982 |  301625   715849 |  121654     977    20840    21.3 |  0.112 % |
c |      1208 |  299431   710877 |  133820    1198    22954    19.2 |  0.706 % |
c |      1545 |  297116   705586 |  147202    1527    31556    20.7 |  1.368 % |
c |      2051 |  289762   688651 |  161922    1908    38949    20.4 |  3.614 % |
c |      2810 |  289762   688651 |  178114    2667    80109    30.0 |  3.614 % |
c |      3950 |  283184   673472 |  195925    3691   115263    31.2 |  5.642 % |
c |      5659 |  280877   668143 |  215518    5389   171535    31.8 |  6.362 % |
c |      8221 |  279105   664045 |  237070    7940   248832    31.3 |  6.924 % |
c |     12065 |  268746   640058 |  260777   11613   305597    26.3 | 10.222 % |
c |     17831 |  263652   628277 |  286855   17293   477584    27.6 | 11.839 % |
c ==============================================================================
c [1mFound solution: 220110[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18032 |  264157   629680 |   88052   17494   489718    28.0 | 11.839 % |
c |     18132 |  263330   627764 |   96857   17586   490329    27.9 | 12.100 % |
c |     18282 |  261853   624344 |  106542   17715   492446    27.8 | 12.570 % |
c |     18509 |  261848   624329 |  117197   17923   494203    27.6 | 12.571 % |
c |     18846 |  261485   623489 |  128916   18253   504496    27.6 | 12.688 % |
c |     19352 |  261367   623216 |  141808   18757   511514    27.3 | 12.728 % |
c |     20111 |  259027   617786 |  155989   19483   529003    27.2 | 13.486 % |
c |     21251 |  258653   616915 |  171588   20619   585969    28.4 | 13.612 % |
c |     22960 |  258509   616583 |  188747   22326   625627    28.0 | 13.659 % |
c ==============================================================================
c [1mFound solution: 214843[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23285 |  257667   614697 |   85889   22636   641420    28.3 | 13.659 % |
c |     23385 |  257667   614697 |   94477   22736   643957    28.3 | 13.986 % |
c |     23535 |  257667   614697 |  103925   22886   650768    28.4 | 13.986 % |
c |     23760 |  257662   614682 |  114318   23110   652717    28.2 | 13.987 % |
c |     24101 |  256799   612688 |  125750   23381   654454    28.0 | 14.262 % |
c |     24608 |  253879   605922 |  138325   23818   659463    27.7 | 15.191 % |
c |     25369 |  251728   600929 |  152157   24464   673900    27.5 | 15.880 % |
c |     26508 |  251728   600929 |  167373   25603   752124    29.4 | 15.880 % |
c |     28216 |  251728   600929 |  184110   27311   792319    29.0 | 15.880 % |
c |     30779 |  249148   594949 |  202521   29784   907203    30.5 | 16.715 % |
c |     34625 |  247285   590650 |  222773   33582  1208238    36.0 | 17.301 % |
c |     40391 |  245384   586235 |  245051   39061  1416212    36.3 | 17.914 % |
c |     49040 |  243637   582182 |  269556   47541  1865089    39.2 | 18.471 % |
c ==============================================================================
c [1mFound solution: 211135[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:70617     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     54725 |  402113   951620 |  134037   53200  2505608    47.1 | 18.471 % |
c |     54825 |  402089   951567 |  147440   53299  2509252    47.1 | 18.996 % |
c |     54976 |  402082   951552 |  162184   53449  2517139    47.1 | 18.998 % |
c |     55201 |  402017   951405 |  178403   53672  2519564    46.9 | 19.008 % |
c |     55539 |  402017   951405 |  196243   54010  2561558    47.4 | 19.008 % |
c |     56045 |  402017   951405 |  215867   54516  2577112    47.3 | 19.008 % |
c |     56804 |  402017   951405 |  237454   55275  2585403    46.8 | 19.008 % |
c |     57943 |  399040   944728 |  261200   56305  2658077    47.2 | 19.582 % |
c |     59651 |  399030   944705 |  287320   58011  2729715    47.1 | 19.583 % |
c |     62213 |  399030   944705 |  316052   60573  2841044    46.9 | 19.583 % |
c |     66057 |  396738   939491 |  347657   64271  3170358    49.3 | 20.017 % |
c |     71823 |  392797   930473 |  382423   69837  3472038    49.7 | 20.768 % |
c |     80473 |  390063   924235 |  420665   78441  4424846    56.4 | 21.298 % |
c ==============================================================================
c [1mFound solution: 149717[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:36798     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     80550 |  465741  1100763 |  155247   78518  4427471    56.4 | 21.298 % |
c |     80651 |  465713  1100701 |  170771   78618  4428193    56.3 | 21.799 % |
c |     80802 |  465713  1100701 |  187848   78769  4440749    56.4 | 21.799 % |
c ==============================================================================
c [1mFound solution: 143232[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     80864 |  466037  1101637 |  155345   78831  4443808    56.4 | 21.799 % |
c |     80966 |  466037  1101637 |  170879   78933  4445482    56.3 | 21.797 % |
c |     81116 |  466037  1101637 |  187967   79083  4452649    56.3 | 21.797 % |
c |     81341 |  465700  1100876 |  206764   79298  4455807    56.2 | 21.849 % |
c |     81680 |  459578  1086951 |  227440   79144  4460629    56.4 | 22.835 % |
c |     82186 |  459578  1086951 |  250184   79650  4576870    57.5 | 22.835 % |
c |     82945 |  459578  1086951 |  275203   80409  4602204    57.2 | 22.835 % |
c |     84084 |  459211  1086106 |  302723   81298  4626271    56.9 | 22.895 % |
c |     85793 |  454770  1075975 |  332995   82872  4704474    56.8 | 23.597 % |
c |     88356 |  454770  1075975 |  366295   85435  4874882    57.1 | 23.597 % |
c |     92201 |  453222  1072495 |  402924   89256  5153781    57.7 | 23.834 % |
c |     97969 |  449282  1063489 |  443217   94692  5267087    55.6 | 24.475 % |
c ==============================================================================
c [1mFound solution: 142835[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:36103     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    105244 |  519521  1227128 |  173173  101371  5997375    59.2 | 24.475 % |
c |    105344 |  518973  1225900 |  190490  101458  5998409    59.1 | 25.028 % |
c |    105494 |  518802  1225503 |  209539  101594  5999297    59.1 | 25.051 % |
c |    105720 |  518802  1225503 |  230493  101820  6013740    59.1 | 25.051 % |
c |    106057 |  518802  1225503 |  253542  102157  6020260    58.9 | 25.051 % |
c |    106563 |  518647  1225142 |  278896  102653  6042955    58.9 | 25.074 % |
c |    107322 |  518647  1225142 |  306786  103412  6164753    59.6 | 25.074 % |
c |    108461 |  518623  1225088 |  337465  104549  6216022    59.5 | 25.077 % |
c |    110170 |  517463  1222456 |  371211  106038  6245098    58.9 | 25.235 % |
c |    112732 |  517053  1221543 |  408332  108596  6385609    58.8 | 25.293 % |
c |    116578 |  517020  1221463 |  449166  112439  6702903    59.6 | 25.296 % |
c |    122344 |  512717  1211635 |  494082  117816  7552298    64.1 | 25.903 % |
c |    130997 |  507434  1199587 |  543491  126273  8054910    63.8 | 26.635 % |
c ==============================================================================
c [1mFound solution: 140979[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    133550 |  505360  1195075 |  168453  128539  8171207    63.6 | 26.635 % |
c |    133650 |  505360  1195075 |  185298  128639  8183518    63.6 | 26.962 % |
c |    133802 |  505360  1195075 |  203828  128791  8189770    63.6 | 26.962 % |
c |    134027 |  504318  1192690 |  224210  128967  8193048    63.5 | 27.106 % |
c |    134364 |  504318  1192690 |  246632  129304  8201139    63.4 | 27.106 % |
c |    134870 |  504056  1192091 |  271295  129643  8202842    63.3 | 27.145 % |
c |    135629 |  503828  1191572 |  298424  130338  8228275    63.1 | 27.177 % |
c |    136768 |  503828  1191572 |  328267  131477  8406988    63.9 | 27.177 % |
c |    138476 |  502367  1188188 |  361093  132965  8420498    63.3 | 27.374 % |
c |    141038 |  502246  1187916 |  397203  135523  8537448    63.0 | 27.389 % |
c |    144883 |  499272  1181117 |  436923  139255  8887919    63.8 | 27.797 % |
c |    150649 |  498927  1180334 |  480616  145013  9427129    65.0 | 27.839 % |
c ==============================================================================
c [1mFound solution: 88982[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:68304     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    151511 |  642907  1515619 |  214302  145872  9499648    65.1 | 27.839 % |
c |    151614 |  642888  1515577 |  235732  145974  9504895    65.1 | 27.056 % |
c |    151765 |  642888  1515577 |  259305  146125  9512157    65.1 | 27.056 % |
c |    151990 |  642883  1515562 |  285235  146349  9529537    65.1 | 27.056 % |
c |    152328 |  642883  1515562 |  313759  146687  9571361    65.3 | 27.056 % |
c |    152835 |  642878  1515547 |  345135  147193  9610486    65.3 | 27.057 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x_0x2e__0x2e__0x2e_0101_bit0 -x_0x2e__0x2e__0x2e_0101_bit1 -x_0x2e__0x2e__0x2e_0101_bit2 -x_0x2e__0x2e__0x2e_0101_bit3 -x_0x2e__0x2e__0x2e_0201_bit0 -x_0x2e__0x2e__0x2e_0201_bit1 -x_0x2e__0x2e__0x2e_0201_bit2 -x_0x2e__0x2e__0x2e_0201_bit3 -x_0x2e__0x2e__0x2e_0301_bit0 -x_0x2e__0x2e__0x2e_0301_bit1 x_0x2e__0x2e__0x2e_0301_bit2 -x_0x2e__0x2e__0x2e_0301_bit3 -x_0x2e__0x2e__0x2e_0401_bit0 -x_0x2e__0x2e__0x2e_0401_bit1 -x_0x2e__0x2e__0x2e_0401_bit2 -x_0x2e__0x2e__0x2e_0401_bit3 -x_0x2e__0x2e__0x2e_0701_bit0 -x_0x2e__0x2e__0x2e_0701_bit1 -x_0x2e__0x2e__0x2e_0701_bit2 -x_0x2e__0x2e__0x2e_0701_bit3 -x_0x2e__0x2e__0x2e_0801_bit0 -x_0x2e__0x2e__0x2e_0801_bit1 -x_0x2e__0x2e__0x2e_0801_bit2 -x_0x2e__0x2e__0x2e_0801_bit3 -x_0x2e__0x2e__0x2e_0901_bit0 -x_0x2e__0x2e__0x2e_0901_bit1 x_0x2e__0x2e__0x2e_0901_bit2 -x_0x2e__0x2e__0x2e_0901_bit3 -x_0x2e__0x2e__0x2e_1001_bit0 -x_0x2e__0x2e__0x2e_1001_bit1 -x_0x2e__0x2e__0x2e_1001_bit2 -x_0x2e__0x2e__0x2e_1001_bit3 -x_0x2e__0x2e__0x2e_0102_bit0 -x_0x2e__0x2e__0x2e_0102_bit1 -x_0x2e__0x2e__0x2e_0102_bit2 -x_0x2e__0x2e__0x2e_0102_bit3 -x_0x2e__0x2e__0x2e_0202_bit0 -x_0x2e__0x2e__0x2e_0202_bit1 -x_0x2e__0x2e__0x2e_0202_bit2 -x_0x2e__0x2e__0x2e_0202_bit3 -x_0x2e__0x2e__0x2e_0302_bit0 -x_0x2e__0x2e__0x2e_0302_bit1 -x_0x2e__0x2e__0x2e_0302_bit2 -x_0x2e__0x2e__0x2e_0302_bit3 -x_0x2e__0x2e__0x2e_0402_bit0 x_0x2e__0x2e__0x2e_0402_bit1 -x_0x2e__0x2e__0x2e_0402_bit2 -x_0x2e__0x2e__0x2e_0402_bit3 -x_0x2e__0x2e__0x2e_0502_bit0 -x_0x2e__0x2e__0x2e_0502_bit1 -x_0x2e__0x2e__0x2e_0502_bit2 -x_0x2e__0x2e__0x2e_0502_bit3 -x_0x2e__0x2e__0x2e_0602_bit0 -x_0x2e__0x2e__0x2e_0602_bit1 -x_0x2e__0x2e__0x2e_0602_bit2 -x_0x2e__0x2e__0x2e_0602_bit3 -x_0x2e__0x2e__0x2e_0702_bit0 -x_0x2e__0x2e__0x2e_0702_bit1 -x_0x2e__0x2e__0x2e_0702_bit2 -x_0x2e__0x2e__0x2e_0702_bit3 -x_0x2e__0x2e__0x2e_0802_bit0 -x_0x2e__0x2e__0x2e_0802_bit1 -x_0x2e__0x2e__0x2e_0802_bit2 -x_0x2e__0x2e__0x2e_0802_bit3 -x_0x2e__0x2e__0x2e_0902_bit0 -x_0x2e__0x2e__0x2e_0902_bit1 -x_0x2e__0x2e__0x2e_0902_bit2 x_0x2e__0x2e__0x2e_0902_bit3 -x_0x2e__0x2e__0x2e_1002_bit0 -x_0x2e__0x2e__0x2e_1002_bit1 -x_0x2e__0x2e__0x2e_1002_bit2 -x_0x2e__0x2e__0x2e_1002_bit3 -x_0x2e__0x2e__0x2e_1102_bit0 -x_0x2e__0x2e__0x2e_1102_bit1 -x_0x2e__0x2e__0x2e_1102_bit2 -x_0x2e__0x2e__0x2e_1102_bit3 -x_0x2e__0x2e__0x2e_1202_bit0 -x_0x2e__0x2e__0x2e_1202_bit1 -x_0x2e__0x2e__0x2e_1202_bit2 -x_0x2e__0x2e__0x2e_1202_bit3 -x_0x2e__0x2e__0x2e_0103_bit0 -x_0x2e__0x2e__0x2e_0103_bit1 -x_0x2e__0x2e__0x2e_0103_bit2 -x_0x2e__0x2e__0x2e_0103_bit3 -x_0x2e__0x2e__0x2e_0203_bit0 -x_0x2e__0x2e__0x2e_0203_bit1 -x_0x2e__0x2e__0x2e_0203_bit2 -x_0x2e__0x2e__0x2e_0203_bit3 -x_0x2e__0x2e__0x2e_0303_bit0 -x_0x2e__0x2e__0x2e_0303_bit1 -x_0x2e__0x2e__0x2e_0303_bit2 x_0x2e__0x2e__0x2e_0303_bit3 -x_0x2e__0x2e__0x2e_0403_bit0 -x_0x2e__0x2e__0x2e_0403_bit1 -x_0x2e__0x2e__0x2e_0403_bit2 -x_0x2e__0x2e__0x2e_0403_bit3 -x_0x2e__0x2e__0x2e_0503_bit0 -x_0x2e__0x2e__0x2e_0503_bit1 -x_0x2e__0x2e__0x2e_0503_bit2 -x_0x2e__0x2e__0x2e_0503_bit3 -x_0x2e__0x2e__0x2e_0603_bit0 -x_0x2e__0x2e__0x2e_0603_bit1 -x_0x2e__0x2e__0x2e_0603_bit2 -x_0x2e__0x2e__0x2e_0603_bit3 -x_0x2e__0x2e__0x2e_0703_bit0 -x_0x2e__0x2e__0x2e_0703_bit1 -x_0x2e__0x2e__0x2e_0703_bit2 -x_0x2e__0x2e__0x2e_0703_bit3 -x_0x2e__0x2e__0x2e_0803_bit0 -x_0x2e__0x2e__0x2e_0803_bit1 -x_0x2e__0x2e__0x2e_0803_bit2 -x_0x2e__0x2e__0x2e_0803_bit3 -x_0x2e__0x2e__0x2e_0903_bit0 -x_0x2e__0x2e__0x2e_0903_bit1 -x_0x2e__0x2e__0x2e_0903_bit2 -x_0x2e__0x2e__0x2e_0903_bit3 -x_0x2e__0x2e__0x2e_1003_bit0 -x_0x2e__0x2e__0x2e_1003_bit1 -x_0x2e__0x2e__0x2e_1003_bit2 -x_0x2e__0x2e__0x2e_1003_bit3 -x_0x2e__0x2e__0x2e_1103_bit0 -x_0x2e__0x2e__0x2e_1103_bit1 -x_0x2e__0x2e__0x2e_1103_bit2 -x_0x2e__0x2e__0x2e_1103_bit3 -x_0x2e__0x2e__0x2e_1203_bit0 -x_0x2e__0x2e__0x2e_1203_bit1 -x_0x2e__0x2e__0x2e_1203_bit2 -x_0x2e__0x2e__0x2e_1203_bit3 -x_0x2e__0x2e__0x2e_0104_bit0 -x_0x2e__0x2e__0x2e_0204_bit0 -x_0x2e__0x2e__0x2e_0304_bit0 -x_0x2e__0x2e__0x2e_0404_bit0 -x_0x2e__0x2e__0x2e_0504_bit0 -x_0x2e__0x2e__0x2e_0604_bit0 -x_0x2e__0x2e__0x2e_0704_bit0 -x_0x2e__0x2e__0x2e_0804_bit0 x_0x2e__0x2e__0x2e_0904_bit0 -x_0x2e__0x2e__0x2e_1004_bit0 -x_0x2e__0x2e__0x2e_1104_bit0 -x_0x2e__0x2e__0x2e_1204_bit0 -x_0x2e__0x2e__0x2e_0105_bit0 -x_0x2e__0x2e__0x2e_0105_bit1 -x_0x2e__0x2e__0x2e_0105_bit2 -x_0x2e__0x2e__0x2e_0205_bit0 -x_0x2e__0x2e__0x2e_0205_bit1 -x_0x2e__0x2e__0x2e_0205_bit2 -x_0x2e__0x2e__0x2e_0305_bit0 -x_0x2e__0x2e__0x2e_0305_bit1 -x_0x2e__0x2e__0x2e_0305_bit2 -x_0x2e__0x2e__0x2e_0405_bit0 -x_0x2e__0x2e__0x2e_0405_bit1 -x_0x2e__0x2e__0x2e_0405_bit2 -x_0x2e__0x2e__0x2e_0505_bit0 -x_0x2e__0x2e__0x2e_0505_bit1 -x_0x2e__0x2e__0x2e_0505_bit2 -x_0x2e__0x2e__0x2e_0605_bit0 -x_0x2e__0x2e__0x2e_0605_bit1 -x_0x2e__0x2e__0x2e_0605_bit2 -x_0x2e__0x2e__0x2e_0705_bit0 -x_0x2e__0x2e__0x2e_0705_bit1 -x_0x2e__0x2e__0x2e_0705_bit2 -x_0x2e__0x2e__0x2e_0805_bit0 -x_0x2e__0x2e__0x2e_0805_bit1 -x_0x2e__0x2e__0x2e_0805_bit2 -x_0x2e__0x2e__0x2e_0905_bit0 -x_0x2e__0x2e__0x2e_0905_bit1 -x_0x2e__0x2e__0x2e_0905_bit2 -x_0x2e__0x2e__0x2e_1005_bit0 -x_0x2e__0x2e__0x2e_1005_bit1 -x_0x2e__0x2e__0x2e_1005_bit2 -x_0x2e__0x2e__0x2e_1105_bit0 -x_0x2e__0x2e__0x2e_1105_bit1 -x_0x2e__0x2e__0x2e_1105_bit2 -x_0x2e__0x2e__0x2e_1205_bit0 -x_0x2e__0x2e__0x2e_1205_bit1 -x_0x2e__0x2e__0x2e_1205_bit2 -x_0x2e__0x2e__0x2e_0106_bit0 -x_0x2e__0x2e__0x2e_0106_bit1 -x_0x2e__0x2e__0x2e_0106_bit2 -x_0x2e__0x2e__0x2e_0106_bit3 -x_0x2e__0x2e__0x2e_0206_bit0 -x_0x2e__0x2e__0x2e_0206_bit1 -x_0x2e__0x2e__0x2e_0206_bit2 -x_0x2e__0x2e__0x2e_0206_bit3 -x_0x2e__0x2e__0x2e_0306_bit0 -x_0x2e__0x2e__0x2e_0306_bit1 -x_0x2e__0x2e__0x2e_0306_bit2 -x_0x2e__0x2e__0x2e_0306_bit3 -x_0x2e__0x2e__0x2e_0406_bit0 x_0x2e__0x2e__0x2e_0406_bit1 -x_0x2e__0x2e__0x2e_0406_bit2 -x_0x2e__0x2e__0x2e_0406_bit3 -x_0x2e__0x2e__0x2e_0506_bit0 -x_0x2e__0x2e__0x2e_0506_bit1 -x_0x2e__0x2e__0x2e_0506_bit2 -x_0x2e__0x2e__0x2e_0506_bit3 -x_0x2e__0x2e__0x2e_0606_bit0 -x_0x2e__0x2e__0x2e_0606_bit1 -x_0x2e__0x2e__0x2e_0606_bit2 -x_0x2e__0x2e__0x2e_0606_bit3 -x_0x2e__0x2e__0x2e_0706_bit0 -x_0x2e__0x2e__0x2e_0706_bit1 -x_0x2e__0x2e__0x2e_0706_bit2 -x_0x2e__0x2e__0x2e_0706_bit3 -x_0x2e__0x2e__0x2e_0806_bit0 -x_0x2e__0x2e__0x2e_0806_bit1 -x_0x2e__0x2e__0x2e_0806_bit2 -x_0x2e__0x2e__0x2e_0806_bit3 -x_0x2e__0x2e__0x2e_0906_bit0 -x_0x2e__0x2e__0x2e_0906_bit1 -x_0x2e__0x2e__0x2e_0906_bit2 -x_0x2e__0x2e__0x2e_0906_bit3 -x_0x2e__0x2e__0x2e_1006_bit0 -x_0x2e__0x2e__0x2e_1006_bit1 -x_0x2e__0x2e__0x2e_1006_bit2 -x_0x2e__0x2e__0x2e_1006_bit3 -x_0x2e__0x2e__0x2e_1106_bit0 -x_0x2e__0x2e__0x2e_1106_bit1 -x_0x2e__0x2e__0x2e_1106_bit2 -x_0x2e__0x2e__0x2e_1106_bit3 -x_0x2e__0x2e__0x2e_1206_bit0 -x_0x2e__0x2e__0x2e_1206_bit1 -x_0x2e__0x2e__0x2e_1206_bit2 -x_0x2e__0x2e__0x2e_1206_bit3 -x_0x2e__0x2e__0x2e_0507_bit0 -x_0x2e__0x2e__0x2e_0507_bit1 -x_0x2e__0x2e__0x2e_0507_bit2 -x_0x2e__0x2e__0x2e_0607_bit0 -x_0x2e__0x2e__0x2e_0607_bit1 -x_0x2e__0x2e__0x2e_0607_bit2 -x_0x2e__0x2e__0x2e_1107_bit0 -x_0x2e__0x2e__0x2e_1107_bit1 -x_0x2e__0x2e__0x2e_1107_bit2 -x_0x2e__0x2e__0x2e_1207_bit0 -x_0x2e__0x2e__0x2e_1207_bit1 -x_0x2e__0x2e__0x2e_1207_bit2 -x_0x2e__0x2e__0x2e_0108_bit0 -x_0x2e__0x2e__0x2e_0108_bit1 -x_0x2e__0x2e__0x2e_0108_bit2 -x_0x2e__0x2e__0x2e_0108_bit3 -x_0x2e__0x2e__0x2e_0208_bit0 -x_0x2e__0x2e__0x2e_0208_bit1 -x_0x2e__0x2e__0x2e_0208_bit2 -x_0x2e__0x2e__0x2e_0208_bit3 -x_0x2e__0x2e__0x2e_0308_bit0 -x_0x2e__0x2e__0x2e_0308_bit1 -x_0x2e__0x2e__0x2e_0308_bit2 -x_0x2e__0x2e__0x2e_0308_bit3 -x_0x2e__0x2e__0x2e_0408_bit0 -x_0x2e__0x2e__0x2e_0408_bit1 -x_0x2e__0x2e__0x2e_0408_bit2 -x_0x2e__0x2e__0x2e_0408_bit3 -x_0x2e__0x2e__0x2e_0708_bit0 -x_0x2e__0x2e__0x2e_0708_bit1 -x_0x2e__0x2e__0x2e_0708_bit2 -x_0x2e__0x2e__0x2e_0708_bit3 -x_0x2e__0x2e__0x2e_0808_bit0 -x_0x2e__0x2e__0x2e_0808_bit1 -x_0x2e__0x2e__0x2e_0808_bit2 -x_0x2e__0x2e__0x2e_0808_bit3 -x_0x2e__0x2e__0x2e_0908_bit0 -x_0x2e__0x2e__0x2e_0908_bit1 -x_0x2e__0x2e__0x2e_0908_bit2 x_0x2e__0x2e__0x2e_0908_bit3 -x_0x2e__0x2e__0x2e_1008_bit0 -x_0x2e__0x2e__0x2e_1008_bit1 -x_0x2e__0x2e__0x2e_1008_bit2 -x_0x2e__0x2e__0x2e_1008_bit3 -x_0x2e__0x2e__0x2e_0109_bit0 -x_0x2e__0x2e__0x2e_0109_bit1 -x_0x2e__0x2e__0x2e_0109_bit2 -x_0x2e__0x2e__0x2e_0209_bit0 -x_0x2e__0x2e__0x2e_0209_bit1 -x_0x2e__0x2e__0x2e_0209_bit2 -x_0x2e__0x2e__0x2e_0309_bit0 -x_0x2e__0x2e__0x2e_0309_bit1 -x_0x2e__0x2e__0x2e_0309_bit2 -x_0x2e__0x2e__0x2e_0409_bit0 -x_0x2e__0x2e__0x2e_0409_bit1 -x_0x2e__0x2e__0x2e_0409_bit2 -x_0x2e__0x2e__0x2e_0509_bit0 -x_0x2e__0x2e__0x2e_0509_bit1 -x_0x2e__0x2e__0x2e_0509_bit2 x_0x2e__0x2e__0x2e_0609_bit0 x_0x2e__0x2e__0x2e_0609_bit1 -x_0x2e__0x2e__0x2e_0609_bit2 -x_0x2e__0x2e__0x2e_0709_bit0 -x_0x2e__0x2e__0x2e_0709_bit1 -x_0x2e__0x2e__0x2e_0709_bit2 -x_0x2e__0x2e__0x2e_0809_bit0 -x_0x2e__0x2e__0x2e_0809_bit1 -x_0x2e__0x2e__0x2e_0809_bit2 -x_0x2e__0x2e__0x2e_0909_bit0 -x_0x2e__0x2e__0x2e_0909_bit1 -x_0x2e__0x2e__0x2e_0909_bit2 -x_0x2e__0x2e__0x2e_1009_bit0 -x_0x2e__0x2e__0x2e_1009_bit1 -x_0x2e__0x2e__0x2e_1009_bit2 -x_0x2e__0x2e__0x2e_1109_bit0 -x_0x2e__0x2e__0x2e_1109_bit1 -x_0x2e__0x2e__0x2e_1109_bit2 -x_0x2e__0x2e__0x2e_1209_bit0 x_0x2e__0x2e__0x2e_1209_bit1 -x_0x2e__0x2e__0x2e_1209_bit2 -x_0x2e__0x2e__0x2e_0110_bit0 -x_0x2e__0x2e__0x2e_0110_bit1 -x_0x2e__0x2e__0x2e_0110_bit2 -x_0x2e__0x2e__0x2e_0111_bit0 -x_0x2e__0x2e__0x2e_0111_bit1 x_0x2e__0x2e__0x2e_0111_bit2 -x_0x2e__0x2e__0x2e_0112_bit0 -x_0x2e__0x2e__0x2e_0112_bit1 -x_0x2e__0x2e__0x2e_0112_bit2 -x_0x2e__0x2e__0x2e_0112_bit3 -x_0x2e__0x2e__0x2e_0113_bit0 -x_0x2e__0x2e__0x2e_0113_bit1 -x_0x2e__0x2e__0x2e_0113_bit2 -x_0x2e__0x2e__0x2e_0114_bit0 -x_0x2e__0x2e__0x2e_0114_bit1 -x_0x2e__0x2e__0x2e_0114_bit2 x_0x2e__0x2e__0x2e_0115_bit0 -x_0x2e__0x2e__0x2e_0115_bit1 -x_0x2e__0x2e__0x2e_0116_bit0 -x_0x2e__0x2e__0x2e_0116_bit1 x_0x2e__0x2e__0x2e_0117_bit0 x_0x2e__0x2e__0x2e_0210_bit0 -x_0x2e__0x2e__0x2e_0210_bit1 -x_0x2e__0x2e__0x2e_0210_bit2 -x_0x2e__0x2e__0x2e_0211_bit0 -x_0x2e__0x2e__0x2e_0211_bit1 -x_0x2e__0x2e__0x2e_0211_bit2 -x_0x2e__0x2e__0x2e_0212_bit0 -x_0x2e__0x2e__0x2e_0212_bit1 -x_0x2e__0x2e__0x2e_0212_bit2 -x_0x2e__0x2e__0x2e_0212_bit3 x_0x2e__0x2e__0x2e_0213_bit0 -x_0x2e__0x2e__0x2e_0213_bit1 -x_0x2e__0x2e__0x2e_0213_bit2 x_0x2e__0x2e__0x2e_0214_bit0 -x_0x2e__0x2e__0x2e_0214_bit1 -x_0x2e__0x2e__0x2e_0214_bit2 x_0x2e__0x2e__0x2e_0215_bit0 -x_0x2e__0x2e__0x2e_0215_bit1 -x_0x2e__0x2e__0x2e_0216_bit0 -x_0x2e__0x2e__0x2e_0216_bit1 -x_0x2e__0x2e__0x2e_0217_bit0 -x_0x2e__0x2e__0x2e_0310_bit0 -x_0x2e__0x2e__0x2e_0310_bit1 -x_0x2e__0x2e__0x2e_0310_bit2 -x_0x2e__0x2e__0x2e_0311_bit0 -x_0x2e__0x2e__0x2e_0311_bit1 -x_0x2e__0x2e__0x2e_0311_bit2 -x_0x2e__0x2e__0x2e_0312_bit0 -x_0x2e__0x2e__0x2e_0312_bit1 -x_0x2e__0x2e__0x2e_0312_bit2 -x_0x2e__0x2e__0x2e_0312_bit3 x_0x2e__0x2e__0x2e_0313_bit0 -x_0x2e__0x2e__0x2e_0313_bit1 -x_0x2e__0x2e__0x2e_0313_bit2 -x_0x2e__0x2e__0x2e_0314_bit0 -x_0x2e__0x2e__0x2e_0314_bit1 -x_0x2e__0x2e__0x2e_0314_bit2 -x_0x2e__0x2e__0x2e_0315_bit0 -x_0x2e__0x2e__0x2e_0315_bit1 -x_0x2e__0x2e__0x2e_0316_bit0 -x_0x2e__0x2e__0x2e_0316_bit1 -x_0x2e__0x2e__0x2e_0317_bit0 -x_0x2e__0x2e__0x2e_0410_bit0 -x_0x2e__0x2e__0x2e_0410_bit1 -x_0x2e__0x2e__0x2e_0410_bit2 -x_0x2e__0x2e__0x2e_0411_bit0 -x_0x2e__0x2e__0x2e_0411_bit1 -x_0x2e__0x2e__0x2e_0411_bit2 -x_0x2e__0x2e__0x2e_0412_bit0 -x_0x2e__0x2e__0x2e_0412_bit1 -x_0x2e__0x2e__0x2e_0412_bit2 -x_0x2e__0x2e__0x2e_0412_bit3 -x_0x2e__0x2e__0x2e_0413_bit0 -x_0x2e__0x2e__0x2e_0413_bit1 -x_0x2e__0x2e__0x2e_0413_bit2 -x_0x2e__0x2e__0x2e_0414_bit0 -x_0x2e__0x2e__0x2e_0414_bit1 -x_0x2e__0x2e__0x2e_0414_bit2 -x_0x2e__0x2e__0x2e_0415_bit0 -x_0x2e__0x2e__0x2e_0415_bit1 x_0x2e__0x2e__0x2e_0416_bit0 -x_0x2e__0x2e__0x2e_0416_bit1 -x_0x2e__0x2e__0x2e_0417_bit0 x_0x2e__0x2e__0x2e_0510_bit0 -x_0x2e__0x2e__0x2e_0510_bit1 -x_0x2e__0x2e__0x2e_0510_bit2 -x_0x2e__0x2e__0x2e_0511_bit0 -x_0x2e__0x2e__0x2e_0511_bit1 -x_0x2e__0x2e__0x2e_0511_bit2 -x_0x2e__0x2e__0x2e_0512_bit0 -x_0x2e__0x2e__0x2e_0512_bit1 -x_0x2e__0x2e__0x2e_0512_bit2 -x_0x2e__0x2e__0x2e_0512_bit3 -x_0x2e__0x2e__0x2e_0513_bit0 -x_0x2e__0x2e__0x2e_0513_bit1 -x_0x2e__0x2e__0x2e_0513_bit2 x_0x2e__0x2e__0x2e_0514_bit0 -x_0x2e__0x2e__0x2e_0514_bit1 -x_0x2e__0x2e__0x2e_0514_bit2 -x_0x2e__0x2e__0x2e_0515_bit0 -x_0x2e__0x2e__0x2e_0515_bit1 -x_0x2e__0x2e__0x2e_0516_bit0 -x_0x2e__0x2e__0x2e_0516_bit1 -x_0x2e__0x2e__0x2e_0517_bit0 -x_0x2e__0x2e__0x2e_0610_bit0 -x_0x2e__0x2e__0x2e_0610_bit1 -x_0x2e__0x2e__0x2e_0610_bit2 -x_0x2e__0x2e__0x2e_0611_bit0 -x_0x2e__0x2e__0x2e_0611_bit1 -x_0x2e__0x2e__0x2e_0611_bit2 -x_0x2e__0x2e__0x2e_0612_bit0 -x_0x2e__0x2e__0x2e_0612_bit1 -x_0x2e__0x2e__0x2e_0612_bit2 -x_0x2e__0x2e__0x2e_0612_bit3 -x_0x2e__0x2e__0x2e_0613_bit0 -x_0x2e__0x2e__0x2e_0613_bit1 -x_0x2e__0x2e__0x2e_0613_bit2 -x_0x2e__0x2e__0x2e_0614_bit0 -x_0x2e__0x2e__0x2e_0614_bit1 -x_0x2e__0x2e__0x2e_0614_bit2 -x_0x2e__0x2e__0x2e_0615_bit0 -x_0x2e__0x2e__0x2e_0615_bit1 -x_0x2e__0x2e__0x2e_0616_bit0 -x_0x2e__0x2e__0x2e_0616_bit1 -x_0x2e__0x2e__0x2e_0617_bit0 x_0x2e__0x2e__0x2e_0710_bit0 -x_0x2e__0x2e__0x2e_0710_bit1 -x_0x2e__0x2e__0x2e_0710_bit2 -x_0x2e__0x2e__0x2e_0711_bit0 -x_0x2e__0x2e__0x2e_0711_bit1 -x_0x2e__0x2e__0x2e_0711_bit2 x_0x2e__0x2e__0x2e_0712_bit0 -x_0x2e__0x2e__0x2e_0712_bit1 -x_0x2e__0x2e__0x2e_0712_bit2 -x_0x2e__0x2e__0x2e_0712_bit3 x_0x2e__0x2e__0x2e_0713_bit0 -x_0x2e__0x2e__0x2e_0713_bit1 -x_0x2e__0x2e__0x2e_0713_bit2 x_0x2e__0x2e__0x2e_0714_bit0 -x_0x2e__0x2e__0x2e_0714_bit1 -x_0x2e__0x2e__0x2e_0714_bit2 -x_0x2e__0x2e__0x2e_0715_bit0 -x_0x2e__0x2e__0x2e_0715_bit1 -x_0x2e__0x2e__0x2e_0716_bit0 -x_0x2e__0x2e__0x2e_0716_bit1 -x_0x2e__0x2e__0x2e_0717_bit0 -x_0x2e__0x2e__0x2e_0810_bit0 x_0x2e__0x2e__0x2e_0810_bit1 -x_0x2e__0x2e__0x2e_0810_bit2 -x_0x2e__0x2e__0x2e_0811_bit0 -x_0x2e__0x2e__0x2e_0811_bit1 -x_0x2e__0x2e__0x2e_0811_bit2 -x_0x2e__0x2e__0x2e_0812_bit0 -x_0x2e__0x2e__0x2e_0812_bit1 -x_0x2e__0x2e__0x2e_0812_bit2 -x_0x2e__0x2e__0x2e_0812_bit3 x_0x2e__0x2e__0x2e_0813_bit0 -x_0x2e__0x2e__0x2e_0813_bit1 -x_0x2e__0x2e__0x2e_0813_bit2 -x_0x2e__0x2e__0x2e_0814_bit0 -x_0x2e__0x2e__0x2e_0814_bit1 -x_0x2e__0x2e__0x2e_0814_bit2 -x_0x2e__0x2e__0x2e_0815_bit0 -x_0x2e__0x2e__0x2e_0815_bit1 -x_0x2e__0x2e__0x2e_0816_bit0 -x_0x2e__0x2e__0x2e_0816_bit1 -x_0x2e__0x2e__0x2e_0817_bit0 -x_0x2e__0x2e__0x2e_0910_bit0 -x_0x2e__0x2e__0x2e_0910_bit1 -x_0x2e__0x2e__0x2e_0910_bit2 -x_0x2e__0x2e__0x2e_0911_bit0 -x_0x2e__0x2e__0x2e_0911_bit1 -x_0x2e__0x2e__0x2e_0911_bit2 -x_0x2e__0x2e__0x2e_0912_bit0 -x_0x2e__0x2e__0x2e_0912_bit1 -x_0x2e__0x2e__0x2e_0912_bit2 -x_0x2e__0x2e__0x2e_0912_bit3 -x_0x2e__0x2e__0x2e_0913_bit0 -x_0x2e__0x2e__0x2e_0913_bit1 -x_0x2e__0x2e__0x2e_0913_bit2 -x_0x2e__0x2e__0x2e_0914_bit0 -x_0x2e__0x2e__0x2e_0914_bit1 -x_0x2e__0x2e__0x2e_0914_bit2 -x_0x2e__0x2e__0x2e_0915_bit0 -x_0x2e__0x2e__0x2e_0915_bit1 -x_0x2e__0x2e__0x2e_0916_bit0 -x_0x2e__0x2e__0x2e_0916_bit1 -x_0x2e__0x2e__0x2e_0917_bit0 -x_0x2e__0x2e__0x2e_1010_bit0 -x_0x2e__0x2e__0x2e_1010_bit1 -x_0x2e__0x2e__0x2e_1010_bit2 -x_0x2e__0x2e__0x2e_1011_bit0 -x_0x2e__0x2e__0x2e_1011_bit1 -x_0x2e__0x2e__0x2e_1011_bit2 -x_0x2e__0x2e__0x2e_1012_bit0 -x_0x2e__0x2e__0x2e_1012_bit1 -x_0x2e__0x2e__0x2e_1012_bit2 x_0x2e__0x2e__0x2e_1012_bit3 -x_0x2e__0x2e__0x2e_1013_bit0 -x_0x2e__0x2e__0x2e_1013_bit1 -x_0x2e__0x2e__0x2e_1013_bit2 x_0x2e__0x2e__0x2e_1014_bit0 -x_0x2e__0x2e__0x2e_1014_bit1 -x_0x2e__0x2e__0x2e_1014_bit2 -x_0x2e__0x2e__0x2e_1015_bit0 -x_0x2e__0x2e__0x2e_1015_bit1 -x_0x2e__0x2e__0x2e_1016_bit0 -x_0x2e__0x2e__0x2e_1016_bit1 -x_0x2e__0x2e__0x2e_1017_bit0 x_0x2e__0x2e__0x2e_1110_bit0 -x_0x2e__0x2e__0x2e_1110_bit1 -x_0x2e__0x2e__0x2e_1110_bit2 -x_0x2e__0x2e__0x2e_1111_bit0 -x_0x2e__0x2e__0x2e_1111_bit1 -x_0x2e__0x2e__0x2e_1111_bit2 -x_0x2e__0x2e__0x2e_1112_bit0 -x_0x2e__0x2e__0x2e_1112_bit1 -x_0x2e__0x2e__0x2e_1112_bit2 -x_0x2e__0x2e__0x2e_1112_bit3 x_0x2e__0x2e__0x2e_1113_bit0 -x_0x2e__0x2e__0x2e_1113_bit1 -x_0x2e__0x2e__0x2e_1113_bit2 -x_0x2e__0x2e__0x2e_1114_bit0 -x_0x2e__0x2e__0x2e_1114_bit1 -x_0x2e__0x2e__0x2e_1114_bit2 -x_0x2e__0x2e__0x2e_1115_bit0 -x_0x2e__0x2e__0x2e_1115_bit1 x_0x2e__0x2e__0x2e_1116_bit0 -x_0x2e__0x2e__0x2e_1116_bit1 -x_0x2e__0x2e__0x2e_1117_bit0 -x_0x2e__0x2e__0x2e_1210_bit0 -x_0x2e__0x2e__0x2e_1210_bit1 -x_0x2e__0x2e__0x2e_1210_bit2 -x_0x2e__0x2e__0x2e_1211_bit0 -x_0x2e__0x2e__0x2e_1211_bit1 -x_0x2e__0x2e__0x2e_1211_bit2 -x_0x2e__0x2e__0x2e_1212_bit0 -x_0x2e__0x2e__0x2e_1212_bit1 -x_0x2e__0x2e__0x2e_1212_bit2 -x_0x2e__0x2e__0x2e_1212_bit3 -x_0x2e__0x2e__0x2e_1213_bi#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.94 0.90 2/55 12406
Raw data (stat): 12406 (runsolver) R 12405 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 422856129 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0008 s]
Raw data (loadavg): 0.87 0.94 0.90 2/55 12406
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 8908 0 0 0 975 24 0 0 25 0 1 0 422856129 38686720 8265 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9445 8265 603 41 0 9404 0
vsize: 37780
[startup+20.0018 s]
Raw data (loadavg): 0.89 0.94 0.90 2/55 12406
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 8990 0 0 0 1974 24 0 0 25 0 1 0 422856129 39079936 8347 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9541 8347 603 41 0 9500 0
vsize: 38164
[startup+30.0021 s]
Raw data (loadavg): 0.90 0.94 0.90 2/55 12406
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 9103 0 0 0 2974 25 0 0 25 0 1 0 422856129 39485440 8460 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9640 8460 603 41 0 9599 0
vsize: 38560
[startup+40.0029 s]
Raw data (loadavg): 0.92 0.94 0.90 2/55 12406
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 9192 0 0 0 3974 25 0 0 25 0 1 0 422856129 39878656 8549 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9736 8549 603 41 0 9695 0
vsize: 38944
[startup+50.0035 s]
Raw data (loadavg): 0.93 0.94 0.90 2/55 12406
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 9335 0 0 0 4973 26 0 0 25 0 1 0 422856129 40411136 8692 4294967295 134512640 134672761 3221224544 3221223696 134565076 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9866 8692 603 41 0 9825 0
vsize: 39464
[startup+60.0042 s]
Raw data (loadavg): 0.94 0.95 0.90 2/55 12406
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 10052 0 0 0 5971 28 0 0 25 0 1 0 422856129 42467328 9119 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10368 9119 603 41 0 10327 0
vsize: 41472
[startup+70.0049 s]
Raw data (loadavg): 0.95 0.95 0.91 2/55 12406
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 10074 0 0 0 6971 29 0 0 25 0 1 0 422856129 42688512 9141 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10422 9141 603 41 0 10381 0
vsize: 41688
[startup+80.005 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 12406
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 10076 0 0 0 7971 29 0 0 25 0 1 0 422856129 42688512 9143 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10422 9143 603 41 0 10381 0
vsize: 41688
[startup+90.0053 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 12406
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 10515 0 0 0 8970 30 0 0 25 0 1 0 422856129 42688512 9177 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10422 9177 603 41 0 10381 0
vsize: 41688
[startup+100.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 12406
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 10516 0 0 0 9970 30 0 0 25 0 1 0 422856129 42688512 9178 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10422 9178 603 41 0 10381 0
vsize: 41688
[startup+110.006 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 12406
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 10563 0 0 0 10970 30 0 0 25 0 1 0 422856129 42958848 9225 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10488 9225 603 41 0 10447 0
vsize: 41952
[startup+120.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 12406
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 10616 0 0 0 11970 30 0 0 25 0 1 0 422856129 43094016 9278 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10521 9278 603 41 0 10480 0
vsize: 42084
[startup+130.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 12406
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 10703 0 0 0 12969 31 0 0 25 0 1 0 422856129 43491328 9365 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10618 9365 603 41 0 10577 0
vsize: 42472
[startup+140.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 12406
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 10764 0 0 0 13969 31 0 0 25 0 1 0 422856129 43761664 9426 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10684 9426 603 41 0 10643 0
vsize: 42736
[startup+150.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 12406
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 10982 0 0 0 14969 32 0 0 25 0 1 0 422856129 44576768 9644 4294967295 134512640 134672761 3221224544 3221223744 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10883 9644 603 41 0 10842 0
vsize: 43532
[startup+160.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 12406
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 11057 0 0 0 15969 32 0 0 25 0 1 0 422856129 45109248 9719 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11013 9719 603 41 0 10972 0
vsize: 44052
[startup+170.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 12406
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 11124 0 0 0 16969 32 0 0 25 0 1 0 422856129 45375488 9786 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11078 9786 603 41 0 11037 0
vsize: 44312
[startup+180.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 12406
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 11189 0 0 0 17969 33 0 0 25 0 1 0 422856129 45641728 9851 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11143 9851 603 41 0 11102 0
vsize: 44572
[startup+190.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 12406
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 11348 0 0 0 18968 33 0 0 25 0 1 0 422856129 46178304 10010 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11274 10010 603 41 0 11233 0
vsize: 45096
[startup+200.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 12406
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 11490 0 0 0 19968 33 0 0 25 0 1 0 422856129 46829568 10152 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11433 10152 603 41 0 11392 0
vsize: 45732
[startup+210.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 12406
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 11645 0 0 0 20968 34 0 0 25 0 1 0 422856129 47370240 10307 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11565 10307 603 41 0 11524 0
vsize: 46260
[startup+220.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 12406
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 11741 0 0 0 21968 34 0 0 25 0 1 0 422856129 47775744 10403 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11664 10403 603 41 0 11623 0
vsize: 46656
[startup+230.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 12406
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 11884 0 0 0 22967 35 0 0 25 0 1 0 422856129 48447488 10546 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11828 10546 603 41 0 11787 0
vsize: 47312
[startup+240.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 12406
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 12025 0 0 0 23967 36 0 0 25 0 1 0 422856129 48984064 10687 4294967295 134512640 134672761 3221224544 3221223648 134559969 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11959 10687 603 41 0 11918 0
vsize: 47836
[startup+250.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 12406
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 12205 0 0 0 24966 36 0 0 25 0 1 0 422856129 49639424 10867 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12119 10867 603 41 0 12078 0
vsize: 48476
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12406
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 12371 0 0 0 25965 37 0 0 25 0 1 0 422856129 50307072 11033 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12282 11033 603 41 0 12241 0
vsize: 49128
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12406
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 17852 0 0 0 26952 51 0 0 25 0 1 0 422856129 74211328 15707 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18118 15707 603 41 0 18077 0
vsize: 72472
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12406
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 17936 0 0 0 27951 52 0 0 25 0 1 0 422856129 74616832 15791 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18217 15791 603 41 0 18176 0
vsize: 72868
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12406
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 18025 0 0 0 28951 52 0 0 25 0 1 0 422856129 75018240 15880 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18315 15880 603 41 0 18274 0
vsize: 73260
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12406
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 18129 0 0 0 29951 52 0 0 25 0 1 0 422856129 75419648 15984 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18413 15984 603 41 0 18372 0
vsize: 73652
[startup+310.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12406
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 18216 0 0 0 30951 52 0 0 25 0 1 0 422856129 75812864 16071 4294967295 134512640 134672761 3221224544 3221223712 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18509 16071 603 41 0 18468 0
vsize: 74036
[startup+320.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12406
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 18216 0 0 0 31952 52 0 0 25 0 1 0 422856129 75812864 16071 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18509 16071 603 41 0 18468 0
vsize: 74036
[startup+330.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12406
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 18258 0 0 0 32952 53 0 0 25 0 1 0 422856129 76075008 16113 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18573 16113 603 41 0 18532 0
vsize: 74292
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12406
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 18269 0 0 0 33952 53 0 0 25 0 1 0 422856129 76075008 16124 4294967295 134512640 134672761 3221224544 3221223760 134561985 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18573 16124 603 41 0 18532 0
vsize: 74292
[startup+350.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12406
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 18577 0 0 0 34952 53 0 0 25 0 1 0 422856129 77275136 16432 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18866 16432 603 41 0 18825 0
vsize: 75464
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12406
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 18663 0 0 0 35950 53 0 0 25 0 1 0 422856129 77684736 16518 4294967295 134512640 134672761 3221224544 3221223648 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18966 16518 603 41 0 18925 0
vsize: 75864
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12406
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 18741 0 0 0 36950 54 0 0 25 0 1 0 422856129 78213120 16596 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19095 16596 603 41 0 19054 0
vsize: 76380
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12406
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 18789 0 0 0 37950 54 0 0 25 0 1 0 422856129 78479360 16644 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19160 16644 603 41 0 19119 0
vsize: 76640
[startup+390.013 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 12459
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 18883 0 0 0 38949 54 0 0 25 0 1 0 422856129 78749696 16738 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19226 16738 603 41 0 19185 0
vsize: 76904
[startup+400.012 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 12459
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 18964 0 0 0 39949 55 0 0 25 0 1 0 422856129 79147008 16819 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19323 16819 603 41 0 19282 0
vsize: 77292
[startup+410.013 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 12459
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 19040 0 0 0 40949 55 0 0 25 0 1 0 422856129 79413248 16895 4294967295 134512640 134672761 3221224544 3221223680 134560654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19388 16895 603 41 0 19347 0
vsize: 77552
[startup+420.014 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 12459
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 19064 0 0 0 41949 55 0 0 25 0 1 0 422856129 79548416 16919 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19421 16919 603 41 0 19380 0
vsize: 77684
[startup+430.013 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 12459
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 19542 0 0 0 42948 57 0 0 25 0 1 0 422856129 81428480 17397 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19880 17397 603 41 0 19839 0
vsize: 79520
[startup+440.013 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 12459
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 19961 0 0 0 43947 58 0 0 25 0 1 0 422856129 83169280 17816 4294967295 134512640 134672761 3221224544 3221223712 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20305 17816 603 41 0 20264 0
vsize: 81220
[startup+450.014 s]
Raw data (loadavg): 1.10 1.00 0.92 2/55 12463
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 23005 0 0 0 44938 67 0 0 25 0 1 0 422856129 90570752 20280 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22112 20280 603 41 0 22071 0
vsize: 88448
[startup+460.014 s]
Raw data (loadavg): 1.08 1.00 0.92 2/55 12463
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 23005 0 0 0 45938 67 0 0 25 0 1 0 422856129 90570752 20280 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22112 20280 603 41 0 22071 0
vsize: 88448
[startup+470.014 s]
Raw data (loadavg): 1.07 1.00 0.92 2/55 12463
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 23005 0 0 0 46938 67 0 0 25 0 1 0 422856129 90570752 20280 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22112 20280 603 41 0 22071 0
vsize: 88448
[startup+480.014 s]
Raw data (loadavg): 1.06 1.00 0.92 2/55 12463
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 23006 0 0 0 47938 67 0 0 25 0 1 0 422856129 90570752 20281 4294967295 134512640 134672761 3221224544 3221223680 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22112 20281 603 41 0 22071 0
vsize: 88448
[startup+490.014 s]
Raw data (loadavg): 1.05 1.00 0.92 2/55 12463
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 23010 0 0 0 48939 67 0 0 25 0 1 0 422856129 90570752 20285 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22112 20285 603 41 0 22071 0
vsize: 88448
[startup+500.014 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 12463
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 23036 0 0 0 49939 67 0 0 25 0 1 0 422856129 90705920 20311 4294967295 134512640 134672761 3221224544 3221223696 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22145 20311 603 41 0 22104 0
vsize: 88580
[startup+510.015 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 12463
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 23125 0 0 0 50939 67 0 0 25 0 1 0 422856129 91103232 20400 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22242 20400 603 41 0 22201 0
vsize: 88968
[startup+520.015 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 12463
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 23240 0 0 0 51939 67 0 0 25 0 1 0 422856129 91500544 20515 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22339 20515 603 41 0 22298 0
vsize: 89356
[startup+530.015 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 12463
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 23272 0 0 0 52939 68 0 0 25 0 1 0 422856129 91631616 20547 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22371 20547 603 41 0 22330 0
vsize: 89484
[startup+540.015 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 12463
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 23410 0 0 0 53938 68 0 0 25 0 1 0 422856129 92295168 20685 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22533 20685 603 41 0 22492 0
vsize: 90132
[startup+550.014 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 12463
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 23513 0 0 0 54938 69 0 0 25 0 1 0 422856129 92696576 20788 4294967295 134512640 134672761 3221224544 3221223716 134556641 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22631 20788 603 41 0 22590 0
vsize: 90524
[startup+560.015 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 12463
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 23599 0 0 0 55938 69 0 0 25 0 1 0 422856129 92962816 20874 4294967295 134512640 134672761 3221224544 3221223708 134561028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22696 20874 603 41 0 22655 0
vsize: 90784
[startup+570.015 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 12463
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 23638 0 0 0 56938 69 0 0 25 0 1 0 422856129 93233152 20913 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22762 20913 603 41 0 22721 0
vsize: 91048
[startup+580.015 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 12463
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 23659 0 0 0 57938 69 0 0 25 0 1 0 422856129 93233152 20934 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22762 20934 603 41 0 22721 0
vsize: 91048
[startup+590.015 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 12463
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 23682 0 0 0 58939 69 0 0 25 0 1 0 422856129 93364224 20957 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22794 20957 603 41 0 22753 0
vsize: 91176
[startup+600.015 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 12463
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 23704 0 0 0 59938 69 0 0 25 0 1 0 422856129 93364224 20979 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22794 20979 603 41 0 22753 0
vsize: 91176
[startup+610.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12463
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 23735 0 0 0 60939 69 0 0 25 0 1 0 422856129 93499392 21010 4294967295 134512640 134672761 3221224544 3221223728 134558654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22827 21010 603 41 0 22786 0
vsize: 91308
[startup+620.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12463
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 23835 0 0 0 61938 70 0 0 25 0 1 0 422856129 93904896 21110 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22926 21110 603 41 0 22885 0
vsize: 91704
[startup+630.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12463
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 23881 0 0 0 62938 70 0 0 25 0 1 0 422856129 94175232 21156 4294967295 134512640 134672761 3221224544 3221223680 134560604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22992 21156 603 41 0 22951 0
vsize: 91968
[startup+640.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12463
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 23902 0 0 0 63938 70 0 0 25 0 1 0 422856129 94175232 21177 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22992 21177 603 41 0 22951 0
vsize: 91968
[startup+650.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12463
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 24149 0 0 0 64938 70 0 0 25 0 1 0 422856129 95244288 21424 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23253 21424 603 41 0 23212 0
vsize: 93012
[startup+660.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12463
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 24341 0 0 0 65937 71 0 0 25 0 1 0 422856129 96030720 21616 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23445 21616 603 41 0 23404 0
vsize: 93780
[startup+670.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12463
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 24462 0 0 0 66937 71 0 0 25 0 1 0 422856129 96550912 21737 4294967295 134512640 134672761 3221224544 3221223648 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23572 21737 603 41 0 23531 0
vsize: 94288
[startup+680.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12463
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 26926 0 0 0 67931 77 0 0 25 0 1 0 422856129 102109184 23773 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24929 23773 603 41 0 24888 0
vsize: 99716
[startup+690.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12463
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 26981 0 0 0 68931 78 0 0 25 0 1 0 422856129 102367232 23828 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24992 23828 603 41 0 24951 0
vsize: 99968
[startup+700.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 27128 0 0 0 69931 78 0 0 25 0 1 0 422856129 102907904 23975 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25124 23975 603 41 0 25083 0
vsize: 100496
[startup+710.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 27191 0 0 0 70931 78 0 0 25 0 1 0 422856129 103178240 24038 4294967295 134512640 134672761 3221224544 3221223700 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25190 24038 603 41 0 25149 0
vsize: 100760
[startup+720.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 27240 0 0 0 71931 78 0 0 25 0 1 0 422856129 103313408 24087 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25223 24087 603 41 0 25182 0
vsize: 100892
[startup+730.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 27407 0 0 0 72931 79 0 0 25 0 1 0 422856129 103976960 24254 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25385 24254 603 41 0 25344 0
vsize: 101540
[startup+740.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 27565 0 0 0 73930 79 0 0 25 0 1 0 422856129 104648704 24412 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25549 24412 603 41 0 25508 0
vsize: 102196
[startup+750.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 27693 0 0 0 74930 80 0 0 25 0 1 0 422856129 105177088 24540 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25678 24540 603 41 0 25637 0
vsize: 102712
[startup+760.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 27731 0 0 0 75930 80 0 0 25 0 1 0 422856129 105312256 24578 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25711 24578 603 41 0 25670 0
vsize: 102844
[startup+770.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 27834 0 0 0 76930 80 0 0 25 0 1 0 422856129 105709568 24681 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25808 24681 603 41 0 25767 0
vsize: 103232
[startup+780.011 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 27915 0 0 0 77930 80 0 0 25 0 1 0 422856129 106115072 24762 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25907 24762 603 41 0 25866 0
vsize: 103628
[startup+790.011 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 28024 0 0 0 78930 80 0 0 25 0 1 0 422856129 106516480 24871 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26005 24871 603 41 0 25964 0
vsize: 104020
[startup+800.011 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 28187 0 0 0 79930 81 0 0 25 0 1 0 422856129 107196416 25034 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26171 25034 603 41 0 26130 0
vsize: 104684
[startup+810.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 28353 0 0 0 80929 82 0 0 25 0 1 0 422856129 107868160 25200 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26335 25200 603 41 0 26294 0
vsize: 105340
[startup+820.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 28447 0 0 0 81929 82 0 0 25 0 1 0 422856129 108265472 25294 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26432 25294 603 41 0 26391 0
vsize: 105728
[startup+830.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 28535 0 0 0 82929 82 0 0 25 0 1 0 422856129 108670976 25382 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26531 25382 603 41 0 26490 0
vsize: 106124
[startup+840.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 28591 0 0 0 83929 83 0 0 25 0 1 0 422856129 108802048 25438 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26563 25438 603 41 0 26522 0
vsize: 106252
[startup+850.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 28619 0 0 0 84929 83 0 0 25 0 1 0 422856129 108937216 25466 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26596 25466 603 41 0 26555 0
vsize: 106384
[startup+860.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 28655 0 0 0 85929 83 0 0 25 0 1 0 422856129 109072384 25502 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26629 25502 603 41 0 26588 0
vsize: 106516
[startup+870.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 28683 0 0 0 86929 83 0 0 25 0 1 0 422856129 109203456 25530 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26661 25530 603 41 0 26620 0
vsize: 106644
[startup+880.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 28713 0 0 0 87929 83 0 0 25 0 1 0 422856129 109338624 25560 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26694 25560 603 41 0 26653 0
vsize: 106776
[startup+890.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 28740 0 0 0 88929 83 0 0 25 0 1 0 422856129 109469696 25587 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26726 25587 603 41 0 26685 0
vsize: 106904
[startup+900.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 28884 0 0 0 89929 84 0 0 25 0 1 0 422856129 110002176 25731 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26856 25731 603 41 0 26815 0
vsize: 107424
[startup+910.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 28929 0 0 0 90929 84 0 0 25 0 1 0 422856129 110260224 25776 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26919 25776 603 41 0 26878 0
vsize: 107676
[startup+920.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 28945 0 0 0 91929 84 0 0 25 0 1 0 422856129 110260224 25792 4294967295 134512640 134672761 3221224544 3221223680 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26919 25792 603 41 0 26878 0
vsize: 107676
[startup+930.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 29046 0 0 0 92929 84 0 0 25 0 1 0 422856129 110669824 25893 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27019 25893 603 41 0 26978 0
vsize: 108076
[startup+940.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 29095 0 0 0 93929 84 0 0 25 0 1 0 422856129 110940160 25942 4294967295 134512640 134672761 3221224544 3221223680 134560619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27085 25942 603 41 0 27044 0
vsize: 108340
[startup+950.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 29177 0 0 0 94929 84 0 0 25 0 1 0 422856129 111210496 26024 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27151 26024 603 41 0 27110 0
vsize: 108604
[startup+960.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 29180 0 0 0 95929 84 0 0 25 0 1 0 422856129 111210496 26027 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27151 26027 603 41 0 27110 0
vsize: 108604
[startup+970.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 29197 0 0 0 96929 84 0 0 25 0 1 0 422856129 111325184 26044 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27179 26044 603 41 0 27138 0
vsize: 108716
[startup+980.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 29220 0 0 0 97929 85 0 0 25 0 1 0 422856129 111456256 26067 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27211 26067 603 41 0 27170 0
vsize: 108844
[startup+990.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 29289 0 0 0 98929 85 0 0 25 0 1 0 422856129 111726592 26136 4294967295 134512640 134672761 3221224544 3221223648 134559778 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27277 26136 603 41 0 27236 0
vsize: 109108
[startup+1000.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 29862 0 0 0 99928 86 0 0 25 0 1 0 422856129 112590848 26419 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27488 26419 603 41 0 27447 0
vsize: 109952
[startup+1010.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 29863 0 0 0 100928 86 0 0 25 0 1 0 422856129 112590848 26420 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27488 26420 603 41 0 27447 0
vsize: 109952
[startup+1020.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 29864 0 0 0 101928 86 0 0 25 0 1 0 422856129 112590848 26421 4294967295 134512640 134672761 3221224544 3221223696 134565127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27488 26421 603 41 0 27447 0
vsize: 109952
[startup+1030.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 29916 0 0 0 102928 86 0 0 25 0 1 0 422856129 112852992 26473 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27552 26473 603 41 0 27511 0
vsize: 110208
[startup+1040.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 29940 0 0 0 103928 86 0 0 25 0 1 0 422856129 113512448 26497 4294967295 134512640 134672761 3221224544 3221223700 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27713 26497 603 41 0 27672 0
vsize: 110852
[startup+1050.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 29969 0 0 0 104928 86 0 0 25 0 1 0 422856129 113647616 26526 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27746 26526 603 41 0 27705 0
vsize: 110984
[startup+1060.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 30059 0 0 0 105928 86 0 0 25 0 1 0 422856129 113922048 26616 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27813 26616 603 41 0 27772 0
vsize: 111252
[startup+1070.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 30137 0 0 0 106928 87 0 0 25 0 1 0 422856129 114323456 26694 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27911 26694 603 41 0 27870 0
vsize: 111644
[startup+1080.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 30153 0 0 0 107928 87 0 0 25 0 1 0 422856129 114323456 26710 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27911 26710 603 41 0 27870 0
vsize: 111644
[startup+1090.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 30184 0 0 0 108928 87 0 0 25 0 1 0 422856129 114450432 26741 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27942 26741 603 41 0 27901 0
vsize: 111768
[startup+1100.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 30376 0 0 0 109928 87 0 0 25 0 1 0 422856129 115249152 26933 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28137 26933 603 41 0 28096 0
vsize: 112548
[startup+1110.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 30537 0 0 0 110928 88 0 0 25 0 1 0 422856129 115920896 27094 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28301 27094 603 41 0 28260 0
vsize: 113204
[startup+1120.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 30717 0 0 0 111927 89 0 0 25 0 1 0 422856129 116604928 27274 4294967295 134512640 134672761 3221224544 3221223648 134560344 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28468 27274 603 41 0 28427 0
vsize: 113872
[startup+1130.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 30834 0 0 0 112927 89 0 0 25 0 1 0 422856129 117133312 27391 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28597 27391 603 41 0 28556 0
vsize: 114388
[startup+1140.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 30960 0 0 0 113927 89 0 0 25 0 1 0 422856129 117551104 27517 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28699 27517 603 41 0 28658 0
vsize: 114796
[startup+1150.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 31080 0 0 0 114927 89 0 0 25 0 1 0 422856129 118083584 27637 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28829 27637 603 41 0 28788 0
vsize: 115316
[startup+1160.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 31155 0 0 0 115927 90 0 0 25 0 1 0 422856129 118353920 27712 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28895 27712 603 41 0 28854 0
vsize: 115580
[startup+1170.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 35587 0 0 0 116917 100 0 0 25 0 1 0 422856129 151031808 31698 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36873 31698 603 41 0 36832 0
vsize: 147492
[startup+1180.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 35648 0 0 0 117917 100 0 0 25 0 1 0 422856129 151166976 31759 4294967295 134512640 134672761 3221224544 3221223648 134559979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36906 31759 603 41 0 36865 0
vsize: 147624
[startup+1190.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 35701 0 0 0 118917 100 0 0 25 0 1 0 422856129 151433216 31812 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36971 31812 603 41 0 36930 0
vsize: 147884
[startup+1200.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12465
Raw data (stat): 12406 (minisat+) R 12405 30927 30926 0 -1 0 35734 0 0 0 119917 100 0 0 25 0 1 0 422856129 151568384 31845 4294967295 134512640 134672761 3221224544 3221223680 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37004 31845 603 41 0 36963 0
vsize: 148016
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 1.00 0.92 1/55 12465
Raw data (stat): 12406 (minisat+) Z 12405 30927 30926 0 -1 12 35737 0 0 0 119917 106 0 0 25 0 1 0 422856129 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.07
CPU time (s): 1200.25
CPU user time (s): 1199.18
CPU system time (s): 1.06584
CPU usage (%): 100.014
Max. virtual memory (Kb): 148016
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####