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 14981

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-04-21 02:19:56 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18785 boxname=wulflinc5 idbench=1445 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  d14265fdf4e5a3ef733af1f15b884cbe  /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-pp08a.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-pp08a.opb /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-pp08a.opb
IDLAUNCH: 18785
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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	: 2
cpu MHz		: 451.007
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:        369320 kB
Buffers:         39484 kB
Cached:         600096 kB
SwapCached:       2272 kB
Active:         236068 kB
Inactive:       408632 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        369068 kB
SwapTotal:     2097136 kB
SwapFree:      2094864 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6940 kB
Slab:            14864 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 02:40:08 (client local time) WITH STATUS 0 IN 1210.04 SECONDS
stats: 18785 7 1210.04 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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  197599   469503 |   65866       0        0     nan |  0.000 % |
c |       100 |  197477   469233 |   72452      81      289     3.6 |  5.642 % |
c |       250 |  197339   468926 |   79697     211      869     4.1 |  5.702 % |
c |       475 |  197133   468467 |   87667     404     1540     3.8 |  5.782 % |
c |       812 |  196798   467720 |   96434     692     2682     3.9 |  5.917 % |
c |      1318 |  196714   467532 |  106077    1181     6388     5.4 |  5.961 % |
c |      2077 |  196219   466429 |  116685    1865    10015     5.4 |  6.153 % |
c |      3218 |  195653   465161 |  128354    2938    15772     5.4 |  6.387 % |
c |      4926 |  195423   464646 |  141189    4611    29457     6.4 |  6.479 % |
c |      7488 |  195057   463824 |  155308    7126    54681     7.7 |  6.623 % |
c |     11332 |  194688   462998 |  170839   10920    95189     8.7 |  6.765 % |
c |     17099 |  194339   462218 |  187923   16626   172985    10.4 |  6.905 % |
c |     25748 |  194118   461724 |  206715   25247   365850    14.5 |  6.995 % |
c |     38722 |  192503   458110 |  227387   38002   552368    14.5 |  7.645 % |
c |     58183 |  191603   456090 |  250126   57346  1020041    17.8 |  8.005 % |
c |     87375 |  189541   451471 |  275138   86258  1638973    19.0 |  8.830 % |
c |    131165 |  188706   449594 |  302652  129940  2629040    20.2 |  9.166 % |
c |    196851 |  187584   447065 |  332917  195492  4639873    23.7 |  9.630 % |
c |    295379 |  186283   444129 |  366209  293869  7256664    24.7 | 10.174 % |
c |    443168 |  185745   442914 |  402830  104510  1906734    18.2 | 10.392 % |
#### 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.58 0.85 0.88 2/54 14530
Raw data (stat): 14530 (runsolver) R 14529 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 483208466 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.0004 s]
Raw data (loadavg): 0.64 0.86 0.88 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 6046 0 0 0 988 10 0 0 25 0 1 0 483208466 30449664 5881 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7434 5881 603 41 0 7393 0
vsize: 29736
[startup+20.0001 s]
Raw data (loadavg): 0.70 0.86 0.88 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 6170 0 0 0 1987 11 0 0 25 0 1 0 483208466 30920704 6005 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7549 6005 603 41 0 7508 0
vsize: 30196
[startup+30.0008 s]
Raw data (loadavg): 0.74 0.86 0.88 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 6343 0 0 0 2987 12 0 0 25 0 1 0 483208466 31698944 6178 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7739 6178 603 41 0 7698 0
vsize: 30956
[startup+40.0005 s]
Raw data (loadavg): 0.78 0.87 0.88 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 6624 0 0 0 3985 13 0 0 25 0 1 0 483208466 32776192 6459 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8002 6459 603 41 0 7961 0
vsize: 32008
[startup+50.0012 s]
Raw data (loadavg): 0.82 0.87 0.88 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 6777 0 0 0 4985 14 0 0 25 0 1 0 483208466 33312768 6612 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8133 6612 603 41 0 8092 0
vsize: 32532
[startup+60.001 s]
Raw data (loadavg): 0.84 0.88 0.88 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 6902 0 0 0 5985 14 0 0 25 0 1 0 483208466 33980416 6737 4294967295 134512640 134672761 3221224544 3221223648 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8296 6737 603 41 0 8255 0
vsize: 33184
[startup+70.0007 s]
Raw data (loadavg): 0.87 0.88 0.88 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 7091 0 0 0 6983 15 0 0 25 0 1 0 483208466 34783232 6926 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8492 6926 603 41 0 8451 0
vsize: 33968
[startup+80.0015 s]
Raw data (loadavg): 0.89 0.88 0.88 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 7384 0 0 0 7982 16 0 0 25 0 1 0 483208466 35848192 7219 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8752 7219 603 41 0 8711 0
vsize: 35008
[startup+90.0012 s]
Raw data (loadavg): 0.90 0.89 0.89 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 7575 0 0 0 8981 17 0 0 25 0 1 0 483208466 36655104 7410 4294967295 134512640 134672761 3221224544 3221223668 134566047 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8949 7410 603 41 0 8908 0
vsize: 35796
[startup+100.002 s]
Raw data (loadavg): 0.92 0.89 0.89 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 7738 0 0 0 9980 18 0 0 25 0 1 0 483208466 37326848 7573 4294967295 134512640 134672761 3221224544 3221223716 134556641 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9113 7573 603 41 0 9072 0
vsize: 36452
[startup+110.002 s]
Raw data (loadavg): 0.93 0.89 0.89 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 7902 0 0 0 10980 19 0 0 25 0 1 0 483208466 38256640 7737 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9340 7737 603 41 0 9299 0
vsize: 37360
[startup+120.002 s]
Raw data (loadavg): 0.94 0.90 0.89 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 8010 0 0 0 11979 20 0 0 25 0 1 0 483208466 38653952 7845 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9437 7845 603 41 0 9396 0
vsize: 37748
[startup+130.003 s]
Raw data (loadavg): 0.95 0.90 0.89 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 8047 0 0 0 12979 20 0 0 25 0 1 0 483208466 38789120 7882 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9470 7882 603 41 0 9429 0
vsize: 37880
[startup+140.003 s]
Raw data (loadavg): 0.96 0.90 0.89 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 8168 0 0 0 13978 21 0 0 25 0 1 0 483208466 39190528 8003 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9568 8003 603 41 0 9527 0
vsize: 38272
[startup+150.003 s]
Raw data (loadavg): 0.96 0.90 0.89 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 8392 0 0 0 14977 22 0 0 25 0 1 0 483208466 40128512 8227 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9797 8227 603 41 0 9756 0
vsize: 39188
[startup+160.003 s]
Raw data (loadavg): 0.97 0.91 0.89 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 8541 0 0 0 15976 22 0 0 25 0 1 0 483208466 40677376 8376 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9931 8376 603 41 0 9890 0
vsize: 39724
[startup+170.003 s]
Raw data (loadavg): 0.97 0.91 0.89 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 8649 0 0 0 16975 23 0 0 25 0 1 0 483208466 41082880 8484 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10030 8484 603 41 0 9989 0
vsize: 40120
[startup+180.002 s]
Raw data (loadavg): 0.98 0.91 0.89 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 8809 0 0 0 17975 24 0 0 25 0 1 0 483208466 41750528 8644 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10193 8644 603 41 0 10152 0
vsize: 40772
[startup+190.004 s]
Raw data (loadavg): 0.98 0.91 0.89 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 9147 0 0 0 18973 25 0 0 25 0 1 0 483208466 43089920 8982 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10520 8982 603 41 0 10479 0
vsize: 42080
[startup+200.004 s]
Raw data (loadavg): 0.98 0.92 0.90 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 9292 0 0 0 19972 26 0 0 25 0 1 0 483208466 43630592 9127 4294967295 134512640 134672761 3221224544 3221223668 134566077 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10652 9127 603 41 0 10611 0
vsize: 42608
[startup+210.004 s]
Raw data (loadavg): 0.98 0.92 0.90 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 9556 0 0 0 20972 27 0 0 25 0 1 0 483208466 44695552 9391 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10912 9391 603 41 0 10871 0
vsize: 43648
[startup+220.004 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 9835 0 0 0 21970 28 0 0 25 0 1 0 483208466 45899776 9670 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11206 9670 603 41 0 11165 0
vsize: 44824
[startup+230.004 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 9992 0 0 0 22970 28 0 0 25 0 1 0 483208466 46968832 9827 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11467 9827 603 41 0 11426 0
vsize: 45868
[startup+240.004 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 10075 0 0 0 23969 29 0 0 25 0 1 0 483208466 47370240 9910 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11565 9910 603 41 0 11524 0
vsize: 46260
[startup+250.005 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 10174 0 0 0 24969 29 0 0 25 0 1 0 483208466 47775744 10009 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11664 10009 603 41 0 11623 0
vsize: 46656
[startup+260.005 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 10576 0 0 0 25967 31 0 0 25 0 1 0 483208466 49393664 10411 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12059 10411 603 41 0 12018 0
vsize: 48236
[startup+270.005 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 11089 0 0 0 26965 33 0 0 25 0 1 0 483208466 51412992 10924 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12552 10924 603 41 0 12511 0
vsize: 50208
[startup+280.005 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 11482 0 0 0 27963 35 0 0 25 0 1 0 483208466 53035008 11317 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12948 11317 603 41 0 12907 0
vsize: 51792
[startup+290.005 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 11782 0 0 0 28962 36 0 0 25 0 1 0 483208466 54272000 11617 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13250 11617 603 41 0 13209 0
vsize: 53000
[startup+300.006 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 12044 0 0 0 29961 37 0 0 25 0 1 0 483208466 55312384 11879 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13504 11879 603 41 0 13463 0
vsize: 54016
[startup+310.006 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 12145 0 0 0 30960 38 0 0 25 0 1 0 483208466 55717888 11980 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13603 11980 603 41 0 13562 0
vsize: 54412
[startup+320.006 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 12217 0 0 0 31960 38 0 0 25 0 1 0 483208466 55984128 12052 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13668 12052 603 41 0 13627 0
vsize: 54672
[startup+330.006 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 12436 0 0 0 32959 39 0 0 25 0 1 0 483208466 56930304 12271 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13899 12271 603 41 0 13858 0
vsize: 55596
[startup+340.006 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 12661 0 0 0 33958 40 0 0 25 0 1 0 483208466 57864192 12496 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14127 12496 603 41 0 14086 0
vsize: 56508
[startup+350.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 12862 0 0 0 34957 41 0 0 25 0 1 0 483208466 58683392 12697 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14327 12697 603 41 0 14286 0
vsize: 57308
[startup+360.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 13018 0 0 0 35957 41 0 0 25 0 1 0 483208466 59367424 12853 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14494 12853 603 41 0 14453 0
vsize: 57976
[startup+370.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 13117 0 0 0 36956 42 0 0 25 0 1 0 483208466 59637760 12952 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14560 12952 603 41 0 14519 0
vsize: 58240
[startup+380.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 13180 0 0 0 37955 43 0 0 25 0 1 0 483208466 59908096 13015 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14626 13015 603 41 0 14585 0
vsize: 58504
[startup+390.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 13355 0 0 0 38954 44 0 0 25 0 1 0 483208466 60727296 13190 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14826 13190 603 41 0 14785 0
vsize: 59304
[startup+400.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 13509 0 0 0 39953 45 0 0 25 0 1 0 483208466 61267968 13344 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14958 13344 603 41 0 14917 0
vsize: 59832
[startup+410.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 13566 0 0 0 40953 45 0 0 25 0 1 0 483208466 61546496 13401 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15026 13401 603 41 0 14985 0
vsize: 60104
[startup+420.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 13791 0 0 0 41952 46 0 0 25 0 1 0 483208466 62349312 13626 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15222 13626 603 41 0 15181 0
vsize: 60888
[startup+430.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 13855 0 0 0 42952 46 0 0 25 0 1 0 483208466 62619648 13690 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15288 13690 603 41 0 15247 0
vsize: 61152
[startup+440.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 13918 0 0 0 43951 46 0 0 25 0 1 0 483208466 62885888 13753 4294967295 134512640 134672761 3221224544 3221223712 134560968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15353 13753 603 41 0 15312 0
vsize: 61412
[startup+450.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 14026 0 0 0 44951 47 0 0 25 0 1 0 483208466 63287296 13861 4294967295 134512640 134672761 3221224544 3221223800 134562229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15451 13861 603 41 0 15410 0
vsize: 61804
[startup+460.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 14298 0 0 0 45950 48 0 0 25 0 1 0 483208466 64483328 14133 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15743 14133 603 41 0 15702 0
vsize: 62972
[startup+470.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 14479 0 0 0 46949 49 0 0 25 0 1 0 483208466 65159168 14314 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15908 14314 603 41 0 15867 0
vsize: 63632
[startup+480.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 14589 0 0 0 47949 49 0 0 25 0 1 0 483208466 65695744 14424 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16039 14424 603 41 0 15998 0
vsize: 64156
[startup+490.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 14699 0 0 0 48948 50 0 0 25 0 1 0 483208466 66097152 14534 4294967295 134512640 134672761 3221224544 3221223712 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16137 14534 603 41 0 16096 0
vsize: 64548
[startup+500.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 14761 0 0 0 49948 50 0 0 25 0 1 0 483208466 66367488 14596 4294967295 134512640 134672761 3221224544 3221223808 134562262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16203 14596 603 41 0 16162 0
vsize: 64812
[startup+510.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 14898 0 0 0 50947 51 0 0 25 0 1 0 483208466 66940928 14733 4294967295 134512640 134672761 3221224544 3221223680 134560720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16343 14733 603 41 0 16302 0
vsize: 65372
[startup+520.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 14989 0 0 0 51946 51 0 0 25 0 1 0 483208466 67207168 14824 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16408 14824 603 41 0 16367 0
vsize: 65632
[startup+530.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 15096 0 0 0 52945 52 0 0 25 0 1 0 483208466 68657152 14931 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16762 14931 603 41 0 16721 0
vsize: 67048
[startup+540.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 15147 0 0 0 53945 53 0 0 25 0 1 0 483208466 68923392 14982 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16827 14982 603 41 0 16786 0
vsize: 67308
[startup+550.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 15246 0 0 0 54945 53 0 0 25 0 1 0 483208466 69320704 15081 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16924 15081 603 41 0 16883 0
vsize: 67696
[startup+560.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 15298 0 0 0 55944 54 0 0 25 0 1 0 483208466 69586944 15133 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16989 15133 603 41 0 16948 0
vsize: 67956
[startup+570.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 15347 0 0 0 56944 54 0 0 25 0 1 0 483208466 69722112 15182 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17022 15182 603 41 0 16981 0
vsize: 68088
[startup+580.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 15414 0 0 0 57943 55 0 0 25 0 1 0 483208466 69996544 15249 4294967295 134512640 134672761 3221224544 3221223712 134561259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17089 15249 603 41 0 17048 0
vsize: 68356
[startup+590.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 15510 0 0 0 58942 55 0 0 25 0 1 0 483208466 70393856 15345 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17186 15345 603 41 0 17145 0
vsize: 68744
[startup+600.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 15698 0 0 0 59941 57 0 0 25 0 1 0 483208466 71192576 15533 4294967295 134512640 134672761 3221224544 3221223680 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17381 15533 603 41 0 17340 0
vsize: 69524
[startup+610.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 15808 0 0 0 60941 57 0 0 25 0 1 0 483208466 71618560 15643 4294967295 134512640 134672761 3221224544 3221223728 134558374 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17485 15643 603 41 0 17444 0
vsize: 69940
[startup+620.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 15935 0 0 0 61940 58 0 0 25 0 1 0 483208466 72056832 15770 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17592 15770 603 41 0 17551 0
vsize: 70368
[startup+630.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 16113 0 0 0 62939 59 0 0 25 0 1 0 483208466 72880128 15948 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17793 15948 603 41 0 17752 0
vsize: 71172
[startup+640.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 16237 0 0 0 63938 60 0 0 25 0 1 0 483208466 73453568 16072 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17933 16072 603 41 0 17892 0
vsize: 71732
[startup+650.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 16404 0 0 0 64937 60 0 0 25 0 1 0 483208466 74125312 16239 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18097 16239 603 41 0 18056 0
vsize: 72388
[startup+660.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 16528 0 0 0 65937 61 0 0 25 0 1 0 483208466 74518528 16363 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18193 16363 603 41 0 18152 0
vsize: 72772
[startup+670.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 16595 0 0 0 66936 62 0 0 25 0 1 0 483208466 74784768 16430 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18258 16430 603 41 0 18217 0
vsize: 73032
[startup+680.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 16716 0 0 0 67935 62 0 0 25 0 1 0 483208466 75354112 16551 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18397 16551 603 41 0 18356 0
vsize: 73588
[startup+690.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 16987 0 0 0 68934 63 0 0 25 0 1 0 483208466 76410880 16822 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18655 16822 603 41 0 18614 0
vsize: 74620
[startup+700.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 17141 0 0 0 69933 64 0 0 25 0 1 0 483208466 77094912 16976 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18822 16976 603 41 0 18781 0
vsize: 75288
[startup+710.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 17236 0 0 0 70933 65 0 0 25 0 1 0 483208466 77365248 17071 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18888 17071 603 41 0 18847 0
vsize: 75552
[startup+720.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 17401 0 0 0 71932 66 0 0 25 0 1 0 483208466 78036992 17236 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19052 17236 603 41 0 19011 0
vsize: 76208
[startup+730.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 17589 0 0 0 72931 66 0 0 25 0 1 0 483208466 78958592 17424 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19277 17424 603 41 0 19236 0
vsize: 77108
[startup+740.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 17761 0 0 0 73931 67 0 0 25 0 1 0 483208466 79724544 17596 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19464 17596 603 41 0 19423 0
vsize: 77856
[startup+750.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 17944 0 0 0 74930 68 0 0 25 0 1 0 483208466 80392192 17779 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19627 17779 603 41 0 19586 0
vsize: 78508
[startup+760.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 18112 0 0 0 75929 69 0 0 25 0 1 0 483208466 81059840 17947 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19790 17947 603 41 0 19749 0
vsize: 79160
[startup+770.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 18171 0 0 0 76928 70 0 0 25 0 1 0 483208466 81338368 18006 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19858 18006 603 41 0 19817 0
vsize: 79432
[startup+780.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 18297 0 0 0 77928 70 0 0 25 0 1 0 483208466 81879040 18132 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19990 18132 603 41 0 19949 0
vsize: 79960
[startup+790.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 18450 0 0 0 78927 71 0 0 25 0 1 0 483208466 82440192 18285 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20127 18285 603 41 0 20086 0
vsize: 80508
[startup+800.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 18613 0 0 0 79926 72 0 0 25 0 1 0 483208466 83132416 18448 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20296 18448 603 41 0 20255 0
vsize: 81184
[startup+810.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 18759 0 0 0 80925 73 0 0 25 0 1 0 483208466 83812352 18594 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20462 18594 603 41 0 20421 0
vsize: 81848
[startup+820.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 18959 0 0 0 81924 73 0 0 25 0 1 0 483208466 84496384 18794 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20629 18794 603 41 0 20588 0
vsize: 82516
[startup+830.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 19069 0 0 0 82924 74 0 0 25 0 1 0 483208466 85041152 18904 4294967295 134512640 134672761 3221224544 3221223648 134555175 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20762 18904 603 41 0 20721 0
vsize: 83048
[startup+840.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 19168 0 0 0 83923 74 0 0 25 0 1 0 483208466 85368832 19003 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20842 19003 603 41 0 20801 0
vsize: 83368
[startup+850.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 19308 0 0 0 84923 75 0 0 25 0 1 0 483208466 86024192 19143 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21002 19143 603 41 0 20961 0
vsize: 84008
[startup+860.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 19441 0 0 0 85923 75 0 0 25 0 1 0 483208466 86568960 19276 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21135 19276 603 41 0 21094 0
vsize: 84540
[startup+870.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 19558 0 0 0 86922 76 0 0 25 0 1 0 483208466 87109632 19393 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21267 19393 603 41 0 21226 0
vsize: 85068
[startup+880.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 19683 0 0 0 87921 77 0 0 25 0 1 0 483208466 87506944 19518 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21364 19518 603 41 0 21323 0
vsize: 85456
[startup+890.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 19791 0 0 0 88921 77 0 0 25 0 1 0 483208466 88047616 19626 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21496 19626 603 41 0 21455 0
vsize: 85984
[startup+900.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 19932 0 0 0 89920 78 0 0 25 0 1 0 483208466 88588288 19767 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21628 19767 603 41 0 21587 0
vsize: 86512
[startup+910.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 20075 0 0 0 90919 79 0 0 25 0 1 0 483208466 89210880 19910 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21780 19910 603 41 0 21739 0
vsize: 87120
[startup+920.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 20086 0 0 0 91919 79 0 0 25 0 1 0 483208466 89210880 19921 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21780 19921 603 41 0 21739 0
vsize: 87120
[startup+930.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 20086 0 0 0 92918 80 0 0 25 0 1 0 483208466 89210880 19921 4294967295 134512640 134672761 3221224544 3221223700 134564777 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21780 19921 603 41 0 21739 0
vsize: 87120
[startup+940.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 20086 0 0 0 93918 80 0 0 25 0 1 0 483208466 89210880 19921 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21780 19921 603 41 0 21739 0
vsize: 87120
[startup+950.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 20086 0 0 0 94918 80 0 0 25 0 1 0 483208466 89210880 19921 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21780 19921 603 41 0 21739 0
vsize: 87120
[startup+960.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 20086 0 0 0 95918 80 0 0 25 0 1 0 483208466 89210880 19921 4294967295 134512640 134672761 3221224544 3221223712 134564673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21780 19921 603 41 0 21739 0
vsize: 87120
[startup+970.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 20086 0 0 0 96917 80 0 0 25 0 1 0 483208466 89210880 19921 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21780 19921 603 41 0 21739 0
vsize: 87120
[startup+980.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 20086 0 0 0 97917 81 0 0 25 0 1 0 483208466 89210880 19921 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21780 19921 603 41 0 21739 0
vsize: 87120
[startup+990.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 20086 0 0 0 98917 81 0 0 25 0 1 0 483208466 89210880 19921 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21780 19921 603 41 0 21739 0
vsize: 87120
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 20086 0 0 0 99917 81 0 0 25 0 1 0 483208466 89210880 19921 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21780 19921 603 41 0 21739 0
vsize: 87120
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 20086 0 0 0 100917 81 0 0 25 0 1 0 483208466 89210880 19921 4294967295 134512640 134672761 3221224544 3221223680 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21780 19921 603 41 0 21739 0
vsize: 87120
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 20086 0 0 0 101916 82 0 0 25 0 1 0 483208466 89210880 19921 4294967295 134512640 134672761 3221224544 3221223680 134560613 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21780 19921 603 41 0 21739 0
vsize: 87120
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 20086 0 0 0 102916 82 0 0 25 0 1 0 483208466 89210880 19921 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21780 19921 603 41 0 21739 0
vsize: 87120
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 20086 0 0 0 103916 82 0 0 25 0 1 0 483208466 89210880 19921 4294967295 134512640 134672761 3221224544 3221223712 134564729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21780 19921 603 41 0 21739 0
vsize: 87120
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 20086 0 0 0 104915 83 0 0 25 0 1 0 483208466 89210880 19921 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21780 19921 603 41 0 21739 0
vsize: 87120
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 20086 0 0 0 105915 83 0 0 25 0 1 0 483208466 89210880 19921 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21780 19921 603 41 0 21739 0
vsize: 87120
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 20086 0 0 0 106914 84 0 0 25 0 1 0 483208466 89210880 19921 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21780 19921 603 41 0 21739 0
vsize: 87120
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 20086 0 0 0 107914 84 0 0 25 0 1 0 483208466 89210880 19921 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21780 19921 603 41 0 21739 0
vsize: 87120
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 20086 0 0 0 108914 84 0 0 25 0 1 0 483208466 89210880 19921 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21780 19921 603 41 0 21739 0
vsize: 87120
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 20086 0 0 0 109914 84 0 0 25 0 1 0 483208466 89210880 19921 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21780 19921 603 41 0 21739 0
vsize: 87120
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 20086 0 0 0 110914 84 0 0 25 0 1 0 483208466 89210880 19921 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21780 19921 603 41 0 21739 0
vsize: 87120
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 20086 0 0 0 111913 85 0 0 25 0 1 0 483208466 89210880 19921 4294967295 134512640 134672761 3221224544 3221223700 134564777 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21780 19921 603 41 0 21739 0
vsize: 87120
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 20086 0 0 0 112914 85 0 0 25 0 1 0 483208466 89210880 19921 4294967295 134512640 134672761 3221224544 3221223648 134560136 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21780 19921 603 41 0 21739 0
vsize: 87120
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 20086 0 0 0 113913 85 0 0 25 0 1 0 483208466 89210880 19921 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21780 19921 603 41 0 21739 0
vsize: 87120
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 20086 0 0 0 114913 85 0 0 25 0 1 0 483208466 89210880 19921 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21780 19921 603 41 0 21739 0
vsize: 87120
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 20087 0 0 0 115913 86 0 0 25 0 1 0 483208466 89210880 19922 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21780 19922 603 41 0 21739 0
vsize: 87120
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 20087 0 0 0 116913 86 0 0 25 0 1 0 483208466 89210880 19922 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21780 19922 603 41 0 21739 0
vsize: 87120
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 20087 0 0 0 117913 86 0 0 25 0 1 0 483208466 89210880 19922 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21780 19922 603 41 0 21739 0
vsize: 87120
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 20087 0 0 0 118913 86 0 0 25 0 1 0 483208466 89210880 19922 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21780 19922 603 41 0 21739 0
vsize: 87120
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 20087 0 0 0 119913 86 0 0 25 0 1 0 483208466 89210880 19922 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21780 19922 603 41 0 21739 0
vsize: 87120
[startup+1210.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14530
Raw data (stat): 14530 (minisat+) R 14529 24215 24214 0 -1 0 20087 0 0 0 120912 87 0 0 25 0 1 0 483208466 89210880 19922 4294967295 134512640 134672761 3221224544 3221223728 134559365 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21780 19922 603 41 0 21739 0
vsize: 87120
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 14530
Raw data (stat): 14530 (minisat+) Z 14529 24215 24214 0 -1 12 20089 0 0 0 120912 90 0 0 25 0 1 0 483208466 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): 1210.09
CPU time (s): 1210.04
CPU user time (s): 1209.13
CPU system time (s): 0.908861
CPU usage (%): 99.9956
Max. virtual memory (Kb): 87120
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####