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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. 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.
  4. 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

Nameweb/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-30:30:4.5:0.5:100.opb
MD5SUMbc393d4b1cc38ed414c3e21eb8bc6b60
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 109
Optimality of the best value was proved NO
Number of terms in the objective function 4447
Biggest coefficient in the objective function 2128
Number of bits for the biggest coefficient in the objective function 12
Sum of the numbers in the objective function 12580
Number of bits of the sum of numbers in the objective function 14
Biggest number in a constraint 2128
Number of bits of the biggest number in a constraint 12
Biggest sum of numbers in a constraint 12580
Number of bits of the biggest sum of numbers14
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1189.07
Number of variables4447
Total number of constraints9372
Number of constraints which are clauses4205
Number of constraints which are cardinality constraints (but not clauses)5167
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint27

Trace number 2361

Launcher Data

LAUNCH ON wulflinc9 THE 2005-09-18 19:11:57 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2741 boxname=wulflinc9 idbench=397 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  bc393d4b1cc38ed414c3e21eb8bc6b60  /oldhome/oroussel/tmp/wulflinc9/normalized-30:30:4.5:0.5:100.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc9/normalized-30:30:4.5:0.5:100.opb
IDLAUNCH: 2741
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        925780 kB
Buffers:         30612 kB
Cached:          52256 kB
SwapCached:       1044 kB
Active:          49476 kB
Inactive:        36124 kB
HighTotal:      131008 kB
HighFree:        75180 kB
LowTotal:       903652 kB
LowFree:        850600 kB
SwapTotal:     2097136 kB
SwapFree:      2095568 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5660 kB
Slab:            17660 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 19:32:08 (client local time) WITH STATUS 10 IN 1205.92 SECONDS
stats: 2741 7 1205.92 10

Solver Data

c Parsing PB file...
c Converting 4925 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[ 740]---> BDD-cost:   17
c ---[ 739]---> BDD-cost:   20
c ---[ 738]---> BDD-cost:   20
c ---[ 737]---> BDD-cost:   23
c ---[ 736]---> BDD-cost:   35
c ---[ 735]---> BDD-cost:   35
c ---[ 734]---> BDD-cost:   35
c ---[ 733]---> BDD-cost:   23
c ---[ 732]---> BDD-cost:   26
c ---[ 731]---> BDD-cost:   23
c ---[ 730]---> BDD-cost:   23
c ---[ 729]---> BDD-cost:   29
c ---[ 728]---> BDD-cost:   29
c ---[ 727]---> BDD-cost:   20
c ---[ 726]---> BDD-cost:   26
c ---[ 725]---> BDD-cost:   26
c ---[ 724]---> BDD-cost:   29
c ---[ 723]---> BDD-cost:   17
c ---[ 722]---> BDD-cost:   17
c ---[ 721]---> BDD-cost:   17
c ---[ 720]---> BDD-cost:    7
c ---[ 719]---> BDD-cost:    3
c ---[ 718]---> BDD-cost:    5
c ---[ 717]---> BDD-cost:    5
c ---[ 716]---> BDD-cost:    8
c ---[ 715]---> BDD-cost:    3
c ---[ 714]---> BDD-cost:   20
c ---[ 713]---> BDD-cost:   23
c ---[ 712]---> BDD-cost:   26
c ---[ 711]---> BDD-cost:   32
c ---[ 710]---> BDD-cost:   41
c ---[ 709]---> BDD-cost:   38
c ---[ 708]---> BDD-cost:   44
c ---[ 707]---> BDD-cost:   38
c ---[ 706]---> BDD-cost:   33
c ---[ 705]---> BDD-cost:   29
c ---[ 704]---> BDD-cost:   29
c ---[ 703]---> BDD-cost:   35
c ---[ 702]---> BDD-cost:   38
c ---[ 701]---> BDD-cost:   33
c ---[ 700]---> BDD-cost:   44
c ---[ 699]---> BDD-cost:   32
c ---[ 698]---> BDD-cost:   38
c ---[ 697]---> BDD-cost:   29
c ---[ 696]---> BDD-cost:   29
c ---[ 695]---> BDD-cost:   23
c ---[ 694]---> BDD-cost:   17
c ---[ 693]---> BDD-cost:   14
c ---[ 692]---> BDD-cost:    7
c ---[ 691]---> BDD-cost:   11
c ---[ 690]---> BDD-cost:   11
c ---[ 689]---> BDD-cost:   11
c ---[ 688]---> BDD-cost:    5
c ---[ 686]---> BDD-cost:   20
c ---[ 685]---> BDD-cost:   26
c ---[ 684]---> BDD-cost:   35
c ---[ 683]---> BDD-cost:   41
c ---[ 682]---> BDD-cost:   56
c ---[ 681]---> BDD-cost:   44
c ---[ 680]---> BDD-cost:   44
c ---[ 679]---> BDD-cost:   44
c ---[ 678]---> BDD-cost:   44
c ---[ 677]---> BDD-cost:   38
c ---[ 676]---> BDD-cost:   47
c ---[ 675]---> BDD-cost:   50
c ---[ 674]---> BDD-cost:   53
c ---[ 673]---> BDD-cost:   47
c ---[ 672]---> BDD-cost:   56
c ---[ 671]---> BDD-cost:   47
c ---[ 670]---> BDD-cost:   47
c ---[ 669]---> BDD-cost:   38
c ---[ 668]---> BDD-cost:   41
c ---[ 667]---> BDD-cost:   35
c ---[ 666]---> BDD-cost:   23
c ---[ 665]---> BDD-cost:   20
c ---[ 664]---> BDD-cost:   17
c ---[ 663]---> BDD-cost:   14
c ---[ 662]---> BDD-cost:   20
c ---[ 661]---> BDD-cost:   11
c ---[ 660]---> BDD-cost:   14
c ---[ 659]---> BDD-cost:   14
c ---[ 658]---> BDD-cost:    9
c ---[ 657]---> BDD-cost:    7
c ---[ 656]---> BDD-cost:   29
c ---[ 655]---> BDD-cost:   32
c ---[ 654]---> BDD-cost:   41
c ---[ 653]---> BDD-cost:   47
c ---[ 652]---> BDD-cost:   56
c ---[ 651]---> BDD-cost:   56
c ---[ 650]---> BDD-cost:   59
c ---[ 649]---> BDD-cost:   50
c ---[ 648]---> BDD-cost:   53
c ---[ 647]---> BDD-cost:   53
c ---[ 646]---> BDD-cost:   53
c ---[ 645]---> BDD-cost:   56
c ---[ 644]---> BDD-cost:   56
c ---[ 643]---> BDD-cost:   56
c ---[ 642]---> BDD-cost:   59
c ---[ 641]---> BDD-cost:   53
c ---[ 640]---> BDD-cost:   47
c ---[ 639]---> BDD-cost:   47
c ---[ 638]---> BDD-cost:   44
c ---[ 637]---> BDD-cost:   38
c ---[ 636]---> BDD-cost:   26
c ---[ 635]---> BDD-cost:   26
c ---[ 634]---> BDD-cost:   26
c ---[ 633]---> BDD-cost:   20
c ---[ 632]---> BDD-cost:   23
c ---[ 631]---> BDD-cost:   23
c ---[ 630]---> BDD-cost:   23
c ---[ 629]---> BDD-cost:   17
c ---[ 628]---> BDD-cost:   11
c ---[ 627]---> BDD-cost:   11
c ---[ 626]---> BDD-cost:   29
c ---[ 625]---> BDD-cost:   35
c ---[ 624]---> BDD-cost:   44
c ---[ 623]---> BDD-cost:   47
c ---[ 622]---> BDD-cost:   54
c ---[ 621]---> BDD-cost:   59
c ---[ 620]---> BDD-cost:   65
c ---[ 619]---> BDD-cost:   65
c ---[ 618]---> BDD-cost:   56
c ---[ 617]---> BDD-cost:   50
c ---[ 616]---> BDD-cost:   50
c ---[ 615]---> BDD-cost:   53
c ---[ 614]---> BDD-cost:   62
c ---[ 613]---> BDD-cost:   59
c ---[ 612]---> BDD-cost:   50
c ---[ 611]---> BDD-cost:   50
c ---[ 610]---> BDD-cost:   50
c ---[ 609]---> BDD-cost:   50
c ---[ 608]---> BDD-cost:   47
c ---[ 607]---> BDD-cost:   38
c ---[ 606]---> BDD-cost:   35
c ---[ 605]---> BDD-cost:   32
c ---[ 604]---> BDD-cost:   26
c ---[ 603]---> BDD-cost:   23
c ---[ 602]---> BDD-cost:   26
c ---[ 601]---> BDD-cost:   32
c ---[ 600]---> BDD-cost:   26
c ---[ 599]---> BDD-cost:   20
c ---[ 598]---> BDD-cost:   20
c ---[ 597]---> BDD-cost:   11
c ---[ 596]---> BDD-cost:   20
c ---[ 595]---> BDD-cost:   35
c ---[ 594]---> BDD-cost:   47
c ---[ 593]---> BDD-cost:   50
c ---[ 592]---> BDD-cost:   62
c ---[ 591]---> BDD-cost:   62
c ---[ 590]---> BDD-cost:   59
c ---[ 589]---> BDD-cost:   65
c ---[ 588]---> BDD-cost:   56
c ---[ 587]---> BDD-cost:   47
c ---[ 586]---> BDD-cost:   57
c ---[ 585]---> BDD-cost:   59
c ---[ 584]---> BDD-cost:   59
c ---[ 583]---> BDD-cost:   53
c ---[ 582]---> BDD-cost:   59
c ---[ 581]---> BDD-cost:   56
c ---[ 580]---> BDD-cost:   53
c ---[ 579]---> BDD-cost:   50
c ---[ 578]---> BDD-cost:   44
c ---[ 577]---> BDD-cost:   38
c ---[ 576]---> BDD-cost:   32
c ---[ 575]---> BDD-cost:   32
c ---[ 574]---> BDD-cost:   32
c ---[ 573]---> BDD-cost:   26
c ---[ 572]---> BDD-cost:   26
c ---[ 571]---> BDD-cost:   29
c ---[ 570]---> BDD-cost:   23
c ---[ 569]---> BDD-cost:   26
c ---[ 568]---> BDD-cost:   26
c ---[ 567]---> BDD-cost:   17
c ---[ 566]---> BDD-cost:   23
c ---[ 565]---> BDD-cost:   35
c ---[ 564]---> BDD-cost:   47
c ---[ 563]---> BDD-cost:   53
c ---[ 562]---> BDD-cost:   59
c ---[ 561]---> BDD-cost:   62
c ---[ 560]---> BDD-cost:   56
c ---[ 559]---> BDD-cost:   59
c ---[ 558]---> BDD-cost:   68
c ---[ 557]---> BDD-cost:   65
c ---[ 556]---> BDD-cost:   59
c ---[ 555]---> BDD-cost:   56
c ---[ 554]---> BDD-cost:   62
c ---[ 553]---> BDD-cost:   56
c ---[ 552]---> BDD-cost:   53
c ---[ 551]---> BDD-cost:   59
c ---[ 550]---> BDD-cost:   53
c ---[ 549]---> BDD-cost:   53
c ---[ 548]---> BDD-cost:   44
c ---[ 547]---> BDD-cost:   38
c ---[ 546]---> BDD-cost:   35
c ---[ 545]---> BDD-cost:   35
c ---[ 544]---> BDD-cost:   35
c ---[ 543]---> BDD-cost:   32
c ---[ 542]---> BDD-cost:   29
c ---[ 541]---> BDD-cost:   32
c ---[ 540]---> BDD-cost:   32
c ---[ 539]---> BDD-cost:   26
c ---[ 538]---> BDD-cost:   26
c ---[ 537]---> BDD-cost:   23
c ---[ 536]---> BDD-cost:   30
c ---[ 535]---> BDD-cost:   35
c ---[ 534]---> BDD-cost:   41
c ---[ 533]---> BDD-cost:   50
c ---[ 532]---> BDD-cost:   56
c ---[ 531]---> BDD-cost:   62
c ---[ 530]---> BDD-cost:   62
c ---[ 529]---> BDD-cost:   62
c ---[ 528]---> BDD-cost:   54
c ---[ 527]---> BDD-cost:   65
c ---[ 526]---> BDD-cost:   62
c ---[ 525]---> BDD-cost:   56
c ---[ 524]---> BDD-cost:   47
c ---[ 523]---> BDD-cost:   53
c ---[ 522]---> BDD-cost:   50
c ---[ 521]---> BDD-cost:   53
c ---[ 520]---> BDD-cost:   53
c ---[ 519]---> BDD-cost:   56
c ---[ 518]---> BDD-cost:   47
c ---[ 517]---> BDD-cost:   41
c ---[ 516]---> BDD-cost:   38
c ---[ 515]---> BDD-cost:   41
c ---[ 514]---> BDD-cost:   38
c ---[ 513]---> BDD-cost:   35
c ---[ 512]---> BDD-cost:   32
c ---[ 511]---> BDD-cost:   38
c ---[ 510]---> BDD-cost:   38
c ---[ 509]---> BDD-cost:   35
c ---[ 508]---> BDD-cost:   29
c ---[ 507]---> BDD-cost:   17
c ---[ 506]---> BDD-cost:   35
c ---[ 505]---> BDD-cost:   41
c ---[ 504]---> BDD-cost:   50
c ---[ 503]---> BDD-cost:   53
c ---[ 502]---> BDD-cost:   59
c ---[ 501]---> BDD-cost:   59
c ---[ 500]---> BDD-cost:   62
c ---[ 499]---> BDD-cost:   62
c ---[ 498]---> BDD-cost:   59
c ---[ 497]---> BDD-cost:   56
c ---[ 496]---> BDD-cost:   47
c ---[ 495]---> BDD-cost:   53
c ---[ 494]---> BDD-cost:   47
c ---[ 493]---> BDD-cost:   44
c ---[ 492]---> BDD-cost:   50
c ---[ 491]---> BDD-cost:   59
c ---[ 490]---> BDD-cost:   50
c ---[ 489]---> BDD-cost:   50
c ---[ 488]---> BDD-cost:   35
c ---[ 487]---> BDD-cost:   38
c ---[ 486]---> BDD-cost:   35
c ---[ 485]---> BDD-cost:   41
c ---[ 484]---> BDD-cost:   41
c ---[ 483]---> BDD-cost:   41
c ---[ 482]---> BDD-cost:   38
c ---[ 481]---> BDD-cost:   38
c ---[ 480]---> BDD-cost:   35
c ---[ 479]---> BDD-cost:   35
c ---[ 478]---> BDD-cost:   29
c ---[ 477]---> BDD-cost:   20
c ---[ 476]---> BDD-cost:   32
c ---[ 475]---> BDD-cost:   47
c ---[ 474]---> BDD-cost:   53
c ---[ 473]---> BDD-cost:   59
c ---[ 472]---> BDD-cost:   71
c ---[ 471]---> BDD-cost:   62
c ---[ 470]---> BDD-cost:   59
c ---[ 469]---> BDD-cost:   59
c ---[ 468]---> BDD-cost:   53
c ---[ 467]---> BDD-cost:   50
c ---[ 466]---> BDD-cost:   53
c ---[ 465]---> BDD-cost:   56
c ---[ 464]---> BDD-cost:   53
c ---[ 463]---> BDD-cost:   50
c ---[ 462]---> BDD-cost:   38
c ---[ 461]---> BDD-cost:   47
c ---[ 460]---> BDD-cost:   44
c ---[ 459]---> BDD-cost:   39
c ---[ 458]---> BDD-cost:   32
c ---[ 457]---> BDD-cost:   32
c ---[ 456]---> BDD-cost:   35
c ---[ 455]---> BDD-cost:   44
c ---[ 454]---> BDD-cost:   38
c ---[ 453]---> BDD-cost:   38
c ---[ 452]---> BDD-cost:   41
c ---[ 451]---> BDD-cost:   38
c ---[ 450]---> BDD-cost:   35
c ---[ 449]---> BDD-cost:   35
c ---[ 448]---> BDD-cost:   29
c ---[ 447]---> BDD-cost:   23
c ---[ 446]---> BDD-cost:   33
c ---[ 445]---> BDD-cost:   41
c ---[ 444]---> BDD-cost:   50
c ---[ 443]---> BDD-cost:   68
c ---[ 442]---> BDD-cost:   68
c ---[ 441]---> BDD-cost:   62
c ---[ 440]---> BDD-cost:   53
c ---[ 439]---> BDD-cost:   53
c ---[ 438]---> BDD-cost:   51
c ---[ 437]---> BDD-cost:   56
c ---[ 436]---> BDD-cost:   59
c ---[ 435]---> BDD-cost:   56
c ---[ 434]---> BDD-cost:   38
c ---[ 433]---> BDD-cost:   41
c ---[ 432]---> BDD-cost:   44
c ---[ 431]---> BDD-cost:   50
c ---[ 430]---> BDD-cost:   56
c ---[ 429]---> BDD-cost:   41
c ---[ 428]---> BDD-cost:   35
c ---[ 427]---> BDD-cost:   32
c ---[ 426]---> BDD-cost:   32
c ---[ 425]---> BDD-cost:   38
c ---[ 424]---> BDD-cost:   44
c ---[ 423]---> BDD-cost:   44
c ---[ 422]---> BDD-cost:   44
c ---[ 421]---> BDD-cost:   41
c ---[ 420]---> BDD-cost:   41
c ---[ 419]---> BDD-cost:   32
c ---[ 418]---> BDD-cost:   26
c ---[ 417]---> BDD-cost:   23
c ---[ 416]---> BDD-cost:   35
c ---[ 415]---> BDD-cost:   38
c ---[ 414]---> BDD-cost:   44
c ---[ 413]---> BDD-cost:   59
c ---[ 412]---> BDD-cost:   65
c ---[ 411]---> BDD-cost:   59
c ---[ 410]---> BDD-cost:   50
c ---[ 409]---> BDD-cost:   50
c ---[ 408]---> BDD-cost:   50
c ---[ 407]---> BDD-cost:   53
c ---[ 406]---> BDD-cost:   50
c ---[ 405]---> BDD-cost:   47
c ---[ 404]---> BDD-cost:   44
c ---[ 403]---> BDD-cost:   44
c ---[ 402]---> BDD-cost:   50
c ---[ 401]---> BDD-cost:   59
c ---[ 400]---> BDD-cost:   53
c ---[ 399]---> BDD-cost:   47
c ---[ 398]---> BDD-cost:   44
c ---[ 397]---> BDD-cost:   35
c ---[ 396]---> BDD-cost:   38
c ---[ 395]---> BDD-cost:   32
c ---[ 394]---> BDD-cost:   38
c ---[ 393]---> BDD-cost:   44
c ---[ 392]---> BDD-cost:   45
c ---[ 391]---> BDD-cost:   44
c ---[ 390]---> BDD-cost:   41
c ---[ 389]---> BDD-cost:   38
c ---[ 388]---> BDD-cost:   35
c ---[ 387]---> BDD-cost:   23
c ---[ 386]---> BDD-cost:   35
c ---[ 385]---> BDD-cost:   38
c ---[ 384]---> BDD-cost:   47
c ---[ 383]---> BDD-cost:   56
c ---[ 382]---> BDD-cost:   59
c ---[ 381]---> BDD-cost:   59
c ---[ 380]---> BDD-cost:   50
c ---[ 379]---> BDD-cost:   44
c ---[ 378]---> BDD-cost:   41
c ---[ 377]---> BDD-cost:   44
c ---[ 376]---> BDD-cost:   45
c ---[ 375]---> BDD-cost:   44
c ---[ 374]---> BDD-cost:   53
c ---[ 373]---> BDD-cost:   56
c ---[ 372]---> BDD-cost:   47
c ---[ 371]---> BDD-cost:   53
c ---[ 370]---> BDD-cost:   50
c ---[ 369]---> BDD-cost:   47
c ---[ 368]---> BDD-cost:   44
c ---[ 367]---> BDD-cost:   38
c ---[ 366]---> BDD-cost:   44
c ---[ 365]---> BDD-cost:   41
c ---[ 364]---> BDD-cost:   50
c ---[ 363]---> BDD-cost:   50
c ---[ 362]---> BDD-cost:   47
c ---[ 361]---> BDD-cost:   44
c ---[ 360]---> BDD-cost:   41
c ---[ 359]---> BDD-cost:   41
c ---[ 358]---> BDD-cost:   35
c ---[ 357]---> BDD-cost:   26
c ---[ 356]---> BDD-cost:   35
c ---[ 355]---> BDD-cost:   38
c ---[ 354]---> BDD-cost:   44
c ---[ 353]---> BDD-cost:   53
c ---[ 352]---> BDD-cost:   50
c ---[ 351]---> BDD-cost:   56
c ---[ 350]---> BDD-cost:   53
c ---[ 349]---> BDD-cost:   44
c ---[ 348]---> BDD-cost:   47
c ---[ 347]---> BDD-cost:   44
c ---[ 346]---> BDD-cost:   56
c ---[ 345]---> BDD-cost:   53
c ---[ 344]---> BDD-cost:   56
c ---[ 343]---> BDD-cost:   56
c ---[ 342]---> BDD-cost:   53
c ---[ 341]---> BDD-cost:   53
c ---[ 340]---> BDD-cost:   53
c ---[ 339]---> BDD-cost:   44
c ---[ 338]---> BDD-cost:   56
c ---[ 337]---> BDD-cost:   50
c ---[ 336]---> BDD-cost:   47
c ---[ 335]---> BDD-cost:   41
c ---[ 334]---> BDD-cost:   47
c ---[ 333]---> BDD-cost:   59
c ---[ 332]---> BDD-cost:   50
c ---[ 331]---> BDD-cost:   47
c ---[ 330]---> BDD-cost:   44
c ---[ 329]---> BDD-cost:   38
c ---[ 328]---> BDD-cost:   35
c ---[ 327]---> BDD-cost:   29
c ---[ 326]---> BDD-cost:   35
c ---[ 325]---> BDD-cost:   35
c ---[ 324]---> BDD-cost:   44
c ---[ 323]---> BDD-cost:   50
c ---[ 322]---> BDD-cost:   50
c ---[ 321]---> BDD-cost:   53
c ---[ 320]---> BDD-cost:   53
c ---[ 319]---> BDD-cost:   47
c ---[ 318]---> BDD-cost:   56
c ---[ 317]---> BDD-cost:   56
c ---[ 316]---> BDD-cost:   59
c ---[ 315]---> BDD-cost:   56
c ---[ 314]---> BDD-cost:   68
c ---[ 313]---> BDD-cost:   62
c ---[ 312]---> BDD-cost:   56
c ---[ 311]---> BDD-cost:   59
c ---[ 310]---> BDD-cost:   65
c ---[ 309]---> BDD-cost:   56
c ---[ 308]---> BDD-cost:   56
c ---[ 307]---> BDD-cost:   56
c ---[ 306]---> BDD-cost:   53
c ---[ 305]---> BDD-cost:   41
c ---[ 304]---> BDD-cost:   41
c ---[ 303]---> BDD-cost:   47
c ---[ 302]---> BDD-cost:   47
c ---[ 301]---> BDD-cost:   50
c ---[ 300]---> BDD-cost:   44
c ---[ 299]---> BDD-cost:   38
c ---[ 298]---> BDD-cost:   38
c ---[ 297]---> BDD-cost:   29
c ---[ 296]---> BDD-cost:   32
c ---[ 295]---> BDD-cost:   38
c ---[ 294]---> BDD-cost:   35
c ---[ 293]---> BDD-cost:   44
c ---[ 292]---> BDD-cost:   47
c ---[ 291]---> BDD-cost:   53
c ---[ 290]---> BDD-cost:   56
c ---[ 289]---> BDD-cost:   47
c ---[ 288]---> BDD-cost:   56
c ---[ 287]---> BDD-cost:   56
c ---[ 286]---> BDD-cost:   59
c ---[ 285]---> BDD-cost:   68
c ---[ 284]---> BDD-cost:   74
c ---[ 283]---> BDD-cost:   71
c ---[ 282]---> BDD-cost:   65
c ---[ 281]---> BDD-cost:   59
c ---[ 280]---> BDD-cost:   59
c ---[ 279]---> BDD-cost:   59
c ---[ 278]---> BDD-cost:   50
c ---[ 277]---> BDD-cost:   53
c ---[ 276]---> BDD-cost:   53
c ---[ 275]---> BDD-cost:   50
c ---[ 274]---> BDD-cost:   50
c ---[ 273]---> BDD-cost:   47
c ---[ 272]---> BDD-cost:   50
c ---[ 271]---> BDD-cost:   47
c ---[ 270]---> BDD-cost:   44
c ---[ 269]---> BDD-cost:   38
c ---[ 268]---> BDD-cost:   32
c ---[ 267]---> BDD-cost:   26
c ---[ 266]---> BDD-cost:   20
c ---[ 265]---> BDD-cost:   29
c ---[ 264]---> BDD-cost:   29
c ---[ 263]---> BDD-cost:   38
c ---[ 262]---> BDD-cost:   38
c ---[ 261]---> BDD-cost:   47
c ---[ 260]---> BDD-cost:   50
c ---[ 259]---> BDD-cost:   47
c ---[ 258]---> BDD-cost:   53
c ---[ 257]---> BDD-cost:   53
c ---[ 256]---> BDD-cost:   50
c ---[ 255]---> BDD-cost:   62
c ---[ 254]---> BDD-cost:   68
c ---[ 253]---> BDD-cost:   74
c ---[ 252]---> BDD-cost:   59
c ---[ 251]---> BDD-cost:   53
c ---[ 250]---> BDD-cost:   53
c ---[ 249]---> BDD-cost:   50
c ---[ 248]---> BDD-cost:   56
c ---[ 247]---> BDD-cost:   56
c ---[ 246]---> BDD-cost:   50
c ---[ 245]---> BDD-cost:   47
c ---[ 244]---> BDD-cost:   44
c ---[ 243]---> BDD-cost:   47
c ---[ 242]---> BDD-cost:   50
c ---[ 241]---> BDD-cost:   50
c ---[ 240]---> BDD-cost:   44
c ---[ 239]---> BDD-cost:   35
c ---[ 238]---> BDD-cost:   26
c ---[ 237]---> BDD-cost:   23
c ---[ 236]---> BDD-cost:   20
c ---[ 235]---> BDD-cost:   26
c ---[ 234]---> BDD-cost:   29
c ---[ 233]---> BDD-cost:   32
c ---[ 232]---> BDD-cost:   27
c ---[ 231]---> BDD-cost:   41
c ---[ 230]---> BDD-cost:   47
c ---[ 229]---> BDD-cost:   47
c ---[ 228]---> BDD-cost:   44
c ---[ 227]---> BDD-cost:   47
c ---[ 226]---> BDD-cost:   47
c ---[ 225]---> BDD-cost:   56
c ---[ 224]---> BDD-cost:   59
c ---[ 223]---> BDD-cost:   59
c ---[ 222]---> BDD-cost:   44
c ---[ 221]---> BDD-cost:   47
c ---[ 220]---> BDD-cost:   50
c ---[ 219]---> BDD-cost:   50
c ---[ 218]---> BDD-cost:   44
c ---[ 217]---> BDD-cost:   53
c ---[ 216]---> BDD-cost:   41
c ---[ 215]---> BDD-cost:   38
c ---[ 214]---> BDD-cost:   38
c ---[ 213]---> BDD-cost:   41
c ---[ 212]---> BDD-cost:   44
c ---[ 211]---> BDD-cost:   44
c ---[ 210]---> BDD-cost:   35
c ---[ 209]---> BDD-cost:   32
c ---[ 208]---> BDD-cost:   23
c ---[ 207]---> BDD-cost:   17
c ---[ 206]---> BDD-cost:   17
c ---[ 205]---> BDD-cost:   26
c ---[ 204]---> BDD-cost:   26
c ---[ 203]---> BDD-cost:   29
c ---[ 202]---> BDD-cost:   32
c ---[ 201]---> BDD-cost:   35
c ---[ 200]---> BDD-cost:   38
c ---[ 199]---> BDD-cost:   44
c ---[ 198]---> BDD-cost:   44
c ---[ 197]---> BDD-cost:   44
c ---[ 196]---> BDD-cost:   47
c ---[ 195]---> BDD-cost:   53
c ---[ 194]---> BDD-cost:   50
c ---[ 193]---> BDD-cost:   47
c ---[ 192]---> BDD-cost:   38
c ---[ 191]---> BDD-cost:   38
c ---[ 190]---> BDD-cost:   41
c ---[ 189]---> BDD-cost:   47
c ---[ 188]---> BDD-cost:   35
c ---[ 187]---> BDD-cost:   35
c ---[ 186]---> BDD-cost:   30
c ---[ 185]---> BDD-cost:   35
c ---[ 184]---> BDD-cost:   32
c ---[ 183]---> BDD-cost:   32
c ---[ 182]---> BDD-cost:   35
c ---[ 181]---> BDD-cost:   35
c ---[ 180]---> BDD-cost:   23
c ---[ 179]---> BDD-cost:   26
c ---[ 178]---> BDD-cost:   17
c ---[ 177]---> BDD-cost:   14
c ---[ 176]---> BDD-cost:    7
c ---[ 175]---> BDD-cost:   20
c ---[ 174]---> BDD-cost:   20
c ---[ 173]---> BDD-cost:   26
c ---[ 172]---> BDD-cost:   26
c ---[ 171]---> BDD-cost:   29
c ---[ 170]---> BDD-cost:   26
c ---[ 169]---> BDD-cost:   38
c ---[ 168]---> BDD-cost:   38
c ---[ 167]---> BDD-cost:   44
c ---[ 166]---> BDD-cost:   41
c ---[ 165]---> BDD-cost:   47
c ---[ 164]---> BDD-cost:   44
c ---[ 163]---> BDD-cost:   38
c ---[ 162]---> BDD-cost:   32
c ---[ 161]---> BDD-cost:   35
c ---[ 160]---> BDD-cost:   32
c ---[ 159]---> BDD-cost:   32
c ---[ 158]---> BDD-cost:   26
c ---[ 157]---> BDD-cost:   32
c ---[ 156]---> BDD-cost:   29
c ---[ 155]---> BDD-cost:   29
c ---[ 154]---> BDD-cost:   26
c ---[ 153]---> BDD-cost:   26
c ---[ 152]---> BDD-cost:   23
c ---[ 151]---> BDD-cost:   23
c ---[ 150]---> BDD-cost:   20
c ---[ 149]---> BDD-cost:   17
c ---[ 148]---> BDD-cost:   11
c ---[ 147]---> BDD-cost:   12
c ---[ 146]---> BDD-cost:    7
c ---[ 145]---> BDD-cost:   11
c ---[ 144]---> BDD-cost:    9
c ---[ 143]---> BDD-cost:   14
c ---[ 142]---> BDD-cost:   11
c ---[ 141]---> BDD-cost:   23
c ---[ 140]---> BDD-cost:   17
c ---[ 139]---> BDD-cost:   26
c ---[ 138]---> BDD-cost:   21
c ---[ 137]---> BDD-cost:   35
c ---[ 136]---> BDD-cost:   26
c ---[ 135]---> BDD-cost:   35
c ---[ 134]---> BDD-cost:   29
c ---[ 133]---> BDD-cost:   32
c ---[ 132]---> BDD-cost:   23
c ---[ 131]---> BDD-cost:   29
c ---[ 130]---> BDD-cost:   29
c ---[ 129]---> BDD-cost:   15
c ---[ 128]---> BDD-cost:    9
c ---[ 127]---> BDD-cost:   20
c ---[ 126]---> BDD-cost:   11
c ---[ 125]---> BDD-cost:   23
c ---[ 124]---> BDD-cost:   20
c ---[ 123]---> BDD-cost:   20
c ---[ 122]---> BDD-cost:   20
c ---[ 121]---> BDD-cost:   23
c ---[ 120]---> BDD-cost:   14
c ---[ 119]---> BDD-cost:   11
c ---[ 118]---> BDD-cost:    9
c ---[ 117]---> BDD-cost:   11
c ---[ 116]---> BDD-cost:    3
c ---[ 113]---> BDD-cost:    7
c ---[ 112]---> BDD-cost:   11
c ---[ 111]---> BDD-cost:    9
c ---[ 110]---> BDD-cost:    5
c ---[ 109]---> BDD-cost:   17
c ---[ 108]---> BDD-cost:   13
c ---[ 107]---> BDD-cost:   29
c ---[ 106]---> BDD-cost:   23
c ---[ 105]---> BDD-cost:   20
c ---[ 104]---> BDD-cost:   17
c ---[ 103]---> BDD-cost:   17
c ---[ 102]---> BDD-cost:   17
c ---[ 101]---> BDD-cost:   20
c ---[ 100]---> BDD-cost:   11
c ---[  99]---> BDD-cost:   11
c ---[  98]---> BDD-cost:    7
c ---[  97]---> BDD-cost:    9
c ---[  96]---> BDD-cost:   17
c ---[  95]---> BDD-cost:   17
c ---[  94]---> BDD-cost:   14
c ---[  93]---> BDD-cost:   17
c ---[  92]---> BDD-cost:   11
c ---[  91]---> BDD-cost:   11
c ---[  90]---> BDD-cost:    5
c ---[  89]---> BDD-cost:    7
c ---[  87]---> BDD-cost:    8
c ---[  81]---> BDD-cost:   14
c ---[  80]---> BDD-cost:   14
c ---[  79]---> BDD-cost:   20
c ---[  78]---> BDD-cost:   11
c ---[  77]---> BDD-cost:   11
c ---[  76]---> BDD-cost:    8
c ---[  75]---> BDD-cost:    8
c ---[  74]---> BDD-cost:    9
c ---[  73]---> BDD-cost:    3
c ---[  72]---> BDD-cost:   11
c ---[  71]---> BDD-cost:   11
c ---[  70]---> BDD-cost:   14
c ---[  69]---> BDD-cost:   11
c ---[  68]---> BDD-cost:   11
c ---[  67]---> BDD-cost:    5
c ---[  66]---> BDD-cost:    5
c ---[  64]---> BDD-cost:    5
c ---[  63]---> BDD-cost:   11
c ---[  62]---> BDD-cost:    8
c ---[  61]---> BDD-cost:   11
c ---[  60]---> BDD-cost:    5
c ---[  59]---> BDD-cost:    3
c ---[  58]---> BDD-cost:    5
c ---[  57]---> BDD-cost:    8
c ---[  56]---> BDD-cost:   11
c ---[  55]---> BDD-cost:    8
c ---[  54]---> BDD-cost:   11
c ---[  53]---> BDD-cost:    5
c ---[  52]---> BDD-cost:    6
c ---[  51]---> BDD-cost:    8
c ---[  50]---> BDD-cost:    8
c ---[  49]---> BDD-cost:    8
c ---[  47]---> BDD-cost:    5
c ---[  46]---> BDD-cost:    3
c ---[  45]---> BDD-cost:    5
c ---[  44]---> BDD-cost:    8
c ---[  43]---> BDD-cost:    3
c ---[  42]---> BDD-cost:    7
c ---[  41]---> BDD-cost:    7
c ---[  40]---> BDD-cost:    7
c ---[  39]---> BDD-cost:    8
c ---[  38]---> BDD-cost:    8
c ---[  37]---> BDD-cost:    9
c ---[  36]---> BDD-cost:   17
c ---[  35]---> BDD-cost:   11
c ---[  34]---> BDD-cost:    5
c ---[  32]---> BDD-cost:    3
c ---[  29]---> BDD-cost:    5
c ---[  28]---> BDD-cost:    7
c ---[  27]---> BDD-cost:    8
c ---[  26]---> BDD-cost:    8
c ---[  25]---> BDD-cost:    8
c ---[  24]---> BDD-cost:   11
c ---[  23]---> BDD-cost:   14
c ---[  22]---> BDD-cost:   11
c ---[  21]---> BDD-cost:    5
c ---[  19]---> BDD-cost:    5
c ---[  18]---> BDD-cost:    3
c ---[  17]---> BDD-cost:    8
c ---[  16]---> BDD-cost:    5
c ---[  15]---> BDD-cost:   11
c ---[  14]---> BDD-cost:    8
c ---[  13]---> BDD-cost:    5
c ---[  12]---> BDD-cost:    5
c ---[   8]---> BDD-cost:    3
c ---[   7]---> BDD-cost:    5
c ---[   6]---> BDD-cost:    5
c ---[   5]---> BDD-cost:    5
c ---[   4]---> BDD-cost:    3
c ---[   1]---> BDD-cost:    3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   64290   185949 |   21430       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 5115
c ---[   0]---> Adder-cost: 10943   maxlim: 3209   bits: 13/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  140811   459221 |   46937       0        0     nan |  0.000 % |
c |       100 |  140811   459221 |   51630     100      307     3.1 |  1.755 % |
c |       250 |  140811   459221 |   56793     250      766     3.1 |  1.755 % |
c |       475 |  140811   459221 |   62473     475     1519     3.2 |  1.755 % |
c |       812 |  140811   459221 |   68720     812     2725     3.4 |  1.755 % |
c |      1318 |  140811   459221 |   75592    1318     4688     3.6 |  1.755 % |
c |      2077 |  140811   459221 |   83151    2077     7909     3.8 |  1.755 % |
c |      3216 |  140811   459221 |   91466    3216    13570     4.2 |  1.755 % |
c |      4924 |  140811   459221 |  100613    4924    23280     4.7 |  1.755 % |
c |      7486 |  140811   459221 |  110674    7486    42255     5.6 |  1.755 % |
c |     11332 |  140787   459139 |  121742   11326    94091     8.3 |  1.762 % |
c |     17098 |  140787   459139 |  133916   17092   143507     8.4 |  1.762 % |
c |     25747 |  140778   459108 |  147308   25738   249385     9.7 |  1.765 % |
c |     38722 |  140778   459108 |  162039   38713   411021    10.6 |  1.765 % |
c ==============================================================================
c Found solution: 833
c ---[   0]---> Adder-cost: 2   maxlim: 7491   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43718 |  140802   459205 |   46934   43709   467857    10.7 |  1.765 % |
c |     43818 |  140802   459205 |   51627   43809   468951    10.7 |  1.779 % |
c |     43968 |  140802   459205 |   56790   43959   470502    10.7 |  1.779 % |
c |     44193 |  140802   459205 |   62469   44184   472927    10.7 |  1.779 % |
c ==============================================================================
c Found solution: 735
c ---[   0]---> Adder-cost: 0   maxlim: 7589   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     44502 |  140813   459274 |   46937   44493   475890    10.7 |  1.779 % |
c |     44602 |  140813   459274 |   51630   44593   476830    10.7 |  1.788 % |
c |     44752 |  140813   459274 |   56793   44743   478473    10.7 |  1.788 % |
c |     44977 |  140813   459274 |   62473   44968   480280    10.7 |  1.788 % |
c |     45314 |  140813   459274 |   68720   45305   509303    11.2 |  1.788 % |
c |     45820 |  140813   459274 |   75592   45811   512224    11.2 |  1.788 % |
c |     46580 |  140813   459274 |   83151   46571   520257    11.2 |  1.788 % |
c |     47720 |  140813   459274 |   91466   47711   546703    11.5 |  1.788 % |
c |     49429 |  140813   459274 |  100613   49420   571647    11.6 |  1.788 % |
c |     51994 |  140813   459274 |  110674   51985   632450    12.2 |  1.788 % |
c |     55841 |  140813   459274 |  121742   55832   697929    12.5 |  1.788 % |
c |     61607 |  140813   459274 |  133916   61598   848408    13.8 |  1.788 % |
c |     70256 |  140813   459274 |  147308   70247  1212781    17.3 |  1.788 % |
c |     83231 |  140813   459274 |  162039   83222  2850891    34.3 |  1.788 % |
c |    102692 |  140813   459274 |  178243  102683  4504414    43.9 |  1.788 % |
c |    131886 |  140813   459274 |  196067  131877  6212888    47.1 |  1.788 % |
c |    175675 |  140813   459274 |  215674  175666  9393274    53.5 |  1.788 % |
c |    241359 |  140813   459274 |  237241   37049  7718710   208.3 |  1.788 % |
c |    339888 |  140806   459254 |  260965  135576 14388083   106.1 |  1.791 % |
c |    487677 |  140806   459254 |  287062   38634  3511754    90.9 |  1.791 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v v3896 -v3446 -v3326 -v3226 v3142 v1870 -v192 -v170 -v3447 v3330 -v1960 v1871 v3895 v3451 v3329 -v3227 -v3146 -v1959 -v191 -v169 v3450 v3331 -v3228 -v3144 -v1961 v1477 -v1436 -v195 -v172 -v3901 v3448 v3335 -v3231 -v2283 v1962 -v1851 -v1690 v1476 -v1435 -v217 -v3899 v3449 v3334 -v3229 -v3145 v2287 v1963 -v1689 v1482 -v1437 -v196 -v173 v3332 -v3230 v3149 -v2082 v1970 -v1850 -v1691 v1481 -v1438 -v216 v175 -v3900 v3333 v2440 v1964 -v1694 -v1483 v1439 -v220 v176 v4136 -v3904 v3755 v2439 v1965 -v1856 -v1693 -v1487 v1446 -v1403 v4135 -v2445 v1966 -v1854 v1830 -v1698 -v1486 v1440 -v221 v4137 -v3758 -v3556 v2444 v1829 -v1697 -v1484 v1441 -v4333 v4140 -v3759 -v3560 -v2576 v2446 -v1855 v1831 -v1695 -v1485 -v1442 -v577 -v4332 v4139 -v3730 -v3484 -v2575 v2450 -v1859 v1832 -v1696 -v576 v4338 v4144 -v3483 v2449 v1833 -v578 -v242 v4337 v4143 -v3733 -v3485 -v2577 v2447 -v2395 v1840 -v1570 -v579 -v241 -v4339 v4141 -v3734 -v3488 v2579 -v2448 -v1834 -v1574 v580 v4343 -v4142 v3487 -v2394 -v2378 -v1835 -v973 v587 -v243 v4342 -v3492 -v2580 v2398 -v2377 -v1836 v581 -v245 v4340 -v3999 -v3491 -v2582 -v2379 v582 -v4341 -v3775 -v3489 -v2583 v2399 v4438 v583 -v246 -v3774 -v3490 v1199 v248 v4439 -v4440 v249 v3781 v4441 -v2358 -v2202 v3780 -v2942 v2362 v3778 v2941 -v2201 -v1089 v3779 -v3891 -v3445 -v3223 v3141 -v2722 v1872 v166 v3444 -v3325 -v3225 -v2726 v3897 v3455 -v3327 -v3224 -v3147 -v193 -v171 v3328 -v3232 -v197 v174 -v3902 v3339 v3150 -v2282 -v2078 -v1973 -v1876 -v1846 v178 v3148 v2286 v1974 v1478 v177 v3905 -v2081 v1969 -v1897 -v1852 v1479 -v1449 -v1399 -v218 -v199 v3903 -v1692 v1480 -v1450 -v222 -v200 v3754 -v1967 -v1857 -v1706 -v1491 v1445 v1402 v2441 -v1702 -v3760 -v3555 v2442 -v1860 -v1701 v1443 -v224 v4138 -v3559 -v2571 v2443 -v1858 -v225 v4152 -v3729 -v3375 -v2570 v2454 -v2182 v1843 v4334 -v4148 -v3379 v1844 -v237 v4335 -v4147 -v3800 -v3763 -v3735 -v2578 v1839 -v1569 -v1042 -v969 v590 v236 v4336 -v3486 v2581 -v1573 v1046 v591 v4347 v3995 v3500 -v2585 -v2396 v1837 -v1378 -v972 v586 -v244 v3496 -v2584 v2400 v247 -v3998 -v3738 v3495 -v1195 -v584 v251 -v2380 v250 -v4020 v2402 v2388 v1198 v4024 -v3776 -v2403 v2384 -v3777 v2383 v3785 -v2465 -v2357 -v2198 v1092 v2938 -v2469 v2361 v1093 v2937 -v2203 -v1088 -v3289 -v1086 -v3293 v3458 v3139 -v2721 v1873 -v188 -v3890 v3459 -v3222 v3143 -v2725 v165 -v4092 -v4047 -v3892 v3454 -v3342 -v3240 v3140 -v1972 -v1877 -v194 v167 -v4096 v3898 -v3343 -v3236 v3151 -v1971 -v1875 -v212 -v198 v168 v3894 -v3452 -v3354 v3338 -v3235 -v2284 -v2077 -v1893 -v1448 -v211 -v202 v182 v3906 v2288 -v1845 -v1447 -v201 -v3750 -v3336 -v2083 -v1896 -v1847 -v1703 -v1494 -v1398 -v219 v1853 -v1705 v1495 -v223 v3756 -v2290 -v2010 -v1968 v1849 -v1490 v1404 -v1170 -v227 -v2291 -v1861 -v1174 -v226 -v4149 -v3761 -v3725 -v3684 v3557 -v2457 -v2178 -v2086 -v1842 -v1699 -v1488 v1444 -v49 v4151 v3561 -v2458 -v1841 -v53 -v3796 v3764 -v3731 -v3374 v2453 -v2181 -v1700 -v1407 -v589 -v3762 -v3378 -v2572 -v2390 -v588 -v4350 -v4145 -v3799 -v3736 -v3563 -v3497 -v2573 -v2451 -v2389 -v1571 -v1374 v1124 -v1041 -v968 -v4351 -v3564 -v3499 v2574 v1575 v1045 v238 -v4346 -v4146 v3994 -v3739 v2589 -v2397 v1838 -v1377 -v974 v239 -v3737 v2401 v240 -v4344 -v4000 -v3493 -v3425 v2405 -v2385 -v1577 -v1194 -v585 v255 -v3429 v2404 v2387 -v1578 -v4019 -v3494 v1200 v977 v4023 -v4003 v3788 v2381 -v1091 v3789 -v1090 v3784 -v2464 v2382 -v2359 -v1203 -v873 -v2468 v2363 -v2197 -v3782 v2199 v2939 v2204 -v3288 v2940 v2795 -v2365 -v1087 v3292 -v2799 -v2366 v4442 -v4043 v3456 -v3341 -v3237 -v2723 v1874 -v71 -v3340 -v3239 v3138 -v2727 -v2278 v1878 -v187 v75 -v4091 -v4046 -v3350 v3159 -v2277 -v2073 -v189 v185 -v4095 -v3893 v3155 -v190 v186 -v3914 -v3453 -v3353 -v3233 v3154 -v2729 -v2490 -v2285 v2079 -v1892 -v1493 v1394 -v206 v181 v3910 -v2730 -v2494 v2289 -v1704 -v1492 -v213 v3909 -v3337 -v3234 -v2293 -v2084 -v2006 -v1898 v1400 -v214 v179 -v3749 -v3551 -v2292 -v1848 -v215 -v3751 -v3680 v3550 -v2456 -v2308 -v2087 -v2009 v1869 v1405 -v1169 -v511 -v231 -v4150 v3757 -v2455 -v2312 -v2085 v1865 -v1173 v3753 -v3683 v3558 -v2177 v1901 -v1864 -v1489 -v1408 -v48 v3765 -v3724 v3562 v1565 -v1406 -v52 -v4349 -v3795 -v3726 v3566 -v3376 -v2183 v1564 v1120 -v964 -v4348 -v3732 v3565 -v3498 v3380 -v3990 v3801 v3728 -v2592 -v2452 -v1572 -v1373 v1123 -v1043 -v970 -v3740 -v2593 -v2391 v1576 v1047 v3996 v3382 v2588 -v2392 -v2186 -v1580 -v1379 -v1190 v975 v258 v3383 v2393 -v2386 -v1579 v259 -v4345 -v4001 -v3804 -v3424 v2586 -v2409 -v1674 -v1196 -v1049 v978 v254 -v3428 -v1050 v976 v4021 -v4004 -v3787 v2539 -v1382 v1201 v252 v4025 -v4002 -v3786 -v2543 -v2353 -v2352 v1204 -v994 -v869 -v1202 v998 -v4027 v2466 -v2360 -v872 v333 -v4028 v2470 v2364 -v337 -v3783 -v2368 -v2367 v2200 -v3290 v2945 v2794 -v2472 v2212 v3294 v2946 -v2798 -v2473 v2208 v4042 v3457 -v3238 v3156 -v2724 v1886 -v184 -v70 v3158 -v2728 -v1882 -v183 v74 -v4093 v4048 -v3911 -v3349 -v2732 -v1888 -v1881 -v209 -v4097 -v3913 -v2731 -v2279 -v2072 -v210 -v3355 -v3152 -v2489 -v2280 -v2074 -v1894 -v673 -v205 -v2493 v2281 v2080 v1393 -v677 v4099 v4051 v3907 -v3153 -v2297 v2076 -v2005 -v1899 -v1866 -v1461 v1395 -v507 -v234 -v203 -v180 -v146 v4100 -v2088 -v1868 v1401 -v235 -v150 v3908 -v3679 -v3358 -v2307 -v2173 -v2011 v1902 v1397 -v1171 -v510 -v230 v3752 v3552 -v3370 -v2311 v1900 -v1409 -v1175 -v3791 v3773 -v3685 v3553 -v3369 -v2179 -v1862 -v228 -v50 v3769 v3554 v1037 -v54 -v4307 -v3797 v3768 -v3705 -v3570 -v3377 -v2591 -v2184 -v2014 -v1863 -v1369 v1177 v1119 v1036 -v3727 -v3709 v3381 -v2590 v1566 v1178 -v963 v3802 -v3748 -v3688 v3385 -v2187 v1567 v1375 v1125 -v1044 -v965 -v257 -v56 -v3989 -v3744 v3384 -v2185 v1568 v1048 -v971 -v256 -v57 -v3991 -v3805 -v3743 v2412 -v1670 -v1645 -v1584 -v1380 -v1052 v967 -v4015 v3997 -v3803 v2413 -v1649 -v1189 -v1051 v979 -v4014 v3993 -v3426 -v2587 -v2408 -v1673 -v1383 -v1270 -v1191 -v1128 -v4005 -v3430 -v1381 -v1274 -v1197 v4022 v2538 -v2406 v1193 v253 v4026 -v2542 -v2460 v1205 v4030 -v3432 -v2459 -v993 v868 -v4029 -v3433 v2354 v997 v2467 v2355 -v874 -v408 v332 -v3284 v2471 v2356 -v412 -v336 -v3283 -v2944 v2475 v2372 v2209 -v1019 v2943 v2474 v2211 -v1023 -v3291 v2796 -v877 v3295 -v2800 v2207 -v4088 v4044 -v3345 v3157 -v2720 v1885 -v286 -v208 -v72 -v3912 v2719 -v207 v76 -v4094 v4049 -v3351 v2736 -v1879 -v725 -v457 v4098 -v1887 -v461 v4102 v4052 -v3356 -v2491 v2300 -v2001 -v1889 -v1880 v1457 -v825 -v672 -v233 -v78 v4101 v4050 -v2495 v2301 -v2075 v1895 -v1867 -v1165 -v676 -v232 -v79 -v4068 -v3675 -v3359 -v2296 v2096 -v2007 v1891 -v1460 -v1164 -v506 -v204 v145 v4072 -v3357 -v2092 v1903 v1396 -v149 -v44 v3770 -v3681 -v2497 -v2309 -v2294 -v2091 -v2012 v1417 v1172 -v512 -v43 v3772 -v2498 -v2313 -v2172 -v1413 v1176 -v4303 -v3686 -v3573 -v2174 -v2031 -v2015 -v1412 v1180 -v1115 -v229 -v51 -v3790 -v3574 -v3371 -v2180 -v2035 -v2013 v1179 -v55 -v4306 v3792 -v3766 -v3745 -v3704 -v3689 -v3569 -v3372 -v2315 v2176 v1121 -v1067 -v515 -v59 v3798 -v3747 -v3708 -v3687 v3373 -v2316 -v2188 -v1368 -v1071 v1038 -v58 v3794 -v3767 -v3567 -v3389 -v2411 -v1587 -v1370 v1126 v1039 -v121 -v3806 -v3420 -v2410 -v1588 v1376 v1040 -v966 -v125 -v3741 -v3419 -v1669 -v1644 -v1583 v1372 v1129 v1056 -v987 -v3992 -v1648 -v1384 -v1127 -v983 -v4013 -v3742 -v3427 v1675 -v1581 -v1269 -v982 v4016 -v4009 -v3431 -v1273 -v1192 v4017 -v4008 v3435 v2540 -v2407 -v1213 -v864 v4018 v3434 -v2544 v1209 v4034 -v1678 v1208 -v995 v870 -v2461 v999 -v3964 -v2546 -v2462 v2375 v875 -v407 v334 -v2790 -v2547 v2463 v2376 v2210 -v411 -v338 -v2789 v2479 v2371 -v1018 -v1001 -v878 -v3285 -v1022 -v1002 -v876 v3286 v2797 v2369 -v1311 v340 v3287 -v2801 -v2205 v341 v4040 v3242 v2739 -v1883 -v721 -v285 -v73 v4087 v4045 -v3344 v2740 v2485 v77 v4089 v4041 -v3346 v2735 v2484 v2299 -v821 -v724 -v456 -v81 v4090 v4053 -v3352 v2298 -v460 -v80 -v4106 -v3825 -v3348 v2733 -v2492 -v2093 v1456 -v824 -v674 -v502 -v3360 -v2496 -v2303 v2095 -v2000 -v1890 -v678 -v4067 -v3074 -v2500 -v2302 -v2002 -v1911 -v1462 -v1414 -v508 v147 v4071 v3771 -v3674 -v3078 -v2499 -v2008 v1907 -v1416 v1166 -v151 -v3676 -v3572 -v3123 -v2310 -v2295 -v2089 v2004 v1906 v1167 -v680 -v513 v3682 -v3571 -v2314 -v2016 v1168 -v681 -v45 -v4302 v3678 -v2318 -v2090 -v2030 -v1465 -v1410 -v1184 -v516 -v153 -v46 -v3746 -v3690 -v2317 -v2175 -v2034 -v1114 -v514 -v154 -v47 -v4308 -v3706 v3392 v2196 -v1586 -v1411 -v1116 -v1066 -v63 v3793 -v3710 v3393 -v2192 -v1585 v1122 -v1070 v3814 -v3568 -v3388 -v2191 -v1665 v1118 v1059 -v984 -v120 v3810 -v1371 v1130 v1060 -v986 -v124 -v4311 -v4010 -v3809 v3712 -v3386 -v1671 -v1646 v1392 -v1055 -v4012 -v3713 -v3421 v2534 -v1650 v1388 -v3422 v2533 v1676 -v1582 v1387 v1271 -v1210 -v1053 -v980 -v698 v3423 -v1275 -v1212 v989 -v702 v4037 -v4006 -v3439 v2541 -v1679 -v1652 v988 -v981 -v387 v4038 -v2545 -v1677 -v1653 -v863 -v328 v4033 -v4007 -v3960 -v2549 v2374 v1277 v1206 -v996 -v865 -v327 -v2548 v2373 v1278 v1000 v871 v4031 -v3963 -v2812 v2482 -v1207 -v1004 v867 -v409 v335 v2816 v2483 -v1003 -v879 -v413 -v339 -v3660 v2478 -v1307 -v1020 v343 -v2791 -v1024 v342 v3298 -v2792 v2476 v2370 -v1333 -v1310 v415 v3299 v2793 -v2206 v416 v3241 v2737 -v1884 -v1541 -v1419 -v720 -v287 -v69 v4039 -v1545 -v668 v68 -v4109 -v4061 -v3821 -v1452 -v820 -v726 -v667 -v458 -v85 -v4110 v4057 -v3347 v2486 -v2094 -v462 -v141 -v4105 v4056 -v3824 -v3368 v2734 v2487 -v1908 v1458 -v826 -v675 -v291 -v140 -v3364 v2488 -v1910 -v1415 -v679 -v501 -v4103 v4069 -v3363 -v3119 -v3073 -v2504 -v1463 -v729 -v683 -v503 -v464 v148 v4073 -v3077 -v2304 -v2003 -v682 -v509 -v465 -v152 -v4298 -v3122 -v2305 -v2024 -v1904 v1466 v1187 -v829 -v505 -v156 -v3700 -v3677 -v2306 v2020 -v1464 v1188 -v517 -v155 v4304 -v4075 -v3699 v3698 v3391 -v2322 -v2193 -v2032 v2019 -v1905 -v1183 -v66 -v4076 v3694 v3390 v2195 v2036 -v67 -v4309 -v3811 -v3707 -v3693 -v1181 -v1068 v1058 -v62 v3813 -v3711 -v1640 -v1117 -v1072 v1057 -v985 v4312 v3715 -v2189 -v2038 v1742 -v1639 -v1389 -v1138 -v122 -v60 -v4310 -v4011 v3714 -v2039 -v1664 v1391 -v1265 -v1134 -v126 -v3807 -v3387 -v2190 -v1666 -v1647 v1599 -v1264 -v1133 v1074 -v746 -v1672 -v1651 -v1211 -v1075 -v750 v4036 -v3808 -v3442 v1668 -v1655 v1385 v1272 -v1145 -v1054 -v697 -v383 -v128 v4035 -v3443 v2535 -v1680 -v1654 -v1276 -v1149 -v701 -v129 -v3438 v2536 v1386 v1280 -v386 v2537 v1279 v990 v403 -v3959 -v3436 -v2553 v2481 v991 v402 v2480 -v1014 v992 -v866 -v329 v4032 -v3965 -v3656 -v2811 -v1013 -v1008 -v887 -v410 -v330 v2815 -v883 -v414 v331 -v3659 -v3297 -v3029 -v1329 -v1306 -v1021 -v882 v418 -v347 -v3296 -v1025 v417 -v3968 v2804 -v2477 -v1332 -v1312 -v1026 v2805 -v1027 -v4108 -v4058 v3243 v2738 -v1915 v1540 -v1418 -v816 -v722 -v453 -v288 -v88 -v4107 -v4060 -v1919 -v1544 -v89 -v4116 -v3820 -v3365 -v1790 -v822 -v727 -v459 -v292 -v84 -v4120 v4063 -v3367 -v1909 -v1451 -v669 -v463 -v290 v4062 v4054 -v3826 -v3247 v2507 -v1453 -v827 v730 -v670 v467 -v82 v2508 v1459 -v728 -v671 v466 v142 -v4104 v4070 v4055 -v3361 -v3118 -v3075 -v2976 -v2503 -v2021 v1455 -v1186 -v830 -v800 -v687 v143 v4074 -v3079 -v2980 -v2026 -v2023 v1467 -v1185 -v828 -v504 v144 v4078 -v3829 -v3695 -v3362 v3124 -v2501 -v2325 -v2025 -v648 -v525 -v160 -v65 -v4297 v4077 v3697 -v2326 -v2194 -v1062 -v652 -v521 -v64 -v4299 -v3081 -v2321 -v2033 v2017 v1061 -v520 v4305 -v3812 -v3701 -v3082 v2037 -v116 v4301 -v3875 -v3702 -v3691 -v3127 -v2319 v2041 v2018 -v1738 -v1182 -v1135 -v1069 -v115 v4313 v3703 -v2040 -v1390 -v1137 -v1073 v3719 -v3692 -v2337 v1741 -v1595 v1077 -v123 -v61 -v1641 v1076 -v127 -v3441 -v1642 v1598 -v1131 -v745 -v131 -v3440 -v1667 -v1643 -v1266 -v749 -v130 -v1688 -v1659 -v1267 -v1144 -v1132 -v699 -v382 -v1684 v1268 -v1148 -v703 -v3955 v2556 -v1683 v1284 -v388 v2557 -v3961 -v3437 -v2552 v1011 -v884 -v705 -v532 v1012 -v886 -v706 -v536 v404 -v3966 -v3655 -v3025 -v2813 -v2550 -v1302 -v1007 v405 -v391 v350 v2817 -v1015 v406 v351 -v3969 -v3661 v3028 -v2803 v1815 v1328 -v1308 -v1016 -v1005 -v880 -v422 -v346 -v3967 v2802 v1017 -v2819 -v1334 v1313 -v1031 -v881 -v344 -v2820 -v4059 -v3816 v3244 -v1914 -v1786 v1542 -v1420 -v718 v289 -v86 -v3366 v1918 -v1546 -v815 -v723 -v452 -v293 -v4115 -v3822 v3248 -v2514 -v2506 -v1789 -v1353 -v817 v719 -v454 -v4119 -v3246 -v3069 -v2518 -v2505 v823 v731 v455 -v3827 -v3114 -v3068 -v1548 -v1424 v819 -v796 -v690 -v471 -v83 v4064 -v2022 -v1549 -v1454 -v831 -v691 v4065 -v3830 v3170 v3120 -v3076 -v2975 -v2324 -v1475 -v799 -v686 -v522 -v433 v163 v4066 -v3828 -v3696 -v3080 -v2979 -v2323 -v1471 -v524 -v437 v164 v4082 v3125 v3084 -v2502 -v1470 -v684 -v647 -v159 -v3083 -v2027 -v651 -v3871 v3128 -v2918 -v2028 -v518 -v157 -v4300 -v3126 -v2922 v2029 -v1136 v1063 v4362 -v4321 -v3874 -v3722 v2333 -v2320 -v2045 -v1737 v1064 -v519 -v482 v4317 -v3723 v1065 -v486 -v117 v4316 -v3718 -v2336 v1743 -v1594 v1081 -v118 -v693 -v119 -v3716 -v2751 -v1685 -v1662 v1600 v747 -v692 -v378 -v135 -v1687 -v1663 -v751 v3507 -v2555 v1746 -v1658 -v1287 -v1146 -v700 -v384 v3511 -v2554 -v1288 -v1150 -v704 -v1681 -v1656 v1603 v1283 v1010 -v753 -v708 -v389 -v3954 -v2807 v1009 -v885 -v754 -v707 -v3956 -v3651 -v2806 -v1682 v1281 -v1152 -v531 -v392 v349 -v3962 -v1153 -v535 -v390 v348 -v3958 -v3657 -v3024 -v2814 -v2551 -v1811 v1324 -v1249 v425 -v3970 v2818 -v1301 v426 -v3662 v3030 -v2953 -v2822 v1814 v1330 -v1303 v1034 -v1006 -v421 -v2957 -v2821 -v1309 v1035 -v3663 -v1335 v1305 -v1030 -v419 -v345 -v3664 v1314 v3245 -v1916 -v1785 v1543 -v1421 -v1349 v301 -v87 -v3815 v3249 v1920 -v1547 v717 -v297 v4268 -v4117 -v3817 -v2513 -v1791 -v1551 -v1425 -v1352 -v739 -v689 v474 -v296 -v4121 -v3823 -v2517 -v1550 -v1423 -v818 -v735 -v688 v475 v3819 -v3166 -v1922 -v1472 v839 v795 -v734 -v470 v162 -v3831 -v3113 -v3070 -v1923 -v1474 v835 -v523 v161 -v4123 -v4085 v3169 -v3115 v3071 -v2977 -v1794 -v834 -v801 -v468 -v432 -v4124 v4086 v3121 v3072 -v2981 -v436 v4081 v3117 v3088 -v1468 -v685 -v649 v3129 -v653 v4358 -v4318 v4079 -v3870 -v3721 v2983 -v2917 v2048 -v1733 -v1469 -v804 -v158 -v4320 -v3720 v2984 -v2921 v2049 v4361 -v3876 -v2874 v2332 -v2044 -v1739 -v1590 -v1084 v655 -v481 -v1085 -v741 v656 -v485 -v4314 -v2747 -v2338 -v2042 v1744 -v1661 -v1596 v1080 -v771 -v740 -v138 -v1686 -v1660 -v1140 -v775 -v139 -v4419 -v4315 -v3879 -v3717 -v2750 v1747 v1601 -v1286 -v1139 v1078 v748 -v270 -v134 -v4423 v1745 -v1285 -v752 -v694 -v377 v3506 -v2341 v1604 -v1147 -v756 -v695 -v379 -v132 v3510 v1602 -v1151 -v755 -v696 v385 -v1657 v1155 -v919 -v712 v381 -v1154 v923 -v393 -v3404 -v3020 -v1282 -v1245 -v533 -v424 -v3957 -v3650 v2808 -v537 -v423 -v3978 -v3652 v3026 v2809 -v2675 -v1810 -v1248 v1033 -v3974 -v3658 v2810 -v2679 v1323 v1032 -v3973 -v3654 -v3536 v3031 -v2952 v2826 v1816 v1325 -v846 -v539 -v3665 -v2956 v1331 -v1304 v850 -v540 -v3032 v1327 -v1322 -v1028 -v420 -v3033 v1336 v1318 v4264 -v4112 -v3257 -v1917 v1787 -v1539 -v1422 -v1348 -v736 v473 -v300 -v3253 v1921 v1538 -v1426 -v738 v472 v4267 -v4118 -v3252 -v2897 -v2515 -v1925 -v1792 v1555 -v1354 v836 -v791 -v294 -v4122 v3818 -v2971 -v2519 -v1924 -v1473 v838 -v4126 -v4084 v3839 -v3165 -v2970 -v1795 -v898 v797 -v732 -v295 -v4125 -v4083 v3835 -v1793 -v643 v3834 v3171 -v3091 -v2978 -v2521 -v1357 -v832 -v802 -v733 -v642 -v469 -v434 -v3116 -v3092 v2982 -v2522 -v438 v3866 v3137 v3087 v2986 -v2107 -v2047 -v833 v805 -v650 -v24 -v4319 v3133 v2985 -v2046 -v803 -v654 -v28 v4357 -v4080 -v3872 -v3174 v3132 v3085 -v2919 -v2870 -v2328 -v1083 v658 -v440 -v2923 -v1732 -v1082 v657 -v441 v4363 v3877 -v2873 v2334 -v1734 -v483 -v137 v1740 -v1589 -v487 -v136 v3880 -v3846 -v2925 -v2746 -v2339 -v2043 v1736 -v1591 -v770 -v266 v3878 -v3850 -v2926 v1748 -v1597 -v774 -v742 -v4418 -v4366 -v2752 -v2604 -v2342 v1593 v1079 -v743 v489 -v269 -v4422 -v2340 v1605 -v1141 v744 v490 v3508 -v1142 v760 -v715 -v133 v3512 v1143 -v716 -v527 -v380 -v3400 -v2755 v1159 -v918 -v711 v602 -v526 -v401 v922 v397 -v3975 v3514 -v3403 v2629 -v1806 -v1244 -v709 -v534 -v396 -v3977 v3515 -v3019 -v538 -v3631 -v3532 -v3021 v2829 -v2674 -v1812 -v1250 -v542 -v3653 v3635 v3027 v2830 -v2678 -v541 -v3971 -v3673 -v3535 v3023 -v2954 v2825 v1817 -v1319 -v845 -v3669 -v3034 -v2958 v1326 -v1321 v849 -v3972 -v3668 v2823 v2244 -v1818 -v1344 -v1253 -v1029 -v2248 -v1819 v1340 v1317 v4263 -v3256 -v2893 -v2510 -v1913 -v1783 v1558 v1497 -v1434 -v1350 -v737 -v298 -v4111 v1912 v1788 v1559 -v1430 -v837 v4269 -v4113 -v3836 -v3250 v3161 -v2896 -v2516 v1929 v1784 -v1554 -v1429 -v1355 -v894 -v4114 -v3838 -v2520 -v1796 -v790 -v428 -v4130 -v3251 v3167 -v3090 -v2524 -v1944 -v1552 -v1358 -v897 -v792 -v427 -v3089 -v2972 -v2523 -v1356 v798 v4272 -v3832 v3172 v3134 -v2973 -v2103 v794 -v435 v3136 v2974 -v2913 v806 v644 -v439 v4353 -v3833 -v3175 v2990 -v2912 -v2106 -v1620 v645 -v443 -v23 v3865 -v3173 -v1624 v646 -v477 -v442 -v27 v4359 -v4213 v3867 -v3130 -v3086 -v2920 -v2869 v662 -v476 -v3873 -v2924 -v2327 v4364 v3869 -v3207 -v3131 -v2928 -v2875 -v2742 v2329 -v1713 -v484 v3881 -v2927 v2335 -v1735 -v1717 -v488 -v4367 -v3845 -v2748 -v2600 v2331 v1756 -v772 v492 -v265 -v4365 -v3849 -v3502 -v2343 v1752 -v1592 -v776 v491 -v4420 -v3501 -v2878 -v2753 -v2603 v1751 -v1613 v763 -v714 -v271 -v4424 -v1609 v764 -v713 v3509 -v2756 -v1608 v1162 -v778 v759 -v598 -v398 v3513 -v2754 v1163 -v779 -v400 v4426 -v4163 -v3606 v3517 -v3399 -v2625 -v1240 -v1158 -v920 v757 v601 -v274 v4427 -v3976 -v3610 v3516 v924 -v528 -v3405 -v2828 v2628 -v1246 -v1156 -v710 -v529 -v394 -v2948 -v2827 -v1805 -v530 -v3670 -v3630 -v3531 -v3310 -v2947 -v2676 -v1807 -v1251 v926 -v546 -v395 -v3672 v3634 -v3022 v2680 -v1813 -v1320 -v927 -v3537 -v3408 -v3042 -v2955 v1809 -v1341 -v1254 -v847 v3038 -v2959 v1820 -v1343 -v1252 v851 -v3666 v3037 v2960 v2824 -v2682 v2243 -v2060 v2961 -v2683 -v2247 v1339 -v1315 v4265 -v3916 -v3254 -v2892 v1932 v1556 v1496 -v1433 -v1346 -v299 -v3837 -v2509 v1933 v1782 -v1351 v4270 -v4133 -v2898 -v2511 -v1940 v1928 v1804 -v1427 -v1347 v893 -v4134 v3160 -v2512 v1800 -v1359 v4273 -v4129 v3162 -v2528 -v2424 -v1943 v1926 -v1799 -v1553 -v1428 -v899 v4271 v3168 v3135 -v793 -v429 -v4127 v3164 -v2993 -v2901 v2700 -v2102 v814 -v430 v3176 -v2994 -v2704 -v810 -v431 -v4209 v2989 -v2865 -v2108 -v1619 -v902 -v809 -v665 -v447 -v308 -v25 v4352 -v2914 -v1623 v666 -v312 -v29 v4354 -v4212 -v3203 -v2987 -v2915 -v2871 -v948 v661 v4360 v3868 -v2916 v766 -v478 v4356 -v3889 -v3206 -v2932 -v2876 -v2111 -v1981 -v1753 -v1712 v765 -v659 -v479 -v261 -v31 v4414 -v4368 -v3885 -v2741 v2330 -v1985 v1755 -v1716 v480 -v32 v4413 -v3884 -v3847 -v2879 -v2743 -v2654 -v2599 -v2351 -v2153 -v1610 -v773 v762 -v496 -v267 -v3851 -v2877 -v2749 -v2347 -v2157 -v1612 -v777 v761 -v4421 -v2745 -v2605 -v2346 v1749 -v1161 -v781 -v272 -v100 -v4425 -v3503 -v2757 v1160 -v914 -v780 -v399 v4429 -v4159 v3853 -v3504 -v3395 v1750 -v1606 -v913 -v597 -v362 v275 v4428 v3854 v3505 -v273 -v4162 -v3605 v3521 -v3401 -v2624 -v2608 -v1607 -v921 v758 v603 -v3609 -v2670 -v1239 v925 v3527 -v3406 -v3306 -v3049 -v2669 v2630 -v1241 -v1157 v929 -v549 -v3671 -v3053 -v1247 v928 -v841 -v550 -v3632 -v3533 -v3409 -v3309 -v3039 -v2677 -v1243 v840 -v606 -v545 v3636 -v3407 -v3041 -v2949 v2681 -v1808 -v1342 -v1255 -v3538 -v2950 -v2685 -v2633 -v2056 -v1828 v848 -v543 v2951 -v2684 v1824 v852 -v3942 -v3667 v3638 -v3539 -v3035 v2965 v2245 -v2059 v1823 v853 v3639 -v3540 -v2249 -v1337 -v1316 v854 -v4261 -v4132 -v3915 -v3255 -v2894 v1930 -v1801 v1557 v1498 -v1431 -v889 v4266 -v4131 v1803 -v1345 v4262 -v3000 -v2899 -v2531 -v2420 -v1939 -v1367 v895 v4274 -v3004 -v2532 -v1363 -v2992 -v2902 -v2527 -v2423 -v2098 -v1945 -v1927 -v1797 -v1502 -v1362 -v900 -v811 v3163 -v2991 -v2900 -v813 v19 -v4128 v3184 v2699 -v2525 -v2104 -v1798 v903 -v664 -v450 v18 v3180 -v2703 v901 -v663 -v451 -v4208 -v3179 -v2109 -v1948 -v1621 -v1519 -v944 -v807 -v446 -v307 -v26 -v2864 v1625 -v1523 -v311 -v30 -v4214 -v3886 -v3202 -v2988 -v2935 -v2866 -v2112 -v947 -v808 -v444 v34 v4355 -v3888 -v3841 -v2936 -v2872 -v2110 -v1754 v33 -v4376 -v3840 v3208 -v2931 -v2868 -v2650 -v2595 -v2348 -v1980 -v1714 -v1627 v1224 -v660 v499 -v4372 -v2880 -v2350 -v1984 -v1718 -v1628 -v1611 v767 v500 -v260 -v4371 v4217 -v3882 -v3848 -v2929 -v2653 -v2601 -v2152 v768 -v495 -v262 -v96 v4415 v3852 -v2744 -v2156 v769 -v268 v4416 -v3883 v3856 -v3211 -v2765 -v2606 -v2344 -v1720 v785 -v593 -v493 -v358 v264 -v99 v4417 v3855 -v2761 -v1721 v276 v4433 -v4158 v3524 -v3264 -v2760 -v2620 -v2609 -v2345 -v599 -v361 v3525 -v3394 -v3268 -v2607 -v915 -v4164 -v3607 v3520 -v3396 -v2626 v916 -v627 v604 -v548 v3626 -v3611 -v3402 v917 -v547 v3625 v3518 -v3398 v3305 -v3048 v2631 -v933 v607 -v561 v3526 -v3410 -v3052 -v3040 -v2671 -v1242 -v605 -v4167 -v3633 -v3613 v3528 -v3311 -v2672 -v2634 -v1825 -v1263 v3637 -v3614 -v3534 v2673 -v2632 -v2239 -v1827 -v1259 v842 -v3938 v3641 v3530 v2968 v2689 -v2238 -v2055 -v1258 v843 -v544 v3640 -v3541 v2969 v844 -v3941 -v3314 -v3036 v2964 v2265 v2246 -v2061 -v1821 -v858 -v7 -v2250 -v1338 -v11 v3917 v2890 -v2530 -v1935 -v1931 -v1802 v1499 -v1432 -v1364 -v4260 -v2895 -v2529 -v1366 -v888 -v4282 -v2999 v2891 -v2419 -v1941 v1503 -v890 -v4278 -v3003 -v2903 -v1501 v896 -v812 -v4277 -v3921 v3181 -v2425 -v2128 -v1946 -v1360 v892 -v449 v3183 -v2132 -v2097 v1615 v904 -v448 v4204 v2701 -v2526 -v2099 -v1949 v1614 -v1361 v2705 -v2105 -v1947 v20 -v4210 -v4188 -v3198 -v3177 -v2934 v2428 -v2101 -v1622 -v1518 -v943 -v309 v21 -v3887 -v2933 -v2113 -v1708 v1626 -v1522 v313 v22 -v4373 v4215 v3204 -v3178 -v2707 -v1763 -v1707 -v1630 -v1220 -v949 v498 -v445 -v38 -v4375 -v2867 -v2708 -v2349 -v1767 -v1629 v497 v4218 v3209 -v2888 -v2649 -v2219 -v1982 -v1715 v1223 v315 v4216 -v3842 -v2884 -v2594 -v2223 -v1986 -v1719 -v316 -v4369 -v3843 v3212 -v2930 -v2883 -v2762 -v2655 -v2596 -v2154 -v1723 -v952 -v788 -v95 v3844 -v3210 -v2764 -v2602 -v2158 -v1722 -v789 -v263 v4436 -v4370 -v4154 -v3860 -v3523 -v2598 -v1988 v784 -v494 -v357 -v284 v101 v4437 -v3601 -v3522 -v2610 -v1989 -v592 v280 v4432 -v4160 -v3600 -v3263 -v2758 -v2658 -v2160 -v782 -v623 -v594 v363 v279 -v3267 -v2619 -v2161 -v600 -v4430 -v4165 -v3608 -v3301 v2837 -v2759 -v2621 v936 -v626 v596 -v557 -v104 -v3612 -v3397 -v2841 -v2627 v937 v608 -v4168 -v3616 v3519 -v3418 v3307 -v3050 v2623 -v1260 -v932 -v560 -v366 -v4166 v3627 -v3615 -v3414 v3054 v2635 -v1826 -v1262 v3628 -v3413 -v3312 -v2967 -v2692 -v2051 -v930 v3629 v3529 -v2966 -v2693 -v3937 v3645 -v3549 v3315 -v3056 v2688 v2261 -v2057 -v1256 -v861 v3545 -v3313 -v3057 -v2240 -v862 -v3943 v3544 v2962 -v2686 v2264 -v2241 -v2062 -v1822 -v1257 -v857 -v6 v2242 -v10 -v4279 v3918 -v2415 v1500 -v1365 -v4281 v2889 -v1934 v1504 v3922 v3001 v2911 v2421 -v1936 -v3920 v3182 -v3005 v2907 -v2695 -v1942 -v891 -v4275 -v3465 v2906 -v2694 -v2426 -v2127 -v1938 v912 -v2131 -v1950 v908 -v303 -v4276 -v4184 -v3007 v2702 v2429 -v939 -v907 -v302 v4203 -v3008 v2706 v2427 -v2100 v1616 -v4386 v4205 -v4187 v2710 -v2121 v1617 -v1520 -v945 -v310 -v41 -v4374 v4211 -v3197 v2709 -v2117 -v1976 v1618 -v1524 v314 -v42 v4207 v3199 -v2885 -v2645 -v2116 -v1975 -v1762 -v1634 -v1219 -v950 v318 -v37 v4219 v3205 -v2887 -v2148 -v1766 -v1709 v317 v3201 -v2651 -v2218 -v2147 -v1983 -v1710 -v1526 v1225 -v953 -v787 -v91 -v35 v3213 -v2763 -v2222 -v1987 -v1711 -v1527 -v951 -v786 -v4435 -v3863 -v2881 -v2656 -v2155 -v1991 -v1727 -v353 -v281 v97 -v4434 v3864 -v2597 -v2159 -v1990 -v283 -v3859 -v2882 -v2659 -v2618 v2163 v1228 -v359 v102 -v4153 -v2657 -v2614 -v2162 -v4155 -v3857 v3265 -v2613 -v935 -v783 -v622 v364 -v277 v105 -v4161 -v3602 -v3269 -v3044 v934 -v595 -v103 -v4431 -v4157 -v3603 -v3415 -v3043 v2836 -v1099 v628 -v616 -v556 v367 -v278 -v4169 -v3604 -v3417 -v3300 -v2840 -v2622 -v1261 -v612 -v365 -v3620 -v3302 -v3271 -v3051 -v2691 v2643 -v611 -v562 v3308 -v3272 v3055 -v2690 -v2639 -v3933 -v3648 -v3546 -v3411 v3304 v3059 -v2638 -v931 -v860 -v631 v3649 -v3548 v3316 -v3058 -v2050 -v859 -v3939 v3644 -v3412 v2260 -v2052 v565 -v2058 -v3944 v3642 -v3542 -v2963 -v2687 v2266 v2253 -v2054 -v855 -v8 v2254 -v2063 -v12 -v4280 v3919 -v2996 -v2908 v1512 v1290 v3923 v2910 -v2414 -v1508 -v1294 -v3461 v3002 -v2416 -v1507 v909 -v3006 v2422 -v1937 v911 -v3464 v3010 -v2904 v2418 v2129 -v1958 v3009 -v2696 v2430 -v2133 -v1954 -v1514 -v4382 -v4183 -v2905 -v2697 -v2118 -v1953 -v1513 -v905 -v40 v2698 -v2120 v938 -v304 -v39 -v4385 v4189 -v2714 -v2135 -v1637 -v1521 -v1215 v940 -v906 v305 v4206 -v2886 -v2136 -v1638 -v1525 -v946 v306 -v4227 -v2114 -v1764 -v1633 -v1529 -v1221 v942 v322 v4223 v3200 -v2644 -v1977 -v1768 -v1528 -v954 v4222 -v4192 -v3862 -v3585 -v3221 -v2646 v2220 -v2115 -v1978 -v1730 -v1631 v1226 -v36 -v3861 v3217 -v2652 -v2224 -v2149 -v1979 -v1731 -v282 -v90 v3216 v2648 -v2615 v2150 -v1995 v1770 -v1726 v1229 -v92 v3259 -v2660 -v2617 v2151 v1771 v1227 -v352 v98 v3258 v2226 v2167 -v1724 -v618 -v354 v94 -v2227 -v360 v106 -v3858 v3266 -v2611 -v1095 v624 -v613 -v552 v356 -v4156 -v3416 v3270 -v615 v368 -v4177 -v3623 v3274 v2838 -v2640 -v2612 -v1098 v629 -v558 -v4173 -v3624 -v3273 -v3045 -v2842 -

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/8593/stat): 8593 (minisat+_script) R 8592 8593 30740 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1785450072 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/8593/statm): 174 3 169 147 0 27 0
[pid=8593] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libtermcap.so.2
open syscall for file tls/i686/libtermcap.so.2
open syscall for file tls/mmx/libtermcap.so.2
open syscall for file tls/libtermcap.so.2
open syscall for file i686/mmx/libtermcap.so.2
open syscall for file i686/libtermcap.so.2
open syscall for file mmx/libtermcap.so.2
open syscall for file libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/libtermcap.so.2
open syscall for file /etc/ld.so.cache
open syscall for file /lib/libtermcap.so.2
open syscall for file tls/i686/mmx/libdl.so.2
open syscall for file tls/i686/libdl.so.2
open syscall for file tls/mmx/libdl.so.2
open syscall for file tls/libdl.so.2
open syscall for file i686/mmx/libdl.so.2
open syscall for file i686/libdl.so.2
open syscall for file mmx/libdl.so.2
open syscall for file libdl.so.2
open syscall for file /oldhome/oroussel/lib/libdl.so.2
open syscall for file /lib/libdl.so.2
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /lib/tls/libc.so.6
open syscall for file /dev/tty
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
New process pid=8594
New process pid=8595
New process pid=8596
execve syscall for /bin/sed executable
One traced child (pid=8595) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=8596) exited with status: 0
One traced child (pid=8594) exited with status: 0
New process pid=8597
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc9/normalized-30:30:4.5:0.5:100.opb

[startup+10.0029 s]
Raw data (loadavg): 0.94 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 11128 0 0 0 921 41 0 0 25 0 1 0 1785450077 47509504 9673 4294967295 134512640 135094434 3221224448 3221223060 134563121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 11599 9673 145 145 0 11454 0
[pid=8597] vsize: 46396
Current children cumulated CPU time (s) 9.63
Current children cumulated vsize (Kb) 48520

[startup+20.0047 s]
Raw data (loadavg): 0.95 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 11202 0 0 0 1919 42 0 0 25 0 1 0 1785450077 47812608 9747 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 11673 9747 145 145 0 11528 0
[pid=8597] vsize: 46692
Current children cumulated CPU time (s) 19.62
Current children cumulated vsize (Kb) 48816

[startup+30.0055 s]
Raw data (loadavg): 0.95 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 11295 0 0 0 2917 43 0 0 25 0 1 0 1785450077 48205824 9840 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 11769 9840 145 145 0 11624 0
[pid=8597] vsize: 47076
Current children cumulated CPU time (s) 29.61
Current children cumulated vsize (Kb) 49200

[startup+40.0073 s]
Raw data (loadavg): 0.96 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 11385 0 0 0 3914 45 0 0 25 0 1 0 1785450077 48623616 9930 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 11871 9930 145 145 0 11726 0
[pid=8597] vsize: 47484
Current children cumulated CPU time (s) 39.6
Current children cumulated vsize (Kb) 49608

[startup+50.008 s]
Raw data (loadavg): 0.97 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 11465 0 0 0 4912 47 0 0 25 0 1 0 1785450077 48930816 10010 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 11946 10010 145 145 0 11801 0
[pid=8597] vsize: 47784
Current children cumulated CPU time (s) 49.6
Current children cumulated vsize (Kb) 49908

[startup+60.0088 s]
Raw data (loadavg): 0.97 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 11680 0 0 0 5908 48 0 0 25 0 1 0 1785450077 49778688 10225 4294967295 134512640 135094434 3221224448 3221223060 134563043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 12153 10225 145 145 0 12008 0
[pid=8597] vsize: 48612
Current children cumulated CPU time (s) 59.57
Current children cumulated vsize (Kb) 50736

[startup+70.0106 s]
Raw data (loadavg): 0.97 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 11810 0 0 0 6906 49 0 0 25 0 1 0 1785450077 50421760 10355 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 12310 10355 145 145 0 12165 0
[pid=8597] vsize: 49240
Current children cumulated CPU time (s) 69.56
Current children cumulated vsize (Kb) 51364

[startup+80.0113 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 11925 0 0 0 7903 50 0 0 25 0 1 0 1785450077 50872320 10470 4294967295 134512640 135094434 3221224448 3221223040 134778949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 12420 10470 145 145 0 12275 0
[pid=8597] vsize: 49680
Current children cumulated CPU time (s) 79.54
Current children cumulated vsize (Kb) 51804

[startup+90.0131 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 12249 0 0 0 8900 52 0 0 25 0 1 0 1785450077 51982336 10659 4294967295 134512640 135094434 3221224448 3221221972 134520000 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 12691 10659 145 145 0 12546 0
[pid=8597] vsize: 50764
Current children cumulated CPU time (s) 89.53
Current children cumulated vsize (Kb) 52888

[startup+100.014 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 12561 0 0 0 9898 54 0 0 25 0 1 0 1785450077 52043776 10775 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 12706 10775 145 145 0 12561 0
[pid=8597] vsize: 50824
Current children cumulated CPU time (s) 99.53
Current children cumulated vsize (Kb) 52948

[startup+110.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 12781 0 0 0 10893 56 0 0 25 0 1 0 1785450077 52871168 10995 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 12908 10995 145 145 0 12763 0
[pid=8597] vsize: 51632
Current children cumulated CPU time (s) 109.5
Current children cumulated vsize (Kb) 53756

[startup+120.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 13360 0 0 0 11882 60 0 0 25 0 1 0 1785450077 55459840 11574 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 13540 11574 145 145 0 13395 0
[pid=8597] vsize: 54160
Current children cumulated CPU time (s) 119.43
Current children cumulated vsize (Kb) 56284

[startup+130.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 13798 0 0 0 12874 63 0 0 25 0 1 0 1785450077 57221120 12012 4294967295 134512640 135094434 3221224448 3221223104 134557972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 13970 12012 145 145 0 13825 0
[pid=8597] vsize: 55880
Current children cumulated CPU time (s) 129.38
Current children cumulated vsize (Kb) 58004

[startup+140.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 14693 0 0 0 13859 70 0 0 25 0 1 0 1785450077 60862464 12907 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 14859 12907 145 145 0 14714 0
[pid=8597] vsize: 59436
Current children cumulated CPU time (s) 139.3
Current children cumulated vsize (Kb) 61560

[startup+150.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 15407 0 0 0 14848 75 0 0 25 0 1 0 1785450077 63766528 13621 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 15568 13621 145 145 0 15423 0
[pid=8597] vsize: 62272
Current children cumulated CPU time (s) 149.24
Current children cumulated vsize (Kb) 64396

[startup+160.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 16014 0 0 0 15837 81 0 0 25 0 1 0 1785450077 66220032 14228 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 16167 14228 145 145 0 16022 0
[pid=8597] vsize: 64668
Current children cumulated CPU time (s) 159.19
Current children cumulated vsize (Kb) 66792

[startup+170.019 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) T 8593 8593 30740 0 -1 0 16813 0 0 0 16821 87 0 0 25 0 1 0 1785450077 69464064 15027 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/8597/statm): 16959 15027 145 145 0 16814 0
[pid=8597] vsize: 67836
Current children cumulated CPU time (s) 169.09
Current children cumulated vsize (Kb) 69960

[startup+180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 17193 0 0 0 17815 90 0 0 25 0 1 0 1785450077 71000064 15407 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 17334 15407 145 145 0 17189 0
[pid=8597] vsize: 69336
Current children cumulated CPU time (s) 179.06
Current children cumulated vsize (Kb) 71460

[startup+190.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 17665 0 0 0 18806 93 0 0 25 0 1 0 1785450077 72896512 15879 4294967295 134512640 135094434 3221224448 3221223104 134558169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 17797 15879 145 145 0 17652 0
[pid=8597] vsize: 71188
Current children cumulated CPU time (s) 189
Current children cumulated vsize (Kb) 73312

[startup+200.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 18227 0 0 0 19797 97 0 0 25 0 1 0 1785450077 75173888 16441 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 18353 16441 145 145 0 18208 0
[pid=8597] vsize: 73412
Current children cumulated CPU time (s) 198.95
Current children cumulated vsize (Kb) 75536

[startup+210.023 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) T 8593 8593 30740 0 -1 0 18848 0 0 0 20784 102 0 0 25 0 1 0 1785450077 77684736 17062 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/8597/statm): 18966 17062 145 145 0 18821 0
[pid=8597] vsize: 75864
Current children cumulated CPU time (s) 208.87
Current children cumulated vsize (Kb) 77988

[startup+220.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 19324 0 0 0 21775 106 0 0 25 0 1 0 1785450077 80130048 17538 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 19563 17538 145 145 0 19418 0
[pid=8597] vsize: 78252
Current children cumulated CPU time (s) 218.82
Current children cumulated vsize (Kb) 80376

[startup+230.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 19810 0 0 0 22767 110 0 0 25 0 1 0 1785450077 82087936 18024 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 20041 18024 145 145 0 19896 0
[pid=8597] vsize: 80164
Current children cumulated CPU time (s) 228.78
Current children cumulated vsize (Kb) 82288

[startup+240.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 20466 0 0 0 23755 116 0 0 25 0 1 0 1785450077 84754432 18680 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 20692 18680 145 145 0 20547 0
[pid=8597] vsize: 82768
Current children cumulated CPU time (s) 238.72
Current children cumulated vsize (Kb) 84892

[startup+250.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 20985 0 0 0 24743 121 0 0 25 0 1 0 1785450077 86863872 19199 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 21207 19199 145 145 0 21062 0
[pid=8597] vsize: 84828
Current children cumulated CPU time (s) 248.65
Current children cumulated vsize (Kb) 86952

[startup+260.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 21552 0 0 0 25734 124 0 0 25 0 1 0 1785450077 89174016 19766 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 21771 19766 145 145 0 21626 0
[pid=8597] vsize: 87084
Current children cumulated CPU time (s) 258.59
Current children cumulated vsize (Kb) 89208

[startup+270.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 22080 0 0 0 26725 128 0 0 25 0 1 0 1785450077 91336704 20294 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 22299 20294 145 145 0 22154 0
[pid=8597] vsize: 89196
Current children cumulated CPU time (s) 268.54
Current children cumulated vsize (Kb) 91320

[startup+280.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) T 8593 8593 30740 0 -1 0 22558 0 0 0 27716 131 0 0 25 0 1 0 1785450077 93265920 20772 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/8597/statm): 22770 20772 145 145 0 22625 0
[pid=8597] vsize: 91080
Current children cumulated CPU time (s) 278.48
Current children cumulated vsize (Kb) 93204

[startup+290.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 22899 0 0 0 28710 134 0 0 25 0 1 0 1785450077 94625792 21113 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 23102 21113 145 145 0 22957 0
[pid=8597] vsize: 92408
Current children cumulated CPU time (s) 288.45
Current children cumulated vsize (Kb) 94532

[startup+300.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 23014 0 0 0 29709 134 0 0 25 0 1 0 1785450077 95084544 21228 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 23214 21228 145 145 0 23069 0
[pid=8597] vsize: 92856
Current children cumulated CPU time (s) 298.44
Current children cumulated vsize (Kb) 94980

[startup+310.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 23168 0 0 0 30706 136 0 0 25 0 1 0 1785450077 95698944 21382 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 23364 21382 145 145 0 23219 0
[pid=8597] vsize: 93456
Current children cumulated CPU time (s) 308.43
Current children cumulated vsize (Kb) 95580

[startup+320.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 23709 0 0 0 31697 139 0 0 25 0 1 0 1785450077 97890304 21923 4294967295 134512640 135094434 3221224448 3221223088 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 23899 21923 145 145 0 23754 0
[pid=8597] vsize: 95596
Current children cumulated CPU time (s) 318.37
Current children cumulated vsize (Kb) 97720

[startup+330.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 24499 0 0 0 32684 144 0 0 25 0 1 0 1785450077 101109760 22713 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 24685 22713 145 145 0 24540 0
[pid=8597] vsize: 98740
Current children cumulated CPU time (s) 328.29
Current children cumulated vsize (Kb) 100864

[startup+340.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) T 8593 8593 30740 0 -1 0 25472 0 0 0 33669 150 0 0 25 0 1 0 1785450077 105082880 23686 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/8597/statm): 25655 23686 145 145 0 25510 0
[pid=8597] vsize: 102620
Current children cumulated CPU time (s) 338.2
Current children cumulated vsize (Kb) 104744

[startup+350.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) T 8593 8593 30740 0 -1 0 26458 0 0 0 34657 155 0 0 25 0 1 0 1785450077 109109248 24672 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/8597/statm): 26638 24672 145 145 0 26493 0
[pid=8597] vsize: 106552
Current children cumulated CPU time (s) 348.13
Current children cumulated vsize (Kb) 108676

[startup+360.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 27350 0 0 0 35643 160 0 0 25 0 1 0 1785450077 112754688 25564 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 27528 25564 145 145 0 27383 0
[pid=8597] vsize: 110112
Current children cumulated CPU time (s) 358.04
Current children cumulated vsize (Kb) 112236

[startup+370.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 28109 0 0 0 36630 165 0 0 25 0 1 0 1785450077 115851264 26323 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 28284 26323 145 145 0 28139 0
[pid=8597] vsize: 113136
Current children cumulated CPU time (s) 367.96
Current children cumulated vsize (Kb) 115260

[startup+380.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 28817 0 0 0 37618 170 0 0 25 0 1 0 1785450077 118734848 27031 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 28988 27031 145 145 0 28843 0
[pid=8597] vsize: 115952
Current children cumulated CPU time (s) 377.89
Current children cumulated vsize (Kb) 118076

[startup+390.038 s]
Raw data (loadavg): 0.99 0.97 0.91 3/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 29530 0 0 0 38606 175 0 0 25 0 1 0 1785450077 121638912 27744 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 29697 27744 145 145 0 29552 0
[pid=8597] vsize: 118788
Current children cumulated CPU time (s) 387.82
Current children cumulated vsize (Kb) 120912

[startup+400.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 30185 0 0 0 39593 180 0 0 25 0 1 0 1785450077 124313600 28399 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 30350 28399 145 145 0 30205 0
[pid=8597] vsize: 121400
Current children cumulated CPU time (s) 397.74
Current children cumulated vsize (Kb) 123524

[startup+410.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 31020 0 0 0 40582 185 0 0 25 0 1 0 1785450077 127721472 29234 4294967295 134512640 135094434 3221224448 3221223120 134555826 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 31182 29234 145 145 0 31037 0
[pid=8597] vsize: 124728
Current children cumulated CPU time (s) 407.68
Current children cumulated vsize (Kb) 126852

[startup+420.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 31675 0 0 0 41570 190 0 0 25 0 1 0 1785450077 130392064 29889 4294967295 134512640 135094434 3221224448 3221222848 134562864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 31834 29889 145 145 0 31689 0
[pid=8597] vsize: 127336
Current children cumulated CPU time (s) 417.61
Current children cumulated vsize (Kb) 129460

[startup+430.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 31675 0 0 0 42570 190 0 0 25 0 1 0 1785450077 130392064 29889 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 31834 29889 145 145 0 31689 0
[pid=8597] vsize: 127336
Current children cumulated CPU time (s) 427.61
Current children cumulated vsize (Kb) 129460

[startup+440.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 31675 0 0 0 43571 190 0 0 25 0 1 0 1785450077 130392064 29889 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 31834 29889 145 145 0 31689 0
[pid=8597] vsize: 127336
Current children cumulated CPU time (s) 437.62
Current children cumulated vsize (Kb) 129460

[startup+450.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 31675 0 0 0 44571 190 0 0 25 0 1 0 1785450077 130392064 29889 4294967295 134512640 135094434 3221224448 3221223040 134557518 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 31834 29889 145 145 0 31689 0
[pid=8597] vsize: 127336
Current children cumulated CPU time (s) 447.62
Current children cumulated vsize (Kb) 129460

[startup+460.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 31675 0 0 0 45571 190 0 0 25 0 1 0 1785450077 130392064 29889 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 31834 29889 145 145 0 31689 0
[pid=8597] vsize: 127336
Current children cumulated CPU time (s) 457.62
Current children cumulated vsize (Kb) 129460

[startup+470.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 31675 0 0 0 46571 190 0 0 25 0 1 0 1785450077 130392064 29889 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 31834 29889 145 145 0 31689 0
[pid=8597] vsize: 127336
Current children cumulated CPU time (s) 467.62
Current children cumulated vsize (Kb) 129460

[startup+480.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 31675 0 0 0 47571 190 0 0 25 0 1 0 1785450077 130392064 29889 4294967295 134512640 135094434 3221224448 3221223112 134555971 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 31834 29889 145 145 0 31689 0
[pid=8597] vsize: 127336
Current children cumulated CPU time (s) 477.62
Current children cumulated vsize (Kb) 129460

[startup+490.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 31675 0 0 0 48571 190 0 0 25 0 1 0 1785450077 130392064 29889 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 31834 29889 145 145 0 31689 0
[pid=8597] vsize: 127336
Current children cumulated CPU time (s) 487.62
Current children cumulated vsize (Kb) 129460

[startup+500.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 31675 0 0 0 49570 190 0 0 25 0 1 0 1785450077 130392064 29889 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 31834 29889 145 145 0 31689 0
[pid=8597] vsize: 127336
Current children cumulated CPU time (s) 497.61
Current children cumulated vsize (Kb) 129460

[startup+510.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 31675 0 0 0 50570 190 0 0 25 0 1 0 1785450077 130392064 29889 4294967295 134512640 135094434 3221224448 3221223072 134562144 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 31834 29889 145 145 0 31689 0
[pid=8597] vsize: 127336
Current children cumulated CPU time (s) 507.61
Current children cumulated vsize (Kb) 129460

[startup+520.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 31675 0 0 0 51571 190 0 0 25 0 1 0 1785450077 130392064 29889 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 31834 29889 145 145 0 31689 0
[pid=8597] vsize: 127336
Current children cumulated CPU time (s) 517.62
Current children cumulated vsize (Kb) 129460

[startup+530.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 31675 0 0 0 52571 190 0 0 25 0 1 0 1785450077 130392064 29889 4294967295 134512640 135094434 3221224448 3221223128 134554880 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 31834 29889 145 145 0 31689 0
[pid=8597] vsize: 127336
Current children cumulated CPU time (s) 527.62
Current children cumulated vsize (Kb) 129460

[startup+540.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 31675 0 0 0 53571 190 0 0 25 0 1 0 1785450077 130392064 29889 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 31834 29889 145 145 0 31689 0
[pid=8597] vsize: 127336
Current children cumulated CPU time (s) 537.62
Current children cumulated vsize (Kb) 129460

[startup+550.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 31675 0 0 0 54571 190 0 0 25 0 1 0 1785450077 130392064 29889 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 31834 29889 145 145 0 31689 0
[pid=8597] vsize: 127336
Current children cumulated CPU time (s) 547.62
Current children cumulated vsize (Kb) 129460

[startup+560.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 31675 0 0 0 55572 190 0 0 25 0 1 0 1785450077 130392064 29889 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 31834 29889 145 145 0 31689 0
[pid=8597] vsize: 127336
Current children cumulated CPU time (s) 557.63
Current children cumulated vsize (Kb) 129460

[startup+570.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 31675 0 0 0 56572 190 0 0 25 0 1 0 1785450077 130392064 29889 4294967295 134512640 135094434 3221224448 3221223088 134562149 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 31834 29889 145 145 0 31689 0
[pid=8597] vsize: 127336
Current children cumulated CPU time (s) 567.63
Current children cumulated vsize (Kb) 129460

[startup+580.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 31675 0 0 0 57572 190 0 0 25 0 1 0 1785450077 130392064 29889 4294967295 134512640 135094434 3221224448 3221223136 134554788 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 31834 29889 145 145 0 31689 0
[pid=8597] vsize: 127336
Current children cumulated CPU time (s) 577.63
Current children cumulated vsize (Kb) 129460

[startup+590.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 31675 0 0 0 58572 190 0 0 25 0 1 0 1785450077 130392064 29889 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 31834 29889 145 145 0 31689 0
[pid=8597] vsize: 127336
Current children cumulated CPU time (s) 587.63
Current children cumulated vsize (Kb) 129460

[startup+600.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 31675 0 0 0 59573 190 0 0 25 0 1 0 1785450077 130392064 29889 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 31834 29889 145 145 0 31689 0
[pid=8597] vsize: 127336
Current children cumulated CPU time (s) 597.64
Current children cumulated vsize (Kb) 129460

[startup+610.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 31675 0 0 0 60573 190 0 0 25 0 1 0 1785450077 130392064 29889 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 31834 29889 145 145 0 31689 0
[pid=8597] vsize: 127336
Current children cumulated CPU time (s) 607.64
Current children cumulated vsize (Kb) 129460

[startup+620.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 31675 0 0 0 61573 190 0 0 25 0 1 0 1785450077 130392064 29889 4294967295 134512640 135094434 3221224448 3221223040 134556904 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 31834 29889 145 145 0 31689 0
[pid=8597] vsize: 127336
Current children cumulated CPU time (s) 617.64
Current children cumulated vsize (Kb) 129460

[startup+630.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 31675 0 0 0 62573 190 0 0 25 0 1 0 1785450077 130392064 29889 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 31834 29889 145 145 0 31689 0
[pid=8597] vsize: 127336
Current children cumulated CPU time (s) 627.64
Current children cumulated vsize (Kb) 129460

[startup+640.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 31675 0 0 0 63574 190 0 0 25 0 1 0 1785450077 130392064 29889 4294967295 134512640 135094434 3221224448 3221223120 134555795 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 31834 29889 145 145 0 31689 0
[pid=8597] vsize: 127336
Current children cumulated CPU time (s) 637.65
Current children cumulated vsize (Kb) 129460

[startup+650.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 31675 0 0 0 64574 190 0 0 25 0 1 0 1785450077 130392064 29889 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 31834 29889 145 145 0 31689 0
[pid=8597] vsize: 127336
Current children cumulated CPU time (s) 647.65
Current children cumulated vsize (Kb) 129460

[startup+660.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 31675 0 0 0 65573 190 0 0 25 0 1 0 1785450077 130392064 29889 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 31834 29889 145 145 0 31689 0
[pid=8597] vsize: 127336
Current children cumulated CPU time (s) 657.64
Current children cumulated vsize (Kb) 129460

[startup+670.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 31675 0 0 0 66573 190 0 0 25 0 1 0 1785450077 130392064 29889 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 31834 29889 145 145 0 31689 0
[pid=8597] vsize: 127336
Current children cumulated CPU time (s) 667.64
Current children cumulated vsize (Kb) 129460

[startup+680.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 31675 0 0 0 67574 190 0 0 25 0 1 0 1785450077 130392064 29889 4294967295 134512640 135094434 3221224448 3221223120 134556252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 31834 29889 145 145 0 31689 0
[pid=8597] vsize: 127336
Current children cumulated CPU time (s) 677.65
Current children cumulated vsize (Kb) 129460

[startup+690.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 31675 0 0 0 68574 190 0 0 25 0 1 0 1785450077 130392064 29889 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 31834 29889 145 145 0 31689 0
[pid=8597] vsize: 127336
Current children cumulated CPU time (s) 687.65
Current children cumulated vsize (Kb) 129460

[startup+700.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 31675 0 0 0 69574 190 0 0 25 0 1 0 1785450077 130392064 29889 4294967295 134512640 135094434 3221224448 3221223120 134556291 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 31834 29889 145 145 0 31689 0
[pid=8597] vsize: 127336
Current children cumulated CPU time (s) 697.65
Current children cumulated vsize (Kb) 129460

[startup+710.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 32014 0 0 0 70569 192 0 0 25 0 1 0 1785450077 131780608 30228 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 32173 30228 145 145 0 32028 0
[pid=8597] vsize: 128692
Current children cumulated CPU time (s) 707.62
Current children cumulated vsize (Kb) 130816

[startup+720.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) T 8593 8593 30740 0 -1 0 32725 0 0 0 71558 198 0 0 25 0 1 0 1785450077 134692864 30939 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/8597/statm): 32884 30939 145 145 0 32739 0
[pid=8597] vsize: 131536
Current children cumulated CPU time (s) 717.57
Current children cumulated vsize (Kb) 133660

[startup+730.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 33412 0 0 0 72546 203 0 0 25 0 1 0 1785450077 137506816 31626 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 33571 31626 145 145 0 33426 0
[pid=8597] vsize: 134284
Current children cumulated CPU time (s) 727.5
Current children cumulated vsize (Kb) 136408

[startup+740.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 34137 0 0 0 73533 208 0 0 25 0 1 0 1785450077 140476416 32351 4294967295 134512640 135094434 3221224448 3221223040 134557360 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 34296 32351 145 145 0 34151 0
[pid=8597] vsize: 137184
Current children cumulated CPU time (s) 737.42
Current children cumulated vsize (Kb) 139308

[startup+750.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 34866 0 0 0 74520 214 0 0 25 0 1 0 1785450077 143470592 33080 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 35027 33080 145 145 0 34882 0
[pid=8597] vsize: 140108
Current children cumulated CPU time (s) 747.35
Current children cumulated vsize (Kb) 142232

[startup+760.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 35437 0 0 0 75510 218 0 0 25 0 1 0 1785450077 145809408 33651 4294967295 134512640 135094434 3221224448 3221223104 134558002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 35598 33651 145 145 0 35453 0
[pid=8597] vsize: 142392
Current children cumulated CPU time (s) 757.29
Current children cumulated vsize (Kb) 144516

[startup+770.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 35990 0 0 0 76500 222 0 0 25 0 1 0 1785450077 148070400 34204 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 36150 34204 145 145 0 36005 0
[pid=8597] vsize: 144600
Current children cumulated CPU time (s) 767.23
Current children cumulated vsize (Kb) 146724

[startup+780.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 36542 0 0 0 77489 227 0 0 25 0 1 0 1785450077 150331392 34756 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 36702 34756 145 145 0 36557 0
[pid=8597] vsize: 146808
Current children cumulated CPU time (s) 777.17
Current children cumulated vsize (Kb) 148932

[startup+790.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 37106 0 0 0 78478 231 0 0 25 0 1 0 1785450077 152641536 35320 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 37266 35320 145 145 0 37121 0
[pid=8597] vsize: 149064
Current children cumulated CPU time (s) 787.1
Current children cumulated vsize (Kb) 151188

[startup+800.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 37705 0 0 0 79467 236 0 0 25 0 1 0 1785450077 155103232 35919 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 37867 35919 145 145 0 37722 0
[pid=8597] vsize: 151468
Current children cumulated CPU time (s) 797.04
Current children cumulated vsize (Kb) 153592

[startup+810.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 38285 0 0 0 80455 240 0 0 25 0 1 0 1785450077 157503488 36499 4294967295 134512640 135094434 3221224448 3221223120 134556450 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 38453 36499 145 145 0 38308 0
[pid=8597] vsize: 153812
Current children cumulated CPU time (s) 806.96
Current children cumulated vsize (Kb) 155936

[startup+820.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 38904 0 0 0 81444 246 0 0 25 0 1 0 1785450077 160034816 37118 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 39071 37118 145 145 0 38926 0
[pid=8597] vsize: 156284
Current children cumulated CPU time (s) 816.91
Current children cumulated vsize (Kb) 158408

[startup+830.072 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) T 8593 8593 30740 0 -1 0 39430 0 0 0 82434 250 0 0 25 0 1 0 1785450077 162222080 37644 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/8597/statm): 39605 37644 145 145 0 39460 0
[pid=8597] vsize: 158420
Current children cumulated CPU time (s) 826.85
Current children cumulated vsize (Kb) 160544

[startup+840.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 40036 0 0 0 83425 253 0 0 25 0 1 0 1785450077 164700160 38250 4294967295 134512640 135094434 3221224448 3221223072 134562085 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 40210 38250 145 145 0 40065 0
[pid=8597] vsize: 160840
Current children cumulated CPU time (s) 836.79
Current children cumulated vsize (Kb) 162964

[startup+850.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 40570 0 0 0 84416 257 0 0 25 0 1 0 1785450077 166936576 38784 4294967295 134512640 135094434 3221224448 3221223040 134551908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 40756 38784 145 145 0 40611 0
[pid=8597] vsize: 163024
Current children cumulated CPU time (s) 846.74
Current children cumulated vsize (Kb) 165148

[startup+860.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 41152 0 0 0 85405 262 0 0 25 0 1 0 1785450077 169324544 39366 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 41339 39366 145 145 0 41194 0
[pid=8597] vsize: 165356
Current children cumulated CPU time (s) 856.68
Current children cumulated vsize (Kb) 167480

[startup+870.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 41657 0 0 0 86395 266 0 0 25 0 1 0 1785450077 171393024 39871 4294967295 134512640 135094434 3221224448 3221223084 134557639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 41844 39871 145 145 0 41699 0
[pid=8597] vsize: 167376
Current children cumulated CPU time (s) 866.62
Current children cumulated vsize (Kb) 169500

[startup+880.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 42146 0 0 0 87387 269 0 0 25 0 1 0 1785450077 173424640 40360 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 42340 40360 145 145 0 42195 0
[pid=8597] vsize: 169360
Current children cumulated CPU time (s) 876.57
Current children cumulated vsize (Kb) 171484

[startup+890.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 42643 0 0 0 88377 274 0 0 25 0 1 0 1785450077 175435776 40857 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 42831 40857 145 145 0 42686 0
[pid=8597] vsize: 171324
Current children cumulated CPU time (s) 886.52
Current children cumulated vsize (Kb) 173448

[startup+900.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 43099 0 0 0 89367 278 0 0 25 0 1 0 1785450077 177303552 41313 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 43287 41313 145 145 0 43142 0
[pid=8597] vsize: 173148
Current children cumulated CPU time (s) 896.46
Current children cumulated vsize (Kb) 175272

[startup+910.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 43555 0 0 0 90358 282 0 0 25 0 1 0 1785450077 179175424 41769 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 43744 41769 145 145 0 43599 0
[pid=8597] vsize: 174976
Current children cumulated CPU time (s) 906.41
Current children cumulated vsize (Kb) 177100

[startup+920.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 44001 0 0 0 91350 285 0 0 25 0 1 0 1785450077 181006336 42215 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 44191 42215 145 145 0 44046 0
[pid=8597] vsize: 176764
Current children cumulated CPU time (s) 916.36
Current children cumulated vsize (Kb) 178888

[startup+930.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 44532 0 0 0 92342 289 0 0 25 0 1 0 1785450077 183173120 42746 4294967295 134512640 135094434 3221224448 3221223040 134551682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 44720 42746 145 145 0 44575 0
[pid=8597] vsize: 178880
Current children cumulated CPU time (s) 926.32
Current children cumulated vsize (Kb) 181004

[startup+940.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 45132 0 0 0 93332 293 0 0 25 0 1 0 1785450077 185610240 43346 4294967295 134512640 135094434 3221224448 3221223040 134557375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 45315 43346 145 145 0 45170 0
[pid=8597] vsize: 181260
Current children cumulated CPU time (s) 936.26
Current children cumulated vsize (Kb) 183384

[startup+950.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 45738 0 0 0 94323 297 0 0 25 0 1 0 1785450077 188080128 43952 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 45918 43952 145 145 0 45773 0
[pid=8597] vsize: 183672
Current children cumulated CPU time (s) 946.21
Current children cumulated vsize (Kb) 185796

[startup+960.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 46343 0 0 0 95312 302 0 0 25 0 1 0 1785450077 190541824 44557 4294967295 134512640 135094434 3221224448 3221223040 134551702 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 46519 44557 145 145 0 46374 0
[pid=8597] vsize: 186076
Current children cumulated CPU time (s) 956.15
Current children cumulated vsize (Kb) 188200

[startup+970.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 46953 0 0 0 96300 307 0 0 25 0 1 0 1785450077 193019904 45167 4294967295 134512640 135094434 3221224448 3221223104 134557896 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 47124 45167 145 145 0 46979 0
[pid=8597] vsize: 188496
Current children cumulated CPU time (s) 966.08
Current children cumulated vsize (Kb) 190620

[startup+980.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 47641 0 0 0 97289 311 0 0 25 0 1 0 1785450077 195825664 45855 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 47809 45855 145 145 0 47664 0
[pid=8597] vsize: 191236
Current children cumulated CPU time (s) 976.01
Current children cumulated vsize (Kb) 193360

[startup+990.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 48412 0 0 0 98275 316 0 0 25 0 1 0 1785450077 198975488 46626 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 48578 46626 145 145 0 48433 0
[pid=8597] vsize: 194312
Current children cumulated CPU time (s) 985.92
Current children cumulated vsize (Kb) 196436

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 49162 0 0 0 99264 321 0 0 25 0 1 0 1785450077 203083776 47376 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 49581 47376 145 145 0 49436 0
[pid=8597] vsize: 198324
Current children cumulated CPU time (s) 995.86
Current children cumulated vsize (Kb) 200448

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 49767 0 0 0 100256 325 0 0 25 0 1 0 1785450077 205557760 47981 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 50185 47981 145 145 0 50040 0
[pid=8597] vsize: 200740
Current children cumulated CPU time (s) 1005.82
Current children cumulated vsize (Kb) 202864

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 49767 0 0 0 101255 326 0 0 25 0 1 0 1785450077 205557760 47981 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 50185 47981 145 145 0 50040 0
[pid=8597] vsize: 200740
Current children cumulated CPU time (s) 1015.82
Current children cumulated vsize (Kb) 202864

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 49767 0 0 0 102255 326 0 0 25 0 1 0 1785450077 205557760 47981 4294967295 134512640 135094434 3221224448 3221223104 134558181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 50185 47981 145 145 0 50040 0
[pid=8597] vsize: 200740
Current children cumulated CPU time (s) 1025.82
Current children cumulated vsize (Kb) 202864

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 49767 0 0 0 103254 327 0 0 25 0 1 0 1785450077 205557760 47981 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 50185 47981 145 145 0 50040 0
[pid=8597] vsize: 200740
Current children cumulated CPU time (s) 1035.82
Current children cumulated vsize (Kb) 202864

[startup+1050.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 49767 0 0 0 104253 328 0 0 25 0 1 0 1785450077 205557760 47981 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 50185 47981 145 145 0 50040 0
[pid=8597] vsize: 200740
Current children cumulated CPU time (s) 1045.82
Current children cumulated vsize (Kb) 202864

[startup+1060.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 49767 0 0 0 105253 328 0 0 25 0 1 0 1785450077 205557760 47981 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 50185 47981 145 145 0 50040 0
[pid=8597] vsize: 200740
Current children cumulated CPU time (s) 1055.82
Current children cumulated vsize (Kb) 202864

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 49767 0 0 0 106253 328 0 0 25 0 1 0 1785450077 205557760 47981 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 50185 47981 145 145 0 50040 0
[pid=8597] vsize: 200740
Current children cumulated CPU time (s) 1065.82
Current children cumulated vsize (Kb) 202864

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 49767 0 0 0 107252 329 0 0 25 0 1 0 1785450077 205557760 47981 4294967295 134512640 135094434 3221224448 3221223104 134557920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 50185 47981 145 145 0 50040 0
[pid=8597] vsize: 200740
Current children cumulated CPU time (s) 1075.82
Current children cumulated vsize (Kb) 202864

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 49767 0 0 0 108252 329 0 0 25 0 1 0 1785450077 205557760 47981 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 50185 47981 145 145 0 50040 0
[pid=8597] vsize: 200740
Current children cumulated CPU time (s) 1085.82
Current children cumulated vsize (Kb) 202864

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 49767 0 0 0 109252 329 0 0 25 0 1 0 1785450077 205557760 47981 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 50185 47981 145 145 0 50040 0
[pid=8597] vsize: 200740
Current children cumulated CPU time (s) 1095.82
Current children cumulated vsize (Kb) 202864

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 49767 0 0 0 110251 330 0 0 25 0 1 0 1785450077 205557760 47981 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 50185 47981 145 145 0 50040 0
[pid=8597] vsize: 200740
Current children cumulated CPU time (s) 1105.82
Current children cumulated vsize (Kb) 202864

[startup+1120.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 49767 0 0 0 111251 330 0 0 25 0 1 0 1785450077 205557760 47981 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 50185 47981 145 145 0 50040 0
[pid=8597] vsize: 200740
Current children cumulated CPU time (s) 1115.82
Current children cumulated vsize (Kb) 202864

[startup+1130.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 49767 0 0 0 112251 330 0 0 25 0 1 0 1785450077 205557760 47981 4294967295 134512640 135094434 3221224448 3221223120 134556288 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 50185 47981 145 145 0 50040 0
[pid=8597] vsize: 200740
Current children cumulated CPU time (s) 1125.82
Current children cumulated vsize (Kb) 202864

[startup+1140.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 49767 0 0 0 113251 330 0 0 25 0 1 0 1785450077 205557760 47981 4294967295 134512640 135094434 3221224448 3221223120 134556336 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 50185 47981 145 145 0 50040 0
[pid=8597] vsize: 200740
Current children cumulated CPU time (s) 1135.82
Current children cumulated vsize (Kb) 202864

[startup+1150.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 49767 0 0 0 114251 330 0 0 25 0 1 0 1785450077 205557760 47981 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 50185 47981 145 145 0 50040 0
[pid=8597] vsize: 200740
Current children cumulated CPU time (s) 1145.82
Current children cumulated vsize (Kb) 202864

[startup+1160.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 49767 0 0 0 115250 331 0 0 25 0 1 0 1785450077 205557760 47981 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 50185 47981 145 145 0 50040 0
[pid=8597] vsize: 200740
Current children cumulated CPU time (s) 1155.82
Current children cumulated vsize (Kb) 202864

[startup+1170.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 49767 0 0 0 116249 331 0 0 25 0 1 0 1785450077 205557760 47981 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8597/statm): 50185 47981 145 145 0 50040 0
[pid=8597] vsize: 200740
Current children cumulated CPU time (s) 1165.81
Current children cumulated vsize (Kb) 202864

[startup+1180.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 49767 0 0 0 117249 332 0 0 25 0 1 0 1785450077 205557760 47981 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 50185 47981 145 145 0 50040 0
[pid=8597] vsize: 200740
Current children cumulated CPU time (s) 1175.82
Current children cumulated vsize (Kb) 202864

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 49767 0 0 0 118250 332 0 0 25 0 1 0 1785450077 205557760 47981 4294967295 134512640 135094434 3221224448 3221223040 134557357 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 50185 47981 145 145 0 50040 0
[pid=8597] vsize: 200740
Current children cumulated CPU time (s) 1185.83
Current children cumulated vsize (Kb) 202864

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 49767 0 0 0 119250 332 0 0 25 0 1 0 1785450077 205557760 47981 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 50185 47981 145 145 0 50040 0
[pid=8597] vsize: 200740
Current children cumulated CPU time (s) 1195.83
Current children cumulated vsize (Kb) 202864

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 49767 0 0 0 120250 332 0 0 25 0 1 0 1785450077 205557760 47981 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 50185 47981 145 145 0 50040 0
[pid=8597] vsize: 200740
Current children cumulated CPU time (s) 1205.83
Current children cumulated vsize (Kb) 202864



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8597
Raw data (/proc/8593/stat): 8593 (minisat+_script) S 8592 8593 30740 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1785450072 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8593/statm): 531 226 485 147 0 384 0
[pid=8593] vsize: 2124
Raw data (/proc/8597/stat): 8597 (minisat+_64-bit) R 8593 8593 30740 0 -1 0 49767 0 0 0 120250 332 0 0 25 0 1 0 1785450077 205557760 47981 4294967295 134512640 135094434 3221224448 3221223136 134554685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8597/statm): 50185 47981 145 145 0 50040 0
[pid=8597] vsize: 200740
Current children cumulated CPU time (s) 1205.83
Current children cumulated vsize (Kb) 202864

Sending SIGTERM to -8593
Sleeping 2 seconds
One traced child (pid=8593) ended because it received signal 15 (SIGTERM)
One traced child (pid=8597) exited with status: 10
All traced children have exited ! Game is over.

Child status: 10
Real time (s): 1210.21
CPU time (s): 1205.92
CPU user time (s): 1202.51
CPU system time (s): 3.41148
CPU usage (%): 99.6457
Max. virtual memory (cumulated for all children) (Kb): 202864

Verifier Data

ERROR: no interpretation found !