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 6996

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc21 THE 2005-04-14 20:51:23 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=5057 boxname=wulflinc21 idbench=389 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  dd62132555621025f45a5a6099c90742  /oldhome/oroussel/tmp/wulflinc21/normalized-p0282.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc21/normalized-p0282.opb /oldhome/oroussel/tmp/wulflinc21/normalized-p0282.opb
IDLAUNCH: 5057
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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.161
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:        861768 kB
Buffers:         32016 kB
Cached:         120644 kB
SwapCached:          0 kB
Active:          51572 kB
Inactive:       104028 kB
HighTotal:      131008 kB
HighFree:         6972 kB
LowTotal:       903652 kB
LowFree:        854796 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6932 kB
Slab:            11680 kB
Committed_AS:    63796 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 21:11:09 (client local time) WITH STATUS 30 IN 1185.54 SECONDS
stats: 5057 6 1185.54 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]---> Sorter-cost: 1109     Base: 2 5 3 3
c ---[  41]---> Sorter-cost:  898     Base: 2 5 3 2
c ---[  40]---> Sorter-cost: 1118     Base: 2 5 5
c ---[  38]---> Sorter-cost: 1010     Base: 2 5 5
c ---[  37]---> Sorter-cost:  909     Base: 2 5 5
c ---[  36]---> Sorter-cost:  998     Base: 2 5 3 2
c ---[  35]---> Sorter-cost:  852     Base: 2 5 3 3
c ---[  34]---> Sorter-cost:  843     Base: 5 2 3 3
c ---[  33]---> Sorter-cost:  713     Base: 5 2 3 3
c ---[  32]---> Sorter-cost:  948     Base: 2 5 3 3
c ---[  31]---> Sorter-cost:  843     Base: 2 5 3 3
c ---[  30]---> Sorter-cost:  911     Base: 2 5 5
c ---[  29]---> Sorter-cost:  935     Base: 2 5 3 2
c ---[  28]---> Sorter-cost:  998     Base: 2 5 3
c ---[  27]---> Sorter-cost:  763     Base: 5 2 3 3
c ---[  26]---> Sorter-cost:  910     Base: 2 5 5
c ---[  25]---> Sorter-cost:  908     Base: 2 5 5
c ---[  24]---> Sorter-cost:  714     Base: 5 2 3 3
c ---[  23]---> Sorter-cost:  909     Base: 2 5 5
c ---[  22]---> Sorter-cost:  911     Base: 2 5 5
c ---[  21]---> Sorter-cost: 1008     Base: 2 5 3
c ---[  20]---> Sorter-cost:  898     Base: 2 5 3 3
c ---[  19]---> Sorter-cost:  841     Base: 2 5 3 3
c ---[  18]---> Sorter-cost:  761     Base: 2 5 3 3
c ---[  17]---> Sorter-cost:  714     Base: 5 2 3 3
c ---[  16]---> Sorter-cost: 1071     Base: 2 5 3 3
c ---[  15]---> Sorter-cost:  949     Base: 2 5 3 3
c ---[  14]---> BDD-cost:   26
c ---[  13]---> Sorter-cost: 1108     Base: 2 5 3 3
c ---[  11]---> Sorter-cost: 1081     Base: 2 5 3 3
c ---[  10]---> Sorter-cost:  999     Base: 2 5 3 2
c ---[   9]---> Sorter-cost:  995     Base: 2 5 3 3
c ---[   8]---> Sorter-cost:  982     Base: 2 5 3 2
c ---[   7]---> Sorter-cost:  996     Base: 2 5 3 3
c ---[   5]---> BDD-cost:   56
c ---[   4]---> BDD-cost:   56
c ---[   3]---> BDD-cost:   56
c ---[   2]---> BDD-cost:   12
c ---[   1]---> Sorter-cost:  719     Base: 2 5 3
c ---[   0]---> Sorter-cost:  657     Base: 2 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   78014   183823 |   26004       0        0     nan |  0.000 % |
c |       100 |   77796   183335 |   28604      93      583     6.3 |  0.386 % |
c ==============================================================================
c [1mFound solution: 595390[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:77308     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 |       239 |  299319   701536 |   99773     228     1953     8.6 |  0.386 % |
c |       340 |  299245   701370 |  109750     326     3013     9.2 |  0.172 % |
c |       491 |  299068   700972 |  120725     469     5888    12.6 |  0.210 % |
c |       716 |  298929   700661 |  132797     690     8295    12.0 |  0.245 % |
c |      1053 |  298771   700309 |  146077    1023    11039    10.8 |  0.286 % |
c |      1560 |  298705   700161 |  160685    1526    20833    13.7 |  0.303 % |
c |      2321 |  298682   700110 |  176753    2286    27194    11.9 |  0.309 % |
c |      3460 |  298621   699973 |  194429    3423   138519    40.5 |  0.325 % |
c |      5168 |  298532   699773 |  213872    5128   173595    33.9 |  0.350 % |
c |      7730 |  298449   699586 |  235259    7688   225658    29.4 |  0.371 % |
c ==============================================================================
c [1mFound solution: 595300[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8706 |  299563   702557 |   99854    8662   243040    28.1 |  0.371 % |
c |      8806 |  299563   702557 |  109839    8762   243602    27.8 |  0.409 % |
c |      8958 |  299492   702396 |  120823    8912   245310    27.5 |  0.429 % |
c |      9184 |  299397   702181 |  132905    9135   250630    27.4 |  0.453 % |
c |      9522 |  299397   702181 |  146196    9473   264983    28.0 |  0.453 % |
c |     10028 |  299300   701962 |  160815    9978   272752    27.3 |  0.476 % |
c |     10788 |  299300   701962 |  176897   10738   281506    26.2 |  0.476 % |
c |     11928 |  299300   701962 |  194587   11878   310672    26.2 |  0.476 % |
c ==============================================================================
c [1mFound solution: 595224[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12347 |  301292   706904 |  100430   12295   324382    26.4 |  0.476 % |
c |     12448 |  301237   706779 |  110473   12395   324967    26.2 |  0.533 % |
c |     12598 |  301237   706779 |  121520   12545   331058    26.4 |  0.533 % |
c |     12824 |  301237   706779 |  133672   12771   332704    26.1 |  0.533 % |
c |     13162 |  300840   705886 |  147039   13086   336341    25.7 |  0.633 % |
c |     13668 |  300762   705709 |  161743   13587   344422    25.3 |  0.654 % |
c |     14427 |  300641   705435 |  177917   14333   352964    24.6 |  0.688 % |
c ==============================================================================
c [1mFound solution: 476418[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15497 |  302267   709483 |  100755   15399   390971    25.4 |  0.688 % |
c |     15597 |  302267   709483 |  110830   15499   391559    25.3 |  0.731 % |
c |     15747 |  302267   709483 |  121913   15649   412607    26.4 |  0.731 % |
c |     15973 |  302267   709483 |  134104   15875   415432    26.2 |  0.731 % |
c |     16311 |  302117   709144 |  147515   16200   419367    25.9 |  0.771 % |
c |     16817 |  302012   708905 |  162266   16698   428763    25.7 |  0.802 % |
c |     17576 |  301963   708795 |  178493   17433   453001    26.0 |  0.815 % |
c ==============================================================================
c [1mFound solution: 462850[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   13     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17988 |  302327   709786 |  100775   17845   465436    26.1 |  0.815 % |
c |     18091 |  302327   709786 |  110852   17948   465973    26.0 |  0.816 % |
c |     18241 |  302327   709786 |  121937   18098   466795    25.8 |  0.816 % |
c |     18467 |  302292   709706 |  134131   18322   468075    25.5 |  0.825 % |
c ==============================================================================
c [1mFound solution: 417382[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   13     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18560 |  302986   711402 |  100995   18415   468816    25.5 |  0.825 % |
c |     18660 |  302986   711402 |  111094   18515   469832    25.4 |  0.827 % |
c |     18812 |  302986   711402 |  122203   18667   470717    25.2 |  0.827 % |
c |     19040 |  302986   711402 |  134424   18895   476407    25.2 |  0.827 % |
c |     19379 |  302986   711402 |  147866   19234   481027    25.0 |  0.827 % |
c |     19885 |  302986   711402 |  162653   19740   487341    24.7 |  0.827 % |
c |     20644 |  302986   711402 |  178918   20499   492585    24.0 |  0.827 % |
c |     21783 |  302955   711333 |  196810   21636   504456    23.3 |  0.835 % |
c ==============================================================================
c [1mFound solution: 417380[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   17     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 |     23462 |  303664   713068 |  101221   23314   647492    27.8 |  0.835 % |
c |     23564 |  303664   713068 |  111343   23416   648413    27.7 |  0.847 % |
c |     23714 |  303641   713017 |  122477   23565   649269    27.6 |  0.853 % |
c |     23939 |  303641   713017 |  134725   23790   650899    27.4 |  0.853 % |
c |     24276 |  303641   713017 |  148197   24127   653569    27.1 |  0.853 % |
c |     24784 |  303641   713017 |  163017   24635   666195    27.0 |  0.853 % |
c |     25543 |  303509   712717 |  179319   25391   679180    26.7 |  0.890 % |
c ==============================================================================
c [1mFound solution: 416457[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26510 |  303541   712793 |  101180   26358   816535    31.0 |  0.890 % |
c |     26610 |  303541   712793 |  111298   26458   819360    31.0 |  0.891 % |
c |     26760 |  303509   712722 |  122427   26607   830508    31.2 |  0.899 % |
c |     26988 |  303469   712633 |  134670   26834   836890    31.2 |  0.909 % |
c |     27325 |  303469   712633 |  148137   27171   843151    31.0 |  0.909 % |
c |     27832 |  303469   712633 |  162951   27678   848937    30.7 |  0.909 % |
c |     28592 |  303375   712420 |  179246   28432   889582    31.3 |  0.934 % |
c |     29731 |  303375   712420 |  197171   29571   927399    31.4 |  0.934 % |
c |     31439 |  303351   712366 |  216888   31276   977288    31.2 |  0.941 % |
c |     34001 |  303272   712185 |  238577   33830  1021101    30.2 |  0.963 % |
c |     37845 |  303152   711913 |  262434   37671  1560327    41.4 |  0.994 % |
c |     43611 |  302902   711349 |  288678   43433  1757539    40.5 |  1.055 % |
c ==============================================================================
c [1mFound solution: 397195[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43738 |  302952   711476 |  100984   43560  1763846    40.5 |  1.055 % |
c |     43838 |  302809   711153 |  111082   43656  1764772    40.4 |  1.092 % |
c |     43990 |  302809   711153 |  122190   43808  1766501    40.3 |  1.092 % |
c |     44216 |  302809   711153 |  134409   44034  1771830    40.2 |  1.092 % |
c |     44554 |  302809   711153 |  147850   44372  1813060    40.9 |  1.092 % |
c |     45060 |  302809   711153 |  162635   44878  1820273    40.6 |  1.092 % |
c |     45823 |  302809   711153 |  178899   45641  1846169    40.4 |  1.092 % |
c |     46962 |  302793   711116 |  196789   46779  1903463    40.7 |  1.098 % |
c |     48670 |  302793   711116 |  216468   48487  1982421    40.9 |  1.098 % |
c |     51232 |  302747   711012 |  238114   51045  2092776    41.0 |  1.110 % |
c |     55078 |  302747   711012 |  261926   54891  2566086    46.7 |  1.110 % |
c ==============================================================================
c [1mFound solution: 383749[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     57425 |  302527   710524 |  100842   57218  2607329    45.6 |  1.110 % |
c |     57525 |  302527   710524 |  110926   57318  2608477    45.5 |  1.177 % |
c |     57676 |  302527   710524 |  122018   57469  2625456    45.7 |  1.177 % |
c ==============================================================================
c [1mFound solution: 383587[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     57830 |  302420   710287 |  100806   57621  2641669    45.8 |  1.177 % |
c |     57931 |  302371   710175 |  110886   57719  2642814    45.8 |  1.223 % |
c |     58081 |  302318   710054 |  121975   57868  2643413    45.7 |  1.237 % |
c |     58306 |  302318   710054 |  134172   58093  2667244    45.9 |  1.237 % |
c |     58643 |  302276   709959 |  147590   58429  2700351    46.2 |  1.247 % |
c ==============================================================================
c [1mFound solution: 366075[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     59051 |  302297   710010 |  100765   58837  2712746    46.1 |  1.247 % |
c |     59151 |  302297   710010 |  110841   58937  2713893    46.0 |  1.248 % |
c |     59301 |  302297   710010 |  121925   59087  2714820    45.9 |  1.248 % |
c |     59526 |  302297   710010 |  134118   59312  2721955    45.9 |  1.248 % |
c |     59863 |  302240   709880 |  147530   59648  2738832    45.9 |  1.263 % |
c |     60370 |  302236   709871 |  162283   60153  2749846    45.7 |  1.264 % |
c ==============================================================================
c [1mFound solution: 292219[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     60575 |  302269   709955 |  100756   60358  2758548    45.7 |  1.264 % |
c |     60675 |  302269   709955 |  110831   60458  2759091    45.6 |  1.265 % |
c |     60825 |  302269   709955 |  121914   60608  2763393    45.6 |  1.265 % |
c |     61050 |  302217   709836 |  134106   60831  2766363    45.5 |  1.281 % |
c |     61388 |  302217   709836 |  147516   61169  2783979    45.5 |  1.281 % |
c |     61894 |  302190   709775 |  162268   61674  2808939    45.5 |  1.289 % |
c |     62653 |  302190   709775 |  178495   62433  2836711    45.4 |  1.289 % |
c |     63793 |  302129   709638 |  196344   63571  2933906    46.2 |  1.304 % |
c |     65501 |  301938   709209 |  215979   65272  3153669    48.3 |  1.352 % |
c ==============================================================================
c [1mFound solution: 292218[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     66788 |  301907   709147 |  100635   66558  3260428    49.0 |  1.352 % |
c |     66888 |  301907   709147 |  110698   66658  3262500    48.9 |  1.366 % |
c |     67039 |  301907   709147 |  121768   66809  3267546    48.9 |  1.366 % |
c |     67264 |  301907   709147 |  133945   67034  3277890    48.9 |  1.366 % |
c |     67601 |  301810   708930 |  147339   67369  3298666    49.0 |  1.391 % |
c ==============================================================================
c [1mFound solution: 292216[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     68048 |  301824   708968 |  100608   67816  3315655    48.9 |  1.391 % |
c |     68148 |  301824   708968 |  110668   67916  3321709    48.9 |  1.392 % |
c |     68298 |  301824   708968 |  121735   68066  3328002    48.9 |  1.392 % |
c |     68525 |  301824   708968 |  133909   68293  3329714    48.8 |  1.392 % |
c |     68863 |  301824   708968 |  147300   68631  3338189    48.6 |  1.392 % |
c |     69369 |  301813   708944 |  162030   69136  3362757    48.6 |  1.395 % |
c |     70128 |  301813   708944 |  178233   69895  3456509    49.5 |  1.395 % |
c ==============================================================================
c [1mFound solution: 278200[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     70880 |  301839   709010 |  100613   70647  3486133    49.3 |  1.395 % |
c |     70980 |  301839   709010 |  110674   70747  3489114    49.3 |  1.396 % |
c |     71130 |  301839   709010 |  121741   70897  3537341    49.9 |  1.396 % |
c |     71356 |  301839   709010 |  133915   71123  3560547    50.1 |  1.396 % |
c |     71693 |  301724   708751 |  147307   71459  3582595    50.1 |  1.424 % |
c |     72200 |  301700   708697 |  162038   71955  3594122    49.9 |  1.430 % |
c ==============================================================================
c [1mFound solution: 278199[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     72328 |  301722   708753 |  100574   72083  3623644    50.3 |  1.430 % |
c |     72428 |  301722   708753 |  110631   72183  3624374    50.2 |  1.431 % |
c |     72578 |  301718   708744 |  121694   72332  3630145    50.2 |  1.432 % |
c |     72803 |  301718   708744 |  133863   72557  3639263    50.2 |  1.432 % |
c ==============================================================================
c [1mFound solution: 277639[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     72961 |  301733   708781 |  100577   72715  3657659    50.3 |  1.432 % |
c |     73064 |  301733   708781 |  110634   72818  3658556    50.2 |  1.433 % |
c |     73214 |  301733   708781 |  121698   72968  3659346    50.2 |  1.433 % |
c ==============================================================================
c [1mFound solution: 277638[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     73433 |  301753   708833 |  100584   73187  3669280    50.1 |  1.433 % |
c |     73533 |  301753   708833 |  110642   73287  3671534    50.1 |  1.434 % |
c |     73683 |  301753   708833 |  121706   73437  3684760    50.2 |  1.434 % |
c |     73908 |  301753   708833 |  133877   73662  3703695    50.3 |  1.434 % |
c |     74245 |  301753   708833 |  147265   73999  3713312    50.2 |  1.434 % |
c |     74751 |  301753   708833 |  161991   74505  3787024    50.8 |  1.434 % |
c ==============================================================================
c [1mFound solution: 264351[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   13     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     75043 |  301785   708911 |  100595   74797  3802325    50.8 |  1.434 % |
c |     75146 |  301785   708911 |  110654   74900  3808606    50.8 |  1.434 % |
c ==============================================================================
c [1mFound solution: 264350[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     75279 |  301817   708989 |  100605   75033  3825412    51.0 |  1.434 % |
c |     75382 |  301817   708989 |  110665   75136  3826482    50.9 |  1.435 % |
c ==============================================================================
c [1mFound solution: 264342[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     75438 |  301849   709067 |  100616   75192  3834675    51.0 |  1.435 % |
c |     75538 |  301849   709067 |  110677   75292  3840452    51.0 |  1.436 % |
c ==============================================================================
c [1mFound solution: 264341[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     75586 |  301881   709145 |  100627   75340  3847532    51.1 |  1.436 % |
c |     75686 |  301881   709145 |  110689   75440  3856877    51.1 |  1.437 % |
c ==============================================================================
c [1mFound solution: 264337[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   13     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     75797 |  301912   709220 |  100637   75551  3870281    51.2 |  1.437 % |
c |     75897 |  301912   709220 |  110700   75651  3871402    51.2 |  1.438 % |
c ==============================================================================
c [1mFound solution: 264335[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   13     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     75966 |  301943   709295 |  100647   75720  3881159    51.3 |  1.438 % |
c |     76066 |  301873   709138 |  110711   75816  3882182    51.2 |  1.458 % |
c |     76216 |  301873   709138 |  121782   75966  3886776    51.2 |  1.458 % |
c |     76441 |  301873   709138 |  133961   76191  3888505    51.0 |  1.458 % |
c |     76779 |  301873   709138 |  147357   76529  3914032    51.1 |  1.458 % |
c ==============================================================================
c [1mFound solution: 264334[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     76838 |  301890   709179 |  100630   76588  3920015    51.2 |  1.458 % |
c ==============================================================================
c [1mFound solution: 264333[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     76858 |  301921   709254 |  100640   76608  3923563    51.2 |  1.458 % |
c |     76959 |  301921   709254 |  110704   76709  3925409    51.2 |  1.459 % |
c |     77110 |  301842   709076 |  121774   76853  3926586    51.1 |  1.480 % |
c |     77335 |  301842   709076 |  133951   77078  3953188    51.3 |  1.480 % |
c |     77674 |  301842   709076 |  147347   77417  3958672    51.1 |  1.480 % |
c ==============================================================================
c [1mFound solution: 264332[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   13     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     77796 |  301873   709151 |  100624   77539  3984468    51.4 |  1.480 % |
c |     77897 |  301873   709151 |  110686   77640  3985497    51.3 |  1.481 % |
c |     78048 |  301873   709151 |  121755   77791  4004654    51.5 |  1.481 % |
c |     78274 |  301873   709151 |  133930   78017  4011655    51.4 |  1.481 % |
c ==============================================================================
c [1mFound solution: 264316[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   13     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     78512 |  301344   707940 |  100448   77966  4014859    51.5 |  1.481 % |
c |     78614 |  301344   707940 |  110492   78068  4019397    51.5 |  1.647 % |
c ==============================================================================
c [1mFound solution: 264312[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   13     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     78646 |  301375   708015 |  100458   78100  4021032    51.5 |  1.647 % |
c |     78746 |  301375   708015 |  110503   78200  4034306    51.6 |  1.648 % |
c |     78896 |  301375   708015 |  121554   78350  4048801    51.7 |  1.648 % |
c ==============================================================================
c [1mFound solution: 264275[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     79060 |  301405   708089 |  100468   78514  4071727    51.9 |  1.648 % |
c |     79161 |  301353   707971 |  110514   78614  4088533    52.0 |  1.662 % |
c |     79311 |  301353   707971 |  121566   78764  4097716    52.0 |  1.662 % |
c |     79537 |  301188   707592 |  133722   78963  4098724    51.9 |  1.712 % |
c ==============================================================================
c [1mFound solution: 264274[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     79862 |  301071   707324 |  100357   79202  4161175    52.5 |  1.712 % |
c ==============================================================================
c [1mFound solution: 264248[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   13     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     79902 |  301106   707409 |  100368   79242  4162635    52.5 |  1.712 % |
c |     80002 |  301106   707409 |  110404   79342  4180830    52.7 |  1.760 % |
c |     80160 |  301106   707409 |  121445   79500  4205751    52.9 |  1.760 % |
c |     80387 |  301106   707409 |  133589   79727  4236363    53.1 |  1.760 % |
c ==============================================================================
c [1mFound solution: 264247[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:48563     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 |     80693 |  431735  1013456 |  143911   79795  4233523    53.1 |  1.760 % |
c |     80794 |  431735  1013456 |  158302   79896  4240355    53.1 |  2.090 % |
c ==============================================================================
c [1mFound solution: 264245[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     80857 |  433356  1017693 |  144452   79959  4249359    53.1 |  2.090 % |
c |     80957 |  433356  1017693 |  158897   80059  4252689    53.1 |  2.086 % |
c |     81107 |  433065  1017040 |  174786   80202  4255248    53.1 |  2.138 % |
c |     81332 |  430901  1012134 |  192265   80073  4254503    53.1 |  2.565 % |
c |     81670 |  430901  1012134 |  211492   80411  4275292    53.2 |  2.566 % |
c |     82176 |  430901  1012134 |  232641   80917  4292061    53.0 |  2.565 % |
c ==============================================================================
c [1mFound solution: 264244[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     82415 |  431797  1014439 |  143932   80907  4218296    52.1 |  2.565 % |
c ==============================================================================
c [1mFound solution: 264226[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     82474 |  432784  1016848 |  144261   80966  4221932    52.1 |  2.565 % |
c |     82575 |  432784  1016848 |  158687   81067  4225539    52.1 |  2.630 % |
c |     82725 |  432784  1016848 |  174555   81217  4243898    52.3 |  2.630 % |
c |     82950 |  427550  1004980 |  192011   70880  2532027    35.7 |  3.548 % |
c |     83287 |  427550  1004980 |  211212   71217  2559027    35.9 |  3.547 % |
c |     83793 |  425695  1000730 |  232333   71136  2545847    35.8 |  3.919 % |
c ==============================================================================
c [1mFound solution: 264114[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:45481     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 |     83823 |  552122  1296719 |  184040   71166  2549438    35.8 |  3.919 % |
c |     83924 |  552122  1296719 |  202444   71267  2556475    35.9 |  3.435 % |
c ==============================================================================
c [1mFound solution: 263605[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   13     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     83975 |  554770  1303343 |  184923   71318  2561125    35.9 |  3.435 % |
c |     84075 |  554770  1303343 |  203415   71418  2568666    36.0 |  3.442 % |
c ==============================================================================
c [1mFound solution: 263602[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     84160 |  555185  1304562 |  185061   71503  2575528    36.0 |  3.442 % |
c ==============================================================================
c [1mFound solution: 263600[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     84176 |  555213  1304630 |  185071   71519  2576979    36.0 |  3.442 % |
c |     84276 |  555213  1304630 |  203578   71619  2582852    36.1 |  3.442 % |
c ==============================================================================
c [1mFound solution: 263595[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     84339 |  556323  1307342 |  185441   71682  2588882    36.1 |  3.442 % |
c ==============================================================================
c [1mFound solution: 263590[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     84352 |  556477  1307784 |  185492   71695  2590185    36.1 |  3.442 % |
c ==============================================================================
c [1mFound solution: 263589[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     84414 |  556509  1307862 |  185503   71757  2601859    36.3 |  3.442 % |
c |     84514 |  556465  1307763 |  204053   71856  2602692    36.2 |  3.444 % |
c |     84664 |  556393  1307602 |  224458   72004  2603434    36.2 |  3.454 % |
c |     84889 |  556308  1307412 |  246904   72226  2638490    36.5 |  3.465 % |
c |     85226 |  556308  1307412 |  271594   72563  2667207    36.8 |  3.466 % |
c |     85733 |  553920  1301991 |  298754   72665  2701359    37.2 |  3.832 % |
c |     86494 |  553920  1301991 |  328629   73426  2790417    38.0 |  3.832 % |
c ==============================================================================
c [1mFound solution: 263502[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     87548 |  553171  1300288 |  184390   74306  2856453    38.4 |  3.832 % |
c |     87648 |  553171  1300288 |  202829   74406  2857298    38.4 |  3.958 % |
c |     87798 |  552616  1299036 |  223111   74540  2876370    38.6 |  4.038 % |
c |     88023 |  552616  1299036 |  245423   74765  2884345    38.6 |  4.038 % |
c |     88362 |  551632  1296787 |  269965   74933  3058836    40.8 |  4.194 % |
c ==============================================================================
c [1mFound solution: 261820[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88409 |  550554  1294413 |  183518   74642  3046618    40.8 |  4.194 % |
c |     88509 |  550554  1294413 |  201869   74742  3051605    40.8 |  4.483 % |
c |     88660 |  550363  1293983 |  222056   74890  3056167    40.8 |  4.508 % |
c |     88885 |  550363  1293983 |  244262   75115  3071763    40.9 |  4.508 % |
c |     89222 |  550077  1293335 |  268688   75436  3074536    40.8 |  4.549 % |
c |     89729 |  550024  1293217 |  295557   75942  3079805    40.6 |  4.556 % |
c ==============================================================================
c [1mFound solution: 261793[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     90088 |  549775  1292705 |  183258   76240  3109351    40.8 |  4.556 % |
c |     90188 |  534695  1258027 |  201583   73541  2946212    40.1 |  6.982 % |
c |     90339 |  534085  1256631 |  221742   73690  2949002    40.0 |  7.080 % |
c |     90565 |  533216  1254625 |  243916   73723  2951498    40.0 |  7.223 % |
c |     90902 |  533216  1254625 |  268308   74060  2955430    39.9 |  7.223 % |
c |     91409 |  533118  1254404 |  295138   74563  2959146    39.7 |  7.237 % |
c |     92171 |  531787  1251325 |  324652   75186  3277092    43.6 |  7.451 % |
c ==============================================================================
c [1mFound solution: 259868[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:66437     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 |     92565 |  720777  1693357 |  240259   75580  3297260    43.6 |  7.451 % |
c |     92665 |  575919  1358081 |  264284   56569  2659050    47.0 | 23.504 % |
c |     92815 |  575919  1358081 |  290713   56719  2669668    47.1 | 23.504 % |
c |     93041 |  366694   871547 |  319784   29960  1636917    54.6 | 49.795 % |
c ==============================================================================
c [1mFound solution: 259866[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:28726     Base: 2 2 3 3 3 5 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     93105 |  441816  1047401 |  147272   29415  1588417    54.0 | 49.795 % |
c |     93205 |  441816  1047401 |  161999   29515  1590298    53.9 | 45.671 % |
c ==============================================================================
c [1mFound solution: 259865[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 3 3 3 5 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     93313 |  442231  1048579 |  147410   29620  1600549    54.0 | 45.671 % |
c |     93414 |  439897  1043213 |  162151   29562  1600031    54.1 | 45.916 % |
c |     93564 |  439758  1042900 |  178366   29711  1601036    53.9 | 45.929 % |
c |     93789 |  434597  1030978 |  196202   29502  1581498    53.6 | 51.435 % |
c |     94126 |  391700   930856 |  215822   25298  1190502    47.1 | 51.435 % |
c ==============================================================================
c [1mFound solution: 259842[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:22014     Base: 2 2 3 3 3 5 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     94238 |  452593  1073453 |  150864   25409  1195077    47.0 | 51.435 % |
c ==============================================================================
c [1mFound solution: 259734[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 3 3 3 5 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     94270 |  452654  1073624 |  150884   25441  1197355    47.1 | 51.435 % |
c |     94370 |  452525  1073324 |  165972   25539  1203804    47.1 | 48.031 % |
c |     94520 |  441534  1047746 |  182569   25116  1190113    47.4 | 49.211 % |
c ==============================================================================
c [1mFound solution: 259551[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:21898     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 |     94603 |  497658  1179148 |  165886   24911  1182405    47.5 | 49.211 % |
c |     94704 |  497634  1179092 |  182474   25010  1182976    47.3 | 46.679 % |
c |     94854 |  487508  1155597 |  200722   24598  1130016    45.9 | 47.649 % |
c |     95080 |  487029  1154500 |  220794   24810  1132165    45.6 | 47.693 % |
c |     95418 |  486862  1154115 |  242873   25145  1147628    45.6 | 47.716 % |
c ==============================================================================
c [1mFound solution: 259550[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:18378     Base: 2 2 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     95729 |  537506  1272773 |  179168   25456  1157324    45.5 | 47.716 % |
c |     95829 |  537506  1272773 |  197084   25556  1162965    45.5 | 45.369 % |
c ==============================================================================
c [1mFound solution: 259546[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     95931 |  538175  1274510 |  179391   25655  1165657    45.4 | 45.369 % |
c ==============================================================================
c [1mFound solution: 259031[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     95952 |  538745  1275948 |  179581   25676  1166109    45.4 | 45.369 % |
c |     96052 |  538745  1275948 |  197539   25776  1167457    45.3 | 45.336 % |
c ==============================================================================
c [1mFound solution: 259030[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:15772     Base: 2 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     96137 |  531278  1258733 |  177092   22964   739689    32.2 | 45.336 % |
c |     96237 |  531278  1258733 |  194801   23064   740225    32.1 | 48.267 % |
c |     96388 |  531245  1258658 |  214281   23213   741405    31.9 | 48.269 % |
c |     96613 |  531221  1258602 |  235709   23437   744310    31.8 | 48.272 % |
c |     96950 |  519723  1231913 |  259280   22962   696657    30.3 | 49.297 % |
c ==============================================================================
c [1mFound solution: 259029[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:14642     Base: 2 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     96989 |  559649  1325505 |  186549   22998   696849    30.3 | 49.297 % |
c ==============================================================================
c [1mFound solution: 259028[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     96990 |  560317  1327203 |  186772   22999   696853    30.3 | 49.297 % |
c ==============================================================================
c [1mFound solution: 259027[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     96990 |  560381  1327383 |  186793   22999   696853    30.3 | 49.297 % |
c ==============================================================================
c [1mFound solution: 259026[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     96990 |  560428  1327512 |  186809   22999   696853    30.3 | 49.297 % |
c ==============================================================================
c [1mFound solution: 259025[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     96991 |  560865  1328579 |  186955   23000   696857    30.3 | 49.297 % |
c ==============================================================================
c [1mFound solution: 259024[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     96993 |  561439  1330005 |  187146   23002   696886    30.3 | 49.297 % |
c ==============================================================================
c [1mFound solution: 259022[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     96998 |  561520  1330232 |  187173   23007   697323    30.3 | 49.297 % |
c ==============================================================================
c [1mFound solution: 259016[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     97013 |  561546  1330294 |  187182   23022   698977    30.4 | 49.297 % |
c ==============================================================================
c [1mFound solution: 258999[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     97015 |  561562  1330334 |  187187   23024   699074    30.4 | 49.297 % |
c ==============================================================================
c [1mFound solution: 258997[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     97023 |  561577  1330371 |  187192   23032   699256    30.4 | 49.297 % |
c ==============================================================================
c [1mFound solution: 258996[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     97023 |  561595  1330415 |  187198   23032   699256    30.4 | 49.297 % |
c ==============================================================================
c [1mFound solution: 258995[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     97023 |  561613  1330459 |  187204   23032   699256    30.4 | 49.297 % |
c ==============================================================================
c [1mFound solution: 258992[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     97047 |  561019  1329105 |  187006   23054   699992    30.4 | 49.297 % |
c |     97151 |  560899  1328835 |  205706   23156   701709    30.3 | 47.525 % |
c ==============================================================================
c [1mFound solution: 258934[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     97272 |  561163  1329495 |  187054   23276   711867    30.6 | 47.525 % |
c |     97373 |  560915  1328929 |  205759   23369   713564    30.5 | 47.538 % |
c |     97525 |  560915  1328929 |  226335   23521   722303    30.7 | 47.538 % |
c ==============================================================================
c [1mFound solution: 258932[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     97568 |  560965  1329071 |  186988   23564   724435    30.7 | 47.538 % |
c ==============================================================================
c [1mFound solution: 258928[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     97627 |  560941  1329017 |  186980   23622   725759    30.7 | 47.538 % |
c ==============================================================================
c [1mFound solution: 258924[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     97649 |  560952  1329044 |  186984   23644   726306    30.7 | 47.538 % |
c ==============================================================================
c [1mFound solution: 258916[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     97693 |  560969  1329085 |  186989   23688   730306    30.8 | 47.538 % |
c |     97797 |  560882  1328887 |  205687   23790   730892    30.7 | 47.546 % |
c ==============================================================================
c [1mFound solution: 258911[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     97869 |  560838  1328788 |  186946   23861   734286    30.8 | 47.546 % |
c ==============================================================================
c [1mFound solution: 258743[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:13037     Base: 2 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     97947 |  590230  1397785 |  196743   23747   736475    31.0 | 47.546 % |
c |     98047 |  590230  1397785 |  216417   23847   737160    30.9 | 46.653 % |
c |     98197 |  590226  1397776 |  238059   23996   738377    30.8 | 46.654 % |
c |     98422 |  590226  1397776 |  261864   24221   744570    30.7 | 46.654 % |
c ==============================================================================
c [1mFound solution: 258741[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     98468 |  590544  1398700 |  196848   24267   746132    30.7 | 46.654 % |
c ==============================================================================
c [1mFound solution: 258527[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     98515 |  590294  1398174 |  196764   24311   747697    30.8 | 46.654 % |
c ==============================================================================
c [1mFound solution: 258525[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:15424     Base: 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     98573 |  622559  1473988 |  207519   23893   737648    30.9 | 46.654 % |
c ==============================================================================
c [1mFound solution: 258522[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 |     98613 |  623258  1475835 |  207752   23930   739290    30.9 | 46.654 % |
c ==============================================================================
c [1mFound solution: 258521[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     98619 |  623270  1475865 |  207756   23936   739333    30.9 | 46.654 % |
c ==============================================================================
c [1mFound solution: 258511[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     98637 |  623769  1477084 |  207923   23954   744334    31.1 | 46.654 % |
c ==============================================================================
c [1mFound solution: 258509[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     98667 |  623838  1477281 |  207946   23984   744950    31.1 | 46.654 % |
c ==============================================================================
c [1mFound solution: 258504[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 |     98688 |  623858  1477329 |  207952   24005   747529    31.1 | 46.654 % |
c ==============================================================================
c [1mFound solution: 258469[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     98719 |  624153  1478050 |  208051   24036   747931    31.1 | 46.654 % |
c ==============================================================================
c [1mFound solution: 258437[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     98806 |  624202  1478185 |  208067   24123   754435    31.3 | 46.654 % |
c ==============================================================================
c [1mFound solution: 258436[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 |     98892 |  624227  1478244 |  208075   24209   756554    31.3 | 46.654 % |
c ==============================================================================
c [1mFound solution: 258432[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:13770     Base: 2 2 2 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     98966 |  544443  1293024 |  181481   18575   510106    27.5 | 46.654 % |
c |     99066 |  544373  1292864 |  199629   18636   518711    27.8 | 53.694 % |
c ==============================================================================
c [1mFound solution: 258422[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     99086 |  544483  1293178 |  181494   18656   518955    27.8 | 53.694 % |
c ==============================================================================
c [1mFound solution: 258420[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     99184 |  544501  1293222 |  181500   18754   521343    27.8 | 53.694 % |
c ==============================================================================
c [1mFound solution: 258419[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     99207 |  544336  1292855 |  181445   18775   521601    27.8 | 53.694 % |
c ==============================================================================
c [1mFound solution: 258413[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     99235 |  544403  1293042 |  181467   18803   522687    27.8 | 53.694 % |
c ==============================================================================
c [1mFound solution: 258398[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     99247 |  544411  1293062 |  181470   18815   523979    27.8 | 53.694 % |
c ==============================================================================
c [1mFound solution: 258397[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     99248 |  544420  1293085 |  181473   18816   524042    27.9 | 53.694 % |
c ==============================================================================
c [1mFound solution: 258396[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     99249 |  544107  1292358 |  181369   18816   524042    27.9 | 53.694 % |
c ==============================================================================
c [1mFound solution: 258390[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     99251 |  544123  1292398 |  181374   18818   524221    27.9 | 53.694 % |
c ==============================================================================
c [1mFound solution: 258389[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     99253 |  544131  1292418 |  181377   18820   524287    27.9 | 53.694 % |
c ==============================================================================
c [1mFound solution: 258388[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     99253 |  544146  1292455 |  181382   18820   524287    27.9 | 53.694 % |
c ==============================================================================
c [1mFound solution: 258387[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     99277 |  544111  1292372 |  181370   18841   525012    27.9 | 53.694 % |
c ==============================================================================
c [1mFound solution: 258386[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:10515     Base: 2 3 3 3 11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     99283 |  457346  1090242 |  152448   13884   366000    26.4 | 53.694 % |
c ==============================================================================
c [1mFound solution: 258385[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     99285 |     183      462 |      61       2        7     3.5 | 53.694 % |
c ==============================================================================
c [1mFound solution: 258384[0m
c [1mOptimal solution: 258384[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              : 301
c conflicts             : 99285          (84 /sec)
c decisions             : 307236         (259 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 1184.44 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.92 0.95 0.71 2/55 9497
Raw data (stat): 9497 (runsolver) R 9496 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 364874266 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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.0001 s]
Raw data (loadavg): 0.93 0.95 0.71 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 8627 0 0 0 979 19 0 0 25 0 1 0 364874266 38883328 8294 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9493 8294 603 41 0 9452 0
vsize: 37972
[startup+20.0008 s]
Raw data (loadavg): 0.94 0.96 0.71 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 8836 0 0 0 1978 20 0 0 25 0 1 0 364874266 39710720 8503 4294967295 134512640 134672761 3221224576 3221223776 134557915 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9695 8503 603 41 0 9654 0
vsize: 38780
[startup+30.0014 s]
Raw data (loadavg): 0.95 0.96 0.72 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 9031 0 0 0 2978 21 0 0 25 0 1 0 364874266 40390656 8698 4294967295 134512640 134672761 3221224576 3221223748 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9861 8698 603 41 0 9820 0
vsize: 39444
[startup+40.0021 s]
Raw data (loadavg): 0.96 0.96 0.72 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 9142 0 0 0 3978 21 0 0 25 0 1 0 364874266 40792064 8809 4294967295 134512640 134672761 3221224576 3221223136 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9959 8809 603 41 0 9918 0
vsize: 39836
[startup+50.0028 s]
Raw data (loadavg): 0.96 0.96 0.72 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 9213 0 0 0 4978 21 0 0 25 0 1 0 364874266 41062400 8880 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10025 8880 603 41 0 9984 0
vsize: 40100
[startup+60.0029 s]
Raw data (loadavg): 0.97 0.96 0.73 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 9304 0 0 0 5977 22 0 0 25 0 1 0 364874266 41398272 8971 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10107 8971 603 41 0 10066 0
vsize: 40428
[startup+70.0031 s]
Raw data (loadavg): 0.97 0.96 0.73 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 9352 0 0 0 6977 22 0 0 25 0 1 0 364874266 41627648 9019 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10163 9019 603 41 0 10122 0
vsize: 40652
[startup+80.0038 s]
Raw data (loadavg): 0.98 0.96 0.73 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 9424 0 0 0 7977 23 0 0 25 0 1 0 364874266 41938944 9091 4294967295 134512640 134672761 3221224576 3221223740 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10239 9091 603 41 0 10198 0
vsize: 40956
[startup+90.0045 s]
Raw data (loadavg): 0.98 0.96 0.73 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 9586 0 0 0 8977 23 0 0 25 0 1 0 364874266 42606592 9253 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10402 9253 603 41 0 10361 0
vsize: 41608
[startup+100.004 s]
Raw data (loadavg): 0.98 0.96 0.73 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 9709 0 0 0 9976 24 0 0 25 0 1 0 364874266 43134976 9376 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10531 9376 603 41 0 10490 0
vsize: 42124
[startup+110.004 s]
Raw data (loadavg): 0.98 0.96 0.74 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 9825 0 0 0 10975 24 0 0 25 0 1 0 364874266 43499520 9492 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10620 9492 603 41 0 10579 0
vsize: 42480
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.74 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 9903 0 0 0 11975 25 0 0 25 0 1 0 364874266 43900928 9570 4294967295 134512640 134672761 3221224576 3221223712 134565137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10718 9570 603 41 0 10677 0
vsize: 42872
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.74 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 10045 0 0 0 12974 26 0 0 25 0 1 0 364874266 44560384 9712 4294967295 134512640 134672761 3221224576 3221223744 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10879 9712 603 41 0 10838 0
vsize: 43516
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.74 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 10172 0 0 0 13974 26 0 0 25 0 1 0 364874266 45101056 9839 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11011 9839 603 41 0 10970 0
vsize: 44044
[startup+150.007 s]
Raw data (loadavg): 0.99 0.97 0.74 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 10441 0 0 0 14974 27 0 0 25 0 1 0 364874266 46174208 10108 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11273 10108 603 41 0 11232 0
vsize: 45092
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.75 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 10649 0 0 0 15973 28 0 0 25 0 1 0 364874266 46972928 10316 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11468 10316 603 41 0 11427 0
vsize: 45872
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.75 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 10734 0 0 0 16972 28 0 0 25 0 1 0 364874266 47374336 10401 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11566 10401 603 41 0 11525 0
vsize: 46264
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.75 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 10844 0 0 0 17972 29 0 0 25 0 1 0 364874266 47775744 10511 4294967295 134512640 134672761 3221224576 3221223760 134558883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11664 10511 603 41 0 11623 0
vsize: 46656
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.75 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 10898 0 0 0 18972 29 0 0 25 0 1 0 364874266 47996928 10565 4294967295 134512640 134672761 3221224576 3221223776 134557811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11718 10565 603 41 0 11677 0
vsize: 46872
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.75 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 10970 0 0 0 19972 29 0 0 25 0 1 0 364874266 48267264 10637 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11784 10637 603 41 0 11743 0
vsize: 47136
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.76 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 11046 0 0 0 20972 29 0 0 25 0 1 0 364874266 48533504 10713 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11849 10713 603 41 0 11808 0
vsize: 47396
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.76 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 11109 0 0 0 21972 29 0 0 25 0 1 0 364874266 48791552 10776 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11912 10776 603 41 0 11871 0
vsize: 47648
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.76 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 11203 0 0 0 22972 30 0 0 25 0 1 0 364874266 49192960 10870 4294967295 134512640 134672761 3221224576 3221223728 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12010 10870 603 41 0 11969 0
vsize: 48040
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.76 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 11303 0 0 0 23971 30 0 0 25 0 1 0 364874266 49594368 10970 4294967295 134512640 134672761 3221224576 3221223680 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12108 10970 603 41 0 12067 0
vsize: 48432
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.76 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 11443 0 0 0 24971 31 0 0 25 0 1 0 364874266 50130944 11110 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12239 11110 603 41 0 12198 0
vsize: 48956
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.77 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 11605 0 0 0 25970 31 0 0 25 0 1 0 364874266 50802688 11272 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12403 11272 603 41 0 12362 0
vsize: 49612
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.77 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 11740 0 0 0 26970 32 0 0 25 0 1 0 364874266 51343360 11407 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12535 11407 603 41 0 12494 0
vsize: 50140
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.77 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 11814 0 0 0 27970 32 0 0 25 0 1 0 364874266 51609600 11481 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12600 11481 603 41 0 12559 0
vsize: 50400
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.77 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 11863 0 0 0 28970 32 0 0 25 0 1 0 364874266 51871744 11530 4294967295 134512640 134672761 3221224576 3221223712 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12664 11530 603 41 0 12623 0
vsize: 50656
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.77 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 11940 0 0 0 29970 32 0 0 25 0 1 0 364874266 52170752 11607 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12737 11607 603 41 0 12696 0
vsize: 50948
[startup+310.007 s]
Raw data (loadavg): 0.99 0.97 0.78 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 11997 0 0 0 30969 33 0 0 25 0 1 0 364874266 52404224 11664 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12794 11664 603 41 0 12753 0
vsize: 51176
[startup+320.008 s]
Raw data (loadavg): 0.99 0.97 0.78 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 12019 0 0 0 31970 33 0 0 25 0 1 0 364874266 52535296 11686 4294967295 134512640 134672761 3221224576 3221223776 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12826 11686 603 41 0 12785 0
vsize: 51304
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.78 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 12058 0 0 0 32970 33 0 0 25 0 1 0 364874266 52674560 11725 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12860 11725 603 41 0 12819 0
vsize: 51440
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.78 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 12131 0 0 0 33969 33 0 0 25 0 1 0 364874266 52936704 11798 4294967295 134512640 134672761 3221224576 3221223724 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12924 11798 603 41 0 12883 0
vsize: 51696
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.78 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 12187 0 0 0 34969 34 0 0 25 0 1 0 364874266 53207040 11854 4294967295 134512640 134672761 3221224576 3221223740 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12990 11854 603 41 0 12949 0
vsize: 51960
[startup+360.009 s]
Raw data (loadavg): 0.99 0.97 0.79 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 12301 0 0 0 35969 34 0 0 25 0 1 0 364874266 53735424 11968 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13119 11968 603 41 0 13078 0
vsize: 52476
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.79 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 12370 0 0 0 36969 34 0 0 25 0 1 0 364874266 54005760 12037 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13185 12037 603 41 0 13144 0
vsize: 52740
[startup+380.009 s]
Raw data (loadavg): 0.99 0.97 0.79 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 12432 0 0 0 37968 35 0 0 25 0 1 0 364874266 54403072 12099 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13282 12099 603 41 0 13241 0
vsize: 53128
[startup+390.01 s]
Raw data (loadavg): 0.99 0.97 0.79 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 12522 0 0 0 38968 35 0 0 25 0 1 0 364874266 54808576 12189 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13381 12189 603 41 0 13340 0
vsize: 53524
[startup+400.011 s]
Raw data (loadavg): 0.99 0.97 0.79 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 12592 0 0 0 39968 36 0 0 25 0 1 0 364874266 55173120 12259 4294967295 134512640 134672761 3221224576 3221223744 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13470 12259 603 41 0 13429 0
vsize: 53880
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.79 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 12628 0 0 0 40967 36 0 0 25 0 1 0 364874266 55304192 12295 4294967295 134512640 134672761 3221224576 3221223136 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13502 12295 603 41 0 13461 0
vsize: 54008
[startup+420.01 s]
Raw data (loadavg): 0.99 0.97 0.80 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 12658 0 0 0 41967 36 0 0 25 0 1 0 364874266 55439360 12325 4294967295 134512640 134672761 3221224576 3221223748 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13535 12325 603 41 0 13494 0
vsize: 54140
[startup+430.011 s]
Raw data (loadavg): 0.99 0.97 0.80 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 12747 0 0 0 42967 37 0 0 25 0 1 0 364874266 55840768 12414 4294967295 134512640 134672761 3221224576 3221223712 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13633 12414 603 41 0 13592 0
vsize: 54532
[startup+440.011 s]
Raw data (loadavg): 0.99 0.97 0.80 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 12847 0 0 0 43967 37 0 0 25 0 1 0 364874266 56205312 12514 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13722 12514 603 41 0 13681 0
vsize: 54888
[startup+450.011 s]
Raw data (loadavg): 0.99 0.97 0.80 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 12903 0 0 0 44967 37 0 0 25 0 1 0 364874266 56467456 12570 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13786 12570 603 41 0 13745 0
vsize: 55144
[startup+460.011 s]
Raw data (loadavg): 0.99 0.97 0.80 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 12963 0 0 0 45966 38 0 0 25 0 1 0 364874266 56676352 12630 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13837 12630 603 41 0 13796 0
vsize: 55348
[startup+470.012 s]
Raw data (loadavg): 0.99 0.97 0.81 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 13018 0 0 0 46966 38 0 0 25 0 1 0 364874266 56889344 12685 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13889 12685 603 41 0 13848 0
vsize: 55556
[startup+480.012 s]
Raw data (loadavg): 0.99 0.97 0.81 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 13101 0 0 0 47966 39 0 0 25 0 1 0 364874266 57278464 12768 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13984 12768 603 41 0 13943 0
vsize: 55936
[startup+490.012 s]
Raw data (loadavg): 0.99 0.97 0.81 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 13188 0 0 0 48965 39 0 0 25 0 1 0 364874266 57569280 12855 4294967295 134512640 134672761 3221224576 3221222992 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14055 12855 603 41 0 14014 0
vsize: 56220
[startup+500.013 s]
Raw data (loadavg): 0.99 0.97 0.81 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 13215 0 0 0 49965 39 0 0 25 0 1 0 364874266 57720832 12882 4294967295 134512640 134672761 3221224576 3221223776 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14092 12882 603 41 0 14051 0
vsize: 56368
[startup+510.012 s]
Raw data (loadavg): 0.99 0.97 0.81 2/55 9497
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 13252 0 0 0 50965 40 0 0 25 0 1 0 364874266 57827328 12919 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14118 12919 603 41 0 14077 0
vsize: 56472
[startup+520.013 s]
Raw data (loadavg): 0.99 0.97 0.82 3/56 9498
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 13301 0 0 0 51964 40 0 0 25 0 1 0 364874266 58007552 12968 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14162 12968 603 41 0 14121 0
vsize: 56648
[startup+530.013 s]
Raw data (loadavg): 0.99 0.97 0.82 2/55 9550
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 13373 0 0 0 52959 40 0 0 25 0 1 0 364874266 58417152 13040 4294967295 134512640 134672761 3221224576 3221223760 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14262 13040 603 41 0 14221 0
vsize: 57048
[startup+540.014 s]
Raw data (loadavg): 0.99 0.97 0.82 2/55 9550
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 13429 0 0 0 53959 40 0 0 25 0 1 0 364874266 58560512 13096 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14297 13096 603 41 0 14256 0
vsize: 57188
[startup+550.013 s]
Raw data (loadavg): 0.99 0.97 0.82 2/55 9550
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 13474 0 0 0 54959 40 0 0 25 0 1 0 364874266 58826752 13141 4294967295 134512640 134672761 3221224576 3221223748 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13141 603 41 0 14321 0
vsize: 57448
[startup+560.013 s]
Raw data (loadavg): 0.99 0.97 0.82 2/55 9550
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 13559 0 0 0 55959 41 0 0 25 0 1 0 364874266 59072512 13226 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14422 13226 603 41 0 14381 0
vsize: 57688
[startup+570.013 s]
Raw data (loadavg): 0.99 0.97 0.82 2/55 9550
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 13588 0 0 0 56959 41 0 0 25 0 1 0 364874266 59195392 13255 4294967295 134512640 134672761 3221224576 3221223680 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14452 13255 603 41 0 14411 0
vsize: 57808
[startup+580.013 s]
Raw data (loadavg): 0.99 0.97 0.82 2/55 9552
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 13612 0 0 0 57959 41 0 0 25 0 1 0 364874266 59322368 13279 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14483 13279 603 41 0 14442 0
vsize: 57932
[startup+590.014 s]
Raw data (loadavg): 0.99 0.97 0.82 2/55 9554
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 16946 0 0 0 58952 48 0 0 25 0 1 0 364874266 79368192 16613 4294967295 134512640 134672761 3221224576 3221223736 134561238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19377 16613 603 41 0 19336 0
vsize: 77508
[startup+600.014 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 9554
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 17088 0 0 0 59952 49 0 0 25 0 1 0 364874266 79908864 16755 4294967295 134512640 134672761 3221224576 3221223680 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19509 16755 603 41 0 19468 0
vsize: 78036
[startup+610.013 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 9554
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 17117 0 0 0 60952 49 0 0 25 0 1 0 364874266 80044032 16784 4294967295 134512640 134672761 3221224576 3221223744 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19542 16784 603 41 0 19501 0
vsize: 78168
[startup+620.013 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 9554
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 17125 0 0 0 61952 49 0 0 25 0 1 0 364874266 80044032 16792 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19542 16792 603 41 0 19501 0
vsize: 78168
[startup+630.013 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 9554
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 17141 0 0 0 62952 49 0 0 25 0 1 0 364874266 80166912 16808 4294967295 134512640 134672761 3221224576 3221223680 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19572 16808 603 41 0 19531 0
vsize: 78288
[startup+640.013 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 9554
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 17141 0 0 0 63952 49 0 0 25 0 1 0 364874266 80166912 16808 4294967295 134512640 134672761 3221224576 3221223680 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19572 16808 603 41 0 19531 0
vsize: 78288
[startup+650.013 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 9554
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 17141 0 0 0 64953 49 0 0 25 0 1 0 364874266 80166912 16808 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19572 16808 603 41 0 19531 0
vsize: 78288
[startup+660.013 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 9554
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 17141 0 0 0 65953 49 0 0 25 0 1 0 364874266 80166912 16808 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19572 16808 603 41 0 19531 0
vsize: 78288
[startup+670.013 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 9554
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 17141 0 0 0 66953 49 0 0 25 0 1 0 364874266 80166912 16808 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19572 16808 603 41 0 19531 0
vsize: 78288
[startup+680.013 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 9554
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 17144 0 0 0 67953 49 0 0 25 0 1 0 364874266 80166912 16811 4294967295 134512640 134672761 3221224576 3221223712 134560622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19572 16811 603 41 0 19531 0
vsize: 78288
[startup+690.013 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 9554
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 19239 0 0 0 68950 52 0 0 25 0 1 0 364874266 85639168 18576 4294967295 134512640 134672761 3221224576 3221223680 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20908 18576 603 41 0 20867 0
vsize: 83632
[startup+700.013 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 9554
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 19387 0 0 0 69949 53 0 0 25 0 1 0 364874266 86171648 18724 4294967295 134512640 134672761 3221224576 3221223776 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21038 18724 603 41 0 20997 0
vsize: 84152
[startup+710.012 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 9554
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 19444 0 0 0 70949 53 0 0 25 0 1 0 364874266 86274048 18781 4294967295 134512640 134672761 3221224576 3221223680 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21063 18781 603 41 0 21022 0
vsize: 84252
[startup+720.012 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 9554
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 19485 0 0 0 71950 53 0 0 25 0 1 0 364874266 86409216 18822 4294967295 134512640 134672761 3221224576 3221222560 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21096 18822 603 41 0 21055 0
vsize: 84384
[startup+730.012 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 9554
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 19507 0 0 0 72950 53 0 0 25 0 1 0 364874266 86609920 18844 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21145 18844 603 41 0 21104 0
vsize: 84580
[startup+740.012 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 9554
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 19532 0 0 0 73950 53 0 0 25 0 1 0 364874266 86609920 18869 4294967295 134512640 134672761 3221224576 3221223680 134560269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21145 18869 603 41 0 21104 0
vsize: 84580
[startup+750.012 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 9554
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 19545 0 0 0 74950 53 0 0 25 0 1 0 364874266 86745088 18882 4294967295 134512640 134672761 3221224576 3221223680 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21178 18882 603 41 0 21137 0
vsize: 84712
[startup+760.012 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 9554
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 19555 0 0 0 75950 53 0 0 25 0 1 0 364874266 86745088 18892 4294967295 134512640 134672761 3221224576 3221223680 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21178 18892 603 41 0 21137 0
vsize: 84712
[startup+770.011 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 9554
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 19567 0 0 0 76950 53 0 0 25 0 1 0 364874266 86745088 18904 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21178 18904 603 41 0 21137 0
vsize: 84712
[startup+780.012 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 9554
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 19579 0 0 0 77950 54 0 0 25 0 1 0 364874266 86880256 18916 4294967295 134512640 134672761 3221224576 3221223680 134560191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21211 18916 603 41 0 21170 0
vsize: 84844
[startup+790.012 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 9554
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 19595 0 0 0 78950 54 0 0 25 0 1 0 364874266 86880256 18932 4294967295 134512640 134672761 3221224576 3221223680 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21211 18932 603 41 0 21170 0
vsize: 84844
[startup+800.012 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 9554
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 19621 0 0 0 79950 54 0 0 25 0 1 0 364874266 87015424 18958 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21244 18958 603 41 0 21203 0
vsize: 84976
[startup+810.011 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 9554
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 19642 0 0 0 80950 54 0 0 25 0 1 0 364874266 87150592 18979 4294967295 134512640 134672761 3221224576 3221223680 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21277 18979 603 41 0 21236 0
vsize: 85108
[startup+820.012 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 9554
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 19655 0 0 0 81950 54 0 0 25 0 1 0 364874266 87150592 18992 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21277 18992 603 41 0 21236 0
vsize: 85108
[startup+830.012 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 9554
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 19717 0 0 0 82950 55 0 0 25 0 1 0 364874266 87420928 19054 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21343 19054 603 41 0 21302 0
vsize: 85372
[startup+840.013 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 9556
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 19762 0 0 0 83949 55 0 0 25 0 1 0 364874266 87556096 19099 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21376 19099 603 41 0 21335 0
vsize: 85504
[startup+850.013 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 9556
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 19884 0 0 0 84948 56 0 0 25 0 1 0 364874266 88072192 19221 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21502 19221 603 41 0 21461 0
vsize: 86008
[startup+860.013 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 9556
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 19959 0 0 0 85948 56 0 0 25 0 1 0 364874266 88342528 19296 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21568 19296 603 41 0 21527 0
vsize: 86272
[startup+870.012 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 9556
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 19959 0 0 0 86948 56 0 0 25 0 1 0 364874266 88342528 19296 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21568 19296 603 41 0 21527 0
vsize: 86272
[startup+880.012 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 9556
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 19959 0 0 0 87949 56 0 0 25 0 1 0 364874266 88342528 19296 4294967295 134512640 134672761 3221224576 3221223680 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21568 19296 603 41 0 21527 0
vsize: 86272
[startup+890.016 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 9556
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 19964 0 0 0 88948 56 0 0 25 0 1 0 364874266 88477696 19301 4294967295 134512640 134672761 3221224576 3221223748 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21601 19301 603 41 0 21560 0
vsize: 86404
[startup+900.016 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 9556
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 20021 0 0 0 89948 56 0 0 25 0 1 0 364874266 88612864 19358 4294967295 134512640 134672761 3221224576 3221223680 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21634 19358 603 41 0 21593 0
vsize: 86536
[startup+910.015 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 9556
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 20021 0 0 0 90948 56 0 0 25 0 1 0 364874266 88612864 19358 4294967295 134512640 134672761 3221224576 3221223728 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21634 19358 603 41 0 21593 0
vsize: 86536
[startup+920.016 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 9556
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 20151 0 0 0 91948 57 0 0 25 0 1 0 364874266 89165824 19488 4294967295 134512640 134672761 3221224576 3221223776 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21769 19488 603 41 0 21728 0
vsize: 87076
[startup+930.015 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 9556
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 20215 0 0 0 92948 57 0 0 25 0 1 0 364874266 89419776 19552 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21831 19552 603 41 0 21790 0
vsize: 87324
[startup+940.015 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 9556
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 20215 0 0 0 93948 57 0 0 25 0 1 0 364874266 89419776 19552 4294967295 134512640 134672761 3221224576 3221223680 134560148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21831 19552 603 41 0 21790 0
vsize: 87324
[startup+950.015 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 9556
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 24794 0 0 0 94938 67 0 0 25 0 1 0 364874266 107999232 24131 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26367 24131 603 41 0 26326 0
vsize: 105468
[startup+960.015 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 9556
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 24794 0 0 0 95938 67 0 0 25 0 1 0 364874266 107999232 24131 4294967295 134512640 134672761 3221224576 3221223680 134560148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26367 24131 603 41 0 26326 0
vsize: 105468
[startup+970.015 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 9556
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 24794 0 0 0 96938 67 0 0 25 0 1 0 364874266 107999232 24131 4294967295 134512640 134672761 3221224576 3221223680 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26367 24131 603 41 0 26326 0
vsize: 105468
[startup+980.015 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 9556
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 25253 0 0 0 97938 68 0 0 25 0 1 0 364874266 123363328 24590 4294967295 134512640 134672761 3221224576 3221205184 1075350054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30118 24590 603 41 0 30077 0
vsize: 120472
[startup+990.015 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 9556
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 25429 0 0 0 98938 68 0 0 25 0 1 0 364874266 123297792 24766 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30102 24766 603 41 0 30061 0
vsize: 120408
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 9556
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 25827 0 0 0 99936 70 0 0 25 0 1 0 364874266 123297792 25164 4294967295 134512640 134672761 3221224576 3221222544 134522987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30102 25164 603 41 0 30061 0
vsize: 120408
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 9556
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 27747 0 0 0 100931 75 0 0 25 0 1 0 364874266 126943232 26425 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30992 26425 603 41 0 30951 0
vsize: 123968
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 9556
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 27747 0 0 0 101932 75 0 0 25 0 1 0 364874266 126943232 26425 4294967295 134512640 134672761 3221224576 3221223776 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30992 26425 603 41 0 30951 0
vsize: 123968
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 9556
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 28723 0 0 0 102929 77 0 0 25 0 1 0 364874266 129511424 27401 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31619 27401 603 41 0 31578 0
vsize: 126476
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 9556
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 28800 0 0 0 103929 77 0 0 25 0 1 0 364874266 129646592 27478 4294967295 134512640 134672761 3221224576 3221223764 134556676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31652 27478 603 41 0 31611 0
vsize: 126608
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 9556
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 29202 0 0 0 104929 78 0 0 25 0 1 0 364874266 130322432 27880 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31817 27880 603 41 0 31776 0
vsize: 127268
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 9556
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 30008 0 0 0 105927 80 0 0 25 0 1 0 364874266 132349952 28686 4294967295 134512640 134672761 3221224576 3221223876 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32312 28686 603 41 0 32271 0
vsize: 129248
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 9556
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 30020 0 0 0 106927 80 0 0 25 0 1 0 364874266 132431872 28698 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32332 28698 603 41 0 32291 0
vsize: 129328
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 9556
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 30022 0 0 0 107927 80 0 0 25 0 1 0 364874266 132431872 28700 4294967295 134512640 134672761 3221224576 3221223700 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32332 28700 603 41 0 32291 0
vsize: 129328
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 9556
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 30038 0 0 0 108927 80 0 0 25 0 1 0 364874266 132558848 28716 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32363 28716 603 41 0 32322 0
vsize: 129452
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 9556
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 30056 0 0 0 109927 80 0 0 25 0 1 0 364874266 132558848 28734 4294967295 134512640 134672761 3221224576 3221223700 134566122 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32363 28734 603 41 0 32322 0
vsize: 129452
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.87 2/55 9556
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 30742 0 0 0 110926 82 0 0 25 0 1 0 364874266 134590464 29420 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32859 29420 603 41 0 32818 0
vsize: 131436
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 9556
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 30793 0 0 0 111926 82 0 0 25 0 1 0 364874266 134590464 29471 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32859 29471 603 41 0 32818 0
vsize: 131436
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 9556
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 31630 0 0 0 112924 84 0 0 25 0 1 0 364874266 136908800 30308 4294967295 134512640 134672761 3221224576 3221223876 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33425 30308 603 41 0 33384 0
vsize: 133700
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 9556
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 31648 0 0 0 113924 85 0 0 25 0 1 0 364874266 136908800 30326 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33425 30326 603 41 0 33384 0
vsize: 133700
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 9556
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 31661 0 0 0 114924 85 0 0 25 0 1 0 364874266 137043968 30339 4294967295 134512640 134672761 3221224576 3221223768 134556585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33458 30339 603 41 0 33417 0
vsize: 133832
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 9556
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 32141 0 0 0 115923 86 0 0 25 0 1 0 364874266 137990144 30819 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33689 30819 603 41 0 33648 0
vsize: 134756
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 9556
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 32147 0 0 0 116923 86 0 0 25 0 1 0 364874266 137990144 30825 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33689 30825 603 41 0 33648 0
vsize: 134756
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 9556
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 32154 0 0 0 117923 86 0 0 25 0 1 0 364874266 137990144 30832 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33689 30832 603 41 0 33648 0
vsize: 134756
[startup+1185.46 s]
Raw data (loadavg): 0.99 0.97 0.88 1/54 9556
Raw data (stat): 9497 (minisat+) R 9496 30927 30926 0 -1 0 32154 0 0 0 117923 86 0 0 25 0 1 0 364874266 137990144 30832 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33689 30832 603 41 0 33648 0
vsize: 0

Child status: 30
Real time (s): 1185.46
CPU time (s): 1185.54
CPU user time (s): 1184.61
CPU system time (s): 0.931858
CPU usage (%): 100.007
Max. virtual memory (Kb): 134756
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	FAILED
ERROR: unsatisfied constraint on line 193
#### END VERIFIER DATA ####