PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/submitted/manquinho/primes-dimacs-cnf/normalized-ii8a4.opb
MD5SUM	8a77190c2eeefb9e88447a9087adfd6f
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	283
Optimality of the best value was proved	NO
Number of terms in the objective function	792
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	792
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	792
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02084
Number of variables	792
Total number of constraints	3194
Number of constraints which are clauses	3194
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	8
Trace number 5503

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc7 THE 2005-04-14 00:14:39 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3926 boxname=wulflinc7 idbench=166 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  8a77190c2eeefb9e88447a9087adfd6f  /oldhome/oroussel/tmp/wulflinc7/normalized-ii8a4.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc7/normalized-ii8a4.opb /oldhome/oroussel/tmp/wulflinc7/normalized-ii8a4.opb
IDLAUNCH: 3926
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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	: 2
cpu MHz		: 451.050
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:        900776 kB
Buffers:         37104 kB
Cached:          77272 kB
SwapCached:          0 kB
Active:          72620 kB
Inactive:        44632 kB
HighTotal:      131008 kB
HighFree:        49756 kB
LowTotal:       903652 kB
LowFree:        851020 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            10884 kB
Committed_AS:    63468 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 00:34:41 (client local time) WITH STATUS 10 IN 1200.15 SECONDS
stats: 3926 7 1200.15 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 3194 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    3134     7908 |     940       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  792/792          
c |         0 |    3134     7908 |    1253       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.103984 s)
c ==============================================================================
c [1mFound solution: 357[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:36470     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         4 |   47573   111782 |   14271       4       27     6.8 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/29759          
c   -- var.elim.:  2000/29759          
c   -- var.elim.:  3000/29759          
c   -- var.elim.:  4000/29759          
c   -- var.elim.:  5000/29759          
c   -- var.elim.:  6000/29759          
c   -- var.elim.:  7000/29759          
c   -- var.elim.:  8000/29759          
c   -- var.elim.:  9000/29759          
c   -- var.elim.:  10000/29759          
c   -- var.elim.:  11000/29759          
c   -- var.elim.:  12000/29759          
c   -- var.elim.:  13000/29759          
c   -- var.elim.:  14000/29759          
c   -- var.elim.:  15000/29759          
c   -- var.elim.:  16000/29759          
c   -- var.elim.:  17000/29759          
c   -- var.elim.:  18000/29759          
c   -- var.elim.:  19000/29759          
c   -- var.elim.:  20000/29759          
c   -- var.elim.:  21000/29759          
c   -- var.elim.:  22000/29759          
c   -- var.elim.:  23000/29759          
c   -- var.elim.:  24000/29759          
c   -- var.elim.:  25000/29759          
c   -- var.elim.:  26000/29759          
c   -- var.elim.:  27000/29759          
c   -- var.elim.:  28000/29759          
c   -- var.elim.:  29000/29759          
c   -- var.elim.:  29759/29759          
c   -- var.elim.:  1000/14612          
c   -- var.elim.:  2000/14612          
c   -- var.elim.:  3000/14612          
c   -- var.elim.:  4000/14612          
c   -- var.elim.:  5000/14612          
c   -- var.elim.:  6000/14612          
c   -- var.elim.:  7000/14612          
c   -- var.elim.:  8000/14612          
c   -- var.elim.:  9000/14612          
c   -- var.elim.:  10000/14612          
c   -- var.elim.:  11000/14612          
c   -- var.elim.:  12000/14612          
c   -- var.elim.:  13000/14612          
c   -- var.elim.:  14000/14612          
c   -- var.elim.:  14612/14612          
c   -- var.elim.:  1000/8640          
c   -- var.elim.:  2000/8640          
c   -- var.elim.:  3000/8640          
c   -- var.elim.:  4000/8640          
c   -- var.elim.:  5000/8640          
c   -- var.elim.:  6000/8640          
c   -- var.elim.:  7000/8640          
c   -- var.elim.:  8000/8640          
c   -- var.elim.:  8640/8640          
c   -- var.elim.:  1000/6221          
c   -- var.elim.:  2000/6221          
c   -- var.elim.:  3000/6221          
c   -- var.elim.:  4000/6221          
c   -- var.elim.:  5000/6221          
c   -- var.elim.:  6000/6221          
c   -- var.elim.:  6221/6221          
c   -- var.elim.:  1000/5060          
c   -- var.elim.:  2000/5060          
c   -- var.elim.:  3000/5060          
c   -- var.elim.:  4000/5060          
c   -- var.elim.:  5000/5060          
c   -- var.elim.:  5060/5060          
c   -- var.elim.:  1000/2947          
c   -- var.elim.:  2000/2947          
c   -- var.elim.:  2947/2947          
c   -- var.elim.:  1000/1955          
c   -- var.elim.:  1955/1955          
c   -- var.elim.:  667/667          
c   -- var.elim.:  67/67          
c   -- subsuming                       
c   -- var.elim.:  1000/4469          
c   -- var.elim.:  2000/4469          
c   -- var.elim.:  3000/4469          
c   -- var.elim.:  4000/4469          
c   -- var.elim.:  4469/4469          
c   -- var.elim.:  54/54          
c |         4 |   15541    99505 |      --       4       --      -- |     --   | -32032/-12276
c |         4 |   15541    99505 |    6216       4       27     6.8 |  0.000 % |
c |       104 |   15478    99038 |    6810     101    11734   116.2 |  0.384 % |
c |       254 |   15392    98401 |    7449     248    45635   184.0 |  0.967 % |
c |       479 |   15313    97785 |    8152     469    91220   194.5 |  1.488 % |
c |       817 |   15313    97785 |    8967     807   190153   235.6 |  1.488 % |
c ==============================================================================
c (current CPU-time: 36.3385 s)
c ==============================================================================
c [1mFound solution: 343[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       977 |   46100   173186 |   13829     967   225513   233.2 |  1.488 % |
c   -- subsuming                       
c   -- var.elim.:  1000/28108          
c   -- var.elim.:  2000/28108          
c   -- var.elim.:  3000/28108          
c   -- var.elim.:  4000/28108          
c   -- var.elim.:  5000/28108          
c   -- var.elim.:  6000/28108          
c   -- var.elim.:  7000/28108          
c   -- var.elim.:  8000/28108          
c   -- var.elim.:  9000/28108          
c   -- var.elim.:  10000/28108          
c   -- var.elim.:  11000/28108          
c   -- var.elim.:  12000/28108          
c   -- var.elim.:  13000/28108          
c   -- var.elim.:  14000/28108          
c   -- var.elim.:  15000/28108          
c   -- var.elim.:  16000/28108          
c   -- var.elim.:  17000/28108          
c   -- var.elim.:  18000/28108          
c   -- var.elim.:  19000/28108          
c   -- var.elim.:  20000/28108          
c   -- var.elim.:  21000/28108          
c   -- var.elim.:  22000/28108          
c   -- var.elim.:  23000/28108          
c   -- var.elim.:  24000/28108          
c   -- var.elim.:  25000/28108          
c   -- var.elim.:  26000/28108          
c   -- var.elim.:  27000/28108          
c   -- var.elim.:  28000/28108          
c   -- var.elim.:  28108/28108          
c   -- var.elim.:  1000/13537          
c   -- var.elim.:  2000/13537          
c   -- var.elim.:  3000/13537          
c   -- var.elim.:  4000/13537          
c   -- var.elim.:  5000/13537          
c   -- var.elim.:  6000/13537          
c   -- var.elim.:  7000/13537          
c   -- var.elim.:  8000/13537          
c   -- var.elim.:  9000/13537          
c   -- var.elim.:  10000/13537          
c   -- var.elim.:  11000/13537          
c   -- var.elim.:  12000/13537          
c   -- var.elim.:  13000/13537          
c   -- var.elim.:  13537/13537          
c   -- var.elim.:  1000/8218          
c   -- var.elim.:  2000/8218          
c   -- var.elim.:  3000/8218          
c   -- var.elim.:  4000/8218          
c   -- var.elim.:  5000/8218          
c   -- var.elim.:  6000/8218          
c   -- var.elim.:  7000/8218          
c   -- var.elim.:  8000/8218          
c   -- var.elim.:  8218/8218          
c   -- var.elim.:  1000/6007          
c   -- var.elim.:  2000/6007          
c   -- var.elim.:  3000/6007          
c   -- var.elim.:  4000/6007          
c   -- var.elim.:  5000/6007          
c   -- var.elim.:  6000/6007          
c   -- var.elim.:  6007/6007          
c   -- var.elim.:  1000/4829          
c   -- var.elim.:  2000/4829          
c   -- var.elim.:  3000/4829          
c   -- var.elim.:  4000/4829          
c   -- var.elim.:  4829/4829          
c   -- var.elim.:  1000/3921          
c   -- var.elim.:  2000/3921          
c   -- var.elim.:  3000/3921          
c   -- var.elim.:  3921/3921          
c   -- var.elim.:  1000/3230          
c   -- var.elim.:  2000/3230          
c   -- var.elim.:  3000/3230          
c   -- var.elim.:  3230/3230          
c   -- var.elim.:  1000/1200          
c   -- var.elim.:  1200/1200          
c   -- var.elim.:  124/124          
c   -- subsuming                       
c   -- var.elim.:  1000/2036          
c   -- var.elim.:  2000/2036          
c   -- var.elim.:  2036/2036          
c |       977 |   15641   102416 |      --     967       --      -- |     --   | -30449/-70749
c |       977 |   15641   102416 |    6256     649    29645    45.7 |  1.488 % |
c |      1077 |   15641   102416 |    6882     749    45684    61.0 |  2.149 % |
c |      1227 |   15586   101973 |    7543     896    62594    69.9 |  2.505 % |
c |      1452 |   15388   100342 |    8192    1111    95692    86.1 |  3.721 % |
c |      1790 |   15296    99509 |    8957    1444   227510   157.6 |  4.314 % |
c |      2296 |   15197    98612 |    9789    1946   333291   171.3 |  4.951 % |
c |      3055 |   14970    96536 |   10608    2695   493681   183.2 |  6.478 % |
c ==============================================================================
c (current CPU-time: 72.12 s)
c ==============================================================================
c [1mFound solution: 328[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      3280 |   44727   168577 |   13418    2913   557165   191.3 |  6.478 % |
c   -- subsuming                       
c   -- var.elim.:  1000/27265          
c   -- var.elim.:  2000/27265          
c   -- var.elim.:  3000/27265          
c   -- var.elim.:  4000/27265          
c   -- var.elim.:  5000/27265          
c   -- var.elim.:  6000/27265          
c   -- var.elim.:  7000/27265          
c   -- var.elim.:  8000/27265          
c   -- var.elim.:  9000/27265          
c   -- var.elim.:  10000/27265          
c   -- var.elim.:  11000/27265          
c   -- var.elim.:  12000/27265          
c   -- var.elim.:  13000/27265          
c   -- var.elim.:  14000/27265          
c   -- var.elim.:  15000/27265          
c   -- var.elim.:  16000/27265          
c   -- var.elim.:  17000/27265          
c   -- var.elim.:  18000/27265          
c   -- var.elim.:  19000/27265          
c   -- var.elim.:  20000/27265          
c   -- var.elim.:  21000/27265          
c   -- var.elim.:  22000/27265          
c   -- var.elim.:  23000/27265          
c   -- var.elim.:  24000/27265          
c   -- var.elim.:  25000/27265          
c   -- var.elim.:  26000/27265          
c   -- var.elim.:  27000/27265          
c   -- var.elim.:  27265/27265          
c   -- var.elim.:  1000/12985          
c   -- var.elim.:  2000/12985          
c   -- var.elim.:  3000/12985          
c   -- var.elim.:  4000/12985          
c   -- var.elim.:  5000/12985          
c   -- var.elim.:  6000/12985          
c   -- var.elim.:  7000/12985          
c   -- var.elim.:  8000/12985          
c   -- var.elim.:  9000/12985          
c   -- var.elim.:  10000/12985          
c   -- var.elim.:  11000/12985          
c   -- var.elim.:  12000/12985          
c   -- var.elim.:  12985/12985          
c   -- var.elim.:  1000/8035          
c   -- var.elim.:  2000/8035          
c   -- var.elim.:  3000/8035          
c   -- var.elim.:  4000/8035          
c   -- var.elim.:  5000/8035          
c   -- var.elim.:  6000/8035          
c   -- var.elim.:  7000/8035          
c   -- var.elim.:  8000/8035          
c   -- var.elim.:  8035/8035          
c   -- var.elim.:  1000/6075          
c   -- var.elim.:  2000/6075          
c   -- var.elim.:  3000/6075          
c   -- var.elim.:  4000/6075          
c   -- var.elim.:  5000/6075          
c   -- var.elim.:  6000/6075          
c   -- var.elim.:  6075/6075          
c   -- var.elim.:  1000/4893          
c   -- var.elim.:  2000/4893          
c   -- var.elim.:  3000/4893          
c   -- var.elim.:  4000/4893          
c   -- var.elim.:  4893/4893          
c   -- var.elim.:  1000/3754          
c   -- var.elim.:  2000/3754          
c   -- var.elim.:  3000/3754          
c   -- var.elim.:  3754/3754          
c   -- var.elim.:  1000/3356          
c   -- var.elim.:  2000/3356          
c   -- var.elim.:  3000/3356          
c   -- var.elim.:  3356/3356          
c   -- var.elim.:  1000/2163          
c   -- var.elim.:  2000/2163          
c   -- var.elim.:  2163/2163          
c   -- var.elim.:  535/535          
c   -- var.elim.:  14/14          
c   -- subsuming                       
c   -- var.elim.:  1000/2014          
c   -- var.elim.:  2000/2014          
c   -- var.elim.:  2014/2014          
c |      3280 |   15028    98766 |      --    2913       --      -- |     --   | -29650/-69607
c |      3280 |   15028    98766 |    6011    2913   557165   191.3 |  6.478 % |
c |      3381 |   15028    98766 |    6612    3014   581208   192.8 | 11.286 % |
c |      3531 |   14986    98376 |    7253    2377   150359    63.3 | 11.540 % |
c |      3756 |   14879    97444 |    7921    2598   196009    75.4 | 12.243 % |
c |      4094 |   14835    97019 |    8687    2934   298871   101.9 | 12.496 % |
c |      4600 |   14721    95991 |    9483    3434   414112   120.6 | 13.200 % |
c |      5359 |   14671    95521 |   10396    4189   556983   133.0 | 13.468 % |
c |      6499 |   14583    94691 |   11367    5324   935711   175.8 | 14.030 % |
c |      8208 |   14545    94307 |   12471    7029  1416274   201.5 | 14.270 % |
c |     10770 |   14490    93766 |   13666    9584  2210075   230.6 | 14.593 % |
c |     14615 |   14343    92384 |   14880   13413  3506524   261.4 | 15.550 % |
c ==============================================================================
c (current CPU-time: 139.532 s)
c ==============================================================================
c [1mFound solution: 312[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     17637 |   44065   164582 |   13219   11079  3487340   314.8 | 15.550 % |
c   -- subsuming                       
c   -- var.elim.:  1000/26892          
c   -- var.elim.:  2000/26892          
c   -- var.elim.:  3000/26892          
c   -- var.elim.:  4000/26892          
c   -- var.elim.:  5000/26892          
c   -- var.elim.:  6000/26892          
c   -- var.elim.:  7000/26892          
c   -- var.elim.:  8000/26892          
c   -- var.elim.:  9000/26892          
c   -- var.elim.:  10000/26892          
c   -- var.elim.:  11000/26892          
c   -- var.elim.:  12000/26892          
c   -- var.elim.:  13000/26892          
c   -- var.elim.:  14000/26892          
c   -- var.elim.:  15000/26892          
c   -- var.elim.:  16000/26892          
c   -- var.elim.:  17000/26892          
c   -- var.elim.:  18000/26892          
c   -- var.elim.:  19000/26892          
c   -- var.elim.:  20000/26892          
c   -- var.elim.:  21000/26892          
c   -- var.elim.:  22000/26892          
c   -- var.elim.:  23000/26892          
c   -- var.elim.:  24000/26892          
c   -- var.elim.:  25000/26892          
c   -- var.elim.:  26000/26892          
c   -- var.elim.:  26892/26892          
c   -- var.elim.:  1000/12686          
c   -- var.elim.:  2000/12686          
c   -- var.elim.:  3000/12686          
c   -- var.elim.:  4000/12686          
c   -- var.elim.:  5000/12686          
c   -- var.elim.:  6000/12686          
c   -- var.elim.:  7000/12686          
c   -- var.elim.:  8000/12686          
c   -- var.elim.:  9000/12686          
c   -- var.elim.:  10000/12686          
c   -- var.elim.:  11000/12686          
c   -- var.elim.:  12000/12686          
c   -- var.elim.:  12686/12686          
c   -- var.elim.:  1000/7670          
c   -- var.elim.:  2000/7670          
c   -- var.elim.:  3000/7670          
c   -- var.elim.:  4000/7670          
c   -- var.elim.:  5000/7670          
c   -- var.elim.:  6000/7670          
c   -- var.elim.:  7000/7670          
c   -- var.elim.:  7670/7670          
c   -- var.elim.:  1000/5748          
c   -- var.elim.:  2000/5748          
c   -- var.elim.:  3000/5748          
c   -- var.elim.:  4000/5748          
c   -- var.elim.:  5000/5748          
c   -- var.elim.:  5748/5748          
c   -- var.elim.:  1000/4524          
c   -- var.elim.:  2000/4524          
c   -- var.elim.:  3000/4524          
c   -- var.elim.:  4000/4524          
c   -- var.elim.:  4524/4524          
c   -- var.elim.:  1000/4031          
c   -- var.elim.:  2000/4031          
c   -- var.elim.:  3000/4031          
c   -- var.elim.:  4000/4031          
c   -- var.elim.:  4031/4031          
c   -- var.elim.:  1000/3193          
c   -- var.elim.:  2000/3193          
c   -- var.elim.:  3000/3193          
c   -- var.elim.:  3193/3193          
c   -- var.elim.:  1000/2233          
c   -- var.elim.:  2000/2233          
c   -- var.elim.:  2233/2233          
c   -- var.elim.:  143/143          
c   -- subsuming                       
c   -- var.elim.:  1000/2254          
c   -- var.elim.:  2000/2254          
c   -- var.elim.:  2254/2254          
c |     17637 |   14521    96101 |      --   11079       --      -- |     --   | -29495/-68338
c |     17637 |   14521    96101 |    5808    7052   580450    82.3 | 15.550 % |
c |     17738 |   14521    96101 |    6389    7153   593868    83.0 | 19.197 % |
c |     17888 |   14521    96101 |    7028    7303   611187    83.7 | 19.197 % |
c |     18114 |   14521    96101 |    7730    7529   666367    88.5 | 19.198 % |
c |     18451 |   14521    96101 |    8504    7866   723061    91.9 | 19.198 % |
c |     18957 |   14521    96101 |    9354    8372   851638   101.7 | 19.198 % |
c |     19716 |   14521    96101 |   10289    9131  1051134   115.1 | 19.197 % |
c |     20858 |   14521    96101 |   11318   10273  1462594   142.4 | 19.197 % |
c |     22566 |   14521    96101 |   12450   11981  1948049   162.6 | 19.197 % |
c |     25128 |   14491    95828 |   13667   14540  2735525   188.1 | 19.397 % |
c |     28972 |   14477    95692 |   15019   12497  3169341   253.6 | 19.464 % |
c |     34740 |   14477    95692 |   16521   18265  6802610   372.4 | 19.464 % |
c |     43390 |   14477    95692 |   18174   14444  6996052   484.4 | 19.464 % |
c |     56365 |   14477    95692 |   19991   17198  7359378   427.9 | 19.464 % |
c |     75826 |   14477    95692 |   21990   14448  7372074   510.2 | 19.464 % |
c |    105020 |   14336    94570 |   23954   21359 12896588   603.8 | 20.251 % |
c |    148809 |   14336    94570 |   26349   24276 12854921   529.5 | 20.251 % |
c |    214496 |   14336    94570 |   28984   25958 17253258   664.7 | 20.251 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v x1 -x2 x3 -x4 x5 -x6 x7 -x8 x9 -x10 x11 -x12 -x13 x14 x15 -x16 x17 -x18 x19 -x20 x21 -x22 x23 -x24 x25 -x26 -x27 x28 x29 -x30 x31 -x32 x33 -x34 x35 -x36 x37 -x38 x39 -x40 x41 -x42 x43 -x44 -x45 x46 x47 -x48 x49 -x50 x51 -x52 x53 -x54 x55 -x56 x57 -x58 -x59 x60 x61 -x62 x63 -x64 -x65 x66 x67 -x68 -x69 x70 x71 -x72 x73 -x74 x75 -x76 x77 -x78 -x79 -x80 x81 -x82 x83 -x84 x85 -x86 -x87 x88 x89 -x90 x91 -x92 x93 -x94 x95 -x96 x97 -x98 x99 -x100 x101 -x102 x103 -x104 x105 -x106 -x107 x108 -x109 x110 x111 -x112 x113 -x114 x115 -x116 x117 -x118 x119 -x120 x121 -x122 x123 -x124 x125 -x126 x127 -x128 x129 -x130 x131 -x132 x133 -x134 -x135 -x136 x137 -x138 -x139 x140 -x141 x142 x143 -x144 x145 -x146 x147 -x148 x149 -x150 -x151 -x152 x153 -x154 -x155 -x156 x157 -x158 x159 -x160 x161 -x162 x163 -x164 x165 -x166 x167 -x168 x169 -x170 -x171 x172 -x173 x174 x175 -x176 x177 -x178 x179 -x180 x181 -x182 x183 -x184 x185 -x186 x187 -x188 x189 -x190 x191 -x192 -x193 -x194 -x195 -x196 -x197 x198 x199 -x200 -x201 -x202 -x203 -x204 x205 -x206 -x207 -x208 -x209 x210 -x211 x212 -x213 x214 -x215 x216 -x217 -x218 -x219 -x220#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.95 0.90 2/54 26756
Raw data (stat): 26756 (runsolver) R 26755 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421972546 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 4439 0 0 0 981 16 0 0 25 0 1 0 421972546 20410368 4371 4294967295 134512640 134672761 3221224576 3221223056 134541816 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4983 4371 603 41 0 4942 0
vsize: 19932
[startup+20.0014 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 4544 0 0 0 1974 23 0 0 25 0 1 0 421972546 20955136 4476 4294967295 134512640 134672761 3221224576 3221223024 134643493 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5116 4476 603 41 0 5075 0
vsize: 20464
[startup+30.0014 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 4544 0 0 0 2974 24 0 0 25 0 1 0 421972546 20955136 4476 4294967295 134512640 134672761 3221224576 3221223100 134642908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5116 4476 603 41 0 5075 0
vsize: 20464
[startup+40.0011 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 6524 0 0 0 3965 33 0 0 25 0 1 0 421972546 27021312 5781 4294967295 134512640 134672761 3221224576 3221223088 134636980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6597 5781 603 41 0 6556 0
vsize: 26388
[startup+50.001 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 6554 0 0 0 4957 41 0 0 25 0 1 0 421972546 27021312 5811 4294967295 134512640 134672761 3221224576 3221223024 134643474 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6597 5811 603 41 0 6556 0
vsize: 26388
[startup+60.0013 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 6564 0 0 0 5953 45 0 0 25 0 1 0 421972546 27201536 5821 4294967295 134512640 134672761 3221224576 3221223024 134643493 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6641 5821 603 41 0 6600 0
vsize: 26564
[startup+70.001 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 6564 0 0 0 6952 45 0 0 25 0 1 0 421972546 27201536 5821 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6641 5821 603 41 0 6600 0
vsize: 26564
[startup+80.0025 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 11232 0 0 0 7929 68 0 0 25 0 1 0 421972546 36773888 7274 4294967295 134512640 134672761 3221224576 3221223024 134643483 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8978 7274 603 41 0 8937 0
vsize: 35912
[startup+90.0024 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 11239 0 0 0 8924 73 0 0 25 0 1 0 421972546 36773888 7281 4294967295 134512640 134672761 3221224576 3221223024 134643624 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8978 7281 603 41 0 8937 0
vsize: 35912
[startup+100.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 11239 0 0 0 9907 78 0 0 25 0 1 0 421972546 36773888 7281 4294967295 134512640 134672761 3221224576 3221223024 134643516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8978 7281 603 41 0 8937 0
vsize: 35912
[startup+110.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 11319 0 0 0 10907 78 0 0 25 0 1 0 421972546 37036032 7314 4294967295 134512640 134672761 3221224576 3221223712 134614812 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9042 7314 603 41 0 9001 0
vsize: 36168
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 12378 0 0 0 11904 81 0 0 25 0 1 0 421972546 41385984 8373 4294967295 134512640 134672761 3221224576 3221223760 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10104 8373 603 41 0 10063 0
vsize: 40416
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 13665 0 0 0 12901 84 0 0 25 0 1 0 421972546 46637056 9660 4294967295 134512640 134672761 3221224576 3221223616 134612996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11386 9661 603 41 0 11345 0
vsize: 45544
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 15432 0 0 0 13897 88 0 0 25 0 1 0 421972546 53862400 11427 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13150 11427 603 41 0 13109 0
vsize: 52600
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 19829 0 0 0 14871 113 0 0 25 0 1 0 421972546 54001664 11888 4294967295 134512640 134672761 3221224576 3221223024 134644014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13184 11888 603 41 0 13143 0
vsize: 52736
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 19829 0 0 0 15866 119 0 0 25 0 1 0 421972546 54001664 11888 4294967295 134512640 134672761 3221224576 3221223024 134644016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13184 11888 603 41 0 13143 0
vsize: 52736
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 19829 0 0 0 16864 120 0 0 25 0 1 0 421972546 54001664 11888 4294967295 134512640 134672761 3221224576 3221223120 134621242 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13184 11888 603 41 0 13143 0
vsize: 52736
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 19874 0 0 0 17865 121 0 0 25 0 1 0 421972546 54001664 11888 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13184 11888 603 41 0 13143 0
vsize: 52736
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 19874 0 0 0 18865 121 0 0 25 0 1 0 421972546 54001664 11888 4294967295 134512640 134672761 3221224576 3221223616 134614182 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13184 11888 603 41 0 13143 0
vsize: 52736
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 19874 0 0 0 19865 121 0 0 25 0 1 0 421972546 54001664 11888 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13184 11888 603 41 0 13143 0
vsize: 52736
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 20997 0 0 0 20862 123 0 0 25 0 1 0 421972546 58720256 13011 4294967295 134512640 134672761 3221224576 3221223616 134613769 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14336 13011 603 41 0 14295 0
vsize: 57344
[startup+220.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 22514 0 0 0 21859 127 0 0 25 0 1 0 421972546 64864256 14528 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15836 14528 603 41 0 15795 0
vsize: 63344
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 22859 0 0 0 22858 128 0 0 25 0 1 0 421972546 66273280 14873 4294967295 134512640 134672761 3221224576 3221223616 134613822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16180 14873 603 41 0 16139 0
vsize: 64720
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 24353 0 0 0 23855 131 0 0 25 0 1 0 421972546 72392704 16367 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17674 16367 603 41 0 17633 0
vsize: 70696
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 24487 0 0 0 24855 131 0 0 25 0 1 0 421972546 72941568 16500 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17808 16500 603 41 0 17767 0
vsize: 71232
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 24793 0 0 0 25854 132 0 0 25 0 1 0 421972546 74256384 16806 4294967295 134512640 134672761 3221224576 3221223712 134614690 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18129 16806 603 41 0 18088 0
vsize: 72516
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 26571 0 0 0 26850 137 0 0 25 0 1 0 421972546 81444864 18584 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19884 18584 603 41 0 19843 0
vsize: 79536
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 27171 0 0 0 27848 139 0 0 25 0 1 0 421972546 83914752 19183 4294967295 134512640 134672761 3221224576 3221223584 134522547 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20487 19183 603 41 0 20446 0
vsize: 81948
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 27171 0 0 0 28849 139 0 0 25 0 1 0 421972546 83914752 19183 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20487 19183 603 41 0 20446 0
vsize: 81948
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 27171 0 0 0 29849 139 0 0 25 0 1 0 421972546 83914752 19183 4294967295 134512640 134672761 3221224576 3221223776 134610646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20487 19183 603 41 0 20446 0
vsize: 81948
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 27171 0 0 0 30849 139 0 0 25 0 1 0 421972546 83914752 19183 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20487 19183 603 41 0 20446 0
vsize: 81948
[startup+320.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 27602 0 0 0 31848 140 0 0 25 0 1 0 421972546 85671936 19613 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20916 19613 603 41 0 20875 0
vsize: 83664
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 27602 0 0 0 32848 140 0 0 25 0 1 0 421972546 85671936 19613 4294967295 134512640 134672761 3221224576 3221223712 134614683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20916 19613 603 41 0 20875 0
vsize: 83664
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 27602 0 0 0 33848 140 0 0 25 0 1 0 421972546 85671936 19613 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20916 19613 603 41 0 20875 0
vsize: 83664
[startup+350.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 27602 0 0 0 34849 140 0 0 25 0 1 0 421972546 85671936 19613 4294967295 134512640 134672761 3221224576 3221223616 134612614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20916 19613 603 41 0 20875 0
vsize: 83664
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 28645 0 0 0 35847 142 0 0 25 0 1 0 421972546 89939968 20655 4294967295 134512640 134672761 3221224576 3221223760 134615794 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21958 20655 603 41 0 21917 0
vsize: 87832
[startup+370.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 28645 0 0 0 36847 142 0 0 25 0 1 0 421972546 89939968 20655 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21958 20655 603 41 0 21917 0
vsize: 87832
[startup+380.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 28645 0 0 0 37847 142 0 0 25 0 1 0 421972546 89939968 20655 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21958 20655 603 41 0 21917 0
vsize: 87832
[startup+390.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 28645 0 0 0 38848 142 0 0 25 0 1 0 421972546 89939968 20655 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21958 20655 603 41 0 21917 0
vsize: 87832
[startup+400.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 28645 0 0 0 39848 142 0 0 25 0 1 0 421972546 89935872 20654 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21957 20654 603 41 0 21916 0
vsize: 87828
[startup+410.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 28645 0 0 0 40848 142 0 0 25 0 1 0 421972546 89935872 20654 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21957 20654 603 41 0 21916 0
vsize: 87828
[startup+420.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 28645 0 0 0 41848 142 0 0 25 0 1 0 421972546 89935872 20654 4294967295 134512640 134672761 3221224576 3221223616 134612696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21957 20654 603 41 0 21916 0
vsize: 87828
[startup+430.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 28645 0 0 0 42848 142 0 0 25 0 1 0 421972546 89935872 20654 4294967295 134512640 134672761 3221224576 3221223616 134612840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21957 20654 603 41 0 21916 0
vsize: 87828
[startup+440.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 28645 0 0 0 43848 142 0 0 25 0 1 0 421972546 89935872 20654 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21957 20654 603 41 0 21916 0
vsize: 87828
[startup+450.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 28645 0 0 0 44849 142 0 0 25 0 1 0 421972546 89927680 20654 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21955 20654 603 41 0 21914 0
vsize: 87820
[startup+460.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 28645 0 0 0 45849 142 0 0 25 0 1 0 421972546 89927680 20654 4294967295 134512640 134672761 3221224576 3221223700 134566012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21955 20654 603 41 0 21914 0
vsize: 87820
[startup+470.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 28645 0 0 0 46849 142 0 0 25 0 1 0 421972546 89927680 20654 4294967295 134512640 134672761 3221224576 3221223616 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21955 20654 603 41 0 21914 0
vsize: 87820
[startup+480.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 28645 0 0 0 47849 142 0 0 25 0 1 0 421972546 89927680 20654 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21955 20654 603 41 0 21914 0
vsize: 87820
[startup+490.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 29991 0 0 0 48845 146 0 0 25 0 1 0 421972546 95469568 22000 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23308 22000 603 41 0 23267 0
vsize: 93232
[startup+500.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 31232 0 0 0 49843 148 0 0 25 0 1 0 421972546 100548608 23241 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24548 23241 603 41 0 24507 0
vsize: 98192
[startup+510.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 32785 0 0 0 50840 151 0 0 25 0 1 0 421972546 106872832 24794 4294967295 134512640 134672761 3221224576 3221223616 134612604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26092 24794 603 41 0 26051 0
vsize: 104368
[startup+520.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 33385 0 0 0 51839 153 0 0 25 0 1 0 421972546 109338624 25394 4294967295 134512640 134672761 3221224576 3221223680 134604307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26694 25394 603 41 0 26653 0
vsize: 106776
[startup+530.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 33385 0 0 0 52839 153 0 0 25 0 1 0 421972546 109338624 25394 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26694 25394 603 41 0 26653 0
vsize: 106776
[startup+540.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 33385 0 0 0 53839 153 0 0 25 0 1 0 421972546 109338624 25394 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26694 25394 603 41 0 26653 0
vsize: 106776
[startup+550.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 33385 0 0 0 54840 153 0 0 25 0 1 0 421972546 109338624 25394 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26694 25394 603 41 0 26653 0
vsize: 106776
[startup+560.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 33385 0 0 0 55840 153 0 0 25 0 1 0 421972546 109338624 25394 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26694 25394 603 41 0 26653 0
vsize: 106776
[startup+570.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 33385 0 0 0 56840 153 0 0 25 0 1 0 421972546 109338624 25394 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26694 25394 603 41 0 26653 0
vsize: 106776
[startup+580.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 34130 0 0 0 57838 155 0 0 25 0 1 0 421972546 112422912 26139 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27447 26139 603 41 0 27406 0
vsize: 109788
[startup+590.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 35361 0 0 0 58837 156 0 0 25 0 1 0 421972546 117538816 27370 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28696 27370 603 41 0 28655 0
vsize: 114784
[startup+600.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 35981 0 0 0 59836 158 0 0 25 0 1 0 421972546 119967744 27990 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29289 27990 603 41 0 29248 0
vsize: 117156
[startup+610.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 35981 0 0 0 60836 158 0 0 25 0 1 0 421972546 119967744 27990 4294967295 134512640 134672761 3221224576 3221223616 134612783 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29289 27990 603 41 0 29248 0
vsize: 117156
[startup+620.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 35981 0 0 0 61836 158 0 0 25 0 1 0 421972546 119967744 27990 4294967295 134512640 134672761 3221224576 3221223760 134615801 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29289 27990 603 41 0 29248 0
vsize: 117156
[startup+630.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 35981 0 0 0 62836 158 0 0 25 0 1 0 421972546 119967744 27990 4294967295 134512640 134672761 3221224576 3221223616 134603540 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29289 27990 603 41 0 29248 0
vsize: 117156
[startup+640.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 35981 0 0 0 63836 158 0 0 25 0 1 0 421972546 119967744 27990 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29289 27990 603 41 0 29248 0
vsize: 117156
[startup+650.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 35981 0 0 0 64837 158 0 0 25 0 1 0 421972546 119967744 27990 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29289 27990 603 41 0 29248 0
vsize: 117156
[startup+660.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 35981 0 0 0 65837 158 0 0 25 0 1 0 421972546 119795712 27951 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29247 27951 603 41 0 29206 0
vsize: 116988
[startup+670.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 35981 0 0 0 66837 158 0 0 25 0 1 0 421972546 119795712 27951 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29247 27951 603 41 0 29206 0
vsize: 116988
[startup+680.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 35981 0 0 0 67837 158 0 0 25 0 1 0 421972546 119795712 27951 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29247 27951 603 41 0 29206 0
vsize: 116988
[startup+690.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 35981 0 0 0 68837 158 0 0 25 0 1 0 421972546 119795712 27951 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29247 27951 603 41 0 29206 0
vsize: 116988
[startup+700.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 35981 0 0 0 69837 158 0 0 25 0 1 0 421972546 119795712 27951 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29247 27951 603 41 0 29206 0
vsize: 116988
[startup+710.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 35981 0 0 0 70838 158 0 0 25 0 1 0 421972546 119795712 27951 4294967295 134512640 134672761 3221224576 3221223760 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29247 27951 603 41 0 29206 0
vsize: 116988
[startup+720.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 35981 0 0 0 71838 158 0 0 25 0 1 0 421972546 119791616 27950 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29246 27950 603 41 0 29205 0
vsize: 116984
[startup+730.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 35981 0 0 0 72838 158 0 0 25 0 1 0 421972546 119791616 27950 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29246 27950 603 41 0 29205 0
vsize: 116984
[startup+740.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 35981 0 0 0 73838 158 0 0 25 0 1 0 421972546 119791616 27950 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29246 27950 603 41 0 29205 0
vsize: 116984
[startup+750.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 35981 0 0 0 74839 158 0 0 25 0 1 0 421972546 119791616 27950 4294967295 134512640 134672761 3221224576 3221223760 134615676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29246 27950 603 41 0 29205 0
vsize: 116984
[startup+760.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 35981 0 0 0 75839 158 0 0 25 0 1 0 421972546 119791616 27950 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29246 27950 603 41 0 29205 0
vsize: 116984
[startup+770.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 35981 0 0 0 76839 158 0 0 25 0 1 0 421972546 119791616 27950 4294967295 134512640 134672761 3221224576 3221223616 134614271 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29246 27950 603 41 0 29205 0
vsize: 116984
[startup+780.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 35981 0 0 0 77839 158 0 0 25 0 1 0 421972546 119791616 27950 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29246 27950 603 41 0 29205 0
vsize: 116984
[startup+790.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 35981 0 0 0 78839 158 0 0 25 0 1 0 421972546 119201792 27806 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29102 27806 603 41 0 29061 0
vsize: 116408
[startup+800.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 35981 0 0 0 79840 158 0 0 25 0 1 0 421972546 119201792 27806 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29102 27806 603 41 0 29061 0
vsize: 116408
[startup+810.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 35981 0 0 0 80840 158 0 0 25 0 1 0 421972546 119201792 27806 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29102 27806 603 41 0 29061 0
vsize: 116408
[startup+820.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 35981 0 0 0 81840 158 0 0 25 0 1 0 421972546 119201792 27806 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29102 27806 603 41 0 29061 0
vsize: 116408
[startup+830.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 35981 0 0 0 82840 158 0 0 25 0 1 0 421972546 119201792 27806 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29102 27806 603 41 0 29061 0
vsize: 116408
[startup+840.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 35981 0 0 0 83840 158 0 0 25 0 1 0 421972546 119201792 27806 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29102 27806 603 41 0 29061 0
vsize: 116408
[startup+850.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 35981 0 0 0 84841 158 0 0 25 0 1 0 421972546 119201792 27806 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29102 27806 603 41 0 29061 0
vsize: 116408
[startup+860.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 36436 0 0 0 85840 158 0 0 25 0 1 0 421972546 121122816 28261 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29571 28261 603 41 0 29530 0
vsize: 118284
[startup+870.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 37404 0 0 0 86838 161 0 0 25 0 1 0 421972546 125034496 29229 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30526 29229 603 41 0 30485 0
vsize: 122104
[startup+880.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 37404 0 0 0 87838 161 0 0 25 0 1 0 421972546 125034496 29229 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30526 29229 603 41 0 30485 0
vsize: 122104
[startup+890.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 37404 0 0 0 88838 161 0 0 25 0 1 0 421972546 125034496 29229 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30526 29229 603 41 0 30485 0
vsize: 122104
[startup+900.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 37404 0 0 0 89838 161 0 0 25 0 1 0 421972546 125034496 29229 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30526 29229 603 41 0 30485 0
vsize: 122104
[startup+910.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 37404 0 0 0 90839 161 0 0 25 0 1 0 421972546 125034496 29229 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30526 29229 603 41 0 30485 0
vsize: 122104
[startup+920.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 37404 0 0 0 91839 161 0 0 25 0 1 0 421972546 125034496 29229 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30526 29229 603 41 0 30485 0
vsize: 122104
[startup+930.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 37404 0 0 0 92839 161 0 0 25 0 1 0 421972546 125034496 29229 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30526 29229 603 41 0 30485 0
vsize: 122104
[startup+940.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 37404 0 0 0 93839 161 0 0 25 0 1 0 421972546 125034496 29229 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30526 29229 603 41 0 30485 0
vsize: 122104
[startup+950.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 37874 0 0 0 94838 162 0 0 25 0 1 0 421972546 127057920 29699 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31020 29699 603 41 0 30979 0
vsize: 124080
[startup+960.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 38070 0 0 0 95838 162 0 0 25 0 1 0 421972546 127758336 29894 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31191 29894 603 41 0 31150 0
vsize: 124764
[startup+970.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 38070 0 0 0 96838 162 0 0 25 0 1 0 421972546 127758336 29894 4294967295 134512640 134672761 3221224576 3221223712 134614739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31191 29894 603 41 0 31150 0
vsize: 124764
[startup+980.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 38070 0 0 0 97838 162 0 0 25 0 1 0 421972546 127758336 29894 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31191 29894 603 41 0 31150 0
vsize: 124764
[startup+990.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 38070 0 0 0 98839 162 0 0 25 0 1 0 421972546 127758336 29894 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31191 29894 603 41 0 31150 0
vsize: 124764
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 38070 0 0 0 99839 162 0 0 25 0 1 0 421972546 127758336 29894 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31191 29894 603 41 0 31150 0
vsize: 124764
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 38070 0 0 0 100839 162 0 0 25 0 1 0 421972546 127758336 29894 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31191 29894 603 41 0 31150 0
vsize: 124764
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 38070 0 0 0 101839 162 0 0 25 0 1 0 421972546 127758336 29894 4294967295 134512640 134672761 3221224576 3221223760 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31191 29894 603 41 0 31150 0
vsize: 124764
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 38070 0 0 0 102839 162 0 0 25 0 1 0 421972546 127758336 29894 4294967295 134512640 134672761 3221224576 3221223584 134522555 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31191 29894 603 41 0 31150 0
vsize: 124764
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 38762 0 0 0 103838 164 0 0 25 0 1 0 421972546 130723840 30586 4294967295 134512640 134672761 3221224576 3221223380 1075358820 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31915 30586 603 41 0 31874 0
vsize: 127660
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 38807 0 0 0 104838 164 0 0 25 0 1 0 421972546 130772992 30630 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31927 30630 603 41 0 31886 0
vsize: 127708
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 38807 0 0 0 105838 164 0 0 25 0 1 0 421972546 130772992 30630 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31927 30630 603 41 0 31886 0
vsize: 127708
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 38807 0 0 0 106838 164 0 0 25 0 1 0 421972546 130772992 30630 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31927 30630 603 41 0 31886 0
vsize: 127708
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 38807 0 0 0 107839 164 0 0 25 0 1 0 421972546 130772992 30630 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31927 30630 603 41 0 31886 0
vsize: 127708
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 38807 0 0 0 108839 164 0 0 25 0 1 0 421972546 130772992 30630 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31927 30630 603 41 0 31886 0
vsize: 127708
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 38807 0 0 0 109839 164 0 0 25 0 1 0 421972546 130772992 30630 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31927 30630 603 41 0 31886 0
vsize: 127708
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 38807 0 0 0 110839 164 0 0 25 0 1 0 421972546 130772992 30630 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31927 30630 603 41 0 31886 0
vsize: 127708
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 38807 0 0 0 111839 164 0 0 25 0 1 0 421972546 130772992 30630 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31927 30630 603 41 0 31886 0
vsize: 127708
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 38807 0 0 0 112840 164 0 0 25 0 1 0 421972546 130772992 30630 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31927 30630 603 41 0 31886 0
vsize: 127708
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 38807 0 0 0 113840 164 0 0 25 0 1 0 421972546 130772992 30630 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31927 30630 603 41 0 31886 0
vsize: 127708
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 39653 0 0 0 114838 166 0 0 25 0 1 0 421972546 134303744 31476 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32789 31476 603 41 0 32748 0
vsize: 131156
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 40887 0 0 0 115836 168 0 0 25 0 1 0 421972546 139472896 32710 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34051 32710 603 41 0 34010 0
vsize: 136204
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 42060 0 0 0 116835 170 0 0 25 0 1 0 421972546 144297984 33883 4294967295 134512640 134672761 3221224576 3221223616 134614266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35229 33883 603 41 0 35188 0
vsize: 140916
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 42250 0 0 0 117834 171 0 0 25 0 1 0 421972546 144990208 34069 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35398 34069 603 41 0 35357 0
vsize: 141592
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 42250 0 0 0 118834 171 0 0 25 0 1 0 421972546 144990208 34069 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35398 34069 603 41 0 35357 0
vsize: 141592
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26756
Raw data (stat): 26756 (minisat+) R 26755 22932 22931 0 -1 0 42250 0 0 0 119834 171 0 0 25 0 1 0 421972546 144990208 34069 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35398 34069 603 41 0 35357 0
vsize: 141592
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 26756
Raw data (stat): 26756 (minisat+) Z 26755 22932 22931 0 -1 12 42251 0 0 0 119835 180 0 0 25 0 1 0 421972546 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.11
CPU time (s): 1200.15
CPU user time (s): 1198.35
CPU system time (s): 1.80272
CPU usage (%): 100.003
Max. virtual memory (Kb): 141592
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####