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-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-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	1177.34
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 21329

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc23 THE 2005-04-21 23:25:25 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13455 boxname=wulflinc23 idbench=1035 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f1382105ee9fb79777762a53cf6a73c1  /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-gt2.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-gt2.opb /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-gt2.opb
IDLAUNCH: 13455
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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.037
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:        683936 kB
Buffers:         20064 kB
Cached:         306808 kB
SwapCached:        548 kB
Active:          63600 kB
Inactive:       265348 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        683684 kB
SwapTotal:     2097136 kB
SwapFree:      2095732 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5104 kB
Slab:            16112 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 23:45:27 (client local time) WITH STATUS 10 IN 1200.37 SECONDS
stats: 13455 7 1200.37 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 
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.50 0.84 0.88 2/54 16613
Raw data (stat): 16613 (runsolver) R 16612 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 549022963 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.58 0.84 0.88 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 8908 0 0 0 979 19 0 0 25 0 1 0 549022963 38686720 8265 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9445 8265 603 41 0 9404 0
vsize: 37780
[startup+20.0012 s]
Raw data (loadavg): 0.64 0.85 0.88 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 8990 0 0 0 1978 20 0 0 25 0 1 0 549022963 39079936 8347 4294967295 134512640 134672761 3221224544 3221223680 134560575 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9541 8347 603 41 0 9500 0
vsize: 38164
[startup+30.0025 s]
Raw data (loadavg): 0.70 0.85 0.88 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 9104 0 0 0 2978 21 0 0 25 0 1 0 549022963 39485440 8461 4294967295 134512640 134672761 3221224544 3221223744 134557814 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9640 8461 603 41 0 9599 0
vsize: 38560
[startup+40.0029 s]
Raw data (loadavg): 0.74 0.86 0.88 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 9192 0 0 0 3977 21 0 0 25 0 1 0 549022963 39878656 8549 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9736 8549 603 41 0 9695 0
vsize: 38944
[startup+50.003 s]
Raw data (loadavg): 0.78 0.86 0.88 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 9341 0 0 0 4977 22 0 0 25 0 1 0 549022963 40411136 8698 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9866 8698 603 41 0 9825 0
vsize: 39464
[startup+60.0028 s]
Raw data (loadavg): 0.81 0.86 0.88 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 10052 0 0 0 5975 24 0 0 25 0 1 0 549022963 42467328 9119 4294967295 134512640 134672761 3221224544 3221223648 134559841 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.0035 s]
Raw data (loadavg): 0.84 0.87 0.88 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 10074 0 0 0 6975 24 0 0 25 0 1 0 549022963 42688512 9141 4294967295 134512640 134672761 3221224544 3221223712 134561229 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.0038 s]
Raw data (loadavg): 0.87 0.87 0.89 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 10076 0 0 0 7975 24 0 0 25 0 1 0 549022963 42688512 9143 4294967295 134512640 134672761 3221224544 3221223680 134560729 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.004 s]
Raw data (loadavg): 0.89 0.88 0.89 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 10514 0 0 0 8974 25 0 0 25 0 1 0 549022963 42688512 9176 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10422 9176 603 41 0 10381 0
vsize: 41688
[startup+100.004 s]
Raw data (loadavg): 0.90 0.88 0.89 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 10516 0 0 0 9974 25 0 0 25 0 1 0 549022963 42688512 9178 4294967295 134512640 134672761 3221224544 3221223696 134565086 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.005 s]
Raw data (loadavg): 0.92 0.88 0.89 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 10561 0 0 0 10974 25 0 0 25 0 1 0 549022963 42958848 9223 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10488 9223 603 41 0 10447 0
vsize: 41952
[startup+120.006 s]
Raw data (loadavg): 0.93 0.89 0.89 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 10612 0 0 0 11975 25 0 0 25 0 1 0 549022963 43094016 9274 4294967295 134512640 134672761 3221224544 3221223648 134560148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10521 9274 603 41 0 10480 0
vsize: 42084
[startup+130.005 s]
Raw data (loadavg): 0.94 0.89 0.89 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 10701 0 0 0 12975 25 0 0 25 0 1 0 549022963 43491328 9363 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10618 9363 603 41 0 10577 0
vsize: 42472
[startup+140.005 s]
Raw data (loadavg): 0.95 0.89 0.89 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 10745 0 0 0 13974 25 0 0 25 0 1 0 549022963 43626496 9407 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10651 9407 603 41 0 10610 0
vsize: 42604
[startup+150.005 s]
Raw data (loadavg): 0.96 0.89 0.89 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 10968 0 0 0 14974 26 0 0 25 0 1 0 549022963 44576768 9630 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10883 9630 603 41 0 10842 0
vsize: 43532
[startup+160.004 s]
Raw data (loadavg): 0.96 0.90 0.89 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 11057 0 0 0 15974 26 0 0 25 0 1 0 549022963 45109248 9719 4294967295 134512640 134672761 3221224544 3221223680 134560608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11013 9719 603 41 0 10972 0
vsize: 44052
[startup+170.005 s]
Raw data (loadavg): 0.97 0.90 0.89 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 11084 0 0 0 16974 26 0 0 25 0 1 0 549022963 45109248 9746 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11013 9746 603 41 0 10972 0
vsize: 44052
[startup+180.005 s]
Raw data (loadavg): 0.97 0.90 0.90 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 11181 0 0 0 17974 27 0 0 25 0 1 0 549022963 45506560 9843 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11110 9843 603 41 0 11069 0
vsize: 44440
[startup+190.004 s]
Raw data (loadavg): 0.98 0.91 0.90 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 11323 0 0 0 18973 27 0 0 25 0 1 0 549022963 46178304 9985 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11274 9985 603 41 0 11233 0
vsize: 45096
[startup+200.005 s]
Raw data (loadavg): 0.98 0.91 0.90 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 11487 0 0 0 19973 28 0 0 25 0 1 0 549022963 46829568 10149 4294967295 134512640 134672761 3221224544 3221223744 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11433 10149 603 41 0 11392 0
vsize: 45732
[startup+210.005 s]
Raw data (loadavg): 0.98 0.91 0.90 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 11629 0 0 0 20973 28 0 0 25 0 1 0 549022963 47370240 10291 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11565 10291 603 41 0 11524 0
vsize: 46260
[startup+220.005 s]
Raw data (loadavg): 0.98 0.91 0.90 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 11685 0 0 0 21973 29 0 0 25 0 1 0 549022963 47505408 10347 4294967295 134512640 134672761 3221224544 3221223692 134565030 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11598 10347 603 41 0 11557 0
vsize: 46392
[startup+230.005 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 11853 0 0 0 22972 29 0 0 25 0 1 0 549022963 48312320 10515 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11795 10515 603 41 0 11754 0
vsize: 47180
[startup+240.005 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 11985 0 0 0 23972 29 0 0 25 0 1 0 549022963 48848896 10647 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11926 10647 603 41 0 11885 0
vsize: 47704
[startup+250.006 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 12189 0 0 0 24972 30 0 0 25 0 1 0 549022963 49639424 10851 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12119 10851 603 41 0 12078 0
vsize: 48476
[startup+260.006 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 12326 0 0 0 25971 31 0 0 25 0 1 0 549022963 50171904 10988 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12249 10988 603 41 0 12208 0
vsize: 48996
[startup+270.008 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 16240 0 0 0 26961 41 0 0 25 0 1 0 549022963 69226496 14095 4294967295 134512640 134672761 3221224544 3221192080 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16901 14096 603 41 0 16860 0
vsize: 67604
[startup+280.008 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 17920 0 0 0 27958 44 0 0 25 0 1 0 549022963 74481664 15775 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18184 15775 603 41 0 18143 0
vsize: 72736
[startup+290.007 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 18004 0 0 0 28958 44 0 0 25 0 1 0 549022963 74883072 15859 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18282 15859 603 41 0 18241 0
vsize: 73128
[startup+300.008 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 18114 0 0 0 29959 44 0 0 25 0 1 0 549022963 75284480 15969 4294967295 134512640 134672761 3221224544 3221223648 134560361 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18380 15969 603 41 0 18339 0
vsize: 73520
[startup+310.008 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 18166 0 0 0 30958 45 0 0 25 0 1 0 549022963 75550720 16021 4294967295 134512640 134672761 3221224544 3221223648 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18445 16021 603 41 0 18404 0
vsize: 73780
[startup+320.008 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 18216 0 0 0 31959 45 0 0 25 0 1 0 549022963 75812864 16071 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18509 16071 603 41 0 18468 0
vsize: 74036
[startup+330.011 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 18237 0 0 0 32959 45 0 0 25 0 1 0 549022963 75943936 16092 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18541 16092 603 41 0 18500 0
vsize: 74164
[startup+340.013 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 18266 0 0 0 33959 45 0 0 25 0 1 0 549022963 76075008 16121 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18573 16121 603 41 0 18532 0
vsize: 74292
[startup+350.013 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 18470 0 0 0 34958 46 0 0 25 0 1 0 549022963 76869632 16325 4294967295 134512640 134672761 3221224544 3221223648 134559916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18767 16325 603 41 0 18726 0
vsize: 75068
[startup+360.02 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 18636 0 0 0 35959 46 0 0 25 0 1 0 549022963 77545472 16491 4294967295 134512640 134672761 3221224544 3221223680 134565064 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18932 16491 603 41 0 18891 0
vsize: 75728
[startup+370.122 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 18686 0 0 0 36969 46 0 0 25 0 1 0 549022963 77815808 16541 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18998 16541 603 41 0 18957 0
vsize: 75992
[startup+380.122 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 18746 0 0 0 37969 47 0 0 25 0 1 0 549022963 78213120 16601 4294967295 134512640 134672761 3221224544 3221223712 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19095 16601 603 41 0 19054 0
vsize: 76380
[startup+390.122 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 18821 0 0 0 38969 47 0 0 25 0 1 0 549022963 78614528 16676 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19193 16676 603 41 0 19152 0
vsize: 76772
[startup+400.122 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 18931 0 0 0 39969 47 0 0 25 0 1 0 549022963 79015936 16786 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19291 16786 603 41 0 19250 0
vsize: 77164
[startup+410.122 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 19005 0 0 0 40969 48 0 0 25 0 1 0 549022963 79282176 16860 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19356 16860 603 41 0 19315 0
vsize: 77424
[startup+420.123 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 19045 0 0 0 41969 48 0 0 25 0 1 0 549022963 79413248 16900 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19388 16900 603 41 0 19347 0
vsize: 77552
[startup+430.122 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 19189 0 0 0 42968 48 0 0 25 0 1 0 549022963 80080896 17044 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19551 17044 603 41 0 19510 0
vsize: 78204
[startup+440.122 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 19699 0 0 0 43966 51 0 0 25 0 1 0 549022963 82100224 17554 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20044 17554 603 41 0 20003 0
vsize: 80176
[startup+450.122 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 22376 0 0 0 44961 56 0 0 25 0 1 0 549022963 88915968 19941 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21708 19941 603 41 0 21667 0
vsize: 86832
[startup+460.122 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 23005 0 0 0 45960 57 0 0 25 0 1 0 549022963 90570752 20280 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22112 20280 603 41 0 22071 0
vsize: 88448
[startup+470.123 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 23005 0 0 0 46960 58 0 0 25 0 1 0 549022963 90570752 20280 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22112 20280 603 41 0 22071 0
vsize: 88448
[startup+480.124 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 23005 0 0 0 47960 58 0 0 25 0 1 0 549022963 90570752 20280 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22112 20280 603 41 0 22071 0
vsize: 88448
[startup+490.123 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 23006 0 0 0 48960 58 0 0 25 0 1 0 549022963 90570752 20281 4294967295 134512640 134672761 3221224544 3221223712 134561027 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22112 20281 603 41 0 22071 0
vsize: 88448
[startup+500.123 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 23012 0 0 0 49960 58 0 0 25 0 1 0 549022963 90570752 20287 4294967295 134512640 134672761 3221224544 3221223728 134556589 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22112 20287 603 41 0 22071 0
vsize: 88448
[startup+510.123 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 23082 0 0 0 50960 58 0 0 25 0 1 0 549022963 90972160 20357 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22210 20357 603 41 0 22169 0
vsize: 88840
[startup+520.123 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 23159 0 0 0 51960 59 0 0 25 0 1 0 549022963 91242496 20434 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22276 20434 603 41 0 22235 0
vsize: 89104
[startup+530.123 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 23244 0 0 0 52959 59 0 0 25 0 1 0 549022963 91631616 20519 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22371 20519 603 41 0 22330 0
vsize: 89484
[startup+540.123 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 23278 0 0 0 53959 59 0 0 25 0 1 0 549022963 91762688 20553 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22403 20553 603 41 0 22362 0
vsize: 89612
[startup+550.123 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 23427 0 0 0 54959 60 0 0 25 0 1 0 549022963 92295168 20702 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22533 20702 603 41 0 22492 0
vsize: 90132
[startup+560.123 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 23515 0 0 0 55958 61 0 0 25 0 1 0 549022963 92696576 20790 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22631 20790 603 41 0 22590 0
vsize: 90524
[startup+570.124 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 23601 0 0 0 56958 61 0 0 25 0 1 0 549022963 92962816 20876 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22696 20876 603 41 0 22655 0
vsize: 90784
[startup+580.124 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 23639 0 0 0 57958 61 0 0 25 0 1 0 549022963 93233152 20914 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22762 20914 603 41 0 22721 0
vsize: 91048
[startup+590.124 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 23665 0 0 0 58958 61 0 0 25 0 1 0 549022963 93233152 20940 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22762 20940 603 41 0 22721 0
vsize: 91048
[startup+600.124 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 23683 0 0 0 59958 61 0 0 25 0 1 0 549022963 93364224 20958 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22794 20958 603 41 0 22753 0
vsize: 91176
[startup+610.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 23704 0 0 0 60958 62 0 0 25 0 1 0 549022963 93364224 20979 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22794 20979 603 41 0 22753 0
vsize: 91176
[startup+620.124 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 23735 0 0 0 61958 62 0 0 25 0 1 0 549022963 93499392 21010 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22827 21010 603 41 0 22786 0
vsize: 91308
[startup+630.124 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 23833 0 0 0 62958 62 0 0 25 0 1 0 549022963 93904896 21108 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22926 21108 603 41 0 22885 0
vsize: 91704
[startup+640.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 23875 0 0 0 63958 62 0 0 25 0 1 0 549022963 94175232 21150 4294967295 134512640 134672761 3221224544 3221223712 134561018 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22992 21150 603 41 0 22951 0
vsize: 91968
[startup+650.124 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 23902 0 0 0 64959 62 0 0 25 0 1 0 549022963 94175232 21177 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22992 21177 603 41 0 22951 0
vsize: 91968
[startup+660.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 24093 0 0 0 65958 63 0 0 25 0 1 0 549022963 94973952 21368 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23187 21368 603 41 0 23146 0
vsize: 92748
[startup+670.124 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 24321 0 0 0 66957 64 0 0 25 0 1 0 549022963 95895552 21596 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23412 21596 603 41 0 23371 0
vsize: 93648
[startup+680.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 24437 0 0 0 67957 65 0 0 25 0 1 0 549022963 96419840 21712 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23540 21712 603 41 0 23499 0
vsize: 94160
[startup+690.124 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 26896 0 0 0 68950 72 0 0 25 0 1 0 549022963 102109184 23743 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24929 23743 603 41 0 24888 0
vsize: 99716
[startup+700.124 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 26960 0 0 0 69950 72 0 0 25 0 1 0 549022963 102244352 23807 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24962 23807 603 41 0 24921 0
vsize: 99848
[startup+710.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 27124 0 0 0 70949 72 0 0 25 0 1 0 549022963 102907904 23971 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25124 23971 603 41 0 25083 0
vsize: 100496
[startup+720.124 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 27186 0 0 0 71949 73 0 0 25 0 1 0 549022963 103178240 24033 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25190 24033 603 41 0 25149 0
vsize: 100760
[startup+730.124 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 27223 0 0 0 72949 73 0 0 25 0 1 0 549022963 103313408 24070 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25223 24070 603 41 0 25182 0
vsize: 100892
[startup+740.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 27385 0 0 0 73948 73 0 0 25 0 1 0 549022963 103976960 24232 4294967295 134512640 134672761 3221224544 3221223808 134562552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25385 24232 603 41 0 25344 0
vsize: 101540
[startup+750.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 27504 0 0 0 74948 73 0 0 25 0 1 0 549022963 104378368 24351 4294967295 134512640 134672761 3221224544 3221223648 134560313 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25483 24351 603 41 0 25442 0
vsize: 101932
[startup+760.124 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 27636 0 0 0 75948 73 0 0 25 0 1 0 549022963 104914944 24483 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25614 24483 603 41 0 25573 0
vsize: 102456
[startup+770.124 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 27726 0 0 0 76948 74 0 0 25 0 1 0 549022963 105312256 24573 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25711 24573 603 41 0 25670 0
vsize: 102844
[startup+780.124 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 27742 0 0 0 77948 74 0 0 25 0 1 0 549022963 105443328 24589 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25743 24589 603 41 0 25702 0
vsize: 102972
[startup+790.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 27888 0 0 0 78948 74 0 0 25 0 1 0 549022963 105979904 24735 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25874 24735 603 41 0 25833 0
vsize: 103496
[startup+800.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 27972 0 0 0 79948 74 0 0 25 0 1 0 549022963 106381312 24819 4294967295 134512640 134672761 3221224544 3221223712 134561266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25972 24819 603 41 0 25931 0
vsize: 103888
[startup+810.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 28095 0 0 0 80948 75 0 0 25 0 1 0 549022963 106786816 24942 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26071 24942 603 41 0 26030 0
vsize: 104284
[startup+820.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 28289 0 0 0 81947 75 0 0 25 0 1 0 549022963 107597824 25136 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26269 25136 603 41 0 26228 0
vsize: 105076
[startup+830.124 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 28405 0 0 0 82947 76 0 0 25 0 1 0 549022963 108138496 25252 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26401 25252 603 41 0 26360 0
vsize: 105604
[startup+840.124 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 28488 0 0 0 83947 76 0 0 25 0 1 0 549022963 108400640 25335 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26465 25335 603 41 0 26424 0
vsize: 105860
[startup+850.124 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 28575 0 0 0 84947 77 0 0 25 0 1 0 549022963 108802048 25422 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26563 25422 603 41 0 26522 0
vsize: 106252
[startup+860.125 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 28603 0 0 0 85947 77 0 0 25 0 1 0 549022963 108937216 25450 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26596 25450 603 41 0 26555 0
vsize: 106384
[startup+870.126 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 28631 0 0 0 86947 77 0 0 25 0 1 0 549022963 109072384 25478 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26629 25478 603 41 0 26588 0
vsize: 106516
[startup+880.126 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 28664 0 0 0 87947 77 0 0 25 0 1 0 549022963 109203456 25511 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26661 25511 603 41 0 26620 0
vsize: 106644
[startup+890.126 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 28689 0 0 0 88947 77 0 0 25 0 1 0 549022963 109203456 25536 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26661 25536 603 41 0 26620 0
vsize: 106644
[startup+900.127 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 28722 0 0 0 89947 77 0 0 25 0 1 0 549022963 109338624 25569 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26694 25569 603 41 0 26653 0
vsize: 106776
[startup+910.126 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 28794 0 0 0 90947 77 0 0 25 0 1 0 549022963 109735936 25641 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25641 603 41 0 26750 0
vsize: 107164
[startup+920.127 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 28893 0 0 0 91946 78 0 0 25 0 1 0 549022963 110129152 25740 4294967295 134512640 134672761 3221224544 3221223680 134560716 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26887 25740 603 41 0 26846 0
vsize: 107548
[startup+930.128 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 28931 0 0 0 92946 78 0 0 25 0 1 0 549022963 110260224 25778 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26919 25778 603 41 0 26878 0
vsize: 107676
[startup+940.127 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 28975 0 0 0 93946 79 0 0 25 0 1 0 549022963 110399488 25822 4294967295 134512640 134672761 3221224544 3221223680 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26953 25822 603 41 0 26912 0
vsize: 107812
[startup+950.127 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 29060 0 0 0 94946 79 0 0 25 0 1 0 549022963 110804992 25907 4294967295 134512640 134672761 3221224544 3221223648 134560010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27052 25907 603 41 0 27011 0
vsize: 108208
[startup+960.127 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 29105 0 0 0 95946 79 0 0 25 0 1 0 549022963 110940160 25952 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27085 25952 603 41 0 27044 0
vsize: 108340
[startup+970.127 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 29177 0 0 0 96946 80 0 0 25 0 1 0 549022963 111210496 26024 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27151 26024 603 41 0 27110 0
vsize: 108604
[startup+980.128 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 29180 0 0 0 97946 80 0 0 25 0 1 0 549022963 111210496 26027 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27151 26027 603 41 0 27110 0
vsize: 108604
[startup+990.128 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 29199 0 0 0 98946 80 0 0 25 0 1 0 549022963 111325184 26046 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27179 26046 603 41 0 27138 0
vsize: 108716
[startup+1000.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 29220 0 0 0 99946 80 0 0 25 0 1 0 549022963 111456256 26067 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27211 26067 603 41 0 27170 0
vsize: 108844
[startup+1010.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 29294 0 0 0 100946 80 0 0 25 0 1 0 549022963 111726592 26141 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27277 26141 603 41 0 27236 0
vsize: 109108
[startup+1020.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 29862 0 0 0 101945 81 0 0 25 0 1 0 549022963 112590848 26419 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27488 26419 603 41 0 27447 0
vsize: 109952
[startup+1030.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 29863 0 0 0 102945 81 0 0 25 0 1 0 549022963 112590848 26420 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27488 26420 603 41 0 27447 0
vsize: 109952
[startup+1040.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 29864 0 0 0 103945 82 0 0 25 0 1 0 549022963 112590848 26421 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27488 26421 603 41 0 27447 0
vsize: 109952
[startup+1050.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 29915 0 0 0 104945 82 0 0 25 0 1 0 549022963 112852992 26472 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27552 26472 603 41 0 27511 0
vsize: 110208
[startup+1060.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 29940 0 0 0 105945 82 0 0 25 0 1 0 549022963 113512448 26497 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27713 26497 603 41 0 27672 0
vsize: 110852
[startup+1070.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 29965 0 0 0 106945 82 0 0 25 0 1 0 549022963 113512448 26522 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27713 26522 603 41 0 27672 0
vsize: 110852
[startup+1080.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 30033 0 0 0 107945 83 0 0 25 0 1 0 549022963 113922048 26590 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27813 26590 603 41 0 27772 0
vsize: 111252
[startup+1090.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 30130 0 0 0 108945 83 0 0 25 0 1 0 549022963 114192384 26687 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27879 26687 603 41 0 27838 0
vsize: 111516
[startup+1100.13 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 30142 0 0 0 109945 83 0 0 25 0 1 0 549022963 114323456 26699 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27911 26699 603 41 0 27870 0
vsize: 111644
[startup+1110.13 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 30177 0 0 0 110945 83 0 0 25 0 1 0 549022963 114450432 26734 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27942 26734 603 41 0 27901 0
vsize: 111768
[startup+1120.13 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 30284 0 0 0 111945 84 0 0 25 0 1 0 549022963 114851840 26841 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28040 26841 603 41 0 27999 0
vsize: 112160
[startup+1130.13 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 30492 0 0 0 112944 85 0 0 25 0 1 0 549022963 115777536 27049 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28266 27049 603 41 0 28225 0
vsize: 113064
[startup+1140.13 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 30668 0 0 0 113944 85 0 0 25 0 1 0 549022963 116465664 27225 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28434 27225 603 41 0 28393 0
vsize: 113736
[startup+1150.13 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 30777 0 0 0 114944 85 0 0 25 0 1 0 549022963 116862976 27334 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28531 27334 603 41 0 28490 0
vsize: 114124
[startup+1160.13 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 30934 0 0 0 115943 86 0 0 25 0 1 0 549022963 117551104 27491 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28699 27491 603 41 0 28658 0
vsize: 114796
[startup+1170.13 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 31043 0 0 0 116943 87 0 0 25 0 1 0 549022963 117952512 27600 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28797 27600 603 41 0 28756 0
vsize: 115188
[startup+1180.13 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 31119 0 0 0 117943 87 0 0 25 0 1 0 549022963 118218752 27676 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28862 27676 603 41 0 28821 0
vsize: 115448
[startup+1190.13 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 35548 0 0 0 118932 98 0 0 25 0 1 0 549022963 151031808 31659 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36873 31659 603 41 0 36832 0
vsize: 147492
[startup+1200.13 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 16613
Raw data (stat): 16613 (minisat+) R 16612 3260 3259 0 -1 0 35607 0 0 0 119932 98 0 0 25 0 1 0 549022963 151031808 31718 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36873 31718 603 41 0 36832 0
vsize: 147492
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.2 s]
Raw data (loadavg): 1.01 0.99 0.91 1/54 16613
Raw data (stat): 16613 (minisat+) Z 16612 3260 3259 0 -1 12 35610 0 0 0 119932 104 0 0 25 0 1 0 549022963 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.2
CPU time (s): 1200.37
CPU user time (s): 1199.33
CPU system time (s): 1.04684
CPU usage (%): 100.015
Max. virtual memory (Kb): 147492
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####