Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
  1. LAUNCHER DATA
    These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. WATCHER DATA
    This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
    Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
    When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
  4. VERIFIER DATA
    The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.

General information on the benchmark

Namenormalized-opb/mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-vpm2.opb
MD5SUMc1b4c3ad409db732d2b559e570b6f24c
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 138
Optimality of the best value was proved NO
Number of terms in the objective function 168
Biggest coefficient in the objective function 5
Number of bits for the biggest coefficient in the objective function 3
Sum of the numbers in the objective function 504
Number of bits of the sum of numbers in the objective function 9
Biggest number in a constraint 819200
Number of bits of the biggest number in a constraint 20
Biggest sum of numbers in a constraint 4941871
Number of bits of the biggest sum of numbers23
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1189.01
Number of variables2754
Total number of constraints612
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)168
Number of constraints which are nor clauses,nor cardinality constraints444
Minimum length of a constraint1
Maximum length of a constraint84

Trace number 21479 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc12 THE 2005-04-22 00:02:35 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13143 boxname=wulflinc12 idbench=1011 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c1b4c3ad409db732d2b559e570b6f24c  /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-20-10-vpm2.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-20-10-vpm2.opb /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-20-10-vpm2.opb
IDLAUNCH: 13143
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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.091
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:        221688 kB
Buffers:         33676 kB
Cached:         757676 kB
SwapCached:        508 kB
Active:         161260 kB
Inactive:       632264 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        221436 kB
SwapTotal:     2097136 kB
SwapFree:      2095888 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5276 kB
Slab:            13836 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 00:22:38 (client local time) WITH STATUS 0 IN 1200.56 SECONDS
stats: 13143 7 1200.56 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 486 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ##############################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 485]---> BDD-cost:   10
c ---[ 484]---> BDD-cost:   10
c ---[ 483]---> BDD-cost:   10
c ---[ 482]---> BDD-cost:   10
c ---[ 481]---> BDD-cost:   10
c ---[ 480]---> BDD-cost:   10
c ---[ 479]---> BDD-cost:   10
c ---[ 478]---> BDD-cost:   10
c ---[ 477]---> BDD-cost:   10
c ---[ 474]---> BDD-cost:   10
c ---[ 473]---> BDD-cost:   10
c ---[ 472]---> BDD-cost:   10
c ---[ 471]---> BDD-cost:   10
c ---[ 468]---> BDD-cost:   10
c ---[ 467]---> BDD-cost:   10
c ---[ 466]---> BDD-cost:   10
c ---[ 465]---> BDD-cost:   10
c ---[ 462]---> BDD-cost:   10
c ---[ 459]---> BDD-cost:   10
c ---[ 458]---> BDD-cost:   10
c ---[ 457]---> BDD-cost:   10
c ---[ 454]---> BDD-cost:   10
c ---[ 453]---> BDD-cost:   10
c ---[ 452]---> BDD-cost:   10
c ---[ 451]---> BDD-cost:   10
c ---[ 450]---> BDD-cost:   10
c ---[ 448]---> BDD-cost:   10
c ---[ 447]---> BDD-cost:   10
c ---[ 446]---> BDD-cost:   10
c ---[ 445]---> BDD-cost:   10
c ---[ 444]---> BDD-cost:   10
c ---[ 441]---> BDD-cost:   10
c ---[ 440]---> BDD-cost:   10
c ---[ 439]---> BDD-cost:   10
c ---[ 433]---> BDD-cost:   10
c ---[ 427]---> BDD-cost:   10
c ---[ 422]---> BDD-cost:   10
c ---[ 421]---> BDD-cost:   10
c ---[ 415]---> BDD-cost:   10
c ---[ 409]---> BDD-cost:   10
c ---[ 408]---> BDD-cost:   10
c ---[ 402]---> BDD-cost:   10
c ---[ 397]---> BDD-cost:   10
c ---[ 396]---> BDD-cost:   10
c ---[ 391]---> BDD-cost:   10
c ---[ 390]---> BDD-cost:   10
c ---[ 386]---> BDD-cost:   10
c ---[ 385]---> BDD-cost:   10
c ---[ 384]---> BDD-cost:   10
c ---[ 380]---> BDD-cost:   10
c ---[ 379]---> BDD-cost:   10
c ---[ 378]---> BDD-cost:   10
c ---[ 374]---> BDD-cost:   10
c ---[ 373]---> BDD-cost:   10
c ---[ 372]---> BDD-cost:   10
c ---[ 368]---> BDD-cost:   10
c ---[ 367]---> BDD-cost:   10
c ---[ 366]---> BDD-cost:   10
c ---[ 365]---> BDD-cost:   10
c ---[ 364]---> BDD-cost:   10
c ---[ 359]---> BDD-cost:   10
c ---[ 353]---> BDD-cost:   10
c ---[ 347]---> BDD-cost:   10
c ---[ 339]---> BDD-cost:   10
c ---[ 333]---> BDD-cost:   10
c ---[ 327]---> BDD-cost:   10
c ---[ 321]---> BDD-cost:   10
c ---[ 317]---> BDD-cost:   17
c ---[ 316]---> BDD-cost:   17
c ---[ 315]---> BDD-cost:   17
c ---[ 314]---> BDD-cost:   17
c ---[ 313]---> BDD-cost:   17
c ---[ 312]---> BDD-cost:   17
c ---[ 310]---> BDD-cost:   17
c ---[ 309]---> BDD-cost:   17
c ---[ 308]---> BDD-cost:   17
c ---[ 307]---> BDD-cost:   17
c ---[ 306]---> BDD-cost:   17
c ---[ 302]---> BDD-cost:   16
c ---[ 301]---> BDD-cost:   16
c ---[ 300]---> BDD-cost:   16
c ---[ 295]---> BDD-cost:   16
c ---[ 294]---> BDD-cost:   16
c ---[ 290]---> BDD-cost:   18
c ---[ 289]---> BDD-cost:   18
c ---[ 288]---> BDD-cost:   18
c ---[ 287]---> BDD-cost:   16
c ---[ 286]---> BDD-cost:   16
c ---[ 285]---> BDD-cost:   16
c ---[ 284]---> BDD-cost:   16
c ---[ 283]---> BDD-cost:   16
c ---[ 282]---> BDD-cost:   16
c ---[ 280]---> BDD-cost:   16
c ---[ 279]---> BDD-cost:   16
c ---[ 278]---> BDD-cost:   16
c ---[ 277]---> BDD-cost:   16
c ---[ 276]---> BDD-cost:   16
c ---[ 274]---> Adder-cost: 352   maxlim: 2411343   bits: 22/22
c ---[ 272]---> Adder-cost: 288   maxlim: 1694643   bits: 21/21
c ---[ 271]---> BDD-cost:    3
c ---[ 270]---> BDD-cost:    3
c ---[ 269]---> BDD-cost:    3
c ---[ 267]---> BDD-cost:    3
c ---[ 266]---> BDD-cost:    3
c ---[ 265]---> BDD-cost:    3
c ---[ 264]---> BDD-cost:    3
c ---[ 263]---> BDD-cost:    3
c ---[ 259]---> BDD-cost:   10
c ---[ 258]---> BDD-cost:    3
c ---[ 257]---> BDD-cost:    3
c ---[ 256]---> BDD-cost:    3
c ---[ 255]---> BDD-cost:   10
c ---[ 251]---> BDD-cost:   10
c ---[ 250]---> BDD-cost:    3
c ---[ 247]---> BDD-cost:    9
c ---[ 243]---> BDD-cost:   10
c ---[ 242]---> BDD-cost:    3
c ---[ 241]---> BDD-cost:    9
c ---[ 236]---> Sorter-cost: 2294     Base: 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[ 235]---> BDD-cost:    3
c ---[ 234]---> BDD-cost:    3
c ---[ 233]---> BDD-cost:    9
c ---[ 229]---> BDD-cost:   10
c ---[ 228]---> BDD-cost:    3
c ---[ 227]---> BDD-cost:    9
c ---[ 224]---> Adder-cost: 312   maxlim: 2587171   bits: 22/22
c ---[ 220]---> BDD-cost:    3
c ---[ 219]---> BDD-cost:    3
c ---[ 214]---> BDD-cost:   10
c ---[ 212]---> Adder-cost: 260   maxlim: 897571   bits: 20/20
c ---[ 211]---> BDD-cost:    3
c ---[ 206]---> BDD-cost:    3
c ---[ 205]---> BDD-cost:    3
c ---[ 198]---> BDD-cost:    3
c ---[ 197]---> BDD-cost:    3
c ---[ 193]---> BDD-cost:    3
c ---[ 192]---> BDD-cost:    3
c ---[ 191]---> BDD-cost:    3
c ---[ 185]---> BDD-cost:    3
c ---[ 184]---> BDD-cost:    3
c ---[ 183]---> BDD-cost:    3
c ---[ 179]---> BDD-cost:    3
c ---[ 178]---> BDD-cost:    3
c ---[ 175]---> BDD-cost:    3
c ---[ 171]---> BDD-cost:    3
c ---[ 170]---> BDD-cost:    3
c ---[ 169]---> BDD-cost:    3
c ---[ 168]---> BDD-cost:    3
c ---[ 167]---> BDD-cost:    3
c ---[ 166]---> BDD-cost:    9
c ---[ 164]---> Sorter-cost: 2815     Base: 2 2 2 5 5 2 2 2 2 2 2 2 2 3
c ---[ 163]---> BDD-cost:    9
c ---[ 162]---> BDD-cost:    9
c ---[ 161]---> BDD-cost:    9
c ---[ 160]---> BDD-cost:    3
c ---[ 159]---> BDD-cost:   10
c ---[ 158]---> BDD-cost:    9
c ---[ 157]---> BDD-cost:    9
c ---[ 156]---> BDD-cost:    9
c ---[ 155]---> BDD-cost:    9
c ---[ 154]---> BDD-cost:    3
c ---[ 152]---> Adder-cost: 352   maxlim: 2411343   bits: 22/22
c ---[ 150]---> Adder-cost: 350   maxlim: 1768271   bits: 22/21
c ---[ 149]---> BDD-cost:   10
c ---[ 148]---> BDD-cost:    8
c ---[ 147]---> BDD-cost:    8
c ---[ 146]---> BDD-cost:    8
c ---[ 145]---> BDD-cost:    8
c ---[ 144]---> BDD-cost:    3
c ---[ 143]---> BDD-cost:   10
c ---[ 142]---> BDD-cost:    8
c ---[ 141]---> BDD-cost:    8
c ---[ 140]---> BDD-cost:    8
c ---[ 137]---> BDD-cost:    8
c ---[ 135]---> BDD-cost:   10
c ---[ 134]---> BDD-cost:    3
c ---[ 133]---> BDD-cost:    9
c ---[ 132]---> BDD-cost:    9
c ---[ 131]---> BDD-cost:    9
c ---[ 129]---> BDD-cost:   10
c ---[ 128]---> BDD-cost:    3
c ---[ 125]---> BDD-cost:    9
c ---[ 124]---> BDD-cost:    9
c ---[ 123]---> BDD-cost:    9
c ---[ 121]---> BDD-cost:   10
c ---[ 120]---> BDD-cost:    3
c ---[ 119]---> BDD-cost:    9
c ---[ 118]---> BDD-cost:    9
c ---[ 117]---> BDD-cost:    9
c ---[ 114]---> Adder-cost: 274   maxlim: 1228100   bits: 21/21
c ---[ 113]---> BDD-cost:   10
c ---[ 112]---> BDD-cost:    3
c ---[ 111]---> BDD-cost:    8
c ---[ 110]---> BDD-cost:    8
c ---[ 109]---> BDD-cost:    8
c ---[ 107]---> Adder-cost: 312   maxlim: 1957187   bits: 22/21
c ---[ 105]---> Adder-cost: 312   maxlim: 1854787   bits: 22/21
c ---[ 103]---> Adder-cost: 390   maxlim: 2279471   bits: 22/22
c ---[ 101]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[  99]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[  97]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[  95]---> Adder-cost: 330   maxlim: 1694543   bits: 21/21
c ---[  93]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[  91]---> Sorter-cost: 3240     Base: 2 2 2 2 5 5 2 2 2 2 2 2 5
c ---[  89]---> Adder-cost: 440   maxlim: 3713071   bits: 23/22
c ---[  87]---> Adder-cost: 368   maxlim: 999471   bits: 21/20
c ---[  85]---> Adder-cost: 368   maxlim: 999471   bits: 21/20
c ---[  83]---> Adder-cost: 368   maxlim: 999471   bits: 21/20
c ---[  81]---> Sorter-cost: 3227     Base: 2 2 2 5 5 2 2 2 2 2 2 2 2 3
c ---[  73]---> Adder-cost: 330   maxlim: 1694543   bits: 21/21
c ---[  69]---> Sorter-cost: 3277     Base: 2 2 2 5 5 2 2 2 2 2 2 3 2 2 2
c ---[  66]---> BDD-cost:  230
c ---[  65]---> BDD-cost:  661
c ---[  64]---> BDD-cost:  660
c ---[  63]---> Sorter-cost: 1990     Base: 5 5 5 2 2 2 2 2 2 2 2 2
c ---[  62]---> Sorter-cost: 2375     Base: 5 5 5 2 2 2 2 2 2 2 2 2
c ---[  61]---> Sorter-cost: 2299     Base: 5 5 5 2 2 2 2 2 2 2 2 2
c ---[  60]---> Sorter-cost:  417     Base: 2 2 2 2 2 2 2 2 5 2
c ---[  58]---> Adder-cost: 352   maxlim: 2104143   bits: 22/22
c ---[  57]---> Sorter-cost: 1129     Base: 5 2 2 2 2 2 2 2 2 2
c ---[  56]---> Sorter-cost: 1147     Base: 5 2 2 2 2 2 2 2 2 2
c ---[  55]---> Sorter-cost: 1626     Base: 5 2 2 2 2 2 2 2 2 2
c ---[  54]---> Sorter-cost: 1906     Base: 5 2 2 2 2 2 2 2 2 2
c ---[  53]---> Sorter-cost: 1910     Base: 5 2 2 2 2 2 2 2 2 2
c ---[  52]---> Sorter-cost:  449     Base: 2 2 2 2 2 2 2 2 2 5
c ---[  51]---> Sorter-cost: 1242     Base: 2 2 2 2 2 5 2 2 2 2
c ---[  50]---> Sorter-cost: 1199     Base: 2 2 2 2 2 2 2 2 2 5
c ---[  49]---> Sorter-cost: 1719     Base: 5 2 2 2 2 2 2 2 2 2
c ---[  48]---> Sorter-cost: 2067     Base: 5 2 2 2 2 2 2 2 2 2
c ---[  46]---> Sorter-cost: 2487     Base: 2 2 2 2 2 2 2 2 5 5 2 2 2 2
c ---[  45]---> Sorter-cost: 2045     Base: 5 2 2 2 2 2 2 2 2 2
c ---[  44]---> Sorter-cost:  223     Base: 2 2 2 2 2 2 2 2 2
c ---[  43]---> Sorter-cost:  590     Base: 2 2 2 2 2 2 2 2
c ---[  42]---> Sorter-cost:  538     Base: 2 2 2 2 2 2 2 2 2
c ---[  41]---> Sorter-cost: 1025     Base: 2 2 2 2 2 2 2 2
c ---[  40]---> Sorter-cost: 1211     Base: 2 2 2 2 2 2 2 2 2
c ---[  39]---> Sorter-cost: 1390     Base: 2 2 2 2 2 2 2 2
c ---[  38]---> BDD-cost:    3
c ---[  37]---> BDD-cost:    3
c ---[  36]---> BDD-cost:    3
c ---[  34]---> Adder-cost: 304   maxlim: 2309043   bits: 22/22
c ---[  33]---> BDD-cost:    3
c ---[  32]---> BDD-cost:    3
c ---[  31]---> BDD-cost:    3
c ---[  30]---> BDD-cost:    3
c ---[  29]---> BDD-cost:    3
c ---[  28]---> BDD-cost:    3
c ---[  27]---> BDD-cost:   10
c ---[  26]---> BDD-cost:   10
c ---[  25]---> BDD-cost:    3
c ---[  24]---> BDD-cost:    3
c ---[  22]---> Adder-cost: 304   maxlim: 2104243   bits: 22/22
c ---[  21]---> BDD-cost:    3
c ---[  20]---> BDD-cost:    3
c ---[  19]---> BDD-cost:   10
c ---[  18]---> BDD-cost:   10
c ---[  17]---> BDD-cost:    3
c ---[  16]---> BDD-cost:    3
c ---[  15]---> BDD-cost:    3
c ---[  14]---> BDD-cost:    3
c ---[  13]---> BDD-cost:   10
c ---[  12]---> BDD-cost:   10
c ---[  10]---> Adder-cost: 304   maxlim: 2104243   bits: 22/22
c ---[   9]---> BDD-cost:    3
c ---[   7]---> BDD-cost:   10
c ---[   6]---> BDD-cost:    3
c ---[   5]---> BDD-cost:    3
c ---[   4]---> BDD-cost:    3
c ---[   3]---> BDD-cost:   10
c ---[   1]---> BDD-cost:    3
c ---[   0]---> BDD-cost:    3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  181739   495453 |   60579       0        0     nan |  0.000 % |
c |       100 |  181739   495453 |   66636     100      320     3.2 |  5.013 % |
c |       251 |  181701   495340 |   73300     250     1016     4.1 |  5.023 % |
c |       477 |  181500   494853 |   80630     467     2243     4.8 |  5.114 % |
c |       816 |  181500   494853 |   88693     806     5952     7.4 |  5.114 % |
c |      1322 |  181432   494671 |   97563    1309    10523     8.0 |  5.139 % |
c |      2081 |  181100   493757 |  107319    2057    20821    10.1 |  5.250 % |
c |      3220 |  180869   493187 |  118051    3182    33678    10.6 |  5.355 % |
c |      4929 |  180361   491927 |  129856    4846    61611    12.7 |  5.630 % |
c |      7491 |  180224   491498 |  142842    7395   127715    17.3 |  5.672 % |
c |     11335 |  179713   490268 |  157126   11204   235245    21.0 |  5.925 % |
c |     17103 |  179525   489766 |  172838   16964   427519    25.2 |  6.016 % |
c |     25754 |  179483   489664 |  190122   25612   728225    28.4 |  6.037 % |
c |     38728 |  179112   488700 |  209135   38563  1204776    31.2 |  6.204 % |
c |     58190 |  178605   487473 |  230048   58004  1846514    31.8 |  6.429 % |
c |     87383 |  177588   485014 |  253053   87134  3136088    36.0 |  6.901 % |
c |    131174 |  176889   483352 |  278358  130854  4426948    33.8 |  7.272 % |
c |    196858 |  176285   481786 |  306194  196493  6896169    35.1 |  7.563 % |
c |    295384 |  175149   478998 |  336814  294937 10403858    35.3 |  8.170 % |
c |    443173 |  174296   477006 |  370495  132068  3977764    30.1 |  8.673 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.97 0.91 2/54 8788
Raw data (stat): 8788 (runsolver) R 8787 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 491021495 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0004 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 5224 0 0 0 986 12 0 0 25 0 1 0 491021495 24027136 5047 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5866 5047 603 41 0 5825 0
vsize: 23464
[startup+20.0012 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 5688 0 0 0 1984 14 0 0 25 0 1 0 491021495 25997312 5511 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6347 5511 603 41 0 6306 0
vsize: 25388
[startup+30.0016 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 6030 0 0 0 2983 15 0 0 25 0 1 0 491021495 27332608 5853 4294967295 134512640 134672761 3221224544 3221223648 134560059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6673 5853 603 41 0 6632 0
vsize: 26692
[startup+40.0009 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 6443 0 0 0 3981 17 0 0 25 0 1 0 491021495 29065216 6266 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7096 6266 603 41 0 7055 0
vsize: 28384
[startup+50.0017 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 6792 0 0 0 4980 17 0 0 25 0 1 0 491021495 30531584 6615 4294967295 134512640 134672761 3221224544 3221223712 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7454 6615 603 41 0 7413 0
vsize: 29816
[startup+60.0019 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 7145 0 0 0 5979 19 0 0 25 0 1 0 491021495 31875072 6968 4294967295 134512640 134672761 3221224544 3221223712 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7782 6968 603 41 0 7741 0
vsize: 31128
[startup+70.0024 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 7448 0 0 0 6978 20 0 0 25 0 1 0 491021495 33214464 7271 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8109 7271 603 41 0 8068 0
vsize: 32436
[startup+80.0023 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 7678 0 0 0 7977 22 0 0 25 0 1 0 491021495 34013184 7501 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8304 7501 603 41 0 8263 0
vsize: 33216
[startup+90.0024 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 7861 0 0 0 8976 22 0 0 25 0 1 0 491021495 35082240 7684 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8565 7684 603 41 0 8524 0
vsize: 34260
[startup+100.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 8095 0 0 0 9975 23 0 0 25 0 1 0 491021495 36040704 7918 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8799 7918 603 41 0 8758 0
vsize: 35196
[startup+110.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 8320 0 0 0 10975 24 0 0 25 0 1 0 491021495 36843520 8143 4294967295 134512640 134672761 3221224544 3221223680 134560608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8995 8143 603 41 0 8954 0
vsize: 35980
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 8743 0 0 0 11973 26 0 0 25 0 1 0 491021495 38580224 8566 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9419 8566 603 41 0 9378 0
vsize: 37676
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 9075 0 0 0 12972 27 0 0 25 0 1 0 491021495 39919616 8898 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9746 8898 603 41 0 9705 0
vsize: 38984
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 9332 0 0 0 13971 28 0 0 25 0 1 0 491021495 41005056 9155 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10011 9155 603 41 0 9970 0
vsize: 40044
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 9604 0 0 0 14971 28 0 0 25 0 1 0 491021495 42078208 9427 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10273 9427 603 41 0 10232 0
vsize: 41092
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 9831 0 0 0 15970 29 0 0 25 0 1 0 491021495 43012096 9654 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10501 9654 603 41 0 10460 0
vsize: 42004
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 10061 0 0 0 16970 30 0 0 25 0 1 0 491021495 43950080 9884 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10730 9884 603 41 0 10689 0
vsize: 42920
[startup+180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 10246 0 0 0 17971 30 0 0 25 0 1 0 491021495 44638208 10069 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10898 10069 603 41 0 10857 0
vsize: 43592
[startup+190.247 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 10557 0 0 0 18993 31 0 0 25 0 1 0 491021495 45969408 10380 4294967295 134512640 134672761 3221224544 3221223680 134565098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11223 10380 603 41 0 11182 0
vsize: 44892
[startup+200.247 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 10808 0 0 0 19992 32 0 0 25 0 1 0 491021495 47435776 10631 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11581 10631 603 41 0 11540 0
vsize: 46324
[startup+210.253 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 11098 0 0 0 20992 33 0 0 25 0 1 0 491021495 48631808 10921 4294967295 134512640 134672761 3221224544 3221223700 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11873 10921 603 41 0 11832 0
vsize: 47492
[startup+220.258 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 11352 0 0 0 21993 33 0 0 25 0 1 0 491021495 49700864 11175 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12134 11175 603 41 0 12093 0
vsize: 48536
[startup+230.258 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 11567 0 0 0 22993 33 0 0 25 0 1 0 491021495 50507776 11390 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12331 11390 603 41 0 12290 0
vsize: 49324
[startup+240.258 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 11797 0 0 0 23992 34 0 0 25 0 1 0 491021495 51441664 11620 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12559 11620 603 41 0 12518 0
vsize: 50236
[startup+250.259 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 11959 0 0 0 24992 35 0 0 25 0 1 0 491021495 52150272 11782 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12732 11782 603 41 0 12691 0
vsize: 50928
[startup+260.259 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 12138 0 0 0 25991 35 0 0 25 0 1 0 491021495 52838400 11961 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12900 11961 603 41 0 12859 0
vsize: 51600
[startup+270.259 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 12325 0 0 0 26991 36 0 0 25 0 1 0 491021495 53641216 12148 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13096 12148 603 41 0 13055 0
vsize: 52384
[startup+280.263 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 12442 0 0 0 27991 36 0 0 25 0 1 0 491021495 54038528 12265 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13193 12265 603 41 0 13152 0
vsize: 52772
[startup+290.267 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 12551 0 0 0 28991 36 0 0 25 0 1 0 491021495 54464512 12374 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13297 12374 603 41 0 13256 0
vsize: 53188
[startup+300.273 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 12662 0 0 0 29992 37 0 0 25 0 1 0 491021495 55017472 12485 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13432 12485 603 41 0 13391 0
vsize: 53728
[startup+310.273 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 12767 0 0 0 30991 37 0 0 25 0 1 0 491021495 55414784 12590 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13529 12590 603 41 0 13488 0
vsize: 54116
[startup+320.273 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 12906 0 0 0 31991 38 0 0 25 0 1 0 491021495 55959552 12729 4294967295 134512640 134672761 3221224544 3221223716 134556646 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13662 12729 603 41 0 13621 0
vsize: 54648
[startup+330.273 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 13037 0 0 0 32991 38 0 0 25 0 1 0 491021495 56504320 12860 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13795 12860 603 41 0 13754 0
vsize: 55180
[startup+340.273 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 13172 0 0 0 33991 38 0 0 25 0 1 0 491021495 57036800 12995 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13925 12995 603 41 0 13884 0
vsize: 55700
[startup+350.274 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 13288 0 0 0 34991 39 0 0 25 0 1 0 491021495 57577472 13111 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14057 13111 603 41 0 14016 0
vsize: 56228
[startup+360.274 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 13365 0 0 0 35991 39 0 0 25 0 1 0 491021495 57847808 13188 4294967295 134512640 134672761 3221224544 3221223688 134560630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14123 13188 603 41 0 14082 0
vsize: 56492
[startup+370.275 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 13448 0 0 0 36991 39 0 0 25 0 1 0 491021495 58265600 13271 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14225 13271 603 41 0 14184 0
vsize: 56900
[startup+380.275 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 13552 0 0 0 37991 39 0 0 25 0 1 0 491021495 58658816 13375 4294967295 134512640 134672761 3221224544 3221223680 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14321 13375 603 41 0 14280 0
vsize: 57284
[startup+390.276 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 13650 0 0 0 38990 40 0 0 25 0 1 0 491021495 59060224 13473 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14419 13473 603 41 0 14378 0
vsize: 57676
[startup+400.276 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 13755 0 0 0 39990 40 0 0 25 0 1 0 491021495 59453440 13578 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14515 13578 603 41 0 14474 0
vsize: 58060
[startup+410.276 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 13853 0 0 0 40990 40 0 0 25 0 1 0 491021495 59846656 13676 4294967295 134512640 134672761 3221224544 3221223712 134560954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14611 13676 603 41 0 14570 0
vsize: 58444
[startup+420.287 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 13989 0 0 0 41991 40 0 0 25 0 1 0 491021495 60383232 13812 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14742 13812 603 41 0 14701 0
vsize: 58968
[startup+430.288 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 14134 0 0 0 42991 41 0 0 25 0 1 0 491021495 61091840 13957 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14915 13957 603 41 0 14874 0
vsize: 59660
[startup+440.287 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 14234 0 0 0 43991 41 0 0 25 0 1 0 491021495 61497344 14057 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15014 14057 603 41 0 14973 0
vsize: 60056
[startup+450.295 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 14342 0 0 0 44991 41 0 0 25 0 1 0 491021495 61902848 14165 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15113 14165 603 41 0 15072 0
vsize: 60452
[startup+460.295 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 14601 0 0 0 45990 43 0 0 25 0 1 0 491021495 62984192 14424 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15377 14424 603 41 0 15336 0
vsize: 61508
[startup+470.295 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 14880 0 0 0 46989 44 0 0 25 0 1 0 491021495 64057344 14703 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15639 14703 603 41 0 15598 0
vsize: 62556
[startup+480.299 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 15203 0 0 0 47989 45 0 0 25 0 1 0 491021495 65388544 15026 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15964 15026 603 41 0 15923 0
vsize: 63856
[startup+490.306 s]
Raw data (loadavg): 1.15 1.00 0.92 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 15458 0 0 0 48989 45 0 0 25 0 1 0 491021495 66367488 15281 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16203 15281 603 41 0 16162 0
vsize: 64812
[startup+500.306 s]
Raw data (loadavg): 1.12 1.00 0.92 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 15805 0 0 0 49988 46 0 0 25 0 1 0 491021495 67825664 15628 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16559 15628 603 41 0 16518 0
vsize: 66236
[startup+510.307 s]
Raw data (loadavg): 1.10 1.00 0.92 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 15927 0 0 0 50988 47 0 0 25 0 1 0 491021495 68407296 15750 4294967295 134512640 134672761 3221224544 3221223696 134561040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16701 15750 603 41 0 16660 0
vsize: 66804
[startup+520.307 s]
Raw data (loadavg): 1.09 1.00 0.92 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 16002 0 0 0 51988 47 0 0 25 0 1 0 491021495 68673536 15825 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16766 15825 603 41 0 16725 0
vsize: 67064
[startup+530.307 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 16080 0 0 0 52988 47 0 0 25 0 1 0 491021495 68976640 15903 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16840 15903 603 41 0 16799 0
vsize: 67360
[startup+540.307 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 16251 0 0 0 53987 48 0 0 25 0 1 0 491021495 69640192 16074 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17002 16074 603 41 0 16961 0
vsize: 68008
[startup+550.308 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 16410 0 0 0 54987 48 0 0 25 0 1 0 491021495 70316032 16233 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17167 16233 603 41 0 17126 0
vsize: 68668
[startup+560.308 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 16535 0 0 0 55987 49 0 0 25 0 1 0 491021495 70754304 16358 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17274 16358 603 41 0 17233 0
vsize: 69096
[startup+570.309 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 16660 0 0 0 56987 49 0 0 25 0 1 0 491021495 71286784 16483 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17404 16483 603 41 0 17363 0
vsize: 69616
[startup+580.309 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 16825 0 0 0 57986 50 0 0 25 0 1 0 491021495 71950336 16648 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17566 16648 603 41 0 17525 0
vsize: 70264
[startup+590.309 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 16957 0 0 0 58986 50 0 0 25 0 1 0 491021495 72515584 16780 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17704 16780 603 41 0 17663 0
vsize: 70816
[startup+600.309 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 17164 0 0 0 59986 51 0 0 25 0 1 0 491021495 73322496 16987 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17901 16987 603 41 0 17860 0
vsize: 71604
[startup+610.31 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 17399 0 0 0 60986 51 0 0 25 0 1 0 491021495 75309056 17222 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18386 17222 603 41 0 18345 0
vsize: 73544
[startup+620.311 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 17661 0 0 0 61985 52 0 0 25 0 1 0 491021495 76369920 17484 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18645 17484 603 41 0 18604 0
vsize: 74580
[startup+630.311 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 17839 0 0 0 62984 53 0 0 25 0 1 0 491021495 77058048 17662 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18813 17662 603 41 0 18772 0
vsize: 75252
[startup+640.311 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 18076 0 0 0 63983 54 0 0 25 0 1 0 491021495 78000128 17899 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19043 17899 603 41 0 19002 0
vsize: 76172
[startup+650.311 s]
Raw data (loadavg): 1.08 1.02 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 18227 0 0 0 64983 54 0 0 25 0 1 0 491021495 78544896 18050 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19176 18050 603 41 0 19135 0
vsize: 76704
[startup+660.311 s]
Raw data (loadavg): 1.07 1.02 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 18415 0 0 0 65983 55 0 0 25 0 1 0 491021495 79351808 18238 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19373 18238 603 41 0 19332 0
vsize: 77492
[startup+670.325 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 18590 0 0 0 66983 56 0 0 25 0 1 0 491021495 80023552 18413 4294967295 134512640 134672761 3221224544 3221223712 134561156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19537 18413 603 41 0 19496 0
vsize: 78148
[startup+680.339 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 18793 0 0 0 67983 56 0 0 25 0 1 0 491021495 80850944 18616 4294967295 134512640 134672761 3221224544 3221223744 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19739 18616 603 41 0 19698 0
vsize: 78956
[startup+690.338 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 18986 0 0 0 68983 56 0 0 25 0 1 0 491021495 81657856 18809 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19936 18809 603 41 0 19895 0
vsize: 79744
[startup+700.338 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 19120 0 0 0 69982 57 0 0 25 0 1 0 491021495 82198528 18943 4294967295 134512640 134672761 3221224544 3221223728 134558648 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20068 18943 603 41 0 20027 0
vsize: 80272
[startup+710.339 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 19272 0 0 0 70982 57 0 0 25 0 1 0 491021495 82874368 19095 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20233 19095 603 41 0 20192 0
vsize: 80932
[startup+720.34 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 19406 0 0 0 71982 58 0 0 25 0 1 0 491021495 83419136 19229 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20366 19229 603 41 0 20325 0
vsize: 81464
[startup+730.34 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 19536 0 0 0 72982 58 0 0 25 0 1 0 491021495 83963904 19359 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20499 19359 603 41 0 20458 0
vsize: 81996
[startup+740.34 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 19651 0 0 0 73981 59 0 0 25 0 1 0 491021495 84500480 19474 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20630 19474 603 41 0 20589 0
vsize: 82520
[startup+750.34 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 19781 0 0 0 74981 60 0 0 25 0 1 0 491021495 84901888 19604 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20728 19604 603 41 0 20687 0
vsize: 82912
[startup+760.348 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 19903 0 0 0 75981 60 0 0 25 0 1 0 491021495 85471232 19726 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20867 19726 603 41 0 20826 0
vsize: 83468
[startup+770.348 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20007 0 0 0 76981 60 0 0 25 0 1 0 491021495 85884928 19830 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20968 19830 603 41 0 20927 0
vsize: 83872
[startup+780.353 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20087 0 0 0 77981 61 0 0 25 0 1 0 491021495 86155264 19910 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21034 19910 603 41 0 20993 0
vsize: 84136
[startup+790.365 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20215 0 0 0 78982 61 0 0 25 0 1 0 491021495 86687744 20038 4294967295 134512640 134672761 3221224544 3221223728 134558658 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21164 20038 603 41 0 21123 0
vsize: 84656
[startup+800.366 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20374 0 0 0 79982 61 0 0 25 0 1 0 491021495 87355392 20197 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21327 20197 603 41 0 21286 0
vsize: 85308
[startup+810.366 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20427 0 0 0 80982 61 0 0 25 0 1 0 491021495 87490560 20250 4294967295 134512640 134672761 3221224544 3221223648 134554617 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21360 20250 603 41 0 21319 0
vsize: 85440
[startup+820.367 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20427 0 0 0 81983 61 0 0 25 0 1 0 491021495 87490560 20250 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21360 20250 603 41 0 21319 0
vsize: 85440
[startup+830.366 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20427 0 0 0 82983 61 0 0 25 0 1 0 491021495 87490560 20250 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21360 20250 603 41 0 21319 0
vsize: 85440
[startup+840.366 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20427 0 0 0 83983 61 0 0 25 0 1 0 491021495 87490560 20250 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21360 20250 603 41 0 21319 0
vsize: 85440
[startup+850.377 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20427 0 0 0 84984 61 0 0 25 0 1 0 491021495 87490560 20250 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21360 20250 603 41 0 21319 0
vsize: 85440
[startup+860.377 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20427 0 0 0 85984 61 0 0 25 0 1 0 491021495 87490560 20250 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21360 20250 603 41 0 21319 0
vsize: 85440
[startup+870.378 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20427 0 0 0 86985 61 0 0 25 0 1 0 491021495 87490560 20250 4294967295 134512640 134672761 3221224544 3221223712 134561025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21360 20250 603 41 0 21319 0
vsize: 85440
[startup+880.378 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20427 0 0 0 87985 61 0 0 25 0 1 0 491021495 87490560 20250 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21360 20250 603 41 0 21319 0
vsize: 85440
[startup+890.377 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20427 0 0 0 88985 61 0 0 25 0 1 0 491021495 87490560 20250 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21360 20250 603 41 0 21319 0
vsize: 85440
[startup+900.377 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20427 0 0 0 89985 61 0 0 25 0 1 0 491021495 87490560 20250 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21360 20250 603 41 0 21319 0
vsize: 85440
[startup+910.377 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20427 0 0 0 90985 61 0 0 25 0 1 0 491021495 87490560 20250 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21360 20250 603 41 0 21319 0
vsize: 85440
[startup+920.379 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20427 0 0 0 91986 61 0 0 25 0 1 0 491021495 87490560 20250 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21360 20250 603 41 0 21319 0
vsize: 85440
[startup+930.379 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20427 0 0 0 92986 61 0 0 25 0 1 0 491021495 87490560 20250 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21360 20250 603 41 0 21319 0
vsize: 85440
[startup+940.379 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20427 0 0 0 93986 61 0 0 25 0 1 0 491021495 87490560 20250 4294967295 134512640 134672761 3221224544 3221223728 134559376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21360 20250 603 41 0 21319 0
vsize: 85440
[startup+950.379 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20427 0 0 0 94986 61 0 0 25 0 1 0 491021495 87490560 20250 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21360 20250 603 41 0 21319 0
vsize: 85440
[startup+960.379 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20429 0 0 0 95986 61 0 0 25 0 1 0 491021495 87490560 20252 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21360 20252 603 41 0 21319 0
vsize: 85440
[startup+970.381 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20429 0 0 0 96987 61 0 0 25 0 1 0 491021495 87490560 20252 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21360 20252 603 41 0 21319 0
vsize: 85440
[startup+980.381 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20429 0 0 0 97987 61 0 0 25 0 1 0 491021495 87490560 20252 4294967295 134512640 134672761 3221224544 3221223728 134558275 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21360 20252 603 41 0 21319 0
vsize: 85440
[startup+990.381 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20429 0 0 0 98987 61 0 0 25 0 1 0 491021495 87490560 20252 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21360 20252 603 41 0 21319 0
vsize: 85440
[startup+1000.38 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20429 0 0 0 99987 61 0 0 25 0 1 0 491021495 87490560 20252 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21360 20252 603 41 0 21319 0
vsize: 85440
[startup+1010.38 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20429 0 0 0 100987 61 0 0 25 0 1 0 491021495 87490560 20252 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21360 20252 603 41 0 21319 0
vsize: 85440
[startup+1020.38 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20429 0 0 0 101986 62 0 0 25 0 1 0 491021495 87490560 20252 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21360 20252 603 41 0 21319 0
vsize: 85440
[startup+1030.38 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20429 0 0 0 102986 62 0 0 25 0 1 0 491021495 87490560 20252 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21360 20252 603 41 0 21319 0
vsize: 85440
[startup+1040.38 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20430 0 0 0 103986 62 0 0 25 0 1 0 491021495 87490560 20253 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21360 20253 603 41 0 21319 0
vsize: 85440
[startup+1050.38 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20430 0 0 0 104987 62 0 0 25 0 1 0 491021495 87490560 20253 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21360 20253 603 41 0 21319 0
vsize: 85440
[startup+1060.38 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20430 0 0 0 105987 62 0 0 25 0 1 0 491021495 87490560 20253 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21360 20253 603 41 0 21319 0
vsize: 85440
[startup+1070.38 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20430 0 0 0 106987 62 0 0 25 0 1 0 491021495 87490560 20253 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21360 20253 603 41 0 21319 0
vsize: 85440
[startup+1080.38 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20431 0 0 0 107987 62 0 0 25 0 1 0 491021495 87490560 20254 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21360 20254 603 41 0 21319 0
vsize: 85440
[startup+1090.38 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20431 0 0 0 108987 62 0 0 25 0 1 0 491021495 87490560 20254 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21360 20254 603 41 0 21319 0
vsize: 85440
[startup+1100.38 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20431 0 0 0 109987 62 0 0 25 0 1 0 491021495 87490560 20254 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21360 20254 603 41 0 21319 0
vsize: 85440
[startup+1110.38 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20432 0 0 0 110988 62 0 0 25 0 1 0 491021495 87490560 20255 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21360 20255 603 41 0 21319 0
vsize: 85440
[startup+1120.39 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20432 0 0 0 111988 62 0 0 25 0 1 0 491021495 87490560 20255 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21360 20255 603 41 0 21319 0
vsize: 85440
[startup+1130.39 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20433 0 0 0 112988 62 0 0 25 0 1 0 491021495 87490560 20256 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21360 20256 603 41 0 21319 0
vsize: 85440
[startup+1140.39 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20435 0 0 0 113988 62 0 0 25 0 1 0 491021495 87490560 20258 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21360 20258 603 41 0 21319 0
vsize: 85440
[startup+1150.39 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20437 0 0 0 114989 62 0 0 25 0 1 0 491021495 87490560 20260 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21360 20260 603 41 0 21319 0
vsize: 85440
[startup+1160.39 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20437 0 0 0 115989 62 0 0 25 0 1 0 491021495 87490560 20260 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21360 20260 603 41 0 21319 0
vsize: 85440
[startup+1170.39 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20437 0 0 0 116989 62 0 0 25 0 1 0 491021495 87490560 20260 4294967295 134512640 134672761 3221224544 3221223744 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21360 20260 603 41 0 21319 0
vsize: 85440
[startup+1180.39 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20437 0 0 0 117989 62 0 0 25 0 1 0 491021495 87490560 20260 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21360 20260 603 41 0 21319 0
vsize: 85440
[startup+1190.39 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20437 0 0 0 118989 62 0 0 25 0 1 0 491021495 87490560 20260 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21360 20260 603 41 0 21319 0
vsize: 85440
[startup+1200.39 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 8790
Raw data (stat): 8788 (minisat+) R 8787 25285 25284 0 -1 0 20437 0 0 0 119990 62 0 0 25 0 1 0 491021495 87490560 20260 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21360 20260 603 41 0 21319 0
vsize: 85440
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.43 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 8790
Raw data (stat): 8788 (minisat+) Z 8787 25285 25284 0 -1 12 20439 0 0 0 119990 66 0 0 25 0 1 0 491021495 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.43
CPU time (s): 1200.56
CPU user time (s): 1199.9
CPU system time (s): 0.661899
CPU usage (%): 100.011
Max. virtual memory (Kb): 85440
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####