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 21471

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc18 THE 2005-04-21 23:56:42 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13156 boxname=wulflinc18 idbench=1012 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  130bea0863cb3f92addf09aabe15daa3  /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-10teams.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-10teams.opb /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-10teams.opb
IDLAUNCH: 13156
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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.177
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:        440652 kB
Buffers:         27892 kB
Cached:         542952 kB
SwapCached:        764 kB
Active:         181476 kB
Inactive:       391372 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        440400 kB
SwapTotal:     2097892 kB
SwapFree:      2096152 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            15444 kB
Committed_AS:    63804 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 00:16:45 (client local time) WITH STATUS 10 IN 1200.36 SECONDS
stats: 13156 7 1200.36 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 |   96879   272271 |   32293       0        0     nan |  0.000 % |
c |       101 |   96879   272271 |   35522     101      967     9.6 |  1.808 % |
c |       251 |   96879   272271 |   39074     251    15560    62.0 |  1.808 % |
c |       476 |   96859   272211 |   42981     461    20922    45.4 |  1.825 % |
c |       814 |   96859   272211 |   47280     799    66018    82.6 |  1.825 % |
c |      1321 |   96859   272211 |   52008    1306   126690    97.0 |  1.825 % |
c |      2080 |   96824   272106 |   57209    2026   204576   101.0 |  1.856 % |
c |      3219 |   96797   272025 |   62929    3128   342205   109.4 |  1.878 % |
c |      4927 |   96797   272025 |   69222    4836   478953    99.0 |  1.878 % |
c |      7493 |   96733   271837 |   76145    7313   886114   121.2 |  1.935 % |
c |     11338 |   96733   271837 |   83759   11158  1485894   133.2 |  1.935 % |
c ==============================================================================
c [1mFound solution: 1002[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 7750   maxlim: 38998   bits: 16/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13502 |  150826   465059 |   50275   13201  1752710   132.8 |  1.935 % |
c |     13602 |  150816   465029 |   55302   13291  1755401   132.1 |  1.537 % |
c |     13752 |  150816   465029 |   60832   13441  1758879   130.9 |  1.537 % |
c |     13979 |  150816   465029 |   66916   13668  1766286   129.2 |  1.537 % |
c |     14318 |  150802   464989 |   73607   13984  1792741   128.2 |  1.547 % |
c |     14824 |  150797   464974 |   80968   14488  1877274   129.6 |  1.551 % |
c ==============================================================================
c [1mFound solution: 954[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 39046   bits: 16/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15322 |  150798   464996 |   50266   14974  1929135   128.8 |  1.551 % |
c |     15425 |  150798   464996 |   55292   15077  1930454   128.0 |  1.570 % |
c |     15576 |  150798   464996 |   60821   15228  1948982   128.0 |  1.570 % |
c |     15804 |  150784   464958 |   66904   15447  1959100   126.8 |  1.580 % |
c |     16141 |  150764   464898 |   73594   15757  1972279   125.2 |  1.593 % |
c |     16648 |  150739   464825 |   80953   16253  2035906   125.3 |  1.609 % |
c |     17423 |  150715   464757 |   89049   17016  2132837   125.3 |  1.626 % |
c |     18563 |  150701   464719 |   97954   18151  2329014   128.3 |  1.636 % |
c |     20275 |  150691   464689 |  107749   19847  2613250   131.7 |  1.642 % |
c |     22837 |  150637   464531 |  118524   22374  3010744   134.6 |  1.678 % |
c |     26683 |  150627   464501 |  130377   26207  3912167   149.3 |  1.685 % |
c |     32449 |  150608   464446 |  143414   31953  5128065   160.5 |  1.698 % |
c |     41098 |  150535   464227 |  157756   40216  6927844   172.3 |  1.744 % |
c |     54072 |  150315   463587 |  173531   52863  9224192   174.5 |  1.892 % |
c |     73534 |  149943   462473 |  190885   71782 13329193   185.7 |  2.132 % |
c |    102727 |  149532   461246 |  209973  100311 19710121   196.5 |  2.394 % |
c ==============================================================================
c [1mFound solution: 948[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 39052   bits: 16/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    115811 |  149292   460556 |   49764  113123 22734321   201.0 |  2.394 % |
c |    115911 |  149287   460541 |   54740   25375  3049145   120.2 |  2.565 % |
c |    116061 |  149275   460505 |   60214   25520  3080514   120.7 |  2.572 % |
c |    116286 |  149259   460457 |   66235   25743  3089063   120.0 |  2.581 % |
c |    116623 |  149259   460457 |   72859   26080  3126141   119.9 |  2.581 % |
c |    117130 |  149239   460397 |   80145   26576  3168858   119.2 |  2.595 % |
c |    117889 |  149214   460322 |   88159   27321  3290242   120.4 |  2.611 % |
c |    119029 |  149214   460322 |   96975   28461  3538289   124.3 |  2.611 % |
c |    120738 |  149203   460289 |  106673   30164  3865069   128.1 |  2.617 % |
c |    123302 |  149128   460064 |  117340   32651  4295278   131.6 |  2.667 % |
c |    127147 |  149054   459844 |  129074   36444  5104109   140.1 |  2.716 % |
c |    132913 |  148983   459635 |  141982   42176  5971945   141.6 |  2.762 % |
c |    141562 |  148707   458815 |  156180   50638  7514908   148.4 |  2.939 % |
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.85 0.96 0.91 2/55 11231
Raw data (stat): 11231 (runsolver) R 11230 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 549202429 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.87 0.96 0.91 2/55 11231
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 2821 0 0 0 992 6 0 0 25 0 1 0 549202429 13705216 2782 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3346 2782 603 41 0 3305 0
vsize: 13384
[startup+20.0014 s]
Raw data (loadavg): 0.89 0.96 0.91 2/55 11231
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 3238 0 0 0 1990 7 0 0 25 0 1 0 549202429 15482880 3199 4294967295 134512640 134672761 3221224544 3221223728 134559345 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3780 3199 603 41 0 3739 0
vsize: 15120
[startup+30.0021 s]
Raw data (loadavg): 0.91 0.96 0.91 2/55 11231
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 3643 0 0 0 2989 8 0 0 25 0 1 0 549202429 17117184 3604 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4179 3604 603 41 0 4138 0
vsize: 16716
[startup+40.0027 s]
Raw data (loadavg): 0.92 0.96 0.91 2/55 11231
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 4047 0 0 0 3989 9 0 0 25 0 1 0 549202429 18735104 4008 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4574 4008 603 41 0 4533 0
vsize: 18296
[startup+50.003 s]
Raw data (loadavg): 0.93 0.96 0.91 2/55 11231
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 10458 0 0 0 4974 23 0 0 25 0 1 0 549202429 41345024 9098 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10094 9098 603 41 0 10053 0
vsize: 40376
[startup+60.0028 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 11231
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 10825 0 0 0 5974 24 0 0 25 0 1 0 549202429 42590208 9397 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10398 9397 603 41 0 10357 0
vsize: 41592
[startup+70.0035 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 11231
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 11151 0 0 0 6973 25 0 0 25 0 1 0 549202429 43986944 9723 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10739 9723 603 41 0 10698 0
vsize: 42956
[startup+80.0037 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 11231
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 11453 0 0 0 7972 26 0 0 25 0 1 0 549202429 45195264 10025 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11034 10025 603 41 0 10993 0
vsize: 44136
[startup+90.0047 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 11231
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 11790 0 0 0 8971 27 0 0 25 0 1 0 549202429 46534656 10362 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11361 10362 603 41 0 11320 0
vsize: 45444
[startup+100.004 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 11231
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 12147 0 0 0 9970 28 0 0 25 0 1 0 549202429 48013312 10719 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11722 10719 603 41 0 11681 0
vsize: 46888
[startup+110.004 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 11231
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 12566 0 0 0 10970 29 0 0 25 0 1 0 549202429 49766400 11138 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12150 11138 603 41 0 12109 0
vsize: 48600
[startup+120.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 11231
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 12894 0 0 0 11969 29 0 0 25 0 1 0 549202429 51113984 11466 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12479 11466 603 41 0 12438 0
vsize: 49916
[startup+130.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 11231
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 13228 0 0 0 12968 31 0 0 25 0 1 0 549202429 52445184 11800 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12804 11800 603 41 0 12763 0
vsize: 51216
[startup+140.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 11231
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 13561 0 0 0 13967 32 0 0 25 0 1 0 549202429 53780480 12133 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13130 12133 603 41 0 13089 0
vsize: 52520
[startup+150.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 11231
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 13878 0 0 0 14966 33 0 0 25 0 1 0 549202429 55123968 12450 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13458 12450 603 41 0 13417 0
vsize: 53832
[startup+160.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11231
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 14235 0 0 0 15966 34 0 0 25 0 1 0 549202429 56594432 12807 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13817 12807 603 41 0 13776 0
vsize: 55268
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11231
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 14534 0 0 0 16965 34 0 0 25 0 1 0 549202429 57917440 13106 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14140 13106 603 41 0 14099 0
vsize: 56560
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11231
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 14820 0 0 0 17965 35 0 0 25 0 1 0 549202429 59125760 13392 4294967295 134512640 134672761 3221224544 3221223648 134560022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14435 13392 603 41 0 14394 0
vsize: 57740
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11231
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 15067 0 0 0 18964 36 0 0 25 0 1 0 549202429 60067840 13639 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14665 13639 603 41 0 14624 0
vsize: 58660
[startup+200.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11231
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 15418 0 0 0 19964 36 0 0 25 0 1 0 549202429 61538304 13990 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15024 13990 603 41 0 14983 0
vsize: 60096
[startup+210.008 s]
Raw data (loadavg): 1.15 1.00 0.92 2/55 11284
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 15702 0 0 0 20943 57 0 0 25 0 1 0 549202429 62619648 14274 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15288 14274 603 41 0 15247 0
vsize: 61152
[startup+220.009 s]
Raw data (loadavg): 1.12 1.00 0.92 2/55 11284
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 16011 0 0 0 21942 59 0 0 25 0 1 0 549202429 63954944 14583 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15614 14583 603 41 0 15573 0
vsize: 62456
[startup+230.009 s]
Raw data (loadavg): 1.10 1.00 0.92 2/55 11284
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 16299 0 0 0 22941 60 0 0 25 0 1 0 549202429 65163264 14871 4294967295 134512640 134672761 3221224544 3221223648 134560002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15909 14871 603 41 0 15868 0
vsize: 63636
[startup+240.009 s]
Raw data (loadavg): 1.09 1.00 0.92 2/55 11286
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 16576 0 0 0 23939 61 0 0 25 0 1 0 549202429 66236416 15148 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16171 15148 603 41 0 16130 0
vsize: 64684
[startup+250.01 s]
Raw data (loadavg): 1.07 1.00 0.92 2/55 11286
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 16809 0 0 0 24939 62 0 0 25 0 1 0 549202429 67170304 15381 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16399 15381 603 41 0 16358 0
vsize: 65596
[startup+260.01 s]
Raw data (loadavg): 1.06 1.00 0.92 2/55 11286
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 17100 0 0 0 25938 63 0 0 25 0 1 0 549202429 68378624 15672 4294967295 134512640 134672761 3221224544 3221223648 134560276 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16694 15672 603 41 0 16653 0
vsize: 66776
[startup+270.01 s]
Raw data (loadavg): 1.05 1.00 0.92 2/55 11288
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 17399 0 0 0 26936 65 0 0 25 0 1 0 549202429 69595136 15971 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16991 15971 603 41 0 16950 0
vsize: 67964
[startup+280.01 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 11288
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 17674 0 0 0 27935 66 0 0 25 0 1 0 549202429 70664192 16246 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17252 16246 603 41 0 17211 0
vsize: 69008
[startup+290.011 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 11288
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 17852 0 0 0 28935 67 0 0 25 0 1 0 549202429 71467008 16424 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17448 16424 603 41 0 17407 0
vsize: 69792
[startup+300.011 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 11288
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 18140 0 0 0 29934 68 0 0 25 0 1 0 549202429 72675328 16712 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17743 16712 603 41 0 17702 0
vsize: 70972
[startup+310.011 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 11288
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 18316 0 0 0 30933 68 0 0 25 0 1 0 549202429 73338880 16888 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17905 16888 603 41 0 17864 0
vsize: 71620
[startup+320.011 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 11288
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 18542 0 0 0 31933 69 0 0 25 0 1 0 549202429 74276864 17114 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18134 17114 603 41 0 18093 0
vsize: 72536
[startup+330.012 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 11288
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 18792 0 0 0 32931 71 0 0 25 0 1 0 549202429 75214848 17364 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18363 17364 603 41 0 18322 0
vsize: 73452
[startup+340.012 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 11288
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 19055 0 0 0 33930 72 0 0 25 0 1 0 549202429 76292096 17627 4294967295 134512640 134672761 3221224544 3221223680 134560604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18626 17627 603 41 0 18585 0
vsize: 74504
[startup+350.012 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 11288
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 19358 0 0 0 34930 73 0 0 25 0 1 0 549202429 77619200 17930 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18950 17930 603 41 0 18909 0
vsize: 75800
[startup+360.013 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 11288
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 19644 0 0 0 35929 74 0 0 25 0 1 0 549202429 78688256 18216 4294967295 134512640 134672761 3221224544 3221223728 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19211 18216 603 41 0 19170 0
vsize: 76844
[startup+370.013 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 11288
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 20015 0 0 0 36927 76 0 0 25 0 1 0 549202429 80293888 18587 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19603 18587 603 41 0 19562 0
vsize: 78412
[startup+380.013 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 11288
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 20183 0 0 0 37926 77 0 0 25 0 1 0 549202429 80965632 18755 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19767 18755 603 41 0 19726 0
vsize: 79068
[startup+390.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11288
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 20436 0 0 0 38926 77 0 0 25 0 1 0 549202429 82038784 19008 4294967295 134512640 134672761 3221224544 3221223720 134553585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20029 19008 603 41 0 19988 0
vsize: 80116
[startup+400.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11288
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 20668 0 0 0 39925 78 0 0 25 0 1 0 549202429 82968576 19240 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20256 19240 603 41 0 20215 0
vsize: 81024
[startup+410.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11288
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 20766 0 0 0 40925 79 0 0 25 0 1 0 549202429 83374080 19338 4294967295 134512640 134672761 3221224544 3221223712 134561226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20355 19338 603 41 0 20314 0
vsize: 81420
[startup+420.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11288
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 20984 0 0 0 41924 80 0 0 25 0 1 0 549202429 84172800 19556 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20550 19556 603 41 0 20509 0
vsize: 82200
[startup+430.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11288
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 21217 0 0 0 42923 81 0 0 25 0 1 0 549202429 85094400 19789 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20775 19789 603 41 0 20734 0
vsize: 83100
[startup+440.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11288
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 21425 0 0 0 43922 83 0 0 25 0 1 0 549202429 86294528 19997 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21068 19997 603 41 0 21027 0
vsize: 84272
[startup+450.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11288
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 21760 0 0 0 44921 83 0 0 25 0 1 0 549202429 87617536 20332 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21391 20332 603 41 0 21350 0
vsize: 85564
[startup+460.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11288
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 22011 0 0 0 45920 84 0 0 25 0 1 0 549202429 88690688 20583 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21653 20583 603 41 0 21612 0
vsize: 86612
[startup+470.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11288
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 22191 0 0 0 46920 85 0 0 25 0 1 0 549202429 89374720 20763 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21820 20763 603 41 0 21779 0
vsize: 87280
[startup+480.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11288
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 22419 0 0 0 47919 86 0 0 25 0 1 0 549202429 90312704 20991 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22049 20991 603 41 0 22008 0
vsize: 88196
[startup+490.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11288
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 22566 0 0 0 48918 87 0 0 25 0 1 0 549202429 90849280 21138 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22180 21138 603 41 0 22139 0
vsize: 88720
[startup+500.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11288
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 22806 0 0 0 49917 88 0 0 25 0 1 0 549202429 91918336 21378 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22441 21378 603 41 0 22400 0
vsize: 89764
[startup+510.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11288
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 23029 0 0 0 50916 90 0 0 25 0 1 0 549202429 92839936 21601 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22666 21601 603 41 0 22625 0
vsize: 90664
[startup+520.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11288
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 23301 0 0 0 51916 91 0 0 25 0 1 0 549202429 93908992 21873 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22927 21873 603 41 0 22886 0
vsize: 91708
[startup+530.037 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11288
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 23574 0 0 0 52916 92 0 0 25 0 1 0 549202429 94978048 22146 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23188 22146 603 41 0 23147 0
vsize: 92752
[startup+540.037 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11290
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 23685 0 0 0 53915 93 0 0 25 0 1 0 549202429 95518720 22257 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22257 603 41 0 23279 0
vsize: 93280
[startup+550.042 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11290
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 23971 0 0 0 54914 94 0 0 25 0 1 0 549202429 96583680 22543 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23580 22543 603 41 0 23539 0
vsize: 94320
[startup+560.043 s]
Raw data (loadavg): 1.07 1.02 0.93 2/55 11292
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 24140 0 0 0 55913 96 0 0 25 0 1 0 549202429 97386496 22712 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23776 22712 603 41 0 23735 0
vsize: 95104
[startup+570.052 s]
Raw data (loadavg): 1.06 1.02 0.93 2/55 11292
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 24393 0 0 0 56913 97 0 0 25 0 1 0 549202429 98332672 22965 4294967295 134512640 134672761 3221224544 3221223648 134560148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24007 22965 603 41 0 23966 0
vsize: 96028
[startup+580.063 s]
Raw data (loadavg): 1.05 1.01 0.93 2/55 11292
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 24568 0 0 0 57914 97 0 0 25 0 1 0 549202429 99135488 23140 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24203 23140 603 41 0 24162 0
vsize: 96812
[startup+590.064 s]
Raw data (loadavg): 1.04 1.01 0.93 2/55 11292
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 24770 0 0 0 58913 99 0 0 25 0 1 0 549202429 99938304 23342 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24399 23342 603 41 0 24358 0
vsize: 97596
[startup+600.066 s]
Raw data (loadavg): 1.04 1.01 0.93 2/55 11292
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 24928 0 0 0 59912 100 0 0 25 0 1 0 549202429 100478976 23500 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24531 23500 603 41 0 24490 0
vsize: 98124
[startup+610.065 s]
Raw data (loadavg): 1.03 1.01 0.93 2/55 11292
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 25200 0 0 0 60911 101 0 0 25 0 1 0 549202429 101691392 23772 4294967295 134512640 134672761 3221224544 3221223648 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24827 23772 603 41 0 24786 0
vsize: 99308
[startup+620.066 s]
Raw data (loadavg): 1.02 1.01 0.93 2/55 11292
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 25374 0 0 0 61910 102 0 0 25 0 1 0 549202429 102367232 23946 4294967295 134512640 134672761 3221224544 3221223712 134560845 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24992 23946 603 41 0 24951 0
vsize: 99968
[startup+630.066 s]
Raw data (loadavg): 1.02 1.01 0.93 2/55 11292
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 25563 0 0 0 62909 103 0 0 25 0 1 0 549202429 103165952 24135 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25187 24135 603 41 0 25146 0
vsize: 100748
[startup+640.066 s]
Raw data (loadavg): 1.02 1.01 0.93 2/55 11292
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 25787 0 0 0 63909 104 0 0 25 0 1 0 549202429 104095744 24359 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25414 24359 603 41 0 25373 0
vsize: 101656
[startup+650.067 s]
Raw data (loadavg): 1.01 1.01 0.93 2/55 11292
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 26067 0 0 0 64908 105 0 0 25 0 1 0 549202429 105164800 24639 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25675 24639 603 41 0 25634 0
vsize: 102700
[startup+660.071 s]
Raw data (loadavg): 1.01 1.01 0.93 2/55 11292
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 26169 0 0 0 65908 105 0 0 25 0 1 0 549202429 105566208 24741 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25773 24741 603 41 0 25732 0
vsize: 103092
[startup+670.072 s]
Raw data (loadavg): 1.01 1.01 0.93 2/55 11292
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 26356 0 0 0 66907 106 0 0 25 0 1 0 549202429 106369024 24928 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25969 24928 603 41 0 25928 0
vsize: 103876
[startup+680.072 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 11292
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 26650 0 0 0 67906 108 0 0 25 0 1 0 549202429 107569152 25222 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26262 25222 603 41 0 26221 0
vsize: 105048
[startup+690.073 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 11292
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 26869 0 0 0 68905 109 0 0 25 0 1 0 549202429 108498944 25441 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26489 25441 603 41 0 26448 0
vsize: 105956
[startup+700.074 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11292
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 27162 0 0 0 69904 110 0 0 25 0 1 0 549202429 109731840 25734 4294967295 134512640 134672761 3221224544 3221223648 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26790 25734 603 41 0 26749 0
vsize: 107160
[startup+710.073 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11292
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 27463 0 0 0 70903 111 0 0 25 0 1 0 549202429 110936064 26035 4294967295 134512640 134672761 3221224544 3221223680 134560703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27084 26035 603 41 0 27043 0
vsize: 108336
[startup+720.074 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11292
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 27706 0 0 0 71902 112 0 0 25 0 1 0 549202429 111874048 26278 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27313 26278 603 41 0 27272 0
vsize: 109252
[startup+730.074 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11292
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 27939 0 0 0 72901 113 0 0 25 0 1 0 549202429 112816128 26511 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27543 26511 603 41 0 27502 0
vsize: 110172
[startup+740.075 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11292
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 28119 0 0 0 73901 114 0 0 25 0 1 0 549202429 113627136 26691 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27741 26691 603 41 0 27700 0
vsize: 110964
[startup+750.075 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11292
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 28238 0 0 0 74901 114 0 0 25 0 1 0 549202429 114032640 26810 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27840 26810 603 41 0 27799 0
vsize: 111360
[startup+760.075 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11292
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 28288 0 0 0 75901 115 0 0 25 0 1 0 549202429 114298880 26860 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27905 26860 603 41 0 27864 0
vsize: 111620
[startup+770.076 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11292
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 28406 0 0 0 76900 116 0 0 25 0 1 0 549202429 114700288 26978 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28003 26978 603 41 0 27962 0
vsize: 112012
[startup+780.076 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11292
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 28610 0 0 0 77899 117 0 0 25 0 1 0 549202429 115638272 27182 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28232 27182 603 41 0 28191 0
vsize: 112928
[startup+790.077 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11292
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 28888 0 0 0 78898 118 0 0 25 0 1 0 549202429 116682752 27460 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28487 27460 603 41 0 28446 0
vsize: 113948
[startup+800.078 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11292
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 29193 0 0 0 79897 120 0 0 25 0 1 0 549202429 118022144 27765 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28814 27765 603 41 0 28773 0
vsize: 115256
[startup+810.078 s]
Raw data (loadavg): 1.08 1.02 0.93 2/55 11292
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 29404 0 0 0 80896 120 0 0 25 0 1 0 549202429 118833152 27976 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29012 27976 603 41 0 28971 0
vsize: 116048
[startup+820.078 s]
Raw data (loadavg): 1.07 1.02 0.93 2/55 11292
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 29607 0 0 0 81895 121 0 0 25 0 1 0 549202429 119635968 28179 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29208 28179 603 41 0 29167 0
vsize: 116832
[startup+830.078 s]
Raw data (loadavg): 1.06 1.01 0.93 2/55 11292
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 29753 0 0 0 82894 122 0 0 25 0 1 0 549202429 120311808 28325 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29373 28325 603 41 0 29332 0
vsize: 117492
[startup+840.085 s]
Raw data (loadavg): 1.05 1.01 0.93 2/55 11294
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 29963 0 0 0 83893 123 0 0 25 0 1 0 549202429 121118720 28535 4294967295 134512640 134672761 3221224544 3221223744 134557806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29570 28535 603 41 0 29529 0
vsize: 118280
[startup+850.085 s]
Raw data (loadavg): 1.04 1.01 0.93 2/55 11294
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 30227 0 0 0 84892 125 0 0 25 0 1 0 549202429 122179584 28799 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29829 28799 603 41 0 29788 0
vsize: 119316
[startup+860.085 s]
Raw data (loadavg): 1.03 1.01 0.93 2/55 11294
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 30424 0 0 0 85891 126 0 0 25 0 1 0 549202429 122982400 28996 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30025 28996 603 41 0 29984 0
vsize: 120100
[startup+870.086 s]
Raw data (loadavg): 1.03 1.01 0.93 2/55 11294
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 30717 0 0 0 86890 127 0 0 25 0 1 0 549202429 124174336 29289 4294967295 134512640 134672761 3221224544 3221223648 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30316 29289 603 41 0 30275 0
vsize: 121264
[startup+880.086 s]
Raw data (loadavg): 1.02 1.01 0.93 2/55 11294
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 30961 0 0 0 87889 128 0 0 25 0 1 0 549202429 125247488 29533 4294967295 134512640 134672761 3221224544 3221223716 134556646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30578 29533 603 41 0 30537 0
vsize: 122312
[startup+890.087 s]
Raw data (loadavg): 1.02 1.01 0.93 2/55 11294
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 31032 0 0 0 88889 129 0 0 25 0 1 0 549202429 125521920 29604 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30645 29604 603 41 0 30604 0
vsize: 122580
[startup+900.087 s]
Raw data (loadavg): 1.02 1.01 0.93 2/55 11294
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 31289 0 0 0 89888 130 0 0 25 0 1 0 549202429 126586880 29861 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30905 29861 603 41 0 30864 0
vsize: 123620
[startup+910.088 s]
Raw data (loadavg): 1.01 1.01 0.93 2/55 11294
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 31595 0 0 0 90887 131 0 0 25 0 1 0 549202429 127778816 30167 4294967295 134512640 134672761 3221224544 3221223648 134560229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31196 30167 603 41 0 31155 0
vsize: 124784
[startup+920.089 s]
Raw data (loadavg): 1.01 1.01 0.93 2/55 11294
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 31871 0 0 0 91887 132 0 0 25 0 1 0 549202429 128843776 30443 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31456 30443 603 41 0 31415 0
vsize: 125824
[startup+930.089 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 11294
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 32105 0 0 0 92886 132 0 0 25 0 1 0 549202429 129921024 30677 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31719 30677 603 41 0 31678 0
vsize: 126876
[startup+940.09 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 11294
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 32288 0 0 0 93886 133 0 0 25 0 1 0 549202429 130592768 30860 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31883 30860 603 41 0 31842 0
vsize: 127532
[startup+950.089 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11294
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 32389 0 0 0 94886 133 0 0 25 0 1 0 549202429 130998272 30961 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31982 30961 603 41 0 31941 0
vsize: 127928
[startup+960.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11294
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 32528 0 0 0 95886 133 0 0 25 0 1 0 549202429 131538944 31100 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32114 31100 603 41 0 32073 0
vsize: 128456
[startup+970.091 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11294
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 32591 0 0 0 96886 133 0 0 25 0 1 0 549202429 131809280 31163 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32180 31163 603 41 0 32139 0
vsize: 128720
[startup+980.091 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11294
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 32751 0 0 0 97886 134 0 0 25 0 1 0 549202429 131932160 31203 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+990.092 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11294
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 32751 0 0 0 98886 134 0 0 25 0 1 0 549202429 131932160 31203 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1000.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11294
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 32751 0 0 0 99886 134 0 0 25 0 1 0 549202429 131932160 31203 4294967295 134512640 134672761 3221224544 3221223500 1075350544 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1010.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11294
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 32751 0 0 0 100886 134 0 0 25 0 1 0 549202429 131932160 31203 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1020.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11294
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 32751 0 0 0 101886 134 0 0 25 0 1 0 549202429 131932160 31203 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1030.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11294
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 32751 0 0 0 102886 134 0 0 25 0 1 0 549202429 131932160 31203 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1040.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11294
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 32751 0 0 0 103886 134 0 0 25 0 1 0 549202429 131932160 31203 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1050.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11294
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 32751 0 0 0 104887 134 0 0 25 0 1 0 549202429 131932160 31203 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1060.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11294
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 32751 0 0 0 105887 134 0 0 25 0 1 0 549202429 131932160 31203 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1070.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11294
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 32751 0 0 0 106887 134 0 0 25 0 1 0 549202429 131932160 31203 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1080.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11294
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 32751 0 0 0 107887 134 0 0 25 0 1 0 549202429 131932160 31203 4294967295 134512640 134672761 3221224544 3221223680 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1090.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11294
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 32751 0 0 0 108887 134 0 0 25 0 1 0 549202429 131932160 31203 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1100.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11294
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 32751 0 0 0 109887 134 0 0 25 0 1 0 549202429 131932160 31203 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1110.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11294
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 32751 0 0 0 110887 134 0 0 25 0 1 0 549202429 131932160 31203 4294967295 134512640 134672761 3221224544 3221223744 134561967 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1120.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11294
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 32751 0 0 0 111887 134 0 0 25 0 1 0 549202429 131932160 31203 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1130.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11294
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 32751 0 0 0 112888 134 0 0 25 0 1 0 549202429 131932160 31203 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1140.13 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11296
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 32751 0 0 0 113891 134 0 0 25 0 1 0 549202429 131932160 31203 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1150.15 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11296
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 32751 0 0 0 114893 134 0 0 25 0 1 0 549202429 131932160 31203 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1160.15 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11296
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 32751 0 0 0 115893 134 0 0 25 0 1 0 549202429 131932160 31203 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1170.15 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11296
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 32751 0 0 0 116893 134 0 0 25 0 1 0 549202429 131932160 31203 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1180.15 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11296
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 32751 0 0 0 117893 134 0 0 25 0 1 0 549202429 131932160 31203 4294967295 134512640 134672761 3221224544 3221223712 134561275 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1190.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11296
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 32751 0 0 0 118894 134 0 0 25 0 1 0 549202429 131932160 31203 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1200.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 11296
Raw data (stat): 11231 (minisat+) R 11230 20024 20023 0 -1 0 32751 0 0 0 119895 134 0 0 25 0 1 0 549202429 131932160 31203 4294967295 134512640 134672761 3221224544 3221223712 134561156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.25 s]
Raw data (loadavg): 1.00 1.00 0.93 1/55 11296
Raw data (stat): 11231 (minisat+) Z 11230 20024 20023 0 -1 12 32754 0 0 0 119895 140 0 0 23 0 1 0 549202429 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.25
CPU time (s): 1200.36
CPU user time (s): 1198.96
CPU system time (s): 1.40679
CPU usage (%): 100.009
Max. virtual memory (Kb): 128840
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####