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/web/www.ps.uni-sb.de/~walser/benchmarks/course-ass/normalized-ws97-5.opb
MD5SUM	6049145b9f1adfd7114adf044503d587
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2642
Optimality of the best value was proved	NO
Number of terms in the objective function	748
Biggest coefficient in the objective function	240
Number of bits for the biggest coefficient in the objective function	8
Sum of the numbers in the objective function	33855
Number of bits of the sum of numbers in the objective function	16
Biggest number in a constraint	240
Number of bits of the biggest number in a constraint	8
Biggest sum of numbers in a constraint	33855
Number of bits of the biggest sum of numbers	16
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02984
Number of variables	907
Total number of constraints	1309
Number of constraints which are clauses	126
Number of constraints which are cardinality constraints (but not clauses)	1183
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	134
Trace number 5652

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-04-14 01:17:59 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4118 boxname=wulflinc31 idbench=358 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6049145b9f1adfd7114adf044503d587  /oldhome/oroussel/tmp/wulflinc31/normalized-ws97-5.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc31/normalized-ws97-5.opb /oldhome/oroussel/tmp/wulflinc31/normalized-ws97-5.opb
IDLAUNCH: 4118
/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:        906120 kB
Buffers:         35920 kB
Cached:          54060 kB
SwapCached:        392 kB
Active:          51636 kB
Inactive:        41496 kB
HighTotal:      131008 kB
HighFree:        73276 kB
LowTotal:       903652 kB
LowFree:        832844 kB
SwapTotal:     2097892 kB
SwapFree:      2097452 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6832 kB
Slab:            29772 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 01:38:01 (client local time) WITH STATUS 10 IN 1200.22 SECONDS
stats: 4118 7 1200.22 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 661 PB-constraints to clauses...
c   -- Unit propagations: ppp
c   -- Detecting intervals from adjacent constraints: ##################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): .............................................................................................................................
c ---[ 660]---> Adder-cost: 238   maxlim: 90   bits: 7/7
c ---[ 659]---> Adder-cost: 238   maxlim: 90   bits: 7/7
c ---[ 658]---> Adder-cost: 238   maxlim: 90   bits: 7/7
c ---[ 657]---> Adder-cost: 238   maxlim: 91   bits: 7/7
c ---[ 656]---> Adder-cost: 260   maxlim: 85   bits: 8/7
c ---[ 655]---> Adder-cost: 260   maxlim: 84   bits: 8/7
c ---[ 654]---> Adder-cost: 260   maxlim: 84   bits: 8/7
c ---[ 653]---> Adder-cost: 19   maxlim: 23   bits: 6/5
c ---[ 652]---> Adder-cost: 19   maxlim: 23   bits: 6/5
c ---[ 651]---> Adder-cost: 19   maxlim: 23   bits: 6/5
c ---[ 650]---> Adder-cost: 19   maxlim: 22   bits: 6/5
c ---[ 649]---> Adder-cost: 28   maxlim: 33   bits: 7/6
c ---[ 648]---> Adder-cost: 28   maxlim: 34   bits: 7/6
c ---[ 647]---> Adder-cost: 28   maxlim: 34   bits: 7/6
c ---[ 645]---> BDD-cost:    5
c ---[ 643]---> BDD-cost:    3
c ---[ 641]---> BDD-cost:    5
c ---[ 639]---> BDD-cost:    3
c ---[ 637]---> BDD-cost:    5
c ---[ 635]---> BDD-cost:    3
c ---[ 633]---> BDD-cost:    5
c ---[ 631]---> BDD-cost:    3
c ---[ 629]---> BDD-cost:    5
c ---[ 627]---> BDD-cost:    3
c ---[ 625]---> BDD-cost:    5
c ---[ 623]---> BDD-cost:    3
c ---[ 621]---> BDD-cost:    3
c ---[ 619]---> BDD-cost:    5
c ---[ 617]---> BDD-cost:    3
c ---[ 615]---> BDD-cost:    5
c ---[ 613]---> BDD-cost:    3
c ---[ 611]---> BDD-cost:    5
c ---[ 609]---> BDD-cost:    3
c ---[ 607]---> BDD-cost:    3
c ---[ 605]---> BDD-cost:    5
c ---[ 603]---> BDD-cost:    3
c ---[ 601]---> BDD-cost:    5
c ---[ 599]---> BDD-cost:    3
c ---[ 597]---> BDD-cost:    5
c ---[ 595]---> BDD-cost:    3
c ---[ 593]---> BDD-cost:    5
c ---[ 591]---> BDD-cost:    3
c ---[ 589]---> BDD-cost:    5
c ---[ 587]---> BDD-cost:    3
c ---[ 585]---> BDD-cost:    5
c ---[ 583]---> BDD-cost:    3
c ---[ 581]---> BDD-cost:    5
c ---[ 579]---> BDD-cost:    3
c ---[ 577]---> BDD-cost:    5
c ---[ 575]---> BDD-cost:    3
c ---[ 573]---> BDD-cost:    5
c ---[ 571]---> BDD-cost:    3
c ---[ 569]---> BDD-cost:    5
c ---[ 567]---> BDD-cost:    3
c ---[ 565]---> BDD-cost:    5
c ---[ 563]---> BDD-cost:    3
c ---[ 561]---> BDD-cost:    5
c ---[ 559]---> BDD-cost:    3
c ---[ 557]---> BDD-cost:    5
c ---[ 555]---> BDD-cost:    3
c ---[ 553]---> BDD-cost:    5
c ---[ 551]---> BDD-cost:    3
c ---[ 549]---> BDD-cost:    5
c ---[ 547]---> BDD-cost:    3
c ---[ 545]---> BDD-cost:    5
c ---[ 543]---> BDD-cost:    3
c ---[ 541]---> BDD-cost:    5
c ---[ 539]---> BDD-cost:    3
c ---[ 537]---> BDD-cost:    5
c ---[ 535]---> BDD-cost:    3
c ---[ 533]---> BDD-cost:    5
c ---[ 531]---> BDD-cost:    3
c ---[ 529]---> BDD-cost:    5
c ---[ 527]---> BDD-cost:    3
c ---[ 525]---> BDD-cost:    5
c ---[ 523]---> BDD-cost:    3
c ---[ 521]---> BDD-cost:    5
c ---[ 519]---> BDD-cost:    3
c ---[ 517]---> BDD-cost:    5
c ---[ 515]---> BDD-cost:    3
c ---[ 513]---> BDD-cost:    5
c ---[ 511]---> BDD-cost:    3
c ---[ 509]---> BDD-cost:    5
c ---[ 507]---> BDD-cost:    3
c ---[ 505]---> BDD-cost:    5
c ---[ 503]---> BDD-cost:    3
c ---[ 501]---> BDD-cost:    5
c ---[ 499]---> BDD-cost:    3
c ---[ 497]---> BDD-cost:    5
c ---[ 495]---> BDD-cost:    3
c ---[ 493]---> BDD-cost:    5
c ---[ 491]---> BDD-cost:    3
c ---[ 489]---> BDD-cost:    5
c ---[ 487]---> BDD-cost:    3
c ---[ 485]---> BDD-cost:    5
c ---[ 483]---> BDD-cost:    3
c ---[ 481]---> BDD-cost:    5
c ---[ 479]---> BDD-cost:    3
c ---[ 477]---> BDD-cost:    5
c ---[ 475]---> BDD-cost:    3
c ---[ 473]---> BDD-cost:    5
c ---[ 471]---> BDD-cost:    3
c ---[ 469]---> BDD-cost:    5
c ---[ 467]---> BDD-cost:    3
c ---[ 465]---> BDD-cost:    3
c ---[ 463]---> BDD-cost:    5
c ---[ 461]---> BDD-cost:    3
c ---[ 459]---> BDD-cost:    5
c ---[ 457]---> BDD-cost:    3
c ---[ 455]---> BDD-cost:    5
c ---[ 453]---> BDD-cost:    3
c ---[ 451]---> BDD-cost:    5
c ---[ 449]---> BDD-cost:    3
c ---[ 447]---> BDD-cost:    5
c ---[ 445]---> BDD-cost:    3
c ---[ 443]---> BDD-cost:    5
c ---[ 441]---> BDD-cost:    3
c ---[ 439]---> BDD-cost:    5
c ---[ 437]---> BDD-cost:    3
c ---[ 435]---> BDD-cost:    5
c ---[ 433]---> BDD-cost:    3
c ---[ 431]---> BDD-cost:    5
c ---[ 429]---> BDD-cost:    3
c ---[ 427]---> BDD-cost:    5
c ---[ 425]---> BDD-cost:    3
c ---[ 423]---> BDD-cost:    5
c ---[ 421]---> BDD-cost:    3
c ---[ 419]---> BDD-cost:    5
c ---[ 417]---> BDD-cost:    3
c ---[ 415]---> BDD-cost:    5
c ---[ 413]---> BDD-cost:    3
c ---[ 411]---> BDD-cost:    5
c ---[ 409]---> BDD-cost:    3
c ---[ 407]---> BDD-cost:    3
c ---[ 405]---> BDD-cost:    5
c ---[ 403]---> BDD-cost:    3
c ---[ 401]---> BDD-cost:    3
c ---[ 399]---> BDD-cost:    5
c ---[ 397]---> BDD-cost:    3
c ---[ 395]---> BDD-cost:    5
c ---[ 393]---> BDD-cost:    3
c ---[ 391]---> BDD-cost:    5
c ---[ 389]---> BDD-cost:    3
c ---[ 387]---> BDD-cost:    5
c ---[ 385]---> BDD-cost:    3
c ---[ 383]---> BDD-cost:    5
c ---[ 381]---> BDD-cost:    3
c ---[ 379]---> BDD-cost:    5
c ---[ 377]---> BDD-cost:    3
c ---[ 375]---> BDD-cost:    5
c ---[ 373]---> BDD-cost:    3
c ---[ 371]---> BDD-cost:    5
c ---[ 369]---> BDD-cost:    3
c ---[ 367]---> BDD-cost:    5
c ---[ 365]---> BDD-cost:    3
c ---[ 363]---> BDD-cost:    5
c ---[ 361]---> BDD-cost:    3
c ---[ 359]---> BDD-cost:    5
c ---[ 357]---> BDD-cost:    3
c ---[ 355]---> BDD-cost:    5
c ---[ 353]---> BDD-cost:    3
c ---[ 351]---> BDD-cost:    5
c ---[ 349]---> BDD-cost:    3
c ---[ 347]---> BDD-cost:    5
c ---[ 345]---> BDD-cost:    3
c ---[ 343]---> BDD-cost:    5
c ---[ 341]---> BDD-cost:    3
c ---[ 339]---> BDD-cost:    5
c ---[ 337]---> BDD-cost:    3
c ---[ 335]---> BDD-cost:    5
c ---[ 333]---> BDD-cost:    3
c ---[ 327]---> BDD-cost:    5
c ---[ 325]---> BDD-cost:    3
c ---[ 323]---> BDD-cost:    5
c ---[ 321]---> BDD-cost:    3
c ---[ 319]---> BDD-cost:    5
c ---[ 317]---> BDD-cost:    3
c ---[ 315]---> BDD-cost:    5
c ---[ 313]---> BDD-cost:    3
c ---[ 311]---> BDD-cost:    5
c ---[ 309]---> BDD-cost:    3
c ---[ 307]---> BDD-cost:    5
c ---[ 305]---> BDD-cost:    3
c ---[ 303]---> BDD-cost:    5
c ---[ 301]---> BDD-cost:    3
c ---[ 299]---> BDD-cost:    5
c ---[ 297]---> BDD-cost:    3
c ---[ 295]---> BDD-cost:    5
c ---[ 293]---> BDD-cost:    3
c ---[ 291]---> BDD-cost:    5
c ---[ 289]---> BDD-cost:    3
c ---[ 287]---> BDD-cost:    5
c ---[ 285]---> BDD-cost:    3
c ---[ 283]---> BDD-cost:    5
c ---[ 281]---> BDD-cost:    3
c ---[ 279]---> BDD-cost:    5
c ---[ 277]---> BDD-cost:    3
c ---[ 275]---> BDD-cost:    3
c ---[ 273]---> BDD-cost:    5
c ---[ 271]---> BDD-cost:    3
c ---[ 269]---> BDD-cost:    5
c ---[ 267]---> BDD-cost:    3
c ---[ 265]---> BDD-cost:    5
c ---[ 263]---> BDD-cost:    3
c ---[ 261]---> BDD-cost:    5
c ---[ 259]---> BDD-cost:    3
c ---[ 257]---> BDD-cost:    5
c ---[ 255]---> BDD-cost:    3
c ---[ 253]---> BDD-cost:    5
c ---[ 251]---> BDD-cost:    3
c ---[ 249]---> BDD-cost:    5
c ---[ 247]---> BDD-cost:    3
c ---[ 245]---> BDD-cost:    5
c ---[ 243]---> BDD-cost:    3
c ---[ 241]---> BDD-cost:    5
c ---[ 239]---> BDD-cost:    3
c ---[ 237]---> BDD-cost:    5
c ---[ 235]---> BDD-cost:    3
c ---[ 233]---> BDD-cost:    5
c ---[ 231]---> BDD-cost:    3
c ---[ 229]---> BDD-cost:    5
c ---[ 227]---> BDD-cost:    3
c ---[ 225]---> BDD-cost:    5
c ---[ 223]---> BDD-cost:    3
c ---[ 221]---> BDD-cost:    5
c ---[ 219]---> BDD-cost:    3
c ---[ 217]---> BDD-cost:    5
c ---[ 215]---> BDD-cost:    3
c ---[ 213]---> BDD-cost:    5
c ---[ 211]---> BDD-cost:    3
c ---[ 209]---> BDD-cost:    5
c ---[ 207]---> BDD-cost:    3
c ---[ 205]---> BDD-cost:    5
c ---[ 203]---> BDD-cost:    3
c ---[ 201]---> BDD-cost:    5
c ---[ 199]---> BDD-cost:    3
c ---[ 197]---> BDD-cost:    5
c ---[ 195]---> BDD-cost:    3
c ---[ 193]---> BDD-cost:    5
c ---[ 191]---> BDD-cost:    3
c ---[ 189]---> BDD-cost:    5
c ---[ 187]---> BDD-cost:    3
c ---[ 185]---> BDD-cost:    5
c ---[ 183]---> BDD-cost:    3
c ---[ 181]---> BDD-cost:    5
c ---[ 179]---> BDD-cost:    3
c ---[ 177]---> BDD-cost:    5
c ---[ 175]---> BDD-cost:    3
c ---[ 173]---> BDD-cost:    5
c ---[ 171]---> BDD-cost:    3
c ---[ 169]---> BDD-cost:    3
c ---[ 167]---> BDD-cost:    5
c ---[ 165]---> BDD-cost:    3
c ---[ 163]---> BDD-cost:    3
c ---[ 161]---> BDD-cost:    5
c ---[ 159]---> BDD-cost:    3
c ---[ 157]---> BDD-cost:    5
c ---[ 155]---> BDD-cost:    3
c ---[ 153]---> BDD-cost:    5
c ---[ 151]---> BDD-cost:    3
c ---[ 149]---> BDD-cost:    5
c ---[ 147]---> BDD-cost:    3
c ---[ 145]---> BDD-cost:    5
c ---[ 143]---> BDD-cost:    3
c ---[ 141]---> BDD-cost:    5
c ---[ 139]---> BDD-cost:    3
c ---[ 137]---> BDD-cost:    5
c ---[ 135]---> BDD-cost:    3
c ---[ 133]---> BDD-cost:    5
c ---[ 131]---> BDD-cost:    3
c ---[ 129]---> BDD-cost:    5
c ---[ 127]---> BDD-cost:    3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   15378    52452 |    4613       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3545          
c   -- var.elim.:  2000/3545          
c   -- var.elim.:  3000/3545          
c   -- var.elim.:  3545/3545          
c   -- var.elim.:  1000/1307          
c   -- var.elim.:  1307/1307          
c   -- var.elim.:  8/8          
c   -- subsuming                       
c   -- var.elim.:  651/651          
c   -- var.elim.:  500/500          
c   -- subsuming                       
c |         0 |   14202    48742 |      --       0       --      -- |     --   | -1160/-2812
c |         0 |   14202    48742 |    5680       0        0     nan |  0.000 % |
c |       100 |   14180    48668 |    6239      98      381     3.9 | 10.472 % |
c |       250 |   14180    48668 |    6863     248      955     3.9 | 10.472 % |
c |       475 |   14180    48668 |    7549     473     1829     3.9 | 10.472 % |
c |       812 |   14180    48668 |    8304     810     3723     4.6 | 10.472 % |
c |      1318 |   14180    48668 |    9134    1316     6738     5.1 | 10.472 % |
c |      2077 |   14180    48668 |   10048    2075    20613     9.9 | 10.472 % |
c |      3217 |   14180    48668 |   11053    3215    34064    10.6 | 10.472 % |
c |      4925 |   14180    48668 |   12158    4923    63910    13.0 | 10.472 % |
c ==============================================================================
c (current CPU-time: 1.71074 s)
c ==============================================================================
c [1mFound solution: 8706[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:30425     Base: 5 5 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      5319 |   78040   197967 |   23411    5317    71080    13.4 | 10.472 % |
c   -- subsuming                       
c   -- var.elim.:  1000/26590          
c   -- var.elim.:  2000/26590          
c   -- var.elim.:  3000/26590          
c   -- var.elim.:  4000/26590          
c   -- var.elim.:  5000/26590          
c   -- var.elim.:  6000/26590          
c   -- var.elim.:  7000/26590          
c   -- var.elim.:  8000/26590          
c   -- var.elim.:  9000/26590          
c   -- var.elim.:  10000/26590          
c   -- var.elim.:  11000/26590          
c   -- var.elim.:  12000/26590          
c   -- var.elim.:  13000/26590          
c   -- var.elim.:  14000/26590          
c   -- var.elim.:  15000/26590          
c   -- var.elim.:  16000/26590          
c   -- var.elim.:  17000/26590          
c   -- var.elim.:  18000/26590          
c   -- var.elim.:  19000/26590          
c   -- var.elim.:  20000/26590          
c   -- var.elim.:  21000/26590          
c   -- var.elim.:  22000/26590          
c   -- var.elim.:  23000/26590          
c   -- var.elim.:  24000/26590          
c   -- var.elim.:  25000/26590          
c   -- var.elim.:  26000/26590          
c   -- var.elim.:  26590/26590          
c   -- var.elim.:  1000/15151          
c   -- var.elim.:  2000/15151          
c   -- var.elim.:  3000/15151          
c   -- var.elim.:  4000/15151          
c   -- var.elim.:  5000/15151          
c   -- var.elim.:  6000/15151          
c   -- var.elim.:  7000/15151          
c   -- var.elim.:  8000/15151          
c   -- var.elim.:  9000/15151          
c   -- var.elim.:  10000/15151          
c   -- var.elim.:  11000/15151          
c   -- var.elim.:  12000/15151          
c   -- var.elim.:  13000/15151          
c   -- var.elim.:  14000/15151          
c   -- var.elim.:  15000/15151          
c   -- var.elim.:  15151/15151          
c   -- var.elim.:  1000/3621          
c   -- var.elim.:  2000/3621          
c   -- var.elim.:  3000/3621          
c   -- var.elim.:  3621/3621          
c   -- var.elim.:  1000/2905          
c   -- var.elim.:  2000/2905          
c   -- var.elim.:  2905/2905          
c   -- var.elim.:  1000/2156          
c   -- var.elim.:  2000/2156          
c   -- var.elim.:  2156/2156          
c   -- var.elim.:  271/271          
c   -- subsuming                       
c   -- var.elim.:  1000/3112          
c   -- var.elim.:  2000/3112          
c   -- var.elim.:  3000/3112          
c   -- var.elim.:  3112/3112          
c   -- var.elim.:  1000/2000          
c   -- var.elim.:  2000/2000          
c   -- var.elim.:  1000/2057          
c   -- var.elim.:  2000/2057          
c   -- var.elim.:  2057/2057          
c   -- var.elim.:  1000/2144          
c   -- var.elim.:  2000/2144          
c   -- var.elim.:  2144/2144          
c   -- var.elim.:  1000/1589          
c   -- var.elim.:  1589/1589          
c   -- var.elim.:  182/182          
c   -- subsuming                       
c   -- var.elim.:  1000/1735          
c   -- var.elim.:  1735/1735          
c   -- var.elim.:  591/591          
c |      5319 |   54190   186469 |      --    5317       --      -- |     --   | -23850/-11497
c |      5319 |   54190   186469 |   21676    5317    71080    13.4 | 10.472 % |
c |      5420 |   54190   186469 |   23843    5418    71579    13.2 | 22.137 % |
c |      5570 |   54190   186469 |   26227    5568    72418    13.0 | 22.137 % |
c |      5797 |   54109   186199 |   28807    5794    73824    12.7 | 22.200 % |
c |      6134 |   52255   180061 |   30602    5987    76942    12.9 | 24.043 % |
c |      6640 |   52255   180061 |   33662    6493    88961    13.7 | 24.043 % |
c |      7400 |   49911   172291 |   35368    7176    97010    13.5 | 26.382 % |
c |      8539 |   44780   155625 |   34905    8048   101165    12.6 | 31.759 % |
c ==============================================================================
c (current CPU-time: 23.6054 s)
c ==============================================================================
c [1mFound solution: 5386[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 5 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      9568 |   51861   173053 |   15558    9046   114594    12.7 | 31.759 % |
c   -- subsuming                       
c   -- var.elim.:  1000/11993          
c   -- var.elim.:  2000/11993          
c   -- var.elim.:  3000/11993          
c   -- var.elim.:  4000/11993          
c   -- var.elim.:  5000/11993          
c   -- var.elim.:  6000/11993          
c   -- var.elim.:  7000/11993          
c   -- var.elim.:  8000/11993          
c   -- var.elim.:  9000/11993          
c   -- var.elim.:  10000/11993          
c   -- var.elim.:  11000/11993          
c   -- var.elim.:  11993/11993          
c   -- var.elim.:  1000/6128          
c   -- var.elim.:  2000/6128          
c   -- var.elim.:  3000/6128          
c   -- var.elim.:  4000/6128          
c   -- var.elim.:  5000/6128          
c   -- var.elim.:  6000/6128          
c   -- var.elim.:  6128/6128          
c   -- var.elim.:  1000/2834          
c   -- var.elim.:  2000/2834          
c   -- var.elim.:  2834/2834          
c   -- var.elim.:  1000/2616          
c   -- var.elim.:  2000/2616          
c   -- var.elim.:  2616/2616          
c   -- var.elim.:  1000/1975          
c   -- var.elim.:  1975/1975          
c   -- var.elim.:  1000/1039          
c   -- var.elim.:  1039/1039          
c   -- subsuming                       
c   -- var.elim.:  1000/2480          
c   -- var.elim.:  2000/2480          
c   -- var.elim.:  2480/2480          
c   -- var.elim.:  1000/1332          
c   -- var.elim.:  1332/1332          
c   -- var.elim.:  1000/1898          
c   -- var.elim.:  1898/1898          
c   -- var.elim.:  1000/1629          
c   -- var.elim.:  1629/1629          
c   -- var.elim.:  863/863          
c   -- var.elim.:  335/335          
c   -- var.elim.:  2/2          
c   -- subsuming                       
c   -- var.elim.:  403/403          
c   -- var.elim.:  14/14          
c |      9568 |   43648   153700 |      --    9046       --      -- |     --   | -8211/-19348
c |      9568 |   43648   153700 |   17459    8712   110034    12.6 | 31.759 % |
c |      9668 |   43648   153700 |   19205    8812   111704    12.7 | 33.626 % |
c |      9818 |   43603   153548 |   21103    8961   113211    12.6 | 33.665 % |
c |     10043 |   43603   153548 |   23214    9186   115943    12.6 | 33.665 % |
c |     10381 |   43603   153548 |   25535    9524   119675    12.6 | 33.665 % |
c |     10887 |   43603   153548 |   28089   10030   132992    13.3 | 33.665 % |
c |     11648 |   43603   153548 |   30898   10791   155385    14.4 | 33.665 % |
c |     12788 |   43603   153548 |   33987   11931   181355    15.2 | 33.665 % |
c |     14497 |   43603   153548 |   37386   13640   231160    16.9 | 33.665 % |
c |     17059 |   43603   153548 |   41125   16202   287267    17.7 | 33.665 % |
c |     20905 |   43603   153548 |   45237   20048   407859    20.3 | 33.665 % |
c ==============================================================================
c (current CPU-time: 39.329 s)
c ==============================================================================
c [1mFound solution: 4172[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 5 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     22173 |   50502   171091 |   15150   21316   442441    20.8 | 33.665 % |
c   -- subsuming                       
c   -- var.elim.:  1000/7965          
c   -- var.elim.:  2000/7965          
c   -- var.elim.:  3000/7965          
c   -- var.elim.:  4000/7965          
c   -- var.elim.:  5000/7965          
c   -- var.elim.:  6000/7965          
c   -- var.elim.:  7000/7965          
c   -- var.elim.:  7965/7965          
c   -- var.elim.:  1000/3881          
c   -- var.elim.:  2000/3881          
c   -- var.elim.:  3000/3881          
c   -- var.elim.:  3881/3881          
c   -- var.elim.:  1000/2451          
c   -- var.elim.:  2000/2451          
c   -- var.elim.:  2451/2451          
c   -- var.elim.:  1000/1985          
c   -- var.elim.:  1985/1985          
c   -- var.elim.:  1000/1436          
c   -- var.elim.:  1436/1436          
c   -- var.elim.:  1000/1109          
c   -- var.elim.:  1109/1109          
c   -- var.elim.:  801/801          
c   -- subsuming                       
c   -- var.elim.:  1000/1745          
c   -- var.elim.:  1745/1745          
c   -- var.elim.:  1000/1063          
c   -- var.elim.:  1063/1063          
c   -- var.elim.:  1000/1289          
c   -- var.elim.:  1289/1289          
c   -- var.elim.:  1000/1230          
c   -- var.elim.:  1230/1230          
c   -- var.elim.:  626/626          
c   -- subsuming                       
c |     22173 |   44110   156210 |      --   21316       --      -- |     --   | -6378/-14852
c |     22173 |   44110   156210 |   17644   21315   442439    20.8 | 33.665 % |
c |     22275 |   44110   156210 |   19408   21417   443585    20.7 | 34.905 % |
c |     22425 |   44110   156210 |   21349   21567   446599    20.7 | 34.905 % |
c |     22650 |   43795   155145 |   23316   21781   448926    20.6 | 35.173 % |
c |     22987 |   43795   155145 |   25648   22118   453454    20.5 | 35.173 % |
c |     23494 |   43675   154716 |   28135   22607   464543    20.5 | 35.260 % |
c |     24253 |   43496   154125 |   30822   23364   471089    20.2 | 35.429 % |
c |     25392 |   43355   153660 |   33794   24489   493278    20.1 | 35.566 % |
c |     27100 |   43161   152941 |   37007   26192   521503    19.9 | 35.716 % |
c |     29662 |   43153   152916 |   40701   28743   608193    21.2 | 35.722 % |
c |     33506 |   43034   152518 |   44647   32576   756472    23.2 | 35.828 % |
c ==============================================================================
c (current CPU-time: 59.5729 s)
c ==============================================================================
c [1mFound solution: 4068[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 5 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     36744 |   49279   168426 |   14783   35814   867477    24.2 | 35.828 % |
c   -- subsuming                       
c   -- var.elim.:  1000/7811          
c   -- var.elim.:  2000/7811          
c   -- var.elim.:  3000/7811          
c   -- var.elim.:  4000/7811          
c   -- var.elim.:  5000/7811          
c   -- var.elim.:  6000/7811          
c   -- var.elim.:  7000/7811          
c   -- var.elim.:  7811/7811          
c   -- var.elim.:  1000/3810          
c   -- var.elim.:  2000/3810          
c   -- var.elim.:  3000/3810          
c   -- var.elim.:  3810/3810          
c   -- var.elim.:  1000/2380          
c   -- var.elim.:  2000/2380          
c   -- var.elim.:  2380/2380          
c   -- var.elim.:  1000/1924          
c   -- var.elim.:  1924/1924          
c   -- var.elim.:  1000/1445          
c   -- var.elim.:  1445/1445          
c   -- var.elim.:  875/875          
c   -- var.elim.:  742/742          
c   -- var.elim.:  390/390          
c   -- subsuming                       
c   -- var.elim.:  1000/1435          
c   -- var.elim.:  1435/1435          
c   -- var.elim.:  1000/1073          
c   -- var.elim.:  1073/1073          
c   -- var.elim.:  1000/1215          
c   -- var.elim.:  1215/1215          
c   -- var.elim.:  974/974          
c   -- var.elim.:  160/160          
c   -- var.elim.:  2/2          
c   -- subsuming                       
c |     36744 |   43373   154611 |      --   35814       --      -- |     --   | -5895/-13792
c |     36744 |   43373   154611 |   17349   35291   830411    23.5 | 35.828 % |
c |     36844 |   43373   154611 |   19084   14454   357599    24.7 | 36.422 % |
c |     36995 |   43373   154611 |   20992   14605   359890    24.6 | 36.422 % |
c |     37221 |   43373   154611 |   23091   14831   366718    24.7 | 36.422 % |
c |     37558 |   43373   154611 |   25400   15168   378234    24.9 | 36.422 % |
c |     38065 |   43373   154611 |   27941   15675   384626    24.5 | 36.422 % |
c |     38824 |   43373   154611 |   30735   16434   420465    25.6 | 36.422 % |
c |     39963 |   43368   154591 |   33804   17572   434533    24.7 | 36.429 % |
c |     41673 |   43368   154591 |   37185   19282   512771    26.6 | 36.429 % |
c |     44236 |   43351   154534 |   40887   21843   578091    26.5 | 36.447 % |
c |     48080 |   43351   154534 |   44976   25687   684759    26.7 | 36.447 % |
c |     53846 |   43218   154082 |   49322   31447   985095    31.3 | 36.576 % |
c |     62496 |   43208   154046 |   54242   40092  1302671    32.5 | 36.583 % |
c |     75471 |   43208   154046 |   59666   53067  2119948    39.9 | 36.583 % |
c |     94933 |   43208   154046 |   65632   18875   823837    43.6 | 36.583 % |
c |    124125 |   43208   154046 |   72196   48067  3121643    64.9 | 36.583 % |
c |    167914 |   43208   154046 |   79415   27928  2435445    87.2 | 36.583 % |
c |    233599 |   43208   154046 |   87357   23696  2610820   110.2 | 36.583 % |
c |    332125 |   43203   154030 |   96082   42228  3317810    78.6 | 36.589 % |
c |    479914 |   43203   154030 |  105690  103130  8712647    84.5 | 36.589 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -v1 v127 v505 -v640 v774 -v4 v256 v508 -v5 -v131 -v257 v383 v509 v6 -v132 -v258 -v510 v7 -v133 -v512 -v8 v134 v513 v388 v516 -v11 v137 v517 -v12 v138 v518 -v14 v392 v520 -v15 -v141 v267 v521 -v16 v394 -v522 -v17 v143 v523 -v18 v396 v524 v19 -v525 v659 -v20 v146 -v526 -v21 v273 v527 v22 -v528 v662 -v23 v149 -v529 -v24 v150 v530 -v25 -v151 v403 -v531 -v26 -v152 v532 -v27 -v153 -v533 -v28 v406 v534 -v29 v407 v535 -v30 v156 v536 -v31 v157 v537 -v32 -v158 -v672 -v806 -v33 -v159 -v285 -v539 -v34 v160 -v540 -v287 -v413 -v36 -v162 -v542 -v37 v163 v543 -v38 v164 v544 v39 -v545 -v679 v813 -v40 v166 v546 -v41 v419 v547 v42 -v168 -v548 -v43 -v421 v549 v44 -v170 -v550 -v551 -v45 v171 -v552 v686 v46 -v172 -v553 v47 -v173 -v425 -v554 -v48 -v174 v426 -v555 -v49 v175 -v556 v428 v51 -v177 -v558 v52 -v178 -v559 v431 -v694 v828 -v54 -v180 v432 v561 -v55 v433 v562 -v56 v308 -v563 v697 -v831 v57 -v435 -v564 -v58 v436 -v565 -v566 -v59 v185 v567 v568 v60 -v569 -v703 v837 -v61 v187 v570 -v62 v314 -v440 v571 -v705 -v839 -v63 -v189 -v572 v64 -v316 -v573 -v65 v317 -v574 -v66 v318 -v575 -v67 v193 -v576 v710 -v68 -v194 v320 -v577 v711 -v845 v69 -v195 -v447 -v578 -v70 v196 -v579 v71 -v580 v714 v72 -v198 -v581 v73 -v582 -v74 v200 -v583 v75 -v201 -v584 -v76 v202 v585 -v78 -v204 -v330 v456 v587 -v79 v457 -v588 v722 -v589 v81 -v207 -v333 -v459 -v590 -v82 v334 -v591 v83 -v335 -v461 -v592 v726 v727 -v861 v85 -v211 -v594 v728 -v862 -v86 -v212 v464 v595 v87 -v213 -v596 v730 -v864 -v88 v214 v597 -v89 v467 -v598 v732 v90 -v216 -v468 -v599 -v600 -v92 v218 v602 -v93 v219 v603 v94 -v220 -v604 -v738 v872 -v96 -v222 -v606 -v349 v475 v741 -v98 v224 -v608 -v99 -v351 v477 -v609 -v743 v877 v226 v744 -v878 v227 v745 -v879 -v102 -v228 v354 -v480 v612 -v103 -v229 v355 -v481 v613 -v104 -v614 -v748 v105 -v231 -v357 -v483 -v615 v106 -v616 v107 -v233 -v485 -v617 v108 -v234 -v618 v109 -v235 -v619 v753 -v110 -v236 -v362 v488 -v620 -v754 v888 -v756 v890 -v113 v365 -v623 v240 -v115 -v241 v493 -v625 v759 v116 -v242 -v626 v627 -v761 -v895 -v117 v495 v628 -v118 -v370 -v630 -v764 v898 v119 -v631 v765 -v899 -v120 v246 v632 -v766 -v900 -v121 v373 v633 -v122 -v374 -v500 -v634 -v123 -v635 -v903 -v124 -v376 -v502 -v636 -v770 v904 -v771 v905 v126 -v638 v772 -v2 -v128 -v506 -v3 -v507 -v641 -v130 -v642 -v776 -v643 -v777 -v384 -v644 v778 -v645 -v779 -v259 -v646 v780 -v260 -v386 -v647 -v781 -v261 -v387 -v136 -v389 -v264 -v390 -v652 -v786 -v654 -v788 -v655 -v789 -v142 v656 -v790 -v269 -v657 -v791 -v270 -v658 -v792 -v145 -v271 -v272 -v398 -v660 v794 -v147 -v399 -v661 -v795 -v148 -v400 -v275 -v663 v797 -v276 -v402 -v664 -v798 -v277 v665 -v799 -v278 v404 #### 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.85 0.95 0.90 2/54 28796
Raw data (stat): 28796 (runsolver) R 28795 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480556722 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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.0005 s]
Raw data (loadavg): 0.87 0.95 0.90 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 4923 0 3 0 976 21 0 0 25 0 1 0 480556722 22106112 4684 4294967295 134512640 134672761 3221224576 3221223024 134643524 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5397 4684 603 41 0 5356 0
vsize: 21588
[startup+20.0011 s]
Raw data (loadavg): 0.89 0.95 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 5159 0 3 0 1973 24 0 0 25 0 1 0 480556722 22106112 4689 4294967295 134512640 134672761 3221224576 3221223760 134615583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5397 4689 603 41 0 5356 0
vsize: 21588
[startup+30.0019 s]
Raw data (loadavg): 0.91 0.95 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 6511 0 3 0 2963 33 0 0 25 0 1 0 480556722 25784320 5139 4294967295 134512640 134672761 3221224576 3221223024 134643565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6295 5139 603 41 0 6254 0
vsize: 25180
[startup+40.0029 s]
Raw data (loadavg): 0.92 0.95 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 7839 0 3 0 3958 38 0 0 25 0 1 0 480556722 33316864 6318 4294967295 134512640 134672761 3221224576 3221222912 134604485 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8134 6318 603 41 0 8093 0
vsize: 32536
[startup+50.0038 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 8764 0 3 0 4950 45 0 0 25 0 1 0 480556722 26943488 5515 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6578 5515 603 41 0 6537 0
vsize: 26312
[startup+60.0036 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 9128 0 3 0 5949 47 0 0 25 0 1 0 480556722 28667904 5879 4294967295 134512640 134672761 3221224576 3221223616 134612665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6999 5879 603 41 0 6958 0
vsize: 27996
[startup+70.0051 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 11735 0 3 0 6936 60 0 0 25 0 1 0 480556722 29917184 6294 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7304 6294 603 41 0 7263 0
vsize: 29216
[startup+80.0055 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 11735 0 3 0 7935 60 0 0 25 0 1 0 480556722 29917184 6294 4294967295 134512640 134672761 3221224576 3221223760 134615660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7304 6294 603 41 0 7263 0
vsize: 29216
[startup+90.0064 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 11981 0 3 0 8935 61 0 0 25 0 1 0 480556722 30965760 6540 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7560 6540 603 41 0 7519 0
vsize: 30240
[startup+100.007 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 12288 0 3 0 9934 62 0 0 25 0 1 0 480556722 32157696 6847 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7851 6847 603 41 0 7810 0
vsize: 31404
[startup+110.006 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 12683 0 3 0 10932 64 0 0 25 0 1 0 480556722 33878016 7242 4294967295 134512640 134672761 3221224576 3221223616 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8271 7242 603 41 0 8230 0
vsize: 33084
[startup+120.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 13173 0 3 0 11930 65 0 0 25 0 1 0 480556722 35745792 7732 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8727 7732 603 41 0 8686 0
vsize: 34908
[startup+130.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 13549 0 3 0 12929 67 0 0 25 0 1 0 480556722 37326848 8108 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9113 8108 603 41 0 9072 0
vsize: 36452
[startup+140.007 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 13869 0 3 0 13929 67 0 0 25 0 1 0 480556722 38924288 8428 4294967295 134512640 134672761 3221224576 3221223760 134615926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9503 8428 603 41 0 9462 0
vsize: 38012
[startup+150.007 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 14090 0 3 0 14929 68 0 0 25 0 1 0 480556722 39358464 8551 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9609 8551 603 41 0 9568 0
vsize: 38436
[startup+160.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 14090 0 3 0 15929 68 0 0 25 0 1 0 480556722 39358464 8551 4294967295 134512640 134672761 3221224576 3221223760 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9609 8551 603 41 0 9568 0
vsize: 38436
[startup+170.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 14090 0 3 0 16929 68 0 0 25 0 1 0 480556722 39358464 8551 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9609 8551 603 41 0 9568 0
vsize: 38436
[startup+180.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 14090 0 3 0 17929 68 0 0 25 0 1 0 480556722 39358464 8551 4294967295 134512640 134672761 3221224576 3221223568 134565137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9609 8551 603 41 0 9568 0
vsize: 38436
[startup+190.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 14090 0 3 0 18929 68 0 0 25 0 1 0 480556722 39358464 8551 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9609 8551 603 41 0 9568 0
vsize: 38436
[startup+200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 14262 0 3 0 19929 68 0 0 25 0 1 0 480556722 40169472 8723 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9807 8723 603 41 0 9766 0
vsize: 39228
[startup+210.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 14643 0 3 0 20928 69 0 0 25 0 1 0 480556722 41758720 9104 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10195 9104 603 41 0 10154 0
vsize: 40780
[startup+220.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 14952 0 3 0 21927 71 0 0 25 0 1 0 480556722 42946560 9413 4294967295 134512640 134672761 3221224576 3221223760 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10485 9413 603 41 0 10444 0
vsize: 41940
[startup+230.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 15313 0 3 0 22926 71 0 0 25 0 1 0 480556722 44417024 9774 4294967295 134512640 134672761 3221224576 3221223568 134565101 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10844 9775 603 41 0 10803 0
vsize: 43376
[startup+240.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 15620 0 3 0 23925 73 0 0 25 0 1 0 480556722 45735936 10081 4294967295 134512640 134672761 3221224576 3221223408 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11166 10082 603 41 0 11125 0
vsize: 44664
[startup+250.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 15897 0 3 0 24925 74 0 0 25 0 1 0 480556722 46792704 10358 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11424 10358 603 41 0 11383 0
vsize: 45696
[startup+260.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 16188 0 3 0 25923 75 0 0 25 0 1 0 480556722 47988736 10649 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11716 10649 603 41 0 11675 0
vsize: 46864
[startup+270.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 16479 0 3 0 26922 77 0 0 25 0 1 0 480556722 49201152 10940 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12012 10940 603 41 0 11971 0
vsize: 48048
[startup+280.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 16751 0 3 0 27921 77 0 0 25 0 1 0 480556722 50388992 11212 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12302 11212 603 41 0 12261 0
vsize: 49208
[startup+290.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 17022 0 3 0 28921 78 0 0 25 0 1 0 480556722 51449856 11483 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12561 11483 603 41 0 12520 0
vsize: 50244
[startup+300.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 17289 0 3 0 29920 80 0 0 25 0 1 0 480556722 52510720 11750 4294967295 134512640 134672761 3221224576 3221223760 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12820 11750 603 41 0 12779 0
vsize: 51280
[startup+310.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 17673 0 3 0 30919 81 0 0 25 0 1 0 480556722 54157312 12102 4294967295 134512640 134672761 3221224576 3221223632 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13222 12102 603 41 0 13181 0
vsize: 52888
[startup+320.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 17684 0 3 0 31919 81 0 0 25 0 1 0 480556722 53633024 12035 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13094 12035 603 41 0 13053 0
vsize: 52376
[startup+330.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 17684 0 3 0 32919 81 0 0 25 0 1 0 480556722 53633024 12035 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13094 12035 603 41 0 13053 0
vsize: 52376
[startup+340.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 17685 0 3 0 33919 81 0 0 25 0 1 0 480556722 53633024 12036 4294967295 134512640 134672761 3221224576 3221223760 134615660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13094 12036 603 41 0 13053 0
vsize: 52376
[startup+350.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 17685 0 3 0 34919 81 0 0 25 0 1 0 480556722 53633024 12036 4294967295 134512640 134672761 3221224576 3221223760 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13094 12036 603 41 0 13053 0
vsize: 52376
[startup+360.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 17685 0 3 0 35920 81 0 0 25 0 1 0 480556722 53633024 12036 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13094 12036 603 41 0 13053 0
vsize: 52376
[startup+370.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 17685 0 3 0 36920 81 0 0 25 0 1 0 480556722 53633024 12036 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13094 12036 603 41 0 13053 0
vsize: 52376
[startup+380.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 17686 0 3 0 37920 81 0 0 25 0 1 0 480556722 53633024 12037 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13094 12037 603 41 0 13053 0
vsize: 52376
[startup+390.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 17686 0 3 0 38920 81 0 0 25 0 1 0 480556722 53633024 12037 4294967295 134512640 134672761 3221224576 3221223760 134615686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13094 12037 603 41 0 13053 0
vsize: 52376
[startup+400.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 17686 0 3 0 39920 81 0 0 25 0 1 0 480556722 53633024 12037 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13094 12037 603 41 0 13053 0
vsize: 52376
[startup+410.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 17686 0 3 0 40920 81 0 0 25 0 1 0 480556722 53633024 12037 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13094 12037 603 41 0 13053 0
vsize: 52376
[startup+420.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 17686 0 3 0 41921 81 0 0 25 0 1 0 480556722 53633024 12037 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13094 12037 603 41 0 13053 0
vsize: 52376
[startup+430.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 17837 0 3 0 42920 81 0 0 25 0 1 0 480556722 54321152 12188 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13262 12188 603 41 0 13221 0
vsize: 53048
[startup+440.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 18113 0 3 0 43920 82 0 0 25 0 1 0 480556722 55508992 12464 4294967295 134512640 134672761 3221224576 3221223712 134614753 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13552 12464 603 41 0 13511 0
vsize: 54208
[startup+450.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 18420 0 3 0 44919 83 0 0 25 0 1 0 480556722 56696832 12771 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13842 12771 603 41 0 13801 0
vsize: 55368
[startup+460.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 18729 0 3 0 45918 84 0 0 25 0 1 0 480556722 58023936 13080 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14166 13080 603 41 0 14125 0
vsize: 56664
[startup+470.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 19045 0 3 0 46916 86 0 0 25 0 1 0 480556722 59342848 13396 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14488 13396 603 41 0 14447 0
vsize: 57952
[startup+480.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 19375 0 3 0 47916 87 0 0 25 0 1 0 480556722 60674048 13726 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14813 13726 603 41 0 14772 0
vsize: 59252
[startup+490.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 19688 0 3 0 48915 88 0 0 25 0 1 0 480556722 61992960 14039 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15135 14039 603 41 0 15094 0
vsize: 60540
[startup+500.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 19986 0 3 0 49914 89 0 0 25 0 1 0 480556722 63193088 14337 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15428 14337 603 41 0 15387 0
vsize: 61712
[startup+510.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 20285 0 3 0 50913 90 0 0 25 0 1 0 480556722 64376832 14636 4294967295 134512640 134672761 3221224576 3221223728 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15717 14636 603 41 0 15676 0
vsize: 62868
[startup+520.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 20576 0 3 0 51911 92 0 0 25 0 1 0 480556722 65560576 14927 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16006 14927 603 41 0 15965 0
vsize: 64024
[startup+530.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 20832 0 3 0 52910 93 0 0 25 0 1 0 480556722 66633728 15183 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16268 15183 603 41 0 16227 0
vsize: 65072
[startup+540.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21102 0 3 0 53910 94 0 0 25 0 1 0 480556722 67817472 15453 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16557 15453 603 41 0 16516 0
vsize: 66228
[startup+550.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21366 0 3 0 54910 95 0 0 25 0 1 0 480556722 68530176 15599 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16731 15599 603 41 0 16690 0
vsize: 66924
[startup+560.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21366 0 3 0 55910 95 0 0 25 0 1 0 480556722 68530176 15599 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16731 15599 603 41 0 16690 0
vsize: 66924
[startup+570.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21366 0 3 0 56910 95 0 0 25 0 1 0 480556722 68530176 15599 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16731 15599 603 41 0 16690 0
vsize: 66924
[startup+580.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21366 0 3 0 57910 95 0 0 25 0 1 0 480556722 68530176 15599 4294967295 134512640 134672761 3221224576 3221223760 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16731 15599 603 41 0 16690 0
vsize: 66924
[startup+590.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21366 0 3 0 58910 95 0 0 25 0 1 0 480556722 68530176 15599 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16731 15599 603 41 0 16690 0
vsize: 66924
[startup+600.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21366 0 3 0 59910 95 0 0 25 0 1 0 480556722 68530176 15599 4294967295 134512640 134672761 3221224576 3221223760 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16731 15599 603 41 0 16690 0
vsize: 66924
[startup+610.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21366 0 3 0 60911 95 0 0 25 0 1 0 480556722 68530176 15599 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16731 15599 603 41 0 16690 0
vsize: 66924
[startup+620.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21366 0 3 0 61911 95 0 0 25 0 1 0 480556722 68530176 15599 4294967295 134512640 134672761 3221224576 3221223712 134614560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16731 15599 603 41 0 16690 0
vsize: 66924
[startup+630.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21367 0 3 0 62911 95 0 0 25 0 1 0 480556722 68530176 15600 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16731 15600 603 41 0 16690 0
vsize: 66924
[startup+640.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21367 0 3 0 63911 95 0 0 25 0 1 0 480556722 68530176 15600 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16731 15600 603 41 0 16690 0
vsize: 66924
[startup+650.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21367 0 3 0 64912 95 0 0 25 0 1 0 480556722 68530176 15600 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16731 15600 603 41 0 16690 0
vsize: 66924
[startup+660.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21367 0 3 0 65912 95 0 0 25 0 1 0 480556722 68530176 15600 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16731 15600 603 41 0 16690 0
vsize: 66924
[startup+670.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21367 0 3 0 66912 95 0 0 25 0 1 0 480556722 68530176 15600 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16731 15600 603 41 0 16690 0
vsize: 66924
[startup+680.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21367 0 3 0 67912 95 0 0 25 0 1 0 480556722 68530176 15600 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16731 15600 603 41 0 16690 0
vsize: 66924
[startup+690.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21367 0 3 0 68912 95 0 0 25 0 1 0 480556722 68530176 15600 4294967295 134512640 134672761 3221224576 3221223760 134615671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16731 15600 603 41 0 16690 0
vsize: 66924
[startup+700.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21369 0 3 0 69912 95 0 0 25 0 1 0 480556722 68530176 15602 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16731 15602 603 41 0 16690 0
vsize: 66924
[startup+710.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21371 0 3 0 70913 95 0 0 25 0 1 0 480556722 68530176 15604 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16731 15604 603 41 0 16690 0
vsize: 66924
[startup+720.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21373 0 3 0 71913 95 0 0 25 0 1 0 480556722 68530176 15606 4294967295 134512640 134672761 3221224576 3221223760 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16731 15606 603 41 0 16690 0
vsize: 66924
[startup+730.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21469 0 3 0 72913 95 0 0 25 0 1 0 480556722 68792320 15638 4294967295 134512640 134672761 3221224576 3221223632 134644266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16795 15638 603 41 0 16754 0
vsize: 67180
[startup+740.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21480 0 3 0 73913 95 0 0 25 0 1 0 480556722 68268032 15555 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16667 15555 603 41 0 16626 0
vsize: 66668
[startup+750.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21482 0 3 0 74913 95 0 0 25 0 1 0 480556722 68268032 15557 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16667 15557 603 41 0 16626 0
vsize: 66668
[startup+760.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21482 0 3 0 75913 95 0 0 25 0 1 0 480556722 68268032 15557 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16667 15557 603 41 0 16626 0
vsize: 66668
[startup+770.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21482 0 3 0 76914 95 0 0 25 0 1 0 480556722 68268032 15557 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16667 15557 603 41 0 16626 0
vsize: 66668
[startup+780.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21482 0 3 0 77914 95 0 0 25 0 1 0 480556722 68268032 15557 4294967295 134512640 134672761 3221224576 3221223760 134615830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16667 15557 603 41 0 16626 0
vsize: 66668
[startup+790.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21482 0 3 0 78914 95 0 0 25 0 1 0 480556722 68268032 15557 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16667 15557 603 41 0 16626 0
vsize: 66668
[startup+800.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21483 0 3 0 79914 95 0 0 25 0 1 0 480556722 68268032 15558 4294967295 134512640 134672761 3221224576 3221223616 134612510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16667 15558 603 41 0 16626 0
vsize: 66668
[startup+810.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21483 0 3 0 80914 95 0 0 25 0 1 0 480556722 68268032 15558 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16667 15558 603 41 0 16626 0
vsize: 66668
[startup+820.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21483 0 3 0 81914 95 0 0 25 0 1 0 480556722 68268032 15558 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16667 15558 603 41 0 16626 0
vsize: 66668
[startup+830.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21484 0 3 0 82914 95 0 0 25 0 1 0 480556722 68268032 15559 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16667 15559 603 41 0 16626 0
vsize: 66668
[startup+840.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21484 0 3 0 83915 95 0 0 25 0 1 0 480556722 68268032 15559 4294967295 134512640 134672761 3221224576 3221223760 134615638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16667 15559 603 41 0 16626 0
vsize: 66668
[startup+850.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21484 0 3 0 84915 95 0 0 25 0 1 0 480556722 68268032 15559 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16667 15559 603 41 0 16626 0
vsize: 66668
[startup+860.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21484 0 3 0 85915 95 0 0 25 0 1 0 480556722 68268032 15559 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16667 15559 603 41 0 16626 0
vsize: 66668
[startup+870.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21484 0 3 0 86915 95 0 0 25 0 1 0 480556722 68268032 15559 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16667 15559 603 41 0 16626 0
vsize: 66668
[startup+880.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21484 0 3 0 87915 95 0 0 25 0 1 0 480556722 68268032 15559 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16667 15559 603 41 0 16626 0
vsize: 66668
[startup+890.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21484 0 3 0 88916 95 0 0 25 0 1 0 480556722 68268032 15559 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16667 15559 603 41 0 16626 0
vsize: 66668
[startup+900.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21485 0 3 0 89916 95 0 0 25 0 1 0 480556722 68268032 15560 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16667 15560 603 41 0 16626 0
vsize: 66668
[startup+910.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21485 0 3 0 90916 95 0 0 25 0 1 0 480556722 68268032 15560 4294967295 134512640 134672761 3221224576 3221223760 134615632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16667 15560 603 41 0 16626 0
vsize: 66668
[startup+920.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21489 0 3 0 91916 95 0 0 25 0 1 0 480556722 68268032 15564 4294967295 134512640 134672761 3221224576 3221223700 134566029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16667 15564 603 41 0 16626 0
vsize: 66668
[startup+930.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21593 0 3 0 92916 96 0 0 25 0 1 0 480556722 68792320 15668 4294967295 134512640 134672761 3221224576 3221223040 134645454 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16795 15668 603 41 0 16754 0
vsize: 67180
[startup+940.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21599 0 3 0 93916 96 0 0 25 0 1 0 480556722 68268032 15573 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16667 15573 603 41 0 16626 0
vsize: 66668
[startup+950.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21599 0 3 0 94916 96 0 0 25 0 1 0 480556722 68268032 15573 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16667 15573 603 41 0 16626 0
vsize: 66668
[startup+960.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21599 0 3 0 95917 96 0 0 25 0 1 0 480556722 68268032 15573 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16667 15573 603 41 0 16626 0
vsize: 66668
[startup+970.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21599 0 3 0 96917 96 0 0 25 0 1 0 480556722 68268032 15573 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16667 15573 603 41 0 16626 0
vsize: 66668
[startup+980.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21599 0 3 0 97917 96 0 0 25 0 1 0 480556722 68268032 15573 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16667 15573 603 41 0 16626 0
vsize: 66668
[startup+990.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21599 0 3 0 98917 96 0 0 25 0 1 0 480556722 68268032 15573 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16667 15573 603 41 0 16626 0
vsize: 66668
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21599 0 3 0 99917 96 0 0 25 0 1 0 480556722 68268032 15573 4294967295 134512640 134672761 3221224576 3221223760 134615632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16667 15573 603 41 0 16626 0
vsize: 66668
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21599 0 3 0 100917 96 0 0 25 0 1 0 480556722 68268032 15573 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16667 15573 603 41 0 16626 0
vsize: 66668
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21599 0 3 0 101918 96 0 0 25 0 1 0 480556722 68268032 15573 4294967295 134512640 134672761 3221224576 3221223776 134610675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16667 15573 603 41 0 16626 0
vsize: 66668
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21599 0 3 0 102918 96 0 0 25 0 1 0 480556722 68268032 15573 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16667 15573 603 41 0 16626 0
vsize: 66668
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21599 0 3 0 103918 96 0 0 25 0 1 0 480556722 68268032 15573 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16667 15573 603 41 0 16626 0
vsize: 66668
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21600 0 3 0 104918 96 0 0 25 0 1 0 480556722 68268032 15574 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16667 15574 603 41 0 16626 0
vsize: 66668
[startup+1060.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21600 0 3 0 105918 96 0 0 25 0 1 0 480556722 68268032 15574 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16667 15574 603 41 0 16626 0
vsize: 66668
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21600 0 3 0 106918 96 0 0 25 0 1 0 480556722 68268032 15574 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16667 15574 603 41 0 16626 0
vsize: 66668
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21600 0 3 0 107918 96 0 0 25 0 1 0 480556722 68268032 15574 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16667 15574 603 41 0 16626 0
vsize: 66668
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21600 0 3 0 108919 96 0 0 25 0 1 0 480556722 68268032 15574 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16667 15574 603 41 0 16626 0
vsize: 66668
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21600 0 3 0 109919 96 0 0 25 0 1 0 480556722 68268032 15574 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16667 15574 603 41 0 16626 0
vsize: 66668
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21600 0 3 0 110919 96 0 0 25 0 1 0 480556722 68268032 15574 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16667 15574 603 41 0 16626 0
vsize: 66668
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21600 0 3 0 111919 96 0 0 25 0 1 0 480556722 68268032 15574 4294967295 134512640 134672761 3221224576 3221223760 134615617 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16667 15574 603 41 0 16626 0
vsize: 66668
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21600 0 3 0 112919 96 0 0 25 0 1 0 480556722 68268032 15574 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16667 15574 603 41 0 16626 0
vsize: 66668
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21600 0 3 0 113919 96 0 0 25 0 1 0 480556722 68268032 15574 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16667 15574 603 41 0 16626 0
vsize: 66668
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21719 0 3 0 114919 97 0 0 25 0 1 0 480556722 68939776 15693 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16831 15693 603 41 0 16790 0
vsize: 67324
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 21905 0 3 0 115918 98 0 0 25 0 1 0 480556722 69595136 15879 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16991 15879 603 41 0 16950 0
vsize: 67964
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 22139 0 3 0 116918 98 0 0 25 0 1 0 480556722 70696960 16113 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17260 16113 603 41 0 17219 0
vsize: 69040
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 22370 0 3 0 117917 100 0 0 25 0 1 0 480556722 71622656 16344 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17486 16344 603 41 0 17445 0
vsize: 69944
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 22575 0 3 0 118916 100 0 0 25 0 1 0 480556722 72409088 16549 4294967295 134512640 134672761 3221224576 3221223760 134615535 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17678 16549 603 41 0 17637 0
vsize: 70712
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28796
Raw data (stat): 28796 (minisat+) R 28795 23176 23175 0 -1 0 22745 0 3 0 119916 101 0 0 25 0 1 0 480556722 73121792 16719 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17852 16719 603 41 0 17811 0
vsize: 71408
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 28796
Raw data (stat): 28796 (minisat+) Z 28795 23176 23175 0 -1 12 22747 0 3 0 119916 105 0 0 25 0 1 0 480556722 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: 10
Real time (s): 1200.1
CPU time (s): 1200.22
CPU user time (s): 1199.16
CPU system time (s): 1.05984
CPU usage (%): 100.01
Max. virtual memory (Kb): 71408
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####