PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-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.335948
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 22057

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        335016 kB
Buffers:         26744 kB
Cached:         649104 kB
SwapCached:        548 kB
Active:          92280 kB
Inactive:       585620 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        334764 kB
SwapTotal:     2097136 kB
SwapFree:      2095732 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5104 kB
Slab:            16084 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 02:22:19 (client local time) WITH STATUS 10 IN 1209.64 SECONDS
stats: 12153 7 1209.64 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.6539 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: 65.0811 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: 113.096 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.54 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: 240.02 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: 295.202 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.808 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: 409.668 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: 475.219 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: 532.326 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: 601.298 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: 669.045 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: 728.554 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: 802.502 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: 886.61 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: 947.015 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: 1037.82 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: 1108.35 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: 1199.72 s)
c 
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 -X0029AN_bit0 -Y0001S_bit0 -Y0102S_bit0 -Y0202S_bit0 -Y0302S_bit0 -Y0003S_bit0 -Y0004S_bit0 Y0005S_bit0 -Y0001AN_bit0 -Y0102AN_bit0 -Y0202AN_bit0 Y0302AN_bit0 -Y0003AN_bit0 -Y0005AN_bit0 Y0007AN_bit0 Y0111AN_bit0 -Y021#### 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.90 0.99 0.92 2/54 20201
Raw data (stat): 20201 (runsolver) R 20200 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 549963304 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.92 0.99 0.92 2/54 20201
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 1245 0 0 0 995 3 0 0 25 0 1 0 549963304 5865472 1012 4294967295 134512640 134672761 3221224544 3221222240 134597203 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1432 1012 603 41 0 1391 0
vsize: 5728
[startup+20.0012 s]
Raw data (loadavg): 0.93 0.99 0.92 2/54 20201
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 1245 0 0 0 1995 4 0 0 25 0 1 0 549963304 5865472 1012 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1432 1012 603 41 0 1391 0
vsize: 5728
[startup+30.0008 s]
Raw data (loadavg): 0.94 0.99 0.92 2/54 20201
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 1245 0 0 0 2995 4 0 0 25 0 1 0 549963304 5865472 1012 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1432 1012 603 41 0 1391 0
vsize: 5728
[startup+40.0012 s]
Raw data (loadavg): 0.95 0.99 0.92 2/54 20201
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 1245 0 0 0 3994 4 0 0 25 0 1 0 549963304 5865472 1012 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1432 1012 603 41 0 1391 0
vsize: 5728
[startup+50.0013 s]
Raw data (loadavg): 0.96 0.99 0.92 2/54 20201
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 17892 0 0 0 4954 44 0 0 25 0 1 0 549963304 77709312 17366 4294967295 134512640 134672761 3221224544 3221223136 134621410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18972 17366 603 41 0 18931 0
vsize: 75888
[startup+60.0021 s]
Raw data (loadavg): 0.96 0.99 0.92 2/54 20201
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 18481 0 0 0 5908 65 0 0 25 0 1 0 549963304 76308480 17285 4294967295 134512640 134672761 3221224544 3221222992 134644040 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.0022 s]
Raw data (loadavg): 0.97 0.99 0.92 2/54 20201
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 23212 0 0 0 6893 80 0 0 25 0 1 0 549963304 76759040 17425 4294967295 134512640 134672761 3221224544 3221222096 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+80.0022 s]
Raw data (loadavg): 0.97 0.99 0.92 2/54 20201
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 23212 0 0 0 7893 80 0 0 25 0 1 0 549963304 76759040 17425 4294967295 134512640 134672761 3221224544 3221221808 134597218 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.0028 s]
Raw data (loadavg): 0.98 0.99 0.92 2/54 20201
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 23212 0 0 0 8892 81 0 0 25 0 1 0 549963304 76759040 17425 4294967295 134512640 134672761 3221224544 3221222240 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.002 s]
Raw data (loadavg): 0.98 0.99 0.92 2/54 20201
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 23212 0 0 0 9892 81 0 0 25 0 1 0 549963304 76759040 17425 4294967295 134512640 134672761 3221224544 3221222528 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+110.003 s]
Raw data (loadavg): 0.98 0.99 0.92 2/54 20201
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 23212 0 0 0 10893 81 0 0 25 0 1 0 549963304 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.003 s]
Raw data (loadavg): 0.98 0.99 0.92 2/54 20201
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 28174 0 0 0 11874 99 0 0 25 0 1 0 549963304 76832768 17486 4294967295 134512640 134672761 3221224544 3221222096 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+130.002 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20201
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 28174 0 0 0 12874 99 0 0 25 0 1 0 549963304 76832768 17486 4294967295 134512640 134672761 3221224544 3221221808 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18758 17486 603 41 0 18717 0
vsize: 75032
[startup+140.003 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20201
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 28174 0 0 0 13874 99 0 0 25 0 1 0 549963304 76832768 17486 4294967295 134512640 134672761 3221224544 3221221664 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18758 17486 603 41 0 18717 0
vsize: 75032
[startup+150.004 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20201
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 28174 0 0 0 14874 99 0 0 25 0 1 0 549963304 76832768 17486 4294967295 134512640 134672761 3221224544 3221221808 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18758 17486 603 41 0 18717 0
vsize: 75032
[startup+160.004 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20201
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 29120 0 0 0 15872 101 0 0 25 0 1 0 549963304 77774848 17694 4294967295 134512640 134672761 3221224544 3221223264 134542427 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18988 17700 603 41 0 18947 0
vsize: 75952
[startup+170.004 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20201
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 32920 0 0 0 16860 113 0 0 25 0 1 0 549963304 91574272 20678 4294967295 134512640 134672761 3221224544 3221222848 134541817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22357 20678 603 41 0 22316 0
vsize: 89428
[startup+180.004 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20201
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 33179 0 0 0 17858 115 0 0 25 0 1 0 549963304 77115392 17539 4294967295 134512640 134672761 3221224544 3221222528 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+190.004 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20201
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 33179 0 0 0 18858 115 0 0 25 0 1 0 549963304 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+200.004 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20201
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 33179 0 0 0 19859 115 0 0 25 0 1 0 549963304 77115392 17539 4294967295 134512640 134672761 3221224544 3221222528 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.004 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20201
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 33179 0 0 0 20859 115 0 0 25 0 1 0 549963304 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+220.005 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20201
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 44412 0 0 0 21829 145 0 0 25 0 1 0 549963304 124719104 26693 4294967295 134512640 134672761 3221224544 3221222720 134605574 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.005 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20201
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 45916 0 0 0 22793 155 0 0 25 0 1 0 549963304 124162048 26601 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30313 26601 603 41 0 30272 0
vsize: 121252
[startup+240.005 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20201
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 45964 0 0 0 23793 156 0 0 25 0 1 0 549963304 124424192 26649 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30377 26649 603 41 0 30336 0
vsize: 121508
[startup+250.006 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20201
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 52052 0 0 0 24770 178 0 0 25 0 1 0 549963304 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.007 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 52052 0 0 0 25771 178 0 0 25 0 1 0 549963304 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+270.006 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 52052 0 0 0 26771 178 0 0 25 0 1 0 549963304 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+280.006 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 52052 0 0 0 27771 178 0 0 25 0 1 0 549963304 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.006 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 54503 0 0 0 28765 184 0 0 25 0 1 0 549963304 133136384 28119 4294967295 134512640 134672761 3221224544 3221222432 134566554 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.005 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 60632 0 0 0 29742 207 0 0 25 0 1 0 549963304 125231104 26961 4294967295 134512640 134672761 3221224544 3221223744 134610675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30574 26961 603 41 0 30533 0
vsize: 122296
[startup+310.006 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 60757 0 0 0 30740 208 0 0 25 0 1 0 549963304 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+320.005 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 60757 0 0 0 31740 208 0 0 25 0 1 0 549963304 125231104 26961 4294967295 134512640 134672761 3221224544 3221222528 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+330.005 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 60757 0 0 0 32740 208 0 0 25 0 1 0 549963304 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+340.005 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 60757 0 0 0 33741 208 0 0 25 0 1 0 549963304 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+350.005 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 68358 0 0 0 34721 227 0 0 25 0 1 0 549963304 152932352 32039 4294967295 134512640 134672761 3221224544 3221222832 134541856 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37337 32039 603 41 0 37296 0
vsize: 149348
[startup+360.006 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 69341 0 0 0 35710 237 0 0 25 0 1 0 549963304 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+370.006 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 69341 0 0 0 36710 237 0 0 25 0 1 0 549963304 125497344 26994 4294967295 134512640 134672761 3221224544 3221222816 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30639 26994 603 41 0 30598 0
vsize: 122556
[startup+380.006 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 69341 0 0 0 37710 237 0 0 25 0 1 0 549963304 125497344 26994 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30639 26994 603 41 0 30598 0
vsize: 122556
[startup+390.007 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 69341 0 0 0 38710 237 0 0 25 0 1 0 549963304 125497344 26994 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30639 26994 603 41 0 30598 0
vsize: 122556
[startup+400.007 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 70513 0 0 0 39707 240 0 0 25 0 1 0 549963304 125497344 26997 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30639 26997 603 41 0 30598 0
vsize: 122556
[startup+410.008 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 70513 0 0 0 40707 240 0 0 25 0 1 0 549963304 125497344 26997 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30639 26997 603 41 0 30598 0
vsize: 122556
[startup+420.008 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 76864 0 0 0 41685 263 0 0 25 0 1 0 549963304 125530112 27005 4294967295 134512640 134672761 3221224544 3221221936 134597656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30647 27005 603 41 0 30606 0
vsize: 122588
[startup+430.007 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 76864 0 0 0 42685 263 0 0 25 0 1 0 549963304 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+440.007 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 76864 0 0 0 43685 263 0 0 25 0 1 0 549963304 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+450.007 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 76864 0 0 0 44685 263 0 0 25 0 1 0 549963304 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+460.007 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 78047 0 0 0 45683 266 0 0 25 0 1 0 549963304 125530112 27013 4294967295 134512640 134672761 3221224544 3221222992 134644016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30647 27013 603 41 0 30606 0
vsize: 122588
[startup+470.007 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 79220 0 0 0 46681 268 0 0 25 0 1 0 549963304 125530112 27013 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30647 27013 603 41 0 30606 0
vsize: 122588
[startup+480.007 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 84920 0 0 0 47664 284 0 0 25 0 1 0 549963304 156016640 32691 4294967295 134512640 134672761 3221224544 3221222732 1075346675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38090 32691 603 41 0 38049 0
vsize: 152360
[startup+490.007 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 85593 0 0 0 48658 290 0 0 25 0 1 0 549963304 125562880 27021 4294967295 134512640 134672761 3221224544 3221222360 1075353072 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.007 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 85593 0 0 0 49658 290 0 0 25 0 1 0 549963304 125562880 27021 4294967295 134512640 134672761 3221224544 3221222816 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.008 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 85593 0 0 0 50658 290 0 0 25 0 1 0 549963304 125562880 27021 4294967295 134512640 134672761 3221224544 3221222816 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.008 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 85593 0 0 0 51659 290 0 0 25 0 1 0 549963304 125562880 27021 4294967295 134512640 134672761 3221224544 3221222528 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.008 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 87939 0 0 0 52652 297 0 0 25 0 1 0 549963304 125562880 27021 4294967295 134512640 134672761 3221224544 3221223744 134610661 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.009 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 94243 0 0 0 53628 320 0 0 25 0 1 0 549963304 125816832 27082 4294967295 134512640 134672761 3221224544 3221221520 134597224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30717 27082 603 41 0 30676 0
vsize: 122868
[startup+550.008 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 94243 0 0 0 54628 320 0 0 25 0 1 0 549963304 125816832 27082 4294967295 134512640 134672761 3221224544 3221221664 134597184 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.009 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 94243 0 0 0 55628 320 0 0 25 0 1 0 549963304 125816832 27082 4294967295 134512640 134672761 3221224544 3221221800 134597648 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.009 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 94243 0 0 0 56628 320 0 0 25 0 1 0 549963304 125816832 27082 4294967295 134512640 134672761 3221224544 3221222816 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.008 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 94243 0 0 0 57628 320 0 0 25 0 1 0 549963304 125816832 27082 4294967295 134512640 134672761 3221224544 3221222384 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+590.009 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 96597 0 0 0 58622 326 0 0 25 0 1 0 549963304 132976640 28263 4294967295 134512640 134672761 3221224544 3221223088 134621062 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32465 28263 603 41 0 32424 0
vsize: 129860
[startup+600.009 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 96597 0 0 0 59622 326 0 0 25 0 1 0 549963304 125816832 27090 4294967295 134512640 134672761 3221224544 3221223648 134604328 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30717 27090 603 41 0 30676 0
vsize: 122868
[startup+610.009 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 103091 0 0 0 60598 350 0 0 25 0 1 0 549963304 126017536 27140 4294967295 134512640 134672761 3221224544 3221222096 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+620.01 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 103091 0 0 0 61598 350 0 0 25 0 1 0 549963304 126017536 27140 4294967295 134512640 134672761 3221224544 3221222096 134597176 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30766 27140 603 41 0 30725 0
vsize: 123064
[startup+630.009 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 103091 0 0 0 62598 350 0 0 25 0 1 0 549963304 126017536 27140 4294967295 134512640 134672761 3221224544 3221221504 134597477 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30766 27140 603 41 0 30725 0
vsize: 123064
[startup+640.01 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 103091 0 0 0 63599 350 0 0 25 0 1 0 549963304 126017536 27140 4294967295 134512640 134672761 3221224544 3221222672 134597188 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.01 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 103276 0 0 0 64598 350 0 0 25 0 1 0 549963304 126554112 27325 4294967295 134512640 134672761 3221224544 3221219744 134522881 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30897 27326 603 41 0 30856 0
vsize: 123588
[startup+660.011 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 109676 0 0 0 65578 371 0 0 25 0 1 0 549963304 144158720 32063 4294967295 134512640 134672761 3221224544 3221223256 134643275 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.011 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 109676 0 0 0 66577 371 0 0 25 0 1 0 549963304 135806976 30595 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33156 30595 603 41 0 33115 0
vsize: 132624
[startup+680.01 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 116859 0 0 0 67550 399 0 0 25 0 1 0 549963304 138051584 31178 4294967295 134512640 134672761 3221224544 3221221784 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33704 31178 603 41 0 33663 0
vsize: 134816
[startup+690.011 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 116859 0 0 0 68550 399 0 0 25 0 1 0 549963304 138051584 31178 4294967295 134512640 134672761 3221224544 3221221664 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.011 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 116859 0 0 0 69550 399 0 0 25 0 1 0 549963304 138051584 31178 4294967295 134512640 134672761 3221224544 3221222208 1075351041 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.011 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 116859 0 0 0 70550 399 0 0 25 0 1 0 549963304 138051584 31178 4294967295 134512640 134672761 3221224544 3221221952 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.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 118116 0 0 0 71548 401 0 0 25 0 1 0 549963304 144621568 32435 4294967295 134512640 134672761 3221224544 3221223088 134621095 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.012 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 119331 0 0 0 72544 405 0 0 25 0 1 0 549963304 145698816 32434 4294967295 134512640 134672761 3221224544 3221223088 134621068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35571 32434 603 41 0 35530 0
vsize: 142284
[startup+740.012 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 126039 0 0 0 73518 431 0 0 25 0 1 0 549963304 138059776 31222 4294967295 134512640 134672761 3221224544 3221221664 134597176 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33706 31222 603 41 0 33665 0
vsize: 134824
[startup+750.012 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 126039 0 0 0 74518 431 0 0 25 0 1 0 549963304 138059776 31222 4294967295 134512640 134672761 3221224544 3221221664 134597203 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33706 31222 603 41 0 33665 0
vsize: 134824
[startup+760.013 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 126039 0 0 0 75518 431 0 0 25 0 1 0 549963304 138059776 31222 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33706 31222 603 41 0 33665 0
vsize: 134824
[startup+770.013 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 126039 0 0 0 76518 431 0 0 25 0 1 0 549963304 138059776 31222 4294967295 134512640 134672761 3221224544 3221221952 134597200 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33706 31222 603 41 0 33665 0
vsize: 134824
[startup+780.013 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 127255 0 0 0 77515 434 0 0 25 0 1 0 549963304 138059776 31226 4294967295 134512640 134672761 3221224544 3221223744 134610681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33706 31226 603 41 0 33665 0
vsize: 134824
[startup+790.013 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 127255 0 0 0 78515 434 0 0 25 0 1 0 549963304 138059776 31226 4294967295 134512640 134672761 3221224544 3221223728 134615625 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.013 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 127255 0 0 0 79516 434 0 0 25 0 1 0 549963304 138059776 31226 4294967295 134512640 134672761 3221224544 3221223680 134614701 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.014 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 134199 0 0 0 80492 459 0 0 25 0 1 0 549963304 170110976 38106 4294967295 134512640 134672761 3221224544 3221222736 134564929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41531 38106 603 41 0 41490 0
vsize: 166124
[startup+820.015 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 134230 0 0 0 81489 461 0 0 25 0 1 0 549963304 141197312 31983 4294967295 134512640 134672761 3221224544 3221222672 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.014 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 134230 0 0 0 82489 461 0 0 25 0 1 0 549963304 141197312 31983 4294967295 134512640 134672761 3221224544 3221222240 134597191 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.014 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 134230 0 0 0 83489 461 0 0 25 0 1 0 549963304 141197312 31983 4294967295 134512640 134672761 3221224544 3221222040 1075346913 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.014 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 134230 0 0 0 84488 462 0 0 25 0 1 0 549963304 141197312 31983 4294967295 134512640 134672761 3221224544 3221222096 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+860.014 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 136659 0 0 0 85482 468 0 0 25 0 1 0 549963304 148246528 33198 4294967295 134512640 134672761 3221224544 3221223088 134621235 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.014 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 136659 0 0 0 86482 468 0 0 25 0 1 0 549963304 141197312 31983 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34472 31983 603 41 0 34431 0
vsize: 137888
[startup+880.014 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 136671 0 0 0 87482 469 0 0 25 0 1 0 549963304 141197312 31995 4294967295 134512640 134672761 3221224544 3221223744 134610707 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.015 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 136671 0 0 0 88482 469 0 0 25 0 1 0 549963304 141197312 31995 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34472 31995 603 41 0 34431 0
vsize: 137888
[startup+900.015 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 143156 0 0 0 89456 495 0 0 25 0 1 0 549963304 141209600 32007 4294967295 134512640 134672761 3221224544 3221221952 134597191 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.015 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 143156 0 0 0 90456 495 0 0 25 0 1 0 549963304 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+920.016 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 143156 0 0 0 91455 495 0 0 25 0 1 0 549963304 141209600 32007 4294967295 134512640 134672761 3221224544 3221221952 134597191 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.016 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 143156 0 0 0 92455 495 0 0 25 0 1 0 549963304 141209600 32007 4294967295 134512640 134672761 3221224544 3221221808 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.016 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 144384 0 0 0 93452 499 0 0 25 0 1 0 549963304 150130688 33235 4294967295 134512640 134672761 3221224544 3221223088 134621062 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36653 33235 603 41 0 36612 0
vsize: 146612
[startup+950.017 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 144992 0 0 0 94450 501 0 0 25 0 1 0 549963304 141209600 32019 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34475 32019 603 41 0 34434 0
vsize: 137900
[startup+960.018 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 151379 0 0 0 95426 525 0 0 25 0 1 0 549963304 141213696 32020 4294967295 134512640 134672761 3221224544 3221221664 134597235 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.018 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 151379 0 0 0 96426 525 0 0 25 0 1 0 549963304 141213696 32020 4294967295 134512640 134672761 3221224544 3221222240 134597224 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.018 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 151379 0 0 0 97425 526 0 0 25 0 1 0 549963304 141213696 32020 4294967295 134512640 134672761 3221224544 3221222096 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+990.019 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 151379 0 0 0 98425 526 0 0 25 0 1 0 549963304 141213696 32020 4294967295 134512640 134672761 3221224544 3221221868 1075349878 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.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 152597 0 0 0 99421 530 0 0 25 0 1 0 549963304 141213696 32022 4294967295 134512640 134672761 3221224544 3221223744 134610707 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.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 152597 0 0 0 100421 530 0 0 25 0 1 0 549963304 141213696 32022 4294967295 134512640 134672761 3221224544 3221223728 134615727 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.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 152597 0 0 0 101421 531 0 0 25 0 1 0 549963304 141213696 32022 4294967295 134512640 134672761 3221224544 3221223584 134612783 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.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 152597 0 0 0 102421 531 0 0 25 0 1 0 549963304 141213696 32022 4294967295 134512640 134672761 3221224544 3221223728 134615625 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.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 152597 0 0 0 103421 531 0 0 25 0 1 0 549963304 141213696 32022 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34476 32022 603 41 0 34435 0
vsize: 137904
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 159329 0 0 0 104392 559 0 0 25 0 1 0 549963304 141213696 32022 4294967295 134512640 134672761 3221224544 3221221664 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.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 159329 0 0 0 105392 559 0 0 25 0 1 0 549963304 141213696 32022 4294967295 134512640 134672761 3221224544 3221221952 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+1070.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 159329 0 0 0 106392 559 0 0 25 0 1 0 549963304 141213696 32022 4294967295 134512640 134672761 3221224544 3221221664 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.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 159329 0 0 0 107392 559 0 0 25 0 1 0 549963304 141213696 32022 4294967295 134512640 134672761 3221224544 3221222096 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+1090.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 166720 0 0 0 108376 576 0 0 25 0 1 0 549963304 195682304 39409 4294967295 134512640 134672761 3221224544 3221223152 134541802 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.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 166949 0 0 0 109368 584 0 0 25 0 1 0 549963304 186671104 37699 4294967295 134512640 134672761 3221224544 3221222848 134621730 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45574 37699 603 41 0 45533 0
vsize: 182296
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 168811 0 0 0 110360 592 0 0 25 0 1 0 549963304 197763072 39444 4294967295 134512640 134672761 3221224544 3221223088 134621202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48282 39444 603 41 0 48241 0
vsize: 193128
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 177431 0 0 0 111325 626 0 0 25 0 1 0 549963304 187080704 37723 4294967295 134512640 134672761 3221224544 3221221808 134597188 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.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 177431 0 0 0 112324 626 0 0 25 0 1 0 549963304 187080704 37723 4294967295 134512640 134672761 3221224544 3221222240 134597191 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.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 177431 0 0 0 113324 626 0 0 25 0 1 0 549963304 187080704 37723 4294967295 134512640 134672761 3221224544 3221222384 134597195 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.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 177431 0 0 0 114324 626 0 0 25 0 1 0 549963304 187080704 37723 4294967295 134512640 134672761 3221224544 3221221808 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.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 186283 0 0 0 115304 646 0 0 25 0 1 0 549963304 211275776 45916 4294967295 134512640 134672761 3221224544 3221128184 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51581 45917 603 41 0 51540 0
vsize: 206324
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 192771 0 0 0 116276 673 0 0 25 0 1 0 549963304 233385984 49652 4294967295 134512640 134672761 3221224544 3221223312 134629735 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56979 49652 603 41 0 56938 0
vsize: 227916
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 193095 0 0 0 117274 675 0 0 25 0 1 0 549963304 219869184 47651 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53679 47651 603 41 0 53638 0
vsize: 214716
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 193124 0 0 0 118274 675 0 0 25 0 1 0 549963304 219869184 47680 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53679 47680 603 41 0 53638 0
vsize: 214716
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 193186 0 0 0 119273 675 0 0 25 0 1 0 549963304 220250112 47742 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53772 47742 603 41 0 53731 0
vsize: 215088
[startup+1210.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 20203
Raw data (stat): 20201 (minisat+) R 20200 3260 3259 0 -1 0 203584 0 0 0 120235 713 0 0 25 0 1 0 549963304 279965696 58005 4294967295 134512640 134672761 3221224544 3221222880 134603771 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68351 58005 603 41 0 68310 0
vsize: 273404
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1210.18 s]
Raw data (loadavg): 0.99 0.99 0.92 1/54 20203
Raw data (stat): 20201 (minisat+) Z 20200 3260 3259 0 -1 12 203585 0 0 0 120235 728 0 0 25 0 1 0 549963304 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.18
CPU time (s): 1209.64
CPU user time (s): 1202.36
CPU system time (s): 7.28489
CPU usage (%): 99.9557
Max. virtual memory (Kb): 273404
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####