PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-neos5.opb
MD5SUM	e6bff154156b54af3a9a38f7579209b6
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	17324
Optimality of the best value was proved	NO
Number of terms in the objective function	163
Biggest coefficient in the objective function	1024
Number of bits for the biggest coefficient in the objective function	11
Sum of the numbers in the objective function	74742
Number of bits of the sum of numbers in the objective function	17
Biggest number in a constraint	8192
Number of bits of the biggest number in a constraint	14
Biggest sum of numbers in a constraint	74742
Number of bits of the biggest sum of numbers	17
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.06984
Number of variables	163
Total number of constraints	126
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	56
Number of constraints which are nor clauses,nor cardinality constraints	70
Minimum length of a constraint	1
Maximum length of a constraint	102
Trace number 20710

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc22 THE 2005-04-21 21:41:40 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=14716 boxname=wulflinc22 idbench=1132 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  e6bff154156b54af3a9a38f7579209b6  /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-neos5.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-neos5.opb /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-neos5.opb
IDLAUNCH: 14716
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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.031
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:        230672 kB
Buffers:         32692 kB
Cached:         741808 kB
SwapCached:         20 kB
Active:         185916 kB
Inactive:       591268 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        230420 kB
SwapTotal:     2097892 kB
SwapFree:      2097664 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6640 kB
Slab:            21020 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 22:01:42 (client local time) WITH STATUS 10 IN 1200.38 SECONDS
stats: 14716 7 1200.38 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 73 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[  72]---> BDD-cost:   10
c ---[  71]---> BDD-cost:   10
c ---[  70]---> BDD-cost:   10
c ---[  69]---> BDD-cost:   10
c ---[  68]---> BDD-cost:   10
c ---[  67]---> BDD-cost:   10
c ---[  66]---> BDD-cost:   10
c ---[  65]---> BDD-cost:   10
c ---[  64]---> BDD-cost:   10
c ---[  63]---> BDD-cost:   10
c ---[  62]---> Sorter-cost:  382     Base:
c ---[  61]---> Sorter-cost:  831     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  60]---> Sorter-cost:  417     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  59]---> Sorter-cost: 1471     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  58]---> Sorter-cost: 1060     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  57]---> Sorter-cost:  429     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  56]---> Sorter-cost: 1241     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  55]---> Sorter-cost: 1058     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  54]---> Sorter-cost: 1090     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  53]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  52]---> Sorter-cost: 1269     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  51]---> Sorter-cost:  216     Base:
c ---[  50]---> Sorter-cost: 1042     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  49]---> Sorter-cost: 1289     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  48]---> Sorter-cost:  548     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  47]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  46]---> Sorter-cost:  373     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  45]---> Sorter-cost:  405     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  44]---> Sorter-cost:  343     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  43]---> Sorter-cost:  365     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  42]---> Sorter-cost:  397     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  41]---> Sorter-cost:  379     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  40]---> Sorter-cost:  351     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  39]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  38]---> Sorter-cost: 1195     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  37]---> Sorter-cost:  345     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  36]---> Sorter-cost:  365     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  35]---> Sorter-cost:  397     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  34]---> Sorter-cost:  379     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  33]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  32]---> Sorter-cost: 1215     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  31]---> Sorter-cost:  405     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  30]---> Sorter-cost:  417     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  29]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  28]---> Sorter-cost: 1020     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  27]---> Sorter-cost: 1259     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  26]---> Sorter-cost:  337     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  25]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  24]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  23]---> Sorter-cost:  365     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  22]---> Sorter-cost:  397     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  21]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  20]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  19]---> Sorter-cost:  365     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  18]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  17]---> Sorter-cost:  397     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  16]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  15]---> Sorter-cost:  355     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  14]---> Sorter-cost:  387     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  13]---> Sorter-cost:  389     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  12]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  11]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  10]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   9]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   8]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   7]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   6]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   5]---> Sorter-cost:  355     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   4]---> Sorter-cost:  387     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   3]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   2]---> Sorter-cost:  130     Base:
c ---[   1]---> Sorter-cost:  301     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   0]---> Sorter-cost:  301     Base: 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 |         0 |   58197   137532 |   19399       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 27646[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 2665     Base: 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 |        25 |   65091   153767 |   21697      25      322    12.9 |  0.000 % |
c ==============================================================================
c [1mFound solution: 26643[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       112 |   65126   153860 |   21708     112      886     7.9 |  0.000 % |
c |       212 |   65123   153854 |   23878     211     1448     6.9 |  0.383 % |
c ==============================================================================
c [1mFound solution: 26642[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       276 |   65153   153936 |   21717     275     1891     6.9 |  0.383 % |
c ==============================================================================
c [1mFound solution: 26638[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       356 |   65168   153975 |   21722     355     2383     6.7 |  0.383 % |
c ==============================================================================
c [1mFound solution: 26637[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       439 |   65180   154013 |   21726     437     2855     6.5 |  0.383 % |
c |       539 |   65180   154013 |   23898     537     3646     6.8 |  0.416 % |
c ==============================================================================
c [1mFound solution: 26635[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       572 |   65195   154052 |   21731     570     3932     6.9 |  0.416 % |
c |       672 |   65195   154052 |   23904     670     4775     7.1 |  0.420 % |
c ==============================================================================
c [1mFound solution: 26110[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       721 |   65265   154229 |   21755     719     4959     6.9 |  0.420 % |
c ==============================================================================
c [1mFound solution: 25598[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       738 |   65281   154271 |   21760     736     5215     7.1 |  0.420 % |
c ==============================================================================
c [1mFound solution: 25594[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       777 |   65292   154302 |   21764     775     5720     7.4 |  0.420 % |
c ==============================================================================
c [1mFound solution: 25593[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       794 |   65304   154336 |   21768     792     5836     7.4 |  0.420 % |
c ==============================================================================
c [1mFound solution: 25592[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       797 |   65323   154389 |   21774     795     5852     7.4 |  0.420 % |
c ==============================================================================
c [1mFound solution: 25591[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 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 |       800 |   65335   154421 |   21778     798     5868     7.4 |  0.420 % |
c ==============================================================================
c [1mFound solution: 25116[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       894 |   65360   154482 |   21786     892     6371     7.1 |  0.420 % |
c ==============================================================================
c [1mFound solution: 25071[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       933 |   65372   154514 |   21790     931     6621     7.1 |  0.420 % |
c ==============================================================================
c [1mFound solution: 24719[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       975 |   65388   154554 |   21796     973     6811     7.0 |  0.420 % |
c ==============================================================================
c [1mFound solution: 24621[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       999 |   65395   154574 |   21798     995     7013     7.0 |  0.420 % |
c ==============================================================================
c [1mFound solution: 24613[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1003 |   65412   154617 |   21804     999     7031     7.0 |  0.420 % |
c ==============================================================================
c [1mFound solution: 24612[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1006 |   65429   154660 |   21809    1002     7059     7.0 |  0.420 % |
c ==============================================================================
c [1mFound solution: 24606[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1008 |   65443   154696 |   21814    1004     7067     7.0 |  0.420 % |
c ==============================================================================
c [1mFound solution: 24570[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1051 |   65456   154731 |   21818    1047     7384     7.1 |  0.420 % |
c ==============================================================================
c [1mFound solution: 23614[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1088 |   65497   154835 |   21832    1084     7660     7.1 |  0.420 % |
c ==============================================================================
c [1mFound solution: 23590[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1152 |   65519   154891 |   21839    1148     8169     7.1 |  0.420 % |
c ==============================================================================
c [1mFound solution: 23586[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1167 |   65536   154934 |   21845    1163     8217     7.1 |  0.420 % |
c ==============================================================================
c [1mFound solution: 23570[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1172 |   65547   154963 |   21849    1168     8252     7.1 |  0.420 % |
c ==============================================================================
c [1mFound solution: 23058[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1231 |   65567   155013 |   21855    1227     9106     7.4 |  0.420 % |
c ==============================================================================
c [1mFound solution: 23057[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1277 |   65587   155063 |   21862    1273     9466     7.4 |  0.420 % |
c ==============================================================================
c [1mFound solution: 21010[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1308 |   65642   155196 |   21880    1304     9712     7.4 |  0.420 % |
c ==============================================================================
c [1mFound solution: 21006[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1390 |   65655   155229 |   21885    1386    10549     7.6 |  0.420 % |
c |      1490 |   65655   155229 |   24073    1486    11153     7.5 |  0.535 % |
c |      1641 |   65630   155174 |   26480    1620    12301     7.6 |  0.568 % |
c |      1866 |   65630   155174 |   29128    1845    14247     7.7 |  0.568 % |
c ==============================================================================
c [1mFound solution: 20542[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1889 |   65639   155197 |   21879    1868    14532     7.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 20541[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1941 |   65650   155227 |   21883    1918    14913     7.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 20525[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1957 |   65660   155253 |   21886    1934    15004     7.8 |  0.568 % |
c |      2061 |   65660   155253 |   24074    2038    15808     7.8 |  0.586 % |
c |      2211 |   65660   155253 |   26482    2188    16557     7.6 |  0.586 % |
c ==============================================================================
c [1mFound solution: 20276[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2275 |   65703   155360 |   21901    2252    17279     7.7 |  0.586 % |
c |      2379 |   65703   155360 |   24091    2356    18377     7.8 |  0.591 % |
c |      2531 |   65703   155360 |   26500    2508    21217     8.5 |  0.591 % |
c ==============================================================================
c [1mFound solution: 19958[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2635 |   65721   155408 |   21907    2612    21761     8.3 |  0.591 % |
c ==============================================================================
c [1mFound solution: 19700[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2728 |   65731   155434 |   21910    2705    22765     8.4 |  0.591 % |
c |      2828 |   65731   155434 |   24101    2805    23852     8.5 |  0.600 % |
c ==============================================================================
c [1mFound solution: 19598[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2947 |   65744   155467 |   21914    2924    25248     8.6 |  0.600 % |
c ==============================================================================
c [1mFound solution: 19566[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2979 |   65755   155496 |   21918    2956    25428     8.6 |  0.600 % |
c |      3079 |   65755   155496 |   24109    3056    26888     8.8 |  0.609 % |
c ==============================================================================
c [1mFound solution: 19563[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3180 |   65766   155525 |   21922    3157    27710     8.8 |  0.609 % |
c ==============================================================================
c [1mFound solution: 19527[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3229 |   65779   155558 |   21926    3206    28087     8.8 |  0.609 % |
c ==============================================================================
c [1mFound solution: 18530[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3266 |   65797   155604 |   21932    3243    28411     8.8 |  0.609 % |
c |      3367 |   65797   155604 |   24125    3344    29184     8.7 |  0.623 % |
c |      3518 |   65797   155604 |   26537    3495    30873     8.8 |  0.623 % |
c ==============================================================================
c [1mFound solution: 18486[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3572 |   65809   155636 |   21936    3549    32003     9.0 |  0.623 % |
c |      3673 |   65773   155558 |   24129    3646    33099     9.1 |  0.669 % |
c ==============================================================================
c [1mFound solution: 18381[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3738 |   65816   155665 |   21938    3711    34635     9.3 |  0.669 % |
c |      3839 |   65816   155665 |   24131    3812    35915     9.4 |  0.688 % |
c |      3989 |   65816   155665 |   26544    3962    37882     9.6 |  0.688 % |
c |      4214 |   65816   155665 |   29199    4187    43523    10.4 |  0.688 % |
c |      4551 |   65801   155632 |   32119    4523    46638    10.3 |  0.706 % |
c |      5057 |   65801   155632 |   35331    5029    59377    11.8 |  0.706 % |
c |      5817 |   65801   155632 |   38864    5789    67671    11.7 |  0.706 % |
c ==============================================================================
c [1mFound solution: 18294[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5915 |   65820   155679 |   21940    5887    69427    11.8 |  0.706 % |
c |      6015 |   65820   155679 |   24134    5987    71585    12.0 |  0.711 % |
c |      6166 |   65820   155679 |   26547    6138    74150    12.1 |  0.711 % |
c |      6391 |   65808   155649 |   29202    6362    81448    12.8 |  0.715 % |
c |      6728 |   65808   155649 |   32122    6699    85694    12.8 |  0.715 % |
c |      7234 |   65808   155649 |   35334    7205    94998    13.2 |  0.715 % |
c |      7993 |   65808   155649 |   38868    7964   111247    14.0 |  0.715 % |
c ==============================================================================
c [1mFound solution: 17905[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8543 |   65819   155678 |   21939    8514   117539    13.8 |  0.715 % |
c |      8643 |   65819   155678 |   24132    8614   118472    13.8 |  0.720 % |
c |      8793 |   65819   155678 |   26546    8764   120881    13.8 |  0.720 % |
c |      9018 |   65819   155678 |   29200    8989   122638    13.6 |  0.720 % |
c ==============================================================================
c [1mFound solution: 17135[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9349 |   65841   155732 |   21947    9320   138755    14.9 |  0.720 % |
c |      9450 |   65841   155732 |   24141    9421   140287    14.9 |  0.724 % |
c |      9600 |   65841   155732 |   26555    9571   143640    15.0 |  0.724 % |
c |      9826 |   65841   155732 |   29211    9797   149410    15.3 |  0.724 % |
c |     10164 |   65841   155732 |   32132   10135   154716    15.3 |  0.724 % |
c |     10670 |   65841   155732 |   35345   10641   170047    16.0 |  0.724 % |
c |     11429 |   65841   155732 |   38880   11400   182824    16.0 |  0.724 % |
c |     12569 |   65841   155732 |   42768   12540   239262    19.1 |  0.724 % |
c |     14277 |   65834   155716 |   47045   14247   270590    19.0 |  0.729 % |
c |     16839 |   65834   155716 |   51749   16809   319345    19.0 |  0.729 % |
c ==============================================================================
c [1mFound solution: 16982[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17606 |   65853   155761 |   21951   17576   334748    19.0 |  0.729 % |
c |     17706 |   65853   155761 |   24146   17676   336786    19.1 |  0.734 % |
c |     17856 |   65853   155761 |   26560   17826   338365    19.0 |  0.734 % |
c |     18081 |   65853   155761 |   29216   18051   344738    19.1 |  0.734 % |
c |     18420 |   65853   155761 |   32138   18390   356466    19.4 |  0.734 % |
c |     18927 |   65853   155761 |   35352   18897   367798    19.5 |  0.734 % |
c ==============================================================================
c [1mFound solution: 16981[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19372 |   65872   155806 |   21957   19342   386569    20.0 |  0.734 % |
c |     19472 |   65872   155806 |   24152   19442   389446    20.0 |  0.738 % |
c |     19622 |   65872   155806 |   26567   19592   392076    20.0 |  0.738 % |
c |     19848 |   65872   155806 |   29224   19818   400489    20.2 |  0.738 % |
c |     20185 |   65872   155806 |   32147   20155   414408    20.6 |  0.738 % |
c |     20693 |   65872   155806 |   35361   20663   431560    20.9 |  0.738 % |
c ==============================================================================
c [1mFound solution: 16966[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21148 |   65888   155844 |   21962   21118   454396    21.5 |  0.738 % |
c |     21249 |   65888   155844 |   24158   21219   455874    21.5 |  0.742 % |
c |     21401 |   65888   155844 |   26574   21371   458074    21.4 |  0.742 % |
c |     21627 |   65888   155844 |   29231   21597   462045    21.4 |  0.742 % |
c |     21966 |   65729   155488 |   32154   21872   468420    21.4 |  0.934 % |
c |     22474 |   65729   155488 |   35370   22380   488305    21.8 |  0.934 % |
c |     23234 |   65729   155488 |   38907   23140   522886    22.6 |  0.934 % |
c ==============================================================================
c [1mFound solution: 16965[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23625 |   65745   155526 |   21915   23531   531466    22.6 |  0.934 % |
c |     23726 |   65745   155526 |   24106   11867   253370    21.4 |  0.938 % |
c |     23877 |   65745   155526 |   26517   12018   260261    21.7 |  0.938 % |
c |     24102 |   65745   155526 |   29168   12243   265761    21.7 |  0.938 % |
c |     24439 |   65745   155526 |   32085   12580   275233    21.9 |  0.938 % |
c |     24947 |   65745   155526 |   35294   13088   285369    21.8 |  0.938 % |
c |     25706 |   65745   155526 |   38823   13847   299246    21.6 |  0.938 % |
c |     26846 |   65732   155498 |   42706   14985   318939    21.3 |  0.952 % |
c ==============================================================================
c [1mFound solution: 16908[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26927 |   65750   155542 |   21916   15066   321169    21.3 |  0.952 % |
c |     27028 |   65750   155542 |   24107   15167   324193    21.4 |  0.957 % |
c |     27179 |   65750   155542 |   26518   15318   327543    21.4 |  0.957 % |
c |     27404 |   65750   155542 |   29170   15543   334593    21.5 |  0.957 % |
c |     27741 |   65750   155542 |   32087   15880   343985    21.7 |  0.957 % |
c |     28248 |   65750   155542 |   35295   16387   360803    22.0 |  0.957 % |
c ==============================================================================
c [1mFound solution: 16907[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28555 |   65762   155572 |   21920   16694   370898    22.2 |  0.957 % |
c |     28656 |   65762   155572 |   24112   16795   371787    22.1 |  0.961 % |
c |     28806 |   65762   155572 |   26523   16945   379975    22.4 |  0.961 % |
c |     29032 |   65762   155572 |   29175   17171   391110    22.8 |  0.961 % |
c |     29370 |   65762   155572 |   32093   17509   398260    22.7 |  0.961 % |
c |     29880 |   65762   155572 |   35302   18019   411778    22.9 |  0.961 % |
c |     30642 |   65762   155572 |   38832   18781   425455    22.7 |  0.961 % |
c |     31781 |   65762   155572 |   42715   19920   453683    22.8 |  0.961 % |
c |     33489 |   65762   155572 |   46987   21628   513146    23.7 |  0.961 % |
c ==============================================================================
c [1mFound solution: 16902[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34835 |   65773   155599 |   21924   22974   566569    24.7 |  0.961 % |
c |     34935 |   65773   155599 |   24116   11587   244904    21.1 |  0.966 % |
c |     35086 |   65773   155599 |   26528   11738   249448    21.3 |  0.966 % |
c |     35311 |   65773   155599 |   29180   11963   256318    21.4 |  0.966 % |
c ==============================================================================
c [1mFound solution: 16901[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35476 |   65784   155626 |   21928   12128   261340    21.5 |  0.966 % |
c |     35576 |   65730   155506 |   24120   12216   261805    21.4 |  1.035 % |
c |     35728 |   65730   155506 |   26532   12368   265241    21.4 |  1.035 % |
c |     35954 |   65674   155378 |   29186   12565   270020    21.5 |  1.115 % |
c |     36292 |   65674   155378 |   32104   12903   276462    21.4 |  1.115 % |
c |     36798 |   65674   155378 |   35315   13409   298309    22.2 |  1.115 % |
c |     37557 |   65674   155378 |   38846   14168   311424    22.0 |  1.115 % |
c |     38698 |   65674   155378 |   42731   15309   360852    23.6 |  1.115 % |
c |     40408 |   65674   155378 |   47004   17019   404347    23.8 |  1.115 % |
c |     42970 |   65674   155378 |   51705   19581   574460    29.3 |  1.115 % |
c ==============================================================================
c [1mFound solution: 16900[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     44987 |   65654   155339 |   21884   21593   617833    28.6 |  1.115 % |
c |     45087 |   65654   155339 |   24072   21693   618682    28.5 |  1.161 % |
c |     45237 |   65654   155339 |   26479   21843   621005    28.4 |  1.161 % |
c |     45462 |   65654   155339 |   29127   22068   625008    28.3 |  1.161 % |
c ==============================================================================
c [1mFound solution: 16898[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45771 |   65666   155369 |   21888   22377   638968    28.6 |  1.161 % |
c |     45871 |   65666   155369 |   24076   11289   277568    24.6 |  1.166 % |
c |     46021 |   65666   155369 |   26484   11439   282273    24.7 |  1.166 % |
c ==============================================================================
c [1mFound solution: 16897[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     46145 |   65682   155409 |   21894   11563   286748    24.8 |  1.166 % |
c |     46247 |   65682   155409 |   24083   11665   289346    24.8 |  1.170 % |
c |     46397 |   65682   155409 |   26491   11815   293241    24.8 |  1.170 % |
c |     46622 |   65682   155409 |   29140   12040   298503    24.8 |  1.170 % |
c |     46960 |   65682   155409 |   32055   12378   305688    24.7 |  1.170 % |
c ==============================================================================
c [1mFound solution: 16886[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     47128 |   65688   155423 |   21896   12546   309689    24.7 |  1.170 % |
c |     47228 |   65688   155423 |   24085   12646   312198    24.7 |  1.175 % |
c |     47378 |   65688   155423 |   26494   12796   314829    24.6 |  1.175 % |
c |     47603 |   65688   155423 |   29143   13021   322217    24.7 |  1.175 % |
c |     47941 |   65688   155423 |   32057   13359   330788    24.8 |  1.175 % |
c ==============================================================================
c [1mFound solution: 16885[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     48223 |   65698   155449 |   21899   13641   340258    24.9 |  1.175 % |
c |     48324 |   65698   155449 |   24088   13742   343752    25.0 |  1.179 % |
c |     48474 |   65698   155449 |   26497   13892   351300    25.3 |  1.179 % |
c |     48699 |   65698   155449 |   29147   14117   356238    25.2 |  1.179 % |
c |     49036 |   65698   155449 |   32062   14454   365752    25.3 |  1.179 % |
c ==============================================================================
c [1mFound solution: 16854[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     49500 |   65706   155469 |   21902   14918   389574    26.1 |  1.179 % |
c |     49600 |   65706   155469 |   24092   15018   393107    26.2 |  1.184 % |
c |     49750 |   65706   155469 |   26501   15168   395631    26.1 |  1.184 % |
c |     49975 |   65706   155469 |   29151   15393   401562    26.1 |  1.184 % |
c |     50313 |   65706   155469 |   32066   15731   412993    26.3 |  1.184 % |
c |     50819 |   65706   155469 |   35273   16237   427069    26.3 |  1.184 % |
c ==============================================================================
c [1mFound solution: 16358[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     51294 |   65730   155529 |   21910   16712   445136    26.6 |  1.184 % |
c |     51394 |   65730   155529 |   24101   16812   446848    26.6 |  1.202 % |
c |     51546 |   65730   155529 |   26511   16964   449176    26.5 |  1.202 % |
c |     51771 |   65730   155529 |   29162   17189   450751    26.2 |  1.202 % |
c |     52111 |   65730   155529 |   32078   17529   459606    26.2 |  1.202 % |
c |     52618 |   65730   155529 |   35286   18036   475658    26.4 |  1.202 % |
c |     53377 |   65730   155529 |   38814   18795   499386    26.6 |  1.202 % |
c |     54516 |   65730   155529 |   42696   19934   517720    26.0 |  1.202 % |
c |     56224 |   65730   155529 |   46966   21642   598612    27.7 |  1.202 % |
c |     58786 |   65730   155529 |   51662   24204   660203    27.3 |  1.202 % |
c |     62630 |   65730   155529 |   56828   28048   785927    28.0 |  1.202 % |
c |     68396 |   65730   155529 |   62511   33814  1250834    37.0 |  1.202 % |
c |     77045 |   65718   155503 |   68762   42461  1822979    42.9 |  1.216 % |
c ==============================================================================
c [1mFound solution: 16356[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     78426 |   65732   155539 |   21910   43842  1850126    42.2 |  1.216 % |
c |     78526 |   65732   155539 |   24101   20856   867131    41.6 |  1.220 % |
c |     78676 |   65732   155539 |   26511   21006   872525    41.5 |  1.220 % |
c |     78901 |   65732   155539 |   29162   21231   882001    41.5 |  1.220 % |
c |     79238 |   65732   155539 |   32078   21568   888978    41.2 |  1.220 % |
c |     79744 |   65732   155539 |   35286   22074   918313    41.6 |  1.220 % |
c |     80503 |   65732   155539 |   38814   22833   969096    42.4 |  1.220 % |
c |     81643 |   65732   155539 |   42696   23973   998521    41.7 |  1.220 % |
c |     83351 |   65732   155539 |   46966   25681  1097070    42.7 |  1.220 % |
c |     85913 |   65732   155539 |   51662   28243  1156585    41.0 |  1.220 % |
c |     89761 |   65732   155539 |   56828   32091  1251537    39.0 |  1.220 % |
c ==============================================================================
c [1mFound solution: 16352[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     92358 |   65752   155589 |   21917   34688  1365557    39.4 |  1.220 % |
c |     92458 |   65752   155589 |   24108   17444   334367    19.2 |  1.224 % |
c |     92609 |   65752   155589 |   26519   17595   337457    19.2 |  1.224 % |
c |     92834 |   65752   155589 |   29171   17820   342329    19.2 |  1.224 % |
c |     93171 |   65752   155589 |   32088   18157   354048    19.5 |  1.224 % |
c |     93678 |   65752   155589 |   35297   18664   367124    19.7 |  1.224 % |
c |     94438 |   65752   155589 |   38827   19424   406586    20.9 |  1.224 % |
c |     95579 |   65752   155589 |   42710   20565   436781    21.2 |  1.224 % |
c |     97287 |   65752   155589 |   46981   22273   518782    23.3 |  1.224 % |
c ==============================================================================
c [1mFound solution: 16350[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     97572 |   65762   155615 |   21920   22558   535861    23.8 |  1.224 % |
c |     97673 |   65762   155615 |   24112   11380   206729    18.2 |  1.229 % |
c |     97823 |   65762   155615 |   26523   11530   209009    18.1 |  1.229 % |
c |     98051 |   65762   155615 |   29175   11758   214968    18.3 |  1.229 % |
c |     98388 |   65762   155615 |   32093   12095   225574    18.7 |  1.229 % |
c |     98894 |   65762   155615 |   35302   12601   234985    18.6 |  1.229 % |
c |     99654 |   65762   155615 |   38832   13361   262080    19.6 |  1.229 % |
c |    100793 |   65762   155615 |   42715   14500   313906    21.6 |  1.229 % |
c |    102501 |   65762   155615 |   46987   16208   340816    21.0 |  1.229 % |
c |    105063 |   65762   155615 |   51686   18770   438547    23.4 |  1.229 % |
c ==============================================================================
c [1mFound solution: 16086[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    106484 |   65775   155646 |   21925   20191   489352    24.2 |  1.229 % |
c |    106584 |   65775   155646 |   24117   20291   490124    24.2 |  1.233 % |
c |    106736 |   65752   155596 |   26529   20349   490585    24.1 |  1.266 % |
c |    106962 |   65752   155596 |   29182   20575   497601    24.2 |  1.266 % |
c |    107301 |   65752   155596 |   32100   20914   505889    24.2 |  1.266 % |
c |    107809 |   65752   155596 |   35310   21422   518305    24.2 |  1.266 % |
c |    108569 |   65752   155596 |   38841   22182   599160    27.0 |  1.266 % |
c ==============================================================================
c [1mFound solution: 16034[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    109173 |   65768   155634 |   21922   22786   610881    26.8 |  1.266 % |
c |    109273 |   65768   155634 |   24114   11493   211076    18.4 |  1.270 % |
c |    109423 |   65768   155634 |   26525   11643   214691    18.4 |  1.270 % |
c |    109648 |   65768   155634 |   29178   11868   224125    18.9 |  1.270 % |
c |    109986 |   65768   155634 |   32096   12206   241069    19.8 |  1.270 % |
c |    110492 |   65768   155634 |   35305   12712   260849    20.5 |  1.270 % |
c |    111251 |   65768   155634 |   38836   13471   311267    23.1 |  1.270 % |
c ==============================================================================
c [1mFound solution: 16018[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    111701 |   65785   155675 |   21928   13921   324318    23.3 |  1.270 % |
c |    111802 |   65785   155675 |   24120   14022   328067    23.4 |  1.274 % |
c |    111952 |   65785   155675 |   26532   14172   332695    23.5 |  1.274 % |
c |    112177 |   65785   155675 |   29186   14397   341943    23.8 |  1.274 % |
c |    112516 |   65785   155675 |   32104   14736   360705    24.5 |  1.274 % |
c |    113023 |   65785   155675 |   35315   15243   374103    24.5 |  1.274 % |
c |    113783 |   65785   155675 |   38846   16003   385451    24.1 |  1.274 % |
c |    114922 |   65785   155675 |   42731   17142   448585    26.2 |  1.274 % |
c |    116630 |   65785   155675 |   47004   18850   546247    29.0 |  1.274 % |
c |    119192 |   65785   155675 |   51705   21412   683109    31.9 |  1.274 % |
c ==============================================================================
c [1mFound solution: 15974[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    122546 |   65799   155709 |   21933   24766   742648    30.0 |  1.274 % |
c |    122647 |   65799   155709 |   24126   12484   197983    15.9 |  1.279 % |
c |    122797 |   65799   155709 |   26538   12634   200073    15.8 |  1.279 % |
c |    123022 |   65799   155709 |   29192   12859   204681    15.9 |  1.279 % |
c |    123362 |   65799   155709 |   32112   13199   213850    16.2 |  1.279 % |
c |    123868 |   65799   155709 |   35323   13705   235879    17.2 |  1.279 % |
c |    124627 |   65799   155709 |   38855   14464   274626    19.0 |  1.279 % |
c |    125766 |   65799   155709 |   42741   15603   357729    22.9 |  1.279 % |
c |    127474 |   65799   155709 |   47015   17311   415801    24.0 |  1.279 % |
c ==============================================================================
c [1mFound solution: 15958[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    128652 |   65803   155719 |   21934   18489   449780    24.3 |  1.279 % |
c |    128752 |   65803   155719 |   24127   18589   451857    24.3 |  1.283 % |
c |    128902 |   65803   155719 |   26540   18739   458747    24.5 |  1.283 % |
c |    129128 |   65803   155719 |   29194   18965   464560    24.5 |  1.283 % |
c |    129466 |   65803   155719 |   32113   19303   467894    24.2 |  1.283 % |
c |    129978 |   65592   155234 |   35324   19792   487968    24.7 |  1.557 % |
c |    130737 |   65574   155195 |   38857   20546   537124    26.1 |  1.581 % |
c |    131876 |   65574   155195 |   42743   21685   599563    27.6 |  1.581 % |
c |    133584 |   65574   155195 |   47017   23393   638830    27.3 |  1.581 % |
c |    136146 |   65574   155195 |   51719   25955   750430    28.9 |  1.581 % |
c ==============================================================================
c [1mFound solution: 15814[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    136856 |   65583   155218 |   21861   26665   803572    30.1 |  1.581 % |
c |    136957 |   65583   155218 |   24047   13434   274814    20.5 |  1.585 % |
c |    137107 |   65583   155218 |   26451   13584   282870    20.8 |  1.585 % |
c |    137333 |   65583   155218 |   29096   13810   288513    20.9 |  1.585 % |
c |    137670 |   65583   155218 |   32006   14147   296134    20.9 |  1.585 % |
c |    138176 |   65583   155218 |   35207   14653   320733    21.9 |  1.585 % |
c |    138937 |   65583   155218 |   38728   15414   341154    22.1 |  1.585 % |
c |    140079 |   65583   155218 |   42600   16556   404007    24.4 |  1.585 % |
c |    141788 |   65583   155218 |   46860   18265   442711    24.2 |  1.585 % |
c |    144350 |   65583   155218 |   51547   20827   495810    23.8 |  1.585 % |
c |    148195 |   65583   155218 |   56701   24672   585721    23.7 |  1.585 % |
c |    153961 |   65583   155218 |   62371   30438  1172474    38.5 |  1.585 % |
c |    162610 |   65563   155174 |   68609   39083  1814744    46.4 |  1.608 % |
c |    175584 |   65563   155174 |   75470   52057  2316020    44.5 |  1.608 % |
c |    195046 |   65563   155174 |   83017   71519  3488775    48.8 |  1.608 % |
c |    224238 |   65563   155174 |   91318   27869  2434896    87.4 |  1.608 % |
c |    268027 |   65560   155168 |  100450   71657  4324177    60.3 |  1.613 % |
c |    333712 |   65560   155168 |  110495   51481  3823993    74.3 |  1.613 % |
c |    432239 |   65560   155168 |  121545   56446  2324776    41.2 |  1.613 % |
#### 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.90 0.98 0.93 2/54 9444
Raw data (stat): 9444 (runsolver) R 9443 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 548399261 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.91 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 2364 0 0 0 993 6 0 0 25 0 1 0 548399261 12337152 2286 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3012 2286 603 41 0 2971 0
vsize: 12048
[startup+20.0007 s]
Raw data (loadavg): 0.93 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 2549 0 0 0 1992 7 0 0 25 0 1 0 548399261 13176832 2471 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3217 2471 603 41 0 3176 0
vsize: 12868
[startup+30.0004 s]
Raw data (loadavg): 0.94 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 2751 0 0 0 2991 8 0 0 25 0 1 0 548399261 14073856 2673 4294967295 134512640 134672761 3221224544 3221223680 134560640 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3436 2673 603 41 0 3395 0
vsize: 13744
[startup+40.0004 s]
Raw data (loadavg): 0.95 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 2972 0 0 0 3989 9 0 0 25 0 1 0 548399261 14876672 2894 4294967295 134512640 134672761 3221224544 3221223692 1074732966 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3632 2894 603 41 0 3591 0
vsize: 14528
[startup+50.0008 s]
Raw data (loadavg): 0.95 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 3030 0 0 0 4989 9 0 0 25 0 1 0 548399261 15142912 2952 4294967295 134512640 134672761 3221224544 3221223648 134560326 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3697 2952 603 41 0 3656 0
vsize: 14788
[startup+60.0005 s]
Raw data (loadavg): 0.96 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 3030 0 0 0 5989 10 0 0 25 0 1 0 548399261 15142912 2952 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3697 2952 603 41 0 3656 0
vsize: 14788
[startup+70.0016 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 3101 0 0 0 6989 10 0 0 25 0 1 0 548399261 15413248 3023 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3763 3023 603 41 0 3722 0
vsize: 15052
[startup+80.002 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 3112 0 0 0 7989 10 0 0 25 0 1 0 548399261 15413248 3034 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3763 3034 603 41 0 3722 0
vsize: 15052
[startup+90.0017 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 3201 0 0 0 8988 11 0 0 25 0 1 0 548399261 15814656 3123 4294967295 134512640 134672761 3221224544 3221223680 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3861 3123 603 41 0 3820 0
vsize: 15444
[startup+100.002 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 3202 0 0 0 9987 12 0 0 25 0 1 0 548399261 15814656 3124 4294967295 134512640 134672761 3221224544 3221223760 134557650 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3861 3124 603 41 0 3820 0
vsize: 15444
[startup+110.002 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 3333 0 0 0 10987 12 0 0 25 0 1 0 548399261 16355328 3255 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3993 3255 603 41 0 3952 0
vsize: 15972
[startup+120.003 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 3705 0 0 0 11986 13 0 0 25 0 1 0 548399261 17838080 3627 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4355 3627 603 41 0 4314 0
vsize: 17420
[startup+130.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 4066 0 0 0 12985 15 0 0 25 0 1 0 548399261 19435520 3988 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4745 3988 603 41 0 4704 0
vsize: 18980
[startup+140.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 4451 0 0 0 13984 16 0 0 25 0 1 0 548399261 21028864 4373 4294967295 134512640 134672761 3221224544 3221223648 134560347 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5134 4373 603 41 0 5093 0
vsize: 20536
[startup+150.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 4621 0 0 0 14983 17 0 0 25 0 1 0 548399261 21692416 4543 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5296 4543 603 41 0 5255 0
vsize: 21184
[startup+160.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 4621 0 0 0 15983 17 0 0 25 0 1 0 548399261 21692416 4543 4294967295 134512640 134672761 3221224544 3221223728 134559041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5296 4543 603 41 0 5255 0
vsize: 21184
[startup+170.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 4621 0 0 0 16983 17 0 0 25 0 1 0 548399261 21692416 4543 4294967295 134512640 134672761 3221224544 3221223648 134560408 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5296 4543 603 41 0 5255 0
vsize: 21184
[startup+180.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 4621 0 0 0 17983 17 0 0 25 0 1 0 548399261 21692416 4543 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5296 4543 603 41 0 5255 0
vsize: 21184
[startup+190.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 4621 0 0 0 18983 18 0 0 25 0 1 0 548399261 21692416 4543 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5296 4543 603 41 0 5255 0
vsize: 21184
[startup+200.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 4621 0 0 0 19983 18 0 0 25 0 1 0 548399261 21692416 4543 4294967295 134512640 134672761 3221224544 3221223680 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5296 4543 603 41 0 5255 0
vsize: 21184
[startup+210.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 4621 0 0 0 20984 18 0 0 25 0 1 0 548399261 21692416 4543 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5296 4543 603 41 0 5255 0
vsize: 21184
[startup+220.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 4623 0 0 0 21984 18 0 0 25 0 1 0 548399261 21692416 4545 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5296 4545 603 41 0 5255 0
vsize: 21184
[startup+230.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 4624 0 0 0 22984 18 0 0 25 0 1 0 548399261 21692416 4546 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5296 4546 603 41 0 5255 0
vsize: 21184
[startup+240.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 4624 0 0 0 23984 18 0 0 25 0 1 0 548399261 21692416 4546 4294967295 134512640 134672761 3221224544 3221223728 134559028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5296 4546 603 41 0 5255 0
vsize: 21184
[startup+250.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 4624 0 0 0 24984 18 0 0 25 0 1 0 548399261 21692416 4546 4294967295 134512640 134672761 3221224544 3221223712 134561086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5296 4546 603 41 0 5255 0
vsize: 21184
[startup+260.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 4624 0 0 0 25984 18 0 0 25 0 1 0 548399261 21692416 4546 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5296 4546 603 41 0 5255 0
vsize: 21184
[startup+270.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 4624 0 0 0 26984 18 0 0 25 0 1 0 548399261 21692416 4546 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5296 4546 603 41 0 5255 0
vsize: 21184
[startup+280.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 4624 0 0 0 27984 18 0 0 25 0 1 0 548399261 21692416 4546 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5296 4546 603 41 0 5255 0
vsize: 21184
[startup+290.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 4837 0 0 0 28983 19 0 0 25 0 1 0 548399261 22622208 4759 4294967295 134512640 134672761 3221224544 3221223668 134566122 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5523 4759 603 41 0 5482 0
vsize: 22092
[startup+300.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 5087 0 0 0 29983 20 0 0 25 0 1 0 548399261 23547904 5009 4294967295 134512640 134672761 3221224544 3221223648 134560506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5749 5009 603 41 0 5708 0
vsize: 22996
[startup+310.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 5379 0 0 0 30982 21 0 0 25 0 1 0 548399261 24764416 5301 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6046 5301 603 41 0 6005 0
vsize: 24184
[startup+320.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 5610 0 0 0 31982 22 0 0 25 0 1 0 548399261 25690112 5532 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6272 5532 603 41 0 6231 0
vsize: 25088
[startup+330.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 5854 0 0 0 32981 23 0 0 25 0 1 0 548399261 26607616 5776 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6496 5776 603 41 0 6455 0
vsize: 25984
[startup+340.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 6108 0 0 0 33980 23 0 0 25 0 1 0 548399261 27664384 6030 4294967295 134512640 134672761 3221224544 3221223648 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6754 6030 603 41 0 6713 0
vsize: 27016
[startup+350.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 6328 0 0 0 34980 24 0 0 25 0 1 0 548399261 28856320 6250 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7045 6250 603 41 0 7004 0
vsize: 28180
[startup+360.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 6534 0 0 0 35980 24 0 0 25 0 1 0 548399261 29646848 6456 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7238 6456 603 41 0 7197 0
vsize: 28952
[startup+370.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 6762 0 0 0 36980 24 0 0 25 0 1 0 548399261 30588928 6684 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7468 6684 603 41 0 7427 0
vsize: 29872
[startup+380.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 7064 0 0 0 37979 25 0 0 25 0 1 0 548399261 31911936 6986 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7791 6986 603 41 0 7750 0
vsize: 31164
[startup+390.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 7356 0 0 0 38978 26 0 0 25 0 1 0 548399261 33116160 7278 4294967295 134512640 134672761 3221224544 3221223648 134554910 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8085 7278 603 41 0 8044 0
vsize: 32340
[startup+400.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 7645 0 0 0 39978 27 0 0 25 0 1 0 548399261 34181120 7567 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8345 7567 603 41 0 8304 0
vsize: 33380
[startup+410.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 7955 0 0 0 40977 28 0 0 25 0 1 0 548399261 35500032 7877 4294967295 134512640 134672761 3221224544 3221223728 134558851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8667 7877 603 41 0 8626 0
vsize: 34668
[startup+420.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 8278 0 0 0 41976 29 0 0 25 0 1 0 548399261 36835328 8200 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8993 8200 603 41 0 8952 0
vsize: 35972
[startup+430.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 8611 0 0 0 42976 30 0 0 25 0 1 0 548399261 38170624 8533 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9319 8533 603 41 0 9278 0
vsize: 37276
[startup+440.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 8940 0 0 0 43975 31 0 0 25 0 1 0 548399261 39579648 8862 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9663 8862 603 41 0 9622 0
vsize: 38652
[startup+450.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 9304 0 0 0 44974 32 0 0 25 0 1 0 548399261 41050112 9226 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10022 9226 603 41 0 9981 0
vsize: 40088
[startup+460.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 9648 0 0 0 45973 33 0 0 25 0 1 0 548399261 42414080 9570 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10355 9570 603 41 0 10314 0
vsize: 41420
[startup+470.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 9990 0 0 0 46973 34 0 0 25 0 1 0 548399261 43847680 9912 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10705 9912 603 41 0 10664 0
vsize: 42820
[startup+480.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 10332 0 0 0 47972 34 0 0 25 0 1 0 548399261 45182976 10254 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11064 10255 603 41 0 11023 0
vsize: 44124
[startup+490.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 10443 0 0 0 48972 35 0 0 25 0 1 0 548399261 45711360 10365 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11160 10365 603 41 0 11119 0
vsize: 44640
[startup+500.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 10443 0 0 0 49972 35 0 0 25 0 1 0 548399261 45711360 10365 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11160 10365 603 41 0 11119 0
vsize: 44640
[startup+510.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 10443 0 0 0 50971 35 0 0 25 0 1 0 548399261 45711360 10365 4294967295 134512640 134672761 3221224544 3221223712 134561115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11160 10365 603 41 0 11119 0
vsize: 44640
[startup+520.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 10443 0 0 0 51972 35 0 0 25 0 1 0 548399261 45711360 10365 4294967295 134512640 134672761 3221224544 3221223680 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11160 10365 603 41 0 11119 0
vsize: 44640
[startup+530.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 10443 0 0 0 52972 35 0 0 25 0 1 0 548399261 45711360 10365 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11160 10365 603 41 0 11119 0
vsize: 44640
[startup+540.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 10443 0 0 0 53972 35 0 0 25 0 1 0 548399261 45711360 10365 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11160 10365 603 41 0 11119 0
vsize: 44640
[startup+550.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 10452 0 0 0 54972 36 0 0 25 0 1 0 548399261 45711360 10374 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11160 10374 603 41 0 11119 0
vsize: 44640
[startup+560.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 10463 0 0 0 55972 36 0 0 25 0 1 0 548399261 45887488 10385 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11203 10385 603 41 0 11162 0
vsize: 44812
[startup+570.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 10474 0 0 0 56972 36 0 0 25 0 1 0 548399261 45887488 10396 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11203 10396 603 41 0 11162 0
vsize: 44812
[startup+580.016 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 10504 0 0 0 57973 36 0 0 25 0 1 0 548399261 46051328 10426 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11243 10426 603 41 0 11202 0
vsize: 44972
[startup+590.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 10510 0 0 0 58973 36 0 0 25 0 1 0 548399261 46051328 10432 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11243 10432 603 41 0 11202 0
vsize: 44972
[startup+600.018 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 10510 0 0 0 59973 36 0 0 25 0 1 0 548399261 46051328 10432 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11243 10432 603 41 0 11202 0
vsize: 44972
[startup+610.018 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 10510 0 0 0 60973 36 0 0 25 0 1 0 548399261 46051328 10432 4294967295 134512640 134672761 3221224544 3221223728 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11243 10432 603 41 0 11202 0
vsize: 44972
[startup+620.019 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 10510 0 0 0 61973 36 0 0 25 0 1 0 548399261 46051328 10432 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11243 10432 603 41 0 11202 0
vsize: 44972
[startup+630.018 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 10510 0 0 0 62974 36 0 0 25 0 1 0 548399261 46051328 10432 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11243 10432 603 41 0 11202 0
vsize: 44972
[startup+640.018 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 10510 0 0 0 63974 36 0 0 25 0 1 0 548399261 46051328 10432 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11243 10432 603 41 0 11202 0
vsize: 44972
[startup+650.018 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 10510 0 0 0 64974 36 0 0 25 0 1 0 548399261 46051328 10432 4294967295 134512640 134672761 3221224544 3221223728 134559327 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11243 10432 603 41 0 11202 0
vsize: 44972
[startup+660.023 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 10510 0 0 0 65974 36 0 0 25 0 1 0 548399261 46051328 10432 4294967295 134512640 134672761 3221224544 3221223648 134560036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11243 10432 603 41 0 11202 0
vsize: 44972
[startup+670.037 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 10510 0 0 0 66976 36 0 0 25 0 1 0 548399261 46051328 10432 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11243 10432 603 41 0 11202 0
vsize: 44972
[startup+680.037 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 10512 0 0 0 67976 37 0 0 25 0 1 0 548399261 46051328 10434 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11243 10434 603 41 0 11202 0
vsize: 44972
[startup+690.036 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 10514 0 0 0 68975 37 0 0 25 0 1 0 548399261 46051328 10436 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11243 10436 603 41 0 11202 0
vsize: 44972
[startup+700.057 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 10517 0 0 0 69977 37 0 0 25 0 1 0 548399261 46051328 10439 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11243 10439 603 41 0 11202 0
vsize: 44972
[startup+710.082 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 10618 0 0 0 70980 37 0 0 25 0 1 0 548399261 46452736 10540 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11341 10540 603 41 0 11300 0
vsize: 45364
[startup+720.081 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 10891 0 0 0 71979 39 0 0 25 0 1 0 548399261 47525888 10813 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11603 10813 603 41 0 11562 0
vsize: 46412
[startup+730.093 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11093 0 0 0 72979 40 0 0 25 0 1 0 548399261 48324608 11015 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11798 11015 603 41 0 11757 0
vsize: 47192
[startup+740.101 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11100 0 0 0 73980 40 0 0 25 0 1 0 548399261 48324608 11022 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11798 11022 603 41 0 11757 0
vsize: 47192
[startup+750.101 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11100 0 0 0 74980 40 0 0 25 0 1 0 548399261 48324608 11022 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11798 11022 603 41 0 11757 0
vsize: 47192
[startup+760.101 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11100 0 0 0 75980 40 0 0 25 0 1 0 548399261 48324608 11022 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11798 11022 603 41 0 11757 0
vsize: 47192
[startup+770.101 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11100 0 0 0 76980 40 0 0 25 0 1 0 548399261 48324608 11022 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11798 11022 603 41 0 11757 0
vsize: 47192
[startup+780.109 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11100 0 0 0 77981 40 0 0 25 0 1 0 548399261 48324608 11022 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11798 11022 603 41 0 11757 0
vsize: 47192
[startup+790.109 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11100 0 0 0 78981 40 0 0 25 0 1 0 548399261 48324608 11022 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11798 11022 603 41 0 11757 0
vsize: 47192
[startup+800.109 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11100 0 0 0 79981 41 0 0 25 0 1 0 548399261 48324608 11022 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11798 11022 603 41 0 11757 0
vsize: 47192
[startup+810.109 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11100 0 0 0 80981 41 0 0 25 0 1 0 548399261 48324608 11022 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11798 11022 603 41 0 11757 0
vsize: 47192
[startup+820.11 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11100 0 0 0 81981 41 0 0 25 0 1 0 548399261 48324608 11022 4294967295 134512640 134672761 3221224544 3221223680 134560625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11798 11022 603 41 0 11757 0
vsize: 47192
[startup+830.109 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11100 0 0 0 82981 41 0 0 25 0 1 0 548399261 48324608 11022 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11798 11022 603 41 0 11757 0
vsize: 47192
[startup+840.112 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11100 0 0 0 83982 41 0 0 25 0 1 0 548399261 48324608 11022 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11798 11022 603 41 0 11757 0
vsize: 47192
[startup+850.121 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11100 0 0 0 84981 41 0 0 25 0 1 0 548399261 48324608 11022 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11798 11022 603 41 0 11757 0
vsize: 47192
[startup+860.128 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11100 0 0 0 85982 41 0 0 25 0 1 0 548399261 48324608 11022 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11798 11022 603 41 0 11757 0
vsize: 47192
[startup+870.143 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11100 0 0 0 86984 41 0 0 25 0 1 0 548399261 48324608 11022 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11798 11022 603 41 0 11757 0
vsize: 47192
[startup+880.143 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11100 0 0 0 87984 41 0 0 25 0 1 0 548399261 48324608 11022 4294967295 134512640 134672761 3221224544 3221223712 134561269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11798 11022 603 41 0 11757 0
vsize: 47192
[startup+890.143 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11100 0 0 0 88984 41 0 0 25 0 1 0 548399261 48324608 11022 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11798 11022 603 41 0 11757 0
vsize: 47192
[startup+900.144 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11100 0 0 0 89984 41 0 0 25 0 1 0 548399261 48324608 11022 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11798 11022 603 41 0 11757 0
vsize: 47192
[startup+910.144 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11100 0 0 0 90985 41 0 0 25 0 1 0 548399261 48324608 11022 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11798 11022 603 41 0 11757 0
vsize: 47192
[startup+920.149 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11100 0 0 0 91985 41 0 0 25 0 1 0 548399261 48324608 11022 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11798 11022 603 41 0 11757 0
vsize: 47192
[startup+930.149 s]
Raw data (loadavg): 1.07 1.00 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11101 0 0 0 92985 41 0 0 25 0 1 0 548399261 48324608 11023 4294967295 134512640 134672761 3221224544 3221223700 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11798 11023 603 41 0 11757 0
vsize: 47192
[startup+940.152 s]
Raw data (loadavg): 1.06 1.00 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11101 0 0 0 93986 41 0 0 25 0 1 0 548399261 48324608 11023 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11798 11023 603 41 0 11757 0
vsize: 47192
[startup+950.155 s]
Raw data (loadavg): 1.05 1.00 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11118 0 0 0 94986 41 0 0 25 0 1 0 548399261 48578560 11040 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11860 11040 603 41 0 11819 0
vsize: 47440
[startup+960.16 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11119 0 0 0 95987 41 0 0 25 0 1 0 548399261 48578560 11041 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11860 11041 603 41 0 11819 0
vsize: 47440
[startup+970.175 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11119 0 0 0 96988 42 0 0 25 0 1 0 548399261 48578560 11041 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11860 11041 603 41 0 11819 0
vsize: 47440
[startup+980.187 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11119 0 0 0 97990 42 0 0 25 0 1 0 548399261 48578560 11041 4294967295 134512640 134672761 3221224544 3221223712 134560954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11860 11041 603 41 0 11819 0
vsize: 47440
[startup+990.187 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11119 0 0 0 98990 42 0 0 25 0 1 0 548399261 48578560 11041 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11860 11041 603 41 0 11819 0
vsize: 47440
[startup+1000.19 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11119 0 0 0 99990 42 0 0 25 0 1 0 548399261 48578560 11041 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11860 11041 603 41 0 11819 0
vsize: 47440
[startup+1010.19 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11119 0 0 0 100990 42 0 0 25 0 1 0 548399261 48578560 11041 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11860 11041 603 41 0 11819 0
vsize: 47440
[startup+1020.19 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11119 0 0 0 101991 42 0 0 25 0 1 0 548399261 48578560 11041 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11860 11041 603 41 0 11819 0
vsize: 47440
[startup+1030.19 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11120 0 0 0 102991 42 0 0 25 0 1 0 548399261 48578560 11042 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11860 11042 603 41 0 11819 0
vsize: 47440
[startup+1040.19 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11122 0 0 0 103991 42 0 0 25 0 1 0 548399261 48578560 11044 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11860 11044 603 41 0 11819 0
vsize: 47440
[startup+1050.19 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11238 0 0 0 104991 42 0 0 25 0 1 0 548399261 49033216 11160 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11971 11160 603 41 0 11930 0
vsize: 47884
[startup+1060.19 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11384 0 0 0 105990 43 0 0 25 0 1 0 548399261 49623040 11306 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12115 11306 603 41 0 12074 0
vsize: 48460
[startup+1070.19 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11497 0 0 0 106991 43 0 0 25 0 1 0 548399261 50020352 11419 4294967295 134512640 134672761 3221224544 3221223648 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12212 11419 603 41 0 12171 0
vsize: 48848
[startup+1080.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11497 0 0 0 107991 43 0 0 25 0 1 0 548399261 50020352 11419 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12212 11419 603 41 0 12171 0
vsize: 48848
[startup+1090.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11497 0 0 0 108991 43 0 0 25 0 1 0 548399261 50020352 11419 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12212 11419 603 41 0 12171 0
vsize: 48848
[startup+1100.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 9444
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11497 0 0 0 109991 43 0 0 25 0 1 0 548399261 50020352 11419 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12212 11419 603 41 0 12171 0
vsize: 48848
[startup+1110.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 9497
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11497 0 0 0 110990 43 0 0 25 0 1 0 548399261 50020352 11419 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12212 11419 603 41 0 12171 0
vsize: 48848
[startup+1120.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 9497
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11497 0 0 0 111991 43 0 0 25 0 1 0 548399261 50020352 11419 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12212 11419 603 41 0 12171 0
vsize: 48848
[startup+1130.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 9497
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11497 0 0 0 112991 43 0 0 25 0 1 0 548399261 50020352 11419 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12212 11419 603 41 0 12171 0
vsize: 48848
[startup+1140.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 9497
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11497 0 0 0 113991 44 0 0 25 0 1 0 548399261 50020352 11419 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12212 11419 603 41 0 12171 0
vsize: 48848
[startup+1150.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 9497
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11497 0 0 0 114991 44 0 0 25 0 1 0 548399261 50020352 11419 4294967295 134512640 134672761 3221224544 3221223648 134555105 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12212 11419 603 41 0 12171 0
vsize: 48848
[startup+1160.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 9497
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11497 0 0 0 115991 44 0 0 25 0 1 0 548399261 50020352 11419 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12212 11419 603 41 0 12171 0
vsize: 48848
[startup+1170.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 9499
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11497 0 0 0 116991 44 0 0 25 0 1 0 548399261 50020352 11419 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12212 11419 603 41 0 12171 0
vsize: 48848
[startup+1180.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 9499
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11497 0 0 0 117991 44 0 0 25 0 1 0 548399261 50020352 11419 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12212 11419 603 41 0 12171 0
vsize: 48848
[startup+1190.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 9499
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11497 0 0 0 118991 44 0 0 25 0 1 0 548399261 50020352 11419 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12212 11419 603 41 0 12171 0
vsize: 48848
[startup+1200.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 9499
Raw data (stat): 9444 (minisat+) R 9443 26298 26297 0 -1 0 11497 0 0 0 119991 44 0 0 25 0 1 0 548399261 50020352 11419 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12212 11419 603 41 0 12171 0
vsize: 48848
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.23 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 9499
Raw data (stat): 9444 (minisat+) Z 9443 26298 26297 0 -1 12 11500 0 0 0 119991 46 0 0 25 0 1 0 548399261 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.23
CPU time (s): 1200.38
CPU user time (s): 1199.92
CPU system time (s): 0.466929
CPU usage (%): 100.013
Max. virtual memory (Kb): 48848
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####