PB'05 competition: run trace

Some explanations

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

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

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.220
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        796044 kB
Buffers:         25688 kB
Cached:         193072 kB
SwapCached:        744 kB
Active:          73948 kB
Inactive:       146756 kB
HighTotal:      131008 kB
HighFree:        32200 kB
LowTotal:       903652 kB
LowFree:        763844 kB
SwapTotal:     2097892 kB
SwapFree:      2096220 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           4992 kB
Slab:            12408 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 14:54:40 (client local time) WITH STATUS 10 IN 1200.52 SECONDS
stats: 18146 7 1200.52 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: 44.4862 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.019 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.95 0.90 2/54 7960
Raw data (stat): 7960 (runsolver) R 7959 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 545848805 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.87 0.95 0.90 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 4647 0 0 0 986 12 0 0 25 0 1 0 545848805 20340736 4279 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4966 4279 603 41 0 4925 0
vsize: 19864
[startup+20.0011 s]
Raw data (loadavg): 0.89 0.95 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 5615 0 0 0 1983 15 0 0 25 0 1 0 545848805 24432640 5247 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5965 5247 603 41 0 5924 0
vsize: 23860
[startup+30.0006 s]
Raw data (loadavg): 0.91 0.95 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 6626 0 0 0 2981 18 0 0 25 0 1 0 545848805 28516352 6258 4294967295 134512640 134672761 3221224544 3221223552 134522549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6962 6258 603 41 0 6921 0
vsize: 27848
[startup+40.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 7671 0 0 0 3978 21 0 0 25 0 1 0 545848805 32854016 7303 4294967295 134512640 134672761 3221224544 3221223716 134615856 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8021 7303 603 41 0 7980 0
vsize: 32084
[startup+50.0009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 15887 0 0 0 4959 40 0 0 25 0 1 0 545848805 59637760 13471 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14560 13471 603 41 0 14519 0
vsize: 58240
[startup+60.0014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 16468 0 0 0 5957 42 0 0 25 0 1 0 545848805 62140416 14052 4294967295 134512640 134672761 3221224544 3221223584 134612601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15171 14053 603 41 0 15130 0
vsize: 60684
[startup+70.0017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 17018 0 0 0 6956 43 0 0 25 0 1 0 545848805 64380928 14602 4294967295 134512640 134672761 3221224544 3221223744 134610667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15718 14602 603 41 0 15677 0
vsize: 62872
[startup+80.0019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 17783 0 0 0 7955 45 0 0 25 0 1 0 545848805 67502080 15367 4294967295 134512640 134672761 3221224544 3221223648 134604307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16480 15367 603 41 0 16439 0
vsize: 65920
[startup+90.0022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 18720 0 0 0 8953 46 0 0 25 0 1 0 545848805 71303168 16304 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17408 16304 603 41 0 17367 0
vsize: 69632
[startup+100.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 19410 0 0 0 9952 48 0 0 25 0 1 0 545848805 74076160 16994 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18085 16994 603 41 0 18044 0
vsize: 72340
[startup+110.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 20109 0 0 0 10950 50 0 0 25 0 1 0 545848805 76992512 17693 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18797 17693 603 41 0 18756 0
vsize: 75188
[startup+120.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 20731 0 0 0 11948 52 0 0 25 0 1 0 545848805 79486976 18315 4294967295 134512640 134672761 3221224544 3221223728 134615585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19406 18315 603 41 0 19365 0
vsize: 77624
[startup+130.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 21583 0 0 0 12946 54 0 0 25 0 1 0 545848805 82980864 19167 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20259 19167 603 41 0 20218 0
vsize: 81036
[startup+140.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 22529 0 0 0 13944 57 0 0 25 0 1 0 545848805 86851584 20113 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21204 20113 603 41 0 21163 0
vsize: 84816
[startup+150.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 23539 0 0 0 14943 58 0 0 25 0 1 0 545848805 90988544 21123 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22214 21123 603 41 0 22173 0
vsize: 88856
[startup+160.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 24311 0 0 0 15941 60 0 0 25 0 1 0 545848805 94101504 21895 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22974 21895 603 41 0 22933 0
vsize: 91896
[startup+170.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 24957 0 0 0 16940 61 0 0 25 0 1 0 545848805 96886784 22541 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23654 22541 603 41 0 23613 0
vsize: 94616
[startup+180.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 25658 0 0 0 17939 63 0 0 25 0 1 0 545848805 99770368 23242 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24358 23242 603 41 0 24317 0
vsize: 97432
[startup+190.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 26415 0 0 0 18937 64 0 0 25 0 1 0 545848805 102920192 23999 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25127 23999 603 41 0 25086 0
vsize: 100508
[startup+200.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 26965 0 0 0 19936 66 0 0 25 0 1 0 545848805 105164800 24549 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25675 24549 603 41 0 25634 0
vsize: 102700
[startup+210.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 27615 0 0 0 20935 67 0 0 25 0 1 0 545848805 107761664 25199 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26309 25199 603 41 0 26268 0
vsize: 105236
[startup+220.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 28270 0 0 0 21934 68 0 0 25 0 1 0 545848805 110522368 25854 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26983 25854 603 41 0 26942 0
vsize: 107932
[startup+230.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 28671 0 0 0 22933 69 0 0 25 0 1 0 545848805 112099328 26255 4294967295 134512640 134672761 3221224544 3221223744 134610618 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27368 26255 603 41 0 27327 0
vsize: 109472
[startup+240.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 29195 0 0 0 23933 70 0 0 25 0 1 0 545848805 114192384 26779 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27879 26779 603 41 0 27838 0
vsize: 111516
[startup+250.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 29799 0 0 0 24931 72 0 0 25 0 1 0 545848805 116707328 27383 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28493 27383 603 41 0 28452 0
vsize: 113972
[startup+260.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 30549 0 0 0 25930 74 0 0 25 0 1 0 545848805 119746560 28133 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29235 28133 603 41 0 29194 0
vsize: 116940
[startup+270.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 31408 0 0 0 26928 76 0 0 25 0 1 0 545848805 123289600 28992 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30100 28992 603 41 0 30059 0
vsize: 120400
[startup+280.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 32285 0 0 0 27926 77 0 0 25 0 1 0 545848805 126910464 29869 4294967295 134512640 134672761 3221224544 3221223552 134522369 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30984 29869 603 41 0 30943 0
vsize: 123936
[startup+290.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 32931 0 0 0 28925 79 0 0 25 0 1 0 545848805 129523712 30515 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31622 30515 603 41 0 31581 0
vsize: 126488
[startup+300.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 33617 0 0 0 29923 81 0 0 25 0 1 0 545848805 132300800 31201 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32300 31201 603 41 0 32259 0
vsize: 129200
[startup+310.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 34361 0 0 0 30922 83 0 0 25 0 1 0 545848805 135434240 31945 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33065 31945 603 41 0 33024 0
vsize: 132260
[startup+320.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 35058 0 0 0 31921 84 0 0 25 0 1 0 545848805 138276864 32642 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33759 32642 603 41 0 33718 0
vsize: 135036
[startup+330.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 35661 0 0 0 32919 86 0 0 25 0 1 0 545848805 140644352 33245 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34337 33245 603 41 0 34296 0
vsize: 137348
[startup+340.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 36180 0 0 0 33919 86 0 0 25 0 1 0 545848805 142872576 33764 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34881 33764 603 41 0 34840 0
vsize: 139524
[startup+350.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 36844 0 0 0 34917 88 0 0 25 0 1 0 545848805 145502208 34428 4294967295 134512640 134672761 3221224544 3221223744 134610646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35523 34428 603 41 0 35482 0
vsize: 142092
[startup+360.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 37647 0 0 0 35916 90 0 0 25 0 1 0 545848805 148791296 35231 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36326 35231 603 41 0 36285 0
vsize: 145304
[startup+370.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 38228 0 0 0 36915 91 0 0 25 0 1 0 545848805 151142400 35812 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36900 35812 603 41 0 36859 0
vsize: 147600
[startup+380.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 38826 0 0 0 37914 92 0 0 25 0 1 0 545848805 153628672 36410 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37507 36410 603 41 0 37466 0
vsize: 150028
[startup+390.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 39556 0 0 0 38912 94 0 0 25 0 1 0 545848805 156651520 37140 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38245 37140 603 41 0 38204 0
vsize: 152980
[startup+400.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 40318 0 0 0 39910 96 0 0 25 0 1 0 545848805 159768576 37902 4294967295 134512640 134672761 3221224544 3221223744 134610675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39006 37902 603 41 0 38965 0
vsize: 156024
[startup+410.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 41061 0 0 0 40908 98 0 0 25 0 1 0 545848805 162766848 38645 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39738 38645 603 41 0 39697 0
vsize: 158952
[startup+420.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 41691 0 0 0 41907 99 0 0 25 0 1 0 545848805 165392384 39275 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40379 39275 603 41 0 40338 0
vsize: 161516
[startup+430.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 42455 0 0 0 42906 101 0 0 25 0 1 0 545848805 168521728 40039 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41143 40039 603 41 0 41102 0
vsize: 164572
[startup+440.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 43176 0 0 0 43904 103 0 0 25 0 1 0 545848805 171651072 40760 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41907 40760 603 41 0 41866 0
vsize: 167628
[startup+450.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 43846 0 0 0 44903 104 0 0 25 0 1 0 545848805 174379008 41430 4294967295 134512640 134672761 3221224544 3221223728 134615505 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42573 41430 603 41 0 42532 0
vsize: 170292
[startup+460.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 44493 0 0 0 45902 105 0 0 25 0 1 0 545848805 177098752 42077 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43237 42077 603 41 0 43196 0
vsize: 172948
[startup+470.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 45187 0 0 0 46901 106 0 0 25 0 1 0 545848805 179961856 42771 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43936 42771 603 41 0 43895 0
vsize: 175744
[startup+480.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 45881 0 0 0 47899 108 0 0 25 0 1 0 545848805 182837248 43465 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44638 43465 603 41 0 44597 0
vsize: 178552
[startup+490.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 46514 0 0 0 48898 110 0 0 25 0 1 0 545848805 185434112 44098 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45272 44098 603 41 0 45231 0
vsize: 181088
[startup+500.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 47175 0 0 0 49896 112 0 0 25 0 1 0 545848805 188035072 44759 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45907 44759 603 41 0 45866 0
vsize: 183628
[startup+510.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 47759 0 0 0 50896 113 0 0 25 0 1 0 545848805 190513152 45343 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46512 45343 603 41 0 46471 0
vsize: 186048
[startup+520.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 48355 0 0 0 51895 114 0 0 25 0 1 0 545848805 192872448 45939 4294967295 134512640 134672761 3221224544 3221223716 134615856 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47088 45939 603 41 0 47047 0
vsize: 188352
[startup+530.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 48753 0 0 0 52894 115 0 0 25 0 1 0 545848805 194465792 46337 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47477 46337 603 41 0 47436 0
vsize: 189908
[startup+540.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 49164 0 0 0 53894 116 0 0 25 0 1 0 545848805 196173824 46748 4294967295 134512640 134672761 3221224544 3221223680 134614551 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.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 49673 0 0 0 54894 116 0 0 25 0 1 0 545848805 198266880 47257 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48405 47257 603 41 0 48364 0
vsize: 193620
[startup+560.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 50250 0 0 0 55894 118 0 0 25 0 1 0 545848805 200634368 47834 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48983 47834 603 41 0 48942 0
vsize: 195932
[startup+570.032 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 51037 0 0 0 56892 120 0 0 25 0 1 0 545848805 203890688 48621 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49778 48621 603 41 0 49737 0
vsize: 199112
[startup+580.035 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 51652 0 0 0 57891 122 0 0 25 0 1 0 545848805 206393344 49236 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50389 49236 603 41 0 50348 0
vsize: 201556
[startup+590.038 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 52411 0 0 0 58889 124 0 0 25 0 1 0 545848805 209506304 49995 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51149 49995 603 41 0 51108 0
vsize: 204596
[startup+600.038 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 53093 0 0 0 59887 126 0 0 25 0 1 0 545848805 212234240 50677 4294967295 134512640 134672761 3221224544 3221223552 134522549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51815 50677 603 41 0 51774 0
vsize: 207260
[startup+610.038 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54738 0 0 0 60883 130 0 0 25 0 1 0 545848805 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.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 61882 130 0 0 25 0 1 0 545848805 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52472 51365 603 41 0 52431 0
vsize: 209888
[startup+630.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 62882 130 0 0 25 0 1 0 545848805 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615526 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.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 63882 130 0 0 25 0 1 0 545848805 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+650.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 64882 130 0 0 25 0 1 0 545848805 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+660.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 65883 130 0 0 25 0 1 0 545848805 214925312 51365 4294967295 134512640 134672761 3221224544 3221223680 134614825 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.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 66883 130 0 0 25 0 1 0 545848805 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.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 67883 130 0 0 25 0 1 0 545848805 214925312 51365 4294967295 134512640 134672761 3221224544 3221223680 134614701 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.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 68883 130 0 0 25 0 1 0 545848805 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615929 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.041 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 69883 130 0 0 25 0 1 0 545848805 214925312 51365 4294967295 134512640 134672761 3221224544 3221223744 134610686 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.041 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 70884 130 0 0 25 0 1 0 545848805 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+720.041 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 71884 130 0 0 25 0 1 0 545848805 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+730.041 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 72884 130 0 0 25 0 1 0 545848805 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+740.041 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 73884 130 0 0 25 0 1 0 545848805 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+750.041 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 74884 130 0 0 25 0 1 0 545848805 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615673 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.041 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 75885 130 0 0 25 0 1 0 545848805 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+770.042 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 76885 130 0 0 25 0 1 0 545848805 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615554 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.042 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 77885 130 0 0 25 0 1 0 545848805 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615583 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.042 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 78885 130 0 0 25 0 1 0 545848805 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+800.042 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 79885 130 0 0 25 0 1 0 545848805 214925312 51365 4294967295 134512640 134672761 3221224544 3221223584 134612696 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.043 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 80886 130 0 0 25 0 1 0 545848805 214925312 51365 4294967295 134512640 134672761 3221224544 3221223680 134614699 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.042 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 81886 130 0 0 25 0 1 0 545848805 214925312 51365 4294967295 134512640 134672761 3221224544 3221223712 134615859 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.042 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 82886 130 0 0 25 0 1 0 545848805 214925312 51365 4294967295 134512640 134672761 3221224544 3221223744 134610646 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.042 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 83886 130 0 0 25 0 1 0 545848805 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615833 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.042 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 84886 130 0 0 25 0 1 0 545848805 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615739 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.043 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 85887 130 0 0 25 0 1 0 545848805 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.044 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 86887 130 0 0 25 0 1 0 545848805 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+880.043 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 87887 130 0 0 25 0 1 0 545848805 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+890.043 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 88887 130 0 0 25 0 1 0 545848805 214925312 51365 4294967295 134512640 134672761 3221224544 3221223744 134610709 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.043 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 89887 130 0 0 25 0 1 0 545848805 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615833 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.043 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 90888 130 0 0 25 0 1 0 545848805 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.043 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 91888 130 0 0 25 0 1 0 545848805 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615711 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.043 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 92888 130 0 0 25 0 1 0 545848805 214925312 51365 4294967295 134512640 134672761 3221224544 3221223744 134610618 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.043 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 93888 130 0 0 25 0 1 0 545848805 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+950.043 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 94888 130 0 0 25 0 1 0 545848805 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615671 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.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 95889 130 0 0 25 0 1 0 545848805 214925312 51365 4294967295 134512640 134672761 3221224544 3221223744 134610646 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.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 96889 131 0 0 25 0 1 0 545848805 214925312 51365 4294967295 134512640 134672761 3221224544 3221223584 134613112 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.056 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 97890 131 0 0 25 0 1 0 545848805 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+990.056 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 98890 131 0 0 25 0 1 0 545848805 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615720 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.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 99890 131 0 0 25 0 1 0 545848805 214925312 51365 4294967295 134512640 134672761 3221224544 3221223744 134610697 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.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 100891 131 0 0 25 0 1 0 545848805 214925312 51365 4294967295 134512640 134672761 3221224544 3221223744 134610675 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.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 101891 131 0 0 25 0 1 0 545848805 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+1030.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 102891 131 0 0 25 0 1 0 545848805 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+1040.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 103892 131 0 0 25 0 1 0 545848805 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+1050.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 104892 131 0 0 25 0 1 0 545848805 214925312 51365 4294967295 134512640 134672761 3221224544 3221223680 134614690 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.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 105892 131 0 0 25 0 1 0 545848805 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615747 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.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 106893 131 0 0 25 0 1 0 545848805 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+1080.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 107893 131 0 0 25 0 1 0 545848805 214925312 51365 4294967295 134512640 134672761 3221224544 3221223744 134610686 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.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 108893 131 0 0 25 0 1 0 545848805 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+1100.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 109894 131 0 0 25 0 1 0 545848805 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+1110.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 110895 131 0 0 25 0 1 0 545848805 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+1120.19 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 54945 0 0 0 111906 131 0 0 25 0 1 0 545848805 214925312 51365 4294967295 134512640 134672761 3221224544 3221223728 134615833 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.19 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 55483 0 0 0 112905 132 0 0 25 0 1 0 545848805 217260032 51903 4294967295 134512640 134672761 3221224544 3221223744 134610667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53042 51903 603 41 0 53001 0
vsize: 212168
[startup+1140.2 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 56095 0 0 0 113905 133 0 0 25 0 1 0 545848805 219742208 52515 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53648 52515 603 41 0 53607 0
vsize: 214592
[startup+1150.2 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 56760 0 0 0 114903 135 0 0 25 0 1 0 545848805 222486528 53180 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54318 53180 603 41 0 54277 0
vsize: 217272
[startup+1160.2 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 57378 0 0 0 115902 137 0 0 25 0 1 0 545848805 224972800 53798 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54925 53798 603 41 0 54884 0
vsize: 219700
[startup+1170.2 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 57762 0 0 0 116901 138 0 0 25 0 1 0 545848805 226549760 54182 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55310 54182 603 41 0 55269 0
vsize: 221240
[startup+1180.2 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 58634 0 0 0 117900 139 0 0 25 0 1 0 545848805 230174720 55054 4294967295 134512640 134672761 3221224544 3221223552 134522549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56195 55054 603 41 0 56154 0
vsize: 224780
[startup+1190.2 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 59697 0 0 0 118899 141 0 0 25 0 1 0 545848805 234414080 56117 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57230 56117 603 41 0 57189 0
vsize: 228920
[startup+1200.2 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 7960
Raw data (stat): 7960 (minisat+) R 7959 28099 28098 0 -1 0 60709 0 0 0 119896 143 0 0 25 0 1 0 545848805 238661632 57129 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58267 57129 603 41 0 58226 0
vsize: 233068
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.32 s]
Raw data (loadavg): 1.00 0.97 0.91 1/54 7960
Raw data (stat): 7960 (minisat+) Z 7959 28099 28098 0 -1 12 60710 0 0 0 119896 154 0 0 25 0 1 0 545848805 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.32
CPU time (s): 1200.52
CPU user time (s): 1198.97
CPU system time (s): 1.54676
CPU usage (%): 100.016
Max. virtual memory (Kb): 233068
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####