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/miplib/normalized-mps-v2-13-7-vpm1.opb
MD5SUM	96fe6be9d2b9e3e89a4b05733b0daf45
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	20
Optimality of the best value was proved	NO
Number of terms in the objective function	168
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	168
Number of bits of the sum of numbers in the objective function	8
Biggest number in a constraint	102400
Number of bits of the biggest number in a constraint	17
Biggest sum of numbers in a constraint	615983
Number of bits of the biggest sum of numbers	20
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.07084
Number of variables	2124
Total number of constraints	612
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	168
Number of constraints which are nor clauses,nor cardinality constraints	444
Minimum length of a constraint	1
Maximum length of a constraint	64
Trace number 18914

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        392696 kB
Buffers:         28460 kB
Cached:         589348 kB
SwapCached:        516 kB
Active:          19920 kB
Inactive:       599888 kB
HighTotal:      131008 kB
HighFree:        34804 kB
LowTotal:       903652 kB
LowFree:        357892 kB
SwapTotal:     2097892 kB
SwapFree:      2096480 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5116 kB
Slab:            16432 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 17:20:48 (client local time) WITH STATUS 0 IN 1200.33 SECONDS
stats: 17366 7 1200.33 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 486 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ##############################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 485]---> BDD-cost:    7
c ---[ 484]---> BDD-cost:    7
c ---[ 483]---> BDD-cost:    7
c ---[ 482]---> BDD-cost:    7
c ---[ 481]---> BDD-cost:    7
c ---[ 480]---> BDD-cost:    7
c ---[ 479]---> BDD-cost:    7
c ---[ 478]---> BDD-cost:    7
c ---[ 477]---> BDD-cost:    7
c ---[ 474]---> BDD-cost:    7
c ---[ 473]---> BDD-cost:    7
c ---[ 472]---> BDD-cost:    7
c ---[ 471]---> BDD-cost:    7
c ---[ 468]---> BDD-cost:    7
c ---[ 467]---> BDD-cost:    7
c ---[ 466]---> BDD-cost:    7
c ---[ 465]---> BDD-cost:    7
c ---[ 462]---> BDD-cost:    7
c ---[ 459]---> BDD-cost:    7
c ---[ 458]---> BDD-cost:    7
c ---[ 457]---> BDD-cost:    7
c ---[ 454]---> BDD-cost:    7
c ---[ 453]---> BDD-cost:    7
c ---[ 452]---> BDD-cost:    7
c ---[ 451]---> BDD-cost:    7
c ---[ 450]---> BDD-cost:    7
c ---[ 448]---> BDD-cost:    7
c ---[ 447]---> BDD-cost:    7
c ---[ 446]---> BDD-cost:    7
c ---[ 445]---> BDD-cost:    7
c ---[ 444]---> BDD-cost:    7
c ---[ 441]---> BDD-cost:    7
c ---[ 440]---> BDD-cost:    7
c ---[ 439]---> BDD-cost:    7
c ---[ 433]---> BDD-cost:    7
c ---[ 427]---> BDD-cost:    7
c ---[ 422]---> BDD-cost:    7
c ---[ 421]---> BDD-cost:    7
c ---[ 415]---> BDD-cost:    7
c ---[ 409]---> BDD-cost:    7
c ---[ 408]---> BDD-cost:    7
c ---[ 402]---> BDD-cost:    7
c ---[ 397]---> BDD-cost:    7
c ---[ 396]---> BDD-cost:    7
c ---[ 391]---> BDD-cost:    7
c ---[ 390]---> BDD-cost:    7
c ---[ 386]---> BDD-cost:    7
c ---[ 385]---> BDD-cost:    7
c ---[ 384]---> BDD-cost:    7
c ---[ 380]---> BDD-cost:    7
c ---[ 379]---> BDD-cost:    7
c ---[ 378]---> BDD-cost:    7
c ---[ 374]---> BDD-cost:    7
c ---[ 373]---> BDD-cost:    7
c ---[ 372]---> BDD-cost:    7
c ---[ 368]---> BDD-cost:    7
c ---[ 367]---> BDD-cost:    7
c ---[ 366]---> BDD-cost:    7
c ---[ 365]---> BDD-cost:    7
c ---[ 364]---> BDD-cost:    7
c ---[ 359]---> BDD-cost:    7
c ---[ 353]---> BDD-cost:    7
c ---[ 347]---> BDD-cost:    7
c ---[ 339]---> BDD-cost:    7
c ---[ 333]---> BDD-cost:    7
c ---[ 327]---> BDD-cost:    7
c ---[ 321]---> BDD-cost:    7
c ---[ 317]---> BDD-cost:   14
c ---[ 316]---> BDD-cost:   14
c ---[ 315]---> BDD-cost:   14
c ---[ 314]---> BDD-cost:   14
c ---[ 313]---> BDD-cost:   14
c ---[ 312]---> BDD-cost:   14
c ---[ 310]---> BDD-cost:   14
c ---[ 309]---> BDD-cost:   14
c ---[ 308]---> BDD-cost:   14
c ---[ 307]---> BDD-cost:   14
c ---[ 306]---> BDD-cost:   14
c ---[ 302]---> BDD-cost:   13
c ---[ 301]---> BDD-cost:   13
c ---[ 300]---> BDD-cost:   13
c ---[ 295]---> BDD-cost:   13
c ---[ 294]---> BDD-cost:   13
c ---[ 290]---> BDD-cost:   15
c ---[ 289]---> BDD-cost:   15
c ---[ 288]---> BDD-cost:   15
c ---[ 287]---> BDD-cost:   13
c ---[ 286]---> BDD-cost:   13
c ---[ 285]---> BDD-cost:   13
c ---[ 284]---> BDD-cost:   13
c ---[ 283]---> BDD-cost:   13
c ---[ 282]---> BDD-cost:   13
c ---[ 280]---> BDD-cost:   13
c ---[ 279]---> BDD-cost:   13
c ---[ 278]---> BDD-cost:   13
c ---[ 277]---> BDD-cost:   13
c ---[ 276]---> BDD-cost:   13
c ---[ 274]---> Sorter-cost: 1988     Base: 2 2 2 5 5 2 2 2 2 2 3
c ---[ 264]---> Sorter-cost: 1826     Base: 2 2 2 5 5 2 2 2 3 2 2 2
c ---[ 260]---> Adder-cost: 262   maxlim: 300367   bits: 19/19
c ---[ 258]---> Adder-cost: 262   maxlim: 300367   bits: 19/19
c ---[ 256]---> Sorter-cost: 2565     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 254]---> Sorter-cost: 2565     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 252]---> Adder-cost: 262   maxlim: 261967   bits: 19/18
c ---[ 250]---> Sorter-cost: 1411     Base: 2 2 2 2 5 5 2 2 2 2 2
c ---[ 248]---> Sorter-cost: 2230     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 246]---> Sorter-cost: 2232     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 244]---> Sorter-cost: 2232     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 242]---> Sorter-cost: 2159     Base: 2 2 2 2 2 2 2 2 2 2 3 2 2
c ---[ 236]---> Sorter-cost: 1318     Base: 2 2 2 2 5 5 2 2 2 2 2
c ---[ 234]---> Sorter-cost: 2540     Base: 2 2 2 2 5 5 2 2 2 2 2 2
c ---[ 232]---> Sorter-cost: 1903     Base: 2 2 2 2 2 2 2 2 2 2 2 3
c ---[ 224]---> Sorter-cost: 1582     Base: 2 2 2 5 5 2 2 2 2 2 3
c ---[ 222]---> Adder-cost: 260   maxlim: 219983   bits: 19/18
c ---[ 216]---> Sorter-cost: 1742     Base: 2 2 2 5 5 2 2 2 2 2 2
c ---[ 214]---> Sorter-cost: 2471     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 212]---> Sorter-cost: 2473     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 210]---> Sorter-cost: 3095     Base: 2 2 2 2 2 3 5 2 2 2 5
c ---[ 208]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[ 206]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[ 204]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[ 202]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[ 200]---> Sorter-cost: 1882     Base: 2 2 2 2 5 5 2 2 2 5
c ---[ 198]---> Sorter-cost: 3211     Base: 2 2 2 2 5 5 2 2 2 2 5
c ---[ 196]---> Adder-cost: 254   maxlim: 123183   bits: 18/17
c ---[ 194]---> Adder-cost: 254   maxlim: 123183   bits: 18/17
c ---[ 192]---> Adder-cost: 254   maxlim: 123183   bits: 18/17
c ---[ 191]---> BDD-cost:   33
c ---[ 190]---> Sorter-cost:  269     Base: 2 2 2 2 2 2
c ---[ 189]---> Sorter-cost:  283     Base: 2 2 2 2 2 2
c ---[ 188]---> Sorter-cost:  540     Base: 2 2 2 2 2 2
c ---[ 187]---> Sorter-cost:  761     Base: 2 2 2 2 2 2
c ---[ 186]---> Sorter-cost:  655     Base: 2 2 2 2 2 2
c ---[ 185]---> BDD-cost:   33
c ---[ 184]---> Sorter-cost:  269     Base: 2 2 2 2 2 2
c ---[ 183]---> Sorter-cost:  283     Base: 2 2 2 2 2 2
c ---[ 182]---> Sorter-cost:  520     Base: 2 2 2 2 2 2
c ---[ 181]---> Sorter-cost:  707     Base: 2 2 2 2 2 2
c ---[ 180]---> Sorter-cost:  705     Base: 2 2 2 2 2 2
c ---[ 179]---> BDD-cost:   33
c ---[ 178]---> Sorter-cost:  269     Base: 2 2 2 2 2 2
c ---[ 177]---> Sorter-cost:  274     Base: 2 2 2 2 2 2
c ---[ 176]---> Sorter-cost:  527     Base: 2 2 2 2 2 2
c ---[ 175]---> Sorter-cost:  720     Base: 2 2 2 2 2 2
c ---[ 174]---> Sorter-cost:  692     Base: 2 2 2 2 2 2
c ---[ 173]---> BDD-cost:   33
c ---[ 172]---> Sorter-cost:  253     Base: 2 2 2 2 2 2
c ---[ 171]---> Sorter-cost:  274     Base: 2 2 2 2 2 2
c ---[ 170]---> Sorter-cost:  486     Base: 2 2 2 2 2 2
c ---[ 169]---> Sorter-cost:  695     Base: 2 2 2 2 2 2
c ---[ 168]---> Sorter-cost:  625     Base: 2 2 2 2 2 2
c ---[ 167]---> BDD-cost:    3
c ---[ 166]---> BDD-cost:    3
c ---[ 165]---> BDD-cost:    3
c ---[ 164]---> BDD-cost:    3
c ---[ 163]---> BDD-cost:    3
c ---[ 162]---> BDD-cost:    3
c ---[ 161]---> BDD-cost:    3
c ---[ 160]---> BDD-cost:    3
c ---[ 159]---> BDD-cost:    3
c ---[ 158]---> BDD-cost:    7
c ---[ 157]---> BDD-cost:    7
c ---[ 156]---> BDD-cost:    3
c ---[ 155]---> BDD-cost:    3
c ---[ 154]---> BDD-cost:    3
c ---[ 153]---> BDD-cost:    3
c ---[ 152]---> BDD-cost:    7
c ---[ 151]---> BDD-cost:    7
c ---[ 150]---> BDD-cost:    3
c ---[ 149]---> BDD-cost:    3
c ---[ 148]---> BDD-cost:    3
c ---[ 147]---> BDD-cost:    3
c ---[ 146]---> BDD-cost:    7
c ---[ 145]---> BDD-cost:    7
c ---[ 144]---> BDD-cost:    3
c ---[ 142]---> BDD-cost:    7
c ---[ 141]---> BDD-cost:    3
c ---[ 140]---> BDD-cost:    3
c ---[ 139]---> BDD-cost:    3
c ---[ 138]---> BDD-cost:    7
c ---[ 136]---> BDD-cost:    3
c ---[ 135]---> BDD-cost:    3
c ---[ 134]---> BDD-cost:    3
c ---[ 133]---> BDD-cost:    3
c ---[ 132]---> BDD-cost:    3
c ---[ 130]---> BDD-cost:    3
c ---[ 129]---> BDD-cost:    3
c ---[ 128]---> BDD-cost:    3
c ---[ 127]---> BDD-cost:    3
c ---[ 126]---> BDD-cost:    3
c ---[ 124]---> BDD-cost:    7
c ---[ 123]---> BDD-cost:    3
c ---[ 122]---> BDD-cost:    3
c ---[ 121]---> BDD-cost:    3
c ---[ 120]---> BDD-cost:    7
c ---[ 116]---> BDD-cost:    7
c ---[ 115]---> BDD-cost:    3
c ---[ 114]---> BDD-cost:    6
c ---[ 110]---> BDD-cost:    7
c ---[ 109]---> BDD-cost:    3
c ---[ 108]---> BDD-cost:    6
c ---[ 104]---> BDD-cost:    3
c ---[ 103]---> BDD-cost:    3
c ---[ 102]---> BDD-cost:    5
c ---[  98]---> BDD-cost:    7
c ---[  97]---> BDD-cost:    3
c ---[  96]---> BDD-cost:    6
c ---[  91]---> BDD-cost:    3
c ---[  90]---> BDD-cost:    3
c ---[  85]---> BDD-cost:    7
c ---[  84]---> BDD-cost:    3
c ---[  79]---> BDD-cost:    3
c ---[  78]---> BDD-cost:    3
c ---[  73]---> BDD-cost:    3
c ---[  72]---> BDD-cost:    3
c ---[  68]---> BDD-cost:    3
c ---[  67]---> BDD-cost:    3
c ---[  66]---> BDD-cost:    3
c ---[  62]---> BDD-cost:    3
c ---[  61]---> BDD-cost:    3
c ---[  60]---> BDD-cost:    3
c ---[  56]---> BDD-cost:    3
c ---[  55]---> BDD-cost:    3
c ---[  54]---> BDD-cost:    3
c ---[  50]---> BDD-cost:    3
c ---[  49]---> BDD-cost:    3
c ---[  48]---> BDD-cost:    3
c ---[  47]---> BDD-cost:    3
c ---[  46]---> BDD-cost:    3
c ---[  45]---> BDD-cost:    6
c ---[  44]---> BDD-cost:    6
c ---[  43]---> BDD-cost:    6
c ---[  42]---> BDD-cost:    6
c ---[  41]---> BDD-cost:    3
c ---[  40]---> BDD-cost:    7
c ---[  39]---> BDD-cost:    6
c ---[  38]---> BDD-cost:    6
c ---[  37]---> BDD-cost:    6
c ---[  36]---> BDD-cost:    6
c ---[  35]---> BDD-cost:    3
c ---[  34]---> BDD-cost:    7
c ---[  33]---> BDD-cost:    5
c ---[  32]---> BDD-cost:    5
c ---[  31]---> BDD-cost:    5
c ---[  30]---> BDD-cost:    5
c ---[  29]---> BDD-cost:    3
c ---[  28]---> BDD-cost:    7
c ---[  27]---> BDD-cost:    5
c ---[  26]---> BDD-cost:    5
c ---[  25]---> BDD-cost:    5
c ---[  24]---> BDD-cost:    5
c ---[  22]---> BDD-cost:    7
c ---[  21]---> BDD-cost:    3
c ---[  20]---> BDD-cost:    6
c ---[  19]---> BDD-cost:    6
c ---[  18]---> BDD-cost:    6
c ---[  16]---> BDD-cost:    7
c ---[  15]---> BDD-cost:    3
c ---[  14]---> BDD-cost:    6
c ---[  13]---> BDD-cost:    6
c ---[  12]---> BDD-cost:    6
c ---[  10]---> BDD-cost:    7
c ---[   9]---> BDD-cost:    3
c ---[   8]---> BDD-cost:    6
c ---[   7]---> BDD-cost:    6
c ---[   6]---> BDD-cost:    6
c ---[   4]---> BDD-cost:    6
c ---[   3]---> BDD-cost:    3
c ---[   2]---> BDD-cost:    5
c ---[   1]---> BDD-cost:    5
c ---[   0]---> BDD-cost:    5
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  150816   377413 |   45244       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/46036          
c   -- var.elim.:  2000/46036          
c   -- var.elim.:  3000/46036          
c   -- var.elim.:  4000/46036          
c   -- var.elim.:  5000/46036          
c   -- var.elim.:  6000/46036          
c   -- var.elim.:  7000/46036          
c   -- var.elim.:  8000/46036          
c   -- var.elim.:  9000/46036          
c   -- var.elim.:  10000/46036          
c   -- var.elim.:  11000/46036          
c   -- var.elim.:  12000/46036          
c   -- var.elim.:  13000/46036          
c   -- var.elim.:  14000/46036          
c   -- var.elim.:  15000/46036          
c   -- var.elim.:  16000/46036          
c   -- var.elim.:  17000/46036          
c   -- var.elim.:  18000/46036          
c   -- var.elim.:  19000/46036          
c   -- var.elim.:  20000/46036          
c   -- var.elim.:  21000/46036          
c   -- var.elim.:  22000/46036          
c   -- var.elim.:  23000/46036          
c   -- var.elim.:  24000/46036          
c   -- var.elim.:  25000/46036          
c   -- var.elim.:  26000/46036          
c   -- var.elim.:  27000/46036          
c   -- var.elim.:  28000/46036          
c   -- var.elim.:  29000/46036          
c   -- var.elim.:  30000/46036          
c   -- var.elim.:  31000/46036          
c   -- var.elim.:  32000/46036          
c   -- var.elim.:  33000/46036          
c   -- var.elim.:  34000/46036          
c   -- var.elim.:  35000/46036          
c   -- var.elim.:  36000/46036          
c   -- var.elim.:  37000/46036          
c   -- var.elim.:  38000/46036          
c   -- var.elim.:  39000/46036          
c   -- var.elim.:  40000/460#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.95 0.91 2/54 9758
Raw data (stat): 9758 (runsolver) R 9757 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546714526 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.0013 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 9758
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 8802 0 0 0 971 27 0 0 25 0 1 0 546714526 35987456 7584 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8786 7584 603 41 0 8745 0
vsize: 35144
[startup+20.002 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 9758
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 9235 0 0 0 1970 29 0 0 25 0 1 0 546714526 37769216 8017 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9221 8017 603 41 0 9180 0
vsize: 36884
[startup+30.0023 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 9760
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 9909 0 0 0 2967 31 0 0 25 0 1 0 546714526 40394752 8691 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9862 8691 603 41 0 9821 0
vsize: 39448
[startup+40.0024 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 9760
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 10852 0 0 0 3965 33 0 0 25 0 1 0 546714526 44371968 9634 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10833 9634 603 41 0 10792 0
vsize: 43332
[startup+50.0032 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 9760
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 11501 0 0 0 4963 35 0 0 25 0 1 0 546714526 47017984 10283 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11479 10283 603 41 0 11438 0
vsize: 45916
[startup+60.0039 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 9760
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 12654 0 0 0 5959 39 0 0 25 0 1 0 546714526 51765248 11436 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12638 11436 603 41 0 12597 0
vsize: 50552
[startup+70.0046 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 9760
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 13364 0 0 0 6956 42 0 0 25 0 1 0 546714526 54669312 12146 4294967295 134512640 134672761 3221224544 3221223716 134615856 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13347 12146 603 41 0 13306 0
vsize: 53388
[startup+80.0053 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 9760
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 14332 0 0 0 7953 46 0 0 25 0 1 0 546714526 58761216 13114 4294967295 134512640 134672761 3221224544 3221223536 134565078 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14346 13114 603 41 0 14305 0
vsize: 57384
[startup+90.0061 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 9760
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 15070 0 0 0 8951 48 0 0 25 0 1 0 546714526 61788160 13852 4294967295 134512640 134672761 3221224544 3221223760 134610366 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15085 13852 603 41 0 15044 0
vsize: 60340
[startup+100.007 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 9760
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 16137 0 0 0 9948 51 0 0 25 0 1 0 546714526 66125824 14919 4294967295 134512640 134672761 3221224544 3221223728 134615461 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16144 14919 603 41 0 16103 0
vsize: 64576
[startup+110.008 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 9760
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 16815 0 0 0 10945 54 0 0 25 0 1 0 546714526 68915200 15597 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16825 15597 603 41 0 16784 0
vsize: 67300
[startup+120.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9760
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 17474 0 0 0 11943 56 0 0 25 0 1 0 546714526 71577600 16256 4294967295 134512640 134672761 3221224544 3221223584 134612892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17475 16256 603 41 0 17434 0
vsize: 69900
[startup+130.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9760
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 18055 0 0 0 12942 57 0 0 25 0 1 0 546714526 73953280 16837 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18055 16837 603 41 0 18014 0
vsize: 72220
[startup+140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9760
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 18495 0 0 0 13941 58 0 0 25 0 1 0 546714526 75694080 17277 4294967295 134512640 134672761 3221224544 3221223728 134615951 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18480 17277 603 41 0 18439 0
vsize: 73920
[startup+150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9760
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 18906 0 0 0 14940 59 0 0 25 0 1 0 546714526 77406208 17688 4294967295 134512640 134672761 3221224544 3221223688 134616189 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18898 17688 603 41 0 18857 0
vsize: 75592
[startup+160.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9760
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 19210 0 0 0 15939 61 0 0 25 0 1 0 546714526 78602240 17992 4294967295 134512640 134672761 3221224544 3221223728 134615779 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19190 17992 603 41 0 19149 0
vsize: 76760
[startup+170.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9760
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 19574 0 0 0 16938 62 0 0 25 0 1 0 546714526 80048128 18356 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19543 18356 603 41 0 19502 0
vsize: 78172
[startup+180.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9760
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 19938 0 0 0 17937 63 0 0 25 0 1 0 546714526 81629184 18720 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19929 18720 603 41 0 19888 0
vsize: 79716
[startup+190.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9760
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 20375 0 0 0 18937 64 0 0 25 0 1 0 546714526 83386368 19157 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20358 19157 603 41 0 20317 0
vsize: 81432
[startup+200.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9760
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 20677 0 0 0 19936 65 0 0 25 0 1 0 546714526 84713472 19459 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20682 19459 603 41 0 20641 0
vsize: 82728
[startup+210.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9760
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 20993 0 0 0 20935 65 0 0 25 0 1 0 546714526 86425600 19775 4294967295 134512640 134672761 3221224544 3221223688 134616139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21100 19775 603 41 0 21059 0
vsize: 84400
[startup+220.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9760
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 21289 0 0 0 21934 67 0 0 25 0 1 0 546714526 87605248 20071 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21388 20071 603 41 0 21347 0
vsize: 85552
[startup+230.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9760
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 21625 0 0 0 22934 67 0 0 25 0 1 0 546714526 89051136 20407 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21741 20408 603 41 0 21700 0
vsize: 86964
[startup+240.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9760
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 21981 0 0 0 23933 68 0 0 25 0 1 0 546714526 90505216 20763 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22096 20763 603 41 0 22055 0
vsize: 88384
[startup+250.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9760
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 22325 0 0 0 24932 70 0 0 25 0 1 0 546714526 91947008 21107 4294967295 134512640 134672761 3221224544 3221223728 134615581 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22448 21107 603 41 0 22407 0
vsize: 89792
[startup+260.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9760
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 22977 0 0 0 25930 71 0 0 25 0 1 0 546714526 94584832 21759 4294967295 134512640 134672761 3221224544 3221223728 134615830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23092 21759 603 41 0 23051 0
vsize: 92368
[startup+270.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9760
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 23728 0 0 0 26929 73 0 0 25 0 1 0 546714526 97619968 22510 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23833 22510 603 41 0 23792 0
vsize: 95332
[startup+280.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9760
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 24418 0 0 0 27927 75 0 0 25 0 1 0 546714526 100384768 23200 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24508 23200 603 41 0 24467 0
vsize: 98032
[startup+290.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 25037 0 0 0 28924 78 0 0 25 0 1 0 546714526 102912000 23819 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25125 23819 603 41 0 25084 0
vsize: 100500
[startup+300.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 25662 0 0 0 29922 80 0 0 25 0 1 0 546714526 105431040 24444 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25740 24444 603 41 0 25699 0
vsize: 102960
[startup+310.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 26241 0 0 0 30920 82 0 0 25 0 1 0 546714526 107806720 25023 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26320 25023 603 41 0 26279 0
vsize: 105280
[startup+320.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 26794 0 0 0 31920 83 0 0 25 0 1 0 546714526 110051328 25576 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26868 25576 603 41 0 26827 0
vsize: 107472
[startup+330.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 27258 0 0 0 32918 85 0 0 25 0 1 0 546714526 112017408 26040 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27348 26040 603 41 0 27307 0
vsize: 109392
[startup+340.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 27681 0 0 0 33918 86 0 0 25 0 1 0 546714526 113733632 26463 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27767 26463 603 41 0 27726 0
vsize: 111068
[startup+350.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 28111 0 0 0 34916 87 0 0 25 0 1 0 546714526 115437568 26893 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28183 26893 603 41 0 28142 0
vsize: 112732
[startup+360.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 28533 0 0 0 35915 89 0 0 25 0 1 0 546714526 117153792 27315 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28602 27316 603 41 0 28561 0
vsize: 114408
[startup+370.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 28830 0 0 0 36914 90 0 0 25 0 1 0 546714526 118476800 27612 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28925 27612 603 41 0 28884 0
vsize: 115700
[startup+380.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 29051 0 0 0 37913 91 0 0 25 0 1 0 546714526 119398400 27833 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29150 27833 603 41 0 29109 0
vsize: 116600
[startup+390.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 29261 0 0 0 38913 91 0 0 25 0 1 0 546714526 120233984 28043 4294967295 134512640 134672761 3221224544 3221223688 134616178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29354 28043 603 41 0 29313 0
vsize: 117416
[startup+400.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 29562 0 0 0 39913 92 0 0 25 0 1 0 546714526 121442304 28344 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29649 28344 603 41 0 29608 0
vsize: 118596
[startup+410.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 29898 0 0 0 40912 93 0 0 25 0 1 0 546714526 122757120 28680 4294967295 134512640 134672761 3221224544 3221223688 134616317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29970 28680 603 41 0 29929 0
vsize: 119880
[startup+420.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 30144 0 0 0 41911 93 0 0 25 0 1 0 546714526 123822080 28926 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30230 28926 603 41 0 30189 0
vsize: 120920
[startup+430.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 30409 0 0 0 42911 94 0 0 25 0 1 0 546714526 124878848 29191 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30488 29191 603 41 0 30447 0
vsize: 121952
[startup+440.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 30671 0 0 0 43910 95 0 0 25 0 1 0 546714526 125935616 29453 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30746 29453 603 41 0 30705 0
vsize: 122984
[startup+450.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 30925 0 0 0 44910 96 0 0 25 0 1 0 546714526 127025152 29707 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31012 29707 603 41 0 30971 0
vsize: 124048
[startup+460.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 31203 0 0 0 45909 97 0 0 25 0 1 0 546714526 128102400 29985 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31275 29985 603 41 0 31234 0
vsize: 125100
[startup+470.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 31495 0 0 0 46908 98 0 0 25 0 1 0 546714526 129318912 30277 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31572 30277 603 41 0 31531 0
vsize: 126288
[startup+480.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 31779 0 0 0 47907 99 0 0 25 0 1 0 546714526 130519040 30561 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31865 30561 603 41 0 31824 0
vsize: 127460
[startup+490.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 32032 0 0 0 48907 100 0 0 25 0 1 0 546714526 131571712 30814 4294967295 134512640 134672761 3221224544 3221223688 134616233 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32122 30814 603 41 0 32081 0
vsize: 128488
[startup+500.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 32239 0 0 0 49906 101 0 0 25 0 1 0 546714526 132358144 31021 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32314 31021 603 41 0 32273 0
vsize: 129256
[startup+510.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 32517 0 0 0 50905 101 0 0 25 0 1 0 546714526 133541888 31299 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32603 31299 603 41 0 32562 0
vsize: 130412
[startup+520.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 32793 0 0 0 51905 102 0 0 25 0 1 0 546714526 134590464 31575 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32859 31575 603 41 0 32818 0
vsize: 131436
[startup+530.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 33045 0 0 0 52905 102 0 0 25 0 1 0 546714526 135639040 31827 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33115 31827 603 41 0 33074 0
vsize: 132460
[startup+540.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 33299 0 0 0 53904 103 0 0 25 0 1 0 546714526 136687616 32081 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33371 32081 603 41 0 33330 0
vsize: 133484
[startup+550.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 33577 0 0 0 54903 105 0 0 25 0 1 0 546714526 137740288 32359 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33628 32359 603 41 0 33587 0
vsize: 134512
[startup+560.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 33870 0 0 0 55902 106 0 0 25 0 1 0 546714526 138997760 32652 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33935 32652 603 41 0 33894 0
vsize: 135740
[startup+570.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 34150 0 0 0 56902 106 0 0 25 0 1 0 546714526 140177408 32932 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34223 32932 603 41 0 34182 0
vsize: 136892
[startup+580.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 34411 0 0 0 57901 108 0 0 25 0 1 0 546714526 141225984 33193 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34479 33193 603 41 0 34438 0
vsize: 137916
[startup+590.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 34642 0 0 0 58900 108 0 0 25 0 1 0 546714526 142204928 33424 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34718 33424 603 41 0 34677 0
vsize: 138872
[startup+600.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 34953 0 0 0 59900 109 0 0 25 0 1 0 546714526 143523840 33735 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35040 33735 603 41 0 34999 0
vsize: 140160
[startup+610.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 35184 0 0 0 60899 110 0 0 25 0 1 0 546714526 144445440 33966 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35265 33966 603 41 0 35224 0
vsize: 141060
[startup+620.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 35383 0 0 0 61898 111 0 0 25 0 1 0 546714526 145235968 34165 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35458 34165 603 41 0 35417 0
vsize: 141832
[startup+630.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 35565 0 0 0 62898 111 0 0 25 0 1 0 546714526 146022400 34347 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35650 34347 603 41 0 35609 0
vsize: 142600
[startup+640.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 35664 0 0 0 63898 111 0 0 25 0 1 0 546714526 146477056 34446 4294967295 134512640 134672761 3221224544 3221223688 134616254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35761 34446 603 41 0 35720 0
vsize: 143044
[startup+650.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 36256 0 0 0 64896 113 0 0 25 0 1 0 546714526 148848640 35038 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36340 35038 603 41 0 36299 0
vsize: 145360
[startup+660.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 36718 0 0 0 65895 114 0 0 25 0 1 0 546714526 150691840 35500 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36790 35500 603 41 0 36749 0
vsize: 147160
[startup+670.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 36963 0 0 0 66895 115 0 0 25 0 1 0 546714526 151740416 35745 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37046 35745 603 41 0 37005 0
vsize: 148184
[startup+680.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 37213 0 0 0 67894 116 0 0 25 0 1 0 546714526 152788992 35995 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37302 35995 603 41 0 37261 0
vsize: 149208
[startup+690.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 37503 0 0 0 68894 117 0 0 25 0 1 0 546714526 153972736 36285 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37591 36285 603 41 0 37550 0
vsize: 150364
[startup+700.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 37809 0 0 0 69893 118 0 0 25 0 1 0 546714526 155152384 36591 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37879 36591 603 41 0 37838 0
vsize: 151516
[startup+710.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 38109 0 0 0 70892 118 0 0 25 0 1 0 546714526 156336128 36891 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38168 36891 603 41 0 38127 0
vsize: 152672
[startup+720.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 38367 0 0 0 71892 119 0 0 25 0 1 0 546714526 157396992 37149 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38427 37149 603 41 0 38386 0
vsize: 153708
[startup+730.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 38561 0 0 0 72892 119 0 0 25 0 1 0 546714526 158232576 37343 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38631 37343 603 41 0 38590 0
vsize: 154524
[startup+740.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 38744 0 0 0 73891 120 0 0 25 0 1 0 546714526 159019008 37526 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38823 37526 603 41 0 38782 0
vsize: 155292
[startup+750.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 38952 0 0 0 74891 120 0 0 25 0 1 0 546714526 159948800 37734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39050 37734 603 41 0 39009 0
vsize: 156200
[startup+760.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39564 0 0 0 75890 122 0 0 25 0 1 0 546714526 162725888 38314 4294967295 134512640 134672761 3221224544 3221223600 134644266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39728 38314 603 41 0 39687 0
vsize: 158912
[startup+770.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39654 0 0 0 76889 123 0 0 25 0 1 0 546714526 161677312 38153 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38153 603 41 0 39431 0
vsize: 157888
[startup+780.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39654 0 0 0 77889 123 0 0 25 0 1 0 546714526 161677312 38153 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38153 603 41 0 39431 0
vsize: 157888
[startup+790.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39654 0 0 0 78890 123 0 0 25 0 1 0 546714526 161677312 38153 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38153 603 41 0 39431 0
vsize: 157888
[startup+800.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39654 0 0 0 79890 123 0 0 25 0 1 0 546714526 161677312 38153 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38153 603 41 0 39431 0
vsize: 157888
[startup+810.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39654 0 0 0 80890 123 0 0 25 0 1 0 546714526 161677312 38153 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38153 603 41 0 39431 0
vsize: 157888
[startup+820.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39654 0 0 0 81890 123 0 0 25 0 1 0 546714526 161677312 38153 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38153 603 41 0 39431 0
vsize: 157888
[startup+830.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39654 0 0 0 82890 123 0 0 25 0 1 0 546714526 161677312 38153 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38153 603 41 0 39431 0
vsize: 157888
[startup+840.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39654 0 0 0 83891 123 0 0 25 0 1 0 546714526 161677312 38153 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38153 603 41 0 39431 0
vsize: 157888
[startup+850.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39654 0 0 0 84891 123 0 0 25 0 1 0 546714526 161677312 38153 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38153 603 41 0 39431 0
vsize: 157888
[startup+860.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39657 0 0 0 85891 123 0 0 25 0 1 0 546714526 161677312 38156 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38156 603 41 0 39431 0
vsize: 157888
[startup+870.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39657 0 0 0 86891 123 0 0 25 0 1 0 546714526 161677312 38156 4294967295 134512640 134672761 3221224544 3221223728 134615594 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38156 603 41 0 39431 0
vsize: 157888
[startup+880.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39657 0 0 0 87891 123 0 0 25 0 1 0 546714526 161677312 38156 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38156 603 41 0 39431 0
vsize: 157888
[startup+890.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39657 0 0 0 88891 123 0 0 25 0 1 0 546714526 161677312 38156 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38156 603 41 0 39431 0
vsize: 157888
[startup+900.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39657 0 0 0 89892 123 0 0 25 0 1 0 546714526 161677312 38156 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38156 603 41 0 39431 0
vsize: 157888
[startup+910.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39658 0 0 0 90892 123 0 0 25 0 1 0 546714526 161677312 38157 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38157 603 41 0 39431 0
vsize: 157888
[startup+920.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39658 0 0 0 91892 123 0 0 25 0 1 0 546714526 161677312 38157 4294967295 134512640 134672761 3221224544 3221223688 134616178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38157 603 41 0 39431 0
vsize: 157888
[startup+930.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39658 0 0 0 92892 123 0 0 25 0 1 0 546714526 161677312 38157 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38157 603 41 0 39431 0
vsize: 157888
[startup+940.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39658 0 0 0 93892 123 0 0 25 0 1 0 546714526 161677312 38157 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38157 603 41 0 39431 0
vsize: 157888
[startup+950.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39658 0 0 0 94893 123 0 0 25 0 1 0 546714526 161677312 38157 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38157 603 41 0 39431 0
vsize: 157888
[startup+960.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39660 0 0 0 95893 123 0 0 25 0 1 0 546714526 161677312 38159 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38159 603 41 0 39431 0
vsize: 157888
[startup+970.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39660 0 0 0 96893 123 0 0 25 0 1 0 546714526 161677312 38159 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38159 603 41 0 39431 0
vsize: 157888
[startup+980.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39660 0 0 0 97893 123 0 0 25 0 1 0 546714526 161677312 38159 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38159 603 41 0 39431 0
vsize: 157888
[startup+990.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39660 0 0 0 98893 123 0 0 25 0 1 0 546714526 161677312 38159 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38159 603 41 0 39431 0
vsize: 157888
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39660 0 0 0 99893 123 0 0 25 0 1 0 546714526 161677312 38159 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38159 603 41 0 39431 0
vsize: 157888
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39663 0 0 0 100894 123 0 0 25 0 1 0 546714526 161677312 38162 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38162 603 41 0 39431 0
vsize: 157888
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39666 0 0 0 101894 123 0 0 25 0 1 0 546714526 161677312 38165 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38165 603 41 0 39431 0
vsize: 157888
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39666 0 0 0 102894 123 0 0 25 0 1 0 546714526 161677312 38165 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38165 603 41 0 39431 0
vsize: 157888
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39667 0 0 0 103894 123 0 0 25 0 1 0 546714526 161677312 38166 4294967295 134512640 134672761 3221224544 3221223728 134615686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38166 603 41 0 39431 0
vsize: 157888
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39667 0 0 0 104894 123 0 0 25 0 1 0 546714526 161677312 38166 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38166 603 41 0 39431 0
vsize: 157888
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39670 0 0 0 105895 123 0 0 25 0 1 0 546714526 161677312 38169 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38169 603 41 0 39431 0
vsize: 157888
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39670 0 0 0 106895 123 0 0 25 0 1 0 546714526 161677312 38169 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38169 603 41 0 39431 0
vsize: 157888
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39671 0 0 0 107895 123 0 0 25 0 1 0 546714526 161677312 38170 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38170 603 41 0 39431 0
vsize: 157888
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39671 0 0 0 108895 123 0 0 25 0 1 0 546714526 161677312 38170 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38170 603 41 0 39431 0
vsize: 157888
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39672 0 0 0 109895 123 0 0 25 0 1 0 546714526 161677312 38171 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38171 603 41 0 39431 0
vsize: 157888
[startup+1110.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39672 0 0 0 110898 123 0 0 25 0 1 0 546714526 161677312 38171 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38171 603 41 0 39431 0
vsize: 157888
[startup+1120.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39672 0 0 0 111899 123 0 0 25 0 1 0 546714526 161677312 38171 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38171 603 41 0 39431 0
vsize: 157888
[startup+1130.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39672 0 0 0 112899 123 0 0 25 0 1 0 546714526 161677312 38171 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38171 603 41 0 39431 0
vsize: 157888
[startup+1140.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39672 0 0 0 113899 124 0 0 25 0 1 0 546714526 161677312 38171 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38171 603 41 0 39431 0
vsize: 157888
[startup+1150.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39673 0 0 0 114899 124 0 0 25 0 1 0 546714526 161677312 38172 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38172 603 41 0 39431 0
vsize: 157888
[startup+1160.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39673 0 0 0 115900 124 0 0 25 0 1 0 546714526 161677312 38172 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38172 603 41 0 39431 0
vsize: 157888
[startup+1170.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39674 0 0 0 116900 124 0 0 25 0 1 0 546714526 161677312 38173 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38173 603 41 0 39431 0
vsize: 157888
[startup+1180.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39676 0 0 0 117900 124 0 0 25 0 1 0 546714526 161677312 38175 4294967295 134512640 134672761 3221224544 3221223680 134614674 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38175 603 41 0 39431 0
vsize: 157888
[startup+1190.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39676 0 0 0 118901 124 0 0 25 0 1 0 546714526 161677312 38175 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38175 603 41 0 39431 0
vsize: 157888
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9762
Raw data (stat): 9758 (minisat+) R 9757 27565 27564 0 -1 0 39676 0 0 0 119901 124 0 0 25 0 1 0 546714526 161677312 38175 4294967295 134512640 134672761 3221224544 3221223728 134615801 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38175 603 41 0 39431 0
vsize: 157888
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.15 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 9762
Raw data (stat): 9758 (minisat+) Z 9757 27565 27564 0 -1 12 39676 0 0 0 119901 131 0 0 25 0 1 0 546714526 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.15
CPU time (s): 1200.33
CPU user time (s): 1199.01
CPU system time (s): 1.3158
CPU usage (%): 100.015
Max. virtual memory (Kb): 158912
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####