Name | mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-danoint.opb |
MD5SUM | cdd5642b047e784e87a00fe758efc418 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 30 |
Biggest coefficient in the objective function | 536870912 |
Number of bits for the biggest coefficient in the objective function | 30 |
Sum of the numbers in the objective function | 1073741823 |
Number of bits of the sum of numbers in the objective function | 30 |
Biggest number in a constraint | 13421772800 |
Number of bits of the biggest number in a constraint | 34 |
Biggest sum of numbers in a constraint | 53690300878 |
Number of bits of the biggest sum of numbers | 36 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 13898 |
Total number of constraints | 728 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 72 |
Number of constraints which are nor clauses,nor cardinality constraints | 656 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 1500 |
LAUNCH ON wulflinc9 THE 2005-09-19 17:45:47 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2966 boxname=wulflinc9 idbench=622 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: cdd5642b047e784e87a00fe758efc418 /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-20-10-danoint.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-20-10-danoint.opb IDLAUNCH: 2966 /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: 878352 kB Buffers: 36800 kB Cached: 92784 kB SwapCached: 1044 kB Active: 65548 kB Inactive: 66796 kB HighTotal: 131008 kB HighFree: 42560 kB LowTotal: 903652 kB LowFree: 835792 kB SwapTotal: 2097136 kB SwapFree: 2095568 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5664 kB Slab: 18408 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-19 18:05:57 (client local time) WITH STATUS 0 IN 1207.59 SECONDS stats: 2966 7 1207.59 0
c Parsing PB file... c Converting 816 PB-constraints to clauses... c -- Unit propagations: pppppppp c -- Detecting intervals from adjacent constraints: ################################################################################################################################################ c -- Clauses(.)/Splits(s): sssssssssssssssssss c ---[ 833]---> BDD-cost: 15 c ---[ 832]---> BDD-cost: 16 c ---[ 831]---> BDD-cost: 16 c ---[ 828]---> BDD-cost: 16 c ---[ 827]---> BDD-cost: 16 c ---[ 825]---> Adder-cost: 400 maxlim: 645113 bits: 21/20 c ---[ 823]---> Adder-cost: 400 maxlim: 648185 bits: 21/20 c ---[ 821]---> Adder-cost: 394 maxlim: 707577 bits: 21/20 c ---[ 819]---> Adder-cost: 394 maxlim: 708601 bits: 21/20 c ---[ 817]---> Adder-cost: 394 maxlim: 707577 bits: 21/20 c ---[ 815]---> Adder-cost: 400 maxlim: 649209 bits: 21/20 c ---[ 813]---> Adder-cost: 394 maxlim: 707577 bits: 21/20 c ---[ 811]---> Adder-cost: 408 maxlim: 903161 bits: 21/20 c ---[ 809]---> Adder-cost: 408 maxlim: 902137 bits: 21/20 c ---[ 807]---> Adder-cost: 408 maxlim: 904185 bits: 21/20 c ---[ 805]---> Adder-cost: 408 maxlim: 905209 bits: 21/20 c ---[ 803]---> Adder-cost: 408 maxlim: 908281 bits: 21/20 c ---[ 801]---> Adder-cost: 408 maxlim: 908281 bits: 21/20 c ---[ 799]---> Adder-cost: 408 maxlim: 908281 bits: 21/20 c ---[ 797]---> Adder-cost: 384 maxlim: 445433 bits: 20/19 c ---[ 795]---> Adder-cost: 384 maxlim: 449529 bits: 20/19 c ---[ 793]---> Adder-cost: 384 maxlim: 447481 bits: 20/19 c ---[ 791]---> Adder-cost: 384 maxlim: 452601 bits: 20/19 c ---[ 789]---> Adder-cost: 384 maxlim: 453625 bits: 20/19 c ---[ 787]---> Adder-cost: 384 maxlim: 447481 bits: 20/19 c ---[ 785]---> Adder-cost: 384 maxlim: 450553 bits: 20/19 c ---[ 783]---> Adder-cost: 384 maxlim: 451577 bits: 20/19 c ---[ 781]---> Adder-cost: 384 maxlim: 450553 bits: 20/19 c ---[ 779]---> Adder-cost: 384 maxlim: 443385 bits: 20/19 c ---[ 777]---> Adder-cost: 384 maxlim: 451577 bits: 20/19 c ---[ 775]---> Adder-cost: 384 maxlim: 452601 bits: 20/19 c ---[ 773]---> Adder-cost: 384 maxlim: 447481 bits: 20/19 c ---[ 771]---> Adder-cost: 384 maxlim: 449529 bits: 20/19 c ---[ 769]---> Adder-cost: 402 maxlim: 712697 bits: 21/20 c ---[ 767]---> Adder-cost: 394 maxlim: 774137 bits: 21/20 c ---[ 765]---> Adder-cost: 394 maxlim: 774137 bits: 21/20 c ---[ 763]---> Adder-cost: 402 maxlim: 711673 bits: 21/20 c ---[ 761]---> Adder-cost: 402 maxlim: 711673 bits: 21/20 c ---[ 759]---> Adder-cost: 394 maxlim: 772089 bits: 21/20 c ---[ 757]---> Adder-cost: 402 maxlim: 709625 bits: 21/20 c ---[ 755]---> Adder-cost: 395 maxlim: 519161 bits: 20/19 c ---[ 753]---> Adder-cost: 386 maxlim: 578553 bits: 20/20 c ---[ 751]---> Adder-cost: 386 maxlim: 578553 bits: 20/20 c ---[ 749]---> Adder-cost: 386 maxlim: 582649 bits: 20/20 c ---[ 747]---> Adder-cost: 386 maxlim: 580601 bits: 20/20 c ---[ 745]---> Adder-cost: 386 maxlim: 574457 bits: 20/20 c ---[ 743]---> Adder-cost: 386 maxlim: 577529 bits: 20/20 c ---[ 741]---> Adder-cost: 384 maxlim: 518137 bits: 20/19 c ---[ 739]---> Adder-cost: 384 maxlim: 515065 bits: 20/19 c ---[ 737]---> Adder-cost: 384 maxlim: 517113 bits: 20/19 c ---[ 735]---> Adder-cost: 384 maxlim: 509945 bits: 20/19 c ---[ 733]---> Adder-cost: 384 maxlim: 514041 bits: 20/19 c ---[ 731]---> Adder-cost: 384 maxlim: 511993 bits: 20/19 c ---[ 729]---> Adder-cost: 384 maxlim: 517113 bits: 20/19 c ---[ 727]---> Adder-cost: 384 maxlim: 447481 bits: 20/19 c ---[ 725]---> Adder-cost: 384 maxlim: 451577 bits: 20/19 c ---[ 723]---> Adder-cost: 384 maxlim: 450553 bits: 20/19 c ---[ 721]---> Adder-cost: 384 maxlim: 452601 bits: 20/19 c ---[ 719]---> Adder-cost: 384 maxlim: 448505 bits: 20/19 c ---[ 717]---> Adder-cost: 384 maxlim: 453625 bits: 20/19 c ---[ 715]---> Adder-cost: 384 maxlim: 444409 bits: 20/19 c ---[ 714]---> BDD-cost: 145 c ---[ 713]---> BDD-cost: 145 c ---[ 712]---> BDD-cost: 145 c ---[ 711]---> BDD-cost: 145 c ---[ 710]---> BDD-cost: 145 c ---[ 709]---> BDD-cost: 145 c ---[ 708]---> BDD-cost: 145 c ---[ 707]---> BDD-cost: 145 c ---[ 706]---> BDD-cost: 145 c ---[ 705]---> BDD-cost: 145 c ---[ 704]---> BDD-cost: 145 c ---[ 703]---> BDD-cost: 145 c ---[ 702]---> BDD-cost: 145 c ---[ 701]---> BDD-cost: 145 c ---[ 700]---> BDD-cost: 145 c ---[ 699]---> BDD-cost: 145 c ---[ 698]---> BDD-cost: 145 c ---[ 697]---> BDD-cost: 145 c ---[ 696]---> BDD-cost: 145 c ---[ 695]---> BDD-cost: 145 c ---[ 694]---> BDD-cost: 145 c ---[ 693]---> BDD-cost: 145 c ---[ 692]---> BDD-cost: 145 c ---[ 691]---> BDD-cost: 145 c ---[ 690]---> BDD-cost: 145 c ---[ 689]---> BDD-cost: 145 c ---[ 688]---> BDD-cost: 145 c ---[ 687]---> BDD-cost: 145 c ---[ 686]---> BDD-cost: 145 c ---[ 685]---> BDD-cost: 145 c ---[ 684]---> BDD-cost: 145 c ---[ 683]---> BDD-cost: 145 c ---[ 682]---> BDD-cost: 145 c ---[ 681]---> BDD-cost: 145 c ---[ 680]---> BDD-cost: 145 c ---[ 679]---> BDD-cost: 145 c ---[ 678]---> BDD-cost: 145 c ---[ 677]---> BDD-cost: 145 c ---[ 676]---> BDD-cost: 145 c ---[ 675]---> BDD-cost: 145 c ---[ 674]---> BDD-cost: 145 c ---[ 673]---> BDD-cost: 145 c ---[ 672]---> BDD-cost: 145 c ---[ 671]---> BDD-cost: 145 c ---[ 670]---> BDD-cost: 145 c ---[ 669]---> BDD-cost: 145 c ---[ 668]---> BDD-cost: 145 c ---[ 667]---> BDD-cost: 145 c ---[ 666]---> BDD-cost: 145 c ---[ 665]---> BDD-cost: 145 c ---[ 664]---> BDD-cost: 145 c ---[ 663]---> BDD-cost: 145 c ---[ 662]---> BDD-cost: 145 c ---[ 661]---> BDD-cost: 145 c ---[ 660]---> BDD-cost: 145 c ---[ 659]---> BDD-cost: 145 c ---[ 657]---> Sorter-cost: 2151 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 655]---> Sorter-cost: 2183 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 653]---> Sorter-cost: 2183 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 651]---> Sorter-cost: 2151 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 649]---> Sorter-cost: 2151 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 647]---> Sorter-cost: 2183 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 645]---> Sorter-cost: 2183 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 643]---> Sorter-cost: 2099 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 641]---> Sorter-cost: 2127 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 639]---> Sorter-cost: 2127 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 637]---> Sorter-cost: 2127 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 635]---> Sorter-cost: 2127 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 633]---> Sorter-cost: 2127 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 631]---> Sorter-cost: 2127 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 629]---> Sorter-cost: 2099 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 627]---> Sorter-cost: 2099 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 625]---> Sorter-cost: 2127 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 623]---> Sorter-cost: 2127 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 621]---> Sorter-cost: 2127 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 619]---> Sorter-cost: 2127 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 617]---> Sorter-cost: 2127 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 615]---> Sorter-cost: 2127 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 613]---> Sorter-cost: 2099 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 611]---> Sorter-cost: 2127 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 609]---> Sorter-cost: 2099 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 607]---> Sorter-cost: 2127 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 605]---> Sorter-cost: 2127 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 603]---> Sorter-cost: 2127 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 601]---> Sorter-cost: 2127 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 599]---> Sorter-cost: 2099 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 597]---> Sorter-cost: 2127 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 595]---> Sorter-cost: 2127 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 593]---> Sorter-cost: 2127 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 591]---> Sorter-cost: 2127 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 589]---> Sorter-cost: 2127 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 587]---> Sorter-cost: 2151 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 585]---> Sorter-cost: 2127 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 583]---> Sorter-cost: 2151 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 581]---> Sorter-cost: 2151 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 579]---> Sorter-cost: 2127 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 577]---> Sorter-cost: 2151 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 575]---> Sorter-cost: 2151 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 573]---> Sorter-cost: 2127 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 571]---> Sorter-cost: 2127 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 569]---> Sorter-cost: 2151 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 567]---> Sorter-cost: 2151 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 565]---> Sorter-cost: 2151 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 563]---> Sorter-cost: 2151 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 561]---> Sorter-cost: 2151 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 559]---> Sorter-cost: 2127 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 557]---> Sorter-cost: 2099 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 555]---> Sorter-cost: 2127 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 553]---> Sorter-cost: 2127 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 551]---> Sorter-cost: 2099 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 549]---> Sorter-cost: 2127 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 547]---> Sorter-cost: 2127 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 545]---> Adder-cost: 1495 maxlim: 8388607 bits: 24/23 c ---[ 543]---> Adder-cost: 1507 maxlim: 8388607 bits: 24/23 c ---[ 541]---> Adder-cost: 1419 maxlim: 4194303 bits: 23/22 c ---[ 539]---> Adder-cost: 1419 maxlim: 4194303 bits: 23/22 c ---[ 537]---> Adder-cost: 1438 maxlim: 8388607 bits: 24/23 c ---[ 535]---> Adder-cost: 1403 maxlim: 4194303 bits: 23/22 c ---[ 533]---> Adder-cost: 1395 maxlim: 4194303 bits: 23/22 c ---[ 531]---> Adder-cost: 1387 maxlim: 4194303 bits: 23/22 c ---[ 529]---> BDD-cost: 15 c ---[ 527]---> BDD-cost: 15 c ---[ 525]---> BDD-cost: 15 c ---[ 523]---> BDD-cost: 15 c ---[ 521]---> BDD-cost: 15 c ---[ 519]---> BDD-cost: 15 c ---[ 517]---> BDD-cost: 15 c ---[ 515]---> BDD-cost: 15 c ---[ 513]---> BDD-cost: 15 c ---[ 511]---> BDD-cost: 15 c ---[ 509]---> BDD-cost: 15 c ---[ 507]---> BDD-cost: 15 c ---[ 505]---> BDD-cost: 15 c ---[ 503]---> BDD-cost: 15 c ---[ 501]---> BDD-cost: 15 c ---[ 499]---> BDD-cost: 15 c ---[ 498]---> Sorter-cost: 1899 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 497]---> Sorter-cost: 1923 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 496]---> Sorter-cost: 1725 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 495]---> Sorter-cost: 1690 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 494]---> Sorter-cost: 1725 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 493]---> Sorter-cost: 1899 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 492]---> Sorter-cost: 1725 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 491]---> Sorter-cost: 1912 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 490]---> Sorter-cost: 1936 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 489]---> Sorter-cost: 1923 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 488]---> Sorter-cost: 1888 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 487]---> Sorter-cost: 1910 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 486]---> Sorter-cost: 1910 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 485]---> Sorter-cost: 1910 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 484]---> Sorter-cost: 1803 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 483]---> Sorter-cost: 1790 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 482]---> Sorter-cost: 1803 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 481]---> Sorter-cost: 1779 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 480]---> Sorter-cost: 1790 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 479]---> Sorter-cost: 1803 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 478]---> Sorter-cost: 1744 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 477]---> Sorter-cost: 1803 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 476]---> Sorter-cost: 1744 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 475]---> Sorter-cost: 1816 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 474]---> Sorter-cost: 1803 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 473]---> Sorter-cost: 1779 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 472]---> Sorter-cost: 1803 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 471]---> Sorter-cost: 1790 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 470]---> Sorter-cost: 1864 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 469]---> Sorter-cost: 1690 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 468]---> Sorter-cost: 1690 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 467]---> Sorter-cost: 1910 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 466]---> Sorter-cost: 1910 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 465]---> Sorter-cost: 1714 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 464]---> Sorter-cost: 1923 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 463]---> Sorter-cost: 1910 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 462]---> Sorter-cost: 1725 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 461]---> Sorter-cost: 1725 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 460]---> Sorter-cost: 1725 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 459]---> Sorter-cost: 1712 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 458]---> Sorter-cost: 1738 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 457]---> Sorter-cost: 1690 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 456]---> Sorter-cost: 1701 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 455]---> Sorter-cost: 1712 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 454]---> Sorter-cost: 1725 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 453]---> Sorter-cost: 1714 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 452]---> Sorter-cost: 1701 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 451]---> Sorter-cost: 1690 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 450]---> Sorter-cost: 1725 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 449]---> Sorter-cost: 1803 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 448]---> Sorter-cost: 1803 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 447]---> Sorter-cost: 1744 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 446]---> Sorter-cost: 1779 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 445]---> Sorter-cost: 1779 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 444]---> Sorter-cost: 1790 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 443]---> Sorter-cost: 1792 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 441]---> Sorter-cost: 2323 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 439]---> Sorter-cost: 2324 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 437]---> Sorter-cost: 2322 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 435]---> Sorter-cost: 2322 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 433]---> Sorter-cost: 2324 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 431]---> Sorter-cost: 2323 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 429]---> Sorter-cost: 2322 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 427]---> Sorter-cost: 2322 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 410]---> BDD-cost: 25 c ---[ 409]---> BDD-cost: 25 c ---[ 408]---> BDD-cost: 25 c ---[ 407]---> BDD-cost: 25 c ---[ 406]---> BDD-cost: 25 c ---[ 405]---> BDD-cost: 25 c ---[ 404]---> BDD-cost: 25 c ---[ 403]---> BDD-cost: 18 c ---[ 402]---> BDD-cost: 18 c ---[ 401]---> BDD-cost: 18 c ---[ 400]---> BDD-cost: 18 c ---[ 399]---> BDD-cost: 18 c ---[ 398]---> BDD-cost: 18 c ---[ 397]---> BDD-cost: 25 c ---[ 396]---> BDD-cost: 25 c ---[ 395]---> BDD-cost: 25 c ---[ 394]---> BDD-cost: 25 c ---[ 393]---> BDD-cost: 25 c ---[ 392]---> BDD-cost: 25 c ---[ 391]---> BDD-cost: 22 c ---[ 390]---> BDD-cost: 22 c ---[ 389]---> BDD-cost: 22 c ---[ 388]---> BDD-cost: 22 c ---[ 387]---> BDD-cost: 22 c ---[ 386]---> BDD-cost: 22 c ---[ 385]---> BDD-cost: 21 c ---[ 384]---> BDD-cost: 21 c ---[ 383]---> BDD-cost: 21 c ---[ 382]---> BDD-cost: 21 c ---[ 381]---> BDD-cost: 21 c ---[ 380]---> BDD-cost: 21 c ---[ 379]---> BDD-cost: 22 c ---[ 378]---> BDD-cost: 22 c ---[ 377]---> BDD-cost: 22 c ---[ 376]---> BDD-cost: 22 c ---[ 375]---> BDD-cost: 22 c ---[ 374]---> BDD-cost: 22 c ---[ 373]---> BDD-cost: 25 c ---[ 372]---> BDD-cost: 25 c ---[ 371]---> BDD-cost: 25 c ---[ 370]---> BDD-cost: 25 c ---[ 369]---> BDD-cost: 25 c ---[ 368]---> BDD-cost: 25 c ---[ 367]---> BDD-cost: 22 c ---[ 366]---> BDD-cost: 22 c ---[ 365]---> BDD-cost: 22 c ---[ 364]---> BDD-cost: 22 c ---[ 363]---> BDD-cost: 22 c ---[ 362]---> BDD-cost: 22 c ---[ 361]---> BDD-cost: 25 c ---[ 360]---> BDD-cost: 25 c ---[ 359]---> BDD-cost: 25 c ---[ 358]---> BDD-cost: 25 c ---[ 357]---> BDD-cost: 25 c ---[ 356]---> BDD-cost: 25 c ---[ 355]---> BDD-cost: 25 c ---[ 354]---> BDD-cost: 25 c ---[ 353]---> BDD-cost: 25 c ---[ 352]---> BDD-cost: 25 c ---[ 351]---> BDD-cost: 25 c ---[ 350]---> BDD-cost: 25 c ---[ 349]---> BDD-cost: 25 c ---[ 348]---> BDD-cost: 23 c ---[ 347]---> BDD-cost: 23 c ---[ 346]---> BDD-cost: 23 c ---[ 345]---> BDD-cost: 23 c ---[ 344]---> BDD-cost: 23 c ---[ 343]---> BDD-cost: 23 c ---[ 342]---> BDD-cost: 25 c ---[ 341]---> BDD-cost: 25 c ---[ 340]---> BDD-cost: 25 c ---[ 339]---> BDD-cost: 25 c ---[ 338]---> BDD-cost: 25 c ---[ 337]---> BDD-cost: 25 c ---[ 336]---> BDD-cost: 25 c ---[ 335]---> BDD-cost: 25 c ---[ 334]---> BDD-cost: 25 c ---[ 333]---> BDD-cost: 25 c ---[ 332]---> BDD-cost: 25 c ---[ 331]---> BDD-cost: 25 c ---[ 330]---> BDD-cost: 25 c ---[ 329]---> BDD-cost: 25 c ---[ 328]---> BDD-cost: 25 c ---[ 327]---> BDD-cost: 25 c ---[ 326]---> BDD-cost: 25 c ---[ 325]---> BDD-cost: 25 c ---[ 324]---> BDD-cost: 25 c ---[ 323]---> BDD-cost: 25 c ---[ 322]---> BDD-cost: 25 c ---[ 321]---> BDD-cost: 25 c ---[ 320]---> BDD-cost: 25 c ---[ 319]---> BDD-cost: 25 c ---[ 318]---> BDD-cost: 25 c ---[ 317]---> BDD-cost: 25 c ---[ 316]---> BDD-cost: 25 c ---[ 315]---> BDD-cost: 25 c ---[ 314]---> BDD-cost: 25 c ---[ 313]---> BDD-cost: 25 c ---[ 312]---> BDD-cost: 21 c ---[ 311]---> BDD-cost: 21 c ---[ 310]---> BDD-cost: 21 c ---[ 309]---> BDD-cost: 21 c ---[ 308]---> BDD-cost: 21 c ---[ 307]---> BDD-cost: 21 c ---[ 306]---> BDD-cost: 21 c ---[ 305]---> BDD-cost: 21 c ---[ 304]---> BDD-cost: 21 c ---[ 303]---> BDD-cost: 21 c ---[ 302]---> BDD-cost: 21 c ---[ 301]---> BDD-cost: 21 c ---[ 300]---> BDD-cost: 22 c ---[ 299]---> BDD-cost: 22 c ---[ 298]---> BDD-cost: 22 c ---[ 297]---> BDD-cost: 22 c ---[ 296]---> BDD-cost: 22 c ---[ 295]---> BDD-cost: 22 c ---[ 294]---> BDD-cost: 22 c ---[ 293]---> BDD-cost: 20 c ---[ 292]---> BDD-cost: 20 c ---[ 291]---> BDD-cost: 20 c ---[ 290]---> BDD-cost: 20 c ---[ 289]---> BDD-cost: 20 c ---[ 288]---> BDD-cost: 20 c ---[ 287]---> BDD-cost: 22 c ---[ 286]---> BDD-cost: 22 c ---[ 285]---> BDD-cost: 22 c ---[ 284]---> BDD-cost: 22 c ---[ 283]---> BDD-cost: 22 c ---[ 282]---> BDD-cost: 22 c ---[ 281]---> BDD-cost: 21 c ---[ 280]---> BDD-cost: 21 c ---[ 279]---> BDD-cost: 21 c ---[ 278]---> BDD-cost: 21 c ---[ 277]---> BDD-cost: 21 c ---[ 276]---> BDD-cost: 21 c ---[ 275]---> BDD-cost: 20 c ---[ 274]---> BDD-cost: 20 c ---[ 273]---> BDD-cost: 20 c ---[ 272]---> BDD-cost: 20 c ---[ 271]---> BDD-cost: 20 c ---[ 270]---> BDD-cost: 20 c ---[ 269]---> BDD-cost: 22 c ---[ 268]---> BDD-cost: 22 c ---[ 267]---> BDD-cost: 22 c ---[ 266]---> BDD-cost: 22 c ---[ 265]---> BDD-cost: 22 c ---[ 264]---> BDD-cost: 22 c ---[ 263]---> BDD-cost: 19 c ---[ 262]---> BDD-cost: 19 c ---[ 261]---> BDD-cost: 19 c ---[ 260]---> BDD-cost: 19 c ---[ 259]---> BDD-cost: 19 c ---[ 258]---> BDD-cost: 19 c ---[ 257]---> BDD-cost: 22 c ---[ 256]---> BDD-cost: 22 c ---[ 255]---> BDD-cost: 22 c ---[ 254]---> BDD-cost: 22 c ---[ 253]---> BDD-cost: 22 c ---[ 252]---> BDD-cost: 22 c ---[ 251]---> BDD-cost: 18 c ---[ 250]---> BDD-cost: 18 c ---[ 249]---> BDD-cost: 18 c ---[ 248]---> BDD-cost: 18 c ---[ 247]---> BDD-cost: 18 c ---[ 246]---> BDD-cost: 18 c ---[ 245]---> BDD-cost: 22 c ---[ 244]---> BDD-cost: 22 c ---[ 243]---> BDD-cost: 22 c ---[ 242]---> BDD-cost: 22 c ---[ 241]---> BDD-cost: 22 c ---[ 240]---> BDD-cost: 22 c ---[ 239]---> BDD-cost: 22 c ---[ 238]---> BDD-cost: 19 c ---[ 237]---> BDD-cost: 19 c ---[ 236]---> BDD-cost: 19 c ---[ 235]---> BDD-cost: 19 c ---[ 234]---> BDD-cost: 19 c ---[ 233]---> BDD-cost: 19 c ---[ 232]---> BDD-cost: 22 c ---[ 231]---> BDD-cost: 22 c ---[ 230]---> BDD-cost: 22 c ---[ 229]---> BDD-cost: 22 c ---[ 228]---> BDD-cost: 22 c ---[ 227]---> BDD-cost: 22 c ---[ 226]---> BDD-cost: 20 c ---[ 225]---> BDD-cost: 20 c ---[ 224]---> BDD-cost: 20 c ---[ 223]---> BDD-cost: 20 c ---[ 222]---> BDD-cost: 20 c ---[ 221]---> BDD-cost: 20 c ---[ 220]---> BDD-cost: 21 c ---[ 219]---> BDD-cost: 21 c ---[ 218]---> BDD-cost: 21 c ---[ 217]---> BDD-cost: 21 c ---[ 216]---> BDD-cost: 21 c ---[ 215]---> BDD-cost: 21 c ---[ 214]---> BDD-cost: 25 c ---[ 213]---> BDD-cost: 25 c ---[ 212]---> BDD-cost: 25 c ---[ 211]---> BDD-cost: 25 c ---[ 210]---> BDD-cost: 25 c ---[ 209]---> BDD-cost: 25 c ---[ 208]---> BDD-cost: 22 c ---[ 207]---> BDD-cost: 22 c ---[ 206]---> BDD-cost: 22 c ---[ 205]---> BDD-cost: 22 c ---[ 204]---> BDD-cost: 22 c ---[ 203]---> BDD-cost: 22 c ---[ 202]---> BDD-cost: 22 c ---[ 201]---> BDD-cost: 22 c ---[ 200]---> BDD-cost: 22 c ---[ 199]---> BDD-cost: 22 c ---[ 198]---> BDD-cost: 22 c ---[ 197]---> BDD-cost: 22 c ---[ 196]---> BDD-cost: 23 c ---[ 195]---> BDD-cost: 23 c ---[ 194]---> BDD-cost: 23 c ---[ 193]---> BDD-cost: 23 c ---[ 192]---> BDD-cost: 23 c ---[ 191]---> BDD-cost: 23 c ---[ 190]---> BDD-cost: 25 c ---[ 189]---> BDD-cost: 25 c ---[ 188]---> BDD-cost: 25 c ---[ 187]---> BDD-cost: 25 c ---[ 186]---> BDD-cost: 25 c ---[ 185]---> BDD-cost: 25 c ---[ 184]---> BDD-cost: 25 c ---[ 183]---> BDD-cost: 23 c ---[ 182]---> BDD-cost: 23 c ---[ 181]---> BDD-cost: 23 c ---[ 180]---> BDD-cost: 23 c ---[ 179]---> BDD-cost: 23 c ---[ 178]---> BDD-cost: 23 c ---[ 177]---> BDD-cost: 22 c ---[ 176]---> BDD-cost: 22 c ---[ 175]---> BDD-cost: 22 c ---[ 174]---> BDD-cost: 22 c ---[ 173]---> BDD-cost: 22 c ---[ 172]---> BDD-cost: 22 c ---[ 171]---> BDD-cost: 18 c ---[ 170]---> BDD-cost: 18 c ---[ 169]---> BDD-cost: 18 c ---[ 168]---> BDD-cost: 18 c ---[ 167]---> BDD-cost: 18 c ---[ 166]---> BDD-cost: 18 c ---[ 165]---> BDD-cost: 24 c ---[ 164]---> BDD-cost: 24 c ---[ 163]---> BDD-cost: 24 c ---[ 162]---> BDD-cost: 24 c ---[ 161]---> BDD-cost: 24 c ---[ 160]---> BDD-cost: 24 c ---[ 159]---> BDD-cost: 22 c ---[ 158]---> BDD-cost: 22 c ---[ 157]---> BDD-cost: 22 c ---[ 156]---> BDD-cost: 22 c ---[ 155]---> BDD-cost: 22 c ---[ 154]---> BDD-cost: 22 c ---[ 153]---> BDD-cost: 22 c ---[ 152]---> BDD-cost: 22 c ---[ 151]---> BDD-cost: 22 c ---[ 150]---> BDD-cost: 22 c ---[ 149]---> BDD-cost: 22 c ---[ 148]---> BDD-cost: 22 c ---[ 147]---> BDD-cost: 22 c ---[ 146]---> BDD-cost: 22 c ---[ 145]---> BDD-cost: 22 c ---[ 144]---> BDD-cost: 22 c ---[ 143]---> BDD-cost: 22 c ---[ 142]---> BDD-cost: 22 c ---[ 141]---> BDD-cost: 22 c ---[ 140]---> BDD-cost: 22 c ---[ 139]---> BDD-cost: 22 c ---[ 138]---> BDD-cost: 22 c ---[ 137]---> BDD-cost: 22 c ---[ 136]---> BDD-cost: 22 c ---[ 135]---> BDD-cost: 25 c ---[ 134]---> BDD-cost: 25 c ---[ 133]---> BDD-cost: 25 c ---[ 132]---> BDD-cost: 25 c ---[ 131]---> BDD-cost: 25 c ---[ 130]---> BDD-cost: 25 c ---[ 129]---> BDD-cost: 25 c ---[ 128]---> BDD-cost: 22 c ---[ 127]---> BDD-cost: 22 c ---[ 126]---> BDD-cost: 22 c ---[ 125]---> BDD-cost: 22 c ---[ 124]---> BDD-cost: 22 c ---[ 123]---> BDD-cost: 22 c ---[ 122]---> BDD-cost: 21 c ---[ 121]---> BDD-cost: 21 c ---[ 120]---> BDD-cost: 21 c ---[ 119]---> BDD-cost: 21 c ---[ 118]---> BDD-cost: 21 c ---[ 117]---> BDD-cost: 21 c ---[ 116]---> BDD-cost: 22 c ---[ 115]---> BDD-cost: 22 c ---[ 114]---> BDD-cost: 22 c ---[ 113]---> BDD-cost: 22 c ---[ 112]---> BDD-cost: 22 c ---[ 111]---> BDD-cost: 22 c ---[ 110]---> BDD-cost: 19 c ---[ 109]---> BDD-cost: 19 c ---[ 108]---> BDD-cost: 19 c ---[ 107]---> BDD-cost: 19 c ---[ 106]---> BDD-cost: 19 c ---[ 105]---> BDD-cost: 19 c ---[ 104]---> BDD-cost: 21 c ---[ 103]---> BDD-cost: 21 c ---[ 102]---> BDD-cost: 21 c ---[ 101]---> BDD-cost: 21 c ---[ 100]---> BDD-cost: 21 c ---[ 99]---> BDD-cost: 21 c ---[ 98]---> BDD-cost: 22 c ---[ 97]---> BDD-cost: 22 c ---[ 96]---> BDD-cost: 22 c ---[ 95]---> BDD-cost: 22 c ---[ 94]---> BDD-cost: 22 c ---[ 93]---> BDD-cost: 22 c ---[ 92]---> BDD-cost: 22 c ---[ 91]---> BDD-cost: 22 c ---[ 90]---> BDD-cost: 22 c ---[ 89]---> BDD-cost: 22 c ---[ 88]---> BDD-cost: 22 c ---[ 87]---> BDD-cost: 22 c ---[ 86]---> BDD-cost: 22 c ---[ 85]---> BDD-cost: 22 c ---[ 84]---> BDD-cost: 22 c ---[ 83]---> BDD-cost: 22 c ---[ 82]---> BDD-cost: 22 c ---[ 81]---> BDD-cost: 22 c ---[ 80]---> BDD-cost: 24 c ---[ 79]---> BDD-cost: 24 c ---[ 78]---> BDD-cost: 24 c ---[ 77]---> BDD-cost: 24 c ---[ 76]---> BDD-cost: 24 c ---[ 75]---> BDD-cost: 24 c ---[ 74]---> BDD-cost: 24 c ---[ 73]---> BDD-cost: 21 c ---[ 72]---> BDD-cost: 21 c ---[ 71]---> BDD-cost: 21 c ---[ 70]---> BDD-cost: 21 c ---[ 69]---> BDD-cost: 21 c ---[ 68]---> BDD-cost: 21 c ---[ 67]---> BDD-cost: 21 c ---[ 66]---> BDD-cost: 21 c ---[ 65]---> BDD-cost: 21 c ---[ 64]---> BDD-cost: 21 c ---[ 63]---> BDD-cost: 21 c ---[ 62]---> BDD-cost: 21 c ---[ 61]---> BDD-cost: 21 c ---[ 60]---> BDD-cost: 21 c ---[ 59]---> BDD-cost: 21 c ---[ 58]---> BDD-cost: 21 c ---[ 57]---> BDD-cost: 21 c ---[ 56]---> BDD-cost: 21 c ---[ 55]---> BDD-cost: 22 c ---[ 54]---> BDD-cost: 22 c ---[ 53]---> BDD-cost: 22 c ---[ 52]---> BDD-cost: 22 c ---[ 51]---> BDD-cost: 22 c ---[ 50]---> BDD-cost: 22 c ---[ 49]---> BDD-cost: 22 c ---[ 48]---> BDD-cost: 22 c ---[ 47]---> BDD-cost: 22 c ---[ 46]---> BDD-cost: 22 c ---[ 45]---> BDD-cost: 22 c ---[ 44]---> BDD-cost: 22 c ---[ 43]---> BDD-cost: 22 c ---[ 42]---> BDD-cost: 22 c ---[ 41]---> BDD-cost: 22 c ---[ 40]---> BDD-cost: 22 c ---[ 39]---> BDD-cost: 22 c ---[ 38]---> BDD-cost: 22 c ---[ 37]---> BDD-cost: 19 c ---[ 36]---> BDD-cost: 19 c ---[ 35]---> BDD-cost: 19 c ---[ 34]---> BDD-cost: 19 c ---[ 33]---> BDD-cost: 19 c ---[ 32]---> BDD-cost: 19 c ---[ 31]---> BDD-cost: 22 c ---[ 30]---> BDD-cost: 22 c ---[ 29]---> BDD-cost: 22 c ---[ 28]---> BDD-cost: 22 c ---[ 27]---> BDD-cost: 22 c ---[ 26]---> BDD-cost: 22 c ---[ 25]---> BDD-cost: 22 c ---[ 24]---> BDD-cost: 22 c ---[ 23]---> BDD-cost: 22 c ---[ 22]---> BDD-cost: 22 c ---[ 21]---> BDD-cost: 22 c ---[ 20]---> BDD-cost: 22 c ---[ 19]---> BDD-cost: 22 c ---[ 18]---> BDD-cost: 13 c ---[ 17]---> BDD-cost: 13 c ---[ 16]---> BDD-cost: 10 c ---[ 15]---> BDD-cost: 58 c ---[ 14]---> BDD-cost: 60 c ---[ 13]---> BDD-cost: 63 c ---[ 12]---> BDD-cost: 63 c ---[ 11]---> BDD-cost: 60 c ---[ 10]---> BDD-cost: 58 c ---[ 9]---> BDD-cost: 63 c ---[ 8]---> BDD-cost: 63 c ---[ 7]---> BDD-cost: 123 c ---[ 6]---> Sorter-cost: 420 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 5]---> Sorter-cost: 278 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 4]---> Sorter-cost: 314 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 3]---> Sorter-cost: 298 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 2]---> Sorter-cost: 332 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 1]---> Sorter-cost: 293 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 0]---> Sorter-cost: 381 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 846996 2262333 | 282332 0 0 nan | 0.000 % | c | 100 | 846881 2262075 | 310565 87 326 3.7 | 4.643 % | c | 250 | 846689 2261663 | 341621 219 839 3.8 | 4.666 % | c | 475 | 846600 2261466 | 375783 437 1777 4.1 | 4.675 % | c | 812 | 846482 2261214 | 413362 759 5366 7.1 | 4.690 % | c | 1318 | 846474 2261188 | 454698 1264 13759 10.9 | 4.690 % | c | 2077 | 846279 2260757 | 500168 2015 26139 13.0 | 4.709 % | c | 3216 | 845923 2259977 | 550185 3121 37580 12.0 | 4.747 % | c | 4924 | 845212 2258409 | 605203 4743 51824 10.9 | 4.823 % | c | 7486 | 844789 2257448 | 665724 7283 75727 10.4 | 4.863 % | c | 11330 | 844351 2256468 | 732296 11073 137214 12.4 | 4.909 % | c | 17098 | 843982 2255655 | 805526 16802 365193 21.7 | 4.947 % | c | 25747 | 842540 2252426 | 886078 25267 539057 21.3 | 5.101 % | c | 38722 | 841729 2250612 | 974686 38164 947119 24.8 | 5.188 % | c | 58184 | 841043 2249110 | 1072155 57562 1482885 25.8 | 5.262 % | c | 87376 | 840158 2247147 | 1179370 86686 3104618 35.8 | 5.353 % | c | 131165 | 840078 2246973 | 1297307 130466 10578116 81.1 | 5.361 % |
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/14891/stat): 14891 (minisat+_script) R 14890 14891 30740 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1793574118 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/14891/statm): 174 3 169 147 0 27 0 [pid=14891] 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=14892 New process pid=14893 New process pid=14894 execve syscall for /bin/sed executable One traced child (pid=14893) 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=14894) exited with status: 0 One traced child (pid=14892) exited with status: 0 New process pid=14895 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-mps-v2-20-10-danoint.opb [startup+10.0052 s] Raw data (loadavg): 0.93 0.95 0.70 1/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) T 14891 14891 30740 0 -1 0 13781 0 3 0 869 58 0 0 22 0 1 0 1793574123 65777664 13100 4294967295 134512640 135094434 3221224432 3221209852 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/14895/statm): 16059 13100 145 145 0 15914 0 [pid=14895] vsize: 64236 Current children cumulated CPU time (s) 9.27 Current children cumulated vsize (Kb) 66360 [startup+20.006 s] Raw data (loadavg): 0.94 0.96 0.70 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 22994 0 3 0 1787 98 0 0 25 0 1 0 1793574123 113037312 22313 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14895/statm): 27597 22313 145 145 0 27452 0 [pid=14895] vsize: 110388 Current children cumulated CPU time (s) 18.85 Current children cumulated vsize (Kb) 112512 [startup+30.0088 s] Raw data (loadavg): 0.95 0.96 0.71 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23043 0 3 0 2785 99 0 0 25 0 1 0 1793574123 113238016 22362 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14895/statm): 27646 22362 145 145 0 27501 0 [pid=14895] vsize: 110584 Current children cumulated CPU time (s) 28.84 Current children cumulated vsize (Kb) 112708 [startup+40.0096 s] Raw data (loadavg): 0.96 0.96 0.71 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23101 0 3 0 3783 100 0 0 25 0 1 0 1793574123 113475584 22420 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 27704 22420 145 145 0 27559 0 [pid=14895] vsize: 110816 Current children cumulated CPU time (s) 38.83 Current children cumulated vsize (Kb) 112940 [startup+50.0103 s] Raw data (loadavg): 0.96 0.96 0.71 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23145 0 3 0 4782 101 0 0 25 0 1 0 1793574123 113623040 22464 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 27740 22464 145 145 0 27595 0 [pid=14895] vsize: 110960 Current children cumulated CPU time (s) 48.83 Current children cumulated vsize (Kb) 113084 [startup+60.0111 s] Raw data (loadavg): 0.97 0.96 0.71 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23158 0 3 0 5783 102 0 0 25 0 1 0 1793574123 113684480 22477 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 27755 22477 145 145 0 27610 0 [pid=14895] vsize: 111020 Current children cumulated CPU time (s) 58.85 Current children cumulated vsize (Kb) 113144 [startup+70.0219 s] Raw data (loadavg): 0.97 0.96 0.72 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23173 0 3 0 6782 102 0 0 25 0 1 0 1793574123 113745920 22492 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 27770 22492 145 145 0 27625 0 [pid=14895] vsize: 111080 Current children cumulated CPU time (s) 68.84 Current children cumulated vsize (Kb) 113204 [startup+80.0227 s] Raw data (loadavg): 0.98 0.96 0.72 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23220 0 3 0 7781 103 0 0 25 0 1 0 1793574123 113930240 22539 4294967295 134512640 135094434 3221224432 3221223092 134553454 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 27815 22539 145 145 0 27670 0 [pid=14895] vsize: 111260 Current children cumulated CPU time (s) 78.84 Current children cumulated vsize (Kb) 113384 [startup+90.0235 s] Raw data (loadavg): 0.98 0.96 0.72 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23238 0 3 0 8781 103 0 0 25 0 1 0 1793574123 114003968 22557 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 27833 22557 145 145 0 27688 0 [pid=14895] vsize: 111332 Current children cumulated CPU time (s) 88.84 Current children cumulated vsize (Kb) 113456 [startup+100.023 s] Raw data (loadavg): 0.98 0.96 0.73 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23264 0 3 0 9780 103 0 0 25 0 1 0 1793574123 114139136 22583 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 27866 22583 145 145 0 27721 0 [pid=14895] vsize: 111464 Current children cumulated CPU time (s) 98.83 Current children cumulated vsize (Kb) 113588 [startup+110.024 s] Raw data (loadavg): 0.98 0.96 0.73 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23295 0 3 0 10780 103 0 0 25 0 1 0 1793574123 114257920 22614 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 27895 22614 145 145 0 27750 0 [pid=14895] vsize: 111580 Current children cumulated CPU time (s) 108.83 Current children cumulated vsize (Kb) 113704 [startup+120.025 s] Raw data (loadavg): 0.99 0.97 0.73 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23378 0 3 0 11779 104 0 0 25 0 1 0 1793574123 114589696 22697 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 27976 22697 145 145 0 27831 0 [pid=14895] vsize: 111904 Current children cumulated CPU time (s) 118.83 Current children cumulated vsize (Kb) 114028 [startup+130.026 s] Raw data (loadavg): 0.99 0.97 0.73 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23513 0 3 0 12777 105 0 0 25 0 1 0 1793574123 115134464 22832 4294967295 134512640 135094434 3221224432 3221223088 134557882 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 28109 22832 145 145 0 27964 0 [pid=14895] vsize: 112436 Current children cumulated CPU time (s) 128.82 Current children cumulated vsize (Kb) 114560 [startup+140.027 s] Raw data (loadavg): 0.99 0.97 0.73 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23541 0 3 0 13777 105 0 0 25 0 1 0 1793574123 115249152 22860 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 28137 22860 145 145 0 27992 0 [pid=14895] vsize: 112548 Current children cumulated CPU time (s) 138.82 Current children cumulated vsize (Kb) 114672 [startup+150.027 s] Raw data (loadavg): 0.99 0.97 0.74 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23566 0 3 0 14776 106 0 0 25 0 1 0 1793574123 115347456 22885 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 28161 22885 145 145 0 28016 0 [pid=14895] vsize: 112644 Current children cumulated CPU time (s) 148.82 Current children cumulated vsize (Kb) 114768 [startup+160.028 s] Raw data (loadavg): 0.99 0.97 0.74 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23593 0 3 0 15776 106 0 0 25 0 1 0 1793574123 115458048 22912 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 28188 22912 145 145 0 28043 0 [pid=14895] vsize: 112752 Current children cumulated CPU time (s) 158.82 Current children cumulated vsize (Kb) 114876 [startup+170.029 s] Raw data (loadavg): 0.99 0.97 0.74 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23648 0 3 0 16775 106 0 0 25 0 1 0 1793574123 115720192 22967 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 28252 22967 145 145 0 28107 0 [pid=14895] vsize: 113008 Current children cumulated CPU time (s) 168.81 Current children cumulated vsize (Kb) 115132 [startup+180.03 s] Raw data (loadavg): 0.99 0.97 0.74 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23674 0 3 0 17775 107 0 0 25 0 1 0 1793574123 115818496 22993 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 28276 22993 145 145 0 28131 0 [pid=14895] vsize: 113104 Current children cumulated CPU time (s) 178.82 Current children cumulated vsize (Kb) 115228 [startup+190.031 s] Raw data (loadavg): 0.99 0.97 0.74 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23721 0 3 0 18774 107 0 0 25 0 1 0 1793574123 116006912 23040 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 28322 23040 145 145 0 28177 0 [pid=14895] vsize: 113288 Current children cumulated CPU time (s) 188.81 Current children cumulated vsize (Kb) 115412 [startup+200.031 s] Raw data (loadavg): 0.99 0.97 0.75 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23768 0 3 0 19774 108 0 0 25 0 1 0 1793574123 116195328 23087 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 28368 23087 145 145 0 28223 0 [pid=14895] vsize: 113472 Current children cumulated CPU time (s) 198.82 Current children cumulated vsize (Kb) 115596 [startup+210.032 s] Raw data (loadavg): 0.99 0.97 0.75 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23809 0 3 0 20774 108 0 0 25 0 1 0 1793574123 116363264 23128 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 28409 23128 145 145 0 28264 0 [pid=14895] vsize: 113636 Current children cumulated CPU time (s) 208.82 Current children cumulated vsize (Kb) 115760 [startup+220.033 s] Raw data (loadavg): 0.99 0.97 0.75 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23850 0 3 0 21773 108 0 0 25 0 1 0 1793574123 116523008 23169 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 28448 23169 145 145 0 28303 0 [pid=14895] vsize: 113792 Current children cumulated CPU time (s) 218.81 Current children cumulated vsize (Kb) 115916 [startup+230.034 s] Raw data (loadavg): 0.99 0.97 0.75 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23868 0 3 0 22773 108 0 0 25 0 1 0 1793574123 116588544 23187 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 28464 23187 145 145 0 28319 0 [pid=14895] vsize: 113856 Current children cumulated CPU time (s) 228.81 Current children cumulated vsize (Kb) 115980 [startup+240.035 s] Raw data (loadavg): 0.99 0.97 0.75 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23878 0 3 0 23773 108 0 0 25 0 1 0 1793574123 116625408 23197 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 28473 23197 145 145 0 28328 0 [pid=14895] vsize: 113892 Current children cumulated CPU time (s) 238.81 Current children cumulated vsize (Kb) 116016 [startup+250.035 s] Raw data (loadavg): 0.99 0.97 0.76 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23895 0 3 0 24773 108 0 0 25 0 1 0 1793574123 116690944 23214 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 28489 23214 145 145 0 28344 0 [pid=14895] vsize: 113956 Current children cumulated CPU time (s) 248.81 Current children cumulated vsize (Kb) 116080 [startup+260.036 s] Raw data (loadavg): 0.99 0.97 0.76 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23905 0 3 0 25773 108 0 0 25 0 1 0 1793574123 116731904 23224 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 28499 23224 145 145 0 28354 0 [pid=14895] vsize: 113996 Current children cumulated CPU time (s) 258.81 Current children cumulated vsize (Kb) 116120 [startup+270.037 s] Raw data (loadavg): 0.99 0.97 0.76 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23946 0 3 0 26772 109 0 0 25 0 1 0 1793574123 116883456 23265 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 28536 23265 145 145 0 28391 0 [pid=14895] vsize: 114144 Current children cumulated CPU time (s) 268.81 Current children cumulated vsize (Kb) 116268 [startup+280.038 s] Raw data (loadavg): 0.99 0.97 0.76 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23977 0 3 0 27772 109 0 0 25 0 1 0 1793574123 117002240 23296 4294967295 134512640 135094434 3221224432 3221223092 134553528 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 28565 23296 145 145 0 28420 0 [pid=14895] vsize: 114260 Current children cumulated CPU time (s) 278.81 Current children cumulated vsize (Kb) 116384 [startup+290.039 s] Raw data (loadavg): 0.99 0.97 0.76 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 23993 0 3 0 28772 109 0 0 25 0 1 0 1793574123 117067776 23312 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 28581 23312 145 145 0 28436 0 [pid=14895] vsize: 114324 Current children cumulated CPU time (s) 288.81 Current children cumulated vsize (Kb) 116448 [startup+300.039 s] Raw data (loadavg): 0.99 0.97 0.77 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 24068 0 3 0 29771 110 0 0 25 0 1 0 1793574123 117309440 23387 4294967295 134512640 135094434 3221224432 3221223120 134554676 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 28640 23387 145 145 0 28495 0 [pid=14895] vsize: 114560 Current children cumulated CPU time (s) 298.81 Current children cumulated vsize (Kb) 116684 [startup+310.04 s] Raw data (loadavg): 0.99 0.97 0.77 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 24137 0 3 0 30770 110 0 0 25 0 1 0 1793574123 117587968 23456 4294967295 134512640 135094434 3221224432 3221223092 134553519 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 28708 23456 145 145 0 28563 0 [pid=14895] vsize: 114832 Current children cumulated CPU time (s) 308.8 Current children cumulated vsize (Kb) 116956 [startup+320.04 s] Raw data (loadavg): 0.99 0.97 0.77 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 24251 0 3 0 31769 111 0 0 25 0 1 0 1793574123 118173696 23570 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 28851 23570 145 145 0 28706 0 [pid=14895] vsize: 115404 Current children cumulated CPU time (s) 318.8 Current children cumulated vsize (Kb) 117528 [startup+330.042 s] Raw data (loadavg): 0.99 0.97 0.77 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 24337 0 3 0 32768 111 0 0 25 0 1 0 1793574123 118517760 23656 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 28935 23656 145 145 0 28790 0 [pid=14895] vsize: 115740 Current children cumulated CPU time (s) 328.79 Current children cumulated vsize (Kb) 117864 [startup+340.042 s] Raw data (loadavg): 0.99 0.97 0.77 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 24483 0 3 0 33764 113 0 0 25 0 1 0 1793574123 119111680 23802 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 29080 23802 145 145 0 28935 0 [pid=14895] vsize: 116320 Current children cumulated CPU time (s) 338.77 Current children cumulated vsize (Kb) 118444 [startup+350.042 s] Raw data (loadavg): 0.99 0.97 0.78 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 24539 0 3 0 34763 113 0 0 25 0 1 0 1793574123 119336960 23858 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 29135 23858 145 145 0 28990 0 [pid=14895] vsize: 116540 Current children cumulated CPU time (s) 348.76 Current children cumulated vsize (Kb) 118664 [startup+360.043 s] Raw data (loadavg): 0.99 0.97 0.78 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 24616 0 3 0 35762 114 0 0 25 0 1 0 1793574123 119640064 23935 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 29209 23935 145 145 0 29064 0 [pid=14895] vsize: 116836 Current children cumulated CPU time (s) 358.76 Current children cumulated vsize (Kb) 118960 [startup+370.044 s] Raw data (loadavg): 0.99 0.97 0.78 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 24739 0 3 0 36760 115 0 0 25 0 1 0 1793574123 120131584 24058 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 29329 24058 145 145 0 29184 0 [pid=14895] vsize: 117316 Current children cumulated CPU time (s) 368.75 Current children cumulated vsize (Kb) 119440 [startup+380.045 s] Raw data (loadavg): 0.99 0.97 0.78 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 24842 0 3 0 37758 117 0 0 25 0 1 0 1793574123 120541184 24161 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 29429 24161 145 145 0 29284 0 [pid=14895] vsize: 117716 Current children cumulated CPU time (s) 378.75 Current children cumulated vsize (Kb) 119840 [startup+390.045 s] Raw data (loadavg): 0.99 0.97 0.78 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 24898 0 3 0 38757 117 0 0 25 0 1 0 1793574123 120766464 24217 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 29484 24217 145 145 0 29339 0 [pid=14895] vsize: 117936 Current children cumulated CPU time (s) 388.74 Current children cumulated vsize (Kb) 120060 [startup+400.046 s] Raw data (loadavg): 0.99 0.97 0.79 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 25033 0 3 0 39756 118 0 0 25 0 1 0 1793574123 121303040 24352 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 29615 24352 145 145 0 29470 0 [pid=14895] vsize: 118460 Current children cumulated CPU time (s) 398.74 Current children cumulated vsize (Kb) 120584 [startup+410.047 s] Raw data (loadavg): 0.99 0.97 0.79 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 25071 0 3 0 40756 118 0 0 25 0 1 0 1793574123 121454592 24390 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 29652 24390 145 145 0 29507 0 [pid=14895] vsize: 118608 Current children cumulated CPU time (s) 408.74 Current children cumulated vsize (Kb) 120732 [startup+420.048 s] Raw data (loadavg): 0.99 0.97 0.79 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 25240 0 3 0 41753 119 0 0 25 0 1 0 1793574123 122134528 24559 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14895/statm): 29818 24559 145 145 0 29673 0 [pid=14895] vsize: 119272 Current children cumulated CPU time (s) 418.72 Current children cumulated vsize (Kb) 121396 [startup+430.049 s] Raw data (loadavg): 0.99 0.97 0.79 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 25300 0 3 0 42751 120 0 0 25 0 1 0 1793574123 122372096 24619 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14895/statm): 29876 24619 145 145 0 29731 0 [pid=14895] vsize: 119504 Current children cumulated CPU time (s) 428.71 Current children cumulated vsize (Kb) 121628 [startup+440.049 s] Raw data (loadavg): 0.99 0.97 0.79 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 25386 0 3 0 43749 121 0 0 25 0 1 0 1793574123 122720256 24705 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14895/statm): 29961 24705 145 145 0 29816 0 [pid=14895] vsize: 119844 Current children cumulated CPU time (s) 438.7 Current children cumulated vsize (Kb) 121968 [startup+450.05 s] Raw data (loadavg): 0.99 0.97 0.80 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 25452 0 3 0 44747 123 0 0 25 0 1 0 1793574123 122990592 24771 4294967295 134512640 135094434 3221224432 3221223088 134557853 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14895/statm): 30027 24771 145 145 0 29882 0 [pid=14895] vsize: 120108 Current children cumulated CPU time (s) 448.7 Current children cumulated vsize (Kb) 122232 [startup+460.051 s] Raw data (loadavg): 0.99 0.97 0.80 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 25509 0 3 0 45746 123 0 0 25 0 1 0 1793574123 123219968 24828 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14895/statm): 30083 24828 145 145 0 29938 0 [pid=14895] vsize: 120332 Current children cumulated CPU time (s) 458.69 Current children cumulated vsize (Kb) 122456 [startup+470.052 s] Raw data (loadavg): 0.99 0.97 0.80 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 25582 0 3 0 46744 124 0 0 25 0 1 0 1793574123 123514880 24901 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14895/statm): 30155 24901 145 145 0 30010 0 [pid=14895] vsize: 120620 Current children cumulated CPU time (s) 468.68 Current children cumulated vsize (Kb) 122744 [startup+480.053 s] Raw data (loadavg): 0.99 0.97 0.80 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 25666 0 3 0 47743 125 0 0 25 0 1 0 1793574123 123854848 24985 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14895/statm): 30238 24985 145 145 0 30093 0 [pid=14895] vsize: 120952 Current children cumulated CPU time (s) 478.68 Current children cumulated vsize (Kb) 123076 [startup+490.054 s] Raw data (loadavg): 0.99 0.97 0.80 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 25761 0 3 0 48741 126 0 0 25 0 1 0 1793574123 124239872 25080 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14895/statm): 30332 25080 145 145 0 30187 0 [pid=14895] vsize: 121328 Current children cumulated CPU time (s) 488.67 Current children cumulated vsize (Kb) 123452 [startup+500.055 s] Raw data (loadavg): 0.99 0.97 0.81 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 25850 0 3 0 49739 127 0 0 25 0 1 0 1793574123 124604416 25169 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14895/statm): 30421 25169 145 145 0 30276 0 [pid=14895] vsize: 121684 Current children cumulated CPU time (s) 498.66 Current children cumulated vsize (Kb) 123808 [startup+510.057 s] Raw data (loadavg): 0.99 0.97 0.81 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 25926 0 3 0 50737 128 0 0 25 0 1 0 1793574123 125173760 25245 4294967295 134512640 135094434 3221224432 3221223056 134557574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14895/statm): 30560 25245 145 145 0 30415 0 [pid=14895] vsize: 122240 Current children cumulated CPU time (s) 508.65 Current children cumulated vsize (Kb) 124364 [startup+520.058 s] Raw data (loadavg): 0.99 0.97 0.81 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 26001 0 3 0 51736 129 0 0 25 0 1 0 1793574123 125476864 25320 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14895/statm): 30634 25320 145 145 0 30489 0 [pid=14895] vsize: 122536 Current children cumulated CPU time (s) 518.65 Current children cumulated vsize (Kb) 124660 [startup+530.058 s] Raw data (loadavg): 0.99 0.97 0.81 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 26086 0 3 0 52733 130 0 0 25 0 1 0 1793574123 125820928 25405 4294967295 134512640 135094434 3221224432 3221223056 134557702 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14895/statm): 30718 25405 145 145 0 30573 0 [pid=14895] vsize: 122872 Current children cumulated CPU time (s) 528.63 Current children cumulated vsize (Kb) 124996 [startup+540.06 s] Raw data (loadavg): 0.99 0.97 0.81 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 26158 0 3 0 53731 131 0 0 25 0 1 0 1793574123 126107648 25477 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14895/statm): 30788 25477 145 145 0 30643 0 [pid=14895] vsize: 123152 Current children cumulated CPU time (s) 538.62 Current children cumulated vsize (Kb) 125276 [startup+550.061 s] Raw data (loadavg): 0.99 0.97 0.81 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 26667 0 3 0 54721 135 0 0 25 0 1 0 1793574123 128172032 25986 4294967295 134512640 135094434 3221224432 3221223024 134556776 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14895/statm): 31292 25986 145 145 0 31147 0 [pid=14895] vsize: 125168 Current children cumulated CPU time (s) 548.56 Current children cumulated vsize (Kb) 127292 [startup+560.062 s] Raw data (loadavg): 0.99 0.97 0.82 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 26778 0 3 0 55719 136 0 0 25 0 1 0 1793574123 128622592 26097 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14895/statm): 31402 26097 145 145 0 31257 0 [pid=14895] vsize: 125608 Current children cumulated CPU time (s) 558.55 Current children cumulated vsize (Kb) 127732 [startup+570.062 s] Raw data (loadavg): 0.99 0.97 0.82 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 26852 0 3 0 56717 137 0 0 25 0 1 0 1793574123 128917504 26171 4294967295 134512640 135094434 3221224432 3221223056 134557662 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14895/statm): 31474 26171 145 145 0 31329 0 [pid=14895] vsize: 125896 Current children cumulated CPU time (s) 568.54 Current children cumulated vsize (Kb) 128020 [startup+580.064 s] Raw data (loadavg): 0.99 0.97 0.82 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 26887 0 3 0 57716 138 0 0 25 0 1 0 1793574123 129056768 26206 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14895/statm): 31508 26206 145 145 0 31363 0 [pid=14895] vsize: 126032 Current children cumulated CPU time (s) 578.54 Current children cumulated vsize (Kb) 128156 [startup+590.065 s] Raw data (loadavg): 0.99 0.97 0.82 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 26979 0 3 0 58715 138 0 0 25 0 1 0 1793574123 129421312 26298 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14895/statm): 31597 26298 145 145 0 31452 0 [pid=14895] vsize: 126388 Current children cumulated CPU time (s) 588.53 Current children cumulated vsize (Kb) 128512 [startup+600.066 s] Raw data (loadavg): 0.99 0.97 0.82 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 27078 0 3 0 59713 140 0 0 25 0 1 0 1793574123 129818624 26397 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14895/statm): 31694 26397 145 145 0 31549 0 [pid=14895] vsize: 126776 Current children cumulated CPU time (s) 598.53 Current children cumulated vsize (Kb) 128900 [startup+610.067 s] Raw data (loadavg): 0.99 0.97 0.82 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 27166 0 3 0 60710 142 0 0 25 0 1 0 1793574123 130170880 26485 4294967295 134512640 135094434 3221224432 3221223056 134557574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14895/statm): 31780 26485 145 145 0 31635 0 [pid=14895] vsize: 127120 Current children cumulated CPU time (s) 608.52 Current children cumulated vsize (Kb) 129244 [startup+620.068 s] Raw data (loadavg): 0.99 0.97 0.82 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 27230 0 3 0 61709 142 0 0 25 0 1 0 1793574123 130424832 26549 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14895/statm): 31842 26549 145 145 0 31697 0 [pid=14895] vsize: 127368 Current children cumulated CPU time (s) 618.51 Current children cumulated vsize (Kb) 129492 [startup+630.07 s] Raw data (loadavg): 0.99 0.97 0.82 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 27480 0 3 0 62705 144 0 0 25 0 1 0 1793574123 131440640 26799 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14895/statm): 32090 26799 145 145 0 31945 0 [pid=14895] vsize: 128360 Current children cumulated CPU time (s) 628.49 Current children cumulated vsize (Kb) 130484 [startup+640.071 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 28223 0 3 0 63691 151 0 0 25 0 1 0 1793574123 134463488 27542 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 32828 27542 145 145 0 32683 0 [pid=14895] vsize: 131312 Current children cumulated CPU time (s) 638.42 Current children cumulated vsize (Kb) 133436 [startup+650.074 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 28928 0 3 0 64678 156 0 0 25 0 1 0 1793574123 137334784 28247 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14895/statm): 33529 28247 145 145 0 33384 0 [pid=14895] vsize: 134116 Current children cumulated CPU time (s) 648.34 Current children cumulated vsize (Kb) 136240 [startup+660.074 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 29627 0 3 0 65667 160 0 0 25 0 1 0 1793574123 140189696 28946 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 34226 28946 145 145 0 34081 0 [pid=14895] vsize: 136904 Current children cumulated CPU time (s) 658.27 Current children cumulated vsize (Kb) 139028 [startup+670.075 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 30280 0 3 0 66654 165 0 0 25 0 1 0 1793574123 142856192 29599 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 34877 29599 145 145 0 34732 0 [pid=14895] vsize: 139508 Current children cumulated CPU time (s) 668.19 Current children cumulated vsize (Kb) 141632 [startup+680.077 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 30882 0 3 0 67643 170 0 0 25 0 1 0 1793574123 145309696 30201 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 35476 30201 145 145 0 35331 0 [pid=14895] vsize: 141904 Current children cumulated CPU time (s) 678.13 Current children cumulated vsize (Kb) 144028 [startup+690.078 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 31548 0 3 0 68632 174 0 0 25 0 1 0 1793574123 148021248 30867 4294967295 134512640 135094434 3221224432 3221223056 134557711 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 36138 30867 145 145 0 35993 0 [pid=14895] vsize: 144552 Current children cumulated CPU time (s) 688.06 Current children cumulated vsize (Kb) 146676 [startup+700.077 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 32363 0 3 0 69619 181 0 0 25 0 1 0 1793574123 151343104 31682 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 36949 31682 145 145 0 36804 0 [pid=14895] vsize: 147796 Current children cumulated CPU time (s) 698 Current children cumulated vsize (Kb) 149920 [startup+710.078 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 32924 0 3 0 70609 185 0 0 25 0 1 0 1793574123 153628672 32243 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14895/statm): 37507 32243 145 145 0 37362 0 [pid=14895] vsize: 150028 Current children cumulated CPU time (s) 707.94 Current children cumulated vsize (Kb) 152152 [startup+720.079 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 33542 0 3 0 71600 188 0 0 25 0 1 0 1793574123 156155904 32861 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 38124 32861 145 145 0 37979 0 [pid=14895] vsize: 152496 Current children cumulated CPU time (s) 717.88 Current children cumulated vsize (Kb) 154620 [startup+730.08 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 34180 0 3 0 72589 192 0 0 25 0 1 0 1793574123 158765056 33499 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 38761 33499 145 145 0 38616 0 [pid=14895] vsize: 155044 Current children cumulated CPU time (s) 727.81 Current children cumulated vsize (Kb) 157168 [startup+740.081 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 34891 0 3 0 73577 196 0 0 25 0 1 0 1793574123 161673216 34210 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 39471 34210 145 145 0 39326 0 [pid=14895] vsize: 157884 Current children cumulated CPU time (s) 737.73 Current children cumulated vsize (Kb) 160008 [startup+750.081 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 34999 0 3 0 74576 198 0 0 25 0 1 0 1793574123 162123776 34318 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 39581 34318 145 145 0 39436 0 [pid=14895] vsize: 158324 Current children cumulated CPU time (s) 747.74 Current children cumulated vsize (Kb) 160448 [startup+760.082 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 35053 0 3 0 75575 198 0 0 25 0 1 0 1793574123 162344960 34372 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14895/statm): 39635 34372 145 145 0 39490 0 [pid=14895] vsize: 158540 Current children cumulated CPU time (s) 757.73 Current children cumulated vsize (Kb) 160664 [startup+770.083 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 35096 0 3 0 76574 198 0 0 25 0 1 0 1793574123 163041280 34415 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 39805 34415 145 145 0 39660 0 [pid=14895] vsize: 159220 Current children cumulated CPU time (s) 767.72 Current children cumulated vsize (Kb) 161344 [startup+780.085 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 35132 0 3 0 77573 199 0 0 25 0 1 0 1793574123 163184640 34451 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 39840 34451 145 145 0 39695 0 [pid=14895] vsize: 159360 Current children cumulated CPU time (s) 777.72 Current children cumulated vsize (Kb) 161484 [startup+790.086 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 35281 0 3 0 78571 200 0 0 25 0 1 0 1793574123 163786752 34600 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 39987 34600 145 145 0 39842 0 [pid=14895] vsize: 159948 Current children cumulated CPU time (s) 787.71 Current children cumulated vsize (Kb) 162072 [startup+800.085 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 35307 0 3 0 79571 200 0 0 25 0 1 0 1793574123 163889152 34626 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 40012 34626 145 145 0 39867 0 [pid=14895] vsize: 160048 Current children cumulated CPU time (s) 797.71 Current children cumulated vsize (Kb) 162172 [startup+810.086 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 35357 0 3 0 80570 201 0 0 25 0 1 0 1793574123 164093952 34676 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 40062 34676 145 145 0 39917 0 [pid=14895] vsize: 160248 Current children cumulated CPU time (s) 807.71 Current children cumulated vsize (Kb) 162372 [startup+820.087 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 35465 0 3 0 81568 202 0 0 25 0 1 0 1793574123 164528128 34784 4294967295 134512640 135094434 3221224432 3221223056 134557660 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 40168 34784 145 145 0 40023 0 [pid=14895] vsize: 160672 Current children cumulated CPU time (s) 817.7 Current children cumulated vsize (Kb) 162796 [startup+830.088 s] Raw data (loadavg): 0.99 0.97 0.84 1/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) T 14891 14891 30740 0 -1 0 35556 0 3 0 82567 202 0 0 25 0 1 0 1793574123 164896768 34875 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/14895/statm): 40258 34875 145 145 0 40113 0 [pid=14895] vsize: 161032 Current children cumulated CPU time (s) 827.69 Current children cumulated vsize (Kb) 163156 [startup+840.088 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 35664 0 3 0 83565 203 0 0 25 0 1 0 1793574123 165335040 34983 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 40365 34983 145 145 0 40220 0 [pid=14895] vsize: 161460 Current children cumulated CPU time (s) 837.68 Current children cumulated vsize (Kb) 163584 [startup+850.088 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 35771 0 3 0 84564 204 0 0 25 0 1 0 1793574123 165769216 35090 4294967295 134512640 135094434 3221224432 3221223088 134557835 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 40471 35090 145 145 0 40326 0 [pid=14895] vsize: 161884 Current children cumulated CPU time (s) 847.68 Current children cumulated vsize (Kb) 164008 [startup+860.089 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 35889 0 3 0 85563 204 0 0 25 0 1 0 1793574123 166252544 35208 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 40589 35208 145 145 0 40444 0 [pid=14895] vsize: 162356 Current children cumulated CPU time (s) 857.67 Current children cumulated vsize (Kb) 164480 [startup+870.09 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 35995 0 3 0 86561 206 0 0 25 0 1 0 1793574123 166682624 35314 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 40694 35314 145 145 0 40549 0 [pid=14895] vsize: 162776 Current children cumulated CPU time (s) 867.67 Current children cumulated vsize (Kb) 164900 [startup+880.091 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 36103 0 3 0 87559 207 0 0 25 0 1 0 1793574123 167120896 35422 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 40801 35422 145 145 0 40656 0 [pid=14895] vsize: 163204 Current children cumulated CPU time (s) 877.66 Current children cumulated vsize (Kb) 165328 [startup+890.091 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 36231 0 3 0 88557 208 0 0 25 0 1 0 1793574123 167641088 35550 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 40928 35550 145 145 0 40783 0 [pid=14895] vsize: 163712 Current children cumulated CPU time (s) 887.65 Current children cumulated vsize (Kb) 165836 [startup+900.092 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 36351 0 3 0 89555 208 0 0 25 0 1 0 1793574123 168120320 35670 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 41045 35670 145 145 0 40900 0 [pid=14895] vsize: 164180 Current children cumulated CPU time (s) 897.63 Current children cumulated vsize (Kb) 166304 [startup+910.093 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 36459 0 3 0 90554 209 0 0 25 0 1 0 1793574123 168570880 35778 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 41155 35778 145 145 0 41010 0 [pid=14895] vsize: 164620 Current children cumulated CPU time (s) 907.63 Current children cumulated vsize (Kb) 166744 [startup+920.094 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 36563 0 3 0 91553 210 0 0 25 0 1 0 1793574123 169013248 35882 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 41263 35882 145 145 0 41118 0 [pid=14895] vsize: 165052 Current children cumulated CPU time (s) 917.63 Current children cumulated vsize (Kb) 167176 [startup+930.095 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 36653 0 3 0 92552 210 0 0 25 0 1 0 1793574123 169381888 35972 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 41353 35972 145 145 0 41208 0 [pid=14895] vsize: 165412 Current children cumulated CPU time (s) 927.62 Current children cumulated vsize (Kb) 167536 [startup+940.096 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 36747 0 3 0 93550 211 0 0 25 0 1 0 1793574123 169758720 36066 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 41445 36066 145 145 0 41300 0 [pid=14895] vsize: 165780 Current children cumulated CPU time (s) 937.61 Current children cumulated vsize (Kb) 167904 [startup+950.096 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 36858 0 3 0 94549 212 0 0 25 0 1 0 1793574123 170201088 36177 4294967295 134512640 135094434 3221224432 3221223064 134557561 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 41553 36177 145 145 0 41408 0 [pid=14895] vsize: 166212 Current children cumulated CPU time (s) 947.61 Current children cumulated vsize (Kb) 168336 [startup+960.098 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 36929 0 3 0 95548 212 0 0 25 0 1 0 1793574123 170491904 36248 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 41624 36248 145 145 0 41479 0 [pid=14895] vsize: 166496 Current children cumulated CPU time (s) 957.6 Current children cumulated vsize (Kb) 168620 [startup+970.099 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 36982 0 3 0 96547 213 0 0 25 0 1 0 1793574123 170704896 36301 4294967295 134512640 135094434 3221224432 3221223088 134557859 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 41676 36301 145 145 0 41531 0 [pid=14895] vsize: 166704 Current children cumulated CPU time (s) 967.6 Current children cumulated vsize (Kb) 168828 [startup+980.099 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 37039 0 3 0 97546 214 0 0 25 0 1 0 1793574123 170938368 36358 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 41733 36358 145 145 0 41588 0 [pid=14895] vsize: 166932 Current children cumulated CPU time (s) 977.6 Current children cumulated vsize (Kb) 169056 [startup+990.1 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 37091 0 3 0 98546 214 0 0 25 0 1 0 1793574123 171147264 36410 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 41784 36410 145 145 0 41639 0 [pid=14895] vsize: 167136 Current children cumulated CPU time (s) 987.6 Current children cumulated vsize (Kb) 169260 [startup+1000.1 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 37137 0 3 0 99545 214 0 0 25 0 1 0 1793574123 171335680 36456 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 41830 36456 145 145 0 41685 0 [pid=14895] vsize: 167320 Current children cumulated CPU time (s) 997.59 Current children cumulated vsize (Kb) 169444 [startup+1010.1 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 37222 0 3 0 100545 215 0 0 25 0 1 0 1793574123 171679744 36541 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 41914 36541 145 145 0 41769 0 [pid=14895] vsize: 167656 Current children cumulated CPU time (s) 1007.6 Current children cumulated vsize (Kb) 169780 [startup+1020.1 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 37298 0 3 0 101543 216 0 0 25 0 1 0 1793574123 171986944 36617 4294967295 134512640 135094434 3221224432 3221223072 134558264 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 41989 36617 145 145 0 41844 0 [pid=14895] vsize: 167956 Current children cumulated CPU time (s) 1017.59 Current children cumulated vsize (Kb) 170080 [startup+1030.1 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 37354 0 3 0 102542 216 0 0 25 0 1 0 1793574123 172216320 36673 4294967295 134512640 135094434 3221224432 3221223056 134557636 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 42045 36673 145 145 0 41900 0 [pid=14895] vsize: 168180 Current children cumulated CPU time (s) 1027.58 Current children cumulated vsize (Kb) 170304 [startup+1040.1 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 37420 0 3 0 103540 218 0 0 25 0 1 0 1793574123 172482560 36739 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 42110 36739 145 145 0 41965 0 [pid=14895] vsize: 168440 Current children cumulated CPU time (s) 1037.58 Current children cumulated vsize (Kb) 170564 [startup+1050.11 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 37481 0 3 0 104539 218 0 0 25 0 1 0 1793574123 172732416 36800 4294967295 134512640 135094434 3221224432 3221223088 134558276 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 42171 36800 145 145 0 42026 0 [pid=14895] vsize: 168684 Current children cumulated CPU time (s) 1047.57 Current children cumulated vsize (Kb) 170808 [startup+1060.11 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 37542 0 3 0 105538 219 0 0 25 0 1 0 1793574123 172978176 36861 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 42231 36861 145 145 0 42086 0 [pid=14895] vsize: 168924 Current children cumulated CPU time (s) 1057.57 Current children cumulated vsize (Kb) 171048 [startup+1070.11 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 37601 0 3 0 106537 219 0 0 25 0 1 0 1793574123 173219840 36920 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 42290 36920 145 145 0 42145 0 [pid=14895] vsize: 169160 Current children cumulated CPU time (s) 1067.56 Current children cumulated vsize (Kb) 171284 [startup+1080.11 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 37665 0 3 0 107536 220 0 0 25 0 1 0 1793574123 173490176 36984 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 42356 36984 145 145 0 42211 0 [pid=14895] vsize: 169424 Current children cumulated CPU time (s) 1077.56 Current children cumulated vsize (Kb) 171548 [startup+1090.11 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 37734 0 3 0 108535 220 0 0 25 0 1 0 1793574123 173776896 37053 4294967295 134512640 135094434 3221224432 3221223056 134557619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 42426 37053 145 145 0 42281 0 [pid=14895] vsize: 169704 Current children cumulated CPU time (s) 1087.55 Current children cumulated vsize (Kb) 171828 [startup+1100.11 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 37801 0 3 0 109535 220 0 0 25 0 1 0 1793574123 174047232 37120 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 42492 37120 145 145 0 42347 0 [pid=14895] vsize: 169968 Current children cumulated CPU time (s) 1097.55 Current children cumulated vsize (Kb) 172092 [startup+1110.11 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 37859 0 3 0 110534 221 0 0 25 0 1 0 1793574123 174284800 37178 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 42550 37178 145 145 0 42405 0 [pid=14895] vsize: 170200 Current children cumulated CPU time (s) 1107.55 Current children cumulated vsize (Kb) 172324 [startup+1120.11 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 37919 0 3 0 111533 221 0 0 25 0 1 0 1793574123 174526464 37238 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 42609 37238 145 145 0 42464 0 [pid=14895] vsize: 170436 Current children cumulated CPU time (s) 1117.54 Current children cumulated vsize (Kb) 172560 [startup+1130.11 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 37983 0 3 0 112532 222 0 0 25 0 1 0 1793574123 174796800 37302 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 42675 37302 145 145 0 42530 0 [pid=14895] vsize: 170700 Current children cumulated CPU time (s) 1127.54 Current children cumulated vsize (Kb) 172824 [startup+1140.11 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 38041 0 3 0 113532 222 0 0 25 0 1 0 1793574123 175030272 37360 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 42732 37360 145 145 0 42587 0 [pid=14895] vsize: 170928 Current children cumulated CPU time (s) 1137.54 Current children cumulated vsize (Kb) 173052 [startup+1150.11 s] Raw data (loadavg): 0.99 0.97 0.88 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 38100 0 3 0 114530 223 0 0 25 0 1 0 1793574123 175271936 37419 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 42791 37419 145 145 0 42646 0 [pid=14895] vsize: 171164 Current children cumulated CPU time (s) 1147.53 Current children cumulated vsize (Kb) 173288 [startup+1160.11 s] Raw data (loadavg): 0.99 0.97 0.88 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 38168 0 3 0 115530 224 0 0 25 0 1 0 1793574123 175554560 37487 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 42860 37487 145 145 0 42715 0 [pid=14895] vsize: 171440 Current children cumulated CPU time (s) 1157.54 Current children cumulated vsize (Kb) 173564 [startup+1170.12 s] Raw data (loadavg): 0.99 0.97 0.88 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 38233 0 3 0 116528 225 0 0 25 0 1 0 1793574123 175824896 37552 4294967295 134512640 135094434 3221224432 3221223056 134557681 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 42926 37552 145 145 0 42781 0 [pid=14895] vsize: 171704 Current children cumulated CPU time (s) 1167.53 Current children cumulated vsize (Kb) 173828 [startup+1180.12 s] Raw data (loadavg): 0.99 0.97 0.88 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 38308 0 3 0 117527 225 0 0 25 0 1 0 1793574123 176119808 37627 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 42998 37627 145 145 0 42853 0 [pid=14895] vsize: 171992 Current children cumulated CPU time (s) 1177.52 Current children cumulated vsize (Kb) 174116 [startup+1190.12 s] Raw data (loadavg): 0.99 0.97 0.88 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 38388 0 3 0 118526 226 0 0 25 0 1 0 1793574123 176455680 37707 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 43080 37707 145 145 0 42935 0 [pid=14895] vsize: 172320 Current children cumulated CPU time (s) 1187.52 Current children cumulated vsize (Kb) 174444 [startup+1200.12 s] Raw data (loadavg): 0.99 0.97 0.88 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 38439 0 3 0 119525 226 0 0 25 0 1 0 1793574123 176664576 37758 4294967295 134512640 135094434 3221224432 3221223120 134554796 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 43131 37758 145 145 0 42986 0 [pid=14895] vsize: 172524 Current children cumulated CPU time (s) 1197.51 Current children cumulated vsize (Kb) 174648 [startup+1210.12 s] Raw data (loadavg): 0.99 0.97 0.88 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 38490 0 3 0 120524 227 0 0 25 0 1 0 1793574123 176869376 37809 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 43181 37809 145 145 0 43036 0 [pid=14895] vsize: 172724 Current children cumulated CPU time (s) 1207.51 Current children cumulated vsize (Kb) 174848 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.12 s] Raw data (loadavg): 0.99 0.97 0.88 2/57 14895 Raw data (/proc/14891/stat): 14891 (minisat+_script) S 14890 14891 30740 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793574118 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/14891/statm): 531 226 485 147 0 384 0 [pid=14891] vsize: 2124 Raw data (/proc/14895/stat): 14895 (minisat+_64-bit) R 14891 14891 30740 0 -1 0 38490 0 3 0 120524 227 0 0 25 0 1 0 1793574123 176869376 37809 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14895/statm): 43181 37809 145 145 0 43036 0 [pid=14895] vsize: 172724 Current children cumulated CPU time (s) 1207.51 Current children cumulated vsize (Kb) 174848 Sending SIGTERM to -14891 Sleeping 2 seconds One traced child (pid=14891) ended because it received signal 15 (SIGTERM) One traced child (pid=14895) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.2 CPU time (s): 1207.59 CPU user time (s): 1205.25 CPU system time (s): 2.34364 CPU usage (%): 99.7849 Max. virtual memory (cumulated for all children) (Kb): 174848
ERROR: no interpretation found !