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/miplib3/normalized-mps-v2-20-10-vpm1.opb
MD5SUM	eb50800dc2fc522dd2f29a347fbab1da
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	454.966
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 13791

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc17 THE 2005-04-20 21:45:41 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13947 boxname=wulflinc17 idbench=1073 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  eb50800dc2fc522dd2f29a347fbab1da  /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-vpm1.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-vpm1.opb /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-vpm1.opb
IDLAUNCH: 13947
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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	: 3
cpu MHz		: 451.072
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:        723584 kB
Buffers:         33184 kB
Cached:         245636 kB
SwapCached:         48 kB
Active:          68360 kB
Inactive:       213480 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        723332 kB
SwapTotal:     2097892 kB
SwapFree:      2097840 kB
Dirty:              52 kB
Writeback:           0 kB
Mapped:           7032 kB
Slab:            23560 kB
Committed_AS:    63820 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-20 22:05:44 (client local time) WITH STATUS 0 IN 1200.29 SECONDS
stats: 13947 7 1200.29 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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  135794   388307 |   40738       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/35923          
c   -- var.elim.:  2000/35923          
c   -- var.elim.:  3000/35923          
c   -- var.elim.:  4000/35923          
c   -- var.elim.:  5000/35923          
c   -- var.elim.:  6000/35923          
c   -- var.elim.:  7000/35923          
c   -- var.elim.:  8000/35923          
c   -- var.elim.:  9000/35923          
c   -- var.elim.:  10000/35923          
c   -- var.elim.:  11000/35923          
c   -- var.elim.:  12000/35923          
c   -- var.elim.:  13000/35923          
c   -- var.elim.:  14000/35923          
c   -- var.elim.:  15000/35923          
c   -- var.elim.:  16000/35923          
c   -- var.elim.:  17000/35923          
c   -- var.elim.:  18000/35923          
c   -- var.elim.:  19000/35923          
c   -- var.elim.:  20000/35923          
c   -- var.elim.:  21000/35923          
c   -- var.elim.:  22000/35923          
c   -- var.elim.:  23000/35923          
c   -- var.elim.:  24000/35923          
c   -- var.elim.:  25000/35923          
c   -- var.elim.:  26000/35923          
c   -- var.elim.:  27000/35923          
c   -- var.elim.:  28000/35923          
c   -- var.elim.:  29000/35923          
c   -- var.elim.:  30000/35923          
c   -- var.elim.:  31000/35923          
c   -- var.elim.:  32000/35923          
c   -- var.elim.:  33000/35923          
c   -- var.elim.:  34000/35923          
c   -- var.elim.:  35000/35923          
c   -- var.elim.:  35923/35923          
c   -- var.elim.:  1000/16970          
c   -- var.eli#### 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.97 0.91 2/55 16906
Raw data (stat): 16906 (runsolver) R 16905 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 539791933 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.0003 s]
Raw data (loadavg): 0.93 0.97 0.91 2/55 16906
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 7469 0 0 0 977 21 0 0 25 0 1 0 539791933 32374784 6392 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7904 6392 603 41 0 7863 0
vsize: 31616
[startup+20.0003 s]
Raw data (loadavg): 0.94 0.97 0.91 2/55 16906
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 8258 0 0 0 1975 23 0 0 25 0 1 0 539791933 35590144 7181 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8689 7181 603 41 0 8648 0
vsize: 34756
[startup+29.9999 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 16906
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 8971 0 0 0 2973 25 0 0 25 0 1 0 539791933 38645760 7894 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9435 7894 603 41 0 9394 0
vsize: 37740
[startup+39.9997 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 16906
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 9482 0 0 0 3972 26 0 0 25 0 1 0 539791933 40632320 8405 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9920 8405 603 41 0 9879 0
vsize: 39680
[startup+50.0001 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 16906
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 10173 0 0 0 4971 28 0 0 25 0 1 0 539791933 43679744 9096 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10664 9096 603 41 0 10623 0
vsize: 42656
[startup+59.9997 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 16906
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 10608 0 0 0 5970 29 0 0 25 0 1 0 539791933 45416448 9531 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11088 9531 603 41 0 11047 0
vsize: 44352
[startup+70.0006 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 16906
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 10955 0 0 0 6969 29 0 0 25 0 1 0 539791933 46870528 9878 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11443 9878 603 41 0 11402 0
vsize: 45772
[startup+79.9999 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 16906
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 11256 0 0 0 7969 30 0 0 25 0 1 0 539791933 48070656 10179 4294967295 134512640 134672761 3221224544 3221223584 134603506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11736 10179 603 41 0 11695 0
vsize: 46944
[startup+89.9995 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 16906
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 11821 0 0 0 8967 32 0 0 25 0 1 0 539791933 50339840 10744 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12290 10744 603 41 0 12249 0
vsize: 49160
[startup+99.9994 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 16906
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 12226 0 0 0 9966 33 0 0 25 0 1 0 539791933 51929088 11149 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12678 11149 603 41 0 12637 0
vsize: 50712
[startup+109.999 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 16906
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 12502 0 0 0 10965 34 0 0 25 0 1 0 539791933 53129216 11425 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12971 11425 603 41 0 12930 0
vsize: 51884
[startup+119.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16906
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 12808 0 0 0 11965 34 0 0 25 0 1 0 539791933 54329344 11731 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13264 11731 603 41 0 13223 0
vsize: 53056
[startup+129.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16906
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 13030 0 0 0 12964 36 0 0 25 0 1 0 539791933 55267328 11953 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13493 11953 603 41 0 13452 0
vsize: 53972
[startup+140 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16906
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 13263 0 0 0 13963 37 0 0 25 0 1 0 539791933 56193024 12186 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13719 12186 603 41 0 13678 0
vsize: 54876
[startup+149.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16906
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 13465 0 0 0 14963 37 0 0 25 0 1 0 539791933 56987648 12388 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13913 12388 603 41 0 13872 0
vsize: 55652
[startup+159.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16906
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 13683 0 0 0 15962 38 0 0 25 0 1 0 539791933 57925632 12606 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14142 12606 603 41 0 14101 0
vsize: 56568
[startup+169.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16906
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 13870 0 0 0 16961 39 0 0 25 0 1 0 539791933 58593280 12793 4294967295 134512640 134672761 3221224544 3221223728 134615926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14305 12793 603 41 0 14264 0
vsize: 57220
[startup+179.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 16906
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 14139 0 0 0 17960 40 0 0 25 0 1 0 539791933 60305408 13062 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14723 13062 603 41 0 14682 0
vsize: 58892
[startup+190 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 16906
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 14550 0 0 0 18959 41 0 0 25 0 1 0 539791933 61894656 13473 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15111 13473 603 41 0 15070 0
vsize: 60444
[startup+199.999 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 16906
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 14897 0 0 0 19958 43 0 0 25 0 1 0 539791933 63348736 13820 4294967295 134512640 134672761 3221224544 3221223536 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15466 13820 603 41 0 15425 0
vsize: 61864
[startup+209.999 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 16906
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 15299 0 0 0 20957 44 0 0 25 0 1 0 539791933 64942080 14222 4294967295 134512640 134672761 3221224544 3221223732 134617708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15855 14222 603 41 0 15814 0
vsize: 63420
[startup+220 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 16908
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 16053 0 0 0 21955 46 0 0 25 0 1 0 539791933 67993600 14976 4294967295 134512640 134672761 3221224544 3221223584 134612851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16600 14976 603 41 0 16559 0
vsize: 66400
[startup+230 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 16908
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 16675 0 0 0 22954 48 0 0 25 0 1 0 539791933 70520832 15598 4294967295 134512640 134672761 3221224544 3221223688 134616161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17217 15598 603 41 0 17176 0
vsize: 68868
[startup+240 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 16908
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 17115 0 0 0 23952 50 0 0 25 0 1 0 539791933 72257536 16038 4294967295 134512640 134672761 3221224544 3221223744 134610675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17641 16038 603 41 0 17600 0
vsize: 70564
[startup+250.001 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 16908
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 17708 0 0 0 24951 51 0 0 25 0 1 0 539791933 74653696 16631 4294967295 134512640 134672761 3221224544 3221223800 134618476 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18226 16631 603 41 0 18185 0
vsize: 72904
[startup+260 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 16908
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 18042 0 0 0 25950 52 0 0 25 0 1 0 539791933 75984896 16965 4294967295 134512640 134672761 3221224544 3221223668 134566054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18551 16965 603 41 0 18510 0
vsize: 74204
[startup+269.999 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 16908
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 18356 0 0 0 26949 53 0 0 25 0 1 0 539791933 77180928 17279 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18843 17279 603 41 0 18802 0
vsize: 75372
[startup+280 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 16908
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 18666 0 0 0 27948 55 0 0 25 0 1 0 539791933 78503936 17589 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19166 17589 603 41 0 19125 0
vsize: 76664
[startup+290 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 16908
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 18952 0 0 0 28947 55 0 0 25 0 1 0 539791933 79687680 17875 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19455 17875 603 41 0 19414 0
vsize: 77820
[startup+299.999 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 16908
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19205 0 0 0 29947 56 0 0 25 0 1 0 539791933 80605184 18128 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19679 18128 603 41 0 19638 0
vsize: 78716
[startup+309.999 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 16908
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19696 0 0 0 30945 57 0 0 25 0 1 0 539791933 82690048 18619 4294967295 134512640 134672761 3221224544 3221222432 134645408 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18619 603 41 0 20147 0
vsize: 80752
[startup+319.999 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16908
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19915 0 0 0 31945 58 0 0 25 0 1 0 539791933 82690048 18601 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18601 603 41 0 20147 0
vsize: 80752
[startup+329.999 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16908
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19915 0 0 0 32945 58 0 0 25 0 1 0 539791933 82690048 18601 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18601 603 41 0 20147 0
vsize: 80752
[startup+339.999 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16908
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19915 0 0 0 33945 58 0 0 25 0 1 0 539791933 82690048 18601 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18601 603 41 0 20147 0
vsize: 80752
[startup+349.999 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16908
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19916 0 0 0 34946 58 0 0 25 0 1 0 539791933 82690048 18602 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18602 603 41 0 20147 0
vsize: 80752
[startup+359.999 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16908
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19916 0 0 0 35946 58 0 0 25 0 1 0 539791933 82690048 18602 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18602 603 41 0 20147 0
vsize: 80752
[startup+369.999 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16908
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19916 0 0 0 36946 58 0 0 25 0 1 0 539791933 82690048 18602 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18602 603 41 0 20147 0
vsize: 80752
[startup+379.999 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16908
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19916 0 0 0 37946 58 0 0 25 0 1 0 539791933 82690048 18602 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18602 603 41 0 20147 0
vsize: 80752
[startup+389.999 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16908
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19917 0 0 0 38946 58 0 0 25 0 1 0 539791933 82690048 18603 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18603 603 41 0 20147 0
vsize: 80752
[startup+399.999 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16908
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19917 0 0 0 39946 58 0 0 25 0 1 0 539791933 82690048 18603 4294967295 134512640 134672761 3221224544 3221223536 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18603 603 41 0 20147 0
vsize: 80752
[startup+409.998 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16908
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19917 0 0 0 40946 58 0 0 25 0 1 0 539791933 82690048 18603 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18603 603 41 0 20147 0
vsize: 80752
[startup+419.998 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16908
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19917 0 0 0 41947 58 0 0 25 0 1 0 539791933 82690048 18603 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18603 603 41 0 20147 0
vsize: 80752
[startup+429.998 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16908
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19917 0 0 0 42947 58 0 0 25 0 1 0 539791933 82690048 18603 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18603 603 41 0 20147 0
vsize: 80752
[startup+439.999 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16908
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19917 0 0 0 43947 58 0 0 25 0 1 0 539791933 82690048 18603 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18603 603 41 0 20147 0
vsize: 80752
[startup+449.999 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16908
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19917 0 0 0 44947 59 0 0 25 0 1 0 539791933 82690048 18603 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18603 603 41 0 20147 0
vsize: 80752
[startup+459.999 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16908
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19917 0 0 0 45947 59 0 0 25 0 1 0 539791933 82690048 18603 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18603 603 41 0 20147 0
vsize: 80752
[startup+469.999 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16908
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19917 0 0 0 46947 59 0 0 25 0 1 0 539791933 82690048 18603 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18603 603 41 0 20147 0
vsize: 80752
[startup+479.999 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16908
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19917 0 0 0 47947 59 0 0 25 0 1 0 539791933 82690048 18603 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18603 603 41 0 20147 0
vsize: 80752
[startup+490.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16908
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19917 0 0 0 48948 59 0 0 25 0 1 0 539791933 82690048 18603 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18603 603 41 0 20147 0
vsize: 80752
[startup+500 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16908
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19917 0 0 0 49948 59 0 0 25 0 1 0 539791933 82690048 18603 4294967295 134512640 134672761 3221224544 3221223688 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18603 603 41 0 20147 0
vsize: 80752
[startup+510 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16908
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19917 0 0 0 50948 59 0 0 25 0 1 0 539791933 82690048 18603 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18603 603 41 0 20147 0
vsize: 80752
[startup+520.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16910
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19917 0 0 0 51948 59 0 0 25 0 1 0 539791933 82690048 18603 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18603 603 41 0 20147 0
vsize: 80752
[startup+530.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16910
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19917 0 0 0 52948 59 0 0 25 0 1 0 539791933 82690048 18603 4294967295 134512640 134672761 3221224544 3221223728 134615785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18603 603 41 0 20147 0
vsize: 80752
[startup+540.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16910
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19917 0 0 0 53948 59 0 0 25 0 1 0 539791933 82690048 18603 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18603 603 41 0 20147 0
vsize: 80752
[startup+550.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16910
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19918 0 0 0 54949 59 0 0 25 0 1 0 539791933 82690048 18604 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18604 603 41 0 20147 0
vsize: 80752
[startup+560.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16910
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19918 0 0 0 55949 59 0 0 25 0 1 0 539791933 82690048 18604 4294967295 134512640 134672761 3221224544 3221223688 134616293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18604 603 41 0 20147 0
vsize: 80752
[startup+570.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16910
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19918 0 0 0 56950 59 0 0 25 0 1 0 539791933 82690048 18604 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18604 603 41 0 20147 0
vsize: 80752
[startup+580.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16910
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19918 0 0 0 57950 59 0 0 25 0 1 0 539791933 82690048 18604 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18604 603 41 0 20147 0
vsize: 80752
[startup+590.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16910
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19918 0 0 0 58951 59 0 0 25 0 1 0 539791933 82690048 18604 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18604 603 41 0 20147 0
vsize: 80752
[startup+600.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16910
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19918 0 0 0 59951 59 0 0 25 0 1 0 539791933 82690048 18604 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18604 603 41 0 20147 0
vsize: 80752
[startup+610.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16910
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19918 0 0 0 60951 59 0 0 25 0 1 0 539791933 82690048 18604 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18604 603 41 0 20147 0
vsize: 80752
[startup+620.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16910
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19918 0 0 0 61951 59 0 0 25 0 1 0 539791933 82690048 18604 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18604 603 41 0 20147 0
vsize: 80752
[startup+630.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16910
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19918 0 0 0 62951 59 0 0 25 0 1 0 539791933 82690048 18604 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18604 603 41 0 20147 0
vsize: 80752
[startup+640.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16910
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19918 0 0 0 63951 59 0 0 25 0 1 0 539791933 82690048 18604 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18604 603 41 0 20147 0
vsize: 80752
[startup+650.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16910
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19918 0 0 0 64952 59 0 0 25 0 1 0 539791933 82690048 18604 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18604 603 41 0 20147 0
vsize: 80752
[startup+660.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16910
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19918 0 0 0 65952 59 0 0 25 0 1 0 539791933 82690048 18604 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18604 603 41 0 20147 0
vsize: 80752
[startup+670.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16910
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19918 0 0 0 66952 59 0 0 25 0 1 0 539791933 82690048 18604 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18604 603 41 0 20147 0
vsize: 80752
[startup+680.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16910
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19918 0 0 0 67952 59 0 0 25 0 1 0 539791933 82690048 18604 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18604 603 41 0 20147 0
vsize: 80752
[startup+690.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16910
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19918 0 0 0 68952 59 0 0 25 0 1 0 539791933 82690048 18604 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18604 603 41 0 20147 0
vsize: 80752
[startup+700.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16910
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19918 0 0 0 69952 59 0 0 25 0 1 0 539791933 82690048 18604 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18604 603 41 0 20147 0
vsize: 80752
[startup+710.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16910
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19918 0 0 0 70953 59 0 0 25 0 1 0 539791933 82690048 18604 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18604 603 41 0 20147 0
vsize: 80752
[startup+720.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16910
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19918 0 0 0 71954 60 0 0 25 0 1 0 539791933 82690048 18604 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 18604 603 41 0 20147 0
vsize: 80752
[startup+730.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16910
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 19926 0 0 0 72954 60 0 0 25 0 1 0 539791933 82821120 18612 4294967295 134512640 134672761 3221224544 3221223688 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20220 18612 603 41 0 20179 0
vsize: 80880
[startup+740.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16910
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 20161 0 0 0 73953 60 0 0 25 0 1 0 539791933 83771392 18847 4294967295 134512640 134672761 3221224544 3221223584 134612665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20452 18847 603 41 0 20411 0
vsize: 81808
[startup+750.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16910
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 20405 0 0 0 74952 61 0 0 25 0 1 0 539791933 84901888 19091 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20728 19091 603 41 0 20687 0
vsize: 82912
[startup+760.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16910
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 20548 0 0 0 75951 62 0 0 25 0 1 0 539791933 85434368 19234 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20858 19234 603 41 0 20817 0
vsize: 83432
[startup+770.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16910
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 20661 0 0 0 76951 62 0 0 25 0 1 0 539791933 85962752 19347 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20987 19347 603 41 0 20946 0
vsize: 83948
[startup+780.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16910
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 20773 0 0 0 77951 62 0 0 25 0 1 0 539791933 86355968 19459 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21083 19459 603 41 0 21042 0
vsize: 84332
[startup+790.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16910
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 20892 0 0 0 78951 62 0 0 25 0 1 0 539791933 86884352 19578 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21212 19578 603 41 0 21171 0
vsize: 84848
[startup+800.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16910
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 21002 0 0 0 79951 63 0 0 25 0 1 0 539791933 87277568 19688 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21308 19688 603 41 0 21267 0
vsize: 85232
[startup+810.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16910
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 21102 0 0 0 80950 63 0 0 25 0 1 0 539791933 87810048 19788 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21438 19788 603 41 0 21397 0
vsize: 85752
[startup+820.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16912
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 21196 0 0 0 81951 63 0 0 25 0 1 0 539791933 88076288 19882 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21503 19882 603 41 0 21462 0
vsize: 86012
[startup+830.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16912
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 21306 0 0 0 82951 64 0 0 25 0 1 0 539791933 88604672 19992 4294967295 134512640 134672761 3221224544 3221223688 134616320 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21632 19992 603 41 0 21591 0
vsize: 86528
[startup+840.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16912
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 21409 0 0 0 83951 64 0 0 25 0 1 0 539791933 89014272 20095 4294967295 134512640 134672761 3221224544 3221223680 134614677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21732 20095 603 41 0 21691 0
vsize: 86928
[startup+850.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16912
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 21500 0 0 0 84950 65 0 0 25 0 1 0 539791933 89427968 20186 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21833 20186 603 41 0 21792 0
vsize: 87332
[startup+860.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16912
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 21594 0 0 0 85950 65 0 0 25 0 1 0 539791933 89825280 20280 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21930 20280 603 41 0 21889 0
vsize: 87720
[startup+870.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16913
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 21681 0 0 0 86950 65 0 0 25 0 1 0 539791933 90218496 20367 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22026 20367 603 41 0 21985 0
vsize: 88104
[startup+880.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16965
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 21838 0 0 0 87945 69 0 0 25 0 1 0 539791933 90910720 20524 4294967295 134512640 134672761 3221224544 3221223728 134615498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22195 20524 603 41 0 22154 0
vsize: 88780
[startup+890.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16965
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 21985 0 0 0 88946 70 0 0 25 0 1 0 539791933 91660288 20671 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22378 20671 603 41 0 22337 0
vsize: 89512
[startup+900.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16965
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 22405 0 0 0 89945 71 0 0 25 0 1 0 539791933 93421568 21091 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22808 21091 603 41 0 22767 0
vsize: 91232
[startup+910.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16965
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 22503 0 0 0 90945 71 0 0 25 0 1 0 539791933 93687808 21189 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22873 21189 603 41 0 22832 0
vsize: 91492
[startup+920.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16965
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 22734 0 0 0 91944 73 0 0 25 0 1 0 539791933 94765056 21420 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23136 21420 603 41 0 23095 0
vsize: 92544
[startup+930.062 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16965
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 22810 0 0 0 92945 73 0 0 25 0 1 0 539791933 95035392 21496 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23202 21496 603 41 0 23161 0
vsize: 92808
[startup+940.066 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16965
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 22889 0 0 0 93945 73 0 0 25 0 1 0 539791933 95301632 21575 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23267 21575 603 41 0 23226 0
vsize: 93068
[startup+950.066 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16967
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 22963 0 0 0 94945 74 0 0 25 0 1 0 539791933 95567872 21649 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23332 21649 603 41 0 23291 0
vsize: 93328
[startup+960.065 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16967
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 23046 0 0 0 95944 75 0 0 25 0 1 0 539791933 95969280 21732 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23430 21732 603 41 0 23389 0
vsize: 93720
[startup+970.066 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16967
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 23160 0 0 0 96944 75 0 0 25 0 1 0 539791933 96370688 21846 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23528 21846 603 41 0 23487 0
vsize: 94112
[startup+980.065 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16967
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 23296 0 0 0 97943 76 0 0 25 0 1 0 539791933 96903168 21982 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23658 21982 603 41 0 23617 0
vsize: 94632
[startup+990.066 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16967
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 23397 0 0 0 98943 76 0 0 25 0 1 0 539791933 98480128 22083 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24043 22083 603 41 0 24002 0
vsize: 96172
[startup+1000.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16967
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 23484 0 0 0 99943 77 0 0 25 0 1 0 539791933 98746368 22170 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24108 22170 603 41 0 24067 0
vsize: 96432
[startup+1010.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16967
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 23576 0 0 0 100942 77 0 0 25 0 1 0 539791933 99139584 22262 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24204 22262 603 41 0 24163 0
vsize: 96816
[startup+1020.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16967
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 23660 0 0 0 101942 78 0 0 25 0 1 0 539791933 99401728 22346 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24268 22346 603 41 0 24227 0
vsize: 97072
[startup+1030.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16967
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 23745 0 0 0 102942 78 0 0 25 0 1 0 539791933 99799040 22431 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24365 22431 603 41 0 24324 0
vsize: 97460
[startup+1040.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16967
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 23826 0 0 0 103942 79 0 0 25 0 1 0 539791933 100192256 22512 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24461 22512 603 41 0 24420 0
vsize: 97844
[startup+1050.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16967
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 23909 0 0 0 104942 79 0 0 25 0 1 0 539791933 100470784 22595 4294967295 134512640 134672761 3221224544 3221223728 134615673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24529 22595 603 41 0 24488 0
vsize: 98116
[startup+1060.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16967
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 23996 0 0 0 105941 79 0 0 25 0 1 0 539791933 100868096 22682 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24626 22682 603 41 0 24585 0
vsize: 98504
[startup+1070.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16967
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 24079 0 0 0 106941 79 0 0 25 0 1 0 539791933 101269504 22765 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24724 22765 603 41 0 24683 0
vsize: 98896
[startup+1080.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16967
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 24156 0 0 0 107942 79 0 0 25 0 1 0 539791933 101531648 22842 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24788 22842 603 41 0 24747 0
vsize: 99152
[startup+1090.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16967
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 24263 0 0 0 108941 80 0 0 25 0 1 0 539791933 101924864 22949 4294967295 134512640 134672761 3221224544 3221223728 134615801 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24884 22949 603 41 0 24843 0
vsize: 99536
[startup+1100.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16967
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 24371 0 0 0 109941 80 0 0 25 0 1 0 539791933 102318080 23057 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24980 23057 603 41 0 24939 0
vsize: 99920
[startup+1110.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16967
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 24467 0 0 0 110941 81 0 0 25 0 1 0 539791933 102772736 23153 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25091 23153 603 41 0 25050 0
vsize: 100364
[startup+1120.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16969
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 24558 0 0 0 111941 81 0 0 25 0 1 0 539791933 103170048 23244 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25188 23244 603 41 0 25147 0
vsize: 100752
[startup+1130.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16969
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 24654 0 0 0 112941 81 0 0 25 0 1 0 539791933 103616512 23340 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25297 23340 603 41 0 25256 0
vsize: 101188
[startup+1140.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16969
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 24730 0 0 0 113940 82 0 0 25 0 1 0 539791933 103878656 23416 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25361 23416 603 41 0 25320 0
vsize: 101444
[startup+1150.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16969
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 25178 0 0 0 114939 83 0 0 25 0 1 0 539791933 106430464 23832 4294967295 134512640 134672761 3221224544 3221223200 134645493 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25984 23832 603 41 0 25943 0
vsize: 103936
[startup+1160.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16969
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 25178 0 0 0 115940 83 0 0 25 0 1 0 539791933 106430464 23832 4294967295 134512640 134672761 3221224544 3221223600 134644269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25984 23832 603 41 0 25943 0
vsize: 103936
[startup+1170.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16969
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 25217 0 0 0 116940 83 0 0 25 0 1 0 539791933 105381888 23588 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25728 23588 603 41 0 25687 0
vsize: 102912
[startup+1180.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16969
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 25217 0 0 0 117940 83 0 0 25 0 1 0 539791933 105381888 23588 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25728 23588 603 41 0 25687 0
vsize: 102912
[startup+1190.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16969
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 25217 0 0 0 118940 83 0 0 25 0 1 0 539791933 105381888 23588 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25728 23588 603 41 0 25687 0
vsize: 102912
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 16971
Raw data (stat): 16906 (minisat+) R 16905 20838 20837 0 -1 0 25217 0 0 0 119940 83 0 0 25 0 1 0 539791933 105381888 23588 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25728 23588 603 41 0 25687 0
vsize: 102912
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.12 s]
Raw data (loadavg): 1.00 0.99 0.91 1/55 16971
Raw data (stat): 16906 (minisat+) Z 16905 20838 20837 0 -1 12 25217 0 0 0 119940 88 0 0 25 0 1 0 539791933 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.12
CPU time (s): 1200.29
CPU user time (s): 1199.41
CPU system time (s): 0.882865
CPU usage (%): 100.014
Max. virtual memory (Kb): 103936
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####