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 21473

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        634900 kB
Buffers:         28816 kB
Cached:         344068 kB
SwapCached:         28 kB
Active:         188928 kB
Inactive:       186780 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        634648 kB
SwapTotal:     2097892 kB
SwapFree:      2097796 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6800 kB
Slab:            18360 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 00:18:07 (client local time) WITH STATUS 10 IN 1200.51 SECONDS
stats: 13155 7 1200.51 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.85 0.97 0.92 2/54 32426
Raw data (stat): 32426 (runsolver) R 32425 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 549216428 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.87 0.97 0.92 2/54 32426
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 2704 0 0 0 991 8 0 0 25 0 1 0 549216428 13152256 2665 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3211 2665 603 41 0 3170 0
vsize: 12844
[startup+20.0004 s]
Raw data (loadavg): 0.89 0.97 0.92 2/54 32426
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 35720 0 0 0 1914 84 0 0 25 0 1 0 549216428 157884416 34392 4294967295 134512640 134672761 3221224528 3221223856 134561967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38546 34392 603 41 0 38505 0
vsize: 154184
[startup+30.0009 s]
Raw data (loadavg): 0.91 0.97 0.92 2/54 32426
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 36022 0 0 0 2913 85 0 0 25 0 1 0 549216428 157884416 34694 4294967295 134512640 134672761 3221224528 3221223728 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38546 34694 603 41 0 38505 0
vsize: 154184
[startup+40.001 s]
Raw data (loadavg): 0.92 0.97 0.92 2/54 32426
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 36143 0 0 0 3912 86 0 0 25 0 1 0 549216428 158289920 34815 4294967295 134512640 134672761 3221224528 3221223700 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38645 34815 603 41 0 38604 0
vsize: 154580
[startup+50.0019 s]
Raw data (loadavg): 0.93 0.97 0.92 2/54 32426
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 36191 0 0 0 4912 86 0 0 25 0 1 0 549216428 158425088 34863 4294967295 134512640 134672761 3221224528 3221223696 134561264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38678 34863 603 41 0 38637 0
vsize: 154712
[startup+60.0023 s]
Raw data (loadavg): 0.94 0.97 0.92 2/54 32426
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 36298 0 0 0 5912 87 0 0 25 0 1 0 549216428 158965760 34970 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38810 34970 603 41 0 38769 0
vsize: 155240
[startup+70.0025 s]
Raw data (loadavg): 0.95 0.97 0.92 2/54 32426
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 36359 0 0 0 6911 87 0 0 25 0 1 0 549216428 159100928 35031 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38843 35031 603 41 0 38802 0
vsize: 155372
[startup+80.0033 s]
Raw data (loadavg): 0.96 0.97 0.92 2/54 32426
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 36471 0 0 0 7910 89 0 0 25 0 1 0 549216428 159637504 35143 4294967295 134512640 134672761 3221224528 3221223664 134560566 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.0027 s]
Raw data (loadavg): 0.96 0.97 0.92 2/54 32426
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 36586 0 0 0 8909 90 0 0 25 0 1 0 549216428 160038912 35258 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39072 35258 603 41 0 39031 0
vsize: 156288
[startup+100.004 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 32426
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 36746 0 0 0 9909 90 0 0 25 0 1 0 549216428 160710656 35418 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39236 35418 603 41 0 39195 0
vsize: 156944
[startup+110.005 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 32426
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 36878 0 0 0 10908 91 0 0 25 0 1 0 549216428 161251328 35550 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39368 35550 603 41 0 39327 0
vsize: 157472
[startup+120.004 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 32427
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 36974 0 0 0 11903 95 0 0 25 0 1 0 549216428 161652736 35646 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39466 35646 603 41 0 39425 0
vsize: 157864
[startup+130.004 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 32479
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 37106 0 0 0 12903 96 0 0 25 0 1 0 549216428 162189312 35778 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39597 35778 603 41 0 39556 0
vsize: 158388
[startup+140.005 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 32479
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 37157 0 0 0 13903 96 0 0 25 0 1 0 549216428 162476032 35829 4294967295 134512640 134672761 3221224528 3221223700 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39667 35829 603 41 0 39626 0
vsize: 158668
[startup+150.006 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 32479
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 37163 0 0 0 14902 97 0 0 25 0 1 0 549216428 162476032 35835 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39667 35835 603 41 0 39626 0
vsize: 158668
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32479
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 37170 0 0 0 15902 97 0 0 25 0 1 0 549216428 162476032 35842 4294967295 134512640 134672761 3221224528 3221223664 134560604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39667 35842 603 41 0 39626 0
vsize: 158668
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32479
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 37181 0 0 0 16902 98 0 0 25 0 1 0 549216428 162476032 35853 4294967295 134512640 134672761 3221224528 3221223700 134556627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39667 35853 603 41 0 39626 0
vsize: 158668
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32479
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 37199 0 0 0 17902 98 0 0 25 0 1 0 549216428 162611200 35871 4294967295 134512640 134672761 3221224528 3221223696 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39700 35871 603 41 0 39659 0
vsize: 158800
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32479
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 37265 0 0 0 18901 99 0 0 25 0 1 0 549216428 162881536 35937 4294967295 134512640 134672761 3221224528 3221223696 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39766 35937 603 41 0 39725 0
vsize: 159064
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32481
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 37392 0 0 0 19900 100 0 0 25 0 1 0 549216428 163418112 36064 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39897 36064 603 41 0 39856 0
vsize: 159588
[startup+210.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32481
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 37566 0 0 0 20900 100 0 0 25 0 1 0 549216428 164085760 36238 4294967295 134512640 134672761 3221224528 3221223696 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40060 36238 603 41 0 40019 0
vsize: 160240
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32481
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 37706 0 0 0 21900 101 0 0 25 0 1 0 549216428 164626432 36378 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40192 36378 603 41 0 40151 0
vsize: 160768
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32481
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 37802 0 0 0 22899 102 0 0 25 0 1 0 549216428 165031936 36474 4294967295 134512640 134672761 3221224528 3221223672 134560630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40291 36474 603 41 0 40250 0
vsize: 161164
[startup+240.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32481
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 37993 0 0 0 23899 103 0 0 25 0 1 0 549216428 165826560 36665 4294967295 134512640 134672761 3221224528 3221223632 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40485 36665 603 41 0 40444 0
vsize: 161940
[startup+250.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32481
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 38195 0 0 0 24898 103 0 0 25 0 1 0 549216428 166637568 36867 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40683 36867 603 41 0 40642 0
vsize: 162732
[startup+260.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32481
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 38372 0 0 0 25897 105 0 0 25 0 1 0 549216428 167436288 37044 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40878 37044 603 41 0 40837 0
vsize: 163512
[startup+270.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32481
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 38438 0 0 0 26896 105 0 0 25 0 1 0 549216428 167698432 37110 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40942 37110 603 41 0 40901 0
vsize: 163768
[startup+280.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32481
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 38553 0 0 0 27896 105 0 0 25 0 1 0 549216428 168198144 37225 4294967295 134512640 134672761 3221224528 3221223724 134556584 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41064 37225 603 41 0 41023 0
vsize: 164256
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32481
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 38562 0 0 0 28897 106 0 0 25 0 1 0 549216428 168198144 37234 4294967295 134512640 134672761 3221224528 3221223664 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41064 37234 603 41 0 41023 0
vsize: 164256
[startup+300.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32481
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 38591 0 0 0 29896 106 0 0 25 0 1 0 549216428 168329216 37263 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41096 37263 603 41 0 41055 0
vsize: 164384
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32481
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 38610 0 0 0 30897 106 0 0 25 0 1 0 549216428 168460288 37282 4294967295 134512640 134672761 3221224528 3221223696 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41128 37282 603 41 0 41087 0
vsize: 164512
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32481
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 38610 0 0 0 31897 106 0 0 25 0 1 0 549216428 168460288 37282 4294967295 134512640 134672761 3221224528 3221223728 134561967 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41128 37282 603 41 0 41087 0
vsize: 164512
[startup+330.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32481
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 38702 0 0 0 32896 107 0 0 25 0 1 0 549216428 168730624 37374 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41194 37374 603 41 0 41153 0
vsize: 164776
[startup+340.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32481
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 38859 0 0 0 33895 108 0 0 25 0 1 0 549216428 169394176 37531 4294967295 134512640 134672761 3221224528 3221223664 134560647 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41356 37531 603 41 0 41315 0
vsize: 165424
[startup+350.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32481
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 38903 0 0 0 34895 109 0 0 25 0 1 0 549216428 169660416 37575 4294967295 134512640 134672761 3221224528 3221223696 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41421 37575 603 41 0 41380 0
vsize: 165684
[startup+360.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32481
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 38903 0 0 0 35894 109 0 0 25 0 1 0 549216428 169660416 37575 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41421 37575 603 41 0 41380 0
vsize: 165684
[startup+370.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32481
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 38905 0 0 0 36894 110 0 0 25 0 1 0 549216428 169660416 37577 4294967295 134512640 134672761 3221224528 3221223700 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41421 37577 603 41 0 41380 0
vsize: 165684
[startup+380.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32481
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 38905 0 0 0 37894 110 0 0 25 0 1 0 549216428 169660416 37577 4294967295 134512640 134672761 3221224528 3221223700 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41421 37577 603 41 0 41380 0
vsize: 165684
[startup+390.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32481
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 38905 0 0 0 38894 110 0 0 25 0 1 0 549216428 169660416 37577 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41421 37577 603 41 0 41380 0
vsize: 165684
[startup+400.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32481
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 38915 0 0 0 39894 110 0 0 25 0 1 0 549216428 169660416 37587 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41421 37587 603 41 0 41380 0
vsize: 165684
[startup+410.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32481
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 38923 0 0 0 40894 111 0 0 25 0 1 0 549216428 169660416 37595 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41421 37595 603 41 0 41380 0
vsize: 165684
[startup+420.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32481
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 39047 0 0 0 41894 112 0 0 25 0 1 0 549216428 170196992 37719 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41552 37719 603 41 0 41511 0
vsize: 166208
[startup+430.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32481
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 39185 0 0 0 42893 113 0 0 25 0 1 0 549216428 170737664 37857 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41684 37857 603 41 0 41643 0
vsize: 166736
[startup+440.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32481
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 39270 0 0 0 43893 113 0 0 25 0 1 0 549216428 171139072 37942 4294967295 134512640 134672761 3221224528 3221223712 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41782 37942 603 41 0 41741 0
vsize: 167128
[startup+450.045 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32481
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 39382 0 0 0 44894 114 0 0 25 0 1 0 549216428 171544576 38054 4294967295 134512640 134672761 3221224528 3221223676 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41881 38054 603 41 0 41840 0
vsize: 167524
[startup+460.152 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 39480 0 0 0 45904 115 0 0 25 0 1 0 549216428 171945984 38152 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41979 38152 603 41 0 41938 0
vsize: 167916
[startup+470.151 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 39613 0 0 0 46903 116 0 0 25 0 1 0 549216428 172474368 38285 4294967295 134512640 134672761 3221224528 3221223664 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42108 38285 603 41 0 42067 0
vsize: 168432
[startup+480.157 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 39719 0 0 0 47904 116 0 0 25 0 1 0 549216428 172879872 38391 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42207 38391 603 41 0 42166 0
vsize: 168828
[startup+490.165 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 39850 0 0 0 48904 117 0 0 25 0 1 0 549216428 173408256 38522 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42336 38522 603 41 0 42295 0
vsize: 169344
[startup+500.176 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 40025 0 0 0 49905 117 0 0 25 0 1 0 549216428 173948928 38697 4294967295 134512640 134672761 3221224528 3221223728 134557800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42468 38697 603 41 0 42427 0
vsize: 169872
[startup+510.188 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 40174 0 0 0 50906 118 0 0 25 0 1 0 549216428 174600192 38846 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42627 38846 603 41 0 42586 0
vsize: 170508
[startup+520.187 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 40312 0 0 0 51905 118 0 0 25 0 1 0 549216428 175140864 38984 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42759 38984 603 41 0 42718 0
vsize: 171036
[startup+530.188 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 40450 0 0 0 52905 119 0 0 25 0 1 0 549216428 175669248 39122 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42888 39122 603 41 0 42847 0
vsize: 171552
[startup+540.187 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 40618 0 0 0 53905 119 0 0 25 0 1 0 549216428 176463872 39290 4294967295 134512640 134672761 3221224528 3221223696 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43082 39290 603 41 0 43041 0
vsize: 172328
[startup+550.188 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 40771 0 0 0 54904 120 0 0 25 0 1 0 549216428 177000448 39443 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43213 39443 603 41 0 43172 0
vsize: 172852
[startup+560.188 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 40904 0 0 0 55904 120 0 0 25 0 1 0 549216428 177528832 39576 4294967295 134512640 134672761 3221224528 3221223664 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43342 39576 603 41 0 43301 0
vsize: 173368
[startup+570.191 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 41014 0 0 0 56904 121 0 0 25 0 1 0 549216428 178069504 39686 4294967295 134512640 134672761 3221224528 3221223728 134557887 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.196 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 41020 0 0 0 57904 121 0 0 25 0 1 0 549216428 178069504 39692 4294967295 134512640 134672761 3221224528 3221223728 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43474 39692 603 41 0 43433 0
vsize: 173896
[startup+590.195 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 41026 0 0 0 58904 121 0 0 25 0 1 0 549216428 178069504 39698 4294967295 134512640 134672761 3221224528 3221223700 134556598 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.195 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 41123 0 0 0 59904 121 0 0 25 0 1 0 549216428 178475008 39795 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43573 39795 603 41 0 43532 0
vsize: 174292
[startup+610.195 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 41240 0 0 0 60904 121 0 0 25 0 1 0 549216428 179015680 39912 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43705 39912 603 41 0 43664 0
vsize: 174820
[startup+620.195 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 41396 0 0 0 61903 122 0 0 25 0 1 0 549216428 179548160 40068 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43835 40068 603 41 0 43794 0
vsize: 175340
[startup+630.195 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 41548 0 0 0 62903 123 0 0 25 0 1 0 549216428 180224000 40220 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44000 40220 603 41 0 43959 0
vsize: 176000
[startup+640.194 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 41548 0 0 0 63903 123 0 0 25 0 1 0 549216428 180224000 40220 4294967295 134512640 134672761 3221224528 3221223700 134556667 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.195 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 41548 0 0 0 64904 123 0 0 25 0 1 0 549216428 180224000 40220 4294967295 134512640 134672761 3221224528 3221223700 134556627 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.195 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 41572 0 0 0 65904 123 0 0 25 0 1 0 549216428 180359168 40244 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44033 40244 603 41 0 43992 0
vsize: 176132
[startup+670.195 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 41715 0 0 0 66903 123 0 0 25 0 1 0 549216428 181018624 40387 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44194 40387 603 41 0 44153 0
vsize: 176776
[startup+680.195 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 41882 0 0 0 67903 124 0 0 25 0 1 0 549216428 181694464 40554 4294967295 134512640 134672761 3221224528 3221223696 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44359 40554 603 41 0 44318 0
vsize: 177436
[startup+690.197 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 42040 0 0 0 68903 124 0 0 25 0 1 0 549216428 182366208 40712 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44523 40712 603 41 0 44482 0
vsize: 178092
[startup+700.197 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 42146 0 0 0 69903 124 0 0 25 0 1 0 549216428 182767616 40818 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44621 40818 603 41 0 44580 0
vsize: 178484
[startup+710.197 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 42259 0 0 0 70903 125 0 0 25 0 1 0 549216428 183300096 40931 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44751 40931 603 41 0 44710 0
vsize: 179004
[startup+720.205 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 42401 0 0 0 71903 125 0 0 25 0 1 0 549216428 183840768 41073 4294967295 134512640 134672761 3221224528 3221223664 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44883 41073 603 41 0 44842 0
vsize: 179532
[startup+730.211 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 42531 0 0 0 72904 125 0 0 25 0 1 0 549216428 184373248 41203 4294967295 134512640 134672761 3221224528 3221223632 134559976 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45013 41203 603 41 0 44972 0
vsize: 180052
[startup+740.21 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 42663 0 0 0 73904 125 0 0 25 0 1 0 549216428 184901632 41335 4294967295 134512640 134672761 3221224528 3221223664 134560611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45142 41335 603 41 0 45101 0
vsize: 180568
[startup+750.212 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 42813 0 0 0 74903 126 0 0 25 0 1 0 549216428 185442304 41485 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45274 41485 603 41 0 45233 0
vsize: 181096
[startup+760.22 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 42978 0 0 0 75903 127 0 0 25 0 1 0 549216428 186109952 41650 4294967295 134512640 134672761 3221224528 3221223632 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45437 41650 603 41 0 45396 0
vsize: 181748
[startup+770.219 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 43131 0 0 0 76903 128 0 0 25 0 1 0 549216428 186781696 41803 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45601 41803 603 41 0 45560 0
vsize: 182404
[startup+780.219 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 43273 0 0 0 77902 128 0 0 25 0 1 0 549216428 187314176 41945 4294967295 134512640 134672761 3221224528 3221223696 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45731 41945 603 41 0 45690 0
vsize: 182924
[startup+790.218 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 43425 0 0 0 78902 128 0 0 25 0 1 0 549216428 187985920 42097 4294967295 134512640 134672761 3221224528 3221223632 134559941 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45895 42097 603 41 0 45854 0
vsize: 183580
[startup+800.218 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 43594 0 0 0 79902 129 0 0 25 0 1 0 549216428 188641280 42266 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46055 42266 603 41 0 46014 0
vsize: 184220
[startup+810.218 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 43762 0 0 0 80902 129 0 0 25 0 1 0 549216428 189440000 42434 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46250 42434 603 41 0 46209 0
vsize: 185000
[startup+820.218 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 43936 0 0 0 81902 129 0 0 25 0 1 0 549216428 190160896 42607 4294967295 134512640 134672761 3221224528 3221223632 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46426 42607 603 41 0 46385 0
vsize: 185704
[startup+830.219 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 44026 0 0 0 82902 129 0 0 25 0 1 0 549216428 190578688 42697 4294967295 134512640 134672761 3221224528 3221223632 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46528 42697 603 41 0 46487 0
vsize: 186112
[startup+840.218 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 44045 0 0 0 83902 129 0 0 25 0 1 0 549216428 190513152 42716 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46512 42716 603 41 0 46471 0
vsize: 186048
[startup+850.218 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 44068 0 0 0 84902 130 0 0 25 0 1 0 549216428 190664704 42739 4294967295 134512640 134672761 3221224528 3221223632 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46549 42739 603 41 0 46508 0
vsize: 186196
[startup+860.224 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 44091 0 0 0 85903 130 0 0 25 0 1 0 549216428 190820352 42762 4294967295 134512640 134672761 3221224528 3221223632 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46587 42762 603 41 0 46546 0
vsize: 186348
[startup+870.231 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 44128 0 0 0 86904 130 0 0 25 0 1 0 549216428 190971904 42799 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46624 42799 603 41 0 46583 0
vsize: 186496
[startup+880.232 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 44158 0 0 0 87904 130 0 0 25 0 1 0 549216428 191057920 42829 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46645 42829 603 41 0 46604 0
vsize: 186580
[startup+890.231 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 44178 0 0 0 88904 130 0 0 25 0 1 0 549216428 191057920 42849 4294967295 134512640 134672761 3221224528 3221223632 134560252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46645 42849 603 41 0 46604 0
vsize: 186580
[startup+900.233 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 44205 0 0 0 89904 130 0 0 25 0 1 0 549216428 191201280 42876 4294967295 134512640 134672761 3221224528 3221223632 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46680 42876 603 41 0 46639 0
vsize: 186720
[startup+910.233 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 44233 0 0 0 90904 130 0 0 25 0 1 0 549216428 191340544 42904 4294967295 134512640 134672761 3221224528 3221223632 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46714 42904 603 41 0 46673 0
vsize: 186856
[startup+920.233 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 44258 0 0 0 91904 131 0 0 25 0 1 0 549216428 191467520 42929 4294967295 134512640 134672761 3221224528 3221223632 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46745 42929 603 41 0 46704 0
vsize: 186980
[startup+930.234 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 44287 0 0 0 92904 131 0 0 25 0 1 0 549216428 191623168 42958 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46783 42958 603 41 0 46742 0
vsize: 187132
[startup+940.235 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 44318 0 0 0 93904 131 0 0 25 0 1 0 549216428 191623168 42989 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46783 42989 603 41 0 46742 0
vsize: 187132
[startup+950.235 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 44348 0 0 0 94904 131 0 0 25 0 1 0 549216428 191774720 43019 4294967295 134512640 134672761 3221224528 3221223632 134559937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46820 43019 603 41 0 46779 0
vsize: 187280
[startup+960.235 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 44386 0 0 0 95904 131 0 0 25 0 1 0 549216428 192057344 43057 4294967295 134512640 134672761 3221224528 3221223632 134559955 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46889 43057 603 41 0 46848 0
vsize: 187556
[startup+970.235 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 44402 0 0 0 96904 131 0 0 25 0 1 0 549216428 191991808 43073 4294967295 134512640 134672761 3221224528 3221223632 134560198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46873 43073 603 41 0 46832 0
vsize: 187492
[startup+980.235 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 44433 0 0 0 97904 131 0 0 25 0 1 0 549216428 192155648 43104 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46913 43104 603 41 0 46872 0
vsize: 187652
[startup+990.235 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 44464 0 0 0 98904 131 0 0 25 0 1 0 549216428 192311296 43135 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46951 43135 603 41 0 46910 0
vsize: 187804
[startup+1000.24 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 44491 0 0 0 99905 131 0 0 25 0 1 0 549216428 192458752 43162 4294967295 134512640 134672761 3221224528 3221223632 134560347 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46987 43162 603 41 0 46946 0
vsize: 187948
[startup+1010.24 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 44523 0 0 0 100905 131 0 0 25 0 1 0 549216428 192614400 43194 4294967295 134512640 134672761 3221224528 3221223632 134560150 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47025 43194 603 41 0 46984 0
vsize: 188100
[startup+1020.24 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 44543 0 0 0 101905 132 0 0 25 0 1 0 549216428 192548864 43214 4294967295 134512640 134672761 3221224528 3221223632 134560212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47009 43214 603 41 0 46968 0
vsize: 188036
[startup+1030.24 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 44572 0 0 0 102905 132 0 0 25 0 1 0 549216428 192700416 43243 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47046 43243 603 41 0 47005 0
vsize: 188184
[startup+1040.24 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 44593 0 0 0 103905 132 0 0 25 0 1 0 549216428 192843776 43264 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47081 43264 603 41 0 47040 0
vsize: 188324
[startup+1050.24 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 44632 0 0 0 104905 132 0 0 25 0 1 0 549216428 192999424 43303 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47119 43303 603 41 0 47078 0
vsize: 188476
[startup+1060.24 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 44664 0 0 0 105905 132 0 0 25 0 1 0 549216428 193191936 43335 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47166 43335 603 41 0 47125 0
vsize: 188664
[startup+1070.24 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 44685 0 0 0 106906 132 0 0 25 0 1 0 549216428 193126400 43356 4294967295 134512640 134672761 3221224528 3221223632 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47150 43356 603 41 0 47109 0
vsize: 188600
[startup+1080.24 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 44708 0 0 0 107906 132 0 0 25 0 1 0 549216428 193286144 43379 4294967295 134512640 134672761 3221224528 3221223632 134560376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47189 43379 603 41 0 47148 0
vsize: 188756
[startup+1090.24 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 44740 0 0 0 108906 132 0 0 25 0 1 0 549216428 193441792 43411 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47227 43411 603 41 0 47186 0
vsize: 188908
[startup+1100.24 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 44762 0 0 0 109906 132 0 0 25 0 1 0 549216428 193441792 43433 4294967295 134512640 134672761 3221224528 3221223712 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47227 43433 603 41 0 47186 0
vsize: 188908
[startup+1110.24 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 44865 0 0 0 110906 132 0 0 25 0 1 0 549216428 193863680 43536 4294967295 134512640 134672761 3221224528 3221223632 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47330 43536 603 41 0 47289 0
vsize: 189320
[startup+1120.24 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 44919 0 0 0 111906 132 0 0 25 0 1 0 549216428 194134016 43590 4294967295 134512640 134672761 3221224528 3221223632 134560051 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47396 43590 603 41 0 47355 0
vsize: 189584
[startup+1130.24 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 44940 0 0 0 112907 132 0 0 25 0 1 0 549216428 194281472 43611 4294967295 134512640 134672761 3221224528 3221223632 134559955 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47432 43611 603 41 0 47391 0
vsize: 189728
[startup+1140.24 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 44970 0 0 0 113907 133 0 0 25 0 1 0 549216428 194281472 43641 4294967295 134512640 134672761 3221224528 3221223632 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47432 43641 603 41 0 47391 0
vsize: 189728
[startup+1150.25 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 44997 0 0 0 114907 133 0 0 25 0 1 0 549216428 194433024 43668 4294967295 134512640 134672761 3221224528 3221223632 134560148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47469 43668 603 41 0 47428 0
vsize: 189876
[startup+1160.24 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 45017 0 0 0 115907 133 0 0 25 0 1 0 549216428 194572288 43688 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47503 43688 603 41 0 47462 0
vsize: 190012
[startup+1170.25 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 45047 0 0 0 116908 133 0 0 25 0 1 0 549216428 194654208 43718 4294967295 134512640 134672761 3221224528 3221223632 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47523 43718 603 41 0 47482 0
vsize: 190092
[startup+1180.25 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 45080 0 0 0 117908 133 0 0 25 0 1 0 549216428 194793472 43751 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47557 43751 603 41 0 47516 0
vsize: 190228
[startup+1190.25 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 45109 0 0 0 118908 133 0 0 25 0 1 0 549216428 194883584 43780 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47579 43780 603 41 0 47538 0
vsize: 190316
[startup+1200.25 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 32483
Raw data (stat): 32426 (minisat+) R 32425 11931 11930 0 -1 0 45136 0 0 0 119908 133 0 0 25 0 1 0 549216428 195031040 43807 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47615 43807 603 41 0 47574 0
vsize: 190460
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.35 s]
Raw data (loadavg): 1.00 0.99 0.92 1/54 32483
Raw data (stat): 32426 (minisat+) Z 32425 11931 11930 0 -1 12 45139 0 0 0 119908 142 0 0 25 0 1 0 549216428 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.35
CPU time (s): 1200.51
CPU user time (s): 1199.09
CPU system time (s): 1.42178
CPU usage (%): 100.014
Max. virtual memory (Kb): 190460
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####