PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-p0291.opb
MD5SUM	1d9168a9335e29df835d07b0bdf2adea
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	10447498
Optimality of the best value was proved	NO
Number of terms in the objective function	289
Biggest coefficient in the objective function	80000000
Number of bits for the biggest coefficient in the objective function	27
Sum of the numbers in the objective function	686518451
Number of bits of the sum of numbers in the objective function	30
Biggest number in a constraint	80000000
Number of bits of the biggest number in a constraint	27
Biggest sum of numbers in a constraint	686518451
Number of bits of the biggest sum of numbers	30
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	0.333948
Number of variables	291
Total number of constraints	543
Number of constraints which are clauses	189
Number of constraints which are cardinality constraints (but not clauses)	295
Number of constraints which are nor clauses,nor cardinality constraints	59
Minimum length of a constraint	1
Maximum length of a constraint	53
Trace number 19025

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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:        888616 kB
Buffers:          3980 kB
Cached:         120324 kB
SwapCached:          0 kB
Active:          53988 kB
Inactive:        73260 kB
HighTotal:      131008 kB
HighFree:        38164 kB
LowTotal:       903652 kB
LowFree:        850452 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6952 kB
Slab:            13008 kB
Committed_AS:    63792 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 17:57:09 (client local time) WITH STATUS 10 IN 1209.45 SECONDS
stats: 17145 7 1209.45 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 205 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .............................................................................................................................................................................................sssss
c ---[ 144]---> BDD-cost:    3
c ---[ 139]---> BDD-cost:    3
c ---[  14]---> Sorter-cost: 1503     Base: 2 2 5 2 3
c ---[  13]---> Sorter-cost: 1241     Base: 2 2 5 2 3
c ---[  11]---> BDD-cost:   52
c ---[  10]---> BDD-cost:   52
c ---[   9]---> BDD-cost:   52
c ---[   8]---> BDD-cost:   12
c ---[   7]---> BDD-cost:    8
c ---[   6]---> BDD-cost:   16
c ---[   5]---> BDD-cost:   28
c ---[   4]---> BDD-cost:   12
c ---[   3]---> BDD-cost:   86
c ---[   2]---> Sorter-cost:  748     Base: 2 5 2 2
c ---[   1]---> Sorter-cost:  880     Base: 2 2 5 3
c ---[   0]---> BDD-cost:    1
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   10113    23792 |    3033       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3539          
c   -- var.elim.:  2000/3539          
c   -- var.elim.:  3000/3539          
c   -- var.elim.:  3539/3539          
c   -- var.elim.:  1000/2060          
c   -- var.elim.:  2000/2060          
c   -- var.elim.:  2060/2060          
c   -- var.elim.:  59/59          
c   -- var.elim.:  7/7          
c   -- subsuming                       
c   -- var.elim.:  565/565          
c   -- var.elim.:  285/285          
c   -- var.elim.:  8/8          
c   -- subsuming                       
c   -- var.elim.:  150/150          
c   -- var.elim.:  62/62          
c |         0 |    8525    27214 |      --       0       --      -- |     --   | -1588/3442
c |         0 |    8525    27214 |    3410       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.668898 s)
c ==============================================================================
c [1mFound solution: 109177996[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:118481     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |        47 |  348762   821555 |  104628      46      371     8.1 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/114394          
c   -- var.elim.:  2000/114394          
c   -- var.elim.:  3000/114394          
c   -- var.elim.:  4000/114394          
c   -- var.elim.:  5000/114394          
c   -- var.elim.:  6000/114394          
c   -- var.elim.:  7000/114394          
c   -- var.elim.:  8000/114394          
c   -- var.elim.:  9000/114394          
c   -- var.elim.:  10000/114394          
c   -- var.elim.:  11000/114394          
c   -- var.elim.:  12000/114394          
c   -- var.elim.:  13000/114394          
c   -- var.elim.:  14000/114394          
c   -- var.elim.:  15000/114394          
c   -- var.elim.:  16000/114394          
c   -- var.elim.:  17000/114394          
c   -- var.elim.:  18000/114394          
c   -- var.elim.:  19000/114394          
c   -- var.elim.:  20000/114394          
c   -- var.elim.:  21000/114394          
c   -- var.elim.:  22000/114394          
c   -- var.elim.:  23000/114394          
c   -- var.elim.:  24000/114394          
c   -- var.elim.:  25000/114394          
c   -- var.elim.:  26000/114394          
c   -- var.elim.:  27000/114394          
c   -- var.elim.:  28000/114394          
c   -- var.elim.:  29000/114394          
c   -- var.elim.:  30000/114394          
c   -- var.elim.:  31000/114394          
c   -- var.elim.:  32000/114394          
c   -- var.elim.:  33000/114394          
c   -- var.elim.:  34000/114394          
c   -- var.elim.:  35000/114394          
c   -- var.elim.:  36000/114394          
c   -- var.elim.:  37000/114394          
c   -- var.elim.:  38000/114394          
c   -- var.elim.:  39000/114394          
c   -- var.elim.:  40000/114394          
c   -- var.elim.:  41000/114394          
c   -- var.elim.:  42000/114394          
c   -- var.elim.:  43000/114394          
c   -- var.elim.:  44000/114394          
c   -- var.elim.:  45000/114394          
c   -- var.elim.:  46000/114394          
c   -- var.elim.:  47000/114394          
c   -- var.elim.:  48000/114394          
c   -- var.elim.:  49000/114394          
c   -- var.elim.:  50000/114394          
c   -- var.elim.:  51000/114394          
c   -- var.elim.:  52000/114394          
c   -- var.elim.:  53000/114394          
c   -- var.elim.:  54000/114394          
c   -- var.elim.:  55000/114394          
c   -- var.elim.:  56000/114394          
c   -- var.elim.:  57000/114394          
c   -- var.elim.:  58000/114394          
c   -- var.elim.:  59000/114394          
c   -- var.elim.:  60000/114394          
c   -- var.elim.:  61000/114394          
c   -- var.elim.:  62000/114394          
c   -- var.elim.:  63000/114394          
c   -- var.elim.:  64000/114394          
c   -- var.elim.:  65000/114394          
c   -- var.elim.:  66000/114394          
c   -- var.elim.:  67000/114394          
c   -- var.elim.:  68000/114394          
c   -- var.elim.:  69000/114394          
c   -- var.elim.:  70000/114394          
c   -- var.elim.:  71000/114394          
c   -- var.elim.:  72000/114394          
c   -- var.elim.:  73000/114394          
c   -- var.elim.:  74000/114394          
c   -- var.elim.:  75000/114394          
c   -- var.elim.:  76000/114394          
c   -- var.elim.:  77000/114394          
c   -- var.elim.:  78000/114394          
c   -- var.elim.:  79000/114394          
c   -- var.elim.:  80000/114394          
c   -- var.elim.:  81000/114394          
c   -- var.elim.:  82000/114394          
c   -- var.elim.:  83000/114394          
c   -- var.elim.:  84000/114394          
c   -- var.elim.:  85000/114394          
c   -- var.elim.:  86000/114394          
c   -- var.elim.:  87000/114394          
c   -- var.elim.:  88000/114394          
c   -- var.elim.:  89000/114394          
c   -- var.elim.:  90000/114394          
c   -- var.elim.:  91000/114394          
c   -- var.elim.:  92000/114394          
c   -- var.elim.:  93000/114394          
c   -- var.elim.:  94000/114394          
c   -- var.elim.:  95000/114394          
c   -- var.elim.:  96000/114394          
c   -- var.elim.:  97000/114394          
c   -- var.elim.:  98000/114394          
c   -- var.elim.:  99000/114394          
c   -- var.elim.:  100000/114394          
c   -- var.elim.:  101000/114394          
c   -- var.elim.:  102000/114394          
c   -- var.elim.:  103000/114394          
c   -- var.elim.:  104000/114394          
c   -- var.elim.:  105000/114394          
c   -- var.elim.:  106000/114394          
c   -- var.elim.:  107000/114394          
c   -- var.elim.:  108000/114394          
c   -- var.elim.:  109000/114394          
c   -- var.elim.:  110000/114394          
c   -- var.elim.:  111000/114394          
c   -- var.elim.:  112000/114394          
c   -- var.elim.:  113000/114394          
c   -- var.elim.:  114000/114394          
c   -- var.elim.:  114394/114394          
c   -- var.elim.:  1000/63334          
c   -- var.elim.:  2000/63334          
c   -- var.elim.:  3000/63334          
c   -- var.elim.:  4000/63334          
c   -- var.elim.:  5000/63334          
c   -- var.elim.:  6000/63334          
c   -- var.elim.:  7000/63334          
c   -- var.elim.:  8000/63334          
c   -- var.elim.:  9000/63334          
c   -- var.elim.:  10000/63334          
c   -- var.elim.:  11000/63334          
c   -- var.elim.:  12000/63334          
c   -- var.elim.:  13000/63334          
c   -- var.elim.:  14000/63334          
c   -- var.elim.:  15000/63334          
c   -- var.elim.:  16000/63334          
c   -- var.elim.:  17000/63334          
c   -- var.elim.:  18000/63334          
c   -- var.elim.:  19000/63334          
c   -- var.elim.:  20000/63334          
c   -- var.elim.:  21000/63334          
c   -- var.elim.:  22000/63334          
c   -- var.elim.:  23000/63334          
c   -- var.elim.:  24000/63334          
c   -- var.elim.:  25000/63334          
c   -- var.elim.:  26000/63334          
c   -- var.elim.:  27000/63334          
c   -- var.elim.:  28000/63334          
c   -- var.elim.:  29000/63334          
c   -- var.elim.:  30000/63334          
c   -- var.elim.:  31000/63334          
c   -- var.elim.:  32000/63334          
c   -- var.elim.:  33000/63334          
c   -- var.elim.:  34000/63334          
c   -- var.elim.:  35000/63334          
c   -- var.elim.:  36000/63334          
c   -- var.elim.:  37000/63334          
c   -- var.elim.:  38000/63334          
c   -- var.elim.:  39000/63334          
c   -- var.elim.:  40000/63334          
c   -- var.elim.:  41000/63334          
c   -- var.elim.:  42000/63334          
c   -- var.elim.:  43000/63334          
c   -- var.elim.:  44000/63334          
c   -- var.elim.:  45000/63334          
c   -- var.elim.:  46000/63334          
c   -- var.elim.:  47000/63334          
c   -- var.elim.:  48000/63334          
c   -- var.elim.:  49000/63334          
c   -- var.elim.:  50000/63334          
c   -- var.elim.:  51000/63334          
c   -- var.elim.:  52000/63334          
c   -- var.elim.:  53000/63334          
c   -- var.elim.:  54000/63334          
c   -- var.elim.:  55000/63334          
c   -- var.elim.:  56000/63334          
c   -- var.elim.:  57000/63334          
c   -- var.elim.:  58000/63334          
c   -- var.elim.:  59000/63334          
c   -- var.elim.:  60000/63334          
c   -- var.elim.:  61000/63334          
c   -- var.elim.:  62000/63334          
c   -- var.elim.:  63000/63334          
c   -- var.elim.:  63334/63334          
c   -- var.elim.:  149/149          
c   -- subsuming                       
c   -- var.elim.:  1000/1503          
c   -- var.elim.:  1503/1503          
c   -- var.elim.:  398/398          
c   -- subsuming                       
c   -- var.elim.:  186/186          
c   -- var.elim.:  18/18          
c |        47 |  320870   980831 |      --      46       --      -- |     --   | -27892/159277
c |        47 |  320870   980831 |  128348      46      371     8.1 |  0.000 % |
c |       147 |  320870   980831 |  141182     146     2117    14.5 |  0.055 % |
c |       297 |  320857   980578 |  155294     295     4003    13.6 |  0.057 % |
c ==============================================================================
c (current CPU-time: 64.4472 s)
c ==============================================================================
c [1mFound solution: 101672545[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   23     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       422 |  322979   986843 |   96893     415     7220    17.4 |  0.057 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4734          
c   -- var.elim.:  2000/4734          
c   -- var.elim.:  3000/4734          
c   -- var.elim.:  4000/4734          
c   -- var.elim.:  4734/4734          
c   -- var.elim.:  1000/3098          
c   -- var.elim.:  2000/3098          
c   -- var.elim.:  3000/3098          
c   -- var.elim.:  3098/3098          
c   -- var.elim.:  8/8          
c   -- var.elim.:  1000/1028          
c   -- var.elim.:  1028/1028          
c   -- subsuming                       
c   -- var.elim.:  78/78          
c   -- var.elim.:  12/12          
c |       422 |  321676   988308 |      --     415       --      -- |     --   | -1303/1466
c |       422 |  321676   988308 |  128670     411     7154    17.4 |  0.057 % |
c ==============================================================================
c (current CPU-time: 112.439 s)
c ==============================================================================
c [1mFound solution: 94247567[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   23     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       518 |  322396   991918 |   96718     507    19356    38.2 |  0.057 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2811          
c   -- var.elim.:  2000/2811          
c   -- var.elim.:  2811/2811          
c   -- var.elim.:  1000/2298          
c   -- var.elim.:  2000/2298          
c   -- var.elim.:  2298/2298          
c   -- var.elim.:  493/493          
c   -- subsuming                       
c   -- var.elim.:  445/445          
c   -- var.elim.:  113/113          
c |       518 |  321953   997012 |      --     507       --      -- |     --   | -443/5095
c |       518 |  321953   997012 |  128781     507    19356    38.2 |  0.057 % |
c |       618 |  321687   994669 |  141542     595    21387    35.9 |  0.145 % |
c |       768 |  321687   994669 |  155696     745    22845    30.7 |  0.145 % |
c |       994 |  321687   994669 |  171266     971    24458    25.2 |  0.145 % |
c |      1331 |  321638   994377 |  188364    1307    26655    20.4 |  0.156 % |
c |      1838 |  320749   990221 |  206627    1810    47144    26.0 |  0.340 % |
c ==============================================================================
c (current CPU-time: 167.204 s)
c ==============================================================================
c [1mFound solution: 88401572[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:80211     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 2 7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2155 |  550375  1526018 |  165112    2119    62244    29.4 |  0.340 % |
c   -- subsuming                       
c   -- var.elim.:  1000/81915          
c   -- var.elim.:  2000/81915          
c   -- var.elim.:  3000/81915          
c   -- var.elim.:  4000/81915          
c   -- var.elim.:  5000/81915          
c   -- var.elim.:  6000/81915          
c   -- var.elim.:  7000/81915          
c   -- var.elim.:  8000/81915          
c   -- var.elim.:  9000/81915          
c   -- var.elim.:  10000/81915          
c   -- var.elim.:  11000/81915          
c   -- var.elim.:  12000/81915          
c   -- var.elim.:  13000/81915          
c   -- var.elim.:  14000/81915          
c   -- var.elim.:  15000/81915          
c   -- var.elim.:  16000/81915          
c   -- var.elim.:  17000/81915          
c   -- var.elim.:  18000/81915          
c   -- var.elim.:  19000/81915          
c   -- var.elim.:  20000/81915          
c   -- var.elim.:  21000/81915          
c   -- var.elim.:  22000/81915          
c   -- var.elim.:  23000/81915          
c   -- var.elim.:  24000/81915          
c   -- var.elim.:  25000/81915          
c   -- var.elim.:  26000/81915          
c   -- var.elim.:  27000/81915          
c   -- var.elim.:  28000/81915          
c   -- var.elim.:  29000/81915          
c   -- var.elim.:  30000/81915          
c   -- var.elim.:  31000/81915          
c   -- var.elim.:  32000/81915          
c   -- var.elim.:  33000/81915          
c   -- var.elim.:  34000/81915          
c   -- var.elim.:  35000/81915          
c   -- var.elim.:  36000/81915          
c   -- var.elim.:  37000/81915          
c   -- var.elim.:  38000/81915          
c   -- var.elim.:  39000/81915          
c   -- var.elim.:  40000/81915          
c   -- var.elim.:  41000/81915          
c   -- var.elim.:  42000/81915          
c   -- var.elim.:  43000/81915          
c   -- var.elim.:  44000/81915          
c   -- var.elim.:  45000/81915          
c   -- var.elim.:  46000/81915          
c   -- var.elim.:  47000/81915          
c   -- var.elim.:  48000/81915          
c   -- var.elim.:  49000/81915          
c   -- var.elim.:  50000/81915          
c   -- var.elim.:  51000/81915          
c   -- var.elim.:  52000/81915          
c   -- var.elim.:  53000/81915          
c   -- var.elim.:  54000/81915          
c   -- var.elim.:  55000/81915          
c   -- var.elim.:  56000/81915          
c   -- var.elim.:  57000/81915          
c   -- var.elim.:  58000/81915          
c   -- var.elim.:  59000/81915          
c   -- var.elim.:  60000/81915          
c   -- var.elim.:  61000/81915          
c   -- var.elim.:  62000/81915          
c   -- var.elim.:  63000/81915          
c   -- var.elim.:  64000/81915          
c   -- var.elim.:  65000/81915          
c   -- var.elim.:  66000/81915          
c   -- var.elim.:  67000/81915          
c   -- var.elim.:  68000/81915          
c   -- var.elim.:  69000/81915          
c   -- var.elim.:  70000/81915          
c   -- var.elim.:  71000/81915          
c   -- var.elim.:  72000/81915          
c   -- var.elim.:  73000/81915          
c   -- var.elim.:  74000/81915          
c   -- var.elim.:  75000/81915          
c   -- var.elim.:  76000/81915          
c   -- var.elim.:  77000/81915          
c   -- var.elim.:  78000/81915          
c   -- var.elim.:  79000/81915          
c   -- var.elim.:  80000/81915          
c   -- var.elim.:  81000/81915          
c   -- var.elim.:  81915/81915          
c   -- var.elim.:  1000/46265          
c   -- var.elim.:  2000/46265          
c   -- var.elim.:  3000/46265          
c   -- var.elim.:  4000/46265          
c   -- var.elim.:  5000/46265          
c   -- var.elim.:  6000/46265          
c   -- var.elim.:  7000/46265          
c   -- var.elim.:  8000/46265          
c   -- var.elim.:  9000/46265          
c   -- var.elim.:  10000/46265          
c   -- var.elim.:  11000/46265          
c   -- var.elim.:  12000/46265          
c   -- var.elim.:  13000/46265          
c   -- var.elim.:  14000/46265          
c   -- var.elim.:  15000/46265          
c   -- var.elim.:  16000/46265          
c   -- var.elim.:  17000/46265          
c   -- var.elim.:  18000/46265          
c   -- var.elim.:  19000/46265          
c   -- var.elim.:  20000/46265          
c   -- var.elim.:  21000/46265          
c   -- var.elim.:  22000/46265          
c   -- var.elim.:  23000/46265          
c   -- var.elim.:  24000/46265          
c   -- var.elim.:  25000/46265          
c   -- var.elim.:  26000/46265          
c   -- var.elim.:  27000/46265          
c   -- var.elim.:  28000/46265          
c   -- var.elim.:  29000/46265          
c   -- var.elim.:  30000/46265          
c   -- var.elim.:  31000/46265          
c   -- var.elim.:  32000/46265          
c   -- var.elim.:  33000/46265          
c   -- var.elim.:  34000/46265          
c   -- var.elim.:  35000/46265          
c   -- var.elim.:  36000/46265          
c   -- var.elim.:  37000/46265          
c   -- var.elim.:  38000/46265          
c   -- var.elim.:  39000/46265          
c   -- var.elim.:  40000/46265          
c   -- var.elim.:  41000/46265          
c   -- var.elim.:  42000/46265          
c   -- var.elim.:  43000/46265          
c   -- var.elim.:  44000/46265          
c   -- var.elim.:  45000/46265          
c   -- var.elim.:  46000/46265          
c   -- var.elim.:  46265/46265          
c   -- var.elim.:  282/282          
c   -- var.elim.:  153/153          
c   -- subsuming                       
c   -- var.elim.:  664/664          
c   -- var.elim.:  192/192          
c |      2155 |  529183  1630245 |      --    2119       --      -- |     --   | -21172/104274
c |      2155 |  529183  1630245 |  211673    1998    41678    20.9 |  0.340 % |
c |      2255 |  529011  1628007 |  232764    2095    42642    20.4 |  0.250 % |
c |      2406 |  528936  1627752 |  256005    2243    52783    23.5 |  0.261 % |
c |      2632 |  528936  1627752 |  281605    2469    82991    33.6 |  0.261 % |
c |      2970 |  528936  1627752 |  309766    2807    95482    34.0 |  0.261 % |
c |      3477 |  528936  1627752 |  340742    3314   111024    33.5 |  0.261 % |
c ==============================================================================
c (current CPU-time: 239.598 s)
c ==============================================================================
c [1mFound solution: 88093023[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   22     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 2 7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      3731 |  534004  1640896 |  160201    3560   139550    39.2 |  0.261 % |
c   -- subsuming                       
c   -- var.elim.:  1000/10112          
c   -- var.elim.:  2000/10112          
c   -- var.elim.:  3000/10112          
c   -- var.elim.:  4000/10112          
c   -- var.elim.:  5000/10112          
c   -- var.elim.:  6000/10112          
c   -- var.elim.:  7000/10112          
c   -- var.elim.:  8000/10112          
c   -- var.elim.:  9000/10112          
c   -- var.elim.:  10000/10112          
c   -- var.elim.:  10112/10112          
c   -- var.elim.:  1000/6607          
c   -- var.elim.:  2000/6607          
c   -- var.elim.:  3000/6607          
c   -- var.elim.:  4000/6607          
c   -- var.elim.:  5000/6607          
c   -- var.elim.:  6000/6607          
c   -- var.elim.:  6607/6607          
c   -- var.elim.:  1000/1123          
c   -- var.elim.:  1123/1123          
c   -- var.elim.:  755/755          
c   -- subsuming                       
c   -- var.elim.:  210/210          
c   -- var.elim.:  123/123          
c |      3731 |  530967  1641834 |      --    3560       --      -- |     --   | -3035/943
c |      3731 |  530967  1641834 |  212386    3451    92879    26.9 |  0.261 % |
c |      3832 |  530967  1641834 |  233625    3552    96219    27.1 |  0.319 % |
c |      3982 |  530967  1641834 |  256988    3702   116482    31.5 |  0.319 % |
c ==============================================================================
c (current CPU-time: 294.608 s)
c ==============================================================================
c [1mFound solution: 84011948[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   21     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 2 7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4067 |  531952  1645845 |  159585    3787   123084    32.5 |  0.319 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2852          
c   -- var.elim.:  2000/2852          
c   -- var.elim.:  2852/2852          
c   -- var.elim.:  1000/2212          
c   -- var.elim.:  2000/2212          
c   -- var.elim.:  2212/2212          
c   -- var.elim.:  413/413          
c   -- var.elim.:  243/243          
c   -- subsuming                       
c   -- var.elim.:  556/556          
c   -- var.elim.:  239/239          
c |      4067 |  531384  1654920 |      --    3787       --      -- |     --   | -566/9080
c |      4067 |  531384  1654920 |  212553    3787   123084    32.5 |  0.319 % |
c |      4167 |  531384  1654920 |  233808    3887   128407    33.0 |  0.321 % |
c ==============================================================================
c (current CPU-time: 346.042 s)
c ==============================================================================
c [1mFound solution: 84003636[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   20     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 2 7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4298 |  531619  1657102 |  159485    4018   136579    34.0 |  0.321 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1926          
c   -- var.elim.:  1926/1926          
c   -- var.elim.:  1000/1776          
c   -- var.elim.:  1776/1776          
c   -- var.elim.:  401/401          
c   -- var.elim.:  528/528          
c |      4298 |  531472  1659068 |      --    4018       --      -- |     --   | -147/1967
c |      4298 |  531472  1659068 |  212588    4018   136579    34.0 |  0.321 % |
c |      4398 |  531213  1655259 |  233733    4116   138924    33.8 |  0.353 % |
c |      4548 |  531213  1655259 |  257107    4266   140116    32.8 |  0.353 % |
c |      4773 |  531213  1655259 |  282817    4491   141807    31.6 |  0.353 % |
c |      5110 |  530653  1651808 |  310771    4827   152227    31.5 |  0.404 % |
c |      5616 |  530653  1651808 |  341848    5333   156095    29.3 |  0.404 % |
c |      6376 |  530653  1651808 |  376033    6093   168588    27.7 |  0.404 % |
c |      7516 |  530488  1645352 |  413508    7231   184745    25.5 |  0.422 % |
c ==============================================================================
c (current CPU-time: 408.703 s)
c ==============================================================================
c [1mFound solution: 83987710[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   21     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 2 7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      7537 |  531097  1648403 |  159329    7246   184981    25.5 |  0.422 % |
c   -- subsuming                       
c   -- var.elim.:  1000/5174          
c   -- var.elim.:  2000/5174          
c   -- var.elim.:  3000/5174          
c   -- var.elim.:  4000/5174          
c   -- var.elim.:  5000/5174          
c   -- var.elim.:  5174/5174          
c   -- var.elim.:  1000/2829          
c   -- var.elim.:  2000/2829          
c   -- var.elim.:  2829/2829          
c   -- var.elim.:  269/269          
c   -- subsuming                       
c   -- var.elim.:  58/58          
c   -- var.elim.:  8/8          
c |      7537 |  530553  1665312 |      --    7246       --      -- |     --   | -540/16918
c |      7537 |  530553  1665312 |  212221    7206   165295    22.9 |  0.422 % |
c |      7637 |  530553  1665312 |  233443    7306   173194    23.7 |  0.431 % |
c |      7787 |  530553  1665312 |  256787    7456   174502    23.4 |  0.431 % |
c |      8012 |  530553  1665312 |  282466    7681   176456    23.0 |  0.431 % |
c |      8349 |  530553  1665312 |  310713    8018   181263    22.6 |  0.431 % |
c |      8855 |  530553  1665312 |  341784    8524   197935    23.2 |  0.431 % |
c |      9614 |  530385  1664144 |  375843    9280   211568    22.8 |  0.454 % |
c ==============================================================================
c (current CPU-time: 473.973 s)
c ==============================================================================
c [1mFound solution: 83946013[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   20     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 2 7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     10082 |  530192  1663893 |  159057    9742   243883    25.0 |  0.454 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2539          
c   -- var.elim.:  2000/2539          
c   -- var.elim.:  2539/2539          
c   -- var.elim.:  1000/3297          
c   -- var.elim.:  2000/3297          
c   -- var.elim.:  3000/3297          
c   -- var.elim.:  3297/3297          
c   -- var.elim.:  983/983          
c   -- var.elim.:  1000/1293          
c   -- var.elim.:  1293/1293          
c   -- subsuming                       
c   -- var.elim.:  141/141          
c |     10082 |  530077  1668467 |      --    9742       --      -- |     --   | -114/4577
c |     10082 |  530077  1668467 |  212030    9693   232836    24.0 |  0.454 % |
c |     10183 |  530077  1668467 |  233233    9794   235663    24.1 |  0.487 % |
c |     10334 |  530077  1668467 |  256557    9945   236626    23.8 |  0.487 % |
c |     10559 |  529879  1667155 |  282107   10168   238798    23.5 |  0.510 % |
c |     10896 |  529520  1665047 |  310108   10498   243990    23.2 |  0.550 % |
c ==============================================================================
c (current CPU-time: 530.886 s)
c ==============================================================================
c [1mFound solution: 83912882[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   20     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 2 7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     11101 |  528542  1662787 |  158562   10700   257827    24.1 |  0.550 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4898          
c   -- var.elim.:  2000/4898          
c   -- var.elim.:  3000/4898          
c   -- var.elim.:  4000/4898          
c   -- var.elim.:  4898/4898          
c   -- var.elim.:  1000/4356          
c   -- var.elim.:  2000/4356          
c   -- var.elim.:  3000/4356          
c   -- var.elim.:  4000/4356          
c   -- var.elim.:  4356/4356          
c   -- var.elim.:  723/723          
c   -- var.elim.:  196/196          
c   -- subsuming                       
c   -- var.elim.:  262/262          
c |     11101 |  528129  1668316 |      --   10700       --      -- |     --   | -408/5540
c |     11101 |  528129  1668316 |  211251   10569   242985    23.0 |  0.550 % |
c |     11202 |  528129  1668316 |  232376   10670   243498    22.8 |  0.715 % |
c |     11352 |  527890  1667441 |  255498   10818   248662    23.0 |  0.740 % |
c |     11578 |  527872  1667372 |  281039   11043   249848    22.6 |  0.741 % |
c |     11916 |  527872  1667372 |  309142   11381   263972    23.2 |  0.741 % |
c |     12422 |  527820  1667196 |  340023   11886   306219    25.8 |  0.749 % |
c |     13182 |  527671  1666200 |  373920   12645   325103    25.7 |  0.766 % |
c ==============================================================================
c (current CPU-time: 599.38 s)
c ==============================================================================
c [1mFound solution: 76818750[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:34402     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     13549 |  622180  1887892 |  186653   13012   344729    26.5 |  0.766 % |
c   -- subsuming                       
c   -- var.elim.:  1000/37723          
c   -- var.elim.:  2000/37723          
c   -- var.elim.:  3000/37723          
c   -- var.elim.:  4000/37723          
c   -- var.elim.:  5000/37723          
c   -- var.elim.:  6000/37723          
c   -- var.elim.:  7000/37723          
c   -- var.elim.:  8000/37723          
c   -- var.elim.:  9000/37723          
c   -- var.elim.:  10000/37723          
c   -- var.elim.:  11000/37723          
c   -- var.elim.:  12000/37723          
c   -- var.elim.:  13000/37723          
c   -- var.elim.:  14000/37723          
c   -- var.elim.:  15000/37723          
c   -- var.elim.:  16000/37723          
c   -- var.elim.:  17000/37723          
c   -- var.elim.:  18000/37723          
c   -- var.elim.:  19000/37723          
c   -- var.elim.:  20000/37723          
c   -- var.elim.:  21000/37723          
c   -- var.elim.:  22000/37723          
c   -- var.elim.:  23000/37723          
c   -- var.elim.:  24000/37723          
c   -- var.elim.:  25000/37723          
c   -- var.elim.:  26000/37723          
c   -- var.elim.:  27000/37723          
c   -- var.elim.:  28000/37723          
c   -- var.elim.:  29000/37723          
c   -- var.elim.:  30000/37723          
c   -- var.elim.:  31000/37723          
c   -- var.elim.:  32000/37723          
c   -- var.elim.:  33000/37723          
c   -- var.elim.:  34000/37723          
c   -- var.elim.:  35000/37723          
c   -- var.elim.:  36000/37723          
c   -- var.elim.:  37000/37723          
c   -- var.elim.:  37723/37723          
c   -- var.elim.:  1000/22092          
c   -- var.elim.:  2000/22092          
c   -- var.elim.:  3000/22092          
c   -- var.elim.:  4000/22092          
c   -- var.elim.:  5000/22092          
c   -- var.elim.:  6000/22092          
c   -- var.elim.:  7000/22092          
c   -- var.elim.:  8000/22092          
c   -- var.elim.:  9000/22092          
c   -- var.elim.:  10000/22092          
c   -- var.elim.:  11000/22092          
c   -- var.elim.:  12000/22092          
c   -- var.elim.:  13000/22092          
c   -- var.elim.:  14000/22092          
c   -- var.elim.:  15000/22092          
c   -- var.elim.:  16000/22092          
c   -- var.elim.:  17000/22092          
c   -- var.elim.:  18000/22092          
c   -- var.elim.:  19000/22092          
c   -- var.elim.:  20000/22092          
c   -- var.elim.:  21000/22092          
c   -- var.elim.:  22000/22092          
c   -- var.elim.:  22092/22092          
c   -- var.elim.:  101/101          
c   -- var.elim.:  48/48          
c   -- subsuming                       
c   -- var.elim.:  628/628          
c   -- var.elim.:  164/164          
c   -- var.elim.:  14/14          
c   -- var.elim.:  8/8          
c |     13549 |  611463  1930683 |      --   13012       --      -- |     --   | -9326/47885
c |     13549 |  611463  1930683 |  244585   12761   294508    23.1 |  0.766 % |
c |     13650 |  610673  1927463 |  268696   12854   311720    24.3 |  1.063 % |
c |     13800 |  610553  1927023 |  295507   13003   317240    24.4 |  1.072 % |
c |     14025 |  610372  1926316 |  324962   13220   321924    24.4 |  1.086 % |
c ==============================================================================
c (current CPU-time: 667.031 s)
c ==============================================================================
c [1mFound solution: 76162675[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   20     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     14175 |  613420  1935203 |  184025   13359   333031    24.9 |  1.086 % |
c   -- subsuming                       
c   -- var.elim.:  1000/8743          
c   -- var.elim.:  2000/8743          
c   -- var.elim.:  3000/8743          
c   -- var.elim.:  4000/8743          
c   -- var.elim.:  5000/8743          
c   -- var.elim.:  6000/8743          
c   -- var.elim.:  7000/8743          
c   -- var.elim.:  8000/8743          
c   -- var.elim.:  8743/8743          
c   -- var.elim.:  1000/6542          
c   -- var.elim.:  2000/6542          
c   -- var.elim.:  3000/6542          
c   -- var.elim.:  4000/6542          
c   -- var.elim.:  5000/6542          
c   -- var.elim.:  6000/6542          
c   -- var.elim.:  6542/6542          
c   -- var.elim.:  446/446          
c   -- var.elim.:  1000/1449          
c   -- var.elim.:  1449/1449          
c   -- subsuming                       
c   -- var.elim.:  421/421          
c   -- var.elim.:  43/43          
c |     14175 |  611585  1938033 |      --   13359       --      -- |     --   | -1826/2849
c |     14175 |  611585  1938033 |  244634   13198   308759    23.4 |  1.086 % |
c ==============================================================================
c (current CPU-time: 726.653 s)
c ==============================================================================
c [1mFound solution: 76076222[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   19     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     14246 |  611737  1939996 |  183521   13269   310901    23.4 |  1.086 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1837          
c   -- var.elim.:  1837/1837          
c   -- var.elim.:  1000/1712          
c   -- var.elim.:  1712/1712          
c   -- var.elim.:  894/894          
c   -- var.elim.:  891/891          
c |     14246 |  611615  1943634 |      --   13269       --      -- |     --   | -122/3639
c |     14246 |  611615  1943634 |  244646   13269   310901    23.4 |  1.086 % |
c |     14346 |  611615  1943634 |  269110   13369   312066    23.3 |  1.095 % |
c |     14496 |  611615  1943634 |  296021   13519   321636    23.8 |  1.095 % |
c |     14722 |  611104  1941248 |  325351   13743   335272    24.4 |  1.143 % |
c |     15059 |  611104  1941248 |  357886   14080   374093    26.6 |  1.143 % |
c |     15566 |  611104  1941248 |  393675   14587   417845    28.6 |  1.143 % |
c |     16325 |  610792  1939474 |  432822   15334   460104    30.0 |  1.174 % |
c ==============================================================================
c (current CPU-time: 800.26 s)
c ==============================================================================
c [1mFound solution: 76075590[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   18     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     16699 |  610924  1941231 |  183277   15708   515658    32.8 |  1.174 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4816          
c   -- var.elim.:  2000/4816          
c   -- var.elim.:  3000/4816          
c   -- var.elim.:  4000/4816          
c   -- var.elim.:  4816/4816          
c   -- var.elim.:  1000/4352          
c   -- var.elim.:  2000/4352          
c   -- var.elim.:  3000/4352          
c   -- var.elim.:  4000/4352          
c   -- var.elim.:  4352/4352          
c   -- var.elim.:  874/874          
c   -- var.elim.:  170/170          
c   -- subsuming                       
c   -- var.elim.:  45/45          
c |     16699 |  610552  1944111 |      --   15708       --      -- |     --   | -369/2887
c |     16699 |  610552  1944111 |  244220   15457   417519    27.0 |  1.174 % |
c |     16800 |  610552  1944111 |  268642   15558   429234    27.6 |  1.191 % |
c |     16950 |  610552  1944111 |  295507   15708   438751    27.9 |  1.191 % |
c |     17176 |  610552  1944111 |  325057   15934   444281    27.9 |  1.191 % |
c |     17513 |  610250  1938154 |  357386   16269   488114    30.0 |  1.223 % |
c |     18019 |  610250  1938154 |  393125   16775   494730    29.5 |  1.223 % |
c |     18779 |  610250  1938154 |  432438   17535   509791    29.1 |  1.223 % |
c |     19918 |  610131  1936630 |  475589   18654   584713    31.3 |  1.234 % |
c ==============================================================================
c (current CPU-time: 883.428 s)
c ==============================================================================
c [1mFound solution: 74571520[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   20     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     20167 |  610646  1939226 |  183193   18899   613056    32.4 |  1.234 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3907          
c   -- var.elim.:  2000/3907          
c   -- var.elim.:  3000/3907          
c   -- var.elim.:  3907/3907          
c   -- var.elim.:  1000/3845          
c   -- var.elim.:  2000/3845          
c   -- var.elim.:  3000/3845          
c   -- var.elim.:  3845/3845          
c   -- var.elim.:  505/505          
c   -- subsuming                       
c   -- var.elim.:  556/556          
c   -- var.elim.:  42/42          
c |     20167 |  610172  1952530 |      --   18899       --      -- |     --   | -471/13311
c |     20167 |  610172  1952530 |  244068   18696   505059    27.0 |  1.234 % |
c |     20267 |  610172  1952530 |  268475   18796   505626    26.9 |  1.251 % |
c |     20417 |  610172  1952530 |  295323   18946   526294    27.8 |  1.251 % |
c ==============================================================================
c (current CPU-time: 943.618 s)
c ==============================================================================
c [1mFound solution: 74509725[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   19     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     20498 |  610347  1954533 |  183104   19027   538803    28.3 |  1.251 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1808          
c   -- var.elim.:  1808/1808          
c   -- var.elim.:  1000/1702          
c   -- var.elim.:  1702/1702          
c   -- var.elim.:  1000/1023          
c   -- var.elim.:  1023/1023          
c   -- var.elim.:  1000/1270          
c   -- var.elim.:  1270/1270          
c   -- var.elim.:  969/969          
c   -- var.elim.:  1000/1506          
c   -- var.elim.:  1506/1506          
c |     20498 |  610206  1960051 |      --   19027       --      -- |     --   | -141/5519
c |     20498 |  610206  1960051 |  244082   19027   538803    28.3 |  1.251 % |
c |     20598 |  610073  1959526 |  268432   19126   539915    28.2 |  1.265 % |
c |     20749 |  609869  1958824 |  295176   19274   560211    29.1 |  1.288 % |
c |     20976 |  609869  1958824 |  324694   19501   577279    29.6 |  1.288 % |
c |     21313 |  609869  1958824 |  357163   19838   586450    29.6 |  1.288 % |
c |     21822 |  609809  1958363 |  392841   20346   595331    29.3 |  1.292 % |
c |     22582 |  609809  1958363 |  432125   21106   773135    36.6 |  1.292 % |
c ==============================================================================
c (current CPU-time: 1033.18 s)
c ==============================================================================
c [1mFound solution: 61237163[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:51939     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     23578 |  755451  2298754 |  226635   22096   912309    41.3 |  1.292 % |
c   -- subsuming                       
c   -- var.elim.:  1000/57553          
c   -- var.elim.:  2000/57553          
c   -- var.elim.:  3000/57553          
c   -- var.elim.:  4000/57553          
c   -- var.elim.:  5000/57553          
c   -- var.elim.:  6000/57553          
c   -- var.elim.:  7000/57553          
c   -- var.elim.:  8000/57553          
c   -- var.elim.:  9000/57553          
c   -- var.elim.:  10000/57553          
c   -- var.elim.:  11000/57553          
c   -- var.elim.:  12000/57553          
c   -- var.elim.:  13000/57553          
c   -- var.elim.:  14000/57553          
c   -- var.elim.:  15000/57553          
c   -- var.elim.:  16000/57553          
c   -- var.elim.:  17000/57553          
c   -- var.elim.:  18000/57553          
c   -- var.elim.:  19000/57553          
c   -- var.elim.:  20000/57553          
c   -- var.elim.:  21000/57553          
c   -- var.elim.:  22000/57553          
c   -- var.elim.:  23000/57553          
c   -- var.elim.:  24000/57553          
c   -- var.elim.:  25000/57553          
c   -- var.elim.:  26000/57553          
c   -- var.elim.:  27000/57553          
c   -- var.elim.:  28000/57553          
c   -- var.elim.:  29000/57553          
c   -- var.elim.:  30000/57553          
c   -- var.elim.:  31000/57553          
c   -- var.elim.:  32000/57553          
c   -- var.elim.:  33000/57553          
c   -- var.elim.:  34000/57553          
c   -- var.elim.:  35000/57553          
c   -- var.elim.:  36000/57553          
c   -- var.elim.:  37000/57553          
c   -- var.elim.:  38000/57553          
c   -- var.elim.:  39000/57553          
c   -- var.elim.:  40000/57553          
c   -- var.elim.:  41000/57553          
c   -- var.elim.:  42000/57553          
c   -- var.elim.:  43000/57553          
c   -- var.elim.:  44000/57553          
c   -- var.elim.:  45000/57553          
c   -- var.elim.:  46000/57553          
c   -- var.elim.:  47000/57553          
c   -- var.elim.:  48000/57553          
c   -- var.elim.:  49000/57553          
c   -- var.elim.:  50000/57553          
c   -- var.elim.:  51000/57553          
c   -- var.elim.:  52000/57553          
c   -- var.elim.:  53000/57553          
c   -- var.elim.:  54000/57553          
c   -- var.elim.:  55000/57553          
c   -- var.elim.:  56000/57553          
c   -- var.elim.:  57000/57553          
c   -- var.elim.:  57553/57553          
c   -- var.elim.:  1000/34023          
c   -- var.elim.:  2000/34023          
c   -- var.elim.:  3000/34023          
c   -- var.elim.:  4000/34023          
c   -- var.elim.:  5000/34023          
c   -- var.elim.:  6000/34023          
c   -- var.elim.:  7000/34023          
c   -- var.elim.:  8000/34023          
c   -- var.elim.:  9000/34023          
c   -- var.elim.:  10000/34023          
c   -- var.elim.:  11000/34023          
c   -- var.elim.:  12000/34023          
c   -- var.elim.:  13000/34023          
c   -- var.elim.:  14000/34023          
c   -- var.elim.:  15000/34023          
c   -- var.elim.:  16000/34023          
c   -- var.elim.:  17000/34023          
c   -- var.elim.:  18000/34023          
c   -- var.elim.:  19000/34023          
c   -- var.elim.:  20000/34023          
c   -- var.elim.:  21000/34023          
c   -- var.elim.:  22000/34023          
c   -- var.elim.:  23000/34023          
c   -- var.elim.:  24000/34023          
c   -- var.elim.:  25000/34023          
c   -- var.elim.:  26000/34023          
c   -- var.elim.:  27000/34023          
c   -- var.elim.:  28000/34023          
c   -- var.elim.:  29000/34023          
c   -- var.elim.:  30000/34023          
c   -- var.elim.:  31000/34023          
c   -- var.elim.:  32000/34023          
c   -- var.elim.:  33000/34023          
c   -- var.elim.:  34000/34023          
c   -- var.elim.:  34023/34023          
c   -- var.elim.:  277/277          
c   -- var.elim.:  483/483          
c   -- subsuming                       
c   -- var.elim.:  1000/1149          
c   -- var.elim.:  1149/1149          
c   -- var.elim.:  181/181          
c |     23578 |  736809  2344356 |      --   22096       --      -- |     --   | -14113/72015
c |     23578 |  736809  2344356 |  294723   20985   643962    30.7 |  1.292 % |
c ==============================================================================
c (current CPU-time: 1103.61 s)
c ==============================================================================
c [1mFound solution: 74505816[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:80369     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     23591 |  965078  2877391 |  289523   20998   644258    30.7 |  1.292 % |
c   -- subsuming                       
c   -- var.elim.:  1000/78566          
c   -- var.elim.:  2000/78566          
c   -- var.elim.:  3000/78566          
c   -- var.elim.:  4000/78566          
c   -- var.elim.:  5000/78566          
c   -- var.elim.:  6000/78566          
c   -- var.elim.:  7000/78566          
c   -- var.elim.:  8000/78566          
c   -- var.elim.:  9000/78566          
c   -- var.elim.:  10000/78566          
c   -- var.elim.:  11000/78566          
c   -- var.elim.:  12000/78566          
c   -- var.elim.:  13000/78566          
c   -- var.elim.:  14000/78566          
c   -- var.elim.:  15000/78566          
c   -- var.elim.:  16000/78566          
c   -- var.elim.:  17000/78566          
c   -- var.elim.:  18000/78566          
c   -- var.elim.:  19000/78566          
c   -- var.elim.:  20000/78566          
c   -- var.elim.:  21000/78566          
c   -- var.elim.:  22000/78566          
c   -- var.elim.:  23000/78566          
c   -- var.elim.:  24000/78566          
c   -- var.elim.:  25000/78566          
c   -- var.elim.:  26000/78566          
c   -- var.elim.:  27000/78566          
c   -- var.elim.:  28000/78566          
c   -- var.elim.:  29000/78566          
c   -- var.elim.:  30000/78566          
c   -- var.elim.:  31000/78566          
c   -- var.elim.:  32000/78566          
c   -- var.elim.:  33000/78566          
c   -- var.elim.:  34000/78566          
c   -- var.elim.:  35000/78566          
c   -- var.elim.:  36000/78566          
c   -- var.elim.:  37000/78566          
c   -- var.elim.:  38000/78566          
c   -- var.elim.:  39000/78566          
c   -- var.elim.:  40000/78566          
c   -- var.elim.:  41000/78566          
c   -- var.elim.:  42000/78566          
c   -- var.elim.:  43000/78566          
c   -- var.elim.:  44000/78566          
c   -- var.elim.:  45000/78566          
c   -- var.elim.:  46000/78566          
c   -- var.elim.:  47000/78566          
c   -- var.elim.:  48000/78566          
c   -- var.elim.:  49000/78566          
c   -- var.elim.:  50000/78566          
c   -- var.elim.:  51000/78566          
c   -- var.elim.:  52000/78566          
c   -- var.elim.:  53000/78566          
c   -- var.elim.:  54000/78566          
c   -- var.elim.:  55000/78566          
c   -- var.elim.:  56000/78566          
c   -- var.elim.:  57000/78566          
c   -- var.elim.:  58000/78566          
c   -- var.elim.:  59000/78566          
c   -- var.elim.:  60000/78566          
c   -- var.elim.:  61000/78566          
c   -- var.elim.:  62000/78566          
c   -- var.elim.:  63000/78566          
c   -- var.elim.:  64000/78566          
c   -- var.elim.:  65000/78566          
c   -- var.elim.:  66000/78566          
c   -- var.elim.:  67000/78566          
c   -- var.elim.:  68000/78566          
c   -- var.elim.:  69000/78566          
c   -- var.elim.:  70000/78566          
c   -- var.elim.:  71000/78566          
c   -- var.elim.:  72000/78566          
c   -- var.elim.:  73000/78566          
c   -- var.elim.:  74000/78566          
c   -- var.elim.:  75000/78566          
c   -- var.elim.:  76000/78566          
c   -- var.elim.:  77000/78566          
c   -- var.elim.:  78000/78566          
c   -- var.elim.:  78566/78566          
c   -- var.elim.:  1000/43761          
c   -- var.elim.:  2000/43761          
c   -- var.elim.:  3000/43761          
c   -- var.elim.:  4000/43761          
c   -- var.elim.:  5000/43761          
c   -- var.elim.:  6000/43761          
c   -- var.elim.:  7000/43761          
c   -- var.elim.:  8000/43761          
c   -- var.elim.:  9000/43761          
c   -- var.elim.:  10000/43761          
c   -- var.elim.:  11000/43761          
c   -- var.elim.:  12000/43761          
c   -- var.elim.:  13000/43761          
c   -- var.elim.:  14000/43761          
c   -- var.elim.:  15000/43761          
c   -- var.elim.:  16000/43761          
c   -- var.elim.:  17000/43761          
c   -- var.elim.:  18000/43761          
c   -- var.elim.:  19000/43761          
c   -- var.elim.:  20000/43761          
c   -- var.elim.:  21000/43761          
c   -- var.elim.:  22000/43761          
c   -- var.elim.:  23000/43761          
c   -- var.elim.:  24000/43761          
c   -- var.elim.:  25000/43761          
c   -- var.elim.:  26000/43761          
c   -- var.elim.:  27000/43761          
c   -- var.elim.:  28000/43761          
c   -- var.elim.:  29000/43761          
c   -- var.elim.:  30000/43761          
c   -- var.elim.:  31000/43761          
c   -- var.elim.:  32000/43761          
c   -- var.elim.:  33000/43761          
c   -- var.elim.:  34000/43761          
c   -- var.elim.:  35000/43761          
c   -- var.elim.:  36000/43761          
c   -- var.elim.:  37000/43761          
c   -- var.elim.:  38000/43761          
c   -- var.elim.:  39000/43761          
c   -- var.elim.:  40000/43761          
c   -- var.elim.:  41000/43761          
c   -- var.elim.:  42000/43761          
c   -- var.elim.:  43000/43761          
c   -- var.elim.:  43761/43761          
c   -- var.elim.:  850/850          
c   -- var.elim.:  93/93          
c   -- subsuming                       
c   -- var.elim.:  635/635          
c   -- var.elim.:  150/150          
c   -- var.elim.:  11/11          
c |     23591 |  944344  2982623 |      --   20998       --      -- |     --   | -20552/105664
c |     23591 |  944344  2982623 |  377737   20998   644258    30.7 |  1.292 % |
c |     23692 |  944340  2982597 |  415509   21098   647834    30.7 |  1.504 % |
c |     23845 |  942971  2976750 |  456397   21245   648531    30.5 |  1.587 % |
c |     24070 |  942971  2976750 |  502037   21470   665773    31.0 |  1.587 % |
c |     24409 |  942971  2976750 |  552241   21809   694376    31.8 |  1.587 % |
c |     24915 |  942971  2976750 |  607465   22315   726831    32.6 |  1.587 % |
c |     25674 |  942971  2976750 |  668212   23074   776108    33.6 |  1.587 % |
c ==============================================================================
c (current CPU-time: 1193.37 s)
c ==============================================================================
c [1mFound solution: 61234286[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> 
c *** TERMINATED ***
s SATISFIABLE
v -X0101_bit0 -X0102_bit0 -X0103_bit0 -X0104_bit0 -X0201_bit0 -X0202_bit0 -X0203_bit0 -X0204_bit0 -X0301_bit0 -X0302_bit0 -X0303_bit0 -X0304_bit0 -X0401_bit0 -X0402_bit0 -X0403_bit0 X0404_bit0 -X0501_bit0 -X0502_bit0 -X0503_bit0 -X0504_bit0 -X0601_bit0 -X0602_bit0 -X0603_bit0 -X0604_bit0 -X0701_bit0 -X0702_bit0 -X0703_bit0 X0704_bit0 X0801_bit0 -X0802_bit0 -X0803_bit0 -X0804_bit0 -X0901_bit0 -X0902_bit0 -X0903_bit0 -X0904_bit0 -X1001_bit0 -X1002_bit0 -X1003_bit0 -X1004_bit0 -X1101_bit0 -X1102_bit0 -X1103_bit0 X1104_bit0 X1201_bit0 -X1202_bit0 -X1203_bit0 -X1204_bit0 -X1301_bit0 -X1302_bit0 -X1303_bit0 -X1304_bit0 -X1401_bit0 -X1402_bit0 -X1403_bit0 -X1404_bit0 X1501_bit0 -X1502_bit0 -X1503_bit0 -X1504_bit0 -X1601_bit0 -X1602_bit0 -X1603_bit0 -X1604_bit0 -X1701_bit0 -X1702_bit0 -X1703_bit0 -X1704_bit0 -X1801_bit0 -X1802_bit0 -X1803_bit0 -X1804_bit0 -X1901_bit0 -X1902_bit0 -X1903_bit0 -X1904_bit0 -X2001_bit0 -X2002_bit0 -X2003_bit0 -X2004_bit0 -X2101_bit0 -X2102_bit0 -X2103_bit0 -X2104_bit0 -X2105_bit0 -X2201_bit0 -X2202_bit0 -X2203_bit0 -X2204_bit0 -X2205_bit0 -X2301_bit0 -X2302_bit0 -X2303_bit0 -X2304_bit0 -X2305_bit0 -X2401_bit0 -X2402_bit0 -X2403_bit0 -X2404_bit0 -X2405_bit0 -X2501_bit0 -X2502_bit0 -X2503_bit0 -X2504_bit0 -X2601_bit0 -X2603_bit0 -X2604_bit0 -X2701_bit0 -X2702_bit0 -X2703_bit0 -X2704_bit0 -X2801_bit0 -X2802_bit0 -X2803_bit0 -X2804_bit0 -X2901_bit0 -X2902_bit0 -X2903_bit0 -X2904_bit0 -X3001_bit0 -X3002_bit0 -X3003_bit0 -X3004_bit0 X3101_bit0 -X3102_bit0 -X3103_bit0 -X3104_bit0 -X3201_bit0 -X3202_bit0 -X3203_bit0 -X3204_bit0 -X3301_bit0 -X3302_bit0 -X3303_bit0 -X3304_bit0 -X3401_bit0 -X3402_bit0 -X3403_bit0 -X3404_bit0 -X3501_bit0 -X3502_bit0 -X3503_bit0 -X3504_bit0 -X3601_bit0 -X3602_bit0 -X3603_bit0 -X3604_bit0 -X3701_bit0 -X3702_bit0 -X3703_bit0 X3704_bit0 -X3801_bit0 -X3802_bit0 -X3803_bit0 -X3804_bit0 -X3901_bit0 -X3902_bit0 -X3903_bit0 X3904_bit0 -X4001_bit0 -X4002_bit0 -X4003_bit0 -X4004_bit0 -X4101_bit0 -X4102_bit0 -X4103_bit0 -X4104_bit0 -X4201_bit0 -X4202_bit0 -X4203_bit0 -X4204_bit0 -X4301_bit0 -X4302_bit0 -X4303_bit0 -X4304_bit0 -X4401_bit0 -X4402_bit0 -X4403_bit0 -X4404_bit0 X4501_bit0 -X4502_bit0 -X4503_bit0 -X4504_bit0 -X4505_bit0 -X4601_bit0 -X4602_bit0 -X4603_bit0 -X4604_bit0 -X4605_bit0 -X4701_bit0 -X4702_bit0 -X4703_bit0 -X4704_bit0 -X4705_bit0 -X4801_bit0 -X4802_bit0 -X4803_bit0 X4804_bit0 -X4805_bit0 -X4901_bit0 -X4902_bit0 -X4903_bit0 -X4904_bit0 X4905_bit0 -X5001_bit0 -X5002_bit0 -X5003_bit0 -X5004_bit0 -X5005_bit0 -X5101_bit0 X5102_bit0 -X5103_bit0 -X5104_bit0 X5105_bit0 -X5201_bit0 -X5202_bit0 -X5203_bit0 -X5204_bit0 X5205_bit0 -X0001AN_bit0 -X0102AN_bit0 X0202AN_bit0 -X0302AN_bit0 -X0003AN_bit0 -X0005AN_bit0 X0006AN_bit0 X0007AN_bit0 X0010AN_bit0 X0111AN_bit0 X0211AN_bit0 -X0311AN_bit0 -X0012AN_bit0 -X0113AN_bit0 X0213AN_bit0 -X0114AN_bit0 X0214AN_bit0 -X0115AN_bit0 -X0215AN_bit0 -X0315AN_bit0 -X0016AN_bit0 -X0117AN_bit0 -X0217AN_bit0 -X0317AN_bit0 -X0019AN_bit0 X0020AN_bit0 -X0121AN_bit0 -X0221AN_bit0 X0321AN_bit0 -X0122AN_bit0 -X0222AN_bit0 -X0322AN_bit0 -X0023AN_bit0 X0024AN_bit0 -X0025AN_bit0 -X0026AN_bit0 X0028AN_bit0 #### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.94 0.90 2/55 14963
Raw data (stat): 14963 (runsolver) D 14962 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 424196043 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 3225161850 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.88 0.94 0.90 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 1245 0 0 0 997 1 0 0 25 0 1 0 424196043 5865472 1012 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1432 1012 603 41 0 1391 0
vsize: 5728
[startup+20.0007 s]
Raw data (loadavg): 0.89 0.94 0.90 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 1245 0 0 0 1997 1 0 0 25 0 1 0 424196043 5865472 1012 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1432 1012 603 41 0 1391 0
vsize: 5728
[startup+30.0004 s]
Raw data (loadavg): 0.91 0.94 0.90 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 1245 0 0 0 2997 1 0 0 25 0 1 0 424196043 5865472 1012 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1432 1012 603 41 0 1391 0
vsize: 5728
[startup+40.0001 s]
Raw data (loadavg): 0.92 0.94 0.90 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 1245 0 0 0 3998 1 0 0 25 0 1 0 424196043 5865472 1012 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1432 1012 603 41 0 1391 0
vsize: 5728
[startup+49.9997 s]
Raw data (loadavg): 0.93 0.95 0.90 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 18372 0 0 0 4952 47 0 0 25 0 1 0 424196043 76308480 17288 4294967295 134512640 134672761 3221224544 3221222992 134606977 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18630 17288 603 41 0 18589 0
vsize: 74520
[startup+60 s]
Raw data (loadavg): 0.94 0.95 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 18481 0 0 0 5903 68 0 0 25 0 1 0 424196043 76308480 17285 4294967295 134512640 134672761 3221224544 3221222992 134643871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18630 17285 603 41 0 18589 0
vsize: 74520
[startup+70.0002 s]
Raw data (loadavg): 0.95 0.95 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 23212 0 0 0 6889 82 0 0 25 0 1 0 424196043 76759040 17425 4294967295 134512640 134672761 3221224544 3221221520 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18740 17425 603 41 0 18699 0
vsize: 74960
[startup+79.9999 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 23212 0 0 0 7889 82 0 0 25 0 1 0 424196043 76759040 17425 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18740 17425 603 41 0 18699 0
vsize: 74960
[startup+90.0006 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 23212 0 0 0 8889 82 0 0 25 0 1 0 424196043 76759040 17425 4294967295 134512640 134672761 3221224544 3221221808 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18740 17425 603 41 0 18699 0
vsize: 74960
[startup+100 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 23212 0 0 0 9889 82 0 0 25 0 1 0 424196043 76759040 17425 4294967295 134512640 134672761 3221224544 3221222240 134597012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18740 17425 603 41 0 18699 0
vsize: 74960
[startup+110 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 23212 0 0 0 10889 82 0 0 25 0 1 0 424196043 76759040 17425 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18740 17425 603 41 0 18699 0
vsize: 74960
[startup+120 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 28174 0 0 0 11872 99 0 0 25 0 1 0 424196043 76832768 17486 4294967295 134512640 134672761 3221224544 3221221664 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18758 17486 603 41 0 18717 0
vsize: 75032
[startup+129.999 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 28174 0 0 0 12872 99 0 0 25 0 1 0 424196043 76832768 17486 4294967295 134512640 134672761 3221224544 3221221664 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18758 17486 603 41 0 18717 0
vsize: 75032
[startup+140 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 28174 0 0 0 13873 99 0 0 25 0 1 0 424196043 76832768 17486 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18758 17486 603 41 0 18717 0
vsize: 75032
[startup+150 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 28174 0 0 0 14873 99 0 0 25 0 1 0 424196043 76832768 17486 4294967295 134512640 134672761 3221224544 3221221920 134522354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18758 17486 603 41 0 18717 0
vsize: 75032
[startup+159.999 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 29660 0 0 0 15870 102 0 0 25 0 1 0 424196043 80162816 18234 4294967295 134512640 134672761 3221224544 3221223088 134621083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19571 18234 603 41 0 19530 0
vsize: 78284
[startup+170 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 33054 0 0 0 16857 115 0 0 25 0 1 0 424196043 77115392 17539 4294967295 134512640 134672761 3221224544 3221223736 1075349878 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18827 17539 603 41 0 18786 0
vsize: 75308
[startup+180.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 33179 0 0 0 17856 116 0 0 25 0 1 0 424196043 77115392 17539 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18827 17539 603 41 0 18786 0
vsize: 75308
[startup+190.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 33179 0 0 0 18856 116 0 0 25 0 1 0 424196043 77115392 17539 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18827 17539 603 41 0 18786 0
vsize: 75308
[startup+200.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 33179 0 0 0 19856 116 0 0 25 0 1 0 424196043 77115392 17539 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18827 17539 603 41 0 18786 0
vsize: 75308
[startup+210.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 33179 0 0 0 20856 116 0 0 25 0 1 0 424196043 77115392 17539 4294967295 134512640 134672761 3221224544 3221222384 134597191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18827 17539 603 41 0 18786 0
vsize: 75308
[startup+220.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 44412 0 0 0 21823 149 0 0 25 0 1 0 424196043 124719104 26693 4294967295 134512640 134672761 3221224544 3221222880 134633657 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30449 26693 603 41 0 30408 0
vsize: 121796
[startup+230 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 45916 0 0 0 22784 160 0 0 25 0 1 0 424196043 124162048 26601 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30313 26601 603 41 0 30272 0
vsize: 121252
[startup+240.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 45964 0 0 0 23784 160 0 0 25 0 1 0 424196043 124424192 26649 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30377 26649 603 41 0 30336 0
vsize: 121508
[startup+250.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 52052 0 0 0 24764 180 0 0 25 0 1 0 424196043 125145088 26853 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30553 26853 603 41 0 30512 0
vsize: 122212
[startup+260.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 52052 0 0 0 25764 180 0 0 25 0 1 0 424196043 125145088 26853 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30553 26853 603 41 0 30512 0
vsize: 122212
[startup+270.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 52052 0 0 0 26764 180 0 0 25 0 1 0 424196043 125145088 26853 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30553 26853 603 41 0 30512 0
vsize: 122212
[startup+280 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 52052 0 0 0 27764 180 0 0 25 0 1 0 424196043 125145088 26853 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30553 26853 603 41 0 30512 0
vsize: 122212
[startup+290 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 54503 0 0 0 28758 187 0 0 25 0 1 0 424196043 133136384 28119 4294967295 134512640 134672761 3221224544 3221223088 134621098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32504 28119 603 41 0 32463 0
vsize: 130016
[startup+300 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 60757 0 0 0 29736 209 0 0 25 0 1 0 424196043 125231104 26961 4294967295 134512640 134672761 3221224544 3221221808 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30574 26961 603 41 0 30533 0
vsize: 122296
[startup+309.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 60757 0 0 0 30736 209 0 0 25 0 1 0 424196043 125231104 26961 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30574 26961 603 41 0 30533 0
vsize: 122296
[startup+319.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 60757 0 0 0 31736 209 0 0 25 0 1 0 424196043 125231104 26961 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30574 26961 603 41 0 30533 0
vsize: 122296
[startup+329.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 60757 0 0 0 32737 209 0 0 25 0 1 0 424196043 125231104 26961 4294967295 134512640 134672761 3221224544 3221222816 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30574 26961 603 41 0 30533 0
vsize: 122296
[startup+339.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 60757 0 0 0 33737 209 0 0 25 0 1 0 424196043 125231104 26961 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30574 26961 603 41 0 30533 0
vsize: 122296
[startup+349.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 68454 0 0 0 34716 229 0 0 25 0 1 0 424196043 154116096 32135 4294967295 134512640 134672761 3221224544 3221222880 134603769 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37626 32135 603 41 0 37585 0
vsize: 150504
[startup+359.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 69341 0 0 0 35711 235 0 0 25 0 1 0 424196043 125497344 26994 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30639 26994 603 41 0 30598 0
vsize: 122556
[startup+369.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 69341 0 0 0 36711 235 0 0 25 0 1 0 424196043 125497344 26994 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30639 26994 603 41 0 30598 0
vsize: 122556
[startup+379.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 69341 0 0 0 37710 235 0 0 25 0 1 0 424196043 125497344 26994 4294967295 134512640 134672761 3221224544 3221222672 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30639 26994 603 41 0 30598 0
vsize: 122556
[startup+389.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 69341 0 0 0 38711 235 0 0 25 0 1 0 424196043 125497344 26994 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30639 26994 603 41 0 30598 0
vsize: 122556
[startup+399.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 70513 0 0 0 39708 238 0 0 25 0 1 0 424196043 125497344 26997 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30639 26997 603 41 0 30598 0
vsize: 122556
[startup+409.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 70513 0 0 0 40708 238 0 0 25 0 1 0 424196043 125497344 26997 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30639 26997 603 41 0 30598 0
vsize: 122556
[startup+419.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 76864 0 0 0 41688 258 0 0 25 0 1 0 424196043 125530112 27005 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30647 27005 603 41 0 30606 0
vsize: 122588
[startup+429.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 76864 0 0 0 42688 258 0 0 25 0 1 0 424196043 125530112 27005 4294967295 134512640 134672761 3221224544 3221222384 134597176 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30647 27005 603 41 0 30606 0
vsize: 122588
[startup+439.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 76864 0 0 0 43688 259 0 0 25 0 1 0 424196043 125530112 27005 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30647 27005 603 41 0 30606 0
vsize: 122588
[startup+449.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 76864 0 0 0 44688 259 0 0 25 0 1 0 424196043 125530112 27005 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30647 27005 603 41 0 30606 0
vsize: 122588
[startup+459.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 79220 0 0 0 45682 264 0 0 25 0 1 0 424196043 132333568 28186 4294967295 134512640 134672761 3221224544 3221223088 134621095 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32308 28186 603 41 0 32267 0
vsize: 129232
[startup+469.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 79220 0 0 0 46682 265 0 0 25 0 1 0 424196043 125530112 27013 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30647 27013 603 41 0 30606 0
vsize: 122588
[startup+480.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 85593 0 0 0 47660 289 0 0 25 0 1 0 424196043 125562880 27021 4294967295 134512640 134672761 3221224544 3221221232 134597176 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30655 27021 603 41 0 30614 0
vsize: 122620
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 85593 0 0 0 48660 289 0 0 25 0 1 0 424196043 125562880 27021 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30655 27021 603 41 0 30614 0
vsize: 122620
[startup+500.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 85593 0 0 0 49660 289 0 0 25 0 1 0 424196043 125562880 27021 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30655 27021 603 41 0 30614 0
vsize: 122620
[startup+510.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 85593 0 0 0 50660 289 0 0 25 0 1 0 424196043 125562880 27021 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30655 27021 603 41 0 30614 0
vsize: 122620
[startup+520.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 85593 0 0 0 51660 289 0 0 25 0 1 0 424196043 125562880 27021 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30655 27021 603 41 0 30614 0
vsize: 122620
[startup+530.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 87939 0 0 0 52653 297 0 0 25 0 1 0 424196043 125562880 27021 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30655 27021 603 41 0 30614 0
vsize: 122620
[startup+540.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 94243 0 0 0 53632 318 0 0 25 0 1 0 424196043 125816832 27082 4294967295 134512640 134672761 3221224544 3221221832 1075351251 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30717 27082 603 41 0 30676 0
vsize: 122868
[startup+550.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 94243 0 0 0 54632 318 0 0 25 0 1 0 424196043 125816832 27082 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30717 27082 603 41 0 30676 0
vsize: 122868
[startup+560.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 94243 0 0 0 55632 318 0 0 25 0 1 0 424196043 125816832 27082 4294967295 134512640 134672761 3221224544 3221222384 134597212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30717 27082 603 41 0 30676 0
vsize: 122868
[startup+570.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 94243 0 0 0 56632 318 0 0 25 0 1 0 424196043 125816832 27082 4294967295 134512640 134672761 3221224544 3221221808 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30717 27082 603 41 0 30676 0
vsize: 122868
[startup+580.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 95424 0 0 0 57630 321 0 0 25 0 1 0 424196043 133562368 28263 4294967295 134512640 134672761 3221224544 3221223088 134621211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32608 28263 603 41 0 32567 0
vsize: 130432
[startup+590.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 96597 0 0 0 58626 325 0 0 25 0 1 0 424196043 125816832 27090 4294967295 134512640 134672761 3221224544 3221223728 134615679 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30717 27090 603 41 0 30676 0
vsize: 122868
[startup+600.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 96599 0 0 0 59626 325 0 0 25 0 1 0 424196043 125947904 27092 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30749 27092 603 41 0 30708 0
vsize: 122996
[startup+610.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 103091 0 0 0 60604 347 0 0 25 0 1 0 424196043 126017536 27140 4294967295 134512640 134672761 3221224544 3221222240 134597212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30766 27140 603 41 0 30725 0
vsize: 123064
[startup+620.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 103091 0 0 0 61604 347 0 0 25 0 1 0 424196043 126017536 27140 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30766 27140 603 41 0 30725 0
vsize: 123064
[startup+630.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 103091 0 0 0 62604 347 0 0 25 0 1 0 424196043 126017536 27140 4294967295 134512640 134672761 3221224544 3221221808 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30766 27140 603 41 0 30725 0
vsize: 123064
[startup+640.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 103091 0 0 0 63604 347 0 0 25 0 1 0 424196043 126017536 27140 4294967295 134512640 134672761 3221224544 3221221952 134597184 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30766 27140 603 41 0 30725 0
vsize: 123064
[startup+650.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 108010 0 0 0 64593 358 0 0 25 0 1 0 424196043 144629760 32059 4294967295 134512640 134672761 3221224544 3221223088 134621088 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35310 32059 603 41 0 35269 0
vsize: 141240
[startup+660.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 109676 0 0 0 65582 369 0 0 25 0 1 0 424196043 144158720 32063 4294967295 134512640 134672761 3221224544 3221223068 134642908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35195 32063 603 41 0 35154 0
vsize: 140780
[startup+670.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 109676 0 0 0 66581 370 0 0 25 0 1 0 424196043 135806976 30595 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33156 30595 603 41 0 33115 0
vsize: 132624
[startup+680.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 116859 0 0 0 67556 395 0 0 25 0 1 0 424196043 138051584 31178 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33704 31178 603 41 0 33663 0
vsize: 134816
[startup+690.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 116859 0 0 0 68556 395 0 0 25 0 1 0 424196043 138051584 31178 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33704 31178 603 41 0 33663 0
vsize: 134816
[startup+700.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 116859 0 0 0 69556 395 0 0 25 0 1 0 424196043 138051584 31178 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33704 31178 603 41 0 33663 0
vsize: 134816
[startup+710.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 116859 0 0 0 70556 395 0 0 25 0 1 0 424196043 138051584 31178 4294967295 134512640 134672761 3221224544 3221221808 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33704 31178 603 41 0 33663 0
vsize: 134816
[startup+720.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 118116 0 0 0 71553 398 0 0 25 0 1 0 424196043 144621568 32435 4294967295 134512640 134672761 3221224544 3221223088 134621186 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35308 32435 603 41 0 35267 0
vsize: 141232
[startup+730.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 119331 0 0 0 72550 402 0 0 25 0 1 0 424196043 138051584 31219 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33704 31219 603 41 0 33663 0
vsize: 134816
[startup+740.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 126039 0 0 0 73529 423 0 0 25 0 1 0 424196043 138059776 31222 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33706 31222 603 41 0 33665 0
vsize: 134824
[startup+750.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 126039 0 0 0 74529 423 0 0 25 0 1 0 424196043 138059776 31222 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33706 31222 603 41 0 33665 0
vsize: 134824
[startup+760.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 126039 0 0 0 75528 424 0 0 25 0 1 0 424196043 138059776 31222 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33706 31222 603 41 0 33665 0
vsize: 134824
[startup+770.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 126039 0 0 0 76528 424 0 0 25 0 1 0 424196043 138059776 31222 4294967295 134512640 134672761 3221224544 3221222096 134597256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33706 31222 603 41 0 33665 0
vsize: 134824
[startup+780.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 127255 0 0 0 77525 427 0 0 25 0 1 0 424196043 138059776 31226 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33706 31226 603 41 0 33665 0
vsize: 134824
[startup+790.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 127255 0 0 0 78525 427 0 0 25 0 1 0 424196043 138059776 31226 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33706 31226 603 41 0 33665 0
vsize: 134824
[startup+800.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 127255 0 0 0 79525 427 0 0 25 0 1 0 424196043 138059776 31226 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33706 31226 603 41 0 33665 0
vsize: 134824
[startup+810.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 134230 0 0 0 80498 455 0 0 25 0 1 0 424196043 141197312 31983 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34472 31983 603 41 0 34431 0
vsize: 137888
[startup+820.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 134230 0 0 0 81498 455 0 0 25 0 1 0 424196043 141197312 31983 4294967295 134512640 134672761 3221224544 3221221232 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34472 31983 603 41 0 34431 0
vsize: 137888
[startup+830.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 134230 0 0 0 82498 455 0 0 25 0 1 0 424196043 141197312 31983 4294967295 134512640 134672761 3221224544 3221221808 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34472 31983 603 41 0 34431 0
vsize: 137888
[startup+840.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 134230 0 0 0 83498 455 0 0 25 0 1 0 424196043 141197312 31983 4294967295 134512640 134672761 3221224544 3221222528 134597225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34472 31983 603 41 0 34431 0
vsize: 137888
[startup+850.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 134230 0 0 0 84498 455 0 0 25 0 1 0 424196043 141197312 31983 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34472 31983 603 41 0 34431 0
vsize: 137888
[startup+860.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 136659 0 0 0 85493 460 0 0 25 0 1 0 424196043 148246528 33198 4294967295 134512640 134672761 3221224544 3221223088 134621081 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36193 33198 603 41 0 36152 0
vsize: 144772
[startup+870.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 136671 0 0 0 86493 461 0 0 25 0 1 0 424196043 141197312 31995 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34472 31995 603 41 0 34431 0
vsize: 137888
[startup+880.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 136671 0 0 0 87492 461 0 0 25 0 1 0 424196043 141197312 31995 4294967295 134512640 134672761 3221224544 3221223728 134615689 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34472 31995 603 41 0 34431 0
vsize: 137888
[startup+890.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 142105 0 0 0 88478 476 0 0 25 0 1 0 424196043 167456768 37429 4294967295 134512640 134672761 3221224544 3221222964 1075326149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40883 37429 603 41 0 40842 0
vsize: 163532
[startup+900.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 143156 0 0 0 89470 484 0 0 25 0 1 0 424196043 141209600 32007 4294967295 134512640 134672761 3221224544 3221221952 134597215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34475 32007 603 41 0 34434 0
vsize: 137900
[startup+910.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 143156 0 0 0 90470 484 0 0 25 0 1 0 424196043 141209600 32007 4294967295 134512640 134672761 3221224544 3221222240 134597203 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34475 32007 603 41 0 34434 0
vsize: 137900
[startup+920.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 143156 0 0 0 91470 484 0 0 25 0 1 0 424196043 141209600 32007 4294967295 134512640 134672761 3221224544 3221222672 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34475 32007 603 41 0 34434 0
vsize: 137900
[startup+930.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 143156 0 0 0 92470 484 0 0 25 0 1 0 424196043 141209600 32007 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34475 32007 603 41 0 34434 0
vsize: 137900
[startup+940.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 144992 0 0 0 93466 489 0 0 25 0 1 0 424196043 144007168 32627 4294967295 134512640 134672761 3221224544 3221223088 134621211 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35158 32627 603 41 0 35117 0
vsize: 140632
[startup+950.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 150346 0 0 0 94451 503 0 0 25 0 1 0 424196043 166805504 37373 4294967295 134512640 134672761 3221224544 3221222988 1075278878 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40724 37373 603 41 0 40683 0
vsize: 162896
[startup+960.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 151379 0 0 0 95439 516 0 0 25 0 1 0 424196043 141213696 32020 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34476 32020 603 41 0 34435 0
vsize: 137904
[startup+970.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 151379 0 0 0 96439 516 0 0 25 0 1 0 424196043 141213696 32020 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34476 32020 603 41 0 34435 0
vsize: 137904
[startup+980.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 151379 0 0 0 97439 516 0 0 25 0 1 0 424196043 141213696 32020 4294967295 134512640 134672761 3221224544 3221222672 134597169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34476 32020 603 41 0 34435 0
vsize: 137904
[startup+990.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 151379 0 0 0 98439 516 0 0 25 0 1 0 424196043 141213696 32020 4294967295 134512640 134672761 3221224544 3221222096 134597218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34476 32020 603 41 0 34435 0
vsize: 137904
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 152597 0 0 0 99436 519 0 0 25 0 1 0 424196043 141213696 32022 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34476 32022 603 41 0 34435 0
vsize: 137904
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 152597 0 0 0 100436 519 0 0 25 0 1 0 424196043 141213696 32022 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34476 32022 603 41 0 34435 0
vsize: 137904
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 152597 0 0 0 101436 519 0 0 25 0 1 0 424196043 141213696 32022 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34476 32022 603 41 0 34435 0
vsize: 137904
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 152597 0 0 0 102436 520 0 0 25 0 1 0 424196043 141213696 32022 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34476 32022 603 41 0 34435 0
vsize: 137904
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 158219 0 0 0 103422 533 0 0 25 0 1 0 424196043 168398848 37644 4294967295 134512640 134672761 3221224544 3221222732 1075346564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41113 37644 603 41 0 41072 0
vsize: 164452
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 159329 0 0 0 104412 544 0 0 25 0 1 0 424196043 141213696 32022 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34476 32022 603 41 0 34435 0
vsize: 137904
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 159329 0 0 0 105412 544 0 0 25 0 1 0 424196043 141213696 32022 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34476 32022 603 41 0 34435 0
vsize: 137904
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 159329 0 0 0 106412 544 0 0 25 0 1 0 424196043 141213696 32022 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34476 32022 603 41 0 34435 0
vsize: 137904
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 159329 0 0 0 107412 544 0 0 25 0 1 0 424196043 141213696 32022 4294967295 134512640 134672761 3221224544 3221221952 134597195 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34476 32022 603 41 0 34435 0
vsize: 137904
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 166720 0 0 0 108396 561 0 0 25 0 1 0 424196043 195682304 39409 4294967295 134512640 134672761 3221224544 3221223088 134621211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47774 39409 603 41 0 47733 0
vsize: 191096
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 168811 0 0 0 109379 577 0 0 25 0 1 0 424196043 197763072 39444 4294967295 134512640 134672761 3221224544 3221223088 134621049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48282 39444 603 41 0 48241 0
vsize: 193128
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 170785 0 0 0 110375 581 0 0 25 0 1 0 424196043 201416704 39604 4294967295 134512640 134672761 3221224544 3221222880 134605216 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49174 39604 603 41 0 49133 0
vsize: 196696
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 177431 0 0 0 111350 607 0 0 25 0 1 0 424196043 187080704 37723 4294967295 134512640 134672761 3221224544 3221222208 134522368 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45674 37723 603 41 0 45633 0
vsize: 182696
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 177431 0 0 0 112349 607 0 0 25 0 1 0 424196043 187080704 37723 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45674 37723 603 41 0 45633 0
vsize: 182696
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 177431 0 0 0 113350 607 0 0 25 0 1 0 424196043 187080704 37723 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45674 37723 603 41 0 45633 0
vsize: 182696
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 177431 0 0 0 114350 607 0 0 25 0 1 0 424196043 187080704 37723 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45674 37723 603 41 0 45633 0
vsize: 182696
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 190690 0 0 0 115312 645 0 0 25 0 1 0 424196043 220430336 47725 4294967295 134512640 134672761 3221224544 3221222992 134607190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53816 47725 603 41 0 53775 0
vsize: 215264
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 193079 0 0 0 116274 657 0 0 25 0 1 0 424196043 219869184 47635 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53679 47635 603 41 0 53638 0
vsize: 214716
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 193124 0 0 0 117274 657 0 0 25 0 1 0 424196043 219869184 47680 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53679 47680 603 41 0 53638 0
vsize: 214716
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 193140 0 0 0 118274 657 0 0 25 0 1 0 424196043 220000256 47696 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53711 47696 603 41 0 53670 0
vsize: 214844
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 193291 0 0 0 119274 657 0 0 25 0 1 0 424196043 220520448 47847 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53838 47847 603 41 0 53797 0
vsize: 215352
[startup+1210.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14963
Raw data (stat): 14963 (minisat+) R 14962 30927 30926 0 -1 0 204749 0 0 0 120231 699 0 0 25 0 1 0 424196043 221282304 48066 4294967295 134512640 134672761 3221224544 3221222240 134597195 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54024 48066 603 41 0 53983 0
vsize: 216096
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1210.15 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 14963
Raw data (stat): 14963 (minisat+) Z 14962 30927 30926 0 -1 12 204750 0 0 0 120232 712 0 0 25 0 1 0 424196043 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): 1210.14
CPU time (s): 1209.45
CPU user time (s): 1202.32
CPU system time (s): 7.12792
CPU usage (%): 99.9424
Max. virtual memory (Kb): 216096
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####