PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-p0201.opb
MD5SUM	ffa3a55eb53181880328dd1b84f91e66
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 22071

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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:        360532 kB
Buffers:         22680 kB
Cached:         630340 kB
SwapCached:        392 kB
Active:          96128 kB
Inactive:       559048 kB
HighTotal:      131008 kB
HighFree:          336 kB
LowTotal:       903652 kB
LowFree:        360196 kB
SwapTotal:     2097136 kB
SwapFree:      2095968 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5748 kB
Slab:            13228 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 02:23:35 (client local time) WITH STATUS 10 IN 1200.15 SECONDS
stats: 12127 7 1200.15 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.27181 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.19575 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.2804 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.311 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.4806 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.2912 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.1768 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: 25.0612 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.8535 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: 32.0771 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.9178 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: 112.262 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: 127.29 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: 184.607 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: 192.451 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: 271.987 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: 366.753 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: 786.02 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: 800.366 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: 897.351 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: 977.691 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: 991.757 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: 1007.41 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: 1027.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.31 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.6 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   12#### 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.66 0.90 0.97 2/54 792
Raw data (stat): 792 (runsolver) R 791 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 491755170 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99982 s]
Raw data (loadavg): 0.71 0.91 0.97 2/54 792
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 4841 0 0 0 981 17 0 0 25 0 1 0 491755170 18628608 3911 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4548 3911 603 41 0 4507 0
vsize: 18192
[startup+20.0005 s]
Raw data (loadavg): 0.75 0.91 0.97 2/54 792
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 7780 0 0 0 1970 29 0 0 25 0 1 0 491755170 18296832 3844 4294967295 134512640 134672761 3221224544 3221223584 134603565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4467 3844 603 41 0 4426 0
vsize: 17868
[startup+30.0015 s]
Raw data (loadavg): 0.79 0.91 0.97 2/54 792
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 9556 0 0 0 2963 36 0 0 25 0 1 0 491755170 19132416 4052 4294967295 134512640 134672761 3221224544 3221223728 134615665 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.0012 s]
Raw data (loadavg): 0.82 0.91 0.97 2/54 792
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 10857 0 0 0 3957 42 0 0 25 0 1 0 491755170 19611648 4155 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4788 4155 603 41 0 4747 0
vsize: 19152
[startup+50.0014 s]
Raw data (loadavg): 0.85 0.92 0.97 2/54 792
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 11350 0 0 0 4955 44 0 0 25 0 1 0 491755170 21590016 4648 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5271 4648 603 41 0 5230 0
vsize: 21084
[startup+60.0015 s]
Raw data (loadavg): 0.87 0.92 0.97 2/54 792
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 12362 0 0 0 5951 48 0 0 25 0 1 0 491755170 23363584 5079 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5704 5079 603 41 0 5663 0
vsize: 22816
[startup+70.0032 s]
Raw data (loadavg): 0.89 0.92 0.97 2/54 792
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 12362 0 0 0 6951 49 0 0 25 0 1 0 491755170 23363584 5079 4294967295 134512640 134672761 3221224544 3221223728 134615711 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.0034 s]
Raw data (loadavg): 0.91 0.92 0.97 2/54 792
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 12826 0 0 0 7949 50 0 0 25 0 1 0 491755170 25333760 5543 4294967295 134512640 134672761 3221224544 3221223680 134614800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6185 5543 603 41 0 6144 0
vsize: 24740
[startup+90.0035 s]
Raw data (loadavg): 0.92 0.92 0.97 2/54 792
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 13466 0 0 0 8947 53 0 0 25 0 1 0 491755170 27975680 6183 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6830 6183 603 41 0 6789 0
vsize: 27320
[startup+100.004 s]
Raw data (loadavg): 0.93 0.93 0.97 2/54 792
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 14003 0 0 0 9944 55 0 0 25 0 1 0 491755170 30081024 6720 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7344 6720 603 41 0 7303 0
vsize: 29376
[startup+110.004 s]
Raw data (loadavg): 0.94 0.93 0.97 2/54 792
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 14449 0 0 0 10943 56 0 0 25 0 1 0 491755170 31928320 7166 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7795 7166 603 41 0 7754 0
vsize: 31180
[startup+120.005 s]
Raw data (loadavg): 0.95 0.93 0.97 2/54 792
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 15356 0 0 0 11939 61 0 0 25 0 1 0 491755170 34242560 7675 4294967295 134512640 134672761 3221224544 3221223728 134615619 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.006 s]
Raw data (loadavg): 0.96 0.93 0.97 2/54 792
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 15724 0 0 0 12937 63 0 0 25 0 1 0 491755170 33845248 7648 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8263 7648 603 41 0 8222 0
vsize: 33052
[startup+140.005 s]
Raw data (loadavg): 0.96 0.93 0.97 2/54 792
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 15724 0 0 0 13937 63 0 0 25 0 1 0 491755170 33845248 7648 4294967295 134512640 134672761 3221224544 3221223728 134615549 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.006 s]
Raw data (loadavg): 0.97 0.94 0.97 2/54 792
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 15724 0 0 0 14937 63 0 0 25 0 1 0 491755170 33845248 7648 4294967295 134512640 134672761 3221224544 3221223728 134615625 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.007 s]
Raw data (loadavg): 0.97 0.94 0.97 2/54 792
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 15724 0 0 0 15937 63 0 0 25 0 1 0 491755170 33845248 7648 4294967295 134512640 134672761 3221224544 3221223728 134615625 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.007 s]
Raw data (loadavg): 0.98 0.94 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 15724 0 0 0 16936 64 0 0 25 0 1 0 491755170 33845248 7648 4294967295 134512640 134672761 3221224544 3221223728 134615916 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.008 s]
Raw data (loadavg): 0.98 0.94 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 15724 0 0 0 17936 64 0 0 25 0 1 0 491755170 33845248 7648 4294967295 134512640 134672761 3221224544 3221223728 134615916 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.008 s]
Raw data (loadavg): 0.98 0.94 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 16696 0 0 0 18932 69 0 0 25 0 1 0 491755170 36438016 8220 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8896 8220 603 41 0 8855 0
vsize: 35584
[startup+200.008 s]
Raw data (loadavg): 0.98 0.94 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 17090 0 0 0 19929 71 0 0 25 0 1 0 491755170 36630528 8282 4294967295 134512640 134672761 3221224544 3221223636 1075351210 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.009 s]
Raw data (loadavg): 0.99 0.94 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 17090 0 0 0 20929 72 0 0 25 0 1 0 491755170 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.01 s]
Raw data (loadavg): 0.99 0.95 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 17090 0 0 0 21929 72 0 0 25 0 1 0 491755170 36630528 8282 4294967295 134512640 134672761 3221224544 3221223728 134615583 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.01 s]
Raw data (loadavg): 0.99 0.95 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 17090 0 0 0 22929 73 0 0 25 0 1 0 491755170 36630528 8282 4294967295 134512640 134672761 3221224544 3221223728 134615940 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.01 s]
Raw data (loadavg): 0.99 0.95 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 17090 0 0 0 23929 73 0 0 25 0 1 0 491755170 36630528 8282 4294967295 134512640 134672761 3221224544 3221223728 134615791 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.011 s]
Raw data (loadavg): 0.99 0.95 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 17090 0 0 0 24928 73 0 0 25 0 1 0 491755170 36630528 8282 4294967295 134512640 134672761 3221224544 3221223728 134615747 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.011 s]
Raw data (loadavg): 0.99 0.95 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 17090 0 0 0 25928 73 0 0 25 0 1 0 491755170 36630528 8282 4294967295 134512640 134672761 3221224544 3221223728 134615791 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.012 s]
Raw data (loadavg): 0.99 0.95 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 17441 0 0 0 26927 74 0 0 25 0 1 0 491755170 38076416 8633 4294967295 134512640 134672761 3221224544 3221223536 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9296 8633 603 41 0 9255 0
vsize: 37184
[startup+280.013 s]
Raw data (loadavg): 0.99 0.95 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 18329 0 0 0 27923 78 0 0 25 0 1 0 491755170 40247296 9115 4294967295 134512640 134672761 3221224544 3221223584 134612684 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.013 s]
Raw data (loadavg): 0.99 0.95 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 18329 0 0 0 28923 78 0 0 25 0 1 0 491755170 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+300.014 s]
Raw data (loadavg): 0.99 0.95 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 18329 0 0 0 29923 79 0 0 25 0 1 0 491755170 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+310.015 s]
Raw data (loadavg): 0.99 0.95 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 18329 0 0 0 30923 79 0 0 25 0 1 0 491755170 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+320.015 s]
Raw data (loadavg): 0.99 0.96 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 18329 0 0 0 31923 79 0 0 25 0 1 0 491755170 40247296 9115 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9826 9115 603 41 0 9785 0
vsize: 39304
[startup+330.015 s]
Raw data (loadavg): 0.99 0.96 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 18329 0 0 0 32923 79 0 0 25 0 1 0 491755170 40247296 9115 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9826 9115 603 41 0 9785 0
vsize: 39304
[startup+340.015 s]
Raw data (loadavg): 0.99 0.96 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 18329 0 0 0 33923 79 0 0 25 0 1 0 491755170 40247296 9115 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9826 9115 603 41 0 9785 0
vsize: 39304
[startup+350.015 s]
Raw data (loadavg): 0.99 0.96 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 18329 0 0 0 34924 79 0 0 25 0 1 0 491755170 40247296 9115 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9826 9115 603 41 0 9785 0
vsize: 39304
[startup+360.015 s]
Raw data (loadavg): 0.99 0.96 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 18329 0 0 0 35924 79 0 0 25 0 1 0 491755170 40247296 9115 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9826 9115 603 41 0 9785 0
vsize: 39304
[startup+370.015 s]
Raw data (loadavg): 0.99 0.96 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 19008 0 0 0 36922 81 0 0 25 0 1 0 491755170 41537536 9412 4294967295 134512640 134672761 3221224544 3221223688 134616368 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.015 s]
Raw data (loadavg): 0.99 0.96 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 19008 0 0 0 37921 81 0 0 25 0 1 0 491755170 41537536 9412 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10141 9412 603 41 0 10100 0
vsize: 40564
[startup+390.015 s]
Raw data (loadavg): 0.99 0.96 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 19008 0 0 0 38921 81 0 0 25 0 1 0 491755170 41537536 9412 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10141 9412 603 41 0 10100 0
vsize: 40564
[startup+400.016 s]
Raw data (loadavg): 0.99 0.96 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 19008 0 0 0 39921 81 0 0 25 0 1 0 491755170 41537536 9412 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10141 9412 603 41 0 10100 0
vsize: 40564
[startup+410.016 s]
Raw data (loadavg): 0.99 0.96 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 19008 0 0 0 40921 81 0 0 25 0 1 0 491755170 41537536 9412 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10141 9412 603 41 0 10100 0
vsize: 40564
[startup+420.016 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 19008 0 0 0 41922 81 0 0 25 0 1 0 491755170 41537536 9412 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10141 9412 603 41 0 10100 0
vsize: 40564
[startup+430.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 19008 0 0 0 42922 81 0 0 25 0 1 0 491755170 41537536 9412 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10141 9412 603 41 0 10100 0
vsize: 40564
[startup+440.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 19008 0 0 0 43922 81 0 0 25 0 1 0 491755170 41537536 9412 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10141 9412 603 41 0 10100 0
vsize: 40564
[startup+450.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 19008 0 0 0 44922 81 0 0 25 0 1 0 491755170 41537536 9412 4294967295 134512640 134672761 3221224544 3221223536 134565143 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10141 9412 603 41 0 10100 0
vsize: 40564
[startup+460.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 19168 0 0 0 45922 82 0 0 25 0 1 0 491755170 41926656 9572 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10236 9572 603 41 0 10195 0
vsize: 40944
[startup+470.016 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 19325 0 0 0 46922 82 0 0 25 0 1 0 491755170 42291200 9691 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10325 9691 603 41 0 10284 0
vsize: 41300
[startup+480.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 19325 0 0 0 47922 82 0 0 25 0 1 0 491755170 42291200 9691 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10325 9691 603 41 0 10284 0
vsize: 41300
[startup+490.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 19325 0 0 0 48923 82 0 0 25 0 1 0 491755170 42291200 9691 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10325 9691 603 41 0 10284 0
vsize: 41300
[startup+500.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 19325 0 0 0 49923 82 0 0 25 0 1 0 491755170 42291200 9691 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10325 9691 603 41 0 10284 0
vsize: 41300
[startup+510.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 19424 0 0 0 50923 82 0 0 25 0 1 0 491755170 42696704 9790 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10424 9790 603 41 0 10383 0
vsize: 41696
[startup+520.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 19930 0 0 0 51921 83 0 0 25 0 1 0 491755170 44793856 10296 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10936 10296 603 41 0 10895 0
vsize: 43744
[startup+530.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 20456 0 0 0 52920 84 0 0 25 0 1 0 491755170 47026176 10822 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11481 10822 603 41 0 11440 0
vsize: 45924
[startup+540.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 20941 0 0 0 53919 86 0 0 25 0 1 0 491755170 48988160 11307 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11960 11307 603 41 0 11919 0
vsize: 47840
[startup+550.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 21373 0 0 0 54918 87 0 0 25 0 1 0 491755170 50700288 11739 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12378 11739 603 41 0 12337 0
vsize: 49512
[startup+560.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 21691 0 0 0 55917 88 0 0 25 0 1 0 491755170 52031488 12057 4294967295 134512640 134672761 3221224544 3221223728 134615581 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12703 12057 603 41 0 12662 0
vsize: 50812
[startup+570.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 22236 0 0 0 56916 89 0 0 25 0 1 0 491755170 54272000 12602 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13250 12602 603 41 0 13209 0
vsize: 53000
[startup+580.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 22945 0 0 0 57914 91 0 0 25 0 1 0 491755170 57163776 13311 4294967295 134512640 134672761 3221224544 3221222784 134645448 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13956 13311 603 41 0 13915 0
vsize: 55824
[startup+590.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 22945 0 0 0 58915 91 0 0 25 0 1 0 491755170 56901632 13265 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13892 13265 603 41 0 13851 0
vsize: 55568
[startup+600.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 22945 0 0 0 59915 91 0 0 25 0 1 0 491755170 56901632 13265 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13892 13265 603 41 0 13851 0
vsize: 55568
[startup+610.016 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 22945 0 0 0 60915 91 0 0 25 0 1 0 491755170 56901632 13265 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13892 13265 603 41 0 13851 0
vsize: 55568
[startup+620.016 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 22945 0 0 0 61915 91 0 0 25 0 1 0 491755170 56901632 13265 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13892 13265 603 41 0 13851 0
vsize: 55568
[startup+630.016 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 22945 0 0 0 62915 91 0 0 25 0 1 0 491755170 56901632 13265 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13892 13265 603 41 0 13851 0
vsize: 55568
[startup+640.016 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 22945 0 0 0 63915 91 0 0 25 0 1 0 491755170 56901632 13265 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13892 13265 603 41 0 13851 0
vsize: 55568
[startup+650.016 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 22945 0 0 0 64916 91 0 0 25 0 1 0 491755170 56901632 13265 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13892 13265 603 41 0 13851 0
vsize: 55568
[startup+660.016 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 22945 0 0 0 65916 91 0 0 25 0 1 0 491755170 56901632 13265 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13892 13265 603 41 0 13851 0
vsize: 55568
[startup+670.015 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 22945 0 0 0 66916 91 0 0 25 0 1 0 491755170 56901632 13265 4294967295 134512640 134672761 3221224544 3221223728 134616001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13892 13265 603 41 0 13851 0
vsize: 55568
[startup+680.016 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 22945 0 0 0 67916 91 0 0 25 0 1 0 491755170 56901632 13265 4294967295 134512640 134672761 3221224544 3221223728 134615926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13892 13265 603 41 0 13851 0
vsize: 55568
[startup+690.016 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 22945 0 0 0 68916 91 0 0 25 0 1 0 491755170 56901632 13265 4294967295 134512640 134672761 3221224544 3221223688 134616233 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13892 13265 603 41 0 13851 0
vsize: 55568
[startup+700.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 22945 0 0 0 69916 91 0 0 25 0 1 0 491755170 56901632 13265 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13892 13265 603 41 0 13851 0
vsize: 55568
[startup+710.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 22946 0 0 0 70917 91 0 0 25 0 1 0 491755170 56901632 13266 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13892 13266 603 41 0 13851 0
vsize: 55568
[startup+720.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 22990 0 0 0 71917 91 0 0 25 0 1 0 491755170 57159680 13310 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13955 13310 603 41 0 13914 0
vsize: 55820
[startup+730.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 23074 0 0 0 72917 92 0 0 25 0 1 0 491755170 57339904 13376 4294967295 134512640 134672761 3221224544 3221223696 134541816 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13999 13376 603 41 0 13958 0
vsize: 55996
[startup+740.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 23074 0 0 0 73917 92 0 0 25 0 1 0 491755170 57339904 13376 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13999 13376 603 41 0 13958 0
vsize: 55996
[startup+750.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 23074 0 0 0 74917 92 0 0 25 0 1 0 491755170 57339904 13376 4294967295 134512640 134672761 3221224544 3221223680 134614677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13999 13376 603 41 0 13958 0
vsize: 55996
[startup+760.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 23074 0 0 0 75917 92 0 0 25 0 1 0 491755170 57339904 13376 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13999 13376 603 41 0 13958 0
vsize: 55996
[startup+770.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 23074 0 0 0 76918 92 0 0 25 0 1 0 491755170 57339904 13376 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13999 13376 603 41 0 13958 0
vsize: 55996
[startup+780.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 23074 0 0 0 77918 92 0 0 25 0 1 0 491755170 57339904 13376 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13999 13376 603 41 0 13958 0
vsize: 55996
[startup+790.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 23948 0 0 0 78914 96 0 0 25 0 1 0 491755170 57589760 13415 4294967295 134512640 134672761 3221224544 3221223536 134565092 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.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 23948 0 0 0 79913 96 0 0 25 0 1 0 491755170 57589760 13415 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14060 13415 603 41 0 14019 0
vsize: 56240
[startup+810.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 24332 0 0 0 80910 98 0 0 25 0 1 0 491755170 57589760 13415 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14060 13415 603 41 0 14019 0
vsize: 56240
[startup+820.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 24332 0 0 0 81911 98 0 0 25 0 1 0 491755170 57589760 13415 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14060 13415 603 41 0 14019 0
vsize: 56240
[startup+830.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 24332 0 0 0 82911 98 0 0 25 0 1 0 491755170 57589760 13415 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14060 13415 603 41 0 14019 0
vsize: 56240
[startup+840.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 24332 0 0 0 83911 98 0 0 25 0 1 0 491755170 57589760 13415 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14060 13415 603 41 0 14019 0
vsize: 56240
[startup+850.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 24332 0 0 0 84911 98 0 0 25 0 1 0 491755170 57589760 13415 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14060 13415 603 41 0 14019 0
vsize: 56240
[startup+860.019 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 24332 0 0 0 85912 98 0 0 25 0 1 0 491755170 57589760 13415 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14060 13415 603 41 0 14019 0
vsize: 56240
[startup+870.019 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 24332 0 0 0 86911 98 0 0 25 0 1 0 491755170 57589760 13415 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14060 13415 603 41 0 14019 0
vsize: 56240
[startup+880.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 24332 0 0 0 87912 98 0 0 25 0 1 0 491755170 57589760 13415 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14060 13415 603 41 0 14019 0
vsize: 56240
[startup+890.019 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 24332 0 0 0 88912 98 0 0 25 0 1 0 491755170 57589760 13415 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14060 13415 603 41 0 14019 0
vsize: 56240
[startup+900.019 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 24765 0 0 0 89910 100 0 0 25 0 1 0 491755170 57589760 13419 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14060 13419 603 41 0 14019 0
vsize: 56240
[startup+910.019 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 24765 0 0 0 90910 100 0 0 25 0 1 0 491755170 57589760 13419 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14060 13419 603 41 0 14019 0
vsize: 56240
[startup+920.019 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 24765 0 0 0 91910 100 0 0 25 0 1 0 491755170 57589760 13419 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14060 13419 603 41 0 14019 0
vsize: 56240
[startup+930.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 24765 0 0 0 92910 100 0 0 25 0 1 0 491755170 57589760 13419 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14060 13419 603 41 0 14019 0
vsize: 56240
[startup+940.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 24765 0 0 0 93910 100 0 0 25 0 1 0 491755170 57589760 13419 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14060 13419 603 41 0 14019 0
vsize: 56240
[startup+950.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 24765 0 0 0 94910 100 0 0 25 0 1 0 491755170 57589760 13419 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14060 13419 603 41 0 14019 0
vsize: 56240
[startup+960.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 24765 0 0 0 95910 100 0 0 25 0 1 0 491755170 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+970.019 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 24765 0 0 0 96910 101 0 0 25 0 1 0 491755170 57589760 13419 4294967295 134512640 134672761 3221224544 3221223320 1075351193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14060 13419 603 41 0 14019 0
vsize: 56240
[startup+980.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 25162 0 0 0 97907 103 0 0 25 0 1 0 491755170 57589760 13421 4294967295 134512640 134672761 3221224544 3221223640 134616123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14060 13421 603 41 0 14019 0
vsize: 56240
[startup+990.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 25162 0 0 0 98907 103 0 0 25 0 1 0 491755170 57589760 13421 4294967295 134512640 134672761 3221224544 3221223728 134615807 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.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 25559 0 0 0 99905 106 0 0 25 0 1 0 491755170 57540608 13409 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 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.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 25965 0 0 0 100901 108 0 0 25 0 1 0 491755170 57540608 13411 4294967295 134512640 134672761 3221224544 3221223584 134614228 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.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 25965 0 0 0 101901 108 0 0 25 0 1 0 491755170 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+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 26315 0 0 0 102899 110 0 0 25 0 1 0 491755170 57540608 13411 4294967295 134512640 134672761 3221224544 3221223680 134614699 0 0 5 16386 0 0 0 17 1 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.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 26315 0 0 0 103899 110 0 0 25 0 1 0 491755170 57540608 13411 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 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.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 26315 0 0 0 104898 110 0 0 25 0 1 0 491755170 57540608 13411 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 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.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 26315 0 0 0 105898 111 0 0 25 0 1 0 491755170 57540608 13411 4294967295 134512640 134672761 3221224544 3221223744 134610709 0 0 5 16386 0 0 0 17 1 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.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 26315 0 0 0 106898 111 0 0 25 0 1 0 491755170 57540608 13411 4294967295 134512640 134672761 3221224544 3221223728 134615608 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.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 26315 0 0 0 107898 111 0 0 25 0 1 0 491755170 57540608 13411 4294967295 134512640 134672761 3221224544 3221223744 134610618 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.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 26315 0 0 0 108898 111 0 0 25 0 1 0 491755170 57540608 13411 4294967295 134512640 134672761 3221224544 3221223728 134615663 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.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 26315 0 0 0 109898 111 0 0 25 0 1 0 491755170 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+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 26726 0 0 0 110896 113 0 0 25 0 1 0 491755170 57540608 13418 4294967295 134512640 134672761 3221224544 3221223728 134615779 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.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 27079 0 0 0 111894 115 0 0 25 0 1 0 491755170 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+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 27079 0 0 0 112894 115 0 0 25 0 1 0 491755170 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.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 27079 0 0 0 113894 115 0 0 25 0 1 0 491755170 57540608 13420 4294967295 134512640 134672761 3221224544 3221223584 134612628 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.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 27079 0 0 0 114895 115 0 0 25 0 1 0 491755170 57540608 13420 4294967295 134512640 134672761 3221224544 3221223728 134615652 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.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 27079 0 0 0 115895 115 0 0 25 0 1 0 491755170 57540608 13420 4294967295 134512640 134672761 3221224544 3221223584 134612628 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.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 27079 0 0 0 116895 115 0 0 25 0 1 0 491755170 57540608 13420 4294967295 134512640 134672761 3221224544 3221223728 134615681 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.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 27079 0 0 0 117895 115 0 0 25 0 1 0 491755170 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+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 27079 0 0 0 118895 115 0 0 25 0 1 0 491755170 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+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 794
Raw data (stat): 792 (minisat+) R 791 30701 30700 0 -1 0 27079 0 0 0 119895 115 0 0 25 0 1 0 491755170 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
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.97 1/54 794
Raw data (stat): 792 (minisat+) Z 791 30701 30700 0 -1 12 27080 0 0 0 119896 118 0 0 23 0 1 0 491755170 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.09
CPU time (s): 1200.15
CPU user time (s): 1198.96
CPU system time (s): 1.18882
CPU usage (%): 100.006
Max. virtual memory (Kb): 56240
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####