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-vpm2.opb
MD5SUM	fae1fae180d772ad3ee6c1acfa1c8b4f
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	122
Optimality of the best value was proved	NO
Number of terms in the objective function	168
Biggest coefficient in the objective function	5
Number of bits for the biggest coefficient in the objective function	3
Sum of the numbers in the objective function	504
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	2000000
Number of bits of the biggest number in a constraint	21
Biggest sum of numbers in a constraint	30041153
Number of bits of the biggest sum of numbers	25
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.01
Number of variables	2124
Total number of constraints	444
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	444
Minimum length of a constraint	8
Maximum length of a constraint	64
Trace number 17883

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc9 THE 2005-04-21 12:28:30 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18952 boxname=wulflinc9 idbench=1458 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  fae1fae180d772ad3ee6c1acfa1c8b4f  /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-13-7-vpm2.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-13-7-vpm2.opb /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-13-7-vpm2.opb
IDLAUNCH: 18952
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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.242
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:        422616 kB
Buffers:         32528 kB
Cached:         556488 kB
SwapCached:          0 kB
Active:          46156 kB
Inactive:       545644 kB
HighTotal:      131008 kB
HighFree:         1624 kB
LowTotal:       903652 kB
LowFree:        420992 kB
SwapTotal:     2097136 kB
SwapFree:      2097048 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6824 kB
Slab:            14584 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 12:48:32 (client local time) WITH STATUS 0 IN 1200.3 SECONDS
stats: 18952 7 1200.3 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:  110
c ---[ 190]---> BDD-cost:  237
c ---[ 189]---> BDD-cost:  236
c ---[ 188]---> BDD-cost:  393
c ---[ 187]---> BDD-cost:  495
c ---[ 186]---> BDD-cost:  488
c ---[ 185]---> BDD-cost:  131
c ---[ 184]---> BDD-cost:  262
c ---[ 183]---> BDD-cost:  261
c ---[ 182]---> BDD-cost:  448
c ---[ 181]---> BDD-cost:  550
c ---[ 180]---> BDD-cost:  549
c ---[ 179]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 5
c ---[ 178]---> Sorter-cost:  867     Base: 2 2 5 2 2 2 2
c ---[ 177]---> Sorter-cost:  830     Base: 2 2 2 2 2 2 5
c ---[ 176]---> Sorter-cost: 1298     Base: 2 2 5 2 2 2 2
c ---[ 175]---> Sorter-cost: 1687     Base: 2 2 5 2 2 2 2
c ---[ 174]---> Sorter-cost: 1665     Base: 2 2 5 2 2 2 2
c ---[ 173]---> Sorter-cost:  196     Base: 2 2 2 2 2 2
c ---[ 172]---> Sorter-cost:  473     Base: 2 2 2 2 2
c ---[ 171]---> Sorter-cost:  421     Base: 2 2 2 2 2 2
c ---[ 170]---> Sorter-cost:  764     Base: 2 2 2 2 2
c ---[ 169]---> Sorter-cost:  884     Base: 2 2 2 2 2 2
c ---[ 168]---> Sorter-cost: 1063     Base: 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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  163733   413768 |   49119       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/50837          
c   -- var.elim.:  2000/50837          
c   -- var.elim.:  3000/50837          
c   -- var.elim.:  4000/50837          
c   -- var.elim.:  5000/50837          
c   -- var.elim.:  6000/50837          
c   -- var.elim.:  7000/50837          
c   -- var.elim.:  8000/50837          
c   -- var.elim.:  9000/50837          
c   -- var.elim.:  10000/50837          
c   -- var.elim.:  11000/50837          
c   -- var.elim.:  12000/50837          
c   -- var.elim.:  13000/50837          
c   -- var.elim.:  14000/50837          
c   -- var.elim.:  15000/50837          
c   -- var.elim.:  16000/50837          
c   -- var.elim.:  17000/50837          
c   -- var.elim.:  18000/50837          
c   -- var.elim.:  19000/50837          
c   -- var.elim.:  20000/50837          
c   -- var.elim.:  21000/50837          
c   -- var.elim.:  22000/50837          
c   -- var.elim.:  23000/50837          
c   -- var.elim.:  24000/50837          
c   -- var.elim.:  25000/50837          
c   -- var.elim.:  26000/50837          
c   -- var.elim.:  27000/50837          
c   -- var.elim.:  28000/50837          
c   -- var.elim.:  29000/50837          
c   -- var.elim.:  30000/50837          
c   -- var.elim.:  31000/50837          
c   -- var.elim.:  32000/50837          
c   -- var.elim.:  33000/50837          
c   -- var.elim.:  34000/50837          
c   -- var.elim.:  35000/50837          
c   -- var.elim.:  36000/50837          
c   -- var.elim.:  37000/50837          
c   -- var.elim.:  38000/50837          
c   -- var.elim.:  39000/50837          
c   -- var.elim.:  40000/50837          
c   -- var.elim.:  41000/50837          
c   -- var.elim.:  42000/50837          
c   -- var.elim.:  43000/50837          
c   -- var.elim.:  44000/50837          
c   -- var.elim.:#### 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.79 0.95 0.90 2/54 8223
Raw data (stat): 8223 (runsolver) R 8222 30854 30853 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 486860131 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.83 0.95 0.90 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 9598 0 0 0 969 29 0 0 25 0 1 0 486860131 37818368 8209 4294967295 134512640 134672761 3221224560 3221223728 134553616 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9233 8209 603 41 0 9192 0
vsize: 36932
[startup+20.0007 s]
Raw data (loadavg): 0.85 0.95 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 9914 0 0 0 1968 30 0 0 25 0 1 0 486860131 39018496 8525 4294967295 134512640 134672761 3221224560 3221223696 134614756 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9526 8525 603 41 0 9485 0
vsize: 38104
[startup+30.0009 s]
Raw data (loadavg): 0.87 0.95 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 10411 0 0 0 2967 31 0 0 25 0 1 0 486860131 41132032 9022 4294967295 134512640 134672761 3221224560 3221223600 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10042 9022 603 41 0 10001 0
vsize: 40168
[startup+40.0007 s]
Raw data (loadavg): 0.89 0.95 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 10958 0 0 0 3965 32 0 0 25 0 1 0 486860131 43429888 9569 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10603 9569 603 41 0 10562 0
vsize: 42412
[startup+50.0008 s]
Raw data (loadavg): 0.91 0.95 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 11512 0 0 0 4964 34 0 0 25 0 1 0 486860131 45662208 10123 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11148 10123 603 41 0 11107 0
vsize: 44592
[startup+60.0013 s]
Raw data (loadavg): 0.92 0.95 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 12043 0 0 0 5962 35 0 0 25 0 1 0 486860131 47771648 10654 4294967295 134512640 134672761 3221224560 3221223744 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11663 10654 603 41 0 11622 0
vsize: 46652
[startup+70.0011 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 12610 0 0 0 6961 37 0 0 25 0 1 0 486860131 50155520 11221 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12245 11221 603 41 0 12204 0
vsize: 48980
[startup+80.0025 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 13356 0 0 0 7959 39 0 0 25 0 1 0 486860131 53186560 11967 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12985 11967 603 41 0 12944 0
vsize: 51940
[startup+90.0026 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 14154 0 0 0 8955 43 0 0 25 0 1 0 486860131 56483840 12765 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13790 12765 603 41 0 13749 0
vsize: 55160
[startup+100.002 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 14520 0 0 0 9955 44 0 0 25 0 1 0 486860131 57929728 13131 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14143 13131 603 41 0 14102 0
vsize: 56572
[startup+110.004 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 15017 0 0 0 10953 45 0 0 25 0 1 0 486860131 60022784 13628 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14654 13628 603 41 0 14613 0
vsize: 58616
[startup+120.004 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 15636 0 0 0 11951 48 0 0 25 0 1 0 486860131 62537728 14247 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15268 14247 603 41 0 15227 0
vsize: 61072
[startup+130.004 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 16223 0 0 0 12950 49 0 0 25 0 1 0 486860131 65179648 14834 4294967295 134512640 134672761 3221224560 3221223744 134615683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15913 14834 603 41 0 15872 0
vsize: 63652
[startup+140.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 16756 0 0 0 13949 50 0 0 25 0 1 0 486860131 67289088 15367 4294967295 134512640 134672761 3221224560 3221223744 134615635 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16428 15367 603 41 0 16387 0
vsize: 65712
[startup+150.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 17266 0 0 0 14947 52 0 0 25 0 1 0 486860131 69398528 15877 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16943 15877 603 41 0 16902 0
vsize: 67772
[startup+160.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 17730 0 0 0 15946 54 0 0 25 0 1 0 486860131 71241728 16341 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17393 16341 603 41 0 17352 0
vsize: 69572
[startup+170.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 18138 0 0 0 16945 55 0 0 25 0 1 0 486860131 72957952 16749 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17812 16749 603 41 0 17771 0
vsize: 71248
[startup+180.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 18532 0 0 0 17944 56 0 0 25 0 1 0 486860131 74543104 17143 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18199 17143 603 41 0 18158 0
vsize: 72796
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 18992 0 0 0 18942 58 0 0 25 0 1 0 486860131 76402688 17603 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18653 17603 603 41 0 18612 0
vsize: 74612
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 19329 0 0 0 19941 59 0 0 25 0 1 0 486860131 77864960 17940 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19010 17940 603 41 0 18969 0
vsize: 76040
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 19770 0 0 0 20940 61 0 0 25 0 1 0 486860131 79568896 18381 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19426 18381 603 41 0 19385 0
vsize: 77704
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 20177 0 0 0 21938 62 0 0 25 0 1 0 486860131 81285120 18788 4294967295 134512640 134672761 3221224560 3221223744 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19845 18788 603 41 0 19804 0
vsize: 79380
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 20557 0 0 0 22938 63 0 0 25 0 1 0 486860131 82890752 19168 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20237 19168 603 41 0 20196 0
vsize: 80948
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 20925 0 0 0 23937 64 0 0 25 0 1 0 486860131 84340736 19536 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20591 19536 603 41 0 20550 0
vsize: 82364
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 21313 0 0 0 24936 65 0 0 25 0 1 0 486860131 85917696 19924 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20976 19924 603 41 0 20935 0
vsize: 83904
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 21776 0 0 0 25935 67 0 0 25 0 1 0 486860131 87760896 20387 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21426 20387 603 41 0 21385 0
vsize: 85704
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 22077 0 0 0 26934 68 0 0 25 0 1 0 486860131 89079808 20688 4294967295 134512640 134672761 3221224560 3221223696 134614685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21748 20688 603 41 0 21707 0
vsize: 86992
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 22379 0 0 0 27934 68 0 0 25 0 1 0 486860131 90259456 20990 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22036 20990 603 41 0 21995 0
vsize: 88144
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 22694 0 0 0 28933 70 0 0 25 0 1 0 486860131 91574272 21305 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22357 21305 603 41 0 22316 0
vsize: 89428
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 23200 0 0 0 29931 71 0 0 25 0 1 0 486860131 93679616 21811 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22871 21811 603 41 0 22830 0
vsize: 91484
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 23663 0 0 0 30930 73 0 0 25 0 1 0 486860131 95531008 22274 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23323 22274 603 41 0 23282 0
vsize: 93292
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 23979 0 0 0 31929 74 0 0 25 0 1 0 486860131 96731136 22590 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23616 22590 603 41 0 23575 0
vsize: 94464
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 24305 0 0 0 32928 75 0 0 25 0 1 0 486860131 98107392 22916 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23952 22916 603 41 0 23911 0
vsize: 95808
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 24597 0 0 0 33927 76 0 0 25 0 1 0 486860131 99291136 23208 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24241 23208 603 41 0 24200 0
vsize: 96964
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 24864 0 0 0 34926 77 0 0 25 0 1 0 486860131 100999168 23475 4294967295 134512640 134672761 3221224560 3221223704 134616347 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24658 23475 603 41 0 24617 0
vsize: 98632
[startup+360.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 25137 0 0 0 35925 78 0 0 25 0 1 0 486860131 102060032 23748 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24917 23748 603 41 0 24876 0
vsize: 99668
[startup+370.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 25372 0 0 0 36925 79 0 0 25 0 1 0 486860131 103002112 23983 4294967295 134512640 134672761 3221224560 3221223744 134615594 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25147 23983 603 41 0 25106 0
vsize: 100588
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 25622 0 0 0 37924 79 0 0 25 0 1 0 486860131 104054784 24233 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25404 24233 603 41 0 25363 0
vsize: 101616
[startup+390.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 25886 0 0 0 38924 80 0 0 25 0 1 0 486860131 105103360 24497 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25660 24497 603 41 0 25619 0
vsize: 102640
[startup+400.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 26178 0 0 0 39923 81 0 0 25 0 1 0 486860131 106291200 24789 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25950 24789 603 41 0 25909 0
vsize: 103800
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 26422 0 0 0 40922 83 0 0 25 0 1 0 486860131 107339776 25033 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26206 25033 603 41 0 26165 0
vsize: 104824
[startup+420.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 26692 0 0 0 41921 83 0 0 25 0 1 0 486860131 108392448 25303 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26463 25303 603 41 0 26422 0
vsize: 105852
[startup+430.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 26995 0 0 0 42920 84 0 0 25 0 1 0 486860131 109711360 25606 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26785 25606 603 41 0 26744 0
vsize: 107140
[startup+440.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 27252 0 0 0 43919 86 0 0 25 0 1 0 486860131 110764032 25863 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27042 25863 603 41 0 27001 0
vsize: 108168
[startup+450.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 27512 0 0 0 44919 86 0 0 25 0 1 0 486860131 111812608 26123 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27298 26123 603 41 0 27257 0
vsize: 109192
[startup+460.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 27761 0 0 0 45918 87 0 0 25 0 1 0 486860131 112861184 26372 4294967295 134512640 134672761 3221224560 3221223744 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27554 26372 603 41 0 27513 0
vsize: 110216
[startup+470.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 28051 0 0 0 46918 88 0 0 25 0 1 0 486860131 114040832 26662 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27842 26662 603 41 0 27801 0
vsize: 111368
[startup+480.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 28289 0 0 0 47918 88 0 0 25 0 1 0 486860131 114991104 26900 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28074 26900 603 41 0 28033 0
vsize: 112296
[startup+490.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 28538 0 0 0 48916 89 0 0 25 0 1 0 486860131 116043776 27149 4294967295 134512640 134672761 3221224560 3221223744 134615830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28331 27149 603 41 0 28290 0
vsize: 113324
[startup+500.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 28798 0 0 0 49916 90 0 0 25 0 1 0 486860131 117133312 27409 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28597 27409 603 41 0 28556 0
vsize: 114388
[startup+510.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 29079 0 0 0 50916 90 0 0 25 0 1 0 486860131 118185984 27690 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28854 27690 603 41 0 28813 0
vsize: 115416
[startup+520.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 29315 0 0 0 51915 91 0 0 25 0 1 0 486860131 119242752 27926 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29112 27926 603 41 0 29071 0
vsize: 116448
[startup+530.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 29556 0 0 0 52915 92 0 0 25 0 1 0 486860131 120164352 28167 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29337 28167 603 41 0 29296 0
vsize: 117348
[startup+540.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 29789 0 0 0 53914 92 0 0 25 0 1 0 486860131 121081856 28400 4294967295 134512640 134672761 3221224560 3221223600 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29561 28400 603 41 0 29520 0
vsize: 118244
[startup+550.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 29978 0 0 0 54914 93 0 0 25 0 1 0 486860131 121876480 28589 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29755 28589 603 41 0 29714 0
vsize: 119020
[startup+560.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 30237 0 0 0 55914 93 0 0 25 0 1 0 486860131 122925056 28848 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30011 28848 603 41 0 29970 0
vsize: 120044
[startup+570.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 30503 0 0 0 56913 94 0 0 25 0 1 0 486860131 123981824 29114 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30269 29114 603 41 0 30228 0
vsize: 121076
[startup+580.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 30765 0 0 0 57912 95 0 0 25 0 1 0 486860131 125046784 29376 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30529 29376 603 41 0 30488 0
vsize: 122116
[startup+590.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 31016 0 0 0 58912 96 0 0 25 0 1 0 486860131 126115840 29627 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30790 29627 603 41 0 30749 0
vsize: 123160
[startup+600.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 31264 0 0 0 59911 96 0 0 25 0 1 0 486860131 127164416 29875 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31046 29875 603 41 0 31005 0
vsize: 124184
[startup+610.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 31532 0 0 0 60911 97 0 0 25 0 1 0 486860131 128237568 30143 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31308 30143 603 41 0 31267 0
vsize: 125232
[startup+620.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 31770 0 0 0 61910 98 0 0 25 0 1 0 486860131 129167360 30381 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31535 30381 603 41 0 31494 0
vsize: 126140
[startup+630.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 32008 0 0 0 62910 98 0 0 25 0 1 0 486860131 130215936 30619 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31791 30619 603 41 0 31750 0
vsize: 127164
[startup+640.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 32232 0 0 0 63909 99 0 0 25 0 1 0 486860131 131145728 30843 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32018 30843 603 41 0 31977 0
vsize: 128072
[startup+650.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 32460 0 0 0 64909 99 0 0 25 0 1 0 486860131 132063232 31071 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32242 31071 603 41 0 32201 0
vsize: 128968
[startup+660.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 32698 0 0 0 65909 100 0 0 25 0 1 0 486860131 132980736 31309 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32466 31309 603 41 0 32425 0
vsize: 129864
[startup+670.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 32947 0 0 0 66908 101 0 0 25 0 1 0 486860131 134033408 31558 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32723 31558 603 41 0 32682 0
vsize: 130892
[startup+680.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 33170 0 0 0 67908 101 0 0 25 0 1 0 486860131 134955008 31781 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32948 31781 603 41 0 32907 0
vsize: 131792
[startup+690.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 33406 0 0 0 68907 102 0 0 25 0 1 0 486860131 135888896 32017 4294967295 134512640 134672761 3221224560 3221223744 134615611 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33176 32017 603 41 0 33135 0
vsize: 132704
[startup+700.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 33786 0 0 0 69907 103 0 0 25 0 1 0 486860131 137465856 32397 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33561 32397 603 41 0 33520 0
vsize: 134244
[startup+710.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 34114 0 0 0 70905 104 0 0 25 0 1 0 486860131 138792960 32725 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33885 32725 603 41 0 33844 0
vsize: 135540
[startup+720.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 34298 0 0 0 71905 105 0 0 25 0 1 0 486860131 139460608 32909 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34048 32909 603 41 0 34007 0
vsize: 136192
[startup+730.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 34468 0 0 0 72905 105 0 0 25 0 1 0 486860131 140271616 33079 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34246 33079 603 41 0 34205 0
vsize: 136984
[startup+740.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 34635 0 0 0 73904 106 0 0 25 0 1 0 486860131 140926976 33246 4294967295 134512640 134672761 3221224560 3221223744 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34406 33246 603 41 0 34365 0
vsize: 137624
[startup+750.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 34810 0 0 0 74904 106 0 0 25 0 1 0 486860131 141582336 33421 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34566 33421 603 41 0 34525 0
vsize: 138264
[startup+760.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 34972 0 0 0 75904 107 0 0 25 0 1 0 486860131 142237696 33583 4294967295 134512640 134672761 3221224560 3221223744 134615660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34726 33583 603 41 0 34685 0
vsize: 138904
[startup+770.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 35137 0 0 0 76904 107 0 0 25 0 1 0 486860131 142893056 33748 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34886 33748 603 41 0 34845 0
vsize: 139544
[startup+780.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 35316 0 0 0 77903 108 0 0 25 0 1 0 486860131 143679488 33927 4294967295 134512640 134672761 3221224560 3221223744 134615755 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35078 33927 603 41 0 35037 0
vsize: 140312
[startup+790.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 35480 0 0 0 78903 108 0 0 25 0 1 0 486860131 144355328 34091 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35243 34091 603 41 0 35202 0
vsize: 140972
[startup+800.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 35635 0 0 0 79902 109 0 0 25 0 1 0 486860131 145014784 34246 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35404 34246 603 41 0 35363 0
vsize: 141616
[startup+810.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 35800 0 0 0 80902 110 0 0 25 0 1 0 486860131 145670144 34411 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35564 34411 603 41 0 35523 0
vsize: 142256
[startup+820.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 35955 0 0 0 81901 111 0 0 25 0 1 0 486860131 146325504 34566 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35724 34566 603 41 0 35683 0
vsize: 142896
[startup+830.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 36131 0 0 0 82901 111 0 0 25 0 1 0 486860131 146984960 34742 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35885 34742 603 41 0 35844 0
vsize: 143540
[startup+840.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 36311 0 0 0 83900 112 0 0 25 0 1 0 486860131 147771392 34922 4294967295 134512640 134672761 3221224560 3221223712 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36077 34922 603 41 0 36036 0
vsize: 144308
[startup+850.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 36473 0 0 0 84899 113 0 0 25 0 1 0 486860131 148426752 35084 4294967295 134512640 134672761 3221224560 3221223744 134615617 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36237 35084 603 41 0 36196 0
vsize: 144948
[startup+860.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 36639 0 0 0 85899 113 0 0 25 0 1 0 486860131 149094400 35250 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36400 35250 603 41 0 36359 0
vsize: 145600
[startup+870.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 36803 0 0 0 86899 113 0 0 25 0 1 0 486860131 149749760 35414 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36560 35414 603 41 0 36519 0
vsize: 146240
[startup+880.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 36972 0 0 0 87899 114 0 0 25 0 1 0 486860131 150405120 35583 4294967295 134512640 134672761 3221224560 3221223744 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36720 35583 603 41 0 36679 0
vsize: 146880
[startup+890.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 37128 0 0 0 88899 114 0 0 25 0 1 0 486860131 151064576 35739 4294967295 134512640 134672761 3221224560 3221223744 134615676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36881 35739 603 41 0 36840 0
vsize: 147524
[startup+900.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 37283 0 0 0 89898 115 0 0 25 0 1 0 486860131 151719936 35894 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37041 35894 603 41 0 37000 0
vsize: 148164
[startup+910.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 37430 0 0 0 90898 115 0 0 25 0 1 0 486860131 152375296 36041 4294967295 134512640 134672761 3221224560 3221223744 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37201 36041 603 41 0 37160 0
vsize: 148804
[startup+920.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 37580 0 0 0 91897 116 0 0 25 0 1 0 486860131 152899584 36191 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37329 36191 603 41 0 37288 0
vsize: 149316
[startup+930.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 37725 0 0 0 92897 116 0 0 25 0 1 0 486860131 153554944 36336 4294967295 134512640 134672761 3221224560 3221223744 134615681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37489 36336 603 41 0 37448 0
vsize: 149956
[startup+940.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 37873 0 0 0 93897 117 0 0 25 0 1 0 486860131 154136576 36484 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37631 36484 603 41 0 37590 0
vsize: 150524
[startup+950.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 38010 0 0 0 94897 117 0 0 25 0 1 0 486860131 154791936 36621 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37791 36621 603 41 0 37750 0
vsize: 151164
[startup+960.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 38161 0 0 0 95897 117 0 0 25 0 1 0 486860131 155357184 36772 4294967295 134512640 134672761 3221224560 3221223744 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37929 36772 603 41 0 37888 0
vsize: 151716
[startup+970.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 38307 0 0 0 96897 118 0 0 25 0 1 0 486860131 156012544 36918 4294967295 134512640 134672761 3221224560 3221223760 134610618 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38089 36918 603 41 0 38048 0
vsize: 152356
[startup+980.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 38465 0 0 0 97896 118 0 0 25 0 1 0 486860131 156647424 37076 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38244 37076 603 41 0 38203 0
vsize: 152976
[startup+990.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 38611 0 0 0 98896 119 0 0 25 0 1 0 486860131 157200384 37222 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38379 37222 603 41 0 38338 0
vsize: 153516
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 38747 0 0 0 99896 119 0 0 25 0 1 0 486860131 157724672 37358 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38507 37358 603 41 0 38466 0
vsize: 154028
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 38870 0 0 0 100895 120 0 0 25 0 1 0 486860131 158253056 37481 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38636 37481 603 41 0 38595 0
vsize: 154544
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 38997 0 0 0 101895 120 0 0 25 0 1 0 486860131 158777344 37608 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38764 37608 603 41 0 38723 0
vsize: 155056
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 39122 0 0 0 102895 120 0 0 25 0 1 0 486860131 159301632 37733 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38892 37733 603 41 0 38851 0
vsize: 155568
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 39245 0 0 0 103895 121 0 0 25 0 1 0 486860131 159825920 37856 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39020 37856 603 41 0 38979 0
vsize: 156080
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 39370 0 0 0 104895 121 0 0 25 0 1 0 486860131 160362496 37981 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39151 37981 603 41 0 39110 0
vsize: 156604
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 39493 0 0 0 105894 121 0 0 25 0 1 0 486860131 160886784 38104 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39279 38104 603 41 0 39238 0
vsize: 157116
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 39616 0 0 0 106894 122 0 0 25 0 1 0 486860131 161415168 38227 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39408 38227 603 41 0 39367 0
vsize: 157632
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 39745 0 0 0 107893 123 0 0 25 0 1 0 486860131 161939456 38356 4294967295 134512640 134672761 3221224560 3221223744 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39536 38356 603 41 0 39495 0
vsize: 158144
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 39878 0 0 0 108893 123 0 0 25 0 1 0 486860131 162463744 38489 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39664 38489 603 41 0 39623 0
vsize: 158656
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 40073 0 0 0 109893 124 0 0 25 0 1 0 486860131 163373056 38684 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39886 38684 603 41 0 39845 0
vsize: 159544
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 40277 0 0 0 110892 124 0 0 25 0 1 0 486860131 164167680 38888 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40080 38888 603 41 0 40039 0
vsize: 160320
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 40462 0 0 0 111892 125 0 0 25 0 1 0 486860131 164954112 39073 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40272 39073 603 41 0 40231 0
vsize: 161088
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 40678 0 0 0 112891 126 0 0 25 0 1 0 486860131 165879808 39289 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40498 39289 603 41 0 40457 0
vsize: 161992
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 40879 0 0 0 113891 127 0 0 25 0 1 0 486860131 166666240 39490 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40690 39490 603 41 0 40649 0
vsize: 162760
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 41065 0 0 0 114892 127 0 0 25 0 1 0 486860131 167452672 39676 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40882 39676 603 41 0 40841 0
vsize: 163528
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 41248 0 0 0 115893 127 0 0 25 0 1 0 486860131 168239104 39859 4294967295 134512640 134672761 3221224560 3221223600 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41074 39859 603 41 0 41033 0
vsize: 164296
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 41433 0 0 0 116893 128 0 0 25 0 1 0 486860131 168894464 40044 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41234 40044 603 41 0 41193 0
vsize: 164936
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 41592 0 0 0 117893 128 0 0 25 0 1 0 486860131 169549824 40203 4294967295 134512640 134672761 3221224560 3221223704 134616139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41394 40203 603 41 0 41353 0
vsize: 165576
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 41844 0 0 0 118892 129 0 0 25 0 1 0 486860131 170553344 40455 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41639 40455 603 41 0 41598 0
vsize: 166556
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8223
Raw data (stat): 8223 (minisat+) R 8222 30854 30853 0 -1 0 42420 0 0 0 119889 132 0 0 25 0 1 0 486860131 172924928 41031 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42218 41031 603 41 0 42177 0
vsize: 168872
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.13 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 8223
Raw data (stat): 8223 (minisat+) Z 8222 30854 30853 0 -1 12 42420 0 0 0 119889 140 0 0 25 0 1 0 486860131 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.13
CPU time (s): 1200.3
CPU user time (s): 1198.89
CPU system time (s): 1.40879
CPU usage (%): 100.015
Max. virtual memory (Kb): 168872
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####