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/miplib2003/normalized-mps-v2-13-7-10teams.opb
MD5SUM	1ff3cc3253012886aa21be4feac6111e
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.75
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 18874

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc7 THE 2005-04-21 16:57:18 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17381 boxname=wulflinc7 idbench=1337 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  1ff3cc3253012886aa21be4feac6111e  /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-10teams.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-10teams.opb /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-10teams.opb
IDLAUNCH: 17381
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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.050
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:        768320 kB
Buffers:         10188 kB
Cached:         233764 kB
SwapCached:        304 kB
Active:          19624 kB
Inactive:       226908 kB
HighTotal:      131008 kB
HighFree:        68572 kB
LowTotal:       903652 kB
LowFree:        699748 kB
SwapTotal:     2097136 kB
SwapFree:      2096520 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6448 kB
Slab:            13936 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 17:17:21 (client local time) WITH STATUS 10 IN 1200.24 SECONDS
stats: 17381 7 1200.24 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 ---[ 329]---> BDD-cost:  125
c ---[ 328]---> BDD-cost:  185
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 ---[ 307]---> BDD-cost:  185
c ---[ 305]---> BDD-cost:   77
c ---[ 303]---> BDD-cost:   77
c ---[ 301]---> BDD-cost:   77
c ---[ 299]---> BDD-cost:   77
c ---[ 297]---> BDD-cost:   77
c ---[ 295]---> BDD-cost:   77
c ---[ 293]---> BDD-cost:   77
c ---[ 291]---> BDD-cost:   77
c ---[ 289]---> BDD-cost:   77
c ---[ 288]---> BDD-cost:  125
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 ---[ 269]---> BDD-cost:  185
c ---[ 267]---> BDD-cost:   77
c ---[ 265]---> BDD-cost:   77
c ---[ 263]---> BDD-cost:   77
c ---[ 261]---> BDD-cost:   77
c ---[ 259]---> BDD-cost:   77
c ---[ 257]---> BDD-cost:   77
c ---[ 255]---> BDD-cost:   77
c ---[ 253]---> BDD-cost:   77
c ---[ 251]---> BDD-cost:   77
c ---[ 250]---> BDD-cost:  185
c ---[ 248]---> BDD-cost:   70
c ---[ 246]---> BDD-cost:   77
c ---[ 244]---> BDD-cost:   77
c ---[ 242]---> BDD-cost:   77
c ---[ 240]---> BDD-cost:   77
c ---[ 238]---> BDD-cost:   77
c ---[ 236]---> BDD-cost:   77
c ---[ 234]---> BDD-cost:   77
c ---[ 233]---> BDD-cost:  185
c ---[ 231]---> BDD-cost:   77
c ---[ 229]---> BDD-cost:   77
c ---[ 227]---> BDD-cost:   77
c ---[ 225]---> BDD-cost:   77
c ---[ 223]---> BDD-cost:   77
c ---[ 221]---> BDD-cost:   77
c ---[ 219]---> BDD-cost:   77
c ---[ 217]---> BDD-cost:   77
c ---[ 216]---> BDD-cost:  185
c ---[ 214]---> BDD-cost:   70
c ---[ 212]---> BDD-cost:   77
c ---[ 210]---> BDD-cost:   77
c ---[ 208]---> BDD-cost:   77
c ---[ 206]---> BDD-cost:   77
c ---[ 204]---> BDD-cost:   77
c ---[ 202]---> BDD-cost:   77
c ---[ 200]---> BDD-cost:   77
c ---[ 198]---> BDD-cost:   70
c ---[ 197]---> BDD-cost:  185
c ---[ 195]---> BDD-cost:   77
c ---[ 193]---> BDD-cost:   77
c ---[ 191]---> BDD-cost:   77
c ---[ 189]---> BDD-cost:   77
c ---[ 187]---> BDD-cost:   77
c ---[ 185]---> BDD-cost:   77
c ---[ 183]---> BDD-cost:   77
c ---[ 181]---> BDD-cost:   77
c ---[ 179]---> BDD-cost:   77
c ---[ 178]---> BDD-cost:  125
c ---[ 176]---> BDD-cost:   77
c ---[ 174]---> BDD-cost:   77
c ---[ 172]---> BDD-cost:   77
c ---[ 170]---> BDD-cost:   77
c ---[ 168]---> BDD-cost:   77
c ---[ 166]---> BDD-cost:   77
c ---[ 164]---> BDD-cost:   77
c ---[ 162]---> BDD-cost:   77
c ---[ 160]---> BDD-cost:   77
c ---[ 159]---> BDD-cost:  185
c ---[ 157]---> BDD-cost:   77
c ---[ 155]---> BDD-cost:   77
c ---[ 153]---> BDD-cost:   77
c ---[ 151]---> BDD-cost:   77
c ---[ 149]---> BDD-cost:   77
c ---[ 147]---> BDD-cost:   77
c ---[ 145]---> BDD-cost:   77
c ---[ 143]---> BDD-cost:   77
c ---[ 141]---> BDD-cost:   77
c ---[ 140]---> BDD-cost:  185
c ---[ 139]---> BDD-cost:  185
c ---[ 137]---> BDD-cost:   77
c ---[ 135]---> BDD-cost:   77
c ---[ 133]---> BDD-cost:   77
c ---[ 131]---> BDD-cost:   77
c ---[ 129]---> BDD-cost:   77
c ---[ 127]---> BDD-cost:   77
c ---[ 125]---> BDD-cost:   77
c ---[ 123]---> BDD-cost:   77
c ---[ 121]---> BDD-cost:   77
c ---[ 120]---> BDD-cost:  178
c ---[ 118]---> BDD-cost:   77
c ---[ 116]---> BDD-cost:   77
c ---[ 114]---> BDD-cost:   77
c ---[ 112]---> BDD-cost:   77
c ---[ 110]---> BDD-cost:   77
c ---[ 108]---> BDD-cost:   77
c ---[ 106]---> BDD-cost:   77
c ---[ 104]---> BDD-cost:   77
c ---[ 102]---> BDD-cost:   77
c ---[ 101]---> BDD-cost:  185
c ---[  99]---> BDD-cost:   77
c ---[  97]---> BDD-cost:   77
c ---[  95]---> BDD-cost:   77
c ---[  93]---> BDD-cost:   77
c ---[  91]---> BDD-cost:   77
c ---[  89]---> BDD-cost:   77
c ---[  87]---> BDD-cost:   77
c ---[  85]---> BDD-cost:   77
c ---[  83]---> BDD-cost:   77
c ---[  82]---> BDD-cost:  125
c ---[  80]---> BDD-cost:   77
c ---[  79]---> BDD-cost:  185
c ---[  78]---> BDD-cost:  185
c ---[  77]---> BDD-cost:  178
c ---[  76]---> BDD-cost:  185
c ---[  75]---> BDD-cost:  185
c ---[  74]---> BDD-cost:  125
c ---[  73]---> BDD-cost:  185
c ---[  72]---> BDD-cost:  185
c ---[  71]---> BDD-cost:  178
c ---[  70]---> BDD-cost:  185
c ---[  69]---> BDD-cost:  185
c ---[  68]---> BDD-cost:  125
c ---[  67]---> BDD-cost:  185
c ---[  66]---> BDD-cost:  178
c ---[  65]---> BDD-cost:  185
c ---[  64]---> BDD-cost:  185
c ---[  63]---> BDD-cost:  185
c ---[  62]---> BDD-cost:  185
c ---[  61]---> BDD-cost:  125
c ---[  60]---> BDD-cost:  118
c ---[  59]---> BDD-cost:  185
c ---[  58]---> BDD-cost:  185
c ---[  57]---> BDD-cost:  185
c ---[  56]---> BDD-cost:  185
c ---[  55]---> BDD-cost:  178
c ---[  54]---> BDD-cost:  185
c ---[  53]---> BDD-cost:  185
c ---[  52]---> BDD-cost:  185
c ---[  51]---> BDD-cost:  185
c ---[  50]---> BDD-cost:  125
c ---[  49]---> BDD-cost:   76
c ---[  48]---> BDD-cost:   76
c ---[  47]---> BDD-cost:   76
c ---[  46]---> BDD-cost:   76
c ---[  45]---> BDD-cost:   76
c ---[  44]---> BDD-cost:   76
c ---[  43]---> BDD-cost:   76
c ---[  42]---> BDD-cost:   76
c ---[  41]---> BDD-cost:  177
c ---[  40]---> BDD-cost:   77
c ---[  39]---> BDD-cost:   77
c ---[  38]---> BDD-cost:   77
c ---[  37]---> BDD-cost:   77
c ---[  36]---> BDD-cost:   77
c ---[  35]---> BDD-cost:   77
c ---[  34]---> BDD-cost:   77
c ---[  33]---> BDD-cost:   77
c ---[  32]---> BDD-cost:  123
c ---[  31]---> BDD-cost:   77
c ---[  30]---> BDD-cost:   77
c ---[  29]---> BDD-cost:   77
c ---[  28]---> BDD-cost:   77
c ---[  27]---> BDD-cost:   77
c ---[  26]---> BDD-cost:   77
c ---[  25]---> BDD-cost:   77
c ---[  24]---> BDD-cost:   77
c ---[  23]---> BDD-cost:   77
c ---[  22]---> BDD-cost:  183
c ---[  21]---> BDD-cost:   77
c ---[  20]---> BDD-cost:   77
c ---[  19]---> BDD-cost:   77
c ---[  18]---> BDD-cost:   77
c ---[  17]---> BDD-cost:   77
c ---[  16]---> BDD-cost:   77
c ---[  15]---> BDD-cost:   77
c ---[  14]---> BDD-cost:   75
c ---[  13]---> BDD-cost:   77
c ---[  12]---> BDD-cost:  183
c ---[  11]---> BDD-cost:   77
c ---[  10]---> BDD-cost:   77
c ---[   9]---> BDD-cost:   77
c ---[   8]---> BDD-cost:   77
c ---[   7]---> 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 |       100 |   96879   272271 |   35522     100     1730    17.3 |  1.808 % |
c |       254 |   96879   272271 |   39074     254    14889    58.6 |  1.808 % |
c |       479 |   96879   272271 |   42981     479    22013    46.0 |  1.808 % |
c |       817 |   96865   272233 |   47280     772    54650    70.8 |  1.821 % |
c |      1323 |   96860   272218 |   52008    1262   108205    85.7 |  1.825 % |
c |      2082 |   96851   272195 |   57209    2020   215660   106.8 |  1.834 % |
c |      3223 |   96826   272122 |   62929    3107   315239   101.5 |  1.856 % |
c |      4931 |   96816   272092 |   69222    4810   524420   109.0 |  1.865 % |
c |      7494 |   96812   272082 |   76145    7372  1290700   175.1 |  1.869 % |
c |     11340 |   96802   272052 |   83759   11211  2265427   202.1 |  1.878 % |
c ==============================================================================
c [1mFound solution: 990[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 7750   maxlim: 39010   bits: 16/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15218 |  150947   465413 |   50315   15089  2966251   196.6 |  1.878 % |
c |     15319 |  150947   465413 |   55346   15190  2969038   195.5 |  1.449 % |
c |     15470 |  150942   465398 |   60881   15334  2982866   194.5 |  1.452 % |
c |     15695 |  150942   465398 |   66969   15559  3001723   192.9 |  1.452 % |
c |     16033 |  150932   465368 |   73666   15869  3030304   191.0 |  1.459 % |
c |     16541 |  150932   465368 |   81032   16377  3061737   187.0 |  1.459 % |
c |     17300 |  150925   465347 |   89136   17130  3143049   183.5 |  1.462 % |
c |     18439 |  150905   465287 |   98049   18255  3395522   186.0 |  1.475 % |
c |     20150 |  150905   465287 |  107854   19966  3692405   184.9 |  1.475 % |
c ==============================================================================
c [1mFound solution: 960[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 39040   bits: 16/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22213 |  150872   465199 |   50290   21890  3850334   175.9 |  1.475 % |
c |     22313 |  150857   465154 |   55319   21972  3851082   175.3 |  1.514 % |
c |     22468 |  150857   465154 |   60850   22127  3868350   174.8 |  1.514 % |
c |     22695 |  150847   465124 |   66935   22345  3878505   173.6 |  1.521 % |
c |     23032 |  150847   465124 |   73629   22682  3933835   173.4 |  1.521 % |
c |     23538 |  150847   465124 |   80992   23188  4024104   173.5 |  1.521 % |
c |     24297 |  150837   465094 |   89091   23914  4246563   177.6 |  1.528 % |
c |     25437 |  150837   465094 |   98000   25054  4355736   173.9 |  1.528 % |
c |     27145 |  150837   465094 |  107801   26762  4578398   171.1 |  1.528 % |
c |     29708 |  150827   465064 |  118581   29311  4976809   169.8 |  1.534 % |
c |     33553 |  150802   464989 |  130439   33117  5779370   174.5 |  1.551 % |
c |     39319 |  150792   464959 |  143483   38866  7449632   191.7 |  1.557 % |
c |     47969 |  150726   464765 |  157831   47455  9021328   190.1 |  1.600 % |
c |     60944 |  150504   464109 |  173614   60156 11395048   189.4 |  1.741 % |
c ==============================================================================
c [1mFound solution: 950[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 39050   bits: 16/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     63099 |  150510   464147 |   50170   62311 11854221   190.2 |  1.741 % |
c |     63200 |  150510   464147 |   55187   19112  2370976   124.1 |  1.751 % |
c |     63350 |  150510   464147 |   60705   19262  2373735   123.2 |  1.751 % |
c |     63576 |  150505   464132 |   66776   19484  2378803   122.1 |  1.754 % |
c |     63913 |  150489   464084 |   73453   19814  2407439   121.5 |  1.764 % |
c |     64421 |  150479   464054 |   80799   20317  2451285   120.7 |  1.770 % |
c |     65180 |  150449   463964 |   88879   21045  2582629   122.7 |  1.790 % |
c |     66319 |  150439   463934 |   97767   22171  2713574   122.4 |  1.797 % |
c |     68027 |  150384   463771 |  107543   23843  3111362   130.5 |  1.833 % |
c |     70589 |  150331   463612 |  118298   26355  3564494   135.2 |  1.866 % |
c |     74434 |  150267   463422 |  130128   30159  4308765   142.9 |  1.908 % |
c |     80201 |  150113   462960 |  143140   35743  5270348   147.5 |  2.007 % |
c |     88851 |  149878   462261 |  157454   44207  6758786   152.9 |  2.158 % |
c |    101827 |  149770   461941 |  173200   57027  9861937   172.9 |  2.227 % |
c |    121288 |  149438   460957 |  190520   76089 13785506   181.2 |  2.444 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x226_bit0 -x227_bit0 -x228_bit0 -x229_bit0 -x230_bit0 -x231_bit0 -x232_bit0 -x233_bit0 -x234_bit0 -x235_bit0 -x236_bit0 -x237_bit0 -x238_bit0 x239_bit0 -x240_bit0 -x241_bit0 -x242_bit0 -x243_bit0 -x244_bit0 -x245_bit0 -x246_bit0 -x247_bit0 -x248_bit0 -x249_bit0 -x250_bit0 -x251_bit0 -x252_bit0 -x253_bit0 -x254_bit0 -x255_bit0 -x256_bit0 -x257_bit0 -x258_bit0 -x259_bit0 -x260_bit0 -x261_bit0 -x262_bit0 -x263_bit0 -x264_bit0 -x265_bit0 -x266_bit0 -x267_bit0 -x268_bit0 -x269_bit0 -x270_bit0 -x271_bit0 -x272_bit0 -x273_bit0 -x274_bit0 -x275_bit0 -x276_bit0 -x277_bit0 -x278_bit0 -x279_bit0 -x280_bit0 -x281_bit0 -x282_bit0 -x283_bit0 -x284_bit0 -x285_bit0 -x286_bit0 -x287_bit0 -x288_bit0 -x289_bit0 -x290_bit0 -x291_bit0 -x292_bit0 -x293_bit0 -x294_bit0 -x295_bit0 -x296_bit0 -x297_bit0 -x298_bit0 x299_bit0 -x300_bit0 -x301_bit0 -x302_bit0 -x303_bit0 -x304_bit0 -x305_bit0 -x306_bit0 -x307_bit0 -x308_bit0 -x309_bit0 -x310_bit0 -x311_bit0 -x312_bit0 -x313_bit0 -x314_bit0 -x315_bit0 -x316_bit0 -x317_bit0 -x318_bit0 -x319_bit0 -x320_bit0 -x321_bit0 -x322_bit0 -x323_bit0 -x324_bit0 -x325_bit0 -x326_bit0 -x327_bit0 -x328_bit0 -x329_bit0 -x330_bit0 -x331_bit0 -x332_bit0 -x333_bit0 -x334_bit0 -x335_bit0 -x336_bit0 -x337_bit0 -x338_bit0 -x339_bit0 -x340_bit0 -x341_bit0 -x342_bit0 -x343_bit0 -x344_bit0 -x345_bit0 -x346_bit0 -x347_bit0 -x348_bit0 -x349_bit0 -x350_bit0 -x351_bit0 -x352_bit0 x353_bit0 -x354_bit0 -x355_bit0 -x356_bit0 -x357_bit0 -x358_bit0 -x359_bit0 -x360_bit0 -x361_bit0 -x362_bit0 -x363_bit0 -x364_bit0 -x365_bit0 -x366_bit0 -x367_bit0 -x368_bit0 -x369_bit0 -x370_bit0 -x371_bit0 -x372_bit0 -x373_bit0 -x374_bit0 -x375_bit0 -x376_bit0 -x377_bit0 x378_bit0 -x379_bit0 -x380_bit0 -x381_bit0 -x382_bit0 -x383_bit0 -x384_bit0 -x385_bit0 -x386_bit0 -x387_bit0 -x388_bit0 -x389_bit0 -x390_bit0 -x391_bit0 -x392_bit0 -x393_bit0 -x394_bit0 -x395_bit0 -x396_bit0 -x397_bit0 -x398_bit0 -x399_bit0 -x400_bit0 -x401_bit0 -x402_bit0 -x403_bit0 -x404_bit0 -x405_bit0 -x406_bit0 -x407_bit0 -x408_bit0 -x409_bit0 -x410_bit0 -x411_bit0 -x412_bit0 -x413_bit0 -x414_bit0 -x415_bit0 -x416_bit0 -x417_bit0 -x418_bit0 -x419_bit0 -x420_bit0 -x421_bit0 -x422_bit0 -x423_bit0 -x424_bit0 -x425_bit0 -x426_bit0 -x427_bit0 -x428_bit0 -x429_bit0 -x430_bit0 x431_bit0 -x432_bit0 -x433_bit0 -x434_bit0 -x435_bit0 -x436_bit0 -x437_bit0 -x438_bit0 -x439_bit0 -x440_bit0 -x441_bit0 -x442_bit0 -x443_bit0 -x444_bit0 -x445_bit0 -x446_bit0 -x447_bit0 -x448_bit0 -x449_bit0 -x450_bit0 -x451_bit0 -x452_bit0 -x453_bit0 -x454_bit0 -x455_bit0 -x456_bit0 -x457_bit0 -x458_bit0 -x459_bit0 -x460_bit0 -x461_bit0 -x462_bit0 -x463_bit0 -x464_bit0 -x465_bit0 -x466_bit0 x467_bit0 -x468_bit0 -x469_bit0 -x470_bit0 -x471_bit0 -x472_bit0 -x473_bit0 -x474_bit0 -x475_bit0 -x476_bit0 -x477_bit0 -x478_bit0 -x479_bit0 -x480_bit0 -x481_bit0 -x482_bit0 -x483_bit0 -x484_bit0 -x485_bit0 -x486_bit0 -x487_bit0 -x488_bit0 -x489_bit0 -x490_bit0 -x491_bit0 -x492_bit0 -x493_bit0 -x494_bit0 -x495_bit0 -x496_bit0 -x497_bit0 -x498_bit0 -x499_bit0 -x500_bit0 -x501_bit0 x502_bit0 -x503_bit0 -x504_bit0 -x505_bit0 -x506_bit0 -x507_bit0 -x508_bit0 -x509_bit0 -x510_bit0 -x511_bit0 -x512_bit0 -x513_bit0 -x514_bit0 -x515_bit0 -x516_bit0 -x517_bit0 -x518_bit0 -x519_bit0 -x520_bit0 -x521_bit0 -x522_bit0 -x523_bit0 -x524_bit0 -x525_bit0 -x526_bit0 -x527_bit0 -x528_bit0 -x529_bit0 -x530_bit0 -x531_bit0 -x532_bit0 -x533_bit0 -x534_bit0 -x535_bit0 -x536_bit0 -x537_bit0 -x538_bit0 -x539_bit0 -x540_bit0 -x541_bit0 -x542_bit0 -x543_bit0 -x544_bit0 -x545_bit0 -x546_bit0 -x547_bit0 -x548_bit0 -x549_bit0 -x550_bit0 -x551_bit0 -x552_bit0 -x553_bit0 -x554_bit0 -x555_bit0 -x556_bit0 -x557_bit0 -x558_bit0 -x559_bit0 -x560_bit0 -x561_bit0 -x562_bit0 -x563_bit0 -x564_bit0 -x565_bit0 -x566_bit0 -x567_bit0 -x568_bit0 -x569_bit0 -x570_bit0 -x571_bit0 -x572_bit0 -x573_bit0 x574_bit0 -x575_bit0 -x576_bit0 -x577_bit0 -x578_bit0 -x579_bit0 -x580_bit0 -x581_bit0 -x582_bit0 -x583_bit0 -x584_bit0 -x585_bit0 -x586_bit0 -x587_bit0 -x588_bit0 -x589_bit0 -x590_bit0 -x591_bit0 -x592_bit0 -x593_bit0 -x594_bit0 -x595_bit0 -x596_bit0 -x597_bit0 -x598_bit0 -x599_bit0 -x600_bit0 -x601_bit0 -x602_bit0 -x603_bit0 -x604_bit0 -x605_bit0 -x606_bit0 -x607_bit0 -x608_bit0 -x609_bit0 -x610_bit0 -x611_bit0 -x612_bit0 -x613_bit0 -x614_bit0 -x615_bit0 -x616_bit0 -x617_bit0 -x618_bit0 -x619_bit0 -x620_bit0 -x621_bit0 -x622_bit0 -x623_bit0 -x624_bit0 x625_bit0 -x626_bit0 -x627_bit0 -x628_bit0 -x629_bit0 -x630_bit0 -x631_bit0 -x632_bit0 -x633_bit0 -x634_bit0 -x635_bit0 -x636_bit0 -x637_bit0 -x638_bit0 -x639_bit0 -x640_bit0 -x641_bit0 -x642_bit0 -x643_bit0 -x644_bit0 -x645_bit0 -x646_bit0 -x647_bit0 -x648_bit0 -x649_bit0 -x650_bit0 -x651_bit0 -x652_bit0 -x653_bit0 x654_bit0 -x655_bit0 -x656_bit0 -x657_bit0 -x658_bit0 -x659_bit0 -x660_bit0 -x661_bit0 -x662_bit0 -x663_bit0 -x664_bit0 -x665_bit0 -x666_bit0 -x667_bit0 -x668_bit0 -x669_bit0 -x670_bit0 -x671_bit0 -x672_bit0 -x673_bit0 -x674_bit0 -x675_bit0 -x676_bit0 -x677_bit0 -x678_bit0 -x679_bit0 -x680_bit0 -x681_bit0 -x682_bit0 -x683_bit0 -x684_bit0 -x685_bit0 -x686_bit0 -x687_bit0 -x688_bit0 -x689_bit0 -x690_bit0 -x691_bit0 -x692_bit0 -x693_bit0 -x694_bit0 -x695_bit0 -x696_bit0 -x697_bit0 -x698_bit0 -x699_bit0 -x700_bit0 -x701_bit0 -x702_bit0 -x703_bit0 -x704_bit0 -x705_bit0 -x706_bit0 -x707_bit0 x708_bit0 -x709_bit0 -x710_bit0 -x711_bit0 -x712_bit0 -x713_bit0 -x714_bit0 -x715_bit0 -x716_bit0 -x717_bit0 -x718_bit0 -x719_bit0 -x720_bit0 -x721_bit0 -x722_bit0 -x723_bit0 -x724_bit0 -x725_bit0 -x726_bit0 -x727_bit0 -x728_bit0 -x729_bit0 -x730_bit0 -x731_bit0 -x732_bit0 -x733_bit0 -x734_bit0 -x735_bit0 -x736_bit0 -x737_bit0 -x738_bit0 -x739_bit0 -x740_bit0 -x741_bit0 -x742_bit0 -x743_bit0 -x744_bit0 -x745_bit0 -x746_bit0 x747_bit0 -x748_bit0 -x749_bit0 -x750_bit0 -x751_bit0 -x752_bit0 -x753_bit0 -x754_bit0 -x755_bit0 -x756_bit0 -x757_bit0 -x758_bit0 -x759_bit0 -x760_bit0 -x761_bit0 -x762_bit0 -x763_bit0 -x764_bit0 -x765_bit0 -x766_bit0 -x767_bit0 -x768_bit0 -x769_bit0 -x770_bit0 -x771_bit0 -x772_bit0 -x773_bit0 -x774_bit0 -x775_bit0 -x776_bit0 -x777_bit0 -x778_bit0 -x779_bit0 -x780_bit0 -x781_bit0 -x782_bit0 -x783_bit0 x784_bit0 -x785_bit0 -x786_bit0 -x787_bit0 -x788_bit0 -x789_bit0 -x790_bit0 -x791_bit0 -x792_bit0 -x793_bit0 -x794_bit0 -x795_bit0 -x796_bit0 -x797_bit0 -x798_bit0 -x799_bit0 -x800_bit0 -x801_bit0 -x802_bit0 -x803_bit0 -x804_bit0 -x805_bit0 -x806_bit0 -x807_bit0 -x808_bit0 -x809_bit0 -x810_bit0 -x811_bit0 -x812_bit0 -x813_bit0 -x814_bit0 -x815_bit0 -x816_bit0 -x817_bit0 -x818_bit0 -x819_bit0 -x820_bit0 -x821_bit0 -x822_bit0 -x823_bit0 -x824_bit0 -x825_bit0 -x826_bit0 -x827_bit0 -x828_bit0 -x829_bit0 -x830_bit0 -x831_bit0 -x832_bit0 -x833_bit0 -x834_bit0 -x835_bit0 -x836_bit0 -x837_bit0 -x838_bit0 -x839_bit0 -x840_bit0 -x841_bit0 -x842_bit0 -x843_bit0 -x844_bit0 -x845_bit0 -x846_bit0 x847_bit0 -x848_bit0 -x849_bit0 -x850_bit0 -x851_bit0 -x852_bit0 -x853_bit0 -x854_bit0 -x855_bit0 -x856_bit0 -x857_bit0 x858_bit0 -x859_bit0 -x860_bit0 -x861_bit0 -x862_bit0 -x863_bit0 -x864_bit0 -x865_bit0 -x866_bit0 -x867_bit0 -x868_bit0 -x869_bit0 -x870_bit0 -x871_bit0 -x872_bit0 -x873_bit0 -x874_bit0 -x875_bit0 -x876_bit0 -x877_bit0 -x878_bit0 -x879_bit0 -x880_bit0 -x881_bit0 -x882_bit0 -x883_bit0 -x884_bit0 -x885_bit0 -x886_bit0 -x887_bit0 -x888_bit0 -x889_bit0 -x890_bit0 -x891_bit0 -x892_bit0 -x893_bit0 -x894_bit0 -x895_bit0 -x896_bit0 -x897_bit0 -x898_bit0 -x899_bit0 -x900_bit0 -x901_bit0 -x902_bit0 -x903_bit0 -x904_bit0 -x905_bit0 -x906_bit0 -x907_bit0 -x908_bit0 -x909_bit0 -x910_bit0 -x911_bit0 -x912_bit0 -x913_bit0 -x914_bit0 -x915_bit0 -x916_bit0 -x917_bit0 -x918_bit0 -x919_bit0 -x920_bit0 -x921_bit0 -x922_bit0 -x923_bit0 -x924_bit0 -x925_bit0 -x926_bit0 -x927_bit0 -x928_bit0 -x929_bit0 -x930_bit0 x931_bit0 -x932_bit0 -x933_bit0 -x934_bit0 -x935_bit0 -x936_bit0 -x937_bit0 -x938_bit0 -x939_bit0 -x940_bit0 -x941_bit0 -x942_bit0 -x943_bit0 -x944_bit0 -x945_bit0 -x946_bit0 -x947_bit0 -x948_bit0 -x949_bit0 -x950_bit0 -x951_bit0 -x952_bit0 -x953_bit0 -x954_bit0 -x955_bit0 -x956_bit0 -x957_bit0 -x958_bit0 -x959_bit0 -x960_bit0 -x961_bit0 -x962_bit0 -x963_bit0 -x964_bit0 -x965_bit0 -x966_bit0 -x967_bit0 x968_bit0 -x969_bit0 -x970_bit0 -x971_bit0 -x972_bit0 -x973_bit0 -x974_bit0 -x975_bit0 -x976_bit0 -x977_bit0 -x978_bit0 -x979_bit0 -x980_bit0 -x981_bit0 -x982_bit0 -x983_bit0 -x984_bit0 -x985_bit0 -x986_bit0 -x987_bit0 -x988_bit0 -x989_bit0 -x990_bit0 -x991_bit0 -x992_bit0 -x993_bit0 -x994_bit0 -x995_bit0 -x996_bit0 -x997_bit0 -x998_bit0 -x999_bit0 -x1000_bit0 -x1001_bit0 -x1002_bit0 -x1003_bit0 -x1004_bit0 -x1005_bit0 x1006_bit0 -x1007_bit0 -x1008_bit0 -x1009_bit0 -x1010_bit0 -x1011_bit0 -x1012_bit0 -x1013_bit0 -x1014_bit0 -x1015_bit0 -x1016_bit0 -x1017_bit0 -x1018_bit0 -x1019_bit0 -x1020_bit0 -x1021_bit0 -x1022_bit0 -x1023_bit0 -x1024_bit0 -x1025_bit0 -x1026_bit0 -x1027_bit0 -x1028_bit0 -x1029_bit0 -x1030_bit0 -x1031_bit0 -x1032_bit0 -x1033_bit0 -x1034_bit0 -x1035_bit0 -x1036_bit0 -x1037_bit0 -x1038_bit0 -x1039_bit0 -x1040_bit0 -x1041_bit0 -x1042_bit0 -x1043_bit0 -x1044_bit0 x1045_bit0 -x1046_bit0 -x1047_bit0 -x1048_bit0 -x1049_bit0 -x1050_bit0 -x1051_bit0 -x1052_bit0 -x1053_bit0 -x1054_bit0 -x1055_bit0 -x1056_bit0 -x1057_bit0 -x1058_bit0 -x1059_bit0 -x1060_bit0 -x1061_bit0 -x1062_bit0 -x1063_bit0 -x1064_bit0 -x1065_bit0 -x1066_bit0 -x1067_bit0 -x1068_bit0 -x1069_bit0 -x1070_bit0 -x1071_bit0 -x1072_bit0 -x1073_bit0 -x1074_bit0 -x1075_bit0 -x1076_bit0 -x1077_bit0 -x1078_bit0 -x1079_bit0 -x1080_bit0 -x1081_bit0 -x1082_bit0 -x1083_bit0 -x1084_bit0 -x1085_bit0 -x1086_bit0 -x1087_bit0 -x1088_bit0 -x1089_bit0 -x1090_bit0 -x1091_bit0 -x1092_bit0 -x1093_bit0 -x1094_bit0 -x1095_bit0 -x1096_bit0 -x1097_bit0 -x1098_bit0 -x1099_bit0 -x1100_bit0 -x1101_bit0 -x1102_bit0 -x1103_bit0 -x1104_bit0 -x1105_bit0 -x1106_bit0 -x1107_bit0 -x1108_bit0 -x1109_bit0 -x1110_bit0 -x1111_bit0 -x1112_bit0 -x1113_bit0 -x1114_bit0 -x1115_bit0 -x1116_bit0 -x1117_bit0 -x1118_bit0 -x1119_bit0 -x1120_bit0 -x1121_bit0 x1122_bit0 -x1123_bit0 -x1124_bit0 -x1125_bit0 -x1126_bit0 -x1127_bit0 -x1128_bit0 -x1129_bit0 -x1130_bit0 -x1131_bit0 -x1132_bit0 -x1133_bit0 -x1134_bit0 -x1135_bit0 -x1136_bit0 -x1137_bit0 x1138_bit0 -x1139_bit0 -x1140_bit0 -x1141_bit0 -x1142_bit0 -x1143_bit0 -x1144_bit0 -x1145_bit0 -x1146_bit0 -x1147_bit0 -x1148_bit0 -x1149_bit0 -x1150_bit0 -x1151_bit0 -x1152_bit0 -x1153_bit0 -x1154_bit0 -x1155_bit0 -x1156_bit0 -x1157_bit0 -x1158_bit0 -x1159_bit0 -x1160_bit0 -x1161_bit0 -x1162_bit0 -x1163_bit0 -x1164_bit0 -x1165_bit0 -x1166_bit0 -x1167_bit0 -x1168_bit0 -x1169_bit0 -x1170_bit0 -x1171_bit0 -x1172_bit0 -x1173_bit0 -x1174_bit0 -x1175_bit0 -x1176_bit0 -x1177_bit0 -x1178_bit0 -x1179_bit0 -x1180_bit0 -x1181_bit0 -x1182_bit0 -x1183_bit0 -x1184_bit0 -x1185_bit0 -x1186_bit0 -x1187_bit0 -x1188_bit0 -x1189_bit0 -x1190_bit0 -x1191_bit0 -x1192_bit0 -x1193_bit0 -x1194_bit0 -x1195_bit0 -x1196_bit0 -x1197_bit0 -x1198_bit0 -x1199_bit0 -x1200_bit0 -x1201_bit0 -x1202_bit0 -x1203_bit0 -x1204_bit0 x1205_bit0 -x1206_bit0 -x1207_bit0 -x1208_bit0 -x1209_bit0 -x1210_bit0 -x1211_bit0 -x1212_bit0 -x1213_bit0 -x1214_bit0 -x1215_bit0 -x1216_bit0 -x1217_bit0 -x1218_bit0 -x1219_bit0 -x1220_bit0 -x1221_bit0 -x1222_bit0 -x1223_bit0 -x1224_bit0 -x1225_bit0 -x1226_bit0 -x1227_bit0 -x1228_bit0 -x1229_bit0 -x1230_bit0 -x1231_bit0 -x1232_bit0 -x1233_bit0 -x1234_bit0 -x1235_bit0 -x1236_bit0 -x1237_bit0 -x1238_bit0 -x1239_bit0 -x1240_bit0 -x1241_bit0 -x1242_bit0 -x1243_bit0 -x1244_bit0 -x1245_bit0 -x1246_bit0 -x1247_bit0 -x1248_bit0 -x1249_bit0 -x1250_bit0 -x1251_bit0 -x1252_bit0 -x1253_bit0 -x1254_bit0 -x1255_bit0 -x1256_bit0 -x1257_bit0 -x1258_bit0 x1259_bit0 -x1260_bit0 -x1261_bit0 -x1262_bit0 -x1263_bit0 -x1264_bit0 -x1265_bit0 -x1266_bit0 -x1267_bit0 x1268_bit0 -x1269_bit0 -x1270_bit0 -x1271_bit0 -x1272_bit0 -x1273_bit0 -x1274_bit0 -x1275_bit0 -x1276_bit0 -x1277_bit0 -x1278_bit0 -x1279_bit0 -x1280_bit0 -x1281_bit0 -x1282_bit0 -x1283_bit0 -x1284_bit0 -x1285_bit0 -x1286_bit0 -x1287_bit0 -x1288_bit0 -x1289_bit0 -x1290_bit0 -x1291_bit0 -x1292_bit0 -x1293_bit0 -x1294_bit0 -x1295_bit0 -x1296_bit0 -x1297_bit0 -x1298_bit0 -x1299_bit0 -x1300_bit0 -x1301_bit0 -x1302_bit0 -x1303_bit0 -x1304_bit0 -x1305_bit0 -x1306_bit0 -x1307_bit0 -x1308_bit0 x1309_bit0 -x1310_bit0 -x1311_bit0 -x1312_bit0 -x1313_bit0 -x1314_bit0 -x1315_bit0 -x1316_bit0 -x1317_bit0 -x1318_bit0 -x1319_bit0 -x1320_bit0 -x1321_bit0 -x1322_bit0 -x1323_bit0 -x1324_bit0 -x1325_bit0 -x1326_bit0 -x1327_bit0 -x1328_bit0 -x1329_bit0 -x1330_bit0 -x1331_bit0 -x1332_bit0 -x1333_bit0 -x1334_bit0 -x1335_bit0 -x1336_bit0 -x1337_bit0 -x1338_bit0 -x1339_bit0 -x1340_bit0 -x1341_bit0 -x1342_bit0 -x1343_bit0 -x1344_bit0 -x1345_bit0 -x1346_bit0 -x1347_bit0 -x1348_bit0 -x1349_bit0 -x1350_bit0 -x1351_bit0 -x1352_bit0 -x1353_bit0 -x1354_bit0 -x1355_bit0 -x1356_bit0 -x1357_bit0 -x1358_bit0 -x1359_bit0 -x1360_bit0 -x1361_bit0 -x1362_bit0 -x1363_bit0 -x1364_bit0 -x1365_bit0 -x1366_bit0 -x1367_bit0 -x1368_bit0 -x1369_bit0 -x1370_bit0 -x1371_bit0 -x1372_bit0 -x1373_bit0 -x1374_bit0 x1375_bit0 -x1376_bit0 -x1377_bit0 -x1378_bit0 -x1379_bit0 -x1380_bit0 -x1381_bit0 -x1382_bit0 -x1383_bit0 -x1384_bit0 -x1385_bit0 -x1386_bit0 -x1387_bit0 -x1388_bit0 -x1389_bit0 -x1390_bit0 -x1391_bit0 -x1392_bit0 -x1393_bit0 -x1394_bit0 -x1395_bit0 -x1396_bit0 -x1397_bit0 -x1398_bit0 -x1399_bit0 -x1400_bit0 -x1401_bit0 -x1402_bit0 -x1403_bit0 -x1404_bit0 -x1405_bit0 -x1406_bit0 -x1407_bit0 -x1408_bit0 -x1409_bit0 -x1410_bit0 -x1411_bit0 -x1412_bit0 -x1413_bit0 -x1414_bit0 -x1415_bit0 -x1416_bit0 -x1417_bit0 -x1418_bit0 -x1419_bit0 -x1420_bit0 -x1421_bit0 -x1422_bit0 -x1423_bit0 -x1424_bit0 -x1425_bit0 -x1426_bit0 -x1427_bit0 -x1428_bit0 -x1429_bit0 -x1430_bit0 -x1431_bit0 -x1432_bit0 -x1433_bit0 x1434_bit0 -x1435_bit0 -x1436_bit0 -x1437_bit0 -x1438_bit0 -x1439_bit0 -x1440_bit0 -x1441_bit0 -x1442_bit0 -x1443_bit0 -x1444_bit0 -x1445_bit0 -x1446_bit0 -x1447_bit0 -x1448_bit0 -x1449_bit0 -x1450_bit0 -x1451_bit0 -x1452_bit0 -x1453_bit0 -x1454_bit0 -x1455_bit0 -x1456_bit0 -x1457_bit0 -x1458_bit0 -x1459_bit0 -x1460_bit0 -x1461_bit0 -x1462_bit0 -x1463_bit0 -x1464_bit0 -x1465_bit0 -x1466_bit0 -x1467_bit0 -x1468_bit0 -x1469_bit0 x1470_bit0 -x1471_bit0 -x1472_bit0 -x1473_bit0 -x1474_bit0 -x1475_bit0 -x1476_bit0 -x1477_bit0 -x1478_bit0 -x1479_bit0 -x1480_bit0 -x1481_bit0 -x1482_bit0 -x1483_bit0 -x1484_bit0 -x1485_bit0 -x1486_bit0 -x1487_bit0 -x1488_bit0 -x1489_bit0 -x1490_bit0 -x1491_bit0 -x1492_bit0 -x1493_bit0 -x1494_bit0 -x1495_bit0 x1496_bit0 -x1497_bit0 -x1498_bit0 -x1499_bit0 -x1500_bit0 -x1501_bit0 -x1502_bit0 -x1503_bit0 -x1504_bit0 -x1505_bit0 -x1506_bit0 -x1507_bit0 -x1508_bit0 -x1509_bit0 -x1510_bit0 -x1511_bit0 -x1512_bit0 -x1513_bit0 -x1514_bit0 -x1515_bit0 -x1516_bit0 -x1517_bit0 -x1518_bit0 -x1519_bit0 -x1520_bit0 -x1521_bit0 -x1522_bit0 -x1523_bit0 -x1524_bit0 -x1525_bit0 -x1526_bit0 -x1527_bit0 -x1528_bit0 -x1529_bit0 -x1530_bit0 -x1531_bit0 -x1532_bit0 -x1533_bit0 -x1534_bit0 -x1535_bit0 -x1536_bit0 -x1537_bit0 -x1538_bit0 -x1539_bit0 -x1540_bit0 -x1541_bit0 -x1542_bit0 -x1543_bit0 -x1544_bit0 -x1545_bit0 -x1546_bit0 -x1547_bit0 -x1548_bit0 -x1549_bit0 x1550_bit0 -x1551_bit0 -x1552_bit0 -x1553_bit0 -x1554_bit0 -x1555_bit0 -x1556_bit0 -x1557_bit0 -x1558_bit0 -x1559_bit0 -x1560_bit0 -x1561_bit0 -x1562_bit0 -x1563_bit0 -x1564_bit0 -x1565_bit0 -x1566_bit0 -x1567_bit0 -x1568_bit0 -x1569_bit0 -x1570_bit0 -x1571_bit0 -x1572_bit0 -x1573_bit0 -x1574_bit0 -x1575_bit0 -x1576_bit0 -x1577_bit0 -x1578_bit0 -x1579_bit0 -x1580_bit0 -x1581_bit0 -x1582_bit0 -x1583_bit0 -x1584_bit0 -x1585_bit0 -x1586_bit0 -x1587_bit0 -x1588_bit0 -x1589_bit0 -x1590_bit0 -x1591_bit0 -x1592_bit0 -x1593_bit0 -x1594_bit0 -x1595_bit0 -x1596_bit0 x1597_bit0 -x1598_bit0 -x1599_bit0 -x1600_bit0 -x1601_bit0 -x1602_bit0 -x1603_bit0 -x1604_bit0 -x1605_bit0 -x1606_bit0 -x1607_bit0 -x1608_bit0 -x1609_bit0 -x1610_bit0 -x1611_bit0 -x1612_bit0 -x1613_bit0 -x1614_bit0 -x1615_bit0 -x1616_bit0 -x1617_bit0 -x1618_bit0 -x1619_bit0 -x1620_bit0 -x1621_bit0 -x1622_bit0 -x1623_bit0 -x1624_bit0 -x1625_bit0 -x1626_bit0 -x1627_bit0 -x1628_bit0 -x1629_bit0 -x1630_bit0 -x1631_bit0 -x1632_bit0 -x1633_bit0 -x1634_bit0 -x1635_bit0 -x1636_bit0 -x1637_bit0 -x1638_bit0 -x1639_bit0 -x1640_bit0 -x1641_bit0 -x1642_bit0 -x1643_bit0 -x1644_bit0 -x1645_bit0 -x1646_bit0 -x1647_bit0 -x1648_bit0 -x1649_bit0 -x1650_bit0 -x1651_bit0 -x1652_bit0 -x1653_bit0 -x1654_bit0 -x1655_bit0 -x1656_bit0 -x1657_bit0 -x1658_bit0 -x1659_bit0 -x1660_bit0 -x1661_bit0 -x1662_bit0 x1663_bit0 -x1664_bit0 -x1665_bit0 -x1666_bit0 -x1667_bit0 -x1668_bit0 -x1669_bit0 -x1670_bit0 -x1671_bit0 -x1672_bit0 -x1673_bit0 x1674_bit0 -x1675_bit0 -x1676_bit0 -x1677_bit0 -x1678_bit0 -x1679_bit0 -x1680_bit0 -x1681_bit0 -x1682_bit0 -x1683_bit0 -x1684_bit0 -x1685_bit0 -x1686_bit0 -x1687_bit0 -x1688_bit0 -x1689_bit0 -x1690_bit0 -x1691_bit0 -x1692_bit0 -x1693_bit0 -x1694_bit0 -x1695_bit0 -x1696_bit0 -x1697_bit0 -x1698_bit0 -x1699_bit0 -x1700_bit0 -x1701_bit0 -x1702_bit0 -x1703_bit0 -x1704_bit0 -x1705_bit0 -x1706_bit0 -x1707_bit0 -x1708_bit0 -x1709_bit0 -x1710_bit0 -x1711_bit0 -x1712_bit0 -x1713_bit0 -x1714_bit0 -x1715_bit0 -x1716_bit0 -x1717_bit0 -x1718_bit0 -x1719_bit0 -x1720_bit0 -x1721_bit0 x1722_bit0 -x1723_bit0 -x1724_bit0 -x1725_bit0 -x1726_bit0 -x1727_bit0 -x1728_bit0 -x1729_bit0 -x1730_bit0 -x1731_bit0 -x1732_bit0 -x1733_bit0 -x1734_bit0 -x1735_bit0 -x1736_bit0 -x1737_bit0 -x1738_bit0 -x1739_bit0 -x1740_bit0 -x1741_bit0 -x1742_bit0 -x1743_bit0 -x1744_bit0 -x1745_bit0 -x1746_bit0 -x1747_bit0 -x1748_bit0 -x1749_bit0 -x1750_bit0 -x1751_bit0 -x1752_bit0 -x1753_bit0 -x1754_bit0 -x1755_bit0 -x1756_bit0 -x1757_bit0 -x1758_bit0 -x1759_bit0 -x1760_bit0 -x1761_bit0 -x1762_bit0 -x1763_bit0 -x1764_bit0 -x1765_bit0 -x1766_bit0 -x1767_bit0 -x1768_bit0 -x1769_bit0 -x1770_bit0 -x1771_bit0 -x1772_bit0 -x1773_bit0 -x1774_bit0 -x1775_bit0 -x1776_bit0 -x1777_bit0 -x1778_bit0 -x1779_bit0 -x1780_bit0 -x1781_bit0 -x1782_bit0 -x1783_bit0 -x1784_bit0 -x1785_bit0 -x1786_bit0 x1787_bit0 -x1788_bit0 -x1789_bit0 -x1790_bit0 -x1791_bit0 -x1792_bit0 -x1793_bit0 -x1794_bit0 -x1795_bit0 -x1796_bit0 -x1797_bit0 -x1798_bit0 -x1799_bit0 -x1800_bit0 -x1801_bit0 -x1802_bit0 -x1803_bit0 -x1804_bit0 -x1805_bit0 -x1806_bit0 -x1807_bit0 -x1808_bit0 -x1809_bit0 -x1810_bit0 -x1811_bit0 -x1812_bit0 -x1813_bit0 -x1814_bit0 -x1815_bit0 -x1816_bit0 -x1817_bit0 -x1818_bit0 -x1819_bit0 -x1820_bit0 -x1821_bit0 -x1822_bit0 -x1823_bit0 -x1824_bit0 -x1825_bit0 -x1826_bit0 -x1827_bit0 -x1828_bit0 -x1829_bit0 -x1830_bit0 -x1831_bit0 -x1832_bit0 -x1833_bit0 -x1834_bit0 -x1835_bit0 -x1836_bit0 -x1837_bit0 -x1838_bit0 -x1839_bit0 -x1840_bit0 x1841_bit0 -x1842_bit0 -x1843_bit0 -x1844_bit0 -x1845_bit0 -x1846_bit0 -x1847_bit0 -x1848_bit0 -x1849_bit0 x1850_bit0 -x1851_bit0 -x1852_bit0 -x1853_bit0 -x1854_bit0 -x1855_bit0 -x1856_bit0 -x1857_bit0 -x1858_bit0 -x1859_bit0 -x1860_bit0 -x1861_bit0 -x1862_bit0 -x1863_bit0 -x1864_bit0 -x1865_bit0 -x1866_bit0 -x1867_bit0 -x1868_bit0 -x1869_bit0 -x1870_bit0 -x1871_bit0 -x1872_bit0 -x1873_bit0 -x1874_bit0 -x1875_bit0 -x1876_bit0 -x1877_bit0 -x1878_bit0 -x1879_bit0 -x1880_bit0 -x1881_bit0 -x1882_bit0 -x1883_bit0 -x1884_bit0 -x1885_bit0 -x1886_bit0 -x1887_bit0 -x1888_bit0 -x1889_bit0 -x1890_bit0 -x1891_bit0 x1892_bit0 -x1893_bit0 -x1894_bit0 -x1895_bit0 -x1896_bit0 -x1897_bit0 -x1898_bit0 -x1899_bit0 -x1900_bit0 -x1901_bit0 -x1902_bit0 -x1903_bit0 -x1904_bit0 -x1905_bit0 -x1906_bit0 -x1907_bit0 -x1908_bit0 -x1909_bit0 -x1910_bit0 -x1911_bit0 -x1912_bit0 -x1913_bit0 -x1914_bit0 -x1915_bit0 -x1916_bit0 -x1917_bit0 -x1918_bit0 -x1919_bit0 -x1920_bit0 -x1921_bit0 -x1922_bit0 -x1923_bit0 -x1924_bit0 -x1925_bit0 -x1926_bit0 -x1927_bit0 -x1928_bit0 -x1929_bit0 -x1930_bit0 -x1931_bit0 -x1932_bit0 -x1933_bit0 -x1934_bit0 -x1935_bit0 -x1936_bit0 -x1937_bit0 -x1938_bit0 -x1939_bit0 -x1940_bit0 -x1941_bit0 -x1942_bit0 -x1943_bit0 -x1944_bit0 -x1945_bit0 -x1946_bit0 -x1947_bit0 -x1948_bit0 -x1949_bit0 -x1950_bit0 -x1951_bit0 -x1952_bit0 -x1953_bit0 -x1954_bit0 -x1955_bit0 -x1956_bit0 -x1957_bit0 -x1958_bit0 -x1959_bit0 -x1960_bit0 -x1961_bit0 -x1962_bit0 -x1963_bit0 -x1964_bit0 -x1965_bit0 -x1966_bit0 -x1967_bit0 -x1968_bit0 -x1969_bit0 -x1970_bit0 x1971_bit0 -x1972_bit0 -x1973_bit0 -x1974_bit0 -x1975_bit0 -x1976_bit0 -x1977_bit0 -x1978_bit0 -x1979_bit0 -x1980_bit0 -x1981_bit0 -x1982_bit0 -x1983_bit0 -x1984_bit0 -x1985_bit0 -x1986_bit0 -x1987_bit0 -x1988_bit0 -x1989_bit0 -x1990_bit0 -x1991_bit0 -x1992_bit0 -x1993_bit0 -x1994_bit0 -x1995_bit0 -x1996_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.79 0.93 0.90 2/54 11750
Raw data (stat): 11750 (runsolver) R 11749 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 488478105 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.82 0.93 0.90 2/54 11750
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 2819 0 0 0 992 7 0 0 25 0 1 0 488478105 13713408 2778 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3348 2778 603 41 0 3307 0
vsize: 13392
[startup+20.0013 s]
Raw data (loadavg): 0.85 0.93 0.90 2/54 11750
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 3268 0 0 0 1990 8 0 0 25 0 1 0 488478105 15605760 3227 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3810 3227 603 41 0 3769 0
vsize: 15240
[startup+30.0023 s]
Raw data (loadavg): 0.87 0.93 0.90 2/54 11750
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 3821 0 0 0 2989 10 0 0 25 0 1 0 488478105 17899520 3780 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4370 3780 603 41 0 4329 0
vsize: 17480
[startup+40.0025 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 11750
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 4315 0 0 0 3987 12 0 0 25 0 1 0 488478105 19918848 4274 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4863 4274 603 41 0 4822 0
vsize: 19452
[startup+50.0021 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 11750
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 4855 0 0 0 4985 14 0 0 25 0 1 0 488478105 22061056 4814 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5386 4814 603 41 0 5345 0
vsize: 21544
[startup+60.0022 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 11750
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 5334 0 0 0 5984 15 0 0 25 0 1 0 488478105 24084480 5293 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5880 5293 603 41 0 5839 0
vsize: 23520
[startup+70.0024 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 11750
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 11704 0 0 0 6967 32 0 0 25 0 1 0 488478105 46424064 10342 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11334 10342 603 41 0 11293 0
vsize: 45336
[startup+80.003 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 11750
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 11973 0 0 0 7966 33 0 0 25 0 1 0 488478105 47513600 10611 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11600 10611 603 41 0 11559 0
vsize: 46400
[startup+90.0031 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 11750
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 12303 0 0 0 8965 34 0 0 25 0 1 0 488478105 48857088 10941 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11928 10941 603 41 0 11887 0
vsize: 47712
[startup+100.002 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 11750
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 12553 0 0 0 9964 35 0 0 25 0 1 0 488478105 49934336 11191 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12191 11191 603 41 0 12150 0
vsize: 48764
[startup+110.007 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 11750
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 12865 0 0 0 10964 36 0 0 25 0 1 0 488478105 50802688 11439 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12403 11439 603 41 0 12362 0
vsize: 49612
[startup+120.007 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 11750
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 13232 0 0 0 11962 37 0 0 25 0 1 0 488478105 52400128 11806 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12793 11806 603 41 0 12752 0
vsize: 51172
[startup+130.007 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 11750
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 13536 0 0 0 12962 38 0 0 25 0 1 0 488478105 53612544 12110 4294967295 134512640 134672761 3221224544 3221223680 134560622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13089 12110 603 41 0 13048 0
vsize: 52356
[startup+140.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 11750
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 13808 0 0 0 13961 39 0 0 25 0 1 0 488478105 54693888 12382 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13353 12382 603 41 0 13312 0
vsize: 53412
[startup+150.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 11750
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 14069 0 0 0 14960 40 0 0 25 0 1 0 488478105 55758848 12643 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13613 12643 603 41 0 13572 0
vsize: 54452
[startup+160.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 11750
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 14422 0 0 0 15960 40 0 0 25 0 1 0 488478105 57233408 12996 4294967295 134512640 134672761 3221224544 3221223648 134559964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13973 12996 603 41 0 13932 0
vsize: 55892
[startup+170.007 s]
Raw data (loadavg): 1.06 0.97 0.91 4/59 11802
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 14737 0 0 0 16959 42 0 0 25 0 1 0 488478105 58679296 13311 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14326 13311 603 41 0 14285 0
vsize: 57304
[startup+180.008 s]
Raw data (loadavg): 1.05 0.97 0.91 2/54 11803
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 15049 0 0 0 17958 42 0 0 25 0 1 0 488478105 59887616 13623 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14621 13623 603 41 0 14580 0
vsize: 58484
[startup+190.008 s]
Raw data (loadavg): 1.05 0.97 0.91 2/54 11803
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 15470 0 0 0 18957 43 0 0 25 0 1 0 488478105 61612032 14044 4294967295 134512640 134672761 3221224544 3221223648 134559979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15042 14044 603 41 0 15001 0
vsize: 60168
[startup+200.007 s]
Raw data (loadavg): 1.04 0.97 0.91 2/54 11803
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 15903 0 0 0 19956 45 0 0 25 0 1 0 488478105 63340544 14477 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15464 14477 603 41 0 15423 0
vsize: 61856
[startup+210.007 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 11803
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 16191 0 0 0 20955 46 0 0 25 0 1 0 488478105 64552960 14765 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15760 14765 603 41 0 15719 0
vsize: 63040
[startup+220.007 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 11803
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 16493 0 0 0 21954 47 0 0 25 0 1 0 488478105 65748992 15067 4294967295 134512640 134672761 3221224544 3221223648 134560350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16052 15067 603 41 0 16011 0
vsize: 64208
[startup+230.006 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 11803
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 16773 0 0 0 22953 48 0 0 25 0 1 0 488478105 66949120 15347 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16345 15347 603 41 0 16304 0
vsize: 65380
[startup+240.006 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 11805
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 17124 0 0 0 23952 49 0 0 25 0 1 0 488478105 68300800 15698 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16675 15698 603 41 0 16634 0
vsize: 66700
[startup+250.006 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 11805
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 17379 0 0 0 24952 50 0 0 25 0 1 0 488478105 69373952 15953 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16937 15953 603 41 0 16896 0
vsize: 67748
[startup+260.007 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 11805
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 17628 0 0 0 25951 50 0 0 25 0 1 0 488478105 70451200 16202 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17200 16202 603 41 0 17159 0
vsize: 68800
[startup+270.006 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 11805
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 17922 0 0 0 26951 51 0 0 25 0 1 0 488478105 71651328 16496 4294967295 134512640 134672761 3221224544 3221223712 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17493 16496 603 41 0 17452 0
vsize: 69972
[startup+280.007 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 11805
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 18159 0 0 0 27951 51 0 0 25 0 1 0 488478105 72589312 16733 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17722 16733 603 41 0 17681 0
vsize: 70888
[startup+290.007 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 11805
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 18450 0 0 0 28949 53 0 0 25 0 1 0 488478105 73805824 17024 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18019 17024 603 41 0 17978 0
vsize: 72076
[startup+300.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11805
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 18575 0 0 0 29949 53 0 0 25 0 1 0 488478105 74211328 17149 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18118 17149 603 41 0 18077 0
vsize: 72472
[startup+310.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11805
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 18800 0 0 0 30949 54 0 0 25 0 1 0 488478105 75153408 17374 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18348 17374 603 41 0 18307 0
vsize: 73392
[startup+320.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11805
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 19063 0 0 0 31949 54 0 0 25 0 1 0 488478105 76226560 17637 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18610 17637 603 41 0 18569 0
vsize: 74440
[startup+330.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11805
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 19228 0 0 0 32949 54 0 0 25 0 1 0 488478105 76898304 17802 4294967295 134512640 134672761 3221224544 3221223692 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18774 17802 603 41 0 18733 0
vsize: 75096
[startup+340.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11805
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 19508 0 0 0 33948 55 0 0 25 0 1 0 488478105 78114816 18082 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19071 18082 603 41 0 19030 0
vsize: 76284
[startup+350.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11805
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 19774 0 0 0 34947 56 0 0 25 0 1 0 488478105 79183872 18348 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19332 18348 603 41 0 19291 0
vsize: 77328
[startup+360.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11805
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 20022 0 0 0 35947 57 0 0 25 0 1 0 488478105 80130048 18596 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19563 18596 603 41 0 19522 0
vsize: 78252
[startup+370.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11805
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 20204 0 0 0 36947 57 0 0 25 0 1 0 488478105 80941056 18778 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19761 18778 603 41 0 19720 0
vsize: 79044
[startup+380.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11805
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 20488 0 0 0 37946 58 0 0 25 0 1 0 488478105 82010112 19062 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20022 19062 603 41 0 19981 0
vsize: 80088
[startup+390.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11805
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 20651 0 0 0 38946 58 0 0 25 0 1 0 488478105 82681856 19225 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20186 19225 603 41 0 20145 0
vsize: 80744
[startup+400.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11805
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 20908 0 0 0 39945 59 0 0 25 0 1 0 488478105 83750912 19482 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20447 19482 603 41 0 20406 0
vsize: 81788
[startup+410.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11805
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 21296 0 0 0 40945 60 0 0 25 0 1 0 488478105 84840448 19759 4294967295 134512640 134672761 3221224544 3221223844 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+420.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11805
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 21296 0 0 0 41944 60 0 0 25 0 1 0 488478105 84840448 19759 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+430.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11805
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 21296 0 0 0 42944 61 0 0 25 0 1 0 488478105 84840448 19759 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+440.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11805
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 21296 0 0 0 43944 61 0 0 25 0 1 0 488478105 84840448 19759 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+450.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11805
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 21296 0 0 0 44944 61 0 0 25 0 1 0 488478105 84840448 19759 4294967295 134512640 134672761 3221224544 3221223648 134559853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+460.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11805
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 21296 0 0 0 45944 61 0 0 25 0 1 0 488478105 84840448 19759 4294967295 134512640 134672761 3221224544 3221223728 134559503 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+470.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11805
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 21296 0 0 0 46945 61 0 0 25 0 1 0 488478105 84840448 19759 4294967295 134512640 134672761 3221224544 3221223688 134560630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+480.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11805
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 21296 0 0 0 47945 61 0 0 25 0 1 0 488478105 84840448 19759 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+490.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11805
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 21296 0 0 0 48945 61 0 0 25 0 1 0 488478105 84840448 19759 4294967295 134512640 134672761 3221224544 3221223728 134558374 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+500.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11805
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 21296 0 0 0 49945 61 0 0 25 0 1 0 488478105 84840448 19759 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+510.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11805
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 21296 0 0 0 50945 61 0 0 25 0 1 0 488478105 84840448 19759 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+520.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11805
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 21296 0 0 0 51945 61 0 0 25 0 1 0 488478105 84840448 19759 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+530.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11805
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 21296 0 0 0 52946 61 0 0 25 0 1 0 488478105 84840448 19759 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+540.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11805
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 21296 0 0 0 53946 61 0 0 25 0 1 0 488478105 84840448 19759 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+550.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 21296 0 0 0 54946 61 0 0 25 0 1 0 488478105 84840448 19759 4294967295 134512640 134672761 3221224544 3221223744 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+560.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 21296 0 0 0 55946 61 0 0 25 0 1 0 488478105 84840448 19759 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+570.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 21296 0 0 0 56946 61 0 0 25 0 1 0 488478105 84840448 19759 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+580.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 21296 0 0 0 57946 61 0 0 25 0 1 0 488478105 84840448 19759 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+590.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 21296 0 0 0 58947 61 0 0 25 0 1 0 488478105 84840448 19759 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+600.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 21296 0 0 0 59947 61 0 0 25 0 1 0 488478105 84840448 19759 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+610.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 21296 0 0 0 60947 61 0 0 25 0 1 0 488478105 84840448 19759 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+620.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 21296 0 0 0 61947 61 0 0 25 0 1 0 488478105 84840448 19759 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+630.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 21296 0 0 0 62947 61 0 0 25 0 1 0 488478105 84840448 19759 4294967295 134512640 134672761 3221224544 3221223648 134560506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+640.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 21296 0 0 0 63947 61 0 0 25 0 1 0 488478105 84840448 19759 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+650.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 21296 0 0 0 64948 61 0 0 25 0 1 0 488478105 84840448 19759 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+660.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 21296 0 0 0 65948 61 0 0 25 0 1 0 488478105 84840448 19759 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+670.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 21296 0 0 0 66948 61 0 0 25 0 1 0 488478105 84840448 19759 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+680.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 21296 0 0 0 67948 61 0 0 25 0 1 0 488478105 84840448 19759 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+690.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 21296 0 0 0 68948 61 0 0 25 0 1 0 488478105 84840448 19759 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+700.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 21297 0 0 0 69948 61 0 0 25 0 1 0 488478105 84840448 19760 4294967295 134512640 134672761 3221224544 3221223648 134559902 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20713 19760 603 41 0 20672 0
vsize: 82852
[startup+710.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 21297 0 0 0 70949 61 0 0 25 0 1 0 488478105 84840448 19760 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20713 19760 603 41 0 20672 0
vsize: 82852
[startup+720.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 21297 0 0 0 71948 61 0 0 25 0 1 0 488478105 84840448 19760 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20713 19760 603 41 0 20672 0
vsize: 82852
[startup+730.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 21297 0 0 0 72948 61 0 0 25 0 1 0 488478105 84840448 19760 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20713 19760 603 41 0 20672 0
vsize: 82852
[startup+740.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 21297 0 0 0 73948 61 0 0 25 0 1 0 488478105 84840448 19760 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20713 19760 603 41 0 20672 0
vsize: 82852
[startup+750.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 21297 0 0 0 74949 61 0 0 25 0 1 0 488478105 84840448 19760 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20713 19760 603 41 0 20672 0
vsize: 82852
[startup+760.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 21298 0 0 0 75949 61 0 0 25 0 1 0 488478105 84840448 19761 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20713 19761 603 41 0 20672 0
vsize: 82852
[startup+770.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 21306 0 0 0 76949 61 0 0 25 0 1 0 488478105 84975616 19769 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20746 19769 603 41 0 20705 0
vsize: 82984
[startup+780.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 21487 0 0 0 77948 62 0 0 25 0 1 0 488478105 85647360 19950 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20910 19950 603 41 0 20869 0
vsize: 83640
[startup+790.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 21750 0 0 0 78948 62 0 0 25 0 1 0 488478105 86990848 20213 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21238 20213 603 41 0 21197 0
vsize: 84952
[startup+800.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 21818 0 0 0 79948 63 0 0 25 0 1 0 488478105 87261184 20281 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21304 20281 603 41 0 21263 0
vsize: 85216
[startup+810.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 22034 0 0 0 80947 63 0 0 25 0 1 0 488478105 88186880 20497 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21530 20497 603 41 0 21489 0
vsize: 86120
[startup+820.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 22221 0 0 0 81947 64 0 0 25 0 1 0 488478105 88989696 20684 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21726 20684 603 41 0 21685 0
vsize: 86904
[startup+830.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 22482 0 0 0 82947 64 0 0 25 0 1 0 488478105 89923584 20945 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21954 20945 603 41 0 21913 0
vsize: 87816
[startup+840.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 22658 0 0 0 83946 65 0 0 25 0 1 0 488478105 90734592 21121 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22152 21121 603 41 0 22111 0
vsize: 88608
[startup+850.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 22840 0 0 0 84946 65 0 0 25 0 1 0 488478105 91406336 21303 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22316 21303 603 41 0 22275 0
vsize: 89264
[startup+860.01 s]
Raw data (loadavg): 1.00 0.97 0.91 3/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 22994 0 0 0 85946 66 0 0 25 0 1 0 488478105 92078080 21457 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22480 21457 603 41 0 22439 0
vsize: 89920
[startup+870.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 23200 0 0 0 86946 66 0 0 25 0 1 0 488478105 92884992 21663 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22677 21663 603 41 0 22636 0
vsize: 90708
[startup+880.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 23362 0 0 0 87945 67 0 0 25 0 1 0 488478105 93556736 21825 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22841 21825 603 41 0 22800 0
vsize: 91364
[startup+890.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 23527 0 0 0 88944 68 0 0 25 0 1 0 488478105 94232576 21990 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23006 21990 603 41 0 22965 0
vsize: 92024
[startup+900.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 23712 0 0 0 89944 68 0 0 25 0 1 0 488478105 95035392 22175 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23202 22175 603 41 0 23161 0
vsize: 92808
[startup+910.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 23818 0 0 0 90943 69 0 0 25 0 1 0 488478105 95440896 22281 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23301 22281 603 41 0 23260 0
vsize: 93204
[startup+920.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 24101 0 0 0 91943 70 0 0 25 0 1 0 488478105 96649216 22564 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23596 22564 603 41 0 23555 0
vsize: 94384
[startup+930.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 24340 0 0 0 92943 70 0 0 25 0 1 0 488478105 97583104 22803 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23824 22803 603 41 0 23783 0
vsize: 95296
[startup+940.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 24521 0 0 0 93942 71 0 0 25 0 1 0 488478105 98258944 22984 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23989 22984 603 41 0 23948 0
vsize: 95956
[startup+950.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 24767 0 0 0 94942 71 0 0 25 0 1 0 488478105 99332096 23230 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24251 23230 603 41 0 24210 0
vsize: 97004
[startup+960.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 24941 0 0 0 95942 72 0 0 25 0 1 0 488478105 100007936 23404 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24416 23404 603 41 0 24375 0
vsize: 97664
[startup+970.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 25157 0 0 0 96941 73 0 0 25 0 1 0 488478105 100950016 23620 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24646 23620 603 41 0 24605 0
vsize: 98584
[startup+980.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 25357 0 0 0 97941 73 0 0 25 0 1 0 488478105 101756928 23820 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24843 23820 603 41 0 24802 0
vsize: 99372
[startup+990.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 25530 0 0 0 98940 74 0 0 25 0 1 0 488478105 102424576 23993 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25006 23993 603 41 0 24965 0
vsize: 100024
[startup+1000.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 25749 0 0 0 99940 75 0 0 25 0 1 0 488478105 103235584 24212 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25204 24212 603 41 0 25163 0
vsize: 100816
[startup+1010.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 25886 0 0 0 100939 75 0 0 25 0 1 0 488478105 103911424 24349 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25369 24349 603 41 0 25328 0
vsize: 101476
[startup+1020.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 26119 0 0 0 101939 76 0 0 25 0 1 0 488478105 104845312 24582 4294967295 134512640 134672761 3221224544 3221223648 134560350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25597 24583 603 41 0 25556 0
vsize: 102388
[startup+1030.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 26397 0 0 0 102938 77 0 0 25 0 1 0 488478105 105918464 24860 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25859 24860 603 41 0 25818 0
vsize: 103436
[startup+1040.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 26522 0 0 0 103938 77 0 0 25 0 1 0 488478105 106446848 24985 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25988 24985 603 41 0 25947 0
vsize: 103952
[startup+1050.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 26683 0 0 0 104938 77 0 0 25 0 1 0 488478105 107114496 25146 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26151 25146 603 41 0 26110 0
vsize: 104604
[startup+1060.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 26892 0 0 0 105937 78 0 0 25 0 1 0 488478105 107917312 25355 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26347 25355 603 41 0 26306 0
vsize: 105388
[startup+1070.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 27059 0 0 0 106937 78 0 0 25 0 1 0 488478105 108584960 25522 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26510 25522 603 41 0 26469 0
vsize: 106040
[startup+1080.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 27323 0 0 0 107937 79 0 0 25 0 1 0 488478105 109654016 25786 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26771 25786 603 41 0 26730 0
vsize: 107084
[startup+1090.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 27380 0 0 0 108937 79 0 0 25 0 1 0 488478105 109920256 25843 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26836 25843 603 41 0 26795 0
vsize: 107344
[startup+1100.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 27552 0 0 0 109937 79 0 0 25 0 1 0 488478105 110587904 26015 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26999 26015 603 41 0 26958 0
vsize: 107996
[startup+1110.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 27834 0 0 0 110936 80 0 0 25 0 1 0 488478105 111788032 26297 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27292 26297 603 41 0 27251 0
vsize: 109168
[startup+1120.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 28039 0 0 0 111936 81 0 0 25 0 1 0 488478105 112599040 26502 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27490 26502 603 41 0 27449 0
vsize: 109960
[startup+1130.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 28177 0 0 0 112935 81 0 0 25 0 1 0 488478105 113254400 26640 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27650 26640 603 41 0 27609 0
vsize: 110600
[startup+1140.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 28371 0 0 0 113935 82 0 0 25 0 1 0 488478105 114049024 26834 4294967295 134512640 134672761 3221224544 3221223696 134565213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27844 26834 603 41 0 27803 0
vsize: 111376
[startup+1150.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 28650 0 0 0 114934 83 0 0 25 0 1 0 488478105 115130368 27113 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28108 27113 603 41 0 28067 0
vsize: 112432
[startup+1160.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 28910 0 0 0 115933 84 0 0 25 0 1 0 488478105 116199424 27373 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28369 27373 603 41 0 28328 0
vsize: 113476
[startup+1170.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 28975 0 0 0 116933 84 0 0 25 0 1 0 488478105 116465664 27438 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28434 27438 603 41 0 28393 0
vsize: 113736
[startup+1180.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 29177 0 0 0 117933 84 0 0 25 0 1 0 488478105 117272576 27640 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28631 27640 603 41 0 28590 0
vsize: 114524
[startup+1190.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 29316 0 0 0 118933 85 0 0 25 0 1 0 488478105 117813248 27779 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28763 27779 603 41 0 28722 0
vsize: 115052
[startup+1200.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 11807
Raw data (stat): 11750 (minisat+) R 11749 22932 22931 0 -1 0 29423 0 0 0 119932 85 0 0 25 0 1 0 488478105 118341632 27886 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28892 27886 603 41 0 28851 0
vsize: 115568
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.97 0.91 1/54 11807
Raw data (stat): 11750 (minisat+) Z 11749 22932 22931 0 -1 12 29426 0 0 0 119933 90 0 0 25 0 1 0 488478105 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.07
CPU time (s): 1200.24
CPU user time (s): 1199.33
CPU system time (s): 0.909861
CPU usage (%): 100.014
Max. virtual memory (Kb): 115568
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####