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-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-vpm2.opb
MD5SUMfae1fae180d772ad3ee6c1acfa1c8b4f
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 122
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 2000000
Number of bits of the biggest number in a constraint 21
Biggest sum of numbers in a constraint 30041153
Number of bits of the biggest sum of numbers25
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1189.01
Number of variables2124
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 constraint8
Maximum length of a constraint64

Trace number 14945 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc11 THE 2005-04-21 02:12:03 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18953 boxname=wulflinc11 idbench=1458 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  fae1fae180d772ad3ee6c1acfa1c8b4f  /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-13-7-vpm2.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-13-7-vpm2.opb /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-13-7-vpm2.opb
IDLAUNCH: 18953
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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.028
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:        881184 kB
Buffers:         19464 kB
Cached:         113340 kB
SwapCached:          0 kB
Active:          63968 kB
Inactive:        71668 kB
HighTotal:      131008 kB
HighFree:        17108 kB
LowTotal:       903652 kB
LowFree:        864076 kB
SwapTotal:     2097136 kB
SwapFree:      2097048 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6816 kB
Slab:            12308 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 02:32:06 (client local time) WITH STATUS 0 IN 1200.25 SECONDS
stats: 18953 7 1200.25 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:    7
c ---[ 484]---> BDD-cost:    7
c ---[ 483]---> BDD-cost:    7
c ---[ 482]---> BDD-cost:    7
c ---[ 481]---> BDD-cost:    7
c ---[ 480]---> BDD-cost:    7
c ---[ 479]---> BDD-cost:    7
c ---[ 478]---> BDD-cost:    7
c ---[ 477]---> BDD-cost:    7
c ---[ 474]---> BDD-cost:    7
c ---[ 473]---> BDD-cost:    7
c ---[ 472]---> BDD-cost:    7
c ---[ 471]---> BDD-cost:    7
c ---[ 468]---> BDD-cost:    7
c ---[ 467]---> BDD-cost:    7
c ---[ 466]---> BDD-cost:    7
c ---[ 465]---> BDD-cost:    7
c ---[ 462]---> BDD-cost:    7
c ---[ 459]---> BDD-cost:    7
c ---[ 458]---> BDD-cost:    7
c ---[ 457]---> BDD-cost:    7
c ---[ 454]---> BDD-cost:    7
c ---[ 453]---> BDD-cost:    7
c ---[ 452]---> BDD-cost:    7
c ---[ 451]---> BDD-cost:    7
c ---[ 450]---> BDD-cost:    7
c ---[ 448]---> BDD-cost:    7
c ---[ 447]---> BDD-cost:    7
c ---[ 446]---> BDD-cost:    7
c ---[ 445]---> BDD-cost:    7
c ---[ 444]---> BDD-cost:    7
c ---[ 441]---> BDD-cost:    7
c ---[ 440]---> BDD-cost:    7
c ---[ 439]---> BDD-cost:    7
c ---[ 433]---> BDD-cost:    7
c ---[ 427]---> BDD-cost:    7
c ---[ 422]---> BDD-cost:    7
c ---[ 421]---> BDD-cost:    7
c ---[ 415]---> BDD-cost:    7
c ---[ 409]---> BDD-cost:    7
c ---[ 408]---> BDD-cost:    7
c ---[ 402]---> BDD-cost:    7
c ---[ 397]---> BDD-cost:    7
c ---[ 396]---> BDD-cost:    7
c ---[ 391]---> BDD-cost:    7
c ---[ 390]---> BDD-cost:    7
c ---[ 386]---> BDD-cost:    7
c ---[ 385]---> BDD-cost:    7
c ---[ 384]---> BDD-cost:    7
c ---[ 380]---> BDD-cost:    7
c ---[ 379]---> BDD-cost:    7
c ---[ 378]---> BDD-cost:    7
c ---[ 374]---> BDD-cost:    7
c ---[ 373]---> BDD-cost:    7
c ---[ 372]---> BDD-cost:    7
c ---[ 368]---> BDD-cost:    7
c ---[ 367]---> BDD-cost:    7
c ---[ 366]---> BDD-cost:    7
c ---[ 365]---> BDD-cost:    7
c ---[ 364]---> BDD-cost:    7
c ---[ 359]---> BDD-cost:    7
c ---[ 353]---> BDD-cost:    7
c ---[ 347]---> BDD-cost:    7
c ---[ 339]---> BDD-cost:    7
c ---[ 333]---> BDD-cost:    7
c ---[ 327]---> BDD-cost:    7
c ---[ 321]---> BDD-cost:    7
c ---[ 317]---> BDD-cost:   14
c ---[ 316]---> BDD-cost:   14
c ---[ 315]---> BDD-cost:   14
c ---[ 314]---> BDD-cost:   14
c ---[ 313]---> BDD-cost:   14
c ---[ 312]---> BDD-cost:   14
c ---[ 310]---> BDD-cost:   14
c ---[ 309]---> BDD-cost:   14
c ---[ 308]---> BDD-cost:   14
c ---[ 307]---> BDD-cost:   14
c ---[ 306]---> BDD-cost:   14
c ---[ 302]---> BDD-cost:   13
c ---[ 301]---> BDD-cost:   13
c ---[ 300]---> BDD-cost:   13
c ---[ 295]---> BDD-cost:   13
c ---[ 294]---> BDD-cost:   13
c ---[ 290]---> BDD-cost:   15
c ---[ 289]---> BDD-cost:   15
c ---[ 288]---> BDD-cost:   15
c ---[ 287]---> BDD-cost:   13
c ---[ 286]---> BDD-cost:   13
c ---[ 285]---> BDD-cost:   13
c ---[ 284]---> BDD-cost:   13
c ---[ 283]---> BDD-cost:   13
c ---[ 282]---> BDD-cost:   13
c ---[ 280]---> BDD-cost:   13
c ---[ 279]---> BDD-cost:   13
c ---[ 278]---> BDD-cost:   13
c ---[ 277]---> BDD-cost:   13
c ---[ 276]---> BDD-cost:   13
c ---[ 274]---> BDD-cost: 5216
c ---[ 264]---> BDD-cost: 3154
c ---[ 260]---> BDD-cost:10530
c ---[ 258]---> BDD-cost:10530
c ---[ 256]---> BDD-cost: 7522
c ---[ 254]---> BDD-cost: 7522
c ---[ 252]---> BDD-cost:10993
c ---[ 250]---> BDD-cost: 2194
c ---[ 248]---> BDD-cost: 4013
c ---[ 246]---> BDD-cost: 4263
c ---[ 244]---> BDD-cost: 4263
c ---[ 242]---> BDD-cost: 3166
c ---[ 236]---> BDD-cost: 2842
c ---[ 234]---> BDD-cost: 7167
c ---[ 232]---> BDD-cost: 4105
c ---[ 224]---> BDD-cost: 3441
c ---[ 222]---> BDD-cost: 8215
c ---[ 216]---> BDD-cost: 3369
c ---[ 214]---> BDD-cost: 4733
c ---[ 212]---> BDD-cost: 4964
c ---[ 210]---> BDD-cost: 7397
c ---[ 208]---> BDD-cost: 3944
c ---[ 206]---> BDD-cost: 3944
c ---[ 204]---> BDD-cost: 3944
c ---[ 202]---> BDD-cost: 3944
c ---[ 200]---> BDD-cost: 3997
c ---[ 198]---> BDD-cost: 9563
c ---[ 196]---> BDD-cost: 4987
c ---[ 194]---> BDD-cost: 4987
c ---[ 192]---> BDD-cost: 4987
c ---[ 191]---> BDD-cost:  110
c ---[ 190]---> BDD-cost:  237
c ---[ 189]---> BDD-cost:  236
c ---[ 188]---> BDD-cost:  393
c ---[ 187]---> BDD-cost:  495
c ---[ 186]---> BDD-cost:  488
c ---[ 185]---> BDD-cost:  131
c ---[ 184]---> BDD-cost:  262
c ---[ 183]---> BDD-cost:  261
c ---[ 182]---> BDD-cost:  448
c ---[ 181]---> BDD-cost:  550
c ---[ 180]---> BDD-cost:  549
c ---[ 179]---> BDD-cost:  200
c ---[ 178]---> BDD-cost:  446
c ---[ 177]---> BDD-cost:  440
c ---[ 176]---> BDD-cost:  784
c ---[ 175]---> BDD-cost:  985
c ---[ 174]---> BDD-cost:  982
c ---[ 173]---> BDD-cost:   87
c ---[ 172]---> BDD-cost:  178
c ---[ 171]---> BDD-cost:  174
c ---[ 170]---> BDD-cost:  291
c ---[ 169]---> BDD-cost:  374
c ---[ 168]---> BDD-cost:  369
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:    7
c ---[ 157]---> BDD-cost:    7
c ---[ 156]---> BDD-cost:    3
c ---[ 155]---> BDD-cost:    3
c ---[ 154]---> BDD-cost:    3
c ---[ 153]---> BDD-cost:    3
c ---[ 152]---> BDD-cost:    7
c ---[ 151]---> BDD-cost:    7
c ---[ 150]---> BDD-cost:    3
c ---[ 149]---> BDD-cost:    3
c ---[ 148]---> BDD-cost:    3
c ---[ 147]---> BDD-cost:    3
c ---[ 146]---> BDD-cost:    7
c ---[ 145]---> BDD-cost:    7
c ---[ 144]---> BDD-cost:    3
c ---[ 142]---> BDD-cost:    7
c ---[ 141]---> BDD-cost:    3
c ---[ 140]---> BDD-cost:    3
c ---[ 139]---> BDD-cost:    3
c ---[ 138]---> BDD-cost:    7
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:    7
c ---[ 123]---> BDD-cost:    3
c ---[ 122]---> BDD-cost:    3
c ---[ 121]---> BDD-cost:    3
c ---[ 120]---> BDD-cost:    7
c ---[ 116]---> BDD-cost:    7
c ---[ 115]---> BDD-cost:    3
c ---[ 114]---> BDD-cost:    6
c ---[ 110]---> BDD-cost:    7
c ---[ 109]---> BDD-cost:    3
c ---[ 108]---> BDD-cost:    6
c ---[ 104]---> BDD-cost:    3
c ---[ 103]---> BDD-cost:    3
c ---[ 102]---> BDD-cost:    6
c ---[  98]---> BDD-cost:    7
c ---[  97]---> BDD-cost:    3
c ---[  96]---> BDD-cost:    6
c ---[  91]---> BDD-cost:    3
c ---[  90]---> BDD-cost:    3
c ---[  85]---> BDD-cost:    7
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:    6
c ---[  44]---> BDD-cost:    6
c ---[  43]---> BDD-cost:    6
c ---[  42]---> BDD-cost:    6
c ---[  41]---> BDD-cost:    3
c ---[  40]---> BDD-cost:    7
c ---[  39]---> BDD-cost:    6
c ---[  38]---> BDD-cost:    6
c ---[  37]---> BDD-cost:    6
c ---[  36]---> BDD-cost:    6
c ---[  35]---> BDD-cost:    3
c ---[  34]---> BDD-cost:    7
c ---[  33]---> BDD-cost:    5
c ---[  32]---> BDD-cost:    5
c ---[  31]---> BDD-cost:    5
c ---[  30]---> BDD-cost:    5
c ---[  29]---> BDD-cost:    3
c ---[  28]---> BDD-cost:    7
c ---[  27]---> BDD-cost:    5
c ---[  26]---> BDD-cost:    5
c ---[  25]---> BDD-cost:    5
c ---[  24]---> BDD-cost:    5
c ---[  22]---> BDD-cost:    7
c ---[  21]---> BDD-cost:    3
c ---[  20]---> BDD-cost:    6
c ---[  19]---> BDD-cost:    6
c ---[  18]---> BDD-cost:    6
c ---[  16]---> BDD-cost:    7
c ---[  15]---> BDD-cost:    3
c ---[  14]---> BDD-cost:    6
c ---[  13]---> BDD-cost:    6
c ---[  12]---> BDD-cost:    6
c ---[  10]---> BDD-cost:    7
c ---[   9]---> BDD-cost:    3
c ---[   8]---> BDD-cost:    6
c ---[   7]---> BDD-cost:    6
c ---[   6]---> BDD-cost:    6
c ---[   4]---> BDD-cost:    7
c ---[   3]---> BDD-cost:    3
c ---[   2]---> BDD-cost:    5
c ---[   1]---> BDD-cost:    5
c ---[   0]---> BDD-cost:    5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  454043  1255430 |  151347       0        0     nan |  0.000 % |
c |       100 |  453973  1255238 |  166481      93     1660    17.8 |  0.565 % |
c |       250 |  453950  1255172 |  183129     241     4695    19.5 |  0.569 % |
c |       475 |  453902  1255034 |  201442     461     8683    18.8 |  0.578 % |
c |       812 |  453747  1254604 |  221587     784    14296    18.2 |  0.600 % |
c |      1320 |  453734  1254566 |  243745    1290    40773    31.6 |  0.603 % |
c |      2079 |  453659  1254362 |  268120    2042    72297    35.4 |  0.612 % |
c |      3219 |  453617  1254241 |  294932    3179   110292    34.7 |  0.617 % |
c |      4927 |  453566  1254108 |  324425    4884   158566    32.5 |  0.623 % |
c |      7491 |  453409  1253709 |  356868    7433   225238    30.3 |  0.655 % |
c |     11338 |  453377  1253617 |  392555   11275   450448    40.0 |  0.662 % |
c |     17105 |  453353  1253549 |  431810   17039   767695    45.1 |  0.666 % |
c |     25754 |  453306  1253428 |  474991   25686  1096740    42.7 |  0.669 % |
c |     38728 |  453295  1253396 |  522490   38659  1522744    39.4 |  0.671 % |
c |     58189 |  453255  1253283 |  574739   58114  2334938    40.2 |  0.679 % |
c |     87381 |  453249  1253265 |  632213   87304  3998074    45.8 |  0.681 % |
c |    131170 |  453236  1253227 |  695435  131092  5961914    45.5 |  0.684 % |
c |    196855 |  453186  1253082 |  764978  196772 10804657    54.9 |  0.694 % |
#### 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.77 0.92 0.97 2/54 26218
Raw data (stat): 26218 (runsolver) R 26217 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 483158402 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99976 s]
Raw data (loadavg): 0.81 0.92 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 14997 0 0 0 963 35 0 0 25 0 1 0 483158402 67891200 14195 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16575 14195 603 41 0 16534 0
vsize: 66300
[startup+19.9996 s]
Raw data (loadavg): 0.84 0.93 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 15185 0 0 0 1963 36 0 0 25 0 1 0 483158402 68718592 14383 4294967295 134512640 134672761 3221224544 3221223616 1074719016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16777 14383 603 41 0 16736 0
vsize: 67108
[startup+30.0009 s]
Raw data (loadavg): 0.86 0.93 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 15315 0 0 0 2962 37 0 0 25 0 1 0 483158402 69246976 14513 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16906 14513 603 41 0 16865 0
vsize: 67624
[startup+40.0012 s]
Raw data (loadavg): 0.88 0.93 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 15428 0 0 0 3961 38 0 0 25 0 1 0 483158402 69672960 14626 4294967295 134512640 134672761 3221224544 3221223744 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17010 14626 603 41 0 16969 0
vsize: 68040
[startup+50.0019 s]
Raw data (loadavg): 0.90 0.93 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 15592 0 0 0 4960 39 0 0 25 0 1 0 483158402 70459392 14790 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17202 14790 603 41 0 17161 0
vsize: 68808
[startup+60.0022 s]
Raw data (loadavg): 0.91 0.93 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 15765 0 0 0 5959 40 0 0 25 0 1 0 483158402 71131136 14963 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17366 14963 603 41 0 17325 0
vsize: 69464
[startup+70.0026 s]
Raw data (loadavg): 0.93 0.94 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 15914 0 0 0 6958 41 0 0 25 0 1 0 483158402 71667712 15112 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17497 15112 603 41 0 17456 0
vsize: 69988
[startup+80.0038 s]
Raw data (loadavg): 0.94 0.94 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 16097 0 0 0 7957 42 0 0 25 0 1 0 483158402 72511488 15295 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17703 15295 603 41 0 17662 0
vsize: 70812
[startup+90.0046 s]
Raw data (loadavg): 0.95 0.94 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 16341 0 0 0 8957 42 0 0 25 0 1 0 483158402 73445376 15539 4294967295 134512640 134672761 3221224544 3221223712 134560811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17931 15539 603 41 0 17890 0
vsize: 71724
[startup+100.005 s]
Raw data (loadavg): 0.95 0.94 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 16513 0 0 0 9956 43 0 0 25 0 1 0 483158402 74113024 15711 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18094 15711 603 41 0 18053 0
vsize: 72376
[startup+110.006 s]
Raw data (loadavg): 0.96 0.94 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 16657 0 0 0 10956 44 0 0 25 0 1 0 483158402 74772480 15855 4294967295 134512640 134672761 3221224544 3221223728 134558918 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18255 15855 603 41 0 18214 0
vsize: 73020
[startup+120.006 s]
Raw data (loadavg): 0.97 0.94 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 16768 0 0 0 11956 44 0 0 25 0 1 0 483158402 75300864 15966 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18384 15966 603 41 0 18343 0
vsize: 73536
[startup+130.006 s]
Raw data (loadavg): 0.97 0.94 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 16854 0 0 0 12955 45 0 0 25 0 1 0 483158402 75694080 16052 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18480 16052 603 41 0 18439 0
vsize: 73920
[startup+140.007 s]
Raw data (loadavg): 0.98 0.95 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 16930 0 0 0 13955 45 0 0 25 0 1 0 483158402 75964416 16128 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18546 16128 603 41 0 18505 0
vsize: 74184
[startup+150.008 s]
Raw data (loadavg): 0.98 0.95 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 17079 0 0 0 14955 46 0 0 25 0 1 0 483158402 76640256 16277 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18711 16277 603 41 0 18670 0
vsize: 74844
[startup+160.009 s]
Raw data (loadavg): 0.98 0.95 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 17359 0 0 0 15954 46 0 0 25 0 1 0 483158402 77737984 16557 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18979 16557 603 41 0 18938 0
vsize: 75916
[startup+170.008 s]
Raw data (loadavg): 0.98 0.95 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 17643 0 0 0 16953 48 0 0 25 0 1 0 483158402 78823424 16841 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19244 16841 603 41 0 19203 0
vsize: 76976
[startup+180.009 s]
Raw data (loadavg): 0.99 0.95 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 17800 0 0 0 17952 49 0 0 25 0 1 0 483158402 79503360 16998 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19410 16998 603 41 0 19369 0
vsize: 77640
[startup+190.009 s]
Raw data (loadavg): 0.99 0.95 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 18019 0 0 0 18952 49 0 0 25 0 1 0 483158402 80437248 17217 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19638 17217 603 41 0 19597 0
vsize: 78552
[startup+200.01 s]
Raw data (loadavg): 0.99 0.95 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 18143 0 0 0 19951 50 0 0 25 0 1 0 483158402 80969728 17341 4294967295 134512640 134672761 3221224544 3221223728 134558360 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19768 17341 603 41 0 19727 0
vsize: 79072
[startup+210.011 s]
Raw data (loadavg): 0.99 0.95 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 18321 0 0 0 20951 51 0 0 25 0 1 0 483158402 81633280 17519 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19930 17519 603 41 0 19889 0
vsize: 79720
[startup+220.011 s]
Raw data (loadavg): 0.99 0.95 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 18547 0 0 0 21949 53 0 0 25 0 1 0 483158402 82833408 17745 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20223 17745 603 41 0 20182 0
vsize: 80892
[startup+230.011 s]
Raw data (loadavg): 0.99 0.95 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 18785 0 0 0 22948 54 0 0 25 0 1 0 483158402 83763200 17983 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20450 17983 603 41 0 20409 0
vsize: 81800
[startup+240.011 s]
Raw data (loadavg): 0.99 0.96 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 19015 0 0 0 23946 56 0 0 25 0 1 0 483158402 84701184 18213 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20679 18213 603 41 0 20638 0
vsize: 82716
[startup+250.012 s]
Raw data (loadavg): 0.99 0.96 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 19246 0 0 0 24946 57 0 0 25 0 1 0 483158402 85659648 18444 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20913 18444 603 41 0 20872 0
vsize: 83652
[startup+260.013 s]
Raw data (loadavg): 0.99 0.96 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 19468 0 0 0 25944 58 0 0 25 0 1 0 483158402 86556672 18666 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21132 18666 603 41 0 21091 0
vsize: 84528
[startup+270.012 s]
Raw data (loadavg): 0.99 0.96 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 19687 0 0 0 26944 59 0 0 25 0 1 0 483158402 87482368 18885 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21358 18885 603 41 0 21317 0
vsize: 85432
[startup+280.012 s]
Raw data (loadavg): 0.99 0.96 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 19880 0 0 0 27943 59 0 0 25 0 1 0 483158402 88281088 19078 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21553 19078 603 41 0 21512 0
vsize: 86212
[startup+290.012 s]
Raw data (loadavg): 0.99 0.96 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 20049 0 0 0 28943 60 0 0 25 0 1 0 483158402 88969216 19247 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21721 19247 603 41 0 21680 0
vsize: 86884
[startup+300.013 s]
Raw data (loadavg): 0.99 0.96 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 20232 0 0 0 29942 61 0 0 25 0 1 0 483158402 89702400 19430 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21900 19430 603 41 0 21859 0
vsize: 87600
[startup+310.013 s]
Raw data (loadavg): 0.99 0.96 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 20401 0 0 0 30942 61 0 0 25 0 1 0 483158402 90361856 19599 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22061 19599 603 41 0 22020 0
vsize: 88244
[startup+320.014 s]
Raw data (loadavg): 0.99 0.96 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 20588 0 0 0 31941 62 0 0 25 0 1 0 483158402 91160576 19786 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22256 19786 603 41 0 22215 0
vsize: 89024
[startup+330.014 s]
Raw data (loadavg): 0.99 0.96 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 20757 0 0 0 32940 64 0 0 25 0 1 0 483158402 91840512 19955 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22422 19955 603 41 0 22381 0
vsize: 89688
[startup+340.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 20922 0 0 0 33939 64 0 0 25 0 1 0 483158402 92549120 20120 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22595 20120 603 41 0 22554 0
vsize: 90380
[startup+350.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 21086 0 0 0 34938 65 0 0 25 0 1 0 483158402 93310976 20284 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22781 20284 603 41 0 22740 0
vsize: 91124
[startup+360.021 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 21251 0 0 0 35938 66 0 0 25 0 1 0 483158402 93995008 20449 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22948 20449 603 41 0 22907 0
vsize: 91792
[startup+370.021 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 21401 0 0 0 36938 66 0 0 25 0 1 0 483158402 94519296 20599 4294967295 134512640 134672761 3221224544 3221223708 134561028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23076 20599 603 41 0 23035 0
vsize: 92304
[startup+380.021 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 21563 0 0 0 37938 67 0 0 25 0 1 0 483158402 95186944 20761 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23239 20761 603 41 0 23198 0
vsize: 92956
[startup+390.021 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 21688 0 0 0 38937 68 0 0 25 0 1 0 483158402 95727616 20886 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23371 20886 603 41 0 23330 0
vsize: 93484
[startup+400.021 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 21774 0 0 0 39937 68 0 0 25 0 1 0 483158402 96124928 20972 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23468 20972 603 41 0 23427 0
vsize: 93872
[startup+410.021 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 21905 0 0 0 40936 69 0 0 25 0 1 0 483158402 96657408 21103 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23598 21103 603 41 0 23557 0
vsize: 94392
[startup+420.021 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 22003 0 0 0 41935 70 0 0 25 0 1 0 483158402 97083392 21201 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23702 21201 603 41 0 23661 0
vsize: 94808
[startup+430.022 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 22116 0 0 0 42935 70 0 0 25 0 1 0 483158402 97513472 21314 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23807 21314 603 41 0 23766 0
vsize: 95228
[startup+440.022 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 22222 0 0 0 43935 70 0 0 25 0 1 0 483158402 97927168 21420 4294967295 134512640 134672761 3221224544 3221223680 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23908 21420 603 41 0 23867 0
vsize: 95632
[startup+450.023 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 22339 0 0 0 44934 71 0 0 25 0 1 0 483158402 98455552 21537 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24037 21537 603 41 0 23996 0
vsize: 96148
[startup+460.023 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 22424 0 0 0 45934 71 0 0 25 0 1 0 483158402 99241984 21622 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24229 21622 603 41 0 24188 0
vsize: 96916
[startup+470.023 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 22506 0 0 0 46933 72 0 0 25 0 1 0 483158402 99639296 21704 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24326 21704 603 41 0 24285 0
vsize: 97304
[startup+480.023 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 22642 0 0 0 47933 73 0 0 25 0 1 0 483158402 100184064 21840 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24459 21840 603 41 0 24418 0
vsize: 97836
[startup+490.022 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 22753 0 0 0 48932 73 0 0 25 0 1 0 483158402 100601856 21951 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24561 21951 603 41 0 24520 0
vsize: 98244
[startup+500.024 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 22871 0 0 0 49932 74 0 0 25 0 1 0 483158402 101130240 22069 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24690 22069 603 41 0 24649 0
vsize: 98760
[startup+510.024 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 22996 0 0 0 50931 75 0 0 25 0 1 0 483158402 101658624 22194 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24819 22194 603 41 0 24778 0
vsize: 99276
[startup+520.024 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 23111 0 0 0 51931 75 0 0 25 0 1 0 483158402 102060032 22309 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24917 22309 603 41 0 24876 0
vsize: 99668
[startup+530.023 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 23235 0 0 0 52930 76 0 0 25 0 1 0 483158402 102604800 22433 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25050 22433 603 41 0 25009 0
vsize: 100200
[startup+540.025 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 23371 0 0 0 53930 76 0 0 25 0 1 0 483158402 103157760 22569 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25185 22569 603 41 0 25144 0
vsize: 100740
[startup+550.025 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 23480 0 0 0 54930 77 0 0 25 0 1 0 483158402 103555072 22678 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25282 22678 603 41 0 25241 0
vsize: 101128
[startup+560.025 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 23570 0 0 0 55929 77 0 0 25 0 1 0 483158402 103956480 22768 4294967295 134512640 134672761 3221224544 3221223688 134560555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25380 22768 603 41 0 25339 0
vsize: 101520
[startup+570.026 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 23696 0 0 0 56929 78 0 0 25 0 1 0 483158402 104493056 22894 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25511 22894 603 41 0 25470 0
vsize: 102044
[startup+580.025 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 23836 0 0 0 57929 78 0 0 25 0 1 0 483158402 105025536 23034 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25641 23034 603 41 0 25600 0
vsize: 102564
[startup+590.026 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 24126 0 0 0 58927 80 0 0 25 0 1 0 483158402 106237952 23324 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25937 23324 603 41 0 25896 0
vsize: 103748
[startup+600.026 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 24315 0 0 0 59927 80 0 0 25 0 1 0 483158402 106921984 23513 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26104 23513 603 41 0 26063 0
vsize: 104416
[startup+610.027 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 24477 0 0 0 60927 81 0 0 25 0 1 0 483158402 107458560 23675 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26235 23675 603 41 0 26194 0
vsize: 104940
[startup+620.027 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 24639 0 0 0 61926 81 0 0 25 0 1 0 483158402 108052480 23837 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26380 23837 603 41 0 26339 0
vsize: 105520
[startup+630.027 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 24794 0 0 0 62926 82 0 0 25 0 1 0 483158402 108720128 23992 4294967295 134512640 134672761 3221224544 3221223680 134560683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26543 23992 603 41 0 26502 0
vsize: 106172
[startup+640.028 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 24954 0 0 0 63926 82 0 0 25 0 1 0 483158402 109387776 24152 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26706 24152 603 41 0 26665 0
vsize: 106824
[startup+650.029 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 25140 0 0 0 64925 83 0 0 25 0 1 0 483158402 110194688 24338 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26903 24338 603 41 0 26862 0
vsize: 107612
[startup+660.029 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 25325 0 0 0 65925 84 0 0 25 0 1 0 483158402 110862336 24523 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27066 24523 603 41 0 27025 0
vsize: 108264
[startup+670.029 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 25516 0 0 0 66924 85 0 0 25 0 1 0 483158402 111665152 24714 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27262 24714 603 41 0 27221 0
vsize: 109048
[startup+680.031 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 25692 0 0 0 67924 85 0 0 25 0 1 0 483158402 112476160 24890 4294967295 134512640 134672761 3221224544 3221223500 1075350469 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27460 24890 603 41 0 27419 0
vsize: 109840
[startup+690.031 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 25882 0 0 0 68922 87 0 0 25 0 1 0 483158402 113303552 25080 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27662 25080 603 41 0 27621 0
vsize: 110648
[startup+700.031 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 26088 0 0 0 69922 87 0 0 25 0 1 0 483158402 114122752 25286 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27862 25286 603 41 0 27821 0
vsize: 111448
[startup+710.033 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 26282 0 0 0 70922 88 0 0 25 0 1 0 483158402 114925568 25480 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28058 25480 603 41 0 28017 0
vsize: 112232
[startup+720.032 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 26467 0 0 0 71921 88 0 0 25 0 1 0 483158402 115597312 25665 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28222 25665 603 41 0 28181 0
vsize: 112888
[startup+730.032 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 26654 0 0 0 72921 89 0 0 25 0 1 0 483158402 116404224 25852 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28419 25852 603 41 0 28378 0
vsize: 113676
[startup+740.033 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 26839 0 0 0 73920 90 0 0 25 0 1 0 483158402 117231616 26037 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28621 26037 603 41 0 28580 0
vsize: 114484
[startup+750.033 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 27002 0 0 0 74919 91 0 0 25 0 1 0 483158402 117903360 26200 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28785 26200 603 41 0 28744 0
vsize: 115140
[startup+760.033 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 27169 0 0 0 75919 91 0 0 25 0 1 0 483158402 118579200 26367 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28950 26367 603 41 0 28909 0
vsize: 115800
[startup+770.033 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 27332 0 0 0 76918 92 0 0 25 0 1 0 483158402 119115776 26530 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29081 26530 603 41 0 29040 0
vsize: 116324
[startup+780.033 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 27470 0 0 0 77918 93 0 0 25 0 1 0 483158402 119701504 26668 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29224 26668 603 41 0 29183 0
vsize: 116896
[startup+790.033 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 27615 0 0 0 78917 93 0 0 25 0 1 0 483158402 120393728 26813 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29393 26813 603 41 0 29352 0
vsize: 117572
[startup+800.034 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 27776 0 0 0 79917 94 0 0 25 0 1 0 483158402 121131008 26974 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29573 26974 603 41 0 29532 0
vsize: 118292
[startup+810.035 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 27929 0 0 0 80916 95 0 0 25 0 1 0 483158402 121667584 27127 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29704 27127 603 41 0 29663 0
vsize: 118816
[startup+820.034 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 28055 0 0 0 81916 95 0 0 25 0 1 0 483158402 122204160 27253 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29835 27253 603 41 0 29794 0
vsize: 119340
[startup+830.034 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 28130 0 0 0 82915 95 0 0 25 0 1 0 483158402 122474496 27328 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29901 27328 603 41 0 29860 0
vsize: 119604
[startup+840.035 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 28240 0 0 0 83915 96 0 0 25 0 1 0 483158402 122875904 27438 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29999 27438 603 41 0 29958 0
vsize: 119996
[startup+850.035 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 28299 0 0 0 84915 96 0 0 25 0 1 0 483158402 123133952 27497 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30062 27497 603 41 0 30021 0
vsize: 120248
[startup+860.036 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 28420 0 0 0 85915 96 0 0 25 0 1 0 483158402 123666432 27618 4294967295 134512640 134672761 3221224544 3221223700 134561032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30192 27618 603 41 0 30151 0
vsize: 120768
[startup+870.035 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 28591 0 0 0 86914 97 0 0 25 0 1 0 483158402 124334080 27789 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30355 27789 603 41 0 30314 0
vsize: 121420
[startup+880.036 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 28762 0 0 0 87914 97 0 0 25 0 1 0 483158402 125169664 27960 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30559 27960 603 41 0 30518 0
vsize: 122236
[startup+890.036 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 28938 0 0 0 88914 98 0 0 25 0 1 0 483158402 125845504 28136 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30724 28136 603 41 0 30683 0
vsize: 122896
[startup+900.036 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 29096 0 0 0 89913 98 0 0 25 0 1 0 483158402 126382080 28294 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30855 28294 603 41 0 30814 0
vsize: 123420
[startup+910.037 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 29240 0 0 0 90913 99 0 0 25 0 1 0 483158402 127053824 28438 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31019 28438 603 41 0 30978 0
vsize: 124076
[startup+920.037 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 29400 0 0 0 91913 100 0 0 25 0 1 0 483158402 127717376 28598 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31181 28598 603 41 0 31140 0
vsize: 124724
[startup+930.037 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 29562 0 0 0 92912 100 0 0 25 0 1 0 483158402 128393216 28760 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31346 28760 603 41 0 31305 0
vsize: 125384
[startup+940.037 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 29731 0 0 0 93912 100 0 0 25 0 1 0 483158402 129056768 28929 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31508 28929 603 41 0 31467 0
vsize: 126032
[startup+950.038 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 29894 0 0 0 94912 101 0 0 25 0 1 0 483158402 129724416 29092 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31671 29092 603 41 0 31630 0
vsize: 126684
[startup+960.038 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 30055 0 0 0 95911 102 0 0 25 0 1 0 483158402 130392064 29253 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31834 29253 603 41 0 31793 0
vsize: 127336
[startup+970.038 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 30207 0 0 0 96911 102 0 0 25 0 1 0 483158402 130924544 29405 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31964 29405 603 41 0 31923 0
vsize: 127856
[startup+980.039 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 30340 0 0 0 97911 102 0 0 25 0 1 0 483158402 131469312 29538 4294967295 134512640 134672761 3221224544 3221223712 134561156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32097 29538 603 41 0 32056 0
vsize: 128388
[startup+990.039 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 30437 0 0 0 98911 102 0 0 25 0 1 0 483158402 131870720 29635 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32195 29635 603 41 0 32154 0
vsize: 128780
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 30586 0 0 0 99911 103 0 0 25 0 1 0 483158402 132689920 29784 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32395 29784 603 41 0 32354 0
vsize: 129580
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 30720 0 0 0 100911 103 0 0 25 0 1 0 483158402 133230592 29918 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32527 29918 603 41 0 32486 0
vsize: 130108
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 30847 0 0 0 101911 103 0 0 25 0 1 0 483158402 133632000 30045 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32625 30045 603 41 0 32584 0
vsize: 130500
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 30965 0 0 0 102911 103 0 0 25 0 1 0 483158402 134168576 30163 4294967295 134512640 134672761 3221224544 3221223648 134560248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32756 30163 603 41 0 32715 0
vsize: 131024
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 31092 0 0 0 103911 104 0 0 25 0 1 0 483158402 134705152 30290 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32887 30290 603 41 0 32846 0
vsize: 131548
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 31209 0 0 0 104911 104 0 0 25 0 1 0 483158402 135102464 30407 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32984 30407 603 41 0 32943 0
vsize: 131936
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 31324 0 0 0 105911 104 0 0 25 0 1 0 483158402 135634944 30522 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33114 30522 603 41 0 33073 0
vsize: 132456
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 31438 0 0 0 106911 105 0 0 25 0 1 0 483158402 136036352 30636 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33212 30636 603 41 0 33171 0
vsize: 132848
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 31547 0 0 0 107910 105 0 0 25 0 1 0 483158402 136433664 30745 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33309 30745 603 41 0 33268 0
vsize: 133236
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 31665 0 0 0 108910 106 0 0 25 0 1 0 483158402 137019392 30863 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33452 30863 603 41 0 33411 0
vsize: 133808
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 31778 0 0 0 109910 106 0 0 25 0 1 0 483158402 137416704 30976 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33549 30976 603 41 0 33508 0
vsize: 134196
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 31893 0 0 0 110909 107 0 0 25 0 1 0 483158402 137953280 31091 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33680 31091 603 41 0 33639 0
vsize: 134720
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 32003 0 0 0 111909 107 0 0 25 0 1 0 483158402 138420224 31201 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33794 31201 603 41 0 33753 0
vsize: 135176
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 32106 0 0 0 112909 108 0 0 25 0 1 0 483158402 138821632 31304 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33892 31304 603 41 0 33851 0
vsize: 135568
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 32217 0 0 0 113909 108 0 0 25 0 1 0 483158402 139223040 31415 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33990 31415 603 41 0 33949 0
vsize: 135960
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 32336 0 0 0 114908 108 0 0 25 0 1 0 483158402 139759616 31534 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34121 31534 603 41 0 34080 0
vsize: 136484
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 32458 0 0 0 115908 109 0 0 25 0 1 0 483158402 140279808 31656 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34248 31656 603 41 0 34207 0
vsize: 136992
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 32580 0 0 0 116908 109 0 0 25 0 1 0 483158402 140812288 31778 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34378 31778 603 41 0 34337 0
vsize: 137512
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 32691 0 0 0 117908 110 0 0 25 0 1 0 483158402 141213696 31889 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34476 31889 603 41 0 34435 0
vsize: 137904
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 32823 0 0 0 118907 110 0 0 25 0 1 0 483158402 141889536 32021 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34641 32021 603 41 0 34600 0
vsize: 138564
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 26218
Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 32929 0 0 0 119907 110 0 0 25 0 1 0 483158402 142290944 32127 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34739 32127 603 41 0 34698 0
vsize: 138956
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.97 1/54 26218
Raw data (stat): 26218 (minisat+) Z 26217 32461 32460 0 -1 12 32931 0 0 0 119907 117 0 0 25 0 1 0 483158402 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.11
CPU time (s): 1200.25
CPU user time (s): 1199.08
CPU system time (s): 1.17182
CPU usage (%): 100.012
Max. virtual memory (Kb): 138956
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####