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/miplib/normalized-mps-v2-13-7-dcmulti.opb
MD5SUM6ffc4ed72f4dd993b121ae0a2045731e
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.087986
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 19274 

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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:        779968 kB
Buffers:         30420 kB
Cached:         199984 kB
SwapCached:        524 kB
Active:          87516 kB
Inactive:       144908 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        779716 kB
SwapTotal:     2097892 kB
SwapFree:      2096476 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5108 kB
Slab:            16672 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 18:56:10 (client local time) WITH STATUS 0 IN 1200.3 SECONDS
stats: 16769 7 1200.3 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.80 0.94 0.90 2/54 14060
Raw data (stat): 14060 (runsolver) R 14059 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 547284132 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.83 0.94 0.90 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 13931 0 0 0 964 34 0 0 25 0 1 0 547284132 66486272 13537 4294967295 134512640 134672761 3221224528 3221223664 134565080 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16232 13537 603 41 0 16191 0
vsize: 64928
[startup+20.0015 s]
Raw data (loadavg): 0.86 0.94 0.90 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 14619 0 0 0 1962 36 0 0 25 0 1 0 547284132 69300224 14225 4294967295 134512640 134672761 3221224528 3221223632 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16919 14225 603 41 0 16878 0
vsize: 67676
[startup+30.0022 s]
Raw data (loadavg): 0.88 0.94 0.90 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 15366 0 0 0 2959 39 0 0 25 0 1 0 547284132 72470528 14972 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17693 14972 603 41 0 17652 0
vsize: 70772
[startup+40.0019 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 16076 0 0 0 3957 42 0 0 25 0 1 0 547284132 75296768 15682 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18383 15682 603 41 0 18342 0
vsize: 73532
[startup+50.0022 s]
Raw data (loadavg): 0.91 0.95 0.90 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 16673 0 0 0 4954 45 0 0 25 0 1 0 547284132 77717504 16279 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18974 16279 603 41 0 18933 0
vsize: 75896
[startup+60.0023 s]
Raw data (loadavg): 0.92 0.95 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 17058 0 0 0 5952 46 0 0 25 0 1 0 547284132 79433728 16664 4294967295 134512640 134672761 3221224528 3221223696 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19393 16664 603 41 0 19352 0
vsize: 77572
[startup+70.003 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 17746 0 0 0 6950 48 0 0 25 0 1 0 547284132 82239488 17352 4294967295 134512640 134672761 3221224528 3221223632 134560231 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20078 17352 603 41 0 20037 0
vsize: 80312
[startup+80.0037 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 18726 0 0 0 7948 51 0 0 25 0 1 0 547284132 86269952 18332 4294967295 134512640 134672761 3221224528 3221223696 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21062 18332 603 41 0 21021 0
vsize: 84248
[startup+90.0044 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 18997 0 0 0 8947 52 0 0 25 0 1 0 547284132 87326720 18603 4294967295 134512640 134672761 3221224528 3221223696 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21320 18603 603 41 0 21279 0
vsize: 85280
[startup+100.005 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 19426 0 0 0 9945 54 0 0 25 0 1 0 547284132 89079808 19032 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21748 19032 603 41 0 21707 0
vsize: 86992
[startup+110.006 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 20213 0 0 0 10942 57 0 0 25 0 1 0 547284132 92295168 19819 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22533 19819 603 41 0 22492 0
vsize: 90132
[startup+120.007 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 20749 0 0 0 11940 59 0 0 25 0 1 0 547284132 94707712 20355 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23122 20355 603 41 0 23081 0
vsize: 92488
[startup+130.007 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 21189 0 0 0 12938 61 0 0 25 0 1 0 547284132 96448512 20795 4294967295 134512640 134672761 3221224528 3221223696 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23547 20795 603 41 0 23506 0
vsize: 94188
[startup+140.008 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 21621 0 0 0 13937 63 0 0 25 0 1 0 547284132 98201600 21227 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23975 21227 603 41 0 23934 0
vsize: 95900
[startup+150.01 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 22056 0 0 0 14935 65 0 0 25 0 1 0 547284132 100077568 21662 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24433 21662 603 41 0 24392 0
vsize: 97732
[startup+160.01 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 22599 0 0 0 15934 66 0 0 25 0 1 0 547284132 102207488 22205 4294967295 134512640 134672761 3221224528 3221223712 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24953 22205 603 41 0 24912 0
vsize: 99812
[startup+170.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 23097 0 0 0 16932 68 0 0 25 0 1 0 547284132 104337408 22703 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25473 22703 603 41 0 25432 0
vsize: 101892
[startup+180.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 23644 0 0 0 17930 71 0 0 25 0 1 0 547284132 106471424 23250 4294967295 134512640 134672761 3221224528 3221223696 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25994 23250 603 41 0 25953 0
vsize: 103976
[startup+190.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 24139 0 0 0 18928 73 0 0 25 0 1 0 547284132 108482560 23745 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26485 23745 603 41 0 26444 0
vsize: 105940
[startup+200.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 24588 0 0 0 19927 74 0 0 25 0 1 0 547284132 110374912 24194 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26947 24194 603 41 0 26906 0
vsize: 107788
[startup+210.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 25035 0 0 0 20925 76 0 0 25 0 1 0 547284132 112164864 24641 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27384 24641 603 41 0 27343 0
vsize: 109536
[startup+220.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 25458 0 0 0 21924 77 0 0 25 0 1 0 547284132 113934336 25064 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27816 25064 603 41 0 27775 0
vsize: 111264
[startup+230.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 25832 0 0 0 22922 79 0 0 25 0 1 0 547284132 115417088 25438 4294967295 134512640 134672761 3221224528 3221223696 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28178 25438 603 41 0 28137 0
vsize: 112712
[startup+240.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 26202 0 0 0 23920 81 0 0 25 0 1 0 547284132 117035008 25808 4294967295 134512640 134672761 3221224528 3221223696 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28573 25808 603 41 0 28532 0
vsize: 114292
[startup+250.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 26558 0 0 0 24919 82 0 0 25 0 1 0 547284132 118530048 26164 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28938 26164 603 41 0 28897 0
vsize: 115752
[startup+260.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 26909 0 0 0 25918 84 0 0 25 0 1 0 547284132 119902208 26515 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29273 26515 603 41 0 29232 0
vsize: 117092
[startup+270.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 27273 0 0 0 26917 85 0 0 25 0 1 0 547284132 121384960 26879 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29635 26879 603 41 0 29594 0
vsize: 118540
[startup+280.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 27592 0 0 0 27915 86 0 0 25 0 1 0 547284132 122728448 27198 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29963 27198 603 41 0 29922 0
vsize: 119852
[startup+290.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 27951 0 0 0 28914 87 0 0 25 0 1 0 547284132 124735488 27557 4294967295 134512640 134672761 3221224528 3221223712 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30453 27557 603 41 0 30412 0
vsize: 121812
[startup+300.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 28499 0 0 0 29912 89 0 0 25 0 1 0 547284132 126889984 28105 4294967295 134512640 134672761 3221224528 3221223696 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30979 28105 603 41 0 30938 0
vsize: 123916
[startup+310.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 29052 0 0 0 30911 91 0 0 25 0 1 0 547284132 129175552 28658 4294967295 134512640 134672761 3221224528 3221223632 134560148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31537 28658 603 41 0 31496 0
vsize: 126148
[startup+320.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 29702 0 0 0 31909 93 0 0 25 0 1 0 547284132 131870720 29308 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32195 29308 603 41 0 32154 0
vsize: 128780
[startup+330.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 30309 0 0 0 32907 95 0 0 25 0 1 0 547284132 134295552 29915 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32787 29915 603 41 0 32746 0
vsize: 131148
[startup+340.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 30844 0 0 0 33906 96 0 0 25 0 1 0 547284132 136454144 30450 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33314 30450 603 41 0 33273 0
vsize: 133256
[startup+350.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 31358 0 0 0 34904 98 0 0 25 0 1 0 547284132 138596352 30964 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33837 30964 603 41 0 33796 0
vsize: 135348
[startup+360.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 31835 0 0 0 35903 99 0 0 25 0 1 0 547284132 140480512 31441 4294967295 134512640 134672761 3221224528 3221223632 134560276 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34297 31441 603 41 0 34256 0
vsize: 137188
[startup+370.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 32294 0 0 0 36902 100 0 0 25 0 1 0 547284132 142393344 31900 4294967295 134512640 134672761 3221224528 3221223696 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34764 31900 603 41 0 34723 0
vsize: 139056
[startup+380.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 32724 0 0 0 37901 102 0 0 25 0 1 0 547284132 144187392 32330 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35202 32330 603 41 0 35161 0
vsize: 140808
[startup+390.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 33138 0 0 0 38900 103 0 0 25 0 1 0 547284132 145797120 32744 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35595 32744 603 41 0 35554 0
vsize: 142380
[startup+400.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 33548 0 0 0 39898 105 0 0 25 0 1 0 547284132 147554304 33154 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36024 33154 603 41 0 35983 0
vsize: 144096
[startup+410.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 33952 0 0 0 40897 106 0 0 25 0 1 0 547284132 149213184 33558 4294967295 134512640 134672761 3221224528 3221223632 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36429 33558 603 41 0 36388 0
vsize: 145716
[startup+420.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 34347 0 0 0 41897 107 0 0 25 0 1 0 547284132 150839296 33953 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36826 33953 603 41 0 36785 0
vsize: 147304
[startup+430.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 34752 0 0 0 42896 108 0 0 25 0 1 0 547284132 152576000 34358 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37250 34358 603 41 0 37209 0
vsize: 149000
[startup+440.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 35149 0 0 0 43894 110 0 0 25 0 1 0 547284132 154210304 34755 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37649 34755 603 41 0 37608 0
vsize: 150596
[startup+450.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 35544 0 0 0 44893 111 0 0 25 0 1 0 547284132 155820032 35150 4294967295 134512640 134672761 3221224528 3221223696 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38042 35150 603 41 0 38001 0
vsize: 152168
[startup+460.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 35959 0 0 0 45892 113 0 0 25 0 1 0 547284132 157433856 35565 4294967295 134512640 134672761 3221224528 3221223680 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38436 35565 603 41 0 38395 0
vsize: 153744
[startup+470.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 36456 0 0 0 46891 114 0 0 25 0 1 0 547284132 159465472 36062 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38932 36062 603 41 0 38891 0
vsize: 155728
[startup+480.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 36929 0 0 0 47890 115 0 0 25 0 1 0 547284132 161480704 36535 4294967295 134512640 134672761 3221224528 3221223696 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39424 36535 603 41 0 39383 0
vsize: 157696
[startup+490.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 37363 0 0 0 48890 115 0 0 25 0 1 0 547284132 163225600 36969 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39850 36969 603 41 0 39809 0
vsize: 159400
[startup+500.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 37788 0 0 0 49889 116 0 0 25 0 1 0 547284132 164970496 37394 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40276 37394 603 41 0 40235 0
vsize: 161104
[startup+510.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 38215 0 0 0 50888 117 0 0 25 0 1 0 547284132 166719488 37821 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40703 37821 603 41 0 40662 0
vsize: 162812
[startup+520.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 38892 0 0 0 51886 119 0 0 25 0 1 0 547284132 169422848 38498 4294967295 134512640 134672761 3221224528 3221223696 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41363 38498 603 41 0 41322 0
vsize: 165452
[startup+530.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 39543 0 0 0 52884 121 0 0 25 0 1 0 547284132 172113920 39149 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42020 39149 603 41 0 41979 0
vsize: 168080
[startup+540.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 39820 0 0 0 53883 123 0 0 25 0 1 0 547284132 173191168 39426 4294967295 134512640 134672761 3221224528 3221223676 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42283 39426 603 41 0 42242 0
vsize: 169132
[startup+550.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 40417 0 0 0 54881 125 0 0 25 0 1 0 547284132 175599616 40023 4294967295 134512640 134672761 3221224528 3221223696 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42871 40023 603 41 0 42830 0
vsize: 171484
[startup+560.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 40944 0 0 0 55880 126 0 0 25 0 1 0 547284132 177762304 40550 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43399 40550 603 41 0 43358 0
vsize: 173596
[startup+570.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 41393 0 0 0 56879 127 0 0 25 0 1 0 547284132 179634176 40999 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43856 40999 603 41 0 43815 0
vsize: 175424
[startup+580.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 41826 0 0 0 57877 129 0 0 25 0 1 0 547284132 181374976 41432 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44281 41432 603 41 0 44240 0
vsize: 177124
[startup+590.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 42200 0 0 0 58877 130 0 0 25 0 1 0 547284132 182984704 41806 4294967295 134512640 134672761 3221224528 3221223696 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44674 41806 603 41 0 44633 0
vsize: 178696
[startup+600.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 42532 0 0 0 59876 131 0 0 25 0 1 0 547284132 184352768 42138 4294967295 134512640 134672761 3221224528 3221223652 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45008 42138 603 41 0 44967 0
vsize: 180032
[startup+610.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 42829 0 0 0 60875 132 0 0 25 0 1 0 547284132 185569280 42435 4294967295 134512640 134672761 3221224528 3221223696 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45305 42435 603 41 0 45264 0
vsize: 181220
[startup+620.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 43120 0 0 0 61874 133 0 0 25 0 1 0 547284132 186646528 42726 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45568 42726 603 41 0 45527 0
vsize: 182272
[startup+630.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 43426 0 0 0 62873 134 0 0 25 0 1 0 547284132 187887616 43032 4294967295 134512640 134672761 3221224528 3221223696 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45871 43032 603 41 0 45830 0
vsize: 183484
[startup+640.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 43724 0 0 0 63872 135 0 0 25 0 1 0 547284132 189177856 43330 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46186 43330 603 41 0 46145 0
vsize: 184744
[startup+650.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 44029 0 0 0 64871 137 0 0 25 0 1 0 547284132 190509056 43635 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46511 43635 603 41 0 46470 0
vsize: 186044
[startup+660.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 44289 0 0 0 65871 137 0 0 25 0 1 0 547284132 192630784 43895 4294967295 134512640 134672761 3221224528 3221223696 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47029 43895 603 41 0 46988 0
vsize: 188116
[startup+670.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 44554 0 0 0 66870 138 0 0 25 0 1 0 547284132 193703936 44160 4294967295 134512640 134672761 3221224528 3221223696 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47291 44160 603 41 0 47250 0
vsize: 189164
[startup+680.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 44856 0 0 0 67869 139 0 0 25 0 1 0 547284132 194945024 44462 4294967295 134512640 134672761 3221224528 3221223696 134560979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47594 44462 603 41 0 47553 0
vsize: 190376
[startup+690.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 45129 0 0 0 68869 140 0 0 25 0 1 0 547284132 196026368 44735 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47858 44736 603 41 0 47817 0
vsize: 191432
[startup+700.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 45426 0 0 0 69868 141 0 0 25 0 1 0 547284132 197234688 45032 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48153 45032 603 41 0 48112 0
vsize: 192612
[startup+710.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 45747 0 0 0 70867 142 0 0 25 0 1 0 547284132 198578176 45353 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48481 45353 603 41 0 48440 0
vsize: 193924
[startup+720.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 46042 0 0 0 71867 143 0 0 25 0 1 0 547284132 199778304 45648 4294967295 134512640 134672761 3221224528 3221223632 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48774 45648 603 41 0 48733 0
vsize: 195096
[startup+730.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 46336 0 0 0 72866 144 0 0 25 0 1 0 547284132 200986624 45942 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49069 45942 603 41 0 49028 0
vsize: 196276
[startup+740.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 46627 0 0 0 73865 144 0 0 25 0 1 0 547284132 202055680 46233 4294967295 134512640 134672761 3221224528 3221223600 134553549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49330 46233 603 41 0 49289 0
vsize: 197320
[startup+750.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 46921 0 0 0 74865 145 0 0 25 0 1 0 547284132 203288576 46527 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49631 46527 603 41 0 49590 0
vsize: 198524
[startup+760.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 47211 0 0 0 75864 146 0 0 25 0 1 0 547284132 204505088 46817 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49928 46817 603 41 0 49887 0
vsize: 199712
[startup+770.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 47491 0 0 0 76864 147 0 0 25 0 1 0 547284132 205615104 47097 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50199 47097 603 41 0 50158 0
vsize: 200796
[startup+780.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 47773 0 0 0 77863 148 0 0 25 0 1 0 547284132 206819328 47379 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50493 47379 603 41 0 50452 0
vsize: 201972
[startup+790.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 48015 0 0 0 78863 148 0 0 25 0 1 0 547284132 207888384 47621 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50754 47621 603 41 0 50713 0
vsize: 203016
[startup+800.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 48416 0 0 0 79861 149 0 0 25 0 1 0 547284132 209498112 48022 4294967295 134512640 134672761 3221224528 3221223632 134559979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51147 48022 603 41 0 51106 0
vsize: 204588
[startup+810.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 48962 0 0 0 80859 151 0 0 25 0 1 0 547284132 211636224 48568 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51669 48568 603 41 0 51628 0
vsize: 206676
[startup+820.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 49538 0 0 0 81858 153 0 0 25 0 1 0 547284132 214052864 49144 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52259 49144 603 41 0 52218 0
vsize: 209036
[startup+830.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 50172 0 0 0 82856 154 0 0 25 0 1 0 547284132 216621056 49778 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52886 49778 603 41 0 52845 0
vsize: 211544
[startup+840.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 50722 0 0 0 83855 156 0 0 25 0 1 0 547284132 218914816 50328 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53446 50328 603 41 0 53405 0
vsize: 213784
[startup+850.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 51253 0 0 0 84854 157 0 0 25 0 1 0 547284132 221069312 50859 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53972 50859 603 41 0 53931 0
vsize: 215888
[startup+860.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 51709 0 0 0 85853 158 0 0 25 0 1 0 547284132 222818304 51315 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54432 51316 603 41 0 54391 0
vsize: 217596
[startup+870.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 52110 0 0 0 86852 159 0 0 25 0 1 0 547284132 224559104 51716 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54824 51716 603 41 0 54783 0
vsize: 219296
[startup+880.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 52503 0 0 0 87852 160 0 0 25 0 1 0 547284132 226160640 52109 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55215 52109 603 41 0 55174 0
vsize: 220860
[startup+890.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 52936 0 0 0 88850 162 0 0 25 0 1 0 547284132 227926016 52542 4294967295 134512640 134672761 3221224528 3221223696 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55646 52542 603 41 0 55605 0
vsize: 222584
[startup+900.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 53409 0 0 0 89849 163 0 0 25 0 1 0 547284132 229793792 53015 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56102 53015 603 41 0 56061 0
vsize: 224408
[startup+910.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 53814 0 0 0 90848 164 0 0 25 0 1 0 547284132 231407616 53420 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56496 53420 603 41 0 56455 0
vsize: 225984
[startup+920.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 54235 0 0 0 91847 165 0 0 25 0 1 0 547284132 233144320 53841 4294967295 134512640 134672761 3221224528 3221223696 134560797 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56920 53841 603 41 0 56879 0
vsize: 227680
[startup+930.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 54652 0 0 0 92846 167 0 0 25 0 1 0 547284132 234885120 54258 4294967295 134512640 134672761 3221224528 3221223652 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57345 54258 603 41 0 57304 0
vsize: 229380
[startup+940.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 55000 0 0 0 93845 167 0 0 25 0 1 0 547284132 236347392 54606 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57702 54606 603 41 0 57661 0
vsize: 230808
[startup+950.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 55382 0 0 0 94845 168 0 0 25 0 1 0 547284132 237826048 54988 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58063 54988 603 41 0 58022 0
vsize: 232252
[startup+960.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 55727 0 0 0 95844 169 0 0 25 0 1 0 547284132 239296512 55333 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58422 55333 603 41 0 58381 0
vsize: 233688
[startup+970.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 56042 0 0 0 96843 170 0 0 25 0 1 0 547284132 240631808 55648 4294967295 134512640 134672761 3221224528 3221223632 134560148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58748 55648 603 41 0 58707 0
vsize: 234992
[startup+980.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 56348 0 0 0 97843 171 0 0 25 0 1 0 547284132 241831936 55954 4294967295 134512640 134672761 3221224528 3221223696 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59041 55954 603 41 0 59000 0
vsize: 236164
[startup+990.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 56664 0 0 0 98842 172 0 0 25 0 1 0 547284132 243159040 56270 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59365 56270 603 41 0 59324 0
vsize: 237460
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 56959 0 0 0 99841 173 0 0 25 0 1 0 547284132 244371456 56565 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59661 56565 603 41 0 59620 0
vsize: 238644
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 57317 0 0 0 100841 174 0 0 25 0 1 0 547284132 245723136 56923 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59991 56923 603 41 0 59950 0
vsize: 239964
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 57682 0 0 0 101840 175 0 0 25 0 1 0 547284132 247332864 57288 4294967295 134512640 134672761 3221224528 3221223696 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60384 57288 603 41 0 60343 0
vsize: 241536
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 58049 0 0 0 102839 176 0 0 25 0 1 0 547284132 248815616 57655 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60746 57655 603 41 0 60705 0
vsize: 242984
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 58407 0 0 0 103838 177 0 0 25 0 1 0 547284132 250294272 58013 4294967295 134512640 134672761 3221224528 3221223696 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61107 58013 603 41 0 61066 0
vsize: 244428
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 58760 0 0 0 104838 177 0 0 25 0 1 0 547284132 251645952 58366 4294967295 134512640 134672761 3221224528 3221223528 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61437 58366 603 41 0 61396 0
vsize: 245748
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 59121 0 0 0 105837 179 0 0 25 0 1 0 547284132 253112320 58727 4294967295 134512640 134672761 3221224528 3221223696 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61795 58727 603 41 0 61754 0
vsize: 247180
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 59486 0 0 0 106837 179 0 0 25 0 1 0 547284132 254582784 59092 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62154 59092 603 41 0 62113 0
vsize: 248616
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 59839 0 0 0 107836 180 0 0 25 0 1 0 547284132 256053248 59445 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62513 59445 603 41 0 62472 0
vsize: 250052
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 60174 0 0 0 108835 181 0 0 25 0 1 0 547284132 257417216 59780 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62846 59780 603 41 0 62805 0
vsize: 251384
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 60494 0 0 0 109834 182 0 0 25 0 1 0 547284132 258781184 60100 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63179 60100 603 41 0 63138 0
vsize: 252716
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 60811 0 0 0 110834 183 0 0 25 0 1 0 547284132 260128768 60417 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63508 60417 603 41 0 63467 0
vsize: 254032
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 61153 0 0 0 111833 183 0 0 25 0 1 0 547284132 261472256 60759 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63836 60759 603 41 0 63795 0
vsize: 255344
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 61507 0 0 0 112833 184 0 0 25 0 1 0 547284132 262955008 61113 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64198 61113 603 41 0 64157 0
vsize: 256792
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 61843 0 0 0 113831 185 0 0 25 0 1 0 547284132 264302592 61449 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64527 61449 603 41 0 64486 0
vsize: 258108
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 62151 0 0 0 114829 186 0 0 25 0 1 0 547284132 265560064 61757 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64834 61757 603 41 0 64793 0
vsize: 259336
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 62464 0 0 0 115829 187 0 0 25 0 1 0 547284132 266768384 62070 4294967295 134512640 134672761 3221224528 3221223632 134560158 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65129 62070 603 41 0 65088 0
vsize: 260516
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 62782 0 0 0 116828 188 0 0 25 0 1 0 547284132 268115968 62388 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65458 62388 603 41 0 65417 0
vsize: 261832
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 63080 0 0 0 117828 188 0 0 25 0 1 0 547284132 269320192 62686 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65752 62686 603 41 0 65711 0
vsize: 263008
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 63364 0 0 0 118828 189 0 0 25 0 1 0 547284132 270536704 62970 4294967295 134512640 134672761 3221224528 3221223632 134559866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66049 62970 603 41 0 66008 0
vsize: 264196
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14060
Raw data (stat): 14060 (minisat+) R 14059 28546 28545 0 -1 0 63645 0 0 0 119827 190 0 0 25 0 1 0 547284132 271613952 63251 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66312 63251 603 41 0 66271 0
vsize: 265248
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.16 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 14060
Raw data (stat): 14060 (minisat+) Z 14059 28546 28545 0 -1 12 63647 0 0 0 119827 201 0 0 25 0 1 0 547284132 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.16
CPU time (s): 1200.3
CPU user time (s): 1198.28
CPU system time (s): 2.01969
CPU usage (%): 100.012
Max. virtual memory (Kb): 265248
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####