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/miplib2003/normalized-mps-v2-13-7-markshare1.opb
MD5SUM	6f06e375914e0285ec75de90ad627758
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	3712
Optimality of the best value was proved	NO
Number of terms in the objective function	120
Biggest coefficient in the objective function	524288
Number of bits for the biggest coefficient in the objective function	20
Sum of the numbers in the objective function	6291450
Number of bits of the sum of numbers in the objective function	23
Biggest number in a constraint	524288
Number of bits of the biggest number in a constraint	20
Biggest sum of numbers in a constraint	6291450
Number of bits of the biggest sum of numbers	23
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.1
Number of variables	170
Total number of constraints	56
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	50
Number of constraints which are nor clauses,nor cardinality constraints	6
Minimum length of a constraint	1
Maximum length of a constraint	70
Trace number 18700

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        650204 kB
Buffers:         21864 kB
Cached:         337116 kB
SwapCached:        536 kB
Active:          26272 kB
Inactive:       334864 kB
HighTotal:      131008 kB
HighFree:        20804 kB
LowTotal:       903652 kB
LowFree:        629400 kB
SwapTotal:     2097136 kB
SwapFree:      2095852 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5224 kB
Slab:            17600 kB
Committed_AS:    63560 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 16:22:22 (client local time) WITH STATUS 10 IN 1200.25 SECONDS
stats: 17640 7 1200.25 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 12 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ######
c   -- Clauses(.)/Splits(s): (none)
c ---[  10]---> BDD-cost:23437
c ---[   8]---> BDD-cost:28407
c ---[   6]---> BDD-cost:25972
c ---[   4]---> BDD-cost:24798
c ---[   2]---> BDD-cost:25031
c ---[   0]---> BDD-cost:24117
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  436749  1274733 |  145583       0        0     nan |  0.000 % |
c |       100 |  436749  1274733 |  160141     100     9403    94.0 |  0.012 % |
c ==============================================================================
c [1mFound solution: 862848[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 1464     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       102 |  440476  1283432 |  146825     102     9461    92.8 |  0.012 % |
c ==============================================================================
c [1mFound solution: 860928[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       105 |  440500  1283513 |  146833     105     9619    91.6 |  0.012 % |
c ==============================================================================
c [1mFound solution: 848640[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       106 |  440508  1283534 |  146836     106     9694    91.5 |  0.012 % |
c ==============================================================================
c [1mFound solution: 839296[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       109 |  440517  1283557 |  146839     109     9892    90.8 |  0.012 % |
c ==============================================================================
c [1mFound solution: 835328[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       112 |  440525  1283579 |  146841     112    10046    89.7 |  0.012 % |
c ==============================================================================
c [1mFound solution: 811776[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       115 |  440531  1283593 |  146843     115    10228    88.9 |  0.012 % |
c ==============================================================================
c [1mFound solution: 793344[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       138 |  440541  1283616 |  146847     138    11635    84.3 |  0.012 % |
c ==============================================================================
c [1mFound solution: 788224[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       193 |  440551  1283638 |  146850     193    14480    75.0 |  0.012 % |
c ==============================================================================
c [1mFound solution: 784256[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       198 |  440561  1283669 |  146853     198    14774    74.6 |  0.012 % |
c ==============================================================================
c [1mFound solution: 760704[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       199 |  440572  1283698 |  146857     199    14819    74.5 |  0.012 % |
c ==============================================================================
c [1mFound solution: 760064[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       222 |  440584  1283728 |  146861     222    15796    71.2 |  0.012 % |
c ==============================================================================
c [1mFound solution: 755840[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       271 |  440596  1283756 |  146865     271    18033    66.5 |  0.012 % |
c ==============================================================================
c [1mFound solution: 740864[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       330 |  440609  1283788 |  146869     330    20875    63.3 |  0.012 % |
c ==============================================================================
c [1mFound solution: 740224[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       388 |  440620  1283814 |  146873     388    23291    60.0 |  0.012 % |
c ==============================================================================
c [1mFound solution: 669184[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       392 |  440630  1283839 |  146876     392    23497    59.9 |  0.012 % |
c |       493 |  440630  1283839 |  161563     493    25965    52.7 |  0.022 % |
c |       645 |  440630  1283839 |  177719     645    38402    59.5 |  0.022 % |
c |       870 |  440630  1283839 |  195491     870    49510    56.9 |  0.022 % |
c |      1208 |  440630  1283839 |  215041    1208    64325    53.2 |  0.022 % |
c ==============================================================================
c [1mFound solution: 619392[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1350 |  440647  1283882 |  146882    1350    70758    52.4 |  0.022 % |
c |      1450 |  440647  1283882 |  161570    1450    75423    52.0 |  0.022 % |
c |      1600 |  440647  1283882 |  177727    1600    82144    51.3 |  0.022 % |
c |      1826 |  440647  1283882 |  195499    1826    92134    50.5 |  0.022 % |
c |      2164 |  440647  1283882 |  215049    2164   108591    50.2 |  0.022 % |
c ==============================================================================
c [1mFound solution: 616960[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2415 |  440661  1283918 |  146887    2415   120616    49.9 |  0.022 % |
c ==============================================================================
c [1mFound solution: 612992[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2449 |  440671  1283942 |  146890    2449   122229    49.9 |  0.022 % |
c ==============================================================================
c [1mFound solution: 600448[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2513 |  440686  1283977 |  146895    2513   125386    49.9 |  0.022 % |
c |      2613 |  440686  1283977 |  161584    2613   129646    49.6 |  0.024 % |
c ==============================================================================
c [1mFound solution: 594048[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2615 |  440697  1284002 |  146899    2615   129753    49.6 |  0.024 % |
c ==============================================================================
c [1mFound solution: 593792[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2659 |  440707  1284025 |  146902    2659   131977    49.6 |  0.024 % |
c |      2760 |  440707  1284025 |  161592    2760   136347    49.4 |  0.026 % |
c |      2911 |  440707  1284025 |  177751    2911   143046    49.1 |  0.026 % |
c ==============================================================================
c [1mFound solution: 576896[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3074 |  440718  1284052 |  146906    3074   150380    48.9 |  0.026 % |
c |      3175 |  440718  1284052 |  161596    3175   153785    48.4 |  0.026 % |
c ==============================================================================
c [1mFound solution: 576128[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3275 |  440725  1284069 |  146908    3275   158596    48.4 |  0.026 % |
c |      3377 |  440725  1284069 |  161598    3377   162887    48.2 |  0.027 % |
c |      3528 |  440725  1284069 |  177758    3528   168251    47.7 |  0.027 % |
c |      3754 |  440725  1284069 |  195534    3754   180561    48.1 |  0.027 % |
c ==============================================================================
c [1mFound solution: 573568[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3791 |  440733  1284088 |  146911    3791   181744    47.9 |  0.027 % |
c ==============================================================================
c [1mFound solution: 573312[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3880 |  440741  1284108 |  146913    3880   185737    47.9 |  0.027 % |
c |      3980 |  440741  1284108 |  161604    3980   190136    47.8 |  0.028 % |
c ==============================================================================
c [1mFound solution: 572288[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4008 |  440749  1284127 |  146916    4008   191213    47.7 |  0.028 % |
c |      4109 |  440749  1284127 |  161607    4109   195601    47.6 |  0.029 % |
c ==============================================================================
c [1mFound solution: 566400[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4172 |  440763  1284159 |  146921    4172   198808    47.7 |  0.029 % |
c ==============================================================================
c [1mFound solution: 566144[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4218 |  440773  1284182 |  146924    4218   200938    47.6 |  0.029 % |
c ==============================================================================
c [1mFound solution: 542848[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4228 |  440782  1284202 |  146927    4228   201373    47.6 |  0.029 % |
c |      4328 |  440782  1284202 |  161619    4328   205475    47.5 |  0.031 % |
c |      4478 |  440782  1284202 |  177781    4478   212196    47.4 |  0.031 % |
c ==============================================================================
c [1mFound solution: 534400[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4640 |  440791  1284222 |  146930    4640   219034    47.2 |  0.031 % |
c |      4741 |  440791  1284222 |  161623    4741   223846    47.2 |  0.031 % |
c |      4891 |  440791  1284222 |  177785    4891   231251    47.3 |  0.031 % |
c |      5116 |  440791  1284222 |  195563    5116   240547    47.0 |  0.031 % |
c |      5453 |  440791  1284222 |  215120    5453   255602    46.9 |  0.031 % |
c |      5959 |  440791  1284222 |  236632    5959   279577    46.9 |  0.031 % |
c |      6720 |  440791  1284222 |  260295    6720   314985    46.9 |  0.031 % |
c |      7859 |  440791  1284222 |  286325    7859   369091    47.0 |  0.031 % |
c ==============================================================================
c [1mFound solution: 531584[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8101 |  440799  1284241 |  146933    8101   380625    47.0 |  0.031 % |
c |      8203 |  440799  1284241 |  161626    8203   385228    47.0 |  0.032 % |
c ==============================================================================
c [1mFound solution: 509312[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8332 |  440811  1284271 |  146937    8332   391378    47.0 |  0.032 % |
c |      8432 |  440811  1284271 |  161630    8432   395334    46.9 |  0.033 % |
c ==============================================================================
c [1mFound solution: 418560[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8441 |  440817  1284284 |  146939    8441   395745    46.9 |  0.033 % |
c |      8541 |  440817  1284284 |  161632    8541   399910    46.8 |  0.033 % |
c ==============================================================================
c [1mFound solution: 411264[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8583 |  440828  1284309 |  146942    8583   401708    46.8 |  0.033 % |
c |      8683 |  440828  1284309 |  161636    8683   405325    46.7 |  0.034 % |
c |      8833 |  440828  1284309 |  177799    8833   412197    46.7 |  0.034 % |
c ==============================================================================
c [1mFound solution: 408064[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8934 |  440835  1284326 |  146945    8934   416333    46.6 |  0.034 % |
c ==============================================================================
c [1mFound solution: 406016[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8987 |  440844  1284347 |  146948    8987   418999    46.6 |  0.034 % |
c ==============================================================================
c [1mFound solution: 404608[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9069 |  440854  1284370 |  146951    9069   422941    46.6 |  0.034 % |
c |      9169 |  440854  1284370 |  161646    9169   427271    46.6 |  0.036 % |
c ==============================================================================
c [1mFound solution: 401664[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9240 |  440864  1284392 |  146954    9240   430660    46.6 |  0.036 % |
c |      9341 |  440864  1284392 |  161649    9341   435483    46.6 |  0.037 % |
c ==============================================================================
c [1mFound solution: 392064[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9444 |  440872  1284413 |  146957    9444   440094    46.6 |  0.037 % |
c ==============================================================================
c [1mFound solution: 386176[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9491 |  440877  1284428 |  146959    9491   442086    46.6 |  0.037 % |
c |      9593 |  440877  1284428 |  161654    9593   446226    46.5 |  0.038 % |
c |      9743 |  440877  1284428 |  177820    9743   452544    46.4 |  0.038 % |
c ==============================================================================
c [1mFound solution: 381952[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9806 |  440889  1284458 |  146963    9806   455422    46.4 |  0.038 % |
c |      9906 |  440889  1284458 |  161659    9906   459239    46.4 |  0.039 % |
c ==============================================================================
c [1mFound solution: 370176[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10008 |  440898  1284480 |  146966   10008   463532    46.3 |  0.039 % |
c |     10108 |  440898  1284480 |  161662   10108   467155    46.2 |  0.039 % |
c ==============================================================================
c [1mFound solution: 369792[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10173 |  440902  1284490 |  146967   10173   469622    46.2 |  0.039 % |
c |     10273 |  440902  1284490 |  161663   10273   473694    46.1 |  0.040 % |
c |     10424 |  440902  1284490 |  177830   10424   479990    46.0 |  0.040 % |
c ==============================================================================
c [1mFound solution: 366464[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10486 |  440910  1284510 |  146970   10486   482731    46.0 |  0.040 % |
c |     10586 |  440910  1284510 |  161667   10586   487704    46.1 |  0.041 % |
c |     10736 |  440910  1284510 |  177833   10736   495363    46.1 |  0.041 % |
c |     10961 |  440910  1284510 |  195617   10961   506231    46.2 |  0.041 % |
c |     11300 |  440910  1284510 |  215178   11300   523137    46.3 |  0.041 % |
c ==============================================================================
c [1mFound solution: 361728[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11531 |  440922  1284538 |  146974   11531   534301    46.3 |  0.041 % |
c |     11633 |  440922  1284538 |  161671   11633   538758    46.3 |  0.041 % |
c |     11783 |  440922  1284538 |  177838   11783   544623    46.2 |  0.041 % |
c ==============================================================================
c [1mFound solution: 348800[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11924 |  440934  1284566 |  146978   11924   550662    46.2 |  0.041 % |
c |     12024 |  440934  1284566 |  161675   12024   554576    46.1 |  0.042 % |
c |     12174 |  440934  1284566 |  177843   12174   561272    46.1 |  0.042 % |
c |     12400 |  440934  1284566 |  195627   12400   571437    46.1 |  0.042 % |
c ==============================================================================
c [1mFound solution: 334976[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12500 |  440942  1284584 |  146980   12500   575891    46.1 |  0.042 % |
c ==============================================================================
c [1mFound solution: 332032[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12596 |  440953  1284609 |  146984   12596   579613    46.0 |  0.042 % |
c |     12696 |  440953  1284609 |  161682   12696   583453    46.0 |  0.043 % |
c |     12847 |  440953  1284609 |  177850   12847   590255    45.9 |  0.043 % |
c |     13072 |  440953  1284609 |  195635   13072   599872    45.9 |  0.043 % |
c ==============================================================================
c [1mFound solution: 329216[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13274 |  440961  1284627 |  146987   13274   608552    45.8 |  0.043 % |
c |     13374 |  440961  1284627 |  161685   13374   612767    45.8 |  0.044 % |
c |     13524 |  440961  1284627 |  177854   13524   619668    45.8 |  0.044 % |
c ==============================================================================
c [1mFound solution: 319104[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13639 |  440969  1284647 |  146989   13639   625710    45.9 |  0.044 % |
c |     13739 |  440969  1284647 |  161687   13739   629890    45.8 |  0.044 % |
c |     13897 |  440969  1284647 |  177856   13897   637746    45.9 |  0.044 % |
c |     14122 |  440969  1284647 |  195642   14122   648374    45.9 |  0.044 % |
c ==============================================================================
c [1mFound solution: 315904[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14372 |  440977  1284667 |  146992   14372   658242    45.8 |  0.044 % |
c |     14475 |  440971  1284654 |  161691   14465   662041    45.8 |  0.046 % |
c |     14625 |  440971  1284654 |  177860   14615   668757    45.8 |  0.046 % |
c ==============================================================================
c [1mFound solution: 304768[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14711 |  440982  1284679 |  146994   14701   672283    45.7 |  0.046 % |
c |     14816 |  440982  1284679 |  161693   14806   677451    45.8 |  0.047 % |
c |     14966 |  440982  1284679 |  177862   14956   683533    45.7 |  0.047 % |
c |     15191 |  440982  1284679 |  195649   15181   692486    45.6 |  0.047 % |
c |     15528 |  440982  1284679 |  215213   15518   709146    45.7 |  0.047 % |
c ==============================================================================
c [1mFound solution: 299776[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15644 |  440991  1284700 |  146997   15634   713370    45.6 |  0.047 % |
c |     15744 |  440991  1284700 |  161696   15734   717890    45.6 |  0.048 % |
c |     15897 |  440991  1284700 |  177866   15887   725496    45.7 |  0.048 % |
c |     16122 |  440991  1284700 |  195653   16112   739108    45.9 |  0.048 % |
c ==============================================================================
c [1mFound solution: 290944[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16208 |  440997  1284715 |  146999   16198   742649    45.8 |  0.048 % |
c |     16308 |  440997  1284715 |  161698   16298   746278    45.8 |  0.048 % |
c |     16458 |  440997  1284715 |  177868   16448   751421    45.7 |  0.048 % |
c |     16683 |  440997  1284715 |  195655   16673   761580    45.7 |  0.048 % |
c ==============================================================================
c [1mFound solution: 290432[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16824 |  441005  1284734 |  147001   16814   767918    45.7 |  0.048 % |
c |     16925 |  441005  1284734 |  161701   16915   773134    45.7 |  0.049 % |
c |     17076 |  441005  1284734 |  177871   17066   779868    45.7 |  0.049 % |
c ==============================================================================
c [1mFound solution: 274816[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17259 |  441014  1284755 |  147004   17249   787911    45.7 |  0.049 % |
c ==============================================================================
c [1mFound solution: 274304[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17335 |  441023  1284775 |  147007   17325   791218    45.7 |  0.049 % |
c |     17435 |  441023  1284775 |  161707   17425   794011    45.6 |  0.050 % |
c |     17585 |  441023  1284775 |  177878   17575   801040    45.6 |  0.050 % |
c |     17810 |  441023  1284775 |  195666   17800   811743    45.6 |  0.050 % |
c |     18147 |  441015  1284757 |  215232   18136   828050    45.7 |  0.052 % |
c ==============================================================================
c [1mFound solution: 273152[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18499 |  441025  1284780 |  147008   18488   843222    45.6 |  0.052 % |
c |     18599 |  441025  1284780 |  161708   18588   846957    45.6 |  0.052 % |
c |     18749 |  441025  1284780 |  177879   18738   853828    45.6 |  0.052 % |
c ==============================================================================
c [1mFound solution: 272256[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18857 |  441032  1284795 |  147010   18846   858450    45.6 |  0.052 % |
c |     18957 |  441032  1284795 |  161711   18946   863843    45.6 |  0.053 % |
c |     19107 |  441032  1284795 |  177882   19096   869575    45.5 |  0.053 % |
c ==============================================================================
c [1mFound solution: 272128[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19272 |  441042  1284817 |  147014   19261   877445    45.6 |  0.053 % |
c |     19372 |  441042  1284817 |  161715   19361   882035    45.6 |  0.054 % |
c ==============================================================================
c [1mFound solution: 262400[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19382 |  441049  1284832 |  147016   19371   882452    45.6 |  0.054 % |
c |     19484 |  441049  1284832 |  161717   19473   887084    45.6 |  0.054 % |
c ==============================================================================
c [1mFound solution: 246400[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19624 |  441058  1284854 |  147019   19613   893335    45.5 |  0.054 % |
c |     19725 |  441058  1284854 |  161720   19714   897482    45.5 |  0.055 % |
c |     19875 |  441058  1284854 |  177892   19864   911553    45.9 |  0.055 % |
c |     20101 |  441058  1284854 |  195682   20090   919918    45.8 |  0.055 % |
c ==============================================================================
c [1mFound solution: 241536[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20304 |  441064  1284869 |  147021   20293   928231    45.7 |  0.055 % |
c |     20404 |  441064  1284869 |  161723   20393   931629    45.7 |  0.056 % |
c ==============================================================================
c [1mFound solution: 240128[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20439 |  441071  1284887 |  147023   20428   932792    45.7 |  0.056 % |
c |     20539 |  441071  1284887 |  161725   20528   937206    45.7 |  0.056 % |
c ==============================================================================
c [1mFound solution: 235264[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20688 |  441081  1284911 |  147027   20677   944124    45.7 |  0.056 % |
c ==============================================================================
c [1mFound solution: 230400[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20751 |  441089  1284930 |  147029   20740   946610    45.6 |  0.056 % |
c ==============================================================================
c [1mFound solution: 211968[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20777 |  441097  1284951 |  147032   20766   947909    45.6 |  0.056 % |
c |     20877 |  441097  1284951 |  161735   20866   951420    45.6 |  0.058 % |
c ==============================================================================
c [1mFound solution: 205568[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20996 |  441100  1284958 |  147033   20985   957006    45.6 |  0.058 % |
c |     21096 |  441100  1284958 |  161736   21085   960796    45.6 |  0.059 % |
c |     21248 |  441100  1284958 |  177909   21237   967199    45.5 |  0.059 % |
c |     21475 |  441100  1284958 |  195700   21464   976785    45.5 |  0.059 % |
c ==============================================================================
c [1mFound solution: 185472[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21659 |  441110  1284982 |  147036   21648   983981    45.5 |  0.059 % |
c |     21759 |  441097  1284955 |  161739   21715   986335    45.4 |  0.062 % |
c |     21909 |  441097  1284955 |  177913   21865   991891    45.4 |  0.062 % |
c |     22134 |  441097  1284955 |  195704   22090  1000890    45.3 |  0.062 % |
c |     22471 |  441097  1284955 |  215275   22427  1015061    45.3 |  0.062 % |
c ==============================================================================
c [1mFound solution: 183296[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22595 |  441106  1284977 |  147035   22551  1020658    45.3 |  0.062 % |
c ==============================================================================
c [1mFound solution: 153216[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22689 |  441117  1285002 |  147039   22645  1024070    45.2 |  0.062 % |
c |     22794 |  441117  1285002 |  161742   22750  1027704    45.2 |  0.063 % |
c |     22945 |  441117  1285002 |  177917   22901  1033448    45.1 |  0.063 % |
c ==============================================================================
c [1mFound solution: 149888[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23023 |  441125  1285020 |  147041   22979  1036578    45.1 |  0.063 % |
c |     23125 |  441125  1285020 |  161745   23081  1041029    45.1 |  0.064 % |
c |     23275 |  441125  1285020 |  177919   23231  1050876    45.2 |  0.064 % |
c ==============================================================================
c [1mFound solution: 145024[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23385 |  441132  1285036 |  147044   23341  1055448    45.2 |  0.064 % |
c |     23485 |  441132  1285036 |  161748   23441  1059200    45.2 |  0.065 % |
c ==============================================================================
c [1mFound solution: 133248[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23491 |  441137  1285047 |  147045   23447  1059434    45.2 |  0.065 % |
c |     23592 |  441137  1285047 |  161749   23548  1062900    45.1 |  0.065 % |
c |     23742 |  441137  1285047 |  177924   23698  1072862    45.3 |  0.065 % |
c |     23968 |  441137  1285047 |  195716   23924  1082499    45.2 |  0.065 % |
c |     24305 |  441133  1285038 |  215288   24259  1098101    45.3 |  0.066 % |
c ==============================================================================
c [1mFound solution: 130688[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24656 |  441100  1284953 |  147033   23871  1089236    45.6 |  0.066 % |
c |     24756 |  441100  1284953 |  161736   23971  1093219    45.6 |  0.076 % |
c ==============================================================================
c [1mFound solution: 129280[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24893 |  441104  1284965 |  147034   24108  1099317    45.6 |  0.076 % |
c |     24993 |  441104  1284965 |  161737   24208  1103007    45.6 |  0.077 % |
c |     25143 |  441095  1284946 |  177911   24020  1095893    45.6 |  0.078 % |
c ==============================================================================
c [1mFound solution: 121728[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25230 |  441100  1284959 |  147033   24107  1099504    45.6 |  0.078 % |
c ==============================================================================
c [1mFound solution: 121344[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25288 |  441106  1284975 |  147035   24165  1101566    45.6 |  0.078 % |
c |     25388 |  441106  1284975 |  161738   24265  1105059    45.5 |  0.080 % |
c ==============================================================================
c [1mFound solution: 120960[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25496 |  441112  1284991 |  147037   24373  1109073    45.5 |  0.080 % |
c |     25597 |  441112  1284991 |  161740   24474  1112801    45.5 |  0.080 % |
c ==============================================================================
c [1mFound solution: 86016[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25667 |  441122  1285014 |  147040   24544  1114984    45.4 |  0.080 % |
c |     25768 |  441122  1285014 |  161744   24645  1118887    45.4 |  0.081 % |
c |     25919 |  441122  1285014 |  177918   24796  1124465    45.3 |  0.081 % |
#### 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.79 0.92 0.90 2/54 7785
Raw data (stat): 7785 (runsolver) R 7784 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546364118 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+10.0012 s]
Raw data (loadavg): 0.82 0.93 0.90 2/54 7785
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 14381 0 0 0 965 33 0 0 25 0 1 0 546364118 65925120 13296 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16095 13296 603 41 0 16054 0
vsize: 64380
[startup+20.0014 s]
Raw data (loadavg): 0.85 0.93 0.91 2/54 7785
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 14517 0 0 0 1965 34 0 0 25 0 1 0 546364118 66510848 13405 4294967295 134512640 134672761 3221224528 3221223696 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16238 13405 603 41 0 16197 0
vsize: 64952
[startup+30.0015 s]
Raw data (loadavg): 0.87 0.93 0.91 2/54 7785
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 14517 0 0 0 2965 34 0 0 25 0 1 0 546364118 66510848 13405 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16238 13405 603 41 0 16197 0
vsize: 64952
[startup+40.0021 s]
Raw data (loadavg): 0.89 0.93 0.91 2/54 7785
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 14535 0 0 0 3964 35 0 0 25 0 1 0 546364118 66641920 13423 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16270 13423 603 41 0 16229 0
vsize: 65080
[startup+50.0023 s]
Raw data (loadavg): 0.90 0.93 0.91 2/54 7785
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 14553 0 0 0 4964 35 0 0 25 0 1 0 546364118 66772992 13441 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16302 13441 603 41 0 16261 0
vsize: 65208
[startup+60.0034 s]
Raw data (loadavg): 0.92 0.93 0.91 2/54 7785
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 14566 0 0 0 5964 35 0 0 25 0 1 0 546364118 66772992 13454 4294967295 134512640 134672761 3221224528 3221223728 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16302 13454 603 41 0 16261 0
vsize: 65208
[startup+70.0041 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 7785
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 14580 0 0 0 6964 36 0 0 25 0 1 0 546364118 66772992 13468 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16302 13468 603 41 0 16261 0
vsize: 65208
[startup+80.0042 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 7785
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 14598 0 0 0 7963 37 0 0 25 0 1 0 546364118 66908160 13486 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16335 13486 603 41 0 16294 0
vsize: 65340
[startup+90.0043 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 7785
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 14618 0 0 0 8963 37 0 0 25 0 1 0 546364118 67039232 13506 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16367 13506 603 41 0 16326 0
vsize: 65468
[startup+100.004 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 7785
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 14634 0 0 0 9962 38 0 0 25 0 1 0 546364118 67039232 13522 4294967295 134512640 134672761 3221224528 3221223712 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16367 13522 603 41 0 16326 0
vsize: 65468
[startup+110.004 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 7785
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 14646 0 0 0 10962 38 0 0 25 0 1 0 546364118 67162112 13534 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16397 13534 603 41 0 16356 0
vsize: 65588
[startup+120.004 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 7785
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 14660 0 0 0 11961 38 0 0 25 0 1 0 546364118 67162112 13548 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16397 13548 603 41 0 16356 0
vsize: 65588
[startup+130.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 7785
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 14672 0 0 0 12961 39 0 0 25 0 1 0 546364118 67162112 13560 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16397 13560 603 41 0 16356 0
vsize: 65588
[startup+140.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 7785
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 14687 0 0 0 13961 39 0 0 25 0 1 0 546364118 67297280 13575 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16430 13575 603 41 0 16389 0
vsize: 65720
[startup+150.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 7785
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 14702 0 0 0 14961 39 0 0 25 0 1 0 546364118 67297280 13590 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16430 13590 603 41 0 16389 0
vsize: 65720
[startup+160.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 7785
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 14718 0 0 0 15961 40 0 0 25 0 1 0 546364118 67424256 13606 4294967295 134512640 134672761 3221224528 3221223652 134566128 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16461 13606 603 41 0 16420 0
vsize: 65844
[startup+170.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 14735 0 0 0 16960 40 0 0 25 0 1 0 546364118 67424256 13623 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16461 13623 603 41 0 16420 0
vsize: 65844
[startup+180.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 14747 0 0 0 17960 40 0 0 25 0 1 0 546364118 67555328 13635 4294967295 134512640 134672761 3221224528 3221223728 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16493 13635 603 41 0 16452 0
vsize: 65972
[startup+190.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 14763 0 0 0 18960 40 0 0 25 0 1 0 546364118 67555328 13651 4294967295 134512640 134672761 3221224528 3221223696 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16493 13651 603 41 0 16452 0
vsize: 65972
[startup+200.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 14780 0 0 0 19960 40 0 0 25 0 1 0 546364118 67690496 13668 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16526 13668 603 41 0 16485 0
vsize: 66104
[startup+210.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 14794 0 0 0 20961 40 0 0 25 0 1 0 546364118 67690496 13682 4294967295 134512640 134672761 3221224528 3221223680 134561040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16526 13682 603 41 0 16485 0
vsize: 66104
[startup+220.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 14806 0 0 0 21961 40 0 0 25 0 1 0 546364118 67821568 13694 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16558 13694 603 41 0 16517 0
vsize: 66232
[startup+230.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 14821 0 0 0 22961 40 0 0 25 0 1 0 546364118 67821568 13709 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16558 13709 603 41 0 16517 0
vsize: 66232
[startup+240.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 14835 0 0 0 23961 40 0 0 25 0 1 0 546364118 67821568 13723 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16558 13723 603 41 0 16517 0
vsize: 66232
[startup+250.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 14847 0 0 0 24961 41 0 0 25 0 1 0 546364118 67956736 13735 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16591 13735 603 41 0 16550 0
vsize: 66364
[startup+260.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 14860 0 0 0 25961 41 0 0 25 0 1 0 546364118 67956736 13748 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16591 13748 603 41 0 16550 0
vsize: 66364
[startup+270.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 14876 0 0 0 26961 41 0 0 25 0 1 0 546364118 68087808 13764 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16623 13764 603 41 0 16582 0
vsize: 66492
[startup+280.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 14887 0 0 0 27961 41 0 0 25 0 1 0 546364118 68087808 13775 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16623 13775 603 41 0 16582 0
vsize: 66492
[startup+290.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 14902 0 0 0 28961 41 0 0 25 0 1 0 546364118 68087808 13790 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16623 13790 603 41 0 16582 0
vsize: 66492
[startup+300.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 14916 0 0 0 29962 41 0 0 25 0 1 0 546364118 68218880 13804 4294967295 134512640 134672761 3221224528 3221223728 134557820 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16655 13804 603 41 0 16614 0
vsize: 66620
[startup+310.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 14926 0 0 0 30962 41 0 0 25 0 1 0 546364118 68218880 13814 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16655 13814 603 41 0 16614 0
vsize: 66620
[startup+320.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 14937 0 0 0 31962 41 0 0 25 0 1 0 546364118 68354048 13825 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16688 13825 603 41 0 16647 0
vsize: 66752
[startup+330.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 14957 0 0 0 32962 41 0 0 25 0 1 0 546364118 68354048 13845 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16688 13845 603 41 0 16647 0
vsize: 66752
[startup+340.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 14973 0 0 0 33962 41 0 0 25 0 1 0 546364118 68534272 13861 4294967295 134512640 134672761 3221224528 3221223664 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16732 13861 603 41 0 16691 0
vsize: 66928
[startup+350.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 14983 0 0 0 34962 41 0 0 25 0 1 0 546364118 68534272 13871 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16732 13871 603 41 0 16691 0
vsize: 66928
[startup+360.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 14993 0 0 0 35962 41 0 0 25 0 1 0 546364118 68534272 13881 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16732 13881 603 41 0 16691 0
vsize: 66928
[startup+370.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15009 0 0 0 36962 41 0 0 25 0 1 0 546364118 68669440 13897 4294967295 134512640 134672761 3221224528 3221223664 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16765 13897 603 41 0 16724 0
vsize: 67060
[startup+380.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15017 0 0 0 37963 41 0 0 25 0 1 0 546364118 68669440 13905 4294967295 134512640 134672761 3221224528 3221223664 134565140 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16765 13905 603 41 0 16724 0
vsize: 67060
[startup+390.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15027 0 0 0 38963 41 0 0 25 0 1 0 546364118 68669440 13915 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16765 13915 603 41 0 16724 0
vsize: 67060
[startup+400.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15038 0 0 0 39963 41 0 0 25 0 1 0 546364118 68669440 13926 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16765 13926 603 41 0 16724 0
vsize: 67060
[startup+410.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15050 0 0 0 40963 41 0 0 25 0 1 0 546364118 68800512 13938 4294967295 134512640 134672761 3221224528 3221223680 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16797 13938 603 41 0 16756 0
vsize: 67188
[startup+420.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15063 0 0 0 41963 41 0 0 25 0 1 0 546364118 68800512 13951 4294967295 134512640 134672761 3221224528 3221223728 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16797 13951 603 41 0 16756 0
vsize: 67188
[startup+430.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15071 0 0 0 42964 41 0 0 25 0 1 0 546364118 68800512 13959 4294967295 134512640 134672761 3221224528 3221223632 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16797 13959 603 41 0 16756 0
vsize: 67188
[startup+440.006 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15085 0 0 0 43964 41 0 0 25 0 1 0 546364118 68931584 13973 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16829 13973 603 41 0 16788 0
vsize: 67316
[startup+450.006 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15097 0 0 0 44964 41 0 0 25 0 1 0 546364118 68931584 13985 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16829 13985 603 41 0 16788 0
vsize: 67316
[startup+460.007 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15109 0 0 0 45964 41 0 0 25 0 1 0 546364118 69062656 13997 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16861 13997 603 41 0 16820 0
vsize: 67444
[startup+470.007 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15120 0 0 0 46964 42 0 0 25 0 1 0 546364118 69062656 14008 4294967295 134512640 134672761 3221224528 3221223664 134565036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16861 14008 603 41 0 16820 0
vsize: 67444
[startup+480.007 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15132 0 0 0 47964 42 0 0 25 0 1 0 546364118 69062656 14020 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16861 14020 603 41 0 16820 0
vsize: 67444
[startup+490.008 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15144 0 0 0 48965 42 0 0 25 0 1 0 546364118 69193728 14032 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16893 14032 603 41 0 16852 0
vsize: 67572
[startup+500.008 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15156 0 0 0 49965 42 0 0 25 0 1 0 546364118 69193728 14044 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16893 14044 603 41 0 16852 0
vsize: 67572
[startup+510.009 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15168 0 0 0 50965 42 0 0 25 0 1 0 546364118 69193728 14056 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16893 14056 603 41 0 16852 0
vsize: 67572
[startup+520.009 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15182 0 0 0 51965 42 0 0 25 0 1 0 546364118 69320704 14070 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16924 14070 603 41 0 16883 0
vsize: 67696
[startup+530.008 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15196 0 0 0 52965 42 0 0 25 0 1 0 546364118 69320704 14084 4294967295 134512640 134672761 3221224528 3221223828 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16924 14084 603 41 0 16883 0
vsize: 67696
[startup+540.009 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15206 0 0 0 53965 42 0 0 25 0 1 0 546364118 69439488 14094 4294967295 134512640 134672761 3221224528 3221223696 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16953 14094 603 41 0 16912 0
vsize: 67812
[startup+550.009 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15218 0 0 0 54965 42 0 0 25 0 1 0 546364118 69439488 14106 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16953 14106 603 41 0 16912 0
vsize: 67812
[startup+560.009 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15230 0 0 0 55965 42 0 0 25 0 1 0 546364118 69439488 14118 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16953 14118 603 41 0 16912 0
vsize: 67812
[startup+570.01 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15240 0 0 0 56965 42 0 0 25 0 1 0 546364118 69570560 14128 4294967295 134512640 134672761 3221224528 3221223728 134557820 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16985 14128 603 41 0 16944 0
vsize: 67940
[startup+580.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15253 0 0 0 57965 42 0 0 25 0 1 0 546364118 69570560 14141 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16985 14141 603 41 0 16944 0
vsize: 67940
[startup+590.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15269 0 0 0 58966 43 0 0 25 0 1 0 546364118 69701632 14157 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17017 14157 603 41 0 16976 0
vsize: 68068
[startup+600.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15282 0 0 0 59966 43 0 0 25 0 1 0 546364118 69701632 14170 4294967295 134512640 134672761 3221224528 3221223712 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17017 14170 603 41 0 16976 0
vsize: 68068
[startup+610.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15297 0 0 0 60966 43 0 0 25 0 1 0 546364118 69701632 14185 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17017 14185 603 41 0 16976 0
vsize: 68068
[startup+620.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15306 0 0 0 61966 43 0 0 25 0 1 0 546364118 69836800 14194 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17050 14194 603 41 0 17009 0
vsize: 68200
[startup+630.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15321 0 0 0 62966 43 0 0 25 0 1 0 546364118 69836800 14209 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17050 14209 603 41 0 17009 0
vsize: 68200
[startup+640.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15329 0 0 0 63966 43 0 0 25 0 1 0 546364118 69836800 14217 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17050 14217 603 41 0 17009 0
vsize: 68200
[startup+650.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15339 0 0 0 64966 43 0 0 25 0 1 0 546364118 69967872 14227 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17082 14227 603 41 0 17041 0
vsize: 68328
[startup+660.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15348 0 0 0 65967 43 0 0 25 0 1 0 546364118 69967872 14236 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17082 14236 603 41 0 17041 0
vsize: 68328
[startup+670.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15359 0 0 0 66967 43 0 0 25 0 1 0 546364118 69967872 14247 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17082 14247 603 41 0 17041 0
vsize: 68328
[startup+680.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15370 0 0 0 67967 43 0 0 25 0 1 0 546364118 70098944 14258 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17114 14258 603 41 0 17073 0
vsize: 68456
[startup+690.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15382 0 0 0 68967 43 0 0 25 0 1 0 546364118 70098944 14270 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17114 14270 603 41 0 17073 0
vsize: 68456
[startup+700.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15399 0 0 0 69967 43 0 0 25 0 1 0 546364118 70242304 14287 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17149 14287 603 41 0 17108 0
vsize: 68596
[startup+710.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15423 0 0 0 70967 43 0 0 25 0 1 0 546364118 70438912 14311 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17197 14311 603 41 0 17156 0
vsize: 68788
[startup+720.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15423 0 0 0 71967 43 0 0 25 0 1 0 546364118 70438912 14311 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17197 14311 603 41 0 17156 0
vsize: 68788
[startup+730.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15434 0 0 0 72967 43 0 0 25 0 1 0 546364118 70438912 14322 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17197 14322 603 41 0 17156 0
vsize: 68788
[startup+740.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15445 0 0 0 73968 44 0 0 25 0 1 0 546364118 70438912 14333 4294967295 134512640 134672761 3221224528 3221223696 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17197 14333 603 41 0 17156 0
vsize: 68788
[startup+750.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15458 0 0 0 74968 44 0 0 25 0 1 0 546364118 70574080 14346 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17230 14346 603 41 0 17189 0
vsize: 68920
[startup+760.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15467 0 0 0 75968 44 0 0 25 0 1 0 546364118 70574080 14355 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17230 14355 603 41 0 17189 0
vsize: 68920
[startup+770.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15479 0 0 0 76968 44 0 0 25 0 1 0 546364118 70574080 14367 4294967295 134512640 134672761 3221224528 3221223632 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17230 14367 603 41 0 17189 0
vsize: 68920
[startup+780.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15489 0 0 0 77968 44 0 0 25 0 1 0 546364118 70705152 14377 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17262 14377 603 41 0 17221 0
vsize: 69048
[startup+790.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15499 0 0 0 78968 44 0 0 25 0 1 0 546364118 70705152 14387 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17262 14387 603 41 0 17221 0
vsize: 69048
[startup+800.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15511 0 0 0 79968 44 0 0 25 0 1 0 546364118 70705152 14399 4294967295 134512640 134672761 3221224528 3221223728 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17262 14399 603 41 0 17221 0
vsize: 69048
[startup+810.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15520 0 0 0 80968 44 0 0 25 0 1 0 546364118 70823936 14408 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17291 14408 603 41 0 17250 0
vsize: 69164
[startup+820.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15527 0 0 0 81968 44 0 0 25 0 1 0 546364118 70823936 14415 4294967295 134512640 134672761 3221224528 3221223728 134557915 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17291 14415 603 41 0 17250 0
vsize: 69164
[startup+830.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15539 0 0 0 82969 44 0 0 25 0 1 0 546364118 70823936 14427 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17291 14427 603 41 0 17250 0
vsize: 69164
[startup+840.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15548 0 0 0 83969 44 0 0 25 0 1 0 546364118 70823936 14436 4294967295 134512640 134672761 3221224528 3221223680 1074743929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17291 14436 603 41 0 17250 0
vsize: 69164
[startup+850.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15557 0 0 0 84969 44 0 0 25 0 1 0 546364118 70955008 14445 4294967295 134512640 134672761 3221224528 3221223652 134566109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17323 14445 603 41 0 17282 0
vsize: 69292
[startup+860.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15567 0 0 0 85969 45 0 0 25 0 1 0 546364118 70955008 14455 4294967295 134512640 134672761 3221224528 3221223632 134560367 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17323 14455 603 41 0 17282 0
vsize: 69292
[startup+870.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15578 0 0 0 86969 45 0 0 25 0 1 0 546364118 70955008 14466 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17323 14466 603 41 0 17282 0
vsize: 69292
[startup+880.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15590 0 0 0 87969 45 0 0 25 0 1 0 546364118 71081984 14478 4294967295 134512640 134672761 3221224528 3221223664 134560566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17354 14478 603 41 0 17313 0
vsize: 69416
[startup+890.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15608 0 0 0 88969 45 0 0 25 0 1 0 546364118 71081984 14496 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17354 14496 603 41 0 17313 0
vsize: 69416
[startup+900.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15619 0 0 0 89969 45 0 0 25 0 1 0 546364118 71217152 14507 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17387 14507 603 41 0 17346 0
vsize: 69548
[startup+910.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15630 0 0 0 90969 45 0 0 25 0 1 0 546364118 71217152 14518 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17387 14518 603 41 0 17346 0
vsize: 69548
[startup+920.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15638 0 0 0 91969 45 0 0 25 0 1 0 546364118 71217152 14526 4294967295 134512640 134672761 3221224528 3221223632 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17387 14526 603 41 0 17346 0
vsize: 69548
[startup+930.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15649 0 0 0 92969 45 0 0 25 0 1 0 546364118 71352320 14537 4294967295 134512640 134672761 3221224528 3221223688 134561238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17420 14537 603 41 0 17379 0
vsize: 69680
[startup+940.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15661 0 0 0 93970 45 0 0 25 0 1 0 546364118 71352320 14549 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17420 14549 603 41 0 17379 0
vsize: 69680
[startup+950.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15669 0 0 0 94970 45 0 0 25 0 1 0 546364118 71352320 14557 4294967295 134512640 134672761 3221224528 3221223676 1074754688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17420 14557 603 41 0 17379 0
vsize: 69680
[startup+960.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15682 0 0 0 95970 45 0 0 25 0 1 0 546364118 71483392 14570 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17452 14570 603 41 0 17411 0
vsize: 69808
[startup+970.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15689 0 0 0 96970 46 0 0 25 0 1 0 546364118 71483392 14577 4294967295 134512640 134672761 3221224528 3221223652 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17452 14577 603 41 0 17411 0
vsize: 69808
[startup+980.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15696 0 0 0 97970 46 0 0 25 0 1 0 546364118 71483392 14584 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17452 14584 603 41 0 17411 0
vsize: 69808
[startup+990.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15705 0 0 0 98970 46 0 0 25 0 1 0 546364118 71483392 14593 4294967295 134512640 134672761 3221224528 3221223696 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17452 14593 603 41 0 17411 0
vsize: 69808
[startup+1000.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15714 0 0 0 99970 46 0 0 25 0 1 0 546364118 71622656 14602 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17486 14602 603 41 0 17445 0
vsize: 69944
[startup+1010.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15722 0 0 0 100970 46 0 0 25 0 1 0 546364118 71622656 14610 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17486 14610 603 41 0 17445 0
vsize: 69944
[startup+1020.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15731 0 0 0 101970 46 0 0 25 0 1 0 546364118 71622656 14619 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17486 14619 603 41 0 17445 0
vsize: 69944
[startup+1030.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15739 0 0 0 102970 46 0 0 25 0 1 0 546364118 71622656 14627 4294967295 134512640 134672761 3221224528 3221223696 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17486 14627 603 41 0 17445 0
vsize: 69944
[startup+1040.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15749 0 0 0 103971 46 0 0 25 0 1 0 546364118 71753728 14637 4294967295 134512640 134672761 3221224528 3221223728 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17518 14637 603 41 0 17477 0
vsize: 70072
[startup+1050.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15761 0 0 0 104971 46 0 0 25 0 1 0 546364118 71753728 14649 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17518 14649 603 41 0 17477 0
vsize: 70072
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15772 0 0 0 105972 46 0 0 25 0 1 0 546364118 71753728 14660 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17518 14660 603 41 0 17477 0
vsize: 70072
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15778 0 0 0 106972 47 0 0 25 0 1 0 546364118 71872512 14666 4294967295 134512640 134672761 3221224528 3221223696 134561394 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17547 14666 603 41 0 17506 0
vsize: 70188
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15791 0 0 0 107972 47 0 0 25 0 1 0 546364118 71872512 14679 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17547 14679 603 41 0 17506 0
vsize: 70188
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15800 0 0 0 108972 47 0 0 25 0 1 0 546364118 71872512 14688 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17547 14688 603 41 0 17506 0
vsize: 70188
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15816 0 0 0 109972 47 0 0 25 0 1 0 546364118 72003584 14704 4294967295 134512640 134672761 3221224528 3221223664 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17579 14704 603 41 0 17538 0
vsize: 70316
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15833 0 0 0 110972 47 0 0 25 0 1 0 546364118 72146944 14721 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17614 14721 603 41 0 17573 0
vsize: 70456
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15842 0 0 0 111972 47 0 0 25 0 1 0 546364118 72146944 14730 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17614 14730 603 41 0 17573 0
vsize: 70456
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15847 0 0 0 112973 47 0 0 25 0 1 0 546364118 72146944 14735 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17614 14735 603 41 0 17573 0
vsize: 70456
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15847 0 0 0 113973 47 0 0 25 0 1 0 546364118 72146944 14735 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17614 14735 603 41 0 17573 0
vsize: 70456
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15849 0 0 0 114973 47 0 0 25 0 1 0 546364118 72146944 14737 4294967295 134512640 134672761 3221224528 3221223728 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17614 14737 603 41 0 17573 0
vsize: 70456
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15849 0 0 0 115973 47 0 0 25 0 1 0 546364118 72146944 14737 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17614 14737 603 41 0 17573 0
vsize: 70456
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15853 0 0 0 116973 47 0 0 25 0 1 0 546364118 72146944 14741 4294967295 134512640 134672761 3221224528 3221223680 134565083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17614 14741 603 41 0 17573 0
vsize: 70456
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15853 0 0 0 117973 47 0 0 25 0 1 0 546364118 72146944 14741 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17614 14741 603 41 0 17573 0
vsize: 70456
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15860 0 0 0 118973 48 0 0 25 0 1 0 546364118 72146944 14748 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17614 14748 603 41 0 17573 0
vsize: 70456
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 7787
Raw data (stat): 7785 (minisat+) R 7784 3260 3259 0 -1 0 15866 0 0 0 119973 48 0 0 25 0 1 0 546364118 72273920 14754 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17645 14754 603 41 0 17604 0
vsize: 70580
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 7787
Raw data (stat): 7785 (minisat+) Z 7784 3260 3259 0 -1 12 15869 0 0 0 119973 50 0 0 25 0 1 0 546364118 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.25
CPU user time (s): 1199.74
CPU system time (s): 0.507922
CPU usage (%): 100.016
Max. virtual memory (Kb): 70580
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####