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/submitted/een/normalized-p0201.opb
MD5SUM	ff4eb45c2603a47e5b79b2649e926ba4
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.01984
Number of variables	195
Total number of constraints	133
Number of constraints which are clauses	20
Number of constraints which are cardinality constraints (but not clauses)	26
Number of constraints which are nor clauses,nor cardinality constraints	87
Minimum length of a constraint	3
Maximum length of a constraint	65
Trace number 7130

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc11 THE 2005-04-14 21:25:37 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=5159 boxname=wulflinc11 idbench=397 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ff4eb45c2603a47e5b79b2649e926ba4  /oldhome/oroussel/tmp/wulflinc11/normalized-p0201.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc11/normalized-p0201.opb /oldhome/oroussel/tmp/wulflinc11/normalized-p0201.opb
IDLAUNCH: 5159
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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.028
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        846220 kB
Buffers:         36980 kB
Cached:         126660 kB
SwapCached:       4932 kB
Active:          77896 kB
Inactive:        93508 kB
HighTotal:      131008 kB
HighFree:         7252 kB
LowTotal:       903652 kB
LowFree:        838968 kB
SwapTotal:     2097136 kB
SwapFree:      2092204 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            11348 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 21:45:39 (client local time) WITH STATUS 10 IN 1200.12 SECONDS
stats: 5159 7 1200.12 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 ---[ 134]---> BDD-cost:    3
c ---[ 133]---> BDD-cost:    3
c ---[ 132]---> BDD-cost:    3
c ---[ 131]---> BDD-cost:    3
c ---[ 130]---> BDD-cost:    3
c ---[ 129]---> BDD-cost:    3
c ---[ 128]---> BDD-cost:   11
c ---[ 127]---> BDD-cost:   11
c ---[ 126]---> BDD-cost:   11
c ---[ 125]---> BDD-cost:   11
c ---[ 124]---> BDD-cost:   11
c ---[ 123]---> BDD-cost:   11
c ---[ 122]---> BDD-cost:   11
c ---[ 121]---> BDD-cost:   11
c ---[ 120]---> BDD-cost:   11
c ---[ 119]---> BDD-cost:   11
c ---[ 118]---> BDD-cost:   11
c ---[ 117]---> BDD-cost:   11
c ---[ 116]---> BDD-cost:   11
c ---[ 115]---> BDD-cost:   11
c ---[ 114]---> BDD-cost:   11
c ---[ 113]---> BDD-cost:   11
c ---[ 112]---> BDD-cost:   11
c ---[ 111]---> BDD-cost:   11
c ---[ 110]---> BDD-cost:   11
c ---[ 109]---> BDD-cost:   11
c ---[ 108]---> BDD-cost:   11
c ---[ 107]---> BDD-cost:   11
c ---[ 106]---> BDD-cost:   11
c ---[ 105]---> BDD-cost:   11
c ---[ 104]---> BDD-cost:   11
c ---[ 103]---> BDD-cost:   11
c ---[ 102]---> BDD-cost:   11
c ---[ 101]---> BDD-cost:   11
c ---[ 100]---> BDD-cost:   11
c ---[  99]---> BDD-cost:   11
c ---[  98]---> BDD-cost:   11
c ---[  97]---> BDD-cost:   11
c ---[  96]---> BDD-cost:   11
c ---[  95]---> BDD-cost:   11
c ---[  94]---> BDD-cost:   11
c ---[  93]---> BDD-cost:   11
c ---[  92]---> BDD-cost:   11
c ---[  91]---> BDD-cost:   11
c ---[  90]---> BDD-cost:   11
c ---[  89]---> BDD-cost:   11
c ---[  88]---> BDD-cost:   11
c ---[  87]---> BDD-cost:   11
c ---[  86]---> BDD-cost:   11
c ---[  85]---> BDD-cost:   11
c ---[  84]---> BDD-cost:   11
c ---[  83]---> BDD-cost:   11
c ---[  82]---> BDD-cost:   11
c ---[  81]---> BDD-cost:   11
c ---[  80]---> BDD-cost:   11
c ---[  79]---> BDD-cost:   11
c ---[  78]---> BDD-cost:   11
c ---[  77]---> BDD-cost:   11
c ---[  76]---> BDD-cost:   11
c ---[  75]---> BDD-cost:   11
c ---[  74]---> BDD-cost:   11
c ---[  72]---> BDD-cost:   13
c ---[  70]---> BDD-cost:   15
c ---[  68]---> BDD-cost:   15
c ---[  66]---> BDD-cost:   13
c ---[  64]---> BDD-cost:   13
c ---[  62]---> BDD-cost:   13
c ---[  60]---> BDD-cost:   13
c ---[  58]---> BDD-cost:   13
c ---[  56]---> BDD-cost:   13
c ---[  54]---> BDD-cost:   13
c ---[  52]---> BDD-cost:   13
c ---[  50]---> BDD-cost:   13
c ---[  48]---> BDD-cost:   13
c ---[  46]---> BDD-cost:   13
c ---[  44]---> BDD-cost:   13
c ---[  42]---> BDD-cost:   13
c ---[  40]---> BDD-cost:   13
c ---[  38]---> BDD-cost:   13
c ---[  36]---> BDD-cost:   13
c ---[  31]---> BDD-cost:   39
c ---[  28]---> BDD-cost:   54
c ---[  27]---> BDD-cost:   42
c ---[  26]---> BDD-cost:   42
c ---[  25]---> BDD-cost:   73
c ---[  24]---> BDD-cost:   73
c ---[  23]---> BDD-cost:   98
c ---[  22]---> BDD-cost:  160
c ---[  21]---> BDD-cost:   85
c ---[  20]---> BDD-cost:   85
c ---[  19]---> BDD-cost:  201
c ---[  18]---> BDD-cost:  107
c ---[  17]---> BDD-cost:  107
c ---[  16]---> BDD-cost:  241
c ---[  15]---> BDD-cost:  128
c ---[  14]---> BDD-cost:  128
c ---[  13]---> BDD-cost:  150
c ---[  12]---> BDD-cost:  150
c ---[  11]---> BDD-cost:  281
c ---[  10]---> BDD-cost:  321
c ---[   9]---> BDD-cost:  172
c ---[   8]---> BDD-cost:  172
c ---[   7]---> BDD-cost:  194
c ---[   6]---> BDD-cost:  194
c ---[   5]---> BDD-cost:  361
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    34627 |    3522       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4622          
c   -- var.elim.:  2000/4622          
c   -- var.elim.:  3000/4622          
c   -- var.elim.:  4000/4622          
c   -- var.elim.:  4622/4622          
c   -- var.elim.:  1000/1284          
c   -- var.elim.:  1284/1284          
c   -- subsuming                       
c   -- var.elim.:  1000/1090          
c   -- var.elim.:  1090/1090          
c   -- var.elim.:  376/376          
c   -- subsuming                       
c   -- var.elim.:  88/88          
c   -- var.elim.:  23/23          
c |         0 |   10139    50298 |      --       0       --      -- |     --   | -1602/15986
c |         0 |   10139    50298 |    4055       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 1.2808 s)
c ==============================================================================
c [1mFound solution: 2466[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:21989     Base: 5 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |        25 |   59683   165909 |   17904      19      236    12.4 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/19062          
c   -- var.elim.:  2000/19062          
c   -- var.elim.:  3000/19062          
c   -- var.elim.:  4000/19062          
c   -- var.elim.:  5000/19062          
c   -- var.elim.:  6000/19062          
c   -- var.elim.:  7000/19062          
c   -- var.elim.:  8000/19062          
c   -- var.elim.:  9000/19062          
c   -- var.elim.:  10000/19062          
c   -- var.elim.:  11000/19062          
c   -- var.elim.:  12000/19062          
c   -- var.elim.:  13000/19062          
c   -- var.elim.:  14000/19062          
c   -- var.elim.:  15000/19062          
c   -- var.elim.:  16000/19062          
c   -- var.elim.:  17000/19062          
c   -- var.elim.:  18000/19062          
c   -- var.elim.:  19000/19062          
c   -- var.elim.:  19062/19062          
c   -- var.elim.:  1000/10271          
c   -- var.elim.:  2000/10271          
c   -- var.elim.:  3000/10271          
c   -- var.elim.:  4000/10271          
c   -- var.elim.:  5000/10271          
c   -- var.elim.:  6000/10271          
c   -- var.elim.:  7000/10271          
c   -- var.elim.:  8000/10271          
c   -- var.elim.:  9000/10271          
c   -- var.elim.:  10000/10271          
c   -- var.elim.:  10271/10271          
c   -- var.elim.:  562/562          
c   -- var.elim.:  194/194          
c   -- subsuming                       
c   -- var.elim.:  1000/2108          
c   -- var.elim.:  2000/2108          
c   -- var.elim.:  2108/2108          
c   -- var.elim.:  723/723          
c   -- var.elim.:  107/107          
c   -- var.elim.:  219/219          
c   -- subsuming                       
c   -- var.elim.:  485/485          
c   -- var.elim.:  441/441          
c   -- var.elim.:  5/5          
c |        25 |   53402   191768 |      --      19       --      -- |     --   | -6281/25860
c |        25 |   53402   191768 |   21360      19      236    12.4 |  0.000 % |
c |       125 |   53153   190630 |   23387     116     2689    23.2 |  1.229 % |
c ==============================================================================
c (current CPU-time: 5.88711 s)
c ==============================================================================
c [1mFound solution: 2338[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       165 |   51815   185275 |   15544     146     2850    19.5 |  1.229 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2044          
c   -- var.elim.:  2000/2044          
c   -- var.elim.:  2044/2044          
c   -- var.elim.:  1000/1742          
c   -- var.elim.:  1742/1742          
c   -- var.elim.:  626/626          
c   -- var.elim.:  269/269          
c   -- var.elim.:  126/126          
c   -- var.elim.:  49/49          
c   -- subsuming                       
c   -- var.elim.:  425/425          
c   -- var.elim.:  130/130          
c |       165 |   50920   183650 |      --     146       --      -- |     --   | -890/-1614
c |       165 |   50920   183650 |   20368     137     2357    17.2 |  1.229 % |
c ==============================================================================
c (current CPU-time: 6.71098 s)
c ==============================================================================
c [1mFound solution: 2090[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       175 |   51379   185021 |   15413     147     2775    18.9 |  1.229 % |
c   -- subsuming                       
c   -- var.elim.:  979/979          
c   -- var.elim.:  634/634          
c   -- var.elim.:  67/67          
c   -- var.elim.:  80/80          
c   -- subsuming                       
c   -- var.elim.:  48/48          
c |       175 |   51088   185170 |      --     147       --      -- |     --   | -291/150
c |       175 |   51088   185170 |   20435     147     2775    18.9 |  1.229 % |
c |       275 |   51088   185170 |   22478     247     3643    14.7 |  3.533 % |
c ==============================================================================
c (current CPU-time: 7.48786 s)
c ==============================================================================
c [1mFound solution: 2058[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       367 |   50535   183273 |   15160     333    10105    30.3 |  3.533 % |
c   -- subsuming                       
c   -- var.elim.:  750/750          
c   -- var.elim.:  648/648          
c   -- var.elim.:  14/14          
c   -- subsuming                       
c   -- var.elim.:  122/122          
c |       367 |   50431   184148 |      --     333       --      -- |     --   | -102/880
c |       367 |   50431   184148 |   20172     327     7763    23.7 |  3.533 % |
c |       468 |   49568   180750 |   21809     422    10461    24.8 |  4.979 % |
c |       618 |   48764   177754 |   23601     555    11873    21.4 |  5.833 % |
c |       844 |   45069   164974 |   23994     712    14272    20.0 | 10.314 % |
c ==============================================================================
c (current CPU-time: 9.2256 s)
c ==============================================================================
c [1mFound solution: 1972[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       980 |   45228   165521 |   13568     845    21118    25.0 | 10.314 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2457          
c   -- var.elim.:  2000/2457          
c   -- var.elim.:  2457/2457          
c   -- var.elim.:  1000/2017          
c   -- var.elim.:  2000/2017          
c   -- var.elim.:  2017/2017          
c   -- var.elim.:  844/844          
c   -- var.elim.:  226/226          
c   -- subsuming                       
c   -- var.elim.:  715/715          
c   -- var.elim.:  202/202          
c   -- subsuming                       
c   -- var.elim.:  54/54          
c   -- var.elim.:  5/5          
c |       980 |   44376   166055 |      --     845       --      -- |     --   | -839/561
c |       980 |   44376   166055 |   17750     723    13596    18.8 | 10.314 % |
c |      1080 |   43364   162001 |   19080     809    14778    18.3 | 11.946 % |
c |      1230 |   42904   160459 |   20765     950    20048    21.1 | 12.472 % |
c ==============================================================================
c (current CPU-time: 11.0043 s)
c ==============================================================================
c [1mFound solution: 1971[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1296 |   42930   160705 |   12878    1016    22829    22.5 | 12.472 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1142          
c   -- var.elim.:  1142/1142          
c   -- var.elim.:  973/973          
c   -- var.elim.:  353/353          
c   -- var.elim.:  510/510          
c   -- subsuming                       
c   -- var.elim.:  518/518          
c   -- var.elim.:  293/293          
c |      1296 |   42660   160584 |      --    1016       --      -- |     --   | -270/-120
c |      1296 |   42660   160584 |   17064     969    20762    21.4 | 12.472 % |
c |      1396 |   42645   160537 |   18763    1068    26649    25.0 | 12.683 % |
c |      1548 |   41664   156367 |   20165    1203    27923    23.2 | 13.835 % |
c |      1773 |   41622   156239 |   22159    1413    46240    32.7 | 13.936 % |
c |      2113 |   41546   155481 |   24330    1747    64849    37.1 | 14.013 % |
c ==============================================================================
c (current CPU-time: 14.8647 s)
c ==============================================================================
c [1mFound solution: 1963[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2513 |   40260   151235 |   12077    2119    77260    36.5 | 14.013 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1644          
c   -- var.elim.:  1644/1644          
c   -- var.elim.:  1000/1267          
c   -- var.elim.:  1267/1267          
c   -- var.elim.:  506/506          
c   -- var.elim.:  140/140          
c   -- var.elim.:  82/82          
c   -- subsuming                       
c   -- var.elim.:  297/297          
c   -- var.elim.:  62/62          
c |      2513 |   39736   150607 |      --    2119       --      -- |     --   | -518/-615
c |      2513 |   39736   150607 |   15894    2119    77260    36.5 | 14.013 % |
c |      2613 |   39692   150435 |   17464    2218    85793    38.7 | 16.148 % |
c |      2763 |   39432   149530 |   19085    2005    50771    25.3 | 16.400 % |
c |      2991 |   38528   146256 |   20512    2196    63916    29.1 | 17.476 % |
c |      3329 |   38507   146191 |   22551    2533    98671    39.0 | 17.523 % |
c |      3835 |   38507   146191 |   24806    3039   181270    59.6 | 17.523 % |
c ==============================================================================
c (current CPU-time: 19.595 s)
c ==============================================================================
c [1mFound solution: 1785[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 3292     Base: 5 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4193 |   43509   158774 |   13052    3397   206244    60.7 | 17.523 % |
c   -- subsuming                       
c   -- var.elim.:  1000/5875          
c   -- var.elim.:  2000/5875          
c   -- var.elim.:  3000/5875          
c   -- var.elim.:  4000/5875          
c   -- var.elim.:  5000/5875          
c   -- var.elim.:  5875/5875          
c   -- var.elim.:  1000/3321          
c   -- var.elim.:  2000/3321          
c   -- var.elim.:  3000/3321          
c   -- var.elim.:  3321/3321          
c   -- var.elim.:  1000/1238          
c   -- var.elim.:  1238/1238          
c   -- var.elim.:  1000/1309          
c   -- var.elim.:  1309/1309          
c   -- var.elim.:  749/749          
c   -- var.elim.:  187/187          
c   -- subsuming                       
c   -- var.elim.:  1000/1356          
c   -- var.elim.:  1356/1356          
c   -- var.elim.:  689/689          
c   -- var.elim.:  309/309          
c   -- var.elim.:  193/193          
c   -- subsuming                       
c   -- var.elim.:  620/620          
c   -- var.elim.:  235/235          
c   -- var.elim.:  10/10          
c |      4193 |   39488   154966 |      --    3397       --      -- |     --   | -3914/-3303
c |      4193 |   39488   154966 |   15795    3167   131409    41.5 | 17.523 % |
c |      4293 |   39488   154966 |   17374    3267   134263    41.1 | 17.032 % |
c |      4443 |   39410   154013 |   19074    3416   147678    43.2 | 17.093 % |
c |      4668 |   39410   154013 |   20981    3641   149642    41.1 | 17.093 % |
c |      5005 |   39221   153370 |   22969    3975   154340    38.8 | 17.283 % |
c |      5511 |   39221   153370 |   25266    4481   197254    44.0 | 17.283 % |
c |      6272 |   39196   153281 |   27775    5236   309680    59.1 | 17.306 % |
c |      7415 |   38966   152388 |   30373    6371   398791    62.6 | 17.543 % |
c |      9123 |   37914   148479 |   32508    8000   463837    58.0 | 18.707 % |
c |     11685 |   36606   142171 |   34526   10432   616457    59.1 | 20.238 % |
c |     15533 |   34810   135855 |   36115   14145  1294142    91.5 | 22.803 % |
c |     21300 |   33866   132763 |   38649   19741  2636670   133.6 | 24.105 % |
c ==============================================================================
c (current CPU-time: 86.9128 s)
c ==============================================================================
c [1mFound solution: 1739[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     29563 |   33862   132751 |   10158   27952  4255644   152.2 | 24.105 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2764          
c   -- var.elim.:  2000/2764          
c   -- var.elim.:  2764/2764          
c   -- var.elim.:  1000/2042          
c   -- var.elim.:  2000/2042          
c   -- var.elim.:  2042/2042          
c   -- var.elim.:  800/800          
c   -- var.elim.:  786/786          
c   -- var.elim.:  549/549          
c   -- var.elim.:  419/419          
c   -- var.elim.:  305/305          
c   -- subsuming                       
c   -- var.elim.:  583/583          
c   -- var.elim.:  122/122          
c |     29563 |   32570   129838 |      --   27952       --      -- |     --   | -1283/-2894
c |     29563 |   32570   129838 |   13028   13718   396034    28.9 | 24.105 % |
c |     29664 |   32570   129838 |   14330   13819   399063    28.9 | 25.764 % |
c |     29814 |   32570   129838 |   15763   13969   410664    29.4 | 25.764 % |
c |     30039 |   32570   129838 |   17340   14194   432775    30.5 | 25.764 % |
c |     30376 |   32570   129838 |   19074   14531   465228    32.0 | 25.764 % |
c |     30883 |   32570   129838 |   20981   15038   511409    34.0 | 25.764 % |
c |     31642 |   32564   129815 |   23075   15795   585935    37.1 | 25.772 % |
c |     32781 |   32564   129815 |   25383   16934   737646    43.6 | 25.772 % |
c |     34489 |   32564   129815 |   27921   18642   975880    52.3 | 25.772 % |
c |     37051 |   31962   127190 |   30145   21189  1385073    65.4 | 26.411 % |
c ==============================================================================
c (current CPU-time: 112.546 s)
c ==============================================================================
c [1mFound solution: 1733[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     38380 |   32054   127529 |    9616   22518  1594378    70.8 | 26.411 % |
c   -- subsuming                       
c   -- var.elim.:  901/901          
c   -- var.elim.:  806/806          
c   -- var.elim.:  189/189          
c   -- subsuming                       
c   -- var.elim.:  250/250          
c   -- var.elim.:  155/155          
c   -- var.elim.:  251/251          
c |     38380 |   31770   127951 |      --   22518       --      -- |     --   | -284/423
c |     38380 |   31770   127951 |   12708   19080   905567    47.5 | 26.411 % |
c |     38482 |   31770   127951 |   13978   10385   647718    62.4 | 26.658 % |
c |     38633 |   31760   127911 |   15371   10535   655038    62.2 | 26.666 % |
c |     38858 |   31760   127911 |   16909   10760   675014    62.7 | 26.666 % |
c |     39196 |   31760   127911 |   18599   11098   710919    64.1 | 26.666 % |
c |     39702 |   31760   127911 |   20459   11604   785023    67.7 | 26.666 % |
c |     40461 |   31729   127804 |   22483   12361   876682    70.9 | 26.690 % |
c |     41600 |   31705   127449 |   24713   13498   985480    73.0 | 26.706 % |
c |     43308 |   31687   127393 |   27169   15205  1131297    74.4 | 26.747 % |
c |     45871 |   31687   127393 |   29886   17768  1400902    78.8 | 26.747 % |
c ==============================================================================
c (current CPU-time: 135.74 s)
c ==============================================================================
c [1mFound solution: 1727[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     46476 |   31750   127672 |    9524   18373  1513755    82.4 | 26.747 % |
c   -- subsuming                       
c   -- var.elim.:  515/515          
c   -- var.elim.:  420/420          
c   -- var.elim.:  127/127          
c   -- var.elim.:  102/102          
c   -- var.elim.:  109/109          
c   -- subsuming                       
c   -- var.elim.:  424/424          
c   -- var.elim.:  5/5          
c |     46476 |   31678   127641 |      --   18373       --      -- |     --   | -72/-30
c |     46476 |   31678   127641 |   12671   16532  1244031    75.2 | 26.747 % |
c |     46576 |   31678   127641 |   13938   11122   836835    75.2 | 26.789 % |
c |     46728 |   31678   127641 |   15332   11274   859957    76.3 | 26.789 % |
c |     46953 |   31678   127641 |   16865   11499   879726    76.5 | 26.789 % |
c |     47291 |   31678   127641 |   18551   11837   947191    80.0 | 26.789 % |
c |     47797 |   31678   127641 |   20407   12343  1007870    81.7 | 26.789 % |
c |     48557 |   31678   127641 |   22447   13103  1083108    82.7 | 26.789 % |
c |     49697 |   31678   127641 |   24692   14243  1209024    84.9 | 26.789 % |
c |     51405 |   31678   127641 |   27161   15951  1535974    96.3 | 26.789 % |
c |     53968 |   31678   127641 |   29878   18514  2032479   109.8 | 26.789 % |
c |     57812 |   31678   127641 |   32865   22358  2701741   120.8 | 26.789 % |
c |     63578 |   31678   127641 |   36152   28124  3951047   140.5 | 26.789 % |
c |     72228 |   31670   127615 |   39757   36772  5769377   156.9 | 26.797 % |
c ==============================================================================
c (current CPU-time: 237.075 s)
c ==============================================================================
c [1mFound solution: 1717[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     74570 |   31734   127896 |    9520   39114  6423183   164.2 | 26.797 % |
c   -- subsuming                       
c   -- var.elim.:  210/210          
c   -- var.elim.:  179/179          
c   -- var.elim.:  121/121          
c   -- var.elim.:  96/96          
c   -- var.elim.:  103/103          
c |     74570 |   31678   128111 |      --   39114       --      -- |     --   | -56/216
c |     74570 |   31678   128111 |   12671   38359  6247062   162.9 | 26.797 % |
c |     74671 |   31678   128111 |   13938   10830  1679016   155.0 | 26.805 % |
c |     74821 |   31678   128111 |   15332   10980  1692347   154.1 | 26.805 % |
c |     75046 |   31678   128111 |   16865   11205  1740855   155.4 | 26.805 % |
c |     75386 |   31678   128111 |   18551   11545  1772309   153.5 | 26.805 % |
c |     75894 |   31678   128111 |   20407   12053  1893597   157.1 | 26.805 % |
c |     76654 |   31678   128111 |   22447   12813  2115921   165.1 | 26.805 % |
c |     77795 |   31678   128111 |   24692   13954  2299283   164.8 | 26.805 % |
c |     79503 |   31678   128111 |   27161   15662  2650405   169.2 | 26.805 % |
c |     82065 |   31663   128060 |   29863   18220  3111531   170.8 | 26.829 % |
c |     85912 |   31657   128040 |   32844   22066  4177535   189.3 | 26.838 % |
c ==============================================================================
c (current CPU-time: 277.874 s)
c ==============================================================================
c [1mFound solution: 1713[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     86378 |   31745   128369 |    9523   22532  4302931   191.0 | 26.838 % |
c   -- subsuming                       
c   -- var.elim.:  257/257          
c   -- var.elim.:  225/225          
c   -- var.elim.:  135/135          
c |     86378 |   31627   128195 |      --   22532       --      -- |     --   | -118/-173
c |     86378 |   31627   128195 |   12650   19314  2954580   153.0 | 26.838 % |
c |     86478 |   31627   128195 |   13915   12976  1702428   131.2 | 26.925 % |
c |     86629 |   31488   127684 |   15240   13124  1711235   130.4 | 27.062 % |
c |     86855 |   31465   127601 |   16751   13343  1724876   129.3 | 27.078 % |
c |     87192 |   31465   127601 |   18427   13680  1812498   132.5 | 27.078 % |
c |     87698 |   31465   127601 |   20269   14186  1874075   132.1 | 27.078 % |
c |     88459 |   31288   126987 |   22171   14945  1961533   131.3 | 27.247 % |
c |     89599 |   31288   126987 |   24388   16085  2239075   139.2 | 27.247 % |
c ==============================================================================
c (current CPU-time: 292.111 s)
c ==============================================================================
c [1mFound solution: 1709[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     90781 |   31401   127376 |    9420   17267  2462190   142.6 | 27.247 % |
c   -- subsuming                       
c   -- var.elim.:  531/531          
c   -- var.elim.:  437/437          
c   -- var.elim.:  107/107          
c   -- var.elim.:  77/77          
c   -- subsuming                       
c   -- var.elim.:  13/13          
c   -- var.elim.:  8/8          
c |     90781 |   31251   127387 |      --   17267       --      -- |     --   | -148/16
c |     90781 |   31251   127387 |   12500   11040   349617    31.7 | 27.247 % |
c |     90882 |   31167   127081 |   13713   11140   350525    31.5 | 27.417 % |
c |     91032 |   31160   127056 |   15081   11289   363590    32.2 | 27.425 % |
c |     91257 |   31160   127056 |   16589   11514   378944    32.9 | 27.425 % |
c |     91595 |   31160   127056 |   18248   11852   428270    36.1 | 27.425 % |
c |     92101 |   31160   127056 |   20073   12358   460113    37.2 | 27.425 % |
c |     92860 |   31160   127056 |   22080   13117   518969    39.6 | 27.425 % |
c |     94001 |   31145   126998 |   24277   14249   701296    49.2 | 27.441 % |
c |     95710 |   30996   126406 |   26577   15957  1069684    67.0 | 27.587 % |
c |     98274 |   30856   125929 |   29102   18470  1223428    66.2 | 27.748 % |
c |    102119 |   30798   125735 |   31952   22305  1981333    88.8 | 27.813 % |
c |    107886 |   30792   125715 |   35141   28068  3475896   123.8 | 27.821 % |
c ==============================================================================
c (current CPU-time: 353.156 s)
c ==============================================================================
c [1mFound solution: 1704[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    109837 |   30946   126204 |    9283   30019  3973877   132.4 | 27.821 % |
c   -- subsuming                       
c   -- var.elim.:  644/644          
c   -- var.elim.:  654/654          
c   -- var.elim.:  465/465          
c   -- var.elim.:  267/267          
c   -- subsuming                       
c   -- var.elim.:  304/304          
c   -- var.elim.:  39/39          
c |    109837 |   30699   125590 |      --   30019       --      -- |     --   | -245/-609
c |    109837 |   30699   125590 |   12279   20290   832603    41.0 | 27.821 % |
c |    109938 |   30649   125419 |   13485   11224   399437    35.6 | 27.988 % |
c |    110088 |   30649   125419 |   14834   11374   429430    37.8 | 27.989 % |
c |    110314 |   30649   125419 |   16317   11600   435755    37.6 | 27.988 % |
c |    110653 |   30649   125419 |   17949   11939   457406    38.3 | 27.988 % |
c |    111159 |   30649   125419 |   19744   12445   543119    43.6 | 27.988 % |
c |    111918 |   30649   125419 |   21718   13204   663079    50.2 | 27.988 % |
c |    113060 |   30336   123745 |   23646   14341   960490    67.0 | 28.289 % |
c |    114769 |   30336   123745 |   26011   16050  1340882    83.5 | 28.289 % |
c |    117332 |   30336   123745 |   28612   18613  1918987   103.1 | 28.289 % |
c |    121176 |   30336   123745 |   31473   22457  2812409   125.2 | 28.289 % |
c |    126942 |   30336   123745 |   34620   28223  4471817   158.4 | 28.289 % |
c |    135591 |   30256   123457 |   37982   36845  6036977   163.8 | 28.378 % |
c |    148566 |   30188   123232 |   41686   26274  4462879   169.9 | 28.467 % |
c ==============================================================================
c (current CPU-time: 541.396 s)
c ==============================================================================
c [1mFound solution: 1702[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    158684 |   30211   123390 |    9063   36381  6098905   167.6 | 28.467 % |
c   -- subsuming                       
c   -- var.elim.:  731/731          
c   -- var.elim.:  660/660          
c   -- var.elim.:  66/66          
c   -- var.elim.:  54/54          
c   -- subsuming                       
c   -- var.elim.:  236/236          
c   -- var.elim.:  5/5          
c |    158684 |   30085   123977 |      --   36381       --      -- |     --   | -124/592
c |    158684 |   30085   123977 |   12034   24443  1460161    59.7 | 28.467 % |
c |    158785 |   30085   123977 |   13237   14502   663279    45.7 | 28.675 % |
c |    158935 |   30085   123977 |   14561   14652   689053    47.0 | 28.675 % |
c |    159164 |   30085   123977 |   16017   14881   726230    48.8 | 28.675 % |
c |    159501 |   30085   123977 |   17618   15218   755330    49.6 | 28.675 % |
c |    160007 |   30085   123977 |   19380   15724   846548    53.8 | 28.675 % |
c |    160766 |   30085   123977 |   21318   16483   995193    60.4 | 28.675 % |
c |    161905 |   30085   123977 |   23450   17622  1254378    71.2 | 28.675 % |
c |    163613 |   30016   123250 |   25736   19329  1581490    81.8 | 28.732 % |
c |    166175 |   30012   123238 |   28306   21890  2135207    97.5 | 28.740 % |
c ==============================================================================
c (current CPU-time: 573.35 s)
c ==============================================================================
c [1mFound solution: 1692[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    168629 |   30050   123449 |    9014   24344  2640091   108.4 | 28.740 % |
c   -- subsuming                       
c   -- var.elim.:  251/251          
c   -- var.elim.:  191/191          
c   -- var.elim.:  85/85          
c   -- var.elim.:  88/88          
c |    168629 |   30015   123719 |      --   24344       --      -- |     --   | -35/271
c |    168629 |   30015   123719 |   12006   23187  2027167    87.4 | 28.740 % |
c |    168729 |   30015   123719 |   13206   15558  1501701    96.5 | 28.763 % |
c |    168880 |   30015   123719 |   14527   15709  1531262    97.5 | 28.763 % |
c |    169105 |   30015   123719 |   15979   15934  1561893    98.0 | 28.763 % |
c |    169442 |   30015   123719 |   17577   16271  1632675   100.3 | 28.763 % |
c |    169948 |   30015   123719 |   19335   16777  1695595   101.1 | 28.763 % |
c |    170707 |   30015   123719 |   21269   17536  1840120   104.9 | 28.763 % |
c |    171846 |   29999   123672 |   23383   18673  2079392   111.4 | 28.779 % |
c |    173555 |   29927   123412 |   25660   20380  2445399   120.0 | 28.844 % |
c |    176117 |   29918   123339 |   28218   22936  2572467   112.2 | 28.869 % |
c ==============================================================================
c (current CPU-time: 603.64 s)
c ==============================================================================
c [1mFound solution: 1689[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    178633 |   29920   122885 |    8975   25449  3177376   124.9 | 28.869 % |
c   -- subsuming                       
c   -- var.elim.:  581/581          
c   -- var.elim.:  700/700          
c   -- var.elim.:  91/91          
c   -- subsuming                       
c   -- var.elim.:  389/389          
c   -- var.elim.:  5/5          
c |    178633 |   29800   122986 |      --   25449       --      -- |     --   | -119/104
c |    178633 |   29800   122986 |   11920   22367  1939360    86.7 | 28.869 % |
c |    178735 |   29800   122986 |   13112   15014  1039532    69.2 | 29.027 % |
c |    178885 |   29800   122986 |   14423   15164  1070269    70.6 | 29.027 % |
c |    179110 |   29800   122986 |   15865   15389  1116619    72.6 | 29.027 % |
c |    179448 |   29790   122949 |   17446   15725  1148872    73.1 | 29.035 % |
c |    179954 |   29790   122949 |   19190   16231  1163951    71.7 | 29.035 % |
c |    180714 |   29790   122949 |   21109   16991  1340177    78.9 | 29.035 % |
c |    181853 |   29790   122949 |   23220   18130  1476277    81.4 | 29.035 % |
c |    183562 |   29790   122949 |   25543   19839  1891014    95.3 | 29.035 % |
c |    186125 |   29790   122949 |   28097   22402  2438663   108.9 | 29.035 % |
c |    189969 |   29790   122949 |   30907   26246  3445958   131.3 | 29.035 % |
c ==============================================================================
c (current CPU-time: 644.483 s)
c ==============================================================================
c [1mFound solution: 1679[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    191420 |   29910   123351 |    8972   27697  3800742   137.2 | 29.035 % |
c   -- subsuming                       
c   -- var.elim.:  266/266          
c   -- var.elim.:  205/205          
c   -- var.elim.:  98/98          
c   -- var.elim.:  58/58          
c |    191420 |   29799   123162 |      --   27697       --      -- |     --   | -111/-188
c |    191420 |   29799   123162 |   11919   27421  3719085   135.6 | 29.035 % |
c |    191521 |   29799   123162 |   13111   12273  1640055   133.6 | 29.053 % |
c |    191671 |   29799   123162 |   14422   12423  1649354   132.8 | 29.053 % |
c |    191896 |   29799   123162 |   15864   12648  1663605   131.5 | 29.053 % |
c |    192234 |   29799   123162 |   17451   12986  1727440   133.0 | 29.053 % |
c |    192742 |   29644   121709 |   19096   13477  1811174   134.4 | 29.192 % |
c |    193504 |   29644   121709 |   21006   14239  1916650   134.6 | 29.192 % |
c |    194643 |   29644   121709 |   23107   15378  2124586   138.2 | 29.192 % |
c |    196352 |   29644   121709 |   25417   17087  2332516   136.5 | 29.192 % |
c |    198916 |   29644   121709 |   27959   19651  2969429   151.1 | 29.192 % |
c ==============================================================================
c (current CPU-time: 681.338 s)
c ==============================================================================
c [1mFound solution: 1677[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    202120 |   29762   122094 |    8928   22848  3903489   170.8 | 29.192 % |
c   -- subsuming                       
c   -- var.elim.:  619/619          
c   -- var.elim.:  572/572          
c   -- var.elim.:  256/256          
c   -- var.elim.:  3/3          
c   -- var.elim.:  63/63          
c   -- subsuming                       
c   -- var.elim.:  293/293          
c   -- var.elim.:  18/18          
c |    202120 |   29598   122146 |      --   22848       --      -- |     --   | -163/55
c |    202120 |   29598   122146 |   11839   21635  3447942   159.4 | 29.192 % |
c |    202222 |   29598   122146 |   13023   14526  1846109   127.1 | 29.287 % |
c |    202372 |   29598   122146 |   14325   14676  1881635   128.2 | 29.287 % |
c |    202597 |   29598   122146 |   15757   14901  1925831   129.2 | 29.287 % |
c |    202935 |   29598   122146 |   17333   15239  2014886   132.2 | 29.287 % |
c |    203443 |   29598   122146 |   19067   15747  2109259   133.9 | 29.287 % |
c |    204205 |   29598   122146 |   20973   16509  2319947   140.5 | 29.287 % |
c |    205346 |   29598   122146 |   23071   17650  2568395   145.5 | 29.287 % |
c |    207054 |   29598   122146 |   25378   19358  2930655   151.4 | 29.287 % |
c |    209617 |   29598   122146 |   27916   21921  3597567   164.1 | 29.287 % |
c |    213463 |   29598   122146 |   30707   25767  4527610   175.7 | 29.287 % |
c |    219230 |   29586   122108 |   33764   31533  5645992   179.1 | 29.311 % |
c |    227882 |   29586   122108 |   37141   20266  3378868   166.7 | 29.311 % |
c ==============================================================================
c (current CPU-time: 813.134 s)
c ==============================================================================
c [1mFound solution: 1676[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    236258 |   28944   118098 |    8683   28430  5139581   180.8 | 29.311 % |
c   -- subsuming                       
c   -- var.elim.:  829/829          
c   -- var.elim.:  849/849          
c   -- var.elim.:  358/358          
c   -- var.elim.:  250/250          
c   -- var.elim.:  162/162          
c   -- subsuming                       
c   -- var.elim.:  379/379          
c   -- var.elim.:  56/56          
c |    236258 |   28694   118211 |      --   28430       --      -- |     --   | -250/114
c |    236258 |   28694   118211 |   11477   19220  1484027    77.2 | 29.311 % |
c |    236360 |   28694   118211 |   12625   12916   785855    60.8 | 30.376 % |
c |    236512 |   28694   118211 |   13887   13068   808513    61.9 | 30.376 % |
c |    236737 |   28694   118211 |   15276   13293   855199    64.3 | 30.376 % |
c |    237074 |   28694   118211 |   16804   13630   931827    68.4 | 30.376 % |
c |    237580 |   28694   118211 |   18484   14136  1021050    72.2 | 30.376 % |
c |    238340 |   28694   118211 |   20333   14896  1151638    77.3 | 30.376 % |
c |    239481 |   28694   118211 |   22366   16037  1393227    86.9 | 30.376 % |
c |    241190 |   28694   118211 |   24603   17746  1747554    98.5 | 30.376 % |
c |    243752 |   28694   118211 |   27063   20308  2335796   115.0 | 30.376 % |
c |    247596 |   28694   118211 |   29769   24152  3091538   128.0 | 30.376 % |
c |    253362 |   28673   118108 |   32722   29911  4055469   135.6 | 30.409 % |
c |    262011 |   28560   117221 |   35853   19027  2393552   125.8 | 30.500 % |
c ==============================================================================
c (current CPU-time: 931.476 s)
c ==============================================================================
c [1mFound solution: 1664[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    269962 |   28701   117661 |    8610   26978  4160036   154.2 | 30.500 % |
c   -- subsuming                       
c   -- var.elim.:  570/570          
c   -- var.elim.:  505/505          
c   -- var.elim.:  169/169          
c   -- var.elim.:  167/167          
c   -- subsuming                       
c   -- var.elim.:  185/185          
c   -- var.elim.:  33/33          
c |    269962 |   28528   117931 |      --   26978       --      -- |     --   | -171/275
c |    269962 |   28528   117931 |   11411   16314  1033637    63.4 | 30.500 % |
c |    270064 |   28528   117931 |   12552   10978   732180    66.7 | 30.585 % |
c |    270215 |   28528   117931 |   13807   11129   740441    66.5 | 30.585 % |
c |    270442 |   28528   117931 |   15188   11356   780494    68.7 | 30.585 % |
c |    270781 |   28528   117931 |   16707   11695   784346    67.1 | 30.585 % |
c |    271287 |   28528   117931 |   18377   12201   889263    72.9 | 30.585 % |
c |    272046 |   28528   117931 |   20215   12960  1017929    78.5 | 30.585 % |
c |    273185 |   28528   117931 |   22237   14099  1205338    85.5 | 30.585 % |
c |    274893 |   28452   117667 |   24395   15805  1413135    89.4 | 30.660 % |
c |    277455 |   28452   117667 |   26835   18367  2012437   109.6 | 30.659 % |
c |    281299 |   28452   117667 |   29518   22211  2737834   123.3 | 30.660 % |
c |    287066 |   28447   117651 |   32465   27977  4043734   144.5 | 30.668 % |
c ==============================================================================
c (current CPU-time: 1004.14 s)
c ==============================================================================
c [1mFound solution: 1661[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 5 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    292512 |   30458   122299 |    9137   33398  5214485   156.1 | 30.668 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2298          
c   -- var.elim.:  2000/2298          
c   -- var.elim.:  2298/2298          
c   -- var.elim.:  1000/1202          
c   -- var.elim.:  1202/1202          
c   -- var.elim.:  455/455          
c   -- var.elim.:  281/281          
c   -- var.elim.:  285/285          
c   -- var.elim.:  162/162          
c   -- subsuming                       
c   -- var.elim.:  227/227          
c   -- var.elim.:  150/150          
c   -- var.elim.:  7/7          
c   -- var.elim.:  83/83          
c   -- var.elim.:  125/125          
c   -- var.elim.:  77/77          
c |    292512 |   28295   117636 |      --   33398       --      -- |     --   | -2163/-4662
c |    292512 |   28295   117636 |   11318   19920  1070071    53.7 | 30.668 % |
c |    292612 |   28295   117636 |   12449   10794   487390    45.2 | 30.825 % |
c |    292762 |   28295   117636 |   13694   10944   504113    46.1 | 30.825 % |
c |    292989 |   28295   117636 |   15064   11171   533483    47.8 | 30.825 % |
c |    293326 |   28295   117636 |   16570   11508   573843    49.9 | 30.825 % |
c |    293832 |   28295   117636 |   18227   12014   656295    54.6 | 30.825 % |
c |    294591 |   28295   117636 |   20050   12773   717798    56.2 | 30.825 % |
c |    295732 |   28295   117636 |   22055   13914   901401    64.8 | 30.825 % |
c |    297441 |   28295   117636 |   24261   15623  1182466    75.7 | 30.825 % |
c |    300004 |   28295   117636 |   26687   18186  1625855    89.4 | 30.825 % |
c |    303848 |   28295   117636 |   29355   22030  2387740   108.4 | 30.825 % |
c ==============================================================================
c (current CPU-time: 1050.35 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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    305977 |   28462   118132 |    8538   24159  2894073   119.8 | 30.825 % |
c   -- subsuming                       
c   -- var.elim.:  401/401          
c   -- var.elim.:  230/230          
c   -- var.elim.:  182/182          
c |    305977 |   28282   117547 |      --   24159       --      -- |     --   | -177/-578
c |    305977 |   28282   117547 |   11312   24159  2894073   119.8 | 30.825 % |
c |    306077 |   28282   117547 |   12444   10838  1241388   114.5 | 30.819 % |
c |    306229 |   28282   117547 |   13688   10990  1256877   114.4 | 30.819 % |
c |    306454 |   28282   117547 |   15057   11215  1282465   114.4 | 30.819 % |
c |    306791 |   28282   117547 |   16563   11552  1317909   114.1 | 30.819 % |
c |    307297 |   28282   117547 |   18219   12058  1387442   115.1 | 30.819 % |
c |    308056 |   28282   117547 |   20041   12817  1516251   118.3 | 30.819 % |
c |    309195 |   28282   117547 |   22045   13956  1664541   119.3 | 30.819 % |
c |    310903 |   28282   117547 |   24249   15664  1958435   125.0 | 30.819 % |
c |    313467 |   28282   117547 |   26674   18228  2568765   140.9 | 30.819 % |
c |    317313 |   28282   117547 |   29342   22074  3254845   147.5 | 30.819 % |
c |    323079 |   28282   117547 |   32276   27840  3675613   132.0 | 30.819 % |
c |    331728 |   28282   117547 |   35504   36489  5276832   144#### 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.91 0.95 0.90 2/54 12770
Raw data (stat): 12770 (runsolver) R 12769 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 429592825 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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+10.0004 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 7628 0 0 0 972 26 0 0 25 0 1 0 429592825 18317312 3884 4294967295 134512640 134672761 3221224576 3221223024 134644014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4472 3884 603 41 0 4431 0
vsize: 17888
[startup+20.0003 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 10348 0 0 0 1963 34 0 0 25 0 1 0 429592825 21983232 4554 4294967295 134512640 134672761 3221224576 3221222864 134614505 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5367 4554 603 41 0 5326 0
vsize: 21468
[startup+30.0013 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 10559 0 0 0 2960 37 0 0 25 0 1 0 429592825 20144128 4381 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4918 4381 603 41 0 4877 0
vsize: 19672
[startup+40.0009 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 10779 0 0 0 3958 38 0 0 25 0 1 0 429592825 20938752 4601 4294967295 134512640 134672761 3221224576 3221223760 134615734 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5112 4601 603 41 0 5071 0
vsize: 20448
[startup+50.0019 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 11537 0 0 0 4956 41 0 0 25 0 1 0 429592825 24096768 5359 4294967295 134512640 134672761 3221224576 3221223760 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5883 5359 603 41 0 5842 0
vsize: 23532
[startup+60.0017 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 12592 0 0 0 5953 43 0 0 25 0 1 0 429592825 28401664 6414 4294967295 134512640 134672761 3221224576 3221223760 134615683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6934 6414 603 41 0 6893 0
vsize: 27736
[startup+70.0011 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 13187 0 0 0 6952 45 0 0 25 0 1 0 429592825 30904320 7009 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7545 7009 603 41 0 7504 0
vsize: 30180
[startup+80.0022 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 13914 0 0 0 7950 47 0 0 25 0 1 0 429592825 33820672 7736 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8257 7736 603 41 0 8216 0
vsize: 33028
[startup+90.0023 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 15291 0 0 0 8944 53 0 0 25 0 1 0 429592825 37625856 8641 4294967295 134512640 134672761 3221224576 3221223760 134615671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9186 8641 603 41 0 9145 0
vsize: 36744
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 15291 0 0 0 9944 53 0 0 25 0 1 0 429592825 37625856 8641 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9186 8641 603 41 0 9145 0
vsize: 36744
[startup+110.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 15291 0 0 0 10944 53 0 0 25 0 1 0 429592825 37625856 8641 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9186 8641 603 41 0 9145 0
vsize: 36744
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 15926 0 0 0 11941 56 0 0 25 0 1 0 429592825 35807232 8202 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8742 8202 603 41 0 8701 0
vsize: 34968
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 15926 0 0 0 12940 56 0 0 25 0 1 0 429592825 35807232 8202 4294967295 134512640 134672761 3221224576 3221223712 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8742 8202 603 41 0 8701 0
vsize: 34968
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 16811 0 0 0 13938 59 0 0 25 0 1 0 429592825 35807232 8231 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8742 8231 603 41 0 8701 0
vsize: 34968
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 16811 0 0 0 14938 59 0 0 25 0 1 0 429592825 35807232 8231 4294967295 134512640 134672761 3221224576 3221223568 134565101 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8742 8231 603 41 0 8701 0
vsize: 34968
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 16811 0 0 0 15938 59 0 0 25 0 1 0 429592825 35807232 8231 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8742 8231 603 41 0 8701 0
vsize: 34968
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 16811 0 0 0 16939 59 0 0 25 0 1 0 429592825 35807232 8231 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8742 8231 603 41 0 8701 0
vsize: 34968
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 16811 0 0 0 17939 59 0 0 25 0 1 0 429592825 35807232 8231 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8742 8231 603 41 0 8701 0
vsize: 34968
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 16811 0 0 0 18939 59 0 0 25 0 1 0 429592825 35807232 8231 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8742 8231 603 41 0 8701 0
vsize: 34968
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 16884 0 0 0 19939 59 0 0 25 0 1 0 429592825 36200448 8304 4294967295 134512640 134672761 3221224576 3221223760 134616017 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8838 8304 603 41 0 8797 0
vsize: 35352
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 17346 0 0 0 20938 61 0 0 25 0 1 0 429592825 38043648 8766 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9288 8766 603 41 0 9247 0
vsize: 37152
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 17897 0 0 0 21936 63 0 0 25 0 1 0 429592825 40448000 9317 4294967295 134512640 134672761 3221224576 3221223616 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9875 9317 603 41 0 9834 0
vsize: 39500
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 18511 0 0 0 22935 64 0 0 25 0 1 0 429592825 42938368 9931 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10483 9931 603 41 0 10442 0
vsize: 41932
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 20157 0 0 0 23929 70 0 0 25 0 1 0 429592825 47816704 11101 4294967295 134512640 134672761 3221224576 3221223760 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11674 11101 603 41 0 11633 0
vsize: 46696
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 20157 0 0 0 24928 70 0 0 25 0 1 0 429592825 47816704 11101 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11674 11101 603 41 0 11633 0
vsize: 46696
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 20157 0 0 0 25929 70 0 0 25 0 1 0 429592825 47816704 11101 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11674 11101 603 41 0 11633 0
vsize: 46696
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 20157 0 0 0 26929 70 0 0 25 0 1 0 429592825 47816704 11101 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11674 11101 603 41 0 11633 0
vsize: 46696
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 20687 0 0 0 27926 73 0 0 25 0 1 0 429592825 45780992 10655 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11177 10655 603 41 0 11136 0
vsize: 44708
[startup+290.007 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 20687 0 0 0 28926 73 0 0 25 0 1 0 429592825 45780992 10655 4294967295 134512640 134672761 3221224576 3221223760 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11177 10655 603 41 0 11136 0
vsize: 44708
[startup+300.008 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 21394 0 0 0 29921 77 0 0 25 0 1 0 429592825 46927872 10894 4294967295 134512640 134672761 3221224576 3221223616 134613126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11457 10894 603 41 0 11416 0
vsize: 45828
[startup+310.008 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 21394 0 0 0 30921 77 0 0 25 0 1 0 429592825 46927872 10894 4294967295 134512640 134672761 3221224576 3221223760 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11457 10894 603 41 0 11416 0
vsize: 45828
[startup+320.008 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 21394 0 0 0 31921 77 0 0 25 0 1 0 429592825 46927872 10894 4294967295 134512640 134672761 3221224576 3221223616 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11457 10894 603 41 0 11416 0
vsize: 45828
[startup+330.009 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 21394 0 0 0 32921 77 0 0 25 0 1 0 429592825 46927872 10894 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11457 10894 603 41 0 11416 0
vsize: 45828
[startup+340.009 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 21394 0 0 0 33922 77 0 0 25 0 1 0 429592825 46927872 10894 4294967295 134512640 134672761 3221224576 3221223760 134615845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11457 10894 603 41 0 11416 0
vsize: 45828
[startup+350.009 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 21394 0 0 0 34922 77 0 0 25 0 1 0 429592825 46927872 10894 4294967295 134512640 134672761 3221224576 3221223760 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11457 10894 603 41 0 11416 0
vsize: 45828
[startup+360.009 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 22009 0 0 0 35919 80 0 0 25 0 1 0 429592825 46436352 10820 4294967295 134512640 134672761 3221224576 3221223776 134617686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11337 10820 603 41 0 11296 0
vsize: 45348
[startup+370.009 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 22009 0 0 0 36919 80 0 0 25 0 1 0 429592825 46436352 10820 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11337 10820 603 41 0 11296 0
vsize: 45348
[startup+380.01 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 22009 0 0 0 37919 80 0 0 25 0 1 0 429592825 46436352 10820 4294967295 134512640 134672761 3221224576 3221223712 134614753 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11337 10820 603 41 0 11296 0
vsize: 45348
[startup+390.01 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 22009 0 0 0 38919 80 0 0 25 0 1 0 429592825 46436352 10820 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11337 10820 603 41 0 11296 0
vsize: 45348
[startup+400.011 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 22009 0 0 0 39918 80 0 0 25 0 1 0 429592825 46436352 10820 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11337 10820 603 41 0 11296 0
vsize: 45348
[startup+410.011 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 22009 0 0 0 40918 80 0 0 25 0 1 0 429592825 46436352 10820 4294967295 134512640 134672761 3221224576 3221223760 134615711 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11337 10820 603 41 0 11296 0
vsize: 45348
[startup+420.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 22009 0 0 0 41918 80 0 0 25 0 1 0 429592825 46436352 10820 4294967295 134512640 134672761 3221224576 3221223760 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11337 10820 603 41 0 11296 0
vsize: 45348
[startup+430.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 22009 0 0 0 42919 80 0 0 25 0 1 0 429592825 46436352 10820 4294967295 134512640 134672761 3221224576 3221223740 134614476 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11337 10820 603 41 0 11296 0
vsize: 45348
[startup+440.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 22009 0 0 0 43919 80 0 0 25 0 1 0 429592825 46436352 10820 4294967295 134512640 134672761 3221224576 3221223616 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11337 10820 603 41 0 11296 0
vsize: 45348
[startup+450.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 22009 0 0 0 44919 80 0 0 25 0 1 0 429592825 46436352 10820 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11337 10820 603 41 0 11296 0
vsize: 45348
[startup+460.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 22547 0 0 0 45918 82 0 0 25 0 1 0 429592825 48672768 11358 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11883 11358 603 41 0 11842 0
vsize: 47532
[startup+470.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 23151 0 0 0 46916 83 0 0 25 0 1 0 429592825 51179520 11962 4294967295 134512640 134672761 3221224576 3221223760 134615948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12495 11962 603 41 0 12454 0
vsize: 49980
[startup+480.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 23388 0 0 0 47916 84 0 0 25 0 1 0 429592825 51904512 12157 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12672 12157 603 41 0 12631 0
vsize: 50688
[startup+490.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 23388 0 0 0 48916 84 0 0 25 0 1 0 429592825 51904512 12157 4294967295 134512640 134672761 3221224576 3221223712 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12672 12157 603 41 0 12631 0
vsize: 50688
[startup+500.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 23388 0 0 0 49916 84 0 0 25 0 1 0 429592825 51904512 12157 4294967295 134512640 134672761 3221224576 3221223760 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12672 12157 603 41 0 12631 0
vsize: 50688
[startup+510.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 23388 0 0 0 50916 84 0 0 25 0 1 0 429592825 51904512 12157 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12672 12157 603 41 0 12631 0
vsize: 50688
[startup+520.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 23388 0 0 0 51917 84 0 0 25 0 1 0 429592825 51904512 12157 4294967295 134512640 134672761 3221224576 3221223616 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12672 12157 603 41 0 12631 0
vsize: 50688
[startup+530.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 23388 0 0 0 52917 84 0 0 25 0 1 0 429592825 51904512 12157 4294967295 134512640 134672761 3221224576 3221223760 134615794 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12672 12157 603 41 0 12631 0
vsize: 50688
[startup+540.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 23388 0 0 0 53917 84 0 0 25 0 1 0 429592825 51904512 12157 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12672 12157 603 41 0 12631 0
vsize: 50688
[startup+550.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 24212 0 0 0 54913 87 0 0 25 0 1 0 429592825 53493760 12498 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13060 12498 603 41 0 13019 0
vsize: 52240
[startup+560.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 24212 0 0 0 55914 87 0 0 25 0 1 0 429592825 53493760 12498 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13060 12498 603 41 0 13019 0
vsize: 52240
[startup+570.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 24212 0 0 0 56914 87 0 0 25 0 1 0 429592825 53493760 12498 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13060 12498 603 41 0 13019 0
vsize: 52240
[startup+580.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 24768 0 0 0 57910 91 0 0 25 0 1 0 429592825 53067776 12441 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12956 12441 603 41 0 12915 0
vsize: 51824
[startup+590.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 24768 0 0 0 58911 91 0 0 25 0 1 0 429592825 53067776 12441 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12956 12441 603 41 0 12915 0
vsize: 51824
[startup+600.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 24768 0 0 0 59911 91 0 0 25 0 1 0 429592825 53067776 12441 4294967295 134512640 134672761 3221224576 3221223700 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12956 12441 603 41 0 12915 0
vsize: 51824
[startup+610.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 25472 0 0 0 60906 95 0 0 25 0 1 0 429592825 51900416 12158 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12671 12158 603 41 0 12630 0
vsize: 50684
[startup+620.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 25472 0 0 0 61905 95 0 0 25 0 1 0 429592825 51900416 12158 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12671 12158 603 41 0 12630 0
vsize: 50684
[startup+630.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 25472 0 0 0 62905 95 0 0 25 0 1 0 429592825 51900416 12158 4294967295 134512640 134672761 3221224576 3221223616 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12671 12158 603 41 0 12630 0
vsize: 50684
[startup+640.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 25472 0 0 0 63905 95 0 0 25 0 1 0 429592825 51900416 12158 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12671 12158 603 41 0 12630 0
vsize: 50684
[startup+650.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 26189 0 0 0 64903 98 0 0 25 0 1 0 429592825 52686848 12331 4294967295 134512640 134672761 3221224576 3221223568 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12863 12331 603 41 0 12822 0
vsize: 51452
[startup+660.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 26189 0 0 0 65903 98 0 0 25 0 1 0 429592825 52686848 12331 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12863 12331 603 41 0 12822 0
vsize: 51452
[startup+670.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 26189 0 0 0 66903 98 0 0 25 0 1 0 429592825 52686848 12331 4294967295 134512640 134672761 3221224576 3221223760 134615926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12863 12331 603 41 0 12822 0
vsize: 51452
[startup+680.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 26189 0 0 0 67903 98 0 0 25 0 1 0 429592825 52686848 12331 4294967295 134512640 134672761 3221224576 3221223728 134614555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12863 12331 603 41 0 12822 0
vsize: 51452
[startup+690.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 26932 0 0 0 68899 102 0 0 25 0 1 0 429592825 51900416 12164 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12671 12164 603 41 0 12630 0
vsize: 50684
[startup+700.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 26932 0 0 0 69898 102 0 0 25 0 1 0 429592825 51900416 12164 4294967295 134512640 134672761 3221224576 3221223616 134614209 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12671 12164 603 41 0 12630 0
vsize: 50684
[startup+710.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 26932 0 0 0 70899 102 0 0 25 0 1 0 429592825 51900416 12164 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12671 12164 603 41 0 12630 0
vsize: 50684
[startup+720.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 26933 0 0 0 71899 102 0 0 25 0 1 0 429592825 51900416 12165 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12671 12165 603 41 0 12630 0
vsize: 50684
[startup+730.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 26933 0 0 0 72899 102 0 0 25 0 1 0 429592825 51900416 12165 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12671 12165 603 41 0 12630 0
vsize: 50684
[startup+740.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 26933 0 0 0 73899 102 0 0 25 0 1 0 429592825 51900416 12165 4294967295 134512640 134672761 3221224576 3221223760 134615948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12671 12165 603 41 0 12630 0
vsize: 50684
[startup+750.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 26933 0 0 0 74900 102 0 0 25 0 1 0 429592825 51900416 12165 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12671 12165 603 41 0 12630 0
vsize: 50684
[startup+760.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 26933 0 0 0 75900 102 0 0 25 0 1 0 429592825 51900416 12165 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12671 12165 603 41 0 12630 0
vsize: 50684
[startup+770.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 26933 0 0 0 76900 102 0 0 25 0 1 0 429592825 51900416 12165 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12671 12165 603 41 0 12630 0
vsize: 50684
[startup+780.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 26971 0 0 0 77900 102 0 0 25 0 1 0 429592825 51900416 12165 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12671 12165 603 41 0 12630 0
vsize: 50684
[startup+790.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 26971 0 0 0 78900 102 0 0 25 0 1 0 429592825 51900416 12165 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12671 12165 603 41 0 12630 0
vsize: 50684
[startup+800.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 26971 0 0 0 79900 102 0 0 25 0 1 0 429592825 51900416 12165 4294967295 134512640 134672761 3221224576 3221223760 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12671 12165 603 41 0 12630 0
vsize: 50684
[startup+810.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 26971 0 0 0 80901 102 0 0 25 0 1 0 429592825 51900416 12165 4294967295 134512640 134672761 3221224576 3221223712 134614741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12671 12165 603 41 0 12630 0
vsize: 50684
[startup+820.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 27796 0 0 0 81896 106 0 0 25 0 1 0 429592825 53080064 12442 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12959 12442 603 41 0 12918 0
vsize: 51836
[startup+830.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 27796 0 0 0 82897 106 0 0 25 0 1 0 429592825 53080064 12442 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12959 12442 603 41 0 12918 0
vsize: 51836
[startup+840.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 27796 0 0 0 83897 106 0 0 25 0 1 0 429592825 53080064 12442 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12959 12442 603 41 0 12918 0
vsize: 51836
[startup+850.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 27796 0 0 0 84897 106 0 0 25 0 1 0 429592825 53080064 12442 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12959 12442 603 41 0 12918 0
vsize: 51836
[startup+860.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 27796 0 0 0 85897 106 0 0 25 0 1 0 429592825 53080064 12442 4294967295 134512640 134672761 3221224576 3221223720 134616178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12959 12442 603 41 0 12918 0
vsize: 51836
[startup+870.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 27796 0 0 0 86897 106 0 0 25 0 1 0 429592825 53080064 12442 4294967295 134512640 134672761 3221224576 3221223408 1075350746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12959 12442 603 41 0 12918 0
vsize: 51836
[startup+880.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 27796 0 0 0 87898 106 0 0 25 0 1 0 429592825 53080064 12442 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12959 12442 603 41 0 12918 0
vsize: 51836
[startup+890.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 27796 0 0 0 88898 106 0 0 25 0 1 0 429592825 53080064 12442 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12959 12442 603 41 0 12918 0
vsize: 51836
[startup+900.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 27796 0 0 0 89898 106 0 0 25 0 1 0 429592825 53080064 12442 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12959 12442 603 41 0 12918 0
vsize: 51836
[startup+910.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 27796 0 0 0 90898 106 0 0 25 0 1 0 429592825 53080064 12442 4294967295 134512640 134672761 3221224576 3221223776 134610630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12959 12442 603 41 0 12918 0
vsize: 51836
[startup+920.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 27796 0 0 0 91899 106 0 0 25 0 1 0 429592825 53080064 12442 4294967295 134512640 134672761 3221224576 3221223776 134610661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12959 12442 603 41 0 12918 0
vsize: 51836
[startup+930.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 27796 0 0 0 92899 106 0 0 25 0 1 0 429592825 53080064 12442 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12959 12442 603 41 0 12918 0
vsize: 51836
[startup+940.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 28682 0 0 0 93894 110 0 0 25 0 1 0 429592825 51900416 12168 4294967295 134512640 134672761 3221224576 3221223776 134610661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12671 12168 603 41 0 12630 0
vsize: 50684
[startup+950.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 28682 0 0 0 94894 110 0 0 25 0 1 0 429592825 51900416 12168 4294967295 134512640 134672761 3221224576 3221223616 134614256 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12671 12168 603 41 0 12630 0
vsize: 50684
[startup+960.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 28682 0 0 0 95895 110 0 0 25 0 1 0 429592825 51900416 12168 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12671 12168 603 41 0 12630 0
vsize: 50684
[startup+970.029 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 28682 0 0 0 96895 110 0 0 25 0 1 0 429592825 51900416 12168 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12671 12168 603 41 0 12630 0
vsize: 50684
[startup+980.03 s]
Raw data (loadavg): 1.14 1.02 0.93 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 28682 0 0 0 97895 110 0 0 25 0 1 0 429592825 51900416 12168 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12671 12168 603 41 0 12630 0
vsize: 50684
[startup+990.03 s]
Raw data (loadavg): 1.12 1.02 0.93 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 28682 0 0 0 98895 110 0 0 25 0 1 0 429592825 51900416 12168 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12671 12168 603 41 0 12630 0
vsize: 50684
[startup+1000.03 s]
Raw data (loadavg): 1.10 1.02 0.93 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 28682 0 0 0 99895 110 0 0 25 0 1 0 429592825 51900416 12168 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12671 12168 603 41 0 12630 0
vsize: 50684
[startup+1010.03 s]
Raw data (loadavg): 1.08 1.02 0.93 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 29610 0 0 0 100891 115 0 0 25 0 1 0 429592825 51900416 12200 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12671 12200 603 41 0 12630 0
vsize: 50684
[startup+1020.03 s]
Raw data (loadavg): 1.07 1.02 0.93 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 29610 0 0 0 101889 115 0 0 25 0 1 0 429592825 51900416 12200 4294967295 134512640 134672761 3221224576 3221223776 134610644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12671 12200 603 41 0 12630 0
vsize: 50684
[startup+1030.03 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 29610 0 0 0 102890 115 0 0 25 0 1 0 429592825 51900416 12200 4294967295 134512640 134672761 3221224576 3221223952 134620485 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12671 12200 603 41 0 12630 0
vsize: 50684
[startup+1040.03 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 29610 0 0 0 103890 115 0 0 25 0 1 0 429592825 51900416 12200 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12671 12200 603 41 0 12630 0
vsize: 50684
[startup+1050.03 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 29610 0 0 0 104890 115 0 0 25 0 1 0 429592825 51900416 12200 4294967295 134512640 134672761 3221224576 3221223760 134615546 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12671 12200 603 41 0 12630 0
vsize: 50684
[startup+1060.03 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 30374 0 0 0 105887 119 0 0 25 0 1 0 429592825 52686848 12386 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12863 12386 603 41 0 12822 0
vsize: 51452
[startup+1070.03 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 30374 0 0 0 106887 119 0 0 25 0 1 0 429592825 52686848 12386 4294967295 134512640 134672761 3221224576 3221223568 134565121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12863 12386 603 41 0 12822 0
vsize: 51452
[startup+1080.03 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 30374 0 0 0 107887 119 0 0 25 0 1 0 429592825 52686848 12386 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12863 12386 603 41 0 12822 0
vsize: 51452
[startup+1090.03 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 30374 0 0 0 108887 119 0 0 25 0 1 0 429592825 52686848 12386 4294967295 134512640 134672761 3221224576 3221223760 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12863 12386 603 41 0 12822 0
vsize: 51452
[startup+1100.03 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 30374 0 0 0 109887 119 0 0 25 0 1 0 429592825 52686848 12386 4294967295 134512640 134672761 3221224576 3221223760 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12863 12386 603 41 0 12822 0
vsize: 51452
[startup+1110.03 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 30374 0 0 0 110888 119 0 0 25 0 1 0 429592825 52686848 12386 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12863 12386 603 41 0 12822 0
vsize: 51452
[startup+1120.03 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 30374 0 0 0 111888 119 0 0 25 0 1 0 429592825 52686848 12386 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12863 12386 603 41 0 12822 0
vsize: 51452
[startup+1130.03 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 30374 0 0 0 112888 119 0 0 25 0 1 0 429592825 52686848 12386 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12863 12386 603 41 0 12822 0
vsize: 51452
[startup+1140.03 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 30374 0 0 0 113888 119 0 0 25 0 1 0 429592825 52686848 12386 4294967295 134512640 134672761 3221224576 3221223568 134565110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12863 12386 603 41 0 12822 0
vsize: 51452
[startup+1150.03 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 30374 0 0 0 114888 119 0 0 25 0 1 0 429592825 52686848 12386 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12863 12386 603 41 0 12822 0
vsize: 51452
[startup+1160.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 30374 0 0 0 115888 119 0 0 25 0 1 0 429592825 52686848 12386 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12863 12386 603 41 0 12822 0
vsize: 51452
[startup+1170.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 30374 0 0 0 116888 119 0 0 25 0 1 0 429592825 52686848 12386 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12863 12386 603 41 0 12822 0
vsize: 51452
[startup+1180.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 30374 0 0 0 117888 119 0 0 25 0 1 0 429592825 52686848 12386 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12863 12386 603 41 0 12822 0
vsize: 51452
[startup+1190.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 31042 0 0 0 118885 122 0 0 25 0 1 0 429592825 52674560 12383 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12860 12383 603 41 0 12819 0
vsize: 51440
[startup+1200.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12770
Raw data (stat): 12770 (minisat+) R 12769 32461 32460 0 -1 0 31042 0 0 0 119885 122 0 0 25 0 1 0 429592825 52674560 12383 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12860 12383 603 41 0 12819 0
vsize: 51440
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 12770
Raw data (stat): 12770 (minisat+) Z 12769 32461 32460 0 -1 12 31043 0 0 0 119885 125 0 0 25 0 1 0 429592825 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.07
CPU time (s): 1200.12
CPU user time (s): 1198.86
CPU system time (s): 1.25681
CPU usage (%): 100.004
Max. virtual memory (Kb): 52240
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####