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-vpm2.opb
MD5SUM	766b2fe57cb2084b069363491485612e
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	97
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	16000000
Number of bits of the biggest number in a constraint	24
Biggest sum of numbers in a constraint	241094849
Number of bits of the biggest sum of numbers	28
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.23
Number of variables	2754
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	11
Maximum length of a constraint	84
Trace number 21320

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc21 THE 2005-04-21 23:23:44 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13960 boxname=wulflinc21 idbench=1074 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  766b2fe57cb2084b069363491485612e  /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-vpm2.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-vpm2.opb /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-vpm2.opb
IDLAUNCH: 13960
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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:        501496 kB
Buffers:         10104 kB
Cached:         501460 kB
SwapCached:          0 kB
Active:         203656 kB
Inactive:       310828 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        501244 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           6952 kB
Slab:            13060 kB
Committed_AS:    63784 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 23:43:46 (client local time) WITH STATUS 0 IN 1200.27 SECONDS
stats: 13960 7 1200.27 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:  237
c ---[ 190]---> BDD-cost:  601
c ---[ 189]---> BDD-cost:  600
c ---[ 188]---> BDD-cost: 1143
c ---[ 187]---> BDD-cost: 1480
c ---[ 186]---> BDD-cost: 1473
c ---[ 185]---> BDD-cost:  273
c ---[ 184]---> BDD-cost:  768
c ---[ 183]---> BDD-cost:  767
c ---[ 182]---> Sorter-cost: 2076     Base: 5 5 5 2 2 5 5 2 2 2 2 2 2 2
c ---[ 181]---> Sorter-cost: 2697     Base: 5 5 5 2 2 5 5 2 2 2 2 2 2 2
c ---[ 180]---> Sorter-cost: 2701     Base: 5 5 5 2 2 5 5 2 2 2 2 2 2 2
c ---[ 179]---> Sorter-cost:  449     Base: 2 2 2 2 2 2 2 2 2 5
c ---[ 178]---> Sorter-cost: 1242     Base: 2 2 2 2 2 5 2 2 2 2
c ---[ 177]---> Sorter-cost: 1199     Base: 2 2 2 2 2 2 2 2 2 5
c ---[ 176]---> Sorter-cost: 1719     Base: 5 2 2 2 2 2 2 2 2 2
c ---[ 175]---> Sorter-cost: 2067     Base: 5 2 2 2 2 2 2 2 2 2
c ---[ 174]---> Sorter-cost: 2045     Base: 5 2 2 2 2 2 2 2 2 2
c ---[ 173]---> Sorter-cost:  223     Base: 2 2 2 2 2 2 2 2 2
c ---[ 172]---> Sorter-cost:  590     Base: 2 2 2 2 2 2 2 2
c ---[ 171]---> Sorter-cost:  538     Base: 2 2 2 2 2 2 2 2 2
c ---[ 170]---> Sorter-cost: 1025     Base: 2 2 2 2 2 2 2 2
c ---[ 169]---> Sorter-cost: 1211     Base: 2 2 2 2 2 2 2 2 2
c ---[ 168]---> Sorter-cost: 1390     Base: 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 |  171024   481331 |   51307       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/48684          
c   -- var.elim.:  2000/48684          
c   -- var.elim.:  3000/48684          
c   -- var.elim.:  4000/48684          
c   -- var.elim.:  5000/48684          
c   -- var.elim.:  6000/48684          
c   -- var.elim.:  7000/48684          
c   -- var.elim.:  8000/48684          
c   -- var.elim.:  9000/48684          
c   -- var.elim.:  10000/48684          
c   -- var.elim.:  11000/48684          
c   -- var.elim.:  12000/48684          
c   -- var.elim.:  13000/48684          
c   -- var.elim.:  14000/48684          
c   -- var.elim.:  15000/48684          
c   -- var.elim.:  16000/48684          
c   -- var.elim.:  17000/48684          
c   -- var.elim.:  18000/48684          
c   -- var.elim.:  19000/48684          
c   -- var.elim.:  20000/48684          
c   -- var.elim.:  21000/48684          
c   -- var.elim.:  22000/48684          
c   -- var.elim.:  23000/48684          
c   -- var.elim.:  24000/48684          
c   -- var.elim.:  25000/48684          
c   -- var.elim.:  26000/48684          
c   -- var.elim.:  27000/48684          
c   -- var.elim.:  28000/48684          
c   -- var.elim.:  29000/48684          
c   -- var.elim.:  30000/48684          
c   -- var.elim.:  31000/48684          
c   -- var.elim.:  32000/48684          
c   -- var.elim.:  33000/48684          
c   -- var.elim.:  34000/48684          
c   -- var.elim.:  35000/48684          
c   -- var.elim.:  36000/48684          
c   -- var.elim.:  37000/48684          
c   -- var.elim.:  38000/48684          
c   -- var.elim.:  39000/48684          
c   -- var.elim.:  40000/48684          
c   -- va#### 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.84 0.94 0.90 2/55 23863
Raw data (stat): 23863 (runsolver) R 23862 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 426277003 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.87 0.94 0.90 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 9476 0 0 0 972 27 0 0 25 0 1 0 426277003 37396480 8123 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9130 8123 603 41 0 9089 0
vsize: 36520
[startup+20.0005 s]
Raw data (loadavg): 0.89 0.94 0.90 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 9921 0 0 0 1971 28 0 0 25 0 1 0 426277003 39288832 8568 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9592 8568 603 41 0 9551 0
vsize: 38368
[startup+30.0012 s]
Raw data (loadavg): 0.90 0.94 0.90 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 10548 0 0 0 2969 30 0 0 25 0 1 0 426277003 41947136 9195 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10241 9195 603 41 0 10200 0
vsize: 40964
[startup+40.0008 s]
Raw data (loadavg): 0.92 0.94 0.90 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 11248 0 0 0 3968 31 0 0 25 0 1 0 426277003 44736512 9895 4294967295 134512640 134672761 3221224544 3221223688 134616170 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10922 9895 603 41 0 10881 0
vsize: 43688
[startup+50.0015 s]
Raw data (loadavg): 0.93 0.94 0.90 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 11986 0 0 0 4966 34 0 0 25 0 1 0 426277003 47902720 10633 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11695 10633 603 41 0 11654 0
vsize: 46780
[startup+60.0012 s]
Raw data (loadavg): 0.94 0.95 0.90 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 12585 0 0 0 5964 35 0 0 25 0 1 0 426277003 50409472 11232 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12307 11232 603 41 0 12266 0
vsize: 49228
[startup+70.0023 s]
Raw data (loadavg): 0.95 0.95 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 13162 0 0 0 6963 37 0 0 25 0 1 0 426277003 52658176 11809 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12856 11809 603 41 0 12815 0
vsize: 51424
[startup+80.0026 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 13644 0 0 0 7961 39 0 0 25 0 1 0 426277003 54640640 12291 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13340 12291 603 41 0 13299 0
vsize: 53360
[startup+90.0023 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 14246 0 0 0 8960 40 0 0 25 0 1 0 426277003 57020416 12893 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13921 12893 603 41 0 13880 0
vsize: 55684
[startup+100.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 14707 0 0 0 9959 41 0 0 25 0 1 0 426277003 58875904 13354 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14374 13354 603 41 0 14333 0
vsize: 57496
[startup+110.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 15153 0 0 0 10958 42 0 0 25 0 1 0 426277003 60735488 13800 4294967295 134512640 134672761 3221224544 3221223728 134615585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14828 13800 603 41 0 14787 0
vsize: 59312
[startup+120.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 15765 0 0 0 11957 44 0 0 25 0 1 0 426277003 63766528 14412 4294967295 134512640 134672761 3221224544 3221223728 134615686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15568 14412 603 41 0 15527 0
vsize: 62272
[startup+130.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 16305 0 0 0 12955 46 0 0 25 0 1 0 426277003 65871872 14952 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16082 14952 603 41 0 16041 0
vsize: 64328
[startup+140.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 16768 0 0 0 13954 47 0 0 25 0 1 0 426277003 67739648 15415 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16538 15415 603 41 0 16497 0
vsize: 66152
[startup+150.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 17140 0 0 0 14953 48 0 0 25 0 1 0 426277003 69214208 15787 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16898 15787 603 41 0 16857 0
vsize: 67592
[startup+160.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 17434 0 0 0 15952 49 0 0 25 0 1 0 426277003 70414336 16081 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17191 16081 603 41 0 17150 0
vsize: 68764
[startup+170.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 17714 0 0 0 16951 50 0 0 25 0 1 0 426277003 71618560 16361 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17485 16361 603 41 0 17444 0
vsize: 69940
[startup+180.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 17951 0 0 0 17950 52 0 0 25 0 1 0 426277003 72544256 16598 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17711 16598 603 41 0 17670 0
vsize: 70844
[startup+190.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 18241 0 0 0 18950 52 0 0 25 0 1 0 426277003 73740288 16888 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18003 16888 603 41 0 17962 0
vsize: 72012
[startup+200.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 18549 0 0 0 19948 53 0 0 25 0 1 0 426277003 75055104 17196 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18324 17196 603 41 0 18283 0
vsize: 73296
[startup+210.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 18923 0 0 0 20948 54 0 0 25 0 1 0 426277003 76529664 17570 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18684 17570 603 41 0 18643 0
vsize: 74736
[startup+220.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 19573 0 0 0 21946 56 0 0 25 0 1 0 426277003 79065088 18220 4294967295 134512640 134672761 3221224544 3221223688 134616132 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19303 18220 603 41 0 19262 0
vsize: 77212
[startup+230.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 20151 0 0 0 22944 58 0 0 25 0 1 0 426277003 81457152 18798 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19887 18798 603 41 0 19846 0
vsize: 79548
[startup+240.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 20822 0 0 0 23942 60 0 0 25 0 1 0 426277003 84230144 19469 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20564 19469 603 41 0 20523 0
vsize: 82256
[startup+250.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 21263 0 0 0 24941 62 0 0 25 0 1 0 426277003 85958656 19910 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20986 19910 603 41 0 20945 0
vsize: 83944
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 21626 0 0 0 25939 64 0 0 25 0 1 0 426277003 87416832 20273 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21342 20273 603 41 0 21301 0
vsize: 85368
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 22078 0 0 0 26938 65 0 0 25 0 1 0 426277003 89280512 20725 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21797 20725 603 41 0 21756 0
vsize: 87188
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 22520 0 0 0 27937 67 0 0 25 0 1 0 426277003 90996736 21167 4294967295 134512640 134672761 3221224544 3221223728 134615794 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22216 21167 603 41 0 22175 0
vsize: 88864
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 22791 0 0 0 28936 68 0 0 25 0 1 0 426277003 92196864 21438 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22509 21438 603 41 0 22468 0
vsize: 90036
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 23036 0 0 0 29935 68 0 0 25 0 1 0 426277003 93126656 21683 4294967295 134512640 134672761 3221224544 3221223728 134615711 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22736 21683 603 41 0 22695 0
vsize: 90944
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 23341 0 0 0 30934 69 0 0 25 0 1 0 426277003 95379456 21988 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23286 21988 603 41 0 23245 0
vsize: 93144
[startup+320.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 23664 0 0 0 31933 70 0 0 25 0 1 0 426277003 96698368 22311 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23608 22311 603 41 0 23567 0
vsize: 94432
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 23943 0 0 0 32933 71 0 0 25 0 1 0 426277003 97906688 22590 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23903 22590 603 41 0 23862 0
vsize: 95612
[startup+340.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 24171 0 0 0 33933 72 0 0 25 0 1 0 426277003 98836480 22818 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24130 22818 603 41 0 24089 0
vsize: 96520
[startup+350.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 24530 0 0 0 34931 73 0 0 25 0 1 0 426277003 100167680 23177 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24455 23177 603 41 0 24414 0
vsize: 97820
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 25123 0 0 0 35930 74 0 0 25 0 1 0 426277003 102674432 23770 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25067 23770 603 41 0 25026 0
vsize: 100268
[startup+370.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 25712 0 0 0 36928 76 0 0 25 0 1 0 426277003 105058304 24359 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25649 24359 603 41 0 25608 0
vsize: 102596
[startup+380.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 26120 0 0 0 37927 78 0 0 25 0 1 0 426277003 106799104 24767 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26074 24767 603 41 0 26033 0
vsize: 104296
[startup+390.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 26451 0 0 0 38926 79 0 0 25 0 1 0 426277003 108126208 25098 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26398 25098 603 41 0 26357 0
vsize: 105592
[startup+400.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 26697 0 0 0 39925 80 0 0 25 0 1 0 426277003 109068288 25344 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26628 25344 603 41 0 26587 0
vsize: 106512
[startup+410.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 26990 0 0 0 40924 81 0 0 25 0 1 0 426277003 110268416 25637 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26921 25637 603 41 0 26880 0
vsize: 107684
[startup+420.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 27344 0 0 0 41923 82 0 0 25 0 1 0 426277003 111742976 25991 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27281 25991 603 41 0 27240 0
vsize: 109124
[startup+430.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 27706 0 0 0 42922 83 0 0 25 0 1 0 426277003 113205248 26353 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27638 26353 603 41 0 27597 0
vsize: 110552
[startup+440.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 28397 0 0 0 43921 84 0 0 25 0 1 0 426277003 116101120 27044 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28345 27044 603 41 0 28304 0
vsize: 113380
[startup+450.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 28630 0 0 0 44920 85 0 0 25 0 1 0 426277003 116932608 27277 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28548 27277 603 41 0 28507 0
vsize: 114192
[startup+460.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 28991 0 0 0 45919 87 0 0 25 0 1 0 426277003 118382592 27638 4294967295 134512640 134672761 3221224544 3221223584 134614280 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28902 27638 603 41 0 28861 0
vsize: 115608
[startup+470.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 29659 0 0 0 46917 89 0 0 25 0 1 0 426277003 120602624 27976 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29444 27976 603 41 0 29403 0
vsize: 117776
[startup+480.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 29659 0 0 0 47917 89 0 0 25 0 1 0 426277003 120602624 27976 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29444 27976 603 41 0 29403 0
vsize: 117776
[startup+490.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 29659 0 0 0 48917 89 0 0 25 0 1 0 426277003 120602624 27976 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29444 27976 603 41 0 29403 0
vsize: 117776
[startup+500.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 29659 0 0 0 49917 90 0 0 25 0 1 0 426277003 120602624 27976 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29444 27976 603 41 0 29403 0
vsize: 117776
[startup+510.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 29659 0 0 0 50917 90 0 0 25 0 1 0 426277003 120602624 27976 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29444 27976 603 41 0 29403 0
vsize: 117776
[startup+520.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 29659 0 0 0 51918 90 0 0 25 0 1 0 426277003 120602624 27976 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29444 27976 603 41 0 29403 0
vsize: 117776
[startup+530.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 29659 0 0 0 52918 90 0 0 25 0 1 0 426277003 120602624 27976 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29444 27976 603 41 0 29403 0
vsize: 117776
[startup+540.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 29659 0 0 0 53918 90 0 0 25 0 1 0 426277003 120602624 27976 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29444 27976 603 41 0 29403 0
vsize: 117776
[startup+550.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 29659 0 0 0 54918 90 0 0 25 0 1 0 426277003 120602624 27976 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29444 27976 603 41 0 29403 0
vsize: 117776
[startup+560.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 29659 0 0 0 55918 90 0 0 25 0 1 0 426277003 120602624 27976 4294967295 134512640 134672761 3221224544 3221223728 134616001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29444 27976 603 41 0 29403 0
vsize: 117776
[startup+570.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 29659 0 0 0 56918 90 0 0 25 0 1 0 426277003 120602624 27976 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29444 27976 603 41 0 29403 0
vsize: 117776
[startup+580.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 29659 0 0 0 57918 90 0 0 25 0 1 0 426277003 120602624 27976 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29444 27976 603 41 0 29403 0
vsize: 117776
[startup+590.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 29659 0 0 0 58918 90 0 0 25 0 1 0 426277003 120602624 27976 4294967295 134512640 134672761 3221224544 3221223728 134615926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29444 27976 603 41 0 29403 0
vsize: 117776
[startup+600.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 29659 0 0 0 59918 90 0 0 25 0 1 0 426277003 120602624 27976 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29444 27976 603 41 0 29403 0
vsize: 117776
[startup+610.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 29659 0 0 0 60918 91 0 0 25 0 1 0 426277003 120602624 27976 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29444 27976 603 41 0 29403 0
vsize: 117776
[startup+620.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 29659 0 0 0 61918 91 0 0 25 0 1 0 426277003 120602624 27976 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29444 27976 603 41 0 29403 0
vsize: 117776
[startup+630.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 29659 0 0 0 62918 91 0 0 25 0 1 0 426277003 120602624 27976 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29444 27976 603 41 0 29403 0
vsize: 117776
[startup+640.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 29659 0 0 0 63918 91 0 0 25 0 1 0 426277003 120602624 27976 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29444 27976 603 41 0 29403 0
vsize: 117776
[startup+650.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 29659 0 0 0 64918 91 0 0 25 0 1 0 426277003 120602624 27976 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29444 27976 603 41 0 29403 0
vsize: 117776
[startup+660.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 29659 0 0 0 65919 91 0 0 25 0 1 0 426277003 120602624 27976 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29444 27976 603 41 0 29403 0
vsize: 117776
[startup+670.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 29659 0 0 0 66919 91 0 0 25 0 1 0 426277003 120602624 27976 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29444 27976 603 41 0 29403 0
vsize: 117776
[startup+680.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 29660 0 0 0 67919 91 0 0 25 0 1 0 426277003 120602624 27977 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29444 27977 603 41 0 29403 0
vsize: 117776
[startup+690.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 29661 0 0 0 68919 91 0 0 25 0 1 0 426277003 120602624 27978 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29444 27978 603 41 0 29403 0
vsize: 117776
[startup+700.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 29662 0 0 0 69919 91 0 0 25 0 1 0 426277003 120602624 27979 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29444 27979 603 41 0 29403 0
vsize: 117776
[startup+710.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 29664 0 0 0 70919 91 0 0 25 0 1 0 426277003 120602624 27981 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29444 27981 603 41 0 29403 0
vsize: 117776
[startup+720.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 29664 0 0 0 71920 91 0 0 25 0 1 0 426277003 120602624 27981 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29444 27981 603 41 0 29403 0
vsize: 117776
[startup+730.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 29664 0 0 0 72920 91 0 0 25 0 1 0 426277003 120602624 27981 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29444 27981 603 41 0 29403 0
vsize: 117776
[startup+740.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 29664 0 0 0 73920 91 0 0 25 0 1 0 426277003 120602624 27981 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29444 27981 603 41 0 29403 0
vsize: 117776
[startup+750.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 29664 0 0 0 74920 91 0 0 25 0 1 0 426277003 120602624 27981 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29444 27981 603 41 0 29403 0
vsize: 117776
[startup+760.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 29665 0 0 0 75920 91 0 0 25 0 1 0 426277003 120602624 27982 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29444 27982 603 41 0 29403 0
vsize: 117776
[startup+770.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 29666 0 0 0 76921 91 0 0 25 0 1 0 426277003 120602624 27983 4294967295 134512640 134672761 3221224544 3221223712 134553598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29444 27983 603 41 0 29403 0
vsize: 117776
[startup+780.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 29666 0 0 0 77921 91 0 0 25 0 1 0 426277003 120602624 27983 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29444 27983 603 41 0 29403 0
vsize: 117776
[startup+790.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 29666 0 0 0 78921 91 0 0 25 0 1 0 426277003 120602624 27983 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29444 27983 603 41 0 29403 0
vsize: 117776
[startup+800.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 29666 0 0 0 79921 91 0 0 25 0 1 0 426277003 120602624 27983 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29444 27983 603 41 0 29403 0
vsize: 117776
[startup+810.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 29666 0 0 0 80921 91 0 0 25 0 1 0 426277003 120602624 27983 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29444 27983 603 41 0 29403 0
vsize: 117776
[startup+820.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 29666 0 0 0 81921 91 0 0 25 0 1 0 426277003 120602624 27983 4294967295 134512640 134672761 3221224544 3221223728 134615638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29444 27983 603 41 0 29403 0
vsize: 117776
[startup+830.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 30014 0 0 0 82921 92 0 0 25 0 1 0 426277003 122068992 28331 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29802 28331 603 41 0 29761 0
vsize: 119208
[startup+840.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 30310 0 0 0 83920 92 0 0 25 0 1 0 426277003 123404288 28627 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30128 28627 603 41 0 30087 0
vsize: 120512
[startup+850.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 30667 0 0 0 84919 94 0 0 25 0 1 0 426277003 124850176 28984 4294967295 134512640 134672761 3221224544 3221223728 134615830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30481 28984 603 41 0 30440 0
vsize: 121924
[startup+860.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 30958 0 0 0 85917 95 0 0 25 0 1 0 426277003 126050304 29275 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30774 29275 603 41 0 30733 0
vsize: 123096
[startup+870.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 31260 0 0 0 86916 97 0 0 25 0 1 0 426277003 127250432 29577 4294967295 134512640 134672761 3221224544 3221223704 134614477 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31067 29577 603 41 0 31026 0
vsize: 124268
[startup+880.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 31602 0 0 0 87916 97 0 0 25 0 1 0 426277003 128716800 29919 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31425 29919 603 41 0 31384 0
vsize: 125700
[startup+890.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 32029 0 0 0 88915 98 0 0 25 0 1 0 426277003 130437120 30346 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31845 30346 603 41 0 31804 0
vsize: 127380
[startup+900.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 32423 0 0 0 89913 100 0 0 25 0 1 0 426277003 132022272 30740 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32232 30740 603 41 0 32191 0
vsize: 128928
[startup+910.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 32584 0 0 0 90913 100 0 0 25 0 1 0 426277003 132702208 30901 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32398 30901 603 41 0 32357 0
vsize: 129592
[startup+920.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 32862 0 0 0 91912 102 0 0 25 0 1 0 426277003 133890048 31179 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32688 31179 603 41 0 32647 0
vsize: 130752
[startup+930.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 33147 0 0 0 92911 102 0 0 25 0 1 0 426277003 135073792 31464 4294967295 134512640 134672761 3221224544 3221223584 134612636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32977 31464 603 41 0 32936 0
vsize: 131908
[startup+940.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 33360 0 0 0 93911 103 0 0 25 0 1 0 426277003 135872512 31677 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33172 31677 603 41 0 33131 0
vsize: 132688
[startup+950.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 33549 0 0 0 94910 104 0 0 25 0 1 0 426277003 136663040 31866 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33365 31866 603 41 0 33324 0
vsize: 133460
[startup+960.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 33761 0 0 0 95909 105 0 0 25 0 1 0 426277003 137596928 32078 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33593 32078 603 41 0 33552 0
vsize: 134372
[startup+970.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 34061 0 0 0 96908 106 0 0 25 0 1 0 426277003 138797056 32378 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33886 32378 603 41 0 33845 0
vsize: 135544
[startup+980.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 34304 0 0 0 97908 107 0 0 25 0 1 0 426277003 139845632 32621 4294967295 134512640 134672761 3221224544 3221223584 134613012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34142 32621 603 41 0 34101 0
vsize: 136568
[startup+990.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 34652 0 0 0 98907 108 0 0 25 0 1 0 426277003 141307904 32969 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34499 32969 603 41 0 34458 0
vsize: 137996
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 34916 0 0 0 99906 109 0 0 25 0 1 0 426277003 142364672 33233 4294967295 134512640 134672761 3221224544 3221223728 134615761 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34757 33233 603 41 0 34716 0
vsize: 139028
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 35219 0 0 0 100905 110 0 0 25 0 1 0 426277003 143556608 33536 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35048 33536 603 41 0 35007 0
vsize: 140192
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 35466 0 0 0 101905 110 0 0 25 0 1 0 426277003 144609280 33783 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35305 33783 603 41 0 35264 0
vsize: 141220
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 35694 0 0 0 102904 111 0 0 25 0 1 0 426277003 145539072 34011 4294967295 134512640 134672761 3221224544 3221223688 134616317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35532 34011 603 41 0 35491 0
vsize: 142128
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 35916 0 0 0 103904 112 0 0 25 0 1 0 426277003 146460672 34233 4294967295 134512640 134672761 3221224544 3221223688 134616299 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35757 34233 603 41 0 35716 0
vsize: 143028
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 36141 0 0 0 104903 113 0 0 25 0 1 0 426277003 147390464 34458 4294967295 134512640 134672761 3221224544 3221223688 134616356 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35984 34458 603 41 0 35943 0
vsize: 143936
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 36421 0 0 0 105902 114 0 0 25 0 1 0 426277003 148574208 34738 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36273 34738 603 41 0 36232 0
vsize: 145092
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 36722 0 0 0 106901 115 0 0 25 0 1 0 426277003 149770240 35039 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36565 35039 603 41 0 36524 0
vsize: 146260
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 36961 0 0 0 107900 116 0 0 25 0 1 0 426277003 150728704 35278 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36799 35278 603 41 0 36758 0
vsize: 147196
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 37275 0 0 0 108899 117 0 0 25 0 1 0 426277003 152039424 35592 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37119 35592 603 41 0 37078 0
vsize: 148476
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 37432 0 0 0 109898 118 0 0 25 0 1 0 426277003 152719360 35749 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37285 35749 603 41 0 37244 0
vsize: 149140
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 37608 0 0 0 110898 119 0 0 25 0 1 0 426277003 153378816 35925 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37446 35925 603 41 0 37405 0
vsize: 149784
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 37818 0 0 0 111897 119 0 0 25 0 1 0 426277003 154304512 36135 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37672 36135 603 41 0 37631 0
vsize: 150688
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 38052 0 0 0 112896 120 0 0 25 0 1 0 426277003 155226112 36369 4294967295 134512640 134672761 3221224544 3221223728 134615926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37897 36369 603 41 0 37856 0
vsize: 151588
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 38392 0 0 0 113895 122 0 0 25 0 1 0 426277003 156549120 36709 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38220 36709 603 41 0 38179 0
vsize: 152880
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 38724 0 0 0 114895 123 0 0 25 0 1 0 426277003 157863936 37041 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38541 37041 603 41 0 38500 0
vsize: 154164
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 39015 0 0 0 115894 123 0 0 25 0 1 0 426277003 159051776 37332 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38831 37332 603 41 0 38790 0
vsize: 155324
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 39247 0 0 0 116894 124 0 0 25 0 1 0 426277003 159973376 37564 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39056 37564 603 41 0 39015 0
vsize: 156224
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 39679 0 0 0 117893 125 0 0 25 0 1 0 426277003 161824768 37996 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39508 37996 603 41 0 39467 0
vsize: 158032
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 39952 0 0 0 118892 126 0 0 25 0 1 0 426277003 162885632 38269 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39767 38269 603 41 0 39726 0
vsize: 159068
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23863
Raw data (stat): 23863 (minisat+) R 23862 30927 30926 0 -1 0 40300 0 0 0 119890 128 0 0 25 0 1 0 426277003 164339712 38617 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40122 38617 603 41 0 40081 0
vsize: 160488
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 23863
Raw data (stat): 23863 (minisat+) Z 23862 30927 30926 0 -1 12 40300 0 0 0 119891 135 0 0 25 0 1 0 426277003 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.1
CPU time (s): 1200.27
CPU user time (s): 1198.91
CPU system time (s): 1.35879
CPU usage (%): 100.014
Max. virtual memory (Kb): 160488
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####