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 31769

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc23 THE 2005-05-27 06:07:18 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=23143 boxname=wulflinc23 idbench=389 idsolver=16 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  dd62132555621025f45a5a6099c90742  /oldhome/oroussel/tmp/wulflinc23/normalized-p0282.opb
REAL COMMAND:  minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc23/normalized-p0282.opb
IDLAUNCH: 23143
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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	: 3
cpu MHz		: 451.037
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:        843584 kB
Buffers:         32820 kB
Cached:         136736 kB
SwapCached:        648 kB
Active:          16388 kB
Inactive:       155472 kB
HighTotal:      131008 kB
HighFree:        86184 kB
LowTotal:       903652 kB
LowFree:        757400 kB
SwapTotal:     2097136 kB
SwapFree:      2095880 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5616 kB
Slab:            13532 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-27 06:24:43 (client local time) WITH STATUS 30 IN 1044.77 SECONDS
stats: 23143 0 1044.77 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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   0]---> Sorter-cost:45913     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  1348067 |  188524   36552  1302730    35.6 | 16.377 % |
c |     76620 |  564905  1346530 |  207376   36642  1303393    35.6 | 13.398 % |
c |     76770 |  564366  1345291 |  228114   36791  1305213    35.5 | 13.471 % |
c |     76995 |  396117   954804 |  250925   22642   990524    43.7 | 36.828 % |
c ==============================================================================
c [1mFound solution: 264114[0m
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 |     77279 |  470026  1127458 |  156675   22915  1025296    44.7 | 36.828 % |
c |     77379 |  470026  1127458 |  172342   23015  1025849    44.6 | 33.220 % |
c |     77529 |  470026  1127458 |  189576   23165  1026832    44.3 | 33.220 % |
c |     77754 |  469945  1127270 |  208534   23389  1032164    44.1 | 33.231 % |
c ==============================================================================
c [1mFound solution: 264023[0m
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 |     77810 |  470486  1128756 |  156828   23445  1035082    44.1 | 33.231 % |
c |     77911 |  470276  1128272 |  172510   23482  1036704    44.1 | 33.220 % |
c |     78062 |  470276  1128272 |  189761   23633  1054297    44.6 | 33.220 % |
c |     78287 |  470154  1127990 |  208738   23838  1055475    44.3 | 33.235 % |
c |     78624 |  470003  1127640 |  229611   24159  1071459    44.4 | 33.255 % |
c ==============================================================================
c [1mFound solution: 264022[0m
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 |     78804 |  470017  1127807 |  156672   24339  1082842    44.5 | 33.255 % |
c |     78904 |  470017  1127807 |  172339   24439  1083600    44.3 | 33.254 % |
c ==============================================================================
c [1mFound solution: 260781[0m
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 |     78990 |  470033  1127900 |  156677   24525  1091731    44.5 | 33.254 % |
c |     79090 |  461755  1108449 |  172344   22876   799733    35.0 | 34.157 % |
c ==============================================================================
c [1mFound solution: 260774[0m
c ---[   0]---> Sorter-cost:19070     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 |     79146 |  512233  1226431 |  170744   22932   804589    35.1 | 34.157 % |
c ==============================================================================
c [1mFound solution: 260772[0m
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 |     79173 |  512251  1226692 |  170750   22959   805740    35.1 | 34.157 % |
c ==============================================================================
c [1mFound solution: 260768[0m
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 |     79267 |  512552  1227427 |  170850   23053   809385    35.1 | 34.157 % |
c |     79367 |  512552  1227427 |  187935   23153   819982    35.4 | 31.995 % |
c |     79517 |  512388  1227059 |  206728   23296   824919    35.4 | 32.014 % |
c ==============================================================================
c [1mFound solution: 260766[0m
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 |     79579 |  512349  1227038 |  170783   23357   827056    35.4 | 32.014 % |
c ==============================================================================
c [1mFound solution: 260762[0m
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 |     79612 |  512362  1227069 |  170787   23390   830054    35.5 | 32.014 % |
c |     79712 |  512362  1227069 |  187865   23490   830611    35.4 | 32.017 % |
c |     79862 |  512362  1227069 |  206652   23640   832235    35.2 | 32.017 % |
c |     80088 |  512239  1226795 |  227317   23861   836615    35.1 | 32.029 % |
c ==============================================================================
c [1mFound solution: 260761[0m
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 |     80418 |  511946  1226126 |  170648   24181   851184    35.2 | 32.029 % |
c ==============================================================================
c [1mFound solution: 260758[0m
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 |     80494 |  511943  1226119 |  170647   24254   852510    35.1 | 32.029 % |
c ==============================================================================
c [1mFound solution: 260756[0m
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 |     80505 |  511955  1226147 |  170651   24265   853689    35.2 | 32.029 % |
c |     80605 |  511955  1226147 |  187716   24365   856707    35.2 | 32.066 % |
c ==============================================================================
c [1mFound solution: 260685[0m
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 |     80708 |  512320  1227043 |  170773   24467   860888    35.2 | 32.066 % |
c ==============================================================================
c [1mFound solution: 260273[0m
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 |     80743 |  512405  1227301 |  170801   24502   861682    35.2 | 32.066 % |
c ==============================================================================
c [1mFound solution: 259622[0m
c ---[   0]---> Sorter-cost:    5     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 |     80783 |  512411  1227332 |  170803   24542   862948    35.2 | 32.066 % |
c |     80884 |  512232  1226922 |  187883   24640   863529    35.0 | 32.058 % |
c |     81036 |  512042  1226491 |  206671   24765   868371    35.1 | 32.078 % |
c |     81261 |  511791  1225927 |  227338   24987   869773    34.8 | 32.103 % |
c ==============================================================================
c [1mFound solution: 259584[0m
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 |     81376 |  512044  1226545 |  170681   25102   874073    34.8 | 32.103 % |
c |     81476 |  512044  1226545 |  187749   25202   875104    34.7 | 32.088 % |
c ==============================================================================
c [1mFound solution: 259583[0m
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 |     81564 |  512053  1226621 |  170684   25290   879117    34.8 | 32.088 % |
c ==============================================================================
c [1mFound solution: 259562[0m
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 |     81570 |  512060  1226638 |  170686   25296   879545    34.8 | 32.088 % |
c ==============================================================================
c [1mFound solution: 259558[0m
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 |     81615 |  512067  1226655 |  170689   25341   881143    34.8 | 32.088 % |
c ==============================================================================
c [1mFound solution: 259553[0m
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 |     81698 |  512075  1226676 |  170691   25424   886313    34.9 | 32.088 % |
c |     81799 |  512050  1226620 |  187760   25524   887808    34.8 | 32.090 % |
c |     81949 |  512050  1226620 |  206536   25674   888983    34.6 | 32.090 % |
c |     82175 |  511897  1226258 |  227189   25867   891663    34.5 | 32.111 % |
c |     82513 |  511889  1226242 |  249908   26204   907318    34.6 | 32.112 % |
c ==============================================================================
c [1mFound solution: 259410[0m
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 |     82671 |  511301  1224946 |  170433   26336   915094    34.7 | 32.112 % |
c |     82771 |  511066  1224410 |  187476   26431   915936    34.7 | 32.205 % |
c ==============================================================================
c [1mFound solution: 259408[0m
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 |     82915 |  511074  1224431 |  170358   26575   925853    34.8 | 32.205 % |
c |     83015 |  511009  1224283 |  187393   26673   929454    34.8 | 32.213 % |
c ==============================================================================
c [1mFound solution: 258978[0m
c ---[   0]---> Sorter-cost:    4     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 |     83136 |  511054  1224407 |  170351   26793   937813    35.0 | 32.213 % |
c |     83236 |  511054  1224407 |  187386   26893   940060    35.0 | 32.213 % |
c ==============================================================================
c [1mFound solution: 258976[0m
c ---[   0]---> Sorter-cost:    4     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 |     83270 |  510989  1224281 |  170329   26924   940719    34.9 | 32.213 % |
c ==============================================================================
c [1mFound solution: 258974[0m
c ---[   0]---> Sorter-cost:    3     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 |     83289 |  510993  1224291 |  170331   26943   940908    34.9 | 32.213 % |
c ==============================================================================
c [1mFound solution: 258968[0m
c ---[   0]---> Sorter-cost:    5     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 |     83301 |  510997  1224303 |  170332   26955   941533    34.9 | 32.213 % |
c ==============================================================================
c [1mFound solution: 258832[0m
c ---[   0]---> Sorter-cost:    5     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 |     83321 |  511004  1224322 |  170334   26975   941709    34.9 | 32.213 % |
c ==============================================================================
c [1mFound solution: 258826[0m
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 |     83360 |  511013  1224345 |  170337   27014   943127    34.9 | 32.213 % |
c |     83461 |  511013  1224345 |  187370   27115   944941    34.8 | 32.220 % |
c ==============================================================================
c [1mFound solution: 258762[0m
c ---[   0]---> Sorter-cost:    3     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 |     83485 |  511017  1224355 |  170339   27139   945747    34.8 | 32.220 % |
c ==============================================================================
c [1mFound solution: 258760[0m
c ---[   0]---> Sorter-cost:    3     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 |     83493 |  511021  1224365 |  170340   27147   945844    34.8 | 32.220 % |
c |     83593 |  511021  1224365 |  187374   27247   949614    34.9 | 32.220 % |
c |     83743 |  510931  1224163 |  206111   27391   950474    34.7 | 32.229 % |
c |     83968 |  505930  1212504 |  226722   27452   950754    34.6 | 32.825 % |
c |     84305 |  491968  1180080 |  249394   26485   922036    34.8 | 34.379 % |
c |     84812 |  491968  1180080 |  274334   26992   950440    35.2 | 34.379 % |
c ==============================================================================
c [1mFound solution: 258759[0m
c ---[   0]---> Sorter-cost:19609     Base: 2 2 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     84866 |  539229  1290188 |  179743   25930   814365    31.4 | 34.379 % |
c ==============================================================================
c [1mFound solution: 258750[0m
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     84897 |  539854  1291878 |  179951   25961   815942    31.4 | 34.379 % |
c ==============================================================================
c [1mFound solution: 258749[0m
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     84903 |  539866  1292018 |  179955   25967   815990    31.4 | 34.379 % |
c |     85008 |  539866  1292018 |  197950   26072   822063    31.5 | 32.760 % |
c |     85158 |  539740  1291733 |  217745   26202   825894    31.5 | 32.773 % |
c |     85383 |  539740  1291733 |  239520   26427   848255    32.1 | 32.773 % |
c |     85720 |  539700  1291645 |  263472   26763   863624    32.3 | 32.777 % |
c ==============================================================================
c [1mFound solution: 258736[0m
c ---[   0]---> Sorter-cost:18263     Base: 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     85985 |  481761  1153772 |  160587   21542   707742    32.9 | 32.777 % |
c ==============================================================================
c [1mFound solution: 258682[0m
c ---[   0]---> Sorter-cost:    8     Base: 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86022 |  481911  1154173 |  160637   21579   709690    32.9 | 32.777 % |
c |     86122 |  481911  1154173 |  176700   21679   711060    32.8 | 42.330 % |
c ==============================================================================
c [1mFound solution: 258679[0m
c ---[   0]---> Sorter-cost:15295     Base: 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86223 |  518453  1239753 |  172817   21472   701735    32.7 | 42.330 % |
c ==============================================================================
c [1mFound solution: 258670[0m
c ---[   0]---> Sorter-cost:    9     Base: 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86254 |  518863  1240940 |  172954   21503   703248    32.7 | 42.330 % |
c |     86354 |  518459  1240018 |  190249   21597   703691    32.6 | 40.835 % |
c ==============================================================================
c [1mFound solution: 258645[0m
c ---[   0]---> Sorter-cost:12382     Base: 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86427 |  417865  1003848 |  139288   15334   482817    31.5 | 40.835 % |
c ==============================================================================
c [1mFound solution: 258630[0m
c ---[   0]---> Sorter-cost:    9     Base: 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86500 |  418194  1004772 |  139398   15406   484544    31.5 | 40.835 % |
c |     86605 |  418194  1004772 |  153337   15511   485500    31.3 | 52.616 % |
c ==============================================================================
c [1mFound solution: 258610[0m
c ---[   0]---> Sorter-cost: 8905     Base: 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86698 |  406815   978188 |  135605   14431   446719    31.0 | 52.616 % |
c ==============================================================================
c [1mFound solution: 258596[0m
c ---[   0]---> Sorter-cost:    7     Base: 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86735 |  407268   979352 |  135756   14468   448449    31.0 | 52.616 % |
c ==============================================================================
c [1mFound solution: 258595[0m
c ---[   0]---> Sorter-cost:    7     Base: 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86754 |  407234   979384 |  135744   14485   448612    31.0 | 52.616 % |
c ==============================================================================
c [1mFound solution: 258590[0m
c ---[   0]---> Sorter-cost:    7     Base: 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86763 |  407424   979849 |  135808   14494   448830    31.0 | 52.616 % |
c ==============================================================================
c [1mFound solution: 258589[0m
c ---[   0]---> Sorter-cost:    7     Base: 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86780 |  407435   979916 |  135811   14511   449397    31.0 | 52.616 % |
c ==============================================================================
c [1mFound solution: 258578[0m
c ---[   0]---> Sorter-cost:    6     Base: 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86808 |  407412   979867 |  135804   14538   450011    31.0 | 52.616 % |
c ==============================================================================
c [1mFound solution: 258577[0m
c ---[   0]---> Sorter-cost:    6     Base: 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86818 |  407422   979891 |  135807   14548   450245    30.9 | 52.616 % |
c ==============================================================================
c [1mFound solution: 258575[0m
c ---[   0]---> Sorter-cost:    7     Base: 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86829 |  407432   979915 |  135810   14559   450544    30.9 | 52.616 % |
c ==============================================================================
c [1mFound solution: 258573[0m
c ---[   0]---> Sorter-cost:    7     Base: 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86833 |  407442   979939 |  135814   14563   450664    30.9 | 52.616 % |
c ==============================================================================
c [1mFound solution: 258565[0m
c ---[   0]---> Sorter-cost:    7     Base: 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86845 |  407452   979962 |  135817   14575   450996    30.9 | 52.616 % |
c |     86945 |  385665   928702 |  149398   13718   401050    29.2 | 56.788 % |
c ==============================================================================
c [1mFound solution: 258542[0m
c ---[   0]---> Sorter-cost: 6480     Base: 2 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     87047 |  338645   817990 |  112881   11144   286473    25.7 | 56.788 % |
c |     87147 |  338645   817990 |  124169   11244   287569    25.6 | 61.959 % |
c ==============================================================================
c [1mFound solution: 258537[0m
c ---[   0]---> Sorter-cost: 5230     Base: 2 2 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     87200 |  291250   706882 |   97083    9717   256481    26.4 | 61.959 % |
c |     87300 |  288838   701270 |  106791    9794   257623    26.3 | 67.150 % |
c |     87450 |  288838   701270 |  117470    9944   260674    26.2 | 67.150 % |
c ==============================================================================
c [1mFound solution: 258534[0m
c ---[   0]---> Sorter-cost: 4972     Base: 2 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     87531 |  293251   711463 |   97750    9742   255777    26.3 | 67.150 % |
c ==============================================================================
c [1mFound solution: 258533[0m
c ---[   0]---> Sorter-cost:    5     Base: 2 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     87597 |  293632   712418 |   97877    9808   257676    26.3 | 67.150 % |
c ==============================================================================
c [1mFound solution: 258532[0m
c ---[   0]---> Sorter-cost:    5     Base: 2 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     87655 |  293759   712783 |   97919    9866   258255    26.2 | 67.150 % |
c ==============================================================================
c [1mFound solution: 258531[0m
c ---[   0]---> Sorter-cost:    6     Base: 2 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     87685 |  293768   712843 |   97922    9896   258737    26.1 | 67.150 % |
c ==============================================================================
c [1mFound solution: 258527[0m
c ---[   0]---> Sorter-cost: 3473     Base: 2 2 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     87703 |  293019   711164 |   97673    9711   250466    25.8 | 67.150 % |
c |     87804 |  293019   711164 |  107440    9812   252163    25.7 | 67.294 % |
c |     87954 |  293010   711145 |  118184    9961   254453    25.5 | 67.295 % |
c ==============================================================================
c [1mFound solution: 258521[0m
c ---[   0]---> Sorter-cost:    4     Base: 2 2 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88027 |  293351   711983 |   97783   10034   255728    25.5 | 67.295 % |
c ==============================================================================
c [1mFound solution: 258520[0m
c ---[   0]---> Sorter-cost:    5     Base: 2 2 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88094 |  293415   712216 |   97805   10101   258431    25.6 | 67.295 % |
c |     88194 |  293415   712216 |  107585   10201   261099    25.6 | 67.253 % |
c ==============================================================================
c [1mFound solution: 258510[0m
c ---[   0]---> Sorter-cost: 3661     Base: 2 2 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88201 |  278180   676536 |   92726    9549   238683    25.0 | 67.253 % |
c ==============================================================================
c [1mFound solution: 258509[0m
c ---[   0]---> Sorter-cost:    6     Base: 2 2 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88203 |  278337   676946 |   92779    9551   238869    25.0 | 67.253 % |
c ==============================================================================
c [1mFound solution: 258507[0m
c ---[   0]---> Sorter-cost:    6     Base: 2 2 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88204 |  278347   677001 |   92782    9552   238906    25.0 | 67.253 % |
c ==============================================================================
c [1mFound solution: 258506[0m
c ---[   0]---> Sorter-cost:    2     Base: 2 2 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88242 |  278350   677008 |   92783    9590   242570    25.3 | 67.253 % |
c ==============================================================================
c [1mFound solution: 258470[0m
c ---[   0]---> Sorter-cost: 1870     Base: 2 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88265 |  210781   518356 |   70260    7424   171998    23.2 | 67.253 % |
c |     88365 |  210781   518356 |   77286    7524   175727    23.4 | 75.287 % |
c ==============================================================================
c [1mFound solution: 258459[0m
c ---[   0]---> Sorter-cost: 2017     Base: 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88468 |  196727   485278 |   65575    7031   169660    24.1 | 75.287 % |
c ==============================================================================
c [1mFound solution: 258458[0m
c ---[   0]---> Sorter-cost:    3     Base: 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88489 |  196838   485559 |   65612    7052   169881    24.1 | 75.287 % |
c ==============================================================================
c [1mFound solution: 258457[0m
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 |     88490 |  196846   485596 |   65615    7053   169923    24.1 | 75.287 % |
c ==============================================================================
c [1mFound solution: 258456[0m
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 |     88490 |  196852   485610 |   65617    7053   169923    24.1 | 75.287 % |
c ==============================================================================
c [1mFound solution: 258455[0m
c ---[   0]---> Sorter-cost: 1170     Base: 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88497 |  192577   475573 |   64192    6826   164365    24.1 | 75.287 % |
c ==============================================================================
c [1mFound solution: 258454[0m
c ---[   0]---> Sorter-cost:    1     Base: 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88503 |  192582   475586 |   64194    6832   164405    24.1 | 75.287 % |
c ==============================================================================
c [1mFound solution: 258450[0m
c ---[   0]---> Sorter-cost: 1190     Base: 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88511 |  177464   440064 |   59154    6185   151014    24.4 | 75.287 % |
c ==============================================================================
c [1mFound solution: 258447[0m
c ---[   0]---> Sorter-cost:  531     Base: 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88538 |  171817   426581 |   57272    5964   144946    24.3 | 75.287 % |
c ==============================================================================
c [1mFound solution: 258446[0m
c ---[   0]---> Sorter-cost:    3     Base: 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88541 |  171823   426594 |   57274    5967   144954    24.3 | 75.287 % |
c ==============================================================================
c [1mFound solution: 258445[0m
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 |     88545 |  165895   412676 |   55298    5640   139690    24.8 | 75.287 % |
c ==============================================================================
c [1mFound solution: 258444[0m
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 |     88545 |  161321   401922 |   53773    5408   134169    24.8 | 75.287 % |
c ==============================================================================
c [1mFound solution: 258443[0m
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 |     88545 |  161376   402061 |   53792    5408   134169    24.8 | 75.287 % |
c ==============================================================================
c [1mFound solution: 258442[0m
c ---[   0]---> Sorter-cost:    2     Base: 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88545 |  161379   402068 |   53793    5408   134169    24.8 | 75.287 % |
c ==============================================================================
c [1mFound solution: 258439[0m
c ---[   0]---> Sorter-cost:  969     Base: 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88552 |  151336   378488 |   50445    5011   124603    24.9 | 75.287 % |
c ==============================================================================
c [1mFound solution: 258438[0m
c ---[   0]---> Sorter-cost:  885     Base: 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88556 |  147009   368334 |   49003    4855   120234    24.8 | 75.287 % |
c ==============================================================================
c [1mFound solution: 258437[0m
c ---[   0]---> Sorter-cost:    1     Base: 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88556 |  147014   368346 |   49004    4855   120234    24.8 | 75.287 % |
c ==============================================================================
c [1mFound solution: 258436[0m
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 |     88556 |  147085   368521 |   49028    4855   120234    24.8 | 75.287 % |
c ==============================================================================
c [1mFound solution: 258435[0m
c ---[   0]---> Sorter-cost:  235     Base: 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88556 |  144160   361636 |   48053    4648   111929    24.1 | 75.287 % |
c ==============================================================================
c [1mFound solution: 258434[0m
c ---[   0]---> Sorter-cost:  790     Base: 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88556 |  137153   345224 |   45717    4380   105510    24.1 | 75.287 % |
c ==============================================================================
c [1mFound solution: 258433[0m
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 |     88561 |  137216   345402 |   45738    4385   105535    24.1 | 75.287 % |
c ==============================================================================
c [1mFound solution: 258425[0m
c ---[   0]---> Sorter-cost:  286     Base: 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88580 |   77446   203936 |   25815    1980    46738    23.6 | 75.287 % |
c ==============================================================================
c [1mFound solution: 258424[0m
c ---[   0]---> Sorter-cost:    1     Base: 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88604 |   77450   203946 |   25816    2004    46952    23.4 | 75.287 % |
c ==============================================================================
c [1mFound solution: 258422[0m
c ---[   0]---> Sorter-cost:  193     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88607 |   72700   192468 |   24233    1724    38884    22.6 | 75.287 % |
c ==============================================================================
c [1mFound solution: 258421[0m
c ---[   0]---> Sorter-cost:  182     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88609 |   64404   172893 |   21468    1435    31038    21.6 | 75.287 % |
c ==============================================================================
c [1mFound solution: 258416[0m
c ---[   0]---> Sorter-cost:   27     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88611 |   40198   114545 |   13399     427     7313    17.1 | 75.287 % |
c ==============================================================================
c [1mFound solution: 258415[0m
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88612 |   33046    96520 |   11015     207     3205    15.5 | 75.287 % |
c ==============================================================================
c [1mFound solution: 258414[0m
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88613 |   29199    86523 |    9733     115     2272    19.8 | 75.287 % |
c ==============================================================================
c [1mFound solution: 258413[0m
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88613 |   28079    83601 |    9359      84     1520    18.1 | 75.287 % |
c ==============================================================================
c [1mFound solution: 258412[0m
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88613 |   27127    80516 |    9042      68     1241    18.2 | 75.287 % |
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              : 339
c conflicts             : 88613          (85 /sec)
c decisions             : 1501198        (1438 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 1043.67 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.91 0.95 0.90 2/54 27811
Raw data (stat): 27811 (runsolver) R 27810 5562 5561 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 853878059 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.92 0.95 0.90 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0016 s]
Raw data (loadavg): 0.93 0.95 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0015 s]
Raw data (loadavg): 0.94 0.95 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0015 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0174 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0181 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0185 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0183 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.019 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.018 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.02 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.02 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.043 s]
Raw data (loadavg): 0.99 0.97 0.91 3/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1044.64 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 27815
Raw data (stat): 27811 (minisat+_script) S 27810 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853878059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 30
Real time (s): 1044.64
CPU time (s): 1044.77
CPU user time (s): 1043.84
CPU system time (s): 0.928858
CPU usage (%): 100.013
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	258411
#### END VERIFIER DATA ####