PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-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	912
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.97
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 18378

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc29 THE 2005-04-21 14:37:15 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18140 boxname=wulflinc29 idbench=1396 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  130bea0863cb3f92addf09aabe15daa3  /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-10teams.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-10teams.opb
IDLAUNCH: 18140
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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.020
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:        874368 kB
Buffers:          7052 kB
Cached:         130572 kB
SwapCached:        552 kB
Active:          27832 kB
Inactive:       111796 kB
HighTotal:      131008 kB
HighFree:        40460 kB
LowTotal:       903652 kB
LowFree:        833908 kB
SwapTotal:     2097892 kB
SwapFree:      2096432 kB
Dirty:              52 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            14884 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 14:57:17 (client local time) WITH STATUS 10 IN 1200.4 SECONDS
stats: 18140 7 1200.4 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.88 0.97 0.93 2/54 372
Raw data (stat): 372 (runsolver) R 371 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 545851048 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.89 0.97 0.93 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 2693 0 0 0 991 6 0 0 25 0 1 0 545851048 13152256 2654 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3211 2654 603 41 0 3170 0
vsize: 12844
[startup+20.0008 s]
Raw data (loadavg): 0.91 0.97 0.93 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 9231 0 0 0 1976 21 0 0 25 0 1 0 545851048 36073472 7871 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8807 7871 603 41 0 8766 0
vsize: 35228
[startup+30.002 s]
Raw data (loadavg): 0.92 0.97 0.93 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 9638 0 0 0 2974 23 0 0 25 0 1 0 545851048 37834752 8278 4294967295 134512640 134672761 3221224624 3221223728 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9237 8278 603 41 0 9196 0
vsize: 36948
[startup+40.0028 s]
Raw data (loadavg): 0.93 0.97 0.93 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 10107 0 0 0 3972 25 0 0 25 0 1 0 545851048 39727104 8747 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9699 8747 603 41 0 9658 0
vsize: 38796
[startup+50.003 s]
Raw data (loadavg): 0.94 0.97 0.93 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 10623 0 0 0 4970 26 0 0 25 0 1 0 545851048 41746432 9263 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10192 9263 603 41 0 10151 0
vsize: 40768
[startup+60.0031 s]
Raw data (loadavg): 0.95 0.97 0.93 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 11017 0 0 0 5969 27 0 0 25 0 1 0 545851048 43364352 9657 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10587 9657 603 41 0 10546 0
vsize: 42348
[startup+70.0039 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 11443 0 0 0 6968 29 0 0 25 0 1 0 545851048 44765184 10019 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10929 10019 603 41 0 10888 0
vsize: 43716
[startup+80.0044 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 11820 0 0 0 7966 30 0 0 25 0 1 0 545851048 46362624 10396 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11319 10396 603 41 0 11278 0
vsize: 45276
[startup+90.0045 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 12306 0 0 0 8965 31 0 0 25 0 1 0 545851048 48365568 10882 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11808 10882 603 41 0 11767 0
vsize: 47232
[startup+100.004 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 12700 0 0 0 9965 32 0 0 25 0 1 0 545851048 49987584 11276 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12204 11276 603 41 0 12163 0
vsize: 48816
[startup+110.005 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 13106 0 0 0 10964 33 0 0 25 0 1 0 545851048 51728384 11682 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12629 11682 603 41 0 12588 0
vsize: 50516
[startup+120.005 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 13570 0 0 0 11963 34 0 0 25 0 1 0 545851048 53612544 12146 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13089 12146 603 41 0 13048 0
vsize: 52356
[startup+130.006 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 14057 0 0 0 12962 35 0 0 25 0 1 0 545851048 55492608 12633 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13548 12633 603 41 0 13507 0
vsize: 54192
[startup+140.005 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 14467 0 0 0 13961 36 0 0 25 0 1 0 545851048 57217024 13043 4294967295 134512640 134672761 3221224624 3221223728 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13969 13043 603 41 0 13928 0
vsize: 55876
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 14871 0 0 0 14961 36 0 0 25 0 1 0 545851048 58822656 13447 4294967295 134512640 134672761 3221224624 3221223760 134560667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14361 13447 603 41 0 14320 0
vsize: 57444
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 15308 0 0 0 15961 37 0 0 25 0 1 0 545851048 60698624 13884 4294967295 134512640 134672761 3221224624 3221223808 134559038 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14819 13884 603 41 0 14778 0
vsize: 59276
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 15716 0 0 0 16960 38 0 0 25 0 1 0 545851048 62283776 14292 4294967295 134512640 134672761 3221224624 3221223792 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15206 14292 603 41 0 15165 0
vsize: 60824
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 16123 0 0 0 17959 39 0 0 25 0 1 0 545851048 64147456 14699 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15661 14699 603 41 0 15620 0
vsize: 62644
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 16573 0 0 0 18958 41 0 0 25 0 1 0 545851048 65904640 15149 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16090 15149 603 41 0 16049 0
vsize: 64360
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 16989 0 0 0 19957 42 0 0 25 0 1 0 545851048 67653632 15565 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16517 15565 603 41 0 16476 0
vsize: 66068
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 17398 0 0 0 20956 43 0 0 25 0 1 0 545851048 69386240 15974 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16940 15974 603 41 0 16899 0
vsize: 67760
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 17749 0 0 0 21954 45 0 0 25 0 1 0 545851048 70721536 16325 4294967295 134512640 134672761 3221224624 3221223728 134555128 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17266 16325 603 41 0 17225 0
vsize: 69064
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 18109 0 0 0 22954 46 0 0 25 0 1 0 545851048 72192000 16685 4294967295 134512640 134672761 3221224624 3221223728 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17625 16685 603 41 0 17584 0
vsize: 70500
[startup+240.007 s]
Raw data (loadavg): 1.07 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 18450 0 0 0 23953 47 0 0 25 0 1 0 545851048 73666560 17026 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17985 17026 603 41 0 17944 0
vsize: 71940
[startup+250.007 s]
Raw data (loadavg): 1.06 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 18825 0 0 0 24952 48 0 0 25 0 1 0 545851048 75141120 17401 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18345 17401 603 41 0 18304 0
vsize: 73380
[startup+260.008 s]
Raw data (loadavg): 1.05 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 19255 0 0 0 25950 50 0 0 25 0 1 0 545851048 76877824 17831 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18769 17831 603 41 0 18728 0
vsize: 75076
[startup+270.007 s]
Raw data (loadavg): 1.04 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 19627 0 0 0 26949 51 0 0 25 0 1 0 545851048 78483456 18203 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19161 18203 603 41 0 19120 0
vsize: 76644
[startup+280.007 s]
Raw data (loadavg): 1.04 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 20016 0 0 0 27948 52 0 0 25 0 1 0 545851048 79953920 18592 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19520 18592 603 41 0 19479 0
vsize: 78080
[startup+290.008 s]
Raw data (loadavg): 1.03 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 20437 0 0 0 28947 53 0 0 25 0 1 0 545851048 81698816 19013 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19946 19013 603 41 0 19905 0
vsize: 79784
[startup+300.008 s]
Raw data (loadavg): 1.03 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 20885 0 0 0 29946 55 0 0 25 0 1 0 545851048 83582976 19461 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20406 19461 603 41 0 20365 0
vsize: 81624
[startup+310.009 s]
Raw data (loadavg): 1.02 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 21298 0 0 0 30945 56 0 0 25 0 1 0 545851048 85315584 19874 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20829 19874 603 41 0 20788 0
vsize: 83316
[startup+320.01 s]
Raw data (loadavg): 1.02 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 21687 0 0 0 31944 57 0 0 25 0 1 0 545851048 86794240 20263 4294967295 134512640 134672761 3221224624 3221223728 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21190 20263 603 41 0 21149 0
vsize: 84760
[startup+330.01 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 22085 0 0 0 32943 58 0 0 25 0 1 0 545851048 88506368 20661 4294967295 134512640 134672761 3221224624 3221223792 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21608 20661 603 41 0 21567 0
vsize: 86432
[startup+340.01 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 22487 0 0 0 33942 60 0 0 25 0 1 0 545851048 90116096 21063 4294967295 134512640 134672761 3221224624 3221223776 1074744278 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22001 21063 603 41 0 21960 0
vsize: 88004
[startup+350.016 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 22815 0 0 0 34942 60 0 0 25 0 1 0 545851048 91467776 21391 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22331 21391 603 41 0 22290 0
vsize: 89324
[startup+360.025 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 23191 0 0 0 35942 61 0 0 25 0 1 0 545851048 92946432 21767 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22692 21767 603 41 0 22651 0
vsize: 90768
[startup+370.025 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 23554 0 0 0 36941 62 0 0 25 0 1 0 545851048 94420992 22130 4294967295 134512640 134672761 3221224624 3221223640 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23052 22130 603 41 0 23011 0
vsize: 92208
[startup+380.027 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 23947 0 0 0 37941 63 0 0 25 0 1 0 545851048 96006144 22523 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23439 22523 603 41 0 23398 0
vsize: 93756
[startup+390.028 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 24328 0 0 0 38940 64 0 0 25 0 1 0 545851048 97624064 22904 4294967295 134512640 134672761 3221224624 3221223728 134559853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23834 22904 603 41 0 23793 0
vsize: 95336
[startup+400.028 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 24758 0 0 0 39939 65 0 0 25 0 1 0 545851048 99368960 23334 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24260 23334 603 41 0 24219 0
vsize: 97040
[startup+410.032 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 25203 0 0 0 40938 67 0 0 25 0 1 0 545851048 101253120 23779 4294967295 134512640 134672761 3221224624 3221223808 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24720 23779 603 41 0 24679 0
vsize: 98880
[startup+420.032 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 25678 0 0 0 41937 68 0 0 25 0 1 0 545851048 103149568 24254 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25183 24254 603 41 0 25142 0
vsize: 100732
[startup+430.033 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 26117 0 0 0 42936 69 0 0 25 0 1 0 545851048 104902656 24693 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25611 24693 603 41 0 25570 0
vsize: 102444
[startup+440.033 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 26532 0 0 0 43935 70 0 0 25 0 1 0 545851048 106651648 25108 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26038 25108 603 41 0 25997 0
vsize: 104152
[startup+450.032 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 26965 0 0 0 44934 72 0 0 25 0 1 0 545851048 108666880 25541 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26530 25541 603 41 0 26489 0
vsize: 106120
[startup+460.051 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 27408 0 0 0 45935 72 0 0 25 0 1 0 545851048 110444544 25984 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26964 25984 603 41 0 26923 0
vsize: 107856
[startup+470.05 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 27833 0 0 0 46934 74 0 0 25 0 1 0 545851048 112201728 26409 4294967295 134512640 134672761 3221224624 3221223808 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27393 26409 603 41 0 27352 0
vsize: 109572
[startup+480.05 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 28290 0 0 0 47933 75 0 0 25 0 1 0 545851048 114098176 26866 4294967295 134512640 134672761 3221224624 3221223728 134559933 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27856 26867 603 41 0 27815 0
vsize: 111424
[startup+490.051 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 28695 0 0 0 48932 76 0 0 25 0 1 0 545851048 115712000 27271 4294967295 134512640 134672761 3221224624 3221223728 134559966 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28250 27271 603 41 0 28209 0
vsize: 113000
[startup+500.05 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 29136 0 0 0 49932 76 0 0 25 0 1 0 545851048 117481472 27712 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28682 27712 603 41 0 28641 0
vsize: 114728
[startup+510.051 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 29590 0 0 0 50931 78 0 0 25 0 1 0 545851048 119369728 28166 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29143 28166 603 41 0 29102 0
vsize: 116572
[startup+520.05 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 30020 0 0 0 51930 78 0 0 25 0 1 0 545851048 121135104 28596 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29574 28596 603 41 0 29533 0
vsize: 118296
[startup+530.051 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 30473 0 0 0 52930 79 0 0 25 0 1 0 545851048 123035648 29049 4294967295 134512640 134672761 3221224624 3221223808 134559041 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.051 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 30927 0 0 0 53929 80 0 0 25 0 1 0 545851048 124801024 29503 4294967295 134512640 134672761 3221224624 3221223792 134560813 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.052 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 31240 0 0 0 54928 80 0 0 25 0 1 0 545851048 126136320 29816 4294967295 134512640 134672761 3221224624 3221223708 1075346528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30795 29816 603 41 0 30754 0
vsize: 123180
[startup+560.052 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 31591 0 0 0 55925 82 0 0 25 0 1 0 545851048 127614976 30167 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31156 30167 603 41 0 31115 0
vsize: 124624
[startup+570.053 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 31966 0 0 0 56925 83 0 0 25 0 1 0 545851048 129093632 30542 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31517 30542 603 41 0 31476 0
vsize: 126068
[startup+580.053 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 32346 0 0 0 57924 84 0 0 25 0 1 0 545851048 130707456 30922 4294967295 134512640 134672761 3221224624 3221223808 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31911 30922 603 41 0 31870 0
vsize: 127644
[startup+590.053 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 32703 0 0 0 58924 85 0 0 25 0 1 0 545851048 132161536 31279 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32266 31279 603 41 0 32225 0
vsize: 129064
[startup+600.053 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 33094 0 0 0 59923 86 0 0 25 0 1 0 545851048 133775360 31670 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32660 31670 603 41 0 32619 0
vsize: 130640
[startup+610.053 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 33474 0 0 0 60922 87 0 0 25 0 1 0 545851048 135229440 32050 4294967295 134512640 134672761 3221224624 3221223728 134560289 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.053 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 33823 0 0 0 61921 87 0 0 25 0 1 0 545851048 136708096 32399 4294967295 134512640 134672761 3221224624 3221223792 134560830 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.053 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 34183 0 0 0 62920 89 0 0 25 0 1 0 545851048 138182656 32759 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33736 32759 603 41 0 33695 0
vsize: 134944
[startup+640.054 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 34558 0 0 0 63920 90 0 0 25 0 1 0 545851048 139649024 33134 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34094 33134 603 41 0 34053 0
vsize: 136376
[startup+650.053 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 34913 0 0 0 64919 90 0 0 25 0 1 0 545851048 141213696 33489 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34476 33489 603 41 0 34435 0
vsize: 137904
[startup+660.054 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 35279 0 0 0 65918 91 0 0 25 0 1 0 545851048 142655488 33855 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34828 33855 603 41 0 34787 0
vsize: 139312
[startup+670.054 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 35604 0 0 0 66918 91 0 0 25 0 1 0 545851048 144003072 34180 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35157 34180 603 41 0 35116 0
vsize: 140628
[startup+680.055 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 35938 0 0 0 67918 92 0 0 25 0 1 0 545851048 145321984 34514 4294967295 134512640 134672761 3221224624 3221223728 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35479 34514 603 41 0 35438 0
vsize: 141916
[startup+690.055 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 36300 0 0 0 68917 93 0 0 25 0 1 0 545851048 146808832 34876 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35842 34876 603 41 0 35801 0
vsize: 143368
[startup+700.055 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 36645 0 0 0 69916 94 0 0 25 0 1 0 545851048 148254720 35221 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36195 35221 603 41 0 36154 0
vsize: 144780
[startup+710.056 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 36968 0 0 0 70916 95 0 0 25 0 1 0 545851048 149598208 35544 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36523 35544 603 41 0 36482 0
vsize: 146092
[startup+720.056 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 37337 0 0 0 71915 96 0 0 25 0 1 0 545851048 151064576 35913 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36881 35913 603 41 0 36840 0
vsize: 147524
[startup+730.057 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 37746 0 0 0 72914 97 0 0 25 0 1 0 545851048 152821760 36322 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37310 36322 603 41 0 37269 0
vsize: 149240
[startup+740.057 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 38100 0 0 0 73914 98 0 0 25 0 1 0 545851048 154169344 36676 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37639 36676 603 41 0 37598 0
vsize: 150556
[startup+750.057 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 38435 0 0 0 74913 99 0 0 25 0 1 0 545851048 155623424 37011 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37994 37011 603 41 0 37953 0
vsize: 151976
[startup+760.058 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 38756 0 0 0 75912 100 0 0 25 0 1 0 545851048 156966912 37332 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38322 37332 603 41 0 38281 0
vsize: 153288
[startup+770.058 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 39076 0 0 0 76912 100 0 0 25 0 1 0 545851048 158154752 37652 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38612 37652 603 41 0 38571 0
vsize: 154448
[startup+780.064 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 39397 0 0 0 77912 101 0 0 25 0 1 0 545851048 159510528 37973 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38943 37973 603 41 0 38902 0
vsize: 155772
[startup+790.064 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 39697 0 0 0 78912 101 0 0 25 0 1 0 545851048 160747520 38273 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39245 38273 603 41 0 39204 0
vsize: 156980
[startup+800.064 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 40050 0 0 0 79911 102 0 0 25 0 1 0 545851048 162222080 38626 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39605 38626 603 41 0 39564 0
vsize: 158420
[startup+810.068 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 40395 0 0 0 80911 103 0 0 25 0 1 0 545851048 163704832 38971 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39967 38971 603 41 0 39926 0
vsize: 159868
[startup+820.067 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 40770 0 0 0 81910 104 0 0 25 0 1 0 545851048 165179392 39346 4294967295 134512640 134672761 3221224624 3221223728 134560361 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40327 39346 603 41 0 40286 0
vsize: 161308
[startup+830.068 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 41151 0 0 0 82909 105 0 0 25 0 1 0 545851048 166686720 39727 4294967295 134512640 134672761 3221224624 3221223728 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40695 39727 603 41 0 40654 0
vsize: 162780
[startup+840.068 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 41501 0 0 0 83909 106 0 0 25 0 1 0 545851048 168165376 40077 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41056 40077 603 41 0 41015 0
vsize: 164224
[startup+850.078 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 41803 0 0 0 84909 107 0 0 25 0 1 0 545851048 169377792 40379 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41352 40379 603 41 0 41311 0
vsize: 165408
[startup+860.079 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 42074 0 0 0 85908 108 0 0 25 0 1 0 545851048 170459136 40650 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41616 40650 603 41 0 41575 0
vsize: 166464
[startup+870.079 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 42372 0 0 0 86907 109 0 0 25 0 1 0 545851048 171663360 40948 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41910 40948 603 41 0 41869 0
vsize: 167640
[startup+880.08 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 42676 0 0 0 87907 109 0 0 25 0 1 0 545851048 172990464 41252 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42234 41252 603 41 0 42193 0
vsize: 168936
[startup+890.08 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 42957 0 0 0 88906 110 0 0 25 0 1 0 545851048 174063616 41533 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42496 41533 603 41 0 42455 0
vsize: 169984
[startup+900.08 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 43273 0 0 0 89905 111 0 0 25 0 1 0 545851048 175394816 41849 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42821 41849 603 41 0 42780 0
vsize: 171284
[startup+910.081 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 43609 0 0 0 90904 112 0 0 25 0 1 0 545851048 176742400 42185 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43150 42185 603 41 0 43109 0
vsize: 172600
[startup+920.082 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 43928 0 0 0 91904 113 0 0 25 0 1 0 545851048 178069504 42504 4294967295 134512640 134672761 3221224624 3221223792 134561148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43474 42504 603 41 0 43433 0
vsize: 173896
[startup+930.082 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 44247 0 0 0 92903 114 0 0 25 0 1 0 545851048 179437568 42823 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43808 42823 603 41 0 43767 0
vsize: 175232
[startup+940.093 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 44567 0 0 0 93903 115 0 0 25 0 1 0 545851048 180654080 43143 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44105 43143 603 41 0 44064 0
vsize: 176420
[startup+950.111 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 44901 0 0 0 94904 116 0 0 25 0 1 0 545851048 182001664 43477 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44434 43477 603 41 0 44393 0
vsize: 177736
[startup+960.137 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 45315 0 0 0 95906 117 0 0 25 0 1 0 545851048 183767040 43891 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44865 43891 603 41 0 44824 0
vsize: 179460
[startup+970.136 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 45726 0 0 0 96904 118 0 0 25 0 1 0 545851048 185356288 44302 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45253 44302 603 41 0 45212 0
vsize: 181012
[startup+980.148 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 46049 0 0 0 97904 119 0 0 25 0 1 0 545851048 186712064 44625 4294967295 134512640 134672761 3221224624 3221223728 134560158 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45584 44625 603 41 0 45543 0
vsize: 182336
[startup+990.161 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 46380 0 0 0 98904 120 0 0 25 0 1 0 545851048 188051456 44956 4294967295 134512640 134672761 3221224624 3221223808 134559041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45911 44957 603 41 0 45870 0
vsize: 183644
[startup+1000.16 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 46701 0 0 0 99903 122 0 0 25 0 1 0 545851048 189399040 45277 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46240 45277 603 41 0 46199 0
vsize: 184960
[startup+1010.16 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 47010 0 0 0 100903 123 0 0 25 0 1 0 545851048 190607360 45586 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46535 45586 603 41 0 46494 0
vsize: 186140
[startup+1020.16 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 47306 0 0 0 101903 123 0 0 25 0 1 0 545851048 191815680 45882 4294967295 134512640 134672761 3221224624 3221223808 134559482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46830 45882 603 41 0 46789 0
vsize: 187320
[startup+1030.16 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 47588 0 0 0 102902 124 0 0 25 0 1 0 545851048 193019904 46164 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47124 46164 603 41 0 47083 0
vsize: 188496
[startup+1040.16 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 47881 0 0 0 103902 124 0 0 25 0 1 0 545851048 194207744 46457 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47414 46457 603 41 0 47373 0
vsize: 189656
[startup+1050.16 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 48184 0 0 0 104901 125 0 0 25 0 1 0 545851048 195399680 46760 4294967295 134512640 134672761 3221224624 3221223728 134559991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47705 46760 603 41 0 47664 0
vsize: 190820
[startup+1060.16 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 48490 0 0 0 105900 127 0 0 25 0 1 0 545851048 196734976 47066 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48031 47066 603 41 0 47990 0
vsize: 192124
[startup+1070.16 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 48791 0 0 0 106899 127 0 0 25 0 1 0 545851048 197943296 47367 4294967295 134512640 134672761 3221224624 3221223728 134560276 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48326 47367 603 41 0 48285 0
vsize: 193304
[startup+1080.16 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 49070 0 0 0 107899 128 0 0 25 0 1 0 545851048 199151616 47646 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48621 47646 603 41 0 48580 0
vsize: 194484
[startup+1090.16 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 49360 0 0 0 108898 129 0 0 25 0 1 0 545851048 200224768 47936 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48883 47936 603 41 0 48842 0
vsize: 195532
[startup+1100.16 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 49640 0 0 0 109898 129 0 0 25 0 1 0 545851048 201416704 48216 4294967295 134512640 134672761 3221224624 3221223792 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49174 48216 603 41 0 49133 0
vsize: 196696
[startup+1110.16 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 49940 0 0 0 110897 130 0 0 25 0 1 0 545851048 202629120 48516 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49470 48516 603 41 0 49429 0
vsize: 197880
[startup+1120.16 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 50270 0 0 0 111896 131 0 0 25 0 1 0 545851048 203972608 48846 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49798 48846 603 41 0 49757 0
vsize: 199192
[startup+1130.17 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 50649 0 0 0 112896 132 0 0 25 0 1 0 545851048 205590528 49225 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50193 49225 603 41 0 50152 0
vsize: 200772
[startup+1140.17 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 50999 0 0 0 113895 133 0 0 25 0 1 0 545851048 206929920 49575 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50520 49575 603 41 0 50479 0
vsize: 202080
[startup+1150.16 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 51305 0 0 0 114895 133 0 0 25 0 1 0 545851048 208277504 49881 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50849 49881 603 41 0 50808 0
vsize: 203396
[startup+1160.17 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 51646 0 0 0 115894 134 0 0 25 0 1 0 545851048 209608704 50222 4294967295 134512640 134672761 3221224624 3221223728 134559933 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51174 50222 603 41 0 51133 0
vsize: 204696
[startup+1170.17 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 51943 0 0 0 116894 135 0 0 25 0 1 0 545851048 210821120 50519 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51470 50519 603 41 0 51429 0
vsize: 205880
[startup+1180.17 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 52245 0 0 0 117893 135 0 0 25 0 1 0 545851048 212025344 50821 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51764 50821 603 41 0 51723 0
vsize: 207056
[startup+1190.17 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 52533 0 0 0 118893 136 0 0 25 0 1 0 545851048 213225472 51109 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52057 51109 603 41 0 52016 0
vsize: 208228
[startup+1200.17 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 372
Raw data (stat): 372 (minisat+) R 371 27222 27221 0 -1 0 52876 0 0 0 119892 137 0 0 25 0 1 0 545851048 214700032 51452 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52417 51452 603 41 0 52376 0
vsize: 209668
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.27 s]
Raw data (loadavg): 1.00 0.99 0.94 1/54 372
Raw data (stat): 372 (minisat+) Z 371 27222 27221 0 -1 12 52879 0 0 0 119892 147 0 0 25 0 1 0 545851048 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.4
CPU user time (s): 1198.93
CPU system time (s): 1.47578
CPU usage (%): 100.011
Max. virtual memory (Kb): 209668
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####