| Name | mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-danoint.opb |
| MD5SUM | 32dd768e34cdc0e1cb04afadbe97060d |
| Bench Category | optimization, medium integers (OPTMEDINT) |
| 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 | 20 |
| Biggest coefficient in the objective function | 524288 |
| Number of bits for the biggest coefficient in the objective function | 20 |
| Sum of the numbers in the objective function | 1048575 |
| Number of bits of the sum of numbers in the objective function | 20 |
| Biggest number in a constraint | 13107200 |
| Number of bits of the biggest number in a constraint | 24 |
| Biggest sum of numbers in a constraint | 52829966 |
| Number of bits of the biggest sum of numbers | 26 |
| Best result obtained on this benchmark | |
| Best CPU time to get the best result obtained on this benchmark | |
| Number of variables | 9304 |
| 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 | 1000 |
LAUNCH ON wulflinc30 THE 2005-09-20 03:35:08 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3291 boxname=wulflinc30 idbench=947 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 32dd768e34cdc0e1cb04afadbe97060d /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-danoint.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-danoint.opb IDLAUNCH: 3291 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.072 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.072 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 865616 kB Buffers: 29416 kB Cached: 109640 kB SwapCached: 752 kB Active: 33828 kB Inactive: 107840 kB HighTotal: 131008 kB HighFree: 27412 kB LowTotal: 903652 kB LowFree: 838204 kB SwapTotal: 2097892 kB SwapFree: 2096620 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5716 kB Slab: 21676 kB Committed_AS: 64304 kB PageTables: 332 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 03:55:19 (client local time) WITH STATUS 0 IN 1206.05 SECONDS stats: 3291 7 1206.05 0
c Parsing PB file... c Converting 816 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ################################################################################################################################################ c -- Clauses(.)/Splits(s): sssssssssssssssssss c ---[ 833]---> BDD-cost: 12 c ---[ 832]---> BDD-cost: 13 c ---[ 831]---> BDD-cost: 13 c ---[ 828]---> BDD-cost: 13 c ---[ 827]---> BDD-cost: 13 c ---[ 825]---> BDD-cost: 15 c ---[ 823]---> BDD-cost: 15 c ---[ 821]---> Adder-cost: 312 maxlim: 56185 bits: 17/16 c ---[ 819]---> Adder-cost: 330 maxlim: 89081 bits: 18/17 c ---[ 817]---> Adder-cost: 322 maxlim: 96761 bits: 18/17 c ---[ 815]---> Adder-cost: 322 maxlim: 96761 bits: 18/17 c ---[ 813]---> Adder-cost: 330 maxlim: 88953 bits: 18/17 c ---[ 811]---> Adder-cost: 330 maxlim: 88953 bits: 18/17 c ---[ 809]---> Adder-cost: 322 maxlim: 96505 bits: 18/17 c ---[ 807]---> Adder-cost: 330 maxlim: 88697 bits: 18/17 c ---[ 805]---> Adder-cost: 323 maxlim: 64889 bits: 17/16 c ---[ 803]---> Adder-cost: 314 maxlim: 72313 bits: 17/17 c ---[ 801]---> BDD-cost: 15 c ---[ 799]---> Adder-cost: 314 maxlim: 72313 bits: 17/17 c ---[ 797]---> Adder-cost: 314 maxlim: 72825 bits: 17/17 c ---[ 795]---> Adder-cost: 314 maxlim: 72569 bits: 17/17 c ---[ 793]---> Adder-cost: 314 maxlim: 71801 bits: 17/17 c ---[ 791]---> Adder-cost: 314 maxlim: 72185 bits: 17/17 c ---[ 789]---> Adder-cost: 312 maxlim: 64761 bits: 17/16 c ---[ 787]---> Adder-cost: 312 maxlim: 64377 bits: 17/16 c ---[ 785]---> Adder-cost: 312 maxlim: 64633 bits: 17/16 c ---[ 783]---> Adder-cost: 312 maxlim: 63737 bits: 17/16 c ---[ 781]---> Adder-cost: 312 maxlim: 64249 bits: 17/16 c ---[ 779]---> BDD-cost: 15 c ---[ 777]---> Adder-cost: 312 maxlim: 63993 bits: 17/16 c ---[ 775]---> Adder-cost: 312 maxlim: 64633 bits: 17/16 c ---[ 773]---> Adder-cost: 312 maxlim: 55929 bits: 17/16 c ---[ 771]---> Adder-cost: 312 maxlim: 56441 bits: 17/16 c ---[ 769]---> Adder-cost: 312 maxlim: 56313 bits: 17/16 c ---[ 767]---> Adder-cost: 312 maxlim: 56569 bits: 17/16 c ---[ 765]---> Adder-cost: 312 maxlim: 56057 bits: 17/16 c ---[ 763]---> Adder-cost: 312 maxlim: 56697 bits: 17/16 c ---[ 761]---> Adder-cost: 312 maxlim: 55545 bits: 17/16 c ---[ 760]---> BDD-cost: 110 c ---[ 758]---> BDD-cost: 15 c ---[ 757]---> BDD-cost: 110 c ---[ 756]---> BDD-cost: 110 c ---[ 755]---> BDD-cost: 110 c ---[ 754]---> BDD-cost: 110 c ---[ 753]---> BDD-cost: 110 c ---[ 752]---> BDD-cost: 110 c ---[ 751]---> BDD-cost: 110 c ---[ 750]---> BDD-cost: 110 c ---[ 749]---> BDD-cost: 110 c ---[ 748]---> BDD-cost: 110 c ---[ 746]---> BDD-cost: 15 c ---[ 745]---> BDD-cost: 110 c ---[ 744]---> BDD-cost: 110 c ---[ 743]---> BDD-cost: 110 c ---[ 742]---> BDD-cost: 110 c ---[ 741]---> BDD-cost: 110 c ---[ 740]---> BDD-cost: 110 c ---[ 739]---> BDD-cost: 110 c ---[ 738]---> BDD-cost: 110 c ---[ 737]---> BDD-cost: 110 c ---[ 736]---> BDD-cost: 110 c ---[ 734]---> BDD-cost: 15 c ---[ 733]---> BDD-cost: 110 c ---[ 732]---> BDD-cost: 110 c ---[ 731]---> BDD-cost: 110 c ---[ 730]---> BDD-cost: 110 c ---[ 729]---> BDD-cost: 110 c ---[ 728]---> BDD-cost: 110 c ---[ 727]---> BDD-cost: 110 c ---[ 726]---> BDD-cost: 110 c ---[ 725]---> BDD-cost: 110 c ---[ 724]---> BDD-cost: 110 c ---[ 722]---> BDD-cost: 15 c ---[ 721]---> BDD-cost: 110 c ---[ 720]---> BDD-cost: 110 c ---[ 719]---> BDD-cost: 110 c ---[ 718]---> BDD-cost: 110 c ---[ 717]---> BDD-cost: 110 c ---[ 716]---> BDD-cost: 110 c ---[ 715]---> BDD-cost: 110 c ---[ 714]---> BDD-cost: 110 c ---[ 713]---> BDD-cost: 110 c ---[ 712]---> BDD-cost: 110 c ---[ 710]---> Sorter-cost: 1752 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 709]---> BDD-cost: 110 c ---[ 708]---> BDD-cost: 110 c ---[ 707]---> BDD-cost: 110 c ---[ 706]---> BDD-cost: 110 c ---[ 705]---> BDD-cost: 110 c ---[ 704]---> BDD-cost: 110 c ---[ 703]---> BDD-cost: 110 c ---[ 702]---> BDD-cost: 110 c ---[ 701]---> BDD-cost: 110 c ---[ 700]---> BDD-cost: 110 c ---[ 698]---> Sorter-cost: 1784 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 697]---> BDD-cost: 110 c ---[ 696]---> BDD-cost: 110 c ---[ 695]---> BDD-cost: 110 c ---[ 694]---> BDD-cost: 110 c ---[ 693]---> BDD-cost: 110 c ---[ 692]---> BDD-cost: 22 c ---[ 691]---> BDD-cost: 18 c ---[ 690]---> BDD-cost: 16 c ---[ 689]---> BDD-cost: 22 c ---[ 688]---> BDD-cost: 21 c ---[ 686]---> Sorter-cost: 1784 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 685]---> BDD-cost: 19 c ---[ 684]---> BDD-cost: 18 c ---[ 683]---> BDD-cost: 22 c ---[ 682]---> BDD-cost: 22 c ---[ 681]---> BDD-cost: 16 c ---[ 680]---> BDD-cost: 22 c ---[ 679]---> BDD-cost: 21 c ---[ 678]---> BDD-cost: 19 c ---[ 677]---> BDD-cost: 18 c ---[ 676]---> BDD-cost: 22 c ---[ 674]---> BDD-cost: 15 c ---[ 672]---> Sorter-cost: 1752 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 671]---> BDD-cost: 22 c ---[ 670]---> BDD-cost: 18 c ---[ 669]---> BDD-cost: 22 c ---[ 668]---> BDD-cost: 21 c ---[ 667]---> BDD-cost: 19 c ---[ 666]---> BDD-cost: 18 c ---[ 665]---> BDD-cost: 22 c ---[ 664]---> BDD-cost: 22 c ---[ 663]---> BDD-cost: 18 c ---[ 662]---> BDD-cost: 16 c ---[ 660]---> Sorter-cost: 1752 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 659]---> BDD-cost: 21 c ---[ 658]---> BDD-cost: 19 c ---[ 657]---> BDD-cost: 18 c ---[ 656]---> BDD-cost: 22 c ---[ 655]---> BDD-cost: 22 c ---[ 654]---> BDD-cost: 18 c ---[ 653]---> BDD-cost: 16 c ---[ 652]---> BDD-cost: 22 c ---[ 651]---> BDD-cost: 19 c ---[ 650]---> BDD-cost: 18 c ---[ 648]---> Sorter-cost: 1784 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 647]---> BDD-cost: 22 c ---[ 646]---> BDD-cost: 22 c ---[ 645]---> BDD-cost: 18 c ---[ 644]---> BDD-cost: 16 c ---[ 643]---> BDD-cost: 22 c ---[ 642]---> BDD-cost: 21 c ---[ 641]---> BDD-cost: 18 c ---[ 640]---> BDD-cost: 22 c ---[ 639]---> BDD-cost: 22 c ---[ 638]---> BDD-cost: 18 c ---[ 636]---> Sorter-cost: 1784 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 635]---> BDD-cost: 16 c ---[ 634]---> BDD-cost: 22 c ---[ 633]---> BDD-cost: 21 c ---[ 632]---> BDD-cost: 19 c ---[ 631]---> BDD-cost: 22 c ---[ 630]---> BDD-cost: 18 c ---[ 629]---> BDD-cost: 19 c ---[ 628]---> BDD-cost: 19 c ---[ 627]---> BDD-cost: 19 c ---[ 626]---> BDD-cost: 16 c ---[ 624]---> Sorter-cost: 1700 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 623]---> BDD-cost: 18 c ---[ 622]---> BDD-cost: 15 c ---[ 621]---> BDD-cost: 22 c ---[ 620]---> BDD-cost: 19 c ---[ 619]---> BDD-cost: 19 c ---[ 618]---> BDD-cost: 19 c ---[ 617]---> BDD-cost: 16 c ---[ 616]---> BDD-cost: 18 c ---[ 615]---> BDD-cost: 15 c ---[ 614]---> BDD-cost: 22 c ---[ 612]---> Sorter-cost: 1728 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 611]---> BDD-cost: 18 c ---[ 610]---> BDD-cost: 19 c ---[ 609]---> BDD-cost: 19 c ---[ 608]---> BDD-cost: 16 c ---[ 607]---> BDD-cost: 18 c ---[ 606]---> BDD-cost: 15 c ---[ 605]---> BDD-cost: 22 c ---[ 604]---> BDD-cost: 18 c ---[ 603]---> BDD-cost: 19 c ---[ 602]---> BDD-cost: 19 c ---[ 600]---> Sorter-cost: 1728 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 599]---> BDD-cost: 16 c ---[ 598]---> BDD-cost: 18 c ---[ 597]---> BDD-cost: 15 c ---[ 596]---> BDD-cost: 22 c ---[ 595]---> BDD-cost: 18 c ---[ 594]---> BDD-cost: 19 c ---[ 593]---> BDD-cost: 19 c ---[ 592]---> BDD-cost: 16 c ---[ 591]---> BDD-cost: 18 c ---[ 590]---> BDD-cost: 15 c ---[ 588]---> Sorter-cost: 1728 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 587]---> BDD-cost: 22 c ---[ 586]---> BDD-cost: 18 c ---[ 585]---> BDD-cost: 19 c ---[ 584]---> BDD-cost: 19 c ---[ 583]---> BDD-cost: 19 c ---[ 582]---> BDD-cost: 18 c ---[ 581]---> BDD-cost: 15 c ---[ 580]---> BDD-cost: 22 c ---[ 579]---> BDD-cost: 18 c ---[ 578]---> BDD-cost: 19 c ---[ 576]---> Sorter-cost: 1728 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 575]---> BDD-cost: 19 c ---[ 574]---> BDD-cost: 19 c ---[ 573]---> BDD-cost: 16 c ---[ 572]---> BDD-cost: 20 c ---[ 571]---> BDD-cost: 19 c ---[ 570]---> BDD-cost: 15 c ---[ 569]---> BDD-cost: 19 c ---[ 568]---> BDD-cost: 19 c ---[ 567]---> BDD-cost: 18 c ---[ 566]---> BDD-cost: 19 c ---[ 564]---> Sorter-cost: 1728 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 563]---> BDD-cost: 22 c ---[ 562]---> BDD-cost: 19 c ---[ 561]---> BDD-cost: 15 c ---[ 560]---> BDD-cost: 19 c ---[ 559]---> BDD-cost: 19 c ---[ 558]---> BDD-cost: 18 c ---[ 557]---> BDD-cost: 19 c ---[ 556]---> BDD-cost: 22 c ---[ 555]---> BDD-cost: 20 c ---[ 554]---> BDD-cost: 19 c ---[ 552]---> BDD-cost: 15 c ---[ 550]---> Sorter-cost: 1728 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 549]---> BDD-cost: 19 c ---[ 548]---> BDD-cost: 19 c ---[ 547]---> BDD-cost: 18 c ---[ 546]---> BDD-cost: 19 c ---[ 545]---> BDD-cost: 22 c ---[ 544]---> BDD-cost: 20 c ---[ 543]---> BDD-cost: 19 c ---[ 542]---> BDD-cost: 15 c ---[ 541]---> BDD-cost: 19 c ---[ 540]---> BDD-cost: 18 c ---[ 538]---> Sorter-cost: 1700 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 537]---> BDD-cost: 19 c ---[ 536]---> BDD-cost: 22 c ---[ 535]---> BDD-cost: 20 c ---[ 534]---> BDD-cost: 19 c ---[ 533]---> BDD-cost: 15 c ---[ 532]---> BDD-cost: 19 c ---[ 531]---> BDD-cost: 18 c ---[ 530]---> BDD-cost: 19 c ---[ 529]---> BDD-cost: 22 c ---[ 528]---> BDD-cost: 20 c ---[ 526]---> Sorter-cost: 1700 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 525]---> BDD-cost: 19 c ---[ 524]---> BDD-cost: 15 c ---[ 523]---> BDD-cost: 19 c ---[ 522]---> BDD-cost: 19 c ---[ 521]---> BDD-cost: 19 c ---[ 520]---> BDD-cost: 22 c ---[ 519]---> BDD-cost: 20 c ---[ 518]---> BDD-cost: 19 c ---[ 517]---> BDD-cost: 15 c ---[ 516]---> BDD-cost: 19 c ---[ 514]---> Sorter-cost: 1728 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 513]---> BDD-cost: 19 c ---[ 512]---> BDD-cost: 18 c ---[ 511]---> BDD-cost: 22 c ---[ 510]---> BDD-cost: 17 c ---[ 509]---> BDD-cost: 19 c ---[ 508]---> BDD-cost: 20 c ---[ 507]---> BDD-cost: 19 c ---[ 506]---> BDD-cost: 19 c ---[ 505]---> BDD-cost: 19 c ---[ 504]---> BDD-cost: 19 c ---[ 502]---> Sorter-cost: 1728 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 501]---> BDD-cost: 17 c ---[ 500]---> BDD-cost: 19 c ---[ 499]---> BDD-cost: 20 c ---[ 498]---> BDD-cost: 19 c ---[ 497]---> BDD-cost: 19 c ---[ 496]---> BDD-cost: 19 c ---[ 495]---> BDD-cost: 19 c ---[ 494]---> BDD-cost: 22 c ---[ 493]---> BDD-cost: 19 c ---[ 492]---> BDD-cost: 20 c ---[ 490]---> Sorter-cost: 1728 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 489]---> BDD-cost: 19 c ---[ 488]---> BDD-cost: 19 c ---[ 487]---> BDD-cost: 19 c ---[ 486]---> BDD-cost: 19 c ---[ 485]---> BDD-cost: 22 c ---[ 484]---> BDD-cost: 17 c ---[ 483]---> BDD-cost: 19 c ---[ 482]---> BDD-cost: 19 c ---[ 481]---> BDD-cost: 19 c ---[ 480]---> BDD-cost: 19 c ---[ 478]---> Sorter-cost: 1728 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 477]---> BDD-cost: 19 c ---[ 476]---> BDD-cost: 22 c ---[ 475]---> BDD-cost: 17 c ---[ 474]---> BDD-cost: 19 c ---[ 473]---> BDD-cost: 20 c ---[ 472]---> BDD-cost: 19 c ---[ 471]---> BDD-cost: 19 c ---[ 470]---> BDD-cost: 19 c ---[ 469]---> BDD-cost: 22 c ---[ 468]---> BDD-cost: 17 c ---[ 466]---> Sorter-cost: 1728 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 465]---> BDD-cost: 19 c ---[ 464]---> BDD-cost: 20 c ---[ 463]---> BDD-cost: 19 c ---[ 462]---> BDD-cost: 19 c ---[ 461]---> BDD-cost: 19 c ---[ 460]---> BDD-cost: 22 c ---[ 459]---> BDD-cost: 17 c ---[ 458]---> BDD-cost: 19 c ---[ 457]---> BDD-cost: 20 c ---[ 456]---> BDD-cost: 19 c ---[ 454]---> Sorter-cost: 1728 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 453]---> BDD-cost: 19 c ---[ 452]---> BDD-cost: 22 c ---[ 451]---> BDD-cost: 19 c ---[ 450]---> BDD-cost: 16 c ---[ 449]---> BDD-cost: 22 c ---[ 448]---> BDD-cost: 19 c ---[ 447]---> BDD-cost: 19 c ---[ 446]---> BDD-cost: 19 c ---[ 445]---> BDD-cost: 18 c ---[ 444]---> BDD-cost: 19 c ---[ 442]---> Sorter-cost: 1700 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 441]---> BDD-cost: 16 c ---[ 440]---> BDD-cost: 22 c ---[ 439]---> BDD-cost: 19 c ---[ 438]---> BDD-cost: 19 c ---[ 437]---> BDD-cost: 19 c ---[ 436]---> BDD-cost: 18 c ---[ 435]---> BDD-cost: 22 c ---[ 434]---> BDD-cost: 16 c ---[ 433]---> BDD-cost: 22 c ---[ 432]---> BDD-cost: 19 c ---[ 430]---> BDD-cost: 15 c ---[ 428]---> Sorter-cost: 1728 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 427]---> BDD-cost: 19 c ---[ 426]---> BDD-cost: 19 c ---[ 425]---> BDD-cost: 18 c ---[ 424]---> BDD-cost: 22 c ---[ 423]---> BDD-cost: 19 c ---[ 422]---> BDD-cost: 22 c ---[ 421]---> BDD-cost: 19 c ---[ 420]---> BDD-cost: 19 c ---[ 419]---> BDD-cost: 19 c ---[ 418]---> BDD-cost: 18 c ---[ 416]---> Sorter-cost: 1700 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 415]---> BDD-cost: 22 c ---[ 414]---> BDD-cost: 19 c ---[ 413]---> BDD-cost: 16 c ---[ 412]---> BDD-cost: 22 c ---[ 411]---> BDD-cost: 19 c ---[ 410]---> BDD-cost: 19 c ---[ 409]---> BDD-cost: 18 c ---[ 408]---> BDD-cost: 22 c ---[ 407]---> BDD-cost: 19 c ---[ 406]---> BDD-cost: 16 c ---[ 404]---> Sorter-cost: 1728 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 403]---> BDD-cost: 22 c ---[ 402]---> BDD-cost: 19 c ---[ 401]---> BDD-cost: 19 c ---[ 400]---> BDD-cost: 18 c ---[ 399]---> BDD-cost: 22 c ---[ 398]---> BDD-cost: 19 c ---[ 397]---> BDD-cost: 16 c ---[ 396]---> BDD-cost: 22 c ---[ 395]---> BDD-cost: 19 c ---[ 394]---> BDD-cost: 19 c ---[ 392]---> Sorter-cost: 1728 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 391]---> BDD-cost: 22 c ---[ 390]---> BDD-cost: 18 c ---[ 389]---> BDD-cost: 19 c ---[ 388]---> BDD-cost: 20 c ---[ 387]---> BDD-cost: 22 c ---[ 386]---> BDD-cost: 19 c ---[ 385]---> BDD-cost: 16 c ---[ 384]---> BDD-cost: 19 c ---[ 383]---> BDD-cost: 18 c ---[ 382]---> BDD-cost: 19 c ---[ 380]---> Sorter-cost: 1728 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 379]---> BDD-cost: 20 c ---[ 378]---> BDD-cost: 22 c ---[ 377]---> BDD-cost: 19 c ---[ 376]---> BDD-cost: 16 c ---[ 375]---> BDD-cost: 19 c ---[ 374]---> BDD-cost: 22 c ---[ 373]---> BDD-cost: 19 c ---[ 372]---> BDD-cost: 20 c ---[ 371]---> BDD-cost: 22 c ---[ 370]---> BDD-cost: 19 c ---[ 368]---> Sorter-cost: 1728 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 367]---> BDD-cost: 16 c ---[ 366]---> BDD-cost: 19 c ---[ 365]---> BDD-cost: 22 c ---[ 364]---> BDD-cost: 18 c ---[ 363]---> BDD-cost: 20 c ---[ 362]---> BDD-cost: 22 c ---[ 361]---> BDD-cost: 19 c ---[ 360]---> BDD-cost: 16 c ---[ 359]---> BDD-cost: 19 c ---[ 358]---> BDD-cost: 22 c ---[ 356]---> Sorter-cost: 1700 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 355]---> BDD-cost: 18 c ---[ 354]---> BDD-cost: 19 c ---[ 353]---> BDD-cost: 22 c ---[ 352]---> BDD-cost: 19 c ---[ 351]---> BDD-cost: 16 c ---[ 350]---> BDD-cost: 19 c ---[ 349]---> BDD-cost: 22 c ---[ 348]---> BDD-cost: 18 c ---[ 347]---> BDD-cost: 19 c ---[ 346]---> BDD-cost: 20 c ---[ 344]---> Sorter-cost: 1728 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 343]---> BDD-cost: 22 c ---[ 342]---> BDD-cost: 16 c ---[ 341]---> BDD-cost: 19 c ---[ 340]---> BDD-cost: 22 c ---[ 339]---> BDD-cost: 18 c ---[ 338]---> BDD-cost: 19 c ---[ 337]---> BDD-cost: 20 c ---[ 336]---> BDD-cost: 22 c ---[ 335]---> BDD-cost: 19 c ---[ 334]---> BDD-cost: 22 c ---[ 332]---> Sorter-cost: 1728 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 331]---> BDD-cost: 17 c ---[ 330]---> BDD-cost: 17 c ---[ 329]---> BDD-cost: 19 c ---[ 328]---> BDD-cost: 19 c ---[ 327]---> BDD-cost: 21 c ---[ 326]---> BDD-cost: 19 c ---[ 325]---> BDD-cost: 22 c ---[ 324]---> BDD-cost: 17 c ---[ 323]---> BDD-cost: 17 c ---[ 322]---> BDD-cost: 19 c ---[ 320]---> Sorter-cost: 1728 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 319]---> BDD-cost: 19 c ---[ 318]---> BDD-cost: 21 c ---[ 317]---> BDD-cost: 19 c ---[ 316]---> BDD-cost: 22 c ---[ 315]---> BDD-cost: 22 c ---[ 314]---> BDD-cost: 17 c ---[ 313]---> BDD-cost: 19 c ---[ 312]---> BDD-cost: 19 c ---[ 311]---> BDD-cost: 21 c ---[ 310]---> BDD-cost: 19 c ---[ 308]---> BDD-cost: 15 c ---[ 306]---> Sorter-cost: 1728 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 305]---> BDD-cost: 22 c ---[ 304]---> BDD-cost: 22 c ---[ 303]---> BDD-cost: 17 c ---[ 302]---> BDD-cost: 19 c ---[ 301]---> BDD-cost: 19 c ---[ 300]---> BDD-cost: 21 c ---[ 299]---> BDD-cost: 19 c ---[ 298]---> BDD-cost: 22 c ---[ 297]---> BDD-cost: 22 c ---[ 296]---> BDD-cost: 17 c ---[ 294]---> Sorter-cost: 1728 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 293]---> BDD-cost: 17 c ---[ 292]---> BDD-cost: 19 c ---[ 291]---> BDD-cost: 21 c ---[ 290]---> BDD-cost: 19 c ---[ 289]---> BDD-cost: 22 c ---[ 288]---> BDD-cost: 22 c ---[ 287]---> BDD-cost: 17 c ---[ 286]---> BDD-cost: 17 c ---[ 285]---> BDD-cost: 19 c ---[ 284]---> BDD-cost: 21 c ---[ 282]---> Sorter-cost: 1752 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 281]---> BDD-cost: 19 c ---[ 280]---> BDD-cost: 22 c ---[ 279]---> BDD-cost: 22 c ---[ 278]---> BDD-cost: 17 c ---[ 277]---> BDD-cost: 17 c ---[ 276]---> BDD-cost: 19 c ---[ 275]---> BDD-cost: 19 c ---[ 274]---> BDD-cost: 21 c ---[ 273]---> BDD-cost: 22 c ---[ 272]---> BDD-cost: 19 c ---[ 270]---> Sorter-cost: 1728 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 269]---> BDD-cost: 18 c ---[ 268]---> BDD-cost: 15 c ---[ 267]---> BDD-cost: 18 c ---[ 266]---> BDD-cost: 18 c ---[ 265]---> BDD-cost: 19 c ---[ 264]---> BDD-cost: 19 c ---[ 263]---> BDD-cost: 19 c ---[ 262]---> BDD-cost: 18 c ---[ 261]---> BDD-cost: 15 c ---[ 260]---> BDD-cost: 18 c ---[ 258]---> Sorter-cost: 1752 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 257]---> BDD-cost: 18 c ---[ 256]---> BDD-cost: 19 c ---[ 255]---> BDD-cost: 19 c ---[ 254]---> BDD-cost: 22 c ---[ 253]---> BDD-cost: 18 c ---[ 252]---> BDD-cost: 15 c ---[ 251]---> BDD-cost: 18 c ---[ 250]---> BDD-cost: 18 c ---[ 249]---> BDD-cost: 19 c ---[ 248]---> BDD-cost: 19 c ---[ 246]---> Sorter-cost: 1752 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 245]---> BDD-cost: 22 c ---[ 244]---> BDD-cost: 19 c ---[ 243]---> BDD-cost: 15 c ---[ 242]---> BDD-cost: 18 c ---[ 241]---> BDD-cost: 18 c ---[ 240]---> BDD-cost: 19 c ---[ 239]---> BDD-cost: 19 c ---[ 238]---> BDD-cost: 22 c ---[ 237]---> BDD-cost: 19 c ---[ 236]---> BDD-cost: 18 c ---[ 234]---> Sorter-cost: 1728 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 233]---> BDD-cost: 18 c ---[ 232]---> BDD-cost: 18 c ---[ 231]---> BDD-cost: 19 c ---[ 230]---> BDD-cost: 19 c ---[ 229]---> BDD-cost: 22 c ---[ 228]---> BDD-cost: 19 c ---[ 227]---> BDD-cost: 18 c ---[ 226]---> BDD-cost: 15 c ---[ 225]---> BDD-cost: 18 c ---[ 224]---> BDD-cost: 19 c ---[ 222]---> Sorter-cost: 1752 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 221]---> BDD-cost: 19 c ---[ 220]---> BDD-cost: 22 c ---[ 219]---> BDD-cost: 19 c ---[ 218]---> BDD-cost: 18 c ---[ 217]---> BDD-cost: 15 c ---[ 216]---> BDD-cost: 18 c ---[ 215]---> BDD-cost: 19 c ---[ 213]---> Adder-cost: 1336 maxlim: 1048575 bits: 21/20 c ---[ 211]---> Adder-cost: 1384 maxlim: 1048575 bits: 21/20 c ---[ 209]---> Adder-cost: 1286 maxlim: 524287 bits: 20/19 c ---[ 207]---> Sorter-cost: 1752 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 205]---> Adder-cost: 1193 maxlim: 524287 bits: 20/19 c ---[ 203]---> Adder-cost: 1180 maxlim: 1048575 bits: 21/20 c ---[ 201]---> Adder-cost: 1145 maxlim: 524287 bits: 20/19 c ---[ 199]---> Adder-cost: 1137 maxlim: 524287 bits: 20/19 c ---[ 197]---> Adder-cost: 1129 maxlim: 524287 bits: 20/19 c ---[ 190]---> Sorter-cost: 1728 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 185]---> Sorter-cost: 1924 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 182]---> Sorter-cost: 1925 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 179]---> Sorter-cost: 1923 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 176]---> Sorter-cost: 1923 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 174]---> BDD-cost: 15 c ---[ 172]---> Sorter-cost: 1728 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 169]---> Sorter-cost: 1925 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 166]---> Sorter-cost: 1924 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 163]---> Sorter-cost: 1923 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 160]---> Sorter-cost: 1923 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 158]---> Sorter-cost: 1572 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 156]---> Sorter-cost: 1752 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 155]---> Sorter-cost: 1596 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 154]---> Sorter-cost: 1398 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 153]---> Sorter-cost: 1363 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 152]---> Sorter-cost: 1398 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 151]---> Sorter-cost: 1572 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 150]---> Sorter-cost: 1398 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 149]---> Sorter-cost: 1585 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 148]---> Sorter-cost: 1609 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 147]---> Sorter-cost: 1596 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 146]---> Sorter-cost: 1561 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 144]---> Sorter-cost: 1752 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 143]---> Sorter-cost: 1583 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 142]---> Sorter-cost: 1583 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 141]---> Sorter-cost: 1583 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 140]---> Sorter-cost: 1476 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 139]---> Sorter-cost: 1463 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 138]---> Sorter-cost: 1476 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 137]---> Sorter-cost: 1452 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 136]---> Sorter-cost: 1463 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 135]---> Sorter-cost: 1476 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 134]---> Sorter-cost: 1417 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 132]---> Sorter-cost: 1752 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 131]---> Sorter-cost: 1476 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 130]---> Sorter-cost: 1417 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 129]---> Sorter-cost: 1489 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 128]---> Sorter-cost: 1476 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 127]---> Sorter-cost: 1452 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 126]---> Sorter-cost: 1476 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 125]---> Sorter-cost: 1463 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 124]---> Sorter-cost: 1537 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 123]---> Sorter-cost: 1363 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 122]---> Sorter-cost: 1363 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 120]---> Sorter-cost: 1752 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 119]---> Sorter-cost: 1583 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 118]---> Sorter-cost: 1583 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 117]---> Sorter-cost: 1387 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 116]---> Sorter-cost: 1596 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 115]---> Sorter-cost: 1583 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 114]---> Sorter-cost: 1398 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 113]---> Sorter-cost: 1398 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 112]---> Sorter-cost: 1398 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 111]---> Sorter-cost: 1385 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 110]---> Sorter-cost: 1411 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 108]---> Sorter-cost: 1752 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 107]---> Sorter-cost: 1363 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 106]---> Sorter-cost: 1374 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 105]---> Sorter-cost: 1385 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 104]---> Sorter-cost: 1398 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 103]---> Sorter-cost: 1387 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 102]---> Sorter-cost: 1374 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 101]---> Sorter-cost: 1363 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 100]---> Sorter-cost: 1398 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 99]---> Sorter-cost: 1476 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 98]---> Sorter-cost: 1476 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 96]---> Sorter-cost: 1728 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 95]---> Sorter-cost: 1417 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 94]---> Sorter-cost: 1452 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 93]---> Sorter-cost: 1452 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 92]---> Sorter-cost: 1463 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 91]---> Sorter-cost: 1465 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 89]---> Sorter-cost: 1700 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 87]---> Sorter-cost: 1728 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 85]---> Sorter-cost: 1728 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 83]---> BDD-cost: 15 c ---[ 81]---> Sorter-cost: 1700 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 79]---> Sorter-cost: 1728 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 77]---> Sorter-cost: 1728 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 75]---> Adder-cost: 300 maxlim: 80633 bits: 18/17 c ---[ 73]---> Adder-cost: 328 maxlim: 81017 bits: 18/17 c ---[ 71]---> Adder-cost: 322 maxlim: 88441 bits: 18/17 c ---[ 69]---> Adder-cost: 296 maxlim: 88569 bits: 18/17 c ---[ 67]---> Adder-cost: 322 maxlim: 88441 bits: 18/17 c ---[ 65]---> Adder-cost: 328 maxlim: 81145 bits: 18/17 c ---[ 63]---> Adder-cost: 283 maxlim: 88441 bits: 18/17 c ---[ 61]---> BDD-cost: 15 c ---[ 59]---> Adder-cost: 280 maxlim: 112889 bits: 18/17 c ---[ 57]---> Adder-cost: 336 maxlim: 112761 bits: 18/17 c ---[ 55]---> Adder-cost: 336 maxlim: 113017 bits: 18/17 c ---[ 53]---> Adder-cost: 308 maxlim: 113145 bits: 18/17 c ---[ 51]---> Adder-cost: 336 maxlim: 113529 bits: 18/17 c ---[ 49]---> Adder-cost: 336 maxlim: 113529 bits: 18/17 c ---[ 47]---> Adder-cost: 294 maxlim: 113529 bits: 18/17 c ---[ 45]---> Adder-cost: 260 maxlim: 55673 bits: 17/16 c ---[ 43]---> Adder-cost: 312 maxlim: 56185 bits: 17/16 c ---[ 41]---> Adder-cost: 312 maxlim: 55929 bits: 17/16 c ---[ 39]---> BDD-cost: 15 c ---[ 37]---> Adder-cost: 286 maxlim: 56569 bits: 17/16 c ---[ 35]---> Adder-cost: 312 maxlim: 56697 bits: 17/16 c ---[ 33]---> Adder-cost: 312 maxlim: 55929 bits: 17/16 c ---[ 31]---> Adder-cost: 273 maxlim: 56313 bits: 17/16 c ---[ 29]---> Adder-cost: 312 maxlim: 56441 bits: 17/16 c ---[ 27]---> Adder-cost: 286 maxlim: 56313 bits: 17/16 c ---[ 25]---> Adder-cost: 312 maxlim: 55417 bits: 17/16 c ---[ 23]---> Adder-cost: 312 maxlim: 56441 bits: 17/16 c ---[ 21]---> Adder-cost: 312 maxlim: 56569 bits: 17/16 c ---[ 19]---> Adder-cost: 286 maxlim: 55929 bits: 17/16 c ---[ 18]---> BDD-cost: 10 c ---[ 17]---> BDD-cost: 10 c ---[ 16]---> BDD-cost: 7 c ---[ 15]---> Sorter-cost: 435 Base: 2 2 2 2 2 2 2 2 2 3 5 c ---[ 14]---> Sorter-cost: 420 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 13]---> Sorter-cost: 278 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 12]---> Sorter-cost: 314 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 11]---> Sorter-cost: 298 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 10]---> Sorter-cost: 332 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 9]---> Sorter-cost: 293 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 8]---> Sorter-cost: 381 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 7]---> BDD-cost: 49 c ---[ 6]---> BDD-cost: 51 c ---[ 5]---> BDD-cost: 54 c ---[ 4]---> BDD-cost: 54 c ---[ 3]---> BDD-cost: 51 c ---[ 2]---> BDD-cost: 49 c ---[ 1]---> BDD-cost: 54 c ---[ 0]---> BDD-cost: 54 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 685188 1832230 | 228396 0 0 nan | 0.000 % | c | 101 | 685110 1832061 | 251235 95 372 3.9 | 4.002 % | c | 251 | 684916 1831618 | 276359 226 1027 4.5 | 4.018 % | c | 476 | 684773 1831293 | 303995 422 2140 5.1 | 4.038 % | c | 813 | 684765 1831267 | 334394 758 6790 9.0 | 4.038 % | c | 1320 | 684666 1831031 | 367834 1259 11559 9.2 | 4.049 % | c | 2079 | 684300 1830216 | 404617 1978 17448 8.8 | 4.100 % | c | 3218 | 683957 1829446 | 445079 3066 39578 12.9 | 4.146 % | c | 4926 | 683558 1828563 | 489587 4741 74053 15.6 | 4.199 % | c | 7489 | 683180 1827732 | 538545 7268 217137 29.9 | 4.247 % | c | 11333 | 682437 1826073 | 592400 11004 347538 31.6 | 4.343 % | c | 17099 | 681123 1823090 | 651640 16662 456790 27.4 | 4.516 % | c | 25748 | 680147 1820891 | 716804 25173 577625 22.9 | 4.642 % | c | 38722 | 679741 1819902 | 788484 38109 803039 21.1 | 4.690 % | c | 58183 | 679139 1818548 | 867333 57536 1418479 24.7 | 4.766 % | c | 87376 | 679102 1818467 | 954066 86723 5179814 59.7 | 4.772 % | c | 131167 | 678702 1817587 | 1049473 130474 8940803 68.5 | 4.826 % | c | 196853 | 678150 1816369 | 1154420 196088 15507844 79.1 | 4.899 % | c | 295380 | 677613 1815193 | 1269862 294554 29637337 100.6 | 4.973 % |
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/3379/stat): 3379 (minisat+_script) R 3378 3379 5245 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1855325638 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/3379/statm): 174 3 169 147 0 27 0 [pid=3379] 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=3380 New process pid=3381 New process pid=3382 execve syscall for /bin/sed executable One traced child (pid=3381) 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=3382) exited with status: 0 One traced child (pid=3380) exited with status: 0 New process pid=3383 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-danoint.opb [startup+10.0044 s] Raw data (loadavg): 0.87 0.97 0.88 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 18530 0 0 0 845 74 0 0 25 0 1 0 1855325643 78454784 17817 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3383/statm): 19154 17817 145 145 0 19009 0 [pid=3383] vsize: 76616 Current children cumulated CPU time (s) 9.2 Current children cumulated vsize (Kb) 78740 [startup+20.0052 s] Raw data (loadavg): 0.89 0.97 0.89 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 18777 0 0 0 1841 76 0 0 25 0 1 0 1855325643 79175680 18064 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 19330 18064 145 145 0 19185 0 [pid=3383] vsize: 77320 Current children cumulated CPU time (s) 19.18 Current children cumulated vsize (Kb) 79444 [startup+30.006 s] Raw data (loadavg): 0.91 0.97 0.89 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 18832 0 0 0 2840 76 0 0 25 0 1 0 1855325643 79343616 18119 4294967295 134512640 135094434 3221224432 3221223104 134556543 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3383/statm): 19371 18119 145 145 0 19226 0 [pid=3383] vsize: 77484 Current children cumulated CPU time (s) 29.17 Current children cumulated vsize (Kb) 79608 [startup+40.0078 s] Raw data (loadavg): 0.92 0.97 0.89 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 18858 0 0 0 3840 77 0 0 25 0 1 0 1855325643 79446016 18145 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 19396 18145 145 145 0 19251 0 [pid=3383] vsize: 77584 Current children cumulated CPU time (s) 39.18 Current children cumulated vsize (Kb) 79708 [startup+50.0085 s] Raw data (loadavg): 0.93 0.97 0.89 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 18909 0 0 0 4839 77 0 0 25 0 1 0 1855325643 79654912 18196 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 19447 18196 145 145 0 19302 0 [pid=3383] vsize: 77788 Current children cumulated CPU time (s) 49.17 Current children cumulated vsize (Kb) 79912 [startup+60.0093 s] Raw data (loadavg): 0.94 0.97 0.89 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 18926 0 0 0 5839 77 0 0 25 0 1 0 1855325643 79736832 18213 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 19467 18213 145 145 0 19322 0 [pid=3383] vsize: 77868 Current children cumulated CPU time (s) 59.17 Current children cumulated vsize (Kb) 79992 [startup+70.0101 s] Raw data (loadavg): 0.95 0.97 0.89 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 18938 0 0 0 6839 77 0 0 25 0 1 0 1855325643 79781888 18225 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 19478 18225 145 145 0 19333 0 [pid=3383] vsize: 77912 Current children cumulated CPU time (s) 69.17 Current children cumulated vsize (Kb) 80036 [startup+80.0109 s] Raw data (loadavg): 0.96 0.97 0.89 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 19106 0 0 0 7836 78 0 0 25 0 1 0 1855325643 80461824 18393 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 19644 18393 145 145 0 19499 0 [pid=3383] vsize: 78576 Current children cumulated CPU time (s) 79.15 Current children cumulated vsize (Kb) 80700 [startup+90.0117 s] Raw data (loadavg): 0.96 0.97 0.89 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 19212 0 0 0 8834 78 0 0 25 0 1 0 1855325643 80920576 18499 4294967295 134512640 135094434 3221224432 3221223088 134557859 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 19756 18499 145 145 0 19611 0 [pid=3383] vsize: 79024 Current children cumulated CPU time (s) 89.13 Current children cumulated vsize (Kb) 81148 [startup+100.012 s] Raw data (loadavg): 0.97 0.97 0.89 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 19265 0 0 0 9834 79 0 0 25 0 1 0 1855325643 81125376 18552 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 19806 18552 145 145 0 19661 0 [pid=3383] vsize: 79224 Current children cumulated CPU time (s) 99.14 Current children cumulated vsize (Kb) 81348 [startup+110.014 s] Raw data (loadavg): 0.97 0.97 0.89 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 19315 0 0 0 10833 79 0 0 25 0 1 0 1855325643 81260544 18602 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 19839 18602 145 145 0 19694 0 [pid=3383] vsize: 79356 Current children cumulated CPU time (s) 109.13 Current children cumulated vsize (Kb) 81480 [startup+120.015 s] Raw data (loadavg): 0.98 0.97 0.90 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 19384 0 0 0 11833 79 0 0 25 0 1 0 1855325643 81530880 18671 4294967295 134512640 135094434 3221224432 3221223056 134557669 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 19905 18671 145 145 0 19760 0 [pid=3383] vsize: 79620 Current children cumulated CPU time (s) 119.13 Current children cumulated vsize (Kb) 81744 [startup+130.016 s] Raw data (loadavg): 0.98 0.97 0.90 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 19419 0 0 0 12832 80 0 0 25 0 1 0 1855325643 81670144 18706 4294967295 134512640 135094434 3221224432 3221223104 134553523 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 19939 18706 145 145 0 19794 0 [pid=3383] vsize: 79756 Current children cumulated CPU time (s) 129.13 Current children cumulated vsize (Kb) 81880 [startup+140.017 s] Raw data (loadavg): 0.98 0.97 0.90 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 19476 0 0 0 13831 80 0 0 25 0 1 0 1855325643 81899520 18763 4294967295 134512640 135094434 3221224432 3221223056 134557612 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 19995 18763 145 145 0 19850 0 [pid=3383] vsize: 79980 Current children cumulated CPU time (s) 139.12 Current children cumulated vsize (Kb) 82104 [startup+150.017 s] Raw data (loadavg): 0.98 0.97 0.90 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 19501 0 0 0 14831 80 0 0 25 0 1 0 1855325643 82067456 18788 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 20036 18788 145 145 0 19891 0 [pid=3383] vsize: 80144 Current children cumulated CPU time (s) 149.12 Current children cumulated vsize (Kb) 82268 [startup+160.018 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 19528 0 0 0 15831 80 0 0 25 0 1 0 1855325643 82173952 18815 4294967295 134512640 135094434 3221224432 3221223092 134553444 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 20062 18815 145 145 0 19917 0 [pid=3383] vsize: 80248 Current children cumulated CPU time (s) 159.12 Current children cumulated vsize (Kb) 82372 [startup+170.019 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 19573 0 0 0 16831 81 0 0 25 0 1 0 1855325643 82325504 18860 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 20099 18860 145 145 0 19954 0 [pid=3383] vsize: 80396 Current children cumulated CPU time (s) 169.13 Current children cumulated vsize (Kb) 82520 [startup+180.019 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 19635 0 0 0 17829 81 0 0 25 0 1 0 1855325643 82571264 18922 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 20159 18922 145 145 0 20014 0 [pid=3383] vsize: 80636 Current children cumulated CPU time (s) 179.11 Current children cumulated vsize (Kb) 82760 [startup+190.021 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 19673 0 0 0 18829 81 0 0 25 0 1 0 1855325643 82718720 18960 4294967295 134512640 135094434 3221224432 3221223092 134553506 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 20195 18960 145 145 0 20050 0 [pid=3383] vsize: 80780 Current children cumulated CPU time (s) 189.11 Current children cumulated vsize (Kb) 82904 [startup+200.021 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 19709 0 0 0 19828 81 0 0 25 0 1 0 1855325643 82862080 18996 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 20230 18996 145 145 0 20085 0 [pid=3383] vsize: 80920 Current children cumulated CPU time (s) 199.1 Current children cumulated vsize (Kb) 83044 [startup+210.022 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 19816 0 0 0 20825 82 0 0 25 0 1 0 1855325643 83283968 19103 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 20333 19103 145 145 0 20188 0 [pid=3383] vsize: 81332 Current children cumulated CPU time (s) 209.08 Current children cumulated vsize (Kb) 83456 [startup+220.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 19861 0 0 0 21825 83 0 0 25 0 1 0 1855325643 83464192 19148 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 20377 19148 145 145 0 20232 0 [pid=3383] vsize: 81508 Current children cumulated CPU time (s) 219.09 Current children cumulated vsize (Kb) 83632 [startup+230.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 19955 0 0 0 22823 83 0 0 25 0 1 0 1855325643 83972096 19242 4294967295 134512640 135094434 3221224432 3221223056 134557598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 20501 19242 145 145 0 20356 0 [pid=3383] vsize: 82004 Current children cumulated CPU time (s) 229.07 Current children cumulated vsize (Kb) 84128 [startup+240.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 20009 0 0 0 23823 83 0 0 25 0 1 0 1855325643 84180992 19296 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 20552 19296 145 145 0 20407 0 [pid=3383] vsize: 82208 Current children cumulated CPU time (s) 239.07 Current children cumulated vsize (Kb) 84332 [startup+250.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 20060 0 0 0 24822 84 0 0 25 0 1 0 1855325643 84385792 19347 4294967295 134512640 135094434 3221224432 3221223088 134557804 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 20602 19347 145 145 0 20457 0 [pid=3383] vsize: 82408 Current children cumulated CPU time (s) 249.07 Current children cumulated vsize (Kb) 84532 [startup+260.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 20115 0 0 0 25821 84 0 0 25 0 1 0 1855325643 84602880 19402 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 20655 19402 145 145 0 20510 0 [pid=3383] vsize: 82620 Current children cumulated CPU time (s) 259.06 Current children cumulated vsize (Kb) 84744 [startup+270.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 20166 0 0 0 26820 85 0 0 25 0 1 0 1855325643 84807680 19453 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 20705 19453 145 145 0 20560 0 [pid=3383] vsize: 82820 Current children cumulated CPU time (s) 269.06 Current children cumulated vsize (Kb) 84944 [startup+280.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 20214 0 0 0 27819 85 0 0 25 0 1 0 1855325643 84996096 19501 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 20751 19501 145 145 0 20606 0 [pid=3383] vsize: 83004 Current children cumulated CPU time (s) 279.05 Current children cumulated vsize (Kb) 85128 [startup+290.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 20414 0 0 0 28816 86 0 0 25 0 1 0 1855325643 85798912 19701 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 20947 19701 145 145 0 20802 0 [pid=3383] vsize: 83788 Current children cumulated CPU time (s) 289.03 Current children cumulated vsize (Kb) 85912 [startup+300.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 20611 0 0 0 29813 88 0 0 25 0 1 0 1855325643 86589440 19898 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 21140 19898 145 145 0 20995 0 [pid=3383] vsize: 84560 Current children cumulated CPU time (s) 299.02 Current children cumulated vsize (Kb) 86684 [startup+310.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 20784 0 0 0 30810 89 0 0 25 0 1 0 1855325643 87285760 20071 4294967295 134512640 135094434 3221224432 3221223056 134557633 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 21310 20071 145 145 0 21165 0 [pid=3383] vsize: 85240 Current children cumulated CPU time (s) 309 Current children cumulated vsize (Kb) 87364 [startup+320.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 20844 0 0 0 31809 90 0 0 25 0 1 0 1855325643 87523328 20131 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 21368 20131 145 145 0 21223 0 [pid=3383] vsize: 85472 Current children cumulated CPU time (s) 319 Current children cumulated vsize (Kb) 87596 [startup+330.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 20902 0 0 0 32808 91 0 0 25 0 1 0 1855325643 87752704 20189 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 21424 20189 145 145 0 21279 0 [pid=3383] vsize: 85696 Current children cumulated CPU time (s) 329 Current children cumulated vsize (Kb) 87820 [startup+340.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 21089 0 0 0 33805 92 0 0 25 0 1 0 1855325643 88506368 20376 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 21608 20376 145 145 0 21463 0 [pid=3383] vsize: 86432 Current children cumulated CPU time (s) 338.98 Current children cumulated vsize (Kb) 88556 [startup+350.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 22222 0 0 0 34786 100 0 0 22 0 1 0 1855325643 93380608 21509 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3383/statm): 22798 21509 145 145 0 22653 0 [pid=3383] vsize: 91192 Current children cumulated CPU time (s) 348.87 Current children cumulated vsize (Kb) 93316 [startup+360.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 23106 0 0 0 35769 105 0 0 25 0 1 0 1855325643 96993280 22393 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3383/statm): 23680 22393 145 145 0 23535 0 [pid=3383] vsize: 94720 Current children cumulated CPU time (s) 358.75 Current children cumulated vsize (Kb) 96844 [startup+370.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 23905 0 0 0 36755 111 0 0 25 0 1 0 1855325643 100253696 23192 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3383/statm): 24476 23192 145 145 0 24331 0 [pid=3383] vsize: 97904 Current children cumulated CPU time (s) 368.67 Current children cumulated vsize (Kb) 100028 [startup+380.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 24402 0 0 0 37748 114 0 0 25 0 1 0 1855325643 102273024 23689 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3383/statm): 24969 23689 145 145 0 24824 0 [pid=3383] vsize: 99876 Current children cumulated CPU time (s) 378.63 Current children cumulated vsize (Kb) 102000 [startup+390.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 24636 0 0 0 38744 117 0 0 25 0 1 0 1855325643 103223296 23923 4294967295 134512640 135094434 3221224432 3221223072 134558043 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3383/statm): 25201 23923 145 145 0 25056 0 [pid=3383] vsize: 100804 Current children cumulated CPU time (s) 388.62 Current children cumulated vsize (Kb) 102928 [startup+400.037 s] Raw data (loadavg): 1.07 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 24840 0 0 0 39740 119 0 0 25 0 1 0 1855325643 104050688 24127 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3383/statm): 25403 24127 145 145 0 25258 0 [pid=3383] vsize: 101612 Current children cumulated CPU time (s) 398.6 Current children cumulated vsize (Kb) 103736 [startup+410.038 s] Raw data (loadavg): 1.06 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 24943 0 0 0 40738 120 0 0 25 0 1 0 1855325643 104468480 24230 4294967295 134512640 135094434 3221224432 3221223120 134554705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3383/statm): 25505 24230 145 145 0 25360 0 [pid=3383] vsize: 102020 Current children cumulated CPU time (s) 408.59 Current children cumulated vsize (Kb) 104144 [startup+420.039 s] Raw data (loadavg): 1.05 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 25151 0 0 0 41733 123 0 0 25 0 1 0 1855325643 105304064 24438 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3383/statm): 25709 24438 145 145 0 25564 0 [pid=3383] vsize: 102836 Current children cumulated CPU time (s) 418.57 Current children cumulated vsize (Kb) 104960 [startup+430.04 s] Raw data (loadavg): 1.04 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 25388 0 0 0 42727 126 0 0 25 0 1 0 1855325643 106258432 24675 4294967295 134512640 135094434 3221224432 3221223072 134562078 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3383/statm): 25942 24675 145 145 0 25797 0 [pid=3383] vsize: 103768 Current children cumulated CPU time (s) 428.54 Current children cumulated vsize (Kb) 105892 [startup+440.04 s] Raw data (loadavg): 1.04 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 25756 0 0 0 43721 130 0 0 25 0 1 0 1855325643 107745280 25043 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3383/statm): 26305 25043 145 145 0 26160 0 [pid=3383] vsize: 105220 Current children cumulated CPU time (s) 438.52 Current children cumulated vsize (Kb) 107344 [startup+450.041 s] Raw data (loadavg): 1.03 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 25913 0 0 0 44718 131 0 0 25 0 1 0 1855325643 108384256 25200 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 26461 25200 145 145 0 26316 0 [pid=3383] vsize: 105844 Current children cumulated CPU time (s) 448.5 Current children cumulated vsize (Kb) 107968 [startup+460.043 s] Raw data (loadavg): 1.03 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 26497 0 0 0 45709 135 0 0 25 0 1 0 1855325643 110747648 25784 4294967295 134512640 135094434 3221224432 3221223088 134557917 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 27038 25784 145 145 0 26893 0 [pid=3383] vsize: 108152 Current children cumulated CPU time (s) 458.45 Current children cumulated vsize (Kb) 110276 [startup+470.044 s] Raw data (loadavg): 1.02 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 27259 0 0 0 46696 140 0 0 25 0 1 0 1855325643 113848320 26546 4294967295 134512640 135094434 3221224432 3221223080 134556677 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 27795 26546 145 145 0 27650 0 [pid=3383] vsize: 111180 Current children cumulated CPU time (s) 468.37 Current children cumulated vsize (Kb) 113304 [startup+480.044 s] Raw data (loadavg): 1.02 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 27965 0 0 0 47684 145 0 0 25 0 1 0 1855325643 116723712 27252 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 28497 27252 145 145 0 28352 0 [pid=3383] vsize: 113988 Current children cumulated CPU time (s) 478.3 Current children cumulated vsize (Kb) 116112 [startup+490.045 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 28244 0 0 0 48677 147 0 0 25 0 1 0 1855325643 117862400 27531 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 28775 27531 145 145 0 28630 0 [pid=3383] vsize: 115100 Current children cumulated CPU time (s) 488.25 Current children cumulated vsize (Kb) 117224 [startup+500.046 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 28857 0 0 0 49668 151 0 0 25 0 1 0 1855325643 120340480 28144 4294967295 134512640 135094434 3221224432 3221223088 134557925 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 29380 28144 145 145 0 29235 0 [pid=3383] vsize: 117520 Current children cumulated CPU time (s) 498.2 Current children cumulated vsize (Kb) 119644 [startup+510.047 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 29451 0 0 0 50658 155 0 0 25 0 1 0 1855325643 123273216 28738 4294967295 134512640 135094434 3221224432 3221223100 134555968 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 30096 28738 145 145 0 29951 0 [pid=3383] vsize: 120384 Current children cumulated CPU time (s) 508.14 Current children cumulated vsize (Kb) 122508 [startup+520.048 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 30177 0 0 0 51646 159 0 0 25 0 1 0 1855325643 126226432 29464 4294967295 134512640 135094434 3221224432 3221223056 134557711 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 30817 29464 145 145 0 30672 0 [pid=3383] vsize: 123268 Current children cumulated CPU time (s) 518.06 Current children cumulated vsize (Kb) 125392 [startup+530.049 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 30859 0 0 0 52634 163 0 0 25 0 1 0 1855325643 129003520 30146 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 31495 30146 145 145 0 31350 0 [pid=3383] vsize: 125980 Current children cumulated CPU time (s) 527.98 Current children cumulated vsize (Kb) 128104 [startup+540.049 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 31488 0 0 0 53624 167 0 0 25 0 1 0 1855325643 131571712 30775 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3383/statm): 32122 30775 145 145 0 31977 0 [pid=3383] vsize: 128488 Current children cumulated CPU time (s) 537.92 Current children cumulated vsize (Kb) 130612 [startup+550.05 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 32082 0 0 0 54613 172 0 0 25 0 1 0 1855325643 134004736 31369 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 32716 31369 145 145 0 32571 0 [pid=3383] vsize: 130864 Current children cumulated CPU time (s) 547.86 Current children cumulated vsize (Kb) 132988 [startup+560.052 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 32649 0 0 0 55603 177 0 0 25 0 1 0 1855325643 136323072 31936 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 33282 31936 145 145 0 33137 0 [pid=3383] vsize: 133128 Current children cumulated CPU time (s) 557.81 Current children cumulated vsize (Kb) 135252 [startup+570.053 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 33191 0 0 0 56594 180 0 0 25 0 1 0 1855325643 138543104 32478 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 33824 32478 145 145 0 33679 0 [pid=3383] vsize: 135296 Current children cumulated CPU time (s) 567.75 Current children cumulated vsize (Kb) 137420 [startup+580.054 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 33580 0 0 0 57586 184 0 0 25 0 1 0 1855325643 140140544 32867 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 34214 32867 145 145 0 34069 0 [pid=3383] vsize: 136856 Current children cumulated CPU time (s) 577.71 Current children cumulated vsize (Kb) 138980 [startup+590.054 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 33665 0 0 0 58584 185 0 0 25 0 1 0 1855325643 140484608 32952 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 34298 32952 145 145 0 34153 0 [pid=3383] vsize: 137192 Current children cumulated CPU time (s) 587.7 Current children cumulated vsize (Kb) 139316 [startup+600.055 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 33769 0 0 0 59583 186 0 0 25 0 1 0 1855325643 140910592 33056 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 34402 33056 145 145 0 34257 0 [pid=3383] vsize: 137608 Current children cumulated CPU time (s) 597.7 Current children cumulated vsize (Kb) 139732 [startup+610.057 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 33832 0 0 0 60582 186 0 0 25 0 1 0 1855325643 141160448 33119 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 34463 33119 145 145 0 34318 0 [pid=3383] vsize: 137852 Current children cumulated CPU time (s) 607.69 Current children cumulated vsize (Kb) 139976 [startup+620.058 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 34080 0 0 0 61578 188 0 0 25 0 1 0 1855325643 142159872 33367 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3383/statm): 34707 33367 145 145 0 34562 0 [pid=3383] vsize: 138828 Current children cumulated CPU time (s) 617.67 Current children cumulated vsize (Kb) 140952 [startup+630.058 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 34532 0 0 0 62569 192 0 0 25 0 1 0 1855325643 143998976 33819 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 35156 33819 145 145 0 35011 0 [pid=3383] vsize: 140624 Current children cumulated CPU time (s) 627.62 Current children cumulated vsize (Kb) 142748 [startup+640.06 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 34658 0 0 0 63567 193 0 0 25 0 1 0 1855325643 144502784 33945 4294967295 134512640 135094434 3221224432 3221223092 134553528 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 35279 33945 145 145 0 35134 0 [pid=3383] vsize: 141116 Current children cumulated CPU time (s) 637.61 Current children cumulated vsize (Kb) 143240 [startup+650.061 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 34718 0 0 0 64566 193 0 0 25 0 1 0 1855325643 144744448 34005 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 35338 34005 145 145 0 35193 0 [pid=3383] vsize: 141352 Current children cumulated CPU time (s) 647.6 Current children cumulated vsize (Kb) 143476 [startup+660.062 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 34929 0 0 0 65563 194 0 0 25 0 1 0 1855325643 145592320 34216 4294967295 134512640 135094434 3221224432 3221223024 134551971 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 35545 34216 145 145 0 35400 0 [pid=3383] vsize: 142180 Current children cumulated CPU time (s) 657.58 Current children cumulated vsize (Kb) 144304 [startup+670.064 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 34999 0 0 0 66562 195 0 0 25 0 1 0 1855325643 145874944 34286 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 35614 34286 145 145 0 35469 0 [pid=3383] vsize: 142456 Current children cumulated CPU time (s) 667.58 Current children cumulated vsize (Kb) 144580 [startup+680.063 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 35114 0 0 0 67560 196 0 0 25 0 1 0 1855325643 146341888 34401 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 35728 34401 145 145 0 35583 0 [pid=3383] vsize: 142912 Current children cumulated CPU time (s) 677.57 Current children cumulated vsize (Kb) 145036 [startup+690.064 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 35285 0 0 0 68557 197 0 0 25 0 1 0 1855325643 147030016 34572 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 35896 34572 145 145 0 35751 0 [pid=3383] vsize: 143584 Current children cumulated CPU time (s) 687.55 Current children cumulated vsize (Kb) 145708 [startup+700.065 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 35625 0 0 0 69551 200 0 0 25 0 1 0 1855325643 148410368 34912 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 36233 34912 145 145 0 36088 0 [pid=3383] vsize: 144932 Current children cumulated CPU time (s) 697.52 Current children cumulated vsize (Kb) 147056 [startup+710.065 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 35990 0 0 0 70544 202 0 0 25 0 1 0 1855325643 149897216 35277 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 36596 35277 145 145 0 36451 0 [pid=3383] vsize: 146384 Current children cumulated CPU time (s) 707.47 Current children cumulated vsize (Kb) 148508 [startup+720.066 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 36365 0 0 0 71538 204 0 0 25 0 1 0 1855325643 151420928 35652 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 36968 35652 145 145 0 36823 0 [pid=3383] vsize: 147872 Current children cumulated CPU time (s) 717.43 Current children cumulated vsize (Kb) 149996 [startup+730.066 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 36502 0 0 0 72536 205 0 0 25 0 1 0 1855325643 151973888 35789 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 37103 35789 145 145 0 36958 0 [pid=3383] vsize: 148412 Current children cumulated CPU time (s) 727.42 Current children cumulated vsize (Kb) 150536 [startup+740.067 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 36544 0 0 0 73535 206 0 0 25 0 1 0 1855325643 152141824 35831 4294967295 134512640 135094434 3221224432 3221223092 134553494 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 37144 35831 145 145 0 36999 0 [pid=3383] vsize: 148576 Current children cumulated CPU time (s) 737.42 Current children cumulated vsize (Kb) 150700 [startup+750.068 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 36544 0 0 0 74535 206 0 0 25 0 1 0 1855325643 152141824 35831 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 37144 35831 145 145 0 36999 0 [pid=3383] vsize: 148576 Current children cumulated CPU time (s) 747.42 Current children cumulated vsize (Kb) 150700 [startup+760.069 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 36699 0 0 0 75533 207 0 0 25 0 1 0 1855325643 152768512 35986 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 37297 35986 145 145 0 37152 0 [pid=3383] vsize: 149188 Current children cumulated CPU time (s) 757.41 Current children cumulated vsize (Kb) 151312 [startup+770.07 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 37091 0 0 0 76526 210 0 0 25 0 1 0 1855325643 154361856 36378 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 37686 36378 145 145 0 37541 0 [pid=3383] vsize: 150744 Current children cumulated CPU time (s) 767.37 Current children cumulated vsize (Kb) 152868 [startup+780.069 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 37476 0 0 0 77519 212 0 0 25 0 1 0 1855325643 155930624 36763 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 38069 36763 145 145 0 37924 0 [pid=3383] vsize: 152276 Current children cumulated CPU time (s) 777.32 Current children cumulated vsize (Kb) 154400 [startup+790.071 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 37856 0 0 0 78513 214 0 0 25 0 1 0 1855325643 157478912 37143 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 38447 37143 145 145 0 38302 0 [pid=3383] vsize: 153788 Current children cumulated CPU time (s) 787.28 Current children cumulated vsize (Kb) 155912 [startup+800.072 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 38239 0 0 0 79508 217 0 0 25 0 1 0 1855325643 159035392 37526 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 38827 37526 145 145 0 38682 0 [pid=3383] vsize: 155308 Current children cumulated CPU time (s) 797.26 Current children cumulated vsize (Kb) 157432 [startup+810.072 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 38624 0 0 0 80501 220 0 0 25 0 1 0 1855325643 160595968 37911 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 39208 37911 145 145 0 39063 0 [pid=3383] vsize: 156832 Current children cumulated CPU time (s) 807.22 Current children cumulated vsize (Kb) 158956 [startup+820.073 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 38750 0 0 0 81499 221 0 0 25 0 1 0 1855325643 161112064 38037 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 39334 38037 145 145 0 39189 0 [pid=3383] vsize: 157336 Current children cumulated CPU time (s) 817.21 Current children cumulated vsize (Kb) 159460 [startup+830.073 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3383 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 38852 0 0 0 82497 222 0 0 25 0 1 0 1855325643 161517568 38139 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 39433 38139 145 145 0 39288 0 [pid=3383] vsize: 157732 Current children cumulated CPU time (s) 827.2 Current children cumulated vsize (Kb) 159856 [startup+840.074 s] Raw data (loadavg): 1.15 1.02 0.93 2/57 3434 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 38996 0 0 0 83486 231 0 0 18 0 1 0 1855325643 162103296 38283 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3383/statm): 39576 38283 145 145 0 39431 0 [pid=3383] vsize: 158304 Current children cumulated CPU time (s) 837.18 Current children cumulated vsize (Kb) 160428 [startup+850.075 s] Raw data (loadavg): 1.13 1.02 0.93 2/57 3434 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 39533 0 0 0 84475 236 0 0 25 0 1 0 1855325643 164286464 38820 4294967295 134512640 135094434 3221224432 3221223024 134557002 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 40109 38820 145 145 0 39964 0 [pid=3383] vsize: 160436 Current children cumulated CPU time (s) 847.12 Current children cumulated vsize (Kb) 162560 [startup+860.076 s] Raw data (loadavg): 1.11 1.02 0.93 2/57 3434 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 40048 0 0 0 85465 240 0 0 25 0 1 0 1855325643 166383616 39335 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 40621 39335 145 145 0 40476 0 [pid=3383] vsize: 162484 Current children cumulated CPU time (s) 857.06 Current children cumulated vsize (Kb) 164608 [startup+870.077 s] Raw data (loadavg): 1.09 1.02 0.93 2/57 3434 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 40563 0 0 0 86456 244 0 0 25 0 1 0 1855325643 168497152 39850 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 41137 39850 145 145 0 40992 0 [pid=3383] vsize: 164548 Current children cumulated CPU time (s) 867.01 Current children cumulated vsize (Kb) 166672 [startup+880.077 s] Raw data (loadavg): 1.08 1.02 0.93 2/57 3434 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 41052 0 0 0 87448 247 0 0 25 0 1 0 1855325643 170479616 40339 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 41621 40339 145 145 0 41476 0 [pid=3383] vsize: 166484 Current children cumulated CPU time (s) 876.96 Current children cumulated vsize (Kb) 168608 [startup+890.078 s] Raw data (loadavg): 1.06 1.02 0.93 2/57 3434 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 41526 0 0 0 88438 252 0 0 25 0 1 0 1855325643 172417024 40813 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 42094 40813 145 145 0 41949 0 [pid=3383] vsize: 168376 Current children cumulated CPU time (s) 886.91 Current children cumulated vsize (Kb) 170500 [startup+900.079 s] Raw data (loadavg): 1.05 1.01 0.93 2/57 3434 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 41986 0 0 0 89429 256 0 0 25 0 1 0 1855325643 174288896 41273 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 42551 41273 145 145 0 42406 0 [pid=3383] vsize: 170204 Current children cumulated CPU time (s) 896.86 Current children cumulated vsize (Kb) 172328 [startup+910.08 s] Raw data (loadavg): 1.05 1.01 0.93 1/57 3434 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) T 3379 3379 5245 0 -1 0 42440 0 0 0 90422 260 0 0 25 0 1 0 1855325643 176144384 41727 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/3383/statm): 43004 41727 145 145 0 42859 0 [pid=3383] vsize: 172016 Current children cumulated CPU time (s) 906.83 Current children cumulated vsize (Kb) 174140 [startup+920.081 s] Raw data (loadavg): 1.04 1.01 0.93 2/57 3438 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 42890 0 0 0 91413 264 0 0 25 0 1 0 1855325643 177987584 42177 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 43454 42177 145 145 0 43309 0 [pid=3383] vsize: 173816 Current children cumulated CPU time (s) 916.78 Current children cumulated vsize (Kb) 175940 [startup+930.081 s] Raw data (loadavg): 1.03 1.01 0.93 2/57 3438 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 43276 0 0 0 92409 267 0 0 25 0 1 0 1855325643 179585024 42563 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 43844 42563 145 145 0 43699 0 [pid=3383] vsize: 175376 Current children cumulated CPU time (s) 926.77 Current children cumulated vsize (Kb) 177500 [startup+940.084 s] Raw data (loadavg): 1.03 1.01 0.93 2/57 3438 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 43684 0 0 0 93400 270 0 0 25 0 1 0 1855325643 181231616 42971 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 44246 42971 145 145 0 44101 0 [pid=3383] vsize: 176984 Current children cumulated CPU time (s) 936.71 Current children cumulated vsize (Kb) 179108 [startup+950.085 s] Raw data (loadavg): 1.02 1.01 0.93 2/57 3438 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 44049 0 0 0 94394 273 0 0 25 0 1 0 1855325643 182788096 43336 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 44626 43336 145 145 0 44481 0 [pid=3383] vsize: 178504 Current children cumulated CPU time (s) 946.68 Current children cumulated vsize (Kb) 180628 [startup+960.086 s] Raw data (loadavg): 1.02 1.01 0.93 2/57 3438 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 44399 0 0 0 95387 276 0 0 25 0 1 0 1855325643 184242176 43686 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 44981 43686 145 145 0 44836 0 [pid=3383] vsize: 179924 Current children cumulated CPU time (s) 956.64 Current children cumulated vsize (Kb) 182048 [startup+970.087 s] Raw data (loadavg): 1.02 1.01 0.93 2/57 3438 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 44752 0 0 0 96382 279 0 0 25 0 1 0 1855325643 185663488 44039 4294967295 134512640 135094434 3221224432 3221223024 134557157 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 45328 44039 145 145 0 45183 0 [pid=3383] vsize: 181312 Current children cumulated CPU time (s) 966.62 Current children cumulated vsize (Kb) 183436 [startup+980.087 s] Raw data (loadavg): 1.01 1.01 0.93 2/57 3438 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 45071 0 0 0 97376 282 0 0 25 0 1 0 1855325643 186966016 44358 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 45646 44358 145 145 0 45501 0 [pid=3383] vsize: 182584 Current children cumulated CPU time (s) 976.59 Current children cumulated vsize (Kb) 184708 [startup+990.088 s] Raw data (loadavg): 1.01 1.01 0.93 2/57 3438 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 45393 0 0 0 98370 284 0 0 25 0 1 0 1855325643 188272640 44680 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 45965 44680 145 145 0 45820 0 [pid=3383] vsize: 183860 Current children cumulated CPU time (s) 986.55 Current children cumulated vsize (Kb) 185984 [startup+1000.09 s] Raw data (loadavg): 1.08 1.02 0.93 2/57 3438 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 45730 0 0 0 99362 288 0 0 25 0 1 0 1855325643 189632512 45017 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 46297 45017 145 145 0 46152 0 [pid=3383] vsize: 185188 Current children cumulated CPU time (s) 996.51 Current children cumulated vsize (Kb) 187312 [startup+1010.09 s] Raw data (loadavg): 1.07 1.02 0.93 2/57 3438 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 46065 0 0 0 100356 290 0 0 25 0 1 0 1855325643 191021056 45352 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 46636 45352 145 145 0 46491 0 [pid=3383] vsize: 186544 Current children cumulated CPU time (s) 1006.47 Current children cumulated vsize (Kb) 188668 [startup+1020.09 s] Raw data (loadavg): 1.06 1.02 0.93 2/57 3438 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 46380 0 0 0 101351 292 0 0 25 0 1 0 1855325643 193376256 45667 4294967295 134512640 135094434 3221224432 3221223088 134558029 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 47211 45667 145 145 0 47066 0 [pid=3383] vsize: 188844 Current children cumulated CPU time (s) 1016.44 Current children cumulated vsize (Kb) 190968 [startup+1030.09 s] Raw data (loadavg): 1.05 1.02 0.93 2/57 3438 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 46688 0 0 0 102345 295 0 0 25 0 1 0 1855325643 194666496 45975 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 47526 45975 145 145 0 47381 0 [pid=3383] vsize: 190104 Current children cumulated CPU time (s) 1026.41 Current children cumulated vsize (Kb) 192228 [startup+1040.09 s] Raw data (loadavg): 1.04 1.02 0.93 2/57 3438 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 47019 0 0 0 103341 297 0 0 25 0 1 0 1855325643 196009984 46306 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 47854 46306 145 145 0 47709 0 [pid=3383] vsize: 191416 Current children cumulated CPU time (s) 1036.39 Current children cumulated vsize (Kb) 193540 [startup+1050.09 s] Raw data (loadavg): 1.03 1.02 0.93 2/57 3438 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 47310 0 0 0 104336 299 0 0 18 0 1 0 1855325643 197189632 46597 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3383/statm): 48142 46597 145 145 0 47997 0 [pid=3383] vsize: 192568 Current children cumulated CPU time (s) 1046.36 Current children cumulated vsize (Kb) 194692 [startup+1060.09 s] Raw data (loadavg): 1.03 1.02 0.93 2/57 3438 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 47640 0 0 0 105331 301 0 0 25 0 1 0 1855325643 198619136 46927 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 48491 46927 145 145 0 48346 0 [pid=3383] vsize: 193964 Current children cumulated CPU time (s) 1056.33 Current children cumulated vsize (Kb) 196088 [startup+1070.1 s] Raw data (loadavg): 1.02 1.01 0.93 2/57 3438 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 47892 0 0 0 106327 303 0 0 25 0 1 0 1855325643 199630848 47179 4294967295 134512640 135094434 3221224432 3221223088 134558174 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 48738 47179 145 145 0 48593 0 [pid=3383] vsize: 194952 Current children cumulated CPU time (s) 1066.31 Current children cumulated vsize (Kb) 197076 [startup+1080.1 s] Raw data (loadavg): 1.02 1.01 0.93 2/57 3438 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 48172 0 0 0 107322 305 0 0 25 0 1 0 1855325643 200765440 47459 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 49015 47459 145 145 0 48870 0 [pid=3383] vsize: 196060 Current children cumulated CPU time (s) 1076.28 Current children cumulated vsize (Kb) 198184 [startup+1090.1 s] Raw data (loadavg): 1.02 1.01 0.93 2/57 3438 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 48433 0 0 0 108319 306 0 0 25 0 1 0 1855325643 201842688 47720 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 49278 47720 145 145 0 49133 0 [pid=3383] vsize: 197112 Current children cumulated CPU time (s) 1086.26 Current children cumulated vsize (Kb) 199236 [startup+1100.1 s] Raw data (loadavg): 1.01 1.01 0.93 2/57 3438 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 48694 0 0 0 109314 308 0 0 25 0 1 0 1855325643 202895360 47981 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 49535 47981 145 145 0 49390 0 [pid=3383] vsize: 198140 Current children cumulated CPU time (s) 1096.23 Current children cumulated vsize (Kb) 200264 [startup+1110.1 s] Raw data (loadavg): 1.01 1.01 0.93 2/57 3438 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 48967 0 0 0 110309 310 0 0 25 0 1 0 1855325643 204005376 48254 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 49806 48254 145 145 0 49661 0 [pid=3383] vsize: 199224 Current children cumulated CPU time (s) 1106.2 Current children cumulated vsize (Kb) 201348 [startup+1120.1 s] Raw data (loadavg): 1.01 1.01 0.93 2/57 3438 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 49219 0 0 0 111304 312 0 0 25 0 1 0 1855325643 205029376 48506 4294967295 134512640 135094434 3221224432 3221223024 134557310 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 50056 48506 145 145 0 49911 0 [pid=3383] vsize: 200224 Current children cumulated CPU time (s) 1116.17 Current children cumulated vsize (Kb) 202348 [startup+1130.1 s] Raw data (loadavg): 1.01 1.01 0.93 2/57 3438 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 49560 0 0 0 112300 314 0 0 25 0 1 0 1855325643 206434304 48847 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 50399 48847 145 145 0 50254 0 [pid=3383] vsize: 201596 Current children cumulated CPU time (s) 1126.15 Current children cumulated vsize (Kb) 203720 [startup+1140.1 s] Raw data (loadavg): 1.00 1.01 0.93 2/57 3438 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 49896 0 0 0 113296 315 0 0 25 0 1 0 1855325643 207777792 49183 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 50727 49183 145 145 0 50582 0 [pid=3383] vsize: 202908 Current children cumulated CPU time (s) 1136.12 Current children cumulated vsize (Kb) 205032 [startup+1150.1 s] Raw data (loadavg): 1.00 1.01 0.93 2/57 3438 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 50228 0 0 0 114291 318 0 0 25 0 1 0 1855325643 209149952 49515 4294967295 134512640 135094434 3221224432 3221223024 134557310 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 51062 49515 145 145 0 50917 0 [pid=3383] vsize: 204248 Current children cumulated CPU time (s) 1146.1 Current children cumulated vsize (Kb) 206372 [startup+1160.1 s] Raw data (loadavg): 1.00 1.01 0.93 2/57 3438 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 50562 0 0 0 115286 320 0 0 25 0 1 0 1855325643 210628608 49849 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 51423 49849 145 145 0 51278 0 [pid=3383] vsize: 205692 Current children cumulated CPU time (s) 1156.07 Current children cumulated vsize (Kb) 207816 [startup+1170.11 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 3440 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 50889 0 0 0 116281 322 0 0 25 0 1 0 1855325643 211959808 50176 4294967295 134512640 135094434 3221224432 3221223080 134562037 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3383/statm): 51748 50176 145 145 0 51603 0 [pid=3383] vsize: 206992 Current children cumulated CPU time (s) 1166.04 Current children cumulated vsize (Kb) 209116 [startup+1180.11 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 3440 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 51208 0 0 0 117276 325 0 0 25 0 1 0 1855325643 213237760 50495 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 52060 50495 145 145 0 51915 0 [pid=3383] vsize: 208240 Current children cumulated CPU time (s) 1176.02 Current children cumulated vsize (Kb) 210364 [startup+1190.11 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 3440 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 51491 0 0 0 118271 328 0 0 25 0 1 0 1855325643 214401024 50778 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 52344 50778 145 145 0 52199 0 [pid=3383] vsize: 209376 Current children cumulated CPU time (s) 1186 Current children cumulated vsize (Kb) 211500 [startup+1200.11 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 3440 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 51797 0 0 0 119265 330 0 0 25 0 1 0 1855325643 215609344 51084 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3383/statm): 52639 51084 145 145 0 52494 0 [pid=3383] vsize: 210556 Current children cumulated CPU time (s) 1195.96 Current children cumulated vsize (Kb) 212680 [startup+1210.11 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 3440 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 51991 0 0 0 120262 332 0 0 25 0 1 0 1855325643 216420352 51278 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3383/statm): 52837 51278 145 145 0 52692 0 [pid=3383] vsize: 211348 Current children cumulated CPU time (s) 1205.95 Current children cumulated vsize (Kb) 213472 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.11 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 3440 Raw data (/proc/3379/stat): 3379 (minisat+_script) S 3378 3379 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855325638 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3379/statm): 531 226 485 147 0 384 0 [pid=3379] vsize: 2124 Raw data (/proc/3383/stat): 3383 (minisat+_64-bit) R 3379 3379 5245 0 -1 0 51991 0 0 0 120262 332 0 0 25 0 1 0 1855325643 216420352 51278 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3383/statm): 52837 51278 145 145 0 52692 0 [pid=3383] vsize: 211348 Current children cumulated CPU time (s) 1205.95 Current children cumulated vsize (Kb) 213472 Sending SIGTERM to -3379 Sleeping 2 seconds One traced child (pid=3379) ended because it received signal 15 (SIGTERM) One traced child (pid=3383) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.21 CPU time (s): 1206.05 CPU user time (s): 1202.63 CPU system time (s): 3.41648 CPU usage (%): 99.6557 Max. virtual memory (cumulated for all children) (Kb): 213472
ERROR: no interpretation found !