PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-lseu.opb
MD5SUM	99657262afbbfce7034a3ec6b29d9b3b
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1120
Optimality of the best value was proved	NO
Number of terms in the objective function	85
Biggest coefficient in the objective function	517
Number of bits for the biggest coefficient in the objective function	10
Sum of the numbers in the objective function	15494
Number of bits of the sum of numbers in the objective function	14
Biggest number in a constraint	1656
Number of bits of the biggest number in a constraint	11
Biggest sum of numbers in a constraint	15494
Number of bits of the biggest sum of numbers	14
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02984
Number of variables	89
Total number of constraints	117
Number of constraints which are clauses	2
Number of constraints which are cardinality constraints (but not clauses)	104
Number of constraints which are nor clauses,nor cardinality constraints	11
Minimum length of a constraint	1
Maximum length of a constraint	47
Trace number 21267

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-04-21 23:22:54 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13499 boxname=wulflinc20 idbench=1039 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  99657262afbbfce7034a3ec6b29d9b3b  /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-lseu.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-lseu.opb
IDLAUNCH: 13499
/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:        659256 kB
Buffers:         25776 kB
Cached:         326696 kB
SwapCached:        516 kB
Active:          57036 kB
Inactive:       297424 kB
HighTotal:      131008 kB
HighFree:          392 kB
LowTotal:       903652 kB
LowFree:        658864 kB
SwapTotal:     2097892 kB
SwapFree:      2096480 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5116 kB
Slab:            15332 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 23:33:47 (client local time) WITH STATUS 30 IN 653.18 SECONDS
stats: 13499 0 653.18 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 28 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #
c   -- Clauses(.)/Splits(s): ...s..
c ---[  28]---> BDD-cost:    3
c ---[  27]---> BDD-cost:    7
c ---[  26]---> BDD-cost:    5
c ---[  24]---> BDD-cost:    3
c ---[  23]---> BDD-cost:    5
c ---[  22]---> BDD-cost:   11
c ---[  21]---> BDD-cost:    3
c ---[  20]---> BDD-cost:    7
c ---[  19]---> BDD-cost:    3
c ---[  18]---> BDD-cost:    7
c ---[  17]---> BDD-cost:    5
c ---[  16]---> BDD-cost:    7
c ---[  15]---> BDD-cost:    5
c ---[  14]---> BDD-cost:    3
c ---[  12]---> BDD-cost:    7
c ---[   9]---> Sorter-cost: 3170     Base: 5 2 2 3
c ---[   8]---> BDD-cost:   28
c ---[   7]---> BDD-cost:  202
c ---[   6]---> Sorter-cost: 1878     Base: 5 2 2 3
c ---[   4]---> Sorter-cost: 1741     Base: 5 2 2 2
c ---[   2]---> BDD-cost:   16
c ---[   0]---> BDD-cost:   32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   16046    38074 |    5348       0        0     nan |  0.000 % |
c |       101 |   15986    37942 |    5882      99     1341    13.5 |  0.826 % |
c ==============================================================================
c [1mFound solution: 3697[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:12454     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       202 |   44688   105076 |   14896     173     2195    12.7 |  0.826 % |
c ==============================================================================
c [1mFound solution: 3371[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       256 |   44990   105888 |   14996     226     2982    13.2 |  0.826 % |
c |       356 |   43633   102789 |   16495     292     3359    11.5 |  3.986 % |
c |       507 |   43603   102719 |   18145     441     4465    10.1 |  4.039 % |
c |       733 |   42927   101162 |   19959     655     8311    12.7 |  5.281 % |
c |      1070 |   42674   100581 |   21955     987    12553    12.7 |  5.716 % |
c |      1581 |   41908    98827 |   24151    1477    21494    14.6 |  7.053 % |
c ==============================================================================
c [1mFound solution: 3322[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1681 |   41980    99026 |   13993    1559    22101    14.2 |  7.053 % |
c ==============================================================================
c [1mFound solution: 3266[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1699 |   42327    99876 |   14109    1577    22632    14.4 |  7.053 % |
c |      1799 |   42177    99527 |   15519    1666    25015    15.0 |  7.434 % |
c ==============================================================================
c [1mFound solution: 3256[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1848 |   42261    99747 |   14087    1715    26486    15.4 |  7.434 % |
c |      1948 |   42261    99747 |   15495    1815    27050    14.9 |  7.424 % |
c |      2099 |   42224    99662 |   17045    1963    29077    14.8 |  7.494 % |
c ==============================================================================
c [1mFound solution: 2378[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2173 |   42342    99948 |   14114    2037    30298    14.9 |  7.494 % |
c |      2273 |   40889    96607 |   15525    2082    31508    15.1 | 10.064 % |
c |      2423 |   40747    96295 |   17077    2230    38797    17.4 | 10.314 % |
c ==============================================================================
c [1mFound solution: 2053[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2639 |   40757    96342 |   13585    2445    47397    19.4 | 10.314 % |
c |      2740 |   40697    96205 |   14943    2543    49595    19.5 | 10.462 % |
c |      2891 |   40697    96205 |   16437    2694    52472    19.5 | 10.462 % |
c |      3119 |   40389    95500 |   18081    2918    57025    19.5 | 11.032 % |
c |      3458 |   40186    95030 |   19889    3252    68502    21.1 | 11.363 % |
c ==============================================================================
c [1mFound solution: 2037[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3836 |   40320    95376 |   13440    3628    85309    23.5 | 11.363 % |
c |      3936 |   40286    95298 |   14784    3716    86903    23.4 | 11.496 % |
c ==============================================================================
c [1mFound solution: 1955[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3980 |   40237    95215 |   13412    3759    88809    23.6 | 11.496 % |
c |      4080 |   40237    95215 |   14753    3859    89989    23.3 | 11.595 % |
c |      4230 |   40237    95215 |   16228    4009    94858    23.7 | 11.595 % |
c |      4455 |   40237    95215 |   17851    4234   106663    25.2 | 11.595 % |
c |      4792 |   40237    95215 |   19636    4571   129714    28.4 | 11.595 % |
c |      5299 |   40168    95064 |   21600    5070   155326    30.6 | 11.728 % |
c |      6058 |   40067    94833 |   23760    5826   206079    35.4 | 11.936 % |
c |      7198 |   40035    94764 |   26136    6963   270614    38.9 | 12.011 % |
c |      8909 |   37164    88133 |   28749    8599   344207    40.0 | 17.102 % |
c ==============================================================================
c [1mFound solution: 1950[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10282 |   36034    85530 |   12011    9929   416384    41.9 | 17.102 % |
c |     10387 |   36034    85530 |   13212   10034   417773    41.6 | 19.346 % |
c |     10537 |   36034    85530 |   14533   10184   421049    41.3 | 19.346 % |
c |     10765 |   36034    85530 |   15986   10412   430808    41.4 | 19.346 % |
c |     11102 |   36034    85530 |   17585   10749   448087    41.7 | 19.346 % |
c |     11608 |   36034    85530 |   19343   11255   462432    41.1 | 19.346 % |
c ==============================================================================
c [1mFound solution: 1850[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11882 |   36052    85587 |   12017   11529   471731    40.9 | 19.346 % |
c |     11982 |   36052    85587 |   13218   11629   474845    40.8 | 19.338 % |
c ==============================================================================
c [1mFound solution: 1841[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12017 |   36059    85619 |   12019   11664   476260    40.8 | 19.338 % |
c |     12117 |   36059    85619 |   13220   11764   482121    41.0 | 19.338 % |
c |     12267 |   36059    85619 |   14542   11914   488323    41.0 | 19.338 % |
c |     12493 |   36004    85490 |   15997   12135   500186    41.2 | 19.453 % |
c |     12831 |   36004    85490 |   17597   12473   513216    41.1 | 19.453 % |
c |     13339 |   35900    85252 |   19356   12973   535678    41.3 | 19.631 % |
c |     14098 |   35900    85252 |   21292   13732   565749    41.2 | 19.631 % |
c |     15238 |   35900    85252 |   23421   14872   632272    42.5 | 19.631 % |
c |     16946 |   35900    85252 |   25763   16580   718187    43.3 | 19.631 % |
c |     19508 |   35861    85162 |   28340   19141   820839    42.9 | 19.706 % |
c ==============================================================================
c [1mFound solution: 1831[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20797 |   35868    85178 |   11956   20430   868635    42.5 | 19.706 % |
c ==============================================================================
c [1mFound solution: 1800[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20822 |   35875    85194 |   11958   10240   370925    36.2 | 19.706 % |
c |     20922 |   35875    85194 |   13153   10340   376338    36.4 | 19.709 % |
c |     21073 |   35820    85065 |   14469   10484   379199    36.2 | 19.812 % |
c |     21298 |   35820    85065 |   15916   10709   384451    35.9 | 19.812 % |
c |     21635 |   35820    85065 |   17507   11046   403641    36.5 | 19.812 % |
c |     22141 |   35797    85013 |   19258   11551   425009    36.8 | 19.852 % |
c ==============================================================================
c [1mFound solution: 1729[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22401 |   35807    85052 |   11935   11811   435927    36.9 | 19.852 % |
c |     22503 |   35807    85052 |   13128   11913   437731    36.7 | 19.850 % |
c |     22654 |   35807    85052 |   14441   12064   440540    36.5 | 19.850 % |
c |     22882 |   35807    85052 |   15885   12292   449714    36.6 | 19.850 % |
c |     23220 |   35605    84581 |   17474   12628   457488    36.2 | 20.188 % |
c ==============================================================================
c [1mFound solution: 1727[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23653 |   35611    84596 |   11870   13061   479394    36.7 | 20.188 % |
c ==============================================================================
c [1mFound solution: 1683[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23732 |   35616    84608 |   11872   13140   483575    36.8 | 20.188 % |
c |     23832 |   35616    84608 |   13059   13240   487557    36.8 | 20.192 % |
c |     23983 |   35616    84608 |   14365   13391   493894    36.9 | 20.192 % |
c ==============================================================================
c [1mFound solution: 1675[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24036 |   35621    84619 |   11873   13444   495347    36.8 | 20.192 % |
c |     24136 |   35621    84619 |   13060   13544   503809    37.2 | 20.194 % |
c |     24286 |   35621    84619 |   14366   13694   506670    37.0 | 20.194 % |
c |     24512 |   35621    84619 |   15802   13920   519039    37.3 | 20.194 % |
c |     24849 |   35621    84619 |   17383   14257   537179    37.7 | 20.194 % |
c |     25355 |   35621    84619 |   19121   14763   550379    37.3 | 20.194 % |
c |     26114 |   35023    83235 |   21033   15466   571637    37.0 | 21.324 % |
c |     27253 |   35023    83235 |   23137   16605   619296    37.3 | 21.324 % |
c |     28963 |   35023    83235 |   25450   18315   687059    37.5 | 21.324 % |
c ==============================================================================
c [1mFound solution: 1614[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29392 |   35028    83246 |   11676   18744   708385    37.8 | 21.324 % |
c |     29492 |   35028    83246 |   12843    9472   290847    30.7 | 21.327 % |
c |     29642 |   34964    83098 |   14127    9621   294252    30.6 | 21.447 % |
c |     29869 |   34964    83098 |   15540    9848   299169    30.4 | 21.447 % |
c |     30208 |   34964    83098 |   17094   10187   308569    30.3 | 21.447 % |
c |     30714 |   34964    83098 |   18804   10693   320449    30.0 | 21.447 % |
c ==============================================================================
c [1mFound solution: 1587[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     31206 |   34978    83134 |   11659   11185   339724    30.4 | 21.447 % |
c |     31306 |   34978    83134 |   12824   11285   341955    30.3 | 21.442 % |
c |     31457 |   34978    83134 |   14107   11436   349352    30.5 | 21.442 % |
c ==============================================================================
c [1mFound solution: 1570[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     31521 |   34985    83154 |   11661   11500   352534    30.7 | 21.442 % |
c |     31623 |   34985    83154 |   12827   11602   354369    30.5 | 21.442 % |
c |     31774 |   34985    83154 |   14109   11753   356599    30.3 | 21.442 % |
c |     32001 |   34985    83154 |   15520   11980   363253    30.3 | 21.442 % |
c |     32340 |   34985    83154 |   17072   12319   378819    30.8 | 21.442 % |
c |     32847 |   34985    83154 |   18780   12826   388215    30.3 | 21.442 % |
c |     33608 |   34985    83154 |   20658   13587   426121    31.4 | 21.442 % |
c |     34748 |   34985    83154 |   22723   14727   487779    33.1 | 21.442 % |
c |     36457 |   34985    83154 |   24996   16436   583123    35.5 | 21.442 % |
c |     39020 |   34801    82731 |   27496   18992   681940    35.9 | 21.745 % |
c ==============================================================================
c [1mFound solution: 1517[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     41774 |   34808    82747 |   11602   21746   853274    39.2 | 21.745 % |
c |     41875 |   34808    82747 |   12762   10974   412117    37.6 | 21.746 % |
c |     42025 |   34808    82747 |   14038   11124   417783    37.6 | 21.746 % |
c |     42251 |   34808    82747 |   15442   11350   422061    37.2 | 21.746 % |
c |     42591 |   34808    82747 |   16986   11690   428663    36.7 | 21.746 % |
c |     43099 |   34808    82747 |   18685   12198   438542    36.0 | 21.746 % |
c |     43858 |   34808    82747 |   20553   12957   454152    35.1 | 21.746 % |
c |     44997 |   34808    82747 |   22609   14096   515846    36.6 | 21.746 % |
c ==============================================================================
c [1mFound solution: 1516[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45960 |   34815    82763 |   11605   15059   573361    38.1 | 21.746 % |
c |     46063 |   34815    82763 |   12765   15162   578306    38.1 | 21.747 % |
c |     46214 |   34815    82763 |   14042   15313   582046    38.0 | 21.747 % |
c |     46439 |   34815    82763 |   15446   15538   589238    37.9 | 21.747 % |
c ==============================================================================
c [1mFound solution: 1503[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     46460 |   34820    82775 |   11606   15559   589681    37.9 | 21.747 % |
c |     46561 |   34820    82775 |   12766    7881   213609    27.1 | 21.749 % |
c |     46712 |   34820    82775 |   14043    8032   219155    27.3 | 21.749 % |
c |     46941 |   34820    82775 |   15447    8261   225582    27.3 | 21.749 % |
c |     47278 |   34820    82775 |   16992    8598   236302    27.5 | 21.749 % |
c |     47785 |   34820    82775 |   18691    9105   253128    27.8 | 21.749 % |
c |     48545 |   34652    82385 |   20560    9857   279243    28.3 | 22.070 % |
c ==============================================================================
c [1mFound solution: 1455[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     48864 |   34640    82360 |   11546   10174   303361    29.8 | 22.070 % |
c |     48966 |   34640    82360 |   12700   10276   305980    29.8 | 22.094 % |
c |     49117 |   34640    82360 |   13970   10427   313871    30.1 | 22.094 % |
c |     49342 |   34640    82360 |   15367   10652   325753    30.6 | 22.094 % |
c |     49679 |   34640    82360 |   16904   10989   339980    30.9 | 22.094 % |
c |     50187 |   34640    82360 |   18594   11497   359131    31.2 | 22.094 % |
c |     50948 |   34640    82360 |   20454   12258   394268    32.2 | 22.094 % |
c ==============================================================================
c [1mFound solution: 1417[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     51133 |   34643    82367 |   11547   12443   404938    32.5 | 22.094 % |
c |     51233 |   34643    82367 |   12701   12543   406841    32.4 | 22.098 % |
c |     51383 |   34643    82367 |   13971   12693   415156    32.7 | 22.098 % |
c |     51608 |   34602    82270 |   15369   12916   422055    32.7 | 22.178 % |
c |     51947 |   34602    82270 |   16905   13255   442806    33.4 | 22.178 % |
c |     52453 |   34602    82270 |   18596   13761   461213    33.5 | 22.178 % |
c ==============================================================================
c [1mFound solution: 1404[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     52597 |   34606    82280 |   11535   13905   467095    33.6 | 22.178 % |
c |     52697 |   34606    82280 |   12688   14005   470183    33.6 | 22.180 % |
c |     52848 |   34606    82280 |   13957   14156   476842    33.7 | 22.180 % |
c |     53074 |   34606    82280 |   15353   14382   483083    33.6 | 22.180 % |
c |     53411 |   34606    82280 |   16888   14719   490781    33.3 | 22.180 % |
c |     53918 |   34606    82280 |   18577   15226   502335    33.0 | 22.180 % |
c |     54677 |   34292    81543 |   20434   15982   546741    34.2 | 22.723 % |
c |     55816 |   34292    81543 |   22478   17121   612088    35.8 | 22.723 % |
c ==============================================================================
c [1mFound solution: 1375[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     56923 |   34297    81555 |   11432   18228   678540    37.2 | 22.723 % |
c |     57023 |   34297    81555 |   12575    9214   293213    31.8 | 22.725 % |
c ==============================================================================
c [1mFound solution: 1356[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     57139 |   34304    81571 |   11434    9330   295845    31.7 | 22.725 % |
c |     57241 |   34304    81571 |   12577    9432   297556    31.5 | 22.726 % |
c |     57391 |   34304    81571 |   13835    9582   300893    31.4 | 22.726 % |
c |     57616 |   34304    81571 |   15218    9807   310558    31.7 | 22.726 % |
c ==============================================================================
c [1mFound solution: 1337[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     57898 |   34309    81583 |   11436   10089   322077    31.9 | 22.726 % |
c |     57998 |   34309    81583 |   12579   10189   323845    31.8 | 22.728 % |
c |     58149 |   34259    81469 |   13837   10339   326150    31.5 | 22.819 % |
c |     58374 |   34241    81428 |   15221   10562   336472    31.9 | 22.853 % |
c |     58711 |   34241    81428 |   16743   10899   361196    33.1 | 22.853 % |
c |     59217 |   34241    81428 |   18417   11405   371956    32.6 | 22.853 % |
c |     59976 |   34168    81259 |   20259   12161   416868    34.3 | 22.991 % |
c |     61115 |   34082    81059 |   22285   13297   472342    35.5 | 23.151 % |
c ==============================================================================
c [1mFound solution: 1312[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     61210 |   34089    81075 |   11363   13392   476347    35.6 | 23.151 % |
c |     61311 |   34089    81075 |   12499   13493   483194    35.8 | 23.151 % |
c |     61461 |   34089    81075 |   13749   13643   489705    35.9 | 23.151 % |
c |     61686 |   34089    81075 |   15124   13868   501226    36.1 | 23.151 % |
c ==============================================================================
c [1mFound solution: 1311[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     61812 |   34094    81087 |   11364   13994   506283    36.2 | 23.151 % |
c ==============================================================================
c [1mFound solution: 1308[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     61823 |   34101    81103 |   11367   14005   506542    36.2 | 23.151 % |
c |     61923 |   34101    81103 |   12503   14105   513908    36.4 | 23.154 % |
c |     62075 |   34101    81103 |   13754   14257   521363    36.6 | 23.153 % |
c |     62300 |   34101    81103 |   15129   14482   535416    37.0 | 23.153 % |
c |     62639 |   34043    80967 |   16642   14820   543359    36.7 | 23.262 % |
c |     63145 |   33977    80813 |   18306   15325   570800    37.2 | 23.394 % |
c ==============================================================================
c [1mFound solution: 1276[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     63370 |   33993    80853 |   11331   15550   584365    37.6 | 23.394 % |
c |     63474 |   33993    80853 |   12464    7879   229194    29.1 | 23.386 % |
c |     63624 |   33993    80853 |   13710    8029   235781    29.4 | 23.386 % |
c |     63852 |   33993    80853 |   15081    8257   241118    29.2 | 23.386 % |
c |     64190 |   33993    80853 |   16589    8595   255628    29.7 | 23.386 % |
c |     64696 |   33993    80853 |   18248    9101   265330    29.2 | 23.386 % |
c |     65457 |   33993    80853 |   20073    9862   281658    28.6 | 23.386 % |
c |     66597 |   33993    80853 |   22080   11002   307035    27.9 | 23.386 % |
c |     68305 |   33993    80853 |   24289   12710   368240    29.0 | 23.386 % |
c ==============================================================================
c [1mFound solution: 1261[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     68916 |   33997    80865 |   11332   13321   404243    30.3 | 23.386 % |
c |     69017 |   33997    80865 |   12465   13422   410227    30.6 | 23.388 % |
c |     69167 |   33997    80865 |   13711   13572   415038    30.6 | 23.388 % |
c |     69392 |   33997    80865 |   15082   13797   425319    30.8 | 23.388 % |
c |     69730 |   33997    80865 |   16591   14135   433786    30.7 | 23.388 % |
c |     70236 |   33997    80865 |   18250   14641   444412    30.4 | 23.388 % |
c |     70995 |   33997    80865 |   20075   15400   501489    32.6 | 23.388 % |
c ==============================================================================
c [1mFound solution: 1249[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     71760 |   34004    80893 |   11334   16165   543216    33.6 | 23.388 % |
c |     71861 |   34004    80893 |   12467    8184   240743    29.4 | 23.387 % |
c |     72011 |   34004    80893 |   13714    8334   248316    29.8 | 23.387 % |
c |     72237 |   34000    80884 |   15085    8559   258603    30.2 | 23.392 % |
c |     72578 |   34000    80884 |   16594    8900   269183    30.2 | 23.392 % |
c |     73084 |   34000    80884 |   18253    9406   290102    30.8 | 23.392 % |
c ==============================================================================
c [1mFound solution: 1233[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     73571 |   34004    80894 |   11334    9893   312372    31.6 | 23.392 % |
c |     73671 |   34004    80894 |   12467    9993   316963    31.7 | 23.394 % |
c |     73821 |   34004    80894 |   13714   10143   323069    31.9 | 23.394 % |
c |     74047 |   34004    80894 |   15085   10369   327866    31.6 | 23.394 % |
c |     74385 |   34004    80894 |   16594   10707   342711    32.0 | 23.394 % |
c |     74894 |   34004    80894 |   18253   11216   372879    33.2 | 23.394 % |
c ==============================================================================
c [1mFound solution: 1219[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     75485 |   34009    80905 |   11336   11807   403318    34.2 | 23.394 % |
c |     75585 |   34009    80905 |   12469   11907   407498    34.2 | 23.396 % |
c |     75735 |   34009    80905 |   13716   12057   413667    34.3 | 23.396 % |
c |     75961 |   34009    80905 |   15088   12283   419498    34.2 | 23.396 % |
c |     76300 |   34009    80905 |   16597   12622   434871    34.5 | 23.396 % |
c |     76810 |   34009    80905 |   18256   13132   456938    34.8 | 23.396 % |
c |     77569 |   34009    80905 |   20082   13891   495418    35.7 | 23.396 % |
c ==============================================================================
c [1mFound solution: 1215[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     78703 |   34014    80916 |   11338   15025   556512    37.0 | 23.396 % |
c |     78803 |   34014    80916 |   12471   15125   560304    37.0 | 23.398 % |
c |     78955 |   34014    80916 |   13718   15277   567187    37.1 | 23.397 % |
c |     79180 |   34014    80916 |   15090   15502   570412    36.8 | 23.397 % |
c |     79517 |   34014    80916 |   16599   15839   574576    36.3 | 23.397 % |
c |     80024 |   34014    80916 |   18259   16346   584008    35.7 | 23.397 % |
c |     80783 |   33957    80784 |   20085   17103   609563    35.6 | 23.506 % |
c |     81922 |   33957    80784 |   22094   18242   652586    35.8 | 23.506 % |
c |     83631 |   33957    80784 |   24304   19951   738171    37.0 | 23.506 % |
c |     86193 |   33957    80784 |   26734   22513   862647    38.3 | 23.506 % |
c ==============================================================================
c [1mFound solution: 1194[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86651 |   33964    80800 |   11321   22971   879386    38.3 | 23.506 % |
c ==============================================================================
c [1mFound solution: 1149[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86700 |   33968    80809 |   11322   11535   366925    31.8 | 23.506 % |
c ==============================================================================
c [1mFound solution: 1145[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86718 |   33973    80820 |   11324   11553   367741    31.8 | 23.506 % |
c |     86822 |   33973    80820 |   12456   11657   372147    31.9 | 23.512 % |
c |     86973 |   33973    80820 |   13702   11808   379427    32.1 | 23.512 % |
c |     87198 |   33973    80820 |   15072   12033   388418    32.3 | 23.512 % |
c ==============================================================================
c [1mFound solution: 1136[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     87295 |   33982    80843 |   11327   12130   392054    32.3 | 23.512 % |
c |     87395 |   33982    80843 |   12459   12230   397615    32.5 | 23.510 % |
c |     87546 |   33982    80843 |   13705   12381   401852    32.5 | 23.510 % |
c |     87771 |   33982    80843 |   15076   12606   408267    32.4 | 23.510 % |
c |     88111 |   33982    80843 |   16583   12946   416712    32.2 | 23.510 % |
c |     88617 |   33982    80843 |   18242   13452   438552    32.6 | 23.510 % |
c |     89376 |   33982    80843 |   20066   14211   467515    32.9 | 23.510 % |
c |     90515 |   33982    80843 |   22073   15350   505978    33.0 | 23.510 % |
c |     92223 |   33982    80843 |   24280   17058   574942    33.7 | 23.510 % |
c |     94785 |   33946    80759 |   26708   19618   651326    33.2 | 23.573 % |
c ==============================================================================
c [1mFound solution: 1128[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     98336 |   33952    80774 |   11317   23169   802322    34.6 | 23.573 % |
c |     98438 |   33952    80774 |   12448   11687   310808    26.6 | 23.573 % |
c |     98588 |   33952    80774 |   13693   11837   317230    26.8 | 23.573 % |
c |     98817 |   33952    80774 |   15062   12066   326295    27.0 | 23.573 % |
c |     99155 |   33952    80774 |   16569   12404   336095    27.1 | 23.573 % |
c |     99661 |   33952    80774 |   18226   12910   359193    27.8 | 23.573 % |
c |    100420 |   33952    80774 |   20048   13669   396157    29.0 | 23.573 % |
c |    101560 |   33952    80774 |   22053   14809   437250    29.5 | 23.573 % |
c |    103268 |   33952    80774 |   24258   16517   516374    31.3 | 23.573 % |
c |    105830 |   33952    80774 |   26684   19079   624783    32.7 | 23.573 % |
c |    109676 |   33952    80774 |   29353   22925   762667    33.3 | 23.573 % |
c |    115442 |   33952    80774 |   32288   28691   989080    34.5 | 23.573 % |
c |    124092 |   33952    80774 |   35517   37341  1393060    37.3 | 23.573 % |
c ==============================================================================
c [1mFound solution: 1120[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    136193 |   33955    80781 |   11318   26816  1021714    38.1 | 23.573 % |
c |    136293 |   33955    80781 |   12449   13508   480514    35.6 | 23.576 % |
c |    136444 |   33939    80744 |   13694   13658   485170    35.5 | 23.605 % |
c |    136669 |   33939    80744 |   15064   13883   491212    35.4 | 23.605 % |
c |    137006 |   33939    80744 |   16570   14220   500993    35.2 | 23.605 % |
c |    137516 |   33939    80744 |   18227   14730   521903    35.4 | 23.605 % |
c |    138276 |   33939    80744 |   20050   15490   536341    34.6 | 23.605 % |
c |    139416 |   33939    80744 |   22055   16630   592086    35.6 | 23.605 % |
c |    141124 |   33939    80744 |   24261   18338   662753    36.1 | 23.605 % |
c |    143686 |   33939    80744 |   26687   20900   767136    36.7 | 23.605 % |
c |    147530 |   33939    80744 |   29355   24744   895353    36.2 | 23.605 % |
c |    153296 |   33793    80407 |   32291   30507  1148443    37.6 | 23.901 % |
c ==============================================================================
c [1mOptimal solution: 1120[0m
s OPTIMUM FOUND
v C101_bit0 C102_bit0 -C103_bit0 -C104_bit0 -C105_bit0 -C108_bit0 -C111_bit0 -C112_bit0 -C113_bit0 C114_bit0 -C115_bit0 -C116_bit0 -C117_bit0 -C118_bit0 -C119_bit0 -C120_bit0 -C121_bit0 -C122_bit0 -C123_bit0 -C124_bit0 -C125_bit0 -C126_bit0 C127_bit0 -C128_bit0 -C129_bit0 -C130_bit0 -C131_bit0 -C132_bit0 -C133_bit0 -C134_bit0 C135_bit0 -C136_bit0 -C137_bit0 -C138_bit0 C139_bit0 -C140_bit0 -C141_bit0 -C142_bit0 C143_bit0 -C144_bit0 -C145_bit0 -C146_bit0 -C147_bit0 -C148_bit0 -C149_bit0 -C150_bit0 C151_bit0 -C152_bit0 C153_bit0 -C154_bit0 -C155_bit0 -C156_bit0 -C157_bit0 -C158_bit0 -C159_bit0 -C160_bit0 -C161_bit0 -C162_bit0 -C163_bit0 C164_bit0 -C165_bit0 C166_bit0 -C167_bit0 -C168_bit0 -C169_bit0 -C170_bit0 -C171_bit0 -C172_bit0 -C173_bit0 -C174_bit0 -C175_bit0 -C176_bit0 -C177_bit0 -C178_bit0 -C179_bit0 -C180_bit0 -C181_bit0 -C182_bit0 -C183_bit0 -C184_bit0 -C185_bit0 C186_bit0 -C187_bit0 -C188_bit0 -C189_bit0 -C106_bit0 C107_bit0 -C109_bit0 -C110_bit0
c _______________________________________________________________________________
c 
c restarts              : 247
c conflicts             : 155748         (239 /sec)
c decisions             : 277901         (426 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 653.017 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.80 0.95 0.94 2/54 15851
Raw data (stat): 15851 (runsolver) R 15850 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 549007685 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0006 s]
Raw data (loadavg): 0.83 0.95 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 1827 0 0 0 994 4 0 0 25 0 1 0 549007685 10072064 1794 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2459 1794 603 41 0 2418 0
vsize: 9836
[startup+20.0007 s]
Raw data (loadavg): 0.85 0.96 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 2025 0 0 0 1993 4 0 0 25 0 1 0 549007685 10964992 1992 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2677 1992 603 41 0 2636 0
vsize: 10708
[startup+30.0011 s]
Raw data (loadavg): 0.88 0.96 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 2181 0 0 0 2992 5 0 0 25 0 1 0 549007685 11632640 2148 4294967295 134512640 134672761 3221224624 3221223760 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2840 2148 603 41 0 2799 0
vsize: 11360
[startup+40.0006 s]
Raw data (loadavg): 0.89 0.96 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 2327 0 0 0 3991 5 0 0 25 0 1 0 549007685 12115968 2294 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2958 2294 603 41 0 2917 0
vsize: 11832
[startup+50.0016 s]
Raw data (loadavg): 0.91 0.96 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 2509 0 0 0 4991 6 0 0 25 0 1 0 549007685 12914688 2476 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3153 2476 603 41 0 3112 0
vsize: 12612
[startup+60.0013 s]
Raw data (loadavg): 0.92 0.96 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 2642 0 0 0 5991 7 0 0 25 0 1 0 549007685 13545472 2609 4294967295 134512640 134672761 3221224624 3221223728 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3307 2609 603 41 0 3266 0
vsize: 13228
[startup+70.0007 s]
Raw data (loadavg): 0.93 0.96 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 2769 0 0 0 6990 7 0 0 25 0 1 0 549007685 13946880 2736 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3405 2736 603 41 0 3364 0
vsize: 13620
[startup+80.0017 s]
Raw data (loadavg): 0.94 0.96 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 2785 0 0 0 7990 7 0 0 25 0 1 0 549007685 14077952 2752 4294967295 134512640 134672761 3221224624 3221223792 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3437 2752 603 41 0 3396 0
vsize: 13748
[startup+90.0014 s]
Raw data (loadavg): 0.95 0.96 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 2785 0 0 0 8990 7 0 0 25 0 1 0 549007685 14077952 2752 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3437 2752 603 41 0 3396 0
vsize: 13748
[startup+100.002 s]
Raw data (loadavg): 0.96 0.96 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 2785 0 0 0 9990 7 0 0 25 0 1 0 549007685 14077952 2752 4294967295 134512640 134672761 3221224624 3221223760 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3437 2752 603 41 0 3396 0
vsize: 13748
[startup+110.002 s]
Raw data (loadavg): 0.96 0.96 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 2786 0 0 0 10990 7 0 0 25 0 1 0 549007685 14077952 2753 4294967295 134512640 134672761 3221224624 3221223808 134559550 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3437 2753 603 41 0 3396 0
vsize: 13748
[startup+120.002 s]
Raw data (loadavg): 0.97 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 2786 0 0 0 11990 7 0 0 25 0 1 0 549007685 14077952 2753 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3437 2753 603 41 0 3396 0
vsize: 13748
[startup+130.002 s]
Raw data (loadavg): 0.97 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 2786 0 0 0 12991 7 0 0 25 0 1 0 549007685 14077952 2753 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3437 2753 603 41 0 3396 0
vsize: 13748
[startup+140.002 s]
Raw data (loadavg): 0.98 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 2786 0 0 0 13991 8 0 0 25 0 1 0 549007685 14077952 2753 4294967295 134512640 134672761 3221224624 3221223728 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3437 2753 603 41 0 3396 0
vsize: 13748
[startup+150.003 s]
Raw data (loadavg): 0.98 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 2843 0 0 0 14991 8 0 0 25 0 1 0 549007685 14344192 2810 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3502 2810 603 41 0 3461 0
vsize: 14008
[startup+160.002 s]
Raw data (loadavg): 0.98 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 2861 0 0 0 15991 8 0 0 25 0 1 0 549007685 14344192 2828 4294967295 134512640 134672761 3221224624 3221223808 134558332 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3502 2828 603 41 0 3461 0
vsize: 14008
[startup+170.002 s]
Raw data (loadavg): 0.98 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 2861 0 0 0 16991 8 0 0 25 0 1 0 549007685 14344192 2828 4294967295 134512640 134672761 3221224624 3221223760 134560579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3502 2828 603 41 0 3461 0
vsize: 14008
[startup+180.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 2861 0 0 0 17991 8 0 0 25 0 1 0 549007685 14344192 2828 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3502 2828 603 41 0 3461 0
vsize: 14008
[startup+190.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 2861 0 0 0 18991 8 0 0 25 0 1 0 549007685 14344192 2828 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3502 2828 603 41 0 3461 0
vsize: 14008
[startup+200.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 2861 0 0 0 19991 8 0 0 25 0 1 0 549007685 14344192 2828 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3502 2828 603 41 0 3461 0
vsize: 14008
[startup+210.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 2862 0 0 0 20991 8 0 0 25 0 1 0 549007685 14344192 2829 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3502 2829 603 41 0 3461 0
vsize: 14008
[startup+220.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 2862 0 0 0 21991 8 0 0 25 0 1 0 549007685 14344192 2829 4294967295 134512640 134672761 3221224624 3221223808 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3502 2829 603 41 0 3461 0
vsize: 14008
[startup+230.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 2862 0 0 0 22991 8 0 0 25 0 1 0 549007685 14344192 2829 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3502 2829 603 41 0 3461 0
vsize: 14008
[startup+240 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 2862 0 0 0 23991 8 0 0 25 0 1 0 549007685 14344192 2829 4294967295 134512640 134672761 3221224624 3221223808 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3502 2829 603 41 0 3461 0
vsize: 14008
[startup+250.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 2862 0 0 0 24992 8 0 0 25 0 1 0 549007685 14344192 2829 4294967295 134512640 134672761 3221224624 3221223780 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3502 2829 603 41 0 3461 0
vsize: 14008
[startup+260.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 2862 0 0 0 25992 8 0 0 25 0 1 0 549007685 14344192 2829 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3502 2829 603 41 0 3461 0
vsize: 14008
[startup+270.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 2870 0 0 0 26992 8 0 0 25 0 1 0 549007685 14344192 2837 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3502 2837 603 41 0 3461 0
vsize: 14008
[startup+280.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 2870 0 0 0 27992 9 0 0 25 0 1 0 549007685 14344192 2837 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3502 2837 603 41 0 3461 0
vsize: 14008
[startup+290.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 2870 0 0 0 28992 9 0 0 25 0 1 0 549007685 14344192 2837 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3502 2837 603 41 0 3461 0
vsize: 14008
[startup+300.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 2874 0 0 0 29992 9 0 0 25 0 1 0 549007685 14462976 2841 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3531 2841 603 41 0 3490 0
vsize: 14124
[startup+310.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 2874 0 0 0 30992 9 0 0 25 0 1 0 549007685 14462976 2841 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3531 2841 603 41 0 3490 0
vsize: 14124
[startup+320.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 2908 0 0 0 31992 9 0 0 25 0 1 0 549007685 14594048 2875 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3563 2875 603 41 0 3522 0
vsize: 14252
[startup+330.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 2993 0 0 0 32992 9 0 0 25 0 1 0 549007685 14856192 2960 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3627 2960 603 41 0 3586 0
vsize: 14508
[startup+340.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 2993 0 0 0 33992 9 0 0 25 0 1 0 549007685 14856192 2960 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3627 2960 603 41 0 3586 0
vsize: 14508
[startup+350.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 2993 0 0 0 34992 9 0 0 25 0 1 0 549007685 14856192 2960 4294967295 134512640 134672761 3221224624 3221223792 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3627 2960 603 41 0 3586 0
vsize: 14508
[startup+360.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 3000 0 0 0 35992 9 0 0 25 0 1 0 549007685 14999552 2967 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3662 2967 603 41 0 3621 0
vsize: 14648
[startup+370.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 3004 0 0 0 36993 9 0 0 25 0 1 0 549007685 14999552 2971 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3662 2971 603 41 0 3621 0
vsize: 14648
[startup+380.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 3018 0 0 0 37993 10 0 0 25 0 1 0 549007685 14999552 2985 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3662 2985 603 41 0 3621 0
vsize: 14648
[startup+390.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 3018 0 0 0 38993 10 0 0 25 0 1 0 549007685 14999552 2985 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3662 2985 603 41 0 3621 0
vsize: 14648
[startup+400.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 3018 0 0 0 39993 10 0 0 25 0 1 0 549007685 14999552 2985 4294967295 134512640 134672761 3221224624 3221223760 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3662 2985 603 41 0 3621 0
vsize: 14648
[startup+410.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 3026 0 0 0 40993 10 0 0 25 0 1 0 549007685 14999552 2993 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3662 2993 603 41 0 3621 0
vsize: 14648
[startup+420.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 3026 0 0 0 41993 10 0 0 25 0 1 0 549007685 14999552 2993 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3662 2993 603 41 0 3621 0
vsize: 14648
[startup+430.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 3026 0 0 0 42993 10 0 0 25 0 1 0 549007685 14999552 2993 4294967295 134512640 134672761 3221224624 3221223792 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3662 2993 603 41 0 3621 0
vsize: 14648
[startup+440.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 3049 0 0 0 43993 10 0 0 25 0 1 0 549007685 15130624 3016 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3694 3016 603 41 0 3653 0
vsize: 14776
[startup+450.003 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 3141 0 0 0 44993 10 0 0 25 0 1 0 549007685 15523840 3108 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3790 3108 603 41 0 3749 0
vsize: 15160
[startup+460.003 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 3262 0 0 0 45993 10 0 0 25 0 1 0 549007685 16060416 3229 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3921 3229 603 41 0 3880 0
vsize: 15684
[startup+470.003 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 3373 0 0 0 46993 11 0 0 25 0 1 0 549007685 16457728 3340 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4018 3340 603 41 0 3977 0
vsize: 16072
[startup+480.004 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 3474 0 0 0 47992 12 0 0 25 0 1 0 549007685 16982016 3441 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4146 3441 603 41 0 4105 0
vsize: 16584
[startup+490.003 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 3582 0 0 0 48992 12 0 0 25 0 1 0 549007685 17514496 3549 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4276 3549 603 41 0 4235 0
vsize: 17104
[startup+500.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 3684 0 0 0 49992 13 0 0 25 0 1 0 549007685 17924096 3651 4294967295 134512640 134672761 3221224624 3221223792 134564686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4376 3651 603 41 0 4335 0
vsize: 17504
[startup+510.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 3780 0 0 0 50992 13 0 0 25 0 1 0 549007685 18325504 3747 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4474 3747 603 41 0 4433 0
vsize: 17896
[startup+520.004 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 3875 0 0 0 51991 13 0 0 25 0 1 0 549007685 18722816 3842 4294967295 134512640 134672761 3221224624 3221223792 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4571 3842 603 41 0 4530 0
vsize: 18284
[startup+530.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 3903 0 0 0 52992 13 0 0 25 0 1 0 549007685 18853888 3870 4294967295 134512640 134672761 3221224624 3221223728 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4603 3870 603 41 0 4562 0
vsize: 18412
[startup+540.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 3903 0 0 0 53992 13 0 0 25 0 1 0 549007685 18853888 3870 4294967295 134512640 134672761 3221224624 3221223728 134559937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4603 3870 603 41 0 4562 0
vsize: 18412
[startup+550.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 3908 0 0 0 54992 13 0 0 25 0 1 0 549007685 18853888 3875 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4603 3875 603 41 0 4562 0
vsize: 18412
[startup+560.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 3916 0 0 0 55992 13 0 0 25 0 1 0 549007685 18853888 3883 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4603 3883 603 41 0 4562 0
vsize: 18412
[startup+570.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 3916 0 0 0 56992 13 0 0 25 0 1 0 549007685 18853888 3883 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4603 3883 603 41 0 4562 0
vsize: 18412
[startup+580.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 3917 0 0 0 57993 13 0 0 25 0 1 0 549007685 18853888 3884 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4603 3884 603 41 0 4562 0
vsize: 18412
[startup+590.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 3918 0 0 0 58993 13 0 0 25 0 1 0 549007685 18853888 3885 4294967295 134512640 134672761 3221224624 3221223792 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4603 3885 603 41 0 4562 0
vsize: 18412
[startup+600.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 3920 0 0 0 59992 14 0 0 25 0 1 0 549007685 18853888 3887 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4603 3887 603 41 0 4562 0
vsize: 18412
[startup+610.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 3920 0 0 0 60992 14 0 0 25 0 1 0 549007685 18853888 3887 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4603 3887 603 41 0 4562 0
vsize: 18412
[startup+620.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 3921 0 0 0 61992 14 0 0 25 0 1 0 549007685 18853888 3888 4294967295 134512640 134672761 3221224624 3221223808 134559538 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4603 3888 603 41 0 4562 0
vsize: 18412
[startup+630.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 3933 0 0 0 62993 14 0 0 25 0 1 0 549007685 18853888 3900 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4603 3900 603 41 0 4562 0
vsize: 18412
[startup+640.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 3933 0 0 0 63993 14 0 0 25 0 1 0 549007685 18853888 3900 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4603 3900 603 41 0 4562 0
vsize: 18412
[startup+650.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 3949 0 0 0 64993 14 0 0 25 0 1 0 549007685 19017728 3916 4294967295 134512640 134672761 3221224624 3221223728 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4643 3916 603 41 0 4602 0
vsize: 18572
[startup+653.105 s]
Raw data (loadavg): 0.99 0.97 0.94 1/53 15851
Raw data (stat): 15851 (minisat+) R 15850 27565 27564 0 -1 0 3949 0 0 0 64993 14 0 0 25 0 1 0 549007685 19017728 3916 4294967295 134512640 134672761 3221224624 3221223728 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4643 3916 603 41 0 4602 0
vsize: 0

Child status: 30
Real time (s): 653.104
CPU time (s): 653.18
CPU user time (s): 653.022
CPU system time (s): 0.157975
CPU usage (%): 100.012
Max. virtual memory (Kb): 18572
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	1120
#### END VERIFIER DATA ####