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-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-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.02084
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 18004

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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:        676160 kB
Buffers:         30824 kB
Cached:         305436 kB
SwapCached:          0 kB
Active:          78384 kB
Inactive:       260816 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        675908 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6952 kB
Slab:            13496 kB
Committed_AS:    63560 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 13:25:51 (client local time) WITH STATUS 10 IN 1200.24 SECONDS
stats: 18719 7 1200.24 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 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.98 0.91 2/54 30787
Raw data (stat): 30787 (runsolver) R 30786 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 473519013 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.9998 s]
Raw data (loadavg): 0.93 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 7919 0 0 0 981 17 0 0 25 0 1 0 473519013 36589568 7587 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8933 7587 603 41 0 8892 0
vsize: 35732
[startup+20.0007 s]
Raw data (loadavg): 0.95 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 8148 0 0 0 1980 18 0 0 25 0 1 0 473519013 37511168 7816 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9158 7816 603 41 0 9117 0
vsize: 36632
[startup+30.0019 s]
Raw data (loadavg): 0.95 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 8246 0 0 0 2980 19 0 0 25 0 1 0 473519013 37834752 7914 4294967295 134512640 134672761 3221224544 3221223728 134559590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9237 7914 603 41 0 9196 0
vsize: 36948
[startup+40.0022 s]
Raw data (loadavg): 0.96 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 8327 0 0 0 3979 20 0 0 25 0 1 0 473519013 38154240 7995 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9315 7995 603 41 0 9274 0
vsize: 37260
[startup+50.003 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 8423 0 0 0 4979 20 0 0 25 0 1 0 473519013 38555648 8091 4294967295 134512640 134672761 3221224544 3221223680 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9413 8091 603 41 0 9372 0
vsize: 37652
[startup+60.0033 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 8576 0 0 0 5978 21 0 0 25 0 1 0 473519013 39264256 8244 4294967295 134512640 134672761 3221224544 3221223692 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9586 8244 603 41 0 9545 0
vsize: 38344
[startup+70.0034 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 8729 0 0 0 6977 22 0 0 25 0 1 0 473519013 39800832 8397 4294967295 134512640 134672761 3221224544 3221223712 134561151 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.0032 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 8880 0 0 0 7977 22 0 0 25 0 1 0 473519013 40476672 8548 4294967295 134512640 134672761 3221224544 3221223680 134565092 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.0043 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 8960 0 0 0 8977 22 0 0 25 0 1 0 473519013 40747008 8628 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9948 8628 603 41 0 9907 0
vsize: 39792
[startup+100.004 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 9095 0 0 0 9977 23 0 0 25 0 1 0 473519013 41287680 8763 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10080 8763 603 41 0 10039 0
vsize: 40320
[startup+110.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 9193 0 0 0 10977 23 0 0 25 0 1 0 473519013 41807872 8861 4294967295 134512640 134672761 3221224544 3221223712 134561121 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.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 9240 0 0 0 11977 23 0 0 25 0 1 0 473519013 41947136 8908 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10241 8908 603 41 0 10200 0
vsize: 40964
[startup+130.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 9289 0 0 0 12977 23 0 0 25 0 1 0 473519013 42192896 8957 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10301 8957 603 41 0 10260 0
vsize: 41204
[startup+140.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 9368 0 0 0 13977 23 0 0 25 0 1 0 473519013 42463232 9036 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10367 9036 603 41 0 10326 0
vsize: 41468
[startup+150.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 9452 0 0 0 14976 24 0 0 25 0 1 0 473519013 42864640 9120 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10465 9120 603 41 0 10424 0
vsize: 41860
[startup+160.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 9535 0 0 0 15976 24 0 0 25 0 1 0 473519013 43134976 9203 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10531 9203 603 41 0 10490 0
vsize: 42124
[startup+170.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 9688 0 0 0 16976 25 0 0 25 0 1 0 473519013 43810816 9356 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10696 9356 603 41 0 10655 0
vsize: 42784
[startup+180.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 9771 0 0 0 17976 25 0 0 25 0 1 0 473519013 44077056 9439 4294967295 134512640 134672761 3221224544 3221223744 134557895 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.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 9818 0 0 0 18976 25 0 0 25 0 1 0 473519013 44343296 9486 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10826 9486 603 41 0 10785 0
vsize: 43304
[startup+200.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 9910 0 0 0 19976 25 0 0 25 0 1 0 473519013 44744704 9578 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10924 9578 603 41 0 10883 0
vsize: 43696
[startup+210.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 10006 0 0 0 20975 26 0 0 25 0 1 0 473519013 45010944 9674 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10989 9674 603 41 0 10948 0
vsize: 43956
[startup+220.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 10083 0 0 0 21975 26 0 0 25 0 1 0 473519013 45375488 9751 4294967295 134512640 134672761 3221224544 3221223712 134560839 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.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 10146 0 0 0 22975 27 0 0 25 0 1 0 473519013 45641728 9814 4294967295 134512640 134672761 3221224544 3221223744 134557800 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11143 9814 603 41 0 11102 0
vsize: 44572
[startup+240.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 10215 0 0 0 23975 27 0 0 25 0 1 0 473519013 45912064 9883 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11209 9883 603 41 0 11168 0
vsize: 44836
[startup+250.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 10292 0 0 0 24976 27 0 0 25 0 1 0 473519013 46174208 9960 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11273 9960 603 41 0 11232 0
vsize: 45092
[startup+260.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 10363 0 0 0 25975 27 0 0 25 0 1 0 473519013 46444544 10031 4294967295 134512640 134672761 3221224544 3221223648 134560051 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11339 10031 603 41 0 11298 0
vsize: 45356
[startup+270.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 10441 0 0 0 26975 28 0 0 25 0 1 0 473519013 46841856 10109 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11436 10109 603 41 0 11395 0
vsize: 45744
[startup+280.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 10494 0 0 0 27975 28 0 0 25 0 1 0 473519013 46977024 10162 4294967295 134512640 134672761 3221224544 3221223744 134557849 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.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 10564 0 0 0 28975 28 0 0 25 0 1 0 473519013 47243264 10232 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11534 10232 603 41 0 11493 0
vsize: 46136
[startup+300.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 10658 0 0 0 29975 28 0 0 25 0 1 0 473519013 47648768 10326 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11633 10326 603 41 0 11592 0
vsize: 46532
[startup+310.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 10744 0 0 0 30975 28 0 0 25 0 1 0 473519013 48041984 10412 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11729 10412 603 41 0 11688 0
vsize: 46916
[startup+320.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 10827 0 0 0 31975 29 0 0 25 0 1 0 473519013 48312320 10495 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11795 10495 603 41 0 11754 0
vsize: 47180
[startup+330.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 10928 0 0 0 32975 29 0 0 25 0 1 0 473519013 48836608 10596 4294967295 134512640 134672761 3221224544 3221223728 134558423 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11923 10596 603 41 0 11882 0
vsize: 47692
[startup+340.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 11004 0 0 0 33975 29 0 0 25 0 1 0 473519013 49106944 10672 4294967295 134512640 134672761 3221224544 3221223688 134560555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11989 10672 603 41 0 11948 0
vsize: 47956
[startup+350.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 11066 0 0 0 34975 29 0 0 25 0 1 0 473519013 49635328 10734 4294967295 134512640 134672761 3221224544 3221223648 134560361 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12118 10734 603 41 0 12077 0
vsize: 48472
[startup+360.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 11115 0 0 0 35975 29 0 0 25 0 1 0 473519013 49766400 10783 4294967295 134512640 134672761 3221224544 3221223728 134558341 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12150 10783 603 41 0 12109 0
vsize: 48600
[startup+370.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 11168 0 0 0 36975 30 0 0 25 0 1 0 473519013 50024448 10836 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12213 10836 603 41 0 12172 0
vsize: 48852
[startup+380.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 11222 0 0 0 37974 30 0 0 25 0 1 0 473519013 50286592 10890 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12277 10890 603 41 0 12236 0
vsize: 49108
[startup+390.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 11322 0 0 0 38974 31 0 0 25 0 1 0 473519013 50692096 10990 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12376 10990 603 41 0 12335 0
vsize: 49504
[startup+400.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 11471 0 0 0 39974 32 0 0 25 0 1 0 473519013 51228672 11139 4294967295 134512640 134672761 3221224544 3221223728 134559116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12507 11139 603 41 0 12466 0
vsize: 50028
[startup+410.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 11552 0 0 0 40974 32 0 0 25 0 1 0 473519013 51494912 11220 4294967295 134512640 134672761 3221224544 3221223692 1074733101 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12572 11220 603 41 0 12531 0
vsize: 50288
[startup+420.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 11614 0 0 0 41974 32 0 0 25 0 1 0 473519013 51757056 11282 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12636 11282 603 41 0 12595 0
vsize: 50544
[startup+430.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 11679 0 0 0 42974 32 0 0 25 0 1 0 473519013 52019200 11347 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12700 11347 603 41 0 12659 0
vsize: 50800
[startup+440.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 11726 0 0 0 43973 33 0 0 25 0 1 0 473519013 52224000 11394 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12750 11394 603 41 0 12709 0
vsize: 51000
[startup+450.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 11796 0 0 0 44973 33 0 0 25 0 1 0 473519013 52490240 11464 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12815 11464 603 41 0 12774 0
vsize: 51260
[startup+460.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 11888 0 0 0 45973 34 0 0 25 0 1 0 473519013 52887552 11556 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12912 11556 603 41 0 12871 0
vsize: 51648
[startup+470.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 11981 0 0 0 46973 34 0 0 25 0 1 0 473519013 53284864 11649 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13009 11649 603 41 0 12968 0
vsize: 52036
[startup+480.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 12036 0 0 0 47973 34 0 0 25 0 1 0 473519013 53542912 11704 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13072 11704 603 41 0 13031 0
vsize: 52288
[startup+490.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 12135 0 0 0 48973 34 0 0 25 0 1 0 473519013 53940224 11803 4294967295 134512640 134672761 3221224544 3221223648 134560237 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13169 11803 603 41 0 13128 0
vsize: 52676
[startup+500.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 12226 0 0 0 49973 35 0 0 25 0 1 0 473519013 54337536 11894 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13266 11894 603 41 0 13225 0
vsize: 53064
[startup+510.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 12315 0 0 0 50972 35 0 0 25 0 1 0 473519013 54603776 11983 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13331 11983 603 41 0 13290 0
vsize: 53324
[startup+520.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 12383 0 0 0 51972 35 0 0 25 0 1 0 473519013 54874112 12051 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13397 12051 603 41 0 13356 0
vsize: 53588
[startup+530.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 12483 0 0 0 52972 36 0 0 25 0 1 0 473519013 55267328 12151 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13493 12151 603 41 0 13452 0
vsize: 53972
[startup+540.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 12569 0 0 0 53972 36 0 0 25 0 1 0 473519013 55652352 12237 4294967295 134512640 134672761 3221224544 3221223648 134560303 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13587 12237 603 41 0 13546 0
vsize: 54348
[startup+550.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 12654 0 0 0 54972 36 0 0 25 0 1 0 473519013 56037376 12322 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13681 12322 603 41 0 13640 0
vsize: 54724
[startup+560.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 12736 0 0 0 55972 36 0 0 25 0 1 0 473519013 56291328 12404 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13743 12404 603 41 0 13702 0
vsize: 54972
[startup+570.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 12808 0 0 0 56972 37 0 0 25 0 1 0 473519013 56684544 12476 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13839 12476 603 41 0 13798 0
vsize: 55356
[startup+580.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 12887 0 0 0 57972 37 0 0 25 0 1 0 473519013 56946688 12555 4294967295 134512640 134672761 3221224544 3221223680 134560611 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13903 12555 603 41 0 13862 0
vsize: 55612
[startup+590.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 12962 0 0 0 58972 37 0 0 25 0 1 0 473519013 57208832 12630 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13967 12630 603 41 0 13926 0
vsize: 55868
[startup+600.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13024 0 0 0 59972 38 0 0 25 0 1 0 473519013 57475072 12692 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14032 12692 603 41 0 13991 0
vsize: 56128
[startup+610.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13090 0 0 0 60972 38 0 0 25 0 1 0 473519013 57741312 12758 4294967295 134512640 134672761 3221224544 3221223728 134559604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14097 12758 603 41 0 14056 0
vsize: 56388
[startup+620.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13154 0 0 0 61971 39 0 0 25 0 1 0 473519013 58003456 12822 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14161 12822 603 41 0 14120 0
vsize: 56644
[startup+630.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13258 0 0 0 62971 39 0 0 25 0 1 0 473519013 58531840 12926 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14290 12926 603 41 0 14249 0
vsize: 57160
[startup+640.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13337 0 0 0 63971 39 0 0 25 0 1 0 473519013 58793984 13005 4294967295 134512640 134672761 3221224544 3221223680 134565110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14354 13005 603 41 0 14313 0
vsize: 57416
[startup+650.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13423 0 0 0 64971 39 0 0 25 0 1 0 473519013 59183104 13091 4294967295 134512640 134672761 3221224544 3221223680 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14449 13091 603 41 0 14408 0
vsize: 57796
[startup+660.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13519 0 0 0 65970 40 0 0 25 0 1 0 473519013 59572224 13187 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14544 13187 603 41 0 14503 0
vsize: 58176
[startup+670.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13609 0 0 0 66970 40 0 0 25 0 1 0 473519013 59961344 13277 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14639 13277 603 41 0 14598 0
vsize: 58556
[startup+680.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13636 0 0 0 67970 41 0 0 25 0 1 0 473519013 59961344 13304 4294967295 134512640 134672761 3221224544 3221223744 134557811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14639 13304 603 41 0 14598 0
vsize: 58556
[startup+690.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13636 0 0 0 68970 41 0 0 25 0 1 0 473519013 59961344 13304 4294967295 134512640 134672761 3221224544 3221223648 134559835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14639 13304 603 41 0 14598 0
vsize: 58556
[startup+700.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13636 0 0 0 69970 41 0 0 25 0 1 0 473519013 59961344 13304 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14639 13304 603 41 0 14598 0
vsize: 58556
[startup+710.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13636 0 0 0 70970 41 0 0 25 0 1 0 473519013 59961344 13304 4294967295 134512640 134672761 3221224544 3221223728 134559045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14639 13304 603 41 0 14598 0
vsize: 58556
[startup+720.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13636 0 0 0 71971 41 0 0 25 0 1 0 473519013 59961344 13304 4294967295 134512640 134672761 3221224544 3221223712 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14639 13304 603 41 0 14598 0
vsize: 58556
[startup+730.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13636 0 0 0 72971 41 0 0 25 0 1 0 473519013 59961344 13304 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14639 13304 603 41 0 14598 0
vsize: 58556
[startup+740.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13636 0 0 0 73971 41 0 0 25 0 1 0 473519013 59961344 13304 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14639 13304 603 41 0 14598 0
vsize: 58556
[startup+750.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13636 0 0 0 74971 41 0 0 25 0 1 0 473519013 59961344 13304 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14639 13304 603 41 0 14598 0
vsize: 58556
[startup+760.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13636 0 0 0 75971 41 0 0 25 0 1 0 473519013 59961344 13304 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14639 13304 603 41 0 14598 0
vsize: 58556
[startup+770.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13637 0 0 0 76971 41 0 0 25 0 1 0 473519013 59961344 13305 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14639 13305 603 41 0 14598 0
vsize: 58556
[startup+780.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13638 0 0 0 77971 41 0 0 25 0 1 0 473519013 59961344 13306 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14639 13306 603 41 0 14598 0
vsize: 58556
[startup+790.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13638 0 0 0 78971 41 0 0 25 0 1 0 473519013 59961344 13306 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14639 13306 603 41 0 14598 0
vsize: 58556
[startup+800.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13638 0 0 0 79972 41 0 0 25 0 1 0 473519013 59961344 13306 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14639 13306 603 41 0 14598 0
vsize: 58556
[startup+810.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13638 0 0 0 80972 41 0 0 25 0 1 0 473519013 59961344 13306 4294967295 134512640 134672761 3221224544 3221223648 134560160 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14639 13306 603 41 0 14598 0
vsize: 58556
[startup+820.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13638 0 0 0 81972 41 0 0 25 0 1 0 473519013 59961344 13306 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14639 13306 603 41 0 14598 0
vsize: 58556
[startup+830.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13638 0 0 0 82972 41 0 0 25 0 1 0 473519013 59961344 13306 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14639 13306 603 41 0 14598 0
vsize: 58556
[startup+840.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13638 0 0 0 83972 41 0 0 25 0 1 0 473519013 59961344 13306 4294967295 134512640 134672761 3221224544 3221223728 134559324 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14639 13306 603 41 0 14598 0
vsize: 58556
[startup+850.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13638 0 0 0 84973 41 0 0 25 0 1 0 473519013 59961344 13306 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14639 13306 603 41 0 14598 0
vsize: 58556
[startup+860.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13638 0 0 0 85973 41 0 0 25 0 1 0 473519013 59961344 13306 4294967295 134512640 134672761 3221224544 3221223728 134559613 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14639 13306 603 41 0 14598 0
vsize: 58556
[startup+870.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13638 0 0 0 86973 41 0 0 25 0 1 0 473519013 59961344 13306 4294967295 134512640 134672761 3221224544 3221223680 134560579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14639 13306 603 41 0 14598 0
vsize: 58556
[startup+880.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13646 0 0 0 87973 41 0 0 25 0 1 0 473519013 60149760 13314 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14685 13314 603 41 0 14644 0
vsize: 58740
[startup+890.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13646 0 0 0 88973 41 0 0 25 0 1 0 473519013 60149760 13314 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14685 13314 603 41 0 14644 0
vsize: 58740
[startup+900.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13646 0 0 0 89973 41 0 0 25 0 1 0 473519013 60149760 13314 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14685 13314 603 41 0 14644 0
vsize: 58740
[startup+910.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13646 0 0 0 90973 41 0 0 25 0 1 0 473519013 60149760 13314 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14685 13314 603 41 0 14644 0
vsize: 58740
[startup+920.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13646 0 0 0 91974 41 0 0 25 0 1 0 473519013 60149760 13314 4294967295 134512640 134672761 3221224544 3221223648 134560520 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14685 13314 603 41 0 14644 0
vsize: 58740
[startup+930.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13646 0 0 0 92974 41 0 0 25 0 1 0 473519013 60149760 13314 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14685 13314 603 41 0 14644 0
vsize: 58740
[startup+940.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13646 0 0 0 93974 41 0 0 25 0 1 0 473519013 60149760 13314 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14685 13314 603 41 0 14644 0
vsize: 58740
[startup+950.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13646 0 0 0 94974 41 0 0 25 0 1 0 473519013 60149760 13314 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14685 13314 603 41 0 14644 0
vsize: 58740
[startup+960.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13665 0 0 0 95974 41 0 0 25 0 1 0 473519013 60149760 13333 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14685 13333 603 41 0 14644 0
vsize: 58740
[startup+970.022 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13665 0 0 0 96974 41 0 0 25 0 1 0 473519013 60149760 13333 4294967295 134512640 134672761 3221224544 3221223728 134559356 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14685 13333 603 41 0 14644 0
vsize: 58740
[startup+980.022 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13665 0 0 0 97974 41 0 0 25 0 1 0 473519013 60149760 13333 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14685 13333 603 41 0 14644 0
vsize: 58740
[startup+990.022 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13676 0 0 0 98974 42 0 0 25 0 1 0 473519013 60346368 13344 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14733 13344 603 41 0 14692 0
vsize: 58932
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13677 0 0 0 99974 42 0 0 25 0 1 0 473519013 60346368 13345 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14733 13345 603 41 0 14692 0
vsize: 58932
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13678 0 0 0 100975 42 0 0 25 0 1 0 473519013 60346368 13346 4294967295 134512640 134672761 3221224544 3221223712 134560830 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): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13679 0 0 0 101975 42 0 0 25 0 1 0 473519013 60346368 13347 4294967295 134512640 134672761 3221224544 3221223712 134560898 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): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13679 0 0 0 102975 42 0 0 25 0 1 0 473519013 60346368 13347 4294967295 134512640 134672761 3221224544 3221223648 134560326 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): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13679 0 0 0 103975 42 0 0 25 0 1 0 473519013 60346368 13347 4294967295 134512640 134672761 3221224544 3221223680 134560588 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): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13679 0 0 0 104975 42 0 0 25 0 1 0 473519013 60346368 13347 4294967295 134512640 134672761 3221224544 3221223712 134561198 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): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13679 0 0 0 105976 42 0 0 25 0 1 0 473519013 60346368 13347 4294967295 134512640 134672761 3221224544 3221223680 134560590 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): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13680 0 0 0 106976 42 0 0 25 0 1 0 473519013 60346368 13348 4294967295 134512640 134672761 3221224544 3221223648 134554910 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): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13681 0 0 0 107976 42 0 0 25 0 1 0 473519013 60346368 13349 4294967295 134512640 134672761 3221224544 3221223688 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14733 13349 603 41 0 14692 0
vsize: 58932
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13682 0 0 0 108976 42 0 0 25 0 1 0 473519013 60346368 13350 4294967295 134512640 134672761 3221224544 3221223680 134560625 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.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13682 0 0 0 109976 42 0 0 25 0 1 0 473519013 60346368 13350 4294967295 134512640 134672761 3221224544 3221223712 134560869 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): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13691 0 0 0 110976 42 0 0 25 0 1 0 473519013 60346368 13359 4294967295 134512640 134672761 3221224544 3221223744 134557906 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.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13691 0 0 0 111976 42 0 0 25 0 1 0 473519013 60346368 13359 4294967295 134512640 134672761 3221224544 3221223680 134560588 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.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13697 0 0 0 112977 42 0 0 25 0 1 0 473519013 60346368 13365 4294967295 134512640 134672761 3221224544 3221223712 134560830 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.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13697 0 0 0 113977 42 0 0 25 0 1 0 473519013 60346368 13365 4294967295 134512640 134672761 3221224544 3221222816 134597188 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.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13697 0 0 0 114977 42 0 0 25 0 1 0 473519013 60346368 13365 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14733 13365 603 41 0 14692 0
vsize: 58932
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13703 0 0 0 115977 42 0 0 25 0 1 0 473519013 60346368 13371 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14733 13371 603 41 0 14692 0
vsize: 58932
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13760 0 0 0 116977 42 0 0 25 0 1 0 473519013 60678144 13428 4294967295 134512640 134672761 3221224544 3221223668 134566037 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.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13760 0 0 0 117977 43 0 0 25 0 1 0 473519013 60678144 13428 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14814 13428 603 41 0 14773 0
vsize: 59256
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13860 0 0 0 118977 43 0 0 25 0 1 0 473519013 61173760 13528 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14935 13528 603 41 0 14894 0
vsize: 59740
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 30787
Raw data (stat): 30787 (minisat+) R 30786 26667 26666 0 -1 0 13917 0 0 0 119977 43 0 0 25 0 1 0 473519013 61267968 13585 4294967295 134512640 134672761 3221224544 3221222264 1075349616 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14958 13585 603 41 0 14917 0
vsize: 59832
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.98 0.91 1/54 30787
Raw data (stat): 30787 (minisat+) Z 30786 26667 26666 0 -1 12 13920 0 0 0 119977 46 0 0 25 0 1 0 473519013 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.06
CPU time (s): 1200.24
CPU user time (s): 1199.77
CPU system time (s): 0.465929
CPU usage (%): 100.015
Max. virtual memory (Kb): 59832
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####