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/submitted/een/normalized-p0282.opb
MD5SUM	dd62132555621025f45a5a6099c90742
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	258411
Optimality of the best value was proved	NO
Number of terms in the objective function	282
Biggest coefficient in the objective function	160646
Number of bits for the biggest coefficient in the objective function	18
Sum of the numbers in the objective function	1302615
Number of bits of the sum of numbers in the objective function	21
Biggest number in a constraint	160646
Number of bits of the biggest number in a constraint	18
Biggest sum of numbers in a constraint	1302615
Number of bits of the biggest sum of numbers	21
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.01884
Number of variables	282
Total number of constraints	221
Number of constraints which are clauses	177
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	44
Minimum length of a constraint	2
Maximum length of a constraint	57
Trace number 6973

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-04-14 20:51:18 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=5056 boxname=wulflinc3 idbench=389 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  dd62132555621025f45a5a6099c90742  /oldhome/oroussel/tmp/wulflinc3/normalized-p0282.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc3/normalized-p0282.opb /oldhome/oroussel/tmp/wulflinc3/normalized-p0282.opb
IDLAUNCH: 5056
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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:        828740 kB
Buffers:         36600 kB
Cached:         146036 kB
SwapCached:       3276 kB
Active:          86488 kB
Inactive:       102252 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        828488 kB
SwapTotal:     2097136 kB
SwapFree:      2093860 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            11624 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 21:04:21 (client local time) WITH STATUS 30 IN 783.453 SECONDS
stats: 5056 0 783.453 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 221 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .................................................................................................................................................................................sss
c ---[  46]---> BDD-cost:    4
c ---[  45]---> BDD-cost:    8
c ---[  44]---> BDD-cost:   10
c ---[  43]---> BDD-cost:   16
c ---[  42]---> BDD-cost:  547
c ---[  41]---> BDD-cost:  327
c ---[  40]---> BDD-cost:  564
c ---[  38]---> BDD-cost:  396
c ---[  37]---> BDD-cost:  448
c ---[  36]---> BDD-cost:  323
c ---[  35]---> BDD-cost:  369
c ---[  34]---> BDD-cost:  580
c ---[  33]---> BDD-cost:  587
c ---[  32]---> BDD-cost:  829
c ---[  31]---> BDD-cost:  350
c ---[  30]---> BDD-cost:  363
c ---[  29]---> BDD-cost:  267
c ---[  28]---> BDD-cost:  219
c ---[  27]---> BDD-cost:  593
c ---[  26]---> BDD-cost:  347
c ---[  25]---> BDD-cost:  310
c ---[  24]---> BDD-cost:  528
c ---[  23]---> BDD-cost:  386
c ---[  22]---> BDD-cost:  415
c ---[  21]---> BDD-cost:  348
c ---[  20]---> BDD-cost:  385
c ---[  19]---> BDD-cost:  658
c ---[  18]---> BDD-cost:  473
c ---[  17]---> BDD-cost:  492
c ---[  16]---> BDD-cost:  602
c ---[  15]---> BDD-cost:  578
c ---[  14]---> BDD-cost:   26
c ---[  13]---> BDD-cost:  791
c ---[  11]---> BDD-cost:  872
c ---[  10]---> BDD-cost:  423
c ---[   9]---> BDD-cost:  897
c ---[   8]---> BDD-cost:  362
c ---[   7]---> BDD-cost:  744
c ---[   5]---> BDD-cost:   56
c ---[   4]---> BDD-cost:   56
c ---[   3]---> BDD-cost:   56
c ---[   2]---> BDD-cost:    6
c ---[   1]---> BDD-cost:  143
c ---[   0]---> BDD-cost:   87
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   41898   123412 |   13966       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 512142[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:77328     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         1 |  261012   635354 |   87004       1        2     2.0 |  0.000 % |
c |       101 |  261012   635354 |   95704     101     4887    48.4 |  0.050 % |
c |       252 |  261012   635354 |  105274     252     5744    22.8 |  0.050 % |
c |       478 |  260996   635318 |  115802     477     7975    16.7 |  0.055 % |
c |       818 |  260831   634950 |  127382     812     9672    11.9 |  0.103 % |
c |      1324 |  260831   634950 |  140120    1318    14223    10.8 |  0.103 % |
c |      2083 |  260592   634413 |  154132    2066    60353    29.2 |  0.178 % |
c |      3223 |  260539   634307 |  169546    3201   165921    51.8 |  0.205 % |
c |      4931 |  260499   634227 |  186500    4907   191240    39.0 |  0.227 % |
c ==============================================================================
c [1mFound solution: 512140[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5798 |  260472   634589 |   86824    5772   216990    37.6 |  0.227 % |
c |      5898 |  260472   634589 |   95506    5872   217624    37.1 |  0.241 % |
c |      6048 |  260384   634393 |  105057    6019   218537    36.3 |  0.268 % |
c |      6274 |  260384   634393 |  115562    6245   220938    35.4 |  0.268 % |
c ==============================================================================
c [1mFound solution: 509130[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6425 |  261785   637817 |   87261    6396   223326    34.9 |  0.268 % |
c |      6525 |  261527   637231 |   95987    6493   224117    34.5 |  0.350 % |
c |      6675 |  261527   637231 |  105585    6643   228419    34.4 |  0.350 % |
c |      6905 |  261527   637231 |  116144    6873   230955    33.6 |  0.350 % |
c |      7245 |  261391   636925 |  127758    7207   240728    33.4 |  0.390 % |
c |      7751 |  261375   636893 |  140534    7711   252798    32.8 |  0.399 % |
c |      8510 |  261228   636564 |  154588    8468   257828    30.4 |  0.441 % |
c |      9650 |  261097   636267 |  170047    9605   268100    27.9 |  0.482 % |
c ==============================================================================
c [1mFound solution: 502172[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10062 |  261522   637425 |   87174   10017   285114    28.5 |  0.482 % |
c |     10162 |  261522   637425 |   95891   10117   285772    28.2 |  0.481 % |
c |     10312 |  261522   637425 |  105480   10267   286624    27.9 |  0.481 % |
c |     10538 |  261522   637425 |  116028   10493   290659    27.7 |  0.481 % |
c |     10875 |  261375   637089 |  127631   10815   295964    27.4 |  0.529 % |
c |     11381 |  261351   637035 |  140394   11320   303297    26.8 |  0.535 % |
c |     12142 |  261351   637035 |  154434   12081   321101    26.6 |  0.535 % |
c |     13281 |  261295   636908 |  169877   13217   331584    25.1 |  0.553 % |
c |     14990 |  261123   636524 |  186865   14923   348534    23.4 |  0.601 % |
c ==============================================================================
c [1mFound solution: 502146[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15589 |  261120   636540 |   87040   15520   378746    24.4 |  0.601 % |
c |     15690 |  261120   636540 |   95744   15621   379622    24.3 |  0.608 % |
c |     15840 |  261120   636540 |  105318   15771   382471    24.3 |  0.608 % |
c |     16065 |  261091   636476 |  115850   15993   385069    24.1 |  0.617 % |
c |     16402 |  261021   636317 |  127435   16329   387861    23.8 |  0.640 % |
c |     16908 |  260971   636203 |  140178   16833   394517    23.4 |  0.658 % |
c |     17667 |  260971   636203 |  154196   17592   402111    22.9 |  0.658 % |
c |     18806 |  260962   636183 |  169616   18730   414607    22.1 |  0.661 % |
c |     20514 |  260928   636106 |  186577   20436   440426    21.6 |  0.671 % |
c |     23078 |  260406   634935 |  205235   22905   488656    21.3 |  0.845 % |
c ==============================================================================
c [1mFound solution: 454055[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   13     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23675 |  260312   634836 |   86770   23496   503729    21.4 |  0.845 % |
c |     23775 |  260312   634836 |   95447   23596   504132    21.4 |  0.878 % |
c |     23925 |  260265   634731 |  104991   23743   505446    21.3 |  0.892 % |
c ==============================================================================
c [1mFound solution: 383752[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24068 |  260292   634802 |   86764   23886   510224    21.4 |  0.892 % |
c |     24169 |  260276   634770 |   95440   23986   512541    21.4 |  0.902 % |
c |     24319 |  260258   634734 |  104984   24133   517072    21.4 |  0.910 % |
c |     24545 |  260258   634734 |  115482   24359   519846    21.3 |  0.910 % |
c |     24883 |  260220   634648 |  127031   24696   523089    21.2 |  0.921 % |
c |     25391 |  260220   634648 |  139734   25204   532365    21.1 |  0.921 % |
c |     26150 |  260119   634418 |  153707   25959   551309    21.2 |  0.955 % |
c |     27291 |  260024   634205 |  169078   27084   590296    21.8 |  0.985 % |
c |     28999 |  259993   634140 |  185986   28786   667602    23.2 |  0.999 % |
c ==============================================================================
c [1mFound solution: 383599[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30297 |  259991   634146 |   86663   30083   722960    24.0 |  0.999 % |
c |     30398 |  259991   634146 |   95329   30184   723507    24.0 |  1.009 % |
c |     30548 |  259991   634146 |  104862   30334   731321    24.1 |  1.009 % |
c |     30773 |  259991   634146 |  115348   30559   740044    24.2 |  1.009 % |
c |     31110 |  259991   634146 |  126883   30896   757801    24.5 |  1.009 % |
c |     31616 |  259986   634136 |  139571   31401   795591    25.3 |  1.011 % |
c |     32375 |  259986   634136 |  153528   32160   811569    25.2 |  1.011 % |
c ==============================================================================
c [1mFound solution: 383392[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33409 |  260296   634899 |   86765   33192  1026805    30.9 |  1.011 % |
c |     33510 |  260296   634899 |   95441   33293  1028044    30.9 |  1.019 % |
c |     33660 |  260254   634805 |  104985   33442  1029010    30.8 |  1.032 % |
c ==============================================================================
c [1mFound solution: 383373[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33875 |  260270   634911 |   86756   33657  1039247    30.9 |  1.032 % |
c |     33977 |  260210   634775 |   95431   33756  1040147    30.8 |  1.053 % |
c |     34127 |  260210   634775 |  104974   33906  1052811    31.1 |  1.053 % |
c |     34352 |  260210   634775 |  115472   34131  1056678    31.0 |  1.053 % |
c |     34689 |  260210   634775 |  127019   34468  1061751    30.8 |  1.053 % |
c ==============================================================================
c [1mFound solution: 318384[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35133 |  259715   633655 |   86571   34785  1072391    30.8 |  1.053 % |
c |     35233 |  259715   633655 |   95228   34885  1073164    30.8 |  1.226 % |
c |     35386 |  259649   633523 |  104750   35029  1078371    30.8 |  1.258 % |
c |     35611 |  259618   633461 |  115226   35249  1087712    30.9 |  1.275 % |
c |     35949 |  259614   633453 |  126748   35586  1103199    31.0 |  1.277 % |
c |     36455 |  259599   633423 |  139423   36089  1122017    31.1 |  1.285 % |
c |     37214 |  259579   633383 |  153365   36845  1154883    31.3 |  1.296 % |
c ==============================================================================
c [1mFound solution: 317925[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38325 |  259585   633404 |   86528   37955  1214043    32.0 |  1.296 % |
c |     38427 |  259565   633364 |   95180   38054  1217602    32.0 |  1.310 % |
c |     38577 |  259535   633304 |  104698   38201  1222037    32.0 |  1.325 % |
c |     38802 |  259535   633304 |  115168   38426  1227700    31.9 |  1.325 % |
c |     39141 |  259535   633304 |  126685   38765  1237209    31.9 |  1.325 % |
c |     39648 |  259526   633286 |  139354   39271  1256851    32.0 |  1.330 % |
c |     40407 |  259522   633278 |  153289   40029  1288481    32.2 |  1.332 % |
c |     41546 |  259517   633268 |  168618   41167  1326087    32.2 |  1.334 % |
c |     43254 |  259460   633142 |  185480   42870  1386419    32.3 |  1.356 % |
c |     45816 |  259419   633060 |  204028   45427  1521554    33.5 |  1.377 % |
c |     49660 |  258859   631791 |  224431   49118  1869936    38.1 |  1.558 % |
c ==============================================================================
c [1mFound solution: 305343[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     55343 |  258834   631748 |   86278   54798  2461904    44.9 |  1.558 % |
c |     55443 |  258834   631748 |   94905   54898  2462663    44.9 |  1.575 % |
c |     55593 |  258834   631748 |  104396   55048  2468731    44.8 |  1.575 % |
c |     55818 |  258834   631748 |  114836   55273  2487604    45.0 |  1.575 % |
c |     56156 |  258834   631748 |  126319   55611  2498140    44.9 |  1.575 % |
c |     56662 |  258834   631748 |  138951   56117  2518653    44.9 |  1.575 % |
c |     57421 |  258823   631726 |  152846   56874  2567043    45.1 |  1.581 % |
c ==============================================================================
c [1mFound solution: 290530[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     57859 |  258836   631758 |   86278   57312  2580735    45.0 |  1.581 % |
c |     57960 |  258836   631758 |   94905   57413  2582909    45.0 |  1.582 % |
c |     58112 |  258836   631758 |  104396   57565  2587831    45.0 |  1.582 % |
c |     58337 |  258830   631746 |  114836   57789  2597800    45.0 |  1.583 % |
c ==============================================================================
c [1mFound solution: 290528[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     58358 |  258845   631783 |   86281   57810  2598676    45.0 |  1.583 % |
c ==============================================================================
c [1mFound solution: 290527[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   13     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     58404 |  258860   631820 |   86286   57856  2601769    45.0 |  1.583 % |
c |     58504 |  258860   631820 |   94914   57956  2603402    44.9 |  1.585 % |
c |     58655 |  258852   631804 |  104406   58106  2613659    45.0 |  1.589 % |
c ==============================================================================
c [1mFound solution: 287841[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     58764 |  258862   631832 |   86287   58215  2617539    45.0 |  1.589 % |
c |     58865 |  258856   631820 |   94915   58315  2619535    44.9 |  1.593 % |
c |     59015 |  258856   631820 |  104407   58465  2622663    44.9 |  1.593 % |
c ==============================================================================
c [1mFound solution: 283466[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     59055 |  258864   631843 |   86288   58505  2625065    44.9 |  1.593 % |
c |     59155 |  258864   631843 |   94916   58605  2627960    44.8 |  1.594 % |
c ==============================================================================
c [1mFound solution: 279099[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     59200 |  258871   631861 |   86290   58650  2629948    44.8 |  1.594 % |
c |     59301 |  258868   631855 |   94919   58750  2631351    44.8 |  1.597 % |
c |     59453 |  258860   631839 |  104410   58901  2637144    44.8 |  1.601 % |
c |     59678 |  258860   631839 |  114851   59126  2644810    44.7 |  1.601 % |
c ==============================================================================
c [1mFound solution: 279045[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     59740 |  258864   631852 |   86288   59188  2648305    44.7 |  1.601 % |
c |     59842 |  258864   631852 |   94916   59290  2649226    44.7 |  1.602 % |
c |     59993 |  258864   631852 |  104408   59441  2663337    44.8 |  1.602 % |
c ==============================================================================
c [1mFound solution: 278856[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     60069 |  258870   631870 |   86290   59517  2666809    44.8 |  1.602 % |
c |     60170 |  258870   631870 |   94919   59618  2673298    44.8 |  1.603 % |
c |     60321 |  258870   631870 |  104410   59769  2676279    44.8 |  1.603 % |
c |     60548 |  258870   631870 |  114851   59996  2678394    44.6 |  1.603 % |
c |     60885 |  258822   631759 |  126337   60322  2684244    44.5 |  1.620 % |
c ==============================================================================
c [1mFound solution: 277560[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     61048 |  258566   631181 |   86188   60337  2688173    44.6 |  1.620 % |
c |     61151 |  258566   631181 |   94806   60440  2689659    44.5 |  1.706 % |
c ==============================================================================
c [1mFound solution: 277559[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     61253 |  258576   631209 |   86192   60542  2707018    44.7 |  1.706 % |
c |     61353 |  258576   631209 |   94811   60642  2714710    44.8 |  1.707 % |
c ==============================================================================
c [1mFound solution: 277236[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     61392 |  258585   631232 |   86195   60681  2717923    44.8 |  1.707 % |
c |     61492 |  258585   631232 |   94814   60781  2718678    44.7 |  1.708 % |
c |     61642 |  258585   631232 |  104295   60931  2719454    44.6 |  1.708 % |
c |     61867 |  258585   631232 |  114725   61156  2721153    44.5 |  1.708 % |
c ==============================================================================
c [1mFound solution: 272129[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     62028 |  258564   631188 |   86188   61310  2732343    44.6 |  1.708 % |
c |     62128 |  258564   631188 |   94806   61410  2733047    44.5 |  1.722 % |
c |     62278 |  258564   631188 |  104287   61560  2734312    44.4 |  1.722 % |
c |     62503 |  258564   631188 |  114716   61785  2746631    44.5 |  1.722 % |
c |     62840 |  258564   631188 |  126187   62122  2759703    44.4 |  1.722 % |
c ==============================================================================
c [1mFound solution: 272050[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   13     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     63173 |  258579   631225 |   86193   62455  2785209    44.6 |  1.722 % |
c |     63276 |  258565   631194 |   94812   62557  2786113    44.5 |  1.728 % |
c |     63426 |  258535   631126 |  104293   62703  2787063    44.4 |  1.739 % |
c |     63651 |  258535   631126 |  114722   62928  2790061    44.3 |  1.739 % |
c |     63989 |  258535   631126 |  126195   63266  2802547    44.3 |  1.739 % |
c |     64496 |  258535   631126 |  138814   63773  2821126    44.2 |  1.739 % |
c ==============================================================================
c [1mFound solution: 265650[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     64933 |  258545   631154 |   86181   64210  2852228    44.4 |  1.739 % |
c |     65033 |  258545   631154 |   94799   64310  2853036    44.4 |  1.740 % |
c ==============================================================================
c [1mFound solution: 265638[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     65132 |  258557   631186 |   86185   64409  2869151    44.5 |  1.740 % |
c |     65232 |  258557   631186 |   94803   64509  2871427    44.5 |  1.741 % |
c |     65382 |  258557   631186 |  104283   64659  2881321    44.6 |  1.741 % |
c ==============================================================================
c [1mFound solution: 265637[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     65471 |  258569   631218 |   86189   64748  2901728    44.8 |  1.741 % |
c |     65571 |  258557   631194 |   94807   64847  2911842    44.9 |  1.748 % |
c ==============================================================================
c [1mFound solution: 264519[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     65664 |  258567   631221 |   86189   64940  2917915    44.9 |  1.748 % |
c ==============================================================================
c [1mFound solution: 264518[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     65715 |  258577   631248 |   86192   64991  2921203    44.9 |  1.748 % |
c ==============================================================================
c [1mFound solution: 264465[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     65783 |  258418   630892 |   86139   65056  2923493    44.9 |  1.748 % |
c |     65884 |  258418   630892 |   94752   65157  2928037    44.9 |  1.799 % |
c |     66034 |  258384   630816 |  104228   65299  2932068    44.9 |  1.810 % |
c |     66260 |  258384   630816 |  114651   65525  2958591    45.2 |  1.811 % |
c |     66597 |  258384   630816 |  126116   65862  2966889    45.0 |  1.810 % |
c |     67103 |  258384   630816 |  138727   66368  3037060    45.8 |  1.810 % |
c ==============================================================================
c [1mFound solution: 264447[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     67661 |  258397   630849 |   86132   66926  3090836    46.2 |  1.810 % |
c |     67761 |  258397   630849 |   94745   67026  3100242    46.3 |  1.811 % |
c ==============================================================================
c [1mFound solution: 264444[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     67823 |  258407   630875 |   86135   67088  3103504    46.3 |  1.811 % |
c ==============================================================================
c [1mFound solution: 264383[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     67900 |  258400   630868 |   86133   67164  3107153    46.3 |  1.811 % |
c ==============================================================================
c [1mFound solution: 264357[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     67939 |  258413   630901 |   86137   67203  3109779    46.3 |  1.811 % |
c ==============================================================================
c [1mFound solution: 264355[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     67943 |  258426   630934 |   86142   67207  3110039    46.3 |  1.811 % |
c ==============================================================================
c [1mFound solution: 264354[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     67943 |  258438   630964 |   86146   67207  3110039    46.3 |  1.811 % |
c ==============================================================================
c [1mFound solution: 264353[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     67943 |  258448   630989 |   86149   67207  3110039    46.3 |  1.811 % |
c ==============================================================================
c [1mFound solution: 264302[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     68032 |  258463   631026 |   86154   67296  3119681    46.4 |  1.811 % |
c |     68132 |  258463   631026 |   94769   67396  3124553    46.4 |  1.828 % |
c |     68282 |  258463   631026 |  104246   67546  3125260    46.3 |  1.828 % |
c |     68507 |  258463   631026 |  114670   67771  3127185    46.1 |  1.828 % |
c |     68844 |  258463   631026 |  126138   68108  3144543    46.2 |  1.828 % |
c |     69350 |  258463   631026 |  138751   68614  3214367    46.8 |  1.828 % |
c ==============================================================================
c [1mFound solution: 264301[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     69582 |  257660   629190 |   85886   68549  3225778    47.1 |  1.828 % |
c |     69683 |  257590   629032 |   94474   68622  3234531    47.1 |  2.119 % |
c ==============================================================================
c [1mFound solution: 264300[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     69768 |  257299   628383 |   85766   68625  3233461    47.1 |  2.119 % |
c |     69868 |  257299   628383 |   94342   68725  3234700    47.1 |  2.215 % |
c |     70018 |  257299   628383 |  103776   68875  3238067    47.0 |  2.215 % |
c |     70244 |  257299   628383 |  114154   69101  3302028    47.8 |  2.215 % |
c |     70581 |  256729   627053 |  125570   69183  3313410    47.9 |  2.359 % |
c ==============================================================================
c [1mFound solution: 264299[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:56640     Base: 2 3 3 3 3 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     70744 |  378226   912020 |  126075   47540  1669310    35.1 |  2.359 % |
c |     70844 |  378226   912020 |  138682   47640  1682168    35.3 |  9.615 % |
c |     70994 |  378216   912000 |  152550   47789  1684099    35.2 |  9.618 % |
c |     71220 |  378216   912000 |  167805   48015  1687574    35.1 |  9.618 % |
c |     71557 |  377913   911299 |  184586   48288  1693430    35.1 |  9.685 % |
c ==============================================================================
c [1mFound solution: 264285[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 2 3 3 3 3 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     71778 |  379169   914610 |  126389   48509  1702107    35.1 |  9.685 % |
c |     71879 |  379169   914610 |  139027   48610  1705760    35.1 |  9.640 % |
c |     72029 |  379169   914610 |  152930   48760  1718150    35.2 |  9.640 % |
c |     72258 |  379088   914428 |  168223   48973  1725418    35.2 |  9.657 % |
c |     72595 |  378982   914188 |  185046   49304  1727606    35.0 |  9.677 % |
c |     73102 |  378666   913457 |  203550   49765  1762749    35.4 |  9.747 % |
c ==============================================================================
c [1mFound solution: 264276[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 2 3 3 3 3 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     73391 |  378684   913676 |  126228   50054  1787130    35.7 |  9.747 % |
c |     73491 |  378684   913676 |  138850   50154  1795616    35.8 |  9.747 % |
c |     73641 |  377425   910781 |  152735   50183  1804250    36.0 | 10.003 % |
c |     73867 |  377425   910781 |  168009   50409  1817190    36.0 | 10.003 % |
c |     74204 |  377353   910616 |  184810   50706  1869511    36.9 | 10.018 % |
c |     74710 |  377332   910570 |  203291   51211  1921991    37.5 | 10.022 % |
c ==============================================================================
c [1mFound solution: 264219[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:42445     Base: 2 3 3 3 3 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     75004 |  495338  1186465 |  165112   51448  1938389    37.7 | 10.022 % |
c |     75104 |  495338  1186465 |  181623   51548  1939985    37.6 |  7.895 % |
c |     75254 |  495338  1186465 |  199785   51698  1959166    37.9 |  7.895 % |
c |     75479 |  495241  1186246 |  219764   51921  1960851    37.8 |  7.908 % |
c |     75816 |  495241  1186246 |  241740   52258  1964691    37.6 |  7.908 % |
c |     76322 |  438827  1051984 |  265914   36354  1263820    34.8 | 16.377 % |
c ==============================================================================
c [1mFound solution: 264209[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:45914     Base: 2 2 2 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     76520 |  565573  1348068 |  188524   36552  1302730    35.6 | 16.377 % |
c |     76620 |  564905  1346531 |  207376   36642  1303393    35.6 | 13.398 % |
c |     76770 |  564366  1345292 |  228114   36791  1305213    35.5 | 13.471 % |
c |     76995 |  396117   954805 |  250925   22642   990524    43.7 | 36.828 % |
c ==============================================================================
c [1mFound solution: 264114[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:27015     Base: 2 2 2 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     77256 |  470026  1127459 |  156675   22892  1020758    44.6 | 36.828 % |
c |     77357 |  470026  1127459 |  172342   22993  1021323    44.4 | 33.220 % |
c |     77507 |  469830  1127006 |  189576   23141  1022275    44.2 | 33.245 % |
c ==============================================================================
c [1mFound solution: 261603[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     77706 |  470864  1129532 |  156954   23340  1032986    44.3 | 33.245 % |
c |     77806 |  470864  1129532 |  172649   23440  1037194    44.2 | 33.171 % |
c |     77956 |  447096  1073845 |  189914   20490   679598    33.2 | 36.059 % |
c |     78183 |  446684  1072901 |  208905   20703   681233    32.9 | 36.108 % |
c ==============================================================================
c [1mFound solution: 259554[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:20206     Base: 2 2 2 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     78401 |  500858  1199505 |  166952   20905   684559    32.7 | 36.108 % |
c |     78501 |  498514  1193906 |  183647   20506   600301    29.3 | 33.957 % |
c |     78651 |  498514  1193906 |  202011   20656   602273    29.2 | 33.957 % |
c |     78877 |  497979  1192672 |  222213   20856   604194    29.0 | 34.019 % |
c |     79214 |  497581  1191770 |  244434   21187   607057    28.7 | 34.060 % |
c |     79721 |  497470  1191522 |  268877   21692   618874    28.5 | 34.073 % |
c |     80480 |  497470  1191522 |  295765   22451   652976    29.1 | 34.073 % |
c |     81619 |  497470  1191522 |  325342   23590   667408    28.3 | 34.073 % |
c ==============================================================================
c [1mFound solution: 259398[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:17747     Base: 2 2 2 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     81871 |  543767  1299722 |  181255   23810   671963    28.2 | 34.073 % |
c |     81971 |  543767  1299722 |  199380   23910   675626    28.3 | 32.255 % |
c |     82121 |  543767  1299722 |  219318   24060   677124    28.1 | 32.255 % |
c |     82346 |  543211  1298451 |  241250   24283   685206    28.2 | 32.315 % |
c |     82684 |  543081  1298159 |  265375   24619   724023    29.4 | 32.327 % |
c |     83192 |  543081  1298159 |  291912   25127   759113    30.2 | 32.327 % |
c |     83951 |  538523  1287489 |  321104   25673   761561    29.7 | 32.788 % |
c ==============================================================================
c [1mFound solution: 259268[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:16393     Base: 2 2 2 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     84408 |  580341  1385362 |  193447   26116   767725    29.4 | 32.788 % |
c |     84508 |  579728  1383963 |  212791   26201   771304    29.4 | 31.367 % |
c |     84658 |  579728  1383963 |  234070   26351   775367    29.4 | 31.367 % |
c |     84883 |  579623  1383722 |  257477   26556   779443    29.4 | 31.377 % |
c ==============================================================================
c [1mFound solution: 258723[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     85008 |  580679  1386452 |  193559   26679   782239    29.3 | 31.377 % |
c ==============================================================================
c [1mFound solution: 258686[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     85036 |  580696  1386778 |  193565   26707   783980    29.4 | 31.377 % |
c ==============================================================================
c [1mFound solution: 258675[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     85114 |  580705  1386801 |  193568   26785   787715    29.4 | 31.377 % |
c ==============================================================================
c [1mFound solution: 258673[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     85136 |  580718  1386863 |  193572   26807   789193    29.4 | 31.377 % |
c ==============================================================================
c [1mFound solution: 258574[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     85151 |  580728  1386887 |  193576   26822   790269    29.5 | 31.377 % |
c ==============================================================================
c [1mFound solution: 258572[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     85181 |  580592  1386588 |  193530   26850   791123    29.5 | 31.377 % |
c ==============================================================================
c [1mFound solution: 258565[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     85218 |  580603  1386614 |  193534   26887   792119    29.5 | 31.377 % |
c ==============================================================================
c [1mFound solution: 258564[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     85221 |  580610  1386631 |  193536   26890   792243    29.5 | 31.377 % |
c ==============================================================================
c [1mFound solution: 258503[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     85242 |  580763  1387004 |  193587   26911   793344    29.5 | 31.377 % |
c ==============================================================================
c [1mFound solution: 258499[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     85245 |  580777  1387069 |  193592   26914   793384    29.5 | 31.377 % |
c ==============================================================================
c [1mFound solution: 258498[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     85249 |  580790  1387101 |  193596   26918   793422    29.5 | 31.377 % |
c ==============================================================================
c [1mFound solution: 258495[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     85255 |  580802  1387130 |  193600   26924   793587    29.5 | 31.377 % |
c ==============================================================================
c [1mFound solution: 258491[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:16466     Base: 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     85265 |  473496  1133659 |  157832   19439   546569    28.1 | 31.377 % |
c ==============================================================================
c [1mFound solution: 258487[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     85314 |  473506  1133730 |  157835   19488   547745    28.1 | 31.377 % |
c |     85414 |  473492  1133688 |  173618   19587   555585    28.4 | 45.353 % |
c |     85564 |  349005   841348 |  190980   14088   372704    26.5 | 58.267 % |
c |     85791 |  348792   840857 |  210078   14200   372199    26.2 | 58.287 % |
c ==============================================================================
c [1mFound solution: 258485[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 7830     Base: 2 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     85952 |  289823   701839 |   96607   11007   275553    25.0 | 58.287 % |
c |     86055 |  289823   701839 |  106267   11110   277494    25.0 | 65.229 % |
c |     86206 |  288858   699600 |  116894   11135   277859    25.0 | 65.325 % |
c |     86431 |  288236   698156 |  128583   11325   281557    24.9 | 65.387 % |
c ==============================================================================
c [1mFound solution: 258484[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 3814     Base: 2 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86528 |  197583   484945 |   65861    7354   169071    23.0 | 65.387 % |
c |     86628 |  197583   484945 |   72447    7454   174272    23.4 | 75.051 % |
c ==============================================================================
c [1mFound solution: 258474[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 1800     Base: 2 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86643 |  170196   420223 |   56732    6170   143483    23.3 | 75.051 % |
c ==============================================================================
c [1mFound solution: 258470[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 1664     Base: 2 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86643 |  168420   416084 |   56140    6066   139143    22.9 | 75.051 % |
c ==============================================================================
c [1mFound solution: 258451[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 1686     Base: 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86678 |  153726   381437 |   51242    5352   122454    22.9 | 75.051 % |
c ==============================================================================
c [1mFound solution: 258446[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 1287     Base: 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86683 |  136814   341460 |   45604    4582   105203    23.0 | 75.051 % |
c ==============================================================================
c [1mFound solution: 258445[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 1117     Base: 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86683 |  133252   333086 |   44417    4267   100418    23.5 | 75.051 % |
c |     86785 |  133252   333086 |   48858    4369   102963    23.6 | 81.993 % |
c |     86935 |  133252   333086 |   53744    4519   106395    23.5 | 81.993 % |
c ==============================================================================
c [1mFound solution: 258444[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 1085     Base: 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86956 |  130733   327129 |   43577    4405   103615    23.5 | 81.993 % |
c ==============================================================================
c [1mFound solution: 258443[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86957 |  130788   327268 |   43596    4406   103651    23.5 | 81.993 % |
c ==============================================================================
c [1mFound solution: 258432[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  924     Base: 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86965 |  106418   269969 |   35472    3602    88189    24.5 | 81.993 % |
c ==============================================================================
c [1mFound solution: 258431[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  412     Base: 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86985 |   90527   232196 |   30175    2841    71425    25.1 | 81.993 % |
c ==============================================================================
c [1mFound solution: 258429[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  494     Base: 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86991 |   88565   227476 |   29521    2703    67800    25.1 | 81.993 % |
c ==============================================================================
c [1mFound solution: 258428[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86991 |   88574   227516 |   29524    2703    67800    25.1 | 81.993 % |
c ==============================================================================
c [1mFound solution: 258427[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  395     Base: 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86991 |   81553   210852 |   27184    2400    64782    27.0 | 81.993 % |
c ==============================================================================
c [1mFound solution: 258426[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  321     Base: 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86992 |   66979   176429 |   22326    1843    48696    26.4 | 81.993 % |
c ==============================================================================
c [1mFound solution: 258425[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  283     Base: 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86992 |   63683   168651 |   21227    1578    42076    26.7 | 81.993 % |
c ==============================================================================
c [1mFound solution: 258424[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86997 |   63687   168661 |   21229    1583    42130    26.6 | 81.993 % |
c ==============================================================================
c [1mFound solution: 258419[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  114     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86997 |   47679   130457 |   15893     873    18805    21.5 | 81.993 % |
c ==============================================================================
c [1mFound solution: 258417[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   40     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86997 |   36914   104650 |   12304     449     9241    20.6 | 81.993 % |
c ==============================================================================
c [1mFound solution: 258416[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   27     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     87001 |   33305    95968 |   11101     335     7262    21.7 | 81.993 % |
c ==============================================================================
c [1mFound solution: 258414[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     87004 |   24923    74959 |    8307     157     3553    22.6 | 81.993 % |
c ==============================================================================
c [1mFound solution: 258413[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     87004 |   23089    70204 |    7696     106     2619    24.7 | 81.993 % |
c ==============================================================================
c [1mFound solution: 258411[0m
c [1mOptimal solution: 258411[0m
s OPTIMUM FOUND
v -x0 -x1 -x2 x3 -x4 -x5 -x6 -x7 -x8 -x9 -x10 x11 -x12 -x13 -x14 -x15 -x16 -x17 -x18 -x19 -x20 -x21 -x22 -x23 -x24 -x25 -x26 -x27 -x28 -x29 -x30 -x31 -x32 -x33 -x34 -x35 -x36 -x37 -x38 -x39 -x40 -x41 -x42 -x43 -x44 -x45 -x46 -x47 -x48 -x49 -x50 -x51 -x52 -x53 -x54 -x55 -x56 -x57 -x58 -x59 -x60 -x61 -x62 -x63 -x64 -x65 -x66 -x67 -x68 -x69 -x70 -x71 -x72 -x73 -x74 -x75 -x76 -x77 -x78 -x79 -x80 -x81 -x82 -x83 -x84 -x85 -x86 -x87 -x88 -x89 -x90 x91 -x92 -x93 -x94 -x95 -x96 -x97 -x98 -x99 -x100 x101 -x102 x103 -x104 -x105 -x106 -x107 -x108 -x109 -x110 -x111 -x112 -x113 -x114 -x115 -x116 x117 -x118 -x119 -x120 -x121 -x122 -x123 -x124 -x125 -x126 -x127 -x128 -x129 -x130 -x131 -x132 -x133 -x134 -x135 -x136 -x137 -x138 -x139 -x140 -x141 -x142 -x143 -x144 -x145 -x146 -x147 -x148 -x149 -x150 -x151 -x152 -x153 -x154 x155 -x156 -x157 -x158 -x159 -x160 -x161 -x162 -x163 -x164 -x165 -x166 -x167 -x168 x169 -x170 -x171 -x172 -x173 -x174 -x175 -x176 -x177 -x178 -x179 -x180 -x181 -x182 -x183 -x184 -x185 -x186 -x187 -x188 -x189 -x190 x191 -x192 -x193 -x194 -x195 -x196 -x197 -x198 x199 -x200 -x201 -x202 -x203 -x204 -x205 -x206 -x207 -x208 -x209 -x210 -x211 -x212 -x213 -x214 x215 -x216 -x217 -x218 -x219 -x220 -x221 -x222 x223 -x224 x225 -x226 -x227 -x228 -x229 -x230 -x231 -x232 -x233 -x234 -x235 -x236 x237 -x238 -x239 x240 -x241 x242 x243 x244 -x245 x246 -x247 x248 -x249 -x250 x251 -x252 -x253 x254 -x255 x256 x257 -x258 -x259 x260 -x261 x262 x263 -x264 -x265 -x266 -x267 -x268 -x269 -x270 -x271 -x272 x273 -x274 x275 x276 x277 -x278 -x279 x280 x281
c _______________________________________________________________________________
c 
c restarts              : 271
c conflicts             : 87004          (111 /sec)
c decisions             : 904252         (1156 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 782.453 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.95 0.96 0.72 2/54 24031
Raw data (stat): 24031 (runsolver) R 24030 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 429385165 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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+9.99981 s]
Raw data (loadavg): 0.95 0.96 0.72 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 8008 0 0 0 982 16 0 0 25 0 1 0 429385165 36462592 7662 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8902 7662 603 41 0 8861 0
vsize: 35608
[startup+20.0012 s]
Raw data (loadavg): 0.96 0.96 0.73 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 8165 0 0 0 1982 17 0 0 25 0 1 0 429385165 37003264 7819 4294967295 134512640 134672761 3221224560 3221223800 134558237 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9034 7819 603 41 0 8993 0
vsize: 36136
[startup+30.0015 s]
Raw data (loadavg): 0.97 0.96 0.73 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 8368 0 0 0 2981 17 0 0 25 0 1 0 429385165 37900288 8022 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9253 8022 603 41 0 9212 0
vsize: 37012
[startup+40.0014 s]
Raw data (loadavg): 0.97 0.96 0.73 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 8472 0 0 0 3980 18 0 0 25 0 1 0 429385165 38268928 8126 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9343 8126 603 41 0 9302 0
vsize: 37372
[startup+50.0027 s]
Raw data (loadavg): 0.98 0.96 0.73 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 8562 0 0 0 4979 19 0 0 25 0 1 0 429385165 38674432 8216 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9442 8216 603 41 0 9401 0
vsize: 37768
[startup+60.003 s]
Raw data (loadavg): 0.98 0.96 0.74 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 8636 0 0 0 5978 20 0 0 25 0 1 0 429385165 38998016 8290 4294967295 134512640 134672761 3221224560 3221223696 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9521 8290 603 41 0 9480 0
vsize: 38084
[startup+70.0039 s]
Raw data (loadavg): 0.98 0.96 0.74 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 8707 0 0 0 6978 21 0 0 25 0 1 0 429385165 39264256 8361 4294967295 134512640 134672761 3221224560 3221223744 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9586 8361 603 41 0 9545 0
vsize: 38344
[startup+80.0052 s]
Raw data (loadavg): 0.98 0.96 0.74 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 8780 0 0 0 7977 21 0 0 25 0 1 0 429385165 39583744 8434 4294967295 134512640 134672761 3221224560 3221223696 134560598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9664 8434 603 41 0 9623 0
vsize: 38656
[startup+90.0046 s]
Raw data (loadavg): 0.99 0.96 0.74 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 8818 0 0 0 8976 22 0 0 25 0 1 0 429385165 39718912 8472 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9697 8472 603 41 0 9656 0
vsize: 38788
[startup+100.005 s]
Raw data (loadavg): 0.99 0.97 0.74 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 8873 0 0 0 9975 22 0 0 25 0 1 0 429385165 39985152 8527 4294967295 134512640 134672761 3221224560 3221223664 134560010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9762 8527 603 41 0 9721 0
vsize: 39048
[startup+110.007 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 8923 0 0 0 10975 23 0 0 25 0 1 0 429385165 40116224 8577 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9794 8577 603 41 0 9753 0
vsize: 39176
[startup+120.008 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 9026 0 0 0 11974 24 0 0 25 0 1 0 429385165 40517632 8680 4294967295 134512640 134672761 3221224560 3221223776 134561948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9892 8680 603 41 0 9851 0
vsize: 39568
[startup+130.008 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 9108 0 0 0 12974 24 0 0 25 0 1 0 429385165 40914944 8762 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9989 8762 603 41 0 9948 0
vsize: 39956
[startup+140.008 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 9334 0 0 0 13973 25 0 0 25 0 1 0 429385165 41971712 8988 4294967295 134512640 134672761 3221224560 3221223616 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10247 8988 603 41 0 10206 0
vsize: 40988
[startup+150.009 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 9406 0 0 0 14972 25 0 0 25 0 1 0 429385165 42172416 9060 4294967295 134512640 134672761 3221224560 3221223732 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10296 9060 603 41 0 10255 0
vsize: 41184
[startup+160.009 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 9435 0 0 0 15972 26 0 0 25 0 1 0 429385165 42303488 9089 4294967295 134512640 134672761 3221224560 3221223744 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10328 9089 603 41 0 10287 0
vsize: 41312
[startup+170.011 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 9473 0 0 0 16971 26 0 0 25 0 1 0 429385165 42434560 9127 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10360 9127 603 41 0 10319 0
vsize: 41440
[startup+180.011 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 9521 0 0 0 17971 27 0 0 25 0 1 0 429385165 42700800 9175 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10425 9175 603 41 0 10384 0
vsize: 41700
[startup+190.011 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 9586 0 0 0 18970 27 0 0 25 0 1 0 429385165 42967040 9240 4294967295 134512640 134672761 3221224560 3221222688 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10490 9240 603 41 0 10449 0
vsize: 41960
[startup+200.012 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 9614 0 0 0 19970 27 0 0 25 0 1 0 429385165 43098112 9268 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10522 9268 603 41 0 10481 0
vsize: 42088
[startup+210.013 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 9661 0 0 0 20969 28 0 0 25 0 1 0 429385165 43229184 9315 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10554 9315 603 41 0 10513 0
vsize: 42216
[startup+220.014 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 9743 0 0 0 21969 29 0 0 25 0 1 0 429385165 43663360 9397 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10660 9397 603 41 0 10619 0
vsize: 42640
[startup+230.015 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 9798 0 0 0 22968 29 0 0 25 0 1 0 429385165 43794432 9452 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10692 9452 603 41 0 10651 0
vsize: 42768
[startup+240.014 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 9869 0 0 0 23968 29 0 0 25 0 1 0 429385165 44191744 9523 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10789 9523 603 41 0 10748 0
vsize: 43156
[startup+250.015 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 9916 0 0 0 24968 30 0 0 25 0 1 0 429385165 44322816 9570 4294967295 134512640 134672761 3221224560 3221223704 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10821 9570 603 41 0 10780 0
vsize: 43284
[startup+260.016 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 9970 0 0 0 25967 30 0 0 25 0 1 0 429385165 44449792 9624 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10852 9624 603 41 0 10811 0
vsize: 43408
[startup+270.017 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 10052 0 0 0 26966 31 0 0 25 0 1 0 429385165 44847104 9706 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10949 9706 603 41 0 10908 0
vsize: 43796
[startup+280.017 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 10127 0 0 0 27966 31 0 0 25 0 1 0 429385165 45117440 9781 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11015 9781 603 41 0 10974 0
vsize: 44060
[startup+290.018 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 10218 0 0 0 28965 32 0 0 25 0 1 0 429385165 45506560 9872 4294967295 134512640 134672761 3221224560 3221223664 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11110 9872 603 41 0 11069 0
vsize: 44440
[startup+300.018 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 10290 0 0 0 29964 33 0 0 25 0 1 0 429385165 45764608 9944 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11173 9944 603 41 0 11132 0
vsize: 44692
[startup+310.018 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 10364 0 0 0 30964 33 0 0 25 0 1 0 429385165 46153728 10018 4294967295 134512640 134672761 3221224560 3221223728 134559131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11268 10018 603 41 0 11227 0
vsize: 45072
[startup+320.019 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 10442 0 0 0 31963 34 0 0 25 0 1 0 429385165 46415872 10096 4294967295 134512640 134672761 3221224560 3221223664 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11332 10096 603 41 0 11291 0
vsize: 45328
[startup+330.02 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 10557 0 0 0 32963 34 0 0 25 0 1 0 429385165 46948352 10211 4294967295 134512640 134672761 3221224560 3221223664 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11462 10211 603 41 0 11421 0
vsize: 45848
[startup+340.019 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 10662 0 0 0 33962 35 0 0 25 0 1 0 429385165 47329280 10316 4294967295 134512640 134672761 3221224560 3221223696 134560619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11555 10316 603 41 0 11514 0
vsize: 46220
[startup+350.021 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 10736 0 0 0 34962 35 0 0 25 0 1 0 429385165 47587328 10390 4294967295 134512640 134672761 3221224560 3221223664 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11618 10390 603 41 0 11577 0
vsize: 46472
[startup+360.021 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 10818 0 0 0 35961 36 0 0 25 0 1 0 429385165 47980544 10472 4294967295 134512640 134672761 3221224560 3221223728 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11714 10472 603 41 0 11673 0
vsize: 46856
[startup+370.022 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 10898 0 0 0 36960 36 0 0 25 0 1 0 429385165 48242688 10552 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11778 10552 603 41 0 11737 0
vsize: 47112
[startup+380.023 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 10957 0 0 0 37960 37 0 0 25 0 1 0 429385165 48504832 10611 4294967295 134512640 134672761 3221224560 3221223696 134560611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11842 10611 603 41 0 11801 0
vsize: 47368
[startup+390.023 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 11011 0 0 0 38959 38 0 0 25 0 1 0 429385165 48730112 10665 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11897 10665 603 41 0 11856 0
vsize: 47588
[startup+400.024 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 11053 0 0 0 39958 38 0 0 25 0 1 0 429385165 48873472 10707 4294967295 134512640 134672761 3221224560 3221223728 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11932 10707 603 41 0 11891 0
vsize: 47728
[startup+410.025 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 11106 0 0 0 40958 39 0 0 25 0 1 0 429385165 49135616 10760 4294967295 134512640 134672761 3221224560 3221223684 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11996 10760 603 41 0 11955 0
vsize: 47984
[startup+420.025 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 11184 0 0 0 41957 40 0 0 25 0 1 0 429385165 49405952 10838 4294967295 134512640 134672761 3221224560 3221223860 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12062 10838 603 41 0 12021 0
vsize: 48248
[startup+430.025 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 11208 0 0 0 42956 40 0 0 25 0 1 0 429385165 49528832 10862 4294967295 134512640 134672761 3221224560 3221223728 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12092 10862 603 41 0 12051 0
vsize: 48368
[startup+440.025 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 11229 0 0 0 43956 40 0 0 25 0 1 0 429385165 49594368 10883 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12108 10883 603 41 0 12067 0
vsize: 48432
[startup+450.026 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 11277 0 0 0 44955 41 0 0 25 0 1 0 429385165 49782784 10931 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12154 10931 603 41 0 12113 0
vsize: 48616
[startup+460.027 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 11330 0 0 0 45955 41 0 0 25 0 1 0 429385165 49971200 10984 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12200 10984 603 41 0 12159 0
vsize: 48800
[startup+470.027 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 11412 0 0 0 46954 42 0 0 25 0 1 0 429385165 50331648 11066 4294967295 134512640 134672761 3221224560 3221223728 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12288 11066 603 41 0 12247 0
vsize: 49152
[startup+480.027 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 11489 0 0 0 47954 42 0 0 25 0 1 0 429385165 50601984 11143 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12354 11143 603 41 0 12313 0
vsize: 49416
[startup+490.027 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 11548 0 0 0 48954 42 0 0 25 0 1 0 429385165 50864128 11202 4294967295 134512640 134672761 3221224560 3221223120 134597191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12418 11202 603 41 0 12377 0
vsize: 49672
[startup+500.028 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 11607 0 0 0 49954 42 0 0 25 0 1 0 429385165 51462144 11261 4294967295 134512640 134672761 3221224560 3221223728 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12564 11261 603 41 0 12523 0
vsize: 50256
[startup+510.029 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 11754 0 0 0 50953 43 0 0 25 0 1 0 429385165 52011008 11408 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12698 11408 603 41 0 12657 0
vsize: 50792
[startup+520.029 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 24031
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 11783 0 0 0 51952 44 0 0 25 0 1 0 429385165 52125696 11437 4294967295 134512640 134672761 3221224560 3221223860 134556658 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12726 11437 603 41 0 12685 0
vsize: 50904
[startup+530.028 s]
Raw data (loadavg): 1.07 0.99 0.83 2/57 24072
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 11858 0 0 0 52951 44 0 0 25 0 1 0 429385165 52473856 11512 4294967295 134512640 134672761 3221224560 3221223664 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12811 11512 603 41 0 12770 0
vsize: 51244
[startup+540.029 s]
Raw data (loadavg): 1.14 1.00 0.83 2/54 24084
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 11951 0 0 0 53951 45 0 0 25 0 1 0 429385165 52846592 11605 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12902 11605 603 41 0 12861 0
vsize: 51608
[startup+550.029 s]
Raw data (loadavg): 1.11 1.00 0.84 2/54 24084
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 14207 0 0 0 54947 49 0 0 25 0 1 0 429385165 68694016 13861 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16771 13861 603 41 0 16730 0
vsize: 67084
[startup+560.029 s]
Raw data (loadavg): 1.10 1.00 0.84 2/54 24084
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 14364 0 0 0 55946 50 0 0 25 0 1 0 429385165 69980160 14018 4294967295 134512640 134672761 3221224560 3221223732 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17085 14018 603 41 0 17044 0
vsize: 68340
[startup+570.029 s]
Raw data (loadavg): 1.08 1.00 0.84 2/54 24084
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 14431 0 0 0 56946 50 0 0 25 0 1 0 429385165 70238208 14085 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17148 14085 603 41 0 17107 0
vsize: 68592
[startup+580.029 s]
Raw data (loadavg): 1.07 1.00 0.84 2/54 24084
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 14526 0 0 0 57946 51 0 0 25 0 1 0 429385165 70598656 14180 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17236 14180 603 41 0 17195 0
vsize: 68944
[startup+590.03 s]
Raw data (loadavg): 1.06 1.00 0.84 2/54 24084
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 14585 0 0 0 58945 51 0 0 25 0 1 0 429385165 70868992 14239 4294967295 134512640 134672761 3221224560 3221223744 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17302 14239 603 41 0 17261 0
vsize: 69208
[startup+600.03 s]
Raw data (loadavg): 1.05 1.00 0.84 2/54 24086
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 18342 0 0 0 59937 60 0 0 25 0 1 0 429385165 81137664 17666 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19809 17666 603 41 0 19768 0
vsize: 79236
[startup+610.03 s]
Raw data (loadavg): 1.04 1.00 0.84 2/54 24086
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 18367 0 0 0 60937 60 0 0 25 0 1 0 429385165 81137664 17691 4294967295 134512640 134672761 3221224560 3221223744 134558930 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19809 17691 603 41 0 19768 0
vsize: 79236
[startup+620.03 s]
Raw data (loadavg): 1.03 1.00 0.84 2/54 24086
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 20667 0 0 0 61931 65 0 0 25 0 1 0 429385165 88776704 19991 4294967295 134512640 134672761 3221224560 3221223664 134560506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21674 19991 603 41 0 21633 0
vsize: 86696
[startup+630.031 s]
Raw data (loadavg): 1.03 1.00 0.84 2/54 24086
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 21693 0 0 0 62930 67 0 0 25 0 1 0 429385165 97095680 21017 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23705 21017 603 41 0 23664 0
vsize: 94820
[startup+640.03 s]
Raw data (loadavg): 1.02 1.00 0.84 2/54 24086
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 21787 0 0 0 63930 67 0 0 25 0 1 0 429385165 98242560 21111 4294967295 134512640 134672761 3221224560 3221223728 134560849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23985 21111 603 41 0 23944 0
vsize: 95940
[startup+650.031 s]
Raw data (loadavg): 1.02 1.00 0.85 2/54 24086
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 22528 0 0 0 64928 70 0 0 25 0 1 0 429385165 114270208 21852 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27898 21852 603 41 0 27857 0
vsize: 111592
[startup+660.03 s]
Raw data (loadavg): 1.02 1.00 0.85 2/54 24086
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 22528 0 0 0 65928 70 0 0 25 0 1 0 429385165 114270208 21852 4294967295 134512640 134672761 3221224560 3221223696 134560652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27898 21852 603 41 0 27857 0
vsize: 111592
[startup+670.03 s]
Raw data (loadavg): 1.01 1.00 0.85 2/54 24086
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 22528 0 0 0 66928 70 0 0 25 0 1 0 429385165 114270208 21852 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27898 21852 603 41 0 27857 0
vsize: 111592
[startup+680.03 s]
Raw data (loadavg): 1.01 1.00 0.85 2/54 24086
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 23679 0 0 0 67926 72 0 0 25 0 1 0 429385165 117547008 23003 4294967295 134512640 134672761 3221224560 3221223704 134560630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28698 23003 603 41 0 28657 0
vsize: 114792
[startup+690.03 s]
Raw data (loadavg): 1.01 1.00 0.85 2/54 24086
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 23723 0 0 0 68926 72 0 0 25 0 1 0 429385165 117678080 23047 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28730 23047 603 41 0 28689 0
vsize: 114920
[startup+700.03 s]
Raw data (loadavg): 1.01 1.00 0.85 2/54 24086
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 23756 0 0 0 69926 72 0 0 25 0 1 0 429385165 117809152 23080 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28762 23080 603 41 0 28721 0
vsize: 115048
[startup+710.031 s]
Raw data (loadavg): 1.00 1.00 0.85 2/54 24086
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 24865 0 0 0 70923 75 0 0 25 0 1 0 429385165 121053184 24189 4294967295 134512640 134672761 3221224560 3221223756 134556584 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29554 24189 603 41 0 29513 0
vsize: 118216
[startup+720.03 s]
Raw data (loadavg): 1.00 1.00 0.85 2/54 24086
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 24876 0 0 0 71923 75 0 0 25 0 1 0 429385165 121053184 24200 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29554 24200 603 41 0 29513 0
vsize: 118216
[startup+730.03 s]
Raw data (loadavg): 1.00 1.00 0.85 2/54 24086
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 24950 0 0 0 72924 75 0 0 25 0 1 0 429385165 121196544 24274 4294967295 134512640 134672761 3221224560 3221223684 134566031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29589 24274 603 41 0 29548 0
vsize: 118356
[startup+740.03 s]
Raw data (loadavg): 1.00 1.00 0.85 2/54 24086
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 24959 0 0 0 73924 75 0 0 25 0 1 0 429385165 121298944 24283 4294967295 134512640 134672761 3221224560 3221223728 134564746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29614 24283 603 41 0 29573 0
vsize: 118456
[startup+750.031 s]
Raw data (loadavg): 1.00 1.00 0.85 2/54 24086
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 26807 0 0 0 74920 79 0 0 25 0 1 0 429385165 124809216 25472 4294967295 134512640 134672761 3221224560 3221223712 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30471 25472 603 41 0 30430 0
vsize: 121884
[startup+760.03 s]
Raw data (loadavg): 1.00 1.00 0.86 2/54 24086
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 26809 0 0 0 75920 79 0 0 25 0 1 0 429385165 124809216 25474 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30471 25474 603 41 0 30430 0
vsize: 121884
[startup+770.031 s]
Raw data (loadavg): 1.00 1.00 0.86 2/54 24086
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 26953 0 0 0 76920 80 0 0 25 0 1 0 429385165 124928000 25618 4294967295 134512640 134672761 3221224560 3221223768 134561960 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30500 25618 603 41 0 30459 0
vsize: 122000
[startup+780.031 s]
Raw data (loadavg): 1.00 1.00 0.86 2/54 24086
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 27169 0 0 0 77919 80 0 0 25 0 1 0 429385165 124928000 25834 4294967295 134512640 134672761 3221224560 3221223684 134566068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30500 25834 603 41 0 30459 0
vsize: 122000
[startup+783.483 s]
Raw data (loadavg): 1.00 1.00 0.86 1/53 24086
Raw data (stat): 24031 (minisat+) R 24030 10720 10719 0 -1 0 27169 0 0 0 77919 80 0 0 25 0 1 0 429385165 124928000 25834 4294967295 134512640 134672761 3221224560 3221223684 134566068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30500 25834 603 41 0 30459 0
vsize: 0

Child status: 30
Real time (s): 783.483
CPU time (s): 783.453
CPU user time (s): 782.595
CPU system time (s): 0.857869
CPU usage (%): 99.9962
Max. virtual memory (Kb): 122000
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	258411
#### END VERIFIER DATA ####