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/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-ran10x10a.opb
MD5SUM	133d42fd76e8bbd92509939943f41498
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	398336
Optimality of the best value was proved	NO
Number of terms in the objective function	2100
Biggest coefficient in the objective function	4718592
Number of bits for the biggest coefficient in the objective function	23
Sum of the numbers in the objective function	539671039
Number of bits of the sum of numbers in the objective function	30
Biggest number in a constraint	4718592
Number of bits of the biggest number in a constraint	23
Biggest sum of numbers in a constraint	539671039
Number of bits of the biggest sum of numbers	30
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	913.784
Number of variables	2100
Total number of constraints	120
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	120
Minimum length of a constraint	21
Maximum length of a constraint	200
Trace number 14819

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        293024 kB
Buffers:         38128 kB
Cached:         662816 kB
SwapCached:          0 kB
Active:         245672 kB
Inactive:       458200 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        292772 kB
SwapTotal:     2097892 kB
SwapFree:      2097892 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6964 kB
Slab:            32264 kB
Committed_AS:    63728 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 01:55:29 (client local time) WITH STATUS 10 IN 1200.25 SECONDS
stats: 19201 7 1200.25 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 140 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 138]---> Adder-cost: 178   maxlim: 8310   bits: 14/14
c ---[ 136]---> Adder-cost: 178   maxlim: 8694   bits: 14/14
c ---[ 134]---> Adder-cost: 178   maxlim: 8310   bits: 14/14
c ---[ 132]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2
c ---[ 130]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2
c ---[ 128]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2
c ---[ 126]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2
c ---[ 124]---> Sorter-cost: 2042     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 122]---> Adder-cost: 178   maxlim: 8438   bits: 14/14
c ---[ 120]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2
c ---[ 118]---> Sorter-cost: 1874     Base: 2 2 2 2 2 2 2 2 2
c ---[ 116]---> Sorter-cost: 2034     Base: 2 2 2 2 2 2 2 2 2
c ---[ 114]---> Adder-cost: 194   maxlim: 16374   bits: 15/14
c ---[ 112]---> Sorter-cost: 2034     Base: 2 2 2 2 2 2 2 2 2
c ---[ 110]---> Sorter-cost: 2034     Base: 2 2 2 2 2 2 2 2 2
c ---[ 108]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 106]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 104]---> Sorter-cost: 1874     Base: 2 2 2 2 2 2 2 2 2
c ---[ 102]---> Sorter-cost: 2034     Base: 2 2 2 2 2 2 2 2 2
c ---[ 100]---> Adder-cost: 194   maxlim: 16246   bits: 15/14
c ---[  99]---> BDD-cost:   11
c ---[  98]---> BDD-cost:   13
c ---[  97]---> BDD-cost:   11
c ---[  96]---> BDD-cost:   11
c ---[  95]---> BDD-cost:   11
c ---[  94]---> BDD-cost:   11
c ---[  93]---> BDD-cost:   11
c ---[  92]---> BDD-cost:   10
c ---[  91]---> BDD-cost:   11
c ---[  90]---> BDD-cost:   11
c ---[  89]---> BDD-cost:   11
c ---[  88]---> BDD-cost:   11
c ---[  87]---> BDD-cost:   13
c ---[  86]---> BDD-cost:   11
c ---[  85]---> BDD-cost:   13
c ---[  84]---> BDD-cost:   13
c ---[  83]---> BDD-cost:   13
c ---[  82]---> BDD-cost:   13
c ---[  81]---> BDD-cost:   10
c ---[  80]---> BDD-cost:   11
c ---[  79]---> BDD-cost:   13
c ---[  78]---> BDD-cost:   13
c ---[  77]---> BDD-cost:   13
c ---[  76]---> BDD-cost:   13
c ---[  75]---> BDD-cost:   11
c ---[  74]---> BDD-cost:   12
c ---[  73]---> BDD-cost:   15
c ---[  72]---> BDD-cost:   15
c ---[  71]---> BDD-cost:   15
c ---[  70]---> BDD-cost:   10
c ---[  69]---> BDD-cost:   11
c ---[  68]---> BDD-cost:   13
c ---[  67]---> BDD-cost:   15
c ---[  66]---> BDD-cost:   15
c ---[  65]---> BDD-cost:   13
c ---[  64]---> BDD-cost:   11
c ---[  63]---> BDD-cost:   12
c ---[  62]---> BDD-cost:   13
c ---[  61]---> BDD-cost:   13
c ---[  60]---> BDD-cost:   13
c ---[  59]---> BDD-cost:   10
c ---[  58]---> BDD-cost:   11
c ---[  57]---> BDD-cost:   13
c ---[  56]---> BDD-cost:   13
c ---[  55]---> BDD-cost:   13
c ---[  54]---> BDD-cost:   10
c ---[  53]---> BDD-cost:   11
c ---[  52]---> BDD-cost:   12
c ---[  51]---> BDD-cost:   15
c ---[  50]---> BDD-cost:   15
c ---[  49]---> BDD-cost:   15
c ---[  48]---> BDD-cost:   10
c ---[  47]---> BDD-cost:   11
c ---[  46]---> BDD-cost:   13
c ---[  45]---> BDD-cost:   15
c ---[  44]---> BDD-cost:   15
c ---[  43]---> BDD-cost:   11
c ---[  42]---> BDD-cost:   11
c ---[  41]---> BDD-cost:   12
c ---[  40]---> BDD-cost:   15
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:   15
c ---[  37]---> BDD-cost:   10
c ---[  36]---> BDD-cost:   11
c ---[  35]---> BDD-cost:   13
c ---[  34]---> BDD-cost:   15
c ---[  33]---> BDD-cost:   15
c ---[  32]---> BDD-cost:   13
c ---[  31]---> BDD-cost:   11
c ---[  30]---> BDD-cost:   12
c ---[  29]---> BDD-cost:   13
c ---[  28]---> BDD-cost:   15
c ---[  27]---> BDD-cost:   15
c ---[  26]---> BDD-cost:   10
c ---[  25]---> BDD-cost:   11
c ---[  24]---> BDD-cost:   13
c ---[  23]---> BDD-cost:   15
c ---[  22]---> BDD-cost:   13
c ---[  21]---> BDD-cost:   13
c ---[  20]---> BDD-cost:   11
c ---[  19]---> BDD-cost:   12
c ---[  18]---> BDD-cost:   12
c ---[  17]---> BDD-cost:   12
c ---[  16]---> BDD-cost:   12
c ---[  15]---> BDD-cost:   10
c ---[  14]---> BDD-cost:   11
c ---[  13]---> BDD-cost:   12
c ---[  12]---> BDD-cost:   12
c ---[  11]---> BDD-cost:   12
c ---[  10]---> BDD-cost:   13
c ---[   9]---> BDD-cost:   11
c ---[   8]---> BDD-cost:   12
c ---[   7]---> BDD-cost:   15
c ---[   6]---> BDD-cost:   15
c ---[   5]---> BDD-cost:   15
c ---[   4]---> BDD-cost:   10
c ---[   3]---> BDD-cost:   11
c ---[   2]---> BDD-cost:   13
c ---[   1]---> BDD-cost:   15
c ---[   0]---> BDD-cost:   15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   78813   195092 |   26271       0        0     nan |  0.000 % |
c |       100 |   78796   195041 |   28898      99      424     4.3 |  7.452 % |
c |       250 |   78704   194827 |   31787     240     1061     4.4 |  7.548 % |
c |       475 |   78668   194747 |   34966     464     2342     5.0 |  7.585 % |
c |       812 |   78668   194747 |   38463     801     4231     5.3 |  7.585 % |
c |      1318 |   78668   194747 |   42309    1307     7014     5.4 |  7.585 % |
c |      2079 |   78665   194741 |   46540    2066    11190     5.4 |  7.588 % |
c |      3218 |   78665   194741 |   51194    3205    17864     5.6 |  7.588 % |
c |      4926 |   78636   194677 |   56314    4906    28263     5.8 |  7.621 % |
c |      7488 |   78416   194100 |   61945    7429    44152     5.9 |  7.824 % |
c ==============================================================================
c [1mFound solution: 1601666[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 3925   maxlim: 823677   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10053 |  105727   291776 |   35242    9983    61363     6.1 |  7.824 % |
c |     10153 |  105604   291497 |   38766   10068    61779     6.1 |  7.063 % |
c |     10304 |  105604   291497 |   42642   10219    62750     6.1 |  7.063 % |
c |     10529 |  105530   291330 |   46907   10441    64268     6.2 |  7.130 % |
c |     10867 |  105530   291330 |   51597   10779    68086     6.3 |  7.130 % |
c |     11373 |  105476   291196 |   56757   11278    70665     6.3 |  7.178 % |
c |     12132 |  105460   291144 |   62433   12035    76056     6.3 |  7.188 % |
c ==============================================================================
c [1mFound solution: 1588472[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 836871   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13151 |  105247   290698 |   35082   13039   171118    13.1 |  7.188 % |
c |     13253 |  105247   290698 |   38590   13141   172208    13.1 |  7.396 % |
c |     13404 |  105240   290675 |   42449   13290   173234    13.0 |  7.399 % |
c |     13629 |  105240   290675 |   46694   13515   175361    13.0 |  7.399 % |
c |     13966 |  105240   290675 |   51363   13852   177777    12.8 |  7.399 % |
c |     14472 |  105240   290675 |   56499   14358   182915    12.7 |  7.399 % |
c |     15231 |  104991   290092 |   62149   15111   187653    12.4 |  7.662 % |
c |     16370 |  104933   289900 |   68364   16239   196763    12.1 |  7.698 % |
c |     18079 |  104649   289252 |   75201   17934   276897    15.4 |  7.955 % |
c ==============================================================================
c [1mFound solution: 1144894[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 1280449   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18492 |  104668   289383 |   34889   18347   288789    15.7 |  7.955 % |
c |     18592 |  104668   289383 |   38377   18447   289341    15.7 |  7.980 % |
c |     18742 |  104668   289383 |   42215   18597   290053    15.6 |  7.980 % |
c |     18968 |  104588   289199 |   46437   18821   291301    15.5 |  8.064 % |
c |     19305 |  104588   289199 |   51080   19158   294329    15.4 |  8.064 % |
c |     19811 |  104565   289147 |   56189   19662   298066    15.2 |  8.083 % |
c |     20574 |  104526   289020 |   61807   20420   304191    14.9 |  8.106 % |
c |     21714 |  104225   288323 |   67988   21547   334783    15.5 |  8.404 % |
c |     23422 |  104037   287879 |   74787   23224   399754    17.2 |  8.571 % |
c |     25985 |  104037   287879 |   82266   25787   759192    29.4 |  8.571 % |
c |     29832 |  104037   287879 |   90493   29634  1150445    38.8 |  8.571 % |
c ==============================================================================
c [1mFound solution: 571504[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1853839   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30547 |  104052   287965 |   34684   30348  1208799    39.8 |  8.571 % |
c |     30647 |  103924   287670 |   38152   30446  1209404    39.7 |  8.719 % |
c |     30797 |  103924   287670 |   41967   30596  1210860    39.6 |  8.719 % |
c |     31022 |  103886   287582 |   46164   30820  1212484    39.3 |  8.755 % |
c |     31359 |  103740   287080 |   50780   31145  1215955    39.0 |  8.876 % |
c |     31865 |  103740   287080 |   55858   31651  1226432    38.7 |  8.876 % |
c |     32624 |  103740   287080 |   61444   32410  1287593    39.7 |  8.876 % |
c |     33765 |  103740   287080 |   67589   33551  1307687    39.0 |  8.876 % |
c |     35473 |  103672   286908 |   74348   35250  1376325    39.0 |  8.937 % |
c |     38037 |  103472   286453 |   81783   37798  1650568    43.7 |  9.133 % |
c |     41882 |  103472   286453 |   89961   41643  2099351    50.4 |  9.133 % |
c |     47649 |  103276   286001 |   98957   47400  2440774    51.5 |  9.339 % |
c |     56299 |  103239   285914 |  108853   56045  2955134    52.7 |  9.367 % |
c |     69273 |  103239   285914 |  119738   69019  5055973    73.3 |  9.367 % |
c |     88734 |  103129   285649 |  131712   88468  6163885    69.7 |  9.486 % |
c |    117926 |  103101   285585 |  144883  117656  8070014    68.6 |  9.512 % |
c |    161716 |  103074   285525 |  159372  161441 19922286   123.4 |  9.534 % |
c |    227400 |  102357   283875 |  175309   83514  9986379   119.6 | 10.231 % |
c |    325926 |  101993   283037 |  192840  181984 22040235   121.1 | 10.587 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -X0_bit_7 -X0_bit_6 -X0_bit_5 -X0_bit_4 -X0_bit_3 -X0_bit_2 -X0_bit_1 -X0_bit0 -X0_bit1 -X0_bit2 -X0_bit3 -X0_bit4 -X0_bit5 -X0_bit6 -X0_bit7 -X0_bit8 -X0_bit9 -X0_bit10 -X0_bit11 -X0_bit12 -X1_bit_7 -X1_bit_6 -X1_bit_5 -X1_bit_4 -X1_bit_3 -X1_bit_2 -X1_bit_1 -X1_bit0 -X1_bit1 -X1_bit2 -X1_bit3 -X1_bit4 -X1_bit5 -X1_bit6 -X1_bit7 -X1_bit8 -X1_bit9 -X1_bit10 -X1_bit11 -X1_bit12 X2_bit_7 X2_bit_6 X2_bit_5 X2_bit_4 X2_bit_3 X2_bit_2 X2_bit_1 X2_bit0 X2_bit1 -X2_bit2 -X2_bit3 -X2_bit4 -X2_bit5 -X2_bit6 -X2_bit7 -X2_bit8 -X2_bit9 -X2_bit10 -X2_bit11 -X2_bit12 -X3_bit_7 -X3_bit_6 -X3_bit_5 -X3_bit_4 -X3_bit_3 -X3_bit_2 -X3_bit_1 -X3_bit0 -X3_bit1 -X3_bit2 -X3_bit3 -X3_bit4 -X3_bit5 -X3_bit6 -X3_bit7 -X3_bit8 -X3_bit9 -X3_bit10 -X3_bit11 -X3_bit12 -X4_bit_7 -X4_bit_6 -X4_bit_5 -X4_bit_4 -X4_bit_3 -X4_bit_2 -X4_bit_1 -X4_bit0 -X4_bit1 -X4_bit2 -X4_bit3 -X4_bit4 -X4_bit5 -X4_bit6 -X4_bit7 -X4_bit8 -X4_bit9 -X4_bit10 -X4_bit11 -X4_bit12 -X5_bit_7 -X5_bit_6 -X5_bit_5 -X5_bit_4 -X5_bit_3 -X5_bit_2 -X5_bit_1 -X5_bit0 -X5_bit1 -X5_bit2 -X5_bit3 -X5_bit4 -X5_bit5 -X5_bit6 -X5_bit7 -X5_bit8 -X5_bit9 -X5_bit10 -X5_bit11 -X5_bit12 -X6_bit_7 -X6_bit_6 -X6_bit_5 -X6_bit_4 -X6_bit_3 -X6_bit_2 -X6_bit_1 -X6_bit0 -X6_bit1 -X6_bit2 -X6_bit3 -X6_bit4 -X6_bit5 -X6_bit6 -X6_bit7 -X6_bit8 -X6_bit9 -X6_bit10 -X6_bit11 -X6_bit12 -X7_bit_7 -X7_bit_6 -X7_bit_5 -X7_bit_4 -X7_bit_3 -X7_bit_2 -X7_bit_1 -X7_bit0 -X7_bit1 -X7_bit2 -X7_bit3 -X7_bit4 -X7_bit5 -X7_bit6 -X7_bit7 -X7_bit8 -X7_bit9 -X7_bit10 -X7_bit11 -X7_bit12 X8_bit_7 -X8_bit_6 -X8_bit_5 -X8_bit_4 -X8_bit_3 -X8_bit_2 -X8_bit_1 X8_bit0 X8_bit1 -X8_bit2 -X8_bit3 -X8_bit4 -X8_bit5 -X8_bit6 -X8_bit7 -X8_bit8 -X8_bit9 -X8_bit10 -X8_bit11 -X8_bit12 -X9_bit_7 -X9_bit_6 -X9_bit_5 -X9_bit_4 -X9_bit_3 -X9_bit_2 -X9_bit_1 -X9_bit0 -X9_bit1 -X9_bit2 -X9_bit3 -X9_bit4 -X9_bit5 -X9_bit6 -X9_bit7 -X9_bit8 -X9_bit9 -X9_bit10 -X9_bit11 -X9_bit12 X10_bit_7 -X10_bit_6 -X10_bit_5 X10_bit_4 -X10_bit_3 -X10_bit_2 X10_bit_1 -X10_bit0 -X10_bit1 -X10_bit2 -X10_bit3 -X10_bit4 -X10_bit5 -X10_bit6 -X10_bit7 -X10_bit8 -X10_bit9 -X10_bit10 -X10_bit11 -X10_bit12 -X11_bit_7 -X11_bit_6 -X11_bit_5 X11_bit_4 -X11_bit_3 -X11_bit_2 X11_bit_1 -X11_bit0 -X11_bit1 -X11_bit2 -X11_bit3 -X11_bit4 -X11_bit5 -X11_bit6 -X11_bit7 -X11_bit8 -X11_bit9 -X11_bit10 -X11_bit11 -X11_bit12 -X12_bit_7 -X12_bit_6 -X12_bit_5 -X12_bit_4 -X12_bit_3 -X12_bit_2 -X12_bit_1 -X12_bit0 -X12_bit1 -X12_bit2 -X12_bit3 -X12_bit4 -X12_bit5 -X12_bit6 -X12_bit7 -X12_bit8 -X12_bit9 -X12_bit10 -X12_bit11 -X12_bit12 X13_bit_7 X13_bit_6 X13_bit_5 X13_bit_4 -X13_bit_3 X13_bit_2 -X13_bit_1 X13_bit0 -X13_bit1 -X13_bit2 -X13_bit3 -X13_bit4 -X13_bit5 -X13_bit6 -X13_bit7 -X13_bit8 -X13_bit9 -X13_bit10 -X13_bit11 -X13_bit12 -X14_bit_7 -X14_bit_6 -X14_bit_5 -X14_bit_4 -X14_bit_3 -X14_bit_2 -X14_bit_1 -X14_bit0 -X14_bit1 -X14_bit2 -X14_bit3 -X14_bit4 -X14_bit5 -X14_bit6 -X14_bit7 -X14_bit8 -X14_bit9 -X14_bit10 -X14_bit11 -X14_bit12 -X15_bit_7 -X15_bit_6 -X15_bit_5 -X15_bit_4 -X15_bit_3 -X15_bit_2 -X15_bit_1 -X15_bit0 -X15_bit1 -X15_bit2 -X15_bit3 -X15_bit4 -X15_bit5 -X15_bit6 -X15_bit7 -X15_bit8 -X15_bit9 -X15_bit10 -X15_bit11 -X15_bit12 -X16_bit_7 -X16_bit_6 -X16_bit_5 -X16_bit_4 -X16_bit_3 -X16_bit_2 -X16_bit_1 -X16_bit0 -X16_bit1 -X16_bit2 -X16_bit3 -X16_bit4 -X16_bit5 -X16_bit6 -X16_bit7 -X16_bit8 -X16_bit9 -X16_bit10 -X16_bit11 -X16_bit12 -X17_bit_7 -X17_bit_6 -X17_bit_5 -X17_bit_4 X17_bit_3 X17_bit_2 -X17_bit_1 -X17_bit0 -X17_bit1 -X17_bit2 -X17_bit3 -X17_bit4 -X17_bit5 -X17_bit6 -X17_bit7 -X17_bit8 -X17_bit9 -X17_bit10 -X17_bit11 -X17_bit12 -X18_bit_7 -X18_bit_6 -X18_bit_5 -X18_bit_4 X18_bit_3 -X18_bit_2 -X18_bit_1 X18_bit0 -X18_bit1 -X18_bit2 -X18_bit3 -X18_bit4 -X18_bit5 -X18_bit6 -X18_bit7 -X18_bit8 -X18_bit9 -X18_bit10 -X18_bit11 -X18_bit12 -X19_bit_7 -X19_bit_6 -X19_bit_5 -X19_bit_4 -X19_bit_3 -X19_bit_2 -X19_bit_1 -X19_bit0 -X19_bit1 -X19_bit2 -X19_bit3 -X19_bit4 -X19_bit5 -X19_bit6 -X19_bit7 -X19_bit8 -X19_bit9 -X19_bit10 -X19_bit11 -X19_bit12 -X20_bit_7 -X20_bit_6 -X20_bit_5 -X20_bit_4 -X20_bit_3 -X20_bit_2 -X20_bit_1 -X20_bit0 -X20_bit1 -X20_bit2 -X20_bit3 -X20_bit4 -X20_bit5 -X20_bit6 -X20_bit7 -X20_bit8 -X20_bit9 -X20_bit10 -X20_bit11 -X20_bit12 -X21_bit_7 -X21_bit_6 -X21_bit_5 -X21_bit_4 -X21_bit_3 -X21_bit_2 -X21_bit_1 -X21_bit0 -X21_bit1 -X21_bit2 -X21_bit3 -X21_bit4 -X21_bit5 -X21_bit6 -X21_bit7 -X21_bit8 -X21_bit9 -X21_bit10 -X21_bit11 -X21_bit12 -X22_bit_7 -X22_bit_6 -X22_bit_5 -X22_bit_4 -X22_bit_3 -X22_bit_2 -X22_bit_1 -X22_bit0 -X22_bit1 -X22_bit2 -X22_bit3 -X22_bit4 -X22_bit5 -X22_bit6 -X22_bit7 -X22_bit8 -X22_bit9 -X22_bit10 -X22_bit11 -X22_bit12 -X23_bit_7 -X23_bit_6 -X23_bit_5 -X23_bit_4 -X23_bit_3 -X23_bit_2 -X23_bit_1 -X23_bit0 -X23_bit1 -X23_bit2 -X23_bit3 -X23_bit4 -X23_bit5 -X23_bit6 -X23_bit7 -X23_bit8 -X23_bit9 -X23_bit10 -X23_bit11 -X23_bit12 X24_bit_7 X24_bit_6 X24_bit_5 X24_bit_4 X24_bit_3 X24_bit_2 -X24_bit_1 X24_bit0 -X24_bit1 X24_bit2 -X24_bit3 -X24_bit4 -X24_bit5 -X24_bit6 -X24_bit7 -X24_bit8 -X24_bit9 -X24_bit10 -X24_bit11 -X24_bit12 -X25_bit_7 -X25_bit_6 -X25_bit_5 -X25_bit_4 -X25_bit_3 -X25_bit_2 -X25_bit_1 -X25_bit0 -X25_bit1 -X25_bit2 -X25_bit3 -X25_bit4 -X25_bit5 -X25_bit6 -X25_bit7 -X25_bit8 -X25_bit9 -X25_bit10 -X25_bit11 -X25_bit12 -X26_bit_7 -X26_bit_6 -X26_bit_5 -X26_bit_4 -X26_bit_3 -X26_bit_2 -X26_bit_1 -X26_bit0 -X26_bit1 -X26_bit2 -X26_bit3 -X26_bit4 -X26_bit5 -X26_bit6 -X26_bit7 -X26_bit8 -X26_bit9 -X26_bit10 -X26_bit11 -X26_bit12 -X27_bit_7 -X27_bit_6 -X27_bit_5 -X27_bit_4 -X27_bit_3 -X27_bit_2 -X27_bit_1 -X27_bit0 -X27_bit1 -X27_bit2 -X27_bit3 -X27_bit4 -X27_bit5 -X27_bit6 -X27_bit7 -X27_bit8 -X27_bit9 -X27_bit10 -X27_bit11 -X27_bit12 -X28_bit_7 -X28_bit_6 -X28_bit_5 -X28_bit_4 -X28_bit_3 X28_bit_2 -X28_bit_1 X28_bit0 -X28_bit1 -X28_bit2 -X28_bit3 -X28_bit4 -X28_bit5 -X28_bit6 -X28_bit7 -X28_bit8 -X28_bit9 -X28_bit10 -X28_bit11 -X28_bit12 X29_bit_7 -X29_bit_6 -X29_bit_5 -X29_bit_4 -X29_bit_3 X29_bit_2 -X29_bit_1 -X29_bit0 -X29_bit1 -X29_bit2 -X29_bit3 -X29_bit4 -X29_bit5 -X29_bit6 -X29_bit7 -X29_bit8 -X29_bit9 -X29_bit10 -X29_bit11 -X29_bit12 -X30_bit_7 -X30_bit_6 -X30_bit_5 -X30_bit_4 -X30_bit_3 -X30_bit_2 -X30_bit_1 -X30_bit0 -X30_bit1 -X30_bit2 -X30_bit3 -X30_bit4 -X30_bit5 -X30_bit6 -X30_bit7 -X30_bit8 -X30_bit9 -X30_bit10 -X30_bit11 -X30_bit12 -X31_bit_7 -X31_bit_6 -X31_bit_5 -X31_bit_4 -X31_bit_3 -X31_bit_2 -X31_bit_1 -X31_bit0 -X31_bit1 -X31_bit2 -X31_bit3 -X31_bit4 -X31_bit5 -X31_bit6 -X31_bit7 -X31_bit8 -X31_bit9 -X31_bit10 -X31_bit11 -X31_bit12 X32_bit_7 -X32_bit_6 X32_bit_5 -X32_bit_4 -X32_bit_3 -X32_bit_2 -X32_bit_1 -X32_bit0 -X32_bit1 -X32_bit2 -X32_bit3 -X32_bit4 -X32_bit5 -X32_bit6 -X32_bit7 -X32_bit8 -X32_bit9 -X32_bit10 -X32_bit11 -X32_bit12 X33_bit_7 -X33_bit_6 -X33_bit_5 -X33_bit_4 X33_bit_3 X33_bit_2 -X33_bit_1 -X33_bit0 -X33_bit1 -X33_bit2 X33_bit3 -X33_bit4 -X33_bit5 -X33_bit6 -X33_bit7 -X33_bit8 -X33_bit9 -X33_bit10 -X33_bit11 -X33_bit12 -X34_bit_7 X34_bit_6 -X34_bit_5 X34_bit_4 -X34_bit_3 -X34_bit_2 X34_bit_1 -X34_bit0 -X34_bit1 -X34_bit2 -X34_bit3 -X34_bit4 -X34_bit5 -X34_bit6 -X34_bit7 -X34_bit8 -X34_bit9 -X34_bit10 -X34_bit11 -X34_bit12 -X35_bit_7 -X35_bit_6 -X35_bit_5 -X35_bit_4 -X35_bit_3 -X35_bit_2 -X35_bit_1 -X35_bit0 -X35_bit1 -X35_bit2 -X35_bit3 -X35_bit4 -X35_bit5 -X35_bit6 -X35_bit7 -X35_bit8 -X35_bit9 -X35_bit10 -X35_bit11 -X35_bit12 -X36_bit_7 -X36_bit_6 -X36_bit_5 -X36_bit_4 -X36_bit_3 -X36_bit_2 -X36_bit_1 -X36_bit0 -X36_bit1 -X36_bit2 -X36_bit3 -X36_bit4 -X36_bit5 -X36_bit6 -X36_bit7 -X36_bit8 -X36_bit9 -X36_bit10 -X36_bit11 -X36_bit12 -X37_bit_7 -X37_bit_6 -X37_bit_5 -X37_bit_4 -X37_bit_3 -X37_bit_2 -X37_bit_1 -X37_bit0 -X37_bit1 -X37_bit2 -X37_bit3 -X37_bit4 -X37_bit5 -X37_bit6 -X37_bit7 -X37_bit8 -X37_bit9 -X37_bit10 -X37_bit11 -X37_bit12 -X38_bit_7 -X38_bit_6 -X38_bit_5 -X38_bit_4 -X38_bit_3 -X38_bit_2 -X38_bit_1 -X38_bit0 -X38_bit1 -X38_bit2 -X38_bit3 -X38_bit4 -X38_bit5 -X38_bit6 -X38_bit7 -X38_bit8 -X38_bit9 -X38_bit10 -X38_bit11 -X38_bit12 -X39_bit_7 -X39_bit_6 -X39_bit_5 -X39_bit_4 -X39_bit_3 -X39_bit_2 -X39_bit_1 -X39_bit0 -X39_bit1 -X39_bit2 -X39_bit3 -X39_bit4 -X39_bit5 -X39_bit6 -X39_bit7 -X39_bit8 -X39_bit9 -X39_bit10 -X39_bit11 -X39_bit12 -X40_bit_7 -X40_bit_6 -X40_bit_5 -X40_bit_4 -X40_bit_3 -X40_bit_2 -X40_bit_1 -X40_bit0 -X40_bit1 -X40_bit2 -X40_bit3 -X40_bit4 -X40_bit5 -X40_bit6 -X40_bit7 -X40_bit8 -X40_bit9 -X40_bit10 -X40_bit11 -X40_bit12 X41_bit_7 -X41_bit_6 -X41_bit_5 -X41_bit_4 -X41_bit_3 -X41_bit_2 X41_bit_1 X41_bit0 X41_bit1 -X41_bit2 -X41_bit3 -X41_bit4 -X41_bit5 -X41_bit6 -X41_bit7 -X41_bit8 -X41_bit9 -X41_bit10 -X41_bit11 -X41_bit12 X42_bit_7 X42_bit_6 X42_bit_5 X42_bit_4 -X42_bit_3 X42_bit_2 X42_bit_1 X42_bit0 -X42_bit1 -X42_bit2 -X42_bit3 -X42_bit4 -X42_bit5 -X42_bit6 -X42_bit7 -X42_bit8 -X42_bit9 -X42_bit10 -X42_bit11 -X42_bit12 -X43_bit_7 -X43_bit_6 -X43_bit_5 -X43_bit_4 -X43_bit_3 -X43_bit_2 -X43_bit_1 -X43_bit0 -X43_bit1 -X43_bit2 -X43_bit3 -X43_bit4 -X43_bit5 -X43_bit6 -X43_bit7 -X43_bit8 -X43_bit9 -X43_bit10 -X43_bit11 -X43_bit12 -X44_bit_7 -X44_bit_6 -X44_bit_5 -X44_bit_4 -X44_bit_3 -X44_bit_2 -X44_bit_1 -X44_bit0 -X44_bit1 -X44_bit2 -X44_bit3 -X44_bit4 -X44_bit5 -X44_bit6 -X44_bit7 -X44_bit8 -X44_bit9 -X44_bit10 -X44_bit11 -X44_bit12 -X45_bit_7 -X45_bit_6 -X45_bit_5 -X45_bit_4 -X45_bit_3 -X45_bit_2 -X45_bit_1 -X45_bit0 -X45_bit1 -X45_bit2 -X45_bit3 -X45_bit4 -X45_bit5 -X45_bit6 -X45_bit7 -X45_bit8 -X45_bit9 -X45_bit10 -X45_bit11 -X45_bit12 -X46_bit_7 -X46_bit_6 -X46_bit_5 -X46_bit_4 -X46_bit_3 -X46_bit_2 -X46_bit_1 -X46_bit0 -X46_bit1 -X46_bit2 -X46_bit3 -X46_bit4 -X46_bit5 -X46_bit6 -X46_bit7 -X46_bit8 -X46_bit9 -X46_bit10 -X46_bit11 -X46_bit12 -X47_bit_7 -X47_bit_6 -X47_bit_5 -X47_bit_4 X47_bit_3 -X47_bit_2 X47_bit_1 -X47_bit0 X47_bit1 X47_bit2 -X47_bit3 -X47_bit4 -X47_bit5 -X47_bit6 -X47_bit7 -X47_bit8 -X47_bit9 -X47_bit10 -X47_bit11 -X47_bit12 -X48_bit_7 -X48_bit_6 -X48_bit_5 -X48_bit_4 -X48_bit_3 -X48_bit_2 -X48_bit_1 -X48_bit0 -X48_bit1 -X48_bit2 -X48_bit3 -X48_bit4 -X48_bit5 -X48_bit6 -X48_bit7 -X48_bit8 -X48_bit9 -X48_bit10 -X48_bit11 -X48_bit12 -X49_bit_7 -X49_bit_6 -X49_bit_5 -X49_bit_4 -X49_bit_3 -X49_bit_2 -X49_bit_1 -X49_bit0 -X49_bit1 -X49_bit2 -X49_bit3 -X49_bit4 -X49_bit5 -X49_bit6 -X49_bit7 -X49_bit8 -X49_bit9 -X49_bit10 -X49_bit11 -X49_bit12 -X50_bit_7 -X50_bit_6 -X50_bit_5 -X50_bit_4 -X50_bit_3 -X50_bit_2 -X50_bit_1 -X50_bit0 -X50_bit1 -X50_bit2 -X50_bit3 -X50_bit4 -X50_bit5 -X50_bit6 -X50_bit7 -X50_bit8 -X50_bit9 -X50_bit10 -X50_bit11 -X50_bit12 -X51_bit_7 -X51_bit_6 -X51_bit_5 -X51_bit_4 -X51_bit_3 -X51_bit_2 -X51_bit_1 -X51_bit0 -X51_bit1 -X51_bit2 -X51_bit3 -X51_bit4 -X51_bit5 -X51_bit6 -X51_bit7 -X51_bit8 -X51_bit9 -X51_bit10 -X51_bit11 -X51_bit12 X52_bit_7 X52_bit_6 X52_bit_5 -X52_bit_4 X52_bit_3 X52_bit_2 -X52_bit_1 X52_bit0 X52_bit1 X52_bit2 -X52_bit3 -X52_bit4 -X52_bit5 -X52_bit6 -X52_bit7 -X52_bit8 -X52_bit9 -X52_bit10 -X52_bit11 -X52_bit12 -X53_bit_7 -X53_bit_6 -X53_bit_5 -X53_bit_4 -X53_bit_3 -X53_bit_2 -X53_bit_1 -X53_bit0 -X53_bit1 -X53_bit2 -X53_bit3 -X53_bit4 -X53_bit5 -X53_bit6 -X53_bit7 -X53_bit8 -X53_bit9 -X53_bit10 -X53_bit11 -X53_bit12 -X54_bit_7 -X54_bit_6 -X54_bit_5 -X54_bit_4 -X54_bit_3 -X54_bit_2 -X54_bit_1 -X54_bit0 -X54_bit1 -X54_bit2 -X54_bit3 -X54_bit4 -X54_bit5 -X54_bit6 -X54_bit7 -X54_bit8 -X54_bit9 -X54_bit10 -X54_bit11 -X54_bit12 -X55_bit_7 -X55_bit_6 -X55_bit_5 -X55_bit_4 -X55_bit_3 -X55_bit_2 -X55_bit_1 -X55_bit0 -X55_bit1 -X55_bit2 -X55_bit3 -X55_bit4 -X55_bit5 -X55_bit6 -X55_bit7 -X55_bit8 -X55_bit9 -X55_bit10 -X55_bit11 -X55_bit12 X56_bit_7 -X56_bit_6 -X56_bit_5 X56_bit_4 -X56_bit_3 -X56_bit_2 X56_bit_1 -X56_bit0 -X56_bit1 -X56_bit2 -X56_bit3 -X56_bit4 -X56_bit5 -X56_bit6 -X56_bit7 -X56_bit8 -X56_bit9 -X56_bit10 -X56_bit11 -X56_bit12 -X57_bit_7 -X57_bit_6 -X57_bit_5 -X57_bit_4 -X57_bit_3 -X57_bit_2 -X57_bit_1 -X57_bit0 -X57_bit1 -X57_bit2 -X57_bit3 -X57_bit4 -X57_bit5 -X57_bit6 -X57_bit7 -X57_bit8 -X57_bit9 -X57_bit10 -X57_bit11 -X57_bit12 -X58_bit_7 -X58_bit_6 -X58_bit_5 -X58_bit_4 -X58_bit_3 -X58_bit_2 -X58_bit_1 X58_bit0 X58_bit1 -X58_bit2 -X58_bit3 -X58_bit4 -X58_bit5 -X58_bit6 -X58_bit7 -X58_bit8 -X58_bit9 -X58_bit10 -X58_bit11 -X58_bit12 -X59_bit_7 -X59_bit_6 -X59_bit_5 -X59_bit_4 -X59_bit_3 -X59_bit_2 -X59_bit_1 -X59_bit0 -X59_bit1 -X59_bit2 -X59_bit3 -X59_bit4 -X59_bit5 -X59_bit6 -X59_bit7 -X59_bit8 -X59_bit9 -X59_bit10 -X59_bit11 -X59_bit12 -X60_bit_7 -X60_bit_6 -X60_bit_5 -X60_bit_4 -X60_bit_3 -X60_bit_2 -X60_bit_1 -X60_bit0 -X60_bit1 -X60_bit2 -X60_bit3 -X60_bit4 -X60_bit5 -X60_bit6 -X60_bit7 -X60_bit8 -X60_bit9 -X60_bit10 -X60_bit11 -X60_bit12 -X61_bit_7 -X61_bit_6 -X61_bit_5 -X61_bit_4 -X61_bit_3 -X61_bit_2 -X61_bit_1 -X61_bit0 -X61_bit1 -X61_bit2 -X61_bit3 -X61_bit4 -X61_bit5 -X61_bit6 -X61_bit7 -X61_bit8 -X61_bit9 -X61_bit10 -X61_bit11 -X61_bit12 X62_bit_7 X62_bit_6 X62_bit_5 -X62_bit_4 X62_bit_3 -X62_bit_2 -X62_bit_1 X62_bit0 -X62_bit1 -X62_bit2 -X62_bit3 -X62_bit4 -X62_bit5 -X62_bit6 -X62_bit7 -X62_bit8 -X62_bit9 -X62_bit10 -X62_bit11 -X62_bit12 -X63_bit_7 -X63_bit_6 -X63_bit_5 -X63_bit_4 -X63_bit_3 X63_bit_2 -X63_bit_1 X63_bit0 -X63_bit1 X63_bit2 -X63_bit3 -X63_bit4 -X63_bit5 -X63_bit6 -X63_bit7 -X63_bit8 -X63_bit9 -X63_bit10 -X63_bit11 -X63_bit12 -X64_bit_7 -X64_bit_6 -X64_bit_5 -X64_bit_4 -X64_bit_3 -X64_bit_2 X64_bit_1 X64_bit0 -X64_bit1 X64_bit2 -X64_bit3 -X64_bit4 -X64_bit5 -X64_bit6 -X64_bit7 -X64_bit8 -X64_bit9 -X64_bit10 -X64_bit11 -X64_bit12 X65_bit_7 -X65_bit_6 -X65_bit_5 X65_bit_4 -X65_bit_3 -X65_bit_2 -X65_bit_1 -X65_bit0 -X65_bit1 -X65_bit2 -X65_bit3 -X65_bit4 -X65_bit5 -X65_bit6 -X65_bit7 -X65_bit8 -X65_bit9 -X65_bit10 -X65_bit11 -X65_bit12 -X66_bit_7 -X66_bit_6 -X66_bit_5 -X66_bit_4 -X66_bit_3 -X66_bit_2 -X66_bit_1 X66_bit0 -X66_bit1 -X66_bit2 -X66_bit3 -X66_bit4 -X66_bit5 -X66_bit6 -X66_bit7 -X66_bit8 -X66_bit9 -X66_bit10 -X66_bit11 -X66_bit12 -X67_bit_7 -X67_bit_6 -X67_bit_5 -X67_bit_4 -X67_bit_3 -X67_bit_2 -X67_bit_1 -X67_bit0 -X67_bit1 -X67_bit2 -X67_bit3 -X67_bit4 -X67_bit5 -X67_bit6 -X67_bit7 -X67_bit8 -X67_bit9 -X67_bit10 -X67_bit11 -X67_bit12 -X68_bit_7 -X68_bit_6 -X68_bit_5 -X68_bit_4 -X68_bit_3 -X68_bit_2 -X68_bit_1 -X68_bit0 -X68_bit1 -X68_bit2 -X68_bit3 -X68_bit4 -X68_bit5 -X68_bit6 -X68_bit7 -X68_bit8 -X68_bit9 -X68_bit10 -X68_bit11 -X68_bit12 -X69_bit_7 -X69_bit_6 -X69_bit_5 -X69_bit_4 -X69_bit_3 -X69_bit_2 -X69_bit_1 -X69_bit0 -X69_bit1 -X69_bit2 -X69_bit3 -X69_bit4 -X69_bit5 -X69_bit6 -X69_bit7 -X69_bit8 -X69_bit9 -X69_bit10 -X69_bit11 -X69_bit12 -X70_bit_7 -X70_bit_6 -X70_bit_5 -X70_bit_4 -X70_bit_3 -X70_bit_2 -X70_bit_1 -X70_bit0 -X70_bit1 -X70_bit2 -X70_bit3 -X70_bit4 -X70_bit5 -X70_bit6 -X70_bit7 -X70_bit8 -X70_bit9 -X70_bit10 -X70_bit11 -X70_bit12 -X71_bit_7 -X71_bit_6 -X71_bit_5 -X71_bit_4 -X71_bit_3 -X71_bit_2 -X71_bit_1 -X71_bit0 -X71_bit1 -X71_bit2 -X71_bit3 -X71_bit4 -X71_bit5 -X71_bit6 -X71_bit7 -X71_bit8 -X71_bit9 -X71_bit10 -X71_bit11 -X71_bit12 -X72_bit_7 -X72_bit_6 -X72_bit_5 -X72_bit_4 -X72_bit_3 -X72_bit_2 -X72_bit_1 -X72_bit0 -X72_bit1 -X72_bit2 -X72_bit3 -X72_bit4 -X72_bit5 -X72_bit6 -X72_bit7 -X72_bit8 -X72_bit9 -X72_bit10 -X72_bit11 -X72_bit12 -X73_bit_7 -X73_bit_6 -X73_bit_5 -X73_bit_4 -X73_bit_3 -X73_bit_2 -X73_bit_1 -X73_bit0 -X73_bit1 -X73_bit2 -X73_bit3 -X73_bit4 -X73_bit5 -X73_bit6 -X73_bit7 -X73_bit8 -X73_bit9 -X73_bit10 -X73_bit11 -X73_bit12 -X74_bit_7 -X74_bit_6 -X74_bit_5 -X74_bit_4 -X74_bit_3 -X74_bit_2 -X74_bit_1 -X74_bit0 -X74_bit1 -X74_bit2 -X74_bit3 -X74_bit4 -X74_bit5 -X74_bit6 -X74_bit7 -X74_bit8 -X74_bit9 -X74_bit10 -X74_bit11 -X74_bit12 -X75_bit_7 -X75_bit_6 -X75_bit_5 -X75_bit_4 -X75_bit_3 -X75_bit_2 X75_bit_1 -X75_bit0 -X75_bit1 -X75_bit2 -X75_bit3 -X75_bit4 -X75_bit5 -X75_bit6 -X75_bit7 -X75_bit8 -X75_bit9 -X75_bit10 -X75_bit11 -X75_bit12 -X76_bit_7 -X76_bit_6 -X76_bit_5 -X76_bit_4 -X76_bit_3 -X76_bit_2 -X76_bit_1 -X76_bit0 -X76_bit1 -X76_bit2 -X76_bit3 -X76_bit4 -X76_bit5 -X76_bit6 -X76_bit7 -X76_bit8 -X76_bit9 -X76_bit10 -X76_bit11 -X76_bit12 -X77_bit_7 -X77_bit_6 -X77_bit_5 -X77_bit_4 -X77_bit_3 -X77_bit_2 -X77_bit_1 -X77_bit0 -X77_bit1 -X77_bit2 -X77_bit3 -X77_bit4 -X77_bit5 -X77_bit6 -X77_bit7 -X77_bit8 -X77_bit9 -X77_bit10 -X77_bit11 -X77_bit12 -X78_bit_7 -X78_bit_6 -X78_bit_5 -X78_bit_4 -X78_bit_3 -X78_bit_2 -X78_bit_1 -X78_bit0 -X78_bit1 -X78_bit2 -X78_bit3 -X78_bit4 -X78_bit5 -X78_bit6 -X78_bit7 -X78_bit8 -X78_bit9 -X78_bit10 -X78_bit11 -X78_bit12 -X79_bit_7 -X79_bit_6 -X79_bit_5 -X79_bit_4 -X79_bit_3 -X79_bit_2 X79_bit_1 X79_bit0 X79_bit1 X79_bit2 X79_bit3 -X79_bit4 -X79_bit5 -X79_bit6 -X79_bit7 -X79_bit8 -X79_bit9 -X79_bit10 -X79_bit11 -X79_bit12 -X80_bit_7 -X80_bit_6 -X80_bit_5 -X80_bit_4 -X80_bit_3 -X80_bit_2 -X80_bit_1 -X80_bit0 -X80_bit1 -X80_bit2 -X80_bit3 -X80_bit4 -X80_bit5 -X80_bit6 -X80_bit7 -X80_bit8 -X80_bit9 -X80_bit10 -X80_bit11 -X80_bit12 -X81_bit_7 -X81_bit_6 -X81_bit_5 -X81_bit_4 -X81_bit_3 -X81_bit_2 -X81_bit_1 -X81_bit0 -X81_bit1 -X81_bit2 -X81_bit3 -X81_bit4 -X81_bit5 -X81_bit6 -X81_bit7 -X81_bit8 -X81_bit9 -X81_bit10 -X81_bit11 -X81_bit12 -X82_bit_7 -X82_bit_6 -X82_bit_5 -X82_bit_4 -X82_bit_3 -X82_bit_2 -X82_bit_1 -X82_bit0 -X82_bit1 -X82_bit2 -X82_bit3 -X82_bit4 -X82_bit5 -X82_bit6 -X82_bit7 -X82_bit8 -X82_bit9 -X82_bit10 -X82_bit11 -X82_bit12 -X83_bit_7 -X83_bit_6 -X83_bit_5 -X83_bit_4 -X83_bit_3 -X83_bit_2 -X83_bit_1 -X83_bit0 -X83_bit1 -X83_bit2 -X83_bit3 -X83_bit4 -X83_bit5 -X83_bit6 -X83_bit7 -X83_bit8 -X83_bit9 -X83_bit10 -X83_bit11 -X83_bit12 -X84_bit_7 -X84_bit_6 -X84_bit_5 -X84_bit_4 -X84_bit_3 -X84_bit_2 -X84_bit_1 -X84_bit0 -X84_bit1 -X84_bit2 -X84_bit3 -X84_bit4 -X84_bit5 -X84_bit6 -X84_bit7 -X84_bit8 -X84_bit9 -X84_bit10 -X84_bit11 -X84_bit12 -X85_bit_7 -X85_bit_6 -X85_bit_5 -X85_bit_4 -X85_bit_3 -X85_bit_2 -X85_bit_1 -X85_bit0 -X85_bit1 -X85_bit2 -X85_bit3 -X85_bit4 -X85_bit5 -X85_bit6 -X85_bit7 -X85_bit8 -X85_bit9 -X85_bit10 -X85_bit11 -X85_bit12 -X86_bit_7 -X86_bit_6 -X86_bit_5 -X86_bit_4 -X86_bit_3 -X86_bit_2 -X86_bit_1 -X86_bit0 -X86_bit1 -X86_bit2 -X86_bit3 -X86_bit4 -X86_bit5 -X86_bit6 -X86_bit7 -X86_bit8 -X86_bit9 -X86_bit10 -X86_bit11 -X86_bit12 -X87_bit_7 -X87_bit_6 -X87_bit_5 -X87_bit_4 -X87_bit_3 -X87_bit_2 -X87_bit_1 -X87_bit0 -X87_bit1 -X87_bit2 -X87_bit3 -X87_bit4 -X87_bit5 -X87_bit6 -X87_bit7 -X87_bit8 -X87_bit9 -X87_bit10 -X87_bit11 -X87_bit12 -X88_bit_7 -X88_bit_6 -X88_bit_5 -X88_bit_4 -X88_bit_3 X88_bit_2 X88_bit_1 X88_bit0 -X88_bit1 X88_bit2 -X88_bit3 -X88_bit4 -X88_bit5 -X88_bit6 -X88_bit7 -X88_bit8 -X88_bit9 -X88_bit10 -X88_bit11 -X88_bit12 -X89_bit_7 -X89_bit_6 -X89_bit_5 -X89_bit_4 -X89_bit_3 X89_bit_2 -X89_bit_1 -X89_bit0 -X89_bit1 -X89_bit2 -X89_bit3 -X89_bit4 -X89_bit5 -X89_bit6 -X89_bit7 -X89_bit8 -X89_bit9 -X89_bit10 -X89_bit11 -X89_bit12 X90_bit_7 X90_bit_6 X90_bit_5 -X90_bit_4 X90_bit_3 X90_bit_2 -X90_bit_1 X90_bit0 X90_bit1 -X90_bit2 -X90_bit3 -X90_bit4 -X90_bit5 -X90_bit6 -X90_bit7 -X90_bit8 -X90_bit9 -X90_bit10 -X90_bit11 -X90_bit12 X91_bit_7 X91_bit_6 X91_bit_5 -X91_bit_4 X91_bit_3 X91_bit_2 X91_bit_1 X91_bit0 X91_bit1 -X91_bit2 -X91_bit3 -X91_bit4 -X91_bit5 -X91_bit6 -X91_bit7 -X91_bit8 -X91_bit9 -X91_bit10 -X91_bit11 -X91_bit12 X92_bit_7 X92_bit_6 X92_bit_5 X92_bit_4 X92_bit_3 X92_bit_2 -X92_bit_1 X92_bit0 -X92_bit1 -X92_bit2 -X92_bit3 -X92_bit4 -X92_bit5 -X92_bit6 -X92_bit7 -X92_bit8 -X92_bit9 -X92_bit10 -X92_bit11 -X92_bit12 -X93_bit_7 -X93_bit_6 -X93_bit_5 -X93_bit_4 -X93_bit_3 -X93_bit_2 -X93_bit_1 -X93_bit0 -X93_bit1 -X93_bit2 -X93_bit3 -X93_bit4 -X93_bit5 -X93_bit6 -X93_bit7 -X93_bit8 -X93_bit9 -X93_bit10 -X93_bit11 -X93_bit12 X94_bit_7 X94_bit_6 X94_bit_5 -X94_bit_4 X94_bit_3 X94_bit_2 -X94_bit_1 X94_bit0 -X94_bit1 -X94_bit2 -X94_bit3 -X94_bit4 -X94_bit5 -X94_bit6 -X94_bit7 -X94_bit8 -X94_bit9 -X94_bit10 -X94_bit11 -X94_bit12 X95_bit_7 X95_bit_6 X95_bit_5 -X95_bit_4 X95_bit_3 X95_bit_2 -X95_bit_1 X95_bit0 -X95_bit1 -X95_bit2 -X95_bit3 -X95_bit4 -X95_bit5 -X95_bit6 -X95_bit7 -X95_bit8 -X95_bit9 -X95_bit10 -X95_bit11 -X95_bit12 X96_bit_7 X96_bit_6 X96_bit_5 -X96_bit_4 X96_bit_3 X96_bit_2 -X96_bit_1 X96_bit0 -X96_bit1 -X96_bit2 -X96_bit3 -X96_bit4 -X96_bit5 -X96_bit6 -X96_bit7 -X96_bit8 -X96_bit9 -X96_bit10 -X96_bit11 -X96_bit12 -X97_bit_7 -X97_bit_6 -X97_bit_5 -X97_bit_4 -X97_bit_3 -X97_bit_2 -X97_bit_1 -X97_bit0 -X97_bit1 -X97_bit2 -X97_bit3 -X97_bit4 -X97_bit5 -X97_bit6 -X97_bit7 -X97_bit8 -X97_bit9 -X97_bit10 -X97_bit11 -X97_bit12 X98_bit_7 X98_bit_6 X98_bit_5 X98_bit_4 -X98_bit_3 X98_bit_2 X98_bit_1 -X98_bit0 -X98_bit1 -X98_bit2 -X98_bit3 -X98_bit4 -X98_bit5 -X98_bit6 -X98_bit7 -X98_bit8 -X98_bit9 -X98_bit10 -X98_bit11 -X98_bit#### 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.85 0.97 0.91 2/54 21300
Raw data (stat): 21300 (runsolver) R 21299 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 541167627 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0002 s]
Raw data (loadavg): 0.87 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 4629 0 0 0 988 10 0 0 25 0 1 0 541167627 20811776 4299 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5081 4299 603 41 0 5040 0
vsize: 20324
[startup+20.0006 s]
Raw data (loadavg): 0.89 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 4877 0 0 0 1987 11 0 0 25 0 1 0 541167627 21925888 4547 4294967295 134512640 134672761 3221224544 3221223668 134566115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5353 4547 603 41 0 5312 0
vsize: 21412
[startup+30.001 s]
Raw data (loadavg): 0.91 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 5101 0 0 0 2985 12 0 0 25 0 1 0 541167627 22695936 4751 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5541 4751 603 41 0 5500 0
vsize: 22164
[startup+40.0074 s]
Raw data (loadavg): 0.92 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 5675 0 0 0 3985 12 0 0 25 0 1 0 541167627 24981504 5325 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6099 5325 603 41 0 6058 0
vsize: 24396
[startup+50.0076 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 6174 0 0 0 4985 13 0 0 25 0 1 0 541167627 27090944 5803 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6614 5803 603 41 0 6573 0
vsize: 26456
[startup+60.007 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 6540 0 0 0 5985 14 0 0 25 0 1 0 541167627 28569600 6169 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6975 6169 603 41 0 6934 0
vsize: 27900
[startup+70.0073 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 7066 0 0 0 6983 15 0 0 25 0 1 0 541167627 30699520 6695 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7495 6695 603 41 0 7454 0
vsize: 29980
[startup+80.0078 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 7307 0 0 0 7982 16 0 0 25 0 1 0 541167627 31637504 6936 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7724 6936 603 41 0 7683 0
vsize: 30896
[startup+90.0071 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 7632 0 0 0 8981 17 0 0 25 0 1 0 541167627 32985088 7261 4294967295 134512640 134672761 3221224544 3221223712 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8053 7261 603 41 0 8012 0
vsize: 32212
[startup+100.007 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 7976 0 0 0 9980 19 0 0 25 0 1 0 541167627 34328576 7605 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8381 7605 603 41 0 8340 0
vsize: 33524
[startup+110.008 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 8267 0 0 0 10979 20 0 0 25 0 1 0 541167627 35540992 7896 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8677 7896 603 41 0 8636 0
vsize: 34708
[startup+120.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 8889 0 0 0 11977 22 0 0 25 0 1 0 541167627 38100992 8518 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9302 8518 603 41 0 9261 0
vsize: 37208
[startup+130.014 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 9951 0 0 0 12975 24 0 0 25 0 1 0 541167627 42680320 9580 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10420 9580 603 41 0 10379 0
vsize: 41680
[startup+140.014 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 10411 0 0 0 13974 26 0 0 25 0 1 0 541167627 44568576 10040 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10881 10040 603 41 0 10840 0
vsize: 43524
[startup+150.014 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 10716 0 0 0 14973 27 0 0 25 0 1 0 541167627 45768704 10345 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11174 10345 603 41 0 11133 0
vsize: 44696
[startup+160.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 11116 0 0 0 15972 28 0 0 25 0 1 0 541167627 47386624 10745 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11569 10745 603 41 0 11528 0
vsize: 46276
[startup+170.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 11428 0 0 0 16972 29 0 0 25 0 1 0 541167627 48644096 11057 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11876 11057 603 41 0 11835 0
vsize: 47504
[startup+180.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 11753 0 0 0 17970 30 0 0 25 0 1 0 541167627 49991680 11382 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12205 11382 603 41 0 12164 0
vsize: 48820
[startup+190.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 12016 0 0 0 18970 31 0 0 25 0 1 0 541167627 51068928 11645 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12468 11645 603 41 0 12427 0
vsize: 49872
[startup+200.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 12317 0 0 0 19969 32 0 0 25 0 1 0 541167627 52277248 11946 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12763 11946 603 41 0 12722 0
vsize: 51052
[startup+210.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 12599 0 0 0 20969 32 0 0 25 0 1 0 541167627 53354496 12228 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13026 12228 603 41 0 12985 0
vsize: 52104
[startup+220.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 12889 0 0 0 21968 33 0 0 25 0 1 0 541167627 54571008 12518 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13323 12518 603 41 0 13282 0
vsize: 53292
[startup+230.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 13096 0 0 0 22968 33 0 0 25 0 1 0 541167627 55377920 12725 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13520 12725 603 41 0 13479 0
vsize: 54080
[startup+240.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 13313 0 0 0 23967 34 0 0 25 0 1 0 541167627 56324096 12942 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13751 12942 603 41 0 13710 0
vsize: 55004
[startup+250.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 13624 0 0 0 24967 35 0 0 25 0 1 0 541167627 57528320 13253 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14045 13253 603 41 0 14004 0
vsize: 56180
[startup+260.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 14150 0 0 0 25965 37 0 0 25 0 1 0 541167627 59691008 13779 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14573 13779 603 41 0 14532 0
vsize: 58292
[startup+270.014 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 14736 0 0 0 26965 38 0 0 25 0 1 0 541167627 62107648 14365 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15163 14365 603 41 0 15122 0
vsize: 60652
[startup+280.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 14928 0 0 0 27964 38 0 0 25 0 1 0 541167627 62918656 14557 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15361 14557 603 41 0 15320 0
vsize: 61444
[startup+290.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 15120 0 0 0 28964 38 0 0 25 0 1 0 541167627 63590400 14749 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15525 14749 603 41 0 15484 0
vsize: 62100
[startup+300.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 15350 0 0 0 29964 39 0 0 25 0 1 0 541167627 65060864 14979 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15884 14979 603 41 0 15843 0
vsize: 63536
[startup+310.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 15708 0 0 0 30964 39 0 0 25 0 1 0 541167627 66543616 15337 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16246 15337 603 41 0 16205 0
vsize: 64984
[startup+320.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 16073 0 0 0 31963 40 0 0 25 0 1 0 541167627 68018176 15702 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16606 15702 603 41 0 16565 0
vsize: 66424
[startup+330.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 16367 0 0 0 32961 42 0 0 25 0 1 0 541167627 69226496 15996 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16901 15996 603 41 0 16860 0
vsize: 67604
[startup+340.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 16605 0 0 0 33961 43 0 0 25 0 1 0 541167627 70160384 16234 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17129 16234 603 41 0 17088 0
vsize: 68516
[startup+350.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 16833 0 0 0 34960 44 0 0 25 0 1 0 541167627 71094272 16462 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17357 16462 603 41 0 17316 0
vsize: 69428
[startup+360.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 17461 0 0 0 35959 45 0 0 25 0 1 0 541167627 73650176 17090 4294967295 134512640 134672761 3221224544 3221223728 134559365 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17981 17090 603 41 0 17940 0
vsize: 71924
[startup+370.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 18216 0 0 0 36957 47 0 0 25 0 1 0 541167627 76746752 17845 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18737 17845 603 41 0 18696 0
vsize: 74948
[startup+380.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 18875 0 0 0 37956 49 0 0 25 0 1 0 541167627 79409152 18504 4294967295 134512640 134672761 3221224544 3221223732 1075346949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19387 18504 603 41 0 19346 0
vsize: 77548
[startup+390.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 19487 0 0 0 38954 50 0 0 25 0 1 0 541167627 81907712 19116 4294967295 134512640 134672761 3221224544 3221223648 134560344 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19997 19116 603 41 0 19956 0
vsize: 79988
[startup+400.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 20146 0 0 0 39953 52 0 0 25 0 1 0 541167627 84721664 19775 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20684 19775 603 41 0 20643 0
vsize: 82736
[startup+410.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 20774 0 0 0 40951 53 0 0 25 0 1 0 541167627 87273472 20403 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21307 20403 603 41 0 21266 0
vsize: 85228
[startup+420.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 21425 0 0 0 41950 55 0 0 25 0 1 0 541167627 89935872 21054 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21957 21054 603 41 0 21916 0
vsize: 87828
[startup+430.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 22011 0 0 0 42949 56 0 0 25 0 1 0 541167627 92315648 21640 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22538 21640 603 41 0 22497 0
vsize: 90152
[startup+440.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 22616 0 0 0 43947 58 0 0 25 0 1 0 541167627 94810112 22245 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23147 22245 603 41 0 23106 0
vsize: 92588
[startup+450.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 23228 0 0 0 44946 60 0 0 25 0 1 0 541167627 97316864 22857 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23759 22857 603 41 0 23718 0
vsize: 95036
[startup+460.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 23810 0 0 0 45945 61 0 0 25 0 1 0 541167627 99631104 23439 4294967295 134512640 134672761 3221224544 3221223560 1075353266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24324 23439 603 41 0 24283 0
vsize: 97296
[startup+470.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 24311 0 0 0 46944 62 0 0 25 0 1 0 541167627 101715968 23940 4294967295 134512640 134672761 3221224544 3221223648 134559953 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24833 23940 603 41 0 24792 0
vsize: 99332
[startup+480.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 24848 0 0 0 47943 63 0 0 25 0 1 0 541167627 103923712 24477 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25372 24477 603 41 0 25331 0
vsize: 101488
[startup+490.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25354 0 0 0 48942 64 0 0 25 0 1 0 541167627 105984000 24983 4294967295 134512640 134672761 3221224544 3221223648 134554910 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25875 24983 603 41 0 25834 0
vsize: 103500
[startup+500.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25785 0 0 0 49941 66 0 0 25 0 1 0 541167627 107696128 25414 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26293 25414 603 41 0 26252 0
vsize: 105172
[startup+510.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25943 0 0 0 50940 66 0 0 25 0 1 0 541167627 108376064 25572 4294967295 134512640 134672761 3221224544 3221223680 134556454 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25572 603 41 0 26418 0
vsize: 105836
[startup+520.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25943 0 0 0 51940 66 0 0 25 0 1 0 541167627 108376064 25572 4294967295 134512640 134672761 3221224544 3221223648 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25572 603 41 0 26418 0
vsize: 105836
[startup+530.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25943 0 0 0 52940 66 0 0 25 0 1 0 541167627 108376064 25572 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25572 603 41 0 26418 0
vsize: 105836
[startup+540.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25943 0 0 0 53940 66 0 0 25 0 1 0 541167627 108376064 25572 4294967295 134512640 134672761 3221224544 3221223648 134560136 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25572 603 41 0 26418 0
vsize: 105836
[startup+550.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25943 0 0 0 54940 66 0 0 25 0 1 0 541167627 108376064 25572 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25572 603 41 0 26418 0
vsize: 105836
[startup+560.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25943 0 0 0 55941 66 0 0 25 0 1 0 541167627 108376064 25572 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25572 603 41 0 26418 0
vsize: 105836
[startup+570.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25943 0 0 0 56941 66 0 0 25 0 1 0 541167627 108376064 25572 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25572 603 41 0 26418 0
vsize: 105836
[startup+580.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25943 0 0 0 57941 66 0 0 25 0 1 0 541167627 108376064 25572 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25572 603 41 0 26418 0
vsize: 105836
[startup+590.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25945 0 0 0 58941 66 0 0 25 0 1 0 541167627 108376064 25574 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25574 603 41 0 26418 0
vsize: 105836
[startup+600.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25946 0 0 0 59941 67 0 0 25 0 1 0 541167627 108376064 25575 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25575 603 41 0 26418 0
vsize: 105836
[startup+610.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25946 0 0 0 60941 67 0 0 25 0 1 0 541167627 108376064 25575 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25575 603 41 0 26418 0
vsize: 105836
[startup+620.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25946 0 0 0 61942 67 0 0 25 0 1 0 541167627 108376064 25575 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25575 603 41 0 26418 0
vsize: 105836
[startup+630.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25946 0 0 0 62942 67 0 0 25 0 1 0 541167627 108376064 25575 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25575 603 41 0 26418 0
vsize: 105836
[startup+640.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25946 0 0 0 63942 67 0 0 25 0 1 0 541167627 108376064 25575 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25575 603 41 0 26418 0
vsize: 105836
[startup+650.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25946 0 0 0 64942 67 0 0 25 0 1 0 541167627 108376064 25575 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25575 603 41 0 26418 0
vsize: 105836
[startup+660.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25947 0 0 0 65942 67 0 0 25 0 1 0 541167627 108376064 25576 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25576 603 41 0 26418 0
vsize: 105836
[startup+670.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25947 0 0 0 66942 67 0 0 25 0 1 0 541167627 108376064 25576 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25576 603 41 0 26418 0
vsize: 105836
[startup+680.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25947 0 0 0 67942 67 0 0 25 0 1 0 541167627 108376064 25576 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25576 603 41 0 26418 0
vsize: 105836
[startup+690.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25947 0 0 0 68943 67 0 0 25 0 1 0 541167627 108376064 25576 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25576 603 41 0 26418 0
vsize: 105836
[startup+700.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25948 0 0 0 69943 67 0 0 25 0 1 0 541167627 108376064 25577 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25577 603 41 0 26418 0
vsize: 105836
[startup+710.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25948 0 0 0 70943 67 0 0 25 0 1 0 541167627 108376064 25577 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25577 603 41 0 26418 0
vsize: 105836
[startup+720.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25948 0 0 0 71943 67 0 0 25 0 1 0 541167627 108376064 25577 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25577 603 41 0 26418 0
vsize: 105836
[startup+730.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25949 0 0 0 72943 67 0 0 25 0 1 0 541167627 108376064 25578 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25578 603 41 0 26418 0
vsize: 105836
[startup+740.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25949 0 0 0 73943 67 0 0 25 0 1 0 541167627 108376064 25578 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25578 603 41 0 26418 0
vsize: 105836
[startup+750.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25949 0 0 0 74944 67 0 0 25 0 1 0 541167627 108376064 25578 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25578 603 41 0 26418 0
vsize: 105836
[startup+760.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25949 0 0 0 75944 67 0 0 25 0 1 0 541167627 108376064 25578 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25578 603 41 0 26418 0
vsize: 105836
[startup+770.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25949 0 0 0 76944 67 0 0 25 0 1 0 541167627 108376064 25578 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25578 603 41 0 26418 0
vsize: 105836
[startup+780.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25949 0 0 0 77944 67 0 0 25 0 1 0 541167627 108376064 25578 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25578 603 41 0 26418 0
vsize: 105836
[startup+790.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25949 0 0 0 78944 67 0 0 25 0 1 0 541167627 108376064 25578 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25578 603 41 0 26418 0
vsize: 105836
[startup+800.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25950 0 0 0 79945 67 0 0 25 0 1 0 541167627 108376064 25579 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25579 603 41 0 26418 0
vsize: 105836
[startup+810.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25950 0 0 0 80945 67 0 0 25 0 1 0 541167627 108376064 25579 4294967295 134512640 134672761 3221224544 3221223648 134560022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25579 603 41 0 26418 0
vsize: 105836
[startup+820.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25950 0 0 0 81945 67 0 0 25 0 1 0 541167627 108376064 25579 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25579 603 41 0 26418 0
vsize: 105836
[startup+830.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25951 0 0 0 82945 67 0 0 25 0 1 0 541167627 108376064 25580 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25580 603 41 0 26418 0
vsize: 105836
[startup+840.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25951 0 0 0 83945 67 0 0 25 0 1 0 541167627 108376064 25580 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25580 603 41 0 26418 0
vsize: 105836
[startup+850.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25952 0 0 0 84945 67 0 0 25 0 1 0 541167627 108376064 25581 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25581 603 41 0 26418 0
vsize: 105836
[startup+860.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25952 0 0 0 85946 67 0 0 25 0 1 0 541167627 108376064 25581 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25581 603 41 0 26418 0
vsize: 105836
[startup+870.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25953 0 0 0 86946 67 0 0 25 0 1 0 541167627 108376064 25582 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25582 603 41 0 26418 0
vsize: 105836
[startup+880.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25953 0 0 0 87946 67 0 0 25 0 1 0 541167627 108376064 25582 4294967295 134512640 134672761 3221224544 3221223744 134557820 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25582 603 41 0 26418 0
vsize: 105836
[startup+890.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25953 0 0 0 88946 67 0 0 25 0 1 0 541167627 108376064 25582 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25582 603 41 0 26418 0
vsize: 105836
[startup+900.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25953 0 0 0 89946 67 0 0 25 0 1 0 541167627 108376064 25582 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25582 603 41 0 26418 0
vsize: 105836
[startup+910.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25953 0 0 0 90946 67 0 0 25 0 1 0 541167627 108376064 25582 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25582 603 41 0 26418 0
vsize: 105836
[startup+920.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25953 0 0 0 91947 67 0 0 25 0 1 0 541167627 108376064 25582 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25582 603 41 0 26418 0
vsize: 105836
[startup+930.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25953 0 0 0 92947 67 0 0 25 0 1 0 541167627 108376064 25582 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25582 603 41 0 26418 0
vsize: 105836
[startup+940.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25953 0 0 0 93947 67 0 0 25 0 1 0 541167627 108376064 25582 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25582 603 41 0 26418 0
vsize: 105836
[startup+950.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25954 0 0 0 94947 67 0 0 25 0 1 0 541167627 108376064 25583 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25583 603 41 0 26418 0
vsize: 105836
[startup+960.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25955 0 0 0 95947 67 0 0 25 0 1 0 541167627 108376064 25584 4294967295 134512640 134672761 3221224544 3221223728 134558851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25584 603 41 0 26418 0
vsize: 105836
[startup+970.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25957 0 0 0 96948 67 0 0 25 0 1 0 541167627 108376064 25586 4294967295 134512640 134672761 3221224544 3221223728 134558930 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25586 603 41 0 26418 0
vsize: 105836
[startup+980.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25959 0 0 0 97948 67 0 0 25 0 1 0 541167627 108376064 25588 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25588 603 41 0 26418 0
vsize: 105836
[startup+990.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 25961 0 0 0 98948 67 0 0 25 0 1 0 541167627 108376064 25590 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26459 25590 603 41 0 26418 0
vsize: 105836
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 26139 0 0 0 99947 68 0 0 25 0 1 0 541167627 109051904 25768 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26624 25768 603 41 0 26583 0
vsize: 106496
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 26749 0 0 0 100946 70 0 0 25 0 1 0 541167627 111599616 26378 4294967295 134512640 134672761 3221224544 3221223704 134561240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27246 26378 603 41 0 27205 0
vsize: 108984
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 27285 0 0 0 101944 72 0 0 25 0 1 0 541167627 113729536 26914 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27766 26914 603 41 0 27725 0
vsize: 111064
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 27807 0 0 0 102942 74 0 0 25 0 1 0 541167627 115855360 27436 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28285 27436 603 41 0 28244 0
vsize: 113140
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 28282 0 0 0 103940 75 0 0 25 0 1 0 541167627 117829632 27911 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28767 27911 603 41 0 28726 0
vsize: 115068
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 28591 0 0 0 104940 76 0 0 25 0 1 0 541167627 119226368 28220 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29108 28220 603 41 0 29067 0
vsize: 116432
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 28692 0 0 0 105939 76 0 0 25 0 1 0 541167627 119549952 28321 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29187 28321 603 41 0 29146 0
vsize: 116748
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 28846 0 0 0 106937 78 0 0 25 0 1 0 541167627 120233984 28475 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29354 28475 603 41 0 29313 0
vsize: 117416
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 29055 0 0 0 107937 78 0 0 25 0 1 0 541167627 121036800 28684 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29550 28684 603 41 0 29509 0
vsize: 118200
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 29190 0 0 0 108936 79 0 0 25 0 1 0 541167627 121712640 28819 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29715 28819 603 41 0 29674 0
vsize: 118860
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 29323 0 0 0 109936 79 0 0 25 0 1 0 541167627 122249216 28952 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29846 28952 603 41 0 29805 0
vsize: 119384
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 29465 0 0 0 110936 80 0 0 25 0 1 0 541167627 122789888 29094 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29978 29094 603 41 0 29937 0
vsize: 119912
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 29639 0 0 0 111935 80 0 0 25 0 1 0 541167627 123453440 29268 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30140 29268 603 41 0 30099 0
vsize: 120560
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 29835 0 0 0 112935 81 0 0 25 0 1 0 541167627 124256256 29464 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30336 29464 603 41 0 30295 0
vsize: 121344
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 30023 0 0 0 113935 81 0 0 25 0 1 0 541167627 125059072 29652 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30532 29652 603 41 0 30491 0
vsize: 122128
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 30242 0 0 0 114935 82 0 0 25 0 1 0 541167627 125984768 29871 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30758 29871 603 41 0 30717 0
vsize: 123032
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 30482 0 0 0 115934 82 0 0 25 0 1 0 541167627 126922752 30111 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30987 30111 603 41 0 30946 0
vsize: 123948
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 30701 0 0 0 116934 83 0 0 25 0 1 0 541167627 127864832 30330 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31217 30330 603 41 0 31176 0
vsize: 124868
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 30918 0 0 0 117934 83 0 0 25 0 1 0 541167627 128667648 30547 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31413 30547 603 41 0 31372 0
vsize: 125652
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 30935 0 0 0 118934 83 0 0 25 0 1 0 541167627 128802816 30564 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31446 30564 603 41 0 31405 0
vsize: 125784
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21300
Raw data (stat): 21300 (minisat+) R 21299 22612 22611 0 -1 0 30935 0 0 0 119934 83 0 0 25 0 1 0 541167627 128802816 30564 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31446 30564 603 41 0 31405 0
vsize: 125784
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 21300
Raw data (stat): 21300 (minisat+) Z 21299 22612 22611 0 -1 12 30938 0 0 0 119934 89 0 0 25 0 1 0 541167627 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.09
CPU time (s): 1200.25
CPU user time (s): 1199.35
CPU system time (s): 0.898863
CPU usage (%): 100.013
Max. virtual memory (Kb): 125784
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####