PB'05 competition: run trace

Some explanations

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

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

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        729828 kB
Buffers:         31404 kB
Cached:         236640 kB
SwapCached:        624 kB
Active:          17844 kB
Inactive:       252424 kB
HighTotal:      131008 kB
HighFree:        40068 kB
LowTotal:       903652 kB
LowFree:        689760 kB
SwapTotal:     2097136 kB
SwapFree:      2095788 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5220 kB
Slab:            28828 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-20 21:23:22 (client local time) WITH STATUS 10 IN 1200.22 SECONDS
stats: 14713 7 1200.22 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]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  71]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  70]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  69]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  68]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  67]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  66]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  65]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  64]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  63]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  62]---> Adder-cost: 59   maxlim: 7   bits: 4/3
c ---[  61]---> Adder-cost: 117   maxlim: 7167   bits: 14/13
c ---[  60]---> Adder-cost: 45   maxlim: 7167   bits: 14/13
c ---[  59]---> Adder-cost: 149   maxlim: 7167   bits: 14/13
c ---[  58]---> Adder-cost: 137   maxlim: 7167   bits: 14/13
c ---[  57]---> Adder-cost: 47   maxlim: 7167   bits: 14/13
c ---[  56]---> Adder-cost: 143   maxlim: 7167   bits: 14/13
c ---[  55]---> Adder-cost: 135   maxlim: 7167   bits: 14/13
c ---[  54]---> Adder-cost: 139   maxlim: 7167   bits: 14/13
c ---[  53]---> Adder-cost: 49   maxlim: 7167   bits: 14/13
c ---[  52]---> Adder-cost: 149   maxlim: 7167   bits: 14/13
c ---[  51]---> Adder-cost: 43   maxlim: 7   bits: 4/3
c ---[  50]---> Adder-cost: 135   maxlim: 7167   bits: 14/13
c ---[  49]---> Adder-cost: 159   maxlim: 7167   bits: 14/13
c ---[  48]---> Adder-cost: 69   maxlim: 6143   bits: 14/13
c ---[  47]---> Adder-cost: 39   maxlim: 6143   bits: 14/13
c ---[  46]---> Adder-cost: 39   maxlim: 6143   bits: 14/13
c ---[  45]---> Adder-cost: 41   maxlim: 6143   bits: 14/13
c ---[  44]---> Adder-cost: 39   maxlim: 6143   bits: 14/13
c ---[  43]---> Adder-cost: 35   maxlim: 6143   bits: 14/13
c ---[  42]---> Adder-cost: 37   maxlim: 6143   bits: 14/13
c ---[  41]---> Adder-cost: 39   maxlim: 6143   bits: 14/13
c ---[  40]---> Adder-cost: 39   maxlim: 8191   bits: 14/13
c ---[  39]---> Adder-cost: 39   maxlim: 6143   bits: 14/13
c ---[  38]---> Adder-cost: 145   maxlim: 6143   bits: 14/13
c ---[  37]---> Adder-cost: 39   maxlim: 6143   bits: 14/13
c ---[  36]---> Adder-cost: 35   maxlim: 6143   bits: 14/13
c ---[  35]---> Adder-cost: 37   maxlim: 6143   bits: 14/13
c ---[  34]---> Adder-cost: 39   maxlim: 6143   bits: 14/13
c ---[  33]---> Adder-cost: 39   maxlim: 6143   bits: 14/13
c ---[  32]---> Adder-cost: 145   maxlim: 6143   bits: 14/13
c ---[  31]---> Adder-cost: 47   maxlim: 6143   bits: 14/13
c ---[  30]---> Adder-cost: 43   maxlim: 6143   bits: 14/13
c ---[  29]---> Adder-cost: 33   maxlim: 8191   bits: 14/13
c ---[  28]---> Adder-cost: 129   maxlim: 6143   bits: 14/13
c ---[  27]---> Adder-cost: 155   maxlim: 6143   bits: 14/13
c ---[  26]---> Adder-cost: 33   maxlim: 5119   bits: 14/13
c ---[  25]---> Adder-cost: 33   maxlim: 5119   bits: 14/13
c ---[  24]---> Adder-cost: 33   maxlim: 5119   bits: 14/13
c ---[  23]---> Adder-cost: 35   maxlim: 5119   bits: 14/13
c ---[  22]---> Adder-cost: 35   maxlim: 5119   bits: 14/13
c ---[  21]---> Adder-cost: 33   maxlim: 5119   bits: 14/13
c ---[  20]---> Adder-cost: 33   maxlim: 5119   bits: 14/13
c ---[  19]---> Adder-cost: 35   maxlim: 5119   bits: 14/13
c ---[  18]---> Adder-cost: 33   maxlim: 8191   bits: 14/13
c ---[  17]---> Adder-cost: 35   maxlim: 5119   bits: 14/13
c ---[  16]---> Adder-cost: 35   maxlim: 5119   bits: 14/13
c ---[  15]---> Adder-cost: 33   maxlim: 5119   bits: 14/13
c ---[  14]---> Adder-cost: 37   maxlim: 5119   bits: 14/13
c ---[  13]---> Adder-cost: 41   maxlim: 5119   bits: 14/13
c ---[  12]---> Adder-cost: 37   maxlim: 5119   bits: 14/13
c ---[  11]---> Adder-cost: 123   maxlim: 5119   bits: 14/13
c ---[  10]---> Adder-cost: 30   maxlim: 4095   bits: 13/12
c ---[   9]---> Adder-cost: 30   maxlim: 4095   bits: 13/12
c ---[   8]---> Adder-cost: 30   maxlim: 4095   bits: 13/12
c ---[   7]---> Adder-cost: 33   maxlim: 8191   bits: 14/13
c ---[   6]---> Adder-cost: 30   maxlim: 4095   bits: 13/12
c ---[   5]---> Adder-cost: 30   maxlim: 4095   bits: 13/12
c ---[   4]---> Adder-cost: 34   maxlim: 4095   bits: 13/12
c ---[   3]---> Adder-cost: 30   maxlim: 3071   bits: 13/12
c ---[   2]---> Adder-cost: 39   maxlim: 6   bits: 4/3
c ---[   1]---> Adder-cost: 39   maxlim: 7167   bits: 14/13
c ---[   0]---> Adder-cost: 33   maxlim: 7167   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   23390    83389 |    7796       0        0     nan |  0.000 % |
c |       100 |   23390    83389 |    8575     100      541     5.4 |  5.682 % |
c |       250 |   23390    83389 |    9433     250     1369     5.5 |  5.682 % |
c ==============================================================================
c [1mFound solution: 21746[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 210   maxlim: 52996   bits: 17/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       436 |   24791    88389 |    8263     436     4122     9.5 |  5.682 % |
c ==============================================================================
c [1mFound solution: 21739[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 53003   bits: 17/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       485 |   24795    88426 |    8265     485     4472     9.2 |  5.682 % |
c |       586 |   24795    88426 |    9091     586     5232     8.9 |  5.624 % |
c |       736 |   24795    88426 |   10000     736     5900     8.0 |  5.624 % |
c |       961 |   24789    88409 |   11000     960     7458     7.8 |  5.647 % |
c ==============================================================================
c [1mFound solution: 19959[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 54783   bits: 17/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1102 |   24794    88438 |    8264    1101     8253     7.5 |  5.647 % |
c |      1204 |   24794    88438 |    9090    1203     9076     7.5 |  5.714 % |
c |      1354 |   24794    88438 |    9999    1353     9826     7.3 |  5.714 % |
c |      1579 |   24794    88438 |   10999    1578    13957     8.8 |  5.714 % |
c |      1916 |   24794    88438 |   12099    1915    20125    10.5 |  5.714 % |
c |      2422 |   24794    88438 |   13309    2421    27933    11.5 |  5.714 % |
c ==============================================================================
c [1mFound solution: 19831[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 54911   bits: 17/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2796 |   24795    88449 |    8265    2795    32600    11.7 |  5.714 % |
c |      2896 |   24795    88449 |    9091    2895    33786    11.7 |  5.736 % |
c |      3046 |   24795    88449 |   10000    3045    35261    11.6 |  5.736 % |
c |      3271 |   24795    88449 |   11000    3270    37236    11.4 |  5.736 % |
c |      3608 |   24795    88449 |   12100    3607    41950    11.6 |  5.736 % |
c |      4115 |   24795    88449 |   13310    4114    47443    11.5 |  5.736 % |
c |      4874 |   24795    88449 |   14641    4873    54952    11.3 |  5.736 % |
c ==============================================================================
c [1mFound solution: 19799[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 54943   bits: 17/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5556 |   24800    88478 |    8266    5555    61222    11.0 |  5.736 % |
c |      5656 |   24800    88478 |    9092    5655    62141    11.0 |  5.758 % |
c |      5807 |   24800    88478 |   10001    5806    64089    11.0 |  5.758 % |
c ==============================================================================
c [1mFound solution: 19719[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 55023   bits: 17/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5953 |   24811    88549 |    8270    5952    66546    11.2 |  5.758 % |
c |      6054 |   24811    88549 |    9097    6053    67832    11.2 |  5.824 % |
c |      6204 |   24811    88549 |   10006    6203    70149    11.3 |  5.824 % |
c |      6430 |   24811    88549 |   11007    6429    75307    11.7 |  5.824 % |
c |      6767 |   24811    88549 |   12108    6766    83493    12.3 |  5.824 % |
c ==============================================================================
c [1mFound solution: 19191[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 55551   bits: 17/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7103 |   24813    88566 |    8271    7102    88458    12.5 |  5.824 % |
c |      7204 |   24813    88566 |    9098    7203    89570    12.4 |  5.869 % |
c |      7358 |   24813    88566 |   10007    7357    92116    12.5 |  5.869 % |
c |      7583 |   24813    88566 |   11008    7582    95742    12.6 |  5.869 % |
c |      7921 |   24813    88566 |   12109    7920   100029    12.6 |  5.869 % |
c |      8427 |   24813    88566 |   13320    8426   108551    12.9 |  5.869 % |
c ==============================================================================
c [1mFound solution: 18935[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 55807   bits: 17/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8562 |   24814    88575 |    8271    8561   109895    12.8 |  5.869 % |
c |      8662 |   24814    88575 |    9098    4381    54573    12.5 |  5.891 % |
c |      8812 |   24814    88575 |   10007    4531    56370    12.4 |  5.891 % |
c |      9038 |   24814    88575 |   11008    4757    59165    12.4 |  5.891 % |
c |      9375 |   24814    88575 |   12109    5094    65812    12.9 |  5.891 % |
c |      9881 |   24814    88575 |   13320    5600    75405    13.5 |  5.891 % |
c ==============================================================================
c [1mFound solution: 18679[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 56063   bits: 17/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10435 |   24815    88585 |    8271    6154    85968    14.0 |  5.891 % |
c |     10536 |   24815    88585 |    9098    6255    86750    13.9 |  5.913 % |
c |     10686 |   24815    88585 |   10007    6405    89445    14.0 |  5.913 % |
c |     10912 |   24815    88585 |   11008    6631    93048    14.0 |  5.913 % |
c |     11252 |   24815    88585 |   12109    6971   100052    14.4 |  5.913 % |
c |     11759 |   24815    88585 |   13320    7478   109101    14.6 |  5.913 % |
c |     12518 |   24815    88585 |   14652    8237   138042    16.8 |  5.913 % |
c |     13658 |   24815    88585 |   16117    9377   165001    17.6 |  5.913 % |
c |     15366 |   24815    88585 |   17729   11085   209234    18.9 |  5.913 % |
c |     17929 |   24815    88585 |   19502   13648   261170    19.1 |  5.913 % |
c ==============================================================================
c [1mFound solution: 18455[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 56287   bits: 17/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18851 |   24819    88623 |    8273   14570   278313    19.1 |  5.913 % |
c |     18951 |   24819    88623 |    9100    7385   126364    17.1 |  5.978 % |
c |     19101 |   24819    88623 |   10010    7535   127903    17.0 |  5.978 % |
c |     19326 |   24819    88623 |   11011    7760   131002    16.9 |  5.978 % |
c |     19663 |   24819    88623 |   12112    8097   134894    16.7 |  5.978 % |
c ==============================================================================
c [1mFound solution: 18359[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 56383   bits: 17/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20019 |   24821    88643 |    8273    8453   144428    17.1 |  5.978 % |
c |     20119 |   24821    88643 |    9100    8553   144897    16.9 |  6.022 % |
c |     20269 |   24821    88643 |   10010    8703   146260    16.8 |  6.022 % |
c |     20494 |   24821    88643 |   11011    8928   150502    16.9 |  6.022 % |
c |     20831 |   24821    88643 |   12112    9265   158022    17.1 |  6.022 % |
c |     21337 |   24821    88643 |   13323    9771   163614    16.7 |  6.022 % |
c |     22096 |   24821    88643 |   14656   10530   183015    17.4 |  6.022 % |
c |     23236 |   24821    88643 |   16121   11670   205289    17.6 |  6.022 % |
c ==============================================================================
c [1mFound solution: 18332[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 56410   bits: 17/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23856 |   24833    88739 |    8277   12290   213724    17.4 |  6.022 % |
c |     23956 |   24833    88739 |    9104    6245    89904    14.4 |  6.110 % |
c |     24106 |   24833    88739 |   10015    6395    93025    14.5 |  6.110 % |
c |     24333 |   24833    88739 |   11016    6622    96947    14.6 |  6.110 % |
c ==============================================================================
c [1mFound solution: 18167[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 56575   bits: 17/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24528 |   24834    88749 |    8278    6817    99043    14.5 |  6.110 % |
c |     24630 |   24834    88749 |    9105    6919    99959    14.4 |  6.132 % |
c |     24780 |   24834    88749 |   10016    7069   101945    14.4 |  6.132 % |
c |     25005 |   24834    88749 |   11018    7294   106146    14.6 |  6.132 % |
c |     25342 |   24834    88749 |   12119    7631   112995    14.8 |  6.132 % |
c |     25848 |   24834    88749 |   13331    8137   121460    14.9 |  6.132 % |
c |     26609 |   24834    88749 |   14664    8898   141808    15.9 |  6.132 % |
c |     27748 |   24834    88749 |   16131   10037   161084    16.0 |  6.132 % |
c ==============================================================================
c [1mFound solution: 17917[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 56825   bits: 17/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28330 |   24844    88838 |    8281   10619   172982    16.3 |  6.132 % |
c |     28431 |   24844    88838 |    9109    5411    78780    14.6 |  6.257 % |
c |     28581 |   24844    88838 |   10020    5561    82574    14.8 |  6.257 % |
c |     28806 |   24844    88838 |   11022    5786    87063    15.0 |  6.257 % |
c |     29143 |   24844    88838 |   12124    6123    92543    15.1 |  6.257 % |
c |     29651 |   24844    88838 |   13336    6631   101806    15.4 |  6.257 % |
c |     30410 |   24844    88838 |   14670    7390   112879    15.3 |  6.257 % |
c |     31550 |   24844    88838 |   16137    8530   142387    16.7 |  6.257 % |
c ==============================================================================
c [1mFound solution: 17913[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 56829   bits: 17/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32529 |   24846    88871 |    8282    9509   166119    17.5 |  6.257 % |
c |     32630 |   24846    88871 |    9110    4856    80160    16.5 |  6.301 % |
c |     32780 |   24846    88871 |   10021    5006    83351    16.7 |  6.301 % |
c |     33005 |   24846    88871 |   11023    5231    88003    16.8 |  6.301 % |
c |     33342 |   24846    88871 |   12125    5568    94847    17.0 |  6.301 % |
c |     33848 |   24846    88871 |   13338    6074   104092    17.1 |  6.301 % |
c |     34607 |   24846    88871 |   14672    6833   120842    17.7 |  6.301 % |
c |     35747 |   24846    88871 |   16139    7973   145655    18.3 |  6.301 % |
c |     37455 |   24846    88871 |   17753    9681   182327    18.8 |  6.301 % |
c ==============================================================================
c [1mFound solution: 17271[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 57471   bits: 17/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     39650 |   24852    88903 |    8284   11876   218984    18.4 |  6.301 % |
c |     39750 |   24852    88903 |    9112    6038    88330    14.6 |  6.345 % |
c |     39900 |   24852    88903 |   10023    6188    90952    14.7 |  6.345 % |
c |     40125 |   24852    88903 |   11026    6413    93325    14.6 |  6.345 % |
c |     40463 |   24852    88903 |   12128    6751    98785    14.6 |  6.345 % |
c |     40969 |   24852    88903 |   13341    7257   105464    14.5 |  6.345 % |
c |     41728 |   24852    88903 |   14675    8016   118322    14.8 |  6.345 % |
c |     42869 |   24852    88903 |   16143    9157   136593    14.9 |  6.345 % |
c |     44577 |   24852    88903 |   17757   10865   175522    16.2 |  6.345 % |
c |     47140 |   24852    88903 |   19533   13428   239571    17.8 |  6.345 % |
c |     50985 |   24852    88903 |   21486   17273   348444    20.2 |  6.345 % |
c |     56751 |   24852    88903 |   23635   11890   300326    25.3 |  6.345 % |
c |     65400 |   24852    88903 |   25998   20539   518023    25.2 |  6.345 % |
c ==============================================================================
c [1mFound solution: 17204[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 57538   bits: 17/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     76212 |   24857    88954 |    8285   18110   454394    25.1 |  6.345 % |
c |     76313 |   24857    88954 |    9113    4629    96775    20.9 |  6.407 % |
c |     76465 |   24857    88954 |   10024    4781    98816    20.7 |  6.407 % |
c |     76690 |   24857    88954 |   11027    5006   103711    20.7 |  6.407 % |
c |     77027 |   24857    88954 |   12130    5343   108714    20.3 |  6.407 % |
c |     77539 |   24857    88954 |   13343    5855   120234    20.5 |  6.407 % |
c |     78301 |   24857    88954 |   14677    6617   136948    20.7 |  6.407 % |
c |     79442 |   24857    88954 |   16145    7758   167151    21.5 |  6.407 % |
c |     81152 |   24857    88954 |   17759    9468   206645    21.8 |  6.407 % |
c |     83715 |   24857    88954 |   19535   12031   256487    21.3 |  6.407 % |
c |     87560 |   24857    88954 |   21489   15876   373751    23.5 |  6.407 % |
c ==============================================================================
c [1mFound solution: 17142[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 57600   bits: 17/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88700 |   24860    88984 |    8286   17016   394608    23.2 |  6.407 % |
c |     88800 |   24860    88984 |    9114    8608   183688    21.3 |  6.449 % |
c |     88950 |   24860    88984 |   10026    8758   184742    21.1 |  6.449 % |
c |     89175 |   24860    88984 |   11028    8983   186823    20.8 |  6.449 % |
c |     89512 |   24860    88984 |   12131    9320   193969    20.8 |  6.449 % |
c |     90018 |   24860    88984 |   13344    9826   205331    20.9 |  6.449 % |
c |     90777 |   24860    88984 |   14679   10585   222963    21.1 |  6.449 % |
c |     91916 |   24860    88984 |   16147   11724   252423    21.5 |  6.449 % |
c |     93625 |   24860    88984 |   17761   13433   303817    22.6 |  6.449 % |
c |     96188 |   24860    88984 |   19537   15996   371357    23.2 |  6.449 % |
c ==============================================================================
c [1mFound solution: 17125[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 57617   bits: 17/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     99384 |   24863    89017 |    8287   19192   450034    23.4 |  6.449 % |
c |     99485 |   24863    89017 |    9115    4899    85028    17.4 |  6.491 % |
c |     99636 |   24863    89017 |   10027    5050    86142    17.1 |  6.491 % |
c |     99861 |   24863    89017 |   11029    5275    90127    17.1 |  6.491 % |
c |    100198 |   24863    89017 |   12132    5612    99494    17.7 |  6.491 % |
c |    100705 |   24863    89017 |   13346    6119   106147    17.3 |  6.491 % |
c |    101466 |   24863    89017 |   14680    6880   126147    18.3 |  6.491 % |
c |    102606 |   24863    89017 |   16149    8020   159179    19.8 |  6.491 % |
c |    104318 |   24863    89017 |   17763    9732   187115    19.2 |  6.491 % |
c |    106884 |   24863    89017 |   19540   12298   239134    19.4 |  6.491 % |
c |    110730 |   24863    89017 |   21494   16144   424818    26.3 |  6.491 % |
c |    116496 |   24863    89017 |   23643   21910   626389    28.6 |  6.491 % |
c |    125147 |   24863    89017 |   26008   17524   527205    30.1 |  6.491 % |
c |    138121 |   24863    89017 |   28608   17226   490359    28.5 |  6.491 % |
c ==============================================================================
c [1mFound solution: 17121[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 57621   bits: 17/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    143789 |   24865    89050 |    8288   22894   595118    26.0 |  6.491 % |
c |    143890 |   24865    89050 |    9116    5825    88907    15.3 |  6.535 % |
c |    144041 |   24865    89050 |   10028    5976    90664    15.2 |  6.535 % |
c |    144266 |   24865    89050 |   11031    6201    94148    15.2 |  6.535 % |
c |    144603 |   24865    89050 |   12134    6538    97272    14.9 |  6.535 % |
c |    145109 |   24865    89050 |   13347    7044   106514    15.1 |  6.535 % |
c |    145869 |   24865    89050 |   14682    7804   124531    16.0 |  6.535 % |
c |    147010 |   24865    89050 |   16150    8945   155072    17.3 |  6.535 % |
c |    148718 |   24865    89050 |   17766   10653   203081    19.1 |  6.535 % |
c |    151281 |   24865    89050 |   19542   13216   269253    20.4 |  6.535 % |
c |    155126 |   24865    89050 |   21496   17061   390811    22.9 |  6.535 % |
c |    160892 |   24865    89050 |   23646   22827   547400    24.0 |  6.535 % |
c |    169542 |   24865    89050 |   26011   19286   490721    25.4 |  6.535 % |
c |    182518 |   24865    89050 |   28612   18805   436312    23.2 |  6.535 % |
c |    201981 |   24865    89050 |   31473   22511   560953    24.9 |  6.535 % |
c |    231174 |   24865    89050 |   34621   17632   438267    24.9 |  6.535 % |
c ==============================================================================
c [1mFound solution: 17091[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 57651   bits: 17/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    247437 |   24869    89095 |    8289   33895   987918    29.1 |  6.535 % |
c |    247539 |   24869    89095 |    9117    6494   211138    32.5 |  6.599 % |
c |    247690 |   24869    89095 |   10029    6645   212239    31.9 |  6.599 % |
c |    247915 |   24869    89095 |   11032    6870   214141    31.2 |  6.599 % |
c |    248253 |   24869    89095 |   12135    7208   218503    30.3 |  6.599 % |
c |    248762 |   24869    89095 |   13349    7717   226484    29.3 |  6.599 % |
c |    249523 |   24869    89095 |   14684    8478   244923    28.9 |  6.599 % |
c |    250662 |   24869    89095 |   16152    9617   283846    29.5 |  6.599 % |
c |    252370 |   24869    89095 |   17768   11325   321131    28.4 |  6.599 % |
c |    254932 |   24869    89095 |   19545   13887   368975    26.6 |  6.599 % |
c |    258779 |   24869    89095 |   21499   17734   445164    25.1 |  6.599 % |
c |    264546 |   24869    89095 |   23649   12033   304397    25.3 |  6.599 % |
c |    273197 |   24869    89095 |   26014   20684   595235    28.8 |  6.599 % |
c |    286171 |   24869    89095 |   28615   20399   485440    23.8 |  6.599 % |
c |    305632 |   24869    89095 |   31477   24474   633640    25.9 |  6.599 % |
c ==============================================================================
c [1mFound solution: 17090[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 57652   bits: 17/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    333039 |   24871    89115 |    8290   14577   451638    31.0 |  6.599 % |
c |    333139 |   24871    89115 |    9119    7389   200076    27.1 |  6.619 % |
c |    333290 |   24871    89115 |   10030    7540   201028    26.7 |  6.619 % |
c |    333515 |   24871    89115 |   11033    7765   202356    26.1 |  6.619 % |
c |    333853 |   24871    89115 |   12137    8103   207824    25.6 |  6.619 % |
c |    334359 |   24871    89115 |   13351    8609   217248    25.2 |  6.619 % |
c |    335119 |   24871    89115 |   14686    9369   229031    24.4 |  6.619 % |
c |    336259 |   24871    89115 |   16154   10509   256751    24.4 |  6.619 % |
c |    337967 |   24871    89115 |   17770   12217   288113    23.6 |  6.619 % |
c |    340532 |   24871    89115 |   19547   14782   337067    22.8 |  6.619 % |
c |    344376 |   24871    89115 |   21502   18626   441427    23.7 |  6.619 % |
c |    350142 |   24871    89115 |   23652   13453   274565    20.4 |  6.619 % |
c |    358793 |   24871    89115 |   26017   22104   466462    21.1 |  6.619 % |
c ==============================================================================
c [1mFound solution: 17089[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 57653   bits: 17/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    364636 |   24873    89134 |    8291   27947   648026    23.2 |  6.619 % |
c |    364736 |   24873    89134 |    9120    6907   151271    21.9 |  6.639 % |
c |    364888 |   24873    89134 |   10032    7059   153816    21.8 |  6.639 % |
c |    365113 |   24873    89134 |   11035    7284   157238    21.6 |  6.639 % |
c |    365450 |   24873    89134 |   12138    7621   163712    21.5 |  6.639 % |
c |    365956 |   24873    89134 |   13352    8127   172459    21.2 |  6.639 % |
c |    366717 |   24873    89134 |   14688    8888   187776    21.1 |  6.639 % |
c |    367858 |   24873    89134 |   16156   10029   205659    20.5 |  6.639 % |
c |    369567 |   24873    89134 |   17772   11738   247420    21.1 |  6.639 % |
c |    372129 |   24873    89134 |   19549   14300   368253    25.8 |  6.639 % |
c |    375973 |   24873    89134 |   21504   18144   451052    24.9 |  6.639 % |
c |    381740 |   24873    89134 |   23655   12537   291383    23.2 |  6.639 % |
c |    390389 |   24873    89134 |   26020   21186   488660    23.1 |  6.639 % |
c |    403364 |   24873    89134 |   28622   20716   837594    40.4 |  6.639 % |
c |    422827 |   24873    89134 |   31485   25278   674336    26.7 |  6.639 % |
c ==============================================================================
c [1mFound solution: 17085[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 57657   bits: 17/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    424389 |   24877    89168 |    8292   26840   714766    26.6 |  6.639 % |
c |    424489 |   24877    89168 |    9121    6810   146243    21.5 |  6.679 % |
c |    424640 |   24877    89168 |   10033    6961   147500    21.2 |  6.679 % |
c |    424867 |   24877    89168 |   11036    7188   151912    21.1 |  6.679 % |
c |    425206 |   24877    89168 |   12140    7527   158666    21.1 |  6.679 % |
c |    425712 |   24877    89168 |   13354    8033   167334    20.8 |  6.679 % |
c |    426471 |   24877    89168 |   14689    8792   183574    20.9 |  6.679 % |
c |    427610 |   24877    89168 |   16158    9931   214917    21.6 |  6.679 % |
c |    429319 |   24877    89168 |   17774   11640   262264    22.5 |  6.679 % |
c |    431883 |   24877    89168 |   19552   14204   326420    23.0 |  6.679 % |
c |    435728 |   24877    89168 |   21507   18049   432228    23.9 |  6.679 % |
c |    441497 |   24877    89168 |   23658   12868   259428    20.2 |  6.679 % |
c |    450147 |   24877    89168 |   26023   21518   533956    24.8 |  6.679 % |
c |    463121 |   24877    89168 |   28626   21293   602071    28.3 |  6.679 % |
c |    482582 |   24877    89168 |   31488   26239   669561    25.5 |  6.679 % |
c |    511775 |   24877    89168 |   34637   22508   597606    26.6 |  6.679 % |
c ==============================================================================
c [1mFound solution: 17083[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 57659   bits: 17/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    522333 |   24879    89186 |    8293   33066   866966    26.2 |  6.679 % |
c |    522433 |   24879    89186 |    9122    7910   149325    18.9 |  6.699 % |
c |    522583 |   24879    89186 |   10034    8060   150933    18.7 |  6.699 % |
c |    522808 |   24879    89186 |   11037    8285   153460    18.5 |  6.699 % |
c |    523146 |   24879    89186 |   12141    8623   162516    18.8 |  6.699 % |
c |    523653 |   24879    89186 |   13355    9130   172851    18.9 |  6.699 % |
c |    524412 |   24879    89186 |   14691    9889   190456    19.3 |  6.699 % |
c |    525552 |   24879    89186 |   16160   11029   217008    19.7 |  6.699 % |
c |    527261 |   24879    89186 |   17776   12738   258862    20.3 |  6.699 % |
c |    529824 |   24879    89186 |   19554   15301   296567    19.4 |  6.699 % |
c |    533668 |   24879    89186 |   21509   19145   391456    20.4 |  6.699 % |
c |    539434 |   24879    89186 |   23660   13970   266613    19.1 |  6.699 % |
c ==============================================================================
c [1mFound solution: 17015[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 57727   bits: 17/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    546598 |   24881    89199 |    8293   21134   550111    26.0 |  6.699 % |
c |    546698 |   24881    89199 |    9122    5384   203523    37.8 |  6.719 % |
c |    546850 |   24881    89199 |   10034    5536   204916    37.0 |  6.719 % |
c |    547075 |   24881    89199 |   11037    5761   208875    36.3 |  6.719 % |
c |    547413 |   24881    89199 |   12141    6099   218976    35.9 |  6.719 % |
c |    547920 |   24881    89199 |   13355    6606   228977    34.7 |  6.719 % |
c |    548681 |   24881    89199 |   14691    7367   245229    33.3 |  6.719 % |
c |    549822 |   24881    89199 |   16160    8508   280336    32.9 |  6.719 % |
c |    551531 |   24881    89199 |   17776   10217   334888    32.8 |  6.719 % |
c |    554093 |   24881    89199 |   19554   12779   409396    32.0 |  6.719 % |
c |    557940 |   24881    89199 |   21509   16626   492085    29.6 |  6.719 % |
c |    563706 |   24881    89199 |   23660   22392   662019    29.6 |  6.719 % |
c |    572355 |   24881    89199 |   26026   19026   425808    22.4 |  6.719 % |
c |    585329 |   24881    89199 |   28629   18767   432475    23.0 |  6.719 % |
c ==============================================================================
c [1mFound solution: 16887[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 57855   bits: 17/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    593106 |   24882    89208 |    8294   26544   906372    34.1 |  6.719 % |
c |    593206 |   24882    89208 |    9123    6736   319448    47.4 |  6.741 % |
c |    593356 |   24882    89208 |   10035    6886   320695    46.6 |  6.741 % |
c |    593581 |   24882    89208 |   11039    7111   324843    45.7 |  6.741 % |
c |    593918 |   24882    89208 |   12143    7448   330098    44.3 |  6.741 % |
c |    594428 |   24882    89208 |   13357    7958   346574    43.6 |  6.741 % |
c |    595187 |   24882    89208 |   14693    8717   357245    41.0 |  6.741 % |
c |    596326 |   24882    89208 |   16162    9856   378092    38.4 |  6.741 % |
c |    598037 |   24882    89208 |   17778   11567   414322    35.8 |  6.741 % |
c |    600599 |   24882    89208 |   19556   14129   483921    34.3 |  6.741 % |
c |    604444 |   24882    89208 |   21512   17974   588636    32.7 |  6.741 % |
c |    610212 |   24882    89208 |   23663   12616   322111    25.5 |  6.741 % |
c |    618861 |   24882    89208 |   26030   21265   606031    28.5 |  6.741 % |
c |    631835 |   24882    89208 |   28633   21033   482428    22.9 |  6.741 % |
c |    651297 |   24882    89208 |   31496   22898   569116    24.9 |  6.741 % |
c |    680489 |   24882    89208 |   34646   17454   346528    19.9 |  6.741 % |
c ==============================================================================
c [1mFound solution: 16759[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 57983   bits: 17/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    702130 |   24884    89221 |    8294   16834   438653    26.1 |  6.741 % |
c |    702230 |   24884    89221 |    9123    8517   142723    16.8 |  6.761 % |
c |    702380 |   24884    89221 |   10035    8667   144024    16.6 |  6.761 % |
c |    702606 |   24884    89221 |   11039    8893   147168    16.5 |  6.761 % |
c |    702943 |   24884    89221 |   12143    9230   153328    16.6 |  6.761 % |
c |    703450 |   24884    89221 |   13357    9737   162853    16.7 |  6.761 % |
c |    704210 |   24884    89221 |   14693   10497   184967    17.6 |  6.761 % |
c |    705350 |   24884    89221 |   16162   11637   222467    19.1 |  6.761 % |
c |    707060 |   24884    89221 |   17778   13347   259550    19.4 |  6.761 % |
c |    709622 |   24884    89221 |   19556   15909   357162    22.5 |  6.761 % |
c |    713466 |   24884    89221 |   21512   19753   445850    22.6 |  6.761 % |
c |    719233 |   24884    89221 |   23663   14588   384106    26.3 |  6.761 % |
c ==============================================================================
c [1mFound solution: 16736[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 58006   bits: 17/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    726077 |   24891    89289 |    8297   21432   541801    25.3 |  6.761 % |
c |    726177 |   24891    89289 |    9126    5458   108805    19.9 |  6.842 % |
c |    726327 |   24891    89289 |   10039    5608   110105    19.6 |  6.842 % |
c |    726552 |   24891    89289 |   11043    5833   113039    19.4 |  6.842 % |
c |    726889 |   24891    89289 |   12147    6170   116781    18.9 |  6.842 % |
c |    727395 |   24891    89289 |   13362    6676   132285    19.8 |  6.842 % |
c |    728155 |   24891    89289 |   14698    7436   149089    20.0 |  6.842 % |
c |    729294 |   24891    89289 |   16168    8575   175924    20.5 |  6.842 % |
c |    731002 |   24891    89289 |   17785   10283   210036    20.4 |  6.842 % |
c |    733565 |   24891    89289 |   19563   12846   289575    22.5 |  6.842 % |
c |    737412 |   24891    89289 |   21520   16693   508158    30.4 |  6.842 % |
c |    743178 |   24891    89289 |   23672   22459   707643    31.5 |  6.842 % |
c |    751830 |   24891    89289 |   26039   18851   580472    30.8 |  6.842 % |
c |    764806 |   24891    89289 |   28643   18212   526917    28.9 |  6.842 % |
c |    784267 |   24891    89289 |   31507   20718  1165349    56.2 |  6.842 % |
c |    813459 |   24891    89289 |   34658   31761   836488    26.3 |  6.842 % |
c |    857248 |   24891    89289 |   38124   17589  1078762    61.3 |  6.842 % |
c ==============================================================================
c [1mFound solution: 16631[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 58111   bits: 17/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    878969 |   24893    89301 |    8297   39310  2029149    51.6 |  6.842 % |
c |    879071 |   24893    89301 |    9126    6870   237838    34.6 |  6.862 % |
c |    879223 |   24893    89301 |   10039    7022   239518    34.1 |  6.862 % |
c |    879448 |   24893    89301 |   11043    7247   241410    33.3 |  6.862 % |
c |    879786 |   24893    89301 |   12147    7585   246653    32.5 |  6.862 % |
c |    880293 |   24893    89301 |   13362    8092   254264    31.4 |  6.862 % |
c |    881052 |   24893    89301 |   14698    8851   265179    30.0 |  6.862 % |
c |    882192 |   24893    89301 |   16168    9991   291830    29.2 |  6.862 % |
c |    883901 |   24893    89301 |   17785   11700   320027    27.4 |  6.862 % |
c |    886463 |   24893    89301 |   19563   14262   376268    26.4 |  6.862 % |
c |    890309 |   24893    89301 |   21520   18108   509243    28.1 |  6.862 % |
c |    896076 |   24893    89301 |   23672   12865   379175    29.5 |  6.862 % |
c |    904725 |   24893    89301 |   26039   21514   658359    30.6 |  6.862 % |
c |    917699 |   24893    89301 |   28643   21236   698307    32.9 |  6.862 % |
c |    937160 |   24893    89301 |   31507   25456   893995    35.1 |  6.862 % |
c |    966352 |   24893    89301 |   34658   20076   455588    22.7 |  6.862 % |
c |   1010141 |   24893    89301 |   38124   16897   791574    46.8 |  6.862 % |
c |   1075825 |   24893    89301 |   41936   33154  1092614    33.0 |  6.862 % |
c ==============================================================================
c [1mFound solution: 16175[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 58567   bits: 17/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1109416 |   24900    89352 |    8300   37831  1224876    32.4 |  6.862 % |
c |   1109516 |   24900    89352 |    9130    7899   206012    26.1 |  6.943 % |
c |   1109666 |   24900    89352 |   10043    8049   207337    25.8 |  6.943 % |
c |   1109891 |   24900    89352 |   11047    8274   211066    25.5 |  6.943 % |
c |   1110228 |   24900    89352 |   12152    8611   216696    25.2 |  6.943 % |
c |   1110734 |   24900    89352 |   13367    9117   222824    24.4 |  6.943 % |
c |   1111496 |   24900    89352 |   14703    9879   245993    24.9 |  6.943 % |
c |   1112636 |   24900    89352 |   16174   11019   278704    25.3 |  6.943 % |
c |   1114345 |   24900    89352 |   17791   12728   311780    24.5 |  6.943 % |
c |   1116907 |   24900    89352 |   19570   15290   412264    27.0 |  6.943 % |
c |   1120755 |   24900    89352 |   21528   19138   579260    30.3 |  6.943 % |
c |   1126522 |   24900    89352 |   23680   13912   426021    30.6 |  6.943 % |
c |   1135171 |   24900    89352 |   26048   22561   744561    33.0 |  6.943 % |
c |   1148148 |   24900    89352 |   28653   22292   695909    31.2 |  6.943 % |
c |   1167609 |   24900    89352 |   31519   27213  1004697    36.9 |  6.943 % |
c ==============================================================================
c [1mFound solution: 16055[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 58687   bits: 17/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1186420 |   24903    89376 |    8301   29533   976313    33.1 |  6.943 % |
c |   1186520 |   24903    89376 |    9131    7484   165511    22.1 |  6.985 % |
c |   1186670 |   24903    89376 |   10044    7634   167113    21.9 |  6.985 % |
c |   1186895 |   24903    89376 |   11048    7859   169168    21.5 |  6.985 % |
c |   1187232 |   24903    89376 |   12153    8196   173498    21.2 |  6.985 % |
c |   1187738 |   24903    89376 |   13368    8702   182220    20.9 |  6.985 % |
c |   1188499 |   24894    89345 |   14705    9443   205523    21.8 |  7.008 % |
c |   1189642 |   24894    89345 |   16176   10586   235870    22.3 |  7.008 % |
c |   1191350 |   24894    89345 |   17793   12294   279459    22.7 |  7.008 % |
c |   1193912 |   24894    89345 |   19573   14856   363941    24.5 |  7.008 % |
c |   1197758 |   24894    89345 |   21530   18702   489913    26.2 |  7.008 % |
c |   1203524 |   24894    89345 |   23683   13448   395831    29.4 |  7.008 % |
c |   1212175 |   24894    89345 |   26052   22099   643524    29.1 |  7.008 % |
c |   1225149 |   24894    89345 |   28657   21704   610569    28.1 |  7.008 % |
c |   1244612 |   24894    89345 |   31523   26110   743493    28.5 |  7.008 % |
c |   1273805 |   24894    89345 |   34675   21089   886544    42.0 |  7.008 % |
c |   1317594 |   24894    89345 |   38142   25351   619696    24.4 |  7.008 % |
c |   1383278 |   24894    89345 |   41957   19013  1152392    60.6 |  7.008 % |
#### 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.74 0.91 0.87 2/54 22135
Raw data (stat): 22135 (runsolver) R 22134 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 539529099 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.78 0.91 0.87 2/54 22135
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 1281 0 0 0 994 4 0 0 25 0 1 0 539529099 7086080 1259 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1730 1259 603 41 0 1689 0
vsize: 6920
[startup+20.0015 s]
Raw data (loadavg): 0.81 0.91 0.87 2/54 22135
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 1329 0 0 0 1993 5 0 0 25 0 1 0 539529099 7221248 1307 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1763 1307 603 41 0 1722 0
vsize: 7052
[startup+30.0068 s]
Raw data (loadavg): 0.84 0.92 0.87 2/54 22135
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 1678 0 0 0 2992 6 0 0 25 0 1 0 539529099 8740864 1656 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2134 1656 603 41 0 2093 0
vsize: 8536
[startup+40.0064 s]
Raw data (loadavg): 0.87 0.92 0.87 2/54 22135
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 1917 0 0 0 3991 8 0 0 25 0 1 0 539529099 9678848 1895 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2363 1895 603 41 0 2322 0
vsize: 9452
[startup+50.0074 s]
Raw data (loadavg): 0.89 0.92 0.88 2/54 22135
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 1917 0 0 0 4991 8 0 0 25 0 1 0 539529099 9678848 1895 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2363 1895 603 41 0 2322 0
vsize: 9452
[startup+60.008 s]
Raw data (loadavg): 0.90 0.92 0.88 2/54 22135
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 1997 0 0 0 5990 9 0 0 25 0 1 0 539529099 10084352 1975 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2462 1975 603 41 0 2421 0
vsize: 9848
[startup+70.0082 s]
Raw data (loadavg): 0.92 0.92 0.88 2/54 22135
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2143 0 0 0 6989 9 0 0 25 0 1 0 539529099 10629120 2121 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2595 2121 603 41 0 2554 0
vsize: 10380
[startup+80.0093 s]
Raw data (loadavg): 0.93 0.93 0.88 2/54 22135
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2189 0 0 0 7988 10 0 0 25 0 1 0 539529099 10907648 2167 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2663 2167 603 41 0 2622 0
vsize: 10652
[startup+90.0143 s]
Raw data (loadavg): 0.94 0.93 0.88 2/54 22135
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2189 0 0 0 8988 10 0 0 25 0 1 0 539529099 10907648 2167 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2663 2167 603 41 0 2622 0
vsize: 10652
[startup+100.015 s]
Raw data (loadavg): 0.95 0.93 0.88 2/54 22135
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2190 0 0 0 9988 11 0 0 25 0 1 0 539529099 10907648 2168 4294967295 134512640 134672761 3221224544 3221223668 134566062 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2663 2168 603 41 0 2622 0
vsize: 10652
[startup+110.016 s]
Raw data (loadavg): 0.96 0.93 0.88 2/54 22135
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2196 0 0 0 10988 11 0 0 25 0 1 0 539529099 10907648 2174 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2663 2174 603 41 0 2622 0
vsize: 10652
[startup+120.017 s]
Raw data (loadavg): 0.96 0.93 0.88 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2243 0 0 0 11988 12 0 0 25 0 1 0 539529099 11055104 2221 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2699 2221 603 41 0 2658 0
vsize: 10796
[startup+130.017 s]
Raw data (loadavg): 0.97 0.94 0.88 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2381 0 0 0 12987 13 0 0 25 0 1 0 539529099 11608064 2359 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2834 2359 603 41 0 2793 0
vsize: 11336
[startup+140.017 s]
Raw data (loadavg): 0.97 0.94 0.88 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2402 0 0 0 13987 13 0 0 25 0 1 0 539529099 11743232 2380 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2867 2380 603 41 0 2826 0
vsize: 11468
[startup+150.019 s]
Raw data (loadavg): 0.98 0.94 0.89 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2434 0 0 0 14986 14 0 0 25 0 1 0 539529099 11882496 2412 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2901 2412 603 41 0 2860 0
vsize: 11604
[startup+160.019 s]
Raw data (loadavg): 0.98 0.94 0.89 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2457 0 0 0 15986 14 0 0 25 0 1 0 539529099 12029952 2435 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2937 2435 603 41 0 2896 0
vsize: 11748
[startup+170.019 s]
Raw data (loadavg): 0.98 0.94 0.89 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2648 0 0 0 16985 15 0 0 25 0 1 0 539529099 12967936 2626 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3166 2626 603 41 0 3125 0
vsize: 12664
[startup+180.02 s]
Raw data (loadavg): 0.98 0.94 0.89 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2648 0 0 0 17985 16 0 0 25 0 1 0 539529099 12967936 2626 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3166 2626 603 41 0 3125 0
vsize: 12664
[startup+190.02 s]
Raw data (loadavg): 0.99 0.94 0.89 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2650 0 0 0 18985 16 0 0 25 0 1 0 539529099 12967936 2628 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3166 2628 603 41 0 3125 0
vsize: 12664
[startup+200.021 s]
Raw data (loadavg): 0.99 0.95 0.89 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2652 0 0 0 19984 16 0 0 25 0 1 0 539529099 12967936 2630 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3166 2630 603 41 0 3125 0
vsize: 12664
[startup+210.022 s]
Raw data (loadavg): 0.99 0.95 0.89 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2653 0 0 0 20984 17 0 0 25 0 1 0 539529099 12967936 2631 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3166 2631 603 41 0 3125 0
vsize: 12664
[startup+220.022 s]
Raw data (loadavg): 0.99 0.95 0.89 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2654 0 0 0 21984 17 0 0 25 0 1 0 539529099 12967936 2632 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3166 2632 603 41 0 3125 0
vsize: 12664
[startup+230.03 s]
Raw data (loadavg): 0.99 0.95 0.89 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2929 0 0 0 22984 18 0 0 25 0 1 0 539529099 14045184 2907 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3429 2907 603 41 0 3388 0
vsize: 13716
[startup+240.031 s]
Raw data (loadavg): 0.99 0.95 0.89 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2937 0 0 0 23984 19 0 0 25 0 1 0 539529099 14045184 2915 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3429 2915 603 41 0 3388 0
vsize: 13716
[startup+250.035 s]
Raw data (loadavg): 0.99 0.95 0.89 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2937 0 0 0 24983 20 0 0 25 0 1 0 539529099 14045184 2915 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3429 2915 603 41 0 3388 0
vsize: 13716
[startup+260.038 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2937 0 0 0 25983 20 0 0 25 0 1 0 539529099 14045184 2915 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3429 2915 603 41 0 3388 0
vsize: 13716
[startup+270.038 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2937 0 0 0 26983 20 0 0 25 0 1 0 539529099 14045184 2915 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3429 2915 603 41 0 3388 0
vsize: 13716
[startup+280.038 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2937 0 0 0 27983 20 0 0 25 0 1 0 539529099 14045184 2915 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3429 2915 603 41 0 3388 0
vsize: 13716
[startup+290.039 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2937 0 0 0 28982 21 0 0 25 0 1 0 539529099 14045184 2915 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3429 2915 603 41 0 3388 0
vsize: 13716
[startup+300.04 s]
Raw data (loadavg): 0.99 0.96 0.90 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2950 0 0 0 29982 22 0 0 25 0 1 0 539529099 14184448 2928 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3463 2928 603 41 0 3422 0
vsize: 13852
[startup+310.04 s]
Raw data (loadavg): 0.99 0.96 0.90 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2950 0 0 0 30982 22 0 0 25 0 1 0 539529099 14184448 2928 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3463 2928 603 41 0 3422 0
vsize: 13852
[startup+320.04 s]
Raw data (loadavg): 0.99 0.96 0.90 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2971 0 0 0 31981 22 0 0 25 0 1 0 539529099 14184448 2949 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3463 2949 603 41 0 3422 0
vsize: 13852
[startup+330.041 s]
Raw data (loadavg): 0.99 0.96 0.90 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2978 0 0 0 32981 22 0 0 25 0 1 0 539529099 14331904 2956 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3499 2956 603 41 0 3458 0
vsize: 13996
[startup+340.058 s]
Raw data (loadavg): 0.99 0.96 0.90 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2994 0 0 0 33983 23 0 0 25 0 1 0 539529099 14331904 2972 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3499 2972 603 41 0 3458 0
vsize: 13996
[startup+350.059 s]
Raw data (loadavg): 0.99 0.96 0.90 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3001 0 0 0 34982 23 0 0 25 0 1 0 539529099 14331904 2979 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3499 2979 603 41 0 3458 0
vsize: 13996
[startup+360.059 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3020 0 0 0 35982 24 0 0 25 0 1 0 539529099 14495744 2998 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3539 2998 603 41 0 3498 0
vsize: 14156
[startup+370.059 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3020 0 0 0 36982 24 0 0 25 0 1 0 539529099 14495744 2998 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3539 2998 603 41 0 3498 0
vsize: 14156
[startup+380.06 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3048 0 0 0 37981 25 0 0 25 0 1 0 539529099 14659584 3026 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3579 3026 603 41 0 3538 0
vsize: 14316
[startup+390.06 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3048 0 0 0 38981 26 0 0 25 0 1 0 539529099 14659584 3026 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3579 3026 603 41 0 3538 0
vsize: 14316
[startup+400.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3048 0 0 0 39981 26 0 0 25 0 1 0 539529099 14659584 3026 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3579 3026 603 41 0 3538 0
vsize: 14316
[startup+410.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3048 0 0 0 40981 26 0 0 25 0 1 0 539529099 14659584 3026 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3579 3026 603 41 0 3538 0
vsize: 14316
[startup+420.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3048 0 0 0 41981 26 0 0 25 0 1 0 539529099 14659584 3026 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3579 3026 603 41 0 3538 0
vsize: 14316
[startup+430.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3048 0 0 0 42981 26 0 0 25 0 1 0 539529099 14659584 3026 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3579 3026 603 41 0 3538 0
vsize: 14316
[startup+440.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3054 0 0 0 43982 26 0 0 25 0 1 0 539529099 14659584 3032 4294967295 134512640 134672761 3221224544 3221223728 134558645 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3579 3032 603 41 0 3538 0
vsize: 14316
[startup+450.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3054 0 0 0 44982 26 0 0 25 0 1 0 539529099 14659584 3032 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3579 3032 603 41 0 3538 0
vsize: 14316
[startup+460.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3054 0 0 0 45982 26 0 0 25 0 1 0 539529099 14659584 3032 4294967295 134512640 134672761 3221224544 3221223648 134554677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3579 3032 603 41 0 3538 0
vsize: 14316
[startup+470.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3058 0 0 0 46982 26 0 0 25 0 1 0 539529099 14659584 3036 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3579 3036 603 41 0 3538 0
vsize: 14316
[startup+480.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3070 0 0 0 47982 26 0 0 25 0 1 0 539529099 14823424 3048 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3619 3048 603 41 0 3578 0
vsize: 14476
[startup+490.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3125 0 0 0 48983 26 0 0 25 0 1 0 539529099 14958592 3103 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3652 3103 603 41 0 3611 0
vsize: 14608
[startup+500.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3125 0 0 0 49983 26 0 0 25 0 1 0 539529099 14958592 3103 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3652 3103 603 41 0 3611 0
vsize: 14608
[startup+510.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3126 0 0 0 50984 26 0 0 25 0 1 0 539529099 14958592 3104 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3652 3104 603 41 0 3611 0
vsize: 14608
[startup+520.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3126 0 0 0 51985 26 0 0 25 0 1 0 539529099 14958592 3104 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3652 3104 603 41 0 3611 0
vsize: 14608
[startup+530.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3126 0 0 0 52983 26 0 0 25 0 1 0 539529099 14958592 3104 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3652 3104 603 41 0 3611 0
vsize: 14608
[startup+540.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3328 0 0 0 53983 27 0 0 25 0 1 0 539529099 15769600 3306 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3850 3306 603 41 0 3809 0
vsize: 15400
[startup+550.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3670 0 0 0 54983 28 0 0 25 0 1 0 539529099 17248256 3648 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4211 3648 603 41 0 4170 0
vsize: 16844
[startup+560.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3711 0 0 0 55983 28 0 0 25 0 1 0 539529099 17383424 3689 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4244 3689 603 41 0 4203 0
vsize: 16976
[startup+570.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3711 0 0 0 56972 29 0 0 25 0 1 0 539529099 17383424 3689 4294967295 134512640 134672761 3221224544 3221223728 134559334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4244 3689 603 41 0 4203 0
vsize: 16976
[startup+580.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3711 0 0 0 57972 29 0 0 25 0 1 0 539529099 17383424 3689 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4244 3689 603 41 0 4203 0
vsize: 16976
[startup+590.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3716 0 0 0 58973 29 0 0 25 0 1 0 539529099 17383424 3694 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4244 3694 603 41 0 4203 0
vsize: 16976
[startup+600.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3717 0 0 0 59972 29 0 0 25 0 1 0 539529099 17383424 3695 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4244 3695 603 41 0 4203 0
vsize: 16976
[startup+610.094 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4248 0 0 0 60971 31 0 0 25 0 1 0 539529099 19652608 4226 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4798 4226 603 41 0 4757 0
vsize: 19192
[startup+620.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4492 0 0 0 61970 32 0 0 25 0 1 0 539529099 20611072 4470 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4470 603 41 0 4991 0
vsize: 20128
[startup+630.094 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4492 0 0 0 62970 32 0 0 25 0 1 0 539529099 20611072 4470 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4470 603 41 0 4991 0
vsize: 20128
[startup+640.094 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4507 0 0 0 63970 32 0 0 25 0 1 0 539529099 20611072 4485 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4485 603 41 0 4991 0
vsize: 20128
[startup+650.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4507 0 0 0 64970 32 0 0 25 0 1 0 539529099 20611072 4485 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4485 603 41 0 4991 0
vsize: 20128
[startup+660.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4507 0 0 0 65970 32 0 0 25 0 1 0 539529099 20611072 4485 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4485 603 41 0 4991 0
vsize: 20128
[startup+670.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4507 0 0 0 66970 32 0 0 25 0 1 0 539529099 20611072 4485 4294967295 134512640 134672761 3221224544 3221223136 134565829 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4485 603 41 0 4991 0
vsize: 20128
[startup+680.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4507 0 0 0 67970 32 0 0 25 0 1 0 539529099 20611072 4485 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4485 603 41 0 4991 0
vsize: 20128
[startup+690.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4510 0 0 0 68971 32 0 0 25 0 1 0 539529099 20611072 4488 4294967295 134512640 134672761 3221224544 3221223648 134554671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4488 603 41 0 4991 0
vsize: 20128
[startup+700.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4511 0 0 0 69971 32 0 0 25 0 1 0 539529099 20611072 4489 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4489 603 41 0 4991 0
vsize: 20128
[startup+710.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4511 0 0 0 70971 32 0 0 25 0 1 0 539529099 20611072 4489 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4489 603 41 0 4991 0
vsize: 20128
[startup+720.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4511 0 0 0 71971 32 0 0 25 0 1 0 539529099 20611072 4489 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5032 4489 603 41 0 4991 0
vsize: 20128
[startup+730.094 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4511 0 0 0 72971 33 0 0 25 0 1 0 539529099 20611072 4489 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4489 603 41 0 4991 0
vsize: 20128
[startup+740.094 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4511 0 0 0 73971 33 0 0 25 0 1 0 539529099 20611072 4489 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4489 603 41 0 4991 0
vsize: 20128
[startup+750.094 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4511 0 0 0 74961 33 0 0 24 0 1 0 539529099 20611072 4489 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4489 603 41 0 4991 0
vsize: 20128
[startup+760.095 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4511 0 0 0 75961 33 0 0 25 0 1 0 539529099 20611072 4489 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4489 603 41 0 4991 0
vsize: 20128
[startup+770.095 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4512 0 0 0 76961 33 0 0 25 0 1 0 539529099 20611072 4490 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4490 603 41 0 4991 0
vsize: 20128
[startup+780.095 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4512 0 0 0 77961 33 0 0 25 0 1 0 539529099 20611072 4490 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4490 603 41 0 4991 0
vsize: 20128
[startup+790.094 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4512 0 0 0 78961 33 0 0 25 0 1 0 539529099 20611072 4490 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4490 603 41 0 4991 0
vsize: 20128
[startup+800.094 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4512 0 0 0 79961 33 0 0 25 0 1 0 539529099 20611072 4490 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4490 603 41 0 4991 0
vsize: 20128
[startup+810.098 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4514 0 0 0 80962 33 0 0 25 0 1 0 539529099 20611072 4492 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4492 603 41 0 4991 0
vsize: 20128
[startup+820.098 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4514 0 0 0 81962 33 0 0 25 0 1 0 539529099 20611072 4492 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4492 603 41 0 4991 0
vsize: 20128
[startup+830.099 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4514 0 0 0 82962 33 0 0 25 0 1 0 539529099 20611072 4492 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4492 603 41 0 4991 0
vsize: 20128
[startup+840.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4517 0 0 0 83964 33 0 0 25 0 1 0 539529099 20611072 4495 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4495 603 41 0 4991 0
vsize: 20128
[startup+850.108 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4517 0 0 0 84963 33 0 0 25 0 1 0 539529099 20611072 4495 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4495 603 41 0 4991 0
vsize: 20128
[startup+860.107 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4517 0 0 0 85963 33 0 0 25 0 1 0 539529099 20611072 4495 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4495 603 41 0 4991 0
vsize: 20128
[startup+870.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4517 0 0 0 86964 33 0 0 25 0 1 0 539529099 20611072 4495 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4495 603 41 0 4991 0
vsize: 20128
[startup+880.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4517 0 0 0 87964 33 0 0 25 0 1 0 539529099 20611072 4495 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4495 603 41 0 4991 0
vsize: 20128
[startup+890.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4517 0 0 0 88964 33 0 0 25 0 1 0 539529099 20611072 4495 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4495 603 41 0 4991 0
vsize: 20128
[startup+900.217 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4517 0 0 0 89973 33 0 0 25 0 1 0 539529099 20611072 4495 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4495 603 41 0 4991 0
vsize: 20128
[startup+910.217 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4517 0 0 0 90973 33 0 0 25 0 1 0 539529099 20611072 4495 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4495 603 41 0 4991 0
vsize: 20128
[startup+920.216 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4517 0 0 0 91973 33 0 0 25 0 1 0 539529099 20611072 4495 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4495 603 41 0 4991 0
vsize: 20128
[startup+930.217 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4517 0 0 0 92973 33 0 0 25 0 1 0 539529099 20611072 4495 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4495 603 41 0 4991 0
vsize: 20128
[startup+940.218 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4517 0 0 0 93973 34 0 0 25 0 1 0 539529099 20611072 4495 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4495 603 41 0 4991 0
vsize: 20128
[startup+950.217 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4517 0 0 0 94974 34 0 0 25 0 1 0 539529099 20611072 4495 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4495 603 41 0 4991 0
vsize: 20128
[startup+960.218 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4517 0 0 0 95974 34 0 0 25 0 1 0 539529099 20611072 4495 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4495 603 41 0 4991 0
vsize: 20128
[startup+970.225 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4517 0 0 0 96975 34 0 0 25 0 1 0 539529099 20611072 4495 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4495 603 41 0 4991 0
vsize: 20128
[startup+980.226 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4518 0 0 0 97975 34 0 0 25 0 1 0 539529099 20611072 4496 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4496 603 41 0 4991 0
vsize: 20128
[startup+990.249 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4518 0 0 0 98977 34 0 0 25 0 1 0 539529099 20611072 4496 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4496 603 41 0 4991 0
vsize: 20128
[startup+1000.25 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4518 0 0 0 99977 34 0 0 25 0 1 0 539529099 20611072 4496 4294967295 134512640 134672761 3221224544 3221223728 134559332 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4496 603 41 0 4991 0
vsize: 20128
[startup+1010.25 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4518 0 0 0 100977 34 0 0 25 0 1 0 539529099 20611072 4496 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4496 603 41 0 4991 0
vsize: 20128
[startup+1020.26 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4518 0 0 0 101978 34 0 0 25 0 1 0 539529099 20611072 4496 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4496 603 41 0 4991 0
vsize: 20128
[startup+1030.26 s]
Raw data (loadavg): 1.12 1.00 0.92 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4518 0 0 0 102978 34 0 0 25 0 1 0 539529099 20611072 4496 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4496 603 41 0 4991 0
vsize: 20128
[startup+1040.28 s]
Raw data (loadavg): 1.10 1.00 0.92 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4518 0 0 0 103979 34 0 0 25 0 1 0 539529099 20611072 4496 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4496 603 41 0 4991 0
vsize: 20128
[startup+1050.29 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4518 0 0 0 104981 34 0 0 25 0 1 0 539529099 20611072 4496 4294967295 134512640 134672761 3221224544 3221223648 134554877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4496 603 41 0 4991 0
vsize: 20128
[startup+1060.29 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4520 0 0 0 105981 34 0 0 25 0 1 0 539529099 20611072 4498 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4498 603 41 0 4991 0
vsize: 20128
[startup+1070.29 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4523 0 0 0 106982 34 0 0 25 0 1 0 539529099 20611072 4501 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4501 603 41 0 4991 0
vsize: 20128
[startup+1080.29 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4523 0 0 0 107981 34 0 0 25 0 1 0 539529099 20611072 4501 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4501 603 41 0 4991 0
vsize: 20128
[startup+1090.3 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4523 0 0 0 108982 34 0 0 25 0 1 0 539529099 20611072 4501 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4501 603 41 0 4991 0
vsize: 20128
[startup+1100.3 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4523 0 0 0 109982 34 0 0 25 0 1 0 539529099 20611072 4501 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4501 603 41 0 4991 0
vsize: 20128
[startup+1110.32 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4529 0 0 0 110984 34 0 0 25 0 1 0 539529099 20758528 4507 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5068 4507 603 41 0 5027 0
vsize: 20272
[startup+1120.32 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4606 0 0 0 111984 34 0 0 25 0 1 0 539529099 21024768 4584 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5133 4584 603 41 0 5092 0
vsize: 20532
[startup+1130.32 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4975 0 0 0 112983 35 0 0 25 0 1 0 539529099 22511616 4953 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5496 4953 603 41 0 5455 0
vsize: 21984
[startup+1140.32 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4987 0 0 0 113983 35 0 0 25 0 1 0 539529099 22654976 4965 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5531 4965 603 41 0 5490 0
vsize: 22124
[startup+1150.32 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 5010 0 0 0 114983 35 0 0 25 0 1 0 539529099 22654976 4988 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5531 4988 603 41 0 5490 0
vsize: 22124
[startup+1160.32 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 5453 0 0 0 115983 36 0 0 25 0 1 0 539529099 24526848 5431 4294967295 134512640 134672761 3221224544 3221223728 134558648 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5988 5431 603 41 0 5947 0
vsize: 23952
[startup+1170.32 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 5896 0 0 0 116982 37 0 0 25 0 1 0 539529099 26255360 5874 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6410 5874 603 41 0 6369 0
vsize: 25640
[startup+1180.32 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 5968 0 0 0 117981 38 0 0 25 0 1 0 539529099 26660864 5946 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6509 5946 603 41 0 6468 0
vsize: 26036
[startup+1190.32 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 5968 0 0 0 118981 38 0 0 25 0 1 0 539529099 26660864 5946 4294967295 134512640 134672761 3221224544 3221223728 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6509 5946 603 41 0 6468 0
vsize: 26036
[startup+1200.32 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22137
Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 5968 0 0 0 119981 39 0 0 25 0 1 0 539529099 26660864 5946 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6509 5946 603 41 0 6468 0
vsize: 26036
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.34 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 22137
Raw data (stat): 22135 (minisat+) Z 22134 3260 3259 0 -1 12 5971 0 0 0 119981 40 0 0 25 0 1 0 539529099 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.34
CPU time (s): 1200.22
CPU user time (s): 1199.82
CPU system time (s): 0.403938
CPU usage (%): 99.9901
Max. virtual memory (Kb): 26036
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####