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-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-vpm1.opb
MD5SUM	ec9e3281577e2d3f7b25c1cc88cac9ea
Bench Category	optimization, small integers (OPTSMALLINT)
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	102400
Number of bits of the biggest number in a constraint	17
Biggest sum of numbers in a constraint	615983
Number of bits of the biggest sum of numbers	20
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.06884
Number of variables	2124
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	64
Trace number 17998

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc1 THE 2005-04-21 13:02:59 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18941 boxname=wulflinc1 idbench=1457 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ec9e3281577e2d3f7b25c1cc88cac9ea  /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-vpm1.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-vpm1.opb /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-vpm1.opb
IDLAUNCH: 18941
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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.053
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:        775644 kB
Buffers:          4024 kB
Cached:         229828 kB
SwapCached:          0 kB
Active:          49304 kB
Inactive:       187700 kB
HighTotal:      131008 kB
HighFree:        46088 kB
LowTotal:       903652 kB
LowFree:        729556 kB
SwapTotal:     2097136 kB
SwapFree:      2096968 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7220 kB
Slab:            16200 kB
Committed_AS:    92816 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 13:23:01 (client local time) WITH STATUS 0 IN 1200.21 SECONDS
stats: 18941 7 1200.21 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:    7
c ---[ 484]---> BDD-cost:    7
c ---[ 483]---> BDD-cost:    7
c ---[ 482]---> BDD-cost:    7
c ---[ 481]---> BDD-cost:    7
c ---[ 480]---> BDD-cost:    7
c ---[ 479]---> BDD-cost:    7
c ---[ 478]---> BDD-cost:    7
c ---[ 477]---> BDD-cost:    7
c ---[ 474]---> BDD-cost:    7
c ---[ 473]---> BDD-cost:    7
c ---[ 472]---> BDD-cost:    7
c ---[ 471]---> BDD-cost:    7
c ---[ 468]---> BDD-cost:    7
c ---[ 467]---> BDD-cost:    7
c ---[ 466]---> BDD-cost:    7
c ---[ 465]---> BDD-cost:    7
c ---[ 462]---> BDD-cost:    7
c ---[ 459]---> BDD-cost:    7
c ---[ 458]---> BDD-cost:    7
c ---[ 457]---> BDD-cost:    7
c ---[ 454]---> BDD-cost:    7
c ---[ 453]---> BDD-cost:    7
c ---[ 452]---> BDD-cost:    7
c ---[ 451]---> BDD-cost:    7
c ---[ 450]---> BDD-cost:    7
c ---[ 448]---> BDD-cost:    7
c ---[ 447]---> BDD-cost:    7
c ---[ 446]---> BDD-cost:    7
c ---[ 445]---> BDD-cost:    7
c ---[ 444]---> BDD-cost:    7
c ---[ 441]---> BDD-cost:    7
c ---[ 440]---> BDD-cost:    7
c ---[ 439]---> BDD-cost:    7
c ---[ 433]---> BDD-cost:    7
c ---[ 427]---> BDD-cost:    7
c ---[ 422]---> BDD-cost:    7
c ---[ 421]---> BDD-cost:    7
c ---[ 415]---> BDD-cost:    7
c ---[ 409]---> BDD-cost:    7
c ---[ 408]---> BDD-cost:    7
c ---[ 402]---> BDD-cost:    7
c ---[ 397]---> BDD-cost:    7
c ---[ 396]---> BDD-cost:    7
c ---[ 391]---> BDD-cost:    7
c ---[ 390]---> BDD-cost:    7
c ---[ 386]---> BDD-cost:    7
c ---[ 385]---> BDD-cost:    7
c ---[ 384]---> BDD-cost:    7
c ---[ 380]---> BDD-cost:    7
c ---[ 379]---> BDD-cost:    7
c ---[ 378]---> BDD-cost:    7
c ---[ 374]---> BDD-cost:    7
c ---[ 373]---> BDD-cost:    7
c ---[ 372]---> BDD-cost:    7
c ---[ 368]---> BDD-cost:    7
c ---[ 367]---> BDD-cost:    7
c ---[ 366]---> BDD-cost:    7
c ---[ 365]---> BDD-cost:    7
c ---[ 364]---> BDD-cost:    7
c ---[ 359]---> BDD-cost:    7
c ---[ 353]---> BDD-cost:    7
c ---[ 347]---> BDD-cost:    7
c ---[ 339]---> BDD-cost:    7
c ---[ 333]---> BDD-cost:    7
c ---[ 327]---> BDD-cost:    7
c ---[ 321]---> BDD-cost:    7
c ---[ 317]---> BDD-cost:   14
c ---[ 316]---> BDD-cost:   14
c ---[ 315]---> BDD-cost:   14
c ---[ 314]---> BDD-cost:   14
c ---[ 313]---> BDD-cost:   14
c ---[ 312]---> BDD-cost:   14
c ---[ 310]---> BDD-cost:   14
c ---[ 309]---> BDD-cost:   14
c ---[ 308]---> BDD-cost:   14
c ---[ 307]---> BDD-cost:   14
c ---[ 306]---> BDD-cost:   14
c ---[ 302]---> BDD-cost:   13
c ---[ 301]---> BDD-cost:   13
c ---[ 300]---> BDD-cost:   13
c ---[ 295]---> BDD-cost:   13
c ---[ 294]---> BDD-cost:   13
c ---[ 290]---> BDD-cost:   15
c ---[ 289]---> BDD-cost:   15
c ---[ 288]---> BDD-cost:   15
c ---[ 287]---> BDD-cost:   13
c ---[ 286]---> BDD-cost:   13
c ---[ 285]---> BDD-cost:   13
c ---[ 284]---> BDD-cost:   13
c ---[ 283]---> BDD-cost:   13
c ---[ 282]---> BDD-cost:   13
c ---[ 280]---> BDD-cost:   13
c ---[ 279]---> BDD-cost:   13
c ---[ 278]---> BDD-cost:   13
c ---[ 277]---> BDD-cost:   13
c ---[ 276]---> BDD-cost:   13
c ---[ 274]---> Sorter-cost: 1988     Base: 2 2 2 5 5 2 2 2 2 2 3
c ---[ 264]---> Sorter-cost: 1826     Base: 2 2 2 5 5 2 2 2 3 2 2 2
c ---[ 260]---> Adder-cost: 262   maxlim: 300367   bits: 19/19
c ---[ 258]---> Adder-cost: 262   maxlim: 300367   bits: 19/19
c ---[ 256]---> Sorter-cost: 2565     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 254]---> Sorter-cost: 2565     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 252]---> Adder-cost: 262   maxlim: 261967   bits: 19/18
c ---[ 250]---> Sorter-cost: 1411     Base: 2 2 2 2 5 5 2 2 2 2 2
c ---[ 248]---> Sorter-cost: 2230     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 246]---> Sorter-cost: 2232     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 244]---> Sorter-cost: 2232     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 242]---> Sorter-cost: 2159     Base: 2 2 2 2 2 2 2 2 2 2 3 2 2
c ---[ 236]---> Sorter-cost: 1318     Base: 2 2 2 2 5 5 2 2 2 2 2
c ---[ 234]---> Sorter-cost: 2540     Base: 2 2 2 2 5 5 2 2 2 2 2 2
c ---[ 232]---> Sorter-cost: 1903     Base: 2 2 2 2 2 2 2 2 2 2 2 3
c ---[ 224]---> Sorter-cost: 1582     Base: 2 2 2 5 5 2 2 2 2 2 3
c ---[ 222]---> Adder-cost: 260   maxlim: 219983   bits: 19/18
c ---[ 216]---> Sorter-cost: 1742     Base: 2 2 2 5 5 2 2 2 2 2 2
c ---[ 214]---> Sorter-cost: 2471     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 212]---> Sorter-cost: 2473     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 210]---> Sorter-cost: 3095     Base: 2 2 2 2 2 3 5 2 2 2 5
c ---[ 208]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[ 206]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[ 204]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[ 202]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[ 200]---> Sorter-cost: 1882     Base: 2 2 2 2 5 5 2 2 2 5
c ---[ 198]---> Sorter-cost: 3211     Base: 2 2 2 2 5 5 2 2 2 2 5
c ---[ 196]---> Adder-cost: 254   maxlim: 123183   bits: 18/17
c ---[ 194]---> Adder-cost: 254   maxlim: 123183   bits: 18/17
c ---[ 192]---> Adder-cost: 254   maxlim: 123183   bits: 18/17
c ---[ 191]---> BDD-cost:   33
c ---[ 190]---> Sorter-cost:  269     Base: 2 2 2 2 2 2
c ---[ 189]---> Sorter-cost:  283     Base: 2 2 2 2 2 2
c ---[ 188]---> Sorter-cost:  540     Base: 2 2 2 2 2 2
c ---[ 187]---> Sorter-cost:  761     Base: 2 2 2 2 2 2
c ---[ 186]---> Sorter-cost:  655     Base: 2 2 2 2 2 2
c ---[ 185]---> BDD-cost:   33
c ---[ 184]---> Sorter-cost:  269     Base: 2 2 2 2 2 2
c ---[ 183]---> Sorter-cost:  283     Base: 2 2 2 2 2 2
c ---[ 182]---> Sorter-cost:  520     Base: 2 2 2 2 2 2
c ---[ 181]---> Sorter-cost:  707     Base: 2 2 2 2 2 2
c ---[ 180]---> Sorter-cost:  705     Base: 2 2 2 2 2 2
c ---[ 179]---> BDD-cost:   33
c ---[ 178]---> Sorter-cost:  269     Base: 2 2 2 2 2 2
c ---[ 177]---> Sorter-cost:  274     Base: 2 2 2 2 2 2
c ---[ 176]---> Sorter-cost:  527     Base: 2 2 2 2 2 2
c ---[ 175]---> Sorter-cost:  720     Base: 2 2 2 2 2 2
c ---[ 174]---> Sorter-cost:  692     Base: 2 2 2 2 2 2
c ---[ 173]---> BDD-cost:   33
c ---[ 172]---> Sorter-cost:  253     Base: 2 2 2 2 2 2
c ---[ 171]---> Sorter-cost:  274     Base: 2 2 2 2 2 2
c ---[ 170]---> Sorter-cost:  486     Base: 2 2 2 2 2 2
c ---[ 169]---> Sorter-cost:  695     Base: 2 2 2 2 2 2
c ---[ 168]---> Sorter-cost:  625     Base: 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:    7
c ---[ 157]---> BDD-cost:    7
c ---[ 156]---> BDD-cost:    3
c ---[ 155]---> BDD-cost:    3
c ---[ 154]---> BDD-cost:    3
c ---[ 153]---> BDD-cost:    3
c ---[ 152]---> BDD-cost:    7
c ---[ 151]---> BDD-cost:    7
c ---[ 150]---> BDD-cost:    3
c ---[ 149]---> BDD-cost:    3
c ---[ 148]---> BDD-cost:    3
c ---[ 147]---> BDD-cost:    3
c ---[ 146]---> BDD-cost:    7
c ---[ 145]---> BDD-cost:    7
c ---[ 144]---> BDD-cost:    3
c ---[ 142]---> BDD-cost:    7
c ---[ 141]---> BDD-cost:    3
c ---[ 140]---> BDD-cost:    3
c ---[ 139]---> BDD-cost:    3
c ---[ 138]---> BDD-cost:    7
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:    7
c ---[ 123]---> BDD-cost:    3
c ---[ 122]---> BDD-cost:    3
c ---[ 121]---> BDD-cost:    3
c ---[ 120]---> BDD-cost:    7
c ---[ 116]---> BDD-cost:    7
c ---[ 115]---> BDD-cost:    3
c ---[ 114]---> BDD-cost:    6
c ---[ 110]---> BDD-cost:    7
c ---[ 109]---> BDD-cost:    3
c ---[ 108]---> BDD-cost:    6
c ---[ 104]---> BDD-cost:    3
c ---[ 103]---> BDD-cost:    3
c ---[ 102]---> BDD-cost:    5
c ---[  98]---> BDD-cost:    7
c ---[  97]---> BDD-cost:    3
c ---[  96]---> BDD-cost:    6
c ---[  91]---> BDD-cost:    3
c ---[  90]---> BDD-cost:    3
c ---[  85]---> BDD-cost:    7
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:    6
c ---[  44]---> BDD-cost:    6
c ---[  43]---> BDD-cost:    6
c ---[  42]---> BDD-cost:    6
c ---[  41]---> BDD-cost:    3
c ---[  40]---> BDD-cost:    7
c ---[  39]---> BDD-cost:    6
c ---[  38]---> BDD-cost:    6
c ---[  37]---> BDD-cost:    6
c ---[  36]---> BDD-cost:    6
c ---[  35]---> BDD-cost:    3
c ---[  34]---> BDD-cost:    7
c ---[  33]---> BDD-cost:    5
c ---[  32]---> BDD-cost:    5
c ---[  31]---> BDD-cost:    5
c ---[  30]---> BDD-cost:    5
c ---[  29]---> BDD-cost:    3
c ---[  28]---> BDD-cost:    7
c ---[  27]---> BDD-cost:    5
c ---[  26]---> BDD-cost:    5
c ---[  25]---> BDD-cost:    5
c ---[  24]---> BDD-cost:    5
c ---[  22]---> BDD-cost:    7
c ---[  21]---> BDD-cost:    3
c ---[  20]---> BDD-cost:    6
c ---[  19]---> BDD-cost:    6
c ---[  18]---> BDD-cost:    6
c ---[  16]---> BDD-cost:    7
c ---[  15]---> BDD-cost:    3
c ---[  14]---> BDD-cost:    6
c ---[  13]---> BDD-cost:    6
c ---[  12]---> BDD-cost:    6
c ---[  10]---> BDD-cost:    7
c ---[   9]---> BDD-cost:    3
c ---[   8]---> BDD-cost:    6
c ---[   7]---> BDD-cost:    6
c ---[   6]---> BDD-cost:    6
c ---[   4]---> BDD-cost:    6
c ---[   3]---> BDD-cost:    3
c ---[   2]---> BDD-cost:    5
c ---[   1]---> BDD-cost:    5
c ---[   0]---> BDD-cost:    5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  148702   372357 |   49567       0        0     nan |  0.000 % |
c |       102 |  148663   372268 |   54523      91      571     6.3 |  6.112 % |
c |       252 |  148623   372175 |   59976     240     1215     5.1 |  6.130 % |
c |       477 |  148431   371737 |   65973     441     2603     5.9 |  6.238 % |
c |       814 |  148380   371623 |   72571     771     6041     7.8 |  6.267 % |
c |      1322 |  148107   370999 |   79828    1262    14839    11.8 |  6.415 % |
c |      2082 |  148014   370789 |   87810    2019    25198    12.5 |  6.464 % |
c |      3221 |  147842   370404 |   96592    3150    40977    13.0 |  6.555 % |
c |      4931 |  147649   369972 |  106251    4853   129701    26.7 |  6.657 % |
c |      7493 |  147029   368562 |  116876    7377   174686    23.7 |  7.012 % |
c |     11337 |  146754   367944 |  128564   11204   261201    23.3 |  7.159 % |
c |     17104 |  146347   367032 |  141420   16930   441753    26.1 |  7.388 % |
c |     25753 |  145430   364930 |  155562   25493   671805    26.4 |  7.919 % |
c |     38727 |  144832   363571 |  171118   38390  1228700    32.0 |  8.264 % |
c |     58188 |  144547   362924 |  188230   57831  2100447    36.3 |  8.431 % |
c |     87382 |  143561   360699 |  207053   86949  3225800    37.1 |  8.971 % |
c |    131171 |  143256   360011 |  227759  130707  5802653    44.4 |  9.140 % |
c |    196856 |  141913   356843 |  250534  196227  8645760    44.1 |  9.910 % |
c |    295382 |  140788   354278 |  275588   65040  2471770    38.0 | 10.564 % |
#### 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.91 0.95 0.94 2/56 27976
Raw data (stat): 27976 (runsolver) R 27975 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 430211956 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.93 0.95 0.94 2/56 27976
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 4777 0 0 0 986 13 0 0 25 0 1 0 430211956 21811200 4597 4294967295 134512640 134672761 3221224560 3221223748 134556588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5325 4597 603 41 0 5284 0
vsize: 21300
[startup+20.0012 s]
Raw data (loadavg): 0.94 0.96 0.94 2/56 27976
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 5119 0 0 0 1984 14 0 0 25 0 1 0 430211956 23285760 4939 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5685 4939 603 41 0 5644 0
vsize: 22740
[startup+30.002 s]
Raw data (loadavg): 0.95 0.96 0.94 2/56 27976
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 5402 0 0 0 2983 15 0 0 25 0 1 0 430211956 24354816 5222 4294967295 134512640 134672761 3221224560 3221223712 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5946 5222 603 41 0 5905 0
vsize: 23784
[startup+40.0018 s]
Raw data (loadavg): 0.95 0.96 0.94 2/56 27976
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 5838 0 0 0 3982 17 0 0 25 0 1 0 430211956 26333184 5658 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6429 5658 603 41 0 6388 0
vsize: 25716
[startup+50.0026 s]
Raw data (loadavg): 0.96 0.96 0.94 2/56 27976
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 6371 0 0 0 4980 19 0 0 25 0 1 0 430211956 28450816 6191 4294967295 134512640 134672761 3221224560 3221223692 134565974 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6946 6191 603 41 0 6905 0
vsize: 27784
[startup+60.0024 s]
Raw data (loadavg): 0.97 0.96 0.94 2/56 27976
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 6668 0 0 0 5979 20 0 0 25 0 1 0 430211956 29642752 6488 4294967295 134512640 134672761 3221224560 3221223664 134560291 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7237 6488 603 41 0 7196 0
vsize: 28948
[startup+70.0036 s]
Raw data (loadavg): 0.97 0.96 0.94 2/56 27976
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 6979 0 0 0 6978 21 0 0 25 0 1 0 430211956 30830592 6799 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7527 6799 603 41 0 7486 0
vsize: 30108
[startup+80.0039 s]
Raw data (loadavg): 0.98 0.96 0.94 2/56 27976
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 7247 0 0 0 7977 22 0 0 25 0 1 0 430211956 31887360 7067 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7785 7067 603 41 0 7744 0
vsize: 31140
[startup+90.0037 s]
Raw data (loadavg): 0.98 0.96 0.94 2/56 27976
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 7486 0 0 0 8976 23 0 0 25 0 1 0 430211956 32940032 7306 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8042 7306 603 41 0 8001 0
vsize: 32168
[startup+100.004 s]
Raw data (loadavg): 0.98 0.96 0.94 2/56 27976
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 7750 0 0 0 9976 24 0 0 25 0 1 0 430211956 34258944 7570 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8364 7570 603 41 0 8323 0
vsize: 33456
[startup+110.004 s]
Raw data (loadavg): 0.98 0.96 0.94 2/56 27976
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 8017 0 0 0 10975 25 0 0 25 0 1 0 430211956 35323904 7837 4294967295 134512640 134672761 3221224560 3221223732 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8624 7837 603 41 0 8583 0
vsize: 34496
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27978
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 8258 0 0 0 11974 25 0 0 25 0 1 0 430211956 36257792 8078 4294967295 134512640 134672761 3221224560 3221223704 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8852 8078 603 41 0 8811 0
vsize: 35408
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27978
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 8435 0 0 0 12974 26 0 0 25 0 1 0 430211956 36917248 8255 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9013 8255 603 41 0 8972 0
vsize: 36052
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27978
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 8606 0 0 0 13973 27 0 0 25 0 1 0 430211956 37707776 8426 4294967295 134512640 134672761 3221224560 3221223712 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9206 8426 603 41 0 9165 0
vsize: 36824
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27978
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 8837 0 0 0 14972 28 0 0 25 0 1 0 430211956 38629376 8657 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9431 8657 603 41 0 9390 0
vsize: 37724
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27978
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 9015 0 0 0 15971 28 0 0 25 0 1 0 430211956 39288832 8835 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9592 8835 603 41 0 9551 0
vsize: 38368
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27978
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 9182 0 0 0 16971 29 0 0 25 0 1 0 430211956 39948288 9002 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9753 9002 603 41 0 9712 0
vsize: 39012
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27978
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 9325 0 0 0 17971 29 0 0 25 0 1 0 430211956 40607744 9145 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9914 9145 603 41 0 9873 0
vsize: 39656
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27978
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 9563 0 0 0 18971 30 0 0 25 0 1 0 430211956 41533440 9383 4294967295 134512640 134672761 3221224560 3221223728 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10140 9383 603 41 0 10099 0
vsize: 40560
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27978
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 9744 0 0 0 19970 30 0 0 25 0 1 0 430211956 42344448 9564 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10338 9564 603 41 0 10297 0
vsize: 41352
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27978
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 9931 0 0 0 20970 31 0 0 25 0 1 0 430211956 43003904 9751 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10499 9751 603 41 0 10458 0
vsize: 41996
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27978
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 10114 0 0 0 21970 31 0 0 25 0 1 0 430211956 43810816 9934 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10696 9934 603 41 0 10655 0
vsize: 42784
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27978
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 10291 0 0 0 22969 32 0 0 25 0 1 0 430211956 44494848 10111 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10863 10111 603 41 0 10822 0
vsize: 43452
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27978
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 10445 0 0 0 23969 32 0 0 25 0 1 0 430211956 45154304 10265 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11024 10265 603 41 0 10983 0
vsize: 44096
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27978
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 10618 0 0 0 24969 33 0 0 25 0 1 0 430211956 45813760 10438 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11185 10438 603 41 0 11144 0
vsize: 44740
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27978
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 10788 0 0 0 25968 34 0 0 25 0 1 0 430211956 46604288 10608 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11378 10608 603 41 0 11337 0
vsize: 45512
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27978
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 10952 0 0 0 26968 34 0 0 25 0 1 0 430211956 47271936 10772 4294967295 134512640 134672761 3221224560 3221223664 134560224 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11541 10772 603 41 0 11500 0
vsize: 46164
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27978
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 11126 0 0 0 27966 36 0 0 25 0 1 0 430211956 47869952 10946 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11687 10946 603 41 0 11646 0
vsize: 46748
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27978
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 11298 0 0 0 28966 36 0 0 25 0 1 0 430211956 48668672 11118 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11882 11118 603 41 0 11841 0
vsize: 47528
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27978
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 11501 0 0 0 29965 37 0 0 25 0 1 0 430211956 49475584 11321 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12079 11321 603 41 0 12038 0
vsize: 48316
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27978
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 11664 0 0 0 30964 38 0 0 25 0 1 0 430211956 50683904 11484 4294967295 134512640 134672761 3221224560 3221223664 134560326 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12374 11484 603 41 0 12333 0
vsize: 49496
[startup+320.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27978
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 11859 0 0 0 31963 39 0 0 25 0 1 0 430211956 51482624 11679 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12569 11679 603 41 0 12528 0
vsize: 50276
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27978
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 11997 0 0 0 32962 40 0 0 25 0 1 0 430211956 52015104 11817 4294967295 134512640 134672761 3221224560 3221223696 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12699 11817 603 41 0 12658 0
vsize: 50796
[startup+340.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27978
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 12121 0 0 0 33962 40 0 0 25 0 1 0 430211956 52547584 11941 4294967295 134512640 134672761 3221224560 3221223560 1075350200 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12829 11941 603 41 0 12788 0
vsize: 51316
[startup+350.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27978
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 12385 0 0 0 34962 41 0 0 25 0 1 0 430211956 53608448 12205 4294967295 134512640 134672761 3221224560 3221223728 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13088 12205 603 41 0 13047 0
vsize: 52352
[startup+360.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27978
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 12618 0 0 0 35962 41 0 0 25 0 1 0 430211956 54538240 12438 4294967295 134512640 134672761 3221224560 3221223728 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13315 12438 603 41 0 13274 0
vsize: 53260
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27978
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 12970 0 0 0 36961 42 0 0 25 0 1 0 430211956 55996416 12790 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13671 12790 603 41 0 13630 0
vsize: 54684
[startup+380.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27978
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 13210 0 0 0 37961 43 0 0 25 0 1 0 430211956 56926208 13030 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13898 13030 603 41 0 13857 0
vsize: 55592
[startup+390.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27978
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 13371 0 0 0 38960 43 0 0 25 0 1 0 430211956 57606144 13191 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14064 13191 603 41 0 14023 0
vsize: 56256
[startup+400.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27978
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 13514 0 0 0 39960 44 0 0 25 0 1 0 430211956 58134528 13334 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14193 13334 603 41 0 14152 0
vsize: 56772
[startup+410.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27978
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 13626 0 0 0 40960 44 0 0 25 0 1 0 430211956 58531840 13446 4294967295 134512640 134672761 3221224560 3221223732 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14290 13446 603 41 0 14249 0
vsize: 57160
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27980
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 13790 0 0 0 41959 45 0 0 25 0 1 0 430211956 59334656 13610 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14486 13610 603 41 0 14445 0
vsize: 57944
[startup+430.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27980
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 13928 0 0 0 42959 46 0 0 25 0 1 0 430211956 59858944 13748 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14614 13748 603 41 0 14573 0
vsize: 58456
[startup+440.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27980
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 14041 0 0 0 43958 46 0 0 25 0 1 0 430211956 60256256 13861 4294967295 134512640 134672761 3221224560 3221223760 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14711 13861 603 41 0 14670 0
vsize: 58844
[startup+450.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27980
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 14276 0 0 0 44958 47 0 0 25 0 1 0 430211956 61333504 14096 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14974 14096 603 41 0 14933 0
vsize: 59896
[startup+460.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27980
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 14554 0 0 0 45958 47 0 0 25 0 1 0 430211956 62402560 14374 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15235 14374 603 41 0 15194 0
vsize: 60940
[startup+470.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27980
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 14810 0 0 0 46957 48 0 0 25 0 1 0 430211956 63348736 14630 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15466 14630 603 41 0 15425 0
vsize: 61864
[startup+480.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27980
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 15040 0 0 0 47957 48 0 0 25 0 1 0 430211956 64282624 14860 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15694 14860 603 41 0 15653 0
vsize: 62776
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27980
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 15232 0 0 0 48956 49 0 0 25 0 1 0 430211956 65085440 15052 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15890 15052 603 41 0 15849 0
vsize: 63560
[startup+500.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27980
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 15449 0 0 0 49956 49 0 0 25 0 1 0 430211956 66011136 15269 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16116 15269 603 41 0 16075 0
vsize: 64464
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27980
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 15579 0 0 0 50956 50 0 0 25 0 1 0 430211956 66543616 15399 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16246 15399 603 41 0 16205 0
vsize: 64984
[startup+520.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27980
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 15700 0 0 0 51955 50 0 0 25 0 1 0 430211956 67072000 15520 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16375 15520 603 41 0 16334 0
vsize: 65500
[startup+530.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27980
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 15823 0 0 0 52955 51 0 0 25 0 1 0 430211956 67465216 15643 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16471 15643 603 41 0 16430 0
vsize: 65884
[startup+540.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27980
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 15942 0 0 0 53954 51 0 0 25 0 1 0 430211956 68050944 15762 4294967295 134512640 134672761 3221224560 3221223744 134558903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16614 15762 603 41 0 16573 0
vsize: 66456
[startup+550.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27980
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 16064 0 0 0 54954 52 0 0 25 0 1 0 430211956 68579328 15884 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16743 15884 603 41 0 16702 0
vsize: 66972
[startup+560.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27980
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 16166 0 0 0 55953 53 0 0 25 0 1 0 430211956 68972544 15986 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16839 15986 603 41 0 16798 0
vsize: 67356
[startup+570.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27980
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 16325 0 0 0 56952 54 0 0 25 0 1 0 430211956 69632000 16145 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17000 16145 603 41 0 16959 0
vsize: 68000
[startup+580.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27980
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 16629 0 0 0 57951 55 0 0 25 0 1 0 430211956 70823936 16449 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17291 16449 603 41 0 17250 0
vsize: 69164
[startup+590.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27980
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 16826 0 0 0 58951 55 0 0 25 0 1 0 430211956 71639040 16646 4294967295 134512640 134672761 3221224560 3221223664 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17490 16646 603 41 0 17449 0
vsize: 69960
[startup+600.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27980
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 16957 0 0 0 59951 56 0 0 25 0 1 0 430211956 72163328 16777 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17618 16777 603 41 0 17577 0
vsize: 70472
[startup+610.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27980
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 17076 0 0 0 60951 56 0 0 25 0 1 0 430211956 72564736 16896 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17716 16896 603 41 0 17675 0
vsize: 70864
[startup+620.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27980
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 17195 0 0 0 61950 57 0 0 25 0 1 0 430211956 73093120 17015 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17845 17015 603 41 0 17804 0
vsize: 71380
[startup+630.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27980
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 17289 0 0 0 62950 57 0 0 25 0 1 0 430211956 73494528 17109 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17943 17109 603 41 0 17902 0
vsize: 71772
[startup+640.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27980
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 17371 0 0 0 63950 57 0 0 25 0 1 0 430211956 73756672 17191 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18007 17191 603 41 0 17966 0
vsize: 72028
[startup+650.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27980
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 17462 0 0 0 64949 58 0 0 25 0 1 0 430211956 74149888 17282 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18103 17282 603 41 0 18062 0
vsize: 72412
[startup+660.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27980
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 17553 0 0 0 65949 58 0 0 25 0 1 0 430211956 74555392 17373 4294967295 134512640 134672761 3221224560 3221223716 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18202 17373 603 41 0 18161 0
vsize: 72808
[startup+670.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27980
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 17650 0 0 0 66949 58 0 0 25 0 1 0 430211956 74948608 17470 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18298 17470 603 41 0 18257 0
vsize: 73192
[startup+680.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27980
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 17749 0 0 0 67949 58 0 0 25 0 1 0 430211956 75341824 17569 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18394 17569 603 41 0 18353 0
vsize: 73576
[startup+690.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27980
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 17835 0 0 0 68949 59 0 0 25 0 1 0 430211956 75603968 17655 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18458 17655 603 41 0 18417 0
vsize: 73832
[startup+700.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27980
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 17914 0 0 0 69949 59 0 0 25 0 1 0 430211956 76021760 17734 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18560 17734 603 41 0 18519 0
vsize: 74240
[startup+710.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27980
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 17999 0 0 0 70949 59 0 0 25 0 1 0 430211956 76283904 17819 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18624 17819 603 41 0 18583 0
vsize: 74496
[startup+720.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27982
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18076 0 0 0 71948 60 0 0 25 0 1 0 430211956 76677120 17896 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18720 17896 603 41 0 18679 0
vsize: 74880
[startup+730.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27982
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18156 0 0 0 72949 60 0 0 25 0 1 0 430211956 76939264 17976 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18784 17976 603 41 0 18743 0
vsize: 75136
[startup+740.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27982
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18236 0 0 0 73949 60 0 0 25 0 1 0 430211956 77201408 18056 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18848 18056 603 41 0 18807 0
vsize: 75392
[startup+750.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27982
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18316 0 0 0 74949 60 0 0 25 0 1 0 430211956 77602816 18136 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18946 18136 603 41 0 18905 0
vsize: 75784
[startup+760.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27982
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18400 0 0 0 75949 60 0 0 25 0 1 0 430211956 77869056 18220 4294967295 134512640 134672761 3221224560 3221223664 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19011 18220 603 41 0 18970 0
vsize: 76044
[startup+770.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27982
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18485 0 0 0 76949 60 0 0 25 0 1 0 430211956 78262272 18305 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19107 18305 603 41 0 19066 0
vsize: 76428
[startup+780.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27982
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18563 0 0 0 77949 60 0 0 25 0 1 0 430211956 78528512 18383 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19172 18383 603 41 0 19131 0
vsize: 76688
[startup+790.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27982
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18653 0 0 0 78949 60 0 0 25 0 1 0 430211956 78921728 18473 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19268 18473 603 41 0 19227 0
vsize: 77072
[startup+800.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27982
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18728 0 0 0 79949 61 0 0 25 0 1 0 430211956 79319040 18548 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19365 18548 603 41 0 19324 0
vsize: 77460
[startup+810.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27982
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18784 0 0 0 80949 61 0 0 25 0 1 0 430211956 79450112 18604 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19397 18604 603 41 0 19356 0
vsize: 77588
[startup+820.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27982
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18784 0 0 0 81949 61 0 0 25 0 1 0 430211956 79450112 18604 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19397 18604 603 41 0 19356 0
vsize: 77588
[startup+830.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27982
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18784 0 0 0 82949 61 0 0 25 0 1 0 430211956 79450112 18604 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19397 18604 603 41 0 19356 0
vsize: 77588
[startup+840.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27982
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18784 0 0 0 83949 61 0 0 25 0 1 0 430211956 79450112 18604 4294967295 134512640 134672761 3221224560 3221223664 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19397 18604 603 41 0 19356 0
vsize: 77588
[startup+850.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27982
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18784 0 0 0 84949 61 0 0 25 0 1 0 430211956 79450112 18604 4294967295 134512640 134672761 3221224560 3221223728 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19397 18604 603 41 0 19356 0
vsize: 77588
[startup+860.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27982
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18784 0 0 0 85949 61 0 0 25 0 1 0 430211956 79450112 18604 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19397 18604 603 41 0 19356 0
vsize: 77588
[startup+870.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27982
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18784 0 0 0 86950 61 0 0 25 0 1 0 430211956 79450112 18604 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19397 18604 603 41 0 19356 0
vsize: 77588
[startup+880.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27982
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18784 0 0 0 87950 61 0 0 25 0 1 0 430211956 79450112 18604 4294967295 134512640 134672761 3221224560 3221223732 134556669 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19397 18604 603 41 0 19356 0
vsize: 77588
[startup+890.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27982
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18784 0 0 0 88950 61 0 0 25 0 1 0 430211956 79450112 18604 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19397 18604 603 41 0 19356 0
vsize: 77588
[startup+900.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27982
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18784 0 0 0 89950 61 0 0 25 0 1 0 430211956 79450112 18604 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19397 18604 603 41 0 19356 0
vsize: 77588
[startup+910.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27982
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18784 0 0 0 90950 62 0 0 25 0 1 0 430211956 79450112 18604 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19397 18604 603 41 0 19356 0
vsize: 77588
[startup+920.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27982
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18786 0 0 0 91950 62 0 0 25 0 1 0 430211956 79450112 18606 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19397 18606 603 41 0 19356 0
vsize: 77588
[startup+930.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27982
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18786 0 0 0 92950 62 0 0 25 0 1 0 430211956 79450112 18606 4294967295 134512640 134672761 3221224560 3221223684 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19397 18606 603 41 0 19356 0
vsize: 77588
[startup+940.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27982
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18786 0 0 0 93950 62 0 0 25 0 1 0 430211956 79450112 18606 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19397 18606 603 41 0 19356 0
vsize: 77588
[startup+950.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27982
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18786 0 0 0 94950 62 0 0 25 0 1 0 430211956 79450112 18606 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19397 18606 603 41 0 19356 0
vsize: 77588
[startup+960.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27982
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18786 0 0 0 95950 62 0 0 25 0 1 0 430211956 79450112 18606 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19397 18606 603 41 0 19356 0
vsize: 77588
[startup+970.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27982
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18786 0 0 0 96950 62 0 0 25 0 1 0 430211956 79450112 18606 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19397 18606 603 41 0 19356 0
vsize: 77588
[startup+980.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27982
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18788 0 0 0 97950 62 0 0 25 0 1 0 430211956 79450112 18608 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19397 18608 603 41 0 19356 0
vsize: 77588
[startup+990.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27982
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18788 0 0 0 98950 62 0 0 25 0 1 0 430211956 79450112 18608 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19397 18608 603 41 0 19356 0
vsize: 77588
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27982
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18788 0 0 0 99950 63 0 0 25 0 1 0 430211956 79450112 18608 4294967295 134512640 134672761 3221224560 3221223664 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19397 18608 603 41 0 19356 0
vsize: 77588
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27982
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18788 0 0 0 100950 63 0 0 25 0 1 0 430211956 79450112 18608 4294967295 134512640 134672761 3221224560 3221223728 134560970 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19397 18608 603 41 0 19356 0
vsize: 77588
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27984
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18788 0 0 0 101950 63 0 0 25 0 1 0 430211956 79450112 18608 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19397 18608 603 41 0 19356 0
vsize: 77588
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27984
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18788 0 0 0 102950 63 0 0 25 0 1 0 430211956 79450112 18608 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19397 18608 603 41 0 19356 0
vsize: 77588
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27984
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18788 0 0 0 103950 63 0 0 25 0 1 0 430211956 79450112 18608 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19397 18608 603 41 0 19356 0
vsize: 77588
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27984
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18788 0 0 0 104950 63 0 0 25 0 1 0 430211956 79450112 18608 4294967295 134512640 134672761 3221224560 3221223744 134558513 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19397 18608 603 41 0 19356 0
vsize: 77588
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27984
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18788 0 0 0 105951 63 0 0 25 0 1 0 430211956 79450112 18608 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19397 18608 603 41 0 19356 0
vsize: 77588
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27984
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18788 0 0 0 106951 63 0 0 25 0 1 0 430211956 79450112 18608 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19397 18608 603 41 0 19356 0
vsize: 77588
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27984
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18788 0 0 0 107951 63 0 0 25 0 1 0 430211956 79450112 18608 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19397 18608 603 41 0 19356 0
vsize: 77588
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27984
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18788 0 0 0 108951 63 0 0 25 0 1 0 430211956 79450112 18608 4294967295 134512640 134672761 3221224560 3221223728 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19397 18608 603 41 0 19356 0
vsize: 77588
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27984
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18788 0 0 0 109951 63 0 0 25 0 1 0 430211956 79450112 18608 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19397 18608 603 41 0 19356 0
vsize: 77588
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27984
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18788 0 0 0 110952 63 0 0 25 0 1 0 430211956 79450112 18608 4294967295 134512640 134672761 3221224560 3221223728 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19397 18608 603 41 0 19356 0
vsize: 77588
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27984
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18789 0 0 0 111952 63 0 0 25 0 1 0 430211956 79450112 18609 4294967295 134512640 134672761 3221224560 3221223712 134541816 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19397 18609 603 41 0 19356 0
vsize: 77588
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27984
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18790 0 0 0 112952 63 0 0 25 0 1 0 430211956 79450112 18610 4294967295 134512640 134672761 3221224560 3221223632 134565153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19397 18610 603 41 0 19356 0
vsize: 77588
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27984
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18790 0 0 0 113952 63 0 0 25 0 1 0 430211956 79450112 18610 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19397 18610 603 41 0 19356 0
vsize: 77588
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27984
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18790 0 0 0 114952 63 0 0 25 0 1 0 430211956 79450112 18610 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19397 18610 603 41 0 19356 0
vsize: 77588
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27984
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18790 0 0 0 115953 63 0 0 25 0 1 0 430211956 79450112 18610 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19397 18610 603 41 0 19356 0
vsize: 77588
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27984
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18790 0 0 0 116953 63 0 0 25 0 1 0 430211956 79450112 18610 4294967295 134512640 134672761 3221224560 3221223724 134565024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19397 18610 603 41 0 19356 0
vsize: 77588
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27984
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18791 0 0 0 117953 63 0 0 25 0 1 0 430211956 79450112 18611 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19397 18611 603 41 0 19356 0
vsize: 77588
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27984
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18791 0 0 0 118953 63 0 0 25 0 1 0 430211956 79450112 18611 4294967295 134512640 134672761 3221224560 3221223664 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19397 18611 603 41 0 19356 0
vsize: 77588
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/56 27984
Raw data (stat): 27976 (minisat+) R 27975 12452 12451 0 -1 0 18791 0 0 0 119953 63 0 0 25 0 1 0 430211956 79450112 18611 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19397 18611 603 41 0 19356 0
vsize: 77588
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.94 1/56 27984
Raw data (stat): 27976 (minisat+) Z 27975 12452 12451 0 -1 12 18793 0 0 0 119953 66 0 0 25 0 1 0 430211956 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.06
CPU time (s): 1200.21
CPU user time (s): 1199.54
CPU system time (s): 0.668898
CPU usage (%): 100.012
Max. virtual memory (Kb): 77588
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####