PB'05 competition: run trace

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:
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.
SOLVER DATA
This is the output of the solver (stdout and stderr).
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.
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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-vpm1.opb
MD5SUM	9d68724ddc6098af63bcc619f21688cc
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	20
Optimality of the best value was proved	NO
Number of terms in the objective function	168
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	168
Number of bits of the sum of numbers in the objective function	8
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 numbers	23
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	459.704
Number of variables	2754
Total number of constraints	612
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	168
Number of constraints which are nor clauses,nor cardinality constraints	444
Minimum length of a constraint	1
Maximum length of a constraint	82
Trace number 16869

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc22 THE 2005-04-21 08:52:53 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12376 boxname=wulflinc22 idbench=952 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  9d68724ddc6098af63bcc619f21688cc  /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-vpm1.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-vpm1.opb /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-vpm1.opb
IDLAUNCH: 12376
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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.031
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:        536248 kB
Buffers:         31504 kB
Cached:         436380 kB
SwapCached:         24 kB
Active:         150892 kB
Inactive:       319688 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        535996 kB
SwapTotal:     2097892 kB
SwapFree:      2097660 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6640 kB
Slab:            22264 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 09:12:55 (client local time) WITH STATUS 0 IN 1200.24 SECONDS
stats: 12376 7 1200.24 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 486 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ##############################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 485]---> BDD-cost:   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]---> Sorter-cost: 3227     Base: 2 2 2 5 5 2 2 2 2 2 2 2 2 3
c ---[ 264]---> Sorter-cost: 3277     Base: 2 2 2 5 5 2 2 2 2 2 2 3 2 2 2
c ---[ 260]---> Adder-cost: 352   maxlim: 2411343   bits: 22/22
c ---[ 258]---> Adder-cost: 352   maxlim: 2411343   bits: 22/22
c ---[ 256]---> Adder-cost: 330   maxlim: 1694543   bits: 21/21
c ---[ 254]---> Adder-cost: 330   maxlim: 1694543   bits: 21/21
c ---[ 252]---> Adder-cost: 352   maxlim: 2104143   bits: 22/22
c ---[ 250]---> Sorter-cost: 2487     Base: 2 2 2 2 2 2 2 2 5 5 2 2 2 2
c ---[ 248]---> Adder-cost: 304   maxlim: 2309043   bits: 22/22
c ---[ 246]---> Adder-cost: 304   maxlim: 2104243   bits: 22/22
c ---[ 244]---> Adder-cost: 304   maxlim: 2104243   bits: 22/22
c ---[ 242]---> Adder-cost: 288   maxlim: 1694643   bits: 21/21
c ---[ 236]---> Sorter-cost: 2294     Base: 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[ 234]---> Adder-cost: 312   maxlim: 2587171   bits: 22/22
c ---[ 232]---> Adder-cost: 260   maxlim: 897571   bits: 20/20
c ---[ 224]---> Sorter-cost: 2815     Base: 2 2 2 5 5 2 2 2 2 2 2 2 2 3
c ---[ 222]---> Adder-cost: 350   maxlim: 1768271   bits: 22/21
c ---[ 216]---> Adder-cost: 274   maxlim: 1228100   bits: 21/21
c ---[ 214]---> Adder-cost: 312   maxlim: 1957187   bits: 22/21
c ---[ 212]---> Adder-cost: 312   maxlim: 1854787   bits: 22/21
c ---[ 210]---> Adder-cost: 390   maxlim: 2279471   bits: 22/22
c ---[ 208]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[ 206]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[ 204]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[ 202]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[ 200]---> Sorter-cost: 3241     Base: 2 2 2 2 5 5 2 2 2 2 2 2 5
c ---[ 198]---> Adder-cost: 440   maxlim: 3713071   bits: 23/22
c ---[ 196]---> Adder-cost: 368   maxlim: 999471   bits: 21/20
c ---[ 194]---> Adder-cost: 368   maxlim: 999471   bits: 21/20
c ---[ 192]---> Adder-cost: 368   maxlim: 999471   bits: 21/20
c ---[ 191]---> BDD-cost:   48
c ---[ 190]---> Sorter-cost:  386     Base: 2 2 2 2 2 2 2 2 2
c ---[ 189]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2
c ---[ 188]---> Sorter-cost:  801     Base: 2 2 2 2 2 2 2 2 2
c ---[ 187]---> Sorter-cost: 1088     Base: 2 2 2 2 2 2 2 2 2
c ---[ 186]---> Sorter-cost:  982     Base: 2 2 2 2 2 2 2 2 2
c ---[ 185]---> BDD-cost:   48
c ---[ 184]---> Sorter-cost:  386     Base: 2 2 2 2 2 2 2 2 2
c ---[ 183]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2
c ---[ 182]---> Sorter-cost:  781     Base: 2 2 2 2 2 2 2 2 2
c ---[ 181]---> Sorter-cost: 1034     Base: 2 2 2 2 2 2 2 2 2
c ---[ 180]---> Sorter-cost: 1032     Base: 2 2 2 2 2 2 2 2 2
c ---[ 179]---> BDD-cost:   48
c ---[ 178]---> Sorter-cost:  386     Base: 2 2 2 2 2 2 2 2 2
c ---[ 177]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2
c ---[ 176]---> Sorter-cost:  788     Base: 2 2 2 2 2 2 2 2 2
c ---[ 175]---> Sorter-cost: 1047     Base: 2 2 2 2 2 2 2 2 2
c ---[ 174]---> Sorter-cost: 1019     Base: 2 2 2 2 2 2 2 2 2
c ---[ 173]---> BDD-cost:   48
c ---[ 172]---> Sorter-cost:  370     Base: 2 2 2 2 2 2 2 2 2
c ---[ 171]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2
c ---[ 170]---> Sorter-cost:  747     Base: 2 2 2 2 2 2 2 2 2
c ---[ 169]---> Sorter-cost: 1022     Base: 2 2 2 2 2 2 2 2 2
c ---[ 168]---> Sorter-cost:  952     Base: 2 2 2 2 2 2 2 2 2
c ---[ 167]---> BDD-cost:    3
c ---[ 166]---> BDD-cost:    3
c ---[ 165]---> BDD-cost:    3
c ---[ 164]---> BDD-cost:    3
c ---[ 163]---> BDD-cost:    3
c ---[ 162]---> BDD-cost:    3
c ---[ 161]---> BDD-cost:    3
c ---[ 160]---> BDD-cost:    3
c ---[ 159]---> BDD-cost:    3
c ---[ 158]---> BDD-cost:   10
c ---[ 157]---> BDD-cost:   10
c ---[ 156]---> BDD-cost:    3
c ---[ 155]---> BDD-cost:    3
c ---[ 154]---> BDD-cost:    3
c ---[ 153]---> BDD-cost:    3
c ---[ 152]---> BDD-cost:   10
c ---[ 151]---> BDD-cost:   10
c ---[ 150]---> BDD-cost:    3
c ---[ 149]---> BDD-cost:    3
c ---[ 148]---> BDD-cost:    3
c ---[ 147]---> BDD-cost:    3
c ---[ 146]---> BDD-cost:   10
c ---[ 145]---> BDD-cost:   10
c ---[ 144]---> BDD-cost:    3
c ---[ 142]---> BDD-cost:   10
c ---[ 141]---> BDD-cost:    3
c ---[ 140]---> BDD-cost:    3
c ---[ 139]---> BDD-cost:    3
c ---[ 138]---> BDD-cost:   10
c ---[ 136]---> BDD-cost:    3
c ---[ 135]---> BDD-cost:    3
c ---[ 134]---> BDD-cost:    3
c ---[ 133]---> BDD-cost:    3
c ---[ 132]---> BDD-cost:    3
c ---[ 130]---> BDD-cost:    3
c ---[ 129]---> BDD-cost:    3
c ---[ 128]---> BDD-cost:    3
c ---[ 127]---> BDD-cost:    3
c ---[ 126]---> BDD-cost:    3
c ---[ 124]---> BDD-cost:   10
c ---[ 123]---> BDD-cost:    3
c ---[ 122]---> BDD-cost:    3
c ---[ 121]---> BDD-cost:    3
c ---[ 120]---> BDD-cost:   10
c ---[ 116]---> BDD-cost:   10
c ---[ 115]---> BDD-cost:    3
c ---[ 114]---> BDD-cost:    9
c ---[ 110]---> BDD-cost:   10
c ---[ 109]---> BDD-cost:    3
c ---[ 108]---> BDD-cost:    9
c ---[ 104]---> BDD-cost:    3
c ---[ 103]---> BDD-cost:    3
c ---[ 102]---> BDD-cost:    9
c ---[  98]---> BDD-cost:   10
c ---[  97]---> BDD-cost:    3
c ---[  96]---> BDD-cost:    9
c ---[  91]---> BDD-cost:    3
c ---[  90]---> BDD-cost:    3
c ---[  85]---> BDD-cost:   10
c ---[  84]---> BDD-cost:    3
c ---[  79]---> BDD-cost:    3
c ---[  78]---> BDD-cost:    3
c ---[  73]---> BDD-cost:    3
c ---[  72]---> BDD-cost:    3
c ---[  68]---> BDD-cost:    3
c ---[  67]---> BDD-cost:    3
c ---[  66]---> BDD-cost:    3
c ---[  62]---> BDD-cost:    3
c ---[  61]---> BDD-cost:    3
c ---[  60]---> BDD-cost:    3
c ---[  56]---> BDD-cost:    3
c ---[  55]---> BDD-cost:    3
c ---[  54]---> BDD-cost:    3
c ---[  50]---> BDD-cost:    3
c ---[  49]---> BDD-cost:    3
c ---[  48]---> BDD-cost:    3
c ---[  47]---> BDD-cost:    3
c ---[  46]---> BDD-cost:    3
c ---[  45]---> BDD-cost:    9
c ---[  44]---> BDD-cost:    9
c ---[  43]---> BDD-cost:    9
c ---[  42]---> BDD-cost:    9
c ---[  41]---> BDD-cost:    3
c ---[  40]---> BDD-cost:   10
c ---[  39]---> BDD-cost:    9
c ---[  38]---> BDD-cost:    9
c ---[  37]---> BDD-cost:    9
c ---[  36]---> BDD-cost:    9
c ---[  35]---> BDD-cost:    3
c ---[  34]---> BDD-cost:   10
c ---[  33]---> BDD-cost:    8
c ---[  32]---> BDD-cost:    8
c ---[  31]---> BDD-cost:    8
c ---[  30]---> BDD-cost:    8
c ---[  29]---> BDD-cost:    3
c ---[  28]---> BDD-cost:   10
c ---[  27]---> BDD-cost:    8
c ---[  26]---> BDD-cost:    8
c ---[  25]---> BDD-cost:    8
c ---[  24]---> BDD-cost:    8
c ---[  22]---> BDD-cost:   10
c ---[  21]---> BDD-cost:    3
c ---[  20]---> BDD-cost:    9
c ---[  19]---> BDD-cost:    9
c ---[  18]---> BDD-cost:    9
c ---[  16]---> BDD-cost:   10
c ---[  15]---> BDD-cost:    3
c ---[  14]---> BDD-cost:    9
c ---[  13]---> BDD-cost:    9
c ---[  12]---> BDD-cost:    9
c ---[  10]---> BDD-cost:   10
c ---[   9]---> BDD-cost:    3
c ---[   8]---> BDD-cost:    9
c ---[   7]---> BDD-cost:    9
c ---[   6]---> BDD-cost:    9
c ---[   4]---> BDD-cost:    9
c ---[   3]---> BDD-cost:    3
c ---[   2]---> BDD-cost:    8
c ---[   1]---> BDD-cost:    8
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  136974   386371 |   45658       0        0     nan |  0.000 % |
c |       100 |  136958   386319 |   50223      98      400     4.1 |  6.776 % |
c |       250 |  136942   386267 |   55246     246     2083     8.5 |  6.784 % |
c |       476 |  136915   386207 |   60770     471     3476     7.4 |  6.802 % |
c |       813 |  136828   386012 |   66847     807     5963     7.4 |  6.858 % |
c |      1320 |  136727   385772 |   73532    1301    13310    10.2 |  6.920 % |
c |      2079 |  136696   385703 |   80885    2059    21977    10.7 |  6.941 % |
c |      3218 |  136509   385281 |   88974    3193    36342    11.4 |  7.060 % |
c |      4926 |  136435   385098 |   97871    4891    54411    11.1 |  7.109 % |
c |      7489 |  136392   385002 |  107659    7453    90936    12.2 |  7.137 % |
c |     11333 |  136258   384661 |  118425   11278   151608    13.4 |  7.222 % |
c |     17101 |  135693   383357 |  130267   16967   236451    13.9 |  7.615 % |
c |     25750 |  135442   382723 |  143294   25580   374080    14.6 |  7.770 % |
c |     38725 |  135230   382216 |  157623   38526   623273    16.2 |  7.912 % |
c |     58186 |  134907   381435 |  173386   57948  1013349    17.5 |  8.131 % |
c |     87380 |  134555   380614 |  190724   87063  1637273    18.8 |  8.397 % |
c |    131169 |  134042   379340 |  209797  130769  2791932    21.4 |  8.722 % |
c |    196853 |  133828   378809 |  230777  196431  5226112    26.6 |  8.856 % |
c |    295380 |  133420   377870 |  253854   71774  2364572    32.9 |  9.156 % |
c |    443170 |  132512   375752 |  279240  219500  7855049    35.8 |  9.886 % |
#### 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.93 0.98 0.93 2/54 30411
Raw data (stat): 30411 (runsolver) R 30410 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 543785896 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.94 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 4242 0 0 0 988 11 0 0 25 0 1 0 543785896 20410368 4065 4294967295 134512640 134672761 3221224544 3221223760 134557650 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4983 4065 603 41 0 4942 0
vsize: 19932
[startup+20.0011 s]
Raw data (loadavg): 0.95 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 4644 0 0 0 1986 12 0 0 25 0 1 0 543785896 22048768 4467 4294967295 134512640 134672761 3221224544 3221223668 134566077 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5383 4467 603 41 0 5342 0
vsize: 21532
[startup+30.0018 s]
Raw data (loadavg): 0.95 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 5203 0 0 0 2985 14 0 0 25 0 1 0 543785896 24322048 5026 4294967295 134512640 134672761 3221224544 3221223744 134557806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5938 5026 603 41 0 5897 0
vsize: 23752
[startup+40.0024 s]
Raw data (loadavg): 0.96 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 5731 0 0 0 3983 16 0 0 25 0 1 0 543785896 26472448 5554 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6463 5554 603 41 0 6422 0
vsize: 25852
[startup+50.0032 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 6191 0 0 0 4981 18 0 0 25 0 1 0 543785896 28479488 6014 4294967295 134512640 134672761 3221224544 3221223668 134566031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6953 6014 603 41 0 6912 0
vsize: 27812
[startup+60.0029 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 6534 0 0 0 5980 19 0 0 25 0 1 0 543785896 29822976 6357 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7281 6357 603 41 0 7240 0
vsize: 29124
[startup+70.0036 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 6868 0 0 0 6979 20 0 0 25 0 1 0 543785896 31166464 6691 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7609 6691 603 41 0 7568 0
vsize: 30436
[startup+80.0043 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 7310 0 0 0 7977 22 0 0 25 0 1 0 543785896 33046528 7133 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8068 7133 603 41 0 8027 0
vsize: 32272
[startup+90.0051 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 7706 0 0 0 8976 24 0 0 25 0 1 0 543785896 34521088 7529 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8428 7529 603 41 0 8387 0
vsize: 33712
[startup+100.005 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 8035 0 0 0 9974 25 0 0 25 0 1 0 543785896 35868672 7858 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8757 7858 603 41 0 8716 0
vsize: 35028
[startup+110.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 8492 0 0 0 10973 26 0 0 25 0 1 0 543785896 38256640 8315 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9340 8315 603 41 0 9299 0
vsize: 37360
[startup+120.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 8948 0 0 0 11972 28 0 0 25 0 1 0 543785896 40120320 8771 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9795 8771 603 41 0 9754 0
vsize: 39180
[startup+130.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 9336 0 0 0 12970 29 0 0 25 0 1 0 543785896 41721856 9159 4294967295 134512640 134672761 3221224544 3221223712 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10186 9159 603 41 0 10145 0
vsize: 40744
[startup+140.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 9676 0 0 0 13970 30 0 0 25 0 1 0 543785896 43053056 9499 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10511 9499 603 41 0 10470 0
vsize: 42044
[startup+150.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 9941 0 0 0 14969 31 0 0 25 0 1 0 543785896 44142592 9764 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10777 9764 603 41 0 10736 0
vsize: 43108
[startup+160.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 10303 0 0 0 15967 33 0 0 25 0 1 0 543785896 45625344 10126 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11139 10126 603 41 0 11098 0
vsize: 44556
[startup+170.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 10627 0 0 0 16965 35 0 0 25 0 1 0 543785896 46829568 10450 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11433 10450 603 41 0 11392 0
vsize: 45732
[startup+180.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 11354 0 0 0 17963 37 0 0 25 0 1 0 543785896 49790976 11177 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12156 11177 603 41 0 12115 0
vsize: 48624
[startup+190.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 11728 0 0 0 18962 39 0 0 25 0 1 0 543785896 51290112 11551 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12522 11551 603 41 0 12481 0
vsize: 50088
[startup+200.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 12241 0 0 0 19960 41 0 0 25 0 1 0 543785896 53313536 12064 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13016 12064 603 41 0 12975 0
vsize: 52064
[startup+210.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 12626 0 0 0 20958 42 0 0 25 0 1 0 543785896 54931456 12449 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13411 12449 603 41 0 13370 0
vsize: 53644
[startup+220.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 12959 0 0 0 21958 43 0 0 25 0 1 0 543785896 56274944 12782 4294967295 134512640 134672761 3221224544 3221223712 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13739 12782 603 41 0 13698 0
vsize: 54956
[startup+230.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13250 0 0 0 22957 43 0 0 25 0 1 0 543785896 57470976 13073 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14031 13073 603 41 0 13990 0
vsize: 56124
[startup+240.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13480 0 0 0 23957 44 0 0 25 0 1 0 543785896 58396672 13303 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+250.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13480 0 0 0 24957 44 0 0 25 0 1 0 543785896 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+260.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13480 0 0 0 25957 44 0 0 25 0 1 0 543785896 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+270.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13480 0 0 0 26957 45 0 0 25 0 1 0 543785896 58396672 13303 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+280.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13480 0 0 0 27957 45 0 0 25 0 1 0 543785896 58396672 13303 4294967295 134512640 134672761 3221224544 3221223648 134555130 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+290.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13480 0 0 0 28957 45 0 0 25 0 1 0 543785896 58396672 13303 4294967295 134512640 134672761 3221224544 3221223728 134558651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+300.016 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13480 0 0 0 29956 45 0 0 25 0 1 0 543785896 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+310.016 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13480 0 0 0 30956 46 0 0 25 0 1 0 543785896 58396672 13303 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+320.017 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13480 0 0 0 31956 46 0 0 25 0 1 0 543785896 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+330.016 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13480 0 0 0 32955 46 0 0 25 0 1 0 543785896 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+340.017 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13480 0 0 0 33956 46 0 0 25 0 1 0 543785896 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+350.018 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13480 0 0 0 34955 47 0 0 25 0 1 0 543785896 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+360.019 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13480 0 0 0 35955 47 0 0 25 0 1 0 543785896 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+370.019 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13480 0 0 0 36955 47 0 0 25 0 1 0 543785896 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+380.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13480 0 0 0 37955 47 0 0 25 0 1 0 543785896 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+390.021 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13480 0 0 0 38955 48 0 0 25 0 1 0 543785896 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+400.022 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13480 0 0 0 39955 48 0 0 25 0 1 0 543785896 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+410.022 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13480 0 0 0 40954 48 0 0 25 0 1 0 543785896 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+420.023 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13480 0 0 0 41954 49 0 0 25 0 1 0 543785896 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+430.023 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30411
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13480 0 0 0 42954 49 0 0 25 0 1 0 543785896 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+440.028 s]
Raw data (loadavg): 1.15 1.02 0.94 2/54 30464
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13480 0 0 0 43954 49 0 0 25 0 1 0 543785896 58396672 13303 4294967295 134512640 134672761 3221224544 3221223680 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+450.035 s]
Raw data (loadavg): 1.12 1.02 0.94 2/54 30464
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13480 0 0 0 44955 49 0 0 25 0 1 0 543785896 58396672 13303 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+460.071 s]
Raw data (loadavg): 1.10 1.01 0.94 2/54 30464
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13480 0 0 0 45958 49 0 0 25 0 1 0 543785896 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+470.071 s]
Raw data (loadavg): 1.09 1.01 0.94 2/54 30464
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13480 0 0 0 46958 49 0 0 25 0 1 0 543785896 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+480.072 s]
Raw data (loadavg): 1.07 1.01 0.94 2/54 30464
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13480 0 0 0 47959 49 0 0 25 0 1 0 543785896 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+490.073 s]
Raw data (loadavg): 1.06 1.01 0.94 2/54 30464
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13480 0 0 0 48959 49 0 0 25 0 1 0 543785896 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+500.072 s]
Raw data (loadavg): 1.05 1.01 0.94 2/54 30466
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13480 0 0 0 49959 49 0 0 25 0 1 0 543785896 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+510.072 s]
Raw data (loadavg): 1.04 1.01 0.94 2/54 30466
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13480 0 0 0 50959 49 0 0 25 0 1 0 543785896 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+520.073 s]
Raw data (loadavg): 1.04 1.01 0.94 2/54 30466
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13480 0 0 0 51959 49 0 0 25 0 1 0 543785896 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+530.073 s]
Raw data (loadavg): 1.03 1.01 0.94 2/54 30466
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13480 0 0 0 52960 49 0 0 25 0 1 0 543785896 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+540.074 s]
Raw data (loadavg): 1.03 1.01 0.94 2/54 30466
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13480 0 0 0 53960 49 0 0 25 0 1 0 543785896 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+550.075 s]
Raw data (loadavg): 1.02 1.01 0.94 2/54 30466
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13480 0 0 0 54960 49 0 0 25 0 1 0 543785896 58396672 13303 4294967295 134512640 134672761 3221224544 3221223680 134560640 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+560.075 s]
Raw data (loadavg): 1.02 1.00 0.94 2/54 30466
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13494 0 0 0 55960 50 0 0 25 0 1 0 543785896 58396672 13317 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14257 13317 603 41 0 14216 0
vsize: 57028
[startup+570.075 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 30466
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13495 0 0 0 56960 50 0 0 25 0 1 0 543785896 58396672 13318 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14257 13318 603 41 0 14216 0
vsize: 57028
[startup+580.076 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 30466
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13523 0 0 0 57960 50 0 0 25 0 1 0 543785896 58568704 13346 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14299 13346 603 41 0 14258 0
vsize: 57196
[startup+590.077 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 30466
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13524 0 0 0 58961 50 0 0 25 0 1 0 543785896 58568704 13347 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14299 13347 603 41 0 14258 0
vsize: 57196
[startup+600.076 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 30466
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13529 0 0 0 59960 50 0 0 25 0 1 0 543785896 58568704 13352 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14299 13352 603 41 0 14258 0
vsize: 57196
[startup+610.076 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 30466
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13529 0 0 0 60961 50 0 0 25 0 1 0 543785896 58568704 13352 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14299 13352 603 41 0 14258 0
vsize: 57196
[startup+620.077 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30466
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13540 0 0 0 61961 50 0 0 25 0 1 0 543785896 58732544 13363 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14339 13363 603 41 0 14298 0
vsize: 57356
[startup+630.077 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30466
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13540 0 0 0 62960 51 0 0 25 0 1 0 543785896 58732544 13363 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14339 13363 603 41 0 14298 0
vsize: 57356
[startup+640.078 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30466
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13567 0 0 0 63960 51 0 0 25 0 1 0 543785896 58896384 13390 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14379 13390 603 41 0 14338 0
vsize: 57516
[startup+650.078 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30466
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13567 0 0 0 64961 51 0 0 25 0 1 0 543785896 58896384 13390 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14379 13390 603 41 0 14338 0
vsize: 57516
[startup+660.078 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30466
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13604 0 0 0 65961 51 0 0 25 0 1 0 543785896 59092992 13427 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14427 13427 603 41 0 14386 0
vsize: 57708
[startup+670.078 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30466
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13611 0 0 0 66961 51 0 0 25 0 1 0 543785896 59092992 13434 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14427 13434 603 41 0 14386 0
vsize: 57708
[startup+680.079 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30466
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13611 0 0 0 67961 51 0 0 25 0 1 0 543785896 59092992 13434 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14427 13434 603 41 0 14386 0
vsize: 57708
[startup+690.08 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30466
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13627 0 0 0 68961 51 0 0 25 0 1 0 543785896 59092992 13450 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14427 13450 603 41 0 14386 0
vsize: 57708
[startup+700.08 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30466
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13628 0 0 0 69961 51 0 0 25 0 1 0 543785896 59092992 13451 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14427 13451 603 41 0 14386 0
vsize: 57708
[startup+710.079 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30466
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13628 0 0 0 70961 51 0 0 25 0 1 0 543785896 59092992 13451 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14427 13451 603 41 0 14386 0
vsize: 57708
[startup+720.08 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30466
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13638 0 0 0 71961 51 0 0 25 0 1 0 543785896 59256832 13461 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14467 13461 603 41 0 14426 0
vsize: 57868
[startup+730.08 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30466
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13638 0 0 0 72962 51 0 0 25 0 1 0 543785896 59256832 13461 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14467 13461 603 41 0 14426 0
vsize: 57868
[startup+740.081 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30466
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13639 0 0 0 73961 52 0 0 25 0 1 0 543785896 59256832 13462 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14467 13462 603 41 0 14426 0
vsize: 57868
[startup+750.082 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30466
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13653 0 0 0 74960 52 0 0 25 0 1 0 543785896 59256832 13476 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14467 13476 603 41 0 14426 0
vsize: 57868
[startup+760.081 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30466
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13737 0 0 0 75959 53 0 0 25 0 1 0 543785896 59523072 13560 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14532 13560 603 41 0 14491 0
vsize: 58128
[startup+770.082 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30466
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13814 0 0 0 76959 53 0 0 25 0 1 0 543785896 59928576 13637 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14631 13637 603 41 0 14590 0
vsize: 58524
[startup+780.081 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30466
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13902 0 0 0 77959 53 0 0 25 0 1 0 543785896 60334080 13725 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14730 13725 603 41 0 14689 0
vsize: 58920
[startup+790.082 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30466
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 13979 0 0 0 78959 53 0 0 25 0 1 0 543785896 60743680 13802 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14830 13802 603 41 0 14789 0
vsize: 59320
[startup+800.082 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30468
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 14082 0 0 0 79959 53 0 0 25 0 1 0 543785896 61169664 13905 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14934 13905 603 41 0 14893 0
vsize: 59736
[startup+810.082 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30468
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 14193 0 0 0 80959 54 0 0 25 0 1 0 543785896 61579264 14016 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15034 14016 603 41 0 14993 0
vsize: 60136
[startup+820.083 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30468
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 14279 0 0 0 81959 54 0 0 25 0 1 0 543785896 61984768 14102 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15133 14102 603 41 0 15092 0
vsize: 60532
[startup+830.083 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30468
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 14354 0 0 0 82959 54 0 0 25 0 1 0 543785896 62251008 14177 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15198 14177 603 41 0 15157 0
vsize: 60792
[startup+840.084 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30468
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 14441 0 0 0 83959 55 0 0 25 0 1 0 543785896 62656512 14264 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15297 14264 603 41 0 15256 0
vsize: 61188
[startup+850.083 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30468
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 14504 0 0 0 84959 55 0 0 25 0 1 0 543785896 62922752 14327 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15362 14327 603 41 0 15321 0
vsize: 61448
[startup+860.083 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30468
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 14565 0 0 0 85958 55 0 0 25 0 1 0 543785896 63193088 14388 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15428 14388 603 41 0 15387 0
vsize: 61712
[startup+870.084 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30468
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 14615 0 0 0 86958 56 0 0 25 0 1 0 543785896 63328256 14438 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15461 14438 603 41 0 15420 0
vsize: 61844
[startup+880.084 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30468
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 14677 0 0 0 87958 56 0 0 25 0 1 0 543785896 63733760 14500 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15560 14500 603 41 0 15519 0
vsize: 62240
[startup+890.085 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30468
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 14751 0 0 0 88958 57 0 0 25 0 1 0 543785896 64049152 14574 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15637 14574 603 41 0 15596 0
vsize: 62548
[startup+900.085 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30468
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 14810 0 0 0 89957 57 0 0 25 0 1 0 543785896 64315392 14633 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15702 14633 603 41 0 15661 0
vsize: 62808
[startup+910.085 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30468
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 14870 0 0 0 90957 57 0 0 25 0 1 0 543785896 64450560 14693 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15735 14693 603 41 0 15694 0
vsize: 62940
[startup+920.085 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30468
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 14929 0 0 0 91957 58 0 0 25 0 1 0 543785896 64720896 14752 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15801 14752 603 41 0 15760 0
vsize: 63204
[startup+930.086 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30468
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 15167 0 0 0 92957 59 0 0 25 0 1 0 543785896 65650688 14990 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16028 14990 603 41 0 15987 0
vsize: 64112
[startup+940.087 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30468
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 15228 0 0 0 93957 59 0 0 25 0 1 0 543785896 65921024 15051 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16094 15051 603 41 0 16053 0
vsize: 64376
[startup+950.088 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30468
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 15297 0 0 0 94956 59 0 0 25 0 1 0 543785896 66187264 15120 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15120 603 41 0 16118 0
vsize: 64636
[startup+960.088 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30468
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 15424 0 0 0 95956 59 0 0 25 0 1 0 543785896 66723840 15247 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16290 15247 603 41 0 16249 0
vsize: 65160
[startup+970.089 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30468
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 15529 0 0 0 96955 60 0 0 25 0 1 0 543785896 67125248 15352 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16388 15352 603 41 0 16347 0
vsize: 65552
[startup+980.089 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30468
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 15595 0 0 0 97955 60 0 0 25 0 1 0 543785896 67448832 15418 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16467 15418 603 41 0 16426 0
vsize: 65868
[startup+990.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30468
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 15665 0 0 0 98955 60 0 0 25 0 1 0 543785896 67719168 15488 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16533 15488 603 41 0 16492 0
vsize: 66132
[startup+1000.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30468
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 15734 0 0 0 99955 61 0 0 25 0 1 0 543785896 67989504 15557 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16599 15557 603 41 0 16558 0
vsize: 66396
[startup+1010.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30468
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 15786 0 0 0 100955 61 0 0 25 0 1 0 543785896 68255744 15609 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16664 15609 603 41 0 16623 0
vsize: 66656
[startup+1020.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30468
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 15872 0 0 0 101955 61 0 0 25 0 1 0 543785896 68681728 15695 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16768 15695 603 41 0 16727 0
vsize: 67072
[startup+1030.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30468
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 16195 0 0 0 102954 62 0 0 25 0 1 0 543785896 70053888 16018 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17103 16018 603 41 0 17062 0
vsize: 68412
[startup+1040.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30468
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 16259 0 0 0 103954 63 0 0 25 0 1 0 543785896 70320128 16082 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17168 16082 603 41 0 17127 0
vsize: 68672
[startup+1050.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30468
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 16342 0 0 0 104954 63 0 0 25 0 1 0 543785896 70590464 16165 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17234 16165 603 41 0 17193 0
vsize: 68936
[startup+1060.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30468
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 16401 0 0 0 105953 64 0 0 25 0 1 0 543785896 70856704 16224 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17299 16224 603 41 0 17258 0
vsize: 69196
[startup+1070.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30468
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 16468 0 0 0 106953 64 0 0 25 0 1 0 543785896 71122944 16291 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17364 16291 603 41 0 17323 0
vsize: 69456
[startup+1080.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30468
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 16517 0 0 0 107953 64 0 0 25 0 1 0 543785896 71258112 16340 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17397 16340 603 41 0 17356 0
vsize: 69588
[startup+1090.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30468
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 16576 0 0 0 108953 64 0 0 25 0 1 0 543785896 71524352 16399 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17462 16399 603 41 0 17421 0
vsize: 69848
[startup+1100.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30468
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 16675 0 0 0 109953 65 0 0 25 0 1 0 543785896 71954432 16498 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17567 16498 603 41 0 17526 0
vsize: 70268
[startup+1110.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30468
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 16759 0 0 0 110953 65 0 0 25 0 1 0 543785896 72355840 16582 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17665 16582 603 41 0 17624 0
vsize: 70660
[startup+1120.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30468
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 16892 0 0 0 111953 65 0 0 25 0 1 0 543785896 72892416 16715 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17796 16715 603 41 0 17755 0
vsize: 71184
[startup+1130.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30468
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 16989 0 0 0 112953 66 0 0 25 0 1 0 543785896 73293824 16812 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17894 16812 603 41 0 17853 0
vsize: 71576
[startup+1140.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30468
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 17054 0 0 0 113952 66 0 0 25 0 1 0 543785896 73560064 16877 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17959 16877 603 41 0 17918 0
vsize: 71836
[startup+1150.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30468
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 17212 0 0 0 114952 67 0 0 25 0 1 0 543785896 74125312 17035 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18097 17035 603 41 0 18056 0
vsize: 72388
[startup+1160.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30468
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 17428 0 0 0 115952 67 0 0 25 0 1 0 543785896 76120064 17251 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18584 17251 603 41 0 18543 0
vsize: 74336
[startup+1170.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30468
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 17502 0 0 0 116952 67 0 0 25 0 1 0 543785896 76394496 17325 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18651 17325 603 41 0 18610 0
vsize: 74604
[startup+1180.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30468
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 17554 0 0 0 117952 67 0 0 25 0 1 0 543785896 76656640 17377 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18715 17377 603 41 0 18674 0
vsize: 74860
[startup+1190.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30468
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 17601 0 0 0 118952 67 0 0 25 0 1 0 543785896 76791808 17424 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18748 17424 603 41 0 18707 0
vsize: 74992
[startup+1200.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30468
Raw data (stat): 30411 (minisat+) R 30410 26298 26297 0 -1 0 17650 0 0 0 119952 68 0 0 25 0 1 0 543785896 76926976 17473 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18781 17473 603 41 0 18740 0
vsize: 75124
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.13 s]
Raw data (loadavg): 1.00 1.00 0.94 1/54 30468
Raw data (stat): 30411 (minisat+) Z 30410 26298 26297 0 -1 12 17652 0 0 0 119952 71 0 0 25 0 1 0 543785896 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.13
CPU time (s): 1200.24
CPU user time (s): 1199.52
CPU system time (s): 0.714891
CPU usage (%): 100.009
Max. virtual memory (Kb): 75124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####