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/miplib2003/normalized-mps-v2-20-10-vpm2.opb
MD5SUM	c1b4c3ad409db732d2b559e570b6f24c
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	138
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	819200
Number of bits of the biggest number in a constraint	20
Biggest sum of numbers in a constraint	4941871
Number of bits of the biggest sum of numbers	23
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.01
Number of variables	2754
Total number of constraints	612
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	168
Number of constraints which are nor clauses,nor cardinality constraints	444
Minimum length of a constraint	1
Maximum length of a constraint	84
Trace number 21484

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-04-22 00:03:15 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13141 boxname=wulflinc31 idbench=1011 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c1b4c3ad409db732d2b559e570b6f24c  /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-20-10-vpm2.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-20-10-vpm2.opb /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-20-10-vpm2.opb
IDLAUNCH: 13141
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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.153
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:        724552 kB
Buffers:         20212 kB
Cached:         265488 kB
SwapCached:        580 kB
Active:          59992 kB
Inactive:       227636 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        724300 kB
SwapTotal:     2097892 kB
SwapFree:      2096356 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5024 kB
Slab:            16756 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 00:23:17 (client local time) WITH STATUS 0 IN 1200.56 SECONDS
stats: 13141 7 1200.56 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 486 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
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]---> Adder-cost: 352   maxlim: 2411343   bits: 22/22
c ---[ 272]---> Adder-cost: 288   maxlim: 1694643   bits: 21/21
c ---[ 271]---> BDD-cost:    3
c ---[ 270]---> BDD-cost:    3
c ---[ 269]---> BDD-cost:    3
c ---[ 267]---> BDD-cost:    3
c ---[ 266]---> BDD-cost:    3
c ---[ 265]---> BDD-cost:    3
c ---[ 264]---> BDD-cost:    3
c ---[ 263]---> BDD-cost:    3
c ---[ 259]---> BDD-cost:   10
c ---[ 258]---> BDD-cost:    3
c ---[ 257]---> BDD-cost:    3
c ---[ 256]---> BDD-cost:    3
c ---[ 255]---> BDD-cost:   10
c ---[ 251]---> BDD-cost:   10
c ---[ 250]---> BDD-cost:    3
c ---[ 247]---> BDD-cost:    9
c ---[ 243]---> BDD-cost:   10
c ---[ 242]---> BDD-cost:    3
c ---[ 241]---> BDD-cost:    9
c ---[ 236]---> Sorter-cost: 2294     Base: 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[ 235]---> BDD-cost:    3
c ---[ 234]---> BDD-cost:    3
c ---[ 233]---> BDD-cost:    9
c ---[ 229]---> BDD-cost:   10
c ---[ 228]---> BDD-cost:    3
c ---[ 227]---> BDD-cost:    9
c ---[ 224]---> Adder-cost: 312   maxlim: 2587171   bits: 22/22
c ---[ 220]---> BDD-cost:    3
c ---[ 219]---> BDD-cost:    3
c ---[ 214]---> BDD-cost:   10
c ---[ 212]---> Adder-cost: 260   maxlim: 897571   bits: 20/20
c ---[ 211]---> BDD-cost:    3
c ---[ 206]---> BDD-cost:    3
c ---[ 205]---> BDD-cost:    3
c ---[ 198]---> BDD-cost:    3
c ---[ 197]---> BDD-cost:    3
c ---[ 193]---> BDD-cost:    3
c ---[ 192]---> BDD-cost:    3
c ---[ 191]---> BDD-cost:    3
c ---[ 185]---> BDD-cost:    3
c ---[ 184]---> BDD-cost:    3
c ---[ 183]---> BDD-cost:    3
c ---[ 179]---> BDD-cost:    3
c ---[ 178]---> BDD-cost:    3
c ---[ 175]---> BDD-cost:    3
c ---[ 171]---> BDD-cost:    3
c ---[ 170]---> BDD-cost:    3
c ---[ 169]---> BDD-cost:    3
c ---[ 168]---> BDD-cost:    3
c ---[ 167]---> BDD-cost:    3
c ---[ 166]---> BDD-cost:    9
c ---[ 164]---> Sorter-cost: 2815     Base: 2 2 2 5 5 2 2 2 2 2 2 2 2 3
c ---[ 163]---> BDD-cost:    9
c ---[ 162]---> BDD-cost:    9
c ---[ 161]---> BDD-cost:    9
c ---[ 160]---> BDD-cost:    3
c ---[ 159]---> BDD-cost:   10
c ---[ 158]---> BDD-cost:    9
c ---[ 157]---> BDD-cost:    9
c ---[ 156]---> BDD-cost:    9
c ---[ 155]---> BDD-cost:    9
c ---[ 154]---> BDD-cost:    3
c ---[ 152]---> Adder-cost: 352   maxlim: 2411343   bits: 22/22
c ---[ 150]---> Adder-cost: 350   maxlim: 1768271   bits: 22/21
c ---[ 149]---> BDD-cost:   10
c ---[ 148]---> BDD-cost:    8
c ---[ 147]---> BDD-cost:    8
c ---[ 146]---> BDD-cost:    8
c ---[ 145]---> BDD-cost:    8
c ---[ 144]---> BDD-cost:    3
c ---[ 143]---> BDD-cost:   10
c ---[ 142]---> BDD-cost:    8
c ---[ 141]---> BDD-cost:    8
c ---[ 140]---> BDD-cost:    8
c ---[ 137]---> BDD-cost:    8
c ---[ 135]---> BDD-cost:   10
c ---[ 134]---> BDD-cost:    3
c ---[ 133]---> BDD-cost:    9
c ---[ 132]---> BDD-cost:    9
c ---[ 131]---> BDD-cost:    9
c ---[ 129]---> BDD-cost:   10
c ---[ 128]---> BDD-cost:    3
c ---[ 125]---> BDD-cost:    9
c ---[ 124]---> BDD-cost:    9
c ---[ 123]---> BDD-cost:    9
c ---[ 121]---> BDD-cost:   10
c ---[ 120]---> BDD-cost:    3
c ---[ 119]---> BDD-cost:    9
c ---[ 118]---> BDD-cost:    9
c ---[ 117]---> BDD-cost:    9
c ---[ 114]---> Adder-cost: 274   maxlim: 1228100   bits: 21/21
c ---[ 113]---> BDD-cost:   10
c ---[ 112]---> BDD-cost:    3
c ---[ 111]---> BDD-cost:    8
c ---[ 110]---> BDD-cost:    8
c ---[ 109]---> BDD-cost:    8
c ---[ 107]---> Adder-cost: 312   maxlim: 1957187   bits: 22/21
c ---[ 105]---> Adder-cost: 312   maxlim: 1854787   bits: 22/21
c ---[ 103]---> Adder-cost: 390   maxlim: 2279471   bits: 22/22
c ---[ 101]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[  99]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[  97]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[  95]---> Adder-cost: 330   maxlim: 1694543   bits: 21/21
c ---[  93]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[  91]---> Sorter-cost: 3240     Base: 2 2 2 2 5 5 2 2 2 2 2 2 5
c ---[  89]---> Adder-cost: 440   maxlim: 3713071   bits: 23/22
c ---[  87]---> Adder-cost: 368   maxlim: 999471   bits: 21/20
c ---[  85]---> Adder-cost: 368   maxlim: 999471   bits: 21/20
c ---[  83]---> Adder-cost: 368   maxlim: 999471   bits: 21/20
c ---[  81]---> Sorter-cost: 3227     Base: 2 2 2 5 5 2 2 2 2 2 2 2 2 3
c ---[  73]---> Adder-cost: 330   maxlim: 1694543   bits: 21/21
c ---[  69]---> Sorter-cost: 3277     Base: 2 2 2 5 5 2 2 2 2 2 2 3 2 2 2
c ---[  66]---> BDD-cost:  230
c ---[  65]---> BDD-cost:  661
c ---[  64]---> BDD-cost:  660
c ---[  63]---> Sorter-cost: 1990     Base: 5 5 5 2 2 2 2 2 2 2 2 2
c ---[  62]---> Sorter-cost: 2375     Base: 5 5 5 2 2 2 2 2 2 2 2 2
c ---[  61]---> Sorter-cost: 2299     Base: 5 5 5 2 2 2 2 2 2 2 2 2
c ---[  60]---> Sorter-cost:  417     Base: 2 2 2 2 2 2 2 2 5 2
c ---[  58]---> Adder-cost: 352   maxlim: 2104143   bits: 22/22
c ---[  57]---> Sorter-cost: 1129     Base: 5 2 2 2 2 2 2 2 2 2
c ---[  56]---> Sorter-cost: 1147     Base: 5 2 2 2 2 2 2 2 2 2
c ---[  55]---> Sorter-cost: 1626     Base: 5 2 2 2 2 2 2 2 2 2
c ---[  54]---> Sorter-cost: 1906     Base: 5 2 2 2 2 2 2 2 2 2
c ---[  53]---> Sorter-cost: 1910     Base: 5 2 2 2 2 2 2 2 2 2
c ---[  52]---> Sorter-cost:  449     Base: 2 2 2 2 2 2 2 2 2 5
c ---[  51]---> Sorter-cost: 1242     Base: 2 2 2 2 2 5 2 2 2 2
c ---[  50]---> Sorter-cost: 1199     Base: 2 2 2 2 2 2 2 2 2 5
c ---[  49]---> Sorter-cost: 1719     Base: 5 2 2 2 2 2 2 2 2 2
c ---[  48]---> Sorter-cost: 2067     Base: 5 2 2 2 2 2 2 2 2 2
c ---[  46]---> Sorter-cost: 2487     Base: 2 2 2 2 2 2 2 2 5 5 2 2 2 2
c ---[  45]---> Sorter-cost: 2045     Base: 5 2 2 2 2 2 2 2 2 2
c ---[  44]---> Sorter-cost:  223     Base: 2 2 2 2 2 2 2 2 2
c ---[  43]---> Sorter-cost:  590     Base: 2 2 2 2 2 2 2 2
c ---[  42]---> Sorter-cost:  538     Base: 2 2 2 2 2 2 2 2 2
c ---[  41]---> Sorter-cost: 1025     Base: 2 2 2 2 2 2 2 2
c ---[  40]---> Sorter-cost: 1211     Base: 2 2 2 2 2 2 2 2 2
c ---[  39]---> Sorter-cost: 1390     Base: 2 2 2 2 2 2 2 2
c ---[  38]---> BDD-cost:    3
c ---[  37]---> BDD-cost:    3
c ---[  36]---> BDD-cost:    3
c ---[  34]---> Adder-cost: 304   maxlim: 2309043   bits: 22/22
c ---[  33]---> BDD-cost:    3
c ---[  32]---> BDD-cost:    3
c ---[  31]---> BDD-cost:    3
c ---[  30]---> BDD-cost:    3
c ---[  29]---> BDD-cost:    3
c ---[  28]---> BDD-cost:    3
c ---[  27]---> BDD-cost:   10
c ---[  26]---> BDD-cost:   10
c ---[  25]---> BDD-cost:    3
c ---[  24]---> BDD-cost:    3
c ---[  22]---> Adder-cost: 304   maxlim: 2104243   bits: 22/22
c ---[  21]---> BDD-cost:    3
c ---[  20]---> BDD-cost:    3
c ---[  19]---> BDD-cost:   10
c ---[  18]---> BDD-cost:   10
c ---[  17]---> BDD-cost:    3
c ---[  16]---> BDD-cost:    3
c ---[  15]---> BDD-cost:    3
c ---[  14]---> BDD-cost:    3
c ---[  13]---> BDD-cost:   10
c ---[  12]---> BDD-cost:   10
c ---[  10]---> Adder-cost: 304   maxlim: 2104243   bits: 22/22
c ---[   9]---> BDD-cost:    3
c ---[   7]---> BDD-cost:   10
c ---[   6]---> BDD-cost:    3
c ---[   5]---> BDD-cost:    3
c ---[   4]---> BDD-cost:    3
c ---[   3]---> BDD-cost:   10
c ---[   1]---> BDD-cost:    3
c ---[   0]---> BDD-cost:    3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  174818   481419 |   52445       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/49674          
c   -- var.elim.:  2000/49674          
c   -- var.elim.:  3000/49674          
c   -- var.elim.:  4000/49674          
c   -- var.elim.:  5000/49674          
c   -- var.elim.:  6000/49674          
c   -- var.elim.:  7000/49674          
c   -- var.elim.:  8000/49674          
c   -- var.elim.:  9000/49674          
c   -- var.elim.:  10000/49674          
c   -- var.elim.:  11000/49674          
c   -- var.elim.:  12000/49674          
c   -- var.elim.:  13000/49674          
c   -- var.elim.:  14000/49674          
c   -- var.elim.:  15000/49674          
c   -- var.elim.:  16000/49674          
c   -- var.elim.:  17000/49674          
c   -- var.elim.:  18000/49674          
c   -- var.elim.:  19000/49674          
c   -- var.elim.:  20000/49674          
c   -- var.elim.:  21000/49674          
c   -- var.elim.:  22000/49674          
c   -- var.elim.:  23000/49674          
c   -- var.elim.:  24000/49674          
c   -- var.elim.:  25000/49674          
c   -- var.elim.:  26000/49674          
c   -- var.elim.:  27000/49674          
c   -- var.elim.:  28000/49674          
c   -- var.elim.:  29000/49674          
c   -- var.elim.:  30000/49674          
c   -- var.elim.:  31000/49674          
c   -- var.elim.:  32000/49674          
c   -- var.elim.:  33000/49674          
c   -- var.elim.:  34000/49674          
c   -- var.elim.:  35000/49674          
c   -- var.elim.:  3#### 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.92 0.98 0.91 2/54 4950
Raw data (stat): 4950 (runsolver) R 4949 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 549236269 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.93 0.98 0.91 2/54 4950
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 9709 0 0 0 973 26 0 0 25 0 1 0 549236269 38555648 8266 4294967295 134512640 134672761 3221224544 3221223668 134566122 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9413 8266 603 41 0 9372 0
vsize: 37652
[startup+20.0009 s]
Raw data (loadavg): 0.94 0.98 0.91 2/54 4950
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 10154 0 0 0 1972 27 0 0 25 0 1 0 549236269 40497152 8711 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9887 8711 603 41 0 9846 0
vsize: 39548
[startup+30.0018 s]
Raw data (loadavg): 0.95 0.98 0.91 2/54 4950
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 10679 0 0 0 2970 29 0 0 25 0 1 0 549236269 42610688 9236 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10403 9236 603 41 0 10362 0
vsize: 41612
[startup+40.0032 s]
Raw data (loadavg): 0.96 0.98 0.91 2/54 4950
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 11466 0 0 0 3967 31 0 0 25 0 1 0 549236269 46051328 10023 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11243 10023 603 41 0 11202 0
vsize: 44972
[startup+50.0036 s]
Raw data (loadavg): 0.96 0.98 0.91 2/54 4950
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 11991 0 0 0 4966 33 0 0 25 0 1 0 549236269 48046080 10548 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11730 10548 603 41 0 11689 0
vsize: 46920
[startup+60.0038 s]
Raw data (loadavg): 0.97 0.98 0.91 3/54 4950
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 12364 0 0 0 5964 35 0 0 25 0 1 0 549236269 49631232 10921 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12117 10921 603 41 0 12076 0
vsize: 48468
[startup+70.0046 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 4950
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 12716 0 0 0 6963 36 0 0 25 0 1 0 549236269 50958336 11273 4294967295 134512640 134672761 3221224544 3221223744 134610614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12441 11273 603 41 0 12400 0
vsize: 49764
[startup+80.0053 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 4950
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 13309 0 0 0 7962 37 0 0 25 0 1 0 549236269 53465088 11866 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13053 11866 603 41 0 13012 0
vsize: 52212
[startup+90.0066 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 4950
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 13739 0 0 0 8961 39 0 0 25 0 1 0 549236269 55463936 12296 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13541 12296 603 41 0 13500 0
vsize: 54164
[startup+100.01 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 4950
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 14318 0 0 0 9959 41 0 0 25 0 1 0 549236269 57704448 12875 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14088 12875 603 41 0 14047 0
vsize: 56352
[startup+110.017 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 4950
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 14658 0 0 0 10959 42 0 0 25 0 1 0 549236269 59162624 13215 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14444 13215 603 41 0 14403 0
vsize: 57776
[startup+120.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 14981 0 0 0 11958 44 0 0 25 0 1 0 549236269 60493824 13538 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14769 13538 603 41 0 14728 0
vsize: 59076
[startup+130.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 15433 0 0 0 12956 45 0 0 25 0 1 0 549236269 62214144 13990 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15189 13990 603 41 0 15148 0
vsize: 60756
[startup+140.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 15858 0 0 0 13955 47 0 0 25 0 1 0 549236269 63934464 14415 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15609 14415 603 41 0 15568 0
vsize: 62436
[startup+150.045 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 16211 0 0 0 14957 48 0 0 25 0 1 0 549236269 65392640 14768 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15965 14768 603 41 0 15924 0
vsize: 63860
[startup+160.045 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 16549 0 0 0 15955 50 0 0 25 0 1 0 549236269 66842624 15106 4294967295 134512640 134672761 3221224544 3221223728 134615838 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16319 15106 603 41 0 16278 0
vsize: 65276
[startup+170.051 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 16917 0 0 0 16955 51 0 0 25 0 1 0 549236269 68296704 15474 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16674 15474 603 41 0 16633 0
vsize: 66696
[startup+180.067 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 17250 0 0 0 17955 52 0 0 25 0 1 0 549236269 69627904 15807 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16999 15807 603 41 0 16958 0
vsize: 67996
[startup+190.08 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 17614 0 0 0 18955 54 0 0 25 0 1 0 549236269 71086080 16171 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17355 16171 603 41 0 17314 0
vsize: 69420
[startup+200.081 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 17918 0 0 0 19954 55 0 0 25 0 1 0 549236269 72429568 16475 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17683 16475 603 41 0 17642 0
vsize: 70732
[startup+210.081 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 18405 0 0 0 20953 56 0 0 25 0 1 0 549236269 74285056 16962 4294967295 134512640 134672761 3221224544 3221223728 134615761 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18136 16962 603 41 0 18095 0
vsize: 72544
[startup+220.082 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 18864 0 0 0 21951 58 0 0 25 0 1 0 549236269 76267520 17421 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18620 17421 603 41 0 18579 0
vsize: 74480
[startup+230.083 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 19128 0 0 0 22951 59 0 0 25 0 1 0 549236269 77844480 17685 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19005 17685 603 41 0 18964 0
vsize: 76020
[startup+240.186 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 19375 0 0 0 23960 60 0 0 25 0 1 0 549236269 78790656 17932 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19236 17932 603 41 0 19195 0
vsize: 76944
[startup+250.187 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 19639 0 0 0 24960 61 0 0 25 0 1 0 549236269 79843328 18196 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19493 18196 603 41 0 19452 0
vsize: 77972
[startup+260.187 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 19943 0 0 0 25959 62 0 0 25 0 1 0 549236269 81182720 18500 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19820 18500 603 41 0 19779 0
vsize: 79280
[startup+270.188 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 20196 0 0 0 26958 62 0 0 25 0 1 0 549236269 82116608 18753 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20048 18753 603 41 0 20007 0
vsize: 80192
[startup+280.189 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 20409 0 0 0 27958 63 0 0 25 0 1 0 549236269 83050496 18966 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20276 18966 603 41 0 20235 0
vsize: 81104
[startup+290.191 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 20734 0 0 0 28957 65 0 0 25 0 1 0 549236269 84242432 19291 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20567 19291 603 41 0 20526 0
vsize: 82268
[startup+300.192 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 20998 0 0 0 29956 66 0 0 25 0 1 0 549236269 85307392 19555 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20827 19555 603 41 0 20786 0
vsize: 83308
[startup+310.192 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 21195 0 0 0 30955 67 0 0 25 0 1 0 549236269 86097920 19752 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21020 19752 603 41 0 20979 0
vsize: 84080
[startup+320.193 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 21411 0 0 0 31954 68 0 0 25 0 1 0 549236269 87019520 19968 4294967295 134512640 134672761 3221224544 3221223728 134615622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21245 19968 603 41 0 21204 0
vsize: 84980
[startup+330.193 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 21588 0 0 0 32954 68 0 0 25 0 1 0 549236269 87683072 20145 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21407 20145 603 41 0 21366 0
vsize: 85628
[startup+340.193 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 21774 0 0 0 33953 69 0 0 25 0 1 0 549236269 88477696 20331 4294967295 134512640 134672761 3221224544 3221223728 134615673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21601 20331 603 41 0 21560 0
vsize: 86404
[startup+350.194 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 21978 0 0 0 34952 70 0 0 25 0 1 0 549236269 89313280 20535 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21805 20535 603 41 0 21764 0
vsize: 87220
[startup+360.195 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 22176 0 0 0 35952 71 0 0 25 0 1 0 549236269 90103808 20733 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21998 20733 603 41 0 21957 0
vsize: 87992
[startup+370.196 s]
Raw data (loadavg): 0.99 0.98 0.91 3/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 22367 0 0 0 36952 71 0 0 25 0 1 0 549236269 90914816 20924 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22196 20924 603 41 0 22155 0
vsize: 88784
[startup+380.196 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 22581 0 0 0 37952 72 0 0 25 0 1 0 549236269 91844608 21138 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22423 21138 603 41 0 22382 0
vsize: 89692
[startup+390.197 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 22866 0 0 0 38951 73 0 0 25 0 1 0 549236269 93044736 21423 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22716 21423 603 41 0 22675 0
vsize: 90864
[startup+400.198 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 23208 0 0 0 39950 74 0 0 25 0 1 0 549236269 94396416 21765 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23046 21765 603 41 0 23005 0
vsize: 92184
[startup+410.207 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 23370 0 0 0 40950 75 0 0 25 0 1 0 549236269 95084544 21927 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23214 21927 603 41 0 23173 0
vsize: 92856
[startup+420.207 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 23541 0 0 0 41949 76 0 0 25 0 1 0 549236269 95739904 22098 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23374 22098 603 41 0 23333 0
vsize: 93496
[startup+430.209 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 23753 0 0 0 42948 77 0 0 25 0 1 0 549236269 96542720 22310 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23570 22310 603 41 0 23529 0
vsize: 94280
[startup+440.21 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 24004 0 0 0 43947 78 0 0 25 0 1 0 549236269 97611776 22561 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23831 22561 603 41 0 23790 0
vsize: 95324
[startup+450.215 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 24264 0 0 0 44947 79 0 0 25 0 1 0 549236269 98680832 22821 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24092 22821 603 41 0 24051 0
vsize: 96368
[startup+460.222 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 24664 0 0 0 45947 80 0 0 25 0 1 0 549236269 100270080 23221 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24480 23221 603 41 0 24439 0
vsize: 97920
[startup+470.236 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 25024 0 0 0 46947 81 0 0 25 0 1 0 549236269 101720064 23581 4294967295 134512640 134672761 3221224544 3221223688 134616275 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24834 23581 603 41 0 24793 0
vsize: 99336
[startup+480.236 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 25249 0 0 0 47946 83 0 0 25 0 1 0 549236269 102707200 23806 4294967295 134512640 134672761 3221224544 3221223728 134615801 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25075 23806 603 41 0 25034 0
vsize: 100300
[startup+490.236 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 25513 0 0 0 48945 84 0 0 25 0 1 0 549236269 103776256 24070 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25336 24070 603 41 0 25295 0
vsize: 101344
[startup+500.237 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 25656 0 0 0 49945 85 0 0 25 0 1 0 549236269 104312832 24213 4294967295 134512640 134672761 3221224544 3221223680 134614516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25467 24213 603 41 0 25426 0
vsize: 101868
[startup+510.237 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 25822 0 0 0 50944 85 0 0 25 0 1 0 549236269 104984576 24379 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25631 24379 603 41 0 25590 0
vsize: 102524
[startup+520.237 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 26200 0 0 0 51943 87 0 0 25 0 1 0 549236269 106565632 24757 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26017 24757 603 41 0 25976 0
vsize: 104068
[startup+530.243 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 26553 0 0 0 52941 89 0 0 25 0 1 0 549236269 107905024 25110 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26344 25110 603 41 0 26303 0
vsize: 105376
[startup+540.243 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 26814 0 0 0 53940 90 0 0 25 0 1 0 549236269 108965888 25371 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26603 25371 603 41 0 26562 0
vsize: 106412
[startup+550.243 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 27072 0 0 0 54940 91 0 0 25 0 1 0 549236269 110022656 25629 4294967295 134512640 134672761 3221224544 3221223728 134615638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26861 25629 603 41 0 26820 0
vsize: 107444
[startup+560.243 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 27349 0 0 0 55939 92 0 0 25 0 1 0 549236269 111226880 25906 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27155 25906 603 41 0 27114 0
vsize: 108620
[startup+570.243 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 27630 0 0 0 56938 93 0 0 25 0 1 0 549236269 112291840 26187 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27415 26187 603 41 0 27374 0
vsize: 109660
[startup+580.243 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 27903 0 0 0 57937 94 0 0 25 0 1 0 549236269 113504256 26460 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27711 26460 603 41 0 27670 0
vsize: 110844
[startup+590.244 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 28175 0 0 0 58937 95 0 0 25 0 1 0 549236269 114556928 26732 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27968 26732 603 41 0 27927 0
vsize: 111872
[startup+600.245 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 28357 0 0 0 59937 95 0 0 25 0 1 0 549236269 115363840 26914 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28165 26914 603 41 0 28124 0
vsize: 112660
[startup+610.246 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 28545 0 0 0 60936 95 0 0 25 0 1 0 549236269 117121024 27102 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28594 27102 603 41 0 28553 0
vsize: 114376
[startup+620.247 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 28835 0 0 0 61934 97 0 0 25 0 1 0 549236269 118304768 27392 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28883 27392 603 41 0 28842 0
vsize: 115532
[startup+630.251 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 29136 0 0 0 62933 98 0 0 25 0 1 0 549236269 119504896 27693 4294967295 134512640 134672761 3221224544 3221223536 134565098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29176 27693 603 41 0 29135 0
vsize: 116704
[startup+640.252 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 29382 0 0 0 63933 98 0 0 25 0 1 0 549236269 120557568 27939 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29433 27939 603 41 0 29392 0
vsize: 117732
[startup+650.253 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 29580 0 0 0 64932 100 0 0 25 0 1 0 549236269 121368576 28137 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29631 28137 603 41 0 29590 0
vsize: 118524
[startup+660.254 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 29772 0 0 0 65931 101 0 0 25 0 1 0 549236269 122159104 28329 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29824 28329 603 41 0 29783 0
vsize: 119296
[startup+670.255 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 29990 0 0 0 66931 102 0 0 25 0 1 0 549236269 123092992 28547 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30052 28547 603 41 0 30011 0
vsize: 120208
[startup+680.254 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 30167 0 0 0 67930 102 0 0 25 0 1 0 549236269 123904000 28724 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30250 28724 603 41 0 30209 0
vsize: 121000
[startup+690.255 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 30265 0 0 0 68931 102 0 0 25 0 1 0 549236269 124178432 28822 4294967295 134512640 134672761 3221224544 3221223728 134615794 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30317 28822 603 41 0 30276 0
vsize: 121268
[startup+700.256 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 30392 0 0 0 69930 103 0 0 25 0 1 0 549236269 124719104 28949 4294967295 134512640 134672761 3221224544 3221223728 134615785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30449 28949 603 41 0 30408 0
vsize: 121796
[startup+710.256 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 30540 0 0 0 70930 103 0 0 25 0 1 0 549236269 125386752 29097 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30612 29097 603 41 0 30571 0
vsize: 122448
[startup+720.257 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 30680 0 0 0 71930 103 0 0 25 0 1 0 549236269 125919232 29237 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30742 29237 603 41 0 30701 0
vsize: 122968
[startup+730.258 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 30940 0 0 0 72929 104 0 0 25 0 1 0 549236269 126967808 29497 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30998 29497 603 41 0 30957 0
vsize: 123992
[startup+740.258 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 31099 0 0 0 73929 105 0 0 25 0 1 0 549236269 127627264 29656 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31159 29656 603 41 0 31118 0
vsize: 124636
[startup+750.258 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 31239 0 0 0 74929 105 0 0 25 0 1 0 549236269 128163840 29796 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31290 29796 603 41 0 31249 0
vsize: 125160
[startup+760.262 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 31354 0 0 0 75929 105 0 0 25 0 1 0 549236269 128589824 29911 4294967295 134512640 134672761 3221224544 3221223688 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31394 29911 603 41 0 31353 0
vsize: 125576
[startup+770.273 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 31524 0 0 0 76930 106 0 0 25 0 1 0 549236269 129302528 30081 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31568 30081 603 41 0 31527 0
vsize: 126272
[startup+780.274 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 31726 0 0 0 77929 107 0 0 25 0 1 0 549236269 130224128 30283 4294967295 134512640 134672761 3221224544 3221223584 134614256 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31793 30283 603 41 0 31752 0
vsize: 127172
[startup+790.297 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 31944 0 0 0 78930 108 0 0 25 0 1 0 549236269 131022848 30501 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31988 30501 603 41 0 31947 0
vsize: 127952
[startup+800.297 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 32042 0 0 0 79930 109 0 0 25 0 1 0 549236269 131424256 30599 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32086 30599 603 41 0 32045 0
vsize: 128344
[startup+810.303 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 32187 0 0 0 80930 109 0 0 25 0 1 0 549236269 132087808 30744 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32248 30744 603 41 0 32207 0
vsize: 128992
[startup+820.304 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 32332 0 0 0 81930 109 0 0 25 0 1 0 549236269 132616192 30889 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32377 30889 603 41 0 32336 0
vsize: 129508
[startup+830.304 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 32456 0 0 0 82930 110 0 0 25 0 1 0 549236269 133152768 31013 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32508 31013 603 41 0 32467 0
vsize: 130032
[startup+840.305 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 32591 0 0 0 83929 111 0 0 25 0 1 0 549236269 133808128 31148 4294967295 134512640 134672761 3221224544 3221223688 134616347 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32668 31148 603 41 0 32627 0
vsize: 130672
[startup+850.305 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 32728 0 0 0 84929 111 0 0 25 0 1 0 549236269 134340608 31285 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32798 31285 603 41 0 32757 0
vsize: 131192
[startup+860.313 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 32886 0 0 0 85930 111 0 0 25 0 1 0 549236269 135008256 31443 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32961 31443 603 41 0 32920 0
vsize: 131844
[startup+870.314 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 33089 0 0 0 86929 112 0 0 25 0 1 0 549236269 135798784 31646 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33154 31646 603 41 0 33113 0
vsize: 132616
[startup+880.314 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 33241 0 0 0 87929 113 0 0 25 0 1 0 549236269 136323072 31798 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33282 31798 603 41 0 33241 0
vsize: 133128
[startup+890.314 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 33403 0 0 0 88928 113 0 0 25 0 1 0 549236269 136982528 31960 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33443 31960 603 41 0 33402 0
vsize: 133772
[startup+900.315 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 33591 0 0 0 89928 114 0 0 25 0 1 0 549236269 137781248 32148 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33638 32148 603 41 0 33597 0
vsize: 134552
[startup+910.315 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 33749 0 0 0 90928 114 0 0 25 0 1 0 549236269 138440704 32306 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33799 32306 603 41 0 33758 0
vsize: 135196
[startup+920.315 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 33886 0 0 0 91928 115 0 0 25 0 1 0 549236269 139108352 32443 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33962 32443 603 41 0 33921 0
vsize: 135848
[startup+930.316 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 34042 0 0 0 92927 115 0 0 25 0 1 0 549236269 139776000 32599 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34125 32599 603 41 0 34084 0
vsize: 136500
[startup+940.315 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 34335 0 0 0 93927 116 0 0 25 0 1 0 549236269 140963840 32892 4294967295 134512640 134672761 3221224544 3221223680 134614724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34415 32892 603 41 0 34374 0
vsize: 137660
[startup+950.316 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 34488 0 0 0 94926 116 0 0 25 0 1 0 549236269 141500416 33045 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34546 33045 603 41 0 34505 0
vsize: 138184
[startup+960.317 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 34581 0 0 0 95926 117 0 0 25 0 1 0 549236269 141901824 33138 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34644 33138 603 41 0 34603 0
vsize: 138576
[startup+970.317 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 34683 0 0 0 96926 117 0 0 25 0 1 0 549236269 142303232 33240 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34742 33240 603 41 0 34701 0
vsize: 138968
[startup+980.317 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 35355 0 0 0 97924 119 0 0 25 0 1 0 549236269 144515072 33581 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35282 33581 603 41 0 35241 0
vsize: 141128
[startup+990.317 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 35355 0 0 0 98925 119 0 0 25 0 1 0 549236269 144515072 33581 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35282 33581 603 41 0 35241 0
vsize: 141128
[startup+1000.32 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 35355 0 0 0 99925 119 0 0 25 0 1 0 549236269 144515072 33581 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35282 33581 603 41 0 35241 0
vsize: 141128
[startup+1010.32 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 35355 0 0 0 100925 119 0 0 25 0 1 0 549236269 144515072 33581 4294967295 134512640 134672761 3221224544 3221223696 134614555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35282 33581 603 41 0 35241 0
vsize: 141128
[startup+1020.32 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 35355 0 0 0 101925 119 0 0 25 0 1 0 549236269 144515072 33581 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35282 33581 603 41 0 35241 0
vsize: 141128
[startup+1030.32 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 35355 0 0 0 102925 119 0 0 25 0 1 0 549236269 144515072 33581 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35282 33581 603 41 0 35241 0
vsize: 141128
[startup+1040.32 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 35355 0 0 0 103926 119 0 0 25 0 1 0 549236269 144515072 33581 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35282 33581 603 41 0 35241 0
vsize: 141128
[startup+1050.32 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 35355 0 0 0 104926 119 0 0 25 0 1 0 549236269 144515072 33581 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35282 33581 603 41 0 35241 0
vsize: 141128
[startup+1060.32 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 35355 0 0 0 105926 119 0 0 25 0 1 0 549236269 144515072 33581 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35282 33581 603 41 0 35241 0
vsize: 141128
[startup+1070.32 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 35355 0 0 0 106926 119 0 0 25 0 1 0 549236269 144515072 33581 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35282 33581 603 41 0 35241 0
vsize: 141128
[startup+1080.32 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 35355 0 0 0 107926 119 0 0 25 0 1 0 549236269 144515072 33581 4294967295 134512640 134672761 3221224544 3221223728 134615830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35282 33581 603 41 0 35241 0
vsize: 141128
[startup+1090.32 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 35355 0 0 0 108927 119 0 0 25 0 1 0 549236269 144515072 33581 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35282 33581 603 41 0 35241 0
vsize: 141128
[startup+1100.32 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 35355 0 0 0 109927 119 0 0 25 0 1 0 549236269 144515072 33581 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35282 33581 603 41 0 35241 0
vsize: 141128
[startup+1110.32 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 35355 0 0 0 110927 119 0 0 25 0 1 0 549236269 144515072 33581 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35282 33581 603 41 0 35241 0
vsize: 141128
[startup+1120.32 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 35355 0 0 0 111927 119 0 0 25 0 1 0 549236269 144515072 33581 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35282 33581 603 41 0 35241 0
vsize: 141128
[startup+1130.33 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 35355 0 0 0 112928 119 0 0 25 0 1 0 549236269 144515072 33581 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35282 33581 603 41 0 35241 0
vsize: 141128
[startup+1140.33 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 35355 0 0 0 113928 119 0 0 25 0 1 0 549236269 144515072 33581 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35282 33581 603 41 0 35241 0
vsize: 141128
[startup+1150.33 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 35355 0 0 0 114928 119 0 0 25 0 1 0 549236269 144515072 33581 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35282 33581 603 41 0 35241 0
vsize: 141128
[startup+1160.33 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 35355 0 0 0 115929 119 0 0 25 0 1 0 549236269 144515072 33581 4294967295 134512640 134672761 3221224544 3221223728 134615752 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35282 33581 603 41 0 35241 0
vsize: 141128
[startup+1170.33 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 35355 0 0 0 116929 119 0 0 25 0 1 0 549236269 144515072 33581 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35282 33581 603 41 0 35241 0
vsize: 141128
[startup+1180.33 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 35355 0 0 0 117929 119 0 0 25 0 1 0 549236269 144515072 33581 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35282 33581 603 41 0 35241 0
vsize: 141128
[startup+1190.33 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 35355 0 0 0 118929 119 0 0 25 0 1 0 549236269 144515072 33581 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35282 33581 603 41 0 35241 0
vsize: 141128
[startup+1200.33 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 4952
Raw data (stat): 4950 (minisat+) R 4949 23176 23175 0 -1 0 35355 0 0 0 119929 119 0 0 25 0 1 0 549236269 144515072 33581 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35282 33581 603 41 0 35241 0
vsize: 141128
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.4 s]
Raw data (loadavg): 0.99 0.98 0.91 1/54 4952
Raw data (stat): 4950 (minisat+) Z 4949 23176 23175 0 -1 12 35355 0 0 0 119929 126 0 0 25 0 1 0 549236269 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.4
CPU time (s): 1200.56
CPU user time (s): 1199.3
CPU system time (s): 1.26081
CPU usage (%): 100.013
Max. virtual memory (Kb): 141128
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####