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-dcmulti.opb
MD5SUM28123830d5f7e3646d18978bb347487c
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableNO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 9505
Biggest coefficient in the objective function 697303040
Number of bits for the biggest coefficient in the objective function 30
Sum of the numbers in the objective function 66656504525
Number of bits of the sum of numbers in the objective function 36
Biggest number in a constraint 697303040
Number of bits of the biggest number in a constraint 30
Biggest sum of numbers in a constraint 66656504525
Number of bits of the biggest sum of numbers36
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark0.085986
Number of variables9535
Total number of constraints365
Number of constraints which are clauses27
Number of constraints which are cardinality constraints (but not clauses)80
Number of constraints which are nor clauses,nor cardinality constraints258
Minimum length of a constraint1
Maximum length of a constraint280

Trace number 18293 

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        579068 kB
Buffers:         23340 kB
Cached:         409968 kB
SwapCached:        328 kB
Active:          60032 kB
Inactive:       375756 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        578816 kB
SwapTotal:     2097136 kB
SwapFree:      2096444 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5728 kB
Slab:            14156 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 14:34:00 (client local time) WITH STATUS 0 IN 1200.33 SECONDS
stats: 18290 7 1200.33 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 368 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ##############################################################################
c   -- Clauses(.)/Splits(s): s....s.....sssssssssssssssssss....s.....ssssssssssssssssss....s.....sssssssssssssssssss
c ---[ 427]---> BDD-cost:   14
c ---[ 426]---> BDD-cost:  525
c ---[ 425]---> BDD-cost:  570
c ---[ 424]---> BDD-cost:  570
c ---[ 422]---> BDD-cost:   15
c ---[ 421]---> BDD-cost:   14
c ---[ 420]---> BDD-cost:   14
c ---[ 419]---> BDD-cost:   13
c ---[ 418]---> BDD-cost:   14
c ---[ 416]---> BDD-cost: 3918
c ---[ 415]---> BDD-cost:   14
c ---[ 413]---> BDD-cost: 3850
c ---[ 411]---> BDD-cost: 3918
c ---[ 409]---> BDD-cost: 3850
c ---[ 407]---> BDD-cost: 3918
c ---[ 405]---> BDD-cost: 3850
c ---[ 403]---> BDD-cost: 3918
c ---[ 401]---> BDD-cost: 3850
c ---[ 399]---> BDD-cost: 3918
c ---[ 397]---> BDD-cost: 3850
c ---[ 395]---> BDD-cost:  437
c ---[ 394]---> BDD-cost:   13
c ---[ 392]---> BDD-cost:  411
c ---[ 391]---> BDD-cost:   16
c ---[ 390]---> BDD-cost:    7
c ---[ 389]---> BDD-cost:   15
c ---[ 388]---> BDD-cost:    4
c ---[ 386]---> BDD-cost:  409
c ---[ 385]---> BDD-cost:   24
c ---[ 384]---> BDD-cost:    6
c ---[ 381]---> BDD-cost:  437
c ---[ 380]---> BDD-cost:   14
c ---[ 378]---> BDD-cost:  411
c ---[ 377]---> BDD-cost:   16
c ---[ 376]---> BDD-cost:    7
c ---[ 375]---> BDD-cost:   15
c ---[ 374]---> BDD-cost:    4
c ---[ 372]---> BDD-cost:  409
c ---[ 371]---> BDD-cost:   23
c ---[ 370]---> BDD-cost:    8
c ---[ 367]---> BDD-cost:  420
c ---[ 365]---> BDD-cost: 3159
c ---[ 363]---> BDD-cost:  392
c ---[ 362]---> BDD-cost:   15
c ---[ 361]---> BDD-cost:    6
c ---[ 360]---> BDD-cost:   14
c ---[ 359]---> BDD-cost:    3
c ---[ 357]---> BDD-cost:  379
c ---[ 356]---> BDD-cost:   23
c ---[ 355]---> BDD-cost:    6
c ---[ 352]---> BDD-cost:  437
c ---[ 350]---> BDD-cost: 3023
c ---[ 348]---> BDD-cost:  411
c ---[ 347]---> BDD-cost:   16
c ---[ 346]---> BDD-cost:    7
c ---[ 345]---> BDD-cost:   15
c ---[ 344]---> BDD-cost:    4
c ---[ 342]---> BDD-cost:  409
c ---[ 341]---> BDD-cost:   24
c ---[ 340]---> BDD-cost:    6
c ---[ 337]---> BDD-cost:  437
c ---[ 335]---> BDD-cost: 3159
c ---[ 333]---> BDD-cost:  411
c ---[ 332]---> BDD-cost:   16
c ---[ 331]---> BDD-cost:    7
c ---[ 330]---> BDD-cost:   15
c ---[ 329]---> BDD-cost:    4
c ---[ 327]---> BDD-cost:  409
c ---[ 326]---> BDD-cost:   19
c ---[ 322]---> BDD-cost:   33
c ---[ 320]---> BDD-cost: 3023
c ---[ 308]---> BDD-cost: 3159
c ---[ 296]---> BDD-cost: 3023
c ---[ 293]---> BDD-cost:  570
c ---[ 292]---> BDD-cost:  570
c ---[ 291]---> BDD-cost:  615
c ---[ 290]---> BDD-cost:  525
c ---[ 289]---> BDD-cost:  570
c ---[ 288]---> BDD-cost:  570
c ---[ 286]---> BDD-cost:   15
c ---[ 285]---> BDD-cost:  570
c ---[ 283]---> BDD-cost: 3159
c ---[ 282]---> BDD-cost:   14
c ---[ 281]---> BDD-cost:   14
c ---[ 280]---> BDD-cost:   13
c ---[ 279]---> BDD-cost:   14
c ---[ 277]---> BDD-cost: 3501
c ---[ 275]---> BDD-cost: 3452
c ---[ 273]---> BDD-cost: 3501
c ---[ 271]---> BDD-cost: 3452
c ---[ 269]---> BDD-cost: 3501
c ---[ 267]---> BDD-cost: 3452
c ---[ 265]---> BDD-cost: 3023
c ---[ 263]---> BDD-cost: 3501
c ---[ 261]---> BDD-cost: 3452
c ---[ 259]---> BDD-cost: 3501
c ---[ 257]---> BDD-cost: 3452
c ---[ 255]---> BDD-cost:  437
c ---[ 253]---> BDD-cost:  411
c ---[ 252]---> BDD-cost:   16
c ---[ 251]---> BDD-cost:    7
c ---[ 250]---> BDD-cost:   15
c ---[ 249]---> BDD-cost:    4
c ---[ 247]---> BDD-cost: 3159
c ---[ 245]---> BDD-cost:  409
c ---[ 244]---> BDD-cost:   24
c ---[ 243]---> BDD-cost:    6
c ---[ 240]---> BDD-cost:  437
c ---[ 238]---> BDD-cost:  411
c ---[ 237]---> BDD-cost:   16
c ---[ 236]---> BDD-cost:    7
c ---[ 235]---> BDD-cost:   15
c ---[ 234]---> BDD-cost:    4
c ---[ 232]---> BDD-cost: 3023
c ---[ 230]---> BDD-cost:  409
c ---[ 229]---> BDD-cost:   23
c ---[ 228]---> BDD-cost:    8
c ---[ 225]---> BDD-cost:  420
c ---[ 223]---> BDD-cost:  392
c ---[ 222]---> BDD-cost:   15
c ---[ 221]---> BDD-cost:    6
c ---[ 220]---> BDD-cost:   14
c ---[ 219]---> BDD-cost:    3
c ---[ 217]---> BDD-cost:  430
c ---[ 215]---> BDD-cost:  379
c ---[ 214]---> BDD-cost:   23
c ---[ 213]---> BDD-cost:    6
c ---[ 210]---> BDD-cost:  437
c ---[ 208]---> BDD-cost:  411
c ---[ 207]---> BDD-cost:   16
c ---[ 206]---> BDD-cost:    7
c ---[ 205]---> BDD-cost:   15
c ---[ 204]---> BDD-cost:    4
c ---[ 202]---> BDD-cost:  404
c ---[ 200]---> BDD-cost:  409
c ---[ 199]---> BDD-cost:   24
c ---[ 198]---> BDD-cost:    6
c ---[ 195]---> BDD-cost:  437
c ---[ 193]---> BDD-cost:  411
c ---[ 192]---> BDD-cost:   16
c ---[ 191]---> BDD-cost:    7
c ---[ 190]---> BDD-cost:   15
c ---[ 189]---> BDD-cost:    4
c ---[ 188]---> BDD-cost:   16
c ---[ 186]---> BDD-cost:  409
c ---[ 185]---> BDD-cost:   19
c ---[ 181]---> BDD-cost:   33
c ---[ 175]---> BDD-cost:    7
c ---[ 164]---> BDD-cost:   15
c ---[ 156]---> BDD-cost:    3
c ---[ 155]---> BDD-cost:    3
c ---[ 154]---> BDD-cost:    3
c ---[ 153]---> BDD-cost:    4
c ---[ 152]---> BDD-cost:    3
c ---[ 151]---> BDD-cost:    3
c ---[ 150]---> BDD-cost:  570
c ---[ 148]---> BDD-cost:  409
c ---[ 147]---> BDD-cost:   24
c ---[ 146]---> BDD-cost:    6
c ---[ 143]---> BDD-cost:  430
c ---[ 141]---> BDD-cost:  404
c ---[ 140]---> BDD-cost:   16
c ---[ 139]---> BDD-cost:    7
c ---[ 138]---> BDD-cost:   15
c ---[ 137]---> BDD-cost:    4
c ---[ 136]---> BDD-cost:  615
c ---[ 134]---> BDD-cost:  409
c ---[ 133]---> BDD-cost:   23
c ---[ 132]---> BDD-cost:    8
c ---[ 129]---> BDD-cost:  413
c ---[ 127]---> BDD-cost:  385
c ---[ 126]---> BDD-cost:   15
c ---[ 125]---> BDD-cost:    6
c ---[ 124]---> BDD-cost:   14
c ---[ 123]---> BDD-cost:    3
c ---[ 122]---> BDD-cost:  525
c ---[ 120]---> BDD-cost:  379
c ---[ 119]---> BDD-cost:   23
c ---[ 118]---> BDD-cost:    6
c ---[ 115]---> BDD-cost:  430
c ---[ 113]---> BDD-cost:  404
c ---[ 112]---> BDD-cost:   16
c ---[ 111]---> BDD-cost:    7
c ---[ 110]---> BDD-cost:   15
c ---[ 109]---> BDD-cost:    4
c ---[ 108]---> BDD-cost:  570
c ---[ 106]---> BDD-cost:  409
c ---[ 105]---> BDD-cost:   24
c ---[ 104]---> BDD-cost:    6
c ---[ 101]---> BDD-cost:  430
c ---[  99]---> BDD-cost:  404
c ---[  98]---> BDD-cost:   16
c ---[  97]---> BDD-cost:    7
c ---[  96]---> BDD-cost:   15
c ---[  95]---> BDD-cost:    4
c ---[  94]---> BDD-cost:  570
c ---[  92]---> BDD-cost:  409
c ---[  91]---> BDD-cost:   19
c ---[  87]---> BDD-cost:   33
c ---[  70]---> BDD-cost:   15
c ---[  62]---> BDD-cost:  570
c ---[  61]---> BDD-cost:  570
c ---[  60]---> BDD-cost:  615
c ---[  59]---> BDD-cost:   12
c ---[  58]---> BDD-cost:    5
c ---[  57]---> BDD-cost:  326
c ---[  56]---> BDD-cost:  295
c ---[  55]---> BDD-cost:  330
c ---[  54]---> BDD-cost:  300
c ---[  53]---> BDD-cost:  351
c ---[  52]---> BDD-cost:  330
c ---[  51]---> BDD-cost:  305
c ---[  50]---> BDD-cost:  285
c ---[  49]---> BDD-cost:  305
c ---[  48]---> BDD-cost:  270
c ---[  47]---> BDD-cost:  351
c ---[  46]---> BDD-cost:  305
c ---[  45]---> BDD-cost:  326
c ---[  44]---> BDD-cost:  295
c ---[  43]---> BDD-cost:  296
c ---[  42]---> BDD-cost:  265
c ---[  41]---> BDD-cost:  361
c ---[  40]---> BDD-cost:  326
c ---[  39]---> BDD-cost:   12
c ---[  38]---> BDD-cost:    5
c ---[  37]---> BDD-cost:  321
c ---[  36]---> BDD-cost:  298
c ---[  35]---> BDD-cost:  328
c ---[  34]---> BDD-cost:  326
c ---[  33]---> BDD-cost:  361
c ---[  32]---> BDD-cost:  325
c ---[  31]---> BDD-cost:  321
c ---[  30]---> BDD-cost:  303
c ---[  29]---> BDD-cost:  316
c ---[  28]---> BDD-cost:  285
c ---[  27]---> BDD-cost:  365
c ---[  26]---> BDD-cost:  316
c ---[  25]---> BDD-cost:  320
c ---[  24]---> BDD-cost:  298
c ---[  23]---> BDD-cost:  326
c ---[  22]---> BDD-cost:  291
c ---[  21]---> BDD-cost:  351
c ---[  20]---> BDD-cost:  321
c ---[  19]---> BDD-cost:    5
c ---[  18]---> BDD-cost:  295
c ---[  17]---> BDD-cost:   12
c ---[  16]---> BDD-cost:  266
c ---[  15]---> BDD-cost:  325
c ---[  14]---> BDD-cost:  303
c ---[  13]---> BDD-cost:  340
c ---[  12]---> BDD-cost:  316
c ---[  11]---> BDD-cost:  288
c ---[  10]---> BDD-cost:  270
c ---[   9]---> BDD-cost:  316
c ---[   8]---> BDD-cost:  255
c ---[   7]---> BDD-cost:  361
c ---[   6]---> BDD-cost:  298
c ---[   5]---> BDD-cost:  321
c ---[   4]---> BDD-cost:  266
c ---[   3]---> BDD-cost:  303
c ---[   2]---> BDD-cost:  256
c ---[   1]---> BDD-cost:  356
c ---[   0]---> BDD-cost:  295
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  423454  1230550 |  141151       0        0     nan |  0.000 % |
c |       101 |  423454  1230550 |  155266     101     1825    18.1 |  1.088 % |
c |       251 |  423454  1230550 |  170792     251     3243    12.9 |  1.088 % |
c |       477 |  423434  1230510 |  187871     476    11728    24.6 |  1.094 % |
c |       815 |  423434  1230510 |  206659     814    42382    52.1 |  1.094 % |
c |      1322 |  423414  1230470 |  227325    1319    80154    60.8 |  1.100 % |
c |      2081 |  423414  1230470 |  250057    2078   102974    49.6 |  1.100 % |
c |      3222 |  423394  1230430 |  275063    3218   149575    46.5 |  1.106 % |
c |      4934 |  423394  1230430 |  302569    4930   393978    79.9 |  1.106 % |
c |      7496 |  423394  1230430 |  332826    7492   468185    62.5 |  1.106 % |
c |     11340 |  423374  1230390 |  366109   11335   806679    71.2 |  1.113 % |
c |     17106 |  423374  1230390 |  402720   17101  1557093    91.1 |  1.113 % |
c |     25755 |  423347  1230323 |  442992   25743  2754064   107.0 |  1.118 % |
c |     38729 |  423347  1230323 |  487291   38717  3432430    88.7 |  1.118 % |
c |     58191 |  423301  1230207 |  536020   58168  6257565   107.6 |  1.128 % |
c |     87383 |  423295  1230191 |  589622   87359  8798479   100.7 |  1.130 % |
c |    131172 |  423295  1230191 |  648585  131148 12793307    97.5 |  1.130 % |
c |    196856 |  423295  1230191 |  713443  196832 22712577   115.4 |  1.130 % |
c |    295383 |  423113  1229743 |  784787  295349 31712094   107.4 |  1.182 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.79 0.92 0.90 2/54 23836
Raw data (stat): 23836 (runsolver) R 23835 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487493164 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.82 0.93 0.90 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 13956 0 0 0 965 33 0 0 25 0 1 0 487493164 66617344 13562 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16264 13562 603 41 0 16223 0
vsize: 65056
[startup+20.0017 s]
Raw data (loadavg): 0.85 0.93 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 14649 0 0 0 1962 35 0 0 25 0 1 0 487493164 69435392 14255 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16952 14255 603 41 0 16911 0
vsize: 67808
[startup+30.0016 s]
Raw data (loadavg): 0.87 0.93 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 15396 0 0 0 2960 37 0 0 25 0 1 0 487493164 72605696 15002 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17726 15002 603 41 0 17685 0
vsize: 70904
[startup+40.0015 s]
Raw data (loadavg): 0.89 0.93 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 16154 0 0 0 3958 40 0 0 25 0 1 0 487493164 75698176 15760 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18481 15760 603 41 0 18440 0
vsize: 73924
[startup+50.0019 s]
Raw data (loadavg): 0.90 0.93 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 16714 0 0 0 4956 41 0 0 25 0 1 0 487493164 77987840 16320 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19040 16320 603 41 0 18999 0
vsize: 76160
[startup+60.0027 s]
Raw data (loadavg): 0.92 0.93 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 17145 0 0 0 5955 43 0 0 25 0 1 0 487493164 79831040 16751 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19490 16751 603 41 0 19449 0
vsize: 77960
[startup+70.0027 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 17966 0 0 0 6953 45 0 0 25 0 1 0 487493164 83185664 17572 4294967295 134512640 134672761 3221224544 3221223648 134559941 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20309 17572 603 41 0 20268 0
vsize: 81236
[startup+80.0022 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 18769 0 0 0 7951 47 0 0 25 0 1 0 487493164 86405120 18375 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21095 18375 603 41 0 21054 0
vsize: 84380
[startup+90.0019 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 19074 0 0 0 8950 48 0 0 25 0 1 0 487493164 87732224 18680 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21419 18680 603 41 0 21378 0
vsize: 85676
[startup+100.002 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 19678 0 0 0 9949 50 0 0 25 0 1 0 487493164 90152960 19284 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22010 19284 603 41 0 21969 0
vsize: 88040
[startup+110.002 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 20435 0 0 0 10947 51 0 0 25 0 1 0 487493164 93229056 20041 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22761 20041 603 41 0 22720 0
vsize: 91044
[startup+120.002 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 20901 0 0 0 11946 53 0 0 25 0 1 0 487493164 95375360 20507 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23285 20507 603 41 0 23244 0
vsize: 93140
[startup+130.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 21372 0 0 0 12945 54 0 0 25 0 1 0 487493164 97255424 20978 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23744 20978 603 41 0 23703 0
vsize: 94976
[startup+140.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 21804 0 0 0 13944 55 0 0 25 0 1 0 487493164 99008512 21410 4294967295 134512640 134672761 3221224544 3221223696 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24172 21410 603 41 0 24131 0
vsize: 96688
[startup+150.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 22325 0 0 0 14943 56 0 0 25 0 1 0 487493164 101150720 21931 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24695 21931 603 41 0 24654 0
vsize: 98780
[startup+160.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 22863 0 0 0 15941 58 0 0 25 0 1 0 487493164 103268352 22469 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25212 22469 603 41 0 25171 0
vsize: 100848
[startup+170.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 23421 0 0 0 16940 60 0 0 25 0 1 0 487493164 105537536 23027 4294967295 134512640 134672761 3221224544 3221223680 134565127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25766 23027 603 41 0 25725 0
vsize: 103064
[startup+180.003 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 23951 0 0 0 17938 61 0 0 25 0 1 0 487493164 107671552 23557 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26287 23557 603 41 0 26246 0
vsize: 105148
[startup+190.003 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 24444 0 0 0 18937 62 0 0 25 0 1 0 487493164 109690880 24050 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26780 24050 603 41 0 26739 0
vsize: 107120
[startup+200.003 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 24916 0 0 0 19937 62 0 0 25 0 1 0 487493164 111755264 24522 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27284 24522 603 41 0 27243 0
vsize: 109136
[startup+210.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 25361 0 0 0 20936 63 0 0 25 0 1 0 487493164 113516544 24967 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27714 24967 603 41 0 27673 0
vsize: 110856
[startup+220.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 25744 0 0 0 21935 64 0 0 25 0 1 0 487493164 115015680 25350 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28080 25350 603 41 0 28039 0
vsize: 112320
[startup+230.003 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 26132 0 0 0 22934 65 0 0 25 0 1 0 487493164 116764672 25738 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28507 25738 603 41 0 28466 0
vsize: 114028
[startup+240.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 26515 0 0 0 23933 67 0 0 25 0 1 0 487493164 118259712 26121 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28872 26121 603 41 0 28831 0
vsize: 115488
[startup+250.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 26873 0 0 0 24932 68 0 0 25 0 1 0 487493164 119767040 26479 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29240 26479 603 41 0 29199 0
vsize: 116960
[startup+260.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 27259 0 0 0 25931 69 0 0 25 0 1 0 487493164 121384960 26865 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29635 26865 603 41 0 29594 0
vsize: 118540
[startup+270.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 27592 0 0 0 26931 69 0 0 25 0 1 0 487493164 122728448 27198 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29963 27198 603 41 0 29922 0
vsize: 119852
[startup+280.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 27970 0 0 0 27929 71 0 0 25 0 1 0 487493164 124735488 27576 4294967295 134512640 134672761 3221224544 3221223720 134559668 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30453 27576 603 41 0 30412 0
vsize: 121812
[startup+290.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 28547 0 0 0 28928 73 0 0 25 0 1 0 487493164 127160320 28153 4294967295 134512640 134672761 3221224544 3221223648 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31045 28153 603 41 0 31004 0
vsize: 124180
[startup+300.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 29132 0 0 0 29927 74 0 0 25 0 1 0 487493164 129441792 28738 4294967295 134512640 134672761 3221224544 3221223712 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31602 28738 603 41 0 31561 0
vsize: 126408
[startup+310.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 29807 0 0 0 30925 75 0 0 25 0 1 0 487493164 132272128 29413 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32293 29413 603 41 0 32252 0
vsize: 129172
[startup+320.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 30407 0 0 0 31924 77 0 0 25 0 1 0 487493164 134701056 30013 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32886 30013 603 41 0 32845 0
vsize: 131544
[startup+330.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 30960 0 0 0 32923 78 0 0 25 0 1 0 487493164 136990720 30566 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33445 30566 603 41 0 33404 0
vsize: 133780
[startup+340.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 31472 0 0 0 33922 80 0 0 25 0 1 0 487493164 139001856 31078 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33936 31078 603 41 0 33895 0
vsize: 135744
[startup+350.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 31960 0 0 0 34920 81 0 0 25 0 1 0 487493164 141029376 31566 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34431 31566 603 41 0 34390 0
vsize: 137724
[startup+360.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 32420 0 0 0 35920 82 0 0 25 0 1 0 487493164 142983168 32026 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34908 32026 603 41 0 34867 0
vsize: 139632
[startup+370.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 32858 0 0 0 36919 83 0 0 25 0 1 0 487493164 144723968 32464 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35333 32464 603 41 0 35292 0
vsize: 141332
[startup+380.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 33291 0 0 0 37917 84 0 0 25 0 1 0 487493164 146472960 32897 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35760 32897 603 41 0 35719 0
vsize: 143040
[startup+390.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 33705 0 0 0 38917 85 0 0 25 0 1 0 487493164 148279296 33311 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36201 33311 603 41 0 36160 0
vsize: 144804
[startup+400.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 34123 0 0 0 39919 86 0 0 25 0 1 0 487493164 149897216 33729 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36596 33729 603 41 0 36555 0
vsize: 146384
[startup+410.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 34525 0 0 0 40918 87 0 0 25 0 1 0 487493164 151642112 34131 4294967295 134512640 134672761 3221224544 3221223696 134565101 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37022 34131 603 41 0 36981 0
vsize: 148088
[startup+420.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 34943 0 0 0 41917 88 0 0 25 0 1 0 487493164 153268224 34549 4294967295 134512640 134672761 3221224544 3221223648 134555175 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37419 34549 603 41 0 37378 0
vsize: 149676
[startup+430.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 35347 0 0 0 42916 89 0 0 25 0 1 0 487493164 155013120 34953 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37845 34953 603 41 0 37804 0
vsize: 151380
[startup+440.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 35764 0 0 0 43916 90 0 0 25 0 1 0 487493164 156626944 35370 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38239 35370 603 41 0 38198 0
vsize: 152956
[startup+450.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 36269 0 0 0 44915 91 0 0 25 0 1 0 487493164 158785536 35875 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38766 35875 603 41 0 38725 0
vsize: 155064
[startup+460.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 36735 0 0 0 45914 92 0 0 25 0 1 0 487493164 160677888 36341 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39228 36341 603 41 0 39187 0
vsize: 156912
[startup+470.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 37205 0 0 0 46913 94 0 0 25 0 1 0 487493164 162553856 36811 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39686 36811 603 41 0 39645 0
vsize: 158744
[startup+480.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 37648 0 0 0 47911 95 0 0 25 0 1 0 487493164 164433920 37254 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40145 37254 603 41 0 40104 0
vsize: 160580
[startup+490.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 38094 0 0 0 48911 96 0 0 25 0 1 0 487493164 166182912 37700 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40572 37700 603 41 0 40531 0
vsize: 162288
[startup+500.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 38668 0 0 0 49908 98 0 0 25 0 1 0 487493164 168476672 38274 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41132 38274 603 41 0 41091 0
vsize: 164528
[startup+510.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 39382 0 0 0 50907 100 0 0 25 0 1 0 487493164 171442176 38988 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41856 38988 603 41 0 41815 0
vsize: 167424
[startup+520.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 39746 0 0 0 51906 101 0 0 25 0 1 0 487493164 172920832 39352 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42217 39352 603 41 0 42176 0
vsize: 168868
[startup+530.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 40296 0 0 0 52905 102 0 0 25 0 1 0 487493164 175202304 39902 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42774 39902 603 41 0 42733 0
vsize: 171096
[startup+540.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 40846 0 0 0 53904 103 0 0 25 0 1 0 487493164 177344512 40452 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43297 40452 603 41 0 43256 0
vsize: 173188
[startup+550.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 41321 0 0 0 54902 105 0 0 25 0 1 0 487493164 179363840 40927 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43790 40927 603 41 0 43749 0
vsize: 175160
[startup+560.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 41770 0 0 0 55902 106 0 0 25 0 1 0 487493164 181243904 41376 4294967295 134512640 134672761 3221224544 3221223648 134559896 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44249 41376 603 41 0 44208 0
vsize: 176996
[startup+570.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 42166 0 0 0 56900 107 0 0 25 0 1 0 487493164 182849536 41772 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44641 41772 603 41 0 44600 0
vsize: 178564
[startup+580.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 42516 0 0 0 57899 109 0 0 25 0 1 0 487493164 184217600 42122 4294967295 134512640 134672761 3221224544 3221223712 134560970 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44975 42122 603 41 0 44934 0
vsize: 179900
[startup+590.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 42822 0 0 0 58898 110 0 0 25 0 1 0 487493164 185434112 42428 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45272 42428 603 41 0 45231 0
vsize: 181088
[startup+600.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 43122 0 0 0 59898 110 0 0 25 0 1 0 487493164 186646528 42728 4294967295 134512640 134672761 3221224544 3221223712 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45568 42728 603 41 0 45527 0
vsize: 182272
[startup+610.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 43438 0 0 0 60898 111 0 0 25 0 1 0 487493164 188022784 43044 4294967295 134512640 134672761 3221224544 3221223728 134559463 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45904 43044 603 41 0 45863 0
vsize: 183616
[startup+620.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 43751 0 0 0 61897 112 0 0 25 0 1 0 487493164 189313024 43357 4294967295 134512640 134672761 3221224544 3221223712 134561027 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46219 43357 603 41 0 46178 0
vsize: 184876
[startup+630.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 44061 0 0 0 62896 112 0 0 25 0 1 0 487493164 190644224 43667 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46544 43667 603 41 0 46503 0
vsize: 186176
[startup+640.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 44331 0 0 0 63896 113 0 0 25 0 1 0 487493164 192765952 43937 4294967295 134512640 134672761 3221224544 3221223680 134560647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47062 43937 603 41 0 47021 0
vsize: 188248
[startup+650.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 44607 0 0 0 64896 113 0 0 25 0 1 0 487493164 193839104 44213 4294967295 134512640 134672761 3221224544 3221223728 134559622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47324 44213 603 41 0 47283 0
vsize: 189296
[startup+660.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 44923 0 0 0 65895 114 0 0 25 0 1 0 487493164 195215360 44529 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47660 44529 603 41 0 47619 0
vsize: 190640
[startup+670.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 45216 0 0 0 66895 115 0 0 25 0 1 0 487493164 196431872 44822 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47957 44822 603 41 0 47916 0
vsize: 191828
[startup+680.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 45524 0 0 0 67894 116 0 0 25 0 1 0 487493164 197640192 45130 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48252 45130 603 41 0 48211 0
vsize: 193008
[startup+690.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 45861 0 0 0 68893 117 0 0 25 0 1 0 487493164 198975488 45467 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48578 45467 603 41 0 48537 0
vsize: 194312
[startup+700.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 46165 0 0 0 69893 117 0 0 25 0 1 0 487493164 200183808 45771 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48873 45771 603 41 0 48832 0
vsize: 195492
[startup+710.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 46464 0 0 0 70893 118 0 0 25 0 1 0 487493164 201388032 46070 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49167 46070 603 41 0 49126 0
vsize: 196668
[startup+720.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 46774 0 0 0 71892 118 0 0 25 0 1 0 487493164 202727424 46380 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49494 46380 603 41 0 49453 0
vsize: 197976
[startup+730.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 47082 0 0 0 72892 119 0 0 25 0 1 0 487493164 203964416 46688 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49796 46688 603 41 0 49755 0
vsize: 199184
[startup+740.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 47376 0 0 0 73891 120 0 0 25 0 1 0 487493164 205213696 46982 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50101 46982 603 41 0 50060 0
vsize: 200404
[startup+750.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 47669 0 0 0 74890 121 0 0 25 0 1 0 487493164 206422016 47275 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50396 47275 603 41 0 50355 0
vsize: 201584
[startup+760.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 47930 0 0 0 75890 121 0 0 25 0 1 0 487493164 207486976 47536 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50656 47536 603 41 0 50615 0
vsize: 202624
[startup+770.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 48239 0 0 0 76889 122 0 0 25 0 1 0 487493164 208695296 47845 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50951 47845 603 41 0 50910 0
vsize: 203804
[startup+780.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 48812 0 0 0 77888 124 0 0 25 0 1 0 487493164 211099648 48418 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51538 48418 603 41 0 51497 0
vsize: 206152
[startup+790.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 49375 0 0 0 78886 125 0 0 25 0 1 0 487493164 213377024 48981 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52094 48981 603 41 0 52053 0
vsize: 208376
[startup+800.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 50038 0 0 0 79885 127 0 0 25 0 1 0 487493164 216084480 49644 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52755 49644 603 41 0 52714 0
vsize: 211020
[startup+810.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 50619 0 0 0 80884 128 0 0 25 0 1 0 487493164 218374144 50225 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53314 50225 603 41 0 53273 0
vsize: 213256
[startup+820.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 51152 0 0 0 81882 130 0 0 25 0 1 0 487493164 220667904 50758 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53874 50758 603 41 0 53833 0
vsize: 215496
[startup+830.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 51653 0 0 0 82881 132 0 0 25 0 1 0 487493164 222683136 51259 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54366 51259 603 41 0 54325 0
vsize: 217464
[startup+840.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 52075 0 0 0 83880 133 0 0 25 0 1 0 487493164 224428032 51681 4294967295 134512640 134672761 3221224544 3221223648 134560344 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54792 51681 603 41 0 54751 0
vsize: 219168
[startup+850.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 52462 0 0 0 84879 134 0 0 25 0 1 0 487493164 225894400 52068 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55150 52068 603 41 0 55109 0
vsize: 220600
[startup+860.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 52916 0 0 0 85878 135 0 0 25 0 1 0 487493164 227794944 52522 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55614 52522 603 41 0 55573 0
vsize: 222456
[startup+870.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 53400 0 0 0 86877 136 0 0 25 0 1 0 487493164 229793792 53006 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56102 53006 603 41 0 56061 0
vsize: 224408
[startup+880.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 53817 0 0 0 87876 138 0 0 25 0 1 0 487493164 231542784 53423 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56529 53423 603 41 0 56488 0
vsize: 226116
[startup+890.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 54255 0 0 0 88875 139 0 0 25 0 1 0 487493164 233279488 53861 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56953 53861 603 41 0 56912 0
vsize: 227812
[startup+900.043 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 54688 0 0 0 89875 139 0 0 25 0 1 0 487493164 235020288 54294 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57378 54294 603 41 0 57337 0
vsize: 229512
[startup+910.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 55050 0 0 0 90873 141 0 0 25 0 1 0 487493164 236478464 54656 4294967295 134512640 134672761 3221224544 3221223648 134560198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57734 54656 603 41 0 57693 0
vsize: 230936
[startup+920.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 55434 0 0 0 91872 142 0 0 25 0 1 0 487493164 238096384 55040 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58129 55040 603 41 0 58088 0
vsize: 232516
[startup+930.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 55788 0 0 0 92871 143 0 0 25 0 1 0 487493164 239562752 55394 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58487 55394 603 41 0 58446 0
vsize: 233948
[startup+940.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 56120 0 0 0 93871 144 0 0 25 0 1 0 487493164 240893952 55726 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58812 55726 603 41 0 58771 0
vsize: 235248
[startup+950.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 56434 0 0 0 94870 145 0 0 25 0 1 0 487493164 242225152 56040 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59137 56040 603 41 0 59096 0
vsize: 236548
[startup+960.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 56756 0 0 0 95869 146 0 0 25 0 1 0 487493164 243421184 56362 4294967295 134512640 134672761 3221224544 3221223744 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59429 56362 603 41 0 59388 0
vsize: 237716
[startup+970.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 57079 0 0 0 96869 147 0 0 25 0 1 0 487493164 244776960 56685 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59760 56685 603 41 0 59719 0
vsize: 239040
[startup+980.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 57460 0 0 0 97867 148 0 0 25 0 1 0 487493164 246394880 57066 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60155 57066 603 41 0 60114 0
vsize: 240620
[startup+990.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 57845 0 0 0 98867 149 0 0 25 0 1 0 487493164 247869440 57451 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60515 57451 603 41 0 60474 0
vsize: 242060
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 58222 0 0 0 99866 150 0 0 25 0 1 0 487493164 249487360 57828 4294967295 134512640 134672761 3221224544 3221223728 134559182 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60910 57828 603 41 0 60869 0
vsize: 243640
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 58580 0 0 0 100864 152 0 0 25 0 1 0 487493164 250970112 58186 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61272 58186 603 41 0 61231 0
vsize: 245088
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 58953 0 0 0 101864 152 0 0 25 0 1 0 487493164 252448768 58559 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61633 58559 603 41 0 61592 0
vsize: 246532
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 59337 0 0 0 102863 153 0 0 25 0 1 0 487493164 254046208 58943 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62023 58943 603 41 0 61982 0
vsize: 248092
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 59707 0 0 0 103862 154 0 0 25 0 1 0 487493164 255520768 59313 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62383 59313 603 41 0 62342 0
vsize: 249532
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 60058 0 0 0 104862 155 0 0 25 0 1 0 487493164 257011712 59664 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62747 59664 603 41 0 62706 0
vsize: 250988
[startup+1060.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 60397 0 0 0 105861 156 0 0 25 0 1 0 487493164 258383872 60003 4294967295 134512640 134672761 3221224544 3221223648 134560344 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63082 60003 603 41 0 63041 0
vsize: 252328
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 60732 0 0 0 106861 157 0 0 25 0 1 0 487493164 259727360 60338 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63410 60338 603 41 0 63369 0
vsize: 253640
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 61078 0 0 0 107860 157 0 0 25 0 1 0 487493164 261201920 60684 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63770 60684 603 41 0 63729 0
vsize: 255080
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 61453 0 0 0 108859 159 0 0 25 0 1 0 487493164 262684672 61059 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64132 61059 603 41 0 64091 0
vsize: 256528
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 61803 0 0 0 109858 160 0 0 25 0 1 0 487493164 264167424 61409 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64494 61409 603 41 0 64453 0
vsize: 257976
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 62130 0 0 0 110858 160 0 0 25 0 1 0 487493164 265424896 61736 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64801 61736 603 41 0 64760 0
vsize: 259204
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 62451 0 0 0 111857 161 0 0 25 0 1 0 487493164 266768384 62057 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65129 62057 603 41 0 65088 0
vsize: 260516
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 62782 0 0 0 112857 162 0 0 25 0 1 0 487493164 268115968 62388 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65458 62388 603 41 0 65417 0
vsize: 261832
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 63091 0 0 0 113856 163 0 0 25 0 1 0 487493164 269320192 62697 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65752 62697 603 41 0 65711 0
vsize: 263008
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 63388 0 0 0 114855 163 0 0 25 0 1 0 487493164 270536704 62994 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66049 62995 603 41 0 66008 0
vsize: 264196
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 63683 0 0 0 115855 164 0 0 25 0 1 0 487493164 271749120 63289 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66345 63289 603 41 0 66304 0
vsize: 265380
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 63999 0 0 0 116855 165 0 0 25 0 1 0 487493164 273092608 63605 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66673 63605 603 41 0 66632 0
vsize: 266692
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 64304 0 0 0 117854 165 0 0 25 0 1 0 487493164 274317312 63910 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66972 63910 603 41 0 66931 0
vsize: 267888
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 64602 0 0 0 118854 166 0 0 25 0 1 0 487493164 275529728 64208 4294967295 134512640 134672761 3221224544 3221223648 134560215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67268 64208 603 41 0 67227 0
vsize: 269072
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23836
Raw data (stat): 23836 (minisat+) R 23835 24215 24214 0 -1 0 64885 0 0 0 119854 166 0 0 25 0 1 0 487493164 276754432 64491 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67567 64491 603 41 0 67526 0
vsize: 270268
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.17 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 23836
Raw data (stat): 23836 (minisat+) Z 23835 24215 24214 0 -1 12 64887 0 0 0 119854 178 0 0 25 0 1 0 487493164 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.17
CPU time (s): 1200.33
CPU user time (s): 1198.55
CPU system time (s): 1.78373
CPU usage (%): 100.013
Max. virtual memory (Kb): 270268
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####