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/miplib3/normalized-mps-v2-13-7-pp08a.opb
MD5SUM	d14265fdf4e5a3ef733af1f15b884cbe
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	6661373
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.02
Number of variables	3584
Total number of constraints	136
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	136
Minimum length of a constraint	21
Maximum length of a constraint	160
Trace number 14978

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        826196 kB
Buffers:         19984 kB
Cached:         160152 kB
SwapCached:        540 kB
Active:          83820 kB
Inactive:        98232 kB
HighTotal:      131008 kB
HighFree:        18144 kB
LowTotal:       903652 kB
LowFree:        808052 kB
SwapTotal:     2097892 kB
SwapFree:      2096468 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            20732 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 02:39:58 (client local time) WITH STATUS 0 IN 1200.27 SECONDS
stats: 18783 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 ---[ 199]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 198]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 197]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 196]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 195]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 194]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 193]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 192]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 190]---> BDD-cost:  158
c ---[ 188]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 186]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 184]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 182]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 180]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 178]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 176]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 174]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
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 ---[ 170]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 168]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 166]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 164]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 162]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 160]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 158]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 156]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 154]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 152]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 150]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 148]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 146]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 144]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 142]---> BDD-cost:  158
c ---[ 140]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 138]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 136]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 134]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 132]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 130]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 128]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 126]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 124]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 122]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 120]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 118]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 116]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 114]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 112]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 110]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 108]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 106]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 104]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 102]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 100]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  98]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  96]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  94]---> BDD-cost:  154
c ---[  92]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  90]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  88]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  86]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  84]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  82]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  80]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  78]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  76]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  74]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  72]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  70]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  68]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  66]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  64]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  63]---> BDD-cost:   24
c ---[  62]---> BDD-cost:   24
c ---[  61]---> BDD-cost:   24
c ---[  60]---> BDD-cost:   21
c ---[  59]---> BDD-cost:   21
c ---[  58]---> BDD-cost:   21
c ---[  57]---> BDD-cost:   21
c ---[  56]---> BDD-cost:   23
c ---[  55]---> BDD-cost:   19
c ---[  54]---> BDD-cost:   19
c ---[  53]---> BDD-cost:   19
c ---[  52]---> BDD-cost:   19
c ---[  51]---> BDD-cost:   19
c ---[  50]---> BDD-cost:   19
c ---[  49]---> BDD-cost:   19
c ---[  48]---> BDD-cost:   19
c ---[  47]---> BDD-cost:   24
c ---[  46]---> BDD-cost:   24
c ---[  45]---> BDD-cost:   24
c ---[  44]---> BDD-cost:   21
c ---[  43]---> BDD-cost:   21
c ---[  42]---> BDD-cost:   21
c ---[  41]---> BDD-cost:   21
c ---[  40]---> BDD-cost:   23
c ---[  39]---> BDD-cost:   24
c ---[  38]---> BDD-cost:   24
c ---[  37]---> BDD-cost:   24
c ---[  36]---> BDD-cost:   21
c ---[  35]---> BDD-cost:   21
c ---[  34]---> BDD-cost:   21
c ---[  33]---> BDD-cost:   21
c ---[  32]---> BDD-cost:   23
c ---[  31]---> BDD-cost:   18
c ---[  30]---> BDD-cost:   18
c ---[  29]---> BDD-cost:   18
c ---[  28]---> BDD-cost:   18
c ---[  27]---> BDD-cost:   18
c ---[  26]---> BDD-cost:   18
c ---[  25]---> BDD-cost:   18
c ---[  24]---> BDD-cost:   18
c ---[  23]---> BDD-cost:   24
c ---[  22]---> BDD-cost:   24
c ---[  21]---> BDD-cost:   24
c ---[  20]---> BDD-cost:   21
c ---[  19]---> BDD-cost:   21
c ---[  18]---> BDD-cost:   21
c ---[  17]---> BDD-cost:   21
c ---[  16]---> BDD-cost:   21
c ---[  15]---> BDD-cost:   19
c ---[  14]---> BDD-cost:   19
c ---[  13]---> BDD-cost:   19
c ---[  12]---> BDD-cost:   19
c ---[  11]---> BDD-cost:   19
c ---[  10]---> BDD-cost:   19
c ---[   9]---> BDD-cost:   19
c ---[   8]---> BDD-cost:   19
c ---[   7]---> BDD-cost:   19
c ---[   6]---> BDD-cost:   19
c ---[   5]---> BDD-cost:   19
c ---[   4]---> BDD-cost:   19
c ---[   3]---> BDD-cost:   19
c ---[   2]---> BDD-cost:   19
c ---[   1]---> BDD-cost:   19
c ---[   0]---> BDD-cost:   19
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/36904          
c   -- var.elim.:  2000/36904          
c   -- var.elim.:  3000/36904          
c   -- var.elim.:  4000/36904          
c   -- var.elim.:  5000/36904          
c   -- var.elim.:  6000/36904          
c   -- var.elim.:  7000/36904          
c   -- var.elim.:  8000/36904          
c   -- var.elim.:  9000/36904          
c   -- var.elim.:  10000/36904          
c   -- var.elim.:  11000/36904          
c   -- var.elim.:  12000/36904          
c   -- var.elim.:  13000/36904          
c   -- var.elim.:  14000/36904          
c   -- var.elim.:  15000/36904          
c   -- var.elim.:  16000/36904          
c   -- var.elim.:  17000/36904          
c   -- var.elim.:  18000/36904          
c   -- var.elim.:  19000/36904          
c   -- var.elim.:  20000/36904          
c   -- var.elim.:  21000/36904          
c   -- var.elim.:  22000/36904          
c   -- var.elim.:  23000/36904          
c   -- var.elim.:  24000/36904          
c   -- var.elim.:  25000/36904          
c   -- var.elim.:  26000/36904          
c   -- var.elim.:  27000/36904          
c   -- var.elim.:  28000/36904          
c   -- var.elim.:  29000/36904          
c   -- var.elim.:  30000/36904          
c   -- var.elim.:  31000/36904          
c   -- var.elim.:  32000/36904          
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.54 0.81 0.86 2/54 19847
Raw data (stat): 19847 (runsolver) R 19846 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 541415519 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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+9.99991 s]
Raw data (loadavg): 0.61 0.81 0.86 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 10924 0 0 0 963 35 0 0 25 0 1 0 541415519 52060160 10420 4294967295 134512640 134672761 3221224544 3221223044 1074972061 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12710 10420 603 41 0 12669 0
vsize: 50840
[startup+19.9997 s]
Raw data (loadavg): 0.67 0.82 0.86 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 11655 0 0 0 1961 37 0 0 25 0 1 0 541415519 52584448 10519 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12838 10519 603 41 0 12797 0
vsize: 51352
[startup+30.001 s]
Raw data (loadavg): 0.72 0.82 0.86 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 12210 0 0 0 2959 39 0 0 25 0 1 0 541415519 54841344 11074 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13389 11074 603 41 0 13348 0
vsize: 53556
[startup+40.0007 s]
Raw data (loadavg): 0.76 0.83 0.86 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 12793 0 0 0 3956 42 0 0 25 0 1 0 541415519 57221120 11657 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13970 11657 603 41 0 13929 0
vsize: 55880
[startup+50.0014 s]
Raw data (loadavg): 0.80 0.83 0.86 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 13300 0 0 0 4955 43 0 0 25 0 1 0 541415519 59224064 12164 4294967295 134512640 134672761 3221224544 3221223584 134614333 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14459 12164 603 41 0 14418 0
vsize: 57836
[startup+60.0018 s]
Raw data (loadavg): 0.83 0.84 0.86 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 13730 0 0 0 5953 45 0 0 25 0 1 0 541415519 61210624 12594 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14944 12594 603 41 0 14903 0
vsize: 59776
[startup+70.0012 s]
Raw data (loadavg): 0.85 0.84 0.87 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 13980 0 0 0 6952 46 0 0 25 0 1 0 541415519 62300160 12844 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15210 12844 603 41 0 15169 0
vsize: 60840
[startup+80.0021 s]
Raw data (loadavg): 0.88 0.85 0.87 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 14289 0 0 0 7951 48 0 0 25 0 1 0 541415519 63623168 13153 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15533 13153 603 41 0 15492 0
vsize: 62132
[startup+90.0023 s]
Raw data (loadavg): 0.89 0.85 0.87 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 14589 0 0 0 8951 49 0 0 25 0 1 0 541415519 64704512 13453 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15797 13453 603 41 0 15756 0
vsize: 63188
[startup+100.003 s]
Raw data (loadavg): 0.91 0.86 0.87 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 14870 0 0 0 9950 49 0 0 25 0 1 0 541415519 65892352 13734 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16087 13734 603 41 0 16046 0
vsize: 64348
[startup+110.004 s]
Raw data (loadavg): 0.92 0.86 0.87 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 15206 0 0 0 10949 51 0 0 25 0 1 0 541415519 67215360 14070 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16410 14070 603 41 0 16369 0
vsize: 65640
[startup+120.004 s]
Raw data (loadavg): 0.93 0.87 0.87 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 15616 0 0 0 11948 52 0 0 25 0 1 0 541415519 68931584 14480 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16829 14480 603 41 0 16788 0
vsize: 67316
[startup+130.005 s]
Raw data (loadavg): 0.94 0.87 0.87 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 15901 0 0 0 12947 53 0 0 25 0 1 0 541415519 70131712 14765 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17122 14765 603 41 0 17081 0
vsize: 68488
[startup+140.005 s]
Raw data (loadavg): 0.95 0.87 0.87 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 16191 0 0 0 13947 54 0 0 25 0 1 0 541415519 71319552 15055 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17412 15055 603 41 0 17371 0
vsize: 69648
[startup+150.006 s]
Raw data (loadavg): 0.96 0.88 0.87 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 16461 0 0 0 14945 55 0 0 25 0 1 0 541415519 72380416 15325 4294967295 134512640 134672761 3221224544 3221223688 134616317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17671 15325 603 41 0 17630 0
vsize: 70684
[startup+160.006 s]
Raw data (loadavg): 0.96 0.88 0.87 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 16671 0 0 0 15944 56 0 0 25 0 1 0 541415519 73170944 15535 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17864 15535 603 41 0 17823 0
vsize: 71456
[startup+170.005 s]
Raw data (loadavg): 0.97 0.88 0.88 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 16993 0 0 0 16944 57 0 0 25 0 1 0 541415519 74506240 15857 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18190 15857 603 41 0 18149 0
vsize: 72760
[startup+180.007 s]
Raw data (loadavg): 0.97 0.89 0.88 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 17185 0 0 0 17943 58 0 0 25 0 1 0 541415519 75304960 16049 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18385 16049 603 41 0 18344 0
vsize: 73540
[startup+190.006 s]
Raw data (loadavg): 0.98 0.89 0.88 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 17358 0 0 0 18943 58 0 0 25 0 1 0 541415519 75964416 16222 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18546 16222 603 41 0 18505 0
vsize: 74184
[startup+200.007 s]
Raw data (loadavg): 0.98 0.89 0.88 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 17502 0 0 0 19942 59 0 0 25 0 1 0 541415519 77053952 16366 4294967295 134512640 134672761 3221224544 3221223696 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18812 16366 603 41 0 18771 0
vsize: 75248
[startup+210.007 s]
Raw data (loadavg): 0.98 0.90 0.88 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 17629 0 0 0 20942 60 0 0 25 0 1 0 541415519 77606912 16493 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18947 16493 603 41 0 18906 0
vsize: 75788
[startup+220.007 s]
Raw data (loadavg): 0.98 0.90 0.88 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 17855 0 0 0 21941 60 0 0 25 0 1 0 541415519 78536704 16719 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19174 16719 603 41 0 19133 0
vsize: 76696
[startup+230.008 s]
Raw data (loadavg): 0.99 0.90 0.88 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 18095 0 0 0 22941 61 0 0 25 0 1 0 541415519 79474688 16959 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19403 16959 603 41 0 19362 0
vsize: 77612
[startup+240.008 s]
Raw data (loadavg): 0.99 0.91 0.88 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 18309 0 0 0 23940 62 0 0 25 0 1 0 541415519 80412672 17173 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19632 17173 603 41 0 19591 0
vsize: 78528
[startup+250.009 s]
Raw data (loadavg): 0.99 0.91 0.88 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 18526 0 0 0 24940 63 0 0 25 0 1 0 541415519 81203200 17390 4294967295 134512640 134672761 3221224544 3221223728 134615830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19825 17390 603 41 0 19784 0
vsize: 79300
[startup+260.008 s]
Raw data (loadavg): 0.99 0.91 0.88 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 18656 0 0 0 25940 63 0 0 25 0 1 0 541415519 81747968 17520 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19958 17520 603 41 0 19917 0
vsize: 79832
[startup+270.008 s]
Raw data (loadavg): 0.99 0.91 0.89 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 18765 0 0 0 26940 63 0 0 25 0 1 0 541415519 82149376 17629 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20056 17629 603 41 0 20015 0
vsize: 80224
[startup+280.009 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 18870 0 0 0 27940 63 0 0 25 0 1 0 541415519 82681856 17734 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20186 17734 603 41 0 20145 0
vsize: 80744
[startup+290.009 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 19022 0 0 0 28939 64 0 0 25 0 1 0 541415519 83234816 17886 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20321 17886 603 41 0 20280 0
vsize: 81284
[startup+300.01 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 19195 0 0 0 29939 65 0 0 25 0 1 0 541415519 84029440 18059 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20515 18059 603 41 0 20474 0
vsize: 82060
[startup+310.01 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 19407 0 0 0 30938 65 0 0 25 0 1 0 541415519 84819968 18271 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20708 18271 603 41 0 20667 0
vsize: 82832
[startup+320.01 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 19617 0 0 0 31938 66 0 0 25 0 1 0 541415519 85757952 18481 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20937 18481 603 41 0 20896 0
vsize: 83748
[startup+330.01 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 19737 0 0 0 32938 66 0 0 25 0 1 0 541415519 86151168 18601 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21033 18601 603 41 0 20992 0
vsize: 84132
[startup+340.011 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 19876 0 0 0 33938 66 0 0 25 0 1 0 541415519 86810624 18740 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21194 18740 603 41 0 21153 0
vsize: 84776
[startup+350.011 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 20002 0 0 0 34937 67 0 0 25 0 1 0 541415519 87207936 18866 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21291 18866 603 41 0 21250 0
vsize: 85164
[startup+360.012 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 20170 0 0 0 35936 68 0 0 25 0 1 0 541415519 87875584 19034 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21454 19034 603 41 0 21413 0
vsize: 85816
[startup+370.012 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 20381 0 0 0 36935 69 0 0 25 0 1 0 541415519 88870912 19245 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21697 19245 603 41 0 21656 0
vsize: 86788
[startup+380.012 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 20624 0 0 0 37934 70 0 0 25 0 1 0 541415519 89788416 19488 4294967295 134512640 134672761 3221224544 3221223728 134616017 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21921 19488 603 41 0 21880 0
vsize: 87684
[startup+390.012 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 20866 0 0 0 38934 71 0 0 25 0 1 0 541415519 90845184 19730 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22179 19730 603 41 0 22138 0
vsize: 88716
[startup+400.013 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 21081 0 0 0 39933 71 0 0 25 0 1 0 541415519 91635712 19945 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22372 19945 603 41 0 22331 0
vsize: 89488
[startup+410.014 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 21234 0 0 0 40933 71 0 0 25 0 1 0 541415519 92299264 20098 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22534 20098 603 41 0 22493 0
vsize: 90136
[startup+420.014 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 21418 0 0 0 41933 72 0 0 25 0 1 0 541415519 92966912 20282 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22697 20282 603 41 0 22656 0
vsize: 90788
[startup+430.015 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 21589 0 0 0 42933 72 0 0 25 0 1 0 541415519 93757440 20453 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22890 20453 603 41 0 22849 0
vsize: 91560
[startup+440.016 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 21697 0 0 0 43933 73 0 0 25 0 1 0 541415519 94154752 20561 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22987 20561 603 41 0 22946 0
vsize: 91948
[startup+450.016 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 21856 0 0 0 44933 73 0 0 25 0 1 0 541415519 94818304 20720 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23149 20720 603 41 0 23108 0
vsize: 92596
[startup+460.015 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 21994 0 0 0 45932 73 0 0 25 0 1 0 541415519 95358976 20858 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23281 20858 603 41 0 23240 0
vsize: 93124
[startup+470.015 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 22156 0 0 0 46932 74 0 0 25 0 1 0 541415519 96071680 21020 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23455 21020 603 41 0 23414 0
vsize: 93820
[startup+480.017 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 22328 0 0 0 47932 74 0 0 25 0 1 0 541415519 96739328 21192 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23618 21192 603 41 0 23577 0
vsize: 94472
[startup+490.018 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 22483 0 0 0 48932 75 0 0 25 0 1 0 541415519 97394688 21347 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23778 21347 603 41 0 23737 0
vsize: 95112
[startup+500.018 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 22627 0 0 0 49931 75 0 0 25 0 1 0 541415519 98025472 21491 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23932 21491 603 41 0 23891 0
vsize: 95728
[startup+510.018 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 22781 0 0 0 50931 76 0 0 25 0 1 0 541415519 98553856 21645 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24061 21645 603 41 0 24020 0
vsize: 96244
[startup+520.018 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 22932 0 0 0 51931 76 0 0 25 0 1 0 541415519 99209216 21796 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24221 21796 603 41 0 24180 0
vsize: 96884
[startup+530.019 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 23082 0 0 0 52930 77 0 0 25 0 1 0 541415519 99774464 21946 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24359 21946 603 41 0 24318 0
vsize: 97436
[startup+540.019 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 23228 0 0 0 53930 77 0 0 25 0 1 0 541415519 100429824 22092 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24519 22092 603 41 0 24478 0
vsize: 98076
[startup+550.02 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 23357 0 0 0 54930 78 0 0 25 0 1 0 541415519 100872192 22221 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24627 22221 603 41 0 24586 0
vsize: 98508
[startup+560.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 23457 0 0 0 55930 78 0 0 25 0 1 0 541415519 101318656 22321 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24736 22321 603 41 0 24695 0
vsize: 98944
[startup+570.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 23646 0 0 0 56930 78 0 0 25 0 1 0 541415519 102178816 22510 4294967295 134512640 134672761 3221224544 3221223728 134615801 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24946 22510 603 41 0 24905 0
vsize: 99784
[startup+580.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 23801 0 0 0 57929 79 0 0 25 0 1 0 541415519 102834176 22665 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25106 22665 603 41 0 25065 0
vsize: 100424
[startup+590.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 23942 0 0 0 58929 80 0 0 25 0 1 0 541415519 103395328 22806 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25243 22806 603 41 0 25202 0
vsize: 100972
[startup+600.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 24124 0 0 0 59928 80 0 0 25 0 1 0 541415519 104235008 22988 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25448 22988 603 41 0 25407 0
vsize: 101792
[startup+610.022 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 24282 0 0 0 60928 81 0 0 25 0 1 0 541415519 104804352 23146 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25587 23146 603 41 0 25546 0
vsize: 102348
[startup+620.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 24390 0 0 0 61927 81 0 0 25 0 1 0 541415519 105336832 23254 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25717 23254 603 41 0 25676 0
vsize: 102868
[startup+630.022 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 24511 0 0 0 62927 82 0 0 25 0 1 0 541415519 105738240 23375 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25815 23375 603 41 0 25774 0
vsize: 103260
[startup+640.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 24614 0 0 0 63927 82 0 0 25 0 1 0 541415519 106143744 23478 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25914 23478 603 41 0 25873 0
vsize: 103656
[startup+650.022 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 24761 0 0 0 64927 83 0 0 25 0 1 0 541415519 106676224 23625 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26044 23625 603 41 0 26003 0
vsize: 104176
[startup+660.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 24900 0 0 0 65926 83 0 0 25 0 1 0 541415519 107339776 23764 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26206 23764 603 41 0 26165 0
vsize: 104824
[startup+670.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 25015 0 0 0 66926 83 0 0 25 0 1 0 541415519 107745280 23879 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26305 23879 603 41 0 26264 0
vsize: 105220
[startup+680.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 25114 0 0 0 67926 84 0 0 25 0 1 0 541415519 108138496 23978 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26401 23978 603 41 0 26360 0
vsize: 105604
[startup+690.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 25177 0 0 0 68926 84 0 0 25 0 1 0 541415519 108404736 24041 4294967295 134512640 134672761 3221224544 3221223688 134616126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26466 24041 603 41 0 26425 0
vsize: 105864
[startup+700.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 25264 0 0 0 69926 85 0 0 25 0 1 0 541415519 108818432 24128 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26567 24128 603 41 0 26526 0
vsize: 106268
[startup+710.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 25354 0 0 0 70925 85 0 0 25 0 1 0 541415519 109109248 24218 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26638 24218 603 41 0 26597 0
vsize: 106552
[startup+720.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 25469 0 0 0 71925 86 0 0 25 0 1 0 541415519 109633536 24333 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26766 24333 603 41 0 26725 0
vsize: 107064
[startup+730.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 25593 0 0 0 72925 86 0 0 25 0 1 0 541415519 111206400 24457 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27150 24457 603 41 0 27109 0
vsize: 108600
[startup+740.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 25758 0 0 0 73924 87 0 0 25 0 1 0 541415519 111869952 24622 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27312 24622 603 41 0 27271 0
vsize: 109248
[startup+750.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 25930 0 0 0 74923 88 0 0 25 0 1 0 541415519 112529408 24794 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27473 24794 603 41 0 27432 0
vsize: 109892
[startup+760.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 26117 0 0 0 75923 88 0 0 25 0 1 0 541415519 113340416 24981 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27671 24981 603 41 0 27630 0
vsize: 110684
[startup+770.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 26287 0 0 0 76923 89 0 0 25 0 1 0 541415519 114098176 25151 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27856 25151 603 41 0 27815 0
vsize: 111424
[startup+780.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 26393 0 0 0 77922 90 0 0 25 0 1 0 541415519 114569216 25257 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27971 25257 603 41 0 27930 0
vsize: 111884
[startup+790.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 26474 0 0 0 78922 90 0 0 25 0 1 0 541415519 114847744 25338 4294967295 134512640 134672761 3221224544 3221223680 134614713 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28039 25338 603 41 0 27998 0
vsize: 112156
[startup+800.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 26631 0 0 0 79922 90 0 0 25 0 1 0 541415519 115507200 25495 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28200 25495 603 41 0 28159 0
vsize: 112800
[startup+810.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 26741 0 0 0 80922 91 0 0 25 0 1 0 541415519 115904512 25605 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28297 25605 603 41 0 28256 0
vsize: 113188
[startup+820.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 26887 0 0 0 81921 91 0 0 25 0 1 0 541415519 116445184 25751 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28429 25751 603 41 0 28388 0
vsize: 113716
[startup+830.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 27110 0 0 0 82921 92 0 0 25 0 1 0 541415519 117366784 25974 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28654 25974 603 41 0 28613 0
vsize: 114616
[startup+840.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 27338 0 0 0 83920 93 0 0 25 0 1 0 541415519 118288384 26202 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28879 26202 603 41 0 28838 0
vsize: 115516
[startup+850.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 27472 0 0 0 84920 93 0 0 25 0 1 0 541415519 118812672 26336 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29007 26336 603 41 0 28966 0
vsize: 116028
[startup+860.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 27540 0 0 0 85920 93 0 0 25 0 1 0 541415519 119209984 26404 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29104 26404 603 41 0 29063 0
vsize: 116416
[startup+870.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 27649 0 0 0 86920 93 0 0 25 0 1 0 541415519 119611392 26513 4294967295 134512640 134672761 3221224544 3221223668 134566047 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29202 26513 603 41 0 29161 0
vsize: 116808
[startup+880.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 27750 0 0 0 87920 94 0 0 25 0 1 0 541415519 120033280 26614 4294967295 134512640 134672761 3221224544 3221223728 134616023 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29305 26614 603 41 0 29264 0
vsize: 117220
[startup+890.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 27836 0 0 0 88919 94 0 0 25 0 1 0 541415519 120426496 26700 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29401 26700 603 41 0 29360 0
vsize: 117604
[startup+900.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 27919 0 0 0 89919 95 0 0 25 0 1 0 541415519 120692736 26783 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29466 26783 603 41 0 29425 0
vsize: 117864
[startup+910.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 27985 0 0 0 90919 95 0 0 25 0 1 0 541415519 120958976 26849 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29531 26849 603 41 0 29490 0
vsize: 118124
[startup+920.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 28057 0 0 0 91920 95 0 0 25 0 1 0 541415519 121233408 26921 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29598 26921 603 41 0 29557 0
vsize: 118392
[startup+930.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 28135 0 0 0 92920 95 0 0 25 0 1 0 541415519 121634816 26999 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29696 26999 603 41 0 29655 0
vsize: 118784
[startup+940.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 28221 0 0 0 93920 95 0 0 25 0 1 0 541415519 122032128 27085 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29793 27085 603 41 0 29752 0
vsize: 119172
[startup+950.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 28312 0 0 0 94919 96 0 0 25 0 1 0 541415519 122437632 27176 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29892 27176 603 41 0 29851 0
vsize: 119568
[startup+960.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 28406 0 0 0 95920 96 0 0 25 0 1 0 541415519 122830848 27270 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29988 27270 603 41 0 29947 0
vsize: 119952
[startup+970.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 28489 0 0 0 96919 96 0 0 25 0 1 0 541415519 123097088 27353 4294967295 134512640 134672761 3221224544 3221223728 134615673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30053 27353 603 41 0 30012 0
vsize: 120212
[startup+980.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 28582 0 0 0 97919 96 0 0 25 0 1 0 541415519 123490304 27446 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30149 27446 603 41 0 30108 0
vsize: 120596
[startup+990.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 28688 0 0 0 98919 97 0 0 25 0 1 0 541415519 123887616 27552 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30246 27552 603 41 0 30205 0
vsize: 120984
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 28771 0 0 0 99919 97 0 0 25 0 1 0 541415519 124149760 27635 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30310 27635 603 41 0 30269 0
vsize: 121240
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 28833 0 0 0 100919 97 0 0 25 0 1 0 541415519 124416000 27697 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30375 27697 603 41 0 30334 0
vsize: 121500
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 28924 0 0 0 101919 97 0 0 25 0 1 0 541415519 124862464 27788 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30484 27788 603 41 0 30443 0
vsize: 121936
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 29096 0 0 0 102919 98 0 0 25 0 1 0 541415519 125521920 27960 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30645 27960 603 41 0 30604 0
vsize: 122580
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 29294 0 0 0 103918 99 0 0 25 0 1 0 541415519 126312448 28158 4294967295 134512640 134672761 3221224544 3221223688 134616339 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30838 28158 603 41 0 30797 0
vsize: 123352
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 29371 0 0 0 104918 99 0 0 25 0 1 0 541415519 126574592 28235 4294967295 134512640 134672761 3221224544 3221223688 134616178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30902 28235 603 41 0 30861 0
vsize: 123608
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 29443 0 0 0 105918 99 0 0 25 0 1 0 541415519 126857216 28307 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30971 28307 603 41 0 30930 0
vsize: 123884
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 29491 0 0 0 106918 99 0 0 25 0 1 0 541415519 127123456 28355 4294967295 134512640 134672761 3221224544 3221223688 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31036 28355 603 41 0 30995 0
vsize: 124144
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 29567 0 0 0 107918 99 0 0 25 0 1 0 541415519 127385600 28431 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31100 28431 603 41 0 31059 0
vsize: 124400
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 29657 0 0 0 108918 100 0 0 25 0 1 0 541415519 127791104 28521 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31199 28521 603 41 0 31158 0
vsize: 124796
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 29794 0 0 0 109918 100 0 0 25 0 1 0 541415519 128315392 28658 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31327 28658 603 41 0 31286 0
vsize: 125308
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 29950 0 0 0 110918 100 0 0 25 0 1 0 541415519 129003520 28814 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31495 28814 603 41 0 31454 0
vsize: 125980
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 30078 0 0 0 111917 101 0 0 25 0 1 0 541415519 129536000 28942 4294967295 134512640 134672761 3221224544 3221223668 134566040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31625 28942 603 41 0 31584 0
vsize: 126500
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 30151 0 0 0 112918 101 0 0 25 0 1 0 541415519 129802240 29015 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31690 29015 603 41 0 31649 0
vsize: 126760
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 30199 0 0 0 113918 101 0 0 25 0 1 0 541415519 129937408 29063 4294967295 134512640 134672761 3221224544 3221223688 134616178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31723 29063 603 41 0 31682 0
vsize: 126892
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 30272 0 0 0 114918 101 0 0 25 0 1 0 541415519 130236416 29136 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31796 29136 603 41 0 31755 0
vsize: 127184
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 30333 0 0 0 115918 102 0 0 25 0 1 0 541415519 130502656 29197 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31861 29197 603 41 0 31820 0
vsize: 127444
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 30436 0 0 0 116918 102 0 0 25 0 1 0 541415519 131039232 29300 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31992 29300 603 41 0 31951 0
vsize: 127968
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 30518 0 0 0 117918 102 0 0 25 0 1 0 541415519 131305472 29382 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32057 29382 603 41 0 32016 0
vsize: 128228
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 30598 0 0 0 118918 102 0 0 25 0 1 0 541415519 131702784 29462 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32154 29462 603 41 0 32113 0
vsize: 128616
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19847
Raw data (stat): 19847 (minisat+) R 19846 23176 23175 0 -1 0 30694 0 0 0 119918 103 0 0 25 0 1 0 541415519 131973120 29558 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32220 29558 603 41 0 32179 0
vsize: 128880
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 19847
Raw data (stat): 19847 (minisat+) Z 19846 23176 23175 0 -1 12 30694 0 0 0 119918 109 0 0 25 0 1 0 541415519 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.18
CPU system time (s): 1.09183
CPU usage (%): 100.014
Max. virtual memory (Kb): 128880
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####