PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-pp08a.opb
MD5SUM	962e64054cef66ff1ace4918a032c24a
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1983976
Optimality of the best value was proved	NO
Number of terms in the objective function	2304
Biggest coefficient in the objective function	1048576
Number of bits for the biggest coefficient in the objective function	21
Sum of the numbers in the objective function	178464600
Number of bits of the sum of numbers in the objective function	28
Biggest number in a constraint	1048576
Number of bits of the biggest number in a constraint	21
Biggest sum of numbers in a constraint	178464600
Number of bits of the biggest sum of numbers	28
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.01
Number of variables	3584
Total number of constraints	200
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	64
Number of constraints which are nor clauses,nor cardinality constraints	136
Minimum length of a constraint	1
Maximum length of a constraint	160
Trace number 18476

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc7 THE 2005-04-21 15:14:20 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17925 boxname=wulflinc7 idbench=1379 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  962e64054cef66ff1ace4918a032c24a  /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-pp08a.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-pp08a.opb /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-pp08a.opb
IDLAUNCH: 17925
/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:        470480 kB
Buffers:         26192 kB
Cached:         515628 kB
SwapCached:          4 kB
Active:         191492 kB
Inactive:       353156 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        470228 kB
SwapTotal:     2097136 kB
SwapFree:      2097128 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6940 kB
Slab:            13904 kB
Committed_AS:    63584 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 15:34:22 (client local time) WITH STATUS 0 IN 1200.27 SECONDS
stats: 17925 7 1200.27 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 200 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 198]---> BDD-cost:  158
c ---[ 196]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 195]---> BDD-cost:   21
c ---[ 194]---> BDD-cost:   21
c ---[ 193]---> BDD-cost:   21
c ---[ 192]---> BDD-cost:   21
c ---[ 191]---> BDD-cost:   23
c ---[ 190]---> BDD-cost:   18
c ---[ 189]---> BDD-cost:   18
c ---[ 188]---> BDD-cost:   18
c ---[ 187]---> BDD-cost:   18
c ---[ 186]---> BDD-cost:   18
c ---[ 184]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 183]---> BDD-cost:   18
c ---[ 182]---> BDD-cost:   18
c ---[ 181]---> BDD-cost:   18
c ---[ 180]---> BDD-cost:   24
c ---[ 179]---> BDD-cost:   24
c ---[ 178]---> BDD-cost:   24
c ---[ 177]---> BDD-cost:   21
c ---[ 176]---> BDD-cost:   21
c ---[ 175]---> BDD-cost:   21
c ---[ 174]---> BDD-cost:   21
c ---[ 172]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 171]---> BDD-cost:   21
c ---[ 170]---> BDD-cost:   19
c ---[ 169]---> BDD-cost:   19
c ---[ 168]---> BDD-cost:   19
c ---[ 167]---> BDD-cost:   19
c ---[ 166]---> BDD-cost:   19
c ---[ 165]---> BDD-cost:   19
c ---[ 164]---> BDD-cost:   19
c ---[ 163]---> BDD-cost:   19
c ---[ 162]---> BDD-cost:   19
c ---[ 160]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 159]---> BDD-cost:   19
c ---[ 158]---> BDD-cost:   19
c ---[ 157]---> BDD-cost:   19
c ---[ 156]---> BDD-cost:   19
c ---[ 155]---> BDD-cost:   19
c ---[ 154]---> BDD-cost:   19
c ---[ 153]---> BDD-cost:   19
c ---[ 151]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 149]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 147]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 145]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 143]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 141]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 139]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 137]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 135]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 133]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 131]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 129]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 127]---> BDD-cost:  158
c ---[ 125]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 123]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 121]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 119]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 117]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 115]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 113]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 111]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 109]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 107]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 105]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 103]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 101]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  99]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  97]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  95]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  93]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  91]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  89]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  87]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  85]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  83]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  81]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  79]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  77]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  75]---> BDD-cost:  154
c ---[  73]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  71]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  69]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  67]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  65]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  63]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  61]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  59]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  57]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  55]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  53]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  51]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  49]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  47]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  45]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  43]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  41]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  40]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  39]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  38]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  37]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  36]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  34]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  33]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  32]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  31]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  30]---> BDD-cost:   24
c ---[  29]---> BDD-cost:   24
c ---[  28]---> BDD-cost:   24
c ---[  27]---> BDD-cost:   21
c ---[  26]---> BDD-cost:   21
c ---[  25]---> BDD-cost:   21
c ---[  24]---> BDD-cost:   21
c ---[  22]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  21]---> BDD-cost:   23
c ---[  20]---> BDD-cost:   19
c ---[  19]---> BDD-cost:   19
c ---[  18]---> BDD-cost:   19
c ---[  17]---> BDD-cost:   19
c ---[  16]---> BDD-cost:   19
c ---[  15]---> BDD-cost:   19
c ---[  14]---> BDD-cost:   19
c ---[  13]---> BDD-cost:   19
c ---[  12]---> BDD-cost:   24
c ---[  10]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   9]---> BDD-cost:   24
c ---[   8]---> BDD-cost:   24
c ---[   7]---> BDD-cost:   21
c ---[   6]---> BDD-cost:   21
c ---[   5]---> BDD-cost:   21
c ---[   4]---> BDD-cost:   21
c ---[   3]---> BDD-cost:   23
c ---[   2]---> BDD-cost:   24
c ---[   1]---> BDD-cost:   24
c ---[   0]---> BDD-cost:   24
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  203261   478788 |   60978       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/66517          
c   -- var.elim.:  2000/66517          
c   -- var.elim.:  3000/66517          
c   -- var.elim.:  4000/66517          
c   -- var.elim.:  5000/66517          
c   -- var.elim.:  6000/66517          
c   -- var.elim.:  7000/66517          
c   -- var.elim.:  8000/66517          
c   -- var.elim.:  9000/66517          
c   -- var.elim.:  10000/66517          
c   -- var.elim.:  11000/66517          
c   -- var.elim.:  12000/66517          
c   -- var.elim.:  13000/66517          
c   -- var.elim.:  14000/66517          
c   -- var.elim.:  15000/66517          
c   -- var.elim.:  16000/66517          
c   -- var.elim.:  17000/66517          
c   -- var.elim.:  18000/66517          
c   -- var.elim.:  19000/66517          
c   -- var.elim.:  20000/66517          
c   -- var.elim.:  21000/66517          
c   -- var.elim.:  22000/66517          
c   -- var.elim.:  23000/66517          
c   -- var.elim.:  24000/66517          
c   -- var.elim.:  25000/66517          
c   -- var.elim.:  26000/66517          
c   -- var.elim.:  27000/66517          
c   -- var.elim.:  28000/66517          
c   -- var.elim.:  29000/66517          
c   -- var.elim.:  30000/66517          
c   -- var.elim.:  31000/66517          
c   -- var.elim.:  32000/66517          
c   -- var.elim.:  33000/66517          
c   -- var.elim.:  34000/66517          
c   -- var.elim.:  35000/66517          
c   -- var.elim.:  36000/66517          
c   -- var.elim.:  37000/66517          
c   -- var.elim.:  38000/66517          
c   -- var.elim.:  39000/66517          
c   -- var.elim.:  40000/66517          
c   -- var.elim.:  41000/66517          
c   -- var.elim.:  42000/66517          
c   -- var.elim.:  43000/66517          
c   -- var.elim.:  44000/66517          
c   -- var.elim.:  45000/66517          
c   -- var.elim.:  46000/66517          
c   -- var.elim.:  47000/66517          
c   -- var.elim.:  48000/66517          
c   -- var.elim.:  49000/66517          
c   -- var.elim.:  50000/66517          
c   -- var.elim.:  51000/66517          
c   -- var.elim.:  52000/66517          
c   -- var.elim.:  53000/66517          
c   -- var.elim.:  54000/66517          
c   -- var.elim.:  55000/66517          
c   -- var.elim.:  56000/66517          
c   -- var.elim.:  57000/66517          
c   -- var.elim.:  58000/66517          
c   -- var.elim.:  59000/66517          
c   -- var.elim.:  60000/66517          
c   -- var.elim.:  61000/66517          
c   -- var.elim.:  62000/66517          
c   -- var.elim.:  63000/66517          
c   -- var.elim.:  64000/66517          
c   -- var.elim.:  65000/66517          
c   -- var.elim.:  66000/66517          
c   -- var.elim.:  66517/66517          
c   -- var.elim.:  1000/36898          
c   -- var.elim.:  2000/36898          
c   -- var.elim.:  3000/36898          
c   -- var.elim.:  4000/36898          
c   -- var.elim.:  5000/36898          
c   -- var.elim.:  6000/36898          
c   -- var.elim.:  7000/36898          
c   -- var.elim.:  8000/36898          
c   -- var.elim.:  9000/36898          
c   -- var.elim.:  10000/36898          
c   -- var.elim.:  11000/36898          
c   -- var.elim.:  12000/36898          
c   -- var.elim.:  13000/36898          
c   -- var.elim.:  14000/36898          
c   -- var.elim.:  15000/36898          
c   -- var.elim.:  16000/36898          
c   -- var.elim.:  17000/36898          
c   -- var.elim.:  18000/36898          
c   -- var.elim.:  19000/36898          
c   -- var.elim.:  20000/36898          
c   -- var.elim.:  21000/36898          
c   -- var.elim.:  22000/36898          
c   -- var.elim.:  23000/36898          
c   -- var.elim.:  24000/36898          
c   -- var.elim.:  25000/36898          
c   -- var.elim.:  26000/36898          
c   -- var.elim.:  27000/36898          
c   -- var.elim.:  28000/36898          
c   -- var.elim.:  29000/36898          
c   -- var.elim.:  30000/36898          
c   -- var.elim.:  31000/36898          
c   -- var.elim.:  32000/36898          
c   -- var.eli#### 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.69 0.85 0.88 2/54 10316
Raw data (stat): 10316 (runsolver) R 10315 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487860135 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.0199 s]
Raw data (loadavg): 0.74 0.86 0.88 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 11088 0 0 0 968 32 0 0 25 0 1 0 487860135 51642368 10411 4294967295 134512640 134672761 3221224544 3221223056 134637231 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12608 10411 603 41 0 12567 0
vsize: 50432
[startup+20.0402 s]
Raw data (loadavg): 0.78 0.86 0.88 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 11556 0 0 0 1969 33 0 0 25 0 1 0 487860135 51789824 10446 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12644 10446 603 41 0 12603 0
vsize: 50576
[startup+30.0403 s]
Raw data (loadavg): 0.81 0.87 0.88 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 11567 0 0 0 2969 34 0 0 25 0 1 0 487860135 51986432 10457 4294967295 134512640 134672761 3221224544 3221223688 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12692 10457 603 41 0 12651 0
vsize: 50768
[startup+40.0407 s]
Raw data (loadavg): 0.84 0.87 0.88 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 11575 0 0 0 3968 34 0 0 25 0 1 0 487860135 51986432 10465 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12692 10465 603 41 0 12651 0
vsize: 50768
[startup+50.042 s]
Raw data (loadavg): 0.86 0.87 0.88 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 11582 0 0 0 4969 34 0 0 25 0 1 0 487860135 51986432 10472 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12692 10472 603 41 0 12651 0
vsize: 50768
[startup+60.0422 s]
Raw data (loadavg): 0.88 0.88 0.88 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 11586 0 0 0 5968 34 0 0 25 0 1 0 487860135 51986432 10476 4294967295 134512640 134672761 3221224544 3221223688 134616111 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12692 10476 603 41 0 12651 0
vsize: 50768
[startup+70.0433 s]
Raw data (loadavg): 0.90 0.88 0.88 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 11592 0 0 0 6968 35 0 0 25 0 1 0 487860135 51986432 10482 4294967295 134512640 134672761 3221224544 3221223712 134553613 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12692 10482 603 41 0 12651 0
vsize: 50768
[startup+80.0439 s]
Raw data (loadavg): 0.92 0.88 0.88 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 11629 0 0 0 7968 35 0 0 25 0 1 0 487860135 52248576 10519 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12756 10519 603 41 0 12715 0
vsize: 51024
[startup+90.0431 s]
Raw data (loadavg): 0.93 0.89 0.89 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 11634 0 0 0 8968 35 0 0 25 0 1 0 487860135 52248576 10524 4294967295 134512640 134672761 3221224544 3221223668 134566075 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12756 10524 603 41 0 12715 0
vsize: 51024
[startup+100.044 s]
Raw data (loadavg): 0.94 0.89 0.89 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 11637 0 0 0 9968 36 0 0 25 0 1 0 487860135 52248576 10527 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12756 10527 603 41 0 12715 0
vsize: 51024
[startup+110.045 s]
Raw data (loadavg): 0.95 0.89 0.89 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 11643 0 0 0 10967 36 0 0 25 0 1 0 487860135 52248576 10533 4294967295 134512640 134672761 3221224544 3221223728 134615526 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12756 10533 603 41 0 12715 0
vsize: 51024
[startup+120.045 s]
Raw data (loadavg): 0.96 0.90 0.89 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 11652 0 0 0 11967 36 0 0 25 0 1 0 487860135 52383744 10542 4294967295 134512640 134672761 3221224544 3221223728 134615585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12789 10542 603 41 0 12748 0
vsize: 51156
[startup+130.045 s]
Raw data (loadavg): 0.96 0.90 0.89 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 11687 0 0 0 12967 37 0 0 25 0 1 0 487860135 52518912 10577 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12822 10577 603 41 0 12781 0
vsize: 51288
[startup+140.046 s]
Raw data (loadavg): 0.97 0.90 0.89 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 11731 0 0 0 13966 38 0 0 25 0 1 0 487860135 52649984 10621 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12854 10621 603 41 0 12813 0
vsize: 51416
[startup+150.046 s]
Raw data (loadavg): 0.97 0.90 0.89 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 11827 0 0 0 14966 38 0 0 25 0 1 0 487860135 53338112 10717 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13022 10717 603 41 0 12981 0
vsize: 52088
[startup+160.046 s]
Raw data (loadavg): 0.98 0.91 0.89 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 11908 0 0 0 15966 38 0 0 25 0 1 0 487860135 53608448 10798 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13088 10798 603 41 0 13047 0
vsize: 52352
[startup+170.048 s]
Raw data (loadavg): 0.98 0.91 0.89 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 11995 0 0 0 16966 39 0 0 25 0 1 0 487860135 53878784 10885 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13154 10885 603 41 0 13113 0
vsize: 52616
[startup+180.048 s]
Raw data (loadavg): 0.98 0.91 0.89 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 12087 0 0 0 17965 40 0 0 25 0 1 0 487860135 54280192 10977 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13252 10977 603 41 0 13211 0
vsize: 53008
[startup+190.048 s]
Raw data (loadavg): 0.98 0.91 0.89 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 12171 0 0 0 18965 40 0 0 25 0 1 0 487860135 54685696 11061 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13351 11061 603 41 0 13310 0
vsize: 53404
[startup+200.049 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 12305 0 0 0 19964 41 0 0 25 0 1 0 487860135 55218176 11195 4294967295 134512640 134672761 3221224544 3221223744 134610646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13481 11195 603 41 0 13440 0
vsize: 53924
[startup+210.049 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 12414 0 0 0 20964 41 0 0 25 0 1 0 487860135 55619584 11304 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13579 11304 603 41 0 13538 0
vsize: 54316
[startup+220.05 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 12490 0 0 0 21964 42 0 0 25 0 1 0 487860135 55885824 11380 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13644 11380 603 41 0 13603 0
vsize: 54576
[startup+230.05 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 12629 0 0 0 22963 42 0 0 25 0 1 0 487860135 56414208 11519 4294967295 134512640 134672761 3221224544 3221223744 134610646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13773 11519 603 41 0 13732 0
vsize: 55092
[startup+240.05 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 12720 0 0 0 23963 42 0 0 25 0 1 0 487860135 56815616 11610 4294967295 134512640 134672761 3221224544 3221223728 134615761 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13871 11610 603 41 0 13830 0
vsize: 55484
[startup+250.051 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 12849 0 0 0 24963 43 0 0 25 0 1 0 487860135 57339904 11739 4294967295 134512640 134672761 3221224544 3221223716 134565154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13999 11739 603 41 0 13958 0
vsize: 55996
[startup+260.051 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 12966 0 0 0 25962 44 0 0 25 0 1 0 487860135 57741312 11856 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14097 11856 603 41 0 14056 0
vsize: 56388
[startup+270.051 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 13044 0 0 0 26962 44 0 0 25 0 1 0 487860135 58007552 11934 4294967295 134512640 134672761 3221224544 3221223728 134616023 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14162 11934 603 41 0 14121 0
vsize: 56648
[startup+280.051 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 13173 0 0 0 27961 45 0 0 25 0 1 0 487860135 58540032 12063 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14292 12063 603 41 0 14251 0
vsize: 57168
[startup+290.051 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 13306 0 0 0 28960 46 0 0 25 0 1 0 487860135 59064320 12196 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14420 12196 603 41 0 14379 0
vsize: 57680
[startup+300.051 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 13552 0 0 0 29959 47 0 0 25 0 1 0 487860135 60125184 12442 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14679 12442 603 41 0 14638 0
vsize: 58716
[startup+310.052 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 13644 0 0 0 30959 47 0 0 25 0 1 0 487860135 60919808 12534 4294967295 134512640 134672761 3221224544 3221223744 134610526 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14873 12534 603 41 0 14832 0
vsize: 59492
[startup+320.052 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 13746 0 0 0 31958 48 0 0 25 0 1 0 487860135 61448192 12636 4294967295 134512640 134672761 3221224544 3221223696 134614481 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15002 12636 603 41 0 14961 0
vsize: 60008
[startup+330.052 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 13952 0 0 0 32957 49 0 0 25 0 1 0 487860135 62246912 12842 4294967295 134512640 134672761 3221224544 3221223668 134566062 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15197 12842 603 41 0 15156 0
vsize: 60788
[startup+340.053 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 14136 0 0 0 33956 50 0 0 25 0 1 0 487860135 62914560 13026 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15360 13026 603 41 0 15319 0
vsize: 61440
[startup+350.053 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 14296 0 0 0 34956 51 0 0 25 0 1 0 487860135 63569920 13186 4294967295 134512640 134672761 3221224544 3221223728 134615985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15520 13186 603 41 0 15479 0
vsize: 62080
[startup+360.053 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 14721 0 0 0 35954 52 0 0 25 0 1 0 487860135 65294336 13611 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15941 13611 603 41 0 15900 0
vsize: 63764
[startup+370.053 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 15312 0 0 0 36953 54 0 0 25 0 1 0 487860135 67678208 14202 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16523 14202 603 41 0 16482 0
vsize: 66092
[startup+380.054 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 15441 0 0 0 37952 54 0 0 25 0 1 0 487860135 68218880 14331 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16655 14331 603 41 0 16614 0
vsize: 66620
[startup+390.054 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 15540 0 0 0 38952 55 0 0 25 0 1 0 487860135 68620288 14430 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16753 14430 603 41 0 16712 0
vsize: 67012
[startup+400.055 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 15681 0 0 0 39952 55 0 0 25 0 1 0 487860135 69148672 14571 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16882 14571 603 41 0 16841 0
vsize: 67528
[startup+410.055 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 15774 0 0 0 40951 56 0 0 25 0 1 0 487860135 69550080 14664 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16980 14664 603 41 0 16939 0
vsize: 67920
[startup+420.055 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 15884 0 0 0 41950 57 0 0 25 0 1 0 487860135 69951488 14774 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17078 14774 603 41 0 17037 0
vsize: 68312
[startup+430.056 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 16055 0 0 0 42950 57 0 0 25 0 1 0 487860135 70623232 14945 4294967295 134512640 134672761 3221224544 3221223728 134615591 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17242 14945 603 41 0 17201 0
vsize: 68968
[startup+440.055 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 16219 0 0 0 43950 58 0 0 25 0 1 0 487860135 71286784 15109 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17404 15109 603 41 0 17363 0
vsize: 69616
[startup+450.056 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 16337 0 0 0 44949 59 0 0 25 0 1 0 487860135 71815168 15227 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17533 15227 603 41 0 17492 0
vsize: 70132
[startup+460.057 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 16506 0 0 0 45949 59 0 0 25 0 1 0 487860135 72486912 15396 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17697 15396 603 41 0 17656 0
vsize: 70788
[startup+470.056 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 16610 0 0 0 46948 60 0 0 25 0 1 0 487860135 72888320 15500 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17795 15500 603 41 0 17754 0
vsize: 71180
[startup+480.056 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 16691 0 0 0 47948 60 0 0 25 0 1 0 487860135 73158656 15581 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17861 15581 603 41 0 17820 0
vsize: 71444
[startup+490.055 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 16847 0 0 0 48947 61 0 0 25 0 1 0 487860135 73830400 15737 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18025 15737 603 41 0 17984 0
vsize: 72100
[startup+500.056 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 16961 0 0 0 49947 62 0 0 25 0 1 0 487860135 74231808 15851 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18123 15851 603 41 0 18082 0
vsize: 72492
[startup+510.056 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 17047 0 0 0 50947 62 0 0 25 0 1 0 487860135 74633216 15937 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18221 15937 603 41 0 18180 0
vsize: 72884
[startup+520.056 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 17193 0 0 0 51946 62 0 0 25 0 1 0 487860135 75165696 16083 4294967295 134512640 134672761 3221224544 3221223668 134566142 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18351 16083 603 41 0 18310 0
vsize: 73404
[startup+530.056 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 17308 0 0 0 52946 63 0 0 25 0 1 0 487860135 75567104 16198 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18449 16198 603 41 0 18408 0
vsize: 73796
[startup+540.056 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 17471 0 0 0 53945 64 0 0 25 0 1 0 487860135 76234752 16361 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18612 16361 603 41 0 18571 0
vsize: 74448
[startup+550.056 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 17769 0 0 0 54945 65 0 0 25 0 1 0 487860135 77430784 16659 4294967295 134512640 134672761 3221224544 3221223728 134615752 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18904 16659 603 41 0 18863 0
vsize: 75616
[startup+560.056 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 18035 0 0 0 55944 66 0 0 25 0 1 0 487860135 78491648 16925 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19163 16925 603 41 0 19122 0
vsize: 76652
[startup+570.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 18225 0 0 0 56942 67 0 0 25 0 1 0 487860135 79286272 17115 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19357 17115 603 41 0 19316 0
vsize: 77428
[startup+580.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 18301 0 0 0 57942 67 0 0 25 0 1 0 487860135 79548416 17191 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19421 17191 603 41 0 19380 0
vsize: 77684
[startup+590.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 18391 0 0 0 58942 68 0 0 25 0 1 0 487860135 79949824 17281 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19519 17281 603 41 0 19478 0
vsize: 78076
[startup+600.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 18540 0 0 0 59941 68 0 0 25 0 1 0 487860135 80613376 17430 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19681 17430 603 41 0 19640 0
vsize: 78724
[startup+610.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 18692 0 0 0 60941 69 0 0 25 0 1 0 487860135 81145856 17582 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19811 17582 603 41 0 19770 0
vsize: 79244
[startup+620.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 18771 0 0 0 61941 69 0 0 25 0 1 0 487860135 81551360 17661 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19910 17661 603 41 0 19869 0
vsize: 79640
[startup+630.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 18902 0 0 0 62941 69 0 0 25 0 1 0 487860135 81948672 17792 4294967295 134512640 134672761 3221224544 3221223536 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20007 17792 603 41 0 19966 0
vsize: 80028
[startup+640.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 19354 0 0 0 63940 70 0 0 25 0 1 0 487860135 84865024 18244 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20719 18244 603 41 0 20678 0
vsize: 82876
[startup+650.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 19975 0 0 0 64939 72 0 0 25 0 1 0 487860135 87375872 18865 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21332 18865 603 41 0 21291 0
vsize: 85328
[startup+660.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 20162 0 0 0 65938 73 0 0 25 0 1 0 487860135 88166400 19052 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21525 19052 603 41 0 21484 0
vsize: 86100
[startup+670.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 20349 0 0 0 66938 73 0 0 25 0 1 0 487860135 88956928 19239 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21718 19239 603 41 0 21677 0
vsize: 86872
[startup+680.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 20573 0 0 0 67937 74 0 0 25 0 1 0 487860135 89747456 19463 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21911 19463 603 41 0 21870 0
vsize: 87644
[startup+690.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 20861 0 0 0 68937 75 0 0 25 0 1 0 487860135 90939392 19751 4294967295 134512640 134672761 3221224544 3221223668 134566029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22202 19751 603 41 0 22161 0
vsize: 88808
[startup+700.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 21644 0 0 0 69935 77 0 0 25 0 1 0 487860135 94105600 20534 4294967295 134512640 134672761 3221224544 3221223728 134615964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22975 20534 603 41 0 22934 0
vsize: 91900
[startup+710.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 21839 0 0 0 70935 77 0 0 25 0 1 0 487860135 94900224 20729 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23169 20729 603 41 0 23128 0
vsize: 92676
[startup+720.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 22065 0 0 0 71934 78 0 0 25 0 1 0 487860135 95830016 20955 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23396 20956 603 41 0 23355 0
vsize: 93584
[startup+730.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 22318 0 0 0 72933 79 0 0 25 0 1 0 487860135 96894976 21208 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23656 21208 603 41 0 23615 0
vsize: 94624
[startup+740.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 22598 0 0 0 73933 80 0 0 25 0 1 0 487860135 97955840 21488 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23915 21488 603 41 0 23874 0
vsize: 95660
[startup+750.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 22745 0 0 0 74932 80 0 0 25 0 1 0 487860135 98623488 21635 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24078 21635 603 41 0 24037 0
vsize: 96312
[startup+760.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 22938 0 0 0 75932 81 0 0 25 0 1 0 487860135 99291136 21828 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24241 21828 603 41 0 24200 0
vsize: 96964
[startup+770.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 23207 0 0 0 76931 82 0 0 25 0 1 0 487860135 100487168 22097 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24533 22097 603 41 0 24492 0
vsize: 98132
[startup+780.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 23480 0 0 0 77930 83 0 0 25 0 1 0 487860135 101560320 22370 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24795 22370 603 41 0 24754 0
vsize: 99180
[startup+790.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 23801 0 0 0 78929 84 0 0 25 0 1 0 487860135 102760448 22691 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25088 22691 603 41 0 25047 0
vsize: 100352
[startup+800.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 24030 0 0 0 79928 85 0 0 25 0 1 0 487860135 103698432 22920 4294967295 134512640 134672761 3221224544 3221223584 134612632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25317 22920 603 41 0 25276 0
vsize: 101268
[startup+810.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 24228 0 0 0 80927 86 0 0 25 0 1 0 487860135 104501248 23118 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25513 23118 603 41 0 25472 0
vsize: 102052
[startup+820.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 24454 0 0 0 81927 87 0 0 25 0 1 0 487860135 105431040 23344 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25740 23344 603 41 0 25699 0
vsize: 102960
[startup+830.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 24630 0 0 0 82926 88 0 0 25 0 1 0 487860135 106094592 23520 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25902 23520 603 41 0 25861 0
vsize: 103608
[startup+840.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 83925 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26628 24048 603 41 0 26587 0
vsize: 106512
[startup+850.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 84925 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26628 24048 603 41 0 26587 0
vsize: 106512
[startup+860.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 85925 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26628 24048 603 41 0 26587 0
vsize: 106512
[startup+870.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 86925 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26628 24048 603 41 0 26587 0
vsize: 106512
[startup+880.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 87925 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223696 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26628 24048 603 41 0 26587 0
vsize: 106512
[startup+890.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 88925 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223680 134614753 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26628 24048 603 41 0 26587 0
vsize: 106512
[startup+900.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 89926 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26628 24048 603 41 0 26587 0
vsize: 106512
[startup+910.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 90926 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223712 134564729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26628 24048 603 41 0 26587 0
vsize: 106512
[startup+920.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 91926 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26628 24048 603 41 0 26587 0
vsize: 106512
[startup+930.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 92926 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26628 24048 603 41 0 26587 0
vsize: 106512
[startup+940.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 93926 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26628 24048 603 41 0 26587 0
vsize: 106512
[startup+950.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 94927 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26628 24048 603 41 0 26587 0
vsize: 106512
[startup+960.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 95927 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26628 24048 603 41 0 26587 0
vsize: 106512
[startup+970.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 96927 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26628 24048 603 41 0 26587 0
vsize: 106512
[startup+980.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 97927 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26628 24048 603 41 0 26587 0
vsize: 106512
[startup+990.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 98927 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26628 24048 603 41 0 26587 0
vsize: 106512
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 99928 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223680 134614724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26628 24048 603 41 0 26587 0
vsize: 106512
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 100928 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26628 24048 603 41 0 26587 0
vsize: 106512
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 101928 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26628 24048 603 41 0 26587 0
vsize: 106512
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 102928 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26628 24048 603 41 0 26587 0
vsize: 106512
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 103928 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26628 24048 603 41 0 26587 0
vsize: 106512
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 104928 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26628 24048 603 41 0 26587 0
vsize: 106512
[startup+1060.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 105929 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26628 24048 603 41 0 26587 0
vsize: 106512
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 106929 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26628 24048 603 41 0 26587 0
vsize: 106512
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 107929 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26628 24048 603 41 0 26587 0
vsize: 106512
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 108929 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223680 134614800 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26628 24048 603 41 0 26587 0
vsize: 106512
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 109929 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223712 134614516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26628 24048 603 41 0 26587 0
vsize: 106512
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 110930 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26628 24048 603 41 0 26587 0
vsize: 106512
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 111930 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26628 24048 603 41 0 26587 0
vsize: 106512
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 112930 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26628 24048 603 41 0 26587 0
vsize: 106512
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 113930 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615505 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26628 24048 603 41 0 26587 0
vsize: 106512
[startup+1150.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 114930 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26628 24048 603 41 0 26587 0
vsize: 106512
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 115930 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26628 24048 603 41 0 26587 0
vsize: 106512
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 116931 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26628 24048 603 41 0 26587 0
vsize: 106512
[startup+1180.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 117931 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26628 24048 603 41 0 26587 0
vsize: 106512
[startup+1190.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 118931 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26628 24048 603 41 0 26587 0
vsize: 106512
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10316
Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 119931 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26628 24048 603 41 0 26587 0
vsize: 106512
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 10316
Raw data (stat): 10316 (minisat+) Z 10315 22932 22931 0 -1 12 25502 0 0 0 119931 95 0 0 25 0 1 0 487860135 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: 0
Real time (s): 1200.11
CPU time (s): 1200.27
CPU user time (s): 1199.32
CPU system time (s): 0.952855
CPU usage (%): 100.014
Max. virtual memory (Kb): 106512
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####