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-flugpl.opb
MD5SUM	f7c404708fc3042fadfc18ab8efeb9a5
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	14745600
Optimality of the best value was proved	NO
Number of terms in the objective function	265
Biggest coefficient in the objective function	48318382080
Number of bits for the biggest coefficient in the objective function	36
Sum of the numbers in the objective function	103103023008
Number of bits of the sum of numbers in the objective function	37
Biggest number in a constraint	80530636800
Number of bits of the biggest number in a constraint	37
Biggest sum of numbers in a constraint	162146381673
Number of bits of the biggest sum of numbers	38
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	21.6227
Number of variables	265
Total number of constraints	29
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	29
Minimum length of a constraint	5
Maximum length of a constraint	65
Trace number 31953

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-05-27 07:28:55 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=23385 boxname=wulflinc2 idbench=1029 idsolver=16 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f7c404708fc3042fadfc18ab8efeb9a5  /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-20-10-flugpl.opb
REAL COMMAND:  minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-20-10-flugpl.opb
IDLAUNCH: 23385
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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:        912072 kB
Buffers:         25744 kB
Cached:          76720 kB
SwapCached:        556 kB
Active:          19184 kB
Inactive:        85572 kB
HighTotal:      131008 kB
HighFree:        59444 kB
LowTotal:       903652 kB
LowFree:        852628 kB
SwapTotal:     2097136 kB
SwapFree:      2095840 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5592 kB
Slab:            12040 kB
Committed_AS:    71788 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-27 07:29:17 (client local time) WITH STATUS 30 IN 21.6227 SECONDS
stats: 23385 0 21.6227 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 35 PB-constraints to clauses...
c   -- Unit propagations: pp
c   -- Detecting intervals from adjacent constraints: #####
c   -- Clauses(.)/Splits(s): (none)
c ---[  34]---> BDD-cost:    4
c ---[  33]---> BDD-cost:    4
c ---[  32]---> BDD-cost:    4
c ---[  31]---> BDD-cost:    4
c ---[  30]---> BDD-cost:    4
c ---[  29]---> BDD-cost:    4
c ---[  28]---> BDD-cost:    4
c ---[  27]---> BDD-cost:    4
c ---[  26]---> BDD-cost:    4
c ---[  25]---> BDD-cost:    4
c ---[  24]---> BDD-cost:    4
c ---[  20]---> BDD-cost:   20
c ---[  18]---> BDD-cost:   63
c ---[  16]---> BDD-cost:   63
c ---[  14]---> BDD-cost:   63
c ---[  12]---> BDD-cost:   63
c ---[  11]---> BDD-cost:  107
c ---[  10]---> BDD-cost:  465
c ---[   9]---> BDD-cost:  433
c ---[   8]---> BDD-cost:  476
c ---[   7]---> BDD-cost:  465
c ---[   6]---> BDD-cost:  461
c ---[   5]---> BDD-cost:   20
c ---[   4]---> BDD-cost:   89
c ---[   3]---> BDD-cost:   89
c ---[   2]---> BDD-cost:   89
c ---[   1]---> BDD-cost:   89
c ---[   0]---> BDD-cost:   89
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    5470    14717 |    1823       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 17922048[0m
c ---[   0]---> Sorter-cost: 9301     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         3 |   29153    69990 |    9717       3        8     2.7 |  0.000 % |
c ==============================================================================
c [1mFound solution: 16730337[0m
c ---[   0]---> Sorter-cost: 5677     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        73 |   42806   101871 |   14268      66     1453    22.0 |  0.000 % |
c ==============================================================================
c [1mFound solution: 16238930[0m
c ---[   0]---> Sorter-cost: 5511     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       110 |   51023   121217 |   17007      93     1583    17.0 |  0.000 % |
c ==============================================================================
c [1mFound solution: 16144369[0m
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       131 |   51040   121334 |   17013     114     1726    15.1 |  0.000 % |
c ==============================================================================
c [1mFound solution: 15927790[0m
c ---[   0]---> Sorter-cost:   19     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       147 |   51040   121343 |   17013     128     2547    19.9 |  0.000 % |
c ==============================================================================
c [1mFound solution: 15921286[0m
c ---[   0]---> Sorter-cost: 4809     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       197 |   61194   145099 |   20398     172     3080    17.9 |  0.000 % |
c ==============================================================================
c [1mFound solution: 15912138[0m
c ---[   0]---> Sorter-cost: 3171     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       254 |   67826   160630 |   22608     222     3787    17.1 |  0.000 % |
c ==============================================================================
c [1mFound solution: 15912137[0m
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       285 |   67776   160589 |   22592     244     4059    16.6 |  0.000 % |
c ==============================================================================
c [1mFound solution: 15453386[0m
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       315 |   67786   160615 |   22595     274     4841    17.7 |  0.000 % |
c |       418 |   67771   160582 |   24854     376     7421    19.7 |  9.904 % |
c ==============================================================================
c [1mFound solution: 15386602[0m
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       467 |   67621   160258 |   22540     422     7821    18.5 |  9.904 % |
c ==============================================================================
c [1mFound solution: 15366946[0m
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       517 |   67534   160068 |   22511     469     8594    18.3 |  9.904 % |
c |       617 |   67500   159991 |   24762     567     9059    16.0 | 10.204 % |
c |       771 |   66212   157040 |   27238     704    12874    18.3 | 11.528 % |
c ==============================================================================
c [1mFound solution: 15153962[0m
c ---[   0]---> Sorter-cost: 3677     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       820 |   75173   177941 |   25057     741    13017    17.6 | 11.528 % |
c ==============================================================================
c [1mFound solution: 15063559[0m
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       845 |   75198   178002 |   25066     766    13823    18.0 | 11.528 % |
c ==============================================================================
c [1mFound solution: 14877610[0m
c ---[   0]---> Sorter-cost: 4380     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       887 |   83880   198377 |   27960     791    14481    18.3 | 11.528 % |
c ==============================================================================
c [1mFound solution: 14877288[0m
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       889 |   83902   198545 |   27967     793    14487    18.3 | 11.528 % |
c ==============================================================================
c [1mFound solution: 14877226[0m
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       890 |   83912   198574 |   27970     794    14489    18.2 | 11.528 % |
c ==============================================================================
c [1mFound solution: 14877225[0m
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       890 |   83927   198614 |   27975     794    14489    18.2 | 11.528 % |
c ==============================================================================
c [1mFound solution: 14877224[0m
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       890 |   83940   198650 |   27980     794    14489    18.2 | 11.528 % |
c ==============================================================================
c [1mFound solution: 14877221[0m
c ---[   0]---> Sorter-cost:   19     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       891 |   83958   198697 |   27986     795    14502    18.2 | 11.528 % |
c ==============================================================================
c [1mFound solution: 14877205[0m
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       894 |   83972   198735 |   27990     798    14530    18.2 | 11.528 % |
c ==============================================================================
c [1mFound solution: 14877141[0m
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       896 |   83983   198768 |   27994     800    14542    18.2 | 11.528 % |
c ==============================================================================
c [1mFound solution: 14877007[0m
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       903 |   84000   198813 |   28000     807    14569    18.1 | 11.528 % |
c ==============================================================================
c [1mFound solution: 14876879[0m
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       903 |   84010   198842 |   28003     807    14569    18.1 | 11.528 % |
c ==============================================================================
c [1mFound solution: 14876750[0m
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       903 |   84024   198880 |   28008     807    14569    18.1 | 11.528 % |
c ==============================================================================
c [1mFound solution: 14876683[0m
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       903 |   84036   198912 |   28012     807    14569    18.1 | 11.528 % |
c ==============================================================================
c [1mFound solution: 14876669[0m
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       903 |   84050   198948 |   28016     807    14569    18.1 | 11.528 % |
c ==============================================================================
c [1mFound solution: 14876668[0m
c ---[   0]---> Sorter-cost:   19     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       903 |   84065   198986 |   28021     807    14569    18.1 | 11.528 % |
c ==============================================================================
c [1mFound solution: 14876667[0m
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       903 |   84070   199003 |   28023     807    14569    18.1 | 11.528 % |
c ==============================================================================
c [1mFound solution: 14875723[0m
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       904 |   84085   199042 |   28028     808    14609    18.1 | 11.528 % |
c ==============================================================================
c [1mFound solution: 14874447[0m
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       908 |   84093   199067 |   28031     812    14620    18.0 | 11.528 % |
c ==============================================================================
c [1mFound solution: 14842062[0m
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       954 |   84107   199102 |   28035     858    16203    18.9 | 11.528 % |
c ==============================================================================
c [1mFound solution: 14842061[0m
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1004 |   84061   199019 |   28020     906    16979    18.7 | 11.528 % |
c ==============================================================================
c [1mFound solution: 14812784[0m
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1037 |   84075   199059 |   28025     939    17609    18.8 | 11.528 % |
c ==============================================================================
c [1mFound solution: 14747241[0m
c ---[   0]---> Sorter-cost: 4099     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1106 |   92250   218190 |   30750    1002    20553    20.5 | 11.528 % |
c ==============================================================================
c [1mFound solution: 14746985[0m
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1110 |   92267   218321 |   30755    1006    20563    20.4 | 11.528 % |
c ==============================================================================
c [1mFound solution: 14746981[0m
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1116 |   92123   218005 |   30707    1008    20578    20.4 | 11.528 % |
c ==============================================================================
c [1mFound solution: 14746952[0m
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1118 |   92137   218043 |   30712    1010    20582    20.4 | 11.528 % |
c ==============================================================================
c [1mFound solution: 14746216[0m
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1120 |   92143   218062 |   30714    1012    20606    20.4 | 11.528 % |
c ==============================================================================
c [1mFound solution: 14746184[0m
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1120 |   92154   218092 |   30718    1012    20606    20.4 | 11.528 % |
c ==============================================================================
c [1mFound solution: 14746152[0m
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1122 |   92160   218111 |   30720    1014    20615    20.3 | 11.528 % |
c ==============================================================================
c [1mFound solution: 14746120[0m
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1122 |   92173   218145 |   30724    1014    20615    20.3 | 11.528 % |
c ==============================================================================
c [1mFound solution: 14746024[0m
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1122 |   92185   218178 |   30728    1014    20615    20.3 | 11.528 % |
c ==============================================================================
c [1mFound solution: 14745992[0m
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1122 |   92197   218211 |   30732    1014    20615    20.3 | 11.528 % |
c ==============================================================================
c [1mFound solution: 14745896[0m
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1122 |   92209   218243 |   30736    1014    20615    20.3 | 11.528 % |
c ==============================================================================
c [1mFound solution: 14745864[0m
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1122 |   92221   218275 |   30740    1014    20615    20.3 | 11.528 % |
c ==============================================================================
c [1mFound solution: 14745768[0m
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1122 |   92232   218305 |   30744    1014    20615    20.3 | 11.528 % |
c ==============================================================================
c [1mFound solution: 14745736[0m
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1124 |   92243   218335 |   30747    1016    20636    20.3 | 11.528 % |
c ==============================================================================
c [1mFound solution: 14745704[0m
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1124 |   92252   218360 |   30750    1016    20636    20.3 | 11.528 % |
c ==============================================================================
c [1mFound solution: 14745672[0m
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1124 |   92261   218385 |   30753    1016    20636    20.3 | 11.528 % |
c ==============================================================================
c [1mFound solution: 14745671[0m
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1135 |   92276   218423 |   30758    1027    21154    20.6 | 11.528 % |
c |      1236 |   82683   196522 |   33833    1031    21786    21.1 | 19.518 % |
c ==============================================================================
c [1mFound solution: 14745664[0m
c ---[   0]---> Sorter-cost: 3056     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1283 |   90042   213681 |   30014    1078    22947    21.3 | 19.518 % |
c ==============================================================================
c [1mFound solution: 14745660[0m
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1296 |   90071   213819 |   30023    1091    23703    21.7 | 19.518 % |
c ==============================================================================
c [1mFound solution: 14745659[0m
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1333 |   89993   213652 |   29997    1119    24101    21.5 | 19.518 % |
c ==============================================================================
c [1mFound solution: 14745652[0m
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1343 |   90010   213696 |   30003    1129    24422    21.6 | 19.518 % |
c ==============================================================================
c [1mFound solution: 14745651[0m
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1344 |   90025   213735 |   30008    1130    24451    21.6 | 19.518 % |
c ==============================================================================
c [1mFound solution: 14745650[0m
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1345 |   90040   213773 |   30013    1131    24455    21.6 | 19.518 % |
c ==============================================================================
c [1mFound solution: 14745646[0m
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1347 |   90055   213811 |   30018    1133    24470    21.6 | 19.518 % |
c ==============================================================================
c [1mFound solution: 14745645[0m
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1347 |   90070   213849 |   30023    1133    24470    21.6 | 19.518 % |
c ==============================================================================
c [1mFound solution: 14745644[0m
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1347 |   90087   213892 |   30029    1133    24470    21.6 | 19.518 % |
c ==============================================================================
c [1mFound solution: 14745643[0m
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1349 |   90102   213930 |   30034    1135    24475    21.6 | 19.518 % |
c ==============================================================================
c [1mFound solution: 14745634[0m
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1349 |   90114   213961 |   30038    1135    24475    21.6 | 19.518 % |
c ==============================================================================
c [1mFound solution: 14745633[0m
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1354 |   90129   213999 |   30043    1140    24538    21.5 | 19.518 % |
c ==============================================================================
c [1mFound solution: 14745630[0m
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1355 |   90146   214041 |   30048    1141    24540    21.5 | 19.518 % |
c ==============================================================================
c [1mFound solution: 14745628[0m
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1355 |   90163   214083 |   30054    1141    24540    21.5 | 19.518 % |
c ==============================================================================
c [1mFound solution: 14745627[0m
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1356 |   90177   214118 |   30059    1142    24544    21.5 | 19.518 % |
c ==============================================================================
c [1mFound solution: 14745626[0m
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1356 |   90193   214158 |   30064    1142    24544    21.5 | 19.518 % |
c ==============================================================================
c [1mFound solution: 14745622[0m
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1356 |   90209   214198 |   30069    1142    24544    21.5 | 19.518 % |
c ==============================================================================
c [1mFound solution: 14745621[0m
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1357 |   90220   214227 |   30073    1143    24548    21.5 | 19.518 % |
c ==============================================================================
c [1mFound solution: 14745614[0m
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1360 |   90234   214262 |   30078    1146    24560    21.4 | 19.518 % |
c ==============================================================================
c [1mFound solution: 14745613[0m
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1360 |   90248   214297 |   30082    1146    24560    21.4 | 19.518 % |
c ==============================================================================
c [1mFound solution: 14745612[0m
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1360 |   90264   214337 |   30088    1146    24560    21.4 | 19.518 % |
c ==============================================================================
c [1mFound solution: 14745611[0m
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1360 |   90272   214360 |   30090    1146    24560    21.4 | 19.518 % |
c ==============================================================================
c [1mFound solution: 14745610[0m
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1361 |   90286   214395 |   30095    1147    24563    21.4 | 19.518 % |
c ==============================================================================
c [1mFound solution: 14745609[0m
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1361 |   90300   214430 |   30100    1147    24563    21.4 | 19.518 % |
c ==============================================================================
c [1mFound solution: 14745608[0m
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1361 |   90311   214459 |   30103    1147    24563    21.4 | 19.518 % |
c ==============================================================================
c [1mFound solution: 14745607[0m
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1363 |   90322   214488 |   30107    1149    24772    21.6 | 19.518 % |
c ==============================================================================
c [1mFound solution: 14745606[0m
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1365 |   90335   214521 |   30111    1151    24839    21.6 | 19.518 % |
c ==============================================================================
c [1mFound solution: 14745605[0m
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1367 |   90350   214558 |   30116    1153    24850    21.6 | 19.518 % |
c ==============================================================================
c [1mFound solution: 14745604[0m
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1368 |   90367   214600 |   30122    1154    24864    21.5 | 19.518 % |
c ==============================================================================
c [1mFound solution: 14745603[0m
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1368 |   90383   214639 |   30127    1154    24864    21.5 | 19.518 % |
c ==============================================================================
c [1mFound solution: 14745602[0m
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1368 |   90398   214676 |   30132    1154    24864    21.5 | 19.518 % |
c ==============================================================================
c [1mFound solution: 14745601[0m
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1368 |   90413   214713 |   30137    1154    24864    21.5 | 19.518 % |
c ==============================================================================
c [1mFound solution: 14745600[0m
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1368 |   90427   214748 |   30142    1154    24864    21.5 | 19.518 % |
c ==============================================================================
c [1mOptimal solution: 14745600[0m
s OPTIMUM FOUND
v -STM1_bit_10 -STM1_bit_9 -STM1_bit_8 -STM1_bit_7 -STM1_bit_6 -STM1_bit_5 -STM1_bit_4 -STM1_bit_3 -STM1_bit_2 -STM1_bit_1 -STM1_bit0 -STM1_bit1 STM1_bit2 STM1_bit3 STM1_bit4 STM1_bit5 -STM1_bit6 -STM1_bit7 -STM1_bit8 -STM1_bit9 -STM1_bit10 -STM1_bit11 -STM1_bit12 -STM1_bit13 -STM1_bit14 -STM1_bit15 -STM1_bit16 -STM1_bit17 -STM1_bit18 -STM1_bit19 -ANM1_bit0 ANM1_bit1 ANM1_bit2 -ANM1_bit3 -ANM1_bit4 -UE1_bit_10 -UE1_bit_9 -UE1_bit_8 -UE1_bit_7 -UE1_bit_6 -UE1_bit_5 -UE1_bit_4 -UE1_bit_3 -UE1_bit_2 -UE1_bit_1 -UE1_bit0 -UE1_bit1 -UE1_bit2 -UE1_bit3 -UE1_bit4 -UE1_bit5 -UE1_bit6 -UE1_bit7 -UE1_bit8 -UE1_bit9 -UE1_bit10 -UE1_bit11 -UE1_bit12 -UE1_bit13 -UE1_bit14 -UE1_bit15 -UE1_bit16 -UE1_bit17 -UE1_bit18 -UE1_bit19 STM2_bit0 STM2_bit1 -STM2_bit2 -STM2_bit3 -STM2_bit4 -ANM2_bit0 ANM2_bit1 ANM2_bit2 -ANM2_bit3 -ANM2_bit4 -UE2_bit_10 -UE2_bit_9 -UE2_bit_8 -UE2_bit_7 -UE2_bit_6 -UE2_bit_5 -UE2_bit_4 -UE2_bit_3 -UE2_bit_2 -UE2_bit_1 -UE2_bit0 -UE2_bit1 -UE2_bit2 UE2_bit3 UE2_bit4 -UE2_bit5 UE2_bit6 -UE2_bit7 -UE2_bit8 UE2_bit9 -UE2_bit10 -UE2_bit11 -UE2_bit12 -UE2_bit13 -UE2_bit14 -UE2_bit15 -UE2_bit16 -UE2_bit17 -UE2_bit18 -UE2_bit19 STM3_bit0 STM3_bit1 -STM3_bit2 -STM3_bit3 -STM3_bit4 -ANM3_bit0 -ANM3_bit1 -ANM3_bit2 -ANM3_bit3 ANM3_bit4 -UE3_bit_10 -UE3_bit_9 -UE3_bit_8 -UE3_bit_7 -UE3_bit_6 -UE3_bit_5 -UE3_bit_4 -UE3_bit_3 -UE3_bit_2 -UE3_bit_1 -UE3_bit0 -UE3_bit1 -UE3_bit2 UE3_bit3 UE3_bit4 -UE3_bit5 UE3_bit6 -UE3_bit7 -UE3_bit8 UE3_bit9 -UE3_bit10 -UE3_bit11 -UE3_bit12 -UE3_bit13 -UE3_bit14 -UE3_bit15 -UE3_bit16 -UE3_bit17 -UE3_bit18 -UE3_bit19 STM4_bit0 -STM4_bit1 STM4_bit2 STM4_bit3 -STM4_bit4 ANM4_bit0 ANM4_bit1 ANM4_bit2 -ANM4_bit3 -ANM4_bit4 -UE4_bit_10 -UE4_bit_9 -UE4_bit_8 -UE4_bit_7 -UE4_bit_6 -UE4_bit_5 -UE4_bit_4 -UE4_bit_3 -UE4_bit_2 -UE4_bit_1 -UE4_bit0 -UE4_bit1 -UE4_bit2 UE4_bit3 -UE4_bit4 -UE4_bit5 UE4_bit6 UE4_bit7 -UE4_bit8 -UE4_bit9 -UE4_bit10 -UE4_bit11 -UE4_bit12 -UE4_bit13 -UE4_bit14 -UE4_bit15 -UE4_bit16 -UE4_bit17 -UE4_bit18 -UE4_bit19 STM5_bit0 -STM5_bit1 STM5_bit2 STM5_bit3 -STM5_bit4 -ANM5_bit0 -ANM5_bit1 ANM5_bit2 ANM5_bit3 -ANM5_bit4 -UE5_bit_10 -UE5_bit_9 -UE5_bit_8 -UE5_bit_7 -UE5_bit_6 -UE5_bit_5 -UE5_bit_4 -UE5_bit_3 -UE5_bit_2 -UE5_bit_1 -UE5_bit0 -UE5_bit1 -UE5_bit2 -UE5_bit3 -UE5_bit4 -UE5_bit5 -UE5_bit6 -UE5_bit7 -UE5_bit8 -UE5_bit9 -UE5_bit10 -UE5_bit11 -UE5_bit12 -UE5_bit13 -UE5_bit14 -UE5_bit15 -UE5_bit16 -UE5_bit17 -UE5_bit18 -UE5_bit19 -STM6_bit0 STM6_bit1 -STM6_bit2 -STM6_bit3 STM6_bit4 -ANM6_bit0 -ANM6_bit1 -ANM6_bit2 -ANM6_bit3 -ANM6_bit4 -UE6_bit_10 -UE6_bit_9 -UE6_bit_8 -UE6_bit_7 -UE6_bit_6 -UE6_bit_5 -UE6_bit_4 -UE6_bit_3 -UE6_bit_2 -UE6_bit_1 -UE6_bit0 UE6_bit1 UE6_bit2 UE6_bit3 -UE6_bit4 UE6_bit5 UE6_bit6 UE6_bit7 -UE6_bit8 UE6_bit9 -UE6_bit10 -UE6_bit11 -UE6_bit12 -UE6_bit13 -UE6_bit14 -UE6_bit15 -UE6_bit16 -UE6_bit17 -UE6_bit18 -UE6_bit19
c _______________________________________________________________________________
c 
c restarts              : 88
c conflicts             : 1382           (64 /sec)
c decisions             : 123555         (5751 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 21.4857 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.89 0.95 0.90 2/54 26650
Raw data (stat): 26650 (runsolver) R 26649 31399 31398 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 796147392 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.91 0.95 0.90 2/55 26654
Raw data (stat): 26650 (minisat+_script) S 26649 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796147392 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0016 s]
Raw data (loadavg): 0.92 0.96 0.91 2/55 26654
Raw data (stat): 26650 (minisat+_script) S 26649 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796147392 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+21.6423 s]
Raw data (loadavg): 0.93 0.96 0.91 1/53 26654
Raw data (stat): 26650 (minisat+_script) S 26649 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796147392 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 30
Real time (s): 21.642
CPU time (s): 21.6227
CPU user time (s): 21.5077
CPU system time (s): 0.114982
CPU usage (%): 99.9109
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	14745600
#### END VERIFIER DATA ####