PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-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	924
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.71
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 21936

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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:        193832 kB
Buffers:         34008 kB
Cached:         785156 kB
SwapCached:        508 kB
Active:         171388 kB
Inactive:       649932 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        193580 kB
SwapTotal:     2097136 kB
SwapFree:      2095888 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5276 kB
Slab:            13912 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 01:50:47 (client local time) WITH STATUS 10 IN 1200.35 SECONDS
stats: 12389 7 1200.35 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 |    150487 |  148943   459474 |  209572  104610 19515828   186.6 |  2.756 % |
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.91 0.95 0.92 2/54 10197
Raw data (stat): 10197 (runsolver) R 10196 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 491550568 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.93 0.95 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 2824 0 0 0 992 6 0 0 25 0 1 0 491550568 13848576 2783 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3381 2783 603 41 0 3340 0
vsize: 13524
[startup+20.0009 s]
Raw data (loadavg): 0.94 0.95 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 3277 0 0 0 1990 7 0 0 25 0 1 0 491550568 15605760 3236 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3810 3236 603 41 0 3769 0
vsize: 15240
[startup+30.0007 s]
Raw data (loadavg): 0.95 0.95 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 3830 0 0 0 2988 9 0 0 25 0 1 0 491550568 17899520 3789 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4370 3789 603 41 0 4329 0
vsize: 17480
[startup+40.0009 s]
Raw data (loadavg): 0.95 0.95 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 4331 0 0 0 3987 11 0 0 25 0 1 0 491550568 19918848 4290 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4863 4290 603 41 0 4822 0
vsize: 19452
[startup+50.0017 s]
Raw data (loadavg): 0.96 0.95 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 4861 0 0 0 4986 13 0 0 25 0 1 0 491550568 22196224 4820 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5419 4820 603 41 0 5378 0
vsize: 21676
[startup+60.0012 s]
Raw data (loadavg): 0.97 0.95 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 5340 0 0 0 5985 14 0 0 25 0 1 0 491550568 24084480 5299 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5880 5299 603 41 0 5839 0
vsize: 23520
[startup+70.0024 s]
Raw data (loadavg): 0.97 0.95 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 11711 0 0 0 6970 29 0 0 25 0 1 0 491550568 46424064 10349 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11334 10349 603 41 0 11293 0
vsize: 45336
[startup+80.0032 s]
Raw data (loadavg): 0.98 0.95 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 11981 0 0 0 7969 29 0 0 25 0 1 0 491550568 47513600 10619 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11600 10619 603 41 0 11559 0
vsize: 46400
[startup+90.0038 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 12325 0 0 0 8969 30 0 0 25 0 1 0 491550568 48988160 10963 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11960 10963 603 41 0 11919 0
vsize: 47840
[startup+100.004 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 12564 0 0 0 9968 31 0 0 25 0 1 0 491550568 49934336 11202 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12191 11202 603 41 0 12150 0
vsize: 48764
[startup+110.004 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 12878 0 0 0 10967 32 0 0 25 0 1 0 491550568 50937856 11452 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12436 11452 603 41 0 12395 0
vsize: 49744
[startup+120.004 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 13267 0 0 0 11966 34 0 0 25 0 1 0 491550568 52535296 11841 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12826 11841 603 41 0 12785 0
vsize: 51304
[startup+130.005 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 13548 0 0 0 12964 35 0 0 25 0 1 0 491550568 53612544 12122 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13089 12122 603 41 0 13048 0
vsize: 52356
[startup+140.005 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 13848 0 0 0 13964 35 0 0 25 0 1 0 491550568 54829056 12422 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13386 12422 603 41 0 13345 0
vsize: 53544
[startup+150.005 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 14121 0 0 0 14963 36 0 0 25 0 1 0 491550568 56025088 12695 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13678 12695 603 41 0 13637 0
vsize: 54712
[startup+160.005 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 14463 0 0 0 15963 37 0 0 25 0 1 0 491550568 57364480 13037 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14005 13037 603 41 0 13964 0
vsize: 56020
[startup+170.006 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 14757 0 0 0 16962 38 0 0 25 0 1 0 491550568 58679296 13331 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14326 13331 603 41 0 14285 0
vsize: 57304
[startup+180.005 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 15118 0 0 0 17961 38 0 0 25 0 1 0 491550568 60153856 13692 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14686 13692 603 41 0 14645 0
vsize: 58744
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 15555 0 0 0 18960 40 0 0 25 0 1 0 491550568 62017536 14129 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15141 14129 603 41 0 15100 0
vsize: 60564
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 15931 0 0 0 19959 41 0 0 25 0 1 0 491550568 63475712 14505 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15497 14505 603 41 0 15456 0
vsize: 61988
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 16233 0 0 0 20959 41 0 0 25 0 1 0 491550568 64688128 14807 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15793 14807 603 41 0 15752 0
vsize: 63172
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 16520 0 0 0 21958 42 0 0 25 0 1 0 491550568 65875968 15094 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16083 15094 603 41 0 16042 0
vsize: 64332
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 16888 0 0 0 22957 44 0 0 25 0 1 0 491550568 67354624 15462 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16444 15462 603 41 0 16403 0
vsize: 65776
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 17218 0 0 0 23956 44 0 0 25 0 1 0 491550568 68702208 15792 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16773 15792 603 41 0 16732 0
vsize: 67092
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 17444 0 0 0 24956 45 0 0 25 0 1 0 491550568 69644288 16018 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17003 16018 603 41 0 16962 0
vsize: 68012
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 17700 0 0 0 25955 46 0 0 25 0 1 0 491550568 70717440 16274 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17265 16274 603 41 0 17224 0
vsize: 69060
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 17987 0 0 0 26955 46 0 0 25 0 1 0 491550568 71921664 16561 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17559 16561 603 41 0 17518 0
vsize: 70236
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 18230 0 0 0 27955 47 0 0 25 0 1 0 491550568 72859648 16804 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17788 16804 603 41 0 17747 0
vsize: 71152
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 18504 0 0 0 28954 48 0 0 25 0 1 0 491550568 73940992 17078 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18052 17078 603 41 0 18011 0
vsize: 72208
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 18656 0 0 0 29953 49 0 0 25 0 1 0 491550568 74616832 17230 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18217 17230 603 41 0 18176 0
vsize: 72868
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 18869 0 0 0 30952 50 0 0 25 0 1 0 491550568 75415552 17443 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18412 17443 603 41 0 18371 0
vsize: 73648
[startup+320.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 19172 0 0 0 31952 50 0 0 25 0 1 0 491550568 76632064 17746 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18709 17746 603 41 0 18668 0
vsize: 74836
[startup+330.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 19336 0 0 0 32952 51 0 0 25 0 1 0 491550568 77303808 17910 4294967295 134512640 134672761 3221224544 3221223648 134560019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18873 17910 603 41 0 18832 0
vsize: 75492
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 19595 0 0 0 33952 51 0 0 25 0 1 0 491550568 78381056 18169 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19136 18169 603 41 0 19095 0
vsize: 76544
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 19897 0 0 0 34951 52 0 0 25 0 1 0 491550568 79589376 18471 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19431 18471 603 41 0 19390 0
vsize: 77724
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 20095 0 0 0 35950 53 0 0 25 0 1 0 491550568 80400384 18669 4294967295 134512640 134672761 3221224544 3221223724 134556674 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19629 18669 603 41 0 19588 0
vsize: 78516
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 20352 0 0 0 36950 53 0 0 25 0 1 0 491550568 81469440 18926 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19890 18926 603 41 0 19849 0
vsize: 79560
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 20604 0 0 0 37950 54 0 0 25 0 1 0 491550568 82546688 19178 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20153 19178 603 41 0 20112 0
vsize: 80612
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 20754 0 0 0 38949 54 0 0 25 0 1 0 491550568 83079168 19328 4294967295 134512640 134672761 3221224544 3221223712 134561003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20283 19328 603 41 0 20242 0
vsize: 81132
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 21044 0 0 0 39949 55 0 0 25 0 1 0 491550568 84291584 19618 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20579 19618 603 41 0 20538 0
vsize: 82316
[startup+410.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 21296 0 0 0 40947 56 0 0 25 0 1 0 491550568 84840448 19759 4294967295 134512640 134672761 3221224544 3221223712 134560830 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.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 21296 0 0 0 41947 56 0 0 25 0 1 0 491550568 84840448 19759 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+430.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 21296 0 0 0 42947 56 0 0 25 0 1 0 491550568 84840448 19759 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+440.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 21296 0 0 0 43947 56 0 0 25 0 1 0 491550568 84840448 19759 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+450.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 21296 0 0 0 44947 56 0 0 25 0 1 0 491550568 84840448 19759 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+460.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 21296 0 0 0 45948 56 0 0 25 0 1 0 491550568 84840448 19759 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+470.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 21296 0 0 0 46948 56 0 0 25 0 1 0 491550568 84840448 19759 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+480.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 21296 0 0 0 47948 56 0 0 25 0 1 0 491550568 84840448 19759 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+490.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 21296 0 0 0 48948 56 0 0 25 0 1 0 491550568 84840448 19759 4294967295 134512640 134672761 3221224544 3221223648 134560293 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+500.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 21296 0 0 0 49948 56 0 0 25 0 1 0 491550568 84840448 19759 4294967295 134512640 134672761 3221224544 3221223648 134559883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+510.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 21296 0 0 0 50949 56 0 0 25 0 1 0 491550568 84840448 19759 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+520.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 21296 0 0 0 51949 56 0 0 25 0 1 0 491550568 84840448 19759 4294967295 134512640 134672761 3221224544 3221223648 134559841 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+530.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 21296 0 0 0 52949 57 0 0 25 0 1 0 491550568 84840448 19759 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+540.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 21296 0 0 0 53949 57 0 0 25 0 1 0 491550568 84840448 19759 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+550.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 21296 0 0 0 54949 57 0 0 25 0 1 0 491550568 84840448 19759 4294967295 134512640 134672761 3221224544 3221223648 134559941 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+560.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 21296 0 0 0 55949 57 0 0 25 0 1 0 491550568 84840448 19759 4294967295 134512640 134672761 3221224544 3221223648 134560313 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+570.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 21296 0 0 0 56950 57 0 0 25 0 1 0 491550568 84840448 19759 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+580.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 21296 0 0 0 57950 57 0 0 25 0 1 0 491550568 84840448 19759 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+590.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 21296 0 0 0 58950 57 0 0 25 0 1 0 491550568 84840448 19759 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+600.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 21296 0 0 0 59950 57 0 0 25 0 1 0 491550568 84840448 19759 4294967295 134512640 134672761 3221224544 3221223692 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+610.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 21296 0 0 0 60951 57 0 0 25 0 1 0 491550568 84840448 19759 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+620.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 21296 0 0 0 61951 57 0 0 25 0 1 0 491550568 84840448 19759 4294967295 134512640 134672761 3221224544 3221223648 134560379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+630.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 21296 0 0 0 62951 57 0 0 25 0 1 0 491550568 84840448 19759 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+640.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 21296 0 0 0 63951 57 0 0 25 0 1 0 491550568 84840448 19759 4294967295 134512640 134672761 3221224544 3221223680 134565056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+650.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 21296 0 0 0 64952 57 0 0 25 0 1 0 491550568 84840448 19759 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+660.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 21296 0 0 0 65952 57 0 0 25 0 1 0 491550568 84840448 19759 4294967295 134512640 134672761 3221224544 3221223696 134561040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+670.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 21296 0 0 0 66953 57 0 0 25 0 1 0 491550568 84840448 19759 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+680.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 21296 0 0 0 67953 57 0 0 25 0 1 0 491550568 84840448 19759 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20713 19759 603 41 0 20672 0
vsize: 82852
[startup+690.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 21297 0 0 0 68953 57 0 0 25 0 1 0 491550568 84840448 19760 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20713 19760 603 41 0 20672 0
vsize: 82852
[startup+700.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 21297 0 0 0 69953 57 0 0 25 0 1 0 491550568 84840448 19760 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20713 19760 603 41 0 20672 0
vsize: 82852
[startup+710.136 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 21297 0 0 0 70963 57 0 0 25 0 1 0 491550568 84840448 19760 4294967295 134512640 134672761 3221224544 3221223648 134560054 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.137 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 21297 0 0 0 71964 57 0 0 25 0 1 0 491550568 84840448 19760 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20713 19760 603 41 0 20672 0
vsize: 82852
[startup+730.136 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 21297 0 0 0 72964 57 0 0 25 0 1 0 491550568 84840448 19760 4294967295 134512640 134672761 3221224544 3221223680 134565137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20713 19760 603 41 0 20672 0
vsize: 82852
[startup+740.137 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 21297 0 0 0 73964 57 0 0 25 0 1 0 491550568 84840448 19760 4294967295 134512640 134672761 3221224544 3221223648 134559974 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20713 19760 603 41 0 20672 0
vsize: 82852
[startup+750.137 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 21298 0 0 0 74964 57 0 0 25 0 1 0 491550568 84840448 19761 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20713 19761 603 41 0 20672 0
vsize: 82852
[startup+760.137 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 21299 0 0 0 75964 57 0 0 25 0 1 0 491550568 84840448 19762 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20713 19762 603 41 0 20672 0
vsize: 82852
[startup+770.137 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 21482 0 0 0 76964 57 0 0 25 0 1 0 491550568 85647360 19945 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20910 19945 603 41 0 20869 0
vsize: 83640
[startup+780.137 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 21750 0 0 0 77963 58 0 0 25 0 1 0 491550568 86990848 20213 4294967295 134512640 134672761 3221224544 3221223728 134556675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21238 20213 603 41 0 21197 0
vsize: 84952
[startup+790.138 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 21818 0 0 0 78963 58 0 0 25 0 1 0 491550568 87261184 20281 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21304 20281 603 41 0 21263 0
vsize: 85216
[startup+800.138 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 22037 0 0 0 79963 59 0 0 25 0 1 0 491550568 88186880 20500 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21530 20500 603 41 0 21489 0
vsize: 86120
[startup+810.137 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 22226 0 0 0 80962 59 0 0 25 0 1 0 491550568 88989696 20689 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21726 20689 603 41 0 21685 0
vsize: 86904
[startup+820.138 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 22482 0 0 0 81962 60 0 0 25 0 1 0 491550568 89923584 20945 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21954 20945 603 41 0 21913 0
vsize: 87816
[startup+830.138 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 22666 0 0 0 82961 61 0 0 25 0 1 0 491550568 90734592 21129 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22152 21129 603 41 0 22111 0
vsize: 88608
[startup+840.139 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 22845 0 0 0 83961 62 0 0 25 0 1 0 491550568 91406336 21308 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22316 21308 603 41 0 22275 0
vsize: 89264
[startup+850.139 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 23007 0 0 0 84961 62 0 0 25 0 1 0 491550568 92078080 21470 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22480 21470 603 41 0 22439 0
vsize: 89920
[startup+860.139 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 23221 0 0 0 85961 62 0 0 25 0 1 0 491550568 93020160 21684 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22710 21684 603 41 0 22669 0
vsize: 90840
[startup+870.139 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 23365 0 0 0 86961 62 0 0 25 0 1 0 491550568 93556736 21828 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22841 21828 603 41 0 22800 0
vsize: 91364
[startup+880.139 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 23527 0 0 0 87960 63 0 0 25 0 1 0 491550568 94232576 21990 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23006 21990 603 41 0 22965 0
vsize: 92024
[startup+890.14 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 23712 0 0 0 88959 63 0 0 25 0 1 0 491550568 95035392 22175 4294967295 134512640 134672761 3221224544 3221223712 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23202 22175 603 41 0 23161 0
vsize: 92808
[startup+900.14 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 23858 0 0 0 89959 64 0 0 25 0 1 0 491550568 95576064 22321 4294967295 134512640 134672761 3221224544 3221223648 134560019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23334 22321 603 41 0 23293 0
vsize: 93336
[startup+910.14 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 24132 0 0 0 90958 65 0 0 25 0 1 0 491550568 96649216 22595 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23596 22595 603 41 0 23555 0
vsize: 94384
[startup+920.14 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 24393 0 0 0 91958 66 0 0 25 0 1 0 491550568 97718272 22856 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23857 22856 603 41 0 23816 0
vsize: 95428
[startup+930.14 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 24550 0 0 0 92957 66 0 0 25 0 1 0 491550568 98394112 23013 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24022 23013 603 41 0 23981 0
vsize: 96088
[startup+940.141 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 24803 0 0 0 93956 67 0 0 25 0 1 0 491550568 99467264 23266 4294967295 134512640 134672761 3221224544 3221223680 134560661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24284 23266 603 41 0 24243 0
vsize: 97136
[startup+950.141 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 24976 0 0 0 94956 68 0 0 25 0 1 0 491550568 100143104 23439 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24449 23439 603 41 0 24408 0
vsize: 97796
[startup+960.141 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 25191 0 0 0 95955 69 0 0 25 0 1 0 491550568 101081088 23654 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24678 23654 603 41 0 24637 0
vsize: 98712
[startup+970.141 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 25408 0 0 0 96954 70 0 0 25 0 1 0 491550568 101892096 23871 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24876 23871 603 41 0 24835 0
vsize: 99504
[startup+980.141 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 25567 0 0 0 97954 70 0 0 25 0 1 0 491550568 102559744 24030 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25039 24030 603 41 0 24998 0
vsize: 100156
[startup+990.141 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 25766 0 0 0 98954 71 0 0 25 0 1 0 491550568 103370752 24229 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25237 24229 603 41 0 25196 0
vsize: 100948
[startup+1000.14 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 25926 0 0 0 99953 72 0 0 25 0 1 0 491550568 104042496 24389 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25401 24389 603 41 0 25360 0
vsize: 101604
[startup+1010.14 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 26181 0 0 0 100952 73 0 0 25 0 1 0 491550568 105115648 24644 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25663 24644 603 41 0 25622 0
vsize: 102652
[startup+1020.14 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 26452 0 0 0 101952 73 0 0 25 0 1 0 491550568 106176512 24915 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25922 24915 603 41 0 25881 0
vsize: 103688
[startup+1030.14 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 26554 0 0 0 102952 73 0 0 25 0 1 0 491550568 106582016 25017 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26021 25017 603 41 0 25980 0
vsize: 104084
[startup+1040.14 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 26728 0 0 0 103951 74 0 0 25 0 1 0 491550568 107245568 25191 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26183 25191 603 41 0 26142 0
vsize: 104732
[startup+1050.14 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 26895 0 0 0 104951 75 0 0 25 0 1 0 491550568 107917312 25358 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26347 25358 603 41 0 26306 0
vsize: 105388
[startup+1060.14 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 27115 0 0 0 105950 76 0 0 25 0 1 0 491550568 108847104 25578 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26574 25578 603 41 0 26533 0
vsize: 106296
[startup+1070.15 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 27332 0 0 0 106950 76 0 0 25 0 1 0 491550568 109789184 25795 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26804 25795 603 41 0 26763 0
vsize: 107216
[startup+1080.14 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 27411 0 0 0 107950 77 0 0 25 0 1 0 491550568 110055424 25874 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26869 25874 603 41 0 26828 0
vsize: 107476
[startup+1090.15 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 27634 0 0 0 108950 77 0 0 25 0 1 0 491550568 110985216 26097 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27096 26097 603 41 0 27055 0
vsize: 108384
[startup+1100.15 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 27917 0 0 0 109949 78 0 0 25 0 1 0 491550568 112193536 26380 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27391 26380 603 41 0 27350 0
vsize: 109564
[startup+1110.15 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 28044 0 0 0 110949 78 0 0 25 0 1 0 491550568 112599040 26507 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27490 26507 603 41 0 27449 0
vsize: 109960
[startup+1120.15 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 28231 0 0 0 111948 79 0 0 25 0 1 0 491550568 113385472 26694 4294967295 134512640 134672761 3221224544 3221223648 134559937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27682 26694 603 41 0 27641 0
vsize: 110728
[startup+1130.15 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 28473 0 0 0 112948 79 0 0 25 0 1 0 491550568 114454528 26936 4294967295 134512640 134672761 3221224544 3221223648 134555211 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27943 26936 603 41 0 27902 0
vsize: 111772
[startup+1140.15 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 28726 0 0 0 113947 80 0 0 25 0 1 0 491550568 115396608 27189 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28173 27189 603 41 0 28132 0
vsize: 112692
[startup+1150.15 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 28950 0 0 0 114947 81 0 0 25 0 1 0 491550568 116330496 27413 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28401 27413 603 41 0 28360 0
vsize: 113604
[startup+1160.15 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 29046 0 0 0 115946 81 0 0 25 0 1 0 491550568 116736000 27509 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28500 27509 603 41 0 28459 0
vsize: 114000
[startup+1170.15 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 29257 0 0 0 116946 82 0 0 25 0 1 0 491550568 117542912 27720 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28697 27720 603 41 0 28656 0
vsize: 114788
[startup+1180.15 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 29363 0 0 0 117946 82 0 0 25 0 1 0 491550568 118079488 27826 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28828 27826 603 41 0 28787 0
vsize: 115312
[startup+1190.15 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 29476 0 0 0 118946 82 0 0 25 0 1 0 491550568 118472704 27939 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28924 27939 603 41 0 28883 0
vsize: 115696
[startup+1200.15 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10197
Raw data (stat): 10197 (minisat+) R 10196 25285 25284 0 -1 0 29522 0 0 0 119945 83 0 0 25 0 1 0 491550568 118738944 27985 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28989 27985 603 41 0 28948 0
vsize: 115956
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.21 s]
Raw data (loadavg): 0.99 0.97 0.92 1/54 10197
Raw data (stat): 10197 (minisat+) Z 10196 25285 25284 0 -1 12 29525 0 0 0 119946 88 0 0 25 0 1 0 491550568 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.35
CPU user time (s): 1199.46
CPU system time (s): 0.884865
CPU usage (%): 100.012
Max. virtual memory (Kb): 115956
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####