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 18374

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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:        738068 kB
Buffers:         24760 kB
Cached:         249416 kB
SwapCached:          0 kB
Active:          26124 kB
Inactive:       250828 kB
HighTotal:      131008 kB
HighFree:        86856 kB
LowTotal:       903652 kB
LowFree:        651212 kB
SwapTotal:     2097136 kB
SwapFree:      2096992 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6844 kB
Slab:            13912 kB
Committed_AS:    71824 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 14:54:51 (client local time) WITH STATUS 10 IN 1200.34 SECONDS
stats: 18148 7 1200.34 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 330 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 328]---> BDD-cost:   77
c ---[ 326]---> BDD-cost:   77
c ---[ 324]---> BDD-cost:   77
c ---[ 322]---> BDD-cost:   77
c ---[ 320]---> BDD-cost:   77
c ---[ 318]---> BDD-cost:   77
c ---[ 316]---> BDD-cost:   77
c ---[ 314]---> BDD-cost:   77
c ---[ 312]---> BDD-cost:   77
c ---[ 310]---> BDD-cost:   77
c ---[ 308]---> BDD-cost:   77
c ---[ 306]---> BDD-cost:   77
c ---[ 304]---> BDD-cost:   77
c ---[ 302]---> BDD-cost:   77
c ---[ 300]---> BDD-cost:   77
c ---[ 298]---> BDD-cost:   77
c ---[ 296]---> BDD-cost:   77
c ---[ 294]---> BDD-cost:   77
c ---[ 292]---> BDD-cost:   77
c ---[ 290]---> BDD-cost:   77
c ---[ 288]---> BDD-cost:   77
c ---[ 286]---> BDD-cost:   77
c ---[ 284]---> BDD-cost:   77
c ---[ 282]---> BDD-cost:   77
c ---[ 280]---> BDD-cost:   77
c ---[ 278]---> BDD-cost:   77
c ---[ 276]---> BDD-cost:   77
c ---[ 274]---> BDD-cost:   77
c ---[ 272]---> BDD-cost:   77
c ---[ 270]---> BDD-cost:   77
c ---[ 268]---> BDD-cost:   77
c ---[ 266]---> BDD-cost:   77
c ---[ 264]---> BDD-cost:   77
c ---[ 262]---> BDD-cost:   77
c ---[ 260]---> BDD-cost:   77
c ---[ 258]---> BDD-cost:   77
c ---[ 256]---> BDD-cost:   77
c ---[ 254]---> BDD-cost:   77
c ---[ 252]---> BDD-cost:   77
c ---[ 250]---> BDD-cost:   77
c ---[ 249]---> BDD-cost:  125
c ---[ 248]---> BDD-cost:  185
c ---[ 247]---> BDD-cost:  185
c ---[ 246]---> BDD-cost:  185
c ---[ 245]---> BDD-cost:  185
c ---[ 244]---> BDD-cost:  185
c ---[ 243]---> BDD-cost:  125
c ---[ 242]---> BDD-cost:  185
c ---[ 241]---> BDD-cost:  185
c ---[ 240]---> BDD-cost:  185
c ---[ 239]---> BDD-cost:  185
c ---[ 238]---> BDD-cost:  125
c ---[ 237]---> BDD-cost:  185
c ---[ 236]---> BDD-cost:  185
c ---[ 235]---> BDD-cost:  185
c ---[ 234]---> BDD-cost:  185
c ---[ 233]---> BDD-cost:  185
c ---[ 232]---> BDD-cost:  125
c ---[ 231]---> BDD-cost:  185
c ---[ 230]---> BDD-cost:  185
c ---[ 229]---> BDD-cost:  185
c ---[ 228]---> BDD-cost:  185
c ---[ 227]---> BDD-cost:  125
c ---[ 226]---> BDD-cost:  185
c ---[ 225]---> BDD-cost:  185
c ---[ 224]---> BDD-cost:  185
c ---[ 223]---> BDD-cost:  185
c ---[ 222]---> BDD-cost:  185
c ---[ 221]---> BDD-cost:  125
c ---[ 220]---> BDD-cost:  185
c ---[ 219]---> BDD-cost:  185
c ---[ 218]---> BDD-cost:  185
c ---[ 217]---> BDD-cost:  185
c ---[ 216]---> BDD-cost:  125
c ---[ 215]---> BDD-cost:  185
c ---[ 214]---> BDD-cost:  185
c ---[ 213]---> BDD-cost:  185
c ---[ 212]---> BDD-cost:  185
c ---[ 211]---> BDD-cost:  185
c ---[ 210]---> BDD-cost:  125
c ---[ 209]---> BDD-cost:  125
c ---[ 208]---> BDD-cost:  185
c ---[ 207]---> BDD-cost:  185
c ---[ 206]---> BDD-cost:  185
c ---[ 205]---> BDD-cost:  185
c ---[ 204]---> BDD-cost:  185
c ---[ 203]---> BDD-cost:  185
c ---[ 202]---> BDD-cost:  185
c ---[ 201]---> BDD-cost:  185
c ---[ 200]---> BDD-cost:  125
c ---[ 199]---> BDD-cost:   75
c ---[ 198]---> BDD-cost:   77
c ---[ 197]---> BDD-cost:   77
c ---[ 196]---> BDD-cost:   77
c ---[ 195]---> BDD-cost:   77
c ---[ 194]---> BDD-cost:   77
c ---[ 193]---> BDD-cost:   77
c ---[ 192]---> BDD-cost:   77
c ---[ 191]---> BDD-cost:   75
c ---[ 190]---> BDD-cost:   77
c ---[ 189]---> BDD-cost:   77
c ---[ 188]---> BDD-cost:   77
c ---[ 187]---> BDD-cost:   77
c ---[ 186]---> BDD-cost:   77
c ---[ 185]---> BDD-cost:   77
c ---[ 184]---> BDD-cost:   77
c ---[ 183]---> BDD-cost:   75
c ---[ 182]---> BDD-cost:   77
c ---[ 181]---> BDD-cost:   77
c ---[ 180]---> BDD-cost:   77
c ---[ 179]---> BDD-cost:   77
c ---[ 178]---> BDD-cost:   77
c ---[ 177]---> BDD-cost:   77
c ---[ 176]---> BDD-cost:   77
c ---[ 175]---> BDD-cost:   75
c ---[ 174]---> BDD-cost:   77
c ---[ 173]---> BDD-cost:   77
c ---[ 172]---> BDD-cost:   77
c ---[ 171]---> BDD-cost:   77
c ---[ 170]---> BDD-cost:   77
c ---[ 169]---> BDD-cost:   77
c ---[ 168]---> BDD-cost:   77
c ---[ 167]---> BDD-cost:   75
c ---[ 166]---> BDD-cost:   77
c ---[ 165]---> BDD-cost:   77
c ---[ 164]---> BDD-cost:   77
c ---[ 163]---> BDD-cost:   77
c ---[ 162]---> BDD-cost:   77
c ---[ 161]---> BDD-cost:   77
c ---[ 160]---> BDD-cost:   77
c ---[ 158]---> BDD-cost:   70
c ---[ 156]---> BDD-cost:   77
c ---[ 154]---> BDD-cost:   77
c ---[ 152]---> BDD-cost:   77
c ---[ 150]---> BDD-cost:   77
c ---[ 148]---> BDD-cost:   77
c ---[ 146]---> BDD-cost:   77
c ---[ 144]---> BDD-cost:   77
c ---[ 142]---> BDD-cost:   70
c ---[ 140]---> BDD-cost:   76
c ---[ 138]---> BDD-cost:   76
c ---[ 136]---> BDD-cost:   76
c ---[ 134]---> BDD-cost:   76
c ---[ 132]---> BDD-cost:   76
c ---[ 130]---> BDD-cost:   76
c ---[ 128]---> BDD-cost:   76
c ---[ 126]---> BDD-cost:   70
c ---[ 124]---> BDD-cost:   77
c ---[ 122]---> BDD-cost:   77
c ---[ 120]---> BDD-cost:   77
c ---[ 118]---> BDD-cost:   77
c ---[ 116]---> BDD-cost:   77
c ---[ 114]---> BDD-cost:   77
c ---[ 112]---> BDD-cost:   77
c ---[ 110]---> BDD-cost:   70
c ---[ 108]---> BDD-cost:   77
c ---[ 106]---> BDD-cost:   77
c ---[ 104]---> BDD-cost:   77
c ---[ 102]---> BDD-cost:   77
c ---[ 100]---> BDD-cost:   77
c ---[  98]---> BDD-cost:   77
c ---[  96]---> BDD-cost:   77
c ---[  94]---> BDD-cost:   70
c ---[  92]---> BDD-cost:   77
c ---[  90]---> BDD-cost:   77
c ---[  88]---> BDD-cost:   77
c ---[  86]---> BDD-cost:   77
c ---[  84]---> BDD-cost:   77
c ---[  82]---> BDD-cost:   77
c ---[  80]---> BDD-cost:   77
c ---[  78]---> BDD-cost:   70
c ---[  76]---> BDD-cost:   77
c ---[  74]---> BDD-cost:   77
c ---[  72]---> BDD-cost:   77
c ---[  70]---> BDD-cost:   77
c ---[  68]---> BDD-cost:   77
c ---[  66]---> BDD-cost:   77
c ---[  64]---> BDD-cost:   77
c ---[  62]---> BDD-cost:   70
c ---[  60]---> BDD-cost:   77
c ---[  58]---> BDD-cost:   77
c ---[  56]---> BDD-cost:   77
c ---[  54]---> BDD-cost:   77
c ---[  52]---> BDD-cost:   77
c ---[  50]---> BDD-cost:   77
c ---[  48]---> BDD-cost:   77
c ---[  46]---> BDD-cost:   70
c ---[  44]---> BDD-cost:   77
c ---[  42]---> BDD-cost:   77
c ---[  40]---> BDD-cost:   77
c ---[  38]---> BDD-cost:   77
c ---[  36]---> BDD-cost:   77
c ---[  34]---> BDD-cost:   77
c ---[  32]---> BDD-cost:   77
c ---[  30]---> BDD-cost:   70
c ---[  28]---> BDD-cost:   77
c ---[  26]---> BDD-cost:   77
c ---[  24]---> BDD-cost:   77
c ---[  22]---> BDD-cost:   77
c ---[  20]---> BDD-cost:   77
c ---[  18]---> BDD-cost:   77
c ---[  16]---> BDD-cost:   77
c ---[  14]---> BDD-cost:   70
c ---[  12]---> BDD-cost:   77
c ---[  10]---> BDD-cost:   77
c ---[   8]---> BDD-cost:   77
c ---[   6]---> BDD-cost:   77
c ---[   4]---> BDD-cost:   77
c ---[   2]---> BDD-cost:   77
c ---[   0]---> BDD-cost:   77
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   96879   272271 |   32293       0        0     nan |  0.000 % |
c |       101 |   96879   272271 |   35522     101      967     9.6 |  1.808 % |
c |       251 |   96879   272271 |   39074     251    15560    62.0 |  1.808 % |
c |       476 |   96859   272211 |   42981     461    20922    45.4 |  1.825 % |
c |       814 |   96859   272211 |   47280     799    66018    82.6 |  1.825 % |
c |      1321 |   96859   272211 |   52008    1306   126690    97.0 |  1.825 % |
c |      2080 |   96824   272106 |   57209    2026   204576   101.0 |  1.856 % |
c |      3219 |   96797   272025 |   62929    3128   342205   109.4 |  1.878 % |
c |      4927 |   96797   272025 |   69222    4836   478953    99.0 |  1.878 % |
c |      7493 |   96733   271837 |   76145    7313   886114   121.2 |  1.935 % |
c |     11338 |   96733   271837 |   83759   11158  1485894   133.2 |  1.935 % |
c ==============================================================================
c [1mFound solution: 1002[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 7750   maxlim: 38998   bits: 16/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13502 |  150826   465059 |   50275   13201  1752710   132.8 |  1.935 % |
c |     13602 |  150816   465029 |   55302   13291  1755401   132.1 |  1.537 % |
c |     13752 |  150816   465029 |   60832   13441  1758879   130.9 |  1.537 % |
c |     13979 |  150816   465029 |   66916   13668  1766286   129.2 |  1.537 % |
c |     14318 |  150802   464989 |   73607   13984  1792741   128.2 |  1.547 % |
c |     14824 |  150797   464974 |   80968   14488  1877274   129.6 |  1.551 % |
c ==============================================================================
c [1mFound solution: 954[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 39046   bits: 16/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15322 |  150798   464996 |   50266   14974  1929135   128.8 |  1.551 % |
c |     15425 |  150798   464996 |   55292   15077  1930454   128.0 |  1.570 % |
c |     15576 |  150798   464996 |   60821   15228  1948982   128.0 |  1.570 % |
c |     15804 |  150784   464958 |   66904   15447  1959100   126.8 |  1.580 % |
c |     16141 |  150764   464898 |   73594   15757  1972279   125.2 |  1.593 % |
c |     16648 |  150739   464825 |   80953   16253  2035906   125.3 |  1.609 % |
c |     17423 |  150715   464757 |   89049   17016  2132837   125.3 |  1.626 % |
c |     18563 |  150701   464719 |   97954   18151  2329014   128.3 |  1.636 % |
c |     20275 |  150691   464689 |  107749   19847  2613250   131.7 |  1.642 % |
c |     22837 |  150637   464531 |  118524   22374  3010744   134.6 |  1.678 % |
c |     26683 |  150627   464501 |  130377   26207  3912167   149.3 |  1.685 % |
c |     32449 |  150608   464446 |  143414   31953  5128065   160.5 |  1.698 % |
c |     41098 |  150535   464227 |  157756   40216  6927844   172.3 |  1.744 % |
c |     54072 |  150315   463587 |  173531   52863  9224192   174.5 |  1.892 % |
c |     73534 |  149943   462473 |  190885   71782 13329193   185.7 |  2.132 % |
c |    102727 |  149532   461246 |  209973  100311 19710121   196.5 |  2.394 % |
c ==============================================================================
c [1mFound solution: 948[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 39052   bits: 16/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    115811 |  149292   460556 |   49764  113123 22734321   201.0 |  2.394 % |
c |    115911 |  149287   460541 |   54740   25375  3049145   120.2 |  2.565 % |
c |    116061 |  149275   460505 |   60214   25520  3080514   120.7 |  2.572 % |
c |    116286 |  149259   460457 |   66235   25743  3089063   120.0 |  2.581 % |
c |    116623 |  149259   460457 |   72859   26080  3126141   119.9 |  2.581 % |
c |    117130 |  149239   460397 |   80145   26576  3168858   119.2 |  2.595 % |
c |    117889 |  149214   460322 |   88159   27321  3290242   120.4 |  2.611 % |
c |    119029 |  149214   460322 |   96975   28461  3538289   124.3 |  2.611 % |
c |    120738 |  149203   460289 |  106673   30164  3865069   128.1 |  2.617 % |
c |    123302 |  149128   460064 |  117340   32651  4295278   131.6 |  2.667 % |
c |    127147 |  149054   459844 |  129074   36444  5104109   140.1 |  2.716 % |
c |    132913 |  148983   459635 |  141982   42176  5971945   141.6 |  2.762 % |
c |    141562 |  148707   458815 |  156180   50638  7514908   148.4 |  2.939 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x10212_bit0 -x10312_bit0 -x20312_bit0 -x10412_bit0 -x20412_bit0 -x30412_bit0 -x10512_bit0 -x20512_bit0 -x30512_bit0 -x40512_bit0 -x10612_bit0 -x20612_bit0 -x30612_bit0 -x40612_bit0 -x50612_bit0 -x10712_bit0 -x20712_bit0 -x30712_bit0 -x40712_bit0 -x50712_bit0 -x60712_bit0 -x10812_bit0 -x20812_bit0 -x30812_bit0 -x40812_bit0 -x50812_bit0 -x60812_bit0 -x70812_bit0 -x10912_bit0 -x20912_bit0 -x30912_bit0 -x40912_bit0 -x50912_bit0 x60912_bit0 -x70912_bit0 -x80912_bit0 -x11012_bit0 -x21012_bit0 -x31012_bit0 -x41012_bit0 -x51012_bit0 -x61012_bit0 -x71012_bit0 -x81012_bit0 -x91012_bit0 -x10222_bit0 -x10322_bit0 -x20322_bit0 -x10422_bit0 -x20422_bit0 -x30422_bit0 x10522_bit0 -x20522_bit0 -x30522_bit0 -x40522_bit0 -x10622_bit0 -x20622_bit0 -x30622_bit0 -x40622_bit0 -x50622_bit0 -x10722_bit0 -x20722_bit0 -x30722_bit0 -x40722_bit0 -x50722_bit0 -x60722_bit0 -x10822_bit0 -x20822_bit0 -x30822_bit0 -x40822_bit0 -x50822_bit0 -x60822_bit0 -x70822_bit0 -x10922_bit0 -x20922_bit0 -x30922_bit0 -x40922_bit0 -x50922_bit0 -x60922_bit0 -x70922_bit0 -x80922_bit0 -x11022_bit0 -x21022_bit0 -x31022_bit0 -x41022_bit0 -x51022_bit0 -x61022_bit0 -x71022_bit0 -x81022_bit0 -x91022_bit0 -x10232_bit0 -x10332_bit0 -x20332_bit0 -x10432_bit0 -x20432_bit0 -x30432_bit0 -x10532_bit0 -x20532_bit0 -x30532_bit0 -x40532_bit0 -x10632_bit0 -x20632_bit0 -x30632_bit0 -x40632_bit0 -x50632_bit0 -x10732_bit0 -x20732_bit0 -x30732_bit0 -x40732_bit0 -x50732_bit0 -x60732_bit0 -x10832_bit0 -x20832_bit0 -x30832_bit0 -x40832_bit0 -x50832_bit0 -x60832_bit0 -x70832_bit0 -x10932_bit0 -x20932_bit0 -x30932_bit0 -x40932_bit0 -x50932_bit0 -x60932_bit0 -x70932_bit0 -x80932_bit0 -x11032_bit0 -x21032_bit0 x31032_bit0 -x41032_bit0 -x51032_bit0 -x61032_bit0 -x71032_bit0 -x81032_bit0 -x91032_bit0 -x10242_bit0 -x10342_bit0 -x20342_bit0 -x10442_bit0 -x20442_bit0 -x30442_bit0 -x10542_bit0 -x20542_bit0 -x30542_bit0 -x40542_bit0 -x10642_bit0 -x20642_bit0 -x30642_bit0 -x40642_bit0 -x50642_bit0 -x10742_bit0 -x20742_bit0 -x30742_bit0 -x40742_bit0 -x50742_bit0 -x60742_bit0 -x10842_bit0 -x20842_bit0 -x30842_bit0 x40842_bit0 -x50842_bit0 -x60842_bit0 -x70842_bit0 -x10942_bit0 -x20942_bit0 -x30942_bit0 -x40942_bit0 -x50942_bit0 -x60942_bit0 -x70942_bit0 -x80942_bit0 -x11042_bit0 -x21042_bit0 -x31042_bit0 -x41042_bit0 -x51042_bit0 -x61042_bit0 -x71042_bit0 -x81042_bit0 -x91042_bit0 -x10252_bit0 -x10352_bit0 -x20352_bit0 -x10452_bit0 -x20452_bit0 -x30452_bit0 -x10552_bit0 -x20552_bit0 -x30552_bit0 -x40552_bit0 -x10652_bit0 -x20652_bit0 -x30652_bit0 -x40652_bit0 -x50652_bit0 -x10752_bit0 x20752_bit0 -x30752_bit0 -x40752_bit0 -x50752_bit0 -x60752_bit0 -x10852_bit0 -x20852_bit0 -x30852_bit0 -x40852_bit0 -x50852_bit0 -x60852_bit0 -x70852_bit0 -x10952_bit0 -x20952_bit0 -x30952_bit0 -x40952_bit0 -x50952_bit0 -x60952_bit0 -x70952_bit0 -x80952_bit0 -x11052_bit0 -x21052_bit0 -x31052_bit0 -x41052_bit0 -x51052_bit0 -x61052_bit0 -x71052_bit0 -x81052_bit0 -x91052_bit0 -x10213_bit0 -x10313_bit0 -x20313_bit0 -x10413_bit0 -x20413_bit0 -x30413_bit0 -x10513_bit0 -x20513_bit0 -x30513_bit0 -x40513_bit0 -x10613_bit0 -x20613_bit0 -x30613_bit0 -x40613_bit0 -x50613_bit0 -x10713_bit0 -x20713_bit0 -x30713_bit0 -x40713_bit0 x50713_bit0 -x60713_bit0 -x10813_bit0 -x20813_bit0 -x30813_bit0 -x40813_bit0 -x50813_bit0 -x60813_bit0 -x70813_bit0 -x10913_bit0 -x20913_bit0 -x30913_bit0 -x40913_bit0 -x50913_bit0 -x60913_bit0 -x70913_bit0 -x80913_bit0 -x11013_bit0 -x21013_bit0 -x31013_bit0 -x41013_bit0 -x51013_bit0 -x61013_bit0 -x71013_bit0 -x81013_bit0 -x91013_bit0 -x10223_bit0 -x10323_bit0 -x20323_bit0 -x10423_bit0 -x20423_bit0 -x30423_bit0 -x10523_bit0 -x20523_bit0 -x30523_bit0 -x40523_bit0 -x10623_bit0 -x20623_bit0 -x30623_bit0 -x40623_bit0 -x50623_bit0 -x10723_bit0 -x20723_bit0 -x30723_bit0 -x40723_bit0 -x50723_bit0 -x60723_bit0 -x10823_bit0 -x20823_bit0 -x30823_bit0 -x40823_bit0 -x50823_bit0 -x60823_bit0 -x70823_bit0 -x10923_bit0 -x20923_bit0 -x30923_bit0 -x40923_bit0 -x50923_bit0 -x60923_bit0 -x70923_bit0 -x80923_bit0 -x11023_bit0 -x21023_bit0 -x31023_bit0 x41023_bit0 -x51023_bit0 -x61023_bit0 -x71023_bit0 -x81023_bit0 -x91023_bit0 -x10233_bit0 -x10333_bit0 -x20333_bit0 -x10433_bit0 -x20433_bit0 -x30433_bit0 -x10533_bit0 -x20533_bit0 -x30533_bit0 -x40533_bit0 -x10633_bit0 -x20633_bit0 -x30633_bit0 -x40633_bit0 -x50633_bit0 -x10733_bit0 -x20733_bit0 -x30733_bit0 -x40733_bit0 -x50733_bit0 -x60733_bit0 -x10833_bit0 -x20833_bit0 -x30833_bit0 -x40833_bit0 -x50833_bit0 -x60833_bit0 -x70833_bit0 -x10933_bit0 x20933_bit0 -x30933_bit0 -x40933_bit0 -x50933_bit0 -x60933_bit0 -x70933_bit0 -x80933_bit0 -x11033_bit0 -x21033_bit0 -x31033_bit0 -x41033_bit0 -x51033_bit0 -x61033_bit0 -x71033_bit0 -x81033_bit0 -x91033_bit0 -x10243_bit0 -x10343_bit0 -x20343_bit0 -x10443_bit0 -x20443_bit0 -x30443_bit0 -x10543_bit0 -x20543_bit0 -x30543_bit0 -x40543_bit0 x10643_bit0 -x20643_bit0 -x30643_bit0 -x40643_bit0 -x50643_bit0 -x10743_bit0 -x20743_bit0 -x30743_bit0 -x40743_bit0 -x50743_bit0 -x60743_bit0 -x10843_bit0 -x20843_bit0 -x30843_bit0 -x40843_bit0 -x50843_bit0 -x60843_bit0 -x70843_bit0 -x10943_bit0 -x20943_bit0 -x30943_bit0 -x40943_bit0 -x50943_bit0 -x60943_bit0 -x70943_bit0 -x80943_bit0 -x11043_bit0 -x21043_bit0 -x31043_bit0 -x41043_bit0 -x51043_bit0 -x61043_bit0 -x71043_bit0 -x81043_bit0 -x91043_bit0 -x10253_bit0 -x10353_bit0 -x20353_bit0 -x10453_bit0 -x20453_bit0 -x30453_bit0 -x10553_bit0 -x20553_bit0 -x30553_bit0 -x40553_bit0 -x10653_bit0 -x20653_bit0 -x30653_bit0 -x40653_bit0 -x50653_bit0 -x10753_bit0 -x20753_bit0 -x30753_bit0 -x40753_bit0 -x50753_bit0 -x60753_bit0 -x10853_bit0 -x20853_bit0 x30853_bit0 -x40853_bit0 -x50853_bit0 -x60853_bit0 -x70853_bit0 -x10953_bit0 -x20953_bit0 -x30953_bit0 -x40953_bit0 -x50953_bit0 -x60953_bit0 -x70953_bit0 -x80953_bit0 -x11053_bit0 -x21053_bit0 -x31053_bit0 -x41053_bit0 -x51053_bit0 -x61053_bit0 -x71053_bit0 -x81053_bit0 -x91053_bit0 -x10214_bit0 -x10314_bit0 -x20314_bit0 -x10414_bit0 -x20414_bit0 -x30414_bit0 -x10514_bit0 -x20514_bit0 -x30514_bit0 -x40514_bit0 -x10614_bit0 -x20614_bit0 x30614_bit0 -x40614_bit0 -x50614_bit0 -x10714_bit0 -x20714_bit0 -x30714_bit0 -x40714_bit0 -x50714_bit0 -x60714_bit0 -x10814_bit0 -x20814_bit0 -x30814_bit0 -x40814_bit0 -x50814_bit0 -x60814_bit0 -x70814_bit0 -x10914_bit0 -x20914_bit0 -x30914_bit0 -x40914_bit0 -x50914_bit0 -x60914_bit0 -x70914_bit0 -x80914_bit0 -x11014_bit0 -x21014_bit0 -x31014_bit0 -x41014_bit0 -x51014_bit0 -x61014_bit0 -x71014_bit0 -x81014_bit0 -x91014_bit0 -x10224_bit0 -x10324_bit0 -x20324_bit0 -x10424_bit0 -x20424_bit0 -x30424_bit0 -x10524_bit0 -x20524_bit0 -x30524_bit0 -x40524_bit0 -x10624_bit0 -x20624_bit0 -x30624_bit0 -x40624_bit0 -x50624_bit0 -x10724_bit0 -x20724_bit0 -x30724_bit0 -x40724_bit0 -x50724_bit0 -x60724_bit0 -x10824_bit0 -x20824_bit0 -x30824_bit0 -x40824_bit0 -x50824_bit0 -x60824_bit0 -x70824_bit0 -x10924_bit0 -x20924_bit0 -x30924_bit0 -x40924_bit0 -x50924_bit0 -x60924_bit0 -x70924_bit0 -x80924_bit0 -x11024_bit0 x21024_bit0 -x31024_bit0 -x41024_bit0 -x51024_bit0 -x61024_bit0 -x71024_bit0 -x81024_bit0 -x91024_bit0 -x10234_bit0 -x10334_bit0 -x20334_bit0 -x10434_bit0 -x20434_bit0 -x30434_bit0 -x10534_bit0 -x20534_bit0 -x30534_bit0 -x40534_bit0 -x10634_bit0 -x20634_bit0 -x30634_bit0 -x40634_bit0 -x50634_bit0 -x10734_bit0 -x20734_bit0 -x30734_bit0 -x40734_bit0 -x50734_bit0 -x60734_bit0 -x10834_bit0 -x20834_bit0 -x30834_bit0 -x40834_bit0 -x50834_bit0 -x60834_bit0 -x70834_bit0 -x10934_bit0 -x20934_bit0 -x30934_bit0 -x40934_bit0 -x50934_bit0 -x60934_bit0 -x70934_bit0 x80934_bit0 -x11034_bit0 -x21034_bit0 -x31034_bit0 -x41034_bit0 -x51034_bit0 -x61034_bit0 -x71034_bit0 -x81034_bit0 -x91034_bit0 -x10244_bit0 -x10344_bit0 -x20344_bit0 -x10444_bit0 -x20444_bit0 -x30444_bit0 -x10544_bit0 -x20544_bit0 -x30544_bit0 -x40544_bit0 -x10644_bit0 -x20644_bit0 -x30644_bit0 -x40644_bit0 -x50644_bit0 x10744_bit0 -x20744_bit0 -x30744_bit0 -x40744_bit0 -x50744_bit0 -x60744_bit0 -x10844_bit0 -x20844_bit0 -x30844_bit0 -x40844_bit0 -x50844_bit0 -x60844_bit0 -x70844_bit0 -x10944_bit0 -x20944_bit0 -x30944_bit0 -x40944_bit0 -x50944_bit0 -x60944_bit0 -x70944_bit0 -x80944_bit0 -x11044_bit0 -x21044_bit0 -x31044_bit0 -x41044_bit0 -x51044_bit0 -x61044_bit0 -x71044_bit0 -x81044_bit0 -x91044_bit0 -x10254_bit0 -x10354_bit0 -x20354_bit0 -x10454_bit0 -x20454_bit0 -x30454_bit0 -x10554_bit0 -x20554_bit0 -x30554_bit0 x40554_bit0 -x10654_bit0 -x20654_bit0 -x30654_bit0 -x40654_bit0 -x50654_bit0 -x10754_bit0 -x20754_bit0 -x30754_bit0 -x40754_bit0 -x50754_bit0 -x60754_bit0 -x10854_bit0 -x20854_bit0 -x30854_bit0 -x40854_bit0 -x50854_bit0 -x60854_bit0 -x70854_bit0 -x10954_bit0 -x20954_bit0 -x30954_bit0 -x40954_bit0 -x50954_bit0 -x60954_bit0 -x70954_bit0 -x80954_bit0 -x11054_bit0 -x21054_bit0 -x31054_bit0 -x41054_bit0 -x51054_bit0 -x61054_bit0 -x71054_bit0 -x81054_bit0 -x91054_bit0 -x10215_bit0 -x10315_bit0 -x20315_bit0 -x10415_bit0 -x20415_bit0 -x30415_bit0 -x10515_bit0 -x20515_bit0 -x30515_bit0 -x40515_bit0 -x10615_bit0 -x20615_bit0 -x30615_bit0 -x40615_bit0 -x50615_bit0 -x10715_bit0 -x20715_bit0 -x30715_bit0 -x40715_bit0 -x50715_bit0 -x60715_bit0 -x10815_bit0 -x20815_bit0 -x30815_bit0 -x40815_bit0 -x50815_bit0 -x60815_bit0 -x70815_bit0 -x10915_bit0 -x20915_bit0 -x30915_bit0 x40915_bit0 -x50915_bit0 -x60915_bit0 -x70915_bit0 -x80915_bit0 -x11015_bit0 -x21015_bit0 -x31015_bit0 -x41015_bit0 -x51015_bit0 -x61015_bit0 -x71015_bit0 -x81015_bit0 -x91015_bit0 -x10225_bit0 -x10325_bit0 -x20325_bit0 -x10425_bit0 -x20425_bit0 -x30425_bit0 -x10525_bit0 -x20525_bit0 -x30525_bit0 -x40525_bit0 -x10625_bit0 x20625_bit0 -x30625_bit0 -x40625_bit0 -x50625_bit0 -x10725_bit0 -x20725_bit0 -x30725_bit0 -x40725_bit0 -x50725_bit0 -x60725_bit0 -x10825_bit0 -x20825_bit0 -x30825_bit0 -x40825_bit0 -x50825_bit0 -x60825_bit0 -x70825_bit0 -x10925_bit0 -x20925_bit0 -x30925_bit0 -x40925_bit0 -x50925_bit0 -x60925_bit0 -x70925_bit0 -x80925_bit0 -x11025_bit0 -x21025_bit0 -x31025_bit0 -x41025_bit0 -x51025_bit0 -x61025_bit0 -x71025_bit0 -x81025_bit0 -x91025_bit0 -x10235_bit0 -x10335_bit0 -x20335_bit0 -x10435_bit0 -x20435_bit0 -x30435_bit0 -x10535_bit0 -x20535_bit0 -x30535_bit0 -x40535_bit0 -x10635_bit0 -x20635_bit0 -x30635_bit0 -x40635_bit0 -x50635_bit0 -x10735_bit0 -x20735_bit0 -x30735_bit0 -x40735_bit0 -x50735_bit0 -x60735_bit0 x10835_bit0 -x20835_bit0 -x30835_bit0 -x40835_bit0 -x50835_bit0 -x60835_bit0 -x70835_bit0 -x10935_bit0 -x20935_bit0 -x30935_bit0 -x40935_bit0 -x50935_bit0 -x60935_bit0 -x70935_bit0 -x80935_bit0 -x11035_bit0 -x21035_bit0 -x31035_bit0 -x41035_bit0 -x51035_bit0 -x61035_bit0 -x71035_bit0 -x81035_bit0 -x91035_bit0 -x10245_bit0 -x10345_bit0 -x20345_bit0 -x10445_bit0 -x20445_bit0 -x30445_bit0 -x10545_bit0 -x20545_bit0 -x30545_bit0 -x40545_bit0 -x10645_bit0 -x20645_bit0 -x30645_bit0 -x40645_bit0 -x50645_bit0 -x10745_bit0 -x20745_bit0 -x30745_bit0 -x40745_bit0 -x50745_bit0 -x60745_bit0 -x10845_bit0 -x20845_bit0 -x30845_bit0 -x40845_bit0 -x50845_bit0 -x60845_bit0 -x70845_bit0 -x10945_bit0 -x20945_bit0 -x30945_bit0 -x40945_bit0 -x50945_bit0 -x60945_bit0 -x70945_bit0 -x80945_bit0 -x11045_bit0 -x21045_bit0 -x31045_bit0 -x41045_bit0 x51045_bit0 -x61045_bit0 -x71045_bit0 -x81045_bit0 -x91045_bit0 -x10255_bit0 -x10355_bit0 -x20355_bit0 -x10455_bit0 -x20455_bit0 -x30455_bit0 -x10555_bit0 -x20555_bit0 -x30555_bit0 -x40555_bit0 -x10655_bit0 -x20655_bit0 -x30655_bit0 -x40655_bit0 -x50655_bit0 -x10755_bit0 -x20755_bit0 x30755_bit0 -x40755_bit0 -x50755_bit0 -x60755_bit0 -x10855_bit0 -x20855_bit0 -x30855_bit0 -x40855_bit0 -x50855_bit0 -x60855_bit0 -x70855_bit0 -x10955_bit0 -x20955_bit0 -x30955_bit0 -x40955_bit0 -x50955_bit0 -x60955_bit0 -x70955_bit0 -x80955_bit0 -x11055_bit0 -x21055_bit0 -x31055_bit0 -x41055_bit0 -x51055_bit0 -x61055_bit0 -x71055_bit0 -x81055_bit0 -x91055_bit0 -x10216_bit0 -x10316_bit0 -x20316_bit0 -x10416_bit0 -x20416_bit0 -x30416_bit0 -x10516_bit0 -x20516_bit0 x30516_bit0 -x40516_bit0 -x10616_bit0 -x20616_bit0 -x30616_bit0 -x40616_bit0 -x50616_bit0 -x10716_bit0 -x20716_bit0 -x30716_bit0 -x40716_bit0 -x50716_bit0 -x60716_bit0 -x10816_bit0 -x20816_bit0 -x30816_bit0 -x40816_bit0 -x50816_bit0 -x60816_bit0 -x70816_bit0 -x10916_bit0 -x20916_bit0 -x30916_bit0 -x40916_bit0 -x50916_bit0 -x60916_bit0 -x70916_bit0 -x80916_bit0 -x11016_bit0 -x21016_bit0 -x31016_bit0 -x41016_bit0 -x51016_bit0 -x61016_bit0 -x71016_bit0 -x81016_bit0 -x91016_bit0 -x10226_bit0 -x10326_bit0 -x20326_bit0 -x10426_bit0 -x20426_bit0 -x30426_bit0 -x10526_bit0 -x20526_bit0 -x30526_bit0 -x40526_bit0 -x10626_bit0 -x20626_bit0 -x30626_bit0 -x40626_bit0 -x50626_bit0 -x10726_bit0 -x20726_bit0 -x30726_bit0 -x40726_bit0 -x50726_bit0 -x60726_bit0 -x10826_bit0 -x20826_bit0 -x30826_bit0 -x40826_bit0 -x50826_bit0 -x60826_bit0 -x70826_bit0 -x10926_bit0 -x20926_bit0 -x30926_bit0 -x40926_bit0 -x50926_bit0 -x60926_bit0 x70926_bit0 -x80926_bit0 -x11026_bit0 -x21026_bit0 -x31026_bit0 -x41026_bit0 -x51026_bit0 -x61026_bit0 -x71026_bit0 -x81026_bit0 -x91026_bit0 -x10236_bit0 -x10336_bit0 -x20336_bit0 -x10436_bit0 -x20436_bit0 -x30436_bit0 -x10536_bit0 -x20536_bit0 -x30536_bit0 -x40536_bit0 -x10636_bit0 -x20636_bit0 -x30636_bit0 -x40636_bit0 -x50636_bit0 -x10736_bit0 -x20736_bit0 -x30736_bit0 -x40736_bit0 -x50736_bit0 -x60736_bit0 -x10836_bit0 -x20836_bit0 -x30836_bit0 -x40836_bit0 -x50836_bit0 -x60836_bit0 -x70836_bit0 -x10936_bit0 -x20936_bit0 -x30936_bit0 -x40936_bit0 -x50936_bit0 -x60936_bit0 -x70936_bit0 -x80936_bit0 x11036_bit0 -x21036_bit0 -x31036_bit0 -x41036_bit0 -x51036_bit0 -x61036_bit0 -x71036_bit0 -x81036_bit0 -x91036_bit0 -x10246_bit0 -x10346_bit0 -x20346_bit0 -x10446_bit0 x20446_bit0 -x30446_bit0 -x10546_bit0 -x20546_bit0 -x30546_bit0 -x40546_bit0 -x10646_bit0 -x20646_bit0 -x30646_bit0 -x40646_bit0 -x50646_bit0 -x10746_bit0 -x20746_bit0 -x30746_bit0 -x40746_bit0 -x50746_bit0 -x60746_bit0 -x10846_bit0 -x20846_bit0 -x30846_bit0 -x40846_bit0 -x50846_bit0 -x60846_bit0 -x70846_bit0 -x10946_bit0 -x20946_bit0 -x30946_bit0 -x40946_bit0 -x50946_bit0 -x60946_bit0 -x70946_bit0 -x80946_bit0 -x11046_bit0 -x21046_bit0 -x31046_bit0 -x41046_bit0 -x51046_bit0 -x61046_bit0 -x71046_bit0 -x81046_bit0 -x91046_bit0 -x10256_bit0 -x10356_bit0 -x20356_bit0 -x10456_bit0 -x20456_bit0 -x30456_bit0 -x10556_bit0 -x20556_bit0 -x30556_bit0 -x40556_bit0 -x10656_bit0 -x20656_bit0 -x30656_bit0 -x40656_bit0 -x50656_bit0 -x10756_bit0 -x20756_bit0 -x30756_bit0 -x40756_bit0 -x50756_bit0 -x60756_bit0 -x10856_bit0 -x20856_bit0 -x30856_bit0 -x40856_bit0 -x50856_bit0 x60856_bit0 -x70856_bit0 -x10956_bit0 -x20956_bit0 -x30956_bit0 -x40956_bit0 -x50956_bit0 -x60956_bit0 -x70956_bit0 -x80956_bit0 -x11056_bit0 -x21056_bit0 -x31056_bit0 -x41056_bit0 -x51056_bit0 -x61056_bit0 -x71056_bit0 -x81056_bit0 -x91056_bit0 -x10217_bit0 -x10317_bit0 -x20317_bit0 -x10417_bit0 -x20417_bit0 -x30417_bit0 -x10517_bit0 -x20517_bit0 -x30517_bit0 -x40517_bit0 -x10617_bit0 -x20617_bit0 -x30617_bit0 -x40617_bit0 -x50617_bit0 -x10717_bit0 -x20717_bit0 -x30717_bit0 -x40717_bit0 -x50717_bit0 -x60717_bit0 -x10817_bit0 x20817_bit0 -x30817_bit0 -x40817_bit0 -x50817_bit0 -x60817_bit0 -x70817_bit0 -x10917_bit0 -x20917_bit0 -x30917_bit0 -x40917_bit0 -x50917_bit0 -x60917_bit0 -x70917_bit0 -x80917_bit0 -x11017_bit0 -x21017_bit0 -x31017_bit0 -x41017_bit0 -x51017_bit0 -x61017_bit0 -x71017_bit0 -x81017_bit0 -x91017_bit0 -x10227_bit0 x10327_bit0 -x20327_bit0 -x10427_bit0 -x20427_bit0 -x30427_bit0 -x10527_bit0 -x20527_bit0 -x30527_bit0 -x40527_bit0 -x10627_bit0 -x20627_bit0 -x30627_bit0 -x40627_bit0 -x50627_bit0 -x10727_bit0 -x20727_bit0 -x30727_bit0 -x40727_bit0 -x50727_bit0 -x60727_bit0 -x10827_bit0 -x20827_bit0 -x30827_bit0 -x40827_bit0 -x50827_bit0 -x60827_bit0 -x70827_bit0 -x10927_bit0 -x20927_bit0 -x30927_bit0 -x40927_bit0 -x50927_bit0 -x60927_bit0 -x70927_bit0 -x80927_bit0 -x11027_bit0 -x21027_bit0 -x31027_bit0 -x41027_bit0 -x51027_bit0 -x61027_bit0 -x71027_bit0 -x81027_bit0 -x91027_bit0 -x10237_bit0 -x10337_bit0 -x20337_bit0 -x10437_bit0 -x20437_bit0 -x30437_bit0 -x10537_bit0 -x20537_bit0 -x30537_bit0 -x40537_bit0 -x10637_bit0 -x20637_bit0 -x30637_bit0 -x40637_bit0 -x50637_bit0 -x10737_bit0 -x20737_bit0 -x30737_bit0 x40737_bit0 -x50737_bit0 -x60737_bit0 -x10837_bit0 -x20837_bit0 -x30837_bit0 -x40837_bit0 -x50837_bit0 -x60837_bit0 -x70837_bit0 -x10937_bit0 -x20937_bit0 -x30937_bit0 -x40937_bit0 -x50937_bit0 -x60937_bit0 -x70937_bit0 -x80937_bit0 -x11037_bit0 -x21037_bit0 -x31037_bit0 -x41037_bit0 -x51037_bit0 -x61037_bit0 -x71037_bit0 -x81037_bit0 -x91037_bit0 -x10247_bit0 -x10347_bit0 -x20347_bit0 -x10447_bit0 -x20447_bit0 -x30447_bit0 -x10547_bit0 -x20547_bit0 -x30547_bit0 -x40547_bit0 -x10647_bit0 -x20647_bit0 -x30647_bit0 -x40647_bit0 -x50647_bit0 -x10747_bit0 -x20747_bit0 -x30747_bit0 -x40747_bit0 -x50747_bit0 -x60747_bit0 -x10847_bit0 -x20847_bit0 -x30847_bit0 -x40847_bit0 -x50847_bit0 -x60847_bit0 -x70847_bit0 -x10947_bit0 -x20947_bit0 -x30947_bit0 -x40947_bit0 x50947_bit0 -x60947_bit0 -x70947_bit0 -x80947_bit0 -x11047_bit0 -x21047_bit0 -x31047_bit0 -x41047_bit0 -x51047_bit0 -x61047_bit0 -x71047_bit0 -x81047_bit0 -x91047_bit0 -x10257_bit0 -x10357_bit0 -x20357_bit0 -x10457_bit0 -x20457_bit0 -x30457_bit0 -x10557_bit0 -x20557_bit0 -x30557_bit0 -x40557_bit0 -x10657_bit0 -x20657_bit0 -x30657_bit0 -x40657_bit0 -x50657_bit0 -x10757_bit0 -x20757_bit0 -x30757_bit0 -x40757_bit0 -x50757_bit0 -x60757_bit0 -x10857_bit0 -x20857_bit0 -x30857_bit0 -x40857_bit0 -x50857_bit0 -x60857_bit0 -x70857_bit0 -x10957_bit0 -x20957_bit0 -x30957_bit0 -x40957_bit0 -x50957_bit0 -x60957_bit0 -x70957_bit0 -x80957_bit0 -x11057_bit0 -x21057_bit0 -x31057_bit0 -x41057_bit0 -x51057_bit0 x61057_bit0 -x71057_bit0 -x81057_bit0 -x91057_bit0 -x10218_bit0 -x10318_bit0 -x20318_bit0 -x10418_bit0 -x20418_bit0 -x30418_bit0 -x10518_bit0 -x20518_bit0 -x30518_bit0 -x40518_bit0 -x10618_bit0 -x20618_bit0 -x30618_bit0 -x40618_bit0 -x50618_bit0 -x10718_bit0 -x20718_bit0 -x30718_bit0 -x40718_bit0 -x50718_bit0 -x60718_bit0 -x10818_bit0 -x20818_bit0 -x30818_bit0 -x40818_bit0 -x50818_bit0 -x60818_bit0 -x70818_bit0 -x10918_bit0 -x20918_bit0 -x30918_bit0 -x40918_bit0 -x50918_bit0 -x60918_bit0 -x70918_bit0 -x80918_bit0 -x11018_bit0 -x21018_bit0 -x31018_bit0 -x41018_bit0 -x51018_bit0 -x61018_bit0 x71018_bit0 -x81018_bit0 -x91018_bit0 -x10228_bit0 -x10328_bit0 -x20328_bit0 -x10428_bit0 -x20428_bit0 -x30428_bit0 -x10528_bit0 -x20528_bit0 -x30528_bit0 -x40528_bit0 -x10628_bit0 -x20628_bit0 -x30628_bit0 -x40628_bit0 -x50628_bit0 -x10728_bit0 -x20728_bit0 -x30728_bit0 -x40728_bit0 -x50728_bit0 -x60728_bit0 -x10828_bit0 -x20828_bit0 -x30828_bit0 -x40828_bit0 x50828_bit0 -x60828_bit0 -x70828_bit0 -x10928_bit0 -x20928_bit0 -x30928_bit0 -x40928_bit0 -x50928_bit0 -x60928_bit0 -x70928_bit0 -x80928_bit0 -x11028_bit0 -x21028_bit0 -x31028_bit0 -x41028_bit0 -x51028_bit0 -x61028_bit0 -x71028_bit0 -x81028_bit0 -x91028_bit0 -x10238_bit0 -x10338_bit0 -x20338_bit0 -x10438_bit0 -x20438_bit0 -x30438_bit0 -x10538_bit0 -x20538_bit0 -x30538_bit0 -x40538_bit0 -x10638_bit0 -x20638_bit0 -x30638_bit0 x40638_bit0 -x50638_bit0 -x10738_bit0 -x20738_bit0 -x30738_bit0 -x40738_bit0 -x50738_bit0 -x60738_bit0 -x10838_bit0 -x20838_bit0 -x30838_bit0 -x40838_bit0 -x50838_bit0 -x60838_bit0 -x70838_bit0 -x10938_bit0 -x20938_bit0 -x30938_bit0 -x40938_bit0 -x50938_bit0 -x60938_bit0 -x70938_bit0 -x80938_bit0 -x11038_bit0 -x21038_bit0 -x31038_bit0 -x41038_bit0 -x51038_bit0 -x61038_bit0 -x71038_bit0 -x81038_bit0 -x91038_bit0 -x10248_bit0 -x10348_bit0 x20348_bit0 -x10448_bit0 -x20448_bit0 -x30448_bit0 -x10548_bit0 -x20548_bit0 -x30548_bit0 -x40548_bit0 -x10648_bit0 -x20648_bit0 -x30648_bit0 -x40648_bit0 -x50648_bit0 -x10748_bit0 -x20748_bit0 -x30748_bit0 -x40748_bit0 -x50748_bit0 -x60748_bit0 -x10848_bit0 -x20848_bit0 -x30848_bit0 -x40848_bit0 -x50848_bit0 -x60848_bit0 -x70848_bit0 -x10948_bit0 -x20948_bit0 -x30948_bit0 -x40948_bit0 -x50948_bit0 -x60948_bit0 -x70948_bit0 -x80948_bit0 -x11048_bit0 -x21048_bit0 -x31048_bit0 -x41048_bit0 -x51048_bit0 -x61048_bit0 -x71048_bit0 -x81048_bit0 -x91048_bit0 -x10258_bit0 -x10358_bit0 -x20358_bit0 -x10458_bit0 -x20458_bit0 -x30458_bit0 -x10558_bit0 -x20558_bit0 -x30558_bit0 -x40558_bit0 -x10658_bit0 -x20658_bit0 -x30658_bit0 -x40658_bit0 -x50658_bit0 -x10758_bit0 -x20758_bit0 -x30758_bit0 -x40758_bit0 -x50758_bit0 -x60758_bit0 -x10858_bit0 -x20858_bit0 -x30858_bit0 -x40858_bit0 -x50858_bit0 -x60858_bit0 -x70858_bit0 x10958_bit0 -x20958_bit0 -x30958_bit0 -x40958_bit0 -x50958_bit0 -x60958_bit0 -x70958_bit0 -x80958_bit0 -x11058_bit0 -x21058_bit0 -x31058_bit0 -x41058_bit0 -x51058_bit0 -x61058_bit0 -x71058_bit0 -x81058_bit0 -x91058_bit0 #### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.97 0.91 2/54 13367
Raw data (stat): 13367 (runsolver) R 13366 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487613552 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0008 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 2819 0 0 0 991 7 0 0 25 0 1 0 487613552 13705216 2780 4294967295 134512640 134672761 3221224544 3221223696 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3346 2780 603 41 0 3305 0
vsize: 13384
[startup+20.0019 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 3224 0 0 0 1989 8 0 0 25 0 1 0 487613552 15347712 3185 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3747 3185 603 41 0 3706 0
vsize: 14988
[startup+30.002 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 3619 0 0 0 2988 9 0 0 25 0 1 0 487613552 16982016 3580 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4146 3580 603 41 0 4105 0
vsize: 16584
[startup+40.0022 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 4013 0 0 0 3987 11 0 0 25 0 1 0 487613552 18599936 3974 4294967295 134512640 134672761 3221224544 3221223560 1075353266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4541 3974 603 41 0 4500 0
vsize: 18164
[startup+50.0023 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 10437 0 0 0 4972 25 0 0 25 0 1 0 487613552 41345024 9077 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10094 9077 603 41 0 10053 0
vsize: 40376
[startup+60.0032 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 10825 0 0 0 5971 27 0 0 25 0 1 0 487613552 42590208 9397 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10398 9397 603 41 0 10357 0
vsize: 41592
[startup+70.0037 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 11094 0 0 0 6970 27 0 0 25 0 1 0 487613552 43716608 9666 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10673 9666 603 41 0 10632 0
vsize: 42692
[startup+80.0038 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 11402 0 0 0 7969 29 0 0 25 0 1 0 487613552 45060096 9974 4294967295 134512640 134672761 3221224544 3221223648 134559995 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11001 9974 603 41 0 10960 0
vsize: 44004
[startup+90.0047 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 11698 0 0 0 8968 30 0 0 25 0 1 0 487613552 46264320 10270 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11295 10270 603 41 0 11254 0
vsize: 45180
[startup+100.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 12035 0 0 0 9967 31 0 0 25 0 1 0 487613552 47611904 10607 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11624 10607 603 41 0 11583 0
vsize: 46496
[startup+110.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 12498 0 0 0 10966 31 0 0 25 0 1 0 487613552 49496064 11070 4294967295 134512640 134672761 3221224544 3221223648 134559908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12084 11070 603 41 0 12043 0
vsize: 48336
[startup+120.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 12851 0 0 0 11964 34 0 0 25 0 1 0 487613552 50978816 11423 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12446 11423 603 41 0 12405 0
vsize: 49784
[startup+130.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 13159 0 0 0 12963 35 0 0 25 0 1 0 487613552 52183040 11731 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12740 11731 603 41 0 12699 0
vsize: 50960
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 13450 0 0 0 13962 36 0 0 25 0 1 0 487613552 53391360 12022 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13035 12022 603 41 0 12994 0
vsize: 52140
[startup+150.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 13790 0 0 0 14962 37 0 0 25 0 1 0 487613552 54722560 12362 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13360 12362 603 41 0 13319 0
vsize: 53440
[startup+160.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 14149 0 0 0 15961 38 0 0 25 0 1 0 487613552 56205312 12721 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13722 12721 603 41 0 13681 0
vsize: 54888
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 14432 0 0 0 16960 39 0 0 25 0 1 0 487613552 57516032 13004 4294967295 134512640 134672761 3221224544 3221223728 134559607 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14042 13004 603 41 0 14001 0
vsize: 56168
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 14730 0 0 0 17959 40 0 0 25 0 1 0 487613552 58720256 13302 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14336 13302 603 41 0 14295 0
vsize: 57344
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 15000 0 0 0 18959 40 0 0 25 0 1 0 487613552 59797504 13572 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14599 13572 603 41 0 14558 0
vsize: 58396
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 15281 0 0 0 19958 41 0 0 25 0 1 0 487613552 61005824 13853 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14894 13853 603 41 0 14853 0
vsize: 59576
[startup+210.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 15626 0 0 0 20958 42 0 0 25 0 1 0 487613552 62349312 14198 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15222 14198 603 41 0 15181 0
vsize: 60888
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 15920 0 0 0 21957 43 0 0 25 0 1 0 487613552 63561728 14492 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15518 14492 603 41 0 15477 0
vsize: 62072
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 16193 0 0 0 22956 44 0 0 25 0 1 0 487613552 64626688 14765 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15778 14765 603 41 0 15737 0
vsize: 63112
[startup+240.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 16478 0 0 0 23955 45 0 0 25 0 1 0 487613552 65830912 15050 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16072 15050 603 41 0 16031 0
vsize: 64288
[startup+250.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 16724 0 0 0 24955 46 0 0 25 0 1 0 487613552 66899968 15296 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16333 15296 603 41 0 16292 0
vsize: 65332
[startup+260.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 16990 0 0 0 25954 47 0 0 25 0 1 0 487613552 67977216 15562 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16596 15562 603 41 0 16555 0
vsize: 66384
[startup+270.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 17267 0 0 0 26953 48 0 0 25 0 1 0 487613552 69054464 15839 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16859 15839 603 41 0 16818 0
vsize: 67436
[startup+280.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 17577 0 0 0 27953 48 0 0 25 0 1 0 487613552 70266880 16149 4294967295 134512640 134672761 3221224544 3221223680 134565064 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17155 16149 603 41 0 17114 0
vsize: 68620
[startup+290.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 17778 0 0 0 28953 49 0 0 25 0 1 0 487613552 71069696 16350 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17351 16350 603 41 0 17310 0
vsize: 69404
[startup+300.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 18016 0 0 0 29952 49 0 0 25 0 1 0 487613552 72138752 16588 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17612 16588 603 41 0 17571 0
vsize: 70448
[startup+310.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 18190 0 0 0 30952 49 0 0 25 0 1 0 487613552 72810496 16762 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17776 16762 603 41 0 17735 0
vsize: 71104
[startup+320.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 18388 0 0 0 31952 50 0 0 25 0 1 0 487613552 73609216 16960 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17971 16960 603 41 0 17930 0
vsize: 71884
[startup+330.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 18655 0 0 0 32951 51 0 0 25 0 1 0 487613552 74678272 17227 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18232 17227 603 41 0 18191 0
vsize: 72928
[startup+340.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 18918 0 0 0 33951 52 0 0 25 0 1 0 487613552 75755520 17490 4294967295 134512640 134672761 3221224544 3221223680 134565089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18495 17490 603 41 0 18454 0
vsize: 73980
[startup+350.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 19227 0 0 0 34950 52 0 0 25 0 1 0 487613552 77086720 17799 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18820 17799 603 41 0 18779 0
vsize: 75280
[startup+360.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 19400 0 0 0 35950 53 0 0 25 0 1 0 487613552 77754368 17972 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18983 17972 603 41 0 18942 0
vsize: 75932
[startup+370.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 19828 0 0 0 36949 54 0 0 25 0 1 0 487613552 79491072 18400 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19407 18400 603 41 0 19366 0
vsize: 77628
[startup+380.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 20085 0 0 0 37948 55 0 0 25 0 1 0 487613552 80564224 18657 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19669 18657 603 41 0 19628 0
vsize: 78676
[startup+390.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 20289 0 0 0 38948 56 0 0 25 0 1 0 487613552 81362944 18861 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19864 18861 603 41 0 19823 0
vsize: 79456
[startup+400.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 20534 0 0 0 39947 57 0 0 25 0 1 0 487613552 82436096 19106 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20126 19106 603 41 0 20085 0
vsize: 80504
[startup+410.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 20669 0 0 0 40947 57 0 0 25 0 1 0 487613552 82968576 19241 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20256 19241 603 41 0 20215 0
vsize: 81024
[startup+420.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 20872 0 0 0 41947 57 0 0 25 0 1 0 487613552 83771392 19444 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20452 19444 603 41 0 20411 0
vsize: 81808
[startup+430.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 21085 0 0 0 42946 58 0 0 25 0 1 0 487613552 84570112 19657 4294967295 134512640 134672761 3221224544 3221223680 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20647 19657 603 41 0 20606 0
vsize: 82588
[startup+440.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 21244 0 0 0 43945 59 0 0 25 0 1 0 487613552 85491712 19816 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20872 19816 603 41 0 20831 0
vsize: 83488
[startup+450.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 21536 0 0 0 44945 59 0 0 25 0 1 0 487613552 86683648 20108 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21163 20108 603 41 0 21122 0
vsize: 84652
[startup+460.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 21821 0 0 0 45944 60 0 0 25 0 1 0 487613552 87883776 20393 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21456 20393 603 41 0 21415 0
vsize: 85824
[startup+470.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 22055 0 0 0 46944 61 0 0 25 0 1 0 487613552 88829952 20627 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21687 20627 603 41 0 21646 0
vsize: 86748
[startup+480.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 22228 0 0 0 47943 62 0 0 25 0 1 0 487613552 89509888 20800 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21853 20800 603 41 0 21812 0
vsize: 87412
[startup+490.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 22425 0 0 0 48943 62 0 0 25 0 1 0 487613552 90312704 20997 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22049 20997 603 41 0 22008 0
vsize: 88196
[startup+500.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 22635 0 0 0 49942 63 0 0 25 0 1 0 487613552 91254784 21207 4294967295 134512640 134672761 3221224544 3221223648 134560501 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22279 21207 603 41 0 22238 0
vsize: 89116
[startup+510.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 22873 0 0 0 50942 64 0 0 25 0 1 0 487613552 92176384 21445 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22504 21446 603 41 0 22463 0
vsize: 90016
[startup+520.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 23100 0 0 0 51941 64 0 0 25 0 1 0 487613552 93110272 21672 4294967295 134512640 134672761 3221224544 3221223728 134558883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22732 21672 603 41 0 22691 0
vsize: 90928
[startup+530.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 23349 0 0 0 52940 65 0 0 25 0 1 0 487613552 94044160 21921 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22960 21921 603 41 0 22919 0
vsize: 91840
[startup+540.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 23576 0 0 0 53942 66 0 0 25 0 1 0 487613552 94978048 22148 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23188 22148 603 41 0 23147 0
vsize: 92752
[startup+550.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 23731 0 0 0 54942 67 0 0 25 0 1 0 487613552 95653888 22303 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23353 22303 603 41 0 23312 0
vsize: 93412
[startup+560.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 24033 0 0 0 55941 67 0 0 25 0 1 0 487613552 96854016 22605 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23646 22605 603 41 0 23605 0
vsize: 94584
[startup+570.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 24161 0 0 0 56942 68 0 0 25 0 1 0 487613552 97386496 22733 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23776 22733 603 41 0 23735 0
vsize: 95104
[startup+580.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 24439 0 0 0 57941 69 0 0 25 0 1 0 487613552 98603008 23011 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24073 23011 603 41 0 24032 0
vsize: 96292
[startup+590.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 24568 0 0 0 58941 69 0 0 25 0 1 0 487613552 99135488 23140 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24203 23140 603 41 0 24162 0
vsize: 96812
[startup+600.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 24794 0 0 0 59942 70 0 0 25 0 1 0 487613552 99938304 23366 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24399 23366 603 41 0 24358 0
vsize: 97596
[startup+610.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 24964 0 0 0 60942 71 0 0 25 0 1 0 487613552 100749312 23536 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24597 23536 603 41 0 24556 0
vsize: 98388
[startup+620.077 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 25224 0 0 0 61942 71 0 0 25 0 1 0 487613552 101691392 23796 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24827 23796 603 41 0 24786 0
vsize: 99308
[startup+630.077 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 25406 0 0 0 62941 71 0 0 25 0 1 0 487613552 102494208 23978 4294967295 134512640 134672761 3221224544 3221223648 134559937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25023 23978 603 41 0 24982 0
vsize: 100092
[startup+640.077 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 25579 0 0 0 63941 72 0 0 25 0 1 0 487613552 103165952 24151 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25187 24151 603 41 0 25146 0
vsize: 100748
[startup+650.078 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 25811 0 0 0 64941 73 0 0 25 0 1 0 487613552 104095744 24383 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25414 24383 603 41 0 25373 0
vsize: 101656
[startup+660.079 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 26083 0 0 0 65940 74 0 0 25 0 1 0 487613552 105299968 24655 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25708 24655 603 41 0 25667 0
vsize: 102832
[startup+670.079 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 26169 0 0 0 66940 74 0 0 25 0 1 0 487613552 105566208 24741 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25773 24741 603 41 0 25732 0
vsize: 103092
[startup+680.079 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 26367 0 0 0 67939 74 0 0 25 0 1 0 487613552 106369024 24939 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25969 24939 603 41 0 25928 0
vsize: 103876
[startup+690.08 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 26658 0 0 0 68939 75 0 0 25 0 1 0 487613552 107569152 25230 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26262 25230 603 41 0 26221 0
vsize: 105048
[startup+700.08 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 26869 0 0 0 69939 75 0 0 25 0 1 0 487613552 108498944 25441 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26489 25441 603 41 0 26448 0
vsize: 105956
[startup+710.081 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 27170 0 0 0 70939 76 0 0 25 0 1 0 487613552 109731840 25742 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26790 25742 603 41 0 26749 0
vsize: 107160
[startup+720.081 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 27467 0 0 0 71938 76 0 0 25 0 1 0 487613552 110936064 26039 4294967295 134512640 134672761 3221224544 3221223728 134559033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27084 26039 603 41 0 27043 0
vsize: 108336
[startup+730.08 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 27706 0 0 0 72938 77 0 0 25 0 1 0 487613552 111874048 26278 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27313 26278 603 41 0 27272 0
vsize: 109252
[startup+740.081 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 27939 0 0 0 73938 77 0 0 25 0 1 0 487613552 112816128 26511 4294967295 134512640 134672761 3221224544 3221223716 134556685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27543 26511 603 41 0 27502 0
vsize: 110172
[startup+750.081 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 28115 0 0 0 74937 78 0 0 25 0 1 0 487613552 113627136 26687 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27741 26687 603 41 0 27700 0
vsize: 110964
[startup+760.082 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 28238 0 0 0 75937 79 0 0 25 0 1 0 487613552 114032640 26810 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27840 26810 603 41 0 27799 0
vsize: 111360
[startup+770.082 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 28281 0 0 0 76937 79 0 0 25 0 1 0 487613552 114298880 26853 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27905 26853 603 41 0 27864 0
vsize: 111620
[startup+780.082 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 28405 0 0 0 77937 79 0 0 25 0 1 0 487613552 114700288 26977 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28003 26977 603 41 0 27962 0
vsize: 112012
[startup+790.082 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 28591 0 0 0 78936 80 0 0 25 0 1 0 487613552 115503104 27163 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28199 27163 603 41 0 28158 0
vsize: 112796
[startup+800.082 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 28878 0 0 0 79936 80 0 0 25 0 1 0 487613552 116682752 27450 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28487 27450 603 41 0 28446 0
vsize: 113948
[startup+810.083 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 29178 0 0 0 80936 80 0 0 25 0 1 0 487613552 117886976 27750 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28781 27750 603 41 0 28740 0
vsize: 115124
[startup+820.083 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 29384 0 0 0 81936 81 0 0 25 0 1 0 487613552 118697984 27956 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28979 27956 603 41 0 28938 0
vsize: 115916
[startup+830.083 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 29607 0 0 0 82934 82 0 0 25 0 1 0 487613552 119635968 28179 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29208 28179 603 41 0 29167 0
vsize: 116832
[startup+840.084 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 29722 0 0 0 83934 82 0 0 25 0 1 0 487613552 120180736 28294 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29341 28294 603 41 0 29300 0
vsize: 117364
[startup+850.084 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 29952 0 0 0 84933 83 0 0 25 0 1 0 487613552 121118720 28524 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29570 28524 603 41 0 29529 0
vsize: 118280
[startup+860.084 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 30194 0 0 0 85932 84 0 0 25 0 1 0 487613552 122044416 28766 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29796 28766 603 41 0 29755 0
vsize: 119184
[startup+870.084 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 30394 0 0 0 86932 85 0 0 25 0 1 0 487613552 122847232 28966 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29992 28966 603 41 0 29951 0
vsize: 119968
[startup+880.084 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 30662 0 0 0 87932 85 0 0 25 0 1 0 487613552 123916288 29234 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30253 29234 603 41 0 30212 0
vsize: 121012
[startup+890.084 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 30957 0 0 0 88930 87 0 0 25 0 1 0 487613552 125112320 29529 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30545 29529 603 41 0 30504 0
vsize: 122180
[startup+900.086 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 31032 0 0 0 89930 87 0 0 25 0 1 0 487613552 125521920 29604 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30645 29604 603 41 0 30604 0
vsize: 122580
[startup+910.086 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 31242 0 0 0 90930 87 0 0 25 0 1 0 487613552 126324736 29814 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30841 29814 603 41 0 30800 0
vsize: 123364
[startup+920.091 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 31542 0 0 0 91930 88 0 0 25 0 1 0 487613552 127508480 30114 4294967295 134512640 134672761 3221224544 3221223712 134560845 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31130 30114 603 41 0 31089 0
vsize: 124520
[startup+930.095 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 31816 0 0 0 92930 89 0 0 25 0 1 0 487613552 128708608 30388 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31423 30388 603 41 0 31382 0
vsize: 125692
[startup+940.096 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 32074 0 0 0 93930 89 0 0 25 0 1 0 487613552 129785856 30646 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31686 30646 603 41 0 31645 0
vsize: 126744
[startup+950.096 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 32243 0 0 0 94929 90 0 0 25 0 1 0 487613552 130457600 30815 4294967295 134512640 134672761 3221224544 3221223648 134559853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31850 30815 603 41 0 31809 0
vsize: 127400
[startup+960.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 32357 0 0 0 95929 90 0 0 25 0 1 0 487613552 130863104 30929 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31949 30929 603 41 0 31908 0
vsize: 127796
[startup+970.099 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 32486 0 0 0 96929 91 0 0 25 0 1 0 487613552 131403776 31058 4294967295 134512640 134672761 3221224544 3221223648 134560520 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32081 31058 603 41 0 32040 0
vsize: 128324
[startup+980.099 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 32568 0 0 0 97929 91 0 0 25 0 1 0 487613552 131674112 31140 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32147 31140 603 41 0 32106 0
vsize: 128588
[startup+990.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 32751 0 0 0 98928 91 0 0 25 0 1 0 487613552 131932160 31203 4294967295 134512640 134672761 3221224544 3221223728 134559463 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1000.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 32751 0 0 0 99929 91 0 0 25 0 1 0 487613552 131932160 31203 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1010.12 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 32751 0 0 0 100930 91 0 0 25 0 1 0 487613552 131932160 31203 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1020.14 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 32751 0 0 0 101932 91 0 0 25 0 1 0 487613552 131932160 31203 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1030.14 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 32751 0 0 0 102933 91 0 0 25 0 1 0 487613552 131932160 31203 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1040.14 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 32751 0 0 0 103933 92 0 0 25 0 1 0 487613552 131932160 31203 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1050.14 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 32751 0 0 0 104933 92 0 0 25 0 1 0 487613552 131932160 31203 4294967295 134512640 134672761 3221224544 3221223648 134559853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1060.14 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 32751 0 0 0 105933 92 0 0 25 0 1 0 487613552 131932160 31203 4294967295 134512640 134672761 3221224544 3221223728 134558875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1070.14 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 32751 0 0 0 106933 92 0 0 25 0 1 0 487613552 131932160 31203 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1080.14 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 32751 0 0 0 107933 92 0 0 25 0 1 0 487613552 131932160 31203 4294967295 134512640 134672761 3221224544 3221223744 134557887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1090.14 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 32751 0 0 0 108933 92 0 0 25 0 1 0 487613552 131932160 31203 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1100.14 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 32751 0 0 0 109934 92 0 0 25 0 1 0 487613552 131932160 31203 4294967295 134512640 134672761 3221224544 3221223712 134561234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1110.14 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 32751 0 0 0 110933 92 0 0 25 0 1 0 487613552 131932160 31203 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1120.14 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 32751 0 0 0 111933 92 0 0 25 0 1 0 487613552 131932160 31203 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1130.14 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 32751 0 0 0 112934 92 0 0 25 0 1 0 487613552 131932160 31203 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1140.14 s]
Raw data (loadavg): 1.07 1.00 0.93 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 32751 0 0 0 113935 92 0 0 25 0 1 0 487613552 131932160 31203 4294967295 134512640 134672761 3221224544 3221223712 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1150.14 s]
Raw data (loadavg): 1.06 1.00 0.93 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 32751 0 0 0 114935 92 0 0 25 0 1 0 487613552 131932160 31203 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1160.15 s]
Raw data (loadavg): 1.05 1.00 0.93 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 32751 0 0 0 115935 92 0 0 25 0 1 0 487613552 131932160 31203 4294967295 134512640 134672761 3221224544 3221223680 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1170.14 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 32751 0 0 0 116935 92 0 0 25 0 1 0 487613552 131932160 31203 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1180.14 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 32751 0 0 0 117935 92 0 0 25 0 1 0 487613552 131932160 31203 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1190.14 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 32751 0 0 0 118935 92 0 0 25 0 1 0 487613552 131932160 31203 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
[startup+1200.15 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 13367
Raw data (stat): 13367 (minisat+) R 13366 10720 10719 0 -1 0 32751 0 0 0 119936 92 0 0 25 0 1 0 487613552 131932160 31203 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32210 31203 603 41 0 32169 0
vsize: 128840
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.21 s]
Raw data (loadavg): 1.02 1.00 0.93 1/54 13367
Raw data (stat): 13367 (minisat+) Z 13366 10720 10719 0 -1 12 32754 0 0 0 119936 97 0 0 25 0 1 0 487613552 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.21
CPU time (s): 1200.34
CPU user time (s): 1199.37
CPU system time (s): 0.977851
CPU usage (%): 100.011
Max. virtual memory (Kb): 128840
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####