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/miplib/normalized-mps-v2-13-7-misc05.opb
MD5SUM	4f7891bf040f9fa135208e1a9808a8bc
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1430464
Optimality of the best value was proved	NO
Number of terms in the objective function	21
Biggest coefficient in the objective function	1048576
Number of bits for the biggest coefficient in the objective function	21
Sum of the numbers in the objective function	2097151
Number of bits of the sum of numbers in the objective function	21
Biggest number in a constraint	5242880
Number of bits of the biggest number in a constraint	23
Biggest sum of numbers in a constraint	81788220
Number of bits of the biggest sum of numbers	27
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	6.00309
Number of variables	1320
Total number of constraints	374
Number of constraints which are clauses	155
Number of constraints which are cardinality constraints (but not clauses)	82
Number of constraints which are nor clauses,nor cardinality constraints	137
Minimum length of a constraint	1
Maximum length of a constraint	301
Trace number 19121

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-04-21 18:03:11 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16989 boxname=wulflinc20 idbench=1307 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4f7891bf040f9fa135208e1a9808a8bc  /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-misc05.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-misc05.opb /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-misc05.opb
IDLAUNCH: 16989
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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.215
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:        685312 kB
Buffers:         21744 kB
Cached:         304616 kB
SwapCached:        516 kB
Active:          15504 kB
Inactive:       312812 kB
HighTotal:      131008 kB
HighFree:        98812 kB
LowTotal:       903652 kB
LowFree:        586500 kB
SwapTotal:     2097892 kB
SwapFree:      2096480 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5116 kB
Slab:            15468 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 18:20:20 (client local time) WITH STATUS 30 IN 1028.43 SECONDS
stats: 16989 0 1028.43 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 327 PB-constraints to clauses...
c   -- Unit propagations: ppppppppppp
c   -- Detecting intervals from adjacent constraints: ############################
c   -- Clauses(.)/Splits(s): ...............................................................................................................................ssssssssssssssssssssssss
c ---[ 349]---> Sorter-cost:  471     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 345]---> Adder-cost: 718   maxlim: 5243515   bits: 24/23
c ---[ 343]---> Sorter-cost: 4443     Base: 2 2 2 2 2 2 3 5 2 2 2 17 2
c ---[ 341]---> BDD-cost:   13
c ---[ 339]---> BDD-cost:   13
c ---[ 337]---> BDD-cost:   13
c ---[ 335]---> BDD-cost:   11
c ---[ 333]---> BDD-cost:   13
c ---[ 331]---> BDD-cost:   13
c ---[ 329]---> BDD-cost:   13
c ---[ 200]---> Sorter-cost:  118     Base:
c ---[ 198]---> Sorter-cost:  127     Base:
c ---[ 196]---> Sorter-cost:  126     Base:
c ---[ 194]---> Sorter-cost:  119     Base:
c ---[ 192]---> Sorter-cost:  126     Base:
c ---[ 190]---> Sorter-cost:  123     Base:
c ---[ 188]---> Sorter-cost:  126     Base:
c ---[ 186]---> Sorter-cost:  127     Base:
c ---[ 184]---> Sorter-cost:  127     Base:
c ---[ 182]---> Adder-cost: 371   maxlim: 235002   bits: 19/18
c ---[ 180]---> Adder-cost: 414   maxlim: 398330   bits: 20/19
c ---[ 178]---> Adder-cost: 414   maxlim: 418810   bits: 20/19
c ---[ 176]---> Adder-cost: 371   maxlim: 195835   bits: 19/18
c ---[ 174]---> Adder-cost: 414   maxlim: 400890   bits: 20/19
c ---[ 172]---> Adder-cost: 414   maxlim: 397050   bits: 20/19
c ---[ 170]---> Adder-cost: 414   maxlim: 416250   bits: 20/19
c ---[ 168]---> BDD-cost:   72
c ---[ 166]---> BDD-cost:   72
c ---[ 165]---> Sorter-cost: 1614     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 164]---> Sorter-cost: 1614     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 135]---> BDD-cost:   98
c ---[ 134]---> BDD-cost:   20
c ---[ 133]---> BDD-cost:   20
c ---[ 132]---> BDD-cost:   20
c ---[ 131]---> BDD-cost:   20
c ---[ 130]---> BDD-cost:   20
c ---[ 129]---> BDD-cost:   20
c ---[ 128]---> BDD-cost:   23
c ---[ 127]---> BDD-cost:   23
c ---[ 126]---> BDD-cost:   23
c ---[ 125]---> BDD-cost:   23
c ---[ 124]---> BDD-cost:   23
c ---[ 123]---> BDD-cost:   23
c ---[ 122]---> BDD-cost:   23
c ---[ 121]---> BDD-cost:   23
c ---[ 120]---> BDD-cost:   23
c ---[ 119]---> BDD-cost:   23
c ---[ 118]---> BDD-cost:   23
c ---[ 117]---> BDD-cost:   23
c ---[ 115]---> BDD-cost:   22
c ---[ 114]---> BDD-cost:   22
c ---[ 113]---> BDD-cost:   22
c ---[ 112]---> BDD-cost:   22
c ---[ 111]---> BDD-cost:   22
c ---[ 110]---> BDD-cost:   22
c ---[ 109]---> BDD-cost:   22
c ---[ 108]---> BDD-cost:   22
c ---[ 107]---> BDD-cost:   22
c ---[ 106]---> BDD-cost:   22
c ---[ 105]---> BDD-cost:   22
c ---[ 104]---> BDD-cost:   24
c ---[ 103]---> BDD-cost:   24
c ---[ 102]---> BDD-cost:   24
c ---[ 101]---> BDD-cost:   24
c ---[ 100]---> BDD-cost:   24
c ---[  99]---> BDD-cost:   24
c ---[  98]---> BDD-cost:   19
c ---[  97]---> BDD-cost:   19
c ---[  96]---> BDD-cost:   19
c ---[  95]---> BDD-cost:   19
c ---[  94]---> BDD-cost:   19
c ---[  93]---> BDD-cost:   19
c ---[  92]---> BDD-cost:   23
c ---[  91]---> BDD-cost:   23
c ---[  90]---> BDD-cost:   23
c ---[  89]---> BDD-cost:   23
c ---[  88]---> BDD-cost:   23
c ---[  87]---> BDD-cost:   23
c ---[  86]---> BDD-cost:   23
c ---[  85]---> BDD-cost:   23
c ---[  84]---> BDD-cost:   23
c ---[  83]---> BDD-cost:   23
c ---[  82]---> BDD-cost:   23
c ---[  81]---> BDD-cost:   23
c ---[  80]---> BDD-cost:   23
c ---[  79]---> BDD-cost:   23
c ---[  77]---> BDD-cost:    5
c ---[  76]---> BDD-cost:    7
c ---[  73]---> BDD-cost:    6
c ---[  72]---> BDD-cost:    7
c ---[  71]---> BDD-cost:    6
c ---[  70]---> BDD-cost:    8
c ---[  67]---> BDD-cost:    7
c ---[  66]---> BDD-cost:    7
c ---[  64]---> BDD-cost:    8
c ---[  61]---> BDD-cost:    7
c ---[  59]---> BDD-cost:    5
c ---[  56]---> BDD-cost:    6
c ---[  55]---> BDD-cost:    7
c ---[  53]---> BDD-cost:    6
c ---[  52]---> BDD-cost:    8
c ---[  50]---> BDD-cost:    7
c ---[  49]---> BDD-cost:    7
c ---[  47]---> BDD-cost:    6
c ---[  46]---> BDD-cost:    8
c ---[  44]---> BDD-cost:    7
c ---[  43]---> BDD-cost:    7
c ---[  41]---> BDD-cost:    6
c ---[  40]---> BDD-cost:    8
c ---[  37]---> BDD-cost:    7
c ---[  35]---> BDD-cost:    6
c ---[  34]---> BDD-cost:    8
c ---[  31]---> BDD-cost:    7
c ---[  30]---> BDD-cost:    7
c ---[  28]---> BDD-cost:    6
c ---[  27]---> BDD-cost:    8
c ---[  24]---> BDD-cost:    7
c ---[  23]---> BDD-cost:    3
c ---[  22]---> BDD-cost:    4
c ---[  21]---> BDD-cost:    4
c ---[  20]---> BDD-cost:    4
c ---[  19]---> BDD-cost:    4
c ---[  18]---> BDD-cost:    3
c ---[  17]---> BDD-cost:    4
c ---[  16]---> BDD-cost:    4
c ---[  15]---> BDD-cost:    3
c ---[  14]---> BDD-cost:    4
c ---[  13]---> BDD-cost:    4
c ---[  12]---> BDD-cost:    3
c ---[  11]---> BDD-cost:    4
c ---[  10]---> BDD-cost:    3
c ---[   9]---> BDD-cost:    4
c ---[   8]---> BDD-cost:    3
c ---[   7]---> BDD-cost:    4
c ---[   6]---> BDD-cost:    4
c ---[   5]---> BDD-cost:    3
c ---[   4]---> BDD-cost:    4
c ---[   3]---> BDD-cost:    4
c ---[   2]---> BDD-cost:    3
c ---[   1]---> BDD-cost:    4
c ---[   0]---> BDD-cost:    4
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   50230   151151 |   15068       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/12572          
c   -- var.elim.:  2000/12572          
c   -- var.elim.:  3000/12572          
c   -- var.elim.:  4000/12572          
c   -- var.elim.:  5000/12572          
c   -- var.elim.:  6000/12572          
c   -- var.elim.:  7000/12572          
c   -- var.elim.:  8000/12572          
c   -- var.elim.:  9000/12572          
c   -- var.elim.:  10000/12572          
c   -- var.elim.:  11000/12572          
c   -- var.elim.:  12000/12572          
c   -- var.elim.:  12572/12572          
c   -- var.elim.:  1000/5065          
c   -- var.elim.:  2000/5065          
c   -- var.elim.:  3000/5065          
c   -- var.elim.:  4000/5065          
c   -- var.elim.:  5000/5065          
c   -- var.elim.:  5065/5065          
c   -- var.elim.:  63/63          
c   -- var.elim.:  20/20          
c   -- var.elim.:  10/10          
c   -- var.elim.:  5/5          
c   -- subsuming                       
c   -- var.elim.:  857/857          
c   -- var.elim.:  746/746          
c   -- var.elim.:  540/540          
c   -- var.elim.:  203/203          
c   -- var.elim.:  7/7          
c   -- var.elim.:  5/5          
c   -- subsuming                       
c   -- var.elim.:  278/278          
c   -- var.elim.:  203/203          
c   -- var.elim.:  62/62          
c   -- subsuming                       
c   -- var.elim.:  124/124          
c   -- var.elim.:  33/33          
c   -- var.elim.:  11/11          
c |         0 |   43932   145479 |      --       0       --      -- |     --   | -4876/903
c |         0 |   43932   145479 |   17572       0        0     nan |  0.000 % |
c |       100 |   43932   145479 |   19330     100     7553    75.5 | 11.641 % |
c |       250 |   43918   145420 |   21256     248    21743    87.7 | 11.651 % |
c |       475 |   43890   145302 |   23367     468    24692    52.8 | 11.673 % |
c |       812 |   43890   145302 |   25703     805    38354    47.6 | 11.673 % |
c |      1318 |   43890   145302 |   28274    1311    48923    37.3 | 11.673 % |
c |      2077 |   43832   145101 |   31060    2066    73875    35.8 | 11.758 % |
c ==============================================================================
c (current CPU-time: 3.64744 s)
c ==============================================================================
c [1mFound solution: 1468288[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   13
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2264 |   43844   145133 |   13153    2253    79749    35.4 | 11.758 % |
c   -- subsuming                       
c   -- var.elim.:  100/100          
c   -- var.elim.:  67/67          
c   -- var.elim.:  23/23          
c |      2264 |   43815   145084 |      --    2253       --      -- |     --   | -29/-48
c |      2264 |   43815   145084 |   17526    2104    57169    27.2 | 11.758 % |
c |      2364 |   43815   145084 |   19278    2204    59457    27.0 | 11.795 % |
c |      2515 |   43769   144922 |   21184    2309    60197    26.1 | 11.870 % |
c ==============================================================================
c (current CPU-time: 4.24235 s)
c ==============================================================================
c [1mFound solution: 1460736[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2695 |   43765   144887 |   13129    2486    66466    26.7 | 11.870 % |
c   -- subsuming                       
c   -- var.elim.:  121/121          
c   -- var.elim.:  41/41          
c   -- var.elim.:  74/74          
c   -- var.elim.:  33/33          
c |      2695 |   43687   144631 |      --    2486       --      -- |     --   | -78/-255
c |      2695 |   43687   144631 |   17474    2486    66466    26.7 | 11.870 % |
c ==============================================================================
c (current CPU-time: 4.46232 s)
c ==============================================================================
c [1mFound solution: 1458688[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   10
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2710 |   43701   144663 |   13110    2501    69078    27.6 | 11.870 % |
c   -- subsuming                       
c   -- var.elim.:  27/27          
c   -- var.elim.:  12/12          
c |      2710 |   43687   144627 |      --    2501       --      -- |     --   | -14/-35
c |      2710 |   43687   144627 |   17474    2500    69076    27.6 | 11.870 % |
c |      2810 |   43687   144627 |   19222    2600    78719    30.3 | 11.995 % |
c |      2960 |   43687   144627 |   21144    2750   103424    37.6 | 11.995 % |
c |      3185 |   42557   140921 |   22657    2959   107841    36.4 | 13.811 % |
c ==============================================================================
c (current CPU-time: 5.34019 s)
c ==============================================================================
c [1mFound solution: 1449600[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   13
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      3202 |   42569   140952 |   12770    2976   108742    36.5 | 13.811 % |
c   -- subsuming                       
c   -- var.elim.:  569/569          
c   -- var.elim.:  269/269          
c   -- var.elim.:  10/10          
c   -- subsuming                       
c   -- var.elim.:  22/22          
c   -- var.elim.:  25/25          
c |      3202 |   42478   140885 |      --    2976       --      -- |     --   | -91/-66
c |      3202 |   42478   140885 |   16991    2848    84733    29.8 | 13.811 % |
c |      3302 |   42417   140659 |   18663    2947    90603    30.7 | 13.983 % |
c |      3452 |   42417   140659 |   20529    3097    95972    31.0 | 13.983 % |
c |      3677 |   42417   140659 |   22582    3322   105822    31.9 | 13.983 % |
c |      4014 |   42417   140659 |   24841    3659   149954    41.0 | 13.983 % |
c |      4520 |   42300   140230 |   27249    4161   228626    54.9 | 14.145 % |
c ==============================================================================
c (current CPU-time: 8.41472 s)
c ==============================================================================
c [1mFound solution: 1434304[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   14
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4677 |   42297   140202 |   12689    4294   237298    55.3 | 14.145 % |
c   -- subsuming                       
c   -- var.elim.:  232/232          
c   -- var.elim.:  116/116          
c   -- var.elim.:  9/9          
c   -- subsuming                       
c   -- var.elim.:  38/38          
c   -- var.elim.:  12/12          
c |      4677 |   42201   139962 |      --    4294       --      -- |     --   | -96/-239
c |      4677 |   42201   139962 |   16880    4195   218272    52.0 | 14.145 % |
c |      4777 |   42062   139500 |   18507    4293   222006    51.7 | 14.458 % |
c |      4928 |   41632   138052 |   20149    4404   237169    53.9 | 15.158 % |
c |      5154 |   41615   137990 |   22155    4628   246582    53.3 | 15.180 % |
c |      5491 |   41582   137857 |   24352    4961   254950    51.4 | 15.212 % |
c |      5998 |   41568   137798 |   26778    5467   270856    49.5 | 15.223 % |
c |      6758 |   41568   137798 |   29456    6227   329443    52.9 | 15.223 % |
c |      7897 |   41546   137713 |   32384    7357   386179    52.5 | 15.245 % |
c |      9605 |   41509   137589 |   35591    9056   757717    83.7 | 15.320 % |
c |     12167 |   41447   137359 |   39091   11609  1627586   140.2 | 15.395 % |
c |     16014 |   41405   137182 |   42957   15444  2551827   165.2 | 15.428 % |
c ==============================================================================
c (current CPU-time: 48.6316 s)
c ==============================================================================
c [1mFound solution: 1430464[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   13
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     21241 |   41370   137014 |   12410   20658  4049133   196.0 | 15.428 % |
c   -- subsuming                       
c   -- var.elim.:  571/571          
c   -- var.elim.:  267/267          
c   -- var.elim.:  22/22          
c   -- subsuming                       
c   -- var.elim.:  18/18          
c   -- var.elim.:  13/13          
c |     21241 |   41259   136829 |      --   20658       --      -- |     --   | -111/-184
c |     21241 |   41259   136829 |   16503   13550   778514    57.5 | 15.428 % |
c |     21341 |   41259   136829 |   18153   13650   787484    57.7 | 15.614 % |
c |     21491 |   41259   136829 |   19969   13800   845944    61.3 | 15.614 % |
c |     21716 |   41259   136829 |   21966   14025   924935    65.9 | 15.614 % |
c |     22059 |   41259   136829 |   24162   14368   957833    66.7 | 15.614 % |
c |     22566 |   41259   136829 |   26579   14875  1016471    68.3 | 15.614 % |
c |     23326 |   41259   136829 |   29237   15635  1285597    82.2 | 15.614 % |
c |     24466 |   41259   136829 |   32160   16775  1416124    84.4 | 15.614 % |
c |     26174 |   41259   136829 |   35376   18483  1579792    85.5 | 15.614 % |
c |     28737 |   41218   136646 |   38875   21002  1906828    90.8 | 15.657 % |
c |     32581 |   41134   136333 |   42676   24839  4071089   163.9 | 15.755 % |
c |     38348 |   41092   136168 |   46896   30596  6529756   213.4 | 15.809 % |
c |     46998 |   40958   135626 |   51417   39176 10780063   275.2 | 15.950 % |
c |     59973 |   40706   134771 |   56211   52131 19087926   366.2 | 16.318 % |
c |     79434 |   40466   133868 |   61467   36593 16899698   461.8 | 16.643 % |
c |    108626 |   40368   133483 |   67450   28321 10382829   366.6 | 16.784 % |
c |    152415 |   40327   133320 |   74120   30951  9570614   309.2 | 16.827 % |
c ==============================================================================
c [1mOptimal solution: 1430464[0m
s OPTIMUM FOUND
v -COL133_bit_7 -COL133_bit_6 -COL133_bit_5 -COL133_bit_4 -COL133_bit_3 -COL133_bit_2 COL133_bit_1 COL133_bit0 COL133_bit1 COL133_bit2 -COL133_bit3 -COL133_bit4 COL133_bit5 -COL133_bit6 COL133_bit7 COL133_bit8 COL133_bit9 -COL133_bit10 COL133_bit11 -COL133_bit12 COL133_bit13 -COL001_bit0 -COL002_bit0 -COL003_bit0 -COL004_bit0 -COL005_bit0 -COL006_bit0 COL007_bit0 -COL008_bit0 -COL009_bit0 -COL010_bit0 COL011_bit0 -COL012_bit0 -COL013_bit0 -COL014_bit0 -COL015_bit0 -COL016_bit0 -COL017_bit0 COL018_bit0 -COL019_bit0 -COL020_bit0 -COL021_bit0 -COL022_bit0 -COL023_bit0 -COL024_bit0 -COL025_bit0 -COL026_bit0 -COL027_bit0 -COL028_bit0 -COL029_bit0 -COL030_bit0 COL031_bit0 -COL032_bit0 -COL033_bit0 -COL034_bit0 -COL035_bit0 -COL036_bit0 COL037_bit0 -COL038_bit0 -COL039_bit0 -COL040_bit0 -COL041_bit0 -COL042_bit0 -COL043_bit0 -COL044_bit0 -COL045_bit0 -COL046_bit0 -COL047_bit0 COL048_bit0 -COL049_bit0 -COL050_bit0 -COL051_bit0 -COL052_bit0 -COL053_bit0 -COL054_bit0 -COL055_bit0 COL056_bit0 COL057_bit0 -COL058_bit0 COL059_bit0 -COL060_bit0 -COL061_bit0 -COL062_bit0 -COL063_bit0 -COL064_bit0 -COL065_bit0 -COL066_bit0 -COL067_bit0 -COL068_bit0 COL069_bit0 -COL070_bit0 COL071_bit0 -COL072_bit0 COL129_bit0 COL130_bit0 -COL134_bit_7 -COL134_bit_6 -COL134_bit_5 -COL134_bit_4 -COL134_bit_3 -COL134_bit_2 -COL134_bit_1 COL134_bit0 COL134_bit1 -COL134_bit2 -COL134_bit3 -COL134_bit4 COL134_bit5 -COL134_bit6 COL134_bit7 -COL134_bit8 COL134_bit9 COL134_bit10 -COL134_bit11 -COL134_bit12 COL134_bit13 -COL135_bit_7 -COL135_bit_6 -COL135_bit_5 -COL135_bit_4 -COL135_bit_3 -COL135_bit_2 -COL135_bit_1 COL135_bit0 -COL135_bit1 COL135_bit2 -COL135_bit3 -COL135_bit4 -COL135_bit5 -COL135_bit6 COL135_bit7 COL135_bit8 COL135_bit9 -COL135_bit10 -COL135_bit11 -COL135_bit12 COL135_bit13 -COL136_bit_7 -COL136_bit_6 -COL136_bit_5 -COL136_bit_4 -COL136_bit_3 -COL136_bit_2 COL136_bit_1 COL136_bit0 -COL136_bit1 COL136_bit2 COL136_bit3 COL136_bit4 COL136_bit5 COL136_bit6 -COL136_bit7 COL136_bit8 -COL136_bit9 -COL136_bit10 -COL136_bit11 -COL136_bit12 COL136_bit13 -COL115_bit_7 -COL115_bit_6 -COL115_bit_5 -COL115_bit_4 -COL115_bit_3 -COL115_bit_2 -COL115_bit_1 -COL115_bit0 -COL115_bit1 COL115_bit2 COL115_bit3 -COL115_bit4 COL115_bit5 -COL115_bit6 -COL115_bit7 COL115_bit8 -COL115_bit9 -COL115_bit10 -COL115_bit11 -COL115_bit12 -COL116_bit_7 -COL116_bit_6 -COL116_bit_5 -COL116_bit_4 -COL116_bit_3 -COL116_bit_2 -COL116_bit_1 -COL116_bit0 -COL116_bit1 -COL116_bit2 -COL116_bit3 -COL116_bit4 -COL116_bit5 -COL116_bit6 -COL116_bit7 -COL116_bit8 -COL116_bit9 -COL116_bit10 -COL116_bit11 -COL116_bit12 -COL117_bit_7 -COL117_bit_6 -COL117_bit_5 -COL117_bit_4 -COL117_bit_3 -COL117_bit_2 -COL117_bit_1 -COL117_bit0 COL117_bit1 -COL117_bit2 COL117_bit3 -COL117_bit4 COL117_bit5 COL117_bit6 COL117_bit7 COL117_bit8 -COL117_bit9 -COL117_bit10 -COL117_bit11 -COL117_bit12 -COL118_bit_7 -COL118_bit_6 -COL118_bit_5 -COL118_bit_4 -COL118_bit_3 -COL118_bit_2 -COL118_bit_1 -COL118_bit0 -COL118_bit1 -COL118_bit2 -COL118_bit3 -COL118_bit4 -COL118_bit5 -COL118_bit6 -COL118_bit7 -COL118_bit8 -COL118_bit9 -COL118_bit10 -COL118_bit11 -COL118_bit12 -COL119_bit_7 -COL119_bit_6 -COL119_bit_5 -COL119_bit_4 -COL119_bit_3 -COL119_bit_2 -COL119_bit_1 -COL119_bit0 -COL119_bit1 -COL119_bit2 -COL119_bit3 -COL119_bit4 -COL119_bit5 -COL119_bit6 -COL119_bit7 -COL119_bit8 -COL119_bit9 -COL119_bit10 -COL119_bit11 -COL119_bit12 -COL120_bit_7 -COL120_bit_6 -COL120_bit_5 -COL120_bit_4 -COL120_bit_3 -COL120_bit_2 -COL120_bit_1 -COL120_bit0 -COL120_bit1 -COL120_bit2 -COL120_bit3 -COL120_bit4 -COL120_bit5 -COL120_bit6 -COL120_bit7 -COL120_bit8 -COL120_bit9 -COL120_bit10 -COL120_bit11 -COL120_bit12 -COL121_bit_7 -COL121_bit_6 -COL121_bit_5 -COL121_bit_4 -COL121_bit_3 -COL121_bit_2 -COL121_bit_1 -COL121_bit0 -COL121_bit1 -COL121_bit2 -COL121_bit3 -COL121_bit4 -COL121_bit5 -COL121_bit6 -COL121_bit7 -COL121_bit8 -COL121_bit9 -COL121_bit10 -COL121_bit11 -COL121_bit12 -COL122_bit_7 -COL122_bit_6 -COL122_bit_5 -COL122_bit_4 -COL122_bit_3 -COL122_bit_2 -COL122_bit_1 -COL122_bit0 -COL122_bit1 -COL122_bit2 -COL122_bit3 -COL122_bit4 -COL122_bit5 -COL122_bit6 -COL122_bit7 -COL122_bit8 -COL122_bit9 -COL122_bit10 -COL122_bit11 -COL122_bit12 -COL123_bit_7 -COL123_bit_6 -COL123_bit_5 -COL123_bit_4 -COL123_bit_3 -COL123_bit_2 -COL123_bit_1 -COL123_bit0 -COL123_bit1 -COL123_bit2 -COL123_bit3 -COL123_bit4 -COL123_bit5 -COL123_bit6 -COL123_bit7 -COL123_bit8 -COL123_bit9 -COL123_bit10 -COL123_bit11 -COL123_bit12 -COL124_bit_7 -COL124_bit_6 -COL124_bit_5 -COL124_bit_4 -COL124_bit_3 -COL124_bit_2 -COL124_bit_1 -COL124_bit0 -COL124_bit1 -COL124_bit2 -COL124_bit3 -COL124_bit4 -COL124_bit5 -COL124_bit6 -COL124_bit7 -COL124_bit8 -COL124_bit9 -COL124_bit10 -COL124_bit11 -COL124_bit12 -COL125_bit_7 -COL125_bit_6 -COL125_bit_5 -COL125_bit_4 -COL125_bit_3 -COL125_bit_2 -COL125_bit_1 -COL125_bit0 -COL125_bit1 -COL125_bit2 -COL125_bit3 -COL125_bit4 -COL125_bit5 -COL125_bit6 -COL125_bit7 -COL125_bit8 -COL125_bit9 -COL125_bit10 -COL125_bit11 -COL125_bit12 -COL126_bit_7 -COL126_bit_6 -COL126_bit_5 -COL126_bit_4 -COL126_bit_3 -COL126_bit_2 -COL126_bit_1 -COL126_bit0 COL126_bit1 -COL126_bit2 COL126_bit3 COL126_bit4 -COL126_bit5 COL126_bit6 -COL126_bit7 -COL126_bit8 -COL126_bit9 -COL126_bit10 -COL126_bit11 -COL126_bit12 -COL127_bit_7 -COL127_bit_6 -COL127_bit_5 -COL127_bit_4 -COL127_bit_3 -COL127_bit_2 -COL127_bit_1 -COL127_bit0 -COL127_bit1 -COL127_bit2 -COL127_bit3 -COL127_bit4 -COL127_bit5 -COL127_bit6 -COL127_bit7 -COL127_bit8 -COL127_bit9 -COL127_bit10 -COL127_bit11 -COL127_bit12 -COL128_bit_7 -COL128_bit_6 -COL128_bit_5 -COL128_bit_4 -COL128_bit_3 -COL128_bit_2 -COL128_bit_1 -COL128_bit0 -COL128_bit1 COL128_bit2 -COL128_bit3 COL128_bit4 COL128_bit5 -COL128_bit6 COL128_bit7 -COL128_bit8 -COL128_bit9 -COL128_bit10 -COL128_bit11 -COL128_bit12 -COL073_bit_7 -COL073_bit_6 -COL073_bit_5 -COL073_bit_4 -COL073_bit_3 -COL073_bit_2 -COL073_bit_1 -COL073_bit0 -COL073_bit1 -COL073_bit2 -COL073_bit3 -COL073_bit4 -COL073_bit5 -COL073_bit6 -COL073_bit7 -COL073_bit8 -COL073_bit9 -COL073_bit10 -COL073_bit11 -COL073_bit12 -COL074_bit_7 -COL074_bit_6 -COL074_bit_5 -COL074_bit_4 -COL074_bit_3 -COL074_bit_2 -COL074_bit_1 -COL074_bit0 -COL074_bit1 -COL074_bit2 -COL074_bit3 -COL074_bit4 -COL074_bit5 -COL074_bit6 -COL074_bit7 -COL074_bit8 -COL074_bit9 -COL074_bit10 -COL074_bit11 -COL074_bit12 -COL075_bit_7 -COL075_bit_6 -COL075_bit_5 -COL075_bit_4 -COL075_bit_3 -COL075_bit_2 -COL075_bit_1 -COL075_bit0 -COL075_bit1 -COL075_bit2 -COL075_bit3 -COL075_bit4 -COL075_bit5 -COL075_bit6 -COL075_bit7 -COL075_bit8 -COL075_bit9 -COL075_bit10 -COL075_bit11 -COL075_bit12 -COL076_bit_7 -COL076_bit_6 -COL076_bit_5 -COL076_bit_4 -COL076_bit_3 -COL076_bit_2 -COL076_bit_1 -COL076_bit0 -COL076_bit1 -COL076_bit2 -COL076_bit3 -COL076_bit4 -COL076_bit5 -COL076_bit6 -COL076_bit7 -COL076_bit8 -COL076_bit9 -COL076_bit10 -COL076_bit11 -COL076_bit12 -COL077_bit_7 -COL077_bit_6 -COL077_bit_5 -COL077_bit_4 -COL077_bit_3 -COL077_bit_2 -COL077_bit_1 -COL077_bit0 -COL077_bit1 -COL077_bit2 -COL077_bit3 -COL077_bit4 -COL077_bit5 -COL077_bit6 -COL077_bit7 -COL077_bit8 -COL077_bit9 -COL077_bit10 -COL077_bit11 -COL077_bit12 -COL078_bit_7 -COL078_bit_6 -COL078_bit_5 -COL078_bit_4 -COL078_bit_3 -COL078_bit_2 -COL078_bit_1 -COL078_bit0 -COL078_bit1 -COL078_bit2 -COL078_bit3 -COL078_bit4 -COL078_bit5 -COL078_bit6 -COL078_bit7 -COL078_bit8 -COL078_bit9 -COL078_bit10 -COL078_bit11 -COL078_bit12 -COL079_bit_7 -COL079_bit_6 -COL079_bit_5 -COL079_bit_4 -COL079_bit_3 -COL079_bit_2 -COL079_bit_1 -COL079_bit0 -COL079_bit1 -COL079_bit2 -COL079_bit3 -COL079_bit4 -COL079_bit5 -COL079_bit6 -COL079_bit7 -COL079_bit8 -COL079_bit9 -COL079_bit10 -COL079_bit11 -COL079_bit12 -COL085_bit_7 -COL085_bit_6 -COL085_bit_5 -COL085_bit_4 -COL085_bit_3 -COL085_bit_2 -COL085_bit_1 -COL085_bit0 -COL085_bit1 -COL085_bit2 -COL085_bit3 -COL085_bit4 -COL085_bit5 -COL085_bit6 -COL085_bit7 -COL085_bit8 -COL085_bit9 -COL085_bit10 -COL085_bit11 -COL085_bit12 -COL091_bit_7 -COL091_bit_6 -COL091_bit_5 -COL091_bit_4 -COL091_bit_3 -COL091_bit_2 -COL091_bit_1 -COL091_bit0 -COL091_bit1 -COL091_bit2 -COL091_bit3 -COL091_bit4 -COL091_bit5 -COL091_bit6 -COL091_bit7 -COL091_bit8 -COL091_bit9 -COL091_bit10 -COL091_bit11 -COL091_bit12 -COL097_bit_7 -COL097_bit_6 -COL097_bit_5 -COL097_bit_4 -COL097_bit_3 -COL097_bit_2 -COL097_bit_1 -COL097_bit0 -COL097_bit1 -COL097_bit2 -COL097_bit3 -COL097_bit4 -COL097_bit5 -COL097_bit6 -COL097_bit7 -COL097_bit8 -COL097_bit9 -COL097_bit10 -COL097_bit11 -COL097_bit12 -COL103_bit_7 -COL103_bit_6 -COL103_bit_5 -COL103_bit_4 -COL103_bit_3 -COL103_bit_2 -COL103_bit_1 -COL103_bit0 -COL103_bit1 -COL103_bit2 -COL103_bit3 -COL103_bit4 -COL103_bit5 -COL103_bit6 -COL103_bit7 -COL103_bit8 -COL103_bit9 -COL103_bit10 -COL103_bit11 -COL103_bit12 -COL109_bit_7 -COL109_bit_6 -COL109_bit_5 -COL109_bit_4 -COL109_bit_3 -COL109_bit_2 -COL109_bit_1 -COL109_bit0 -COL109_bit1 -COL109_bit2 -COL109_bit3 -COL109_bit4 -COL109_bit5 -COL109_bit6 -COL109_bit7 -COL109_bit8 -COL109_bit9 -COL109_bit10 -COL109_bit11 -COL109_bit12 -COL080_bit_7 -COL080_bit_6 -COL080_bit_5 -COL080_bit_4 -COL080_bit_3 -COL080_bit_2 -COL080_bit_1 -COL080_bit0 -COL080_bit1 -COL080_bit2 -COL080_bit3 -COL080_bit4 -COL080_bit5 -COL080_bit6 -COL080_bit7 -COL080_bit8 -COL080_bit9 -COL080_bit10 -COL080_bit11 -COL080_bit12 -COL081_bit_7 -COL081_bit_6 -COL081_bit_5 -COL081_bit_4 -COL081_bit_3 -COL081_bit_2 -COL081_bit_1 -COL081_bit0 COL081_bit1 -COL081_bit2 COL081_bit3 COL081_bit4 COL081_bit5 COL081_bit6 COL081_bit7 -COL081_bit8 -COL081_bit9 -COL081_bit10 -COL081_bit11 -COL081_bit12 -COL082_bit_7 -COL082_bit_6 -COL082_bit_5 -COL082_bit_4 -COL082_bit_3 -COL082_bit_2 -COL082_bit_1 -COL082_bit0 -COL082_bit1 -COL082_bit2 -COL082_bit3 -COL082_bit4 -COL082_bit5 -COL082_bit6 -COL082_bit7 -COL082_bit8 -COL082_bit9 -COL082_bit10 -COL082_bit11 -COL082_bit12 -COL083_bit_7 -COL083_bit_6 -COL083_bit_5 -COL083_bit_4 -COL083_bit_3 -COL083_bit_2 -COL083_bit_1 -COL083_bit0 -COL083_bit1 -COL083_bit2 -COL083_bit3 -COL083_bit4 -COL083_bit5 -COL083_bit6 -COL083_bit7 -COL083_bit8 -COL083_bit9 -COL083_bit10 -COL083_bit11 -COL083_bit12 -COL084_bit_7 -COL084_bit_6 -COL084_bit_5 -COL084_bit_4 -COL084_bit_3 -COL084_bit_2 -COL084_bit_1 -COL084_bit0 -COL084_bit1 -COL084_bit2 -COL084_bit3 -COL084_bit4 -COL084_bit5 -COL084_bit6 -COL084_bit7 -COL084_bit8 -COL084_bit9 -COL084_bit10 -COL084_bit11 -COL084_bit12 -COL086_bit_7 -COL086_bit_6 -COL086_bit_5 -COL086_bit_4 -COL086_bit_3 -COL086_bit_2 -COL086_bit_1 -COL086_bit0 COL086_bit1 -COL086_bit2 -COL086_bit3 -COL086_bit4 COL086_bit5 -COL086_bit6 -COL086_bit7 COL086_bit8 -COL086_bit9 -COL086_bit10 -COL086_bit11 -COL086_bit12 -COL092_bit_7 -COL092_bit_6 -COL092_bit_5 -COL092_bit_4 -COL092_bit_3 -COL092_bit_2 -COL092_bit_1 -COL092_bit0 -COL092_bit1 -COL092_bit2 -COL092_bit3 -COL092_bit4 -COL092_bit5 -COL092_bit6 -COL092_bit7 -COL092_bit8 -COL092_bit9 -COL092_bit10 -COL092_bit11 -COL092_bit12 -COL098_bit_7 -COL098_bit_6 -COL098_bit_5 -COL098_bit_4 -COL098_bit_3 -COL098_bit_2 -COL098_bit_1 -COL098_bit0 -COL098_bit1 -COL098_bit2 -COL098_bit3 -COL098_bit4 -COL098_bit5 -COL098_bit6 -COL098_bit7 -COL098_bit8 -COL098_bit9 -COL098_bit10 -COL098_bit11 -COL098_bit12 -COL104_bit_7 -COL104_bit_6 -COL104_bit_5 -COL104_bit_4 -COL104_bit_3 -COL104_bit_2 -COL104_bit_1 -COL104_bit0 -COL104_bit1 -COL104_bit2 -COL104_bit3 -COL104_bit4 -COL104_bit5 -COL104_bit6 -COL104_bit7 -COL104_bit8 -COL104_bit9 -COL104_bit10 -COL104_bit11 -COL104_bit12 -COL110_bit_7 -COL110_bit_6 -COL110_bit_5 -COL110_bit_4 -COL110_bit_3 -COL110_bit_2 -COL110_bit_1 -COL110_bit0 -COL110_bit1 -COL110_bit2 -COL110_bit3 -COL110_bit4 -COL110_bit5 -COL110_bit6 -COL110_bit7 -COL110_bit8 -COL110_bit9 -COL110_bit10 -COL110_bit11 -COL110_bit12 -COL087_bit_7 -COL087_bit_6 -COL087_bit_5 -COL087_bit_4 -COL087_bit_3 -COL087_bit_2 -COL087_bit_1 -COL087_bit0 -COL087_bit1 -COL087_bit2 -COL087_bit3 -COL087_bit4 -COL087_bit5 -COL087_bit6 -COL087_bit7 -COL087_bit8 -COL087_bit9 -COL087_bit10 -COL087_bit11 -COL087_bit12 -COL088_bit_7 -COL088_bit_6 -COL088_bit_5 -COL088_bit_4 -COL088_bit_3 -COL088_bit_2 -COL088_bit_1 -COL088_bit0 -COL088_bit1 -COL088_bit2 -COL088_bit3 -COL088_bit4 -COL088_bit5 -COL088_bit6 -COL088_bit7 -COL088_bit8 -COL088_bit9 -COL088_bit10 -COL088_bit11 -COL088_bit12 -COL089_bit_7 -COL089_bit_6 -COL089_bit_5 -COL089_bit_4 -COL089_bit_3 -COL089_bit_2 -COL089_bit_1 -COL089_bit0 -COL089_bit1 -COL089_bit2 -COL089_bit3 -COL089_bit4 -COL089_bit5 -COL089_bit6 -COL089_bit7 -COL089_bit8 -COL089_bit9 -COL089_bit10 -COL089_bit11 -COL089_bit12 -COL090_bit_7 -COL090_bit_6 -COL090_bit_5 -COL090_bit_4 -COL090_bit_3 -COL090_bit_2 -COL090_bit_1 -COL090_bit0 -COL090_bit1 -COL090_bit2 -COL090_bit3 -COL090_bit4 -COL090_bit5 -COL090_bit6 -COL090_bit7 -COL090_bit8 -COL090_bit9 -COL090_bit10 -COL090_bit11 -COL090_bit12 -COL093_bit_7 -COL093_bit_6 -COL093_bit_5 -COL093_bit_4 -COL093_bit_3 -COL093_bit_2 -COL093_bit_1 -COL093_bit0 -COL093_bit1 -COL093_bit2 -COL093_bit3 -COL093_bit4 -COL093_bit5 -COL093_bit6 -COL093_bit7 -COL093_bit8 -COL093_bit9 -COL093_bit10 -COL093_bit11 -COL093_bit12 -COL099_bit_7 -COL099_bit_6 -COL099_bit_5 -COL099_bit_4 -COL099_bit_3 -COL099_bit_2 -COL099_bit_1 -COL099_bit0 -COL099_bit1 -COL099_bit2 -COL099_bit3 -COL099_bit4 -COL099_bit5 -COL099_bit6 -COL099_bit7 -COL099_bit8 -COL099_bit9 -COL099_bit10 -COL099_bit11 -COL099_bit12 -COL105_bit_7 -COL105_bit_6 -COL105_bit_5 -COL105_bit_4 -COL105_bit_3 -COL105_bit_2 -COL105_bit_1 -COL105_bit0 -COL105_bit1 -COL105_bit2 -COL105_bit3 -COL105_bit4 -COL105_bit5 -COL105_bit6 -COL105_bit7 -COL105_bit8 -COL105_bit9 -COL105_bit10 -COL105_bit11 -COL105_bit12 -COL111_bit_7 -COL111_bit_6 -COL111_bit_5 -COL111_bit_4 -COL111_bit_3 -COL111_bit_2 -COL111_bit_1 -COL111_bit0 -COL111_bit1 -COL111_bit2 -COL111_bit3 -COL111_bit4 -COL111_bit5 -COL111_bit6 -COL111_bit7 -COL111_bit8 -COL111_bit9 -COL111_bit10 -COL111_bit11 -COL111_bit12 -COL094_bit_7 -COL094_bit_6 -COL094_bit_5 -COL094_bit_4 -COL094_bit_3 -COL094_bit_2 -COL094_bit_1 -COL094_bit0 -COL094_bit1 -COL094_bit2 -COL094_bit3 -COL094_bit4 -COL094_bit5 -COL094_bit6 -COL094_bit7 -COL094_bit8 -COL094_bit9 -COL094_bit10 -COL094_bit11 -COL094_bit12 -COL095_bit_7 -COL095_bit_6 -COL095_bit_5 -COL095_bit_4 -COL095_bit_3 -COL095_bit_2 -COL095_bit_1 -COL095_bit0 -COL095_bit1 -COL095_bit2 -COL095_bit3 -COL095_bit4 -COL095_bit5 -COL095_bit6 -COL095_bit7 -COL095_bit8 -COL095_bit9 -COL095_bit10 -COL095_bit11 -COL095_bit12 -COL096_bit_7 -COL096_bit_6 -COL096_bit_5 -COL096_bit_4 -COL096_bit_3 -COL096_bit_2 -COL096_bit_1 -COL096_bit0 -COL096_bit1 -COL096_bit2 -COL096_bit3 -COL096_bit4 -COL096_bit5 -COL096_bit6 -COL096_bit7 -COL096_bit8 -COL096_bit9 -COL096_bit10 -COL096_bit11 -COL096_bit12 -COL100_bit_7 -COL100_bit_6 -COL100_bit_5 -COL100_bit_4 -COL100_bit_3 -COL100_bit_2 -COL100_bit_1 -COL100_bit0 -COL100_bit1 -COL100_bit2 -COL100_bit3 -COL100_bit4 -COL100_bit5 -COL100_bit6 -COL100_bit7 -COL100_bit8 -COL100_bit9 -COL100_bit10 -COL100_bit11 -COL100_bit12 -COL106_bit_7 -COL106_bit_6 -COL106_bit_5 -COL106_bit_4 -COL106_bit_3 -COL106_bit_2 -COL106_bit_1 -COL106_bit0 -COL106_bit1 -COL106_bit2 -COL106_bit3 -COL106_bit4 -COL106_bit5 -COL106_bit6 -COL106_bit7 -COL106_bit8 -COL106_bit9 -COL106_bit10 -COL106_bit11 -COL106_bit12 -COL112_bit_7 -COL112_bit_6 -COL112_bit_5 -COL112_bit_4 -COL112_bit_3 -COL112_bit_2 -COL112_bit_1 -COL112_bit0 -COL112_bit1 -COL112_bit2 -COL112_bit3 -COL112_bit4 -COL112_bit5 -COL112_bit6 -COL112_bit7 -COL112_bit8 -COL112_bit9 -COL112_bit10 -COL112_bit11 -COL112_bit12 -COL101_bit_7 -COL101_bit_6 -COL101_bit_5 -COL101_bit_4 -COL101_bit_3 -COL101_bit_2 -COL101_bit_1 -COL101_bit0 COL101_bit1 COL101_bit2 COL101_bit3 COL101_bit4 -COL101_bit5 -COL101_bit6 -COL101_bit7 -COL101_bit8 -COL101_bit9 -COL101_bit10 -COL101_bit11 -COL101_bit12 -COL102_bit_7 -COL102_bit_6 -COL102_bit_5 -COL102_bit_4 -COL102_bit_3 -COL102_bit_2 -COL102_bit_1 -COL102_bit0 -COL102_bit1 -COL102_bit2 -COL102_bit3 -COL102_bit4 -COL102_bit5 -COL102_bit6 -COL102_bit7 -COL102_bit8 -COL102_bit9 -COL102_bit10 -COL102_bit11 -COL102_bit12 -COL107_bit_7 -COL107_bit_6 -COL107_bit_5 -COL107_bit_4 -COL107_bit_3 -COL107_bit_2 -COL107_bit_1 -COL107_bit0 -COL107_bit1 -COL107_bit2 -COL107_bit3 -COL107_bit4 -COL107_bit5 -COL107_bit6 -COL107_bit7 -COL107_bit8 -COL107_bit9 -COL107_bit10 -COL107_bit11 -COL107_bit12 -COL113_bit_7 -COL113_bit_6 -COL113_bit_5 -COL113_bit_4 -COL113_bit_3 -COL113_bit_2 -COL113_bit_1 -COL113_bit0 -COL113_bit1 -COL113_bit2 -COL113_bit3 -COL113_bit4 -COL113_bit5 -COL113_bit6 -COL113_bit7 -COL113_bit8 -COL113_bit9 -COL113_bit10 -COL113_bit11 -COL113_bit12 -COL108_bit_7 -COL108_bit_6 -COL108_bit_5 -COL108_bit_4 -COL108_bit_3 -COL108_bit_2 -COL108_bit_1 -COL108_bit0 -COL108_bit1 -COL108_bit2 -COL108_bit3 -COL108_bit4 -COL108_bit5 -COL108_bit6 -COL108_bit7 -COL108_bit8 -COL108_bit9 -COL108_bit10 -COL108_bit11 -COL108_bit12 -COL114_bit_7 -COL114_bit_6 -COL114_bit_5 -COL114_bit_4 -COL114_bit_3 -COL114_bit_2 -COL114_bit_1 -COL114_bit0 -COL114_bit1 -COL114_bit2 -COL114_bit3 -COL114_bit4 -COL114_bit5 -COL114_bit6 -COL114_bit7 -COL114_bit8 -COL114_bit9 -COL114_bit10 -COL114_bit11 -COL114_bit12 -COL131_bit_7 -COL131_bit_6 -COL131_bit_5 -COL131_bit_4 -COL131_bit_3 -COL131_bit_2 -COL131_bit_1 COL131_bit0 -COL131_bit1 -COL131_bit2 -COL131_bit3 -COL131_bit4 -COL131_bit5 -COL131_bit6 -COL131_bit7 -COL131_bit8 -COL131_bit9 -COL131_bit10 -COL131_bit11 -COL131_bit12 COL131_bit13 -COL132_bit_7 -COL132_bit_6 -COL132_bit_5 -COL132_bit_4 -COL132_bit_3 -COL132_bit_2 -COL132_bit_1 COL132_bit0 -COL132_bit1 -COL132_bit2 -COL132_bit3 -COL132_bit4 -COL132_bit5 -COL132_bit6 -COL132_bit7 -COL132_bit8 -COL132_bit9 -COL132_bit10 -COL132_bit11 -COL132_bit12 COL132_bit13
c _______________________________________________________________________________
c 
c restarts              : 49
c conflicts             : 167096         (163 /sec)
c decisions             : 307193         (299 /sec)
c propagations          : 117032313      (113932 /sec)
c inspects              : 1230845345     (1198238 /sec)
c CPU time              : 1027.21 s
c _______________________________________________________________________________
#### 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.91 2/54 10458
Raw data (stat): 10458 (runsolver) R 10457 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 547089163 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.0001 s]
Raw data (loadavg): 0.87 0.97 0.91 2/54 10458
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 4621 0 0 0 984 14 0 0 25 0 1 0 547089163 13303808 2734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3248 2734 603 41 0 3207 0
vsize: 12992
[startup+20.0011 s]
Raw data (loadavg): 0.89 0.97 0.91 2/54 10458
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 5604 0 0 0 1982 16 0 0 25 0 1 0 547089163 17350656 3717 4294967295 134512640 134672761 3221224544 3221223648 134604307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4236 3717 603 41 0 4195 0
vsize: 16944
[startup+30.0018 s]
Raw data (loadavg): 0.91 0.97 0.91 2/54 10458
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 6601 0 0 0 2979 19 0 0 25 0 1 0 547089163 21524480 4714 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5255 4714 603 41 0 5214 0
vsize: 21020
[startup+40.0014 s]
Raw data (loadavg): 0.92 0.97 0.91 2/54 10458
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 7720 0 0 0 3976 22 0 0 25 0 1 0 547089163 26132480 5833 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6380 5833 603 41 0 6339 0
vsize: 25520
[startup+50.0021 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 10458
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 8954 0 0 0 4971 26 0 0 25 0 1 0 547089163 30617600 6907 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7475 6907 603 41 0 7434 0
vsize: 29900
[startup+60.002 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 10458
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 8954 0 0 0 5970 26 0 0 25 0 1 0 547089163 30617600 6907 4294967295 134512640 134672761 3221224544 3221223728 134615796 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7475 6907 603 41 0 7434 0
vsize: 29900
[startup+70.0024 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 10458
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 8957 0 0 0 6971 27 0 0 25 0 1 0 547089163 30617600 6910 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7475 6910 603 41 0 7434 0
vsize: 29900
[startup+80.0036 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 10458
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 8959 0 0 0 7971 27 0 0 25 0 1 0 547089163 30617600 6912 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7475 6912 603 41 0 7434 0
vsize: 29900
[startup+90.0031 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 10458
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 9773 0 0 0 8970 28 0 0 25 0 1 0 547089163 33816576 7726 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8256 7726 603 41 0 8215 0
vsize: 33024
[startup+100.004 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 10458
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 10862 0 0 0 9966 32 0 0 25 0 1 0 547089163 38289408 8815 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9348 8815 603 41 0 9307 0
vsize: 37392
[startup+110.004 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 10458
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 11806 0 0 0 10963 35 0 0 25 0 1 0 547089163 42172416 9759 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10296 9759 603 41 0 10255 0
vsize: 41184
[startup+120.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 10458
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 12542 0 0 0 11961 37 0 0 25 0 1 0 547089163 45223936 10495 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11041 10495 603 41 0 11000 0
vsize: 44164
[startup+130.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 10458
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 13215 0 0 0 12959 39 0 0 25 0 1 0 547089163 48062464 11168 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11734 11168 603 41 0 11693 0
vsize: 46936
[startup+140.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 14308 0 0 0 13956 42 0 0 25 0 1 0 547089163 52563968 12261 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12833 12261 603 41 0 12792 0
vsize: 51332
[startup+150.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 15039 0 0 0 14955 44 0 0 25 0 1 0 547089163 55476224 12992 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13544 12992 603 41 0 13503 0
vsize: 54176
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 15888 0 0 0 15954 45 0 0 25 0 1 0 547089163 58974208 13841 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14398 13841 603 41 0 14357 0
vsize: 57592
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 16621 0 0 0 16952 48 0 0 25 0 1 0 547089163 61968384 14574 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15129 14574 603 41 0 15088 0
vsize: 60516
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 17538 0 0 0 17949 50 0 0 25 0 1 0 547089163 65740800 15491 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16050 15491 603 41 0 16009 0
vsize: 64200
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 18679 0 0 0 18947 52 0 0 25 0 1 0 547089163 70443008 16632 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17198 16632 603 41 0 17157 0
vsize: 68792
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 19607 0 0 0 19945 54 0 0 25 0 1 0 547089163 74129408 17560 4294967295 134512640 134672761 3221224544 3221223744 134610697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18098 17560 603 41 0 18057 0
vsize: 72392
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 20538 0 0 0 20943 57 0 0 25 0 1 0 547089163 77942784 18491 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19029 18491 603 41 0 18988 0
vsize: 76116
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 21444 0 0 0 21942 58 0 0 25 0 1 0 547089163 81711104 19397 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19949 19397 603 41 0 19908 0
vsize: 79796
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 22380 0 0 0 22940 60 0 0 25 0 1 0 547089163 85561344 20333 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20889 20333 603 41 0 20848 0
vsize: 83556
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 23200 0 0 0 23938 63 0 0 25 0 1 0 547089163 88850432 21153 4294967295 134512640 134672761 3221224544 3221223688 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21692 21153 603 41 0 21651 0
vsize: 86768
[startup+250.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 23975 0 0 0 24936 65 0 0 25 0 1 0 547089163 92065792 21928 4294967295 134512640 134672761 3221224544 3221223688 134616279 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22477 21928 603 41 0 22436 0
vsize: 89908
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 24400 0 0 0 25935 65 0 0 25 0 1 0 547089163 93773824 22353 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22894 22353 603 41 0 22853 0
vsize: 91576
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 24836 0 0 0 26934 67 0 0 25 0 1 0 547089163 95555584 22789 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23329 22789 603 41 0 23288 0
vsize: 93316
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 25304 0 0 0 27933 68 0 0 25 0 1 0 547089163 97505280 23257 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23805 23257 603 41 0 23764 0
vsize: 95220
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 26237 0 0 0 28929 72 0 0 25 0 1 0 547089163 101277696 24190 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24726 24190 603 41 0 24685 0
vsize: 98904
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 26832 0 0 0 29928 74 0 0 25 0 1 0 547089163 103809024 24785 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25344 24785 603 41 0 25303 0
vsize: 101376
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 27731 0 0 0 30925 76 0 0 25 0 1 0 547089163 107487232 25684 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26242 25684 603 41 0 26201 0
vsize: 104968
[startup+320.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 28310 0 0 0 31925 77 0 0 25 0 1 0 547089163 109629440 26204 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26765 26204 603 41 0 26724 0
vsize: 107060
[startup+330.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 28310 0 0 0 32925 77 0 0 25 0 1 0 547089163 109629440 26204 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26765 26204 603 41 0 26724 0
vsize: 107060
[startup+340.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 28310 0 0 0 33925 77 0 0 25 0 1 0 547089163 109629440 26204 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26765 26204 603 41 0 26724 0
vsize: 107060
[startup+350.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 28310 0 0 0 34925 77 0 0 25 0 1 0 547089163 109629440 26204 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26765 26204 603 41 0 26724 0
vsize: 107060
[startup+360.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 28310 0 0 0 35925 77 0 0 25 0 1 0 547089163 109629440 26204 4294967295 134512640 134672761 3221224544 3221223708 134614558 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26765 26204 603 41 0 26724 0
vsize: 107060
[startup+370.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 28311 0 0 0 36926 77 0 0 25 0 1 0 547089163 109629440 26205 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26765 26205 603 41 0 26724 0
vsize: 107060
[startup+380.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 28311 0 0 0 37926 77 0 0 25 0 1 0 547089163 109629440 26205 4294967295 134512640 134672761 3221224544 3221223728 134615830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26765 26205 603 41 0 26724 0
vsize: 107060
[startup+390.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 28311 0 0 0 38926 77 0 0 25 0 1 0 547089163 109629440 26205 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26765 26205 603 41 0 26724 0
vsize: 107060
[startup+400.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 28312 0 0 0 39926 78 0 0 25 0 1 0 547089163 109629440 26206 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26765 26206 603 41 0 26724 0
vsize: 107060
[startup+410.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 28312 0 0 0 40926 78 0 0 25 0 1 0 547089163 109629440 26206 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26765 26206 603 41 0 26724 0
vsize: 107060
[startup+420.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 28312 0 0 0 41926 78 0 0 25 0 1 0 547089163 109629440 26206 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26765 26206 603 41 0 26724 0
vsize: 107060
[startup+430.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 28312 0 0 0 42927 78 0 0 25 0 1 0 547089163 109629440 26206 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26765 26206 603 41 0 26724 0
vsize: 107060
[startup+440.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 28312 0 0 0 43927 78 0 0 25 0 1 0 547089163 109629440 26206 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26765 26206 603 41 0 26724 0
vsize: 107060
[startup+450.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 28313 0 0 0 44927 78 0 0 25 0 1 0 547089163 109629440 26207 4294967295 134512640 134672761 3221224544 3221223584 134612587 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26765 26207 603 41 0 26724 0
vsize: 107060
[startup+460.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 28313 0 0 0 45927 78 0 0 25 0 1 0 547089163 109629440 26207 4294967295 134512640 134672761 3221224544 3221223728 134615985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26765 26207 603 41 0 26724 0
vsize: 107060
[startup+470.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 28313 0 0 0 46927 78 0 0 25 0 1 0 547089163 109629440 26207 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26765 26207 603 41 0 26724 0
vsize: 107060
[startup+480.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 28940 0 0 0 47926 79 0 0 25 0 1 0 547089163 112279552 26834 4294967295 134512640 134672761 3221224544 3221223584 134613012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27412 26834 603 41 0 27371 0
vsize: 109648
[startup+490.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 29756 0 0 0 48923 82 0 0 25 0 1 0 547089163 115585024 27650 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28219 27650 603 41 0 28178 0
vsize: 112876
[startup+500.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 30785 0 0 0 49922 84 0 0 25 0 1 0 547089163 119943168 28679 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29283 28679 603 41 0 29242 0
vsize: 117132
[startup+510.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 31521 0 0 0 50920 86 0 0 25 0 1 0 547089163 122839040 29415 4294967295 134512640 134672761 3221224544 3221223728 134616004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29990 29415 603 41 0 29949 0
vsize: 119960
[startup+520.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 32292 0 0 0 51918 88 0 0 25 0 1 0 547089163 126029824 30186 4294967295 134512640 134672761 3221224544 3221223584 134614268 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30769 30186 603 41 0 30728 0
vsize: 123076
[startup+530.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 33227 0 0 0 52915 91 0 0 25 0 1 0 547089163 129892352 31121 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31712 31121 603 41 0 31671 0
vsize: 126848
[startup+540.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 34032 0 0 0 53913 93 0 0 25 0 1 0 547089163 133185536 31926 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32516 31926 603 41 0 32475 0
vsize: 130064
[startup+550.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 34771 0 0 0 54912 94 0 0 25 0 1 0 547089163 136278016 32665 4294967295 134512640 134672761 3221224544 3221223356 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33271 32665 603 41 0 33230 0
vsize: 133084
[startup+560.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 35414 0 0 0 55910 97 0 0 25 0 1 0 547089163 138870784 33308 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33904 33308 603 41 0 33863 0
vsize: 135616
[startup+570.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 35824 0 0 0 56909 98 0 0 25 0 1 0 547089163 140554240 33718 4294967295 134512640 134672761 3221224544 3221223728 134616020 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34315 33718 603 41 0 34274 0
vsize: 137260
[startup+580.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 36622 0 0 0 57906 101 0 0 25 0 1 0 547089163 143839232 34516 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35117 34516 603 41 0 35076 0
vsize: 140468
[startup+590.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 37049 0 0 0 58905 102 0 0 25 0 1 0 547089163 145637376 34943 4294967295 134512640 134672761 3221224544 3221223584 134613012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35556 34943 603 41 0 35515 0
vsize: 142224
[startup+600.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 37563 0 0 0 59904 104 0 0 25 0 1 0 547089163 147668992 35457 4294967295 134512640 134672761 3221224544 3221223688 134616181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36052 35457 603 41 0 36011 0
vsize: 144208
[startup+610.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 38158 0 0 0 60902 106 0 0 25 0 1 0 547089163 150061056 36052 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36636 36052 603 41 0 36595 0
vsize: 146544
[startup+620.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39031 0 0 0 61901 107 0 0 25 0 1 0 547089163 153718784 36925 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37529 36925 603 41 0 37488 0
vsize: 150116
[startup+630.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39467 0 0 0 62899 109 0 0 25 0 1 0 547089163 155160576 37298 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37881 37298 603 41 0 37840 0
vsize: 151524
[startup+640.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39467 0 0 0 63899 109 0 0 25 0 1 0 547089163 155160576 37298 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37881 37298 603 41 0 37840 0
vsize: 151524
[startup+650.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39469 0 0 0 64900 109 0 0 25 0 1 0 547089163 155160576 37300 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37881 37300 603 41 0 37840 0
vsize: 151524
[startup+660.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39469 0 0 0 65900 109 0 0 25 0 1 0 547089163 155160576 37300 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37881 37300 603 41 0 37840 0
vsize: 151524
[startup+670.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39469 0 0 0 66900 109 0 0 25 0 1 0 547089163 155160576 37300 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37881 37300 603 41 0 37840 0
vsize: 151524
[startup+680.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39470 0 0 0 67900 109 0 0 25 0 1 0 547089163 155160576 37301 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37881 37301 603 41 0 37840 0
vsize: 151524
[startup+690.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39470 0 0 0 68900 109 0 0 25 0 1 0 547089163 155160576 37301 4294967295 134512640 134672761 3221224544 3221223584 134612604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37881 37301 603 41 0 37840 0
vsize: 151524
[startup+700.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39470 0 0 0 69900 109 0 0 25 0 1 0 547089163 155160576 37301 4294967295 134512640 134672761 3221224544 3221223356 1075350544 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37881 37301 603 41 0 37840 0
vsize: 151524
[startup+710.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39470 0 0 0 70900 109 0 0 25 0 1 0 547089163 155160576 37301 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37881 37301 603 41 0 37840 0
vsize: 151524
[startup+720.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39470 0 0 0 71901 109 0 0 25 0 1 0 547089163 155160576 37301 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37881 37301 603 41 0 37840 0
vsize: 151524
[startup+730.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39470 0 0 0 72901 109 0 0 25 0 1 0 547089163 155160576 37301 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37881 37301 603 41 0 37840 0
vsize: 151524
[startup+740.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39470 0 0 0 73901 109 0 0 25 0 1 0 547089163 155160576 37301 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37881 37301 603 41 0 37840 0
vsize: 151524
[startup+750.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39470 0 0 0 74901 109 0 0 25 0 1 0 547089163 155160576 37301 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37881 37301 603 41 0 37840 0
vsize: 151524
[startup+760.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39470 0 0 0 75901 109 0 0 25 0 1 0 547089163 155160576 37301 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37881 37301 603 41 0 37840 0
vsize: 151524
[startup+770.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39470 0 0 0 76901 110 0 0 25 0 1 0 547089163 155160576 37301 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37881 37301 603 41 0 37840 0
vsize: 151524
[startup+780.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39470 0 0 0 77902 110 0 0 25 0 1 0 547089163 155160576 37301 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37881 37301 603 41 0 37840 0
vsize: 151524
[startup+790.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39470 0 0 0 78902 110 0 0 25 0 1 0 547089163 155160576 37301 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37881 37301 603 41 0 37840 0
vsize: 151524
[startup+800.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39470 0 0 0 79902 110 0 0 25 0 1 0 547089163 155160576 37301 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37881 37301 603 41 0 37840 0
vsize: 151524
[startup+810.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39470 0 0 0 80902 110 0 0 25 0 1 0 547089163 155160576 37301 4294967295 134512640 134672761 3221224544 3221223728 134616004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37881 37301 603 41 0 37840 0
vsize: 151524
[startup+820.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39473 0 0 0 81902 110 0 0 25 0 1 0 547089163 155160576 37304 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37881 37304 603 41 0 37840 0
vsize: 151524
[startup+830.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39473 0 0 0 82902 110 0 0 25 0 1 0 547089163 155160576 37304 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37881 37304 603 41 0 37840 0
vsize: 151524
[startup+840.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39477 0 0 0 83903 110 0 0 25 0 1 0 547089163 155160576 37308 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37881 37308 603 41 0 37840 0
vsize: 151524
[startup+850.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39478 0 0 0 84903 110 0 0 25 0 1 0 547089163 155160576 37309 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37881 37309 603 41 0 37840 0
vsize: 151524
[startup+860.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39478 0 0 0 85903 110 0 0 25 0 1 0 547089163 155160576 37309 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37881 37309 603 41 0 37840 0
vsize: 151524
[startup+870.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39482 0 0 0 86903 110 0 0 25 0 1 0 547089163 155160576 37313 4294967295 134512640 134672761 3221224544 3221223688 134616275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37881 37313 603 41 0 37840 0
vsize: 151524
[startup+880.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39482 0 0 0 87903 110 0 0 25 0 1 0 547089163 155160576 37313 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37881 37313 603 41 0 37840 0
vsize: 151524
[startup+890.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39484 0 0 0 88903 110 0 0 25 0 1 0 547089163 155422720 37315 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37945 37315 603 41 0 37904 0
vsize: 151780
[startup+900.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39485 0 0 0 89904 110 0 0 25 0 1 0 547089163 155422720 37316 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37945 37316 603 41 0 37904 0
vsize: 151780
[startup+910.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39486 0 0 0 90904 110 0 0 25 0 1 0 547089163 155422720 37317 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37945 37317 603 41 0 37904 0
vsize: 151780
[startup+920.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39582 0 0 0 91904 110 0 0 25 0 1 0 547089163 155811840 37413 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38040 37413 603 41 0 37999 0
vsize: 152160
[startup+930.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 40436 0 0 0 92901 113 0 0 25 0 1 0 547089163 159412224 38235 4294967295 134512640 134672761 3221224544 3221223600 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38919 38235 603 41 0 38878 0
vsize: 155676
[startup+940.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 40440 0 0 0 93902 113 0 0 25 0 1 0 547089163 158887936 38170 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38791 38170 603 41 0 38750 0
vsize: 155164
[startup+950.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 40440 0 0 0 94902 113 0 0 25 0 1 0 547089163 158887936 38170 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38791 38170 603 41 0 38750 0
vsize: 155164
[startup+960.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 40440 0 0 0 95902 113 0 0 25 0 1 0 547089163 158887936 38170 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38791 38170 603 41 0 38750 0
vsize: 155164
[startup+970.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 40440 0 0 0 96902 113 0 0 25 0 1 0 547089163 158887936 38170 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38791 38170 603 41 0 38750 0
vsize: 155164
[startup+980.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 40440 0 0 0 97902 113 0 0 25 0 1 0 547089163 158887936 38170 4294967295 134512640 134672761 3221224544 3221223584 134613012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38791 38170 603 41 0 38750 0
vsize: 155164
[startup+990.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 40440 0 0 0 98902 113 0 0 25 0 1 0 547089163 158887936 38170 4294967295 134512640 134672761 3221224544 3221223700 134564777 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38791 38170 603 41 0 38750 0
vsize: 155164
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 40440 0 0 0 99903 113 0 0 25 0 1 0 547089163 158887936 38170 4294967295 134512640 134672761 3221224544 3221223584 134612608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38791 38170 603 41 0 38750 0
vsize: 155164
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 40440 0 0 0 100903 113 0 0 25 0 1 0 547089163 158887936 38170 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38791 38170 603 41 0 38750 0
vsize: 155164
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 40440 0 0 0 101903 113 0 0 25 0 1 0 547089163 158887936 38170 4294967295 134512640 134672761 3221224544 3221223728 134615681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38791 38170 603 41 0 38750 0
vsize: 155164
[startup+1028.28 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 10460
Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 40440 0 0 0 101903 113 0 0 25 0 1 0 547089163 158887936 38170 4294967295 134512640 134672761 3221224544 3221223728 134615681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38791 38170 603 41 0 38750 0
vsize: 0

Child status: 30
Real time (s): 1028.28
CPU time (s): 1028.43
CPU user time (s): 1027.22
CPU system time (s): 1.20582
CPU usage (%): 100.014
Max. virtual memory (Kb): 155676
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	1430464
#### END VERIFIER DATA ####