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 15249

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc19 THE 2005-04-21 03:34:12 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18147 boxname=wulflinc19 idbench=1396 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  130bea0863cb3f92addf09aabe15daa3  /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-10teams.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-10teams.opb /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-10teams.opb
IDLAUNCH: 18147
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        767168 kB
Buffers:         12452 kB
Cached:         226692 kB
SwapCached:        556 kB
Active:          77968 kB
Inactive:       163232 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        766916 kB
SwapTotal:     2097892 kB
SwapFree:      2096436 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5200 kB
Slab:            20540 kB
Committed_AS:    63804 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 03:54:15 (client local time) WITH STATUS 10 IN 1200.41 SECONDS
stats: 18147 7 1200.41 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 330 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 328]---> BDD-cost:   77
c ---[ 326]---> BDD-cost:   77
c ---[ 324]---> BDD-cost:   77
c ---[ 322]---> BDD-cost:   77
c ---[ 320]---> BDD-cost:   77
c ---[ 318]---> BDD-cost:   77
c ---[ 316]---> BDD-cost:   77
c ---[ 314]---> BDD-cost:   77
c ---[ 312]---> BDD-cost:   77
c ---[ 310]---> BDD-cost:   77
c ---[ 308]---> BDD-cost:   77
c ---[ 306]---> BDD-cost:   77
c ---[ 304]---> BDD-cost:   77
c ---[ 302]---> BDD-cost:   77
c ---[ 300]---> BDD-cost:   77
c ---[ 298]---> BDD-cost:   77
c ---[ 296]---> BDD-cost:   77
c ---[ 294]---> BDD-cost:   77
c ---[ 292]---> BDD-cost:   77
c ---[ 290]---> BDD-cost:   77
c ---[ 288]---> BDD-cost:   77
c ---[ 286]---> BDD-cost:   77
c ---[ 284]---> BDD-cost:   77
c ---[ 282]---> BDD-cost:   77
c ---[ 280]---> BDD-cost:   77
c ---[ 278]---> BDD-cost:   77
c ---[ 276]---> BDD-cost:   77
c ---[ 274]---> BDD-cost:   77
c ---[ 272]---> BDD-cost:   77
c ---[ 270]---> BDD-cost:   77
c ---[ 268]---> BDD-cost:   77
c ---[ 266]---> BDD-cost:   77
c ---[ 264]---> BDD-cost:   77
c ---[ 262]---> BDD-cost:   77
c ---[ 260]---> BDD-cost:   77
c ---[ 258]---> BDD-cost:   77
c ---[ 256]---> BDD-cost:   77
c ---[ 254]---> BDD-cost:   77
c ---[ 252]---> BDD-cost:   77
c ---[ 250]---> BDD-cost:   77
c ---[ 249]---> BDD-cost:  125
c ---[ 248]---> BDD-cost:  185
c ---[ 247]---> BDD-cost:  185
c ---[ 246]---> BDD-cost:  185
c ---[ 245]---> BDD-cost:  185
c ---[ 244]---> BDD-cost:  185
c ---[ 243]---> BDD-cost:  125
c ---[ 242]---> BDD-cost:  185
c ---[ 241]---> BDD-cost:  185
c ---[ 240]---> BDD-cost:  185
c ---[ 239]---> BDD-cost:  185
c ---[ 238]---> BDD-cost:  125
c ---[ 237]---> BDD-cost:  185
c ---[ 236]---> BDD-cost:  185
c ---[ 235]---> BDD-cost:  185
c ---[ 234]---> BDD-cost:  185
c ---[ 233]---> BDD-cost:  185
c ---[ 232]---> BDD-cost:  125
c ---[ 231]---> BDD-cost:  185
c ---[ 230]---> BDD-cost:  185
c ---[ 229]---> BDD-cost:  185
c ---[ 228]---> BDD-cost:  185
c ---[ 227]---> BDD-cost:  125
c ---[ 226]---> BDD-cost:  185
c ---[ 225]---> BDD-cost:  185
c ---[ 224]---> BDD-cost:  185
c ---[ 223]---> BDD-cost:  185
c ---[ 222]---> BDD-cost:  185
c ---[ 221]---> BDD-cost:  125
c ---[ 220]---> BDD-cost:  185
c ---[ 219]---> BDD-cost:  185
c ---[ 218]---> BDD-cost:  185
c ---[ 217]---> BDD-cost:  185
c ---[ 216]---> BDD-cost:  125
c ---[ 215]---> BDD-cost:  185
c ---[ 214]---> BDD-cost:  185
c ---[ 213]---> BDD-cost:  185
c ---[ 212]---> BDD-cost:  185
c ---[ 211]---> BDD-cost:  185
c ---[ 210]---> BDD-cost:  125
c ---[ 209]---> BDD-cost:  125
c ---[ 208]---> BDD-cost:  185
c ---[ 207]---> BDD-cost:  185
c ---[ 206]---> BDD-cost:  185
c ---[ 205]---> BDD-cost:  185
c ---[ 204]---> BDD-cost:  185
c ---[ 203]---> BDD-cost:  185
c ---[ 202]---> BDD-cost:  185
c ---[ 201]---> BDD-cost:  185
c ---[ 200]---> BDD-cost:  125
c ---[ 199]---> BDD-cost:   75
c ---[ 198]---> BDD-cost:   77
c ---[ 197]---> BDD-cost:   77
c ---[ 196]---> BDD-cost:   77
c ---[ 195]---> BDD-cost:   77
c ---[ 194]---> BDD-cost:   77
c ---[ 193]---> BDD-cost:   77
c ---[ 192]---> BDD-cost:   77
c ---[ 191]---> BDD-cost:   75
c ---[ 190]---> BDD-cost:   77
c ---[ 189]---> BDD-cost:   77
c ---[ 188]---> BDD-cost:   77
c ---[ 187]---> BDD-cost:   77
c ---[ 186]---> BDD-cost:   77
c ---[ 185]---> BDD-cost:   77
c ---[ 184]---> BDD-cost:   77
c ---[ 183]---> BDD-cost:   75
c ---[ 182]---> BDD-cost:   77
c ---[ 181]---> BDD-cost:   77
c ---[ 180]---> BDD-cost:   77
c ---[ 179]---> BDD-cost:   77
c ---[ 178]---> BDD-cost:   77
c ---[ 177]---> BDD-cost:   77
c ---[ 176]---> BDD-cost:   77
c ---[ 175]---> BDD-cost:   75
c ---[ 174]---> BDD-cost:   77
c ---[ 173]---> BDD-cost:   77
c ---[ 172]---> BDD-cost:   77
c ---[ 171]---> BDD-cost:   77
c ---[ 170]---> BDD-cost:   77
c ---[ 169]---> BDD-cost:   77
c ---[ 168]---> BDD-cost:   77
c ---[ 167]---> BDD-cost:   75
c ---[ 166]---> BDD-cost:   77
c ---[ 165]---> BDD-cost:   77
c ---[ 164]---> BDD-cost:   77
c ---[ 163]---> BDD-cost:   77
c ---[ 162]---> BDD-cost:   77
c ---[ 161]---> BDD-cost:   77
c ---[ 160]---> BDD-cost:   77
c ---[ 158]---> BDD-cost:   70
c ---[ 156]---> BDD-cost:   77
c ---[ 154]---> BDD-cost:   77
c ---[ 152]---> BDD-cost:   77
c ---[ 150]---> BDD-cost:   77
c ---[ 148]---> BDD-cost:   77
c ---[ 146]---> BDD-cost:   77
c ---[ 144]---> BDD-cost:   77
c ---[ 142]---> BDD-cost:   70
c ---[ 140]---> BDD-cost:   76
c ---[ 138]---> BDD-cost:   76
c ---[ 136]---> BDD-cost:   76
c ---[ 134]---> BDD-cost:   76
c ---[ 132]---> BDD-cost:   76
c ---[ 130]---> BDD-cost:   76
c ---[ 128]---> BDD-cost:   76
c ---[ 126]---> BDD-cost:   70
c ---[ 124]---> BDD-cost:   77
c ---[ 122]---> BDD-cost:   77
c ---[ 120]---> BDD-cost:   77
c ---[ 118]---> BDD-cost:   77
c ---[ 116]---> BDD-cost:   77
c ---[ 114]---> BDD-cost:   77
c ---[ 112]---> BDD-cost:   77
c ---[ 110]---> BDD-cost:   70
c ---[ 108]---> BDD-cost:   77
c ---[ 106]---> BDD-cost:   77
c ---[ 104]---> BDD-cost:   77
c ---[ 102]---> BDD-cost:   77
c ---[ 100]---> BDD-cost:   77
c ---[  98]---> BDD-cost:   77
c ---[  96]---> BDD-cost:   77
c ---[  94]---> BDD-cost:   70
c ---[  92]---> BDD-cost:   77
c ---[  90]---> BDD-cost:   77
c ---[  88]---> BDD-cost:   77
c ---[  86]---> BDD-cost:   77
c ---[  84]---> BDD-cost:   77
c ---[  82]---> BDD-cost:   77
c ---[  80]---> BDD-cost:   77
c ---[  78]---> BDD-cost:   70
c ---[  76]---> BDD-cost:   77
c ---[  74]---> BDD-cost:   77
c ---[  72]---> BDD-cost:   77
c ---[  70]---> BDD-cost:   77
c ---[  68]---> BDD-cost:   77
c ---[  66]---> BDD-cost:   77
c ---[  64]---> BDD-cost:   77
c ---[  62]---> BDD-cost:   70
c ---[  60]---> BDD-cost:   77
c ---[  58]---> BDD-cost:   77
c ---[  56]---> BDD-cost:   77
c ---[  54]---> BDD-cost:   77
c ---[  52]---> BDD-cost:   77
c ---[  50]---> BDD-cost:   77
c ---[  48]---> BDD-cost:   77
c ---[  46]---> BDD-cost:   70
c ---[  44]---> BDD-cost:   77
c ---[  42]---> BDD-cost:   77
c ---[  40]---> BDD-cost:   77
c ---[  38]---> BDD-cost:   77
c ---[  36]---> BDD-cost:   77
c ---[  34]---> BDD-cost:   77
c ---[  32]---> BDD-cost:   77
c ---[  30]---> BDD-cost:   70
c ---[  28]---> BDD-cost:   77
c ---[  26]---> BDD-cost:   77
c ---[  24]---> BDD-cost:   77
c ---[  22]---> BDD-cost:   77
c ---[  20]---> BDD-cost:   77
c ---[  18]---> BDD-cost:   77
c ---[  16]---> BDD-cost:   77
c ---[  14]---> BDD-cost:   70
c ---[  12]---> BDD-cost:   77
c ---[  10]---> BDD-cost:   77
c ---[   8]---> BDD-cost:   77
c ---[   6]---> BDD-cost:   77
c ---[   4]---> BDD-cost:   77
c ---[   2]---> BDD-cost:   77
c ---[   0]---> BDD-cost:   77
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   53221   141547 |   17740       0        0     nan |  0.000 % |
c |       100 |   53221   141547 |   19514     100      818     8.2 |  1.808 % |
c |       250 |   53221   141547 |   21465     250    15400    61.6 |  1.808 % |
c |       475 |   53221   141547 |   23611     475    28793    60.6 |  1.808 % |
c |       812 |   53221   141547 |   25973     812    62995    77.6 |  1.808 % |
c |      1318 |   53221   141547 |   28570    1318   139369   105.7 |  1.808 % |
c |      2077 |   53221   141547 |   31427    2077   324252   156.1 |  1.808 % |
c |      3216 |   53221   141547 |   34570    3216   511801   159.1 |  1.808 % |
c ==============================================================================
c [1mFound solution: 968[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:437447     Base: 2 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4874 | 1170249  2748624 |  390083    4874   723583   148.5 |  1.808 % |
c |      4975 | 1170249  2748624 |  429091    4975   727056   146.1 |  0.096 % |
c |      5127 | 1168633  2744934 |  472000    5106   732833   143.5 |  0.203 % |
c |      5352 | 1168239  2744039 |  519200    5330   758649   142.3 |  0.228 % |
c |      5689 | 1168239  2744039 |  571120    5667   801363   141.4 |  0.228 % |
c |      6195 | 1167323  2741954 |  628232    6169   840094   136.2 |  0.289 % |
c |      6956 | 1167291  2741882 |  691055    6929   997315   143.9 |  0.290 % |
c |      8096 | 1161881  2729510 |  760161    8045  1099132   136.6 |  0.658 % |
c |      9806 | 1161881  2729510 |  836177    9755  1464354   150.1 |  0.658 % |
c |     12368 | 1136926  2672080 |  919795   11973  1805356   150.8 |  2.440 % |
c |     16212 | 1136926  2672080 | 1011774   15817  2970224   187.8 |  2.440 % |
c |     21978 | 1118168  2628830 | 1112952   21448  3450350   160.9 |  3.793 % |
c |     30627 | 1079300  2539076 | 1224247   29742  5492558   184.7 |  6.630 % |
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.73 0.92 0.92 2/55 19810
Raw data (stat): 19810 (runsolver) R 19809 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 541870167 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.001 s]
Raw data (loadavg): 0.77 0.92 0.92 2/55 19810
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 2704 0 0 0 991 7 0 0 25 0 1 0 541870167 13152256 2665 4294967295 134512640 134672761 3221224528 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3211 2665 603 41 0 3170 0
vsize: 12844
[startup+20.0022 s]
Raw data (loadavg): 0.81 0.92 0.92 2/55 19810
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 35720 0 0 0 1915 83 0 0 25 0 1 0 541870167 157884416 34392 4294967295 134512640 134672761 3221224528 3221223828 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38546 34392 603 41 0 38505 0
vsize: 154184
[startup+30.0027 s]
Raw data (loadavg): 0.84 0.93 0.92 2/55 19810
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 36022 0 0 0 2914 84 0 0 25 0 1 0 541870167 157884416 34694 4294967295 134512640 134672761 3221224528 3221223696 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38546 34694 603 41 0 38505 0
vsize: 154184
[startup+40.0034 s]
Raw data (loadavg): 0.86 0.93 0.92 2/55 19810
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 36143 0 0 0 3914 84 0 0 25 0 1 0 541870167 158289920 34815 4294967295 134512640 134672761 3221224528 3221223700 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38645 34815 603 41 0 38604 0
vsize: 154580
[startup+50.0038 s]
Raw data (loadavg): 0.88 0.93 0.92 2/55 19812
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 36191 0 0 0 4914 84 0 0 25 0 1 0 541870167 158425088 34863 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38678 34863 603 41 0 38637 0
vsize: 154712
[startup+60.0045 s]
Raw data (loadavg): 0.90 0.93 0.92 2/55 19812
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 36298 0 0 0 5913 85 0 0 25 0 1 0 541870167 158965760 34970 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38810 34970 603 41 0 38769 0
vsize: 155240
[startup+70.0049 s]
Raw data (loadavg): 0.92 0.93 0.92 2/55 19812
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 36360 0 0 0 6913 85 0 0 25 0 1 0 541870167 159100928 35032 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38843 35032 603 41 0 38802 0
vsize: 155372
[startup+80.005 s]
Raw data (loadavg): 0.93 0.94 0.92 2/55 19812
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 36471 0 0 0 7913 86 0 0 25 0 1 0 541870167 159637504 35143 4294967295 134512640 134672761 3221224528 3221223728 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38974 35143 603 41 0 38933 0
vsize: 155896
[startup+90.0057 s]
Raw data (loadavg): 0.94 0.94 0.92 2/55 19812
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 36584 0 0 0 8913 86 0 0 25 0 1 0 541870167 160038912 35256 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39072 35256 603 41 0 39031 0
vsize: 156288
[startup+100.005 s]
Raw data (loadavg): 0.95 0.94 0.92 2/55 19812
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 36741 0 0 0 9912 86 0 0 25 0 1 0 541870167 160710656 35413 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39236 35413 603 41 0 39195 0
vsize: 156944
[startup+110.006 s]
Raw data (loadavg): 0.95 0.94 0.92 2/55 19812
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 36876 0 0 0 10912 87 0 0 25 0 1 0 541870167 161251328 35548 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39368 35548 603 41 0 39327 0
vsize: 157472
[startup+120.007 s]
Raw data (loadavg): 0.96 0.94 0.92 2/55 19812
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 36969 0 0 0 11912 87 0 0 25 0 1 0 541870167 161652736 35641 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39466 35641 603 41 0 39425 0
vsize: 157864
[startup+130.007 s]
Raw data (loadavg): 0.97 0.94 0.92 2/55 19812
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 37097 0 0 0 12912 87 0 0 25 0 1 0 541870167 162189312 35769 4294967295 134512640 134672761 3221224528 3221223664 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39597 35769 603 41 0 39556 0
vsize: 158388
[startup+140.007 s]
Raw data (loadavg): 0.97 0.94 0.92 2/55 19812
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 37157 0 0 0 13912 88 0 0 25 0 1 0 541870167 162476032 35829 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39667 35829 603 41 0 39626 0
vsize: 158668
[startup+150.008 s]
Raw data (loadavg): 0.98 0.95 0.92 2/55 19812
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 37163 0 0 0 14912 88 0 0 25 0 1 0 541870167 162476032 35835 4294967295 134512640 134672761 3221224528 3221223700 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39667 35835 603 41 0 39626 0
vsize: 158668
[startup+160.008 s]
Raw data (loadavg): 0.98 0.95 0.92 2/55 19812
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 37164 0 0 0 15912 88 0 0 25 0 1 0 541870167 162476032 35836 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39667 35836 603 41 0 39626 0
vsize: 158668
[startup+170.008 s]
Raw data (loadavg): 0.98 0.95 0.92 2/55 19812
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 37181 0 0 0 16912 88 0 0 25 0 1 0 541870167 162476032 35853 4294967295 134512640 134672761 3221224528 3221223664 134560667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39667 35853 603 41 0 39626 0
vsize: 158668
[startup+180.008 s]
Raw data (loadavg): 0.98 0.95 0.92 2/55 19812
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 37199 0 0 0 17912 88 0 0 25 0 1 0 541870167 162611200 35871 4294967295 134512640 134672761 3221224528 3221223696 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39700 35871 603 41 0 39659 0
vsize: 158800
[startup+190.009 s]
Raw data (loadavg): 0.99 0.95 0.92 2/55 19812
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 37263 0 0 0 18912 88 0 0 25 0 1 0 541870167 162881536 35935 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39766 35935 603 41 0 39725 0
vsize: 159064
[startup+200.009 s]
Raw data (loadavg): 0.99 0.95 0.92 2/55 19812
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 37388 0 0 0 19912 88 0 0 25 0 1 0 541870167 163418112 36060 4294967295 134512640 134672761 3221224528 3221223696 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39897 36060 603 41 0 39856 0
vsize: 159588
[startup+210.01 s]
Raw data (loadavg): 0.99 0.95 0.92 2/55 19812
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 37560 0 0 0 20912 89 0 0 25 0 1 0 541870167 164085760 36232 4294967295 134512640 134672761 3221224528 3221223632 134560492 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40060 36232 603 41 0 40019 0
vsize: 160240
[startup+220.016 s]
Raw data (loadavg): 0.99 0.95 0.92 2/55 19812
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 37704 0 0 0 21912 90 0 0 25 0 1 0 541870167 164626432 36376 4294967295 134512640 134672761 3221224528 3221223664 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40192 36376 603 41 0 40151 0
vsize: 160768
[startup+230.024 s]
Raw data (loadavg): 0.99 0.95 0.92 2/55 19812
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 37801 0 0 0 22913 90 0 0 25 0 1 0 541870167 165031936 36473 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40291 36473 603 41 0 40250 0
vsize: 161164
[startup+240.024 s]
Raw data (loadavg): 0.99 0.95 0.92 2/55 19812
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 37987 0 0 0 23912 91 0 0 25 0 1 0 541870167 165826560 36659 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40485 36659 603 41 0 40444 0
vsize: 161940
[startup+250.024 s]
Raw data (loadavg): 0.99 0.95 0.92 2/55 19812
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 38192 0 0 0 24912 91 0 0 25 0 1 0 541870167 166637568 36864 4294967295 134512640 134672761 3221224528 3221223712 134559509 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40683 36864 603 41 0 40642 0
vsize: 162732
[startup+260.024 s]
Raw data (loadavg): 0.99 0.96 0.92 2/55 19812
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 38370 0 0 0 25911 92 0 0 25 0 1 0 541870167 167436288 37042 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40878 37042 603 41 0 40837 0
vsize: 163512
[startup+270.029 s]
Raw data (loadavg): 0.99 0.96 0.92 2/55 19812
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 38435 0 0 0 26912 92 0 0 25 0 1 0 541870167 167698432 37107 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40942 37107 603 41 0 40901 0
vsize: 163768
[startup+280.029 s]
Raw data (loadavg): 0.99 0.96 0.92 2/55 19812
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 38553 0 0 0 27912 92 0 0 25 0 1 0 541870167 168198144 37225 4294967295 134512640 134672761 3221224528 3221223700 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41064 37225 603 41 0 41023 0
vsize: 164256
[startup+290.032 s]
Raw data (loadavg): 0.99 0.96 0.92 2/55 19812
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 38562 0 0 0 28912 92 0 0 25 0 1 0 541870167 168198144 37234 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41064 37234 603 41 0 41023 0
vsize: 164256
[startup+300.032 s]
Raw data (loadavg): 0.99 0.96 0.92 2/55 19812
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 38591 0 0 0 29912 93 0 0 25 0 1 0 541870167 168329216 37263 4294967295 134512640 134672761 3221224528 3221223676 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41096 37263 603 41 0 41055 0
vsize: 164384
[startup+310.033 s]
Raw data (loadavg): 0.99 0.96 0.92 2/55 19812
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 38610 0 0 0 30912 93 0 0 25 0 1 0 541870167 168460288 37282 4294967295 134512640 134672761 3221224528 3221223700 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41128 37282 603 41 0 41087 0
vsize: 164512
[startup+320.032 s]
Raw data (loadavg): 0.99 0.96 0.92 2/55 19812
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 38610 0 0 0 31912 93 0 0 25 0 1 0 541870167 168460288 37282 4294967295 134512640 134672761 3221224528 3221223728 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41128 37282 603 41 0 41087 0
vsize: 164512
[startup+330.032 s]
Raw data (loadavg): 0.99 0.96 0.92 2/55 19812
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 38702 0 0 0 32912 93 0 0 25 0 1 0 541870167 168730624 37374 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41194 37374 603 41 0 41153 0
vsize: 164776
[startup+340.032 s]
Raw data (loadavg): 0.99 0.96 0.92 2/55 19812
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 38859 0 0 0 33912 93 0 0 25 0 1 0 541870167 169394176 37531 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41356 37531 603 41 0 41315 0
vsize: 165424
[startup+350.032 s]
Raw data (loadavg): 0.99 0.96 0.92 2/55 19814
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 38903 0 0 0 34912 94 0 0 25 0 1 0 541870167 169660416 37575 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41421 37575 603 41 0 41380 0
vsize: 165684
[startup+360.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19814
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 38903 0 0 0 35912 94 0 0 25 0 1 0 541870167 169660416 37575 4294967295 134512640 134672761 3221224528 3221223712 134556675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41421 37575 603 41 0 41380 0
vsize: 165684
[startup+370.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19814
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 38905 0 0 0 36912 94 0 0 25 0 1 0 541870167 169660416 37577 4294967295 134512640 134672761 3221224528 3221223732 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41421 37577 603 41 0 41380 0
vsize: 165684
[startup+380.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19814
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 38905 0 0 0 37912 94 0 0 25 0 1 0 541870167 169660416 37577 4294967295 134512640 134672761 3221224528 3221223700 134556685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41421 37577 603 41 0 41380 0
vsize: 165684
[startup+390.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19814
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 38905 0 0 0 38912 94 0 0 25 0 1 0 541870167 169660416 37577 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41421 37577 603 41 0 41380 0
vsize: 165684
[startup+400.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19814
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 38915 0 0 0 39913 94 0 0 25 0 1 0 541870167 169660416 37587 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41421 37587 603 41 0 41380 0
vsize: 165684
[startup+410.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19814
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 38923 0 0 0 40913 94 0 0 25 0 1 0 541870167 169660416 37595 4294967295 134512640 134672761 3221224528 3221223652 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41421 37595 603 41 0 41380 0
vsize: 165684
[startup+420.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19814
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 39044 0 0 0 41913 94 0 0 25 0 1 0 541870167 170196992 37716 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41552 37716 603 41 0 41511 0
vsize: 166208
[startup+430.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19814
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 39184 0 0 0 42912 95 0 0 25 0 1 0 541870167 170737664 37856 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41684 37856 603 41 0 41643 0
vsize: 166736
[startup+440.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19814
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 39270 0 0 0 43912 95 0 0 25 0 1 0 541870167 171139072 37942 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41782 37942 603 41 0 41741 0
vsize: 167128
[startup+450.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19814
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 39382 0 0 0 44912 95 0 0 25 0 1 0 541870167 171544576 38054 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41881 38054 603 41 0 41840 0
vsize: 167524
[startup+460.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19814
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 39480 0 0 0 45911 96 0 0 25 0 1 0 541870167 171945984 38152 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41979 38152 603 41 0 41938 0
vsize: 167916
[startup+470.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19814
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 39613 0 0 0 46911 96 0 0 25 0 1 0 541870167 172474368 38285 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42108 38285 603 41 0 42067 0
vsize: 168432
[startup+480.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19814
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 39719 0 0 0 47911 97 0 0 25 0 1 0 541870167 172879872 38391 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42207 38391 603 41 0 42166 0
vsize: 168828
[startup+490.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19814
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 39846 0 0 0 48911 97 0 0 25 0 1 0 541870167 173408256 38518 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42336 38518 603 41 0 42295 0
vsize: 169344
[startup+500.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19814
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 40020 0 0 0 49911 97 0 0 25 0 1 0 541870167 173948928 38692 4294967295 134512640 134672761 3221224528 3221223664 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42468 38692 603 41 0 42427 0
vsize: 169872
[startup+510.037 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19814
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 40170 0 0 0 50910 98 0 0 25 0 1 0 541870167 174600192 38842 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42627 38842 603 41 0 42586 0
vsize: 170508
[startup+520.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19814
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 40305 0 0 0 51910 99 0 0 25 0 1 0 541870167 175140864 38977 4294967295 134512640 134672761 3221224528 3221223664 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42759 38977 603 41 0 42718 0
vsize: 171036
[startup+530.037 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19814
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 40443 0 0 0 52910 99 0 0 25 0 1 0 541870167 175669248 39115 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42888 39115 603 41 0 42847 0
vsize: 171552
[startup+540.037 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19814
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 40608 0 0 0 53910 100 0 0 25 0 1 0 541870167 176332800 39280 4294967295 134512640 134672761 3221224528 3221223692 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43050 39280 603 41 0 43009 0
vsize: 172200
[startup+550.037 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19814
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 40761 0 0 0 54909 100 0 0 25 0 1 0 541870167 177000448 39433 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43213 39433 603 41 0 43172 0
vsize: 172852
[startup+560.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19814
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 40896 0 0 0 55909 101 0 0 25 0 1 0 541870167 177528832 39568 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43342 39568 603 41 0 43301 0
vsize: 173368
[startup+570.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19814
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 41014 0 0 0 56909 101 0 0 25 0 1 0 541870167 178069504 39686 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43474 39686 603 41 0 43433 0
vsize: 173896
[startup+580.042 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19814
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 41017 0 0 0 57908 102 0 0 25 0 1 0 541870167 178069504 39689 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43474 39689 603 41 0 43433 0
vsize: 173896
[startup+590.055 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19814
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 41026 0 0 0 58909 102 0 0 25 0 1 0 541870167 178069504 39698 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43474 39698 603 41 0 43433 0
vsize: 173896
[startup+600.055 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19814
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 41105 0 0 0 59908 103 0 0 25 0 1 0 541870167 178339840 39777 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43540 39777 603 41 0 43499 0
vsize: 174160
[startup+610.067 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19814
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 41223 0 0 0 60909 103 0 0 25 0 1 0 541870167 178880512 39895 4294967295 134512640 134672761 3221224528 3221223688 134561029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43672 39895 603 41 0 43631 0
vsize: 174688
[startup+620.067 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19814
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 41381 0 0 0 61909 103 0 0 25 0 1 0 541870167 179548160 40053 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43835 40053 603 41 0 43794 0
vsize: 175340
[startup+630.074 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19814
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 41519 0 0 0 62910 104 0 0 25 0 1 0 541870167 180088832 40191 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43967 40191 603 41 0 43926 0
vsize: 175868
[startup+640.082 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19814
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 41548 0 0 0 63911 104 0 0 25 0 1 0 541870167 180224000 40220 4294967295 134512640 134672761 3221224528 3221223700 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44000 40220 603 41 0 43959 0
vsize: 176000
[startup+650.083 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19816
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 41548 0 0 0 64911 104 0 0 25 0 1 0 541870167 180224000 40220 4294967295 134512640 134672761 3221224528 3221223700 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44000 40220 603 41 0 43959 0
vsize: 176000
[startup+660.083 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19816
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 41556 0 0 0 65911 104 0 0 25 0 1 0 541870167 180224000 40228 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44000 40228 603 41 0 43959 0
vsize: 176000
[startup+670.083 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19816
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 41685 0 0 0 66911 104 0 0 25 0 1 0 541870167 180883456 40357 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44161 40357 603 41 0 44120 0
vsize: 176644
[startup+680.083 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19816
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 41842 0 0 0 67911 105 0 0 25 0 1 0 541870167 181559296 40514 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44326 40514 603 41 0 44285 0
vsize: 177304
[startup+690.083 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19816
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 42020 0 0 0 68910 105 0 0 25 0 1 0 541870167 182231040 40692 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44490 40692 603 41 0 44449 0
vsize: 177960
[startup+700.083 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19816
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 42127 0 0 0 69910 106 0 0 25 0 1 0 541870167 182767616 40799 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44621 40799 603 41 0 44580 0
vsize: 178484
[startup+710.084 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19816
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 42236 0 0 0 70910 106 0 0 25 0 1 0 541870167 183164928 40908 4294967295 134512640 134672761 3221224528 3221223712 134558654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44718 40908 603 41 0 44677 0
vsize: 178872
[startup+720.085 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19816
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 42369 0 0 0 71909 107 0 0 25 0 1 0 541870167 183705600 41041 4294967295 134512640 134672761 3221224528 3221223696 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44850 41041 603 41 0 44809 0
vsize: 179400
[startup+730.085 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19816
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 42503 0 0 0 72909 107 0 0 25 0 1 0 541870167 184238080 41175 4294967295 134512640 134672761 3221224528 3221223696 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44980 41175 603 41 0 44939 0
vsize: 179920
[startup+740.085 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19816
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 42631 0 0 0 73909 108 0 0 25 0 1 0 541870167 184766464 41303 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45109 41303 603 41 0 45068 0
vsize: 180436
[startup+750.085 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19816
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 42778 0 0 0 74909 108 0 0 25 0 1 0 541870167 185307136 41450 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45241 41450 603 41 0 45200 0
vsize: 180964
[startup+760.086 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19816
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 42940 0 0 0 75909 108 0 0 25 0 1 0 541870167 185978880 41612 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45405 41612 603 41 0 45364 0
vsize: 181620
[startup+770.086 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19816
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 43087 0 0 0 76908 109 0 0 25 0 1 0 541870167 186646528 41759 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45568 41759 603 41 0 45527 0
vsize: 182272
[startup+780.087 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19816
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 43234 0 0 0 77908 109 0 0 25 0 1 0 541870167 187179008 41906 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45698 41906 603 41 0 45657 0
vsize: 182792
[startup+790.087 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19816
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 43377 0 0 0 78908 110 0 0 25 0 1 0 541870167 187850752 42049 4294967295 134512640 134672761 3221224528 3221223696 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45862 42049 603 41 0 45821 0
vsize: 183448
[startup+800.087 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19816
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 43544 0 0 0 79908 110 0 0 25 0 1 0 541870167 188506112 42216 4294967295 134512640 134672761 3221224528 3221223712 134558923 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46022 42216 603 41 0 45981 0
vsize: 184088
[startup+810.088 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19816
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 43716 0 0 0 80908 111 0 0 25 0 1 0 541870167 189177856 42388 4294967295 134512640 134672761 3221224528 3221223632 134560198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46186 42388 603 41 0 46145 0
vsize: 184744
[startup+820.088 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19816
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 43903 0 0 0 81907 111 0 0 25 0 1 0 541870167 190074880 42574 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46405 42574 603 41 0 46364 0
vsize: 185620
[startup+830.088 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19816
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 44021 0 0 0 82907 112 0 0 25 0 1 0 541870167 190423040 42692 4294967295 134512640 134672761 3221224528 3221223632 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46490 42692 603 41 0 46449 0
vsize: 185960
[startup+840.089 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19816
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 44038 0 0 0 83907 112 0 0 25 0 1 0 541870167 190513152 42709 4294967295 134512640 134672761 3221224528 3221223632 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46512 42709 603 41 0 46471 0
vsize: 186048
[startup+850.089 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19816
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 44061 0 0 0 84907 112 0 0 25 0 1 0 541870167 190664704 42732 4294967295 134512640 134672761 3221224528 3221223632 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46549 42732 603 41 0 46508 0
vsize: 186196
[startup+860.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19816
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 44083 0 0 0 85907 112 0 0 25 0 1 0 541870167 190664704 42754 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46549 42754 603 41 0 46508 0
vsize: 186196
[startup+870.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19816
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 44115 0 0 0 86907 112 0 0 25 0 1 0 541870167 190820352 42786 4294967295 134512640 134672761 3221224528 3221223632 134560145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46587 42786 603 41 0 46546 0
vsize: 186348
[startup+880.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19816
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 44144 0 0 0 87907 112 0 0 25 0 1 0 541870167 190971904 42815 4294967295 134512640 134672761 3221224528 3221223632 134559908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46624 42815 603 41 0 46583 0
vsize: 186496
[startup+890.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19816
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 44171 0 0 0 88907 112 0 0 25 0 1 0 541870167 191057920 42842 4294967295 134512640 134672761 3221224528 3221223632 134560212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46645 42842 603 41 0 46604 0
vsize: 186580
[startup+900.091 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19816
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 44198 0 0 0 89908 112 0 0 25 0 1 0 541870167 191201280 42869 4294967295 134512640 134672761 3221224528 3221223632 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46680 42869 603 41 0 46639 0
vsize: 186720
[startup+910.091 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19816
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 44218 0 0 0 90908 112 0 0 25 0 1 0 541870167 191340544 42889 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46714 42889 603 41 0 46673 0
vsize: 186856
[startup+920.092 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19816
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 44258 0 0 0 91908 112 0 0 25 0 1 0 541870167 191533056 42929 4294967295 134512640 134672761 3221224528 3221223632 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46761 42929 603 41 0 46720 0
vsize: 187044
[startup+930.092 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19816
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 44280 0 0 0 92908 113 0 0 25 0 1 0 541870167 191467520 42951 4294967295 134512640 134672761 3221224528 3221223632 134559869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46745 42951 603 41 0 46704 0
vsize: 186980
[startup+940.093 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19816
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 44311 0 0 0 93908 113 0 0 25 0 1 0 541870167 191623168 42982 4294967295 134512640 134672761 3221224528 3221223632 134559869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46783 42982 603 41 0 46742 0
vsize: 187132
[startup+950.093 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19818
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 44341 0 0 0 94908 113 0 0 25 0 1 0 541870167 191774720 43012 4294967295 134512640 134672761 3221224528 3221223632 134559937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46820 43012 603 41 0 46779 0
vsize: 187280
[startup+960.093 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19818
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 44372 0 0 0 95908 113 0 0 25 0 1 0 541870167 191901696 43043 4294967295 134512640 134672761 3221224528 3221223632 134560059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46851 43043 603 41 0 46810 0
vsize: 187404
[startup+970.093 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19818
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 44396 0 0 0 96908 113 0 0 25 0 1 0 541870167 191991808 43067 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46873 43067 603 41 0 46832 0
vsize: 187492
[startup+980.093 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19818
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 44426 0 0 0 97909 113 0 0 25 0 1 0 541870167 192155648 43097 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46913 43097 603 41 0 46872 0
vsize: 187652
[startup+990.094 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19818
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 44447 0 0 0 98909 113 0 0 25 0 1 0 541870167 192155648 43118 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46913 43118 603 41 0 46872 0
vsize: 187652
[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19818
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 44478 0 0 0 99909 113 0 0 25 0 1 0 541870167 192311296 43149 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46951 43149 603 41 0 46910 0
vsize: 187804
[startup+1010.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19818
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 44507 0 0 0 100909 113 0 0 25 0 1 0 541870167 192458752 43178 4294967295 134512640 134672761 3221224528 3221223632 134560276 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46987 43178 603 41 0 46946 0
vsize: 187948
[startup+1020.1 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19818
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 44536 0 0 0 101909 113 0 0 25 0 1 0 541870167 192548864 43207 4294967295 134512640 134672761 3221224528 3221223712 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47009 43207 603 41 0 46968 0
vsize: 188036
[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19818
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 44557 0 0 0 102909 113 0 0 25 0 1 0 541870167 192700416 43228 4294967295 134512640 134672761 3221224528 3221223632 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47046 43228 603 41 0 47005 0
vsize: 188184
[startup+1040.1 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19818
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 44585 0 0 0 103909 113 0 0 25 0 1 0 541870167 192843776 43256 4294967295 134512640 134672761 3221224528 3221223632 134560158 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47081 43256 603 41 0 47040 0
vsize: 188324
[startup+1050.1 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19818
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 44608 0 0 0 104909 113 0 0 25 0 1 0 541870167 192843776 43279 4294967295 134512640 134672761 3221224528 3221223632 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47081 43279 603 41 0 47040 0
vsize: 188324
[startup+1060.1 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19818
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 44647 0 0 0 105909 113 0 0 25 0 1 0 541870167 192999424 43318 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47119 43318 603 41 0 47078 0
vsize: 188476
[startup+1070.1 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19818
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 44670 0 0 0 106910 114 0 0 25 0 1 0 541870167 193126400 43341 4294967295 134512640 134672761 3221224528 3221223632 134560248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47150 43341 603 41 0 47109 0
vsize: 188600
[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19818
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 44700 0 0 0 107910 114 0 0 25 0 1 0 541870167 193286144 43371 4294967295 134512640 134672761 3221224528 3221223632 134559937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47189 43371 603 41 0 47148 0
vsize: 188756
[startup+1090.1 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19818
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 44723 0 0 0 108910 114 0 0 25 0 1 0 541870167 193286144 43394 4294967295 134512640 134672761 3221224528 3221223632 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47189 43394 603 41 0 47148 0
vsize: 188756
[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19818
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 44754 0 0 0 109910 114 0 0 25 0 1 0 541870167 193441792 43425 4294967295 134512640 134672761 3221224528 3221223632 134560158 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47227 43425 603 41 0 47186 0
vsize: 188908
[startup+1110.1 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19818
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 44791 0 0 0 110910 114 0 0 25 0 1 0 541870167 193597440 43462 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47265 43462 603 41 0 47224 0
vsize: 189060
[startup+1120.1 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19818
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 44894 0 0 0 111910 114 0 0 25 0 1 0 541870167 193994752 43565 4294967295 134512640 134672761 3221224528 3221223632 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47362 43565 603 41 0 47321 0
vsize: 189448
[startup+1130.11 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19818
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 44927 0 0 0 112912 114 0 0 25 0 1 0 541870167 194134016 43598 4294967295 134512640 134672761 3221224528 3221223632 134560160 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47396 43598 603 41 0 47355 0
vsize: 189584
[startup+1140.12 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19818
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 44955 0 0 0 113912 114 0 0 25 0 1 0 541870167 194281472 43626 4294967295 134512640 134672761 3221224528 3221223632 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47432 43626 603 41 0 47391 0
vsize: 189728
[startup+1150.12 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19818
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 44984 0 0 0 114913 114 0 0 25 0 1 0 541870167 194433024 43655 4294967295 134512640 134672761 3221224528 3221223632 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47469 43655 603 41 0 47428 0
vsize: 189876
[startup+1160.12 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19818
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 45004 0 0 0 115913 114 0 0 25 0 1 0 541870167 194433024 43675 4294967295 134512640 134672761 3221224528 3221223632 134560154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47469 43675 603 41 0 47428 0
vsize: 189876
[startup+1170.12 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19818
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 45041 0 0 0 116913 114 0 0 25 0 1 0 541870167 194719744 43712 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47539 43712 603 41 0 47498 0
vsize: 190156
[startup+1180.13 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19818
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 45059 0 0 0 117913 115 0 0 25 0 1 0 541870167 194654208 43730 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47523 43730 603 41 0 47482 0
vsize: 190092
[startup+1190.14 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19818
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 45096 0 0 0 118914 115 0 0 25 0 1 0 541870167 194949120 43767 4294967295 134512640 134672761 3221224528 3221223632 134560039 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47595 43767 603 41 0 47554 0
vsize: 190380
[startup+1200.15 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 19818
Raw data (stat): 19810 (minisat+) R 19809 22929 22928 0 -1 0 45123 0 0 0 119916 115 0 0 25 0 1 0 541870167 195031040 43794 4294967295 134512640 134672761 3221224528 3221223632 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47615 43794 603 41 0 47574 0
vsize: 190460
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.25 s]
Raw data (loadavg): 0.99 0.97 0.92 1/55 19818
Raw data (stat): 19810 (minisat+) Z 19809 22929 22928 0 -1 12 45126 0 0 0 119916 124 0 0 25 0 1 0 541870167 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.25
CPU time (s): 1200.41
CPU user time (s): 1199.17
CPU system time (s): 1.24381
CPU usage (%): 100.013
Max. virtual memory (Kb): 190460
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####