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/miplib2003/normalized-mps-v2-20-10-vpm2.opb
MD5SUMc1b4c3ad409db732d2b559e570b6f24c
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 138
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 819200
Number of bits of the biggest number in a constraint 20
Biggest sum of numbers in a constraint 4941871
Number of bits of the biggest sum of numbers23
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1189.01
Number of variables2754
Total number of constraints612
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)168
Number of constraints which are nor clauses,nor cardinality constraints444
Minimum length of a constraint1
Maximum length of a constraint84

Trace number 16564 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc7 THE 2005-04-21 07:44:56 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13142 boxname=wulflinc7 idbench=1011 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c1b4c3ad409db732d2b559e570b6f24c  /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-vpm2.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-vpm2.opb /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-vpm2.opb
IDLAUNCH: 13142
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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	: 2
cpu MHz		: 451.050
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:        714724 kB
Buffers:         17752 kB
Cached:         279880 kB
SwapCached:          4 kB
Active:          59400 kB
Inactive:       241136 kB
HighTotal:      131008 kB
HighFree:          280 kB
LowTotal:       903652 kB
LowFree:        714444 kB
SwapTotal:     2097136 kB
SwapFree:      2097132 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6940 kB
Slab:            13820 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 08:04:59 (client local time) WITH STATUS 0 IN 1201.04 SECONDS
stats: 13142 7 1201.04 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 486 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
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:19664
c ---[ 272]---> BDD-cost: 6299
c ---[ 271]---> BDD-cost:    3
c ---[ 270]---> BDD-cost:    3
c ---[ 269]---> BDD-cost:    3
c ---[ 267]---> BDD-cost:    3
c ---[ 266]---> BDD-cost:    3
c ---[ 265]---> BDD-cost:    3
c ---[ 264]---> BDD-cost:    3
c ---[ 263]---> BDD-cost:    3
c ---[ 259]---> BDD-cost:   10
c ---[ 258]---> BDD-cost:    3
c ---[ 257]---> BDD-cost:    3
c ---[ 256]---> BDD-cost:    3
c ---[ 255]---> BDD-cost:   10
c ---[ 251]---> BDD-cost:   10
c ---[ 250]---> BDD-cost:    3
c ---[ 247]---> BDD-cost:    9
c ---[ 243]---> BDD-cost:   10
c ---[ 242]---> BDD-cost:    3
c ---[ 241]---> BDD-cost:    9
c ---[ 236]---> BDD-cost: 8137
c ---[ 235]---> BDD-cost:    3
c ---[ 234]---> BDD-cost:    3
c ---[ 233]---> BDD-cost:    9
c ---[ 229]---> BDD-cost:   10
c ---[ 228]---> BDD-cost:    3
c ---[ 227]---> BDD-cost:    9
c ---[ 224]---> BDD-cost:15538
c ---[ 220]---> BDD-cost:    3
c ---[ 219]---> BDD-cost:    3
c ---[ 214]---> BDD-cost:   10
c ---[ 212]---> BDD-cost:11932
c ---[ 211]---> BDD-cost:    3
c ---[ 206]---> BDD-cost:    3
c ---[ 205]---> BDD-cost:    3
c ---[ 198]---> BDD-cost:    3
c ---[ 197]---> BDD-cost:    3
c ---[ 193]---> BDD-cost:    3
c ---[ 192]---> BDD-cost:    3
c ---[ 191]---> BDD-cost:    3
c ---[ 185]---> BDD-cost:    3
c ---[ 184]---> BDD-cost:    3
c ---[ 183]---> BDD-cost:    3
c ---[ 179]---> BDD-cost:    3
c ---[ 178]---> BDD-cost:    3
c ---[ 175]---> BDD-cost:    3
c ---[ 171]---> BDD-cost:    3
c ---[ 170]---> BDD-cost:    3
c ---[ 169]---> BDD-cost:    3
c ---[ 168]---> BDD-cost:    3
c ---[ 167]---> BDD-cost:    3
c ---[ 166]---> BDD-cost:    9
c ---[ 164]---> BDD-cost: 9270
c ---[ 163]---> BDD-cost:    9
c ---[ 162]---> BDD-cost:    9
c ---[ 161]---> BDD-cost:    9
c ---[ 160]---> BDD-cost:    3
c ---[ 159]---> BDD-cost:   10
c ---[ 158]---> BDD-cost:    9
c ---[ 157]---> BDD-cost:    9
c ---[ 156]---> BDD-cost:    9
c ---[ 155]---> BDD-cost:    9
c ---[ 154]---> BDD-cost:    3
c ---[ 152]---> BDD-cost:19664
c ---[ 150]---> BDD-cost:17235
c ---[ 149]---> BDD-cost:   10
c ---[ 148]---> BDD-cost:    8
c ---[ 147]---> BDD-cost:    8
c ---[ 146]---> BDD-cost:    8
c ---[ 145]---> BDD-cost:    8
c ---[ 144]---> BDD-cost:    3
c ---[ 143]---> BDD-cost:   10
c ---[ 142]---> BDD-cost:    8
c ---[ 141]---> BDD-cost:    8
c ---[ 140]---> BDD-cost:    8
c ---[ 137]---> BDD-cost:    8
c ---[ 135]---> BDD-cost:   10
c ---[ 134]---> BDD-cost:    3
c ---[ 133]---> BDD-cost:    9
c ---[ 132]---> BDD-cost:    9
c ---[ 131]---> BDD-cost:    9
c ---[ 129]---> BDD-cost:   10
c ---[ 128]---> BDD-cost:    3
c ---[ 125]---> BDD-cost:    9
c ---[ 124]---> BDD-cost:    9
c ---[ 123]---> BDD-cost:    9
c ---[ 121]---> BDD-cost:   10
c ---[ 120]---> BDD-cost:    3
c ---[ 119]---> BDD-cost:    9
c ---[ 118]---> BDD-cost:    9
c ---[ 117]---> BDD-cost:    9
c ---[ 114]---> BDD-cost: 5723
c ---[ 113]---> BDD-cost:   10
c ---[ 112]---> BDD-cost:    3
c ---[ 111]---> BDD-cost:    8
c ---[ 110]---> BDD-cost:    8
c ---[ 109]---> BDD-cost:    8
c ---[ 107]---> BDD-cost: 7949
c ---[ 105]---> BDD-cost: 8185
c ---[ 103]---> BDD-cost:18332
c ---[ 101]---> BDD-cost:13927
c ---[  99]---> BDD-cost:13927
c ---[  97]---> BDD-cost:13927
c ---[  95]---> BDD-cost:16439
c ---[  93]---> BDD-cost:13927
c ---[  91]---> BDD-cost:12600
c ---[  89]---> BDD-cost:22214
c ---[  87]---> BDD-cost:16579
c ---[  85]---> BDD-cost:16579
c ---[  83]---> BDD-cost:16579
c ---[  81]---> BDD-cost:11304
c ---[  73]---> BDD-cost:16439
c ---[  69]---> BDD-cost:10343
c ---[  66]---> BDD-cost:  230
c ---[  65]---> BDD-cost:  661
c ---[  64]---> BDD-cost:  660
c ---[  63]---> BDD-cost: 1305
c ---[  62]---> BDD-cost: 1707
c ---[  61]---> BDD-cost: 1700
c ---[  60]---> BDD-cost:  260
c ---[  58]---> BDD-cost:20156
c ---[  57]---> BDD-cost:  714
c ---[  56]---> BDD-cost:  713
c ---[  55]---> BDD-cost: 1410
c ---[  54]---> BDD-cost: 1834
c ---[  53]---> BDD-cost: 1833
c ---[  52]---> BDD-cost:  275
c ---[  51]---> BDD-cost:  777
c ---[  50]---> BDD-cost:  771
c ---[  49]---> BDD-cost: 1542
c ---[  48]---> BDD-cost: 2010
c ---[  46]---> BDD-cost: 4480
c ---[  45]---> BDD-cost: 2007
c ---[  44]---> BDD-cost:  102
c ---[  43]---> BDD-cost:  244
c ---[  42]---> BDD-cost:  240
c ---[  41]---> BDD-cost:  444
c ---[  40]---> BDD-cost:  584
c ---[  39]---> BDD-cost:  579
c ---[  38]---> BDD-cost:    3
c ---[  37]---> BDD-cost:    3
c ---[  36]---> BDD-cost:    3
c ---[  34]---> BDD-cost: 7193
c ---[  33]---> BDD-cost:    3
c ---[  32]---> BDD-cost:    3
c ---[  31]---> BDD-cost:    3
c ---[  30]---> BDD-cost:    3
c ---[  29]---> BDD-cost:    3
c ---[  28]---> BDD-cost:    3
c ---[  27]---> BDD-cost:   10
c ---[  26]---> BDD-cost:   10
c ---[  25]---> BDD-cost:    3
c ---[  24]---> BDD-cost:    3
c ---[  22]---> BDD-cost: 7455
c ---[  21]---> BDD-cost:    3
c ---[  20]---> BDD-cost:    3
c ---[  19]---> BDD-cost:   10
c ---[  18]---> BDD-cost:   10
c ---[  17]---> BDD-cost:    3
c ---[  16]---> BDD-cost:    3
c ---[  15]---> BDD-cost:    3
c ---[  14]---> BDD-cost:    3
c ---[  13]---> BDD-cost:   10
c ---[  12]---> BDD-cost:   10
c ---[  10]---> BDD-cost: 7455
c ---[   9]---> BDD-cost:    3
c ---[   7]---> BDD-cost:   10
c ---[   6]---> BDD-cost:    3
c ---[   5]---> BDD-cost:    3
c ---[   4]---> BDD-cost:    3
c ---[   3]---> BDD-cost:   10
c ---[   1]---> BDD-cost:    3
c ---[   0]---> BDD-cost:    3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 1104701  3100613 |  368233       0        0     nan |  0.000 % |
c |       100 | 1104701  3100613 |  405056     100     1608    16.1 |  0.276 % |
c |       251 | 1104682  3100560 |  445561     248     7319    29.5 |  0.277 % |
c |       476 | 1104539  3100154 |  490118     455    10942    24.0 |  0.287 % |
c |       813 | 1104396  3099752 |  539129     780    21507    27.6 |  0.297 % |
c |      1320 | 1104278  3099417 |  593042    1280    39539    30.9 |  0.302 % |
c |      2081 | 1104278  3099417 |  652347    2041    83429    40.9 |  0.302 % |
c |      3220 | 1104237  3099300 |  717581    3177   113950    35.9 |  0.305 % |
c |      4928 | 1104229  3099276 |  789340    4884   146015    29.9 |  0.306 % |
c |      7490 | 1104165  3099112 |  868274    7441   250732    33.7 |  0.310 % |
c |     11334 | 1104165  3099112 |  955101   11285   500374    44.3 |  0.310 % |
c |     17100 | 1104094  3098927 | 1050611   17044   811678    47.6 |  0.314 % |
c |     25750 | 1104054  3098812 | 1155672   25691  1160987    45.2 |  0.316 % |
c |     38724 | 1104023  3098726 | 1271240   38662  1603491    41.5 |  0.319 % |
c |     58185 | 1103960  3098567 | 1398364   58113  2472393    42.5 |  0.323 % |
c |     87377 | 1103954  3098549 | 1538200   87303  4227289    48.4 |  0.324 % |
c |    131167 | 1103923  3098472 | 1692020  131091  6433018    49.1 |  0.325 % |
#### 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.92 0.95 0.92 2/54 2432
Raw data (stat): 2432 (runsolver) R 2431 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 485163417 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+10.0016 s]
Raw data (loadavg): 0.93 0.96 0.92 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 34741 0 0 0 922 76 0 0 25 0 1 0 485163417 150183936 32541 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36666 32541 603 41 0 36625 0
vsize: 146664
[startup+20.0016 s]
Raw data (loadavg): 0.94 0.96 0.92 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 35411 0 0 0 1920 77 0 0 25 0 1 0 485163417 152481792 33211 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37227 33211 603 41 0 37186 0
vsize: 148908
[startup+30.0017 s]
Raw data (loadavg): 0.95 0.96 0.92 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 35463 0 0 0 2919 78 0 0 25 0 1 0 485163417 152748032 33263 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37292 33263 603 41 0 37251 0
vsize: 149168
[startup+40.002 s]
Raw data (loadavg): 0.96 0.96 0.92 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 35539 0 0 0 3919 78 0 0 25 0 1 0 485163417 153014272 33339 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37357 33339 603 41 0 37316 0
vsize: 149428
[startup+50.0023 s]
Raw data (loadavg): 0.96 0.96 0.92 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 35569 0 0 0 4919 78 0 0 25 0 1 0 485163417 153145344 33369 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37389 33369 603 41 0 37348 0
vsize: 149556
[startup+60.0023 s]
Raw data (loadavg): 0.97 0.96 0.92 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 35590 0 0 0 5919 78 0 0 25 0 1 0 485163417 153276416 33390 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37421 33390 603 41 0 37380 0
vsize: 149684
[startup+70.0032 s]
Raw data (loadavg): 0.97 0.96 0.92 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 35607 0 0 0 6919 78 0 0 25 0 1 0 485163417 153276416 33407 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37421 33407 603 41 0 37380 0
vsize: 149684
[startup+80.0032 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 35658 0 0 0 7919 79 0 0 25 0 1 0 485163417 153407488 33458 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37453 33458 603 41 0 37412 0
vsize: 149812
[startup+90.0032 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 35717 0 0 0 8919 79 0 0 25 0 1 0 485163417 153677824 33517 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37519 33517 603 41 0 37478 0
vsize: 150076
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 35764 0 0 0 9919 79 0 0 25 0 1 0 485163417 153944064 33564 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37584 33564 603 41 0 37543 0
vsize: 150336
[startup+110.002 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 35833 0 0 0 10917 80 0 0 25 0 1 0 485163417 154214400 33633 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37650 33633 603 41 0 37609 0
vsize: 150600
[startup+120.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 36004 0 0 0 11917 81 0 0 25 0 1 0 485163417 154890240 33804 4294967295 134512640 134672761 3221224544 3221223648 134554910 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37815 33804 603 41 0 37774 0
vsize: 151260
[startup+130.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 36117 0 0 0 12917 81 0 0 25 0 1 0 485163417 155291648 33917 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37913 33917 603 41 0 37872 0
vsize: 151652
[startup+140.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 36189 0 0 0 13917 81 0 0 25 0 1 0 485163417 155693056 33989 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38011 33989 603 41 0 37970 0
vsize: 152044
[startup+150.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 36263 0 0 0 14918 81 0 0 25 0 1 0 485163417 155959296 34063 4294967295 134512640 134672761 3221224544 3221223744 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38076 34063 603 41 0 38035 0
vsize: 152304
[startup+160.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 36336 0 0 0 15918 82 0 0 25 0 1 0 485163417 156225536 34136 4294967295 134512640 134672761 3221224544 3221223640 1075347236 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38141 34136 603 41 0 38100 0
vsize: 152564
[startup+170.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 36403 0 0 0 16918 82 0 0 25 0 1 0 485163417 156614656 34203 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38236 34203 603 41 0 38195 0
vsize: 152944
[startup+180.021 s]
Raw data (loadavg): 1.07 0.99 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 36941 0 0 0 17917 83 0 0 25 0 1 0 485163417 158367744 34741 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38664 34741 603 41 0 38623 0
vsize: 154656
[startup+190.031 s]
Raw data (loadavg): 1.06 0.99 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 37105 0 0 0 18918 83 0 0 25 0 1 0 485163417 159039488 34905 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38828 34905 603 41 0 38787 0
vsize: 155312
[startup+200.031 s]
Raw data (loadavg): 1.05 0.99 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 37177 0 0 0 19918 83 0 0 25 0 1 0 485163417 159305728 34977 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38893 34977 603 41 0 38852 0
vsize: 155572
[startup+210.031 s]
Raw data (loadavg): 1.04 0.99 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 37279 0 0 0 20918 84 0 0 25 0 1 0 485163417 159707136 35079 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38991 35079 603 41 0 38950 0
vsize: 155964
[startup+220.037 s]
Raw data (loadavg): 1.04 0.99 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 37403 0 0 0 21919 84 0 0 25 0 1 0 485163417 160239616 35203 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39121 35203 603 41 0 39080 0
vsize: 156484
[startup+230.037 s]
Raw data (loadavg): 1.03 0.99 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 37513 0 0 0 22919 84 0 0 25 0 1 0 485163417 160636928 35313 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39218 35313 603 41 0 39177 0
vsize: 156872
[startup+240.043 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 37613 0 0 0 23919 84 0 0 25 0 1 0 485163417 161030144 35413 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39314 35413 603 41 0 39273 0
vsize: 157256
[startup+250.042 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 37710 0 0 0 24919 85 0 0 25 0 1 0 485163417 161562624 35510 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39444 35510 603 41 0 39403 0
vsize: 157776
[startup+260.051 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 37799 0 0 0 25920 85 0 0 25 0 1 0 485163417 161968128 35599 4294967295 134512640 134672761 3221224544 3221223712 134560803 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39543 35599 603 41 0 39502 0
vsize: 158172
[startup+270.05 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 37832 0 0 0 26920 85 0 0 25 0 1 0 485163417 162099200 35632 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39575 35632 603 41 0 39534 0
vsize: 158300
[startup+280.05 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 37860 0 0 0 27920 85 0 0 25 0 1 0 485163417 162230272 35660 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39607 35660 603 41 0 39566 0
vsize: 158428
[startup+290.363 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 37953 0 0 0 28951 86 0 0 25 0 1 0 485163417 162496512 35753 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39672 35753 603 41 0 39631 0
vsize: 158688
[startup+300.363 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 37988 0 0 0 29951 86 0 0 25 0 1 0 485163417 162627584 35788 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39704 35788 603 41 0 39663 0
vsize: 158816
[startup+310.388 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 38017 0 0 0 30953 86 0 0 25 0 1 0 485163417 162758656 35817 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39736 35817 603 41 0 39695 0
vsize: 158944
[startup+320.387 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 38076 0 0 0 31953 86 0 0 25 0 1 0 485163417 163028992 35876 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39802 35876 603 41 0 39761 0
vsize: 159208
[startup+330.396 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 38122 0 0 0 32954 86 0 0 25 0 1 0 485163417 163295232 35922 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39867 35922 603 41 0 39826 0
vsize: 159468
[startup+340.395 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 38190 0 0 0 33955 86 0 0 25 0 1 0 485163417 163557376 35990 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39931 35990 603 41 0 39890 0
vsize: 159724
[startup+350.399 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 38244 0 0 0 34955 86 0 0 25 0 1 0 485163417 163688448 36044 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39963 36044 603 41 0 39922 0
vsize: 159852
[startup+360.407 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 38298 0 0 0 35956 86 0 0 25 0 1 0 485163417 163954688 36098 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40028 36098 603 41 0 39987 0
vsize: 160112
[startup+370.407 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 38386 0 0 0 36955 87 0 0 25 0 1 0 485163417 164352000 36186 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40125 36186 603 41 0 40084 0
vsize: 160500
[startup+380.406 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 38462 0 0 0 37955 87 0 0 25 0 1 0 485163417 164618240 36262 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40190 36262 603 41 0 40149 0
vsize: 160760
[startup+390.406 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 38525 0 0 0 38955 88 0 0 25 0 1 0 485163417 164888576 36325 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40256 36325 603 41 0 40215 0
vsize: 161024
[startup+400.406 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 38598 0 0 0 39955 88 0 0 25 0 1 0 485163417 165191680 36398 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40330 36398 603 41 0 40289 0
vsize: 161320
[startup+410.405 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 38686 0 0 0 40955 88 0 0 25 0 1 0 485163417 165490688 36486 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40403 36486 603 41 0 40362 0
vsize: 161612
[startup+420.405 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 38788 0 0 0 41955 88 0 0 25 0 1 0 485163417 165892096 36588 4294967295 134512640 134672761 3221224544 3221223744 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40501 36588 603 41 0 40460 0
vsize: 162004
[startup+430.405 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 38898 0 0 0 42954 89 0 0 25 0 1 0 485163417 166436864 36698 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40634 36698 603 41 0 40593 0
vsize: 162536
[startup+440.405 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 38960 0 0 0 43954 89 0 0 25 0 1 0 485163417 166567936 36760 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40666 36760 603 41 0 40625 0
vsize: 162664
[startup+450.405 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 39028 0 0 0 44954 89 0 0 25 0 1 0 485163417 166969344 36828 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40764 36828 603 41 0 40723 0
vsize: 163056
[startup+460.405 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 39056 0 0 0 45954 89 0 0 25 0 1 0 485163417 166969344 36856 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40764 36856 603 41 0 40723 0
vsize: 163056
[startup+470.406 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 39092 0 0 0 46954 89 0 0 25 0 1 0 485163417 167104512 36892 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40797 36892 603 41 0 40756 0
vsize: 163188
[startup+480.405 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 39129 0 0 0 47954 89 0 0 25 0 1 0 485163417 167378944 36929 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40864 36929 603 41 0 40823 0
vsize: 163456
[startup+490.445 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 39291 0 0 0 48957 90 0 0 25 0 1 0 485163417 167911424 37091 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40994 37091 603 41 0 40953 0
vsize: 163976
[startup+500.461 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 39429 0 0 0 49958 91 0 0 25 0 1 0 485163417 168574976 37229 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41156 37229 603 41 0 41115 0
vsize: 164624
[startup+510.46 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 39582 0 0 0 50958 92 0 0 25 0 1 0 485163417 169369600 37382 4294967295 134512640 134672761 3221224544 3221223640 1075347141 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41350 37382 603 41 0 41309 0
vsize: 165400
[startup+520.467 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 39727 0 0 0 51958 92 0 0 25 0 1 0 485163417 170037248 37527 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41513 37527 603 41 0 41472 0
vsize: 166052
[startup+530.475 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 39868 0 0 0 52959 92 0 0 25 0 1 0 485163417 170569728 37668 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41643 37668 603 41 0 41602 0
vsize: 166572
[startup+540.475 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 40007 0 0 0 53959 93 0 0 25 0 1 0 485163417 171110400 37807 4294967295 134512640 134672761 3221224544 3221223648 134560303 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41775 37807 603 41 0 41734 0
vsize: 167100
[startup+550.484 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 40152 0 0 0 54959 93 0 0 25 0 1 0 485163417 171794432 37952 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41942 37952 603 41 0 41901 0
vsize: 167768
[startup+560.491 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 40281 0 0 0 55960 94 0 0 25 0 1 0 485163417 172326912 38081 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42072 38081 603 41 0 42031 0
vsize: 168288
[startup+570.5 s]
Raw data (loadavg): 1.08 1.00 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 40423 0 0 0 56961 94 0 0 25 0 1 0 485163417 172851200 38223 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42200 38223 603 41 0 42159 0
vsize: 168800
[startup+580.5 s]
Raw data (loadavg): 1.07 1.00 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 40550 0 0 0 57960 94 0 0 25 0 1 0 485163417 173412352 38350 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42337 38350 603 41 0 42296 0
vsize: 169348
[startup+590.5 s]
Raw data (loadavg): 1.06 1.00 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 40681 0 0 0 58960 95 0 0 25 0 1 0 485163417 173961216 38481 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42471 38481 603 41 0 42430 0
vsize: 169884
[startup+600.5 s]
Raw data (loadavg): 1.05 1.00 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 40800 0 0 0 59960 95 0 0 25 0 1 0 485163417 174362624 38600 4294967295 134512640 134672761 3221224544 3221223680 134560726 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42569 38600 603 41 0 42528 0
vsize: 170276
[startup+610.5 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 40917 0 0 0 60960 95 0 0 25 0 1 0 485163417 174891008 38717 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42698 38717 603 41 0 42657 0
vsize: 170792
[startup+620.5 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 41026 0 0 0 61959 96 0 0 25 0 1 0 485163417 175304704 38826 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42799 38826 603 41 0 42758 0
vsize: 171196
[startup+630.5 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 41083 0 0 0 62957 96 0 0 25 0 1 0 485163417 175566848 38883 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42863 38883 603 41 0 42822 0
vsize: 171452
[startup+640.501 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 41162 0 0 0 63957 97 0 0 25 0 1 0 485163417 175841280 38962 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42930 38962 603 41 0 42889 0
vsize: 171720
[startup+650.5 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 41255 0 0 0 64957 97 0 0 25 0 1 0 485163417 176242688 39055 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43028 39055 603 41 0 42987 0
vsize: 172112
[startup+660.5 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 41313 0 0 0 65957 97 0 0 25 0 1 0 485163417 176513024 39113 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43094 39113 603 41 0 43053 0
vsize: 172376
[startup+670.5 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 41369 0 0 0 66957 97 0 0 25 0 1 0 485163417 176783360 39169 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43160 39169 603 41 0 43119 0
vsize: 172640
[startup+680.504 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 41428 0 0 0 67958 97 0 0 25 0 1 0 485163417 176914432 39228 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43192 39228 603 41 0 43151 0
vsize: 172768
[startup+690.504 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 41508 0 0 0 68958 97 0 0 25 0 1 0 485163417 177315840 39308 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43290 39308 603 41 0 43249 0
vsize: 173160
[startup+700.504 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 41595 0 0 0 69958 97 0 0 25 0 1 0 485163417 177582080 39395 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43355 39395 603 41 0 43314 0
vsize: 173420
[startup+710.511 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 41667 0 0 0 70958 98 0 0 25 0 1 0 485163417 177979392 39467 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43452 39467 603 41 0 43411 0
vsize: 173808
[startup+720.51 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 41755 0 0 0 71958 98 0 0 25 0 1 0 485163417 178249728 39555 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43518 39555 603 41 0 43477 0
vsize: 174072
[startup+730.522 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 41868 0 0 0 72959 99 0 0 25 0 1 0 485163417 178802688 39668 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43653 39668 603 41 0 43612 0
vsize: 174612
[startup+740.525 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 41949 0 0 0 73959 99 0 0 25 0 1 0 485163417 179073024 39749 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43719 39749 603 41 0 43678 0
vsize: 174876
[startup+750.525 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 42021 0 0 0 74959 99 0 0 25 0 1 0 485163417 179343360 39821 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43785 39821 603 41 0 43744 0
vsize: 175140
[startup+760.525 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 42099 0 0 0 75959 99 0 0 25 0 1 0 485163417 179761152 39899 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43887 39899 603 41 0 43846 0
vsize: 175548
[startup+770.526 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 42173 0 0 0 76959 99 0 0 25 0 1 0 485163417 180023296 39973 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43951 39973 603 41 0 43910 0
vsize: 175804
[startup+780.525 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 42246 0 0 0 77959 100 0 0 25 0 1 0 485163417 180289536 40046 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44016 40046 603 41 0 43975 0
vsize: 176064
[startup+790.526 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 42326 0 0 0 78959 100 0 0 25 0 1 0 485163417 180682752 40126 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44112 40126 603 41 0 44071 0
vsize: 176448
[startup+800.533 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 42423 0 0 0 79960 100 0 0 25 0 1 0 485163417 181116928 40223 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44218 40223 603 41 0 44177 0
vsize: 176872
[startup+810.532 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 42512 0 0 0 80960 100 0 0 25 0 1 0 485163417 181538816 40312 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44321 40312 603 41 0 44280 0
vsize: 177284
[startup+820.54 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 42610 0 0 0 81960 100 0 0 25 0 1 0 485163417 181940224 40410 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44419 40410 603 41 0 44378 0
vsize: 177676
[startup+830.546 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 42676 0 0 0 82961 101 0 0 25 0 1 0 485163417 182206464 40476 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44484 40476 603 41 0 44443 0
vsize: 177936
[startup+840.546 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 42727 0 0 0 83961 101 0 0 25 0 1 0 485163417 182341632 40527 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44517 40527 603 41 0 44476 0
vsize: 178068
[startup+850.549 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 42796 0 0 0 84962 101 0 0 25 0 1 0 485163417 182607872 40596 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44582 40596 603 41 0 44541 0
vsize: 178328
[startup+860.553 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 42866 0 0 0 85961 101 0 0 25 0 1 0 485163417 182874112 40666 4294967295 134512640 134672761 3221224544 3221223680 134560625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44647 40666 603 41 0 44606 0
vsize: 178588
[startup+870.553 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 42927 0 0 0 86961 102 0 0 25 0 1 0 485163417 183136256 40727 4294967295 134512640 134672761 3221224544 3221223712 134560822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44711 40727 603 41 0 44670 0
vsize: 178844
[startup+880.553 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 42995 0 0 0 87961 102 0 0 25 0 1 0 485163417 183398400 40795 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44775 40795 603 41 0 44734 0
vsize: 179100
[startup+890.559 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 43067 0 0 0 88962 102 0 0 25 0 1 0 485163417 183795712 40867 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44872 40867 603 41 0 44831 0
vsize: 179488
[startup+900.559 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2432
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 43131 0 0 0 89962 102 0 0 25 0 1 0 485163417 184061952 40931 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44937 40931 603 41 0 44896 0
vsize: 179748
[startup+910.801 s]
Raw data (loadavg): 1.08 1.02 0.94 3/58 2436
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 43202 0 0 0 90986 102 0 0 25 0 1 0 485163417 184328192 41002 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45002 41002 603 41 0 44961 0
vsize: 180008
[startup+920.811 s]
Raw data (loadavg): 1.29 1.06 0.95 2/56 2480
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 43258 0 0 0 91986 103 0 0 25 0 1 0 485163417 184598528 41058 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45068 41058 603 41 0 45027 0
vsize: 180272
[startup+930.811 s]
Raw data (loadavg): 1.25 1.06 0.95 2/54 2485
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 43322 0 0 0 92986 103 0 0 25 0 1 0 485163417 184729600 41122 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45100 41122 603 41 0 45059 0
vsize: 180400
[startup+940.811 s]
Raw data (loadavg): 1.21 1.06 0.95 2/54 2485
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 43387 0 0 0 93986 103 0 0 25 0 1 0 485163417 184991744 41187 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45164 41187 603 41 0 45123 0
vsize: 180656
[startup+950.816 s]
Raw data (loadavg): 1.18 1.06 0.95 2/54 2485
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 43459 0 0 0 94986 104 0 0 25 0 1 0 485163417 185405440 41259 4294967295 134512640 134672761 3221224544 3221223680 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45265 41259 603 41 0 45224 0
vsize: 181060
[startup+960.816 s]
Raw data (loadavg): 1.15 1.05 0.95 2/54 2485
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 43535 0 0 0 95986 104 0 0 25 0 1 0 485163417 185696256 41335 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45336 41335 603 41 0 45295 0
vsize: 181344
[startup+970.816 s]
Raw data (loadavg): 1.13 1.05 0.95 2/54 2485
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 43600 0 0 0 96986 104 0 0 25 0 1 0 485163417 185966592 41400 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45402 41400 603 41 0 45361 0
vsize: 181608
[startup+980.815 s]
Raw data (loadavg): 1.11 1.05 0.95 2/54 2485
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 43663 0 0 0 97986 104 0 0 25 0 1 0 485163417 186232832 41463 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45467 41463 603 41 0 45426 0
vsize: 181868
[startup+990.816 s]
Raw data (loadavg): 1.09 1.05 0.95 2/54 2485
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 43767 0 0 0 98986 105 0 0 25 0 1 0 485163417 187174912 41567 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45697 41567 603 41 0 45656 0
vsize: 182788
[startup+1000.82 s]
Raw data (loadavg): 1.08 1.05 0.95 2/54 2487
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 43803 0 0 0 99985 105 0 0 25 0 1 0 485163417 187305984 41603 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45729 41603 603 41 0 45688 0
vsize: 182916
[startup+1010.81 s]
Raw data (loadavg): 1.06 1.04 0.95 2/54 2487
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 43876 0 0 0 100985 106 0 0 25 0 1 0 485163417 187576320 41676 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45795 41676 603 41 0 45754 0
vsize: 183180
[startup+1020.81 s]
Raw data (loadavg): 1.05 1.04 0.95 2/54 2487
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 43953 0 0 0 101985 106 0 0 25 0 1 0 485163417 187842560 41753 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45860 41753 603 41 0 45819 0
vsize: 183440
[startup+1030.81 s]
Raw data (loadavg): 1.04 1.04 0.95 2/54 2487
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 44031 0 0 0 102985 106 0 0 25 0 1 0 485163417 188239872 41831 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45957 41831 603 41 0 45916 0
vsize: 183828
[startup+1040.81 s]
Raw data (loadavg): 1.04 1.04 0.95 2/54 2487
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 44114 0 0 0 103985 106 0 0 25 0 1 0 485163417 188502016 41914 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46021 41914 603 41 0 45980 0
vsize: 184084
[startup+1050.81 s]
Raw data (loadavg): 1.03 1.04 0.95 2/54 2487
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 44192 0 0 0 104984 107 0 0 25 0 1 0 485163417 188899328 41992 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46118 41992 603 41 0 46077 0
vsize: 184472
[startup+1060.81 s]
Raw data (loadavg): 1.03 1.04 0.95 2/54 2487
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 44263 0 0 0 105984 107 0 0 25 0 1 0 485163417 189161472 42063 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46182 42063 603 41 0 46141 0
vsize: 184728
[startup+1070.81 s]
Raw data (loadavg): 1.02 1.03 0.95 2/54 2487
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 44329 0 0 0 106984 107 0 0 25 0 1 0 485163417 189427712 42129 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46247 42129 603 41 0 46206 0
vsize: 184988
[startup+1080.81 s]
Raw data (loadavg): 1.02 1.03 0.95 2/54 2487
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 44427 0 0 0 107984 108 0 0 25 0 1 0 485163417 189837312 42227 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46347 42227 603 41 0 46306 0
vsize: 185388
[startup+1090.81 s]
Raw data (loadavg): 1.01 1.03 0.95 2/54 2487
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 44527 0 0 0 108983 108 0 0 25 0 1 0 485163417 190283776 42327 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46456 42327 603 41 0 46415 0
vsize: 185824
[startup+1100.81 s]
Raw data (loadavg): 1.01 1.03 0.95 2/54 2487
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 44597 0 0 0 109983 109 0 0 25 0 1 0 485163417 190550016 42397 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46521 42397 603 41 0 46480 0
vsize: 186084
[startup+1110.81 s]
Raw data (loadavg): 1.01 1.03 0.95 2/54 2487
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 44673 0 0 0 110983 109 0 0 25 0 1 0 485163417 190861312 42473 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46597 42473 603 41 0 46556 0
vsize: 186388
[startup+1120.81 s]
Raw data (loadavg): 1.01 1.03 0.95 2/54 2487
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 44732 0 0 0 111983 109 0 0 25 0 1 0 485163417 191139840 42532 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46665 42532 603 41 0 46624 0
vsize: 186660
[startup+1130.81 s]
Raw data (loadavg): 1.01 1.03 0.95 2/54 2487
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 44800 0 0 0 112983 109 0 0 25 0 1 0 485163417 191422464 42600 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46734 42600 603 41 0 46693 0
vsize: 186936
[startup+1140.81 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 2487
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 44864 0 0 0 113983 109 0 0 25 0 1 0 485163417 191717376 42664 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46806 42664 603 41 0 46765 0
vsize: 187224
[startup+1150.81 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 2487
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 44928 0 0 0 114983 110 0 0 25 0 1 0 485163417 191987712 42728 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46872 42728 603 41 0 46831 0
vsize: 187488
[startup+1160.81 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 2487
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 45032 0 0 0 115983 110 0 0 25 0 1 0 485163417 192311296 42832 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46951 42832 603 41 0 46910 0
vsize: 187804
[startup+1170.81 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 2487
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 45133 0 0 0 116983 111 0 0 25 0 1 0 485163417 192937984 42933 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47104 42933 603 41 0 47063 0
vsize: 188416
[startup+1180.81 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 2487
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 45207 0 0 0 117982 111 0 0 25 0 1 0 485163417 193208320 43007 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47170 43007 603 41 0 47129 0
vsize: 188680
[startup+1190.81 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 2487
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 45281 0 0 0 118982 111 0 0 25 0 1 0 485163417 193474560 43081 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47235 43081 603 41 0 47194 0
vsize: 188940
[startup+1200.82 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 2487
Raw data (stat): 2432 (minisat+) R 2431 22932 22931 0 -1 0 45356 0 0 0 119983 111 0 0 25 0 1 0 485163417 193740800 43156 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47300 43156 603 41 0 47259 0
vsize: 189200
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.9 s]
Raw data (loadavg): 1.00 1.02 0.95 1/54 2487
Raw data (stat): 2432 (minisat+) Z 2431 22932 22931 0 -1 12 45358 0 0 0 119983 120 0 0 25 0 1 0 485163417 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.9
CPU time (s): 1201.04
CPU user time (s): 1199.83
CPU system time (s): 1.20282
CPU usage (%): 100.011
Max. virtual memory (Kb): 189200
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####