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-10teams.opb
MD5SUM	130bea0863cb3f92addf09aabe15daa3
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	920
Optimality of the best value was proved	NO
Number of terms in the objective function	1800
Biggest coefficient in the objective function	86
Number of bits for the biggest coefficient in the objective function	7
Sum of the numbers in the objective function	41700
Number of bits of the sum of numbers in the objective function	16
Biggest number in a constraint	86
Number of bits of the biggest number in a constraint	7
Biggest sum of numbers in a constraint	41700
Number of bits of the biggest sum of numbers	16
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.54
Number of variables	1800
Total number of constraints	2015
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	2015
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	72
Trace number 21476

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-04-21 23:59:24 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13148 boxname=wulflinc15 idbench=1012 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  130bea0863cb3f92addf09aabe15daa3  /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-20-10-10teams.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-20-10-10teams.opb
IDLAUNCH: 13148
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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	: 2
cpu MHz		: 450.999
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:        220816 kB
Buffers:         30740 kB
Cached:         760960 kB
SwapCached:        432 kB
Active:         164984 kB
Inactive:       628884 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        220564 kB
SwapTotal:     2097136 kB
SwapFree:      2095984 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5364 kB
Slab:            14192 kB
Committed_AS:    63560 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 00:19:27 (client local time) WITH STATUS 10 IN 1200.41 SECONDS
stats: 13148 7 1200.41 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 330 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 328]---> BDD-cost:   77
c ---[ 326]---> BDD-cost:   77
c ---[ 324]---> BDD-cost:   77
c ---[ 322]---> BDD-cost:   77
c ---[ 320]---> BDD-cost:   77
c ---[ 318]---> BDD-cost:   77
c ---[ 316]---> BDD-cost:   77
c ---[ 314]---> BDD-cost:   77
c ---[ 312]---> BDD-cost:   77
c ---[ 310]---> BDD-cost:   77
c ---[ 308]---> BDD-cost:   77
c ---[ 306]---> BDD-cost:   77
c ---[ 304]---> BDD-cost:   77
c ---[ 302]---> BDD-cost:   77
c ---[ 300]---> BDD-cost:   77
c ---[ 298]---> BDD-cost:   77
c ---[ 296]---> BDD-cost:   77
c ---[ 294]---> BDD-cost:   77
c ---[ 292]---> BDD-cost:   77
c ---[ 290]---> BDD-cost:   77
c ---[ 288]---> BDD-cost:   77
c ---[ 286]---> BDD-cost:   77
c ---[ 284]---> BDD-cost:   77
c ---[ 282]---> BDD-cost:   77
c ---[ 280]---> BDD-cost:   77
c ---[ 278]---> BDD-cost:   77
c ---[ 276]---> BDD-cost:   77
c ---[ 274]---> BDD-cost:   77
c ---[ 272]---> BDD-cost:   77
c ---[ 270]---> BDD-cost:   77
c ---[ 268]---> BDD-cost:   77
c ---[ 266]---> BDD-cost:   77
c ---[ 264]---> BDD-cost:   77
c ---[ 262]---> BDD-cost:   77
c ---[ 260]---> BDD-cost:   77
c ---[ 258]---> BDD-cost:   77
c ---[ 256]---> BDD-cost:   77
c ---[ 254]---> BDD-cost:   77
c ---[ 252]---> BDD-cost:   77
c ---[ 250]---> BDD-cost:   77
c ---[ 249]---> BDD-cost:  125
c ---[ 248]---> BDD-cost:  185
c ---[ 247]---> BDD-cost:  185
c ---[ 246]---> BDD-cost:  185
c ---[ 245]---> BDD-cost:  185
c ---[ 244]---> BDD-cost:  185
c ---[ 243]---> BDD-cost:  125
c ---[ 242]---> BDD-cost:  185
c ---[ 241]---> BDD-cost:  185
c ---[ 240]---> BDD-cost:  185
c ---[ 239]---> BDD-cost:  185
c ---[ 238]---> BDD-cost:  125
c ---[ 237]---> BDD-cost:  185
c ---[ 236]---> BDD-cost:  185
c ---[ 235]---> BDD-cost:  185
c ---[ 234]---> BDD-cost:  185
c ---[ 233]---> BDD-cost:  185
c ---[ 232]---> BDD-cost:  125
c ---[ 231]---> BDD-cost:  185
c ---[ 230]---> BDD-cost:  185
c ---[ 229]---> BDD-cost:  185
c ---[ 228]---> BDD-cost:  185
c ---[ 227]---> BDD-cost:  125
c ---[ 226]---> BDD-cost:  185
c ---[ 225]---> BDD-cost:  185
c ---[ 224]---> BDD-cost:  185
c ---[ 223]---> BDD-cost:  185
c ---[ 222]---> BDD-cost:  185
c ---[ 221]---> BDD-cost:  125
c ---[ 220]---> BDD-cost:  185
c ---[ 219]---> BDD-cost:  185
c ---[ 218]---> BDD-cost:  185
c ---[ 217]---> BDD-cost:  185
c ---[ 216]---> BDD-cost:  125
c ---[ 215]---> BDD-cost:  185
c ---[ 214]---> BDD-cost:  185
c ---[ 213]---> BDD-cost:  185
c ---[ 212]---> BDD-cost:  185
c ---[ 211]---> BDD-cost:  185
c ---[ 210]---> BDD-cost:  125
c ---[ 209]---> BDD-cost:  125
c ---[ 208]---> BDD-cost:  185
c ---[ 207]---> BDD-cost:  185
c ---[ 206]---> BDD-cost:  185
c ---[ 205]---> BDD-cost:  185
c ---[ 204]---> BDD-cost:  185
c ---[ 203]---> BDD-cost:  185
c ---[ 202]---> BDD-cost:  185
c ---[ 201]---> BDD-cost:  185
c ---[ 200]---> BDD-cost:  125
c ---[ 199]---> BDD-cost:   75
c ---[ 198]---> BDD-cost:   77
c ---[ 197]---> BDD-cost:   77
c ---[ 196]---> BDD-cost:   77
c ---[ 195]---> BDD-cost:   77
c ---[ 194]---> BDD-cost:   77
c ---[ 193]---> BDD-cost:   77
c ---[ 192]---> BDD-cost:   77
c ---[ 191]---> BDD-cost:   75
c ---[ 190]---> BDD-cost:   77
c ---[ 189]---> BDD-cost:   77
c ---[ 188]---> BDD-cost:   77
c ---[ 187]---> BDD-cost:   77
c ---[ 186]---> BDD-cost:   77
c ---[ 185]---> BDD-cost:   77
c ---[ 184]---> BDD-cost:   77
c ---[ 183]---> BDD-cost:   75
c ---[ 182]---> BDD-cost:   77
c ---[ 181]---> BDD-cost:   77
c ---[ 180]---> BDD-cost:   77
c ---[ 179]---> BDD-cost:   77
c ---[ 178]---> BDD-cost:   77
c ---[ 177]---> BDD-cost:   77
c ---[ 176]---> BDD-cost:   77
c ---[ 175]---> BDD-cost:   75
c ---[ 174]---> BDD-cost:   77
c ---[ 173]---> BDD-cost:   77
c ---[ 172]---> BDD-cost:   77
c ---[ 171]---> BDD-cost:   77
c ---[ 170]---> BDD-cost:   77
c ---[ 169]---> BDD-cost:   77
c ---[ 168]---> BDD-cost:   77
c ---[ 167]---> BDD-cost:   75
c ---[ 166]---> BDD-cost:   77
c ---[ 165]---> BDD-cost:   77
c ---[ 164]---> BDD-cost:   77
c ---[ 163]---> BDD-cost:   77
c ---[ 162]---> BDD-cost:   77
c ---[ 161]---> BDD-cost:   77
c ---[ 160]---> BDD-cost:   77
c ---[ 158]---> BDD-cost:   70
c ---[ 156]---> BDD-cost:   77
c ---[ 154]---> BDD-cost:   77
c ---[ 152]---> BDD-cost:   77
c ---[ 150]---> BDD-cost:   77
c ---[ 148]---> BDD-cost:   77
c ---[ 146]---> BDD-cost:   77
c ---[ 144]---> BDD-cost:   77
c ---[ 142]---> BDD-cost:   70
c ---[ 140]---> BDD-cost:   76
c ---[ 138]---> BDD-cost:   76
c ---[ 136]---> BDD-cost:   76
c ---[ 134]---> BDD-cost:   76
c ---[ 132]---> BDD-cost:   76
c ---[ 130]---> BDD-cost:   76
c ---[ 128]---> BDD-cost:   76
c ---[ 126]---> BDD-cost:   70
c ---[ 124]---> BDD-cost:   77
c ---[ 122]---> BDD-cost:   77
c ---[ 120]---> BDD-cost:   77
c ---[ 118]---> BDD-cost:   77
c ---[ 116]---> BDD-cost:   77
c ---[ 114]---> BDD-cost:   77
c ---[ 112]---> BDD-cost:   77
c ---[ 110]---> BDD-cost:   70
c ---[ 108]---> BDD-cost:   77
c ---[ 106]---> BDD-cost:   77
c ---[ 104]---> BDD-cost:   77
c ---[ 102]---> BDD-cost:   77
c ---[ 100]---> BDD-cost:   77
c ---[  98]---> BDD-cost:   77
c ---[  96]---> BDD-cost:   77
c ---[  94]---> BDD-cost:   70
c ---[  92]---> BDD-cost:   77
c ---[  90]---> BDD-cost:   77
c ---[  88]---> BDD-cost:   77
c ---[  86]---> BDD-cost:   77
c ---[  84]---> BDD-cost:   77
c ---[  82]---> BDD-cost:   77
c ---[  80]---> BDD-cost:   77
c ---[  78]---> BDD-cost:   70
c ---[  76]---> BDD-cost:   77
c ---[  74]---> BDD-cost:   77
c ---[  72]---> BDD-cost:   77
c ---[  70]---> BDD-cost:   77
c ---[  68]---> BDD-cost:   77
c ---[  66]---> BDD-cost:   77
c ---[  64]---> BDD-cost:   77
c ---[  62]---> BDD-cost:   70
c ---[  60]---> BDD-cost:   77
c ---[  58]---> BDD-cost:   77
c ---[  56]---> BDD-cost:   77
c ---[  54]---> BDD-cost:   77
c ---[  52]---> BDD-cost:   77
c ---[  50]---> BDD-cost:   77
c ---[  48]---> BDD-cost:   77
c ---[  46]---> BDD-cost:   70
c ---[  44]---> BDD-cost:   77
c ---[  42]---> BDD-cost:   77
c ---[  40]---> BDD-cost:   77
c ---[  38]---> BDD-cost:   77
c ---[  36]---> BDD-cost:   77
c ---[  34]---> BDD-cost:   77
c ---[  32]---> BDD-cost:   77
c ---[  30]---> BDD-cost:   70
c ---[  28]---> BDD-cost:   77
c ---[  26]---> BDD-cost:   77
c ---[  24]---> BDD-cost:   77
c ---[  22]---> BDD-cost:   77
c ---[  20]---> BDD-cost:   77
c ---[  18]---> BDD-cost:   77
c ---[  16]---> BDD-cost:   77
c ---[  14]---> BDD-cost:   70
c ---[  12]---> BDD-cost:   77
c ---[  10]---> BDD-cost:   77
c ---[   8]---> BDD-cost:   77
c ---[   6]---> BDD-cost:   77
c ---[   4]---> BDD-cost:   77
c ---[   2]---> BDD-cost:   77
c ---[   0]---> BDD-cost:   77
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   53221   141547 |   17740       0        0     nan |  0.000 % |
c |       100 |   53221   141547 |   19514     100      818     8.2 |  1.808 % |
c |       250 |   53221   141547 |   21465     250    15400    61.6 |  1.808 % |
c |       475 |   53221   141547 |   23611     475    28793    60.6 |  1.808 % |
c |       812 |   53221   141547 |   25973     812    62995    77.6 |  1.808 % |
c |      1318 |   53221   141547 |   28570    1318   139369   105.7 |  1.808 % |
c |      2077 |   53221   141547 |   31427    2077   324252   156.1 |  1.808 % |
c |      3216 |   53221   141547 |   34570    3216   511801   159.1 |  1.808 % |
c ==============================================================================
c [1mFound solution: 968[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 7750   maxlim: 39032   bits: 16/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4874 |  107351   334867 |   35783    4874   723583   148.5 |  1.808 % |
c |      4974 |  107351   334867 |   39361    4974   725539   145.9 |  1.399 % |
c |      5125 |  107351   334867 |   43297    5125   734785   143.4 |  1.399 % |
c |      5350 |  107351   334867 |   47627    5350   757972   141.7 |  1.399 % |
c |      5687 |  107351   334867 |   52389    5687   805904   141.7 |  1.399 % |
c |      6194 |  107351   334867 |   57628    6194   880515   142.2 |  1.399 % |
c |      6954 |  107351   334867 |   63391    6954   975482   140.3 |  1.399 % |
c |      8095 |  107351   334867 |   69730    8095  1140642   140.9 |  1.399 % |
c |      9805 |  107351   334867 |   76704    9805  1611033   164.3 |  1.399 % |
c |     12371 |  107351   334867 |   84374   12371  2352458   190.2 |  1.399 % |
c ==============================================================================
c [1mFound solution: 962[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 39038   bits: 16/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14541 |  107358   334912 |   35786   14541  2732241   187.9 |  1.399 % |
c |     14642 |  107358   334912 |   39364   14642  2734861   186.8 |  1.409 % |
c |     14794 |  107358   334912 |   43301   14794  2754967   186.2 |  1.409 % |
c |     15020 |  107358   334912 |   47631   15020  2763373   184.0 |  1.409 % |
c |     15357 |  107358   334912 |   52394   15357  2798874   182.3 |  1.409 % |
c |     15864 |  107358   334912 |   57633   15864  2845711   179.4 |  1.409 % |
c |     16623 |  107358   334912 |   63397   16623  2939938   176.9 |  1.409 % |
c |     17762 |  107358   334912 |   69736   17762  3170459   178.5 |  1.409 % |
c |     19470 |  107358   334912 |   76710   19470  3736178   191.9 |  1.409 % |
c |     22034 |  107358   334912 |   84381   22034  4404757   199.9 |  1.409 % |
c |     25881 |  107358   334912 |   92819   25881  5484850   211.9 |  1.409 % |
c |     31647 |  107358   334912 |  102101   31647  7222673   228.2 |  1.409 % |
c |     40297 |  107358   334912 |  112311   40297  9703101   240.8 |  1.409 % |
c |     53271 |  107358   334912 |  123542   53271 13645727   256.2 |  1.409 % |
c |     72733 |  107358   334912 |  135897   72733 21970585   302.1 |  1.409 % |
c |    101925 |  107350   334882 |  149487  101924 33904393   332.6 |  1.412 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x10212_bit0 -x10312_bit0 -x20312_bit0 -x10412_bit0 -x20412_bit0 -x30412_bit0 -x10512_bit0 -x20512_bit0 -x30512_bit0 -x40512_bit0 x10612_bit0 -x20612_bit0 -x30612_bit0 -x40612_bit0 -x50612_bit0 -x10712_bit0 -x20712_bit0 -x30712_bit0 -x40712_bit0 -x50712_bit0 -x60712_bit0 -x10812_bit0 -x20812_bit0 -x30812_bit0 -x40812_bit0 -x50812_bit0 -x60812_bit0 -x70812_bit0 -x10912_bit0 -x20912_bit0 -x30912_bit0 -x40912_bit0 -x50912_bit0 -x60912_bit0 -x70912_bit0 -x80912_bit0 -x11012_bit0 -x21012_bit0 -x31012_bit0 -x41012_bit0 -x51012_bit0 -x61012_bit0 -x71012_bit0 -x81012_bit0 -x91012_bit0 -x10222_bit0 -x10322_bit0 -x20322_bit0 -x10422_bit0 -x20422_bit0 -x30422_bit0 -x10522_bit0 -x20522_bit0 -x30522_bit0 -x40522_bit0 -x10622_bit0 -x20622_bit0 -x30622_bit0 -x40622_bit0 -x50622_bit0 -x10722_bit0 -x20722_bit0 -x30722_bit0 -x40722_bit0 -x50722_bit0 -x60722_bit0 -x10822_bit0 -x20822_bit0 -x30822_bit0 -x40822_bit0 -x50822_bit0 -x60822_bit0 -x70822_bit0 -x10922_bit0 -x20922_bit0 -x30922_bit0 -x40922_bit0 -x50922_bit0 -x60922_bit0 -x70922_bit0 -x80922_bit0 -x11022_bit0 -x21022_bit0 -x31022_bit0 -x41022_bit0 x51022_bit0 -x61022_bit0 -x71022_bit0 -x81022_bit0 -x91022_bit0 -x10232_bit0 -x10332_bit0 -x20332_bit0 -x10432_bit0 -x20432_bit0 -x30432_bit0 -x10532_bit0 -x20532_bit0 -x30532_bit0 -x40532_bit0 -x10632_bit0 -x20632_bit0 -x30632_bit0 -x40632_bit0 -x50632_bit0 -x10732_bit0 -x20732_bit0 x30732_bit0 -x40732_bit0 -x50732_bit0 -x60732_bit0 -x10832_bit0 -x20832_bit0 -x30832_bit0 -x40832_bit0 -x50832_bit0 -x60832_bit0 -x70832_bit0 -x10932_bit0 -x20932_bit0 -x30932_bit0 -x40932_bit0 -x50932_bit0 -x60932_bit0 -x70932_bit0 -x80932_bit0 -x11032_bit0 -x21032_bit0 -x31032_bit0 -x41032_bit0 -x51032_bit0 -x61032_bit0 -x71032_bit0 -x81032_bit0 -x91032_bit0 -x10242_bit0 -x10342_bit0 -x20342_bit0 -x10442_bit0 -x20442_bit0 -x30442_bit0 -x10542_bit0 -x20542_bit0 -x30542_bit0 -x40542_bit0 -x10642_bit0 -x20642_bit0 -x30642_bit0 -x40642_bit0 -x50642_bit0 -x10742_bit0 -x20742_bit0 -x30742_bit0 -x40742_bit0 -x50742_bit0 -x60742_bit0 -x10842_bit0 -x20842_bit0 -x30842_bit0 -x40842_bit0 -x50842_bit0 -x60842_bit0 -x70842_bit0 -x10942_bit0 x20942_bit0 -x30942_bit0 -x40942_bit0 -x50942_bit0 -x60942_bit0 -x70942_bit0 -x80942_bit0 -x11042_bit0 -x21042_bit0 -x31042_bit0 -x41042_bit0 -x51042_bit0 -x61042_bit0 -x71042_bit0 -x81042_bit0 -x91042_bit0 -x10252_bit0 -x10352_bit0 -x20352_bit0 -x10452_bit0 -x20452_bit0 -x30452_bit0 -x10552_bit0 -x20552_bit0 -x30552_bit0 -x40552_bit0 -x10652_bit0 -x20652_bit0 -x30652_bit0 -x40652_bit0 -x50652_bit0 -x10752_bit0 -x20752_bit0 -x30752_bit0 -x40752_bit0 -x50752_bit0 -x60752_bit0 -x10852_bit0 -x20852_bit0 -x30852_bit0 x40852_bit0 -x50852_bit0 -x60852_bit0 -x70852_bit0 -x10952_bit0 -x20952_bit0 -x30952_bit0 -x40952_bit0 -x50952_bit0 -x60952_bit0 -x70952_bit0 -x80952_bit0 -x11052_bit0 -x21052_bit0 -x31052_bit0 -x41052_bit0 -x51052_bit0 -x61052_bit0 -x71052_bit0 -x81052_bit0 -x91052_bit0 -x10213_bit0 -x10313_bit0 -x20313_bit0 -x10413_bit0 -x20413_bit0 -x30413_bit0 -x10513_bit0 -x20513_bit0 -x30513_bit0 -x40513_bit0 -x10613_bit0 -x20613_bit0 -x30613_bit0 -x40613_bit0 -x50613_bit0 -x10713_bit0 -x20713_bit0 -x30713_bit0 -x40713_bit0 -x50713_bit0 -x60713_bit0 -x10813_bit0 -x20813_bit0 -x30813_bit0 -x40813_bit0 -x50813_bit0 -x60813_bit0 -x70813_bit0 -x10913_bit0 -x20913_bit0 -x30913_bit0 -x40913_bit0 -x50913_bit0 -x60913_bit0 -x70913_bit0 x80913_bit0 -x11013_bit0 -x21013_bit0 -x31013_bit0 -x41013_bit0 -x51013_bit0 -x61013_bit0 -x71013_bit0 -x81013_bit0 -x91013_bit0 -x10223_bit0 -x10323_bit0 -x20323_bit0 -x10423_bit0 -x20423_bit0 -x30423_bit0 x10523_bit0 -x20523_bit0 -x30523_bit0 -x40523_bit0 -x10623_bit0 -x20623_bit0 -x30623_bit0 -x40623_bit0 -x50623_bit0 -x10723_bit0 -x20723_bit0 -x30723_bit0 -x40723_bit0 -x50723_bit0 -x60723_bit0 -x10823_bit0 -x20823_bit0 -x30823_bit0 -x40823_bit0 -x50823_bit0 -x60823_bit0 -x70823_bit0 -x10923_bit0 -x20923_bit0 -x30923_bit0 -x40923_bit0 -x50923_bit0 -x60923_bit0 -x70923_bit0 -x80923_bit0 -x11023_bit0 -x21023_bit0 -x31023_bit0 -x41023_bit0 -x51023_bit0 -x61023_bit0 -x71023_bit0 -x81023_bit0 -x91023_bit0 -x10233_bit0 -x10333_bit0 -x20333_bit0 -x10433_bit0 -x20433_bit0 -x30433_bit0 -x10533_bit0 -x20533_bit0 -x30533_bit0 -x40533_bit0 -x10633_bit0 -x20633_bit0 -x30633_bit0 -x40633_bit0 -x50633_bit0 -x10733_bit0 x20733_bit0 -x30733_bit0 -x40733_bit0 -x50733_bit0 -x60733_bit0 -x10833_bit0 -x20833_bit0 -x30833_bit0 -x40833_bit0 -x50833_bit0 -x60833_bit0 -x70833_bit0 -x10933_bit0 -x20933_bit0 -x30933_bit0 -x40933_bit0 -x50933_bit0 -x60933_bit0 -x70933_bit0 -x80933_bit0 -x11033_bit0 -x21033_bit0 -x31033_bit0 -x41033_bit0 -x51033_bit0 -x61033_bit0 -x71033_bit0 -x81033_bit0 -x91033_bit0 -x10243_bit0 -x10343_bit0 -x20343_bit0 -x10443_bit0 -x20443_bit0 -x30443_bit0 -x10543_bit0 -x20543_bit0 -x30543_bit0 -x40543_bit0 -x10643_bit0 -x20643_bit0 -x30643_bit0 -x40643_bit0 -x50643_bit0 -x10743_bit0 -x20743_bit0 -x30743_bit0 -x40743_bit0 -x50743_bit0 -x60743_bit0 -x10843_bit0 -x20843_bit0 -x30843_bit0 -x40843_bit0 -x50843_bit0 -x60843_bit0 -x70843_bit0 -x10943_bit0 -x20943_bit0 -x30943_bit0 -x40943_bit0 -x50943_bit0 -x60943_bit0 -x70943_bit0 -x80943_bit0 -x11043_bit0 -x21043_bit0 -x31043_bit0 x41043_bit0 -x51043_bit0 -x61043_bit0 -x71043_bit0 -x81043_bit0 -x91043_bit0 -x10253_bit0 -x10353_bit0 -x20353_bit0 -x10453_bit0 -x20453_bit0 -x30453_bit0 -x10553_bit0 -x20553_bit0 -x30553_bit0 -x40553_bit0 -x10653_bit0 -x20653_bit0 x30653_bit0 -x40653_bit0 -x50653_bit0 -x10753_bit0 -x20753_bit0 -x30753_bit0 -x40753_bit0 -x50753_bit0 -x60753_bit0 -x10853_bit0 -x20853_bit0 -x30853_bit0 -x40853_bit0 -x50853_bit0 -x60853_bit0 -x70853_bit0 -x10953_bit0 -x20953_bit0 -x30953_bit0 -x40953_bit0 -x50953_bit0 -x60953_bit0 -x70953_bit0 -x80953_bit0 -x11053_bit0 -x21053_bit0 -x31053_bit0 -x41053_bit0 -x51053_bit0 -x61053_bit0 -x71053_bit0 -x81053_bit0 -x91053_bit0 -x10214_bit0 -x10314_bit0 x20314_bit0 -x10414_bit0 -x20414_bit0 -x30414_bit0 -x10514_bit0 -x20514_bit0 -x30514_bit0 -x40514_bit0 -x10614_bit0 -x20614_bit0 -x30614_bit0 -x40614_bit0 -x50614_bit0 -x10714_bit0 -x20714_bit0 -x30714_bit0 -x40714_bit0 -x50714_bit0 -x60714_bit0 -x10814_bit0 -x20814_bit0 -x30814_bit0 -x40814_bit0 -x50814_bit0 -x60814_bit0 -x70814_bit0 -x10914_bit0 -x20914_bit0 -x30914_bit0 -x40914_bit0 -x50914_bit0 -x60914_bit0 -x70914_bit0 -x80914_bit0 -x11014_bit0 -x21014_bit0 -x31014_bit0 -x41014_bit0 -x51014_bit0 -x61014_bit0 -x71014_bit0 -x81014_bit0 -x91014_bit0 -x10224_bit0 -x10324_bit0 -x20324_bit0 -x10424_bit0 -x20424_bit0 -x30424_bit0 -x10524_bit0 -x20524_bit0 -x30524_bit0 -x40524_bit0 -x10624_bit0 -x20624_bit0 -x30624_bit0 -x40624_bit0 -x50624_bit0 x10724_bit0 -x20724_bit0 -x30724_bit0 -x40724_bit0 -x50724_bit0 -x60724_bit0 -x10824_bit0 -x20824_bit0 -x30824_bit0 -x40824_bit0 -x50824_bit0 -x60824_bit0 -x70824_bit0 -x10924_bit0 -x20924_bit0 -x30924_bit0 -x40924_bit0 -x50924_bit0 -x60924_bit0 -x70924_bit0 -x80924_bit0 -x11024_bit0 -x21024_bit0 -x31024_bit0 -x41024_bit0 -x51024_bit0 -x61024_bit0 -x71024_bit0 -x81024_bit0 -x91024_bit0 -x10234_bit0 -x10334_bit0 -x20334_bit0 -x10434_bit0 -x20434_bit0 -x30434_bit0 -x10534_bit0 -x20534_bit0 -x30534_bit0 -x40534_bit0 -x10634_bit0 -x20634_bit0 -x30634_bit0 -x40634_bit0 -x50634_bit0 -x10734_bit0 -x20734_bit0 -x30734_bit0 -x40734_bit0 -x50734_bit0 -x60734_bit0 -x10834_bit0 -x20834_bit0 -x30834_bit0 -x40834_bit0 -x50834_bit0 -x60834_bit0 -x70834_bit0 -x10934_bit0 -x20934_bit0 -x30934_bit0 x40934_bit0 -x50934_bit0 -x60934_bit0 -x70934_bit0 -x80934_bit0 -x11034_bit0 -x21034_bit0 -x31034_bit0 -x41034_bit0 -x51034_bit0 -x61034_bit0 -x71034_bit0 -x81034_bit0 -x91034_bit0 -x10244_bit0 -x10344_bit0 -x20344_bit0 -x10444_bit0 -x20444_bit0 -x30444_bit0 -x10544_bit0 -x20544_bit0 -x30544_bit0 -x40544_bit0 -x10644_bit0 -x20644_bit0 -x30644_bit0 -x40644_bit0 -x50644_bit0 -x10744_bit0 -x20744_bit0 -x30744_bit0 -x40744_bit0 -x50744_bit0 -x60744_bit0 -x10844_bit0 -x20844_bit0 -x30844_bit0 -x40844_bit0 x50844_bit0 -x60844_bit0 -x70844_bit0 -x10944_bit0 -x20944_bit0 -x30944_bit0 -x40944_bit0 -x50944_bit0 -x60944_bit0 -x70944_bit0 -x80944_bit0 -x11044_bit0 -x21044_bit0 -x31044_bit0 -x41044_bit0 -x51044_bit0 -x61044_bit0 -x71044_bit0 -x81044_bit0 -x91044_bit0 -x10254_bit0 -x10354_bit0 -x20354_bit0 -x10454_bit0 -x20454_bit0 -x30454_bit0 -x10554_bit0 -x20554_bit0 -x30554_bit0 -x40554_bit0 -x10654_bit0 -x20654_bit0 -x30654_bit0 -x40654_bit0 -x50654_bit0 -x10754_bit0 -x20754_bit0 -x30754_bit0 -x40754_bit0 -x50754_bit0 -x60754_bit0 -x10854_bit0 -x20854_bit0 -x30854_bit0 -x40854_bit0 -x50854_bit0 -x60854_bit0 -x70854_bit0 -x10954_bit0 -x20954_bit0 -x30954_bit0 -x40954_bit0 -x50954_bit0 -x60954_bit0 -x70954_bit0 -x80954_bit0 -x11054_bit0 -x21054_bit0 -x31054_bit0 -x41054_bit0 -x51054_bit0 x61054_bit0 -x71054_bit0 -x81054_bit0 -x91054_bit0 -x10215_bit0 -x10315_bit0 -x20315_bit0 -x10415_bit0 -x20415_bit0 -x30415_bit0 -x10515_bit0 -x20515_bit0 -x30515_bit0 -x40515_bit0 -x10615_bit0 -x20615_bit0 -x30615_bit0 -x40615_bit0 -x50615_bit0 -x10715_bit0 -x20715_bit0 -x30715_bit0 -x40715_bit0 -x50715_bit0 -x60715_bit0 -x10815_bit0 -x20815_bit0 -x30815_bit0 -x40815_bit0 -x50815_bit0 -x60815_bit0 -x70815_bit0 -x10915_bit0 -x20915_bit0 -x30915_bit0 -x40915_bit0 x50915_bit0 -x60915_bit0 -x70915_bit0 -x80915_bit0 -x11015_bit0 -x21015_bit0 -x31015_bit0 -x41015_bit0 -x51015_bit0 -x61015_bit0 -x71015_bit0 -x81015_bit0 -x91015_bit0 -x10225_bit0 -x10325_bit0 -x20325_bit0 -x10425_bit0 -x20425_bit0 -x30425_bit0 -x10525_bit0 -x20525_bit0 -x30525_bit0 -x40525_bit0 -x10625_bit0 -x20625_bit0 -x30625_bit0 -x40625_bit0 -x50625_bit0 -x10725_bit0 -x20725_bit0 -x30725_bit0 -x40725_bit0 -x50725_bit0 -x60725_bit0 -x10825_bit0 -x20825_bit0 x30825_bit0 -x40825_bit0 -x50825_bit0 -x60825_bit0 -x70825_bit0 -x10925_bit0 -x20925_bit0 -x30925_bit0 -x40925_bit0 -x50925_bit0 -x60925_bit0 -x70925_bit0 -x80925_bit0 -x11025_bit0 -x21025_bit0 -x31025_bit0 -x41025_bit0 -x51025_bit0 -x61025_bit0 -x71025_bit0 -x81025_bit0 -x91025_bit0 -x10235_bit0 -x10335_bit0 -x20335_bit0 -x10435_bit0 -x20435_bit0 -x30435_bit0 -x10535_bit0 -x20535_bit0 -x30535_bit0 -x40535_bit0 -x10635_bit0 -x20635_bit0 -x30635_bit0 -x40635_bit0 -x50635_bit0 -x10735_bit0 -x20735_bit0 -x30735_bit0 -x40735_bit0 -x50735_bit0 -x60735_bit0 -x10835_bit0 -x20835_bit0 -x30835_bit0 -x40835_bit0 -x50835_bit0 -x60835_bit0 -x70835_bit0 -x10935_bit0 -x20935_bit0 -x30935_bit0 -x40935_bit0 -x50935_bit0 -x60935_bit0 -x70935_bit0 -x80935_bit0 x11035_bit0 -x21035_bit0 -x31035_bit0 -x41035_bit0 -x51035_bit0 -x61035_bit0 -x71035_bit0 -x81035_bit0 -x91035_bit0 -x10245_bit0 -x10345_bit0 -x20345_bit0 -x10445_bit0 -x20445_bit0 -x30445_bit0 -x10545_bit0 -x20545_bit0 -x30545_bit0 -x40545_bit0 -x10645_bit0 x20645_bit0 -x30645_bit0 -x40645_bit0 -x50645_bit0 -x10745_bit0 -x20745_bit0 -x30745_bit0 -x40745_bit0 -x50745_bit0 -x60745_bit0 -x10845_bit0 -x20845_bit0 -x30845_bit0 -x40845_bit0 -x50845_bit0 -x60845_bit0 -x70845_bit0 -x10945_bit0 -x20945_bit0 -x30945_bit0 -x40945_bit0 -x50945_bit0 -x60945_bit0 -x70945_bit0 -x80945_bit0 -x11045_bit0 -x21045_bit0 -x31045_bit0 -x41045_bit0 -x51045_bit0 -x61045_bit0 -x71045_bit0 -x81045_bit0 -x91045_bit0 -x10255_bit0 -x10355_bit0 -x20355_bit0 -x10455_bit0 -x20455_bit0 -x30455_bit0 -x10555_bit0 -x20555_bit0 -x30555_bit0 -x40555_bit0 -x10655_bit0 -x20655_bit0 -x30655_bit0 -x40655_bit0 -x50655_bit0 -x10755_bit0 -x20755_bit0 -x30755_bit0 x40755_bit0 -x50755_bit0 -x60755_bit0 -x10855_bit0 -x20855_bit0 -x30855_bit0 -x40855_bit0 -x50855_bit0 -x60855_bit0 -x70855_bit0 -x10955_bit0 -x20955_bit0 -x30955_bit0 -x40955_bit0 -x50955_bit0 -x60955_bit0 -x70955_bit0 -x80955_bit0 -x11055_bit0 -x21055_bit0 -x31055_bit0 -x41055_bit0 -x51055_bit0 -x61055_bit0 -x71055_bit0 -x81055_bit0 -x91055_bit0 -x10216_bit0 -x10316_bit0 -x20316_bit0 -x10416_bit0 -x20416_bit0 -x30416_bit0 -x10516_bit0 -x20516_bit0 -x30516_bit0 -x40516_bit0 -x10616_bit0 -x20616_bit0 -x30616_bit0 x40616_bit0 -x50616_bit0 -x10716_bit0 -x20716_bit0 -x30716_bit0 -x40716_bit0 -x50716_bit0 -x60716_bit0 -x10816_bit0 -x20816_bit0 -x30816_bit0 -x40816_bit0 -x50816_bit0 -x60816_bit0 -x70816_bit0 -x10916_bit0 -x20916_bit0 -x30916_bit0 -x40916_bit0 -x50916_bit0 -x60916_bit0 -x70916_bit0 -x80916_bit0 -x11016_bit0 -x21016_bit0 -x31016_bit0 -x41016_bit0 -x51016_bit0 -x61016_bit0 -x71016_bit0 -x81016_bit0 -x91016_bit0 -x10226_bit0 -x10326_bit0 -x20326_bit0 -x10426_bit0 -x20426_bit0 -x30426_bit0 -x10526_bit0 -x20526_bit0 -x30526_bit0 -x40526_bit0 -x10626_bit0 -x20626_bit0 -x30626_bit0 -x40626_bit0 -x50626_bit0 -x10726_bit0 -x20726_bit0 -x30726_bit0 -x40726_bit0 -x50726_bit0 -x60726_bit0 -x10826_bit0 -x20826_bit0 -x30826_bit0 -x40826_bit0 -x50826_bit0 -x60826_bit0 -x70826_bit0 -x10926_bit0 -x20926_bit0 -x30926_bit0 -x40926_bit0 -x50926_bit0 -x60926_bit0 -x70926_bit0 -x80926_bit0 -x11026_bit0 x21026_bit0 -x31026_bit0 -x41026_bit0 -x51026_bit0 -x61026_bit0 -x71026_bit0 -x81026_bit0 -x91026_bit0 -x10236_bit0 -x10336_bit0 -x20336_bit0 -x10436_bit0 -x20436_bit0 -x30436_bit0 -x10536_bit0 -x20536_bit0 -x30536_bit0 -x40536_bit0 -x10636_bit0 -x20636_bit0 -x30636_bit0 -x40636_bit0 -x50636_bit0 -x10736_bit0 -x20736_bit0 -x30736_bit0 -x40736_bit0 -x50736_bit0 -x60736_bit0 x10836_bit0 -x20836_bit0 -x30836_bit0 -x40836_bit0 -x50836_bit0 -x60836_bit0 -x70836_bit0 -x10936_bit0 -x20936_bit0 -x30936_bit0 -x40936_bit0 -x50936_bit0 -x60936_bit0 -x70936_bit0 -x80936_bit0 -x11036_bit0 -x21036_bit0 -x31036_bit0 -x41036_bit0 -x51036_bit0 -x61036_bit0 -x71036_bit0 -x81036_bit0 -x91036_bit0 -x10246_bit0 -x10346_bit0 -x20346_bit0 -x10446_bit0 -x20446_bit0 -x30446_bit0 -x10546_bit0 -x20546_bit0 -x30546_bit0 -x40546_bit0 -x10646_bit0 -x20646_bit0 -x30646_bit0 -x40646_bit0 -x50646_bit0 -x10746_bit0 -x20746_bit0 -x30746_bit0 -x40746_bit0 -x50746_bit0 -x60746_bit0 -x10846_bit0 -x20846_bit0 -x30846_bit0 -x40846_bit0 -x50846_bit0 -x60846_bit0 -x70846_bit0 -x10946_bit0 -x20946_bit0 -x30946_bit0 -x40946_bit0 -x50946_bit0 -x60946_bit0 x70946_bit0 -x80946_bit0 -x11046_bit0 -x21046_bit0 -x31046_bit0 -x41046_bit0 -x51046_bit0 -x61046_bit0 -x71046_bit0 -x81046_bit0 -x91046_bit0 -x10256_bit0 -x10356_bit0 -x20356_bit0 -x10456_bit0 -x20456_bit0 -x30456_bit0 -x10556_bit0 -x20556_bit0 x30556_bit0 -x40556_bit0 -x10656_bit0 -x20656_bit0 -x30656_bit0 -x40656_bit0 -x50656_bit0 -x10756_bit0 -x20756_bit0 -x30756_bit0 -x40756_bit0 -x50756_bit0 -x60756_bit0 -x10856_bit0 -x20856_bit0 -x30856_bit0 -x40856_bit0 -x50856_bit0 -x60856_bit0 -x70856_bit0 -x10956_bit0 -x20956_bit0 -x30956_bit0 -x40956_bit0 -x50956_bit0 -x60956_bit0 -x70956_bit0 -x80956_bit0 -x11056_bit0 -x21056_bit0 -x31056_bit0 -x41056_bit0 -x51056_bit0 -x61056_bit0 -x71056_bit0 -x81056_bit0 -x91056_bit0 -x10217_bit0 -x10317_bit0 -x20317_bit0 -x10417_bit0 -x20417_bit0 -x30417_bit0 -x10517_bit0 -x20517_bit0 -x30517_bit0 -x40517_bit0 -x10617_bit0 -x20617_bit0 -x30617_bit0 -x40617_bit0 -x50617_bit0 -x10717_bit0 -x20717_bit0 -x30717_bit0 -x40717_bit0 -x50717_bit0 -x60717_bit0 -x10817_bit0 -x20817_bit0 -x30817_bit0 -x40817_bit0 -x50817_bit0 -x60817_bit0 -x70817_bit0 -x10917_bit0 -x20917_bit0 -x30917_bit0 -x40917_bit0 -x50917_bit0 -x60917_bit0 -x70917_bit0 -x80917_bit0 -x11017_bit0 -x21017_bit0 -x31017_bit0 -x41017_bit0 -x51017_bit0 -x61017_bit0 -x71017_bit0 x81017_bit0 -x91017_bit0 -x10227_bit0 -x10327_bit0 -x20327_bit0 -x10427_bit0 -x20427_bit0 -x30427_bit0 -x10527_bit0 -x20527_bit0 -x30527_bit0 -x40527_bit0 -x10627_bit0 -x20627_bit0 -x30627_bit0 -x40627_bit0 -x50627_bit0 -x10727_bit0 -x20727_bit0 -x30727_bit0 -x40727_bit0 -x50727_bit0 x60727_bit0 -x10827_bit0 -x20827_bit0 -x30827_bit0 -x40827_bit0 -x50827_bit0 -x60827_bit0 -x70827_bit0 -x10927_bit0 -x20927_bit0 -x30927_bit0 -x40927_bit0 -x50927_bit0 -x60927_bit0 -x70927_bit0 -x80927_bit0 -x11027_bit0 -x21027_bit0 -x31027_bit0 -x41027_bit0 -x51027_bit0 -x61027_bit0 -x71027_bit0 -x81027_bit0 -x91027_bit0 -x10237_bit0 -x10337_bit0 -x20337_bit0 -x10437_bit0 -x20437_bit0 -x30437_bit0 -x10537_bit0 -x20537_bit0 -x30537_bit0 -x40537_bit0 -x10637_bit0 -x20637_bit0 -x30637_bit0 -x40637_bit0 -x50637_bit0 -x10737_bit0 -x20737_bit0 -x30737_bit0 -x40737_bit0 -x50737_bit0 -x60737_bit0 -x10837_bit0 -x20837_bit0 -x30837_bit0 -x40837_bit0 -x50837_bit0 -x60837_bit0 -x70837_bit0 -x10937_bit0 -x20937_bit0 x30937_bit0 -x40937_bit0 -x50937_bit0 -x60937_bit0 -x70937_bit0 -x80937_bit0 -x11037_bit0 -x21037_bit0 -x31037_bit0 -x41037_bit0 -x51037_bit0 -x61037_bit0 -x71037_bit0 -x81037_bit0 -x91037_bit0 -x10247_bit0 -x10347_bit0 -x20347_bit0 x10447_bit0 -x20447_bit0 -x30447_bit0 -x10547_bit0 -x20547_bit0 -x30547_bit0 -x40547_bit0 -x10647_bit0 -x20647_bit0 -x30647_bit0 -x40647_bit0 -x50647_bit0 -x10747_bit0 -x20747_bit0 -x30747_bit0 -x40747_bit0 -x50747_bit0 -x60747_bit0 -x10847_bit0 -x20847_bit0 -x30847_bit0 -x40847_bit0 -x50847_bit0 -x60847_bit0 -x70847_bit0 -x10947_bit0 -x20947_bit0 -x30947_bit0 -x40947_bit0 -x50947_bit0 -x60947_bit0 -x70947_bit0 -x80947_bit0 -x11047_bit0 -x21047_bit0 -x31047_bit0 -x41047_bit0 -x51047_bit0 -x61047_bit0 -x71047_bit0 -x81047_bit0 -x91047_bit0 -x10257_bit0 -x10357_bit0 -x20357_bit0 -x10457_bit0 -x20457_bit0 -x30457_bit0 -x10557_bit0 x20557_bit0 -x30557_bit0 -x40557_bit0 -x10657_bit0 -x20657_bit0 -x30657_bit0 -x40657_bit0 -x50657_bit0 -x10757_bit0 -x20757_bit0 -x30757_bit0 -x40757_bit0 -x50757_bit0 -x60757_bit0 -x10857_bit0 -x20857_bit0 -x30857_bit0 -x40857_bit0 -x50857_bit0 -x60857_bit0 -x70857_bit0 -x10957_bit0 -x20957_bit0 -x30957_bit0 -x40957_bit0 -x50957_bit0 -x60957_bit0 -x70957_bit0 -x80957_bit0 -x11057_bit0 -x21057_bit0 -x31057_bit0 -x41057_bit0 -x51057_bit0 -x61057_bit0 -x71057_bit0 -x81057_bit0 -x91057_bit0 -x10218_bit0 -x10318_bit0 -x20318_bit0 -x10418_bit0 -x20418_bit0 -x30418_bit0 -x10518_bit0 -x20518_bit0 -x30518_bit0 -x40518_bit0 -x10618_bit0 -x20618_bit0 -x30618_bit0 -x40618_bit0 -x50618_bit0 -x10718_bit0 -x20718_bit0 -x30718_bit0 -x40718_bit0 x50718_bit0 -x60718_bit0 -x10818_bit0 -x20818_bit0 -x30818_bit0 -x40818_bit0 -x50818_bit0 -x60818_bit0 -x70818_bit0 -x10918_bit0 -x20918_bit0 -x30918_bit0 -x40918_bit0 -x50918_bit0 -x60918_bit0 -x70918_bit0 -x80918_bit0 -x11018_bit0 -x21018_bit0 -x31018_bit0 -x41018_bit0 -x51018_bit0 -x61018_bit0 -x71018_bit0 -x81018_bit0 -x91018_bit0 -x10228_bit0 -x10328_bit0 -x20328_bit0 -x10428_bit0 x20428_bit0 -x30428_bit0 -x10528_bit0 -x20528_bit0 -x30528_bit0 -x40528_bit0 -x10628_bit0 -x20628_bit0 -x30628_bit0 -x40628_bit0 -x50628_bit0 -x10728_bit0 -x20728_bit0 -x30728_bit0 -x40728_bit0 -x50728_bit0 -x60728_bit0 -x10828_bit0 -x20828_bit0 -x30828_bit0 -x40828_bit0 -x50828_bit0 -x60828_bit0 -x70828_bit0 -x10928_bit0 -x20928_bit0 -x30928_bit0 -x40928_bit0 -x50928_bit0 -x60928_bit0 -x70928_bit0 -x80928_bit0 -x11028_bit0 -x21028_bit0 -x31028_bit0 -x41028_bit0 -x51028_bit0 -x61028_bit0 -x71028_bit0 -x81028_bit0 -x91028_bit0 -x10238_bit0 -x10338_bit0 -x20338_bit0 -x10438_bit0 -x20438_bit0 -x30438_bit0 -x10538_bit0 -x20538_bit0 -x30538_bit0 -x40538_bit0 -x10638_bit0 -x20638_bit0 -x30638_bit0 -x40638_bit0 -x50638_bit0 -x10738_bit0 -x20738_bit0 -x30738_bit0 -x40738_bit0 -x50738_bit0 -x60738_bit0 -x10838_bit0 -x20838_bit0 -x30838_bit0 -x40838_bit0 -x50838_bit0 x60838_bit0 -x70838_bit0 -x10938_bit0 -x20938_bit0 -x30938_bit0 -x40938_bit0 -x50938_bit0 -x60938_bit0 -x70938_bit0 -x80938_bit0 -x11038_bit0 -x21038_bit0 -x31038_bit0 -x41038_bit0 -x51038_bit0 -x61038_bit0 -x71038_bit0 -x81038_bit0 -x91038_bit0 -x10248_bit0 -x10348_bit0 -x20348_bit0 -x10448_bit0 -x20448_bit0 -x30448_bit0 -x10548_bit0 -x20548_bit0 -x30548_bit0 -x40548_bit0 -x10648_bit0 -x20648_bit0 -x30648_bit0 -x40648_bit0 -x50648_bit0 -x10748_bit0 -x20748_bit0 -x30748_bit0 -x40748_bit0 -x50748_bit0 -x60748_bit0 -x10848_bit0 -x20848_bit0 -x30848_bit0 -x40848_bit0 -x50848_bit0 -x60848_bit0 -x70848_bit0 -x10948_bit0 -x20948_bit0 -x30948_bit0 -x40948_bit0 -x50948_bit0 -x60948_bit0 -x70948_bit0 -x80948_bit0 -x11048_bit0 -x21048_bit0 x31048_bit0 -x41048_bit0 -x51048_bit0 -x61048_bit0 -x71048_bit0 -x81048_bit0 -x91048_bit0 -x10258_bit0 -x10358_bit0 -x20358_bit0 -x10458_bit0 -x20458_bit0 -x30458_bit0 -x10558_bit0 -x20558_bit0 -x30558_bit0 -x40558_bit0 -x10658_bit0 -x20658_bit0 -x30658_bit0 -x40658_bit0 -x50658_bit0 -x10758_bit0 -x20758_bit0 -x30758_bit0 -x40758_bit0 -x50758_bit0 -x60758_bit0 -x10858_bit0 -x20858_bit0 -x30858_bit0 -x40858_bit0 -x50858_bit0 -x60858_bit0 -x70858_bit0 x10958_bit0 -x20958_bit0 -x30958_bit0 -x40958_bit0 -x50958_bit0 -x60958_bit0 -x70958_bit0 -x80958_bit0 -x11058_bit0 -x21058_bit0 -x31058_bit0 -x41058_bit0 -x51058_bit0 -x61058_bit0 -x71058_bit0 -x81058_bit0 -x91058_bit0 #### 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.79 0.95 0.93 2/54 20458
Raw data (stat): 20458 (runsolver) R 20457 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 491002522 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.82 0.95 0.93 2/54 20458
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 2704 0 0 0 990 8 0 0 25 0 1 0 491002522 13152256 2665 4294967295 134512640 134672761 3221224624 3221223728 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3211 2665 603 41 0 3170 0
vsize: 12844
[startup+20.0021 s]
Raw data (loadavg): 0.85 0.95 0.93 2/54 20458
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 9242 0 0 0 1975 22 0 0 25 0 1 0 491002522 36073472 7882 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8807 7882 603 41 0 8766 0
vsize: 35228
[startup+30.0027 s]
Raw data (loadavg): 0.87 0.95 0.93 2/54 20458
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 9681 0 0 0 2974 23 0 0 25 0 1 0 491002522 37969920 8321 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9270 8321 603 41 0 9229 0
vsize: 37080
[startup+40.0037 s]
Raw data (loadavg): 0.89 0.95 0.93 2/57 20461
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 10162 0 0 0 3971 26 0 0 25 0 1 0 491002522 39862272 8802 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9732 8802 603 41 0 9691 0
vsize: 38928
[startup+50.0044 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 20511
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 10678 0 0 0 4970 27 0 0 25 0 1 0 491002522 42016768 9318 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10258 9318 603 41 0 10217 0
vsize: 41032
[startup+60.0052 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 20511
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 11070 0 0 0 5969 28 0 0 25 0 1 0 491002522 43630592 9710 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10652 9710 603 41 0 10611 0
vsize: 42608
[startup+70.006 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 20511
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 11490 0 0 0 6968 29 0 0 25 0 1 0 491002522 45150208 10066 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11023 10066 603 41 0 10982 0
vsize: 44092
[startup+80.0058 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20511
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 11867 0 0 0 7967 30 0 0 25 0 1 0 491002522 46632960 10443 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11385 10443 603 41 0 11344 0
vsize: 45540
[startup+90.0066 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20511
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 12348 0 0 0 8966 32 0 0 25 0 1 0 491002522 48635904 10924 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11874 10924 603 41 0 11833 0
vsize: 47496
[startup+100.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20511
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 12750 0 0 0 9965 33 0 0 25 0 1 0 491002522 50257920 11326 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12270 11326 603 41 0 12229 0
vsize: 49080
[startup+110.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20511
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 13160 0 0 0 10965 33 0 0 25 0 1 0 491002522 51863552 11736 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12662 11736 603 41 0 12621 0
vsize: 50648
[startup+120.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20513
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 13641 0 0 0 11963 35 0 0 25 0 1 0 491002522 53882880 12217 4294967295 134512640 134672761 3221224624 3221223728 134559841 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13155 12217 603 41 0 13114 0
vsize: 52620
[startup+130.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20513
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 14119 0 0 0 12962 36 0 0 25 0 1 0 491002522 55754752 12695 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13612 12695 603 41 0 13571 0
vsize: 54448
[startup+140.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20513
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 14529 0 0 0 13961 37 0 0 25 0 1 0 491002522 57487360 13105 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14035 13105 603 41 0 13994 0
vsize: 56140
[startup+150.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20513
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 14929 0 0 0 14960 39 0 0 25 0 1 0 491002522 59092992 13505 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14427 13505 603 41 0 14386 0
vsize: 57708
[startup+160.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20513
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 15363 0 0 0 15959 40 0 0 25 0 1 0 491002522 60833792 13939 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14852 13939 603 41 0 14811 0
vsize: 59408
[startup+170.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20513
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 15782 0 0 0 16958 41 0 0 25 0 1 0 491002522 62550016 14358 4294967295 134512640 134672761 3221224624 3221223728 134560267 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15271 14358 603 41 0 15230 0
vsize: 61084
[startup+180.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20513
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 16187 0 0 0 17956 43 0 0 25 0 1 0 491002522 64417792 14763 4294967295 134512640 134672761 3221224624 3221223624 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15727 14763 603 41 0 15686 0
vsize: 62908
[startup+190.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20513
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 16641 0 0 0 18955 44 0 0 25 0 1 0 491002522 66174976 15217 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16156 15217 603 41 0 16115 0
vsize: 64624
[startup+200.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20513
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 17046 0 0 0 19954 45 0 0 25 0 1 0 491002522 67919872 15622 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16582 15622 603 41 0 16541 0
vsize: 66328
[startup+210.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20513
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 17451 0 0 0 20954 46 0 0 25 0 1 0 491002522 69521408 16027 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16973 16027 603 41 0 16932 0
vsize: 67892
[startup+220.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20513
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 17798 0 0 0 21953 47 0 0 25 0 1 0 491002522 70983680 16374 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17330 16374 603 41 0 17289 0
vsize: 69320
[startup+230.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20513
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 18151 0 0 0 22952 48 0 0 25 0 1 0 491002522 72458240 16727 4294967295 134512640 134672761 3221224624 3221223808 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17690 16727 603 41 0 17649 0
vsize: 70760
[startup+240.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20513
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 18494 0 0 0 23951 49 0 0 25 0 1 0 491002522 73801728 17070 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18018 17070 603 41 0 17977 0
vsize: 72072
[startup+250.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20513
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 18882 0 0 0 24951 50 0 0 25 0 1 0 491002522 75403264 17458 4294967295 134512640 134672761 3221224624 3221223728 134555244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18409 17458 603 41 0 18368 0
vsize: 73636
[startup+260.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20513
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 19309 0 0 0 25950 51 0 0 25 0 1 0 491002522 77144064 17885 4294967295 134512640 134672761 3221224624 3221223808 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18834 17886 603 41 0 18793 0
vsize: 75336
[startup+270.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20513
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 19677 0 0 0 26949 52 0 0 25 0 1 0 491002522 78614528 18253 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19193 18253 603 41 0 19152 0
vsize: 76772
[startup+280.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20513
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 20063 0 0 0 27948 53 0 0 25 0 1 0 491002522 80220160 18639 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19585 18639 603 41 0 19544 0
vsize: 78340
[startup+290.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20513
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 20487 0 0 0 28947 54 0 0 25 0 1 0 491002522 81965056 19063 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20011 19063 603 41 0 19970 0
vsize: 80044
[startup+300.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20513
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 20941 0 0 0 29945 57 0 0 25 0 1 0 491002522 83845120 19517 4294967295 134512640 134672761 3221224624 3221223760 134560703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20470 19517 603 41 0 20429 0
vsize: 81880
[startup+310.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20513
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 21343 0 0 0 30944 58 0 0 25 0 1 0 491002522 85450752 19919 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20862 19919 603 41 0 20821 0
vsize: 83448
[startup+320.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20513
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 21732 0 0 0 31943 59 0 0 25 0 1 0 491002522 87056384 20308 4294967295 134512640 134672761 3221224624 3221223728 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21254 20308 603 41 0 21213 0
vsize: 85016
[startup+330.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20513
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 22127 0 0 0 32942 60 0 0 25 0 1 0 491002522 88641536 20703 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21641 20703 603 41 0 21600 0
vsize: 86564
[startup+340.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20513
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 22518 0 0 0 33942 61 0 0 25 0 1 0 491002522 90251264 21094 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22034 21094 603 41 0 21993 0
vsize: 88136
[startup+350.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20513
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 22848 0 0 0 34942 62 0 0 25 0 1 0 491002522 91602944 21424 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22364 21424 603 41 0 22323 0
vsize: 89456
[startup+360.039 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20513
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 23225 0 0 0 35942 63 0 0 25 0 1 0 491002522 93081600 21801 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22725 21801 603 41 0 22684 0
vsize: 90900
[startup+370.048 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20513
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 23586 0 0 0 36942 64 0 0 25 0 1 0 491002522 94547968 22162 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23083 22162 603 41 0 23042 0
vsize: 92332
[startup+380.049 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20513
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 23982 0 0 0 37941 65 0 0 25 0 1 0 491002522 96141312 22558 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23472 22558 603 41 0 23431 0
vsize: 93888
[startup+390.059 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20513
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 24360 0 0 0 38941 67 0 0 25 0 1 0 491002522 97759232 22936 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23867 22936 603 41 0 23826 0
vsize: 95468
[startup+400.062 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 24788 0 0 0 39939 69 0 0 25 0 1 0 491002522 99504128 23364 4294967295 134512640 134672761 3221224624 3221223728 134560260 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24293 23364 603 41 0 24252 0
vsize: 97172
[startup+410.062 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 25239 0 0 0 40938 70 0 0 25 0 1 0 491002522 101388288 23815 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24753 23815 603 41 0 24712 0
vsize: 99012
[startup+420.07 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 25700 0 0 0 41937 72 0 0 25 0 1 0 491002522 103284736 24276 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25216 24276 603 41 0 25175 0
vsize: 100864
[startup+430.079 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 26139 0 0 0 42937 73 0 0 25 0 1 0 491002522 105037824 24715 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25644 24715 603 41 0 25603 0
vsize: 102576
[startup+440.079 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 26556 0 0 0 43936 74 0 0 25 0 1 0 491002522 106786816 25132 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26071 25132 603 41 0 26030 0
vsize: 104284
[startup+450.079 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 26988 0 0 0 44935 75 0 0 25 0 1 0 491002522 108802048 25564 4294967295 134512640 134672761 3221224624 3221223640 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26563 25564 603 41 0 26522 0
vsize: 106252
[startup+460.08 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 27430 0 0 0 45934 77 0 0 25 0 1 0 491002522 110571520 26006 4294967295 134512640 134672761 3221224624 3221223792 134561226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26995 26006 603 41 0 26954 0
vsize: 107980
[startup+470.08 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 27853 0 0 0 46933 78 0 0 25 0 1 0 491002522 112336896 26429 4294967295 134512640 134672761 3221224624 3221223728 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27426 26429 603 41 0 27385 0
vsize: 109704
[startup+480.08 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 28307 0 0 0 47932 79 0 0 25 0 1 0 491002522 114098176 26883 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27856 26883 603 41 0 27815 0
vsize: 111424
[startup+490.081 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 28709 0 0 0 48931 80 0 0 25 0 1 0 491002522 115847168 27285 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28283 27285 603 41 0 28242 0
vsize: 113132
[startup+500.081 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 29149 0 0 0 49930 81 0 0 25 0 1 0 491002522 117620736 27725 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28716 27725 603 41 0 28675 0
vsize: 114864
[startup+510.081 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 29598 0 0 0 50929 83 0 0 25 0 1 0 491002522 119369728 28174 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29143 28174 603 41 0 29102 0
vsize: 116572
[startup+520.081 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 30027 0 0 0 51928 84 0 0 25 0 1 0 491002522 121135104 28603 4294967295 134512640 134672761 3221224624 3221223760 134560596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29574 28603 603 41 0 29533 0
vsize: 118296
[startup+530.081 s]
Raw data (loadavg): 1.23 1.02 0.95 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 30473 0 0 0 52926 86 0 0 25 0 1 0 491002522 123035648 29049 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30038 29049 603 41 0 29997 0
vsize: 120152
[startup+540.081 s]
Raw data (loadavg): 1.27 1.04 0.95 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 30927 0 0 0 53924 87 0 0 25 0 1 0 491002522 124801024 29503 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30469 29503 603 41 0 30428 0
vsize: 121876
[startup+550.081 s]
Raw data (loadavg): 1.23 1.04 0.95 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 31245 0 0 0 54922 89 0 0 25 0 1 0 491002522 126136320 29821 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30795 29821 603 41 0 30754 0
vsize: 123180
[startup+560.081 s]
Raw data (loadavg): 1.19 1.03 0.95 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 31597 0 0 0 55920 91 0 0 25 0 1 0 491002522 127614976 30173 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31156 30173 603 41 0 31115 0
vsize: 124624
[startup+570.082 s]
Raw data (loadavg): 1.16 1.03 0.95 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 31971 0 0 0 56920 92 0 0 25 0 1 0 491002522 129093632 30547 4294967295 134512640 134672761 3221224624 3221223728 134560154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31517 30547 603 41 0 31476 0
vsize: 126068
[startup+580.082 s]
Raw data (loadavg): 1.14 1.03 0.95 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 32352 0 0 0 57918 94 0 0 25 0 1 0 491002522 130707456 30928 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31911 30928 603 41 0 31870 0
vsize: 127644
[startup+590.082 s]
Raw data (loadavg): 1.12 1.03 0.95 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 32706 0 0 0 58918 94 0 0 25 0 1 0 491002522 132161536 31282 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32266 31282 603 41 0 32225 0
vsize: 129064
[startup+600.089 s]
Raw data (loadavg): 1.10 1.03 0.95 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 33096 0 0 0 59917 96 0 0 25 0 1 0 491002522 133775360 31672 4294967295 134512640 134672761 3221224624 3221223728 134555098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32660 31672 603 41 0 32619 0
vsize: 130640
[startup+610.09 s]
Raw data (loadavg): 1.08 1.03 0.95 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 33474 0 0 0 60916 97 0 0 25 0 1 0 491002522 135229440 32050 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33015 32050 603 41 0 32974 0
vsize: 132060
[startup+620.089 s]
Raw data (loadavg): 1.15 1.04 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 33823 0 0 0 61915 98 0 0 25 0 1 0 491002522 136708096 32399 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33376 32399 603 41 0 33335 0
vsize: 133504
[startup+630.089 s]
Raw data (loadavg): 1.13 1.04 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 34179 0 0 0 62914 99 0 0 25 0 1 0 491002522 138182656 32755 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33736 32755 603 41 0 33695 0
vsize: 134944
[startup+640.09 s]
Raw data (loadavg): 1.11 1.04 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 34553 0 0 0 63913 100 0 0 25 0 1 0 491002522 139649024 33129 4294967295 134512640 134672761 3221224624 3221223776 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34094 33129 603 41 0 34053 0
vsize: 136376
[startup+650.089 s]
Raw data (loadavg): 1.09 1.04 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 34906 0 0 0 64913 101 0 0 25 0 1 0 491002522 141086720 33482 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34445 33482 603 41 0 34404 0
vsize: 137780
[startup+660.09 s]
Raw data (loadavg): 1.08 1.03 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 35271 0 0 0 65911 103 0 0 25 0 1 0 491002522 142655488 33847 4294967295 134512640 134672761 3221224624 3221223808 134559611 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34828 33847 603 41 0 34787 0
vsize: 139312
[startup+670.09 s]
Raw data (loadavg): 1.06 1.03 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 35598 0 0 0 66911 103 0 0 25 0 1 0 491002522 144003072 34174 4294967295 134512640 134672761 3221224624 3221223728 134560226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35157 34174 603 41 0 35116 0
vsize: 140628
[startup+680.09 s]
Raw data (loadavg): 1.05 1.03 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 35926 0 0 0 67910 104 0 0 25 0 1 0 491002522 145321984 34502 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35479 34502 603 41 0 35438 0
vsize: 141916
[startup+690.09 s]
Raw data (loadavg): 1.04 1.03 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 36287 0 0 0 68909 105 0 0 25 0 1 0 491002522 146808832 34863 4294967295 134512640 134672761 3221224624 3221223808 134559594 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35842 34863 603 41 0 35801 0
vsize: 143368
[startup+700.09 s]
Raw data (loadavg): 1.04 1.03 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 36635 0 0 0 69908 106 0 0 25 0 1 0 491002522 148254720 35211 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36195 35211 603 41 0 36154 0
vsize: 144780
[startup+710.09 s]
Raw data (loadavg): 1.03 1.03 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 36950 0 0 0 70907 108 0 0 25 0 1 0 491002522 149463040 35526 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36490 35526 603 41 0 36449 0
vsize: 145960
[startup+720.09 s]
Raw data (loadavg): 1.03 1.03 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 37320 0 0 0 71907 108 0 0 25 0 1 0 491002522 151064576 35896 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36881 35896 603 41 0 36840 0
vsize: 147524
[startup+730.091 s]
Raw data (loadavg): 1.02 1.02 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 37727 0 0 0 72906 109 0 0 25 0 1 0 491002522 152686592 36303 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37277 36303 603 41 0 37236 0
vsize: 149108
[startup+740.091 s]
Raw data (loadavg): 1.02 1.02 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 38081 0 0 0 73904 111 0 0 25 0 1 0 491002522 154169344 36657 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37639 36657 603 41 0 37598 0
vsize: 150556
[startup+750.091 s]
Raw data (loadavg): 1.01 1.02 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 38418 0 0 0 74904 112 0 0 25 0 1 0 491002522 155488256 36994 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37961 36994 603 41 0 37920 0
vsize: 151844
[startup+760.091 s]
Raw data (loadavg): 1.01 1.02 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 38737 0 0 0 75903 113 0 0 25 0 1 0 491002522 156831744 37313 4294967295 134512640 134672761 3221224624 3221223792 134560970 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38289 37313 603 41 0 38248 0
vsize: 153156
[startup+770.09 s]
Raw data (loadavg): 1.01 1.02 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 39058 0 0 0 76902 114 0 0 25 0 1 0 491002522 158154752 37634 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38612 37634 603 41 0 38571 0
vsize: 154448
[startup+780.094 s]
Raw data (loadavg): 1.01 1.02 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 39378 0 0 0 77902 115 0 0 25 0 1 0 491002522 159510528 37954 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38943 37954 603 41 0 38902 0
vsize: 155772
[startup+790.104 s]
Raw data (loadavg): 1.01 1.02 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 39674 0 0 0 78902 115 0 0 25 0 1 0 491002522 160612352 38250 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39212 38250 603 41 0 39171 0
vsize: 156848
[startup+800.104 s]
Raw data (loadavg): 1.00 1.02 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 40014 0 0 0 79901 117 0 0 25 0 1 0 491002522 162086912 38590 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39572 38591 603 41 0 39531 0
vsize: 158288
[startup+810.112 s]
Raw data (loadavg): 1.00 1.02 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 40358 0 0 0 80901 118 0 0 25 0 1 0 491002522 163438592 38934 4294967295 134512640 134672761 3221224624 3221223760 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39902 38934 603 41 0 39861 0
vsize: 159608
[startup+820.111 s]
Raw data (loadavg): 1.00 1.02 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 40735 0 0 0 81900 119 0 0 25 0 1 0 491002522 165044224 39311 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40294 39311 603 41 0 40253 0
vsize: 161176
[startup+830.111 s]
Raw data (loadavg): 1.00 1.02 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 41121 0 0 0 82899 120 0 0 25 0 1 0 491002522 166686720 39697 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40695 39697 603 41 0 40654 0
vsize: 162780
[startup+840.112 s]
Raw data (loadavg): 1.00 1.01 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 41468 0 0 0 83899 121 0 0 25 0 1 0 491002522 168030208 40044 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41023 40044 603 41 0 40982 0
vsize: 164092
[startup+850.113 s]
Raw data (loadavg): 1.00 1.01 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 41773 0 0 0 84898 121 0 0 25 0 1 0 491002522 169242624 40349 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41319 40349 603 41 0 41278 0
vsize: 165276
[startup+860.114 s]
Raw data (loadavg): 1.00 1.01 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 42045 0 0 0 85897 123 0 0 25 0 1 0 491002522 170323968 40621 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41583 40621 603 41 0 41542 0
vsize: 166332
[startup+870.114 s]
Raw data (loadavg): 1.00 1.01 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 42337 0 0 0 86896 124 0 0 25 0 1 0 491002522 171532288 40913 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41878 40913 603 41 0 41837 0
vsize: 167512
[startup+880.119 s]
Raw data (loadavg): 1.00 1.01 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 42636 0 0 0 87896 125 0 0 25 0 1 0 491002522 172863488 41212 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42203 41212 603 41 0 42162 0
vsize: 168812
[startup+890.119 s]
Raw data (loadavg): 1.00 1.01 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 42924 0 0 0 88895 126 0 0 25 0 1 0 491002522 173928448 41500 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42463 41500 603 41 0 42422 0
vsize: 169852
[startup+900.119 s]
Raw data (loadavg): 1.00 1.01 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 43221 0 0 0 89893 127 0 0 25 0 1 0 491002522 175132672 41797 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42757 41797 603 41 0 42716 0
vsize: 171028
[startup+910.121 s]
Raw data (loadavg): 1.00 1.01 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 43568 0 0 0 90892 129 0 0 25 0 1 0 491002522 176611328 42144 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43118 42144 603 41 0 43077 0
vsize: 172472
[startup+920.121 s]
Raw data (loadavg): 1.00 1.01 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 43897 0 0 0 91891 130 0 0 25 0 1 0 491002522 177938432 42473 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43442 42473 603 41 0 43401 0
vsize: 173768
[startup+930.121 s]
Raw data (loadavg): 1.00 1.01 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 44213 0 0 0 92890 131 0 0 25 0 1 0 491002522 179167232 42789 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43742 42789 603 41 0 43701 0
vsize: 174968
[startup+940.121 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 44533 0 0 0 93890 131 0 0 25 0 1 0 491002522 180518912 43109 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44072 43109 603 41 0 44031 0
vsize: 176288
[startup+950.121 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 44855 0 0 0 94889 132 0 0 25 0 1 0 491002522 181862400 43431 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44400 43431 603 41 0 44359 0
vsize: 177600
[startup+960.121 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 45260 0 0 0 95888 133 0 0 25 0 1 0 491002522 183492608 43836 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44798 43836 603 41 0 44757 0
vsize: 179192
[startup+970.121 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 45670 0 0 0 96888 134 0 0 25 0 1 0 491002522 185237504 44246 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45224 44246 603 41 0 45183 0
vsize: 180896
[startup+980.121 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 46007 0 0 0 97887 135 0 0 25 0 1 0 491002522 186576896 44583 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45551 44583 603 41 0 45510 0
vsize: 182204
[startup+990.134 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 46336 0 0 0 98888 136 0 0 25 0 1 0 491002522 187924480 44912 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45880 44912 603 41 0 45839 0
vsize: 183520
[startup+1000.13 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 46652 0 0 0 99887 136 0 0 25 0 1 0 491002522 189263872 45228 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46207 45228 603 41 0 46166 0
vsize: 184828
[startup+1010.13 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 46969 0 0 0 100886 138 0 0 25 0 1 0 491002522 190472192 45545 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46502 45545 603 41 0 46461 0
vsize: 186008
[startup+1020.15 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 47268 0 0 0 101886 139 0 0 25 0 1 0 491002522 191680512 45844 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46797 45844 603 41 0 46756 0
vsize: 187188
[startup+1030.15 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 47536 0 0 0 102885 140 0 0 25 0 1 0 491002522 192749568 46112 4294967295 134512640 134672761 3221224624 3221223792 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47058 46112 603 41 0 47017 0
vsize: 188232
[startup+1040.15 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 47837 0 0 0 103885 141 0 0 25 0 1 0 491002522 194080768 46413 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47383 46413 603 41 0 47342 0
vsize: 189532
[startup+1050.15 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 48135 0 0 0 104884 142 0 0 25 0 1 0 491002522 195268608 46711 4294967295 134512640 134672761 3221224624 3221223824 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47673 46711 603 41 0 47632 0
vsize: 190692
[startup+1060.16 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 48451 0 0 0 105884 143 0 0 25 0 1 0 491002522 196603904 47027 4294967295 134512640 134672761 3221224624 3221223792 134561127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47999 47027 603 41 0 47958 0
vsize: 191996
[startup+1070.16 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 48746 0 0 0 106883 144 0 0 25 0 1 0 491002522 197808128 47322 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48293 47322 603 41 0 48252 0
vsize: 193172
[startup+1080.16 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 49023 0 0 0 107883 145 0 0 25 0 1 0 491002522 198889472 47599 4294967295 134512640 134672761 3221224624 3221223728 134559902 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48557 47599 603 41 0 48516 0
vsize: 194228
[startup+1090.17 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 49303 0 0 0 108882 146 0 0 25 0 1 0 491002522 200097792 47879 4294967295 134512640 134672761 3221224624 3221223728 134560022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48852 47879 603 41 0 48811 0
vsize: 195408
[startup+1100.17 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 49591 0 0 0 109882 147 0 0 25 0 1 0 491002522 201281536 48167 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49141 48167 603 41 0 49100 0
vsize: 196564
[startup+1110.17 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 49877 0 0 0 110881 147 0 0 25 0 1 0 491002522 202354688 48453 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49403 48453 603 41 0 49362 0
vsize: 197612
[startup+1120.17 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 50204 0 0 0 111881 148 0 0 25 0 1 0 491002522 203702272 48780 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49732 48780 603 41 0 49691 0
vsize: 198928
[startup+1130.17 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 50571 0 0 0 112880 148 0 0 25 0 1 0 491002522 205185024 49147 4294967295 134512640 134672761 3221224624 3221223728 134559976 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50094 49147 603 41 0 50053 0
vsize: 200376
[startup+1140.17 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 50932 0 0 0 113879 150 0 0 25 0 1 0 491002522 206659584 49508 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50454 49508 603 41 0 50413 0
vsize: 201816
[startup+1150.17 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 51241 0 0 0 114878 151 0 0 25 0 1 0 491002522 208003072 49817 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50782 49817 603 41 0 50741 0
vsize: 203128
[startup+1160.17 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 51561 0 0 0 115878 152 0 0 25 0 1 0 491002522 209338368 50137 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51108 50137 603 41 0 51067 0
vsize: 204432
[startup+1170.17 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 51882 0 0 0 116877 152 0 0 25 0 1 0 491002522 210550784 50458 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51404 50458 603 41 0 51363 0
vsize: 205616
[startup+1180.17 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 52175 0 0 0 117876 153 0 0 25 0 1 0 491002522 211755008 50751 4294967295 134512640 134672761 3221224624 3221223640 1075353266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51698 50751 603 41 0 51657 0
vsize: 206792
[startup+1190.17 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 52471 0 0 0 118876 154 0 0 25 0 1 0 491002522 212967424 51047 4294967295 134512640 134672761 3221224624 3221223728 134560169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51994 51047 603 41 0 51953 0
vsize: 207976
[startup+1200.17 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 20515
Raw data (stat): 20458 (minisat+) R 20457 29151 29150 0 -1 0 52798 0 0 0 119875 155 0 0 25 0 1 0 491002522 214298624 51374 4294967295 134512640 134672761 3221224624 3221223728 134559890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52319 51374 603 41 0 52278 0
vsize: 209276
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.27 s]
Raw data (loadavg): 1.00 1.00 0.96 1/54 20515
Raw data (stat): 20458 (minisat+) Z 20457 29151 29150 0 -1 12 52801 0 0 0 119875 164 0 0 25 0 1 0 491002522 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.27
CPU time (s): 1200.41
CPU user time (s): 1198.76
CPU system time (s): 1.64975
CPU usage (%): 100.011
Max. virtual memory (Kb): 209276
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####