PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-10teams.opb
MD5SUM	130bea0863cb3f92addf09aabe15daa3
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	920
Optimality of the best value was proved	NO
Number of terms in the objective function	1800
Biggest coefficient in the objective function	86
Number of bits for the biggest coefficient in the objective function	7
Sum of the numbers in the objective function	41700
Number of bits of the sum of numbers in the objective function	16
Biggest number in a constraint	86
Number of bits of the biggest number in a constraint	7
Biggest sum of numbers in a constraint	41700
Number of bits of the biggest sum of numbers	16
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.54
Number of variables	1800
Total number of constraints	2015
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	2015
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	72
Trace number 16557

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc11 THE 2005-04-21 07:42:32 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13154 boxname=wulflinc11 idbench=1012 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  130bea0863cb3f92addf09aabe15daa3  /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-10teams.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-10teams.opb /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-10teams.opb
IDLAUNCH: 13154
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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.028
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:        764424 kB
Buffers:         28708 kB
Cached:         220716 kB
SwapCached:          0 kB
Active:          95400 kB
Inactive:       156772 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        764172 kB
SwapTotal:     2097136 kB
SwapFree:      2097048 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6816 kB
Slab:            12484 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 08:02:35 (client local time) WITH STATUS 10 IN 1200.88 SECONDS
stats: 13154 7 1200.88 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 330 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 328]---> BDD-cost:   77
c ---[ 326]---> BDD-cost:   77
c ---[ 324]---> BDD-cost:   77
c ---[ 322]---> BDD-cost:   77
c ---[ 320]---> BDD-cost:   77
c ---[ 318]---> BDD-cost:   77
c ---[ 316]---> BDD-cost:   77
c ---[ 314]---> BDD-cost:   77
c ---[ 312]---> BDD-cost:   77
c ---[ 310]---> BDD-cost:   77
c ---[ 308]---> BDD-cost:   77
c ---[ 306]---> BDD-cost:   77
c ---[ 304]---> BDD-cost:   77
c ---[ 302]---> BDD-cost:   77
c ---[ 300]---> BDD-cost:   77
c ---[ 298]---> BDD-cost:   77
c ---[ 296]---> BDD-cost:   77
c ---[ 294]---> BDD-cost:   77
c ---[ 292]---> BDD-cost:   77
c ---[ 290]---> BDD-cost:   77
c ---[ 288]---> BDD-cost:   77
c ---[ 286]---> BDD-cost:   77
c ---[ 284]---> BDD-cost:   77
c ---[ 282]---> BDD-cost:   77
c ---[ 280]---> BDD-cost:   77
c ---[ 278]---> BDD-cost:   77
c ---[ 276]---> BDD-cost:   77
c ---[ 274]---> BDD-cost:   77
c ---[ 272]---> BDD-cost:   77
c ---[ 270]---> BDD-cost:   77
c ---[ 268]---> BDD-cost:   77
c ---[ 266]---> BDD-cost:   77
c ---[ 264]---> BDD-cost:   77
c ---[ 262]---> BDD-cost:   77
c ---[ 260]---> BDD-cost:   77
c ---[ 258]---> BDD-cost:   77
c ---[ 256]---> BDD-cost:   77
c ---[ 254]---> BDD-cost:   77
c ---[ 252]---> BDD-cost:   77
c ---[ 250]---> BDD-cost:   77
c ---[ 249]---> BDD-cost:  125
c ---[ 248]---> BDD-cost:  185
c ---[ 247]---> BDD-cost:  185
c ---[ 246]---> BDD-cost:  185
c ---[ 245]---> BDD-cost:  185
c ---[ 244]---> BDD-cost:  185
c ---[ 243]---> BDD-cost:  125
c ---[ 242]---> BDD-cost:  185
c ---[ 241]---> BDD-cost:  185
c ---[ 240]---> BDD-cost:  185
c ---[ 239]---> BDD-cost:  185
c ---[ 238]---> BDD-cost:  125
c ---[ 237]---> BDD-cost:  185
c ---[ 236]---> BDD-cost:  185
c ---[ 235]---> BDD-cost:  185
c ---[ 234]---> BDD-cost:  185
c ---[ 233]---> BDD-cost:  185
c ---[ 232]---> BDD-cost:  125
c ---[ 231]---> BDD-cost:  185
c ---[ 230]---> BDD-cost:  185
c ---[ 229]---> BDD-cost:  185
c ---[ 228]---> BDD-cost:  185
c ---[ 227]---> BDD-cost:  125
c ---[ 226]---> BDD-cost:  185
c ---[ 225]---> BDD-cost:  185
c ---[ 224]---> BDD-cost:  185
c ---[ 223]---> BDD-cost:  185
c ---[ 222]---> BDD-cost:  185
c ---[ 221]---> BDD-cost:  125
c ---[ 220]---> BDD-cost:  185
c ---[ 219]---> BDD-cost:  185
c ---[ 218]---> BDD-cost:  185
c ---[ 217]---> BDD-cost:  185
c ---[ 216]---> BDD-cost:  125
c ---[ 215]---> BDD-cost:  185
c ---[ 214]---> BDD-cost:  185
c ---[ 213]---> BDD-cost:  185
c ---[ 212]---> BDD-cost:  185
c ---[ 211]---> BDD-cost:  185
c ---[ 210]---> BDD-cost:  125
c ---[ 209]---> BDD-cost:  125
c ---[ 208]---> BDD-cost:  185
c ---[ 207]---> BDD-cost:  185
c ---[ 206]---> BDD-cost:  185
c ---[ 205]---> BDD-cost:  185
c ---[ 204]---> BDD-cost:  185
c ---[ 203]---> BDD-cost:  185
c ---[ 202]---> BDD-cost:  185
c ---[ 201]---> BDD-cost:  185
c ---[ 200]---> BDD-cost:  125
c ---[ 199]---> BDD-cost:   75
c ---[ 198]---> BDD-cost:   77
c ---[ 197]---> BDD-cost:   77
c ---[ 196]---> BDD-cost:   77
c ---[ 195]---> BDD-cost:   77
c ---[ 194]---> BDD-cost:   77
c ---[ 193]---> BDD-cost:   77
c ---[ 192]---> BDD-cost:   77
c ---[ 191]---> BDD-cost:   75
c ---[ 190]---> BDD-cost:   77
c ---[ 189]---> BDD-cost:   77
c ---[ 188]---> BDD-cost:   77
c ---[ 187]---> BDD-cost:   77
c ---[ 186]---> BDD-cost:   77
c ---[ 185]---> BDD-cost:   77
c ---[ 184]---> BDD-cost:   77
c ---[ 183]---> BDD-cost:   75
c ---[ 182]---> BDD-cost:   77
c ---[ 181]---> BDD-cost:   77
c ---[ 180]---> BDD-cost:   77
c ---[ 179]---> BDD-cost:   77
c ---[ 178]---> BDD-cost:   77
c ---[ 177]---> BDD-cost:   77
c ---[ 176]---> BDD-cost:   77
c ---[ 175]---> BDD-cost:   75
c ---[ 174]---> BDD-cost:   77
c ---[ 173]---> BDD-cost:   77
c ---[ 172]---> BDD-cost:   77
c ---[ 171]---> BDD-cost:   77
c ---[ 170]---> BDD-cost:   77
c ---[ 169]---> BDD-cost:   77
c ---[ 168]---> BDD-cost:   77
c ---[ 167]---> BDD-cost:   75
c ---[ 166]---> BDD-cost:   77
c ---[ 165]---> BDD-cost:   77
c ---[ 164]---> BDD-cost:   77
c ---[ 163]---> BDD-cost:   77
c ---[ 162]---> BDD-cost:   77
c ---[ 161]---> BDD-cost:   77
c ---[ 160]---> BDD-cost:   77
c ---[ 158]---> BDD-cost:   70
c ---[ 156]---> BDD-cost:   77
c ---[ 154]---> BDD-cost:   77
c ---[ 152]---> BDD-cost:   77
c ---[ 150]---> BDD-cost:   77
c ---[ 148]---> BDD-cost:   77
c ---[ 146]---> BDD-cost:   77
c ---[ 144]---> BDD-cost:   77
c ---[ 142]---> BDD-cost:   70
c ---[ 140]---> BDD-cost:   76
c ---[ 138]---> BDD-cost:   76
c ---[ 136]---> BDD-cost:   76
c ---[ 134]---> BDD-cost:   76
c ---[ 132]---> BDD-cost:   76
c ---[ 130]---> BDD-cost:   76
c ---[ 128]---> BDD-cost:   76
c ---[ 126]---> BDD-cost:   70
c ---[ 124]---> BDD-cost:   77
c ---[ 122]---> BDD-cost:   77
c ---[ 120]---> BDD-cost:   77
c ---[ 118]---> BDD-cost:   77
c ---[ 116]---> BDD-cost:   77
c ---[ 114]---> BDD-cost:   77
c ---[ 112]---> BDD-cost:   77
c ---[ 110]---> BDD-cost:   70
c ---[ 108]---> BDD-cost:   77
c ---[ 106]---> BDD-cost:   77
c ---[ 104]---> BDD-cost:   77
c ---[ 102]---> BDD-cost:   77
c ---[ 100]---> BDD-cost:   77
c ---[  98]---> BDD-cost:   77
c ---[  96]---> BDD-cost:   77
c ---[  94]---> BDD-cost:   70
c ---[  92]---> BDD-cost:   77
c ---[  90]---> BDD-cost:   77
c ---[  88]---> BDD-cost:   77
c ---[  86]---> BDD-cost:   77
c ---[  84]---> BDD-cost:   77
c ---[  82]---> BDD-cost:   77
c ---[  80]---> BDD-cost:   77
c ---[  78]---> BDD-cost:   70
c ---[  76]---> BDD-cost:   77
c ---[  74]---> BDD-cost:   77
c ---[  72]---> BDD-cost:   77
c ---[  70]---> BDD-cost:   77
c ---[  68]---> BDD-cost:   77
c ---[  66]---> BDD-cost:   77
c ---[  64]---> BDD-cost:   77
c ---[  62]---> BDD-cost:   70
c ---[  60]---> BDD-cost:   77
c ---[  58]---> BDD-cost:   77
c ---[  56]---> BDD-cost:   77
c ---[  54]---> BDD-cost:   77
c ---[  52]---> BDD-cost:   77
c ---[  50]---> BDD-cost:   77
c ---[  48]---> BDD-cost:   77
c ---[  46]---> BDD-cost:   70
c ---[  44]---> BDD-cost:   77
c ---[  42]---> BDD-cost:   77
c ---[  40]---> BDD-cost:   77
c ---[  38]---> BDD-cost:   77
c ---[  36]---> BDD-cost:   77
c ---[  34]---> BDD-cost:   77
c ---[  32]---> BDD-cost:   77
c ---[  30]---> BDD-cost:   70
c ---[  28]---> BDD-cost:   77
c ---[  26]---> BDD-cost:   77
c ---[  24]---> BDD-cost:   77
c ---[  22]---> BDD-cost:   77
c ---[  20]---> BDD-cost:   77
c ---[  18]---> BDD-cost:   77
c ---[  16]---> BDD-cost:   77
c ---[  14]---> BDD-cost:   70
c ---[  12]---> BDD-cost:   77
c ---[  10]---> BDD-cost:   77
c ---[   8]---> BDD-cost:   77
c ---[   6]---> BDD-cost:   77
c ---[   4]---> BDD-cost:   77
c ---[   2]---> BDD-cost:   77
c ---[   0]---> BDD-cost:   77
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   53221   141547 |   15966       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/22273          
c   -- var.elim.:  2000/22273          
c   -- var.elim.:  3000/22273          
c   -- var.elim.:  4000/22273          
c   -- var.elim.:  5000/22273          
c   -- var.elim.:  6000/22273          
c   -- var.elim.:  7000/22273          
c   -- var.elim.:  8000/22273          
c   -- var.elim.:  9000/22273          
c   -- var.elim.:  10000/22273          
c   -- var.elim.:  11000/22273          
c   -- var.elim.:  12000/22273          
c   -- var.elim.:  13000/22273          
c   -- var.elim.:  14000/22273          
c   -- var.elim.:  15000/22273          
c   -- var.elim.:  16000/22273          
c   -- var.elim.:  17000/22273          
c   -- var.elim.:  18000/22273          
c   -- var.elim.:  19000/22273          
c   -- var.elim.:  20000/22273          
c   -- var.elim.:  21000/22273          
c   -- var.elim.:  22000/22273          
c   -- var.elim.:  22273/22273          
c   -- var.elim.:  1000/1593          
c   -- var.elim.:  1593/1593          
c   -- subsuming                       
c   -- var.elim.:  1000/1133          
c   -- var.elim.:  1133/1133          
c   -- var.elim.:  1000/1203          
c   -- var.elim.:  1203/1203          
c   -- subsuming                       
c   -- var.elim.:  734/734          
c   -- var.elim.:  187/187          
c   -- subsuming                       
c   -- var.elim.:  185/185          
c |         0 |   52136   138492 |      --       0       --      -- |     --   | -1085/-2425
c |         0 |   52136   138492 |   20854       0        0     nan |  0.000 % |
c |       100 |   52136   138492 |   22939     100     1429    14.3 |  1.881 % |
c |       251 |   52136   138492 |   25233     251     2817    11.2 |  1.881 % |
c |       476 |   52136   138492 |   27757     476    45711    96.0 |  1.881 % |
c |       814 |   52136   138492 |   30532     814    78470    96.4 |  1.881 % |
c |      1320 |   52136   138492 |   33586    1320    94579    71.7 |  1.881 % |
c |      2080 |   52136   138492 |   36944    2080   342454   164.6 |  1.881 % |
c |      3219 |   52136   138492 |   40639    3219   763811   237.3 |  1.881 % |
c |      4928 |   52136   138492 |   44703    4928  1116624   226.6 |  1.881 % |
c |      7498 |   52136   138492 |   49173    7498  1797948   239.8 |  1.881 % |
c |     11342 |   52136   138492 |   54090   11342  3018671   266.1 |  1.881 % |
c ==============================================================================
c (current CPU-time: 43.8283 s)
c ==============================================================================
c [1mFound solution: 968[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 7750   maxlim: 39032   bits: 16/16
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     14144 |  106296   331915 |   31888   14144  4345410   307.2 |  1.881 % |
c   -- subsuming                       
c   -- var.elim.:  1000/9299          
c   -- var.elim.:  2000/9299          
c   -- var.elim.:  3000/9299          
c   -- var.elim.:  4000/9299          
c   -- var.elim.:  5000/9299          
c   -- var.elim.:  6000/9299          
c   -- var.elim.:  7000/9299          
c   -- var.elim.:  8000/9299          
c   -- var.elim.:  9000/9299          
c   -- var.elim.:  9299/9299          
c   -- var.elim.:  23/23          
c |     14144 |  105937   330467 |      --   14144       --      -- |     --   | -327/-1291
c |     14144 |  105937   330467 |   42374   14144  4345410   307.2 |  1.881 % |
c |     14244 |  105937   330467 |   46612   14244  4347585   305.2 |  1.584 % |
c |     14394 |  105937   330467 |   51273   14394  4351647   302.3 |  1.584 % |
c |     14620 |  105937   330467 |   56400   14620  4384983   299.9 |  1.584 % |
c |     14957 |  105937   330467 |   62040   14957  4460921   298.2 |  1.584 % |
c |     15465 |  105937   330467 |   68245   15465  4562481   295.0 |  1.584 % |
c |     16227 |  105937   330467 |   75069   16227  4820412   297.1 |  1.584 % |
c |     17367 |  105937   330467 |   82576   17367  5037115   290.0 |  1.584 % |
c |     19077 |  105937   330467 |   90834   19077  5701910   298.9 |  1.584 % |
c |     21642 |  105937   330467 |   99917   21642  7081420   327.2 |  1.584 % |
c |     25486 |  105937   330467 |  109909   25486  8630865   338.7 |  1.584 % |
c |     31253 |  105937   330467 |  120900   31253 12433546   397.8 |  1.584 % |
c |     39902 |  105937   330467 |  132990   39902 16688811   418.2 |  1.584 % |
c |     52876 |  105937   330467 |  146289   52876 23499696   444.4 |  1.584 % |
c |     72338 |  105937   330467 |  160918   72338 36744269   508.0 |  1.584 % |
c ==============================================================================
c (current CPU-time: 607.685 s)
c ==============================================================================
c [1mFound solution: 954[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 39046   bits: 16/16
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     81317 |  105961   330569 |   31788   81317 41683767   512.6 |  1.584 % |
c   -- subsuming                       
c   -- var.elim.:  28/28          
c   -- var.elim.:  15/15          
c |     81317 |  105937   330453 |      --   81317       --      -- |     --   | -10/-12
c |     81317 |  105937   330453 |   42374   81317 41683767   512.6 |  1.584 % |
c |     81417 |  105937   330453 |   46612   17775  7239412   407.3 |  1.597 % |
c |     81568 |  105937   330453 |   51273   17926  7277974   406.0 |  1.597 % |
c |     81794 |  105937   330453 |   56400   18152  7306505   402.5 |  1.597 % |
c |     82131 |  105937   330453 |   62040   18489  7355725   397.8 |  1.597 % |
c |     82637 |  105937   330453 |   68245   18995  7481058   393.8 |  1.597 % |
c |     83398 |  105937   330453 |   75069   19756  7647110   387.1 |  1.597 % |
c |     84537 |  105937   330453 |   82576   20895  7904280   378.3 |  1.597 % |
c |     86246 |  105937   330453 |   90834   22604  8417948   372.4 |  1.597 % |
c |     88808 |  105937   330453 |   99917   25166  9215033   366.2 |  1.597 % |
c |     92652 |  105937   330453 |  109909   29010 11000741   379.2 |  1.597 % |
c |     98419 |  105937   330453 |  120900   34777 13494486   388.0 |  1.597 % |
c |    107070 |  105937   330453 |  132990   43428 16511680   380.2 |  1.597 % |
c |    120047 |  105937   330453 |  146289   56405 25548802   453.0 |  1.597 % |
c |    139510 |  105937   330453 |  160918   75868 43995138   579.9 |  1.597 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x10212_bit0 -x10312_bit0 -x20312_bit0 -x10412_bit0 -x20412_bit0 -x30412_bit0 -x10512_bit0 -x20512_bit0 -x30512_bit0 -x40512_bit0 -x10612_bit0 -x20612_bit0 -x30612_bit0 -x40612_bit0 -x50612_bit0 -x10712_bit0 -x20712_bit0 -x30712_bit0 x40712_bit0 -x50712_bit0 -x60712_bit0 -x10812_bit0 -x20812_bit0 -x30812_bit0 -x40812_bit0 -x50812_bit0 -x60812_bit0 -x70812_bit0 -x10912_bit0 -x20912_bit0 -x30912_bit0 -x40912_bit0 -x50912_bit0 -x60912_bit0 -x70912_bit0 -x80912_bit0 -x11012_bit0 -x21012_bit0 -x31012_bit0 -x41012_bit0 -x51012_bit0 -x61012_bit0 -x71012_bit0 -x81012_bit0 -x91012_bit0 -x10222_bit0 -x10322_bit0 -x20322_bit0 -x10422_bit0 -x20422_bit0 -x30422_bit0 -x10522_bit0 x20522_bit0 -x30522_bit0 -x40522_bit0 -x10622_bit0 -x20622_bit0 -x30622_bit0 -x40622_bit0 -x50622_bit0 -x10722_bit0 -x20722_bit0 -x30722_bit0 -x40722_bit0 -x50722_bit0 -x60722_bit0 -x10822_bit0 -x20822_bit0 -x30822_bit0 -x40822_bit0 -x50822_bit0 -x60822_bit0 -x70822_bit0 -x10922_bit0 -x20922_bit0 -x30922_bit0 -x40922_bit0 -x50922_bit0 -x60922_bit0 -x70922_bit0 -x80922_bit0 -x11022_bit0 -x21022_bit0 -x31022_bit0 -x41022_bit0 -x51022_bit0 -x61022_bit0 -x71022_bit0 -x81022_bit0 -x91022_bit0 -x10232_bit0 -x10332_bit0 -x20332_bit0 -x10432_bit0 -x20432_bit0 -x30432_bit0 -x10532_bit0 -x20532_bit0 -x30532_bit0 -x40532_bit0 -x10632_bit0 -x20632_bit0 -x30632_bit0 -x40632_bit0 -x50632_bit0 -x10732_bit0 -x20732_bit0 -x30732_bit0 -x40732_bit0 -x50732_bit0 -x60732_bit0 -x10832_bit0 -x20832_bit0 x30832_bit0 -x40832_bit0 -x50832_bit0 -x60832_bit0 -x70832_bit0 -x10932_bit0 -x20932_bit0 -x30932_bit0 -x40932_bit0 -x50932_bit0 -x60932_bit0 -x70932_bit0 -x80932_bit0 -x11032_bit0 -x21032_bit0 -x31032_bit0 -x41032_bit0 -x51032_bit0 -x61032_bit0 -x71032_bit0 -x81032_bit0 -x91032_bit0 -x10242_bit0 -x10342_bit0 -x20342_bit0 -x10442_bit0 -x20442_bit0 -x30442_bit0 -x10542_bit0 -x20542_bit0 -x30542_bit0 -x40542_bit0 -x10642_bit0 -x20642_bit0 -x30642_bit0 -x40642_bit0 -x50642_bit0 -x10742_bit0 -x20742_bit0 -x30742_bit0 -x40742_bit0 -x50742_bit0 -x60742_bit0 -x10842_bit0 -x20842_bit0 -x30842_bit0 -x40842_bit0 -x50842_bit0 -x60842_bit0 -x70842_bit0 -x10942_bit0 -x20942_bit0 -x30942_bit0 -x40942_bit0 -x50942_bit0 -x60942_bit0 -x70942_bit0 -x80942_bit0 -x11042_bit0 -x21042_bit0 -x31042_bit0 -x41042_bit0 -x51042_bit0 x61042_bit0 -x71042_bit0 -x81042_bit0 -x91042_bit0 -x10252_bit0 -x10352_bit0 -x20352_bit0 -x10452_bit0 -x20452_bit0 -x30452_bit0 -x10552_bit0 -x20552_bit0 -x30552_bit0 -x40552_bit0 -x10652_bit0 -x20652_bit0 -x30652_bit0 -x40652_bit0 -x50652_bit0 -x10752_bit0 -x20752_bit0 -x30752_bit0 -x40752_bit0 -x50752_bit0 -x60752_bit0 -x10852_bit0 -x20852_bit0 -x30852_bit0 -x40852_bit0 -x50852_bit0 -x60852_bit0 -x70852_bit0 x10952_bit0 -x20952_bit0 -x30952_bit0 -x40952_bit0 -x50952_bit0 -x60952_bit0 -x70952_bit0 -x80952_bit0 -x11052_bit0 -x21052_bit0 -x31052_bit0 -x41052_bit0 -x51052_bit0 -x61052_bit0 -x71052_bit0 -x81052_bit0 -x91052_bit0 -x10213_bit0 -x10313_bit0 -x20313_bit0 -x10413_bit0 -x20413_bit0 -x30413_bit0 -x10513_bit0 -x20513_bit0 -x30513_bit0 -x40513_bit0 -x10613_bit0 -x20613_bit0 -x30613_bit0 -x40613_bit0 -x50613_bit0 -x10713_bit0 -x20713_bit0 -x30713_bit0 -x40713_bit0 -x50713_bit0 -x60713_bit0 -x10813_bit0 -x20813_bit0 -x30813_bit0 -x40813_bit0 -x50813_bit0 -x60813_bit0 -x70813_bit0 -x10913_bit0 x20913_bit0 -x30913_bit0 -x40913_bit0 -x50913_bit0 -x60913_bit0 -x70913_bit0 -x80913_bit0 -x11013_bit0 -x21013_bit0 -x31013_bit0 -x41013_bit0 -x51013_bit0 -x61013_bit0 -x71013_bit0 -x81013_bit0 -x91013_bit0 -x10223_bit0 -x10323_bit0 -x20323_bit0 -x10423_bit0 -x20423_bit0 -x30423_bit0 -x10523_bit0 -x20523_bit0 -x30523_bit0 -x40523_bit0 -x10623_bit0 -x20623_bit0 -x30623_bit0 -x40623_bit0 -x50623_bit0 -x10723_bit0 -x20723_bit0 -x30723_bit0 -x40723_bit0 -x50723_bit0 -x60723_bit0 -x10823_bit0 -x20823_bit0 -x30823_bit0 -x40823_bit0 -x50823_bit0 -x60823_bit0 -x70823_bit0 -x10923_bit0 -x20923_bit0 -x30923_bit0 -x40923_bit0 -x50923_bit0 -x60923_bit0 -x70923_bit0 -x80923_bit0 -x11023_bit0 -x21023_bit0 -x31023_bit0 -x41023_bit0 x51023_bit0 -x61023_bit0 -x71023_bit0 -x81023_bit0 -x91023_bit0 -x10233_bit0 -x10333_bit0 -x20333_bit0 -x10433_bit0 -x20433_bit0 -x30433_bit0 -x10533_bit0 -x20533_bit0 -x30533_bit0 -x40533_bit0 x10633_bit0 -x20633_bit0 -x30633_bit0 -x40633_bit0 -x50633_bit0 -x10733_bit0 -x20733_bit0 -x30733_bit0 -x40733_bit0 -x50733_bit0 -x60733_bit0 -x10833_bit0 -x20833_bit0 -x30833_bit0 -x40833_bit0 -x50833_bit0 -x60833_bit0 -x70833_bit0 -x10933_bit0 -x20933_bit0 -x30933_bit0 -x40933_bit0 -x50933_bit0 -x60933_bit0 -x70933_bit0 -x80933_bit0 -x11033_bit0 -x21033_bit0 -x31033_bit0 -x41033_bit0 -x51033_bit0 -x61033_bit0 -x71033_bit0 -x81033_bit0 -x91033_bit0 -x10243_bit0 -x10343_bit0 -x20343_bit0 -x10443_bit0 -x20443_bit0 -x30443_bit0 -x10543_bit0 -x20543_bit0 -x30543_bit0 -x40543_bit0 -x10643_bit0 -x20643_bit0 -x30643_bit0 -x40643_bit0 -x50643_bit0 -x10743_bit0 -x20743_bit0 x30743_bit0 -x40743_bit0 -x50743_bit0 -x60743_bit0 -x10843_bit0 -x20843_bit0 -x30843_bit0 -x40843_bit0 -x50843_bit0 -x60843_bit0 -x70843_bit0 -x10943_bit0 -x20943_bit0 -x30943_bit0 -x40943_bit0 -x50943_bit0 -x60943_bit0 -x70943_bit0 -x80943_bit0 -x11043_bit0 -x21043_bit0 -x31043_bit0 -x41043_bit0 -x51043_bit0 -x61043_bit0 -x71043_bit0 -x81043_bit0 -x91043_bit0 -x10253_bit0 -x10353_bit0 -x20353_bit0 -x10453_bit0 -x20453_bit0 -x30453_bit0 -x10553_bit0 -x20553_bit0 -x30553_bit0 -x40553_bit0 -x10653_bit0 -x20653_bit0 -x30653_bit0 -x40653_bit0 -x50653_bit0 -x10753_bit0 -x20753_bit0 -x30753_bit0 -x40753_bit0 -x50753_bit0 -x60753_bit0 -x10853_bit0 -x20853_bit0 -x30853_bit0 x40853_bit0 -x50853_bit0 -x60853_bit0 -x70853_bit0 -x10953_bit0 -x20953_bit0 -x30953_bit0 -x40953_bit0 -x50953_bit0 -x60953_bit0 -x70953_bit0 -x80953_bit0 -x11053_bit0 -x21053_bit0 -x31053_bit0 -x41053_bit0 -x51053_bit0 -x61053_bit0 -x71053_bit0 -x81053_bit0 -x91053_bit0 -x10214_bit0 -x10314_bit0 -x20314_bit0 -x10414_bit0 -x20414_bit0 -x30414_bit0 -x10514_bit0 -x20514_bit0 -x30514_bit0 -x40514_bit0 -x10614_bit0 -x20614_bit0 -x30614_bit0 -x40614_bit0 -x50614_bit0 -x10714_bit0 -x20714_bit0 -x30714_bit0 -x40714_bit0 -x50714_bit0 -x60714_bit0 -x10814_bit0 -x20814_bit0 -x30814_bit0 -x40814_bit0 -x50814_bit0 -x60814_bit0 -x70814_bit0 -x10914_bit0 -x20914_bit0 -x30914_bit0 -x40914_bit0 -x50914_bit0 -x60914_bit0 -x70914_bit0 -x80914_bit0 -x11014_bit0 -x21014_bit0 -x31014_bit0 x41014_bit0 -x51014_bit0 -x61014_bit0 -x71014_bit0 -x81014_bit0 -x91014_bit0 -x10224_bit0 -x10324_bit0 -x20324_bit0 -x10424_bit0 -x20424_bit0 -x30424_bit0 -x10524_bit0 -x20524_bit0 -x30524_bit0 -x40524_bit0 -x10624_bit0 -x20624_bit0 -x30624_bit0 -x40624_bit0 -x50624_bit0 -x10724_bit0 -x20724_bit0 -x30724_bit0 -x40724_bit0 -x50724_bit0 -x60724_bit0 -x10824_bit0 -x20824_bit0 -x30824_bit0 -x40824_bit0 -x50824_bit0 -x60824_bit0 -x70824_bit0 -x10924_bit0 -x20924_bit0 -x30924_bit0 -x40924_bit0 -x50924_bit0 -x60924_bit0 -x70924_bit0 x80924_bit0 -x11024_bit0 -x21024_bit0 -x31024_bit0 -x41024_bit0 -x51024_bit0 -x61024_bit0 -x71024_bit0 -x81024_bit0 -x91024_bit0 -x10234_bit0 -x10334_bit0 -x20334_bit0 -x10434_bit0 -x20434_bit0 -x30434_bit0 -x10534_bit0 -x20534_bit0 -x30534_bit0 -x40534_bit0 -x10634_bit0 -x20634_bit0 -x30634_bit0 -x40634_bit0 -x50634_bit0 -x10734_bit0 x20734_bit0 -x30734_bit0 -x40734_bit0 -x50734_bit0 -x60734_bit0 -x10834_bit0 -x20834_bit0 -x30834_bit0 -x40834_bit0 -x50834_bit0 -x60834_bit0 -x70834_bit0 -x10934_bit0 -x20934_bit0 -x30934_bit0 -x40934_bit0 -x50934_bit0 -x60934_bit0 -x70934_bit0 -x80934_bit0 -x11034_bit0 -x21034_bit0 -x31034_bit0 -x41034_bit0 -x51034_bit0 -x61034_bit0 -x71034_bit0 -x81034_bit0 -x91034_bit0 -x10244_bit0 -x10344_bit0 -x20344_bit0 -x10444_bit0 -x20444_bit0 -x30444_bit0 x10544_bit0 -x20544_bit0 -x30544_bit0 -x40544_bit0 -x10644_bit0 -x20644_bit0 -x30644_bit0 -x40644_bit0 -x50644_bit0 -x10744_bit0 -x20744_bit0 -x30744_bit0 -x40744_bit0 -x50744_bit0 -x60744_bit0 -x10844_bit0 -x20844_bit0 -x30844_bit0 -x40844_bit0 -x50844_bit0 -x60844_bit0 -x70844_bit0 -x10944_bit0 -x20944_bit0 -x30944_bit0 -x40944_bit0 -x50944_bit0 -x60944_bit0 -x70944_bit0 -x80944_bit0 -x11044_bit0 -x21044_bit0 -x31044_bit0 -x41044_bit0 -x51044_bit0 -x61044_bit0 -x71044_bit0 -x81044_bit0 -x91044_bit0 -x10254_bit0 -x10354_bit0 -x20354_bit0 -x10454_bit0 -x20454_bit0 -x30454_bit0 -x10554_bit0 -x20554_bit0 -x30554_bit0 -x40554_bit0 -x10654_bit0 -x20654_bit0 x30654_bit0 -x40654_bit0 -x50654_bit0 -x10754_bit0 -x20754_bit0 -x30754_bit0 -x40754_bit0 -x50754_bit0 -x60754_bit0 -x10854_bit0 -x20854_bit0 -x30854_bit0 -x40854_bit0 -x50854_bit0 -x60854_bit0 -x70854_bit0 -x10954_bit0 -x20954_bit0 -x30954_bit0 -x40954_bit0 -x50954_bit0 -x60954_bit0 -x70954_bit0 -x80954_bit0 -x11054_bit0 -x21054_bit0 -x31054_bit0 -x41054_bit0 -x51054_bit0 -x61054_bit0 -x71054_bit0 -x81054_bit0 -x91054_bit0 -x10215_bit0 -x10315_bit0 -x20315_bit0 -x10415_bit0 -x20415_bit0 -x30415_bit0 -x10515_bit0 -x20515_bit0 -x30515_bit0 -x40515_bit0 -x10615_bit0 -x20615_bit0 -x30615_bit0 -x40615_bit0 -x50615_bit0 -x10715_bit0 -x20715_bit0 -x30715_bit0 -x40715_bit0 -x50715_bit0 -x60715_bit0 -x10815_bit0 -x20815_bit0 -x30815_bit0 -x40815_bit0 -x50815_bit0 x60815_bit0 -x70815_bit0 -x10915_bit0 -x20915_bit0 -x30915_bit0 -x40915_bit0 -x50915_bit0 -x60915_bit0 -x70915_bit0 -x80915_bit0 -x11015_bit0 -x21015_bit0 -x31015_bit0 -x41015_bit0 -x51015_bit0 -x61015_bit0 -x71015_bit0 -x81015_bit0 -x91015_bit0 -x10225_bit0 -x10325_bit0 -x20325_bit0 -x10425_bit0 -x20425_bit0 -x30425_bit0 -x10525_bit0 -x20525_bit0 -x30525_bit0 -x40525_bit0 -x10625_bit0 -x20625_bit0 -x30625_bit0 -x40625_bit0 -x50625_bit0 -x10725_bit0 -x20725_bit0 -x30725_bit0 -x40725_bit0 -x50725_bit0 -x60725_bit0 -x10825_bit0 -x20825_bit0 -x30825_bit0 -x40825_bit0 -x50825_bit0 -x60825_bit0 -x70825_bit0 -x10925_bit0 -x20925_bit0 -x30925_bit0 -x40925_bit0 -x50925_bit0 -x60925_bit0 -x70925_bit0 -x80925_bit0 x11025_bit0 -x21025_bit0 -x31025_bit0 -x41025_bit0 -x51025_bit0 -x61025_bit0 -x71025_bit0 -x81025_bit0 -x91025_bit0 -x10235_bit0 -x10335_bit0 x20335_bit0 -x10435_bit0 -x20435_bit0 -x30435_bit0 -x10535_bit0 -x20535_bit0 -x30535_bit0 -x40535_bit0 -x10635_bit0 -x20635_bit0 -x30635_bit0 -x40635_bit0 -x50635_bit0 -x10735_bit0 -x20735_bit0 -x30735_bit0 -x40735_bit0 -x50735_bit0 -x60735_bit0 -x10835_bit0 -x20835_bit0 -x30835_bit0 -x40835_bit0 -x50835_bit0 -x60835_bit0 -x70835_bit0 -x10935_bit0 -x20935_bit0 -x30935_bit0 -x40935_bit0 -x50935_bit0 -x60935_bit0 -x70935_bit0 -x80935_bit0 -x11035_bit0 -x21035_bit0 -x31035_bit0 -x41035_bit0 -x51035_bit0 -x61035_bit0 -x71035_bit0 -x81035_bit0 -x91035_bit0 -x10245_bit0 -x10345_bit0 -x20345_bit0 -x10445_bit0 -x20445_bit0 -x30445_bit0 -x10545_bit0 -x20545_bit0 -x30545_bit0 -x40545_bit0 -x10645_bit0 -x20645_bit0 -x30645_bit0 -x40645_bit0 -x50645_bit0 -x10745_bit0 -x20745_bit0 -x30745_bit0 -x40745_bit0 -x50745_bit0 -x60745_bit0 -x10845_bit0 -x20845_bit0 -x30845_bit0 -x40845_bit0 -x50845_bit0 -x60845_bit0 -x70845_bit0 -x10945_bit0 -x20945_bit0 -x30945_bit0 x40945_bit0 -x50945_bit0 -x60945_bit0 -x70945_bit0 -x80945_bit0 -x11045_bit0 -x21045_bit0 -x31045_bit0 -x41045_bit0 -x51045_bit0 -x61045_bit0 -x71045_bit0 -x81045_bit0 -x91045_bit0 -x10255_bit0 -x10355_bit0 -x20355_bit0 -x10455_bit0 -x20455_bit0 -x30455_bit0 -x10555_bit0 -x20555_bit0 -x30555_bit0 -x40555_bit0 -x10655_bit0 -x20655_bit0 -x30655_bit0 -x40655_bit0 -x50655_bit0 -x10755_bit0 -x20755_bit0 -x30755_bit0 -x40755_bit0 x50755_bit0 -x60755_bit0 -x10855_bit0 -x20855_bit0 -x30855_bit0 -x40855_bit0 -x50855_bit0 -x60855_bit0 -x70855_bit0 -x10955_bit0 -x20955_bit0 -x30955_bit0 -x40955_bit0 -x50955_bit0 -x60955_bit0 -x70955_bit0 -x80955_bit0 -x11055_bit0 -x21055_bit0 -x31055_bit0 -x41055_bit0 -x51055_bit0 -x61055_bit0 -x71055_bit0 -x81055_bit0 -x91055_bit0 -x10216_bit0 -x10316_bit0 -x20316_bit0 -x10416_bit0 -x20416_bit0 -x30416_bit0 -x10516_bit0 -x20516_bit0 x30516_bit0 -x40516_bit0 -x10616_bit0 -x20616_bit0 -x30616_bit0 -x40616_bit0 -x50616_bit0 -x10716_bit0 -x20716_bit0 -x30716_bit0 -x40716_bit0 -x50716_bit0 -x60716_bit0 -x10816_bit0 -x20816_bit0 -x30816_bit0 -x40816_bit0 -x50816_bit0 -x60816_bit0 -x70816_bit0 -x10916_bit0 -x20916_bit0 -x30916_bit0 -x40916_bit0 -x50916_bit0 -x60916_bit0 -x70916_bit0 -x80916_bit0 -x11016_bit0 -x21016_bit0 -x31016_bit0 -x41016_bit0 -x51016_bit0 -x61016_bit0 -x71016_bit0 -x81016_bit0 -x91016_bit0 -x10226_bit0 -x10326_bit0 -x20326_bit0 -x10426_bit0 -x20426_bit0 -x30426_bit0 -x10526_bit0 -x20526_bit0 -x30526_bit0 -x40526_bit0 -x10626_bit0 -x20626_bit0 -x30626_bit0 x40626_bit0 -x50626_bit0 -x10726_bit0 -x20726_bit0 -x30726_bit0 -x40726_bit0 -x50726_bit0 -x60726_bit0 -x10826_bit0 -x20826_bit0 -x30826_bit0 -x40826_bit0 -x50826_bit0 -x60826_bit0 -x70826_bit0 -x10926_bit0 -x20926_bit0 -x30926_bit0 -x40926_bit0 -x50926_bit0 -x60926_bit0 -x70926_bit0 -x80926_bit0 -x11026_bit0 -x21026_bit0 -x31026_bit0 -x41026_bit0 -x51026_bit0 -x61026_bit0 -x71026_bit0 -x81026_bit0 -x91026_bit0 -x10236_bit0 -x10336_bit0 -x20336_bit0 -x10436_bit0 -x20436_bit0 -x30436_bit0 -x10536_bit0 -x20536_bit0 -x30536_bit0 -x40536_bit0 -x10636_bit0 -x20636_bit0 -x30636_bit0 -x40636_bit0 -x50636_bit0 -x10736_bit0 -x20736_bit0 -x30736_bit0 -x40736_bit0 -x50736_bit0 -x60736_bit0 -x10836_bit0 -x20836_bit0 -x30836_bit0 -x40836_bit0 -x50836_bit0 -x60836_bit0 -x70836_bit0 -x10936_bit0 -x20936_bit0 -x30936_bit0 -x40936_bit0 -x50936_bit0 -x60936_bit0 x70936_bit0 -x80936_bit0 -x11036_bit0 -x21036_bit0 -x31036_bit0 -x41036_bit0 -x51036_bit0 -x61036_bit0 -x71036_bit0 -x81036_bit0 -x91036_bit0 -x10246_bit0 -x10346_bit0 -x20346_bit0 -x10446_bit0 -x20446_bit0 -x30446_bit0 -x10546_bit0 -x20546_bit0 -x30546_bit0 -x40546_bit0 -x10646_bit0 -x20646_bit0 -x30646_bit0 -x40646_bit0 -x50646_bit0 -x10746_bit0 -x20746_bit0 -x30746_bit0 -x40746_bit0 -x50746_bit0 -x60746_bit0 x10846_bit0 -x20846_bit0 -x30846_bit0 -x40846_bit0 -x50846_bit0 -x60846_bit0 -x70846_bit0 -x10946_bit0 -x20946_bit0 -x30946_bit0 -x40946_bit0 -x50946_bit0 -x60946_bit0 -x70946_bit0 -x80946_bit0 -x11046_bit0 -x21046_bit0 -x31046_bit0 -x41046_bit0 -x51046_bit0 -x61046_bit0 -x71046_bit0 -x81046_bit0 -x91046_bit0 -x10256_bit0 -x10356_bit0 -x20356_bit0 -x10456_bit0 -x20456_bit0 -x30456_bit0 -x10556_bit0 -x20556_bit0 -x30556_bit0 -x40556_bit0 -x10656_bit0 -x20656_bit0 -x30656_bit0 -x40656_bit0 -x50656_bit0 -x10756_bit0 -x20756_bit0 -x30756_bit0 -x40756_bit0 -x50756_bit0 -x60756_bit0 -x10856_bit0 -x20856_bit0 -x30856_bit0 -x40856_bit0 -x50856_bit0 -x60856_bit0 -x70856_bit0 -x10956_bit0 -x20956_bit0 -x30956_bit0 -x40956_bit0 -x50956_bit0 -x60956_bit0 -x70956_bit0 -x80956_bit0 -x11056_bit0 x21056_bit0 -x31056_bit0 -x41056_bit0 -x51056_bit0 -x61056_bit0 -x71056_bit0 -x81056_bit0 -x91056_bit0 -x10217_bit0 -x10317_bit0 -x20317_bit0 -x10417_bit0 -x20417_bit0 -x30417_bit0 -x10517_bit0 -x20517_bit0 -x30517_bit0 -x40517_bit0 -x10617_bit0 -x20617_bit0 -x30617_bit0 -x40617_bit0 -x50617_bit0 -x10717_bit0 -x20717_bit0 -x30717_bit0 -x40717_bit0 -x50717_bit0 -x60717_bit0 -x10817_bit0 -x20817_bit0 -x30817_bit0 -x40817_bit0 -x50817_bit0 -x60817_bit0 -x70817_bit0 -x10917_bit0 -x20917_bit0 -x30917_bit0 -x40917_bit0 -x50917_bit0 -x60917_bit0 -x70917_bit0 -x80917_bit0 -x11017_bit0 -x21017_bit0 -x31017_bit0 -x41017_bit0 -x51017_bit0 -x61017_bit0 x71017_bit0 -x81017_bit0 -x91017_bit0 -x10227_bit0 -x10327_bit0 -x20327_bit0 -x10427_bit0 -x20427_bit0 -x30427_bit0 -x10527_bit0 -x20527_bit0 -x30527_bit0 -x40527_bit0 -x10627_bit0 -x20627_bit0 -x30627_bit0 -x40627_bit0 -x50627_bit0 -x10727_bit0 -x20727_bit0 -x30727_bit0 -x40727_bit0 -x50727_bit0 -x60727_bit0 -x10827_bit0 -x20827_bit0 -x30827_bit0 -x40827_bit0 -x50827_bit0 -x60827_bit0 -x70827_bit0 -x10927_bit0 -x20927_bit0 x30927_bit0 -x40927_bit0 -x50927_bit0 -x60927_bit0 -x70927_bit0 -x80927_bit0 -x11027_bit0 -x21027_bit0 -x31027_bit0 -x41027_bit0 -x51027_bit0 -x61027_bit0 -x71027_bit0 -x81027_bit0 -x91027_bit0 -x10237_bit0 -x10337_bit0 -x20337_bit0 x10437_bit0 -x20437_bit0 -x30437_bit0 -x10537_bit0 -x20537_bit0 -x30537_bit0 -x40537_bit0 -x10637_bit0 -x20637_bit0 -x30637_bit0 -x40637_bit0 -x50637_bit0 -x10737_bit0 -x20737_bit0 -x30737_bit0 -x40737_bit0 -x50737_bit0 -x60737_bit0 -x10837_bit0 -x20837_bit0 -x30837_bit0 -x40837_bit0 -x50837_bit0 -x60837_bit0 -x70837_bit0 -x10937_bit0 -x20937_bit0 -x30937_bit0 -x40937_bit0 -x50937_bit0 -x60937_bit0 -x70937_bit0 -x80937_bit0 -x11037_bit0 -x21037_bit0 -x31037_bit0 -x41037_bit0 -x51037_bit0 -x61037_bit0 -x71037_bit0 -x81037_bit0 -x91037_bit0 -x10247_bit0 -x10347_bit0 -x20347_bit0 -x10447_bit0 -x20447_bit0 -x30447_bit0 -x10547_bit0 -x20547_bit0 -x30547_bit0 -x40547_bit0 -x10647_bit0 x20647_bit0 -x30647_bit0 -x40647_bit0 -x50647_bit0 -x10747_bit0 -x20747_bit0 -x30747_bit0 -x40747_bit0 -x50747_bit0 -x60747_bit0 -x10847_bit0 -x20847_bit0 -x30847_bit0 -x40847_bit0 -x50847_bit0 -x60847_bit0 -x70847_bit0 -x10947_bit0 -x20947_bit0 -x30947_bit0 -x40947_bit0 -x50947_bit0 -x60947_bit0 -x70947_bit0 -x80947_bit0 -x11047_bit0 -x21047_bit0 -x31047_bit0 -x41047_bit0 -x51047_bit0 -x61047_bit0 -x71047_bit0 -x81047_bit0 -x91047_bit0 -x10257_bit0 -x10357_bit0 -x20357_bit0 -x10457_bit0 -x20457_bit0 -x30457_bit0 -x10557_bit0 -x20557_bit0 -x30557_bit0 -x40557_bit0 -x10657_bit0 -x20657_bit0 -x30657_bit0 -x40657_bit0 -x50657_bit0 -x10757_bit0 -x20757_bit0 -x30757_bit0 -x40757_bit0 -x50757_bit0 -x60757_bit0 -x10857_bit0 -x20857_bit0 -x30857_bit0 -x40857_bit0 x50857_bit0 -x60857_bit0 -x70857_bit0 -x10957_bit0 -x20957_bit0 -x30957_bit0 -x40957_bit0 -x50957_bit0 -x60957_bit0 -x70957_bit0 -x80957_bit0 -x11057_bit0 -x21057_bit0 -x31057_bit0 -x41057_bit0 -x51057_bit0 -x61057_bit0 -x71057_bit0 -x81057_bit0 -x91057_bit0 -x10218_bit0 -x10318_bit0 -x20318_bit0 -x10418_bit0 -x20418_bit0 -x30418_bit0 -x10518_bit0 -x20518_bit0 -x30518_bit0 -x40518_bit0 -x10618_bit0 -x20618_bit0 -x30618_bit0 -x40618_bit0 -x50618_bit0 -x10718_bit0 -x20718_bit0 -x30718_bit0 -x40718_bit0 -x50718_bit0 -x60718_bit0 -x10818_bit0 -x20818_bit0 -x30818_bit0 -x40818_bit0 -x50818_bit0 -x60818_bit0 -x70818_bit0 -x10918_bit0 -x20918_bit0 -x30918_bit0 -x40918_bit0 -x50918_bit0 x60918_bit0 -x70918_bit0 -x80918_bit0 -x11018_bit0 -x21018_bit0 -x31018_bit0 -x41018_bit0 -x51018_bit0 -x61018_bit0 -x71018_bit0 -x81018_bit0 -x91018_bit0 -x10228_bit0 -x10328_bit0 -x20328_bit0 -x10428_bit0 -x20428_bit0 -x30428_bit0 -x10528_bit0 -x20528_bit0 -x30528_bit0 -x40528_bit0 -x10628_bit0 -x20628_bit0 -x30628_bit0 -x40628_bit0 -x50628_bit0 -x10728_bit0 -x20728_bit0 -x30728_bit0 -x40728_bit0 -x50728_bit0 -x60728_bit0 -x10828_bit0 x20828_bit0 -x30828_bit0 -x40828_bit0 -x50828_bit0 -x60828_bit0 -x70828_bit0 -x10928_bit0 -x20928_bit0 -x30928_bit0 -x40928_bit0 -x50928_bit0 -x60928_bit0 -x70928_bit0 -x80928_bit0 -x11028_bit0 -x21028_bit0 -x31028_bit0 -x41028_bit0 -x51028_bit0 -x61028_bit0 -x71028_bit0 -x81028_bit0 -x91028_bit0 -x10238_bit0 -x10338_bit0 -x20338_bit0 -x10438_bit0 -x20438_bit0 -x30438_bit0 -x10538_bit0 -x20538_bit0 -x30538_bit0 x40538_bit0 -x10638_bit0 -x20638_bit0 -x30638_bit0 -x40638_bit0 -x50638_bit0 -x10738_bit0 -x20738_bit0 -x30738_bit0 -x40738_bit0 -x50738_bit0 -x60738_bit0 -x10838_bit0 -x20838_bit0 -x30838_bit0 -x40838_bit0 -x50838_bit0 -x60838_bit0 -x70838_bit0 -x10938_bit0 -x20938_bit0 -x30938_bit0 -x40938_bit0 -x50938_bit0 -x60938_bit0 -x70938_bit0 -x80938_bit0 -x11038_bit0 -x21038_bit0 -x31038_bit0 -x41038_bit0 -x51038_bit0 -x61038_bit0 -x71038_bit0 -x81038_bit0 -x91038_bit0 -x10248_bit0 -x10348_bit0 -x20348_bit0 -x10448_bit0 -x20448_bit0 -x30448_bit0 -x10548_bit0 -x20548_bit0 -x30548_bit0 -x40548_bit0 -x10648_bit0 -x20648_bit0 -x30648_bit0 -x40648_bit0 -x50648_bit0 -x10748_bit0 -x20748_bit0 -x30748_bit0 -x40748_bit0 -x50748_bit0 -x60748_bit0 -x10848_bit0 -x20848_bit0 -x30848_bit0 -x40848_bit0 -x50848_bit0 -x60848_bit0 -x70848_bit0 -x10948_bit0 -x20948_bit0 -x30948_bit0 -x40948_bit0 -x50948_bit0 -x60948_bit0 -x70948_bit0 -x80948_bit0 -x11048_bit0 -x21048_bit0 x31048_bit0 -x41048_bit0 -x51048_bit0 -x61048_bit0 -x71048_bit0 -x81048_bit0 -x91048_bit0 -x10258_bit0 -x10358_bit0 -x20358_bit0 -x10458_bit0 -x20458_bit0 -x30458_bit0 -x10558_bit0 -x20558_bit0 -x30558_bit0 -x40558_bit0 -x10658_bit0 -x20658_bit0 -x30658_bit0 -x40658_bit0 -x50658_bit0 x10758_bit0 -x20758_bit0 -x30758_bit0 -x40758_bit0 -x50758_bit0 -x60758_bit0 -x10858_bit0 -x20858_bit0 -x30858_bit0 -x40858_bit0 -x50858_bit0 -x60858_bit0 -x70858_bit0 -x10958_bit0 -x20958_bit0 -x30958_bit0 -x40958_bit0 -x50958_bit0 -x60958_bit0 -x70958_bit0 -x80958_bit0 -x11058_bit0 -x21058_bit0 -x31058_bit0 -x41058_bit0 -x51058_bit0 -x61058_bit0 -x71058_bit0 -x81058_bit0 -x91058_bit0 -x10219_bit0 x10319_bit0 -x20319_bit0 -x10419_bit0 -x20419_bit0 -x30419_bit0 -x10519_bit0 -x20519_bit0 -x30519_bit0 -x40519_bit0 -x10619_bit0 -x20619_bit0 -x30619_bit0 -x40619_bit0 -x50619_bit0 -x10719_bit0 -x20719_bit0 -x30719_bit0 -x40719_bit0 -x50719_bit0 -x60719_bit0 -x10819_bit0 -x20819_bit0 -x30819_bit0 -x40819_bit0 -x50819_bit0 -x60819_bit0 -x70819_bit0 -x10919_bit0 -x20919_bit0 -x30919_bit0 -x40919_bit0 -x50919_bit0 -x60919_bit0 -x70919_bit0 -x80919_bit0 -x11019_bit0 -x21019_bit0 -x31019_bit0 -x41019_bit0 -x51019_bit0 -x61019_bit0 -x71019_bit0 -x81019_bit0 -x91019_bit0 -x10229_bit0 -x10329_bit0 -x20329_bit0 -x10429_bit0 -x20429_bit0 -x30429_bit0 -x10529_bit0 -x20529_bit0 -x30529_bit0 -x40529_bit0 -x10629_bit0 -x20629_bit0 -x30629_bit0 -x40629_bit0 -x50629_bit0 -x10729_bit0 -x20729_bit0 -x30729_bit0 -x40729_bit0 -x50729_bit0 x60729_bit0 -x10829_bit0 -x20829_bit0 -x30829_bit0 -x40829_bit0 -x50829_bit0 -x60829_bit0 -x70829_bit0 -x10929_bit0 -x20929_bit0 -x30929_bit0 -x40929_bit0 -x50929_bit0 -x60929_bit0 -x70929_bit0 -x80929_bit0 -x11029_bit0 -x21029_bit0 -x31029_bit0 -x41029_bit0 -x51029_bit0 -x61029_bit0 -x71029_bit0 -x81029_bit0 -x91029_bit0 -x10239_bit0 -x10339_bit0 -x20339_bit0 -x10439_bit0 -x20439_bit0 -x30439_bit0 -x10539_bit0 -x20539_bit0 -x30539_bit0 -x40539_bit0 -x10639_bit0 -x20639_bit0 -x30639_bit0 -x40639_bit0 -x50639_bit0 -x10739_bit0 -x20739_bit0 -x30739_bit0 -x40739_bit0 -x50739_bit0 -x60739_bit0 -x10839_bit0 -x20839_bit0 -x30839_bit0 -x40839_bit0 -x50839_bit0 -x60839_bit0 -x70839_bit0 -x10939_bit0 -x20939_bit0 -x30939_bit0 -x40939_bit0 -x50939_bit0 -x60939_bit0 -x70939_bit0 -x80939_bit0 -x11039_bit0 -x21039_bit0 -x31039_bit0 -x41039_bit0 -x51039_bit0 -x61039_bit0 -x71039_bit0 x81039_bit0 -x91039_bit0 -x10249_bit0 -x10349_bit0 -x20349_bit0 -x10449_bit0 -x20449_bit0 -x30449_bit0 -x10549_bit0 -x20549_bit0 -x30549_bit0 -x40549_bit0 -x10649_bit0 -x20649_bit0 -x30649_bit0 -x40649_bit0 -x50649_bit0 -x10749_bit0 -x20749_bit0 -#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.97 0.98 2/54 30504
Raw data (stat): 30504 (runsolver) R 30503 32461 32460 0 -1 64 1 0 0 0 0 0 0 0 19 0 1 0 485141558 1052672 97 4294967295 134512640 135381576 3221224432 3221219804 135024803 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 97 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.87 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 4671 0 0 0 986 12 0 0 25 0 1 0 485141558 20475904 4303 4294967295 134512640 134672761 3221224544 3221223680 134614756 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4999 4303 603 41 0 4958 0
vsize: 19996
[startup+20.0016 s]
Raw data (loadavg): 0.89 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 5635 0 0 0 1985 14 0 0 25 0 1 0 485141558 24432640 5267 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5965 5267 603 41 0 5924 0
vsize: 23860
[startup+30.0023 s]
Raw data (loadavg): 0.91 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 6667 0 0 0 2982 17 0 0 25 0 1 0 485141558 28647424 6299 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6994 6299 603 41 0 6953 0
vsize: 27976
[startup+40.0021 s]
Raw data (loadavg): 0.92 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 7742 0 0 0 3979 20 0 0 25 0 1 0 485141558 33116160 7374 4294967295 134512640 134672761 3221224544 3221223728 134615951 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8085 7374 603 41 0 8044 0
vsize: 32340
[startup+50.0019 s]
Raw data (loadavg): 0.93 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 15925 0 0 0 4961 38 0 0 25 0 1 0 485141558 59772928 13509 4294967295 134512640 134672761 3221224544 3221223680 134614685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14593 13509 603 41 0 14552 0
vsize: 58372
[startup+60.0022 s]
Raw data (loadavg): 0.94 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 16494 0 0 0 5960 40 0 0 25 0 1 0 485141558 62140416 14078 4294967295 134512640 134672761 3221224544 3221223648 134604257 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15171 14078 603 41 0 15130 0
vsize: 60684
[startup+70.0025 s]
Raw data (loadavg): 0.95 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 17136 0 0 0 6958 42 0 0 25 0 1 0 485141558 64770048 14720 4294967295 134512640 134672761 3221224544 3221223728 134615711 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15813 14720 603 41 0 15772 0
vsize: 63252
[startup+80.0033 s]
Raw data (loadavg): 0.96 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 17890 0 0 0 7957 43 0 0 25 0 1 0 485141558 67891200 15474 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16575 15474 603 41 0 16534 0
vsize: 66300
[startup+90.003 s]
Raw data (loadavg): 0.96 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 18767 0 0 0 8954 46 0 0 25 0 1 0 485141558 71434240 16351 4294967295 134512640 134672761 3221224544 3221223584 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17440 16351 603 41 0 17399 0
vsize: 69760
[startup+100.003 s]
Raw data (loadavg): 0.97 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 19488 0 0 0 9953 48 0 0 25 0 1 0 485141558 74473472 17072 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18182 17072 603 41 0 18141 0
vsize: 72728
[startup+110.004 s]
Raw data (loadavg): 0.97 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 20173 0 0 0 10951 49 0 0 25 0 1 0 485141558 77258752 17757 4294967295 134512640 134672761 3221224544 3221223744 134610644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18862 17757 603 41 0 18821 0
vsize: 75448
[startup+120.004 s]
Raw data (loadavg): 0.98 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 20814 0 0 0 11950 51 0 0 25 0 1 0 485141558 79888384 18398 4294967295 134512640 134672761 3221224544 3221223728 134615785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19504 18398 603 41 0 19463 0
vsize: 78016
[startup+130.005 s]
Raw data (loadavg): 0.98 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 21653 0 0 0 12949 52 0 0 25 0 1 0 485141558 83259392 19237 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20327 19237 603 41 0 20286 0
vsize: 81308
[startup+140.005 s]
Raw data (loadavg): 0.98 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 22632 0 0 0 13947 54 0 0 25 0 1 0 485141558 87236608 20216 4294967295 134512640 134672761 3221224544 3221223584 134613012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21298 20216 603 41 0 21257 0
vsize: 85192
[startup+150.006 s]
Raw data (loadavg): 0.98 0.97 0.98 3/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 23627 0 0 0 14944 57 0 0 25 0 1 0 485141558 91377664 21211 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22309 21211 603 41 0 22268 0
vsize: 89236
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 24394 0 0 0 15942 59 0 0 25 0 1 0 485141558 94494720 21978 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23070 21978 603 41 0 23029 0
vsize: 92280
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 25049 0 0 0 16940 61 0 0 25 0 1 0 485141558 97284096 22633 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23751 22633 603 41 0 23710 0
vsize: 95004
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 25726 0 0 0 17938 63 0 0 25 0 1 0 485141558 100040704 23310 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24424 23310 603 41 0 24383 0
vsize: 97696
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 26491 0 0 0 18937 65 0 0 25 0 1 0 485141558 103186432 24075 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25192 24075 603 41 0 25151 0
vsize: 100768
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 27054 0 0 0 19934 68 0 0 25 0 1 0 485141558 105541632 24638 4294967295 134512640 134672761 3221224544 3221223728 134615840 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25767 24638 603 41 0 25726 0
vsize: 103068
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 27717 0 0 0 20933 69 0 0 25 0 1 0 485141558 108154880 25301 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26405 25301 603 41 0 26364 0
vsize: 105620
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 28335 0 0 0 21931 71 0 0 25 0 1 0 485141558 110788608 25919 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27048 25919 603 41 0 27007 0
vsize: 108192
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 28740 0 0 0 22930 73 0 0 25 0 1 0 485141558 112361472 26324 4294967295 134512640 134672761 3221224544 3221223744 134610669 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27432 26324 603 41 0 27391 0
vsize: 109728
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 29293 0 0 0 23928 75 0 0 25 0 1 0 485141558 114712576 26877 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28006 26877 603 41 0 27965 0
vsize: 112024
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 29883 0 0 0 24927 76 0 0 25 0 1 0 485141558 117112832 27467 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28592 27467 603 41 0 28551 0
vsize: 114368
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 30687 0 0 0 25924 79 0 0 25 0 1 0 485141558 120397824 28271 4294967295 134512640 134672761 3221224544 3221223584 134614256 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29394 28271 603 41 0 29353 0
vsize: 117576
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 31520 0 0 0 26922 81 0 0 25 0 1 0 485141558 123817984 29104 4294967295 134512640 134672761 3221224544 3221223744 134610618 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30229 29104 603 41 0 30188 0
vsize: 120916
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 32426 0 0 0 27920 83 0 0 25 0 1 0 485141558 127438848 30010 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31113 30010 603 41 0 31072 0
vsize: 124452
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 33043 0 0 0 28918 86 0 0 25 0 1 0 485141558 129925120 30627 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31720 30627 603 41 0 31679 0
vsize: 126880
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 33749 0 0 0 29915 88 0 0 25 0 1 0 485141558 132820992 31333 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32427 31333 603 41 0 32386 0
vsize: 129708
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 34543 0 0 0 30914 90 0 0 25 0 1 0 485141558 136073216 32127 4294967295 134512640 134672761 3221224544 3221223680 134614753 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33221 32127 603 41 0 33180 0
vsize: 132884
[startup+320.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 35165 0 0 0 31912 92 0 0 25 0 1 0 485141558 138674176 32749 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33856 32749 603 41 0 33815 0
vsize: 135424
[startup+330.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 35761 0 0 0 32910 94 0 0 25 0 1 0 485141558 141033472 33345 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34432 33345 603 41 0 34391 0
vsize: 137728
[startup+340.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 36246 0 0 0 33909 95 0 0 25 0 1 0 485141558 143130624 33830 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34944 33830 603 41 0 34903 0
vsize: 139776
[startup+350.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 36945 0 0 0 34909 96 0 0 25 0 1 0 485141558 145899520 34529 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35620 34529 603 41 0 35579 0
vsize: 142480
[startup+360.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 37738 0 0 0 35908 97 0 0 25 0 1 0 485141558 149176320 35322 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36420 35322 603 41 0 36379 0
vsize: 145680
[startup+370.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 38296 0 0 0 36907 98 0 0 25 0 1 0 485141558 151408640 35880 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36965 35880 603 41 0 36924 0
vsize: 147860
[startup+380.022 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 38919 0 0 0 37905 100 0 0 25 0 1 0 485141558 154017792 36503 4294967295 134512640 134672761 3221224544 3221223584 134612851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37602 36503 603 41 0 37561 0
vsize: 150408
[startup+390.022 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 39657 0 0 0 38904 102 0 0 25 0 1 0 485141558 157040640 37241 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38340 37241 603 41 0 38299 0
vsize: 153360
[startup+400.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 40411 0 0 0 39902 104 0 0 25 0 1 0 485141558 160161792 37995 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39102 37995 603 41 0 39061 0
vsize: 156408
[startup+410.032 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 41133 0 0 0 40901 105 0 0 25 0 1 0 485141558 163028992 38717 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39802 38717 603 41 0 39761 0
vsize: 159208
[startup+420.032 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 41764 0 0 0 41899 108 0 0 25 0 1 0 485141558 165654528 39348 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40443 39348 603 41 0 40402 0
vsize: 161772
[startup+430.033 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 42520 0 0 0 42897 110 0 0 25 0 1 0 485141558 168787968 40104 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41208 40104 603 41 0 41167 0
vsize: 164832
[startup+440.033 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 43232 0 0 0 43897 111 0 0 25 0 1 0 485141558 171909120 40816 4294967295 134512640 134672761 3221224544 3221223680 134614696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41970 40816 603 41 0 41929 0
vsize: 167880
[startup+450.045 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 43899 0 0 0 44897 112 0 0 25 0 1 0 485141558 174637056 41483 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42636 41483 603 41 0 42595 0
vsize: 170544
[startup+460.045 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 44547 0 0 0 45896 113 0 0 25 0 1 0 485141558 177360896 42131 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43301 42131 603 41 0 43260 0
vsize: 173204
[startup+470.045 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 45219 0 0 0 46894 115 0 0 25 0 1 0 485141558 180092928 42803 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43968 42803 603 41 0 43927 0
vsize: 175872
[startup+480.053 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 45912 0 0 0 47894 117 0 0 25 0 1 0 485141558 182968320 43496 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44670 43496 603 41 0 44629 0
vsize: 178680
[startup+490.052 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 46531 0 0 0 48893 118 0 0 25 0 1 0 485141558 185434112 44115 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45272 44115 603 41 0 45231 0
vsize: 181088
[startup+500.059 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 47200 0 0 0 49892 119 0 0 25 0 1 0 485141558 188162048 44784 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45938 44784 603 41 0 45897 0
vsize: 183752
[startup+510.086 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 47771 0 0 0 50893 121 0 0 25 0 1 0 485141558 190513152 45355 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46512 45355 603 41 0 46471 0
vsize: 186048
[startup+520.104 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 48367 0 0 0 51894 123 0 0 25 0 1 0 485141558 193003520 45951 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47120 45951 603 41 0 47079 0
vsize: 188480
[startup+530.105 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 48761 0 0 0 52892 124 0 0 25 0 1 0 485141558 194596864 46345 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47509 46345 603 41 0 47468 0
vsize: 190036
[startup+540.105 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 49164 0 0 0 53891 125 0 0 25 0 1 0 485141558 196173824 46748 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47894 46748 603 41 0 47853 0
vsize: 191576
[startup+550.105 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 49669 0 0 0 54891 126 0 0 25 0 1 0 485141558 198266880 47253 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48405 47253 603 41 0 48364 0
vsize: 193620
[startup+560.106 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 50238 0 0 0 55890 127 0 0 25 0 1 0 485141558 200634368 47822 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48983 47822 603 41 0 48942 0
vsize: 195932
[startup+570.113 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 51021 0 0 0 56889 129 0 0 25 0 1 0 485141558 203759616 48605 4294967295 134512640 134672761 3221224544 3221223744 134610705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49746 48605 603 41 0 49705 0
vsize: 198984
[startup+580.122 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 51628 0 0 0 57888 130 0 0 25 0 1 0 485141558 206262272 49212 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50357 49212 603 41 0 50316 0
vsize: 201428
[startup+590.122 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 52367 0 0 0 58888 131 0 0 25 0 1 0 485141558 209248256 49951 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51086 49951 603 41 0 51045 0
vsize: 204344
[startup+600.122 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 53053 0 0 0 59886 133 0 0 25 0 1 0 485141558 212103168 50637 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51783 50637 603 41 0 51742 0
vsize: 207132
[startup+610.123 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54738 0 0 0 60880 137 0 0 25 0 1 0 485141558 214593536 51270 4294967295 134512640 134672761 3221224544 3221223800 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52391 51270 603 41 0 52350 0
vsize: 209564
[startup+620.123 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 61880 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+630.124 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 62880 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+640.124 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 63880 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+650.132 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 64881 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+660.132 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 65881 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+670.14 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 66882 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+680.245 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 67893 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+690.254 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 68894 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+700.254 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 69894 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+710.255 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 70894 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+720.255 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 71894 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+730.256 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 72895 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+740.256 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 73895 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+750.256 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 74895 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+760.265 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 75896 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+770.266 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 76896 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+780.266 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 77897 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+790.266 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 78897 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+800.266 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 79897 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+810.267 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 80897 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+820.271 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 81898 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+830.271 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 82898 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+840.272 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 83898 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615773 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+850.277 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 84899 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+860.279 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 85899 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+870.388 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 86910 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+880.394 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 87911 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134616008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+890.394 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 88911 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223696 134541817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+900.396 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 89912 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+910.401 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 90912 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+920.41 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 91913 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223584 134614266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+930.41 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 92914 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+940.411 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 93914 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+950.425 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 94915 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+960.426 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 95916 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223584 134612606 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+970.438 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 96917 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+980.442 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 97918 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223584 134612604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+990.467 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 98920 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+1000.47 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 99920 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+1010.47 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 100921 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+1020.47 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 101921 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+1030.47 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 102922 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+1040.47 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 103922 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+1050.5 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 30504
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 104924 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+1060.51 s]
Raw data (loadavg): 1.15 1.00 1.00 3/57 30544
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 105925 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+1070.61 s]
Raw data (loadavg): 1.20 1.02 1.00 4/54 30557
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 106936 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+1080.61 s]
Raw data (loadavg): 1.17 1.02 1.00 2/54 30557
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 107936 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223648 134604307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+1090.61 s]
Raw data (loadavg): 1.14 1.02 1.00 2/54 30557
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 108936 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+1100.61 s]
Raw data (loadavg): 1.12 1.02 1.00 2/54 30557
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 109936 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+1110.61 s]
Raw data (loadavg): 1.10 1.02 1.00 2/54 30557
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 110936 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+1120.61 s]
Raw data (loadavg): 1.08 1.01 1.00 2/54 30557
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 54945 0 0 0 111936 138 0 0 25 0 1 0 485141558 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+1130.62 s]
Raw data (loadavg): 1.07 1.01 1.00 2/54 30557
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 55186 0 0 0 112937 138 0 0 25 0 1 0 485141558 215961600 51606 4294967295 134512640 134672761 3221224544 3221223744 134610646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52725 51606 603 41 0 52684 0
vsize: 210900
[startup+1140.62 s]
Raw data (loadavg): 1.06 1.01 1.00 2/54 30559
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 55794 0 0 0 113936 139 0 0 25 0 1 0 485141558 218431488 52214 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53328 52214 603 41 0 53287 0
vsize: 213312
[startup+1150.62 s]
Raw data (loadavg): 1.05 1.01 1.00 2/54 30559
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 56412 0 0 0 114935 140 0 0 25 0 1 0 485141558 221052928 52832 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53968 52832 603 41 0 53927 0
vsize: 215872
[startup+1160.62 s]
Raw data (loadavg): 1.04 1.01 1.00 2/54 30559
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 57051 0 0 0 115933 142 0 0 25 0 1 0 485141558 223666176 53471 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54606 53471 603 41 0 54565 0
vsize: 218424
[startup+1170.62 s]
Raw data (loadavg): 1.04 1.01 1.00 2/54 30559
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 57581 0 0 0 116932 144 0 0 25 0 1 0 485141558 225759232 54001 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55117 54001 603 41 0 55076 0
vsize: 220468
[startup+1180.62 s]
Raw data (loadavg): 1.03 1.01 1.00 2/54 30559
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 58089 0 0 0 117931 145 0 0 25 0 1 0 485141558 227860480 54509 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55630 54509 603 41 0 55589 0
vsize: 222520
[startup+1190.62 s]
Raw data (loadavg): 1.02 1.01 1.00 2/54 30559
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 59064 0 0 0 118928 148 0 0 25 0 1 0 485141558 231878656 55484 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56611 55484 603 41 0 56570 0
vsize: 226444
[startup+1200.62 s]
Raw data (loadavg): 1.02 1.01 1.00 2/54 30559
Raw data (stat): 30504 (minisat+) R 30503 32461 32460 0 -1 0 60170 0 0 0 119926 150 0 0 25 0 1 0 485141558 236462080 56590 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57730 56590 603 41 0 57689 0
vsize: 230920
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.74 s]
Raw data (loadavg): 1.02 1.01 1.00 1/54 30559
Raw data (stat): 30504 (minisat+) Z 30503 32461 32460 0 -1 12 60171 0 0 0 119926 161 0 0 25 0 1 0 485141558 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.74
CPU time (s): 1200.88
CPU user time (s): 1199.27
CPU system time (s): 1.61275
CPU usage (%): 100.012
Max. virtual memory (Kb): 230920
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####