PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-p0201.opb
MD5SUM	8c361d02d5162bb0b133ab6ed38f9294
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1523
Optimality of the best value was proved	NO
Number of terms in the objective function	201
Biggest coefficient in the objective function	1920
Number of bits for the biggest coefficient in the objective function	11
Sum of the numbers in the objective function	19980
Number of bits of the sum of numbers in the objective function	15
Biggest number in a constraint	1920
Number of bits of the biggest number in a constraint	11
Biggest sum of numbers in a constraint	19980
Number of bits of the biggest sum of numbers	15
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02284
Number of variables	201
Total number of constraints	334
Number of constraints which are clauses	20
Number of constraints which are cardinality constraints (but not clauses)	227
Number of constraints which are nor clauses,nor cardinality constraints	87
Minimum length of a constraint	1
Maximum length of a constraint	67
Trace number 18014

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.220
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        806524 kB
Buffers:         22784 kB
Cached:         185572 kB
SwapCached:        744 kB
Active:          64228 kB
Inactive:       146104 kB
HighTotal:      131008 kB
HighFree:        39592 kB
LowTotal:       903652 kB
LowFree:        766932 kB
SwapTotal:     2097892 kB
SwapFree:      2096220 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           4992 kB
Slab:            12136 kB
Committed_AS:    63588 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 13:30:16 (client local time) WITH STATUS 10 IN 1200.14 SECONDS
stats: 18705 7 1200.14 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 133 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################
c   -- Clauses(.)/Splits(s): sssss
c ---[ 137]---> BDD-cost:    3
c ---[ 136]---> BDD-cost:    3
c ---[ 135]---> BDD-cost:    3
c ---[ 133]---> BDD-cost:   15
c ---[ 131]---> BDD-cost:   15
c ---[ 129]---> BDD-cost:   15
c ---[ 127]---> BDD-cost:   15
c ---[ 125]---> BDD-cost:   15
c ---[ 123]---> BDD-cost:   15
c ---[ 121]---> BDD-cost:   15
c ---[ 119]---> BDD-cost:   15
c ---[ 117]---> BDD-cost:   15
c ---[ 115]---> BDD-cost:   15
c ---[ 113]---> BDD-cost:   15
c ---[ 111]---> BDD-cost:   15
c ---[ 109]---> BDD-cost:   15
c ---[ 107]---> BDD-cost:   15
c ---[ 105]---> BDD-cost:   15
c ---[ 103]---> BDD-cost:   15
c ---[ 101]---> BDD-cost:   15
c ---[  99]---> BDD-cost:   15
c ---[  97]---> BDD-cost:   15
c ---[  95]---> BDD-cost:   15
c ---[  89]---> BDD-cost:   39
c ---[  88]---> BDD-cost:   42
c ---[  87]---> BDD-cost:   42
c ---[  86]---> BDD-cost:   54
c ---[  85]---> BDD-cost:   73
c ---[  84]---> BDD-cost:   73
c ---[  83]---> BDD-cost:   98
c ---[  82]---> BDD-cost:   85
c ---[  81]---> BDD-cost:   85
c ---[  80]---> BDD-cost:  160
c ---[  79]---> BDD-cost:  107
c ---[  78]---> BDD-cost:  107
c ---[  77]---> BDD-cost:  201
c ---[  76]---> BDD-cost:  128
c ---[  75]---> BDD-cost:  128
c ---[  74]---> BDD-cost:  241
c ---[  73]---> BDD-cost:  150
c ---[  72]---> BDD-cost:  150
c ---[  71]---> BDD-cost:  281
c ---[  70]---> BDD-cost:  172
c ---[  69]---> BDD-cost:  172
c ---[  68]---> BDD-cost:  321
c ---[  67]---> BDD-cost:  194
c ---[  66]---> BDD-cost:  194
c ---[  65]---> BDD-cost:  361
c ---[  64]---> BDD-cost:    3
c ---[  63]---> BDD-cost:    3
c ---[  62]---> BDD-cost:    3
c ---[  61]---> BDD-cost:    3
c ---[  60]---> BDD-cost:    3
c ---[  59]---> BDD-cost:    3
c ---[  58]---> BDD-cost:    9
c ---[  57]---> BDD-cost:   11
c ---[  56]---> BDD-cost:   11
c ---[  55]---> BDD-cost:    9
c ---[  54]---> BDD-cost:   11
c ---[  53]---> BDD-cost:   11
c ---[  52]---> BDD-cost:    9
c ---[  51]---> BDD-cost:   11
c ---[  50]---> BDD-cost:   11
c ---[  49]---> BDD-cost:    9
c ---[  48]---> BDD-cost:   11
c ---[  47]---> BDD-cost:   11
c ---[  46]---> BDD-cost:    9
c ---[  45]---> BDD-cost:   11
c ---[  44]---> BDD-cost:   11
c ---[  43]---> BDD-cost:    9
c ---[  42]---> BDD-cost:   11
c ---[  41]---> BDD-cost:   11
c ---[  40]---> BDD-cost:    9
c ---[  39]---> BDD-cost:   11
c ---[  38]---> BDD-cost:   11
c ---[  37]---> BDD-cost:    9
c ---[  36]---> BDD-cost:   11
c ---[  35]---> BDD-cost:   11
c ---[  34]---> BDD-cost:    9
c ---[  33]---> BDD-cost:   11
c ---[  32]---> BDD-cost:   11
c ---[  31]---> BDD-cost:    9
c ---[  30]---> BDD-cost:   11
c ---[  29]---> BDD-cost:   11
c ---[  28]---> BDD-cost:    9
c ---[  27]---> BDD-cost:   11
c ---[  26]---> BDD-cost:   11
c ---[  25]---> BDD-cost:    9
c ---[  24]---> BDD-cost:   11
c ---[  23]---> BDD-cost:   11
c ---[  22]---> BDD-cost:    9
c ---[  21]---> BDD-cost:   11
c ---[  20]---> BDD-cost:   11
c ---[  19]---> BDD-cost:    9
c ---[  18]---> BDD-cost:   11
c ---[  17]---> BDD-cost:   11
c ---[  16]---> BDD-cost:    9
c ---[  15]---> BDD-cost:   11
c ---[  14]---> BDD-cost:   11
c ---[  13]---> BDD-cost:    9
c ---[  12]---> BDD-cost:   11
c ---[  11]---> BDD-cost:   11
c ---[  10]---> BDD-cost:    9
c ---[   9]---> BDD-cost:   11
c ---[   8]---> BDD-cost:   11
c ---[   7]---> BDD-cost:    9
c ---[   6]---> BDD-cost:   11
c ---[   5]---> BDD-cost:   11
c ---[   4]---> BDD-cost:    1
c ---[   3]---> BDD-cost:    1
c ---[   2]---> BDD-cost:    1
c ---[   1]---> BDD-cost:    1
c ---[   0]---> BDD-cost:    1
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   11741    34621 |    3522       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4624          
c   -- var.elim.:  2000/4624          
c   -- var.elim.:  3000/4624          
c   -- var.elim.:  4000/4624          
c   -- var.elim.:  4624/4624          
c   -- var.elim.:  1000/1249          
c   -- var.elim.:  1249/1249          
c   -- subsuming                       
c   -- var.elim.:  1000/1056          
c   -- var.elim.:  1056/1056          
c   -- var.elim.:  355/355          
c   -- subsuming                       
c   -- var.elim.:  60/60          
c |         0 |   10127    50233 |      --       0       --      -- |     --   | -1614/15927
c |         0 |   10127    50233 |    4050       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 1.27381 s)
c ==============================================================================
c [1mFound solution: 2179[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:21098     Base: 5 2 3 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |        29 |   56899   159451 |   17069      29      236     8.1 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/18366          
c   -- var.elim.:  2000/18366          
c   -- var.elim.:  3000/18366          
c   -- var.elim.:  4000/18366          
c   -- var.elim.:  5000/18366          
c   -- var.elim.:  6000/18366          
c   -- var.elim.:  7000/18366          
c   -- var.elim.:  8000/18366          
c   -- var.elim.:  9000/18366          
c   -- var.elim.:  10000/18366          
c   -- var.elim.:  11000/18366          
c   -- var.elim.:  12000/18366          
c   -- var.elim.:  13000/18366          
c   -- var.elim.:  14000/18366          
c   -- var.elim.:  15000/18366          
c   -- var.elim.:  16000/18366          
c   -- var.elim.:  17000/18366          
c   -- var.elim.:  18000/18366          
c   -- var.elim.:  18366/18366          
c   -- var.elim.:  1000/9788          
c   -- var.elim.:  2000/9788          
c   -- var.elim.:  3000/9788          
c   -- var.elim.:  4000/9788          
c   -- var.elim.:  5000/9788          
c   -- var.elim.:  6000/9788          
c   -- var.elim.:  7000/9788          
c   -- var.elim.:  8000/9788          
c   -- var.elim.:  9000/9788          
c   -- var.elim.:  9788/9788          
c   -- var.elim.:  226/226          
c   -- var.elim.:  379/379          
c   -- subsuming                       
c   -- var.elim.:  1000/2416          
c   -- var.elim.:  2000/2416          
c   -- var.elim.:  2416/2416          
c   -- var.elim.:  810/810          
c   -- var.elim.:  85/85          
c   -- subsuming                       
c   -- var.elim.:  286/286          
c   -- var.elim.:  32/32          
c |        29 |   50913   185351 |      --      29       --      -- |     --   | -5986/25901
c |        29 |   50913   185351 |   20365      29      236     8.1 |  0.000 % |
c |       129 |   50534   183439 |   22234     126     2017    16.0 |  1.251 % |
c |       280 |   46387   169012 |   22451     236     5240    22.2 |  6.332 % |
c |       505 |   45858   167232 |   24414     452    43000    95.1 |  7.017 % |
c |       842 |   45791   167030 |   26817     782    68357    87.4 |  7.175 % |
c ==============================================================================
c (current CPU-time: 8.12776 s)
c ==============================================================================
c [1mFound solution: 2110[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 3 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       988 |   46055   167801 |   13816     927    81633    88.1 |  7.175 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2384          
c   -- var.elim.:  2000/2384          
c   -- var.elim.:  2384/2384          
c   -- var.elim.:  1000/2123          
c   -- var.elim.:  2000/2123          
c   -- var.elim.:  2123/2123          
c   -- var.elim.:  940/940          
c   -- var.elim.:  786/786          
c   -- var.elim.:  387/387          
c   -- subsuming                       
c   -- var.elim.:  928/928          
c   -- var.elim.:  98/98          
c |       988 |   44981   166457 |      --     927       --      -- |     --   | -1069/-1333
c |       988 |   44981   166457 |   17992     720    32289    44.8 |  7.175 % |
c |      1088 |   44981   166457 |   19791     820    38955    47.5 |  7.806 % |
c |      1239 |   44889   166018 |   21726     969    44833    46.3 |  7.899 % |
c ==============================================================================
c (current CPU-time: 10.2084 s)
c ==============================================================================
c [1mFound solution: 2058[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 2 3 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1441 |   44975   165863 |   13492    1168    57904    49.6 |  7.899 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1580          
c   -- var.elim.:  1580/1580          
c   -- var.elim.:  791/791          
c   -- var.elim.:  328/328          
c   -- var.elim.:  326/326          
c   -- var.elim.:  227/227          
c   -- subsuming                       
c   -- var.elim.:  359/359          
c   -- var.elim.:  39/39          
c |      1441 |   44674   165701 |      --    1168       --      -- |     --   | -296/-151
c |      1441 |   44674   165701 |   17869    1154    54983    47.6 |  7.899 % |
c |      1541 |   44674   165701 |   19656    1254    77529    61.8 |  8.255 % |
c |      1691 |   44513   165154 |   21544    1403    82178    58.6 |  8.426 % |
c |      1917 |   44310   163959 |   23590    1628   113721    69.9 |  8.611 % |
c |      2254 |   41256   151869 |   24161    1903   128053    67.3 | 12.260 % |
c ==============================================================================
c (current CPU-time: 13.235 s)
c ==============================================================================
c [1mFound solution: 2040[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 3 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2573 |   40659   149690 |   12197    2210   143432    64.9 | 12.260 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2386          
c   -- var.elim.:  2000/2386          
c   -- var.elim.:  2386/2386          
c   -- var.elim.:  1000/2019          
c   -- var.elim.:  2000/2019          
c   -- var.elim.:  2019/2019          
c   -- var.elim.:  573/573          
c   -- var.elim.:  753/753          
c   -- var.elim.:  251/251          
c   -- var.elim.:  68/68          
c   -- subsuming                       
c   -- var.elim.:  929/929          
c   -- var.elim.:  141/141          
c   -- var.elim.:  9/9          
c |      2573 |   40038   150349 |      --    2210       --      -- |     --   | -619/664
c |      2573 |   40038   150349 |   16015    1853    63009    34.0 | 12.260 % |
c |      2673 |   40024   150300 |   17610    1952    64440    33.0 | 13.505 % |
c |      2825 |   40024   150300 |   19371    2103    74331    35.3 | 13.505 % |
c |      3050 |   39895   149523 |   21240    2322    88414    38.1 | 13.648 % |
c ==============================================================================
c (current CPU-time: 15.4107 s)
c ==============================================================================
c [1mFound solution: 2018[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 3 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      3129 |   39929   149755 |   11978    2401    96552    40.2 | 13.648 % |
c   -- subsuming                       
c   -- var.elim.:  548/548          
c   -- var.elim.:  413/413          
c   -- var.elim.:  103/103          
c   -- subsuming                       
c   -- var.elim.:  169/169          
c |      3129 |   39879   150331 |      --    2401       --      -- |     --   | -49/579
c |      3129 |   39879   150331 |   15951    2354    92182    39.2 | 13.648 % |
c |      3229 |   39879   150331 |   17546    2454    94173    38.4 | 13.681 % |
c |      3379 |   38941   146564 |   18847    2578   100269    38.9 | 14.685 % |
c |      3604 |   38570   145283 |   20534    2792   102951    36.9 | 15.163 % |
c |      3942 |   38489   145013 |   22540    3124   140677    45.0 | 15.267 % |
c ==============================================================================
c (current CPU-time: 18.2272 s)
c ==============================================================================
c [1mFound solution: 1993[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 2 3 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4440 |   38344   144720 |   11503    3614   190783    52.8 | 15.267 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1125          
c   -- var.elim.:  1125/1125          
c   -- var.elim.:  1000/1068          
c   -- var.elim.:  1068/1068          
c   -- var.elim.:  423/423          
c   -- var.elim.:  241/241          
c   -- var.elim.:  80/80          
c   -- subsuming                       
c   -- var.elim.:  196/196          
c   -- var.elim.:  33/33          
c |      4440 |   37876   143859 |      --    3614       --      -- |     --   | -467/-858
c |      4440 |   37876   143859 |   15150    3176   118170    37.2 | 15.267 % |
c |      4540 |   37876   143859 |   16665    3276   122353    37.3 | 15.956 % |
c |      4691 |   37876   143859 |   18331    3427   128267    37.4 | 15.956 % |
c |      4917 |   37603   142710 |   20019    3649   141340    38.7 | 16.206 % |
c |      5254 |   37430   142133 |   21920    3977   148730    37.4 | 16.400 % |
c ==============================================================================
c (current CPU-time: 21.1068 s)
c ==============================================================================
c [1mFound solution: 1919[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 3 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      5517 |   37608   142689 |   11282    4236   213097    50.3 | 16.400 % |
c   -- subsuming                       
c   -- var.elim.:  887/887          
c   -- var.elim.:  816/816          
c   -- var.elim.:  32/32          
c   -- var.elim.:  2/2          
c   -- subsuming                       
c   -- var.elim.:  209/209          
c   -- var.elim.:  8/8          
c |      5517 |   37391   143162 |      --    4236       --      -- |     --   | -201/509
c |      5517 |   37391   143162 |   14956    4081   156873    38.4 | 16.400 % |
c |      5618 |   37178   142079 |   16358    4180   160211    38.3 | 16.815 % |
c |      5768 |   37072   141708 |   17942    4323   163200    37.8 | 16.944 % |
c |      5993 |   37066   141689 |   19733    4547   182718    40.2 | 16.960 % |
c |      6330 |   37066   141689 |   21707    4884   201052    41.2 | 16.960 % |
c |      6836 |   37066   141689 |   23878    5390   255312    47.4 | 16.960 % |
c ==============================================================================
c (current CPU-time: 24.9702 s)
c ==============================================================================
c [1mFound solution: 1858[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 3 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      6936 |   37156   142034 |   11146    5490   258105    47.0 | 16.960 % |
c   -- subsuming                       
c   -- var.elim.:  652/652          
c   -- var.elim.:  620/620          
c   -- var.elim.:  158/158          
c   -- subsuming                       
c   -- var.elim.:  226/226          
c   -- var.elim.:  4/4          
c |      6936 |   37042   142973 |      --    5490       --      -- |     --   | -107/955
c |      6936 |   37042   142973 |   14816    5034   192376    38.2 | 16.960 % |
c |      7037 |   37042   142973 |   16298    5135   196980    38.4 | 17.038 % |
c |      7187 |   37037   142953 |   17925    5280   213049    40.4 | 17.046 % |
c |      7412 |   36740   140951 |   19560    5502   223844    40.7 | 17.346 % |
c |      7749 |   36740   140951 |   21516    5839   246654    42.2 | 17.346 % |
c |      8257 |   36288   139349 |   23376    6321   275380    43.6 | 17.775 % |
c ==============================================================================
c (current CPU-time: 29.7055 s)
c ==============================================================================
c [1mFound solution: 1796[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 3 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      8603 |   36384   139721 |   10915    6667   301298    45.2 | 17.775 % |
c   -- subsuming                       
c   -- var.elim.:  949/949          
c   -- var.elim.:  762/762          
c   -- var.elim.:  165/165          
c   -- var.elim.:  67/67          
c   -- subsuming                       
c   -- var.elim.:  169/169          
c   -- var.elim.:  21/21          
c |      8603 |   36194   139857 |      --    6667       --      -- |     --   | -184/149
c |      8603 |   36194   139857 |   14477    6398   269179    42.1 | 17.775 % |
c |      8704 |   36194   139857 |   15925    6499   275431    42.4 | 17.961 % |
c |      8859 |   36194   139857 |   17517    6654   288899    43.4 | 17.961 % |
c |      9085 |   36194   139857 |   19269    6880   306911    44.6 | 17.961 % |
c ==============================================================================
c (current CPU-time: 31.9012 s)
c ==============================================================================
c [1mFound solution: 1728[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 3 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      9294 |   36288   140259 |   10886    7089   333913    47.1 | 17.961 % |
c   -- subsuming                       
c   -- var.elim.:  308/308          
c   -- var.elim.:  303/303          
c   -- var.elim.:  176/176          
c   -- var.elim.:  178/178          
c |      9294 |   36196   140155 |      --    7089       --      -- |     --   | -90/-99
c |      9294 |   36196   140155 |   14478    7009   322443    46.0 | 17.961 % |
c |      9394 |   36196   140155 |   15926    7109   327399    46.1 | 17.972 % |
c |      9546 |   36123   139915 |   17483    7257   343350    47.3 | 18.054 % |
c |      9771 |   36123   139915 |   19231    7482   368335    49.2 | 18.054 % |
c |     10109 |   35606   137861 |   20852    7808   393186    50.4 | 18.616 % |
c |     10615 |   35606   137861 |   22937    8314   459656    55.3 | 18.616 % |
c |     11376 |   35606   137861 |   25231    9075   586055    64.6 | 18.616 % |
c |     12515 |   35585   137796 |   27738   10211   752344    73.7 | 18.665 % |
c |     14225 |   34605   133995 |   29671   11893  1023732    86.1 | 19.886 % |
c |     16788 |   34605   133995 |   32638   14456  1234156    85.4 | 19.886 % |
c ==============================================================================
c (current CPU-time: 53.4749 s)
c ==============================================================================
c [1mFound solution: 1721[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 3 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     17072 |   34625   134143 |   10387   14740  1286555    87.3 | 19.886 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1306          
c   -- var.elim.:  1306/1306          
c   -- var.elim.:  1000/1321          
c   -- var.elim.:  1321/1321          
c   -- var.elim.:  683/683          
c   -- var.elim.:  618/618          
c   -- var.elim.:  187/187          
c   -- subsuming                       
c   -- var.elim.:  848/848          
c   -- var.elim.:  452/452          
c |     17072 |   34341   135086 |      --   14740       --      -- |     --   | -283/946
c |     17072 |   34341   135086 |   13736   11943   611032    51.2 | 19.886 % |
c |     17172 |   34341   135086 |   15110   12043   625869    52.0 | 20.210 % |
c |     17322 |   34130   134362 |   16518   12188   631029    51.8 | 20.458 % |
c |     17547 |   34130   134362 |   18170   12413   645645    52.0 | 20.458 % |
c |     17884 |   34130   134362 |   19987   12750   688033    54.0 | 20.458 % |
c |     18392 |   34109   134297 |   21973   13255   790711    59.7 | 20.508 % |
c |     19151 |   34061   134056 |   24136   14011   867175    61.9 | 20.615 % |
c |     20292 |   34029   133955 |   26525   15144   972095    64.2 | 20.681 % |
c |     22000 |   34024   133939 |   29173   16851  1279425    75.9 | 20.690 % |
c |     24563 |   34024   133939 |   32090   19414  1805068    93.0 | 20.690 % |
c |     28408 |   34024   133939 |   35299   23259  2575438   110.7 | 20.690 % |
c |     34174 |   33527   130779 |   38262   28982  3507655   121.0 | 21.227 % |
c ==============================================================================
c (current CPU-time: 111.4 s)
c ==============================================================================
c [1mFound solution: 1714[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 3 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     35166 |   33615   131092 |   10084   29971  3629557   121.1 | 21.227 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1757          
c   -- var.elim.:  1757/1757          
c   -- var.elim.:  1000/1324          
c   -- var.elim.:  1324/1324          
c   -- var.elim.:  43/43          
c   -- var.elim.:  78/78          
c   -- subsuming                       
c   -- var.elim.:  722/722          
c   -- var.elim.:  204/204          
c |     35166 |   33410   131988 |      --   29971       --      -- |     --   | -203/901
c |     35166 |   33410   131988 |   13364   22099  1078456    48.8 | 21.227 % |
c |     35266 |   33410   131988 |   14700   10537   379123    36.0 | 21.413 % |
c |     35416 |   33197   130747 |   16067   10685   385857    36.1 | 21.630 % |
c |     35642 |   33197   130747 |   17674   10911   412111    37.8 | 21.630 % |
c |     35981 |   33161   130634 |   19420   11241   443750    39.5 | 21.713 % |
c |     36487 |   33161   130634 |   21362   11747   532184    45.3 | 21.713 % |
c |     37246 |   33161   130634 |   23498   12506   659820    52.8 | 21.713 % |
c |     38386 |   33161   130634 |   25848   13646   866368    63.5 | 21.713 % |
c |     40095 |   33147   130589 |   28421   15354  1198982    78.1 | 21.730 % |
c ==============================================================================
c (current CPU-time: 126.248 s)
c ==============================================================================
c [1mFound solution: 1710[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 3 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     40229 |   32917   129102 |    9875   15479  1210468    78.2 | 21.730 % |
c   -- subsuming                       
c   -- var.elim.:  987/987          
c   -- var.elim.:  1000/1067          
c   -- var.elim.:  1067/1067          
c   -- var.elim.:  425/425          
c   -- var.elim.:  288/288          
c   -- subsuming                       
c   -- var.elim.:  532/532          
c |     40229 |   32735   130137 |      --   15479       --      -- |     --   | -178/1044
c |     40229 |   32735   130137 |   13094   15479  1210468    78.2 | 21.730 % |
c |     40329 |   32735   130137 |   14403   15579  1212674    77.8 | 22.201 % |
c |     40479 |   32735   130137 |   15843   15729  1215941    77.3 | 22.201 % |
c |     40705 |   32735   130137 |   17428   15955  1252593    78.5 | 22.201 % |
c |     41042 |   32735   130137 |   19170   16292  1287697    79.0 | 22.201 % |
c |     41548 |   32519   129382 |   20948   15841   947215    59.8 | 22.435 % |
c |     42307 |   32512   129362 |   23038   16599  1076177    64.8 | 22.444 % |
c |     43446 |   32507   129342 |   25338   17725  1282169    72.3 | 22.452 % |
c |     45154 |   32507   129342 |   27872   19433  1667376    85.8 | 22.452 % |
c |     47716 |   32280   128496 |   30445   21978  2143494    97.5 | 22.703 % |
c |     51560 |   32231   128349 |   33439   25815  3047085   118.0 | 22.762 % |
c ==============================================================================
c (current CPU-time: 183.112 s)
c ==============================================================================
c [1mFound solution: 1707[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 3 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     56576 |   32447   128955 |    9734   30828  4095135   132.8 | 22.762 % |
c   -- subsuming                       
c   -- var.elim.:  860/860          
c   -- var.elim.:  586/586          
c   -- var.elim.:  49/49          
c   -- subsuming                       
c   -- var.elim.:  151/151          
c |     56576 |   32227   128890 |      --   30828       --      -- |     --   | -210/-44
c |     56576 |   32227   128890 |   12890   25126  1914313    76.2 | 22.762 % |
c |     56677 |   32227   128890 |   14179   13017   967020    74.3 | 22.872 % |
c |     56827 |   32227   128890 |   15597   13167   987913    75.0 | 22.872 % |
c |     57052 |   32222   128874 |   17154   13390  1004408    75.0 | 22.880 % |
c |     57390 |   32222   128874 |   18870   13728  1045288    76.1 | 22.880 % |
c |     57897 |   32191   128762 |   20737   14234  1129254    79.3 | 22.914 % |
c ==============================================================================
c (current CPU-time: 190.986 s)
c ==============================================================================
c [1mFound solution: 1706[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 3 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     58590 |   32210   128907 |    9662   14927  1226559    82.2 | 22.914 % |
c   -- subsuming                       
c   -- var.elim.:  160/160          
c   -- var.elim.:  199/199          
c   -- var.elim.:  49/49          
c |     58590 |   32194   128893 |      --   14927       --      -- |     --   | -16/-13
c |     58590 |   32194   128893 |   12877   13669   884745    64.7 | 22.914 % |
c |     58691 |   32194   128893 |   14165   13770   902436    65.5 | 22.928 % |
c |     58843 |   32189   128877 |   15579   13918   917727    65.9 | 22.936 % |
c |     59068 |   32189   128877 |   17137   14143   958504    67.8 | 22.936 % |
c |     59405 |   32189   128877 |   18851   14480  1022609    70.6 | 22.936 % |
c |     59914 |   32189   128877 |   20736   14989  1071923    71.5 | 22.936 % |
c |     60673 |   32142   128720 |   22776   15745  1187821    75.4 | 22.978 % |
c |     61812 |   32142   128720 |   25054   16884  1397967    82.8 | 22.978 % |
c |     63520 |   31956   127065 |   27400   18586  1655422    89.1 | 23.171 % |
c |     66082 |   31952   127053 |   30136   21138  2044209    96.7 | 23.179 % |
c |     69927 |   31714   126257 |   32903   24970  2749424   110.1 | 23.490 % |
c |     75694 |   31208   124124 |   35616   30709  4199777   136.8 | 24.043 % |
c ==============================================================================
c (current CPU-time: 269.81 s)
c ==============================================================================
c [1mFound solution: 1704[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 3 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     79985 |   31241   124250 |    9372   34954  4909549   140.5 | 24.043 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1120          
c   -- var.elim.:  1120/1120          
c   -- var.elim.:  1000/1099          
c   -- var.elim.:  1099/1099          
c   -- var.elim.:  591/591          
c   -- var.elim.:  626/626          
c   -- var.elim.:  582/582          
c   -- var.elim.:  326/326          
c   -- subsuming                       
c   -- var.elim.:  601/601          
c   -- var.elim.:  29/29          
c |     79985 |   30895   124299 |      --   34954       --      -- |     --   | -342/58
c |     79985 |   30895   124299 |   12358   25895  1815691    70.1 | 24.043 % |
c |     80085 |   30889   124278 |   13591   12897   708897    55.0 | 24.476 % |
c |     80236 |   30889   124278 |   14950   13048   714058    54.7 | 24.476 % |
c |     80462 |   30889   124278 |   16445   13274   742439    55.9 | 24.476 % |
c |     80799 |   30889   124278 |   18089   13611   790500    58.1 | 24.476 % |
c |     81307 |   30889   124278 |   19898   14119   806153    57.1 | 24.476 % |
c |     82067 |   30889   124278 |   21888   14879   948295    63.7 | 24.476 % |
c |     83209 |   30889   124278 |   24077   16021  1220457    76.2 | 24.476 % |
c |     84918 |   30889   124278 |   26485   17730  1518536    85.6 | 24.476 % |
c |     87480 |   30889   124278 |   29133   20292  2069775   102.0 | 24.476 % |
c |     91326 |   30889   124278 |   32047   24138  2775961   115.0 | 24.476 % |
c |     97092 |   30889   124278 |   35251   29904  3597056   120.3 | 24.476 % |
c ==============================================================================
c (current CPU-time: 364.456 s)
c ==============================================================================
c [1mFound solution: 1703[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 3 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    104034 |   31006   124640 |    9301   36843  5115014   138.8 | 24.476 % |
c   -- subsuming                       
c   -- var.elim.:  267/267          
c   -- var.elim.:  216/216          
c   -- var.elim.:  103/103          
c   -- var.elim.:  2/2          
c |    104034 |   30878   124398 |      --   36843       --      -- |     --   | -127/-239
c |    104034 |   30878   124398 |   12351   32685  3710751   113.5 | 24.476 % |
c |    104135 |   30755   123921 |   13532   15205  1471765    96.8 | 24.612 % |
c |    104286 |   30755   123921 |   14885   15356  1494458    97.3 | 24.612 % |
c |    104512 |   30744   123859 |   16368   15578  1519916    97.6 | 24.654 % |
c |    104850 |   30744   123859 |   18004   15916  1578494    99.2 | 24.654 % |
c |    105356 |   30744   123859 |   19805   16422  1644182   100.1 | 24.654 % |
c |    106115 |   30744   123859 |   21785   17181  1785308   103.9 | 24.654 % |
c |    107254 |   30744   123859 |   23964   18320  1898677   103.6 | 24.654 % |
c |    108962 |   30744   123859 |   26360   20028  2250995   112.4 | 24.654 % |
c |    111525 |   30744   123859 |   28997   22591  2635346   116.7 | 24.654 % |
c |    115370 |   30738   123838 |   31890   26435  3424205   129.5 | 24.663 % |
c |    121136 |   30417   122575 |   34713   32178  4324932   134.4 | 25.061 % |
c |    129785 |   30325   122083 |   38069   19968  2538414   127.1 | 25.163 % |
c |    142761 |   30027   120406 |   41464   32938  6090613   184.9 | 25.503 % |
c |    162222 |   29945   119722 |   45486   23365  3594317   153.8 | 25.587 % |
c |    191415 |   29846   119415 |   49869   20541  3331169   162.2 | 25.731 % |
c ==============================================================================
c (current CPU-time: 784.46 s)
c ==============================================================================
c [1mFound solution: 1701[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 3 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    205392 |   29905   119657 |    8971   34495  7187571   208.4 | 25.731 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1332          
c   -- var.elim.:  1332/1332          
c   -- var.elim.:  1000/1535          
c   -- var.elim.:  1535/1535          
c   -- var.elim.:  862/862          
c   -- var.elim.:  586/586          
c   -- subsuming                       
c   -- var.elim.:  883/883          
c   -- var.elim.:  32/32          
c |    205392 |   29592   119055 |      --   34495       --      -- |     --   | -311/-597
c |    205392 |   29592   119055 |   11836   20948  1446269    69.0 | 25.731 % |
c |    205493 |   29592   119055 |   13020    9739   714047    73.3 | 26.127 % |
c |    205644 |   29592   119055 |   14322    9890   724340    73.2 | 26.127 % |
c |    205869 |   29592   119055 |   15754   10115   755412    74.7 | 26.127 % |
c |    206206 |   29592   119055 |   17330   10452   816582    78.1 | 26.127 % |
c |    206716 |   29592   119055 |   19063   10962   893083    81.5 | 26.127 % |
c |    207478 |   29592   119055 |   20969   11724   972731    83.0 | 26.127 % |
c |    208617 |   29587   119039 |   23062   12860  1147196    89.2 | 26.135 % |
c ==============================================================================
c (current CPU-time: 798.675 s)
c ==============================================================================
c [1mFound solution: 1693[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 3 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    209783 |   29685   119392 |    8905   14026  1362318    97.1 | 26.135 % |
c   -- subsuming                       
c   -- var.elim.:  240/240          
c   -- var.elim.:  199/199          
c   -- var.elim.:  74/74          
c   -- var.elim.:  44/44          
c |    209783 |   29592   119263 |      --   14026       --      -- |     --   | -91/-124
c |    209783 |   29592   119263 |   11836   13974  1353877    96.9 | 26.135 % |
c |    209883 |   29592   119263 |   13020   14074  1358366    96.5 | 26.157 % |
c |    210033 |   29592   119263 |   14322   14224  1375823    96.7 | 26.158 % |
c |    210260 |   29592   119263 |   15754   14451  1415562    98.0 | 26.157 % |
c |    210598 |   29592   119263 |   17330   14789  1471364    99.5 | 26.157 % |
c |    211104 |   29592   119263 |   19063   15295  1552997   101.5 | 26.157 % |
c |    211864 |   29592   119263 |   20969   16055  1665154   103.7 | 26.157 % |
c |    213003 |   29592   119263 |   23066   17194  1908317   111.0 | 26.157 % |
c |    214712 |   29592   119263 |   25373   18903  2135902   113.0 | 26.157 % |
c |    217277 |   29592   119263 |   27910   21468  2681732   124.9 | 26.157 % |
c |    221122 |   29587   119250 |   30696   25310  3477334   137.4 | 26.166 % |
c |    226889 |   29587   119250 |   33766   31077  4882683   157.1 | 26.166 % |
c ==============================================================================
c (current CPU-time: 895.814 s)
c ==============================================================================
c [1mFound solution: 1680[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 3 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    235303 |   29761   119753 |    8928   18698  2969607   158.8 | 26.166 % |
c   -- subsuming                       
c   -- var.elim.:  319/319          
c   -- var.elim.:  230/230          
c   -- var.elim.:  166/166          
c   -- var.elim.:  110/110          
c   -- var.elim.:  108/108          
c |    235303 |   29592   119379 |      --   18698       --      -- |     --   | -167/-369
c |    235303 |   29592   119379 |   11836   18655  2961532   158.8 | 26.166 % |
c |    235403 |   29592   119379 |   13020   12537  1549085   123.6 | 26.178 % |
c |    235553 |   29592   119379 |   14322   12687  1561375   123.1 | 26.178 % |
c |    235778 |   29592   119379 |   15754   12912  1587604   123.0 | 26.178 % |
c |    236115 |   29592   119379 |   17330   13249  1625929   122.7 | 26.178 % |
c |    236623 |   29592   119379 |   19063   13757  1699757   123.6 | 26.178 % |
c |    237385 |   29592   119379 |   20969   14519  1801541   124.1 | 26.178 % |
c |    238527 |   29592   119379 |   23066   15661  1979846   126.4 | 26.178 % |
c |    240236 |   29592   119379 |   25373   17370  2216528   127.6 | 26.178 % |
c |    242798 |   29592   119379 |   27910   19932  2682373   134.6 | 26.178 % |
c |    246642 |   29581   119338 |   30690   23768  3107135   130.7 | 26.195 % |
c |    252408 |   29581   119338 |   33759   29534  4279500   144.9 | 26.195 % |
c ==============================================================================
c (current CPU-time: 976.204 s)
c ==============================================================================
c [1mFound solution: 1676[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 3 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    257785 |   29680   119659 |    8903   34911  5312285   152.2 | 26.195 % |
c   -- subsuming                       
c   -- var.elim.:  234/234          
c   -- var.elim.:  177/177          
c   -- var.elim.:  121/121          
c |    257785 |   29583   119464 |      --   34911       --      -- |     --   | -97/-194
c |    257785 |   29583   119464 |   11833   32754  4860380   148.4 | 26.195 % |
c |    257885 |   29572   119429 |   13011   10469  1297199   123.9 | 26.234 % |
c |    258035 |   29572   119429 |   14312   10619  1312908   123.6 | 26.234 % |
c |    258260 |   29572   119429 |   15744   10844  1323462   122.0 | 26.234 % |
c |    258598 |   29572   119429 |   17318   11182  1371279   122.6 | 26.234 % |
c |    259106 |   29572   119429 |   19050   11690  1414100   121.0 | 26.234 % |
c |    259865 |   29566   119409 |   20951   12446  1518123   122.0 | 26.242 % |
c |    261005 |   29566   119409 |   23046   13586  1584228   116.6 | 26.242 % |
c ==============================================================================
c (current CPU-time: 990.407 s)
c ==============================================================================
c [1mFound solution: 1674[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 3 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    262367 |   29710   119846 |    8912   14948  1811543   121.2 | 26.242 % |
c   -- subsuming                       
c   -- var.elim.:  279/279          
c   -- var.elim.:  209/209          
c   -- var.elim.:  148/148          
c |    262367 |   29574   119633 |      --   14948       --      -- |     --   | -135/-210
c |    262367 |   29574   119633 |   11829   14944  1811455   121.2 | 26.242 % |
c |    262470 |   29574   119633 |   13012   10066   978874    97.2 | 26.248 % |
c |    262620 |   29574   119633 |   14313   10216   989629    96.9 | 26.248 % |
c |    262846 |   29574   119633 |   15745   10442  1018887    97.6 | 26.248 % |
c |    263183 |   29569   119620 |   17316   10778  1060906    98.4 | 26.257 % |
c |    263689 |   29569   119620 |   19048   11284  1141706   101.2 | 26.257 % |
c |    264450 |   29569   119620 |   20953   12045  1273488   105.7 | 26.257 % |
c |    265592 |   29569   119620 |   23048   13187  1510277   114.5 | 26.257 % |
c ==============================================================================
c (current CPU-time: 1006.11 s)
c ==============================================================================
c [1mFound solution: 1668[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 3 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    267291 |   29673   119992 |    8901   14886  1880053   126.3 | 26.257 % |
c   -- subsuming                       
c   -- var.elim.:  262/262          
c   -- var.elim.:  207/207          
c   -- var.elim.:  130/130          
c |    267291 |   29576   119870 |      --   14886       --      -- |     --   | -97/-121
c |    267291 |   29576   119870 |   11830   14886  1880053   126.3 | 26.257 % |
c |    267391 |   29576   119870 |   13013   10024  1180970   117.8 | 26.266 % |
c |    267542 |   29576   119870 |   14314   10175  1205346   118.5 | 26.266 % |
c |    267775 |   29576   119870 |   15746   10408  1227816   118.0 | 26.266 % |
c |    268113 |   29576   119870 |   17320   10746  1295927   120.6 | 26.266 % |
c |    268620 |   29576   119870 |   19052   11253  1325933   117.8 | 26.266 % |
c |    269379 |   29576   119870 |   20958   12012  1465321   122.0 | 26.266 % |
c |    270520 |   29576   119870 |   23054   13153  1548742   117.7 | 26.266 % |
c |    272229 |   29565   119834 |   25350   14859  1888396   127.1 | 26.283 % |
c ==============================================================================
c (current CPU-time: 1026.11 s)
c ==============================================================================
c [1mFound solution: 1667[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 3 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    273554 |   29707   120298 |    8912   16184  2134997   131.9 | 26.283 % |
c   -- subsuming                       
c   -- var.elim.:  314/314          
c   -- var.elim.:  235/235          
c   -- var.elim.:  143/143          
c   -- var.elim.:  111/111          
c |    273554 |   29573   120392 |      --   16184       --      -- |     --   | -133/97
c |    273554 |   29573   120392 |   11829   15694  2007220   127.9 | 26.283 % |
c |    273655 |   29573   120392 |   13012   10564  1139654   107.9 | 26.300 % |
c |    273806 |   29573   120392 |   14313   10715  1163193   108.6 | 26.300 % |
c |    274031 |   29573   120392 |   15744   10940  1178101   107.7 | 26.300 % |
c |    274369 |   29573   120392 |   17319   11278  1249635   110.8 | 26.300 % |
c |    274875 |   29573   120392 |   19051   11784  1331954   113.0 | 26.300 % |
c |    275634 |   29573   120392 |   20956   12543  1475191   117.6 | 26.300 % |
c |    276773 |   29573   120392 |   23051   13682  1714801   125.3 | 26.300 % |
c |    278484 |   29573   120392 |   25356   15393  2066557   134.3 | 26.300 % |
c |    281046 |   29573   120392 |   27892   17955  2496483   139.0 | 26.300 % |
c |    284891 |   29573   120392 |   30681   21800  3389005   155.5 | 26.300 % |
c |    290657 |   29472   118843 |   33634   27562  4719645   171.2 | 26.403 % |
c ==============================================================================
c (current CPU-time: 1099.03 s)
c ==============================================================================
c [1mFound solution: 1656[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 3 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    294568 |   29572   119164 |    8871   31473  5545007   176.2 | 26.403 % |
c   -- subsuming                       
c   -- var.elim.:  664/664          
c   -- var.elim.:  696/696          
c   -- var.elim.:  87/87          
c   -- subsuming                       
c   -- var.elim.:  472/472          
c   -- var.elim.:  8/8          
c |    294568 |   29460   120248 |      --   31473       --      -- |     --   | -112/1085
c |    294568 |   29460   120248 |   11784   31434  5534395   176.1 | 26.403 % |
c |    294668 |   29460   120248 |   12962   11195  1864412   166.5 | 26.457 % |
c |    294818 |   29460   120248 |   14258   11345  1880068   165.7 | 26.457 % |
c |    295043 |   29451   120220 |   15679   11569  1912658   165.3 | 26.465 % |
c |    295382 |   29451   120220 |   17247   11908  1958515   164.5 | 26.465 % |
c |    295888 |   29451   120220 |   18972   12414  2027680   163.3 | 26.465 % |
c |    296649 |   29451   120220 |   20869   13175  2122412   161.1 | 26.465 % |
c ==============================================================================
c (current CPU-time: 1109.41 s)
c ==============================================================================
c [1mFound solution: 1655[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 3 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    297188 |   29587   120637 |    8876   13714  2236057   163.0 | 26.465 % |
c   -- subsuming                       
c   -- var.elim.:  273/273          
c   -- var.elim.:  233/233          
c   -- var.elim.:  113/113          
c   -- var.elim.:  64/64          
c   -- var.elim.:  63/63          
c |    297188 |   29453   120346 |      --   13714       --      -- |     --   | -134/-290
c |    297188 |   29453   120346 |   11781   13496  2094104   155.2 | 26.465 % |
c |    297288 |   29453   120346 |   12959   13596  2095769   154.1 | 26.476 % |
c |    297440 |   29440   120293 |   14248   13747  2107609   153.3 | 26.485 % |
c |    297666 |   29440   120#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.97 0.91 2/54 6444
Raw data (stat): 6444 (runsolver) R 6443 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 545342413 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+9.99993 s]
Raw data (loadavg): 0.87 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 4841 0 0 0 982 16 0 0 25 0 1 0 545342413 18628608 3911 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4548 3911 603 41 0 4507 0
vsize: 18192
[startup+20.0005 s]
Raw data (loadavg): 0.89 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 7780 0 0 0 1970 27 0 0 25 0 1 0 545342413 18296832 3844 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4467 3844 603 41 0 4426 0
vsize: 17868
[startup+30.0003 s]
Raw data (loadavg): 0.91 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 9556 0 0 0 2962 35 0 0 25 0 1 0 545342413 19132416 4052 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4671 4052 603 41 0 4630 0
vsize: 18684
[startup+40.0009 s]
Raw data (loadavg): 0.92 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 10864 0 0 0 3957 40 0 0 25 0 1 0 545342413 19611648 4162 4294967295 134512640 134672761 3221224544 3221223688 134616317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4788 4162 603 41 0 4747 0
vsize: 19152
[startup+50.0012 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 11365 0 0 0 4955 42 0 0 25 0 1 0 545342413 21721088 4663 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5303 4663 603 41 0 5262 0
vsize: 21212
[startup+60.0013 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 12362 0 0 0 5950 47 0 0 25 0 1 0 545342413 23363584 5079 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5704 5079 603 41 0 5663 0
vsize: 22816
[startup+70.0017 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 12362 0 0 0 6949 47 0 0 25 0 1 0 545342413 23363584 5079 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5704 5079 603 41 0 5663 0
vsize: 22816
[startup+80.002 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 12870 0 0 0 7948 49 0 0 25 0 1 0 545342413 25464832 5587 4294967295 134512640 134672761 3221224544 3221223728 134615581 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6217 5587 603 41 0 6176 0
vsize: 24868
[startup+90.0019 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 13500 0 0 0 8946 51 0 0 25 0 1 0 545342413 28110848 6217 4294967295 134512640 134672761 3221224544 3221223728 134616004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6863 6217 603 41 0 6822 0
vsize: 27452
[startup+100.002 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 14051 0 0 0 9944 53 0 0 25 0 1 0 545342413 30343168 6768 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7408 6768 603 41 0 7367 0
vsize: 29632
[startup+110.001 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 14481 0 0 0 10943 54 0 0 25 0 1 0 545342413 32067584 7198 4294967295 134512640 134672761 3221224544 3221223552 134522549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7829 7198 603 41 0 7788 0
vsize: 31316
[startup+120.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 15356 0 0 0 11939 58 0 0 25 0 1 0 545342413 34242560 7675 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8360 7675 603 41 0 8319 0
vsize: 33440
[startup+130.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 15724 0 0 0 12936 61 0 0 25 0 1 0 545342413 33845248 7648 4294967295 134512640 134672761 3221224544 3221223744 134610622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8263 7648 603 41 0 8222 0
vsize: 33052
[startup+140.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 15724 0 0 0 13936 61 0 0 25 0 1 0 545342413 33845248 7648 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8263 7648 603 41 0 8222 0
vsize: 33052
[startup+150.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 15724 0 0 0 14936 61 0 0 25 0 1 0 545342413 33845248 7648 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8263 7648 603 41 0 8222 0
vsize: 33052
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 15724 0 0 0 15936 61 0 0 25 0 1 0 545342413 33845248 7648 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8263 7648 603 41 0 8222 0
vsize: 33052
[startup+170.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 15724 0 0 0 16937 61 0 0 25 0 1 0 545342413 33845248 7648 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8263 7648 603 41 0 8222 0
vsize: 33052
[startup+180.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 15724 0 0 0 17937 61 0 0 25 0 1 0 545342413 33845248 7648 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8263 7648 603 41 0 8222 0
vsize: 33052
[startup+190.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 16696 0 0 0 18933 65 0 0 25 0 1 0 545342413 36438016 8220 4294967295 134512640 134672761 3221224544 3221223712 134615864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8896 8220 603 41 0 8855 0
vsize: 35584
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 17090 0 0 0 19930 68 0 0 25 0 1 0 545342413 36630528 8282 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8943 8282 603 41 0 8902 0
vsize: 35772
[startup+210.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 17090 0 0 0 20930 68 0 0 25 0 1 0 545342413 36630528 8282 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8943 8282 603 41 0 8902 0
vsize: 35772
[startup+220.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 17090 0 0 0 21930 68 0 0 25 0 1 0 545342413 36630528 8282 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8943 8282 603 41 0 8902 0
vsize: 35772
[startup+230.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 17090 0 0 0 22930 68 0 0 25 0 1 0 545342413 36630528 8282 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8943 8282 603 41 0 8902 0
vsize: 35772
[startup+240.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 17090 0 0 0 23930 68 0 0 25 0 1 0 545342413 36630528 8282 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8943 8282 603 41 0 8902 0
vsize: 35772
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 17090 0 0 0 24931 68 0 0 25 0 1 0 545342413 36630528 8282 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8943 8282 603 41 0 8902 0
vsize: 35772
[startup+260.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 17090 0 0 0 25931 68 0 0 25 0 1 0 545342413 36630528 8282 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8943 8282 603 41 0 8902 0
vsize: 35772
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 17497 0 0 0 26931 68 0 0 25 0 1 0 545342413 38207488 8689 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9328 8689 603 41 0 9287 0
vsize: 37312
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 18329 0 0 0 27925 73 0 0 25 0 1 0 545342413 40247296 9115 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9826 9115 603 41 0 9785 0
vsize: 39304
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 18329 0 0 0 28926 73 0 0 25 0 1 0 545342413 40247296 9115 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9826 9115 603 41 0 9785 0
vsize: 39304
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 18329 0 0 0 29926 73 0 0 25 0 1 0 545342413 40247296 9115 4294967295 134512640 134672761 3221224544 3221223728 134615838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9826 9115 603 41 0 9785 0
vsize: 39304
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 18329 0 0 0 30926 73 0 0 25 0 1 0 545342413 40247296 9115 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9826 9115 603 41 0 9785 0
vsize: 39304
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 18329 0 0 0 31926 73 0 0 25 0 1 0 545342413 40247296 9115 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9826 9115 603 41 0 9785 0
vsize: 39304
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 18329 0 0 0 32926 73 0 0 25 0 1 0 545342413 40247296 9115 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9826 9115 603 41 0 9785 0
vsize: 39304
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 18329 0 0 0 33926 73 0 0 25 0 1 0 545342413 40247296 9115 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9826 9115 603 41 0 9785 0
vsize: 39304
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 18329 0 0 0 34927 73 0 0 25 0 1 0 545342413 40247296 9115 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9826 9115 603 41 0 9785 0
vsize: 39304
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 18329 0 0 0 35927 73 0 0 25 0 1 0 545342413 40247296 9115 4294967295 134512640 134672761 3221224544 3221223584 134613118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9826 9115 603 41 0 9785 0
vsize: 39304
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 19008 0 0 0 36923 77 0 0 25 0 1 0 545342413 41537536 9412 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10141 9412 603 41 0 10100 0
vsize: 40564
[startup+380.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 19008 0 0 0 37923 77 0 0 25 0 1 0 545342413 41537536 9412 4294967295 134512640 134672761 3221224544 3221223584 134612614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10141 9412 603 41 0 10100 0
vsize: 40564
[startup+390.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 19008 0 0 0 38923 77 0 0 25 0 1 0 545342413 41537536 9412 4294967295 134512640 134672761 3221224544 3221223536 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10141 9412 603 41 0 10100 0
vsize: 40564
[startup+400.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 19008 0 0 0 39923 77 0 0 25 0 1 0 545342413 41537536 9412 4294967295 134512640 134672761 3221224544 3221223728 134615796 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10141 9412 603 41 0 10100 0
vsize: 40564
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 19008 0 0 0 40923 77 0 0 25 0 1 0 545342413 41537536 9412 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10141 9412 603 41 0 10100 0
vsize: 40564
[startup+420.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 19008 0 0 0 41924 77 0 0 25 0 1 0 545342413 41537536 9412 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10141 9412 603 41 0 10100 0
vsize: 40564
[startup+430.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 19008 0 0 0 42924 77 0 0 25 0 1 0 545342413 41537536 9412 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10141 9412 603 41 0 10100 0
vsize: 40564
[startup+440.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 19008 0 0 0 43924 77 0 0 25 0 1 0 545342413 41537536 9412 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10141 9412 603 41 0 10100 0
vsize: 40564
[startup+450.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 19009 0 0 0 44924 77 0 0 25 0 1 0 545342413 41537536 9413 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10141 9413 603 41 0 10100 0
vsize: 40564
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 19325 0 0 0 45924 77 0 0 25 0 1 0 545342413 42553344 9729 4294967295 134512640 134672761 3221224544 3221223640 134616181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10389 9729 603 41 0 10348 0
vsize: 41556
[startup+470.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 19325 0 0 0 46924 77 0 0 25 0 1 0 545342413 42291200 9691 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10325 9691 603 41 0 10284 0
vsize: 41300
[startup+480.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 19325 0 0 0 47924 77 0 0 25 0 1 0 545342413 42291200 9691 4294967295 134512640 134672761 3221224544 3221223728 134615838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10325 9691 603 41 0 10284 0
vsize: 41300
[startup+490.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 19325 0 0 0 48924 77 0 0 25 0 1 0 545342413 42291200 9691 4294967295 134512640 134672761 3221224544 3221223728 134615838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10325 9691 603 41 0 10284 0
vsize: 41300
[startup+500.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 19325 0 0 0 49925 77 0 0 25 0 1 0 545342413 42291200 9691 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10325 9691 603 41 0 10284 0
vsize: 41300
[startup+510.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 19500 0 0 0 50924 78 0 0 25 0 1 0 545342413 43089920 9866 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10520 9866 603 41 0 10479 0
vsize: 42080
[startup+520.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 20086 0 0 0 51922 80 0 0 25 0 1 0 545342413 45445120 10452 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11095 10452 603 41 0 11054 0
vsize: 44380
[startup+530.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 20528 0 0 0 52921 81 0 0 25 0 1 0 545342413 47284224 10894 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11544 10894 603 41 0 11503 0
vsize: 46176
[startup+540.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 21011 0 0 0 53920 82 0 0 25 0 1 0 545342413 49250304 11377 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12024 11377 603 41 0 11983 0
vsize: 48096
[startup+550.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 21451 0 0 0 54920 83 0 0 25 0 1 0 545342413 51093504 11817 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12474 11817 603 41 0 12433 0
vsize: 49896
[startup+560.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 21774 0 0 0 55919 83 0 0 25 0 1 0 545342413 52432896 12140 4294967295 134512640 134672761 3221224544 3221223744 134610642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12801 12140 603 41 0 12760 0
vsize: 51204
[startup+570.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 22330 0 0 0 56918 85 0 0 25 0 1 0 545342413 54669312 12696 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13347 12696 603 41 0 13306 0
vsize: 53388
[startup+580.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 22945 0 0 0 57917 86 0 0 25 0 1 0 545342413 56901632 13265 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13892 13265 603 41 0 13851 0
vsize: 55568
[startup+590.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 22945 0 0 0 58917 86 0 0 25 0 1 0 545342413 56901632 13265 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13892 13265 603 41 0 13851 0
vsize: 55568
[startup+600.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 22945 0 0 0 59917 86 0 0 25 0 1 0 545342413 56901632 13265 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13892 13265 603 41 0 13851 0
vsize: 55568
[startup+610.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 22945 0 0 0 60917 86 0 0 25 0 1 0 545342413 56901632 13265 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13892 13265 603 41 0 13851 0
vsize: 55568
[startup+620.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 22945 0 0 0 61917 86 0 0 25 0 1 0 545342413 56901632 13265 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13892 13265 603 41 0 13851 0
vsize: 55568
[startup+630.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 22945 0 0 0 62918 86 0 0 25 0 1 0 545342413 56901632 13265 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13892 13265 603 41 0 13851 0
vsize: 55568
[startup+640.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 22945 0 0 0 63918 87 0 0 25 0 1 0 545342413 56901632 13265 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13892 13265 603 41 0 13851 0
vsize: 55568
[startup+650.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 22945 0 0 0 64918 87 0 0 25 0 1 0 545342413 56901632 13265 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13892 13265 603 41 0 13851 0
vsize: 55568
[startup+660.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 22945 0 0 0 65918 87 0 0 25 0 1 0 545342413 56901632 13265 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13892 13265 603 41 0 13851 0
vsize: 55568
[startup+670.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 22945 0 0 0 66918 87 0 0 25 0 1 0 545342413 56901632 13265 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13892 13265 603 41 0 13851 0
vsize: 55568
[startup+680.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 22945 0 0 0 67919 87 0 0 25 0 1 0 545342413 56901632 13265 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13892 13265 603 41 0 13851 0
vsize: 55568
[startup+690.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 22945 0 0 0 68919 87 0 0 25 0 1 0 545342413 56901632 13265 4294967295 134512640 134672761 3221224544 3221223680 134614685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13892 13265 603 41 0 13851 0
vsize: 55568
[startup+700.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 22945 0 0 0 69919 87 0 0 25 0 1 0 545342413 56901632 13265 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13892 13265 603 41 0 13851 0
vsize: 55568
[startup+710.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 22947 0 0 0 70919 87 0 0 25 0 1 0 545342413 56901632 13267 4294967295 134512640 134672761 3221224544 3221223728 134615996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13892 13267 603 41 0 13851 0
vsize: 55568
[startup+720.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 23074 0 0 0 71919 87 0 0 25 0 1 0 545342413 57339904 13376 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13999 13376 603 41 0 13958 0
vsize: 55996
[startup+730.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 23074 0 0 0 72919 87 0 0 25 0 1 0 545342413 57339904 13376 4294967295 134512640 134672761 3221224544 3221223680 134614825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13999 13376 603 41 0 13958 0
vsize: 55996
[startup+740.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 23074 0 0 0 73919 87 0 0 25 0 1 0 545342413 57339904 13376 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13999 13376 603 41 0 13958 0
vsize: 55996
[startup+750.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 23074 0 0 0 74920 87 0 0 25 0 1 0 545342413 57339904 13376 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13999 13376 603 41 0 13958 0
vsize: 55996
[startup+760.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 23074 0 0 0 75920 87 0 0 25 0 1 0 545342413 57339904 13376 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13999 13376 603 41 0 13958 0
vsize: 55996
[startup+770.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 23074 0 0 0 76920 87 0 0 25 0 1 0 545342413 57339904 13376 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13999 13376 603 41 0 13958 0
vsize: 55996
[startup+780.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 23074 0 0 0 77920 87 0 0 25 0 1 0 545342413 57339904 13376 4294967295 134512640 134672761 3221224544 3221223728 134615523 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13999 13376 603 41 0 13958 0
vsize: 55996
[startup+790.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 23948 0 0 0 78917 90 0 0 25 0 1 0 545342413 57589760 13415 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14060 13415 603 41 0 14019 0
vsize: 56240
[startup+800.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 24332 0 0 0 79913 94 0 0 25 0 1 0 545342413 57589760 13415 4294967295 134512640 134672761 3221224544 3221223800 134616181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14060 13415 603 41 0 14019 0
vsize: 56240
[startup+810.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 24332 0 0 0 80914 94 0 0 25 0 1 0 545342413 57589760 13415 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14060 13415 603 41 0 14019 0
vsize: 56240
[startup+820.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 24332 0 0 0 81914 94 0 0 25 0 1 0 545342413 57589760 13415 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14060 13415 603 41 0 14019 0
vsize: 56240
[startup+830.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 24332 0 0 0 82914 94 0 0 25 0 1 0 545342413 57589760 13415 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14060 13415 603 41 0 14019 0
vsize: 56240
[startup+840.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 24332 0 0 0 83914 94 0 0 25 0 1 0 545342413 57589760 13415 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14060 13415 603 41 0 14019 0
vsize: 56240
[startup+850.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 24332 0 0 0 84914 94 0 0 25 0 1 0 545342413 57589760 13415 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14060 13415 603 41 0 14019 0
vsize: 56240
[startup+860.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 24332 0 0 0 85915 94 0 0 25 0 1 0 545342413 57589760 13415 4294967295 134512640 134672761 3221224544 3221223728 134616004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14060 13415 603 41 0 14019 0
vsize: 56240
[startup+870.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 24332 0 0 0 86914 94 0 0 25 0 1 0 545342413 57589760 13415 4294967295 134512640 134672761 3221224544 3221223536 134565070 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14060 13415 603 41 0 14019 0
vsize: 56240
[startup+880.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 24332 0 0 0 87915 94 0 0 25 0 1 0 545342413 57589760 13415 4294967295 134512640 134672761 3221224544 3221223728 134615779 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14060 13415 603 41 0 14019 0
vsize: 56240
[startup+890.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 24369 0 0 0 88915 94 0 0 25 0 1 0 545342413 57589760 13415 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14060 13415 603 41 0 14019 0
vsize: 56240
[startup+900.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 24765 0 0 0 89913 96 0 0 25 0 1 0 545342413 57589760 13419 4294967295 134512640 134672761 3221224544 3221223680 134614812 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14060 13419 603 41 0 14019 0
vsize: 56240
[startup+910.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 24765 0 0 0 90912 96 0 0 25 0 1 0 545342413 57589760 13419 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14060 13419 603 41 0 14019 0
vsize: 56240
[startup+920.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 24765 0 0 0 91912 96 0 0 25 0 1 0 545342413 57589760 13419 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14060 13419 603 41 0 14019 0
vsize: 56240
[startup+930.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 24765 0 0 0 92913 96 0 0 25 0 1 0 545342413 57589760 13419 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14060 13419 603 41 0 14019 0
vsize: 56240
[startup+940.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 24765 0 0 0 93913 96 0 0 25 0 1 0 545342413 57589760 13419 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14060 13419 603 41 0 14019 0
vsize: 56240
[startup+950.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 24765 0 0 0 94913 96 0 0 25 0 1 0 545342413 57589760 13419 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14060 13419 603 41 0 14019 0
vsize: 56240
[startup+960.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 24765 0 0 0 95913 96 0 0 25 0 1 0 545342413 57589760 13419 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14060 13419 603 41 0 14019 0
vsize: 56240
[startup+970.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 24765 0 0 0 96913 96 0 0 25 0 1 0 545342413 57589760 13419 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14060 13419 603 41 0 14019 0
vsize: 56240
[startup+980.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 25162 0 0 0 97911 99 0 0 25 0 1 0 545342413 57589760 13421 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14060 13421 603 41 0 14019 0
vsize: 56240
[startup+990.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 25162 0 0 0 98910 99 0 0 25 0 1 0 545342413 57589760 13421 4294967295 134512640 134672761 3221224544 3221223744 134610622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14060 13421 603 41 0 14019 0
vsize: 56240
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 25559 0 0 0 99907 101 0 0 25 0 1 0 545342413 57540608 13409 4294967295 134512640 134672761 3221224544 3221223696 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14048 13409 603 41 0 14007 0
vsize: 56192
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 25965 0 0 0 100904 104 0 0 25 0 1 0 545342413 57540608 13411 4294967295 134512640 134672761 3221224544 3221223628 1074733103 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14048 13411 603 41 0 14007 0
vsize: 56192
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 25965 0 0 0 101905 104 0 0 25 0 1 0 545342413 57540608 13411 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14048 13411 603 41 0 14007 0
vsize: 56192
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 26315 0 0 0 102902 106 0 0 25 0 1 0 545342413 57540608 13411 4294967295 134512640 134672761 3221224544 3221223728 134615505 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14048 13411 603 41 0 14007 0
vsize: 56192
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 26315 0 0 0 103903 106 0 0 25 0 1 0 545342413 57540608 13411 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14048 13411 603 41 0 14007 0
vsize: 56192
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 26315 0 0 0 104903 107 0 0 25 0 1 0 545342413 57540608 13411 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14048 13411 603 41 0 14007 0
vsize: 56192
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 26315 0 0 0 105902 107 0 0 25 0 1 0 545342413 57540608 13411 4294967295 134512640 134672761 3221224544 3221223696 134541817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14048 13411 603 41 0 14007 0
vsize: 56192
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 26315 0 0 0 106902 107 0 0 25 0 1 0 545342413 57540608 13411 4294967295 134512640 134672761 3221224544 3221223680 134614822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14048 13411 603 41 0 14007 0
vsize: 56192
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 26315 0 0 0 107902 107 0 0 25 0 1 0 545342413 57540608 13411 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14048 13411 603 41 0 14007 0
vsize: 56192
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 26315 0 0 0 108902 108 0 0 25 0 1 0 545342413 57540608 13411 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14048 13411 603 41 0 14007 0
vsize: 56192
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 26315 0 0 0 109901 108 0 0 25 0 1 0 545342413 57540608 13411 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14048 13411 603 41 0 14007 0
vsize: 56192
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 26726 0 0 0 110899 110 0 0 25 0 1 0 545342413 57540608 13418 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14048 13418 603 41 0 14007 0
vsize: 56192
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 27079 0 0 0 111897 112 0 0 25 0 1 0 545342413 57540608 13420 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14048 13420 603 41 0 14007 0
vsize: 56192
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 27079 0 0 0 112897 113 0 0 25 0 1 0 545342413 57540608 13420 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14048 13420 603 41 0 14007 0
vsize: 56192
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 27079 0 0 0 113897 113 0 0 25 0 1 0 545342413 57540608 13420 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14048 13420 603 41 0 14007 0
vsize: 56192
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 27079 0 0 0 114897 113 0 0 25 0 1 0 545342413 57540608 13420 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14048 13420 603 41 0 14007 0
vsize: 56192
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 27079 0 0 0 115896 113 0 0 25 0 1 0 545342413 57540608 13420 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14048 13420 603 41 0 14007 0
vsize: 56192
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 27079 0 0 0 116896 114 0 0 25 0 1 0 545342413 57540608 13420 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14048 13420 603 41 0 14007 0
vsize: 56192
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 27079 0 0 0 117896 114 0 0 25 0 1 0 545342413 57540608 13420 4294967295 134512640 134672761 3221224544 3221223744 134610602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14048 13420 603 41 0 14007 0
vsize: 56192
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 27079 0 0 0 118896 114 0 0 25 0 1 0 545342413 57540608 13420 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14048 13420 603 41 0 14007 0
vsize: 56192
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6444
Raw data (stat): 6444 (minisat+) R 6443 28099 28098 0 -1 0 27079 0 0 0 119896 115 0 0 25 0 1 0 545342413 57540608 13420 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14048 13420 603 41 0 14007 0
vsize: 56192
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 6444
Raw data (stat): 6444 (minisat+) Z 6443 28099 28098 0 -1 12 27080 0 0 0 119896 117 0 0 25 0 1 0 545342413 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.06
CPU time (s): 1200.14
CPU user time (s): 1198.96
CPU system time (s): 1.17982
CPU usage (%): 100.007
Max. virtual memory (Kb): 56240
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####