PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-misc05.opb
MD5SUM	5e97a4ad772c87cdf15a611dd5b54048
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1076796928
Optimality of the best value was proved	NO
Number of terms in the objective function	31
Biggest coefficient in the objective function	1073741824
Number of bits for the biggest coefficient in the objective function	31
Sum of the numbers in the objective function	2147483647
Number of bits of the sum of numbers in the objective function	31
Biggest number in a constraint	5368709120
Number of bits of the biggest number in a constraint	33
Biggest sum of numbers in a constraint	83751857084
Number of bits of the biggest sum of numbers	37
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	952.576
Number of variables	1940
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	451
Trace number 30707

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc29 THE 2005-05-25 18:46:44 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22107 boxname=wulflinc29 idbench=923 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  5e97a4ad772c87cdf15a611dd5b54048  /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-misc05.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-misc05.opb
IDLAUNCH: 22107
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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.020
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        451768 kB
Buffers:         35300 kB
Cached:         522544 kB
SwapCached:        572 kB
Active:          66392 kB
Inactive:       496968 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        451516 kB
SwapTotal:     2097892 kB
SwapFree:      2096728 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5612 kB
Slab:            13944 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 19:02:37 (client local time) WITH STATUS 30 IN 952.576 SECONDS
stats: 22107 0 952.576 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]---> Adder-cost: 124   maxlim: 3219483647   bits: 33/32
c ---[ 345]---> Adder-cost: 876   maxlim: 5368714235   bits: 34/33
c ---[ 343]---> Sorter-cost: 5504     Base: 2 2 2 2 2 2 2 2 2 3 5 2 2 2 17 2 2 2 2 2 2 2 2 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: 443   maxlim: 1880058   bits: 22/21
c ---[ 180]---> Adder-cost: 492   maxlim: 3186682   bits: 23/22
c ---[ 178]---> Adder-cost: 492   maxlim: 3350522   bits: 23/22
c ---[ 176]---> Adder-cost: 443   maxlim: 1566715   bits: 22/21
c ---[ 174]---> Adder-cost: 492   maxlim: 3207162   bits: 23/22
c ---[ 172]---> Adder-cost: 492   maxlim: 3176442   bits: 23/22
c ---[ 170]---> Adder-cost: 492   maxlim: 3330042   bits: 23/22
c ---[ 168]---> BDD-cost:   89
c ---[ 166]---> BDD-cost:   89
c ---[ 165]---> Sorter-cost: 1941     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 164]---> Sorter-cost: 1941     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 135]---> BDD-cost:  148
c ---[ 134]---> BDD-cost:   23
c ---[ 133]---> BDD-cost:   23
c ---[ 132]---> BDD-cost:   23
c ---[ 131]---> BDD-cost:   23
c ---[ 130]---> BDD-cost:   23
c ---[ 129]---> BDD-cost:   23
c ---[ 128]---> BDD-cost:   26
c ---[ 127]---> BDD-cost:   26
c ---[ 126]---> BDD-cost:   26
c ---[ 125]---> BDD-cost:   26
c ---[ 124]---> BDD-cost:   26
c ---[ 123]---> BDD-cost:   26
c ---[ 122]---> BDD-cost:   26
c ---[ 121]---> BDD-cost:   26
c ---[ 120]---> BDD-cost:   26
c ---[ 119]---> BDD-cost:   26
c ---[ 118]---> BDD-cost:   26
c ---[ 117]---> BDD-cost:   26
c ---[ 115]---> BDD-cost:   25
c ---[ 114]---> BDD-cost:   25
c ---[ 113]---> BDD-cost:   25
c ---[ 112]---> BDD-cost:   25
c ---[ 111]---> BDD-cost:   25
c ---[ 110]---> BDD-cost:   25
c ---[ 109]---> BDD-cost:   25
c ---[ 108]---> BDD-cost:   25
c ---[ 107]---> BDD-cost:   25
c ---[ 106]---> BDD-cost:   25
c ---[ 105]---> BDD-cost:   25
c ---[ 104]---> BDD-cost:   27
c ---[ 103]---> BDD-cost:   27
c ---[ 102]---> BDD-cost:   27
c ---[ 101]---> BDD-cost:   27
c ---[ 100]---> BDD-cost:   27
c ---[  99]---> BDD-cost:   27
c ---[  98]---> BDD-cost:   22
c ---[  97]---> BDD-cost:   22
c ---[  96]---> BDD-cost:   22
c ---[  95]---> BDD-cost:   22
c ---[  94]---> BDD-cost:   22
c ---[  93]---> BDD-cost:   22
c ---[  92]---> BDD-cost:   26
c ---[  91]---> BDD-cost:   26
c ---[  90]---> BDD-cost:   26
c ---[  89]---> BDD-cost:   26
c ---[  88]---> BDD-cost:   26
c ---[  87]---> BDD-cost:   26
c ---[  86]---> BDD-cost:   26
c ---[  85]---> BDD-cost:   26
c ---[  84]---> BDD-cost:   26
c ---[  83]---> BDD-cost:   26
c ---[  82]---> BDD-cost:   26
c ---[  81]---> BDD-cost:   26
c ---[  80]---> BDD-cost:   26
c ---[  79]---> BDD-cost:   26
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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   58171   173898 |   19390       0        0     nan |  0.000 % |
c |       101 |   58132   173812 |   21329      97     7432    76.6 |  8.780 % |
c |       251 |   57582   172244 |   23461     238    11120    46.7 |  9.366 % |
c |       476 |   57522   172103 |   25808     449    15016    33.4 |  9.465 % |
c |       814 |   57285   171316 |   28388     597    15054    25.2 |  9.644 % |
c |      1320 |   56930   170167 |   31227    1085    26049    24.0 |  9.952 % |
c |      2079 |   56586   169348 |   34350    1816    45304    24.9 | 10.526 % |
c |      3218 |   56489   169107 |   37785    2938    82358    28.0 | 10.699 % |
c |      4926 |   56311   168498 |   41564    4556   218527    48.0 | 10.835 % |
c ==============================================================================
c [1mFound solution: 1076964352[0m
c ---[   0]---> BDD-cost:   20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5271 |   55995   167536 |   18665    4830   225170    46.6 | 10.835 % |
c ==============================================================================
c [1mFound solution: 1076947456[0m
c ---[   0]---> BDD-cost:   21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5340 |   55507   166422 |   18502    4890   226414    46.3 | 10.835 % |
c |      5442 |   55507   166422 |   20352    4992   236085    47.3 | 12.149 % |
c ==============================================================================
c [1mFound solution: 1076900864[0m
c ---[   0]---> BDD-cost:   20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5569 |   55528   166469 |   18509    5119   244096    47.7 | 12.149 % |
c |      5670 |   55528   166469 |   20359    5220   247204    47.4 | 12.150 % |
c |      5821 |   55519   166438 |   22395    5369   250573    46.7 | 12.157 % |
c |      6047 |   52914   160284 |   24635    5564   255118    45.9 | 16.741 % |
c |      6384 |   52862   160158 |   27099    5893   271670    46.1 | 16.821 % |
c |      6890 |   52862   160158 |   29808    6399   333114    52.1 | 16.821 % |
c |      7650 |   52352   158884 |   32789    7124   352380    49.5 | 17.671 % |
c |      8789 |   52222   158565 |   36068    8253   414040    50.2 | 17.905 % |
c |     10497 |   52134   158263 |   39675    9932   485154    48.8 | 17.961 % |
c |     13061 |   52051   157993 |   43643   12452   585909    47.1 | 18.047 % |
c |     16905 |   51977   157757 |   48007   16281   758756    46.6 | 18.108 % |
c ==============================================================================
c [1mFound solution: 1076880384[0m
c ---[   0]---> BDD-cost:   19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21950 |   51156   155790 |   17052   21253  1085951    51.1 | 18.108 % |
c |     22050 |   51156   155790 |   18757   10727   513729    47.9 | 19.654 % |
c |     22200 |   51156   155790 |   20632   10877   520756    47.9 | 19.654 % |
c |     22427 |   51156   155790 |   22696   11104   540071    48.6 | 19.654 % |
c |     22764 |   51156   155790 |   24965   11441   575411    50.3 | 19.654 % |
c |     23271 |   51111   155635 |   27462   11938   591452    49.5 | 19.685 % |
c |     24030 |   51093   155573 |   30208   12694   630406    49.7 | 19.697 % |
c |     25170 |   51050   155442 |   33229   13822   699257    50.6 | 19.752 % |
c |     26879 |   51001   155278 |   36552   15522   821447    52.9 | 19.789 % |
c ==============================================================================
c [1mFound solution: 1076868608[0m
c ---[   0]---> BDD-cost:   21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28936 |   50882   154867 |   16960   17540   949700    54.1 | 19.789 % |
c |     29039 |   50882   154867 |   18656   17643   952141    54.0 | 19.895 % |
c |     29190 |   50882   154867 |   20521   17794   969905    54.5 | 19.895 % |
c |     29421 |   50882   154867 |   22573   18025   979052    54.3 | 19.895 % |
c |     29758 |   50882   154867 |   24831   18362  1014438    55.2 | 19.895 % |
c |     30265 |   50091   152926 |   27314   18809  1073650    57.1 | 21.360 % |
c ==============================================================================
c [1mFound solution: 1076843520[0m
c ---[   0]---> BDD-cost:   18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30530 |   49814   152283 |   16604   19065  1098747    57.6 | 21.360 % |
c |     30631 |   49814   152283 |   18264   19166  1100477    57.4 | 21.952 % |
c |     30781 |   49806   152257 |   20090   19315  1109769    57.5 | 21.958 % |
c |     31006 |   49806   152257 |   22099   19540  1119143    57.3 | 21.958 % |
c |     31343 |   49806   152257 |   24309   19877  1133582    57.0 | 21.958 % |
c |     31849 |   49748   152122 |   26740   20378  1168990    57.4 | 22.075 % |
c |     32609 |   49748   152122 |   29414   21138  1222866    57.9 | 22.075 % |
c |     33749 |   49748   152122 |   32356   22278  1286227    57.7 | 22.075 % |
c |     35457 |   49739   152091 |   35592   23984  1483501    61.9 | 22.081 % |
c |     38019 |   49681   151919 |   39151   26538  1757628    66.2 | 22.148 % |
c |     41864 |   49646   151808 |   43066   30377  2481999    81.7 | 22.179 % |
c ==============================================================================
c [1mFound solution: 1076835840[0m
c ---[   0]---> BDD-cost:   16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43893 |   49635   151755 |   16545   32404  2805306    86.6 | 22.179 % |
c |     43993 |   49635   151755 |   18199   16302  1661740   101.9 | 22.202 % |
c |     44144 |   49635   151755 |   20019   16453  1668912   101.4 | 22.202 % |
c |     44370 |   49635   151755 |   22021   16679  1733512   103.9 | 22.202 % |
c |     44708 |   49635   151755 |   24223   17017  1789160   105.1 | 22.202 % |
c |     45215 |   49571   151535 |   26645   17510  1828409   104.4 | 22.263 % |
c |     45976 |   49571   151535 |   29310   18271  2002629   109.6 | 22.263 % |
c |     47115 |   49557   151487 |   32241   19409  2134532   110.0 | 22.269 % |
c ==============================================================================
c [1mFound solution: 1076831744[0m
c ---[   0]---> BDD-cost:   19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     47596 |   49577   151534 |   16525   19890  2181717   109.7 | 22.269 % |
c |     47697 |   49577   151534 |   18177   19991  2191723   109.6 | 22.265 % |
c |     47847 |   49577   151534 |   19995   20141  2207453   109.6 | 22.265 % |
c |     48072 |   49577   151534 |   21994   20366  2236047   109.8 | 22.265 % |
c |     48410 |   49577   151534 |   24194   20704  2278546   110.1 | 22.265 % |
c |     48921 |   49559   151472 |   26613   21213  2366062   111.5 | 22.277 % |
c |     49683 |   49550   151441 |   29275   21974  2515580   114.5 | 22.283 % |
c |     50825 |   49550   151441 |   32202   23116  2608821   112.9 | 22.283 % |
c |     52533 |   49541   151410 |   35422   24822  2925765   117.9 | 22.289 % |
c ==============================================================================
c [1mFound solution: 1076822016[0m
c ---[   0]---> BDD-cost:   14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     55046 |   49548   151428 |   16516   27334  3394217   124.2 | 22.289 % |
c |     55148 |   49548   151428 |   18167   13769  1320369    95.9 | 22.301 % |
c |     55299 |   49548   151428 |   19984   13920  1345783    96.7 | 22.301 % |
c |     55525 |   49548   151428 |   21982   14146  1384925    97.9 | 22.301 % |
c |     55866 |   49548   151428 |   24181   14487  1429569    98.7 | 22.301 % |
c |     56372 |   49548   151428 |   26599   14993  1516898   101.2 | 22.301 % |
c |     57131 |   49548   151428 |   29259   15752  1623288   103.1 | 22.301 % |
c |     58271 |   49548   151428 |   32185   16892  1856440   109.9 | 22.301 % |
c |     59979 |   49548   151428 |   35403   18600  2153057   115.8 | 22.301 % |
c |     62544 |   49548   151428 |   38943   21165  2645957   125.0 | 22.301 % |
c |     66390 |   49483   151284 |   42838   25004  2947670   117.9 | 22.405 % |
c ==============================================================================
c [1mFound solution: 1076801024[0m
c ---[   0]---> BDD-cost:   20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     69269 |   49506   151338 |   16502   27883  3500976   125.6 | 22.405 % |
c |     69372 |   49506   151338 |   18152   14045  1208054    86.0 | 22.396 % |
c |     69522 |   49506   151338 |   19967   14195  1235914    87.1 | 22.396 % |
c |     69748 |   49506   151338 |   21964   14421  1270763    88.1 | 22.396 % |
c ==============================================================================
c [1mFound solution: 1076796928[0m
c ---[   0]---> BDD-cost:   19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     69837 |   49518   151356 |   16506   14507  1283000    88.4 | 22.396 % |
c |     69938 |   49518   151356 |   18156   14608  1298896    88.9 | 22.396 % |
c |     70090 |   49518   151356 |   19972   14760  1325230    89.8 | 22.396 % |
c |     70317 |   49518   151356 |   21969   14987  1360231    90.8 | 22.396 % |
c |     70654 |   49518   151356 |   24166   15324  1394300    91.0 | 22.396 % |
c |     71160 |   49518   151356 |   26583   15830  1522421    96.2 | 22.396 % |
c |     71919 |   49510   151338 |   29241   16588  1677890   101.2 | 22.408 % |
c |     73059 |   49510   151338 |   32165   17728  1868791   105.4 | 22.408 % |
c |     74767 |   49510   151338 |   35382   19436  2217347   114.1 | 22.408 % |
c |     77329 |   49510   151338 |   38920   21998  2800862   127.3 | 22.408 % |
c |     81174 |   49496   151290 |   42812   25842  3410796   132.0 | 22.415 % |
c |     86940 |   49413   151046 |   47093   31599  4280012   135.4 | 22.519 % |
c |     95596 |   49387   150958 |   51802   40250  5527965   137.3 | 22.537 % |
c |    108572 |   49387   150958 |   56983   53226  8269961   155.4 | 22.537 % |
c |    128033 |   49293   150700 |   62681   35170  5094862   144.9 | 22.672 % |
c |    157225 |   49276   150651 |   68949   64359  9964945   154.8 | 22.691 % |
c ==============================================================================
c [1mOptimal solution: 1076796928[0m
s OPTIMUM FOUND
v -COL133_bit_10 -COL133_bit_9 -COL133_bit_8 -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 -COL133_bit14 -COL133_bit15 -COL133_bit16 -COL133_bit17 -COL133_bit18 -COL133_bit19 COL133_bit20 -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_10 -COL134_bit_9 -COL134_bit_8 -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 -COL134_bit14 -COL134_bit15 -COL134_bit16 -COL134_bit17 -COL134_bit18 -COL134_bit19 COL134_bit20 -COL135_bit_10 -COL135_bit_9 -COL135_bit_8 -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 -COL135_bit14 -COL135_bit15 -COL135_bit16 -COL135_bit17 -COL135_bit18 -COL135_bit19 COL135_bit20 -COL136_bit_10 -COL136_bit_9 -COL136_bit_8 -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 -COL136_bit14 -COL136_bit15 -COL136_bit16 -COL136_bit17 -COL136_bit18 -COL136_bit19 COL136_bit20 -COL115_bit_10 -COL115_bit_9 -COL115_bit_8 -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 -COL115_bit13 -COL115_bit14 -COL115_bit15 -COL115_bit16 -COL115_bit17 -COL115_bit18 -COL115_bit19 -COL116_bit_10 -COL116_bit_9 -COL116_bit_8 -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 -COL116_bit13 -COL116_bit14 -COL116_bit15 -COL116_bit16 -COL116_bit17 -COL116_bit18 -COL116_bit19 -COL117_bit_10 -COL117_bit_9 -COL117_bit_8 -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 -COL117_bit13 -COL117_bit14 -COL117_bit15 -COL117_bit16 -COL117_bit17 -COL117_bit18 -COL117_bit19 -COL118_bit_10 -COL118_bit_9 -COL118_bit_8 -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 -COL118_bit13 -COL118_bit14 -COL118_bit15 -COL118_bit16 -COL118_bit17 -COL118_bit18 -COL118_bit19 -COL119_bit_10 -COL119_bit_9 -COL119_bit_8 -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 -COL119_bit13 -COL119_bit14 -COL119_bit15 -COL119_bit16 -COL119_bit17 -COL119_bit18 -COL119_bit19 -COL120_bit_10 -COL120_bit_9 -COL120_bit_8 -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 -COL120_bit13 -COL120_bit14 -COL120_bit15 -COL120_bit16 -COL120_bit17 -COL120_bit18 -COL120_bit19 -COL121_bit_10 -COL121_bit_9 -COL121_bit_8 -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 -COL121_bit13 -COL121_bit14 -COL121_bit15 -COL121_bit16 -COL121_bit17 -COL121_bit18 -COL121_bit19 -COL122_bit_10 -COL122_bit_9 -COL122_bit_8 -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 -COL122_bit13 -COL122_bit14 -COL122_bit15 -COL122_bit16 -COL122_bit17 -COL122_bit18 -COL122_bit19 -COL123_bit_10 -COL123_bit_9 -COL123_bit_8 -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 -COL123_bit13 -COL123_bit14 -COL123_bit15 -COL123_bit16 -COL123_bit17 -COL123_bit18 -COL123_bit19 -COL124_bit_10 -COL124_bit_9 -COL124_bit_8 -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 -COL124_bit13 -COL124_bit14 -COL124_bit15 -COL124_bit16 -COL124_bit17 -COL124_bit18 -COL124_bit19 -COL125_bit_10 -COL125_bit_9 -COL125_bit_8 -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 -COL125_bit13 -COL125_bit14 -COL125_bit15 -COL125_bit16 -COL125_bit17 -COL125_bit18 -COL125_bit19 -COL126_bit_10 -COL126_bit_9 -COL126_bit_8 -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 -COL126_bit13 -COL126_bit14 -COL126_bit15 -COL126_bit16 -COL126_bit17 -COL126_bit18 -COL126_bit19 -COL127_bit_10 -COL127_bit_9 -COL127_bit_8 -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 -COL127_bit13 -COL127_bit14 -COL127_bit15 -COL127_bit16 -COL127_bit17 -COL127_bit18 -COL127_bit19 -COL128_bit_10 -COL128_bit_9 -COL128_bit_8 -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 -COL128_bit13 -COL128_bit14 -COL128_bit15 -COL128_bit16 -COL128_bit17 -COL128_bit18 -COL128_bit19 -COL073_bit_10 -COL073_bit_9 -COL073_bit_8 -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 -COL073_bit13 -COL073_bit14 -COL073_bit15 -COL073_bit16 -COL073_bit17 -COL073_bit18 -COL073_bit19 -COL074_bit_10 -COL074_bit_9 -COL074_bit_8 -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 -COL074_bit13 -COL074_bit14 -COL074_bit15 -COL074_bit16 -COL074_bit17 -COL074_bit18 -COL074_bit19 -COL075_bit_10 -COL075_bit_9 -COL075_bit_8 -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 -COL075_bit13 -COL075_bit14 -COL075_bit15 -COL075_bit16 -COL075_bit17 -COL075_bit18 -COL075_bit19 -COL076_bit_10 -COL076_bit_9 -COL076_bit_8 -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 -COL076_bit13 -COL076_bit14 -COL076_bit15 -COL076_bit16 -COL076_bit17 -COL076_bit18 -COL076_bit19 -COL077_bit_10 -COL077_bit_9 -COL077_bit_8 -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 -COL077_bit13 -COL077_bit14 -COL077_bit15 -COL077_bit16 -COL077_bit17 -COL077_bit18 -COL077_bit19 -COL078_bit_10 -COL078_bit_9 -COL078_bit_8 -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 -COL078_bit13 -COL078_bit14 -COL078_bit15 -COL078_bit16 -COL078_bit17 -COL078_bit18 -COL078_bit19 -COL079_bit_10 -COL079_bit_9 -COL079_bit_8 -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 -COL079_bit13 -COL079_bit14 -COL079_bit15 -COL079_bit16 -COL079_bit17 -COL079_bit18 -COL079_bit19 -COL085_bit_10 -COL085_bit_9 -COL085_bit_8 -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 -COL085_bit13 -COL085_bit14 -COL085_bit15 -COL085_bit16 -COL085_bit17 -COL085_bit18 -COL085_bit19 -COL091_bit_10 -COL091_bit_9 -COL091_bit_8 -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 -COL091_bit13 -COL091_bit14 -COL091_bit15 -COL091_bit16 -COL091_bit17 -COL091_bit18 -COL091_bit19 -COL097_bit_10 -COL097_bit_9 -COL097_bit_8 -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 -COL097_bit13 -COL097_bit14 -COL097_bit15 -COL097_bit16 -COL097_bit17 -COL097_bit18 -COL097_bit19 -COL103_bit_10 -COL103_bit_9 -COL103_bit_8 -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 -COL103_bit13 -COL103_bit14 -COL103_bit15 -COL103_bit16 -COL103_bit17 -COL103_bit18 -COL103_bit19 -COL109_bit_10 -COL109_bit_9 -COL109_bit_8 -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 -COL109_bit13 -COL109_bit14 -COL109_bit15 -COL109_bit16 -COL109_bit17 -COL109_bit18 -COL109_bit19 -COL080_bit_10 -COL080_bit_9 -COL080_bit_8 -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 -COL080_bit13 -COL080_bit14 -COL080_bit15 -COL080_bit16 -COL080_bit17 -COL080_bit18 -COL080_bit19 -COL081_bit_10 -COL081_bit_9 -COL081_bit_8 -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 -COL081_bit13 -COL081_bit14 -COL081_bit15 -COL081_bit16 -COL081_bit17 -COL081_bit18 -COL081_bit19 -COL082_bit_10 -COL082_bit_9 -COL082_bit_8 -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 -COL082_bit13 -COL082_bit14 -COL082_bit15 -COL082_bit16 -COL082_bit17 -COL082_bit18 -COL082_bit19 -COL083_bit_10 -COL083_bit_9 -COL083_bit_8 -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 -COL083_bit13 -COL083_bit14 -COL083_bit15 -COL083_bit16 -COL083_bit17 -COL083_bit18 -COL083_bit19 -COL084_bit_10 -COL084_bit_9 -COL084_bit_8 -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 -COL084_bit13 -COL084_bit14 -COL084_bit15 -COL084_bit16 -COL084_bit17 -COL084_bit18 -COL084_bit19 -COL086_bit_10 -COL086_bit_9 -COL086_bit_8 -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 -COL086_bit13 -COL086_bit14 -COL086_bit15 -COL086_bit16 -COL086_bit17 -COL086_bit18 -COL086_bit19 -COL092_bit_10 -COL092_bit_9 -COL092_bit_8 -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 -COL092_bit13 -COL092_bit14 -COL092_bit15 -COL092_bit16 -COL092_bit17 -COL092_bit18 -COL092_bit19 -COL098_bit_10 -COL098_bit_9 -COL098_bit_8 -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 -COL098_bit13 -COL098_bit14 -COL098_bit15 -COL098_bit16 -COL098_bit17 -COL098_bit18 -COL098_bit19 -COL104_bit_10 -COL104_bit_9 -COL104_bit_8 -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 -COL104_bit13 -COL104_bit14 -COL104_bit15 -COL104_bit16 -COL104_bit17 -COL104_bit18 -COL104_bit19 -COL110_bit_10 -COL110_bit_9 -COL110_bit_8 -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 -COL110_bit13 -COL110_bit14 -COL110_bit15 -COL110_bit16 -COL110_bit17 -COL110_bit18 -COL110_bit19 -COL087_bit_10 -COL087_bit_9 -COL087_bit_8 -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 -COL087_bit13 -COL087_bit14 -COL087_bit15 -COL087_bit16 -COL087_bit17 -COL087_bit18 -COL087_bit19 -COL088_bit_10 -COL088_bit_9 -COL088_bit_8 -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 -COL088_bit13 -COL088_bit14 -COL088_bit15 -COL088_bit16 -COL088_bit17 -COL088_bit18 -COL088_bit19 -COL089_bit_10 -COL089_bit_9 -COL089_bit_8 -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 -COL089_bit13 -COL089_bit14 -COL089_bit15 -COL089_bit16 -COL089_bit17 -COL089_bit18 -COL089_bit19 -COL090_bit_10 -COL090_bit_9 -COL090_bit_8 -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 -COL090_bit13 -COL090_bit14 -COL090_bit15 -COL090_bit16 -COL090_bit17 -COL090_bit18 -COL090_bit19 -COL093_bit_10 -COL093_bit_9 -COL093_bit_8 -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 -COL093_bit13 -COL093_bit14 -COL093_bit15 -COL093_bit16 -COL093_bit17 -COL093_bit18 -COL093_bit19 -COL099_bit_10 -COL099_bit_9 -COL099_bit_8 -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 -COL099_bit13 -COL099_bit14 -COL099_bit15 -COL099_bit16 -COL099_bit17 -COL099_bit18 -COL099_bit19 -COL105_bit_10 -COL105_bit_9 -COL105_bit_8 -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 -COL105_bit13 -COL105_bit14 -COL105_bit15 -COL105_bit16 -COL105_bit17 -COL105_bit18 -COL105_bit19 -COL111_bit_10 -COL111_bit_9 -COL111_bit_8 -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 -COL111_bit13 -COL111_bit14 -COL111_bit15 -COL111_bit16 -COL111_bit17 -COL111_bit18 -COL111_bit19 -COL094_bit_10 -COL094_bit_9 -COL094_bit_8 -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 -COL094_bit13 -COL094_bit14 -COL094_bit15 -COL094_bit16 -COL094_bit17 -COL094_bit18 -COL094_bit19 -COL095_bit_10 -COL095_bit_9 -COL095_bit_8 -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 -COL095_bit13 -COL095_bit14 -COL095_bit15 -COL095_bit16 -COL095_bit17 -COL095_bit18 -COL095_bit19 -COL096_bit_10 -COL096_bit_9 -COL096_bit_8 -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 -COL096_bit13 -COL096_bit14 -COL096_bit15 -COL096_bit16 -COL096_bit17 -COL096_bit18 -COL096_bit19 -COL100_bit_10 -COL100_bit_9 -COL100_bit_8 -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 -COL100_bit13 -COL100_bit14 -COL100_bit15 -COL100_bit16 -COL100_bit17 -COL100_bit18 -COL100_bit19 -COL106_bit_10 -COL106_bit_9 -COL106_bit_8 -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 -COL106_bit13 -COL106_bit14 -COL106_bit15 -COL106_bit16 -COL106_bit17 -COL106_bit18 -COL106_bit19 -COL112_bit_10 -COL112_bit_9 -COL112_bit_8 -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 -COL112_bit13 -COL112_bit14 -COL112_bit15 -COL112_bit16 -COL112_bit17 -COL112_bit18 -COL112_bit19 -COL101_bit_10 -COL101_bit_9 -COL101_bit_8 -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 -COL101_bit13 -COL101_bit14 -COL101_bit15 -COL101_bit16 -COL101_bit17 -COL101_bit18 -COL101_bit19 -COL102_bit_10 -COL102_bit_9 -COL102_bit_8 -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 -COL102_bit13 -COL102_bit14 -COL102_bit15 -COL102_bit16 -COL102_bit17 -COL102_bit18 -COL102_bit19 -COL107_bit_10 -COL107_bit_9 -COL107_bit_8 -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 -COL107_bit13 -COL107_bit14 -COL107_bit15 -COL107_bit16 -COL107_bit17 -COL107_bit18 -COL107_bit19 -COL113_bit_10 -COL113_bit_9 -COL113_bit_8 -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 -COL113_bit13 -COL113_bit14 -COL113_bit15 -COL113_bit16 -COL113_bit17 -COL113_bit18 -COL113_bit19 -COL108_bit_10 -COL108_bit_9 -COL108_bit_8 -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 -COL108_bit13 -COL108_bit14 -COL108_bit15 -COL108_bit16 -COL108_bit17 -COL108_bit18 -COL108_bit19 -COL114_bit_10 -COL114_bit_9 -COL114_bit_8 -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 -COL114_bit13 -COL114_bit14 -COL114_bit15 -COL114_bit16 -COL114_bit17 -COL114_bit18 -COL114_bit19 -COL131_bit_10 -COL131_bit_9 -COL131_bit_8 -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 -COL131_bit14 -COL131_bit15 -COL131_bit16 -COL131_bit17 -COL131_bit18 -COL131_bit19 COL131_bit20 -COL132_bit_10 -COL132_bit_9 -COL132_bit_8 -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 -COL132_bit14 -COL132_bit15 -COL132_bit16 -COL132_bit17 -COL132_bit18 -COL132_bit19 COL132_bit20
c _______________________________________________________________________________
c 
c restarts              : 97
c conflicts             : 164435         (173 /sec)
c decisions             : 316278         (332 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 952.129 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.88 0.94 0.97 2/54 4018
Raw data (stat): 4018 (runsolver) R 4017 20001 20000 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 841146137 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 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.0011 s]
Raw data (loadavg): 0.90 0.94 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0017 s]
Raw data (loadavg): 0.91 0.95 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0019 s]
Raw data (loadavg): 0.93 0.95 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0025 s]
Raw data (loadavg): 0.94 0.95 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0029 s]
Raw data (loadavg): 0.95 0.95 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.003 s]
Raw data (loadavg): 0.95 0.95 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0037 s]
Raw data (loadavg): 0.96 0.95 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0033 s]
Raw data (loadavg): 0.97 0.95 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0033 s]
Raw data (loadavg): 0.97 0.95 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.003 s]
Raw data (loadavg): 0.98 0.95 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.004 s]
Raw data (loadavg): 0.98 0.95 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.005 s]
Raw data (loadavg): 0.98 0.96 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.004 s]
Raw data (loadavg): 0.98 0.96 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.005 s]
Raw data (loadavg): 0.99 0.96 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.005 s]
Raw data (loadavg): 0.99 0.96 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.006 s]
Raw data (loadavg): 0.99 0.96 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.005 s]
Raw data (loadavg): 0.99 0.96 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.005 s]
Raw data (loadavg): 0.99 0.96 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.006 s]
Raw data (loadavg): 0.99 0.96 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.006 s]
Raw data (loadavg): 0.99 0.96 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.007 s]
Raw data (loadavg): 0.99 0.96 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.011 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.011 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.011 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.011 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.011 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.011 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.015 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.015 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.016 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.016 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.016 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.019 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.019 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.019 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.019 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.019 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.019 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.022 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.022 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4022
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.022 s]
Raw data (loadavg): 0.99 0.97 0.97 2/59 4026
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.023 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4075
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.024 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4075
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.024 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4075
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.024 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4075
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.024 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4075
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.025 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4075
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.025 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4075
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.025 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4077
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.026 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4077
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.027 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4077
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.028 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4077
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.028 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4077
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.028 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4077
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.029 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4077
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.03 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 4077
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+952.477 s]
Raw data (loadavg): 0.99 0.97 0.97 1/53 4077
Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 30
Real time (s): 952.477
CPU time (s): 952.576
CPU user time (s): 952.145
CPU system time (s): 0.430934
CPU usage (%): 100.01
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	1076796928
#### END VERIFIER DATA ####