PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-p0282.opb
MD5SUM	1a8deb577df7e72871b7e1004c098336
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.01984
Number of variables	282
Total number of constraints	523
Number of constraints which are clauses	177
Number of constraints which are cardinality constraints (but not clauses)	282
Number of constraints which are nor clauses,nor cardinality constraints	64
Minimum length of a constraint	1
Maximum length of a constraint	57
Trace number 21116

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc17 THE 2005-04-21 22:50:38 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13727 boxname=wulflinc17 idbench=1056 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  1a8deb577df7e72871b7e1004c098336  /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-p0282.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-p0282.opb /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-p0282.opb
IDLAUNCH: 13727
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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:        416160 kB
Buffers:         27736 kB
Cached:         565088 kB
SwapCached:        408 kB
Active:         144012 kB
Inactive:       451340 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        415908 kB
SwapTotal:     2097892 kB
SwapFree:      2097056 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5860 kB
Slab:            17448 kB
Committed_AS:    63820 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 23:10:40 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 13727 7 1200.2 10
#### 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 ---[ 223]---> BDD-cost:  580
c ---[ 222]---> BDD-cost:  587
c ---[ 221]---> BDD-cost:  540
c ---[ 220]---> BDD-cost:  394
c ---[ 219]---> BDD-cost:  497
c ---[ 218]---> BDD-cost:  370
c ---[ 217]---> BDD-cost:  386
c ---[ 216]---> BDD-cost:  415
c ---[ 215]---> BDD-cost:  348
c ---[ 214]---> BDD-cost:  385
c ---[ 213]---> BDD-cost:  744
c ---[ 211]---> BDD-cost:  791
c ---[ 209]---> BDD-cost:  828
c ---[ 208]---> BDD-cost:  473
c ---[ 207]---> BDD-cost:  492
c ---[ 206]---> BDD-cost:  528
c ---[ 205]---> BDD-cost:  310
c ---[ 204]---> BDD-cost:  347
c ---[ 203]---> BDD-cost:  219
c ---[ 202]---> BDD-cost:  267
c ---[ 201]---> BDD-cost:  593
c ---[ 199]---> BDD-cost:  396
c ---[ 198]---> BDD-cost:  448
c ---[ 197]---> BDD-cost:  323
c ---[ 196]---> BDD-cost:  369
c ---[ 195]---> BDD-cost:  578
c ---[ 194]---> BDD-cost:  602
c ---[ 193]---> BDD-cost:  659
c ---[ 192]---> BDD-cost:  350
c ---[ 191]---> BDD-cost:  872
c ---[ 190]---> BDD-cost:  362
c ---[ 189]---> BDD-cost:  897
c ---[ 188]---> BDD-cost:  423
c ---[ 187]---> BDD-cost:   56
c ---[ 186]---> BDD-cost:   10
c ---[ 185]---> BDD-cost:   56
c ---[ 184]---> BDD-cost:   56
c ---[ 183]---> BDD-cost:   16
c ---[ 182]---> BDD-cost:   26
c ---[ 181]---> BDD-cost:    8
c ---[ 180]---> BDD-cost:    4
c ---[   2]---> BDD-cost:   87
c ---[   1]---> BDD-cost:  143
c ---[   0]---> BDD-cost:    6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   41898   123412 |   13966       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 513010[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:77326     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 |         0 |  259193   631180 |   86397       0        0     nan |  0.000 % |
c |       101 |  259155   631099 |   95036      98     3620    36.9 |  0.064 % |
c |       251 |  259139   631065 |  104540     247     4873    19.7 |  0.069 % |
c |       478 |  259124   631032 |  114994     473     6580    13.9 |  0.073 % |
c |       815 |  259124   631032 |  126493     810     8587    10.6 |  0.073 % |
c |      1321 |  259099   630977 |  139143    1314    13473    10.3 |  0.081 % |
c |      2081 |  258740   630169 |  153057    2065    21521    10.4 |  0.191 % |
c ==============================================================================
c [1mFound solution: 498997[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 |      2156 |  259176   631678 |   86392    2136    22949    10.7 |  0.191 % |
c ==============================================================================
c [1mFound solution: 494881[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 |      2205 |  261090   636467 |   87030    2185    25546    11.7 |  0.191 % |
c |      2305 |  261090   636467 |   95733    2285    26048    11.4 |  0.223 % |
c |      2455 |  261084   636455 |  105306    2434    29181    12.0 |  0.227 % |
c |      2680 |  261020   636313 |  115836    2656    31234    11.8 |  0.245 % |
c ==============================================================================
c [1mFound solution: 489052[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     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 |      2929 |  260996   636263 |   86998    2900    37163    12.8 |  0.245 % |
c |      3029 |  260996   636263 |   95697    3000    38487    12.8 |  0.257 % |
c |      3184 |  260996   636263 |  105267    3155    41943    13.3 |  0.257 % |
c |      3409 |  260996   636263 |  115794    3380    46827    13.9 |  0.257 % |
c |      3746 |  260984   636236 |  127373    3716    51764    13.9 |  0.260 % |
c |      4252 |  260744   635700 |  140111    4216    58764    13.9 |  0.328 % |
c ==============================================================================
c [1mFound solution: 476792[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 |      4639 |  261607   638147 |   87202    4597    65258    14.2 |  0.328 % |
c |      4739 |  261607   638147 |   95922    4697    66637    14.2 |  0.387 % |
c |      4891 |  261599   638131 |  105514    4848    69883    14.4 |  0.391 % |
c |      5117 |  261265   637377 |  116065    5015    72749    14.5 |  0.494 % |
c |      5455 |  261153   637126 |  127672    5351    97792    18.3 |  0.530 % |
c |      5961 |  261134   637088 |  140439    5855   107474    18.4 |  0.540 % |
c |      6723 |  261021   636832 |  154483    6607   114145    17.3 |  0.578 % |
c ==============================================================================
c [1mFound solution: 467587[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 |      7001 |  261035   636870 |   87011    6884   118219    17.2 |  0.578 % |
c |      7101 |  261035   636870 |   95712    6984   118768    17.0 |  0.581 % |
c |      7252 |  261035   636870 |  105283    7135   119612    16.8 |  0.581 % |
c |      7479 |  260920   636614 |  115811    7354   126675    17.2 |  0.619 % |
c |      7816 |  260920   636614 |  127392    7691   132194    17.2 |  0.619 % |
c |      8322 |  260920   636614 |  140132    8197   136987    16.7 |  0.619 % |
c |      9082 |  260781   636299 |  154145    8950   145188    16.2 |  0.663 % |
c |     10222 |  260781   636299 |  169559   10090   163514    16.2 |  0.663 % |
c |     11930 |  260761   636254 |  186515   11797   203194    17.2 |  0.668 % |
c |     14495 |  260761   636254 |  205167   14362   283870    19.8 |  0.668 % |
c |     18339 |  260629   635955 |  225684   18171   377969    20.8 |  0.707 % |
c ==============================================================================
c [1mFound solution: 467586[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 |     21468 |  260976   636813 |   86992   21297   478405    22.5 |  0.707 % |
c |     21569 |  260976   636813 |   95691   21398   478954    22.4 |  0.714 % |
c |     21719 |  260976   636813 |  105260   21548   482573    22.4 |  0.714 % |
c |     21946 |  260976   636813 |  115786   21775   484743    22.3 |  0.714 % |
c |     22283 |  260976   636813 |  127364   22112   489498    22.1 |  0.714 % |
c |     22789 |  260976   636813 |  140101   22618   493010    21.8 |  0.714 % |
c |     23549 |  260976   636813 |  154111   23378   530738    22.7 |  0.714 % |
c |     24688 |  260976   636813 |  169522   24517   549168    22.4 |  0.714 % |
c ==============================================================================
c [1mFound solution: 467532[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 |     26257 |  260882   636798 |   86960   26083   636622    24.4 |  0.714 % |
c |     26357 |  260882   636798 |   95656   26183   638086    24.4 |  0.750 % |
c |     26507 |  260882   636798 |  105221   26333   639047    24.3 |  0.750 % |
c |     26732 |  260882   636798 |  115743   26558   641632    24.2 |  0.750 % |
c |     27069 |  260850   636726 |  127318   26891   643701    23.9 |  0.759 % |
c |     27575 |  260731   636457 |  140049   27392   678269    24.8 |  0.794 % |
c |     28337 |  260680   636355 |  154054   28148   751900    26.7 |  0.821 % |
c |     29477 |  260680   636355 |  169460   29288   771207    26.3 |  0.821 % |
c |     31185 |  260261   635403 |  186406   30951   792866    25.6 |  0.955 % |
c ==============================================================================
c [1mFound solution: 467181[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 |     31818 |  260268   635423 |   86756   31584   808504    25.6 |  0.955 % |
c |     31918 |  260164   635187 |   95431   31682   809278    25.5 |  0.986 % |
c |     32069 |  260164   635187 |  104974   31833   810098    25.4 |  0.986 % |
c ==============================================================================
c [1mFound solution: 416148[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 |     32194 |  260182   635428 |   86727   31958   813972    25.5 |  0.986 % |
c |     32296 |  260166   635396 |   95399   32059   815997    25.5 |  0.996 % |
c |     32448 |  260067   635173 |  104939   32176   820443    25.5 |  1.025 % |
c ==============================================================================
c [1mFound solution: 397360[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 |     32537 |  260074   635188 |   86691   32265   825831    25.6 |  1.025 % |
c |     32639 |  260074   635188 |   95360   32367   826753    25.5 |  1.026 % |
c |     32789 |  260074   635188 |  104896   32517   828781    25.5 |  1.026 % |
c |     33014 |  260034   635098 |  115385   32740   830243    25.4 |  1.038 % |
c |     33354 |  260034   635098 |  126924   33080   844043    25.5 |  1.038 % |
c |     33860 |  259805   634578 |  139616   33569   849366    25.3 |  1.119 % |
c |     34619 |  259715   634373 |  153578   34324   860826    25.1 |  1.149 % |
c ==============================================================================
c [1mFound solution: 397197[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     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 |     35604 |  259582   634080 |   86527   35085   904152    25.8 |  1.149 % |
c |     35706 |  259582   634080 |   95179   35187   905576    25.7 |  1.198 % |
c |     35856 |  259306   633454 |  104697   35277   919906    26.1 |  1.287 % |
c |     36081 |  259301   633444 |  115167   35501   932688    26.3 |  1.290 % |
c |     36419 |  259275   633392 |  126684   35836   945651    26.4 |  1.304 % |
c |     36925 |  259261   633364 |  139352   36340   982345    27.0 |  1.312 % |
c |     37686 |  259253   633348 |  153287   37099  1006608    27.1 |  1.316 % |
c |     38825 |  259019   632824 |  168616   38175  1033078    27.1 |  1.393 % |
c |     40534 |  259000   632786 |  185478   39882  1082583    27.1 |  1.403 % |
c ==============================================================================
c [1mFound solution: 392796[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 |     41981 |  258785   632307 |   86261   41144  1137670    27.7 |  1.403 % |
c |     42081 |  258785   632307 |   94887   41244  1138188    27.6 |  1.478 % |
c |     42231 |  258785   632307 |  104375   41394  1143754    27.6 |  1.478 % |
c |     42456 |  258779   632295 |  114813   41618  1153246    27.7 |  1.481 % |
c |     42793 |  258779   632295 |  126294   41955  1179844    28.1 |  1.481 % |
c |     43299 |  258779   632295 |  138924   42461  1184039    27.9 |  1.481 % |
c |     44058 |  258779   632295 |  152816   43220  1269904    29.4 |  1.481 % |
c ==============================================================================
c [1mFound solution: 392794[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 |     44949 |  258789   632325 |   86263   44111  1320493    29.9 |  1.481 % |
c |     45049 |  258789   632325 |   94889   44211  1321370    29.9 |  1.482 % |
c |     45199 |  258755   632247 |  104378   44358  1323938    29.8 |  1.493 % |
c |     45425 |  258755   632247 |  114816   44584  1337792    30.0 |  1.493 % |
c ==============================================================================
c [1mFound solution: 392793[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 |     45627 |  258765   632277 |   86255   44786  1357005    30.3 |  1.493 % |
c |     45728 |  258765   632277 |   94880   44887  1357995    30.3 |  1.494 % |
c |     45878 |  258765   632277 |  104368   45037  1358984    30.2 |  1.494 % |
c |     46103 |  258761   632269 |  114805   45261  1362350    30.1 |  1.496 % |
c ==============================================================================
c [1mFound solution: 374086[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 |     46345 |  258768   632288 |   86256   45502  1379989    30.3 |  1.496 % |
c |     46445 |  258768   632288 |   94881   45602  1380818    30.3 |  1.502 % |
c |     46595 |  258768   632288 |  104369   45752  1382275    30.2 |  1.502 % |
c |     46822 |  258768   632288 |  114806   45979  1395722    30.4 |  1.502 % |
c |     47161 |  258747   632246 |  126287   46315  1408436    30.4 |  1.513 % |
c |     47668 |  258710   632169 |  138916   46815  1426244    30.5 |  1.528 % |
c |     48427 |  258675   632088 |  152807   47571  1435198    30.2 |  1.540 % |
c |     49568 |  258675   632088 |  168088   48712  1479350    30.4 |  1.540 % |
c |     51277 |  258657   632052 |  184897   50419  1567140    31.1 |  1.550 % |
c ==============================================================================
c [1mFound solution: 357831[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     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 |     51793 |  258550   631822 |   86183   50893  1588490    31.2 |  1.550 % |
c |     51895 |  258550   631822 |   94801   50995  1589403    31.2 |  1.596 % |
c |     52045 |  258550   631822 |  104281   51145  1601493    31.3 |  1.596 % |
c ==============================================================================
c [1mFound solution: 357615[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 |     52195 |  258559   631847 |   86186   51295  1619191    31.6 |  1.596 % |
c |     52295 |  258559   631847 |   94804   51395  1621879    31.6 |  1.597 % |
c |     52446 |  258559   631847 |  104285   51546  1622727    31.5 |  1.597 % |
c |     52672 |  258559   631847 |  114713   51772  1639746    31.7 |  1.597 % |
c |     53010 |  258559   631847 |  126184   52110  1676953    32.2 |  1.597 % |
c |     53516 |  258559   631847 |  138803   52616  1708554    32.5 |  1.597 % |
c |     54275 |  258559   631847 |  152683   53375  1728919    32.4 |  1.597 % |
c |     55417 |  258559   631847 |  167952   54517  1772591    32.5 |  1.597 % |
c ==============================================================================
c [1mFound solution: 357593[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 |     55733 |  258574   632077 |   86191   54833  1797621    32.8 |  1.597 % |
c |     55834 |  258574   632077 |   94810   54934  1799112    32.8 |  1.598 % |
c |     55984 |  258574   632077 |  104291   55084  1800225    32.7 |  1.598 % |
c |     56209 |  258574   632077 |  114720   55309  1804322    32.6 |  1.598 % |
c |     56546 |  258574   632077 |  126192   55646  1822043    32.7 |  1.598 % |
c |     57052 |  258574   632077 |  138811   56152  1826483    32.5 |  1.598 % |
c |     57812 |  258368   631609 |  152692   56905  1861025    32.7 |  1.657 % |
c |     58952 |  258368   631609 |  167961   58045  1955617    33.7 |  1.657 % |
c ==============================================================================
c [1mFound solution: 357592[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 |     59279 |  258368   631616 |   86122   58371  1972295    33.8 |  1.657 % |
c |     59379 |  258302   631467 |   94734   58470  1973365    33.8 |  1.685 % |
c |     59531 |  258302   631467 |  104207   58622  1980332    33.8 |  1.685 % |
c |     59756 |  258302   631467 |  114628   58847  1987941    33.8 |  1.685 % |
c |     60094 |  258286   631435 |  126091   59183  2017275    34.1 |  1.694 % |
c |     60602 |  258280   631423 |  138700   59690  2060743    34.5 |  1.697 % |
c |     61362 |  258147   631118 |  152570   60442  2075956    34.3 |  1.747 % |
c |     62501 |  258147   631118 |  167827   61581  2207444    35.8 |  1.747 % |
c |     64209 |  258147   631118 |  184610   63289  2399678    37.9 |  1.747 % |
c |     66772 |  258141   631106 |  203071   65851  2498520    37.9 |  1.749 % |
c |     70616 |  258141   631106 |  223378   69695  2740735    39.3 |  1.749 % |
c |     76384 |  258119   631056 |  245716   75460  2861887    37.9 |  1.755 % |
c ==============================================================================
c [1mFound solution: 356984[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 |     76768 |  258133   631093 |   86044   75844  2869388    37.8 |  1.755 % |
c |     76868 |  258133   631093 |   94648   75944  2870090    37.8 |  1.756 % |
c |     77020 |  258133   631093 |  104113   76096  2871039    37.7 |  1.756 % |
c |     77246 |  258133   631093 |  114524   76322  2872290    37.6 |  1.756 % |
c ==============================================================================
c [1mFound solution: 353456[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 |     77410 |  258140   631115 |   86046   76486  2880896    37.7 |  1.756 % |
c ==============================================================================
c [1mFound solution: 353455[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 |     77489 |  258147   631133 |   86049   76565  2882170    37.6 |  1.756 % |
c |     77589 |  258147   631133 |   94653   76665  2886845    37.7 |  1.758 % |
c |     77741 |  258147   631133 |  104119   76817  2895212    37.7 |  1.758 % |
c |     77966 |  258147   631133 |  114531   77042  2917655    37.9 |  1.758 % |
c |     78303 |  258133   631105 |  125984   77378  2942805    38.0 |  1.764 % |
c |     78809 |  258129   631097 |  138582   77883  2981995    38.3 |  1.766 % |
c |     79569 |  258129   631097 |  152441   78643  3027838    38.5 |  1.766 % |
c ==============================================================================
c [1mFound solution: 352971[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 |     79610 |  258139   631124 |   86046   78684  3029287    38.5 |  1.766 % |
c ==============================================================================
c [1mFound solution: 352970[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 |     79652 |  258149   631152 |   86049   78726  3033329    38.5 |  1.766 % |
c |     79752 |  258149   631152 |   94653   78826  3036444    38.5 |  1.768 % |
c |     79902 |  258149   631152 |  104119   78976  3047309    38.6 |  1.768 % |
c |     80127 |  258149   631152 |  114531   79201  3065589    38.7 |  1.768 % |
c |     80466 |  258149   631152 |  125984   79540  3098858    39.0 |  1.768 % |
c |     80972 |  258149   631152 |  138582   80046  3136188    39.2 |  1.768 % |
c |     81731 |  258149   631152 |  152441   80805  3264922    40.4 |  1.768 % |
c |     82870 |  258145   631144 |  167685   81943  3333338    40.7 |  1.770 % |
c |     84578 |  258141   631136 |  184453   83650  3569773    42.7 |  1.772 % |
c |     87140 |  258141   631136 |  202899   86212  3850183    44.7 |  1.772 % |
c |     90984 |  258141   631136 |  223188   90056  4371306    48.5 |  1.772 % |
c ==============================================================================
c [1mFound solution: 352969[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 |     94738 |  258139   631140 |   86046   93809  4816374    51.3 |  1.772 % |
c |     94841 |  258139   631140 |   94650   26654  1588476    59.6 |  1.780 % |
c |     94991 |  258139   631140 |  104115   26804  1595613    59.5 |  1.780 % |
c ==============================================================================
c [1mFound solution: 331113[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 |     95154 |  258152   631171 |   86050   26967  1597361    59.2 |  1.780 % |
c |     95255 |  258152   631171 |   94655   27068  1597893    59.0 |  1.781 % |
c |     95406 |  258152   631171 |  104120   27219  1617892    59.4 |  1.781 % |
c |     95632 |  258145   631157 |  114532   27444  1633120    59.5 |  1.784 % |
c |     95969 |  258138   631143 |  125985   27780  1653086    59.5 |  1.787 % |
c |     96476 |  258138   631143 |  138584   28287  1674392    59.2 |  1.787 % |
c |     97235 |  258138   631143 |  152442   29046  1708620    58.8 |  1.787 % |
c |     98375 |  258138   631143 |  167687   30186  1789788    59.3 |  1.787 % |
c |    100087 |  258138   631143 |  184455   31898  1905905    59.7 |  1.787 % |
c ==============================================================================
c [1mFound solution: 330534[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     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 |    102099 |  258141   631152 |   86047   33908  2049525    60.4 |  1.787 % |
c |    102201 |  258141   631152 |   94651   34010  2050464    60.3 |  1.791 % |
c |    102351 |  258141   631152 |  104116   34160  2054690    60.1 |  1.791 % |
c |    102576 |  258141   631152 |  114528   34385  2064233    60.0 |  1.791 % |
c |    102914 |  258132   631134 |  125981   34721  2096107    60.4 |  1.795 % |
c |    103420 |  258123   631116 |  138579   35225  2138135    60.7 |  1.799 % |
c |    104180 |  258123   631116 |  152437   35985  2168832    60.3 |  1.799 % |
c |    105320 |  258123   631116 |  167681   37125  2265246    61.0 |  1.799 % |
c |    107028 |  258123   631116 |  184449   38833  2578414    66.4 |  1.799 % |
c |    109591 |  258105   631080 |  202894   41395  2715872    65.6 |  1.808 % |
c ==============================================================================
c [1mFound solution: 330532[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 |    110485 |  258116   631107 |   86038   42289  2828505    66.9 |  1.808 % |
c |    110586 |  258099   631073 |   94641   42389  2840524    67.0 |  1.818 % |
c |    110736 |  258088   631051 |  104105   42536  2846739    66.9 |  1.822 % |
c |    110964 |  258088   631051 |  114516   42764  2848455    66.6 |  1.822 % |
c |    111301 |  258088   631051 |  125968   43101  2852967    66.2 |  1.822 % |
c |    111808 |  258088   631051 |  138565   43608  2867535    65.8 |  1.822 % |
c ==============================================================================
c [1mFound solution: 330344[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 |    112455 |  258096   631071 |   86032   44254  2898369    65.5 |  1.822 % |
c |    112555 |  258096   631071 |   94635   44354  2898888    65.4 |  1.825 % |
c |    112705 |  258090   631059 |  104098   44503  2907865    65.3 |  1.828 % |
c |    112930 |  258086   631051 |  114508   44727  2920418    65.3 |  1.830 % |
c |    113270 |  258086   631051 |  125959   45067  2944898    65.3 |  1.830 % |
c |    113778 |  258086   631051 |  138555   45575  2997382    65.8 |  1.830 % |
c |    114541 |  258058   630995 |  152410   46335  3026520    65.3 |  1.844 % |
c |    115680 |  258032   630943 |  167652   47470  3094584    65.2 |  1.856 % |
c |    117388 |  258023   630925 |  184417   49177  3249344    66.1 |  1.861 % |
c ==============================================================================
c [1mFound solution: 327168[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 |    118671 |  258035   630957 |   86011   50460  3384068    67.1 |  1.861 % |
c |    118772 |  258035   630957 |   94612   50561  3384947    66.9 |  1.862 % |
c |    118922 |  258035   630957 |  104073   50711  3385943    66.8 |  1.862 % |
c |    119147 |  258035   630957 |  114480   50936  3393108    66.6 |  1.862 % |
c |    119485 |  257975   630822 |  125928   51270  3408370    66.5 |  1.880 % |
c |    119991 |  257973   630818 |  138521   51775  3435578    66.4 |  1.882 % |
c |    120751 |  257967   630806 |  152373   52534  3481224    66.3 |  1.885 % |
c ==============================================================================
c [1mFound solution: 327087[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 |    121845 |  257978   630834 |   85992   53628  3589608    66.9 |  1.885 % |
c |    121945 |  257978   630834 |   94591   53728  3590157    66.8 |  1.886 % |
c |    122095 |  257978   630834 |  104050   53878  3590947    66.6 |  1.886 % |
c |    122320 |  257968   630814 |  114455   54102  3595243    66.5 |  1.891 % |
c |    122657 |  257968   630814 |  125900   54439  3621169    66.5 |  1.891 % |
c |    123163 |  257968   630814 |  138490   54945  3657376    66.6 |  1.891 % |
c |    123922 |  257962   630802 |  152340   55702  3697323    66.4 |  1.895 % |
c ==============================================================================
c [1mFound solution: 326761[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 |    124101 |  257978   630840 |   85992   55881  3725280    66.7 |  1.895 % |
c |    124201 |  257973   630830 |   94591   55980  3736888    66.8 |  1.898 % |
c |    124353 |  257973   630830 |  104050   56132  3744535    66.7 |  1.898 % |
c ==============================================================================
c [1mFound solution: 325755[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 |    124528 |  257984   630856 |   85994   56307  3761684    66.8 |  1.898 % |
c |    124628 |  257984   630856 |   94593   56407  3762535    66.7 |  1.899 % |
c |    124780 |  257984   630856 |  104052   56559  3765066    66.6 |  1.899 % |
c |    125005 |  257984   630856 |  114458   56784  3767067    66.3 |  1.899 % |
c |    125342 |  257976   630840 |  125903   57120  3790584    66.4 |  1.903 % |
c ==============================================================================
c [1mFound solution: 324296[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 |    125572 |  257985   630861 |   85995   57350  3807964    66.4 |  1.903 % |
c |    125675 |  257985   630861 |   94594   57453  3816308    66.4 |  1.904 % |
c |    125827 |  257985   630861 |  104053   57605  3827887    66.5 |  1.904 % |
c |    126052 |  257985   630861 |  114459   57830  3843328    66.5 |  1.904 % |
c |    126389 |  257985   630861 |  125905   58167  3869622    66.5 |  1.904 % |
c |    126897 |  257985   630861 |  138495   58675  3926248    66.9 |  1.904 % |
c |    127657 |  257985   630861 |  152345   59435  3970340    66.8 |  1.904 % |
c |    128797 |  257985   630861 |  167579   60575  4091789    67.5 |  1.904 % |
c ==============================================================================
c [1mFound solution: 324294[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 |    129958 |  257989   630870 |   85996   61736  4150369    67.2 |  1.904 % |
c |    130058 |  257989   630870 |   94595   61836  4156458    67.2 |  1.905 % |
c |    130208 |  257989   630870 |  104055   61986  4157553    67.1 |  1.905 % |
c |    130435 |  257989   630870 |  114460   62213  4163857    66.9 |  1.905 % |
c |    130773 |  257989   630870 |  125906   62551  4212703    67.3 |  1.905 % |
c |    131280 |  257989   630870 |  138497   63058  4277068    67.8 |  1.905 % |
c ==============================================================================
c [1mFound solution: 324261[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 |    131425 |  258003   630905 |   86001   63203  4296758    68.0 |  1.905 % |
c |    131527 |  258003   630905 |   94601   63305  4297414    67.9 |  1.906 % |
c |    131678 |  258003   630905 |  104061   63456  4298367    67.7 |  1.906 % |
c |    131903 |  258003   630905 |  114467   63681  4317691    67.8 |  1.906 % |
c |    132241 |  258003   630905 |  125914   64019  4334770    67.7 |  1.906 % |
c |    132748 |  258003   630905 |  138505   64526  4366368    67.7 |  1.906 % |
c ==============================================================================
c [1mFound solution: 323811[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 |    133502 |  258012   630926 |   86004   65280  4440378    68.0 |  1.906 % |
c |    133603 |  258012   630926 |   94604   65381  4449184    68.1 |  1.907 % |
c |    133753 |  258012   630926 |  104064   65531  4485658    68.5 |  1.907 % |
c |    133979 |  258012   630926 |  114471   65757  4494120    68.3 |  1.907 % |
c |    134316 |  258012   630926 |  125918   66094  4535646    68.6 |  1.907 % |
c ==============================================================================
c [1mFound solution: 323792[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 |    134432 |  258026   630960 |   86008   66210  4546111    68.7 |  1.907 % |
c |    134532 |  258026   630960 |   94608   66310  4548959    68.6 |  1.908 % |
c |    134683 |  258018   630942 |  104069   66460  4550008    68.5 |  1.910 % |
c |    134908 |  258018   630942 |  114476   66685  4553484    68.3 |  1.910 % |
c |    135245 |  258018   630942 |  125924   67022  4569647    68.2 |  1.910 % |
c |    135751 |  258018   630942 |  138516   67528  4644702    68.8 |  1.910 % |
c ==============================================================================
c [1mFound solution: 274665[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 |    136125 |  258042   631003 |   86014   67902  4677304    68.9 |  1.910 % |
c |    136225 |  257923   630734 |   94615   67999  4677961    68.8 |  1.947 % |
c |    136375 |  257905   630693 |  104076   68147  4678723    68.7 |  1.953 % |
c |    136600 |  257883   630643 |  114484   68367  4683640    68.5 |  1.959 % |
c ==============================================================================
c [1mFound solution: 265977[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     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 |    136819 |  257890   630660 |   85963   68586  4707183    68.6 |  1.959 % |
c |    136919 |  257890   630660 |   94559   68686  4708971    68.6 |  1.960 % |
c ==============================================================================
c [1mFound solution: 265974[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 |    137059 |  257897   630678 |   85965   68826  4713599    68.5 |  1.960 % |
c |    137159 |  257880   630640 |   94561   68923  4714256    68.4 |  1.969 % |
c |    137309 |  257880   630640 |  104017   69073  4717909    68.3 |  1.969 % |
c ==============================================================================
c [1mFound solution: 265005[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 |    137468 |  257889   630662 |   85963   69232  4721996    68.2 |  1.969 % |
c |    137568 |  257889   630662 |   94559   69332  4726681    68.2 |  1.970 % |
c ==============================================================================
c [1mFound solution: 265000[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 |    137629 |  257899   630690 |   85966   69393  4732215    68.2 |  1.970 % |
c ==============================================================================
c [1mFound solution: 264988[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 |    137670 |  257909   630715 |   85969   69434  4733739    68.2 |  1.970 % |
c |    137771 |  257909   630715 |   94565   69535  4738675    68.1 |  1.972 % |
c |    137921 |  257909   630715 |  104022   69685  4740505    68.0 |  1.972 % |
c |    138147 |  257797   630461 |  114424   69843  4750759    68.0 |  2.007 % |
c ==============================================================================
c [1mFound solution: 264870[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 |    138445 |  257806   630483 |   85935   70141  4770299    68.0 |  2.007 % |
c |    138545 |  257806   630483 |   94528   70241  4773243    68.0 |  2.008 % |
c |    138696 |  257205   629099 |  103981   70359  4777112    67.9 |  2.213 % |
c ==============================================================================
c [1mFound solution: 264835[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 |    138822 |  257218   629133 |   85739   70485  4782946    67.9 |  2.213 % |
c |    138922 |  257218   629133 |   94312   70585  4788353    67.8 |  2.214 % |
c ==============================================================================
c [1mFound solution: 264600[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 |    138951 |  257228   629157 |   85742   70614  4793705    67.9 |  2.214 % |
c ==============================================================================
c [1mFound solution: 264599[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 |    139048 |  257240   629186 |   85746   70711  4799831    67.9 |  2.214 % |
c |    139149 |  257240   629186 |   94320   70812  4804449    67.8 |  2.216 % |
c ==============================================================================
c [1mFound solution: 264591[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 |    139283 |  257252   629215 |   85750   70946  4812382    67.8 |  2.216 % |
c |    139384 |  257252   629215 |   94325   71047  4812990    67.7 |  2.217 % |
c |    139534 |  257244   629197 |  103757   71196  4814407    67.6 |  2.219 % |
c |    139759 |  257244   629197 |  114133   71421  4834542    67.7 |  2.219 % |
c ==============================================================================
c [1mFound solution: 264585[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 |    140022 |  256769   628110 |   85589   71638  4896753    68.4 |  2.219 % |
c |    140122 |  256769   628110 |   94147   71738  4899538    68.3 |  2.380 % |
c |    140272 |  256769   628110 |  103562   71888  4931442    68.6 |  2.380 % |
c |    140497 |  256769   628110 |  113918   72113  4939066    68.5 |  2.380 % |
c ==============================================================================
c [1mFound solution: 264519[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     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 |    140666 |  256776   628127 |   85592   72282  4956908    68.6 |  2.380 % |
c ==============================================================================
c [1mFound solution: 264500[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 |    140759 |  256786   628152 |   85595   72375  4962193    68.6 |  2.380 % |
c |    140859 |  256786   628152 |   94154   72475  4963196    68.5 |  2.382 % |
c |    141010 |  256732   628030 |  103569   72615  4971024    68.5 |  2.398 % |
c ==============================================================================
c [1mFound solution: 264499[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 |    141130 |  256744   628062 |   85581   72735  4985177    68.5 |  2.398 % |
c |    141231 |  256678   627911 |   94139   72827  4985677    68.5 |  2.419 % |
c |    141381 |  256416   627313 |  103553   72951  4988588    68.4 |  2.505 % |
#### 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.84 0.94 0.90 2/55 6986
Raw data (stat): 6986 (runsolver) R 6985 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 548822930 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0008 s]
Raw data (loadavg): 0.87 0.94 0.90 2/55 6986
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 7919 0 0 0 981 17 0 0 25 0 1 0 548822930 36589568 7587 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8933 7587 603 41 0 8892 0
vsize: 35732
[startup+20.0002 s]
Raw data (loadavg): 0.89 0.94 0.90 2/55 6986
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 8148 0 0 0 1980 18 0 0 25 0 1 0 548822930 37511168 7816 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9158 7816 603 41 0 9117 0
vsize: 36632
[startup+30.0008 s]
Raw data (loadavg): 0.90 0.94 0.90 2/55 6986
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 8245 0 0 0 2980 19 0 0 25 0 1 0 548822930 37834752 7913 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9237 7913 603 41 0 9196 0
vsize: 36948
[startup+40.0009 s]
Raw data (loadavg): 0.92 0.94 0.90 2/55 6986
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 8327 0 0 0 3979 19 0 0 25 0 1 0 548822930 38154240 7995 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9315 7995 603 41 0 9274 0
vsize: 37260
[startup+50.002 s]
Raw data (loadavg): 0.93 0.94 0.90 2/55 6986
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 8421 0 0 0 4979 19 0 0 25 0 1 0 548822930 38555648 8089 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9413 8089 603 41 0 9372 0
vsize: 37652
[startup+60.0016 s]
Raw data (loadavg): 0.94 0.95 0.90 2/55 6986
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 8575 0 0 0 5979 20 0 0 25 0 1 0 548822930 39264256 8243 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9586 8243 603 41 0 9545 0
vsize: 38344
[startup+70.0017 s]
Raw data (loadavg): 0.95 0.95 0.91 2/55 6986
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 8729 0 0 0 6977 22 0 0 25 0 1 0 548822930 39800832 8397 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9717 8397 603 41 0 9676 0
vsize: 38868
[startup+80.0019 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 6986
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 8882 0 0 0 7976 23 0 0 25 0 1 0 548822930 40476672 8550 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9882 8550 603 41 0 9841 0
vsize: 39528
[startup+90.0019 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 6986
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 8961 0 0 0 8976 23 0 0 25 0 1 0 548822930 40747008 8629 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9948 8629 603 41 0 9907 0
vsize: 39792
[startup+100.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 6986
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 9097 0 0 0 9975 24 0 0 25 0 1 0 548822930 41287680 8765 4294967295 134512640 134672761 3221224544 3221223680 134560637 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10080 8765 603 41 0 10039 0
vsize: 40320
[startup+110.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 6986
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 9193 0 0 0 10975 25 0 0 25 0 1 0 548822930 41807872 8861 4294967295 134512640 134672761 3221224544 3221223760 134558131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10207 8861 603 41 0 10166 0
vsize: 40828
[startup+120.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 6986
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 9244 0 0 0 11974 25 0 0 25 0 1 0 548822930 42057728 8912 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10268 8912 603 41 0 10227 0
vsize: 41072
[startup+130.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 6986
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 9290 0 0 0 12973 26 0 0 25 0 1 0 548822930 42192896 8958 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10301 8958 603 41 0 10260 0
vsize: 41204
[startup+140.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 6986
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 9372 0 0 0 13973 27 0 0 25 0 1 0 548822930 42598400 9040 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10400 9040 603 41 0 10359 0
vsize: 41600
[startup+150.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 6986
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 9463 0 0 0 14972 28 0 0 25 0 1 0 548822930 42864640 9131 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10465 9131 603 41 0 10424 0
vsize: 41860
[startup+160.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 6986
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 9561 0 0 0 15972 28 0 0 25 0 1 0 548822930 43270144 9229 4294967295 134512640 134672761 3221224544 3221223712 134561403 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10564 9229 603 41 0 10523 0
vsize: 42256
[startup+170.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 6986
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 9700 0 0 0 16971 29 0 0 25 0 1 0 548822930 43810816 9368 4294967295 134512640 134672761 3221224544 3221223712 134561226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10696 9368 603 41 0 10655 0
vsize: 42784
[startup+180.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 6986
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 9771 0 0 0 17970 30 0 0 25 0 1 0 548822930 44077056 9439 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10761 9439 603 41 0 10720 0
vsize: 43044
[startup+190.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 6986
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 9822 0 0 0 18970 30 0 0 25 0 1 0 548822930 44343296 9490 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10826 9490 603 41 0 10785 0
vsize: 43304
[startup+200.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 6986
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 9917 0 0 0 19969 31 0 0 25 0 1 0 548822930 44744704 9585 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10924 9585 603 41 0 10883 0
vsize: 43696
[startup+210.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 6988
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 10017 0 0 0 20968 32 0 0 25 0 1 0 548822930 45142016 9685 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11021 9685 603 41 0 10980 0
vsize: 44084
[startup+220.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 6988
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 10083 0 0 0 21968 33 0 0 25 0 1 0 548822930 45375488 9751 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11078 9751 603 41 0 11037 0
vsize: 44312
[startup+230.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 6988
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 10151 0 0 0 22967 34 0 0 25 0 1 0 548822930 45641728 9819 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11143 9819 603 41 0 11102 0
vsize: 44572
[startup+240.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 6988
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 10223 0 0 0 23966 34 0 0 25 0 1 0 548822930 45912064 9891 4294967295 134512640 134672761 3221224544 3221223700 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11209 9891 603 41 0 11168 0
vsize: 44836
[startup+250.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 6988
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 10293 0 0 0 24966 35 0 0 25 0 1 0 548822930 46174208 9961 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11273 9961 603 41 0 11232 0
vsize: 45092
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6988
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 10376 0 0 0 25965 36 0 0 25 0 1 0 548822930 46575616 10044 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11371 10044 603 41 0 11330 0
vsize: 45484
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6988
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 10454 0 0 0 26965 37 0 0 25 0 1 0 548822930 46841856 10122 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11436 10122 603 41 0 11395 0
vsize: 45744
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6988
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 10494 0 0 0 27964 37 0 0 25 0 1 0 548822930 46977024 10162 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11469 10162 603 41 0 11428 0
vsize: 45876
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6988
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 10576 0 0 0 28964 38 0 0 25 0 1 0 548822930 47378432 10244 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11567 10244 603 41 0 11526 0
vsize: 46268
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6988
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 10675 0 0 0 29963 38 0 0 25 0 1 0 548822930 47783936 10343 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11666 10343 603 41 0 11625 0
vsize: 46664
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6988
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 10757 0 0 0 30962 40 0 0 25 0 1 0 548822930 48041984 10425 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11729 10425 603 41 0 11688 0
vsize: 46916
[startup+320.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6988
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 10855 0 0 0 31961 41 0 0 25 0 1 0 548822930 48443392 10523 4294967295 134512640 134672761 3221224544 3221223648 134560393 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11827 10523 603 41 0 11786 0
vsize: 47308
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6988
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 10945 0 0 0 32961 41 0 0 25 0 1 0 548822930 48836608 10613 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11923 10613 603 41 0 11882 0
vsize: 47692
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6988
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 11018 0 0 0 33961 41 0 0 25 0 1 0 548822930 49106944 10686 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11989 10686 603 41 0 11948 0
vsize: 47956
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6988
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 11081 0 0 0 34960 42 0 0 25 0 1 0 548822930 49635328 10749 4294967295 134512640 134672761 3221224544 3221223648 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12118 10749 603 41 0 12077 0
vsize: 48472
[startup+360.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6988
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 11128 0 0 0 35960 42 0 0 25 0 1 0 548822930 49893376 10796 4294967295 134512640 134672761 3221224544 3221223808 134562262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12181 10796 603 41 0 12140 0
vsize: 48724
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6988
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 11184 0 0 0 36960 43 0 0 25 0 1 0 548822930 50024448 10852 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12213 10852 603 41 0 12172 0
vsize: 48852
[startup+380.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6988
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 11230 0 0 0 37960 43 0 0 25 0 1 0 548822930 50286592 10898 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12277 10898 603 41 0 12236 0
vsize: 49108
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6988
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 11358 0 0 0 38959 44 0 0 25 0 1 0 548822930 50827264 11026 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12409 11026 603 41 0 12368 0
vsize: 49636
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6988
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 11521 0 0 0 39958 45 0 0 25 0 1 0 548822930 51359744 11189 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12539 11189 603 41 0 12498 0
vsize: 50156
[startup+410.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6988
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 11565 0 0 0 40957 46 0 0 25 0 1 0 548822930 51625984 11233 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12604 11233 603 41 0 12563 0
vsize: 50416
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6988
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 11631 0 0 0 41956 47 0 0 25 0 1 0 548822930 51888128 11299 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12668 11299 603 41 0 12627 0
vsize: 50672
[startup+430.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6988
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 11697 0 0 0 42956 47 0 0 25 0 1 0 548822930 52150272 11365 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12732 11365 603 41 0 12691 0
vsize: 50928
[startup+440.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6988
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 11746 0 0 0 43956 48 0 0 25 0 1 0 548822930 52359168 11414 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12783 11414 603 41 0 12742 0
vsize: 51132
[startup+450.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6988
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 11816 0 0 0 44955 48 0 0 25 0 1 0 548822930 52621312 11484 4294967295 134512640 134672761 3221224544 3221223648 134560399 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12847 11484 603 41 0 12806 0
vsize: 51388
[startup+460.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6988
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 11929 0 0 0 45955 49 0 0 25 0 1 0 548822930 53018624 11597 4294967295 134512640 134672761 3221224544 3221223648 134559866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12944 11597 603 41 0 12903 0
vsize: 51776
[startup+470.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6988
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 12002 0 0 0 46954 49 0 0 25 0 1 0 548822930 53411840 11670 4294967295 134512640 134672761 3221224544 3221223688 134560555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13040 11670 603 41 0 12999 0
vsize: 52160
[startup+480.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6988
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 12067 0 0 0 47954 50 0 0 25 0 1 0 548822930 53673984 11735 4294967295 134512640 134672761 3221224544 3221223696 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13104 11735 603 41 0 13063 0
vsize: 52416
[startup+490.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6988
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 12168 0 0 0 48954 51 0 0 25 0 1 0 548822930 54071296 11836 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13201 11836 603 41 0 13160 0
vsize: 52804
[startup+500.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6988
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 12268 0 0 0 49954 51 0 0 25 0 1 0 548822930 54472704 11936 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13299 11936 603 41 0 13258 0
vsize: 53196
[startup+510.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6990
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 12341 0 0 0 50953 52 0 0 25 0 1 0 548822930 54738944 12009 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13364 12009 603 41 0 13323 0
vsize: 53456
[startup+520.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6990
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 12428 0 0 0 51952 52 0 0 25 0 1 0 548822930 55140352 12096 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13462 12096 603 41 0 13421 0
vsize: 53848
[startup+530.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6990
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 12524 0 0 0 52951 53 0 0 25 0 1 0 548822930 55525376 12192 4294967295 134512640 134672761 3221224544 3221223688 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13556 12192 603 41 0 13515 0
vsize: 54224
[startup+540.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6990
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 12602 0 0 0 53951 54 0 0 25 0 1 0 548822930 55783424 12270 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13619 12270 603 41 0 13578 0
vsize: 54476
[startup+550.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6990
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 12682 0 0 0 54951 54 0 0 25 0 1 0 548822930 56164352 12350 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13712 12350 603 41 0 13671 0
vsize: 54848
[startup+560.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6990
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 12760 0 0 0 55951 54 0 0 25 0 1 0 548822930 56418304 12428 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13774 12428 603 41 0 13733 0
vsize: 55096
[startup+570.017 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 7043
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 12837 0 0 0 56945 60 0 0 25 0 1 0 548822930 56811520 12505 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13870 12505 603 41 0 13829 0
vsize: 55480
[startup+580.017 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 7043
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 12922 0 0 0 57944 61 0 0 25 0 1 0 548822930 57077760 12590 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13935 12590 603 41 0 13894 0
vsize: 55740
[startup+590.017 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 7043
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 12985 0 0 0 58944 61 0 0 25 0 1 0 548822930 57339904 12653 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13999 12653 603 41 0 13958 0
vsize: 55996
[startup+600.016 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 7043
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13050 0 0 0 59943 62 0 0 25 0 1 0 548822930 57610240 12718 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14065 12718 603 41 0 14024 0
vsize: 56260
[startup+610.017 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 7043
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13116 0 0 0 60943 63 0 0 25 0 1 0 548822930 57876480 12784 4294967295 134512640 134672761 3221224544 3221223680 134560647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14130 12784 603 41 0 14089 0
vsize: 56520
[startup+620.017 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 7043
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13196 0 0 0 61942 63 0 0 25 0 1 0 548822930 58273792 12864 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14227 12864 603 41 0 14186 0
vsize: 56908
[startup+630.018 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 7043
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13283 0 0 0 62942 65 0 0 25 0 1 0 548822930 58531840 12951 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14290 12951 603 41 0 14249 0
vsize: 57160
[startup+640.018 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 7045
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13370 0 0 0 63941 66 0 0 25 0 1 0 548822930 58920960 13038 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14385 13038 603 41 0 14344 0
vsize: 57540
[startup+650.017 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 7045
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13465 0 0 0 64940 67 0 0 25 0 1 0 548822930 59314176 13133 4294967295 134512640 134672761 3221224544 3221223648 134559937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14481 13133 603 41 0 14440 0
vsize: 57924
[startup+660.017 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 7045
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13561 0 0 0 65939 68 0 0 25 0 1 0 548822930 59699200 13229 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14575 13229 603 41 0 14534 0
vsize: 58300
[startup+670.017 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 7045
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13636 0 0 0 66938 69 0 0 25 0 1 0 548822930 59961344 13304 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14639 13304 603 41 0 14598 0
vsize: 58556
[startup+680.017 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 7045
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13636 0 0 0 67938 69 0 0 25 0 1 0 548822930 59961344 13304 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14639 13304 603 41 0 14598 0
vsize: 58556
[startup+690.017 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 7045
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13636 0 0 0 68938 70 0 0 25 0 1 0 548822930 59961344 13304 4294967295 134512640 134672761 3221224544 3221223648 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14639 13304 603 41 0 14598 0
vsize: 58556
[startup+700.016 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 7045
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13636 0 0 0 69937 70 0 0 25 0 1 0 548822930 59961344 13304 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14639 13304 603 41 0 14598 0
vsize: 58556
[startup+710.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7045
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13636 0 0 0 70937 70 0 0 25 0 1 0 548822930 59961344 13304 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14639 13304 603 41 0 14598 0
vsize: 58556
[startup+720.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7045
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13636 0 0 0 71937 70 0 0 25 0 1 0 548822930 59961344 13304 4294967295 134512640 134672761 3221224544 3221223680 134560703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14639 13304 603 41 0 14598 0
vsize: 58556
[startup+730.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7045
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13636 0 0 0 72937 71 0 0 25 0 1 0 548822930 59961344 13304 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14639 13304 603 41 0 14598 0
vsize: 58556
[startup+740.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7045
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13636 0 0 0 73936 71 0 0 25 0 1 0 548822930 59961344 13304 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14639 13304 603 41 0 14598 0
vsize: 58556
[startup+750.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7045
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13636 0 0 0 74936 72 0 0 25 0 1 0 548822930 59961344 13304 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14639 13304 603 41 0 14598 0
vsize: 58556
[startup+760.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7045
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13637 0 0 0 75937 72 0 0 25 0 1 0 548822930 59961344 13305 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14639 13305 603 41 0 14598 0
vsize: 58556
[startup+770.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7045
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13637 0 0 0 76936 72 0 0 25 0 1 0 548822930 59961344 13305 4294967295 134512640 134672761 3221224544 3221223696 1074744304 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14639 13305 603 41 0 14598 0
vsize: 58556
[startup+780.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7045
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13638 0 0 0 77936 72 0 0 25 0 1 0 548822930 59961344 13306 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14639 13306 603 41 0 14598 0
vsize: 58556
[startup+790.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7045
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13638 0 0 0 78936 73 0 0 25 0 1 0 548822930 59961344 13306 4294967295 134512640 134672761 3221224544 3221223728 134559003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14639 13306 603 41 0 14598 0
vsize: 58556
[startup+800.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7045
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13638 0 0 0 79936 73 0 0 25 0 1 0 548822930 59961344 13306 4294967295 134512640 134672761 3221224544 3221223648 134559835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14639 13306 603 41 0 14598 0
vsize: 58556
[startup+810.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7047
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13638 0 0 0 80935 74 0 0 25 0 1 0 548822930 59961344 13306 4294967295 134512640 134672761 3221224544 3221223648 134560051 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14639 13306 603 41 0 14598 0
vsize: 58556
[startup+820.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7047
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13638 0 0 0 81935 74 0 0 25 0 1 0 548822930 59961344 13306 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14639 13306 603 41 0 14598 0
vsize: 58556
[startup+830.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7047
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13638 0 0 0 82935 75 0 0 25 0 1 0 548822930 59961344 13306 4294967295 134512640 134672761 3221224544 3221223648 134559937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14639 13306 603 41 0 14598 0
vsize: 58556
[startup+840.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7047
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13638 0 0 0 83934 75 0 0 25 0 1 0 548822930 59961344 13306 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14639 13306 603 41 0 14598 0
vsize: 58556
[startup+850.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7047
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13638 0 0 0 84934 75 0 0 25 0 1 0 548822930 59961344 13306 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14639 13306 603 41 0 14598 0
vsize: 58556
[startup+860.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7047
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13638 0 0 0 85934 76 0 0 25 0 1 0 548822930 59961344 13306 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14639 13306 603 41 0 14598 0
vsize: 58556
[startup+870.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7047
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13638 0 0 0 86934 76 0 0 25 0 1 0 548822930 59961344 13306 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14639 13306 603 41 0 14598 0
vsize: 58556
[startup+880.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7047
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13646 0 0 0 87933 77 0 0 25 0 1 0 548822930 60149760 13314 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14685 13314 603 41 0 14644 0
vsize: 58740
[startup+890.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7049
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13646 0 0 0 88933 78 0 0 25 0 1 0 548822930 60149760 13314 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14685 13314 603 41 0 14644 0
vsize: 58740
[startup+900.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7049
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13646 0 0 0 89932 78 0 0 25 0 1 0 548822930 60149760 13314 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14685 13314 603 41 0 14644 0
vsize: 58740
[startup+910.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7049
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13646 0 0 0 90932 79 0 0 25 0 1 0 548822930 60149760 13314 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14685 13314 603 41 0 14644 0
vsize: 58740
[startup+920.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7049
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13646 0 0 0 91932 79 0 0 25 0 1 0 548822930 60149760 13314 4294967295 134512640 134672761 3221224544 3221223648 134560154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14685 13314 603 41 0 14644 0
vsize: 58740
[startup+930.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7049
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13646 0 0 0 92932 79 0 0 25 0 1 0 548822930 60149760 13314 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14685 13314 603 41 0 14644 0
vsize: 58740
[startup+940.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7049
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13646 0 0 0 93932 79 0 0 25 0 1 0 548822930 60149760 13314 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14685 13314 603 41 0 14644 0
vsize: 58740
[startup+950.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7049
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13655 0 0 0 94931 80 0 0 25 0 1 0 548822930 60149760 13323 4294967295 134512640 134672761 3221224544 3221223712 134561264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14685 13323 603 41 0 14644 0
vsize: 58740
[startup+960.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7049
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13665 0 0 0 95931 80 0 0 25 0 1 0 548822930 60149760 13333 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14685 13333 603 41 0 14644 0
vsize: 58740
[startup+970.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7049
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13665 0 0 0 96931 81 0 0 25 0 1 0 548822930 60149760 13333 4294967295 134512640 134672761 3221224544 3221223648 134554910 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14685 13333 603 41 0 14644 0
vsize: 58740
[startup+980.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7049
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13666 0 0 0 97931 81 0 0 25 0 1 0 548822930 60149760 13334 4294967295 134512640 134672761 3221224544 3221223680 134560585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14685 13334 603 41 0 14644 0
vsize: 58740
[startup+990.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7049
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13677 0 0 0 98931 81 0 0 25 0 1 0 548822930 60346368 13345 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14733 13345 603 41 0 14692 0
vsize: 58932
[startup+1000.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7049
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13678 0 0 0 99932 81 0 0 25 0 1 0 548822930 60346368 13346 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14733 13346 603 41 0 14692 0
vsize: 58932
[startup+1010.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7049
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13678 0 0 0 100932 81 0 0 25 0 1 0 548822930 60346368 13346 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14733 13346 603 41 0 14692 0
vsize: 58932
[startup+1020.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7049
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13679 0 0 0 101932 81 0 0 25 0 1 0 548822930 60346368 13347 4294967295 134512640 134672761 3221224544 3221223696 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14733 13347 603 41 0 14692 0
vsize: 58932
[startup+1030.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7049
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13679 0 0 0 102932 81 0 0 25 0 1 0 548822930 60346368 13347 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14733 13347 603 41 0 14692 0
vsize: 58932
[startup+1040.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7049
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13679 0 0 0 103932 81 0 0 25 0 1 0 548822930 60346368 13347 4294967295 134512640 134672761 3221224544 3221223692 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14733 13347 603 41 0 14692 0
vsize: 58932
[startup+1050.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7049
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13679 0 0 0 104932 81 0 0 25 0 1 0 548822930 60346368 13347 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14733 13347 603 41 0 14692 0
vsize: 58932
[startup+1060.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7049
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13679 0 0 0 105932 81 0 0 25 0 1 0 548822930 60346368 13347 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14733 13347 603 41 0 14692 0
vsize: 58932
[startup+1070.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7049
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13680 0 0 0 106932 81 0 0 25 0 1 0 548822930 60346368 13348 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14733 13348 603 41 0 14692 0
vsize: 58932
[startup+1080.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7049
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13682 0 0 0 107933 81 0 0 25 0 1 0 548822930 60346368 13350 4294967295 134512640 134672761 3221224544 3221222384 134597195 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14733 13350 603 41 0 14692 0
vsize: 58932
[startup+1090.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7049
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13682 0 0 0 108933 81 0 0 25 0 1 0 548822930 60346368 13350 4294967295 134512640 134672761 3221224544 3221223712 134561226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14733 13350 603 41 0 14692 0
vsize: 58932
[startup+1100.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7049
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13682 0 0 0 109933 81 0 0 25 0 1 0 548822930 60346368 13350 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14733 13350 603 41 0 14692 0
vsize: 58932
[startup+1110.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7051
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13691 0 0 0 110933 81 0 0 25 0 1 0 548822930 60346368 13359 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14733 13359 603 41 0 14692 0
vsize: 58932
[startup+1120.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7051
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13691 0 0 0 111933 81 0 0 25 0 1 0 548822930 60346368 13359 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14733 13359 603 41 0 14692 0
vsize: 58932
[startup+1130.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7051
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13697 0 0 0 112933 81 0 0 25 0 1 0 548822930 60346368 13365 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14733 13365 603 41 0 14692 0
vsize: 58932
[startup+1140.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7051
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13697 0 0 0 113933 81 0 0 25 0 1 0 548822930 60346368 13365 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14733 13365 603 41 0 14692 0
vsize: 58932
[startup+1150.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7051
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13698 0 0 0 114933 82 0 0 25 0 1 0 548822930 60346368 13366 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14733 13366 603 41 0 14692 0
vsize: 58932
[startup+1160.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7051
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13713 0 0 0 115933 82 0 0 25 0 1 0 548822930 60346368 13381 4294967295 134512640 134672761 3221224544 3221222128 134544472 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14733 13381 603 41 0 14692 0
vsize: 58932
[startup+1170.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7051
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13760 0 0 0 116933 82 0 0 25 0 1 0 548822930 60678144 13428 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14814 13428 603 41 0 14773 0
vsize: 59256
[startup+1180.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7051
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13832 0 0 0 117933 82 0 0 25 0 1 0 548822930 61038592 13500 4294967295 134512640 134672761 3221224544 3221223844 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14902 13500 603 41 0 14861 0
vsize: 59608
[startup+1190.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7051
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13906 0 0 0 118933 83 0 0 25 0 1 0 548822930 61267968 13574 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14958 13574 603 41 0 14917 0
vsize: 59832
[startup+1200.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 7051
Raw data (stat): 6986 (minisat+) R 6985 20838 20837 0 -1 0 13929 0 0 0 119933 83 0 0 25 0 1 0 548822930 61370368 13597 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14983 13597 603 41 0 14942 0
vsize: 59932
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.91 1/55 7051
Raw data (stat): 6986 (minisat+) Z 6985 20838 20837 0 -1 12 13932 0 0 0 119933 85 0 0 25 0 1 0 548822930 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.05
CPU time (s): 1200.2
CPU user time (s): 1199.34
CPU system time (s): 0.857869
CPU usage (%): 100.012
Max. virtual memory (Kb): 59932
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####