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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. 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.
  4. 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

Namenormalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-vpm2.opb
MD5SUM766b2fe57cb2084b069363491485612e
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 97
Optimality of the best value was proved NO
Number of terms in the objective function 168
Biggest coefficient in the objective function 5
Number of bits for the biggest coefficient in the objective function 3
Sum of the numbers in the objective function 504
Number of bits of the sum of numbers in the objective function 9
Biggest number in a constraint 16000000
Number of bits of the biggest number in a constraint 24
Biggest sum of numbers in a constraint 241094849
Number of bits of the biggest sum of numbers28
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1175.23
Number of variables2754
Total number of constraints444
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints444
Minimum length of a constraint11
Maximum length of a constraint84

Trace number 13786 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc23 THE 2005-04-20 21:45:07 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13961 boxname=wulflinc23 idbench=1074 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  766b2fe57cb2084b069363491485612e  /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-vpm2.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-vpm2.opb /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-vpm2.opb
IDLAUNCH: 13961
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        682584 kB
Buffers:         32148 kB
Cached:         283904 kB
SwapCached:        624 kB
Active:          35828 kB
Inactive:       282484 kB
HighTotal:      131008 kB
HighFree:         3136 kB
LowTotal:       903652 kB
LowFree:        679448 kB
SwapTotal:     2097136 kB
SwapFree:      2095788 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5220 kB
Slab:            28204 kB
Committed_AS:    63624 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-20 22:05:09 (client local time) WITH STATUS 0 IN 1200.52 SECONDS
stats: 13961 7 1200.52 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 486 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ##############################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 485]---> BDD-cost:   10
c ---[ 484]---> BDD-cost:   10
c ---[ 483]---> BDD-cost:   10
c ---[ 482]---> BDD-cost:   10
c ---[ 481]---> BDD-cost:   10
c ---[ 480]---> BDD-cost:   10
c ---[ 479]---> BDD-cost:   10
c ---[ 478]---> BDD-cost:   10
c ---[ 477]---> BDD-cost:   10
c ---[ 474]---> BDD-cost:   10
c ---[ 473]---> BDD-cost:   10
c ---[ 472]---> BDD-cost:   10
c ---[ 471]---> BDD-cost:   10
c ---[ 468]---> BDD-cost:   10
c ---[ 467]---> BDD-cost:   10
c ---[ 466]---> BDD-cost:   10
c ---[ 465]---> BDD-cost:   10
c ---[ 462]---> BDD-cost:   10
c ---[ 459]---> BDD-cost:   10
c ---[ 458]---> BDD-cost:   10
c ---[ 457]---> BDD-cost:   10
c ---[ 454]---> BDD-cost:   10
c ---[ 453]---> BDD-cost:   10
c ---[ 452]---> BDD-cost:   10
c ---[ 451]---> BDD-cost:   10
c ---[ 450]---> BDD-cost:   10
c ---[ 448]---> BDD-cost:   10
c ---[ 447]---> BDD-cost:   10
c ---[ 446]---> BDD-cost:   10
c ---[ 445]---> BDD-cost:   10
c ---[ 444]---> BDD-cost:   10
c ---[ 441]---> BDD-cost:   10
c ---[ 440]---> BDD-cost:   10
c ---[ 439]---> BDD-cost:   10
c ---[ 433]---> BDD-cost:   10
c ---[ 427]---> BDD-cost:   10
c ---[ 422]---> BDD-cost:   10
c ---[ 421]---> BDD-cost:   10
c ---[ 415]---> BDD-cost:   10
c ---[ 409]---> BDD-cost:   10
c ---[ 408]---> BDD-cost:   10
c ---[ 402]---> BDD-cost:   10
c ---[ 397]---> BDD-cost:   10
c ---[ 396]---> BDD-cost:   10
c ---[ 391]---> BDD-cost:   10
c ---[ 390]---> BDD-cost:   10
c ---[ 386]---> BDD-cost:   10
c ---[ 385]---> BDD-cost:   10
c ---[ 384]---> BDD-cost:   10
c ---[ 380]---> BDD-cost:   10
c ---[ 379]---> BDD-cost:   10
c ---[ 378]---> BDD-cost:   10
c ---[ 374]---> BDD-cost:   10
c ---[ 373]---> BDD-cost:   10
c ---[ 372]---> BDD-cost:   10
c ---[ 368]---> BDD-cost:   10
c ---[ 367]---> BDD-cost:   10
c ---[ 366]---> BDD-cost:   10
c ---[ 365]---> BDD-cost:   10
c ---[ 364]---> BDD-cost:   10
c ---[ 359]---> BDD-cost:   10
c ---[ 353]---> BDD-cost:   10
c ---[ 347]---> BDD-cost:   10
c ---[ 339]---> BDD-cost:   10
c ---[ 333]---> BDD-cost:   10
c ---[ 327]---> BDD-cost:   10
c ---[ 321]---> BDD-cost:   10
c ---[ 317]---> BDD-cost:   17
c ---[ 316]---> BDD-cost:   17
c ---[ 315]---> BDD-cost:   17
c ---[ 314]---> BDD-cost:   17
c ---[ 313]---> BDD-cost:   17
c ---[ 312]---> BDD-cost:   17
c ---[ 310]---> BDD-cost:   17
c ---[ 309]---> BDD-cost:   17
c ---[ 308]---> BDD-cost:   17
c ---[ 307]---> BDD-cost:   17
c ---[ 306]---> BDD-cost:   17
c ---[ 302]---> BDD-cost:   16
c ---[ 301]---> BDD-cost:   16
c ---[ 300]---> BDD-cost:   16
c ---[ 295]---> BDD-cost:   16
c ---[ 294]---> BDD-cost:   16
c ---[ 290]---> BDD-cost:   18
c ---[ 289]---> BDD-cost:   18
c ---[ 288]---> BDD-cost:   18
c ---[ 287]---> BDD-cost:   16
c ---[ 286]---> BDD-cost:   16
c ---[ 285]---> BDD-cost:   16
c ---[ 284]---> BDD-cost:   16
c ---[ 283]---> BDD-cost:   16
c ---[ 282]---> BDD-cost:   16
c ---[ 280]---> BDD-cost:   16
c ---[ 279]---> BDD-cost:   16
c ---[ 278]---> BDD-cost:   16
c ---[ 277]---> BDD-cost:   16
c ---[ 276]---> BDD-cost:   16
c ---[ 274]---> BDD-cost:11304
c ---[ 264]---> BDD-cost:10343
c ---[ 260]---> BDD-cost:19664
c ---[ 258]---> BDD-cost:19664
c ---[ 256]---> BDD-cost:16439
c ---[ 254]---> BDD-cost:16439
c ---[ 252]---> BDD-cost:20156
c ---[ 250]---> BDD-cost: 4480
c ---[ 248]---> BDD-cost: 7193
c ---[ 246]---> BDD-cost: 7455
c ---[ 244]---> BDD-cost: 7455
c ---[ 242]---> BDD-cost: 6299
c ---[ 236]---> BDD-cost: 8137
c ---[ 234]---> BDD-cost:15538
c ---[ 232]---> BDD-cost:11932
c ---[ 224]---> BDD-cost: 9270
c ---[ 222]---> BDD-cost:17235
c ---[ 216]---> BDD-cost: 5723
c ---[ 214]---> BDD-cost: 7949
c ---[ 212]---> BDD-cost: 8185
c ---[ 210]---> BDD-cost:18332
c ---[ 208]---> BDD-cost:13927
c ---[ 206]---> BDD-cost:13927
c ---[ 204]---> BDD-cost:13927
c ---[ 202]---> BDD-cost:13927
c ---[ 200]---> BDD-cost:12600
c ---[ 198]---> BDD-cost:22214
c ---[ 196]---> BDD-cost:16579
c ---[ 194]---> BDD-cost:16579
c ---[ 192]---> BDD-cost:16579
c ---[ 191]---> BDD-cost:  237
c ---[ 190]---> BDD-cost:  601
c ---[ 189]---> BDD-cost:  600
c ---[ 188]---> BDD-cost: 1143
c ---[ 187]---> BDD-cost: 1480
c ---[ 186]---> BDD-cost: 1473
c ---[ 185]---> BDD-cost:  273
c ---[ 184]---> BDD-cost:  768
c ---[ 183]---> BDD-cost:  767
c ---[ 182]---> BDD-cost: 1522
c ---[ 181]---> BDD-cost: 2005
c ---[ 180]---> BDD-cost: 2004
c ---[ 179]---> BDD-cost:  275
c ---[ 178]---> BDD-cost:  777
c ---[ 177]---> BDD-cost:  771
c ---[ 176]---> BDD-cost: 1542
c ---[ 175]---> BDD-cost: 2010
c ---[ 174]---> BDD-cost: 2007
c ---[ 173]---> BDD-cost:  102
c ---[ 172]---> BDD-cost:  244
c ---[ 171]---> BDD-cost:  240
c ---[ 170]---> BDD-cost:  444
c ---[ 169]---> BDD-cost:  584
c ---[ 168]---> BDD-cost:  579
c ---[ 167]---> BDD-cost:    3
c ---[ 166]---> BDD-cost:    3
c ---[ 165]---> BDD-cost:    3
c ---[ 164]---> BDD-cost:    3
c ---[ 163]---> BDD-cost:    3
c ---[ 162]---> BDD-cost:    3
c ---[ 161]---> BDD-cost:    3
c ---[ 160]---> BDD-cost:    3
c ---[ 159]---> BDD-cost:    3
c ---[ 158]---> BDD-cost:   10
c ---[ 157]---> BDD-cost:   10
c ---[ 156]---> BDD-cost:    3
c ---[ 155]---> BDD-cost:    3
c ---[ 154]---> BDD-cost:    3
c ---[ 153]---> BDD-cost:    3
c ---[ 152]---> BDD-cost:   10
c ---[ 151]---> BDD-cost:   10
c ---[ 150]---> BDD-cost:    3
c ---[ 149]---> BDD-cost:    3
c ---[ 148]---> BDD-cost:    3
c ---[ 147]---> BDD-cost:    3
c ---[ 146]---> BDD-cost:   10
c ---[ 145]---> BDD-cost:   10
c ---[ 144]---> BDD-cost:    3
c ---[ 142]---> BDD-cost:   10
c ---[ 141]---> BDD-cost:    3
c ---[ 140]---> BDD-cost:    3
c ---[ 139]---> BDD-cost:    3
c ---[ 138]---> BDD-cost:   10
c ---[ 136]---> BDD-cost:    3
c ---[ 135]---> BDD-cost:    3
c ---[ 134]---> BDD-cost:    3
c ---[ 133]---> BDD-cost:    3
c ---[ 132]---> BDD-cost:    3
c ---[ 130]---> BDD-cost:    3
c ---[ 129]---> BDD-cost:    3
c ---[ 128]---> BDD-cost:    3
c ---[ 127]---> BDD-cost:    3
c ---[ 126]---> BDD-cost:    3
c ---[ 124]---> BDD-cost:   10
c ---[ 123]---> BDD-cost:    3
c ---[ 122]---> BDD-cost:    3
c ---[ 121]---> BDD-cost:    3
c ---[ 120]---> BDD-cost:   10
c ---[ 116]---> BDD-cost:   10
c ---[ 115]---> BDD-cost:    3
c ---[ 114]---> BDD-cost:    9
c ---[ 110]---> BDD-cost:   10
c ---[ 109]---> BDD-cost:    3
c ---[ 108]---> BDD-cost:    9
c ---[ 104]---> BDD-cost:    3
c ---[ 103]---> BDD-cost:    3
c ---[ 102]---> BDD-cost:    9
c ---[  98]---> BDD-cost:   10
c ---[  97]---> BDD-cost:    3
c ---[  96]---> BDD-cost:    9
c ---[  91]---> BDD-cost:    3
c ---[  90]---> BDD-cost:    3
c ---[  85]---> BDD-cost:   10
c ---[  84]---> BDD-cost:    3
c ---[  79]---> BDD-cost:    3
c ---[  78]---> BDD-cost:    3
c ---[  73]---> BDD-cost:    3
c ---[  72]---> BDD-cost:    3
c ---[  68]---> BDD-cost:    3
c ---[  67]---> BDD-cost:    3
c ---[  66]---> BDD-cost:    3
c ---[  62]---> BDD-cost:    3
c ---[  61]---> BDD-cost:    3
c ---[  60]---> BDD-cost:    3
c ---[  56]---> BDD-cost:    3
c ---[  55]---> BDD-cost:    3
c ---[  54]---> BDD-cost:    3
c ---[  50]---> BDD-cost:    3
c ---[  49]---> BDD-cost:    3
c ---[  48]---> BDD-cost:    3
c ---[  47]---> BDD-cost:    3
c ---[  46]---> BDD-cost:    3
c ---[  45]---> BDD-cost:    9
c ---[  44]---> BDD-cost:    9
c ---[  43]---> BDD-cost:    9
c ---[  42]---> BDD-cost:    9
c ---[  41]---> BDD-cost:    3
c ---[  40]---> BDD-cost:   10
c ---[  39]---> BDD-cost:    9
c ---[  38]---> BDD-cost:    9
c ---[  37]---> BDD-cost:    9
c ---[  36]---> BDD-cost:    9
c ---[  35]---> BDD-cost:    3
c ---[  34]---> BDD-cost:   10
c ---[  33]---> BDD-cost:    8
c ---[  32]---> BDD-cost:    8
c ---[  31]---> BDD-cost:    8
c ---[  30]---> BDD-cost:    8
c ---[  29]---> BDD-cost:    3
c ---[  28]---> BDD-cost:   10
c ---[  27]---> BDD-cost:    8
c ---[  26]---> BDD-cost:    8
c ---[  25]---> BDD-cost:    8
c ---[  24]---> BDD-cost:    8
c ---[  22]---> BDD-cost:   10
c ---[  21]---> BDD-cost:    3
c ---[  20]---> BDD-cost:    9
c ---[  19]---> BDD-cost:    9
c ---[  18]---> BDD-cost:    9
c ---[  16]---> BDD-cost:   10
c ---[  15]---> BDD-cost:    3
c ---[  14]---> BDD-cost:    9
c ---[  13]---> BDD-cost:    9
c ---[  12]---> BDD-cost:    9
c ---[  10]---> BDD-cost:   10
c ---[   9]---> BDD-cost:    3
c ---[   8]---> BDD-cost:    9
c ---[   7]---> BDD-cost:    9
c ---[   6]---> BDD-cost:    9
c ---[   4]---> BDD-cost:   10
c ---[   3]---> BDD-cost:    3
c ---[   2]---> BDD-cost:    8
c ---[   1]---> BDD-cost:    8
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 1104149  3099037 |  368049       0        0     nan |  0.000 % |
c |       100 | 1104116  3098947 |  404853      90     2073    23.0 |  0.279 % |
c |       251 | 1104089  3098870 |  445339     238     4125    17.3 |  0.281 % |
c |       476 | 1103900  3098404 |  489873     459    10218    22.3 |  0.295 % |
c |       814 | 1103869  3098316 |  538860     793    18675    23.5 |  0.297 % |
c |      1321 | 1103759  3098006 |  592746    1287    35055    27.2 |  0.305 % |
c |      2081 | 1103656  3097707 |  652021    2041    70243    34.4 |  0.312 % |
c |      3220 | 1103510  3097319 |  717223    3169   106047    33.5 |  0.323 % |
c |      4931 | 1103449  3097146 |  788945    4876   214269    43.9 |  0.323 % |
c |      7494 | 1103389  3096973 |  867840    7434   269669    36.3 |  0.328 % |
c |     11339 | 1103316  3096771 |  954624   11272   412524    36.6 |  0.333 % |
c |     17106 | 1103287  3096700 | 1050086   17035   704266    41.3 |  0.335 % |
c |     25756 | 1103264  3096647 | 1155095   25684  1370274    53.4 |  0.335 % |
c |     38730 | 1103264  3096647 | 1270604   38658  2428149    62.8 |  0.335 % |
c |     58193 | 1103264  3096647 | 1397665   58121  3530547    60.7 |  0.335 % |
c |     87385 | 1103264  3096647 | 1537432   87313 13340403   152.8 |  0.335 % |
c |    131174 | 1103148  3096333 | 1691175  131082 17339712   132.3 |  0.344 % |
#### 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.84 0.94 0.90 2/54 22877
Raw data (stat): 22877 (runsolver) R 22876 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 539779829 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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+9.99972 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 34656 0 0 0 916 82 0 0 25 0 1 0 539779829 149921792 32447 4294967295 134512640 134672761 3221224544 3221223744 134561967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36602 32447 603 41 0 36561 0
vsize: 146408
[startup+19.9999 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 35333 0 0 0 1914 83 0 0 25 0 1 0 539779829 152178688 33124 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37153 33124 603 41 0 37112 0
vsize: 148612
[startup+30.0001 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 35637 0 0 0 2913 85 0 0 25 0 1 0 539779829 153260032 33428 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37417 33428 603 41 0 37376 0
vsize: 149668
[startup+40.0002 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 35743 0 0 0 3912 85 0 0 25 0 1 0 539779829 153661440 33534 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37515 33534 603 41 0 37474 0
vsize: 150060
[startup+50.0007 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 35809 0 0 0 4911 85 0 0 25 0 1 0 539779829 153931776 33600 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37581 33600 603 41 0 37540 0
vsize: 150324
[startup+60.0001 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 35909 0 0 0 5911 86 0 0 25 0 1 0 539779829 154361856 33700 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37686 33700 603 41 0 37645 0
vsize: 150744
[startup+70 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 36282 0 0 0 6909 87 0 0 25 0 1 0 539779829 155443200 34073 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37950 34073 603 41 0 37909 0
vsize: 151800
[startup+80.0008 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 36345 0 0 0 7909 87 0 0 25 0 1 0 539779829 155709440 34136 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38015 34136 603 41 0 37974 0
vsize: 152060
[startup+90.0002 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 36431 0 0 0 8909 88 0 0 25 0 1 0 539779829 156164096 34222 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38126 34222 603 41 0 38085 0
vsize: 152504
[startup+100 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 36506 0 0 0 9908 88 0 0 25 0 1 0 539779829 156434432 34297 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38192 34297 603 41 0 38151 0
vsize: 152768
[startup+110.001 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 36630 0 0 0 10908 89 0 0 25 0 1 0 539779829 156835840 34421 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38290 34421 603 41 0 38249 0
vsize: 153160
[startup+120 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 36744 0 0 0 11908 89 0 0 25 0 1 0 539779829 157372416 34535 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38421 34535 603 41 0 38380 0
vsize: 153684
[startup+130 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 36856 0 0 0 12907 90 0 0 25 0 1 0 539779829 157773824 34647 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38519 34647 603 41 0 38478 0
vsize: 154076
[startup+140 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 36968 0 0 0 13907 90 0 0 25 0 1 0 539779829 158285824 34759 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38644 34759 603 41 0 38603 0
vsize: 154576
[startup+150 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 37082 0 0 0 14907 91 0 0 25 0 1 0 539779829 158814208 34873 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38773 34873 603 41 0 38732 0
vsize: 155092
[startup+160 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 37137 0 0 0 15907 91 0 0 25 0 1 0 539779829 158949376 34928 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38806 34928 603 41 0 38765 0
vsize: 155224
[startup+170 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 37213 0 0 0 16907 91 0 0 25 0 1 0 539779829 159346688 35004 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38903 35004 603 41 0 38862 0
vsize: 155612
[startup+180.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 37532 0 0 0 17906 92 0 0 25 0 1 0 539779829 160559104 35323 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39199 35323 603 41 0 39158 0
vsize: 156796
[startup+190 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 37654 0 0 0 18906 92 0 0 25 0 1 0 539779829 161091584 35445 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39329 35445 603 41 0 39288 0
vsize: 157316
[startup+200.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 37709 0 0 0 19906 92 0 0 25 0 1 0 539779829 161357824 35500 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39394 35500 603 41 0 39353 0
vsize: 157576
[startup+210.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 37873 0 0 0 20906 93 0 0 25 0 1 0 539779829 162029568 35664 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39558 35664 603 41 0 39517 0
vsize: 158232
[startup+220.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 38038 0 0 0 21905 94 0 0 25 0 1 0 539779829 162701312 35829 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39722 35829 603 41 0 39681 0
vsize: 158888
[startup+230.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 38188 0 0 0 22904 95 0 0 25 0 1 0 539779829 163233792 35979 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39852 35979 603 41 0 39811 0
vsize: 159408
[startup+240.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 38339 0 0 0 23904 95 0 0 25 0 1 0 539779829 163901440 36130 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40015 36130 603 41 0 39974 0
vsize: 160060
[startup+250.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 38502 0 0 0 24904 96 0 0 25 0 1 0 539779829 164700160 36293 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40210 36293 603 41 0 40169 0
vsize: 160840
[startup+260.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 38637 0 0 0 25904 96 0 0 25 0 1 0 539779829 165240832 36428 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40342 36428 603 41 0 40301 0
vsize: 161368
[startup+270.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 38796 0 0 0 26904 96 0 0 25 0 1 0 539779829 165916672 36587 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40507 36587 603 41 0 40466 0
vsize: 162028
[startup+280.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 38929 0 0 0 27903 97 0 0 25 0 1 0 539779829 166457344 36720 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40639 36720 603 41 0 40598 0
vsize: 162556
[startup+290.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 39030 0 0 0 28903 97 0 0 25 0 1 0 539779829 166862848 36821 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40738 36821 603 41 0 40697 0
vsize: 162952
[startup+300.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 39107 0 0 0 29902 98 0 0 25 0 1 0 539779829 167129088 36898 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40803 36898 603 41 0 40762 0
vsize: 163212
[startup+310.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 39153 0 0 0 30903 98 0 0 25 0 1 0 539779829 167260160 36944 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40835 36944 603 41 0 40794 0
vsize: 163340
[startup+320.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 39203 0 0 0 31902 99 0 0 25 0 1 0 539779829 167530496 36994 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40901 36994 603 41 0 40860 0
vsize: 163604
[startup+330.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 39271 0 0 0 32902 99 0 0 25 0 1 0 539779829 167800832 37062 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40967 37062 603 41 0 40926 0
vsize: 163868
[startup+340.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 39349 0 0 0 33902 99 0 0 25 0 1 0 539779829 168071168 37140 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41033 37140 603 41 0 40992 0
vsize: 164132
[startup+350.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 39417 0 0 0 34902 99 0 0 25 0 1 0 539779829 168337408 37208 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41098 37208 603 41 0 41057 0
vsize: 164392
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 39488 0 0 0 35902 100 0 0 25 0 1 0 539779829 168738816 37279 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41196 37279 603 41 0 41155 0
vsize: 164784
[startup+370.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 39551 0 0 0 36902 100 0 0 25 0 1 0 539779829 168873984 37342 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41229 37342 603 41 0 41188 0
vsize: 164916
[startup+380.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 39611 0 0 0 37902 100 0 0 25 0 1 0 539779829 169140224 37402 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41294 37402 603 41 0 41253 0
vsize: 165176
[startup+390.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 39679 0 0 0 38902 101 0 0 25 0 1 0 539779829 169410560 37470 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41360 37470 603 41 0 41319 0
vsize: 165440
[startup+400.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 39763 0 0 0 39901 101 0 0 25 0 1 0 539779829 169816064 37554 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41459 37554 603 41 0 41418 0
vsize: 165836
[startup+410.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 39849 0 0 0 40901 101 0 0 25 0 1 0 539779829 170086400 37640 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41525 37640 603 41 0 41484 0
vsize: 166100
[startup+420.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 39918 0 0 0 41902 101 0 0 25 0 1 0 539779829 170483712 37709 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41622 37709 603 41 0 41581 0
vsize: 166488
[startup+430.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 39968 0 0 0 42901 102 0 0 25 0 1 0 539779829 170618880 37759 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41655 37759 603 41 0 41614 0
vsize: 166620
[startup+440.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 39996 0 0 0 43901 102 0 0 25 0 1 0 539779829 170754048 37787 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41688 37787 603 41 0 41647 0
vsize: 166752
[startup+450.008 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 40060 0 0 0 44901 102 0 0 25 0 1 0 539779829 171016192 37851 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41752 37851 603 41 0 41711 0
vsize: 167008
[startup+460.007 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 40114 0 0 0 45902 102 0 0 25 0 1 0 539779829 171147264 37905 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41784 37905 603 41 0 41743 0
vsize: 167136
[startup+470.007 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 40158 0 0 0 46902 102 0 0 25 0 1 0 539779829 171409408 37949 4294967295 134512640 134672761 3221224544 3221223680 134560566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41848 37949 603 41 0 41807 0
vsize: 167392
[startup+480.008 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 40197 0 0 0 47901 103 0 0 25 0 1 0 539779829 171540480 37988 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41880 37988 603 41 0 41839 0
vsize: 167520
[startup+490.008 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 40218 0 0 0 48900 103 0 0 25 0 1 0 539779829 171675648 38009 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41913 38009 603 41 0 41872 0
vsize: 167652
[startup+500.01 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 40262 0 0 0 49900 103 0 0 25 0 1 0 539779829 171806720 38053 4294967295 134512640 134672761 3221224544 3221223712 134561025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41945 38053 603 41 0 41904 0
vsize: 167780
[startup+510.014 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 40580 0 0 0 50900 104 0 0 25 0 1 0 539779829 173043712 38371 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42247 38371 603 41 0 42206 0
vsize: 168988
[startup+520.013 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 41416 0 0 0 51899 106 0 0 25 0 1 0 539779829 176476160 39207 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43085 39207 603 41 0 43044 0
vsize: 172340
[startup+530.013 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 42401 0 0 0 52897 108 0 0 25 0 1 0 539779829 180584448 40192 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44088 40192 603 41 0 44047 0
vsize: 176352
[startup+540.014 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 43017 0 0 0 53896 109 0 0 25 0 1 0 539779829 183058432 40808 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44692 40808 603 41 0 44651 0
vsize: 178768
[startup+550.015 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 43715 0 0 0 54894 111 0 0 25 0 1 0 539779829 185933824 41506 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45394 41506 603 41 0 45353 0
vsize: 181576
[startup+560.015 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 44302 0 0 0 55893 113 0 0 25 0 1 0 539779829 188645376 42093 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46056 42093 603 41 0 46015 0
vsize: 184224
[startup+570.015 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 44753 0 0 0 56891 114 0 0 25 0 1 0 539779829 190406656 42544 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46486 42544 603 41 0 46445 0
vsize: 185944
[startup+580.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 45126 0 0 0 57891 115 0 0 25 0 1 0 539779829 191967232 42917 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46867 42917 603 41 0 46826 0
vsize: 187468
[startup+590.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 45501 0 0 0 58890 115 0 0 25 0 1 0 539779829 193454080 43292 4294967295 134512640 134672761 3221224544 3221223728 134559489 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47230 43292 603 41 0 47189 0
vsize: 188920
[startup+600.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 46018 0 0 0 59889 117 0 0 25 0 1 0 539779829 195637248 43809 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47763 43809 603 41 0 47722 0
vsize: 191052
[startup+610.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 46488 0 0 0 60887 119 0 0 25 0 1 0 539779829 197505024 44279 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48219 44279 603 41 0 48178 0
vsize: 192876
[startup+620.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 46933 0 0 0 61887 120 0 0 25 0 1 0 539779829 199360512 44724 4294967295 134512640 134672761 3221224544 3221223692 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48672 44724 603 41 0 48631 0
vsize: 194688
[startup+630.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 47439 0 0 0 62885 121 0 0 25 0 1 0 539779829 201519104 45230 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49199 45230 603 41 0 49158 0
vsize: 196796
[startup+640.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 47798 0 0 0 63884 122 0 0 25 0 1 0 539779829 202862592 45589 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49527 45589 603 41 0 49486 0
vsize: 198108
[startup+650.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 48085 0 0 0 64884 124 0 0 25 0 1 0 539779829 204091392 45876 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49827 45876 603 41 0 49786 0
vsize: 199308
[startup+660.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 48336 0 0 0 65883 124 0 0 25 0 1 0 539779829 205176832 46127 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50092 46127 603 41 0 50051 0
vsize: 200368
[startup+670.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 48505 0 0 0 66883 125 0 0 25 0 1 0 539779829 205848576 46296 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50256 46296 603 41 0 50215 0
vsize: 201024
[startup+680.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 48996 0 0 0 67882 126 0 0 25 0 1 0 539779829 207781888 46787 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50728 46787 603 41 0 50687 0
vsize: 202912
[startup+690.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 49373 0 0 0 68881 126 0 0 25 0 1 0 539779829 209387520 47164 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51120 47164 603 41 0 51079 0
vsize: 204480
[startup+700.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 49965 0 0 0 69880 128 0 0 25 0 1 0 539779829 211742720 47756 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51695 47756 603 41 0 51654 0
vsize: 206780
[startup+710.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 50295 0 0 0 70879 129 0 0 25 0 1 0 539779829 213090304 48086 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52024 48086 603 41 0 51983 0
vsize: 208096
[startup+720.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 50460 0 0 0 71878 129 0 0 25 0 1 0 539779829 213766144 48251 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52189 48251 603 41 0 52148 0
vsize: 208756
[startup+730.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 50715 0 0 0 72878 131 0 0 25 0 1 0 539779829 214843392 48506 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52452 48506 603 41 0 52411 0
vsize: 209808
[startup+740.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 50971 0 0 0 73877 132 0 0 25 0 1 0 539779829 215916544 48762 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52714 48762 603 41 0 52673 0
vsize: 210856
[startup+750.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 51162 0 0 0 74877 132 0 0 25 0 1 0 539779829 216723456 48953 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52911 48953 603 41 0 52870 0
vsize: 211644
[startup+760.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 51414 0 0 0 75876 133 0 0 25 0 1 0 539779829 217800704 49205 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53174 49205 603 41 0 53133 0
vsize: 212696
[startup+770.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 51654 0 0 0 76875 134 0 0 25 0 1 0 539779829 218738688 49445 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53403 49445 603 41 0 53362 0
vsize: 213612
[startup+780.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 51902 0 0 0 77876 135 0 0 25 0 1 0 539779829 219799552 49693 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53662 49693 603 41 0 53621 0
vsize: 214648
[startup+790.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 52167 0 0 0 78875 135 0 0 25 0 1 0 539779829 220876800 49958 4294967295 134512640 134672761 3221224544 3221223640 1075347361 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53925 49958 603 41 0 53884 0
vsize: 215700
[startup+800.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 52233 0 0 0 79875 136 0 0 25 0 1 0 539779829 221143040 50024 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53990 50024 603 41 0 53949 0
vsize: 215960
[startup+810.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 52295 0 0 0 80876 136 0 0 25 0 1 0 539779829 221274112 50086 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54022 50086 603 41 0 53981 0
vsize: 216088
[startup+820.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 52347 0 0 0 81876 136 0 0 25 0 1 0 539779829 221540352 50138 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54087 50138 603 41 0 54046 0
vsize: 216348
[startup+830.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 52360 0 0 0 82877 136 0 0 25 0 1 0 539779829 221540352 50151 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54087 50151 603 41 0 54046 0
vsize: 216348
[startup+840.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 52471 0 0 0 83876 137 0 0 25 0 1 0 539779829 222093312 50262 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54222 50262 603 41 0 54181 0
vsize: 216888
[startup+850.151 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 52588 0 0 0 84887 137 0 0 25 0 1 0 539779829 222490624 50379 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54319 50379 603 41 0 54278 0
vsize: 217276
[startup+860.175 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 52675 0 0 0 85889 137 0 0 25 0 1 0 539779829 222892032 50466 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54417 50466 603 41 0 54376 0
vsize: 217668
[startup+870.174 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 52762 0 0 0 86889 137 0 0 25 0 1 0 539779829 223293440 50553 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54515 50553 603 41 0 54474 0
vsize: 218060
[startup+880.206 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 52850 0 0 0 87892 137 0 0 25 0 1 0 539779829 223563776 50641 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54581 50641 603 41 0 54540 0
vsize: 218324
[startup+890.215 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 52942 0 0 0 88892 138 0 0 25 0 1 0 539779829 223961088 50733 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54678 50733 603 41 0 54637 0
vsize: 218712
[startup+900.226 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22877
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 53034 0 0 0 89894 138 0 0 25 0 1 0 539779829 224374784 50825 4294967295 134512640 134672761 3221224544 3221223728 134558648 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54779 50825 603 41 0 54738 0
vsize: 219116
[startup+910.237 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 22930
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 53128 0 0 0 90894 139 0 0 25 0 1 0 539779829 224772096 50919 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54876 50919 603 41 0 54835 0
vsize: 219504
[startup+920.238 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 22930
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 53213 0 0 0 91894 140 0 0 25 0 1 0 539779829 225038336 51004 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54941 51004 603 41 0 54900 0
vsize: 219764
[startup+930.253 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 22930
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 53322 0 0 0 92895 140 0 0 25 0 1 0 539779829 225579008 51113 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55073 51113 603 41 0 55032 0
vsize: 220292
[startup+940.253 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 22930
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 53421 0 0 0 93895 140 0 0 25 0 1 0 539779829 225976320 51212 4294967295 134512640 134672761 3221224544 3221223712 134561139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55170 51212 603 41 0 55129 0
vsize: 220680
[startup+950.254 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 22930
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 53493 0 0 0 94895 141 0 0 25 0 1 0 539779829 226246656 51284 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55236 51284 603 41 0 55195 0
vsize: 220944
[startup+960.254 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 22930
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 53548 0 0 0 95895 141 0 0 25 0 1 0 539779829 226516992 51339 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55302 51339 603 41 0 55261 0
vsize: 221208
[startup+970.254 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 22930
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 53607 0 0 0 96894 141 0 0 25 0 1 0 539779829 226787328 51398 4294967295 134512640 134672761 3221224544 3221223712 134561256 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55368 51398 603 41 0 55327 0
vsize: 221472
[startup+980.254 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 22932
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 53665 0 0 0 97894 141 0 0 25 0 1 0 539779829 227053568 51456 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55433 51456 603 41 0 55392 0
vsize: 221732
[startup+990.255 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 22932
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 53706 0 0 0 98894 142 0 0 25 0 1 0 539779829 227188736 51497 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55466 51497 603 41 0 55425 0
vsize: 221864
[startup+1000.26 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 22932
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 53779 0 0 0 99895 142 0 0 25 0 1 0 539779829 227459072 51570 4294967295 134512640 134672761 3221224544 3221223680 134560697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55532 51570 603 41 0 55491 0
vsize: 222128
[startup+1010.26 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 22932
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 53910 0 0 0 100894 143 0 0 25 0 1 0 539779829 227999744 51701 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55664 51701 603 41 0 55623 0
vsize: 222656
[startup+1020.26 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 22932
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 54021 0 0 0 101894 143 0 0 25 0 1 0 539779829 228528128 51812 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55793 51812 603 41 0 55752 0
vsize: 223172
[startup+1030.26 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 22932
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 54126 0 0 0 102894 143 0 0 25 0 1 0 539779829 228929536 51917 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55891 51917 603 41 0 55850 0
vsize: 223564
[startup+1040.26 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 22932
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 54273 0 0 0 103894 143 0 0 25 0 1 0 539779829 229457920 52064 4294967295 134512640 134672761 3221224544 3221223680 134560596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56020 52064 603 41 0 55979 0
vsize: 224080
[startup+1050.26 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22932
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 54462 0 0 0 104894 144 0 0 25 0 1 0 539779829 230268928 52253 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56218 52253 603 41 0 56177 0
vsize: 224872
[startup+1060.26 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22932
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 54625 0 0 0 105893 145 0 0 25 0 1 0 539779829 230944768 52416 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56383 52416 603 41 0 56342 0
vsize: 225532
[startup+1070.26 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22932
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 54723 0 0 0 106892 145 0 0 25 0 1 0 539779829 231870464 52514 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56609 52514 603 41 0 56568 0
vsize: 226436
[startup+1080.26 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22932
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 54841 0 0 0 107892 146 0 0 25 0 1 0 539779829 232271872 52632 4294967295 134512640 134672761 3221224544 3221223648 134555175 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56707 52632 603 41 0 56666 0
vsize: 226828
[startup+1090.26 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22932
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 54949 0 0 0 108892 146 0 0 25 0 1 0 539779829 232812544 52740 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56839 52740 603 41 0 56798 0
vsize: 227356
[startup+1100.26 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22932
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 55060 0 0 0 109891 146 0 0 25 0 1 0 539779829 233218048 52851 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56938 52851 603 41 0 56897 0
vsize: 227752
[startup+1110.26 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22932
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 55174 0 0 0 110891 147 0 0 25 0 1 0 539779829 233615360 52965 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57035 52965 603 41 0 56994 0
vsize: 228140
[startup+1120.26 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22932
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 55322 0 0 0 111891 147 0 0 25 0 1 0 539779829 234291200 53113 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57200 53113 603 41 0 57159 0
vsize: 228800
[startup+1130.26 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22932
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 55471 0 0 0 112891 148 0 0 25 0 1 0 539779829 234823680 53262 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57330 53262 603 41 0 57289 0
vsize: 229320
[startup+1140.26 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22932
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 55650 0 0 0 113890 148 0 0 25 0 1 0 539779829 235630592 53441 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57527 53441 603 41 0 57486 0
vsize: 230108
[startup+1150.26 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22932
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 55804 0 0 0 114890 149 0 0 25 0 1 0 539779829 236179456 53595 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57661 53595 603 41 0 57620 0
vsize: 230644
[startup+1160.26 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22932
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 55920 0 0 0 115890 149 0 0 25 0 1 0 539779829 236720128 53711 4294967295 134512640 134672761 3221224544 3221223680 134560596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57793 53711 603 41 0 57752 0
vsize: 231172
[startup+1170.26 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22932
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 56061 0 0 0 116890 150 0 0 25 0 1 0 539779829 237256704 53852 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57924 53852 603 41 0 57883 0
vsize: 231696
[startup+1180.26 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22932
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 56205 0 0 0 117889 150 0 0 25 0 1 0 539779829 237932544 53996 4294967295 134512640 134672761 3221224544 3221223712 134560970 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58089 53996 603 41 0 58048 0
vsize: 232356
[startup+1190.26 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22932
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 56301 0 0 0 118890 150 0 0 25 0 1 0 539779829 238325760 54092 4294967295 134512640 134672761 3221224544 3221223680 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58185 54092 603 41 0 58144 0
vsize: 232740
[startup+1200.27 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 22932
Raw data (stat): 22877 (minisat+) R 22876 3260 3259 0 -1 0 56431 0 0 0 119890 151 0 0 25 0 1 0 539779829 238854144 54222 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58314 54222 603 41 0 58273 0
vsize: 233256
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.37 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 22932
Raw data (stat): 22877 (minisat+) Z 22876 3260 3259 0 -1 12 56433 0 0 0 119890 161 0 0 25 0 1 0 539779829 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.37
CPU time (s): 1200.52
CPU user time (s): 1198.9
CPU system time (s): 1.61775
CPU usage (%): 100.012
Max. virtual memory (Kb): 233256
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####