PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-neos5.opb
MD5SUM	4f5f6e30a602f3968daa9ca41c7da043
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2058
Optimality of the best value was proved	NO
Number of terms in the objective function	133
Biggest coefficient in the objective function	128
Number of bits for the biggest coefficient in the objective function	8
Sum of the numbers in the objective function	9334
Number of bits of the sum of numbers in the objective function	14
Biggest number in a constraint	1024
Number of bits of the biggest number in a constraint	11
Biggest sum of numbers in a constraint	9334
Number of bits of the biggest sum of numbers	14
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.05284
Number of variables	133
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	81
Trace number 14621

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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:        631348 kB
Buffers:         21844 kB
Cached:         353448 kB
SwapCached:          0 kB
Active:         106632 kB
Inactive:       271848 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        631096 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           7220 kB
Slab:            19004 kB
Committed_AS:    92808 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 00:45:21 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 19721 7 1200.21 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:    7
c ---[  71]---> BDD-cost:    7
c ---[  70]---> BDD-cost:    7
c ---[  69]---> BDD-cost:    7
c ---[  68]---> BDD-cost:    7
c ---[  67]---> BDD-cost:    7
c ---[  66]---> BDD-cost:    7
c ---[  65]---> BDD-cost:    7
c ---[  64]---> BDD-cost:    7
c ---[  63]---> BDD-cost:    7
c ---[  62]---> Sorter-cost:  382     Base:
c ---[  61]---> Sorter-cost:  717     Base: 2 2 2 2 2 2 2
c ---[  60]---> Sorter-cost:  417     Base: 2 2 2 2 2 2 2
c ---[  59]---> Sorter-cost: 1147     Base: 2 2 2 2 2 2 2
c ---[  58]---> Sorter-cost:  868     Base: 2 2 2 2 2 2 2
c ---[  57]---> Sorter-cost:  429     Base: 2 2 2 2 2 2 2
c ---[  56]---> Sorter-cost:  989     Base: 2 2 2 2 2 2 2
c ---[  55]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2
c ---[  54]---> Sorter-cost:  898     Base: 2 2 2 2 2 2 2
c ---[  53]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2
c ---[  52]---> Sorter-cost: 1011     Base: 2 2 2 2 2 2 2
c ---[  51]---> Sorter-cost:  216     Base:
c ---[  50]---> Sorter-cost:  856     Base: 2 2 2 2 2 2 2
c ---[  49]---> Sorter-cost: 1043     Base: 2 2 2 2 2 2 2
c ---[  48]---> Sorter-cost:  488     Base: 2 2 2 2 2 2 2
c ---[  47]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2
c ---[  46]---> Sorter-cost:  373     Base: 2 2 2 2 2 2 2
c ---[  45]---> Sorter-cost:  405     Base: 2 2 2 2 2 2 2
c ---[  44]---> Sorter-cost:  343     Base: 2 2 2 2 2 2 2
c ---[  43]---> Sorter-cost:  365     Base: 2 2 2 2 2 2 2
c ---[  42]---> Sorter-cost:  397     Base: 2 2 2 2 2 2 2
c ---[  41]---> Sorter-cost:  379     Base: 2 2 2 2 2 2 2
c ---[  40]---> Sorter-cost:  351     Base: 2 2 2 2 2 2 2
c ---[  39]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2
c ---[  38]---> Sorter-cost:  955     Base: 2 2 2 2 2 2 2
c ---[  37]---> Sorter-cost:  345     Base: 2 2 2 2 2 2 2
c ---[  36]---> Sorter-cost:  365     Base: 2 2 2 2 2 2 2
c ---[  35]---> Sorter-cost:  397     Base: 2 2 2 2 2 2 2
c ---[  34]---> Sorter-cost:  379     Base: 2 2 2 2 2 2 2
c ---[  33]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2
c ---[  32]---> Sorter-cost:  969     Base: 2 2 2 2 2 2 2
c ---[  31]---> Sorter-cost:  405     Base: 2 2 2 2 2 2 2
c ---[  30]---> Sorter-cost:  417     Base: 2 2 2 2 2 2 2
c ---[  29]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2
c ---[  28]---> Sorter-cost:  828     Base: 2 2 2 2 2 2 2
c ---[  27]---> Sorter-cost: 1013     Base: 2 2 2 2 2 2 2
c ---[  26]---> Sorter-cost:  337     Base: 2 2 2 2 2 2 2
c ---[  25]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2
c ---[  24]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2
c ---[  23]---> Sorter-cost:  365     Base: 2 2 2 2 2 2 2
c ---[  22]---> Sorter-cost:  397     Base: 2 2 2 2 2 2 2
c ---[  21]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2
c ---[  20]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2
c ---[  19]---> Sorter-cost:  365     Base: 2 2 2 2 2 2 2
c ---[  18]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2
c ---[  17]---> Sorter-cost:  397     Base: 2 2 2 2 2 2 2
c ---[  16]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2
c ---[  15]---> Sorter-cost:  355     Base: 2 2 2 2 2 2 2
c ---[  14]---> Sorter-cost:  387     Base: 2 2 2 2 2 2 2
c ---[  13]---> Sorter-cost:  389     Base: 2 2 2 2 2 2 2
c ---[  12]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2
c ---[  11]---> Sorter-cost:  810     Base: 2 2 2 2 2 2 2
c ---[  10]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2
c ---[   9]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2
c ---[   8]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2
c ---[   7]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2
c ---[   6]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2
c ---[   5]---> Sorter-cost:  355     Base: 2 2 2 2 2 2 2
c ---[   4]---> Sorter-cost:  387     Base: 2 2 2 2 2 2 2
c ---[   3]---> Sorter-cost:  319     Base: 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
c ---[   0]---> Sorter-cost:  301     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   51069   120750 |   17023       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 2722[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 2068     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        65 |   56239   132928 |   18746      65      252     3.9 |  0.000 % |
c |       166 |   56239   132928 |   20620     166     1269     7.6 |  0.443 % |
c |       316 |   56239   132928 |   22682     316     2023     6.4 |  0.443 % |
c |       541 |   56209   132861 |   24950     522     4232     8.1 |  0.493 % |
c |       878 |   56209   132861 |   27446     859    10977    12.8 |  0.493 % |
c ==============================================================================
c [1mFound solution: 2721[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1029 |   56269   133021 |   18756    1010    12605    12.5 |  0.493 % |
c |      1129 |   56250   132979 |   20631    1109    13436    12.1 |  0.525 % |
c |      1282 |   56250   132979 |   22694    1262    15225    12.1 |  0.525 % |
c ==============================================================================
c [1mFound solution: 2710[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1450 |   56261   133008 |   18753    1430    16784    11.7 |  0.525 % |
c ==============================================================================
c [1mFound solution: 2706[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1479 |   56270   133031 |   18756    1459    17252    11.8 |  0.525 % |
c |      1579 |   56253   132993 |   20631    1536    17716    11.5 |  0.563 % |
c ==============================================================================
c [1mFound solution: 2702[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1583 |   56268   133030 |   18756    1540    17769    11.5 |  0.563 % |
c ==============================================================================
c [1mFound solution: 2678[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1588 |   56283   133067 |   18761    1545    17811    11.5 |  0.563 % |
c ==============================================================================
c [1mFound solution: 2646[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1612 |   56293   133091 |   18764    1569    18042    11.5 |  0.563 % |
c ==============================================================================
c [1mFound solution: 2550[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1635 |   56317   133150 |   18772    1592    18265    11.5 |  0.563 % |
c |      1735 |   56317   133150 |   20649    1692    19260    11.4 |  0.595 % |
c ==============================================================================
c [1mFound solution: 2549[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1869 |   56333   133192 |   18777    1826    20770    11.4 |  0.595 % |
c |      1969 |   56326   133177 |   20654    1922    21376    11.1 |  0.612 % |
c ==============================================================================
c [1mFound solution: 2518[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2084 |   56330   133187 |   18776    2037    22191    10.9 |  0.612 % |
c ==============================================================================
c [1mFound solution: 2438[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2140 |   56340   133213 |   18780    2093    22875    10.9 |  0.612 % |
c |      2241 |   56340   133213 |   20658    2194    26623    12.1 |  0.622 % |
c ==============================================================================
c [1mFound solution: 2437[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2340 |   56351   133242 |   18783    2293    27386    11.9 |  0.622 % |
c ==============================================================================
c [1mFound solution: 2436[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2393 |   56371   133294 |   18790    2346    27843    11.9 |  0.622 % |
c |      2493 |   56371   133294 |   20669    2446    28684    11.7 |  0.633 % |
c ==============================================================================
c [1mFound solution: 2435[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2525 |   56381   133320 |   18793    2478    28967    11.7 |  0.633 % |
c |      2628 |   56381   133320 |   20672    2581    29851    11.6 |  0.638 % |
c |      2779 |   56381   133320 |   22739    2732    31738    11.6 |  0.638 % |
c |      3004 |   56381   133320 |   25013    2957    35374    12.0 |  0.638 % |
c |      3341 |   56381   133320 |   27514    3294    38704    11.7 |  0.638 % |
c ==============================================================================
c [1mFound solution: 2434[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3429 |   56387   133336 |   18795    3382    40387    11.9 |  0.638 % |
c |      3530 |   56387   133336 |   20674    3483    40973    11.8 |  0.644 % |
c |      3680 |   56381   133324 |   22741    3630    42181    11.6 |  0.655 % |
c ==============================================================================
c [1mFound solution: 2433[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3819 |   56387   133340 |   18795    3769    43111    11.4 |  0.655 % |
c ==============================================================================
c [1mFound solution: 2432[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3832 |   56400   133373 |   18800    3782    43201    11.4 |  0.655 % |
c |      3932 |   56289   133122 |   20680    3827    43685    11.4 |  0.840 % |
c |      4083 |   56289   133122 |   22748    3978    45869    11.5 |  0.840 % |
c |      4308 |   56289   133122 |   25022    4203    50025    11.9 |  0.840 % |
c ==============================================================================
c [1mFound solution: 2408[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4434 |   56296   133143 |   18765    4328    50990    11.8 |  0.840 % |
c |      4534 |   56296   133143 |   20641    4428    52127    11.8 |  0.867 % |
c |      4685 |   56296   133143 |   22705    4579    54687    11.9 |  0.867 % |
c ==============================================================================
c [1mFound solution: 2310[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4833 |   56298   133150 |   18766    4720    56365    11.9 |  0.867 % |
c ==============================================================================
c [1mFound solution: 2302[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4867 |   56305   133169 |   18768    4754    56930    12.0 |  0.867 % |
c |      4967 |   56305   133169 |   20644    4854    57730    11.9 |  0.894 % |
c |      5118 |   56305   133169 |   22709    5005    59986    12.0 |  0.894 % |
c |      5345 |   56305   133169 |   24980    5232    65048    12.4 |  0.894 % |
c |      5682 |   56305   133169 |   27478    5569    69073    12.4 |  0.894 % |
c ==============================================================================
c [1mFound solution: 2301[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5738 |   56316   133198 |   18772    5625    69976    12.4 |  0.894 % |
c |      5840 |   56316   133198 |   20649    5727    71701    12.5 |  0.899 % |
c |      5992 |   56316   133198 |   22714    5879    75052    12.8 |  0.899 % |
c |      6217 |   56316   133198 |   24985    6104    77066    12.6 |  0.899 % |
c ==============================================================================
c [1mFound solution: 2276[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6404 |   56352   133285 |   18784    6291    78883    12.5 |  0.899 % |
c |      6504 |   56352   133285 |   20662    6391    80140    12.5 |  0.926 % |
c ==============================================================================
c [1mFound solution: 2275[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6620 |   56368   133325 |   18789    6507    83592    12.8 |  0.926 % |
c |      6720 |   56368   133325 |   20667    6607    84277    12.8 |  0.931 % |
c |      6870 |   56368   133325 |   22734    6757    85848    12.7 |  0.931 % |
c |      7095 |   56368   133325 |   25008    6982    88054    12.6 |  0.931 % |
c ==============================================================================
c [1mFound solution: 2261[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7279 |   56381   133356 |   18793    7166    90811    12.7 |  0.931 % |
c |      7380 |   56381   133356 |   20672    7267    92217    12.7 |  0.936 % |
c |      7530 |   56381   133356 |   22739    7417    94677    12.8 |  0.936 % |
c ==============================================================================
c [1mFound solution: 2260[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7613 |   56394   133387 |   18798    7500    95566    12.7 |  0.936 % |
c |      7714 |   56394   133387 |   20677    7601    97562    12.8 |  0.941 % |
c |      7865 |   56394   133387 |   22745    7752    99600    12.8 |  0.941 % |
c |      8090 |   56394   133387 |   25020    7977   101863    12.8 |  0.941 % |
c |      8427 |   56394   133387 |   27522    8314   106997    12.9 |  0.941 % |
c |      8936 |   56394   133387 |   30274    8823   116681    13.2 |  0.941 % |
c ==============================================================================
c [1mFound solution: 2230[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8991 |   56402   133407 |   18800    8878   117756    13.3 |  0.941 % |
c |      9091 |   56402   133407 |   20680    8978   119615    13.3 |  0.947 % |
c |      9241 |   56402   133407 |   22748    9128   124610    13.7 |  0.946 % |
c ==============================================================================
c [1mFound solution: 2228[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9364 |   56410   133427 |   18803    9251   126240    13.6 |  0.946 % |
c |      9465 |   56410   133427 |   20683    9352   128440    13.7 |  0.952 % |
c |      9616 |   56410   133427 |   22751    9503   131755    13.9 |  0.952 % |
c |      9841 |   56342   133277 |   25026    9696   135290    14.0 |  1.044 % |
c |     10178 |   56342   133277 |   27529   10033   139900    13.9 |  1.044 % |
c |     10684 |   56270   133119 |   30282   10514   146227    13.9 |  1.142 % |
c ==============================================================================
c [1mFound solution: 2198[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10952 |   56127   132788 |   18709   10703   150175    14.0 |  1.142 % |
c |     11053 |   56127   132788 |   20579   10804   151588    14.0 |  1.370 % |
c ==============================================================================
c [1mFound solution: 2197[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11198 |   56132   132801 |   18710   10949   153658    14.0 |  1.370 % |
c |     11298 |   56118   132771 |   20581   11043   154730    14.0 |  1.397 % |
c ==============================================================================
c [1mFound solution: 2190[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11438 |   56114   132763 |   18704   11139   156386    14.0 |  1.397 % |
c ==============================================================================
c [1mFound solution: 2182[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11489 |   56118   132773 |   18706   11190   156754    14.0 |  1.397 % |
c ==============================================================================
c [1mFound solution: 2181[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11584 |   56127   132796 |   18709   11285   159357    14.1 |  1.397 % |
c ==============================================================================
c [1mFound solution: 2180[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11620 |   56135   132816 |   18711   11321   159878    14.1 |  1.397 % |
c |     11720 |   56135   132816 |   20582   11421   163275    14.3 |  1.440 % |
c ==============================================================================
c [1mFound solution: 2179[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11760 |   56143   132836 |   18714   11461   164254    14.3 |  1.440 % |
c |     11862 |   56118   132780 |   20585   11537   164600    14.3 |  1.483 % |
c ==============================================================================
c [1mFound solution: 2178[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12009 |   56126   132800 |   18708   11684   167494    14.3 |  1.483 % |
c ==============================================================================
c [1mFound solution: 2130[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12093 |   56143   132841 |   18714   11768   170573    14.5 |  1.483 % |
c |     12193 |   56143   132841 |   20585   11868   172184    14.5 |  1.493 % |
c |     12344 |   56143   132841 |   22643   12019   174487    14.5 |  1.493 % |
c |     12570 |   56143   132841 |   24908   12245   178468    14.6 |  1.493 % |
c |     12907 |   56143   132841 |   27399   12582   193043    15.3 |  1.493 % |
c |     13413 |   56121   132793 |   30139   13084   199767    15.3 |  1.521 % |
c ==============================================================================
c [1mFound solution: 2129[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13733 |   56134   132824 |   18711   13404   213640    15.9 |  1.521 % |
c |     13834 |   56134   132824 |   20582   13505   216196    16.0 |  1.526 % |
c |     13984 |   56134   132824 |   22640   13655   220579    16.2 |  1.526 % |
c |     14210 |   56115   132773 |   24904   13880   224949    16.2 |  1.531 % |
c ==============================================================================
c [1mFound solution: 2128[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14462 |   56127   132801 |   18709   14132   236076    16.7 |  1.531 % |
c |     14563 |   55881   132243 |   20579   14149   237606    16.8 |  1.927 % |
c |     14713 |   55881   132243 |   22637   14299   242870    17.0 |  1.927 % |
c |     14939 |   55881   132243 |   24901   14525   251117    17.3 |  1.927 % |
c |     15277 |   55881   132243 |   27391   14863   260973    17.6 |  1.927 % |
c |     15783 |   55881   132243 |   30131   15369   273749    17.8 |  1.927 % |
c ==============================================================================
c [1mFound solution: 2127[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16099 |   55893   132271 |   18631   15685   281867    18.0 |  1.927 % |
c |     16199 |   55893   132271 |   20494   15785   284467    18.0 |  1.932 % |
c ==============================================================================
c [1mFound solution: 2095[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16287 |   55900   132288 |   18633   15873   286516    18.1 |  1.932 % |
c |     16387 |   55900   132288 |   20496   15973   288729    18.1 |  1.937 % |
c |     16538 |   55900   132288 |   22545   16124   291879    18.1 |  1.937 % |
c |     16764 |   55900   132288 |   24800   16350   298781    18.3 |  1.937 % |
c ==============================================================================
c [1mFound solution: 2094[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16927 |   55907   132305 |   18635   16513   303113    18.4 |  1.937 % |
c |     17027 |   55879   132244 |   20498   16599   303785    18.3 |  1.985 % |
c |     17179 |   55879   132244 |   22548   16751   309586    18.5 |  1.985 % |
c ==============================================================================
c [1mFound solution: 2093[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17344 |   55890   132271 |   18630   16916   312387    18.5 |  1.985 % |
c |     17444 |   55890   132271 |   20493   17016   314691    18.5 |  1.990 % |
c |     17594 |   55890   132271 |   22542   17166   319330    18.6 |  1.990 % |
c |     17821 |   55890   132271 |   24796   17393   326591    18.8 |  1.990 % |
c |     18158 |   55834   132147 |   27276   17710   332246    18.8 |  2.066 % |
c ==============================================================================
c [1mFound solution: 2092[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18549 |   55848   132181 |   18616   18101   345828    19.1 |  2.066 % |
c |     18649 |   55848   132181 |   20477   18201   347469    19.1 |  2.071 % |
c |     18800 |   55848   132181 |   22525   18352   350688    19.1 |  2.071 % |
c |     19026 |   55848   132181 |   24777   18578   355973    19.2 |  2.071 % |
c |     19364 |   55848   132181 |   27255   18916   363565    19.2 |  2.071 % |
c |     19872 |   55848   132181 |   29981   19424   379789    19.6 |  2.071 % |
c ==============================================================================
c [1mFound solution: 2091[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20055 |   55859   132208 |   18619   19607   388328    19.8 |  2.071 % |
c |     20155 |   55859   132208 |   20480    9904   184596    18.6 |  2.076 % |
c |     20306 |   55859   132208 |   22528   10055   188588    18.8 |  2.076 % |
c |     20531 |   55859   132208 |   24781   10280   199667    19.4 |  2.076 % |
c ==============================================================================
c [1mFound solution: 2088[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20709 |   55867   132228 |   18622   10458   207500    19.8 |  2.076 % |
c |     20809 |   55867   132228 |   20484   10558   208663    19.8 |  2.081 % |
c |     20959 |   55867   132228 |   22532   10708   217357    20.3 |  2.081 % |
c |     21184 |   55867   132228 |   24785   10933   222891    20.4 |  2.081 % |
c |     21521 |   55867   132228 |   27264   11270   230250    20.4 |  2.081 % |
c ==============================================================================
c [1mFound solution: 2086[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21913 |   55877   132252 |   18625   11662   248335    21.3 |  2.081 % |
c |     22013 |   55877   132252 |   20487   11762   251356    21.4 |  2.086 % |
c |     22163 |   55877   132252 |   22536   11912   256358    21.5 |  2.086 % |
c |     22388 |   55877   132252 |   24789   12137   263654    21.7 |  2.086 % |
c |     22725 |   55877   132252 |   27268   12474   271263    21.7 |  2.086 % |
c ==============================================================================
c [1mFound solution: 2054[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23203 |   55880   132259 |   18626   12952   302393    23.3 |  2.086 % |
c |     23304 |   55880   132259 |   20488   13053   306819    23.5 |  2.091 % |
c |     23454 |   55880   132259 |   22537   13203   312901    23.7 |  2.091 % |
c |     23679 |   55880   132259 |   24791   13428   320616    23.9 |  2.091 % |
c |     24016 |   55880   132259 |   27270   13765   334894    24.3 |  2.091 % |
c ==============================================================================
c [1mFound solution: 2053[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24154 |   55883   132266 |   18627   13903   338961    24.4 |  2.091 % |
c |     24255 |   55883   132266 |   20489   14004   343159    24.5 |  2.097 % |
c ==============================================================================
c [1mFound solution: 2050[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24276 |   55886   132273 |   18628   14025   343714    24.5 |  2.097 % |
c ==============================================================================
c [1mFound solution: 2049[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24319 |   55893   132290 |   18631   14068   345000    24.5 |  2.097 % |
c |     24419 |   55893   132290 |   20494   14168   349182    24.6 |  2.107 % |
c |     24569 |   55893   132290 |   22543   14318   352619    24.6 |  2.107 % |
c |     24794 |   55893   132290 |   24797   14543   368848    25.4 |  2.107 % |
c ==============================================================================
c [1mFound solution: 2048[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25025 |   55901   132310 |   18633   14774   375946    25.4 |  2.107 % |
c |     25127 |   55901   132310 |   20496   14876   377247    25.4 |  2.112 % |
c |     25277 |   55901   132310 |   22545   15026   381322    25.4 |  2.112 % |
c |     25502 |   55901   132310 |   24800   15251   387718    25.4 |  2.112 % |
c |     25839 |   55901   132310 |   27280   15588   393728    25.3 |  2.112 % |
c |     26346 |   55901   132310 |   30008   16095   411248    25.6 |  2.112 % |
c |     27106 |   55874   132249 |   33009   16809   423567    25.2 |  2.150 % |
c |     28245 |   55874   132249 |   36310   17948   467399    26.0 |  2.150 % |
c |     29953 |   55874   132249 |   39941   19656   503529    25.6 |  2.150 % |
c |     32515 |   55874   132249 |   43935   22218   554373    25.0 |  2.150 % |
c |     36359 |   55874   132249 |   48329   26062   807868    31.0 |  2.150 % |
c |     42126 |   55874   132249 |   53162   31829   954060    30.0 |  2.150 % |
c ==============================================================================
c [1mFound solution: 2022[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     46344 |   55895   132300 |   18631   36047  1125554    31.2 |  2.150 % |
c |     46446 |   55895   132300 |   20494   18115   463801    25.6 |  2.170 % |
c |     46596 |   55895   132300 |   22543   18265   466560    25.5 |  2.170 % |
c |     46822 |   55895   132300 |   24797   18491   475206    25.7 |  2.170 % |
c |     47159 |   55895   132300 |   27277   18828   495885    26.3 |  2.170 % |
c |     47666 |   55895   132300 |   30005   19335   506618    26.2 |  2.170 % |
c |     48426 |   55895   132300 |   33005   20095   531880    26.5 |  2.170 % |
c |     49567 |   55895   132300 |   36306   21236   581714    27.4 |  2.170 % |
c |     51275 |   55895   132300 |   39937   22944   635670    27.7 |  2.170 % |
c |     53838 |   55895   132300 |   43930   25507   748872    29.4 |  2.170 % |
c ==============================================================================
c [1mFound solution: 2021[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     56145 |   55910   132337 |   18636   27814   834763    30.0 |  2.170 % |
c |     56247 |   55910   132337 |   20499   14009   353505    25.2 |  2.175 % |
c |     56397 |   55910   132337 |   22549   14159   362365    25.6 |  2.175 % |
c |     56623 |   55910   132337 |   24804   14385   368088    25.6 |  2.175 % |
c |     56963 |   55910   132337 |   27284   14725   376201    25.5 |  2.175 % |
c |     57469 |   55910   132337 |   30013   15231   386750    25.4 |  2.175 % |
c |     58228 |   55910   132337 |   33014   15990   416783    26.1 |  2.175 % |
c |     59368 |   55910   132337 |   36316   17130   460512    26.9 |  2.175 % |
c ==============================================================================
c [1mFound solution: 2020[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     59573 |   55914   132347 |   18638   17335   469091    27.1 |  2.175 % |
c |     59673 |   55914   132347 |   20501   17435   471436    27.0 |  2.180 % |
c |     59823 |   55914   132347 |   22551   17585   480501    27.3 |  2.180 % |
c |     60048 |   55914   132347 |   24807   17810   487693    27.4 |  2.180 % |
c |     60385 |   55901   132318 |   27287   18142   503249    27.7 |  2.202 % |
c |     60891 |   55889   132291 |   30016   18641   521846    28.0 |  2.218 % |
c ==============================================================================
c [1mFound solution: 2017[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     60934 |   55896   132308 |   18632   18684   523203    28.0 |  2.218 % |
c |     61034 |   55896   132308 |   20495   18784   530281    28.2 |  2.223 % |
c |     61184 |   55896   132308 |   22544   18934   534213    28.2 |  2.223 % |
c |     61414 |   55896   132308 |   24799   19164   537602    28.1 |  2.223 % |
c ==============================================================================
c [1mFound solution: 2006[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     61689 |   55900   132318 |   18633   19439   548484    28.2 |  2.223 % |
c |     61790 |   55900   132318 |   20496    9821   181030    18.4 |  2.228 % |
c |     61942 |   55900   132318 |   22545    9973   189363    19.0 |  2.228 % |
c |     62168 |   55900   132318 |   24800   10199   193305    19.0 |  2.228 % |
c |     62506 |   55685   131831 |   27280   10407   201536    19.4 |  2.585 % |
c |     63013 |   55685   131831 |   30008   10914   213456    19.6 |  2.585 % |
c |     63773 |   54658   129511 |   33009   11531   246080    21.3 |  4.126 % |
c |     64913 |   54630   129449 |   36310   12670   286459    22.6 |  4.164 % |
c |     66622 |   54630   129449 |   39941   14379   345827    24.1 |  4.164 % |
c |     69185 |   54593   129365 |   43935   16926   543164    32.1 |  4.229 % |
c |     73030 |   54593   129365 |   48329   20771   670363    32.3 |  4.229 % |
c ==============================================================================
c [1mFound solution: 2005[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     75611 |   54597   129375 |   18199   23352   851765    36.5 |  4.229 % |
c |     75711 |   54597   129375 |   20018   11776   337231    28.6 |  4.234 % |
c |     75861 |   54597   129375 |   22020   11926   339998    28.5 |  4.234 % |
c |     76090 |   54597   129375 |   24222   12155   346435    28.5 |  4.234 % |
c |     76427 |   54597   129375 |   26645   12492   356026    28.5 |  4.234 % |
c |     76934 |   54561   129295 |   29309   12997   372802    28.7 |  4.283 % |
c ==============================================================================
c [1mFound solution: 2004[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     77198 |   54565   129305 |   18188   13261   383427    28.9 |  4.283 % |
c |     77298 |   54475   129104 |   20006   13355   385202    28.8 |  4.412 % |
c |     77448 |   54475   129104 |   22007   13505   388994    28.8 |  4.412 % |
c |     77676 |   54475   129104 |   24208   13733   393942    28.7 |  4.412 % |
c |     78013 |   54475   129104 |   26629   14070   405870    28.8 |  4.412 % |
c |     78519 |   54475   129104 |   29291   14576   432502    29.7 |  4.412 % |
c ==============================================================================
c [1mFound solution: 2003[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     78600 |   54488   129135 |   18162   14657   435043    29.7 |  4.412 % |
c |     78700 |   54438   129022 |   19978   14750   438193    29.7 |  4.573 % |
c |     78850 |   54386   128906 |   21976   14898   439684    29.5 |  4.573 % |
c |     79076 |   54319   128757 |   24173   15014   440163    29.3 |  4.676 % |
c |     79415 |   54319   128757 |   26590   15353   450272    29.3 |  4.676 % |
c |     79924 |   54319   128757 |   29250   15862   474214    29.9 |  4.676 % |
c |     80685 |   54319   128757 |   32175   16623   527019    31.7 |  4.676 % |
c |     81825 |   54301   128718 |   35392   17762   564831    31.8 |  4.697 % |
c ==============================================================================
c [1mFound solution: 2001[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     82583 |   54305   128728 |   18101   18520   587254    31.7 |  4.697 % |
c |     82685 |   54305   128728 |   19911   18622   589467    31.7 |  4.702 % |
c |     82835 |   54305   128728 |   21902   18772   597267    31.8 |  4.702 % |
c |     83062 |   54305   128728 |   24092   18999   600770    31.6 |  4.702 % |
c |     83399 |   54305   128728 |   26501   19336   616927    31.9 |  4.702 % |
c |     83905 |   54260   128624 |   29151   19838   637021    32.1 |  4.767 % |
c ==============================================================================
c [1mFound solution: 2000[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     84167 |   54264   128634 |   18088   20100   644991    32.1 |  4.767 % |
c |     84267 |   54264   128634 |   19896   10150   179522    17.7 |  4.772 % |
c |     84417 |   54204   128500 |   21886   10297   183113    17.8 |  4.858 % |
c |     84642 |   54204   128500 |   24075   10522   197528    18.8 |  4.858 % |
c ==============================================================================
c [1mFound solution: 1999[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     84778 |   54208   128510 |   18069   10658   200647    18.8 |  4.858 % |
c |     84878 |   54208   128510 |   19875   10758   203845    18.9 |  4.863 % |
c |     85030 |   54208   128510 |   21863   10910   210403    19.3 |  4.863 % |
c |     85255 |   54192   128474 |   24049   11134   216421    19.4 |  4.890 % |
c |     85594 |   54192   128474 |   26454   11473   229773    20.0 |  4.890 % |
c ==============================================================================
c [1mFound solution: 1998[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     85686 |   54202   128498 |   18067   11565   233795    20.2 |  4.890 % |
c |     85786 |   54202   128498 |   19873   11665   236209    20.2 |  4.895 % |
c |     85939 |   54202   128498 |   21861   11818   242390    20.5 |  4.895 % |
c |     86164 |   54202   128498 |   24047   12043   252594    21.0 |  4.895 % |
c |     86501 |   54202   128498 |   26451   12380   274559    22.2 |  4.895 % |
c ==============================================================================
c [1mFound solution: 1997[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86647 |   54215   128529 |   18071   12526   278548    22.2 |  4.895 % |
c |     86747 |   54215   128529 |   19878   12626   280223    22.2 |  4.899 % |
c |     86898 |   54215   128529 |   21865   12777   285481    22.3 |  4.899 % |
c ==============================================================================
c [1mFound solution: 1996[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86953 |   54228   128560 |   18076   12832   287054    22.4 |  4.899 % |
c |     87053 |   54228   128560 |   19883   12932   290258    22.4 |  4.903 % |
c |     87206 |   54228   128560 |   21871   13085   294976    22.5 |  4.903 % |
c |     87431 |   54228   128560 |   24059   13310   299273    22.5 |  4.903 % |
c |     87769 |   54228   128560 |   26465   13648   307646    22.5 |  4.903 % |
c |     88276 |   54228   128560 |   29111   14155   323670    22.9 |  4.903 % |
c ==============================================================================
c [1mFound solution: 1990[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88841 |   54238   128584 |   18079   14720   344611    23.4 |  4.903 % |
c |     88942 |   54238   128584 |   19886   14821   347259    23.4 |  4.907 % |
c |     89092 |   54238   128584 |   21875   14971   356043    23.8 |  4.907 % |
c |     89317 |   54238   128584 |   24063   15196   364267    24.0 |  4.907 % |
c |     89654 |   54238   128584 |   26469   15533   384329    24.7 |  4.907 % |
c |     90160 |   54238   128584 |   29116   16039   406322    25.3 |  4.907 % |
c |     90921 |   54238   128584 |   32028   16800   448675    26.7 |  4.907 % |
c ==============================================================================
c [1mFound solution: 1988[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     91208 |   54248   128608 |   18082   17087   459999    26.9 |  4.907 % |
c |     91308 |   54248   128608 |   19890   17187   462490    26.9 |  4.912 % |
c |     91459 |   54248   128608 |   21879   17338   467854    27.0 |  4.912 % |
c |     91684 |   54248   128608 |   24067   17563   475025    27.0 |  4.911 % |
c |     92021 |   54248   128608 |   26473   17900   491068    27.4 |  4.912 % |
c |     92527 |   54214   128533 |   29121   18404   512937    27.9 |  4.955 % |
c |     93287 |   54214   128533 |   32033   19164   540218    28.2 |  4.955 % |
c |     94426 |   54214   128533 |   35236   20303   577770    28.5 |  4.955 % |
c ==============================================================================
c [1mFound solution: 1987[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     94886 |   54224   128557 |   18074   20763   590705    28.4 |  4.955 % |
c ==============================================================================
c [1mFound solution: 1985[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     94917 |   54234   128581 |   18078   10413   181302    17.4 |  4.955 % |
c |     95019 |   54234   128581 |   19885   10515   185797    17.7 |  4.963 % |
c |     95170 |   54234   128581 |   21874   10666   189785    17.8 |  4.963 % |
c |     95396 |   54234   128581 |   24061   10892   196351    18.0 |  4.963 % |
c |     95733 |   54234   128581 |   26467   11229   210107    18.7 |  4.963 % |
c |     96239 |   54234   128581 |   29114   11735   235168    20.0 |  4.963 % |
c |     96998 |   54234   128581 |   32026   12494   285596    22.9 |  4.963 % |
c |     98138 |   54234   128581 |   35228   13634   320560    23.5 |  4.963 % |
c |     99847 |   54234   128581 |   38751   15343   394088    25.7 |  4.963 % |
c ==============================================================================
c [1mFound solution: 1984[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    101645 |   54245   128608 |   18081   17141   435493    25.4 |  4.963 % |
c |    101745 |   54245   128608 |   19889   17241   438143    25.4 |  4.968 % |
c |    101895 |   54245   128608 |   21878   17391   443694    25.5 |  4.968 % |
c |    102120 |   54245   128608 |   24065   17616   452539    25.7 |  4.968 % |
c |    102457 |   54245   128608 |   26472   17953   463342    25.8 |  4.968 % |
c |    102963 |   54245   128608 |   29119   18459   485099    26.3 |  4.968 % |
c |    103722 |   54245   128608 |   32031   19218   540619    28.1 |  4.968 % |
c |    104861 |   54245   128608 |   35234   20357   575199    28.3 |  4.968 % |
c |    106571 |   54238   128593 |   38758   22065   607731    27.5 |  4.978 % |
c |    109135 |   54238   128593 |   42634   24629   717707    29.1 |  4.979 % |
c |    112980 |   54206   128520 |   46897   28472   816692    28.7 |  5.032 % |
c |    118749 |   54190   128484 |   51587   34239  1000737    29.2 |  5.059 % |
c |    127398 |   54190   128484 |   56745   42888  1440572    33.6 |  5.059 % |
c |    140372 |   54190   128484 |   62420   55862  2075467    37.2 |  5.059 % |
c |    159835 |   54074   128220 |   68662   33403  1234394    37.0 |  5.237 % |
c ==============================================================================
c [1mFound solution: 1942[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    170323 |   54075   128224 |   18025   43889  1819823    41.5 |  5.237 % |
c |    170424 |   54075   128224 |   19827   10955   239107    21.8 |  5.248 % |
c |    170574 |   54075   128224 |   21810   11105   245478    22.1 |  5.248 % |
c |    170799 |   54075   128224 |   23991   11330   255481    22.5 |  5.248 % |
c |    171136 |   54075   128224 |   26390   11667   272170    23.3 |  5.248 % |
c |    171642 |   54011   128081 |   29029   12168   292609    24.0 |  5.339 % |
c |    172401 |   54011   128081 |   31932   12927   327673    25.3 |  5.339 % |
c |    173540 |   54011   128081 |   35125   14066   408966    29.1 |  5.339 % |
c |    175248 |   54011   128081 |   38638   15774   547473    34.7 |  5.339 % |
c |    177811 |   53971   127990 |   42502   18333   671970    36.7 |  5.404 % |
c |    181655 |   53971   127990 |   46752   22177  1060538    47.8 |  5.404 % |
c |    187421 |   53971   127990 |   51427   27943  1287899    46.1 |  5.404 % |
c |    196070 |   53971   127990 |   56570   36592  1896054    51.8 |  5.404 % |
c |    209044 |   53968   127984 |   62227   49565  2778563    56.1 |  5.409 % |
c |    228506 |   53968   127984 |   68449   69027  4142129    60.0 |  5.409 % |
c |    257699 |   53959   127964 |   75294   47544  2481247    52.2 |  5.426 % |
c |    301488 |   53959   127964 |   82824   33931  1760512    51.9 |  5.426 % |
c |    367173 |   53959   127964 |   91106   35790  2194668    61.3 |  5.426 % |
#### 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.85 0.94 0.91 2/56 16728
Raw data (stat): 16728 (runsolver) R 16727 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 425665329 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99983 s]
Raw data (loadavg): 0.88 0.94 0.91 2/56 16728
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 2166 0 0 0 993 6 0 0 25 0 1 0 425665329 11313152 2088 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2762 2088 603 41 0 2721 0
vsize: 11048
[startup+19.9995 s]
Raw data (loadavg): 0.89 0.94 0.91 2/56 16728
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 2307 0 0 0 1992 6 0 0 25 0 1 0 425665329 11862016 2229 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2896 2229 603 41 0 2855 0
vsize: 11584
[startup+30.0003 s]
Raw data (loadavg): 0.91 0.94 0.91 2/56 16728
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 2497 0 0 0 2992 7 0 0 25 0 1 0 425665329 13017088 2419 4294967295 134512640 134672761 3221224544 3221223680 134560625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3178 2419 603 41 0 3137 0
vsize: 12712
[startup+40.0001 s]
Raw data (loadavg): 0.92 0.95 0.91 2/56 16728
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 2606 0 0 0 3991 7 0 0 25 0 1 0 425665329 13418496 2528 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3276 2528 603 41 0 3235 0
vsize: 13104
[startup+50.0009 s]
Raw data (loadavg): 0.93 0.95 0.91 2/56 16728
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 2645 0 0 0 4991 8 0 0 25 0 1 0 425665329 13553664 2567 4294967295 134512640 134672761 3221224544 3221223712 134560822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3309 2567 603 41 0 3268 0
vsize: 13236
[startup+60.0012 s]
Raw data (loadavg): 0.94 0.95 0.91 2/56 16728
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 2920 0 0 0 5991 8 0 0 25 0 1 0 425665329 14622720 2842 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3570 2842 603 41 0 3529 0
vsize: 14280
[startup+70.0015 s]
Raw data (loadavg): 0.95 0.95 0.91 2/56 16728
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 3282 0 0 0 6989 10 0 0 25 0 1 0 425665329 16084992 3204 4294967295 134512640 134672761 3221224544 3221223688 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3927 3204 603 41 0 3886 0
vsize: 15708
[startup+80.0023 s]
Raw data (loadavg): 0.96 0.95 0.91 2/56 16728
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 3527 0 0 0 7989 10 0 0 25 0 1 0 425665329 17154048 3449 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4188 3449 603 41 0 4147 0
vsize: 16752
[startup+90.0021 s]
Raw data (loadavg): 0.96 0.95 0.91 2/56 16728
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 3527 0 0 0 8989 11 0 0 25 0 1 0 425665329 17154048 3449 4294967295 134512640 134672761 3221224544 3221223648 134560226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4188 3449 603 41 0 4147 0
vsize: 16752
[startup+100.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/56 16728
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 3528 0 0 0 9989 11 0 0 25 0 1 0 425665329 17289216 3450 4294967295 134512640 134672761 3221224544 3221223844 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4221 3450 603 41 0 4180 0
vsize: 16884
[startup+110.011 s]
Raw data (loadavg): 0.97 0.95 0.91 2/56 16728
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 3528 0 0 0 10989 11 0 0 25 0 1 0 425665329 17289216 3450 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4221 3450 603 41 0 4180 0
vsize: 16884
[startup+120.011 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 16728
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 3528 0 0 0 11989 11 0 0 25 0 1 0 425665329 17289216 3450 4294967295 134512640 134672761 3221224544 3221223680 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4221 3450 603 41 0 4180 0
vsize: 16884
[startup+130.011 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 16728
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 3528 0 0 0 12989 12 0 0 25 0 1 0 425665329 17289216 3450 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4221 3450 603 41 0 4180 0
vsize: 16884
[startup+140.011 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 16728
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 3528 0 0 0 13988 12 0 0 25 0 1 0 425665329 17289216 3450 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4221 3450 603 41 0 4180 0
vsize: 16884
[startup+150.012 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 16728
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 3528 0 0 0 14988 12 0 0 25 0 1 0 425665329 17289216 3450 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4221 3450 603 41 0 4180 0
vsize: 16884
[startup+160.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 16728
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 3528 0 0 0 15988 12 0 0 25 0 1 0 425665329 17289216 3450 4294967295 134512640 134672761 3221224544 3221223728 134559611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4221 3450 603 41 0 4180 0
vsize: 16884
[startup+170.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 16728
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 3528 0 0 0 16988 13 0 0 25 0 1 0 425665329 17289216 3450 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4221 3450 603 41 0 4180 0
vsize: 16884
[startup+180.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 16728
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 3528 0 0 0 17988 13 0 0 25 0 1 0 425665329 17289216 3450 4294967295 134512640 134672761 3221224544 3221223728 134559028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4221 3450 603 41 0 4180 0
vsize: 16884
[startup+190.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 16728
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 3528 0 0 0 18988 13 0 0 25 0 1 0 425665329 17289216 3450 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4221 3450 603 41 0 4180 0
vsize: 16884
[startup+200.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 16728
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 3562 0 0 0 19988 13 0 0 25 0 1 0 425665329 17420288 3484 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4253 3484 603 41 0 4212 0
vsize: 17012
[startup+210.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 16728
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 3877 0 0 0 20987 14 0 0 25 0 1 0 425665329 18620416 3799 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4546 3799 603 41 0 4505 0
vsize: 18184
[startup+220.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 16728
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 4120 0 0 0 21987 15 0 0 25 0 1 0 425665329 19685376 4042 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4806 4042 603 41 0 4765 0
vsize: 19224
[startup+230.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 16728
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 4395 0 0 0 22985 16 0 0 25 0 1 0 425665329 20762624 4317 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5069 4317 603 41 0 5028 0
vsize: 20276
[startup+240.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16728
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 4784 0 0 0 23984 18 0 0 25 0 1 0 425665329 22241280 4706 4294967295 134512640 134672761 3221224544 3221223648 134560160 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5430 4706 603 41 0 5389 0
vsize: 21720
[startup+250.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16728
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 4976 0 0 0 24984 18 0 0 25 0 1 0 425665329 23048192 4898 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5627 4898 603 41 0 5586 0
vsize: 22508
[startup+260.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16728
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 5253 0 0 0 25983 19 0 0 25 0 1 0 425665329 24240128 5175 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5918 5175 603 41 0 5877 0
vsize: 23672
[startup+270.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16728
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 5363 0 0 0 26982 20 0 0 25 0 1 0 425665329 24633344 5285 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6014 5285 603 41 0 5973 0
vsize: 24056
[startup+280.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16728
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 5368 0 0 0 27982 20 0 0 25 0 1 0 425665329 24633344 5290 4294967295 134512640 134672761 3221224544 3221223680 134565149 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6014 5290 603 41 0 5973 0
vsize: 24056
[startup+290.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16730
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 5368 0 0 0 28982 20 0 0 25 0 1 0 425665329 24633344 5290 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6014 5290 603 41 0 5973 0
vsize: 24056
[startup+300.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16730
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 5368 0 0 0 29982 20 0 0 25 0 1 0 425665329 24633344 5290 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6014 5290 603 41 0 5973 0
vsize: 24056
[startup+310.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16730
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 5368 0 0 0 30983 20 0 0 25 0 1 0 425665329 24633344 5290 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6014 5290 603 41 0 5973 0
vsize: 24056
[startup+320.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16730
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 5368 0 0 0 31983 20 0 0 25 0 1 0 425665329 24633344 5290 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6014 5290 603 41 0 5973 0
vsize: 24056
[startup+330.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16730
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 5368 0 0 0 32983 20 0 0 25 0 1 0 425665329 24633344 5290 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6014 5290 603 41 0 5973 0
vsize: 24056
[startup+340.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16730
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 5368 0 0 0 33983 20 0 0 25 0 1 0 425665329 24633344 5290 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6014 5290 603 41 0 5973 0
vsize: 24056
[startup+350.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16730
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 5368 0 0 0 34983 20 0 0 25 0 1 0 425665329 24633344 5290 4294967295 134512640 134672761 3221224544 3221223728 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6014 5290 603 41 0 5973 0
vsize: 24056
[startup+360.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16730
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 5368 0 0 0 35983 20 0 0 25 0 1 0 425665329 24633344 5290 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6014 5290 603 41 0 5973 0
vsize: 24056
[startup+370.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16730
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 5368 0 0 0 36983 20 0 0 25 0 1 0 425665329 24633344 5290 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6014 5290 603 41 0 5973 0
vsize: 24056
[startup+380.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16730
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 5368 0 0 0 37984 20 0 0 25 0 1 0 425665329 24633344 5290 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6014 5290 603 41 0 5973 0
vsize: 24056
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16730
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 5433 0 0 0 38983 21 0 0 25 0 1 0 425665329 24895488 5355 4294967295 134512640 134672761 3221224544 3221223728 134558651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6078 5355 603 41 0 6037 0
vsize: 24312
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16730
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 5732 0 0 0 39983 22 0 0 25 0 1 0 425665329 26214400 5654 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6400 5654 603 41 0 6359 0
vsize: 25600
[startup+410.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16730
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 5943 0 0 0 40982 23 0 0 25 0 1 0 425665329 27037696 5865 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6601 5865 603 41 0 6560 0
vsize: 26404
[startup+420.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16730
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 6183 0 0 0 41981 24 0 0 25 0 1 0 425665329 28086272 6105 4294967295 134512640 134672761 3221224544 3221223648 134560350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6857 6105 603 41 0 6816 0
vsize: 27428
[startup+430.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16730
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 6429 0 0 0 42981 24 0 0 25 0 1 0 425665329 29011968 6351 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7083 6351 603 41 0 7042 0
vsize: 28332
[startup+440.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16730
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 6693 0 0 0 43980 25 0 0 25 0 1 0 425665329 30203904 6615 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7374 6615 603 41 0 7333 0
vsize: 29496
[startup+450.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16730
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 6957 0 0 0 44979 26 0 0 25 0 1 0 425665329 31522816 6879 4294967295 134512640 134672761 3221224544 3221223712 134561115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7696 6879 603 41 0 7655 0
vsize: 30784
[startup+460.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16730
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 7194 0 0 0 45979 27 0 0 25 0 1 0 425665329 32448512 7116 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7922 7116 603 41 0 7881 0
vsize: 31688
[startup+470.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16730
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 7385 0 0 0 46978 28 0 0 25 0 1 0 425665329 33247232 7307 4294967295 134512640 134672761 3221224544 3221223692 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8117 7307 603 41 0 8076 0
vsize: 32468
[startup+480.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16730
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 7548 0 0 0 47977 28 0 0 25 0 1 0 425665329 33902592 7470 4294967295 134512640 134672761 3221224544 3221223648 134554665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8277 7470 603 41 0 8236 0
vsize: 33108
[startup+490.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16730
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 7548 0 0 0 48977 28 0 0 25 0 1 0 425665329 33902592 7470 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8277 7470 603 41 0 8236 0
vsize: 33108
[startup+500.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16730
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 7548 0 0 0 49978 28 0 0 25 0 1 0 425665329 33902592 7470 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8277 7470 603 41 0 8236 0
vsize: 33108
[startup+510.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16730
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 7548 0 0 0 50978 28 0 0 25 0 1 0 425665329 33902592 7470 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8277 7470 603 41 0 8236 0
vsize: 33108
[startup+520.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16730
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 7548 0 0 0 51978 28 0 0 25 0 1 0 425665329 33902592 7470 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8277 7470 603 41 0 8236 0
vsize: 33108
[startup+530.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16730
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 7548 0 0 0 52978 28 0 0 25 0 1 0 425665329 33902592 7470 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8277 7470 603 41 0 8236 0
vsize: 33108
[startup+540.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16730
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 7557 0 0 0 53978 28 0 0 25 0 1 0 425665329 33902592 7479 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8277 7479 603 41 0 8236 0
vsize: 33108
[startup+550.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16730
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 7557 0 0 0 54979 28 0 0 25 0 1 0 425665329 33902592 7479 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8277 7479 603 41 0 8236 0
vsize: 33108
[startup+560.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16730
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 7557 0 0 0 55979 28 0 0 25 0 1 0 425665329 33902592 7479 4294967295 134512640 134672761 3221224544 3221223680 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8277 7479 603 41 0 8236 0
vsize: 33108
[startup+570.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16730
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 7557 0 0 0 56980 28 0 0 25 0 1 0 425665329 33902592 7479 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8277 7479 603 41 0 8236 0
vsize: 33108
[startup+580.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16730
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 7557 0 0 0 57980 28 0 0 25 0 1 0 425665329 33902592 7479 4294967295 134512640 134672761 3221224544 3221223648 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8277 7479 603 41 0 8236 0
vsize: 33108
[startup+590.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16732
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 7557 0 0 0 58980 28 0 0 25 0 1 0 425665329 33902592 7479 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8277 7479 603 41 0 8236 0
vsize: 33108
[startup+600.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16732
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 7557 0 0 0 59980 28 0 0 25 0 1 0 425665329 33902592 7479 4294967295 134512640 134672761 3221224544 3221223680 134565101 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8277 7479 603 41 0 8236 0
vsize: 33108
[startup+610.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16732
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 7557 0 0 0 60980 29 0 0 25 0 1 0 425665329 33902592 7479 4294967295 134512640 134672761 3221224544 3221223648 134560379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8277 7479 603 41 0 8236 0
vsize: 33108
[startup+620.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16732
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 7764 0 0 0 61979 29 0 0 25 0 1 0 425665329 34832384 7686 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8504 7686 603 41 0 8463 0
vsize: 34016
[startup+630.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16732
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 7977 0 0 0 62979 30 0 0 25 0 1 0 425665329 35635200 7899 4294967295 134512640 134672761 3221224544 3221223648 134560154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8700 7899 603 41 0 8659 0
vsize: 34800
[startup+640.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16732
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 8185 0 0 0 63978 31 0 0 25 0 1 0 425665329 36429824 8107 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8894 8107 603 41 0 8853 0
vsize: 35576
[startup+650.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16732
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 8467 0 0 0 64976 33 0 0 25 0 1 0 425665329 37638144 8389 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9189 8389 603 41 0 9148 0
vsize: 36756
[startup+660.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16732
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 8543 0 0 0 65976 33 0 0 25 0 1 0 425665329 38039552 8465 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9287 8465 603 41 0 9246 0
vsize: 37148
[startup+670.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16732
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 8543 0 0 0 66976 33 0 0 25 0 1 0 425665329 38039552 8465 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9287 8465 603 41 0 9246 0
vsize: 37148
[startup+680.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16732
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 8543 0 0 0 67976 33 0 0 25 0 1 0 425665329 38039552 8465 4294967295 134512640 134672761 3221224544 3221223728 134559041 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9287 8465 603 41 0 9246 0
vsize: 37148
[startup+690.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16732
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 8543 0 0 0 68976 33 0 0 25 0 1 0 425665329 38039552 8465 4294967295 134512640 134672761 3221224544 3221223712 134561266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9287 8465 603 41 0 9246 0
vsize: 37148
[startup+700.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16732
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 8549 0 0 0 69976 34 0 0 25 0 1 0 425665329 38039552 8471 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9287 8471 603 41 0 9246 0
vsize: 37148
[startup+710.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16732
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 8549 0 0 0 70976 34 0 0 25 0 1 0 425665329 38039552 8471 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9287 8471 603 41 0 9246 0
vsize: 37148
[startup+720.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16732
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 8561 0 0 0 71976 34 0 0 25 0 1 0 425665329 38039552 8483 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9287 8483 603 41 0 9246 0
vsize: 37148
[startup+730.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16732
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 8561 0 0 0 72976 34 0 0 25 0 1 0 425665329 38039552 8483 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9287 8483 603 41 0 9246 0
vsize: 37148
[startup+740.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16732
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 8562 0 0 0 73976 35 0 0 25 0 1 0 425665329 38039552 8484 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9287 8484 603 41 0 9246 0
vsize: 37148
[startup+750.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16732
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 8571 0 0 0 74976 35 0 0 25 0 1 0 425665329 38203392 8493 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9327 8493 603 41 0 9286 0
vsize: 37308
[startup+760.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16732
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 8572 0 0 0 75976 35 0 0 25 0 1 0 425665329 38203392 8494 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9327 8494 603 41 0 9286 0
vsize: 37308
[startup+770.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16732
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 8572 0 0 0 76976 35 0 0 25 0 1 0 425665329 38203392 8494 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9327 8494 603 41 0 9286 0
vsize: 37308
[startup+780.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16732
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 8594 0 0 0 77977 35 0 0 25 0 1 0 425665329 38203392 8516 4294967295 134512640 134672761 3221224544 3221223648 134560248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9327 8516 603 41 0 9286 0
vsize: 37308
[startup+790.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16732
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 8595 0 0 0 78977 35 0 0 25 0 1 0 425665329 38203392 8517 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9327 8517 603 41 0 9286 0
vsize: 37308
[startup+800.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16732
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 8595 0 0 0 79977 35 0 0 25 0 1 0 425665329 38203392 8517 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9327 8517 603 41 0 9286 0
vsize: 37308
[startup+810.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16732
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 8595 0 0 0 80977 35 0 0 25 0 1 0 425665329 38203392 8517 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9327 8517 603 41 0 9286 0
vsize: 37308
[startup+820.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16732
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 8595 0 0 0 81977 35 0 0 25 0 1 0 425665329 38203392 8517 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9327 8517 603 41 0 9286 0
vsize: 37308
[startup+830.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16732
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 8597 0 0 0 82977 35 0 0 25 0 1 0 425665329 38203392 8519 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9327 8519 603 41 0 9286 0
vsize: 37308
[startup+840.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16732
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 8884 0 0 0 83977 36 0 0 25 0 1 0 425665329 39395328 8806 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9618 8806 603 41 0 9577 0
vsize: 38472
[startup+850.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16732
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 9183 0 0 0 84975 37 0 0 25 0 1 0 425665329 40718336 9105 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9941 9105 603 41 0 9900 0
vsize: 39764
[startup+860.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16732
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 9411 0 0 0 85975 38 0 0 25 0 1 0 425665329 41525248 9333 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10138 9333 603 41 0 10097 0
vsize: 40552
[startup+870.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16732
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 9509 0 0 0 86975 38 0 0 25 0 1 0 425665329 41918464 9431 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10234 9431 603 41 0 10193 0
vsize: 40936
[startup+880.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16732
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 9509 0 0 0 87975 38 0 0 25 0 1 0 425665329 41918464 9431 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10234 9431 603 41 0 10193 0
vsize: 40936
[startup+890.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16734
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 9509 0 0 0 88974 39 0 0 25 0 1 0 425665329 41918464 9431 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10234 9431 603 41 0 10193 0
vsize: 40936
[startup+900.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16734
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 9509 0 0 0 89975 39 0 0 25 0 1 0 425665329 41918464 9431 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10234 9431 603 41 0 10193 0
vsize: 40936
[startup+910.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16734
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 9510 0 0 0 90975 39 0 0 25 0 1 0 425665329 41918464 9432 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10234 9432 603 41 0 10193 0
vsize: 40936
[startup+920.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16734
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 9510 0 0 0 91975 39 0 0 25 0 1 0 425665329 41918464 9432 4294967295 134512640 134672761 3221224544 3221223500 1075350790 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10234 9432 603 41 0 10193 0
vsize: 40936
[startup+930.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16734
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 9510 0 0 0 92974 39 0 0 25 0 1 0 425665329 41918464 9432 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10234 9432 603 41 0 10193 0
vsize: 40936
[startup+940.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16734
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 9515 0 0 0 93975 39 0 0 25 0 1 0 425665329 42065920 9437 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10270 9437 603 41 0 10229 0
vsize: 41080
[startup+950.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16734
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 9515 0 0 0 94974 39 0 0 25 0 1 0 425665329 42065920 9437 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10270 9437 603 41 0 10229 0
vsize: 41080
[startup+960.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16734
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 9515 0 0 0 95974 39 0 0 25 0 1 0 425665329 42065920 9437 4294967295 134512640 134672761 3221224544 3221223728 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10270 9437 603 41 0 10229 0
vsize: 41080
[startup+970.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16734
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 9515 0 0 0 96974 39 0 0 25 0 1 0 425665329 42065920 9437 4294967295 134512640 134672761 3221224544 3221223648 134560412 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10270 9437 603 41 0 10229 0
vsize: 41080
[startup+980.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16734
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 9515 0 0 0 97974 40 0 0 25 0 1 0 425665329 42065920 9437 4294967295 134512640 134672761 3221224544 3221223544 1075349851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10270 9437 603 41 0 10229 0
vsize: 41080
[startup+990.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16734
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 9515 0 0 0 98975 40 0 0 25 0 1 0 425665329 42065920 9437 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10270 9437 603 41 0 10229 0
vsize: 41080
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16734
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 9515 0 0 0 99975 40 0 0 25 0 1 0 425665329 42065920 9437 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10270 9437 603 41 0 10229 0
vsize: 41080
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16734
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 9515 0 0 0 100975 40 0 0 25 0 1 0 425665329 42065920 9437 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10270 9437 603 41 0 10229 0
vsize: 41080
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16734
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 9521 0 0 0 101975 40 0 0 25 0 1 0 425665329 42065920 9443 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10270 9443 603 41 0 10229 0
vsize: 41080
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16734
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 9521 0 0 0 102975 40 0 0 25 0 1 0 425665329 42065920 9443 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10270 9443 603 41 0 10229 0
vsize: 41080
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16734
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 9539 0 0 0 103975 40 0 0 25 0 1 0 425665329 42065920 9461 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10270 9461 603 41 0 10229 0
vsize: 41080
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16734
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 9542 0 0 0 104974 41 0 0 25 0 1 0 425665329 42229760 9464 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10310 9464 603 41 0 10269 0
vsize: 41240
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16734
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 9542 0 0 0 105975 41 0 0 25 0 1 0 425665329 42229760 9464 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10310 9464 603 41 0 10269 0
vsize: 41240
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16734
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 9542 0 0 0 106975 41 0 0 25 0 1 0 425665329 42229760 9464 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10310 9464 603 41 0 10269 0
vsize: 41240
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16734
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 9559 0 0 0 107975 41 0 0 25 0 1 0 425665329 42229760 9481 4294967295 134512640 134672761 3221224544 3221223744 134557800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10310 9481 603 41 0 10269 0
vsize: 41240
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16734
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 9560 0 0 0 108974 42 0 0 25 0 1 0 425665329 42229760 9482 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10310 9482 603 41 0 10269 0
vsize: 41240
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16734
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 9584 0 0 0 109974 42 0 0 25 0 1 0 425665329 42393600 9506 4294967295 134512640 134672761 3221224544 3221223648 134559916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10350 9506 603 41 0 10309 0
vsize: 41400
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16734
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 9653 0 0 0 110974 42 0 0 25 0 1 0 425665329 42663936 9575 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10416 9575 603 41 0 10375 0
vsize: 41664
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16734
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 9819 0 0 0 111973 43 0 0 25 0 1 0 425665329 43327488 9741 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10578 9741 603 41 0 10537 0
vsize: 42312
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16734
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 9996 0 0 0 112973 43 0 0 25 0 1 0 425665329 44122112 9918 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10772 9918 603 41 0 10731 0
vsize: 43088
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16734
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 10151 0 0 0 113973 43 0 0 25 0 1 0 425665329 44777472 10073 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10932 10073 603 41 0 10891 0
vsize: 43728
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16734
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 10309 0 0 0 114973 44 0 0 25 0 1 0 425665329 45445120 10231 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11095 10231 603 41 0 11054 0
vsize: 44380
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16734
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 10448 0 0 0 115972 45 0 0 25 0 1 0 425665329 45973504 10370 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10370 603 41 0 11183 0
vsize: 44896
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16734
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 10591 0 0 0 116972 45 0 0 25 0 1 0 425665329 46497792 10513 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11352 10513 603 41 0 11311 0
vsize: 45408
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16734
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 10743 0 0 0 117972 46 0 0 25 0 1 0 425665329 47185920 10665 4294967295 134512640 134672761 3221224544 3221223680 134560604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11520 10665 603 41 0 11479 0
vsize: 46080
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16736
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 10894 0 0 0 118971 46 0 0 25 0 1 0 425665329 47841280 10816 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11680 10816 603 41 0 11639 0
vsize: 46720
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16736
Raw data (stat): 16728 (minisat+) R 16727 12452 12451 0 -1 0 11021 0 0 0 119971 47 0 0 25 0 1 0 425665329 48373760 10943 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11810 10943 603 41 0 11769 0
vsize: 47240
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 1/56 16736
Raw data (stat): 16728 (minisat+) Z 16727 12452 12451 0 -1 12 11024 0 0 0 119971 49 0 0 25 0 1 0 425665329 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.07
CPU time (s): 1200.21
CPU user time (s): 1199.72
CPU system time (s): 0.491925
CPU usage (%): 100.012
Max. virtual memory (Kb): 47240
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####