PB'05 competition: run trace

Some explanations

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

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

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc8 THE 2005-04-21 15:14:29 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17927 boxname=wulflinc8 idbench=1379 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  962e64054cef66ff1ace4918a032c24a  /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-pp08a.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-pp08a.opb /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-pp08a.opb
IDLAUNCH: 17927
/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:        604936 kB
Buffers:         32384 kB
Cached:         374936 kB
SwapCached:          0 kB
Active:         150048 kB
Inactive:       260216 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        604684 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              52 kB
Writeback:           0 kB
Mapped:           6952 kB
Slab:            13768 kB
Committed_AS:    63584 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 15:34:31 (client local time) WITH STATUS 0 IN 1200.23 SECONDS
stats: 17927 7 1200.23 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 200 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 198]---> BDD-cost:  158
c ---[ 196]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 195]---> BDD-cost:   21
c ---[ 194]---> BDD-cost:   21
c ---[ 193]---> BDD-cost:   21
c ---[ 192]---> BDD-cost:   21
c ---[ 191]---> BDD-cost:   23
c ---[ 190]---> BDD-cost:   18
c ---[ 189]---> BDD-cost:   18
c ---[ 188]---> BDD-cost:   18
c ---[ 187]---> BDD-cost:   18
c ---[ 186]---> BDD-cost:   18
c ---[ 184]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 183]---> BDD-cost:   18
c ---[ 182]---> BDD-cost:   18
c ---[ 181]---> BDD-cost:   18
c ---[ 180]---> BDD-cost:   24
c ---[ 179]---> BDD-cost:   24
c ---[ 178]---> BDD-cost:   24
c ---[ 177]---> BDD-cost:   21
c ---[ 176]---> BDD-cost:   21
c ---[ 175]---> BDD-cost:   21
c ---[ 174]---> BDD-cost:   21
c ---[ 172]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 171]---> BDD-cost:   21
c ---[ 170]---> BDD-cost:   19
c ---[ 169]---> BDD-cost:   19
c ---[ 168]---> BDD-cost:   19
c ---[ 167]---> BDD-cost:   19
c ---[ 166]---> BDD-cost:   19
c ---[ 165]---> BDD-cost:   19
c ---[ 164]---> BDD-cost:   19
c ---[ 163]---> BDD-cost:   19
c ---[ 162]---> BDD-cost:   19
c ---[ 160]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 159]---> BDD-cost:   19
c ---[ 158]---> BDD-cost:   19
c ---[ 157]---> BDD-cost:   19
c ---[ 156]---> BDD-cost:   19
c ---[ 155]---> BDD-cost:   19
c ---[ 154]---> BDD-cost:   19
c ---[ 153]---> BDD-cost:   19
c ---[ 151]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 149]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 147]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 145]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 143]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 141]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 139]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 137]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 135]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 133]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 131]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 129]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 127]---> BDD-cost:  158
c ---[ 125]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 123]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 121]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 119]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 117]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 115]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 113]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 111]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 109]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 107]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 105]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 103]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 101]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  99]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  97]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  95]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  93]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  91]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  89]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  87]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  85]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  83]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  81]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  79]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  77]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  75]---> BDD-cost:  154
c ---[  73]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  71]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  69]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  67]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  65]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  63]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  61]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  59]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  57]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  55]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  53]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  51]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  49]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  47]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  45]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  43]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  41]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  40]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  39]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  38]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  37]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  36]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  34]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  33]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  32]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  31]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  30]---> BDD-cost:   24
c ---[  29]---> BDD-cost:   24
c ---[  28]---> BDD-cost:   24
c ---[  27]---> BDD-cost:   21
c ---[  26]---> BDD-cost:   21
c ---[  25]---> BDD-cost:   21
c ---[  24]---> BDD-cost:   21
c ---[  22]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  21]---> BDD-cost:   23
c ---[  20]---> BDD-cost:   19
c ---[  19]---> BDD-cost:   19
c ---[  18]---> BDD-cost:   19
c ---[  17]---> BDD-cost:   19
c ---[  16]---> BDD-cost:   19
c ---[  15]---> BDD-cost:   19
c ---[  14]---> BDD-cost:   19
c ---[  13]---> BDD-cost:   19
c ---[  12]---> BDD-cost:   24
c ---[  10]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   9]---> BDD-cost:   24
c ---[   8]---> BDD-cost:   24
c ---[   7]---> BDD-cost:   21
c ---[   6]---> BDD-cost:   21
c ---[   5]---> BDD-cost:   21
c ---[   4]---> BDD-cost:   21
c ---[   3]---> BDD-cost:   23
c ---[   2]---> BDD-cost:   24
c ---[   1]---> BDD-cost:   24
c ---[   0]---> BDD-cost:   24
c ==================================[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 |  197532   469353 |   72452      89      255     2.9 |  5.616 % |
c |       252 |  197442   469153 |   79697     225      687     3.1 |  5.655 % |
c |       477 |  197220   468661 |   87667     412     1307     3.2 |  5.750 % |
c |       814 |  196904   467953 |   96434     704     2190     3.1 |  5.875 % |
c |      1320 |  196471   466986 |  106077    1158     3681     3.2 |  6.048 % |
c |      2079 |  196167   466308 |  116685    1871     6010     3.2 |  6.171 % |
c |      3218 |  195836   465572 |  128354    2968     9920     3.3 |  6.308 % |
c |      4926 |  194955   463609 |  141189    4564    16110     3.5 |  6.662 % |
c |      7488 |  193922   461305 |  155308    6992    26553     3.8 |  7.081 % |
c |     11332 |  192840   458888 |  170839   10695    42311     4.0 |  7.511 % |
c |     17098 |  191223   455262 |  187923   16272    69453     4.3 |  8.158 % |
c |     25748 |  190082   452704 |  206715   24782   119823     4.8 |  8.608 % |
c |     38722 |  188731   449669 |  227387   37598   214553     5.7 |  9.163 % |
c |     58183 |  187556   447017 |  250126   56913   380254     6.7 |  9.644 % |
c |     87375 |  186779   445255 |  275138   85988   669238     7.8 |  9.978 % |
c |    131165 |  186233   444013 |  302652  129714  1246271     9.6 | 10.218 % |
c |    196849 |  185858   443159 |  332917  195328  2348150    12.0 | 10.368 % |
c |    295375 |  185670   442736 |  366209  293816  5271963    17.9 | 10.452 % |
#### 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.79 0.94 0.92 2/54 32670
Raw data (stat): 32670 (runsolver) R 32669 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 474291168 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.0006 s]
Raw data (loadavg): 0.82 0.94 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 6055 0 0 0 984 14 0 0 25 0 1 0 474291168 30326784 5879 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7404 5879 603 41 0 7363 0
vsize: 29616
[startup+20.0014 s]
Raw data (loadavg): 0.85 0.94 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 6092 0 0 0 1984 14 0 0 25 0 1 0 474291168 30461952 5916 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7437 5916 603 41 0 7396 0
vsize: 29748
[startup+30.0017 s]
Raw data (loadavg): 0.87 0.95 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 6126 0 0 0 2984 14 0 0 25 0 1 0 474291168 30461952 5950 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7437 5950 603 41 0 7396 0
vsize: 29748
[startup+40.002 s]
Raw data (loadavg): 0.89 0.95 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 6156 0 0 0 3984 15 0 0 25 0 1 0 474291168 30597120 5980 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7470 5980 603 41 0 7429 0
vsize: 29880
[startup+50.0028 s]
Raw data (loadavg): 0.91 0.95 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 6182 0 0 0 4983 15 0 0 25 0 1 0 474291168 30732288 6006 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7503 6006 603 41 0 7462 0
vsize: 30012
[startup+60.0043 s]
Raw data (loadavg): 0.92 0.95 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 6207 0 0 0 5983 15 0 0 25 0 1 0 474291168 30867456 6031 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7536 6031 603 41 0 7495 0
vsize: 30144
[startup+70.0043 s]
Raw data (loadavg): 0.93 0.95 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 6237 0 0 0 6983 16 0 0 25 0 1 0 474291168 31055872 6061 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7582 6061 603 41 0 7541 0
vsize: 30328
[startup+80.0041 s]
Raw data (loadavg): 0.94 0.95 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 6266 0 0 0 7983 16 0 0 25 0 1 0 474291168 31055872 6090 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7582 6090 603 41 0 7541 0
vsize: 30328
[startup+90.0053 s]
Raw data (loadavg): 0.95 0.95 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 6300 0 0 0 8982 17 0 0 25 0 1 0 474291168 31191040 6124 4294967295 134512640 134672761 3221224544 3221223760 134557650 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7615 6124 603 41 0 7574 0
vsize: 30460
[startup+100.006 s]
Raw data (loadavg): 0.96 0.95 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 6335 0 0 0 9982 17 0 0 25 0 1 0 474291168 31326208 6159 4294967295 134512640 134672761 3221224544 3221223700 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7648 6159 603 41 0 7607 0
vsize: 30592
[startup+110.006 s]
Raw data (loadavg): 0.96 0.95 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 6376 0 0 0 10982 18 0 0 25 0 1 0 474291168 31461376 6200 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7681 6200 603 41 0 7640 0
vsize: 30724
[startup+120.008 s]
Raw data (loadavg): 0.97 0.95 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 6413 0 0 0 11981 18 0 0 25 0 1 0 474291168 31596544 6237 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7714 6237 603 41 0 7673 0
vsize: 30856
[startup+130.008 s]
Raw data (loadavg): 0.97 0.96 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 6452 0 0 0 12981 19 0 0 25 0 1 0 474291168 31989760 6276 4294967295 134512640 134672761 3221224544 3221223680 134560608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7810 6276 603 41 0 7769 0
vsize: 31240
[startup+140.009 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 6497 0 0 0 13981 19 0 0 25 0 1 0 474291168 32124928 6321 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7843 6321 603 41 0 7802 0
vsize: 31372
[startup+150.009 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 6542 0 0 0 14981 19 0 0 25 0 1 0 474291168 32260096 6366 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7876 6366 603 41 0 7835 0
vsize: 31504
[startup+160.009 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 6581 0 0 0 15981 19 0 0 25 0 1 0 474291168 32391168 6405 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7908 6405 603 41 0 7867 0
vsize: 31632
[startup+170.009 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 6628 0 0 0 16981 20 0 0 25 0 1 0 474291168 32657408 6452 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7973 6452 603 41 0 7932 0
vsize: 31892
[startup+180.009 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 6678 0 0 0 17981 20 0 0 25 0 1 0 474291168 32792576 6502 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8006 6502 603 41 0 7965 0
vsize: 32024
[startup+190.01 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 6728 0 0 0 18981 20 0 0 25 0 1 0 474291168 32923648 6552 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8038 6552 603 41 0 7997 0
vsize: 32152
[startup+200.009 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 6766 0 0 0 19981 20 0 0 25 0 1 0 474291168 33058816 6590 4294967295 134512640 134672761 3221224544 3221223692 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8071 6590 603 41 0 8030 0
vsize: 32284
[startup+210.01 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 6822 0 0 0 20981 20 0 0 25 0 1 0 474291168 33329152 6646 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8137 6646 603 41 0 8096 0
vsize: 32548
[startup+220.011 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 6878 0 0 0 21981 20 0 0 25 0 1 0 474291168 33595392 6702 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8202 6702 603 41 0 8161 0
vsize: 32808
[startup+230.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 6940 0 0 0 22981 20 0 0 25 0 1 0 474291168 33865728 6764 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8268 6764 603 41 0 8227 0
vsize: 33072
[startup+240.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 6999 0 0 0 23981 21 0 0 25 0 1 0 474291168 34258944 6823 4294967295 134512640 134672761 3221224544 3221223680 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8364 6823 603 41 0 8323 0
vsize: 33456
[startup+250.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 7066 0 0 0 24981 21 0 0 25 0 1 0 474291168 34529280 6890 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8430 6890 603 41 0 8389 0
vsize: 33720
[startup+260.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 7126 0 0 0 25981 21 0 0 25 0 1 0 474291168 34799616 6950 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8496 6950 603 41 0 8455 0
vsize: 33984
[startup+270.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 7175 0 0 0 26981 21 0 0 25 0 1 0 474291168 34934784 6999 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8529 6999 603 41 0 8488 0
vsize: 34116
[startup+280.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 7228 0 0 0 27981 22 0 0 25 0 1 0 474291168 35201024 7052 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8594 7052 603 41 0 8553 0
vsize: 34376
[startup+290.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 7281 0 0 0 28981 22 0 0 25 0 1 0 474291168 35336192 7105 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8627 7105 603 41 0 8586 0
vsize: 34508
[startup+300.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 7327 0 0 0 29981 22 0 0 25 0 1 0 474291168 35602432 7151 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8692 7151 603 41 0 8651 0
vsize: 34768
[startup+310.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 7376 0 0 0 30981 22 0 0 25 0 1 0 474291168 35737600 7200 4294967295 134512640 134672761 3221224544 3221223668 134566045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8725 7200 603 41 0 8684 0
vsize: 34900
[startup+320.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 7425 0 0 0 31981 22 0 0 25 0 1 0 474291168 36003840 7249 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8790 7249 603 41 0 8749 0
vsize: 35160
[startup+330.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 7496 0 0 0 32981 23 0 0 25 0 1 0 474291168 36274176 7320 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8856 7320 603 41 0 8815 0
vsize: 35424
[startup+340.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 7614 0 0 0 33981 23 0 0 25 0 1 0 474291168 36671488 7438 4294967295 134512640 134672761 3221224544 3221223712 134560785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8953 7438 603 41 0 8912 0
vsize: 35812
[startup+350.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 7697 0 0 0 34981 23 0 0 25 0 1 0 474291168 37076992 7521 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9052 7521 603 41 0 9011 0
vsize: 36208
[startup+360.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 7757 0 0 0 35981 23 0 0 25 0 1 0 474291168 37208064 7581 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9084 7581 603 41 0 9043 0
vsize: 36336
[startup+370.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 7814 0 0 0 36981 24 0 0 25 0 1 0 474291168 37478400 7638 4294967295 134512640 134672761 3221224544 3221223668 134566092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9150 7638 603 41 0 9109 0
vsize: 36600
[startup+380.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 7865 0 0 0 37981 24 0 0 25 0 1 0 474291168 37613568 7689 4294967295 134512640 134672761 3221224544 3221223680 134560657 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9183 7689 603 41 0 9142 0
vsize: 36732
[startup+390.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 7979 0 0 0 38980 24 0 0 25 0 1 0 474291168 38150144 7803 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9314 7803 603 41 0 9273 0
vsize: 37256
[startup+400.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 8053 0 0 0 39980 25 0 0 25 0 1 0 474291168 38420480 7877 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9380 7877 603 41 0 9339 0
vsize: 37520
[startup+410.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 8118 0 0 0 40980 26 0 0 25 0 1 0 474291168 38690816 7942 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9446 7942 603 41 0 9405 0
vsize: 37784
[startup+420.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 8193 0 0 0 41980 26 0 0 25 0 1 0 474291168 38961152 8017 4294967295 134512640 134672761 3221224544 3221223688 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9512 8017 603 41 0 9471 0
vsize: 38048
[startup+430.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 8282 0 0 0 42980 26 0 0 25 0 1 0 474291168 39366656 8106 4294967295 134512640 134672761 3221224544 3221223668 134566018 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9611 8106 603 41 0 9570 0
vsize: 38444
[startup+440.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 8374 0 0 0 43980 26 0 0 25 0 1 0 474291168 39636992 8198 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9677 8198 603 41 0 9636 0
vsize: 38708
[startup+450.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 8554 0 0 0 44979 27 0 0 25 0 1 0 474291168 40972288 8378 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10003 8378 603 41 0 9962 0
vsize: 40012
[startup+460.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 8643 0 0 0 45979 27 0 0 25 0 1 0 474291168 41242624 8467 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10069 8467 603 41 0 10028 0
vsize: 40276
[startup+470.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 8711 0 0 0 46979 28 0 0 25 0 1 0 474291168 41512960 8535 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10135 8535 603 41 0 10094 0
vsize: 40540
[startup+480.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 8822 0 0 0 47978 28 0 0 25 0 1 0 474291168 41910272 8646 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10232 8646 603 41 0 10191 0
vsize: 40928
[startup+490.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 8918 0 0 0 48978 28 0 0 25 0 1 0 474291168 42307584 8742 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10329 8742 603 41 0 10288 0
vsize: 41316
[startup+500.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 9015 0 0 0 49978 28 0 0 25 0 1 0 474291168 42704896 8839 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10426 8839 603 41 0 10385 0
vsize: 41704
[startup+510.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 9109 0 0 0 50978 29 0 0 25 0 1 0 474291168 43110400 8933 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10525 8933 603 41 0 10484 0
vsize: 42100
[startup+520.02 s]
Raw data (loadavg): 1.07 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 9181 0 0 0 51978 29 0 0 25 0 1 0 474291168 43380736 9005 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10591 9005 603 41 0 10550 0
vsize: 42364
[startup+530.02 s]
Raw data (loadavg): 1.06 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 9263 0 0 0 52978 29 0 0 25 0 1 0 474291168 43642880 9087 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10655 9087 603 41 0 10614 0
vsize: 42620
[startup+540.02 s]
Raw data (loadavg): 1.05 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 9334 0 0 0 53978 29 0 0 25 0 1 0 474291168 43913216 9158 4294967295 134512640 134672761 3221224544 3221223712 134564722 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10721 9158 603 41 0 10680 0
vsize: 42884
[startup+550.02 s]
Raw data (loadavg): 1.04 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 9411 0 0 0 54978 29 0 0 25 0 1 0 474291168 44306432 9235 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10817 9235 603 41 0 10776 0
vsize: 43268
[startup+560.02 s]
Raw data (loadavg): 1.03 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 9476 0 0 0 55978 30 0 0 25 0 1 0 474291168 44576768 9300 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10883 9300 603 41 0 10842 0
vsize: 43532
[startup+570.02 s]
Raw data (loadavg): 1.03 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 9592 0 0 0 56978 30 0 0 25 0 1 0 474291168 44974080 9416 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10980 9416 603 41 0 10939 0
vsize: 43920
[startup+580.02 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 9672 0 0 0 57978 30 0 0 25 0 1 0 474291168 45375488 9496 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11078 9496 603 41 0 11037 0
vsize: 44312
[startup+590.021 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 9771 0 0 0 58978 31 0 0 25 0 1 0 474291168 45645824 9595 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11144 9595 603 41 0 11103 0
vsize: 44576
[startup+600.021 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 9878 0 0 0 59978 31 0 0 25 0 1 0 474291168 46182400 9702 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11275 9702 603 41 0 11234 0
vsize: 45100
[startup+610.022 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 9965 0 0 0 60978 31 0 0 25 0 1 0 474291168 46448640 9789 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11340 9789 603 41 0 11299 0
vsize: 45360
[startup+620.021 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 10036 0 0 0 61978 31 0 0 25 0 1 0 474291168 46718976 9860 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11406 9860 603 41 0 11365 0
vsize: 45624
[startup+630.021 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 10117 0 0 0 62977 32 0 0 25 0 1 0 474291168 47124480 9941 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11505 9941 603 41 0 11464 0
vsize: 46020
[startup+640.021 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 10215 0 0 0 63977 32 0 0 25 0 1 0 474291168 47529984 10039 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11604 10039 603 41 0 11563 0
vsize: 46416
[startup+650.02 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 10301 0 0 0 64976 33 0 0 25 0 1 0 474291168 47792128 10125 4294967295 134512640 134672761 3221224544 3221223700 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11668 10125 603 41 0 11627 0
vsize: 46672
[startup+660.021 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 10393 0 0 0 65976 33 0 0 25 0 1 0 474291168 48197632 10217 4294967295 134512640 134672761 3221224544 3221223668 134566130 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11767 10217 603 41 0 11726 0
vsize: 47068
[startup+670.021 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 10569 0 0 0 66976 34 0 0 25 0 1 0 474291168 48869376 10393 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11931 10393 603 41 0 11890 0
vsize: 47724
[startup+680.021 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 10750 0 0 0 67976 34 0 0 25 0 1 0 474291168 49537024 10574 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12094 10574 603 41 0 12053 0
vsize: 48376
[startup+690.021 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 10851 0 0 0 68976 34 0 0 25 0 1 0 474291168 49942528 10675 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12193 10675 603 41 0 12152 0
vsize: 48772
[startup+700.021 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 11049 0 0 0 69975 35 0 0 25 0 1 0 474291168 50749440 10873 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12390 10873 603 41 0 12349 0
vsize: 49560
[startup+710.021 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 11201 0 0 0 70975 35 0 0 25 0 1 0 474291168 51421184 11025 4294967295 134512640 134672761 3221224544 3221223696 134565039 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12554 11025 603 41 0 12513 0
vsize: 50216
[startup+720.021 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 11394 0 0 0 71974 36 0 0 25 0 1 0 474291168 52088832 11218 4294967295 134512640 134672761 3221224544 3221223760 134557650 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12717 11218 603 41 0 12676 0
vsize: 50868
[startup+730.021 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 11498 0 0 0 72974 36 0 0 25 0 1 0 474291168 52629504 11322 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12849 11322 603 41 0 12808 0
vsize: 51396
[startup+740.021 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 11614 0 0 0 73974 37 0 0 25 0 1 0 474291168 53035008 11438 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12948 11438 603 41 0 12907 0
vsize: 51792
[startup+750.021 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 11705 0 0 0 74973 38 0 0 25 0 1 0 474291168 53440512 11529 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13047 11529 603 41 0 13006 0
vsize: 52188
[startup+760.022 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 11836 0 0 0 75973 38 0 0 25 0 1 0 474291168 53846016 11660 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13146 11660 603 41 0 13105 0
vsize: 52584
[startup+770.023 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 11929 0 0 0 76973 38 0 0 25 0 1 0 474291168 54251520 11753 4294967295 134512640 134672761 3221224544 3221223692 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13245 11753 603 41 0 13204 0
vsize: 52980
[startup+780.023 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 12168 0 0 0 77972 40 0 0 25 0 1 0 474291168 55189504 11992 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13474 11992 603 41 0 13433 0
vsize: 53896
[startup+790.024 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 12328 0 0 0 78972 40 0 0 25 0 1 0 474291168 55865344 12152 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13639 12152 603 41 0 13598 0
vsize: 54556
[startup+800.024 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 12645 0 0 0 79971 41 0 0 25 0 1 0 474291168 58122240 12469 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14190 12469 603 41 0 14149 0
vsize: 56760
[startup+810.025 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 13274 0 0 0 80969 43 0 0 25 0 1 0 474291168 60674048 13098 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14813 13098 603 41 0 14772 0
vsize: 59252
[startup+820.025 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 13388 0 0 0 81969 44 0 0 25 0 1 0 474291168 61210624 13212 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14944 13212 603 41 0 14903 0
vsize: 59776
[startup+830.024 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 13527 0 0 0 82969 44 0 0 25 0 1 0 474291168 61747200 13351 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15075 13351 603 41 0 15034 0
vsize: 60300
[startup+840.025 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 13888 0 0 0 83968 45 0 0 25 0 1 0 474291168 63221760 13712 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15435 13712 603 41 0 15394 0
vsize: 61740
[startup+850.025 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 14047 0 0 0 84967 46 0 0 25 0 1 0 474291168 63893504 13871 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15599 13871 603 41 0 15558 0
vsize: 62396
[startup+860.026 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 14158 0 0 0 85967 46 0 0 25 0 1 0 474291168 64299008 13982 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15698 13982 603 41 0 15657 0
vsize: 62792
[startup+870.027 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 14242 0 0 0 86966 47 0 0 25 0 1 0 474291168 64569344 14066 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15764 14066 603 41 0 15723 0
vsize: 63056
[startup+880.027 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 14485 0 0 0 87965 47 0 0 25 0 1 0 474291168 65646592 14309 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16027 14309 603 41 0 15986 0
vsize: 64108
[startup+890.027 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 14705 0 0 0 88965 48 0 0 25 0 1 0 474291168 66457600 14529 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16225 14529 603 41 0 16184 0
vsize: 64900
[startup+900.027 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 14898 0 0 0 89965 49 0 0 25 0 1 0 474291168 67260416 14722 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16421 14722 603 41 0 16380 0
vsize: 65684
[startup+910.028 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 15161 0 0 0 90964 49 0 0 25 0 1 0 474291168 68321280 14985 4294967295 134512640 134672761 3221224544 3221223484 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16680 14985 603 41 0 16639 0
vsize: 66720
[startup+920.029 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 15300 0 0 0 91964 50 0 0 25 0 1 0 474291168 68853760 15124 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16810 15124 603 41 0 16769 0
vsize: 67240
[startup+930.028 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 15483 0 0 0 92963 50 0 0 25 0 1 0 474291168 69652480 15307 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17005 15307 603 41 0 16964 0
vsize: 68020
[startup+940.028 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 15683 0 0 0 93963 51 0 0 25 0 1 0 474291168 70324224 15507 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17169 15507 603 41 0 17128 0
vsize: 68676
[startup+950.028 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 15771 0 0 0 94963 51 0 0 25 0 1 0 474291168 70729728 15595 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17268 15595 603 41 0 17227 0
vsize: 69072
[startup+960.029 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 15918 0 0 0 95963 51 0 0 25 0 1 0 474291168 71266304 15742 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17399 15742 603 41 0 17358 0
vsize: 69596
[startup+970.029 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 16053 0 0 0 96963 51 0 0 25 0 1 0 474291168 71806976 15877 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17531 15877 603 41 0 17490 0
vsize: 70124
[startup+980.028 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 16199 0 0 0 97963 52 0 0 25 0 1 0 474291168 72474624 16023 4294967295 134512640 134672761 3221224544 3221223696 134542690 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17694 16023 603 41 0 17653 0
vsize: 70776
[startup+990.029 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 16572 0 0 0 98962 53 0 0 25 0 1 0 474291168 73940992 16396 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18052 16396 603 41 0 18011 0
vsize: 72208
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 16756 0 0 0 99961 54 0 0 25 0 1 0 474291168 74747904 16580 4294967295 134512640 134672761 3221224544 3221223744 134557922 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18249 16580 603 41 0 18208 0
vsize: 72996
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 16915 0 0 0 100962 54 0 0 25 0 1 0 474291168 75284480 16739 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18380 16739 603 41 0 18339 0
vsize: 73520
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 17046 0 0 0 101961 54 0 0 25 0 1 0 474291168 75816960 16870 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18510 16870 603 41 0 18469 0
vsize: 74040
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 17185 0 0 0 102961 55 0 0 25 0 1 0 474291168 76357632 17009 4294967295 134512640 134672761 3221224544 3221223724 134565156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18642 17009 603 41 0 18601 0
vsize: 74568
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 17324 0 0 0 103961 55 0 0 25 0 1 0 474291168 76894208 17148 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18773 17148 603 41 0 18732 0
vsize: 75092
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 17471 0 0 0 104960 56 0 0 25 0 1 0 474291168 77570048 17295 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18938 17295 603 41 0 18897 0
vsize: 75752
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 17590 0 0 0 105960 56 0 0 25 0 1 0 474291168 77971456 17414 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19036 17414 603 41 0 18995 0
vsize: 76144
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 17590 0 0 0 106960 56 0 0 25 0 1 0 474291168 77971456 17414 4294967295 134512640 134672761 3221224544 3221223712 134564705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19036 17414 603 41 0 18995 0
vsize: 76144
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 17590 0 0 0 107960 56 0 0 25 0 1 0 474291168 77971456 17414 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19036 17414 603 41 0 18995 0
vsize: 76144
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 17590 0 0 0 108960 56 0 0 25 0 1 0 474291168 77971456 17414 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19036 17414 603 41 0 18995 0
vsize: 76144
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 17591 0 0 0 109960 56 0 0 25 0 1 0 474291168 77971456 17415 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19036 17415 603 41 0 18995 0
vsize: 76144
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 17591 0 0 0 110961 56 0 0 25 0 1 0 474291168 77971456 17415 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19036 17415 603 41 0 18995 0
vsize: 76144
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 17591 0 0 0 111961 56 0 0 25 0 1 0 474291168 77971456 17415 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19036 17415 603 41 0 18995 0
vsize: 76144
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 17591 0 0 0 112961 56 0 0 25 0 1 0 474291168 77971456 17415 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19036 17415 603 41 0 18995 0
vsize: 76144
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 17591 0 0 0 113961 56 0 0 25 0 1 0 474291168 77971456 17415 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19036 17415 603 41 0 18995 0
vsize: 76144
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 17591 0 0 0 114961 57 0 0 25 0 1 0 474291168 77971456 17415 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19036 17415 603 41 0 18995 0
vsize: 76144
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 17592 0 0 0 115961 57 0 0 25 0 1 0 474291168 77971456 17416 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19036 17416 603 41 0 18995 0
vsize: 76144
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 17592 0 0 0 116962 57 0 0 25 0 1 0 474291168 77971456 17416 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19036 17416 603 41 0 18995 0
vsize: 76144
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 17592 0 0 0 117962 57 0 0 25 0 1 0 474291168 77971456 17416 4294967295 134512640 134672761 3221224544 3221223668 134566077 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19036 17416 603 41 0 18995 0
vsize: 76144
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 17592 0 0 0 118962 57 0 0 25 0 1 0 474291168 77971456 17416 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19036 17416 603 41 0 18995 0
vsize: 76144
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 32670
Raw data (stat): 32670 (minisat+) R 32669 26667 26666 0 -1 0 17592 0 0 0 119962 57 0 0 25 0 1 0 474291168 77971456 17416 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19036 17416 603 41 0 18995 0
vsize: 76144
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.93 1/54 32670
Raw data (stat): 32670 (minisat+) Z 32669 26667 26666 0 -1 12 17594 0 0 0 119962 60 0 0 25 0 1 0 474291168 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.07
CPU time (s): 1200.23
CPU user time (s): 1199.63
CPU system time (s): 0.604908
CPU usage (%): 100.013
Max. virtual memory (Kb): 76144
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####