Name | mps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-sp98ic.opb |
MD5SUM | b6b40b25db69f63dc02649b5c9a3693a |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 7728531381 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 10894 |
Biggest coefficient in the objective function | 1079902210 |
Number of bits for the biggest coefficient in the objective function | 31 |
Sum of the numbers in the objective function | 3040671454286 |
Number of bits of the sum of numbers in the objective function | 42 |
Biggest number in a constraint | 1079902210 |
Number of bits of the biggest number in a constraint | 31 |
Biggest sum of numbers in a constraint | 3040671454286 |
Number of bits of the biggest sum of numbers | 42 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1238.61 |
Number of variables | 10894 |
Total number of constraints | 11719 |
Number of constraints which are clauses | 20 |
Number of constraints which are cardinality constraints (but not clauses) | 11518 |
Number of constraints which are nor clauses,nor cardinality constraints | 181 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 5038 |
LAUNCH ON wulflinc22 THE 2005-09-20 02:14:53 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3117 boxname=wulflinc22 idbench=773 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: b6b40b25db69f63dc02649b5c9a3693a /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-sp98ic.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-sp98ic.opb IDLAUNCH: 3117 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.031 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 : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.031 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 902824 kB Buffers: 136 kB Cached: 104376 kB SwapCached: 480 kB Active: 19856 kB Inactive: 87080 kB HighTotal: 131008 kB HighFree: 23016 kB LowTotal: 903652 kB LowFree: 879808 kB SwapTotal: 2097892 kB SwapFree: 2096748 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5668 kB Slab: 19084 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 02:35:03 (client local time) WITH STATUS 0 IN 1207.9 SECONDS stats: 3117 7 1207.9 0
c Parsing PB file... c Converting 825 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ssssss.ssssssss.ss.s..sssss..sssssssssssssssssssssssssssssssssss.sssss.s..sssssssssssssssssssssssssssss.ssssssss.sssss..s.s.s.sssssssssssssssssss.ssss.sssssssssssssssssssss c ---[ 976]---> BDD-cost: 3578 c ---[ 970]---> Adder-cost: 2336 maxlim: 26 bits: 6/5 c ---[ 953]---> BDD-cost: 4629 c ---[ 942]---> Adder-cost: 5853 maxlim: 28 bits: 6/5 c ---[ 931]---> BDD-cost: 1386 c ---[ 912]---> BDD-cost: 1551 c ---[ 910]---> Adder-cost: 1275 maxlim: 21 bits: 6/5 c ---[ 872]---> BDD-cost:10452 c ---[ 866]---> BDD-cost: 21 c ---[ 865]---> BDD-cost: 1846 c ---[ 863]---> BDD-cost: 45 c ---[ 862]---> BDD-cost: 35 c ---[ 861]---> BDD-cost: 39 c ---[ 860]---> BDD-cost: 35 c ---[ 859]---> BDD-cost: 39 c ---[ 858]---> BDD-cost: 35 c ---[ 857]---> BDD-cost: 39 c ---[ 856]---> BDD-cost: 39 c ---[ 855]---> BDD-cost: 35 c ---[ 854]---> BDD-cost: 35 c ---[ 852]---> BDD-cost: 39 c ---[ 851]---> BDD-cost: 45 c ---[ 850]---> BDD-cost: 45 c ---[ 849]---> BDD-cost: 35 c ---[ 848]---> BDD-cost: 35 c ---[ 847]---> BDD-cost: 35 c ---[ 846]---> BDD-cost: 39 c ---[ 845]---> BDD-cost: 35 c ---[ 844]---> BDD-cost: 39 c ---[ 843]---> BDD-cost: 45 c ---[ 841]---> BDD-cost: 21 c ---[ 840]---> BDD-cost: 35 c ---[ 839]---> BDD-cost: 35 c ---[ 838]---> BDD-cost: 35 c ---[ 837]---> BDD-cost: 39 c ---[ 836]---> BDD-cost: 23 c ---[ 835]---> BDD-cost: 11 c ---[ 834]---> BDD-cost: 13 c ---[ 833]---> BDD-cost: 35 c ---[ 832]---> BDD-cost: 39 c ---[ 831]---> Adder-cost: 7378 maxlim: 4 bits: 4/3 c ---[ 830]---> BDD-cost: 35 c ---[ 829]---> BDD-cost: 39 c ---[ 828]---> BDD-cost: 35 c ---[ 827]---> BDD-cost: 39 c ---[ 826]---> BDD-cost: 29 c ---[ 825]---> BDD-cost: 19 c ---[ 824]---> BDD-cost: 29 c ---[ 823]---> BDD-cost: 23 c ---[ 822]---> BDD-cost: 13 c ---[ 821]---> BDD-cost: 39 c ---[ 819]---> BDD-cost: 29 c ---[ 818]---> BDD-cost: 29 c ---[ 817]---> BDD-cost: 39 c ---[ 816]---> BDD-cost: 15 c ---[ 815]---> BDD-cost: 23 c ---[ 814]---> BDD-cost: 19 c ---[ 813]---> BDD-cost: 29 c ---[ 812]---> BDD-cost: 13 c ---[ 811]---> BDD-cost: 29 c ---[ 810]---> BDD-cost: 29 c ---[ 808]---> BDD-cost: 39 c ---[ 807]---> BDD-cost: 39 c ---[ 806]---> BDD-cost: 13 c ---[ 805]---> BDD-cost: 29 c ---[ 804]---> BDD-cost: 29 c ---[ 803]---> BDD-cost: 35 c ---[ 802]---> BDD-cost: 39 c ---[ 801]---> BDD-cost: 29 c ---[ 800]---> BDD-cost: 15 c ---[ 799]---> BDD-cost: 13 c ---[ 797]---> BDD-cost: 25 c ---[ 796]---> BDD-cost: 29 c ---[ 795]---> BDD-cost: 29 c ---[ 794]---> BDD-cost: 35 c ---[ 793]---> BDD-cost: 39 c ---[ 792]---> BDD-cost: 29 c ---[ 791]---> BDD-cost: 13 c ---[ 790]---> BDD-cost: 23 c ---[ 789]---> BDD-cost: 35 c ---[ 788]---> BDD-cost: 39 c ---[ 786]---> BDD-cost: 29 c ---[ 785]---> BDD-cost: 25 c ---[ 784]---> BDD-cost: 29 c ---[ 783]---> BDD-cost: 39 c ---[ 782]---> BDD-cost: 23 c ---[ 781]---> BDD-cost: 23 c ---[ 780]---> BDD-cost: 29 c ---[ 779]---> BDD-cost: 29 c ---[ 778]---> BDD-cost: 25 c ---[ 777]---> BDD-cost: 29 c ---[ 776]---> BDD-cost: 0 c ---[ 775]---> BDD-cost: 35 c ---[ 774]---> BDD-cost: 39 c ---[ 773]---> BDD-cost: 29 c ---[ 772]---> BDD-cost: 39 c ---[ 771]---> BDD-cost: 29 c ---[ 770]---> BDD-cost: 29 c ---[ 769]---> BDD-cost: 35 c ---[ 768]---> BDD-cost: 39 c ---[ 767]---> BDD-cost: 25 c ---[ 766]---> BDD-cost: 45 c ---[ 765]---> Adder-cost: 0 maxlim: 31 bits: 6/5 c ---[ 764]---> BDD-cost: 23 c ---[ 763]---> BDD-cost: 13 c ---[ 762]---> BDD-cost: 23 c ---[ 761]---> BDD-cost: 45 c ---[ 760]---> BDD-cost: 45 c ---[ 759]---> BDD-cost: 13 c ---[ 758]---> BDD-cost: 45 c ---[ 757]---> BDD-cost: 21 c ---[ 756]---> BDD-cost: 45 c ---[ 755]---> BDD-cost: 45 c ---[ 753]---> BDD-cost: 3225 c ---[ 752]---> BDD-cost: 13 c ---[ 751]---> BDD-cost: 23 c ---[ 750]---> BDD-cost: 35 c ---[ 749]---> BDD-cost: 39 c ---[ 748]---> BDD-cost: 29 c ---[ 747]---> BDD-cost: 13 c ---[ 746]---> BDD-cost: 25 c ---[ 745]---> BDD-cost: 29 c ---[ 744]---> BDD-cost: 39 c ---[ 743]---> BDD-cost: 23 c ---[ 742]---> BDD-cost: 1279 c ---[ 741]---> BDD-cost: 13 c ---[ 740]---> BDD-cost: 23 c ---[ 739]---> BDD-cost: 29 c ---[ 738]---> BDD-cost: 29 c ---[ 737]---> BDD-cost: 25 c ---[ 736]---> BDD-cost: 29 c ---[ 735]---> BDD-cost: 35 c ---[ 734]---> BDD-cost: 39 c ---[ 733]---> BDD-cost: 29 c ---[ 732]---> BDD-cost: 39 c ---[ 730]---> BDD-cost: 29 c ---[ 729]---> BDD-cost: 29 c ---[ 728]---> BDD-cost: 35 c ---[ 727]---> BDD-cost: 39 c ---[ 726]---> BDD-cost: 25 c ---[ 725]---> BDD-cost: 13 c ---[ 724]---> BDD-cost: 37 c ---[ 723]---> BDD-cost: 43 c ---[ 722]---> BDD-cost: 43 c ---[ 721]---> BDD-cost: 45 c ---[ 719]---> BDD-cost: 23 c ---[ 718]---> BDD-cost: 45 c ---[ 717]---> BDD-cost: 45 c ---[ 716]---> BDD-cost: 23 c ---[ 715]---> BDD-cost: 13 c ---[ 714]---> BDD-cost: 43 c ---[ 713]---> BDD-cost: 15 c ---[ 712]---> BDD-cost: 23 c ---[ 711]---> BDD-cost: 45 c ---[ 710]---> BDD-cost: 13 c ---[ 708]---> BDD-cost: 45 c ---[ 707]---> BDD-cost: 45 c ---[ 706]---> BDD-cost: 13 c ---[ 705]---> BDD-cost: 45 c ---[ 704]---> BDD-cost: 45 c ---[ 703]---> BDD-cost: 45 c ---[ 702]---> BDD-cost: 43 c ---[ 701]---> BDD-cost: 43 c ---[ 700]---> BDD-cost: 13 c ---[ 699]---> BDD-cost: 45 c ---[ 697]---> BDD-cost: 45 c ---[ 696]---> BDD-cost: 43 c ---[ 695]---> BDD-cost: 45 c ---[ 694]---> BDD-cost: 13 c ---[ 693]---> BDD-cost: 35 c ---[ 692]---> BDD-cost: 39 c ---[ 691]---> BDD-cost: 29 c ---[ 690]---> BDD-cost: 25 c ---[ 689]---> BDD-cost: 29 c ---[ 688]---> BDD-cost: 39 c ---[ 686]---> BDD-cost: 17 c ---[ 685]---> BDD-cost: 25 c ---[ 684]---> BDD-cost: 21 c ---[ 683]---> BDD-cost: 29 c ---[ 682]---> BDD-cost: 29 c ---[ 681]---> BDD-cost: 3 c ---[ 680]---> BDD-cost: 29 c ---[ 679]---> BDD-cost: 35 c ---[ 678]---> BDD-cost: 39 c ---[ 677]---> BDD-cost: 29 c ---[ 675]---> BDD-cost: 39 c ---[ 674]---> BDD-cost: 29 c ---[ 673]---> BDD-cost: 29 c ---[ 672]---> BDD-cost: 35 c ---[ 671]---> BDD-cost: 39 c ---[ 670]---> BDD-cost: 3 c ---[ 669]---> BDD-cost: 11 c ---[ 668]---> BDD-cost: 35 c ---[ 667]---> BDD-cost: 39 c ---[ 666]---> BDD-cost: 35 c ---[ 665]---> BDD-cost: 1030 c ---[ 664]---> BDD-cost: 39 c ---[ 663]---> BDD-cost: 39 c ---[ 662]---> BDD-cost: 35 c ---[ 661]---> BDD-cost: 39 c ---[ 660]---> BDD-cost: 19 c ---[ 659]---> BDD-cost: 35 c ---[ 658]---> BDD-cost: 39 c ---[ 657]---> BDD-cost: 19 c ---[ 656]---> BDD-cost: 35 c ---[ 655]---> BDD-cost: 39 c ---[ 654]---> Adder-cost: 1065 maxlim: 26 bits: 6/5 c ---[ 653]---> BDD-cost: 35 c ---[ 652]---> BDD-cost: 39 c ---[ 651]---> BDD-cost: 17 c ---[ 650]---> BDD-cost: 35 c ---[ 649]---> BDD-cost: 39 c ---[ 648]---> BDD-cost: 5 c ---[ 647]---> BDD-cost: 35 c ---[ 646]---> BDD-cost: 39 c ---[ 645]---> BDD-cost: 35 c ---[ 644]---> BDD-cost: 39 c ---[ 642]---> Adder-cost: 4843 maxlim: 4 bits: 4/3 c ---[ 641]---> BDD-cost: 39 c ---[ 640]---> BDD-cost: 35 c ---[ 639]---> BDD-cost: 39 c ---[ 638]---> BDD-cost: 35 c ---[ 637]---> BDD-cost: 35 c ---[ 636]---> BDD-cost: 35 c ---[ 635]---> BDD-cost: 39 c ---[ 634]---> BDD-cost: 35 c ---[ 633]---> BDD-cost: 35 c ---[ 632]---> BDD-cost: 39 c ---[ 630]---> BDD-cost: 35 c ---[ 629]---> BDD-cost: 35 c ---[ 628]---> BDD-cost: 39 c ---[ 627]---> BDD-cost: 35 c ---[ 625]---> BDD-cost: 35 c ---[ 624]---> BDD-cost: 39 c ---[ 623]---> BDD-cost: 17 c ---[ 622]---> BDD-cost: 35 c ---[ 621]---> BDD-cost: 39 c ---[ 619]---> BDD-cost: 35 c ---[ 618]---> BDD-cost: 39 c ---[ 617]---> BDD-cost: 11 c ---[ 616]---> BDD-cost: 35 c ---[ 615]---> BDD-cost: 39 c ---[ 614]---> BDD-cost: 35 c ---[ 613]---> BDD-cost: 39 c ---[ 612]---> BDD-cost: 35 c ---[ 611]---> BDD-cost: 39 c ---[ 610]---> BDD-cost: 13 c ---[ 608]---> BDD-cost: 35 c ---[ 607]---> BDD-cost: 39 c ---[ 606]---> BDD-cost: 19 c ---[ 605]---> BDD-cost: 35 c ---[ 604]---> BDD-cost: 35 c ---[ 603]---> BDD-cost: 43 c ---[ 602]---> BDD-cost: 35 c ---[ 601]---> BDD-cost: 39 c ---[ 600]---> BDD-cost: 19 c ---[ 599]---> BDD-cost: 35 c ---[ 597]---> BDD-cost: 35 c ---[ 596]---> BDD-cost: 39 c ---[ 595]---> BDD-cost: 19 c ---[ 594]---> BDD-cost: 43 c ---[ 593]---> BDD-cost: 19 c ---[ 592]---> BDD-cost: 35 c ---[ 591]---> BDD-cost: 17 c ---[ 590]---> BDD-cost: 7 c ---[ 589]---> BDD-cost: 19 c ---[ 588]---> BDD-cost: 35 c ---[ 586]---> BDD-cost: 39 c ---[ 585]---> BDD-cost: 29 c ---[ 584]---> BDD-cost: 29 c ---[ 583]---> BDD-cost: 39 c ---[ 582]---> BDD-cost: 27 c ---[ 581]---> BDD-cost: 45 c ---[ 580]---> BDD-cost: 29 c ---[ 579]---> BDD-cost: 45 c ---[ 578]---> BDD-cost: 25 c ---[ 577]---> BDD-cost: 19 c ---[ 575]---> BDD-cost: 29 c ---[ 574]---> BDD-cost: 25 c ---[ 573]---> BDD-cost: 35 c ---[ 572]---> BDD-cost: 27 c ---[ 571]---> BDD-cost: 27 c ---[ 570]---> BDD-cost: 35 c ---[ 569]---> BDD-cost: 29 c ---[ 568]---> BDD-cost: 29 c ---[ 567]---> BDD-cost: 3 c ---[ 566]---> BDD-cost: 25 c ---[ 564]---> BDD-cost: 29 c ---[ 563]---> BDD-cost: 39 c ---[ 562]---> BDD-cost: 23 c ---[ 561]---> BDD-cost: 3 c ---[ 560]---> BDD-cost: 23 c ---[ 559]---> BDD-cost: 29 c ---[ 558]---> BDD-cost: 29 c ---[ 557]---> BDD-cost: 25 c ---[ 556]---> BDD-cost: 29 c ---[ 555]---> BDD-cost: 35 c ---[ 553]---> BDD-cost: 39 c ---[ 552]---> BDD-cost: 29 c ---[ 551]---> BDD-cost: 39 c ---[ 550]---> BDD-cost: 29 c ---[ 549]---> BDD-cost: 29 c ---[ 548]---> BDD-cost: 35 c ---[ 547]---> BDD-cost: 39 c ---[ 546]---> BDD-cost: 25 c ---[ 545]---> BDD-cost: 35 c ---[ 544]---> BDD-cost: 39 c ---[ 542]---> BDD-cost: 45 c ---[ 541]---> BDD-cost: 45 c ---[ 540]---> BDD-cost: 35 c ---[ 539]---> BDD-cost: 35 c ---[ 538]---> BDD-cost: 35 c ---[ 537]---> BDD-cost: 39 c ---[ 536]---> BDD-cost: 35 c ---[ 535]---> BDD-cost: 39 c ---[ 534]---> BDD-cost: 35 c ---[ 533]---> BDD-cost: 39 c ---[ 532]---> BDD-cost:11348 c ---[ 531]---> BDD-cost: 6571 c ---[ 530]---> BDD-cost: 29 c ---[ 529]---> BDD-cost: 29 c ---[ 528]---> BDD-cost: 35 c ---[ 527]---> BDD-cost: 39 c ---[ 526]---> BDD-cost: 39 c ---[ 525]---> BDD-cost: 27 c ---[ 524]---> BDD-cost: 45 c ---[ 523]---> BDD-cost: 29 c ---[ 522]---> BDD-cost: 45 c ---[ 521]---> BDD-cost: 29 c ---[ 520]---> BDD-cost: 2592 c ---[ 519]---> BDD-cost: 19 c ---[ 518]---> BDD-cost: 43 c ---[ 517]---> BDD-cost: 29 c ---[ 516]---> BDD-cost: 19 c ---[ 515]---> BDD-cost: 35 c ---[ 514]---> BDD-cost: 27 c ---[ 513]---> BDD-cost: 45 c ---[ 512]---> BDD-cost: 45 c ---[ 511]---> BDD-cost: 19 c ---[ 510]---> BDD-cost: 21 c ---[ 508]---> BDD-cost: 9 c ---[ 507]---> BDD-cost: 35 c ---[ 506]---> BDD-cost: 29 c ---[ 505]---> BDD-cost: 25 c ---[ 504]---> BDD-cost: 39 c ---[ 503]---> BDD-cost: 29 c ---[ 502]---> BDD-cost: 29 c ---[ 501]---> BDD-cost: 39 c ---[ 500]---> BDD-cost: 23 c ---[ 499]---> BDD-cost: 23 c ---[ 497]---> BDD-cost: 29 c ---[ 496]---> BDD-cost: 25 c ---[ 495]---> BDD-cost: 29 c ---[ 494]---> BDD-cost: 29 c ---[ 493]---> BDD-cost: 39 c ---[ 492]---> BDD-cost: 39 c ---[ 491]---> BDD-cost: 25 c ---[ 490]---> BDD-cost: 29 c ---[ 489]---> BDD-cost: 29 c ---[ 488]---> BDD-cost: 35 c ---[ 486]---> BDD-cost: 39 c ---[ 485]---> BDD-cost: 29 c ---[ 484]---> BDD-cost: 39 c ---[ 483]---> BDD-cost: 23 c ---[ 482]---> BDD-cost: 25 c ---[ 481]---> BDD-cost: 25 c ---[ 480]---> BDD-cost: 29 c ---[ 479]---> BDD-cost: 29 c ---[ 478]---> BDD-cost: 29 c ---[ 477]---> BDD-cost: 35 c ---[ 475]---> BDD-cost: 39 c ---[ 474]---> BDD-cost: 29 c ---[ 473]---> BDD-cost: 25 c ---[ 472]---> BDD-cost: 39 c ---[ 471]---> BDD-cost: 29 c ---[ 470]---> BDD-cost: 29 c ---[ 469]---> BDD-cost: 39 c ---[ 468]---> BDD-cost: 17 c ---[ 467]---> BDD-cost: 25 c ---[ 466]---> BDD-cost: 21 c ---[ 465]---> BDD-cost:10772 c ---[ 464]---> BDD-cost: 29 c ---[ 463]---> BDD-cost: 5 c ---[ 462]---> BDD-cost: 29 c ---[ 461]---> BDD-cost: 29 c ---[ 460]---> BDD-cost: 39 c ---[ 459]---> BDD-cost: 39 c ---[ 458]---> BDD-cost: 5 c ---[ 457]---> BDD-cost: 29 c ---[ 456]---> BDD-cost: 29 c ---[ 455]---> BDD-cost: 35 c ---[ 453]---> BDD-cost: 39 c ---[ 452]---> BDD-cost: 29 c ---[ 451]---> BDD-cost: 39 c ---[ 450]---> BDD-cost: 17 c ---[ 449]---> BDD-cost: 13 c ---[ 448]---> BDD-cost: 25 c ---[ 447]---> BDD-cost: 29 c ---[ 446]---> BDD-cost: 29 c ---[ 445]---> BDD-cost: 29 c ---[ 444]---> BDD-cost: 35 c ---[ 442]---> BDD-cost: 39 c ---[ 441]---> BDD-cost: 29 c ---[ 440]---> BDD-cost: 5 c ---[ 439]---> BDD-cost: 39 c ---[ 438]---> BDD-cost: 29 c ---[ 437]---> BDD-cost: 35 c ---[ 436]---> BDD-cost: 39 c ---[ 435]---> BDD-cost: 39 c ---[ 434]---> BDD-cost: 27 c ---[ 433]---> BDD-cost: 39 c ---[ 431]---> BDD-cost: 29 c ---[ 430]---> BDD-cost: 35 c ---[ 429]---> BDD-cost: 39 c ---[ 428]---> BDD-cost: 39 c ---[ 427]---> BDD-cost: 35 c ---[ 426]---> BDD-cost: 35 c ---[ 425]---> BDD-cost: 39 c ---[ 424]---> BDD-cost: 19 c ---[ 423]---> BDD-cost: 35 c ---[ 422]---> BDD-cost: 39 c ---[ 419]---> BDD-cost: 35 c ---[ 418]---> BDD-cost: 39 c ---[ 417]---> BDD-cost: 29 c ---[ 416]---> BDD-cost: 29 c ---[ 415]---> BDD-cost: 39 c ---[ 414]---> BDD-cost: 39 c ---[ 413]---> BDD-cost: 27 c ---[ 412]---> BDD-cost: 29 c ---[ 411]---> BDD-cost: 39 c ---[ 410]---> BDD-cost: 39 c ---[ 408]---> BDD-cost: 29 c ---[ 407]---> BDD-cost: 27 c ---[ 406]---> BDD-cost: 39 c ---[ 405]---> BDD-cost: 29 c ---[ 404]---> BDD-cost: 39 c ---[ 403]---> BDD-cost: 39 c ---[ 402]---> BDD-cost: 29 c ---[ 401]---> BDD-cost: 35 c ---[ 400]---> BDD-cost: 39 c ---[ 399]---> BDD-cost: 39 c ---[ 397]---> BDD-cost: 29 c ---[ 396]---> BDD-cost: 39 c ---[ 395]---> BDD-cost: 39 c ---[ 394]---> BDD-cost: 29 c ---[ 393]---> BDD-cost: 7 c ---[ 392]---> BDD-cost: 39 c ---[ 391]---> BDD-cost: 27 c ---[ 390]---> BDD-cost: 39 c ---[ 389]---> BDD-cost: 39 c ---[ 388]---> BDD-cost: 29 c ---[ 386]---> BDD-cost: 29 c ---[ 385]---> BDD-cost: 39 c ---[ 384]---> BDD-cost: 23 c ---[ 383]---> BDD-cost: 45 c ---[ 382]---> BDD-cost: 17 c ---[ 381]---> BDD-cost: 45 c ---[ 380]---> BDD-cost: 45 c ---[ 379]---> BDD-cost: 17 c ---[ 378]---> BDD-cost: 45 c ---[ 377]---> BDD-cost: 45 c ---[ 375]---> BDD-cost: 45 c ---[ 374]---> BDD-cost: 45 c ---[ 373]---> BDD-cost: 45 c ---[ 372]---> BDD-cost: 45 c ---[ 371]---> BDD-cost: 45 c ---[ 370]---> BDD-cost: 17 c ---[ 369]---> BDD-cost: 23 c ---[ 368]---> BDD-cost: 29 c ---[ 367]---> BDD-cost: 25 c ---[ 366]---> BDD-cost: 29 c ---[ 365]---> BDD-cost:11754 c ---[ 364]---> BDD-cost: 29 c ---[ 363]---> BDD-cost: 39 c ---[ 362]---> BDD-cost: 39 c ---[ 361]---> BDD-cost: 25 c ---[ 360]---> BDD-cost: 29 c ---[ 359]---> BDD-cost: 29 c ---[ 358]---> BDD-cost: 35 c ---[ 357]---> BDD-cost: 39 c ---[ 356]---> BDD-cost: 29 c ---[ 355]---> BDD-cost: 39 c ---[ 353]---> BDD-cost: 23 c ---[ 352]---> BDD-cost: 25 c ---[ 351]---> BDD-cost: 25 c ---[ 350]---> BDD-cost: 29 c ---[ 349]---> BDD-cost: 29 c ---[ 348]---> BDD-cost: 29 c ---[ 347]---> BDD-cost: 35 c ---[ 346]---> BDD-cost: 39 c ---[ 345]---> BDD-cost: 29 c ---[ 344]---> BDD-cost: 25 c ---[ 342]---> BDD-cost: 45 c ---[ 341]---> BDD-cost: 21 c ---[ 340]---> BDD-cost: 45 c ---[ 339]---> BDD-cost: 45 c ---[ 338]---> BDD-cost: 21 c ---[ 337]---> BDD-cost: 45 c ---[ 336]---> BDD-cost: 45 c ---[ 335]---> BDD-cost: 45 c ---[ 334]---> BDD-cost: 45 c ---[ 333]---> BDD-cost: 45 c ---[ 331]---> BDD-cost: 45 c ---[ 330]---> BDD-cost: 45 c ---[ 329]---> BDD-cost: 21 c ---[ 328]---> BDD-cost: 21 c ---[ 327]---> BDD-cost: 29 c ---[ 326]---> BDD-cost: 21 c ---[ 325]---> BDD-cost: 35 c ---[ 324]---> BDD-cost: 27 c ---[ 323]---> BDD-cost: 23 c ---[ 322]---> BDD-cost: 35 c ---[ 320]---> BDD-cost: 29 c ---[ 319]---> BDD-cost: 29 c ---[ 318]---> BDD-cost: 29 c ---[ 317]---> BDD-cost: 29 c ---[ 316]---> BDD-cost: 35 c ---[ 315]---> BDD-cost: 39 c ---[ 314]---> BDD-cost: 29 c ---[ 313]---> BDD-cost: 39 c ---[ 312]---> BDD-cost: 29 c ---[ 311]---> BDD-cost: 29 c ---[ 310]---> BDD-cost: 7190 c ---[ 308]---> BDD-cost: 35 c ---[ 307]---> BDD-cost: 39 c ---[ 305]---> BDD-cost: 19 c ---[ 304]---> BDD-cost: 43 c ---[ 303]---> BDD-cost: 29 c ---[ 302]---> BDD-cost: 35 c ---[ 301]---> BDD-cost: 13 c ---[ 300]---> BDD-cost: 35 c ---[ 299]---> BDD-cost: 35 c ---[ 297]---> BDD-cost: 29 c ---[ 296]---> BDD-cost: 45 c ---[ 295]---> BDD-cost: 45 c ---[ 294]---> BDD-cost: 23 c ---[ 293]---> BDD-cost: 25 c ---[ 292]---> BDD-cost: 35 c ---[ 291]---> BDD-cost: 19 c ---[ 290]---> BDD-cost: 29 c ---[ 289]---> BDD-cost: 29 c ---[ 288]---> BDD-cost: 19 c ---[ 287]---> BDD-cost: 2951 c ---[ 286]---> BDD-cost: 19 c ---[ 285]---> BDD-cost: 35 c ---[ 284]---> BDD-cost: 27 c ---[ 283]---> BDD-cost: 39 c ---[ 282]---> BDD-cost: 45 c ---[ 281]---> BDD-cost: 45 c ---[ 280]---> BDD-cost: 19 c ---[ 279]---> BDD-cost: 19 c ---[ 278]---> BDD-cost: 35 c ---[ 277]---> BDD-cost: 19 c ---[ 275]---> BDD-cost: 29 c ---[ 274]---> BDD-cost: 39 c ---[ 273]---> BDD-cost: 39 c ---[ 272]---> BDD-cost: 43 c ---[ 271]---> BDD-cost: 43 c ---[ 270]---> BDD-cost: 43 c ---[ 269]---> BDD-cost: 43 c ---[ 268]---> BDD-cost: 39 c ---[ 267]---> BDD-cost: 39 c ---[ 266]---> BDD-cost: 29 c ---[ 264]---> BDD-cost: 29 c ---[ 263]---> BDD-cost: 35 c ---[ 262]---> BDD-cost: 39 c ---[ 261]---> BDD-cost: 29 c ---[ 260]---> BDD-cost: 39 c ---[ 259]---> BDD-cost: 17 c ---[ 258]---> BDD-cost: 13 c ---[ 257]---> BDD-cost: 25 c ---[ 256]---> BDD-cost: 29 c ---[ 255]---> BDD-cost: 29 c ---[ 253]---> BDD-cost: 29 c ---[ 252]---> BDD-cost: 35 c ---[ 251]---> BDD-cost: 39 c ---[ 250]---> BDD-cost: 29 c ---[ 248]---> BDD-cost: 35 c ---[ 247]---> BDD-cost: 35 c ---[ 246]---> BDD-cost: 35 c ---[ 245]---> BDD-cost: 29 c ---[ 244]---> BDD-cost: 45 c ---[ 242]---> BDD-cost: 45 c ---[ 241]---> BDD-cost: 23 c ---[ 240]---> BDD-cost: 25 c ---[ 239]---> BDD-cost: 35 c ---[ 238]---> BDD-cost: 19 c ---[ 237]---> BDD-cost: 29 c ---[ 236]---> BDD-cost: 35 c ---[ 235]---> BDD-cost: 35 c ---[ 234]---> BDD-cost: 39 c ---[ 233]---> BDD-cost: 35 c ---[ 231]---> BDD-cost: 39 c ---[ 230]---> BDD-cost: 45 c ---[ 229]---> BDD-cost: 45 c ---[ 228]---> BDD-cost: 35 c ---[ 227]---> BDD-cost: 35 c ---[ 226]---> BDD-cost: 35 c ---[ 225]---> BDD-cost: 35 c ---[ 224]---> BDD-cost: 39 c ---[ 223]---> BDD-cost: 35 c ---[ 222]---> BDD-cost: 29 c ---[ 220]---> BDD-cost: 23 c ---[ 219]---> BDD-cost: 25 c ---[ 218]---> BDD-cost: 35 c ---[ 217]---> BDD-cost: 29 c ---[ 216]---> BDD-cost: 35 c ---[ 215]---> BDD-cost: 43 c ---[ 214]---> BDD-cost: 35 c ---[ 213]---> BDD-cost: 35 c ---[ 212]---> BDD-cost: 39 c ---[ 211]---> BDD-cost: 5 c ---[ 209]---> BDD-cost: 35 c ---[ 208]---> BDD-cost: 39 c ---[ 207]---> BDD-cost: 43 c ---[ 206]---> BDD-cost: 35 c ---[ 205]---> BDD-cost: 29 c ---[ 204]---> BDD-cost: 11 c ---[ 203]---> BDD-cost: 35 c ---[ 202]---> BDD-cost: 27 c ---[ 201]---> BDD-cost: 35 c ---[ 200]---> BDD-cost: 35 c ---[ 199]---> BDD-cost: 7370 c ---[ 197]---> BDD-cost: 29 c ---[ 196]---> BDD-cost: 29 c ---[ 195]---> BDD-cost: 39 c ---[ 194]---> BDD-cost: 45 c ---[ 193]---> BDD-cost: 45 c ---[ 192]---> BDD-cost: 17 c ---[ 191]---> BDD-cost: 45 c ---[ 190]---> BDD-cost: 43 c ---[ 189]---> BDD-cost: 13 c ---[ 188]---> BDD-cost: 25 c ---[ 186]---> BDD-cost: 23 c ---[ 185]---> BDD-cost: 25 c ---[ 184]---> BDD-cost: 35 c ---[ 183]---> BDD-cost: 29 c ---[ 182]---> BDD-cost: 27 c ---[ 181]---> BDD-cost: 35 c ---[ 180]---> BDD-cost: 39 c ---[ 179]---> BDD-cost: 23 c ---[ 178]---> BDD-cost: 29 c ---[ 177]---> BDD-cost: 35 c ---[ 176]---> Adder-cost: 14905 maxlim: 25 bits: 6/5 c ---[ 175]---> BDD-cost: 25 c ---[ 174]---> BDD-cost: 29 c ---[ 173]---> BDD-cost: 35 c ---[ 172]---> BDD-cost: 35 c ---[ 171]---> BDD-cost: 39 c ---[ 170]---> BDD-cost: 29 c ---[ 169]---> Adder-cost: 4078 maxlim: 22 bits: 6/5 c ---[ 162]---> BDD-cost: 8628 c ---[ 155]---> Adder-cost: 6350 maxlim: 28 bits: 6/5 c ---[ 151]---> BDD-cost: 512 c ---[ 150]---> BDD-cost: 2589 c ---[ 149]---> Adder-cost: 3452 maxlim: 22 bits: 6/5 c ---[ 148]---> BDD-cost: 2014 c ---[ 147]---> Adder-cost: 7393 maxlim: 13 bits: 5/4 c ---[ 146]---> BDD-cost: 4198 c ---[ 145]---> BDD-cost: 7632 c ---[ 144]---> BDD-cost: 2670 c ---[ 143]---> BDD-cost: 218 c ---[ 142]---> BDD-cost: 267 c ---[ 141]---> BDD-cost: 172 c ---[ 140]---> BDD-cost: 156 c ---[ 139]---> BDD-cost: 906 c ---[ 138]---> BDD-cost: 2278 c ---[ 137]---> BDD-cost: 1528 c ---[ 136]---> BDD-cost: 5832 c ---[ 135]---> BDD-cost: 62 c ---[ 134]---> BDD-cost: 252 c ---[ 133]---> BDD-cost: 188 c ---[ 132]---> BDD-cost: 1184 c ---[ 131]---> BDD-cost: 718 c ---[ 130]---> BDD-cost: 1100 c ---[ 129]---> BDD-cost: 2508 c ---[ 128]---> BDD-cost: 1150 c ---[ 127]---> BDD-cost: 3936 c ---[ 126]---> BDD-cost: 42 c ---[ 125]---> BDD-cost: 84 c ---[ 124]---> BDD-cost: 260 c ---[ 123]---> BDD-cost: 3116 c ---[ 122]---> BDD-cost: 4948 c ---[ 121]---> BDD-cost: 677 c ---[ 120]---> BDD-cost: 6103 c ---[ 119]---> BDD-cost: 1076 c ---[ 118]---> BDD-cost: 877 c ---[ 117]---> BDD-cost: 925 c ---[ 116]---> BDD-cost: 5587 c ---[ 115]---> BDD-cost: 3737 c ---[ 114]---> BDD-cost: 6970 c ---[ 113]---> BDD-cost: 750 c ---[ 112]---> BDD-cost: 3897 c ---[ 111]---> BDD-cost: 516 c ---[ 110]---> BDD-cost: 1813 c ---[ 109]---> BDD-cost: 1320 c ---[ 108]---> BDD-cost: 2942 c ---[ 107]---> BDD-cost: 2610 c ---[ 106]---> BDD-cost: 795 c ---[ 105]---> BDD-cost: 4397 c ---[ 104]---> BDD-cost: 1303 c ---[ 103]---> BDD-cost: 4943 c ---[ 102]---> BDD-cost: 1194 c ---[ 101]---> BDD-cost: 4333 c ---[ 100]---> BDD-cost: 437 c ---[ 99]---> BDD-cost: 250 c ---[ 98]---> BDD-cost: 7832 c ---[ 97]---> Adder-cost: 12966 maxlim: 17 bits: 6/5 c ---[ 96]---> BDD-cost: 5415 c ---[ 95]---> Adder-cost: 2316 maxlim: 21 bits: 6/5 c ---[ 94]---> BDD-cost: 234 c ---[ 93]---> BDD-cost: 212 c ---[ 92]---> BDD-cost: 4374 c ---[ 91]---> BDD-cost: 732 c ---[ 90]---> BDD-cost: 2076 c ---[ 89]---> BDD-cost: 286 c ---[ 88]---> BDD-cost: 2622 c ---[ 87]---> BDD-cost: 382 c ---[ 86]---> BDD-cost: 2248 c ---[ 85]---> BDD-cost: 5404 c ---[ 84]---> BDD-cost: 854 c ---[ 83]---> BDD-cost: 7887 c ---[ 82]---> BDD-cost: 991 c ---[ 81]---> BDD-cost: 4578 c ---[ 80]---> BDD-cost: 607 c ---[ 79]---> BDD-cost: 217 c ---[ 78]---> BDD-cost: 1449 c ---[ 77]---> BDD-cost: 1048 c ---[ 76]---> BDD-cost: 862 c ---[ 75]---> BDD-cost: 1956 c ---[ 74]---> BDD-cost: 5181 c ---[ 73]---> BDD-cost: 458 c ---[ 72]---> BDD-cost: 98 c ---[ 71]---> BDD-cost: 3438 c ---[ 70]---> BDD-cost: 878 c ---[ 69]---> BDD-cost: 728 c ---[ 68]---> BDD-cost: 1368 c ---[ 67]---> BDD-cost: 4240 c ---[ 66]---> BDD-cost: 4764 c ---[ 65]---> BDD-cost: 2522 c ---[ 64]---> BDD-cost: 2730 c ---[ 63]---> BDD-cost: 1097 c ---[ 62]---> BDD-cost: 875 c ---[ 61]---> BDD-cost: 776 c ---[ 60]---> BDD-cost: 2126 c ---[ 59]---> BDD-cost: 1226 c ---[ 58]---> BDD-cost: 1144 c ---[ 57]---> BDD-cost: 334 c ---[ 56]---> BDD-cost: 750 c ---[ 55]---> BDD-cost: 146 c ---[ 54]---> BDD-cost: 206 c ---[ 53]---> BDD-cost: 2832 c ---[ 52]---> BDD-cost: 8880 c ---[ 51]---> BDD-cost: 192 c ---[ 50]---> BDD-cost: 2964 c ---[ 49]---> Adder-cost: 8882 maxlim: 20 bits: 6/5 c ---[ 48]---> BDD-cost: 1 c ---[ 47]---> Adder-cost: 7973 maxlim: 20 bits: 6/5 c ---[ 46]---> BDD-cost: 80 c ---[ 45]---> BDD-cost: 238 c ---[ 44]---> BDD-cost: 88 c ---[ 43]---> BDD-cost: 136 c ---[ 42]---> BDD-cost: 4262 c ---[ 41]---> BDD-cost:10085 c ---[ 40]---> BDD-cost: 968 c ---[ 39]---> BDD-cost: 921 c ---[ 38]---> BDD-cost: 2472 c ---[ 37]---> BDD-cost: 2262 c ---[ 36]---> BDD-cost: 1946 c ---[ 35]---> Adder-cost: 11313 maxlim: 17 bits: 6/5 c ---[ 34]---> BDD-cost: 1782 c ---[ 33]---> BDD-cost: 1032 c ---[ 32]---> BDD-cost: 1406 c ---[ 31]---> BDD-cost: 1286 c ---[ 30]---> BDD-cost: 1732 c ---[ 29]---> BDD-cost: 3506 c ---[ 28]---> BDD-cost: 4667 c ---[ 27]---> BDD-cost: 5492 c ---[ 26]---> BDD-cost:15264 c ---[ 25]---> BDD-cost: 692 c ---[ 24]---> BDD-cost: 1291 c ---[ 23]---> BDD-cost: 938 c ---[ 22]---> BDD-cost: 1436 c ---[ 21]---> BDD-cost: 1850 c ---[ 20]---> BDD-cost: 2446 c ---[ 19]---> BDD-cost: 1294 c ---[ 18]---> BDD-cost: 1740 c ---[ 17]---> BDD-cost: 4705 c ---[ 16]---> BDD-cost: 574 c ---[ 15]---> BDD-cost: 2972 c ---[ 14]---> BDD-cost: 1798 c ---[ 13]---> BDD-cost: 2110 c ---[ 12]---> BDD-cost: 4576 c ---[ 11]---> BDD-cost: 7893 c ---[ 10]---> BDD-cost: 964 c ---[ 9]---> BDD-cost: 888 c ---[ 8]---> Adder-cost: 3085 maxlim: 18 bits: 6/5 c ---[ 7]---> BDD-cost:10368 c ---[ 6]---> BDD-cost:13837 c ---[ 5]---> BDD-cost: 2093 c ---[ 4]---> BDD-cost: 5322 c ---[ 3]---> BDD-cost:15898 c ---[ 2]---> BDD-cost:10691 c ---[ 1]---> BDD-cost: 7120 c ---[ 0]---> BDD-cost: 6716 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 1612556 5358940 | 537518 0 0 nan | 0.000 % | c | 100 | 1612556 5358940 | 591269 100 358 3.6 | 0.153 % | c | 251 | 1612545 5358913 | 650396 249 1184 4.8 | 0.154 % | c | 477 | 1612483 5358733 | 715436 425 1871 4.4 | 0.157 % | c | 816 | 1612407 5358505 | 786980 673 3074 4.6 | 0.161 % | c | 1330 | 1612401 5358493 | 865678 1186 5196 4.4 | 0.162 % | c | 2089 | 1612261 5358079 | 952245 1814 8334 4.6 | 0.170 % | c | 3228 | 1611909 5357029 | 1047470 2658 12229 4.6 | 0.185 % | c | 4939 | 1611387 5355431 | 1152217 4193 21511 5.1 | 0.212 % | c | 7501 | 1610810 5353702 | 1267439 6129 30616 5.0 | 0.243 % | c | 11346 | 1610060 5351408 | 1394183 9611 49637 5.2 | 0.281 % | c | 17113 | 1609854 5350770 | 1533601 15286 102328 6.7 | 0.290 % | c | 25762 | 1609239 5348845 | 1686961 23709 187289 7.9 | 0.317 % | c | 38736 | 1608577 5346827 | 1855657 36413 365690 10.0 | 0.351 % | c | 58199 | 1607386 5342910 | 2041223 55516 546629 9.8 | 0.390 % | c | 87393 | 1606181 5339015 | 2245346 84196 834494 9.9 | 0.437 % |
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/15139/stat): 15139 (minisat+_script) R 15138 15139 21452 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1854857232 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/15139/statm): 174 3 169 147 0 27 0 [pid=15139] 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=15140 New process pid=15141 New process pid=15142 One traced child (pid=15141) exited with status: 0 execve syscall for /bin/sed executable 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=15142) exited with status: 0 One traced child (pid=15140) exited with status: 0 New process pid=15143 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-sp98ic.opb [startup+10.004 s] Raw data (loadavg): 0.94 0.96 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 14373 0 0 0 907 51 0 0 25 0 1 0 1854857237 47972352 8903 4294967295 134512640 135094434 3221224432 3221222176 134781741 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 11712 8903 145 145 0 11567 0 [pid=15143] vsize: 46848 Current children cumulated CPU time (s) 9.6 Current children cumulated vsize (Kb) 48972 [startup+20.0047 s] Raw data (loadavg): 0.95 0.96 0.91 1/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) T 15139 15139 21452 0 -1 0 33722 0 0 0 1782 121 0 0 21 0 1 0 1854857237 116551680 26277 4294967295 134512640 135094434 3221224432 3221058044 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/15143/statm): 28455 26277 145 145 0 28310 0 [pid=15143] vsize: 113820 Current children cumulated CPU time (s) 19.05 Current children cumulated vsize (Kb) 115944 [startup+30.0054 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 54406 0 0 0 2600 205 0 0 25 0 1 0 1854857237 230813696 46961 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15143/statm): 56351 46961 145 145 0 56206 0 [pid=15143] vsize: 225404 Current children cumulated CPU time (s) 28.07 Current children cumulated vsize (Kb) 227528 [startup+40.0062 s] Raw data (loadavg): 0.96 0.96 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 54647 0 0 0 3598 206 0 0 25 0 1 0 1854857237 231862272 47202 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15143/statm): 56607 47202 145 145 0 56462 0 [pid=15143] vsize: 226428 Current children cumulated CPU time (s) 38.06 Current children cumulated vsize (Kb) 228552 [startup+50.0079 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 54848 0 0 0 4596 208 0 0 25 0 1 0 1854857237 232714240 47403 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15143/statm): 56815 47403 145 145 0 56670 0 [pid=15143] vsize: 227260 Current children cumulated CPU time (s) 48.06 Current children cumulated vsize (Kb) 229384 [startup+60.0086 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 55569 0 0 0 5588 211 0 0 25 0 1 0 1854857237 235614208 48124 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15143/statm): 57523 48124 145 145 0 57378 0 [pid=15143] vsize: 230092 Current children cumulated CPU time (s) 58.01 Current children cumulated vsize (Kb) 232216 [startup+70.0093 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 56231 0 0 0 6577 216 0 0 25 0 1 0 1854857237 238317568 48786 4294967295 134512640 135094434 3221224432 3221223092 134553444 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15143/statm): 58183 48786 145 145 0 58038 0 [pid=15143] vsize: 232732 Current children cumulated CPU time (s) 67.95 Current children cumulated vsize (Kb) 234856 [startup+80.011 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 57119 0 0 0 7565 223 0 0 25 0 1 0 1854857237 241737728 49674 4294967295 134512640 135094434 3221224432 3221223088 134561502 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15143/statm): 59018 49674 145 145 0 58873 0 [pid=15143] vsize: 236072 Current children cumulated CPU time (s) 77.9 Current children cumulated vsize (Kb) 238196 [startup+90.0117 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 57668 0 0 0 8556 227 0 0 25 0 1 0 1854857237 243855360 50223 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15143/statm): 59535 50223 145 145 0 59390 0 [pid=15143] vsize: 238140 Current children cumulated CPU time (s) 87.85 Current children cumulated vsize (Kb) 240264 [startup+100.012 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 57870 0 0 0 9553 229 0 0 25 0 1 0 1854857237 244666368 50425 4294967295 134512640 135094434 3221224432 3221223120 134558987 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15143/statm): 59733 50425 145 145 0 59588 0 [pid=15143] vsize: 238932 Current children cumulated CPU time (s) 97.84 Current children cumulated vsize (Kb) 241056 [startup+110.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 57964 0 0 0 10551 230 0 0 25 0 1 0 1854857237 245047296 50519 4294967295 134512640 135094434 3221224432 3221223088 134561502 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15143/statm): 59826 50519 145 145 0 59681 0 [pid=15143] vsize: 239304 Current children cumulated CPU time (s) 107.83 Current children cumulated vsize (Kb) 241428 [startup+120.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58112 0 0 0 11548 232 0 0 25 0 1 0 1854857237 245624832 50667 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15143/statm): 59967 50667 145 145 0 59822 0 [pid=15143] vsize: 239868 Current children cumulated CPU time (s) 117.82 Current children cumulated vsize (Kb) 241992 [startup+130.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58167 0 0 0 12547 233 0 0 25 0 1 0 1854857237 245850112 50722 4294967295 134512640 135094434 3221224432 3221223120 134558987 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15143/statm): 60022 50722 145 145 0 59877 0 [pid=15143] vsize: 240088 Current children cumulated CPU time (s) 127.82 Current children cumulated vsize (Kb) 242212 [startup+140.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58251 0 0 0 13544 234 0 0 25 0 1 0 1854857237 246173696 50806 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15143/statm): 60101 50806 145 145 0 59956 0 [pid=15143] vsize: 240404 Current children cumulated CPU time (s) 137.8 Current children cumulated vsize (Kb) 242528 [startup+150.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58331 0 0 0 14542 235 0 0 25 0 1 0 1854857237 246472704 50886 4294967295 134512640 135094434 3221224432 3221223104 134554872 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15143/statm): 60174 50886 145 145 0 60029 0 [pid=15143] vsize: 240696 Current children cumulated CPU time (s) 147.79 Current children cumulated vsize (Kb) 242820 [startup+160.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58339 0 0 0 15541 236 0 0 25 0 1 0 1854857237 246505472 50894 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15143/statm): 60182 50894 145 145 0 60037 0 [pid=15143] vsize: 240728 Current children cumulated CPU time (s) 157.79 Current children cumulated vsize (Kb) 242852 [startup+170.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58411 0 0 0 16539 237 0 0 25 0 1 0 1854857237 246792192 50966 4294967295 134512640 135094434 3221224432 3221223136 134554538 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15143/statm): 60252 50966 145 145 0 60107 0 [pid=15143] vsize: 241008 Current children cumulated CPU time (s) 167.78 Current children cumulated vsize (Kb) 243132 [startup+180.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58464 0 0 0 17538 237 0 0 25 0 1 0 1854857237 246976512 51019 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15143/statm): 60297 51019 145 145 0 60152 0 [pid=15143] vsize: 241188 Current children cumulated CPU time (s) 177.77 Current children cumulated vsize (Kb) 243312 [startup+190.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58516 0 0 0 18537 238 0 0 25 0 1 0 1854857237 247160832 51071 4294967295 134512640 135094434 3221224432 3221223092 134553528 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15143/statm): 60342 51071 145 145 0 60197 0 [pid=15143] vsize: 241368 Current children cumulated CPU time (s) 187.77 Current children cumulated vsize (Kb) 243492 [startup+200.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58522 0 0 0 19537 239 0 0 25 0 1 0 1854857237 247185408 51077 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15143/statm): 60348 51077 145 145 0 60203 0 [pid=15143] vsize: 241392 Current children cumulated CPU time (s) 197.78 Current children cumulated vsize (Kb) 243516 [startup+210.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58562 0 0 0 20536 239 0 0 25 0 1 0 1854857237 247312384 51117 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15143/statm): 60379 51117 145 145 0 60234 0 [pid=15143] vsize: 241516 Current children cumulated CPU time (s) 207.77 Current children cumulated vsize (Kb) 243640 [startup+220.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58578 0 0 0 21535 240 0 0 25 0 1 0 1854857237 247357440 51133 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15143/statm): 60390 51133 145 145 0 60245 0 [pid=15143] vsize: 241560 Current children cumulated CPU time (s) 217.77 Current children cumulated vsize (Kb) 243684 [startup+230.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58587 0 0 0 22534 240 0 0 25 0 1 0 1854857237 247394304 51142 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15143/statm): 60399 51142 145 145 0 60254 0 [pid=15143] vsize: 241596 Current children cumulated CPU time (s) 227.76 Current children cumulated vsize (Kb) 243720 [startup+240.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58604 0 0 0 23534 240 0 0 25 0 1 0 1854857237 247463936 51159 4294967295 134512640 135094434 3221224432 3221223092 134553519 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15143/statm): 60416 51159 145 145 0 60271 0 [pid=15143] vsize: 241664 Current children cumulated CPU time (s) 237.76 Current children cumulated vsize (Kb) 243788 [startup+250.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58612 0 0 0 24534 241 0 0 25 0 1 0 1854857237 247492608 51167 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15143/statm): 60423 51167 145 145 0 60278 0 [pid=15143] vsize: 241692 Current children cumulated CPU time (s) 247.77 Current children cumulated vsize (Kb) 243816 [startup+260.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58629 0 0 0 25533 241 0 0 25 0 1 0 1854857237 247541760 51184 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15143/statm): 60435 51184 145 145 0 60290 0 [pid=15143] vsize: 241740 Current children cumulated CPU time (s) 257.76 Current children cumulated vsize (Kb) 243864 [startup+270.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58637 0 0 0 26533 241 0 0 25 0 1 0 1854857237 247574528 51192 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 60443 51192 145 145 0 60298 0 [pid=15143] vsize: 241772 Current children cumulated CPU time (s) 267.76 Current children cumulated vsize (Kb) 243896 [startup+280.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58671 0 0 0 27533 241 0 0 25 0 1 0 1854857237 247603200 51226 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 60450 51226 145 145 0 60305 0 [pid=15143] vsize: 241800 Current children cumulated CPU time (s) 277.76 Current children cumulated vsize (Kb) 243924 [startup+290.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58690 0 0 0 28532 242 0 0 25 0 1 0 1854857237 247709696 51245 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15143/statm): 60476 51245 145 145 0 60331 0 [pid=15143] vsize: 241904 Current children cumulated CPU time (s) 287.76 Current children cumulated vsize (Kb) 244028 [startup+300.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58691 0 0 0 29532 243 0 0 25 0 1 0 1854857237 247713792 51246 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15143/statm): 60477 51246 145 145 0 60332 0 [pid=15143] vsize: 241908 Current children cumulated CPU time (s) 297.77 Current children cumulated vsize (Kb) 244032 [startup+310.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58725 0 0 0 30531 243 0 0 25 0 1 0 1854857237 247767040 51280 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15143/statm): 60490 51280 145 145 0 60345 0 [pid=15143] vsize: 241960 Current children cumulated CPU time (s) 307.76 Current children cumulated vsize (Kb) 244084 [startup+320.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58731 0 0 0 31530 244 0 0 25 0 1 0 1854857237 247791616 51286 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15143/statm): 60496 51286 145 145 0 60351 0 [pid=15143] vsize: 241984 Current children cumulated CPU time (s) 317.76 Current children cumulated vsize (Kb) 244108 [startup+330.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58751 0 0 0 32530 244 0 0 25 0 1 0 1854857237 247840768 51306 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 60508 51306 145 145 0 60363 0 [pid=15143] vsize: 242032 Current children cumulated CPU time (s) 327.76 Current children cumulated vsize (Kb) 244156 [startup+340.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58857 0 0 0 33529 245 0 0 25 0 1 0 1854857237 247889920 51412 4294967295 134512640 135094434 3221224432 3221223104 134553437 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 60520 51412 145 145 0 60375 0 [pid=15143] vsize: 242080 Current children cumulated CPU time (s) 337.76 Current children cumulated vsize (Kb) 244204 [startup+350.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58898 0 0 0 34528 246 0 0 25 0 1 0 1854857237 248004608 51453 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 60548 51453 145 145 0 60403 0 [pid=15143] vsize: 242192 Current children cumulated CPU time (s) 347.76 Current children cumulated vsize (Kb) 244316 [startup+360.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58914 0 0 0 35528 246 0 0 25 0 1 0 1854857237 248066048 51469 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 60563 51469 145 145 0 60418 0 [pid=15143] vsize: 242252 Current children cumulated CPU time (s) 357.76 Current children cumulated vsize (Kb) 244376 [startup+370.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58935 0 0 0 36527 247 0 0 25 0 1 0 1854857237 248147968 51490 4294967295 134512640 135094434 3221224432 3221223072 134558043 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 60583 51490 145 145 0 60438 0 [pid=15143] vsize: 242332 Current children cumulated CPU time (s) 367.76 Current children cumulated vsize (Kb) 244456 [startup+380.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58952 0 0 0 37527 247 0 0 25 0 1 0 1854857237 248213504 51507 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 60599 51507 145 145 0 60454 0 [pid=15143] vsize: 242396 Current children cumulated CPU time (s) 377.76 Current children cumulated vsize (Kb) 244520 [startup+390.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58965 0 0 0 38526 248 0 0 25 0 1 0 1854857237 248266752 51520 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 60612 51520 145 145 0 60467 0 [pid=15143] vsize: 242448 Current children cumulated CPU time (s) 387.76 Current children cumulated vsize (Kb) 244572 [startup+400.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 58987 0 0 0 39526 248 0 0 25 0 1 0 1854857237 248414208 51542 4294967295 134512640 135094434 3221224432 3221223136 134558999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 60648 51542 145 145 0 60503 0 [pid=15143] vsize: 242592 Current children cumulated CPU time (s) 397.76 Current children cumulated vsize (Kb) 244716 [startup+410.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59003 0 0 0 40526 249 0 0 25 0 1 0 1854857237 248438784 51558 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 60654 51558 145 145 0 60509 0 [pid=15143] vsize: 242616 Current children cumulated CPU time (s) 407.77 Current children cumulated vsize (Kb) 244740 [startup+420.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59015 0 0 0 41526 249 0 0 25 0 1 0 1854857237 248483840 51570 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 60665 51570 145 145 0 60520 0 [pid=15143] vsize: 242660 Current children cumulated CPU time (s) 417.77 Current children cumulated vsize (Kb) 244784 [startup+430.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59053 0 0 0 42525 249 0 0 25 0 1 0 1854857237 248635392 51608 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 60702 51608 145 145 0 60557 0 [pid=15143] vsize: 242808 Current children cumulated CPU time (s) 427.76 Current children cumulated vsize (Kb) 244932 [startup+440.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59065 0 0 0 43525 250 0 0 25 0 1 0 1854857237 248680448 51620 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 60713 51620 145 145 0 60568 0 [pid=15143] vsize: 242852 Current children cumulated CPU time (s) 437.77 Current children cumulated vsize (Kb) 244976 [startup+450.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59077 0 0 0 44525 250 0 0 25 0 1 0 1854857237 248725504 51632 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 60724 51632 145 145 0 60579 0 [pid=15143] vsize: 242896 Current children cumulated CPU time (s) 447.77 Current children cumulated vsize (Kb) 245020 [startup+460.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59089 0 0 0 45524 250 0 0 25 0 1 0 1854857237 248770560 51644 4294967295 134512640 135094434 3221224432 3221223112 134553433 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 60735 51644 145 145 0 60590 0 [pid=15143] vsize: 242940 Current children cumulated CPU time (s) 457.76 Current children cumulated vsize (Kb) 245064 [startup+470.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59101 0 0 0 46524 250 0 0 25 0 1 0 1854857237 248819712 51656 4294967295 134512640 135094434 3221224432 3221223092 134553528 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 60747 51656 145 145 0 60602 0 [pid=15143] vsize: 242988 Current children cumulated CPU time (s) 467.76 Current children cumulated vsize (Kb) 245112 [startup+480.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59112 0 0 0 47524 250 0 0 25 0 1 0 1854857237 248860672 51667 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 60757 51667 145 145 0 60612 0 [pid=15143] vsize: 243028 Current children cumulated CPU time (s) 477.76 Current children cumulated vsize (Kb) 245152 [startup+490.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59132 0 0 0 48524 251 0 0 25 0 1 0 1854857237 248938496 51687 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 60776 51687 145 145 0 60631 0 [pid=15143] vsize: 243104 Current children cumulated CPU time (s) 487.77 Current children cumulated vsize (Kb) 245228 [startup+500.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59141 0 0 0 49523 251 0 0 25 0 1 0 1854857237 248971264 51696 4294967295 134512640 135094434 3221224432 3221223092 134553466 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 60784 51696 145 145 0 60639 0 [pid=15143] vsize: 243136 Current children cumulated CPU time (s) 497.76 Current children cumulated vsize (Kb) 245260 [startup+510.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59148 0 0 0 50523 252 0 0 25 0 1 0 1854857237 248999936 51703 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 60791 51703 145 145 0 60646 0 [pid=15143] vsize: 243164 Current children cumulated CPU time (s) 507.77 Current children cumulated vsize (Kb) 245288 [startup+520.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59163 0 0 0 51524 252 0 0 25 0 1 0 1854857237 249057280 51718 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 60805 51718 145 145 0 60660 0 [pid=15143] vsize: 243220 Current children cumulated CPU time (s) 517.78 Current children cumulated vsize (Kb) 245344 [startup+530.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59179 0 0 0 52524 252 0 0 25 0 1 0 1854857237 249118720 51734 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 60820 51734 145 145 0 60675 0 [pid=15143] vsize: 243280 Current children cumulated CPU time (s) 527.78 Current children cumulated vsize (Kb) 245404 [startup+540.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59207 0 0 0 53523 252 0 0 25 0 1 0 1854857237 249229312 51762 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 60847 51762 145 145 0 60702 0 [pid=15143] vsize: 243388 Current children cumulated CPU time (s) 537.77 Current children cumulated vsize (Kb) 245512 [startup+550.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59229 0 0 0 54523 253 0 0 25 0 1 0 1854857237 249315328 51784 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 60868 51784 145 145 0 60723 0 [pid=15143] vsize: 243472 Current children cumulated CPU time (s) 547.78 Current children cumulated vsize (Kb) 245596 [startup+560.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59237 0 0 0 55523 253 0 0 25 0 1 0 1854857237 249348096 51792 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 60876 51792 145 145 0 60731 0 [pid=15143] vsize: 243504 Current children cumulated CPU time (s) 557.78 Current children cumulated vsize (Kb) 245628 [startup+570.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59245 0 0 0 56523 253 0 0 25 0 1 0 1854857237 249376768 51800 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 60883 51800 145 145 0 60738 0 [pid=15143] vsize: 243532 Current children cumulated CPU time (s) 567.78 Current children cumulated vsize (Kb) 245656 [startup+580.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59251 0 0 0 57523 253 0 0 25 0 1 0 1854857237 249401344 51806 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 60889 51806 145 145 0 60744 0 [pid=15143] vsize: 243556 Current children cumulated CPU time (s) 577.78 Current children cumulated vsize (Kb) 245680 [startup+590.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59268 0 0 0 58523 253 0 0 25 0 1 0 1854857237 249466880 51823 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 60905 51823 145 145 0 60760 0 [pid=15143] vsize: 243620 Current children cumulated CPU time (s) 587.78 Current children cumulated vsize (Kb) 245744 [startup+600.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59286 0 0 0 59523 253 0 0 25 0 1 0 1854857237 249540608 51841 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 60923 51841 145 145 0 60778 0 [pid=15143] vsize: 243692 Current children cumulated CPU time (s) 597.78 Current children cumulated vsize (Kb) 245816 [startup+610.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59390 0 0 0 60522 254 0 0 25 0 1 0 1854857237 250081280 51945 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61055 51945 145 145 0 60910 0 [pid=15143] vsize: 244220 Current children cumulated CPU time (s) 607.78 Current children cumulated vsize (Kb) 246344 [startup+620.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59412 0 0 0 61522 254 0 0 25 0 1 0 1854857237 250167296 51967 4294967295 134512640 135094434 3221224432 3221223088 134561463 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15143/statm): 61076 51967 145 145 0 60931 0 [pid=15143] vsize: 244304 Current children cumulated CPU time (s) 617.78 Current children cumulated vsize (Kb) 246428 [startup+630.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59439 0 0 0 62520 255 0 0 25 0 1 0 1854857237 250273792 51994 4294967295 134512640 135094434 3221224432 3221223120 134554750 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15143/statm): 61102 51994 145 145 0 60957 0 [pid=15143] vsize: 244408 Current children cumulated CPU time (s) 627.77 Current children cumulated vsize (Kb) 246532 [startup+640.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59450 0 0 0 63520 255 0 0 25 0 1 0 1854857237 250314752 52005 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61112 52005 145 145 0 60967 0 [pid=15143] vsize: 244448 Current children cumulated CPU time (s) 637.77 Current children cumulated vsize (Kb) 246572 [startup+650.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59460 0 0 0 64520 255 0 0 25 0 1 0 1854857237 250343424 52015 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61119 52015 145 145 0 60974 0 [pid=15143] vsize: 244476 Current children cumulated CPU time (s) 647.77 Current children cumulated vsize (Kb) 246600 [startup+660.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59478 0 0 0 65520 255 0 0 25 0 1 0 1854857237 250413056 52033 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61136 52033 145 145 0 60991 0 [pid=15143] vsize: 244544 Current children cumulated CPU time (s) 657.77 Current children cumulated vsize (Kb) 246668 [startup+670.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59543 0 0 0 66519 256 0 0 25 0 1 0 1854857237 250667008 52098 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61198 52098 145 145 0 61053 0 [pid=15143] vsize: 244792 Current children cumulated CPU time (s) 667.77 Current children cumulated vsize (Kb) 246916 [startup+680.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59553 0 0 0 67519 256 0 0 25 0 1 0 1854857237 250707968 52108 4294967295 134512640 135094434 3221224432 3221223044 134563110 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61208 52108 145 145 0 61063 0 [pid=15143] vsize: 244832 Current children cumulated CPU time (s) 677.77 Current children cumulated vsize (Kb) 246956 [startup+690.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59564 0 0 0 68519 256 0 0 25 0 1 0 1854857237 250748928 52119 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61218 52119 145 145 0 61073 0 [pid=15143] vsize: 244872 Current children cumulated CPU time (s) 687.77 Current children cumulated vsize (Kb) 246996 [startup+700.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59579 0 0 0 69519 256 0 0 25 0 1 0 1854857237 250806272 52134 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61232 52134 145 145 0 61087 0 [pid=15143] vsize: 244928 Current children cumulated CPU time (s) 697.77 Current children cumulated vsize (Kb) 247052 [startup+710.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59597 0 0 0 70519 256 0 0 25 0 1 0 1854857237 250875904 52152 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61249 52152 145 145 0 61104 0 [pid=15143] vsize: 244996 Current children cumulated CPU time (s) 707.77 Current children cumulated vsize (Kb) 247120 [startup+720.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59614 0 0 0 71518 257 0 0 25 0 1 0 1854857237 250941440 52169 4294967295 134512640 135094434 3221224432 3221223092 134553475 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61265 52169 145 145 0 61120 0 [pid=15143] vsize: 245060 Current children cumulated CPU time (s) 717.77 Current children cumulated vsize (Kb) 247184 [startup+730.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59631 0 0 0 72518 257 0 0 25 0 1 0 1854857237 251006976 52186 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61281 52186 145 145 0 61136 0 [pid=15143] vsize: 245124 Current children cumulated CPU time (s) 727.77 Current children cumulated vsize (Kb) 247248 [startup+740.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59646 0 0 0 73518 257 0 0 25 0 1 0 1854857237 251068416 52201 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61296 52201 145 145 0 61151 0 [pid=15143] vsize: 245184 Current children cumulated CPU time (s) 737.77 Current children cumulated vsize (Kb) 247308 [startup+750.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59659 0 0 0 74518 257 0 0 25 0 1 0 1854857237 251117568 52214 4294967295 134512640 135094434 3221224432 3221223072 134561797 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61308 52214 145 145 0 61163 0 [pid=15143] vsize: 245232 Current children cumulated CPU time (s) 747.77 Current children cumulated vsize (Kb) 247356 [startup+760.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59670 0 0 0 75518 257 0 0 25 0 1 0 1854857237 251158528 52225 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61318 52225 145 145 0 61173 0 [pid=15143] vsize: 245272 Current children cumulated CPU time (s) 757.77 Current children cumulated vsize (Kb) 247396 [startup+770.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59684 0 0 0 76518 257 0 0 25 0 1 0 1854857237 251207680 52239 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61330 52239 145 145 0 61185 0 [pid=15143] vsize: 245320 Current children cumulated CPU time (s) 767.77 Current children cumulated vsize (Kb) 247444 [startup+780.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59693 0 0 0 77519 257 0 0 25 0 1 0 1854857237 251240448 52248 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61338 52248 145 145 0 61193 0 [pid=15143] vsize: 245352 Current children cumulated CPU time (s) 777.78 Current children cumulated vsize (Kb) 247476 [startup+790.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59708 0 0 0 78519 257 0 0 25 0 1 0 1854857237 251273216 52263 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61346 52263 145 145 0 61201 0 [pid=15143] vsize: 245384 Current children cumulated CPU time (s) 787.78 Current children cumulated vsize (Kb) 247508 [startup+800.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59716 0 0 0 79518 258 0 0 25 0 1 0 1854857237 251301888 52271 4294967295 134512640 135094434 3221224432 3221223092 134553519 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61353 52271 145 145 0 61208 0 [pid=15143] vsize: 245412 Current children cumulated CPU time (s) 797.78 Current children cumulated vsize (Kb) 247536 [startup+810.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59723 0 0 0 80519 258 0 0 25 0 1 0 1854857237 251330560 52278 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61360 52278 145 145 0 61215 0 [pid=15143] vsize: 245440 Current children cumulated CPU time (s) 807.79 Current children cumulated vsize (Kb) 247564 [startup+820.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59730 0 0 0 81519 258 0 0 25 0 1 0 1854857237 251359232 52285 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61367 52285 145 145 0 61222 0 [pid=15143] vsize: 245468 Current children cumulated CPU time (s) 817.79 Current children cumulated vsize (Kb) 247592 [startup+830.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59745 0 0 0 82519 258 0 0 25 0 1 0 1854857237 251416576 52300 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61381 52300 145 145 0 61236 0 [pid=15143] vsize: 245524 Current children cumulated CPU time (s) 827.79 Current children cumulated vsize (Kb) 247648 [startup+840.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59760 0 0 0 83519 258 0 0 25 0 1 0 1854857237 251473920 52315 4294967295 134512640 135094434 3221224432 3221223044 134563080 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61395 52315 145 145 0 61250 0 [pid=15143] vsize: 245580 Current children cumulated CPU time (s) 837.79 Current children cumulated vsize (Kb) 247704 [startup+850.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59770 0 0 0 84519 258 0 0 25 0 1 0 1854857237 251510784 52325 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61404 52325 145 145 0 61259 0 [pid=15143] vsize: 245616 Current children cumulated CPU time (s) 847.79 Current children cumulated vsize (Kb) 247740 [startup+860.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59777 0 0 0 85519 258 0 0 25 0 1 0 1854857237 251539456 52332 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61411 52332 145 145 0 61266 0 [pid=15143] vsize: 245644 Current children cumulated CPU time (s) 857.79 Current children cumulated vsize (Kb) 247768 [startup+870.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59787 0 0 0 86519 258 0 0 25 0 1 0 1854857237 251576320 52342 4294967295 134512640 135094434 3221224432 3221223072 134562139 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61420 52342 145 145 0 61275 0 [pid=15143] vsize: 245680 Current children cumulated CPU time (s) 867.79 Current children cumulated vsize (Kb) 247804 [startup+880.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59806 0 0 0 87518 258 0 0 25 0 1 0 1854857237 251650048 52361 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61438 52361 145 145 0 61293 0 [pid=15143] vsize: 245752 Current children cumulated CPU time (s) 877.78 Current children cumulated vsize (Kb) 247876 [startup+890.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59815 0 0 0 88518 259 0 0 25 0 1 0 1854857237 251686912 52370 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61447 52370 145 145 0 61302 0 [pid=15143] vsize: 245788 Current children cumulated CPU time (s) 887.79 Current children cumulated vsize (Kb) 247912 [startup+900.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59823 0 0 0 89518 259 0 0 25 0 1 0 1854857237 251715584 52378 4294967295 134512640 135094434 3221224432 3221223072 134558264 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61454 52378 145 145 0 61309 0 [pid=15143] vsize: 245816 Current children cumulated CPU time (s) 897.79 Current children cumulated vsize (Kb) 247940 [startup+910.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59835 0 0 0 90518 259 0 0 25 0 1 0 1854857237 251760640 52390 4294967295 134512640 135094434 3221224432 3221223044 134563024 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61465 52390 145 145 0 61320 0 [pid=15143] vsize: 245860 Current children cumulated CPU time (s) 907.79 Current children cumulated vsize (Kb) 247984 [startup+920.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59847 0 0 0 91517 260 0 0 25 0 1 0 1854857237 251809792 52402 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61477 52402 145 145 0 61332 0 [pid=15143] vsize: 245908 Current children cumulated CPU time (s) 917.79 Current children cumulated vsize (Kb) 248032 [startup+930.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59857 0 0 0 92517 261 0 0 25 0 1 0 1854857237 251846656 52412 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61486 52412 145 145 0 61341 0 [pid=15143] vsize: 245944 Current children cumulated CPU time (s) 927.8 Current children cumulated vsize (Kb) 248068 [startup+940.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59868 0 0 0 93516 261 0 0 25 0 1 0 1854857237 251887616 52423 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61496 52423 145 145 0 61351 0 [pid=15143] vsize: 245984 Current children cumulated CPU time (s) 937.79 Current children cumulated vsize (Kb) 248108 [startup+950.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59878 0 0 0 94516 262 0 0 25 0 1 0 1854857237 251928576 52433 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61506 52433 145 145 0 61361 0 [pid=15143] vsize: 246024 Current children cumulated CPU time (s) 947.8 Current children cumulated vsize (Kb) 248148 [startup+960.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59888 0 0 0 95516 262 0 0 25 0 1 0 1854857237 251965440 52443 4294967295 134512640 135094434 3221224432 3221223120 134554851 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61515 52443 145 145 0 61370 0 [pid=15143] vsize: 246060 Current children cumulated CPU time (s) 957.8 Current children cumulated vsize (Kb) 248184 [startup+970.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59908 0 0 0 96515 262 0 0 25 0 1 0 1854857237 252043264 52463 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61534 52463 145 145 0 61389 0 [pid=15143] vsize: 246136 Current children cumulated CPU time (s) 967.79 Current children cumulated vsize (Kb) 248260 [startup+980.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59919 0 0 0 97515 263 0 0 25 0 1 0 1854857237 252084224 52474 4294967295 134512640 135094434 3221224432 3221223044 134563089 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61544 52474 145 145 0 61399 0 [pid=15143] vsize: 246176 Current children cumulated CPU time (s) 977.8 Current children cumulated vsize (Kb) 248300 [startup+990.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59929 0 0 0 98515 263 0 0 25 0 1 0 1854857237 252121088 52484 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61553 52484 145 145 0 61408 0 [pid=15143] vsize: 246212 Current children cumulated CPU time (s) 987.8 Current children cumulated vsize (Kb) 248336 [startup+1000.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59936 0 0 0 99515 263 0 0 25 0 1 0 1854857237 252149760 52491 4294967295 134512640 135094434 3221224432 3221223104 134554872 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61560 52491 145 145 0 61415 0 [pid=15143] vsize: 246240 Current children cumulated CPU time (s) 997.8 Current children cumulated vsize (Kb) 248364 [startup+1010.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59940 0 0 0 100515 263 0 0 25 0 1 0 1854857237 252166144 52495 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61564 52495 145 145 0 61419 0 [pid=15143] vsize: 246256 Current children cumulated CPU time (s) 1007.8 Current children cumulated vsize (Kb) 248380 [startup+1020.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59943 0 0 0 101515 263 0 0 25 0 1 0 1854857237 252178432 52498 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61567 52498 145 145 0 61422 0 [pid=15143] vsize: 246268 Current children cumulated CPU time (s) 1017.8 Current children cumulated vsize (Kb) 248392 [startup+1030.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59952 0 0 0 102515 264 0 0 25 0 1 0 1854857237 252452864 52507 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61634 52507 145 145 0 61489 0 [pid=15143] vsize: 246536 Current children cumulated CPU time (s) 1027.81 Current children cumulated vsize (Kb) 248660 [startup+1040.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59961 0 0 0 103515 264 0 0 25 0 1 0 1854857237 252489728 52516 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61643 52516 145 145 0 61498 0 [pid=15143] vsize: 246572 Current children cumulated CPU time (s) 1037.81 Current children cumulated vsize (Kb) 248696 [startup+1050.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59976 0 0 0 104515 264 0 0 25 0 1 0 1854857237 252547072 52531 4294967295 134512640 135094434 3221224432 3221223044 134563130 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61657 52531 145 145 0 61512 0 [pid=15143] vsize: 246628 Current children cumulated CPU time (s) 1047.81 Current children cumulated vsize (Kb) 248752 [startup+1060.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 59989 0 0 0 105515 264 0 0 25 0 1 0 1854857237 252596224 52544 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61669 52544 145 145 0 61524 0 [pid=15143] vsize: 246676 Current children cumulated CPU time (s) 1057.81 Current children cumulated vsize (Kb) 248800 [startup+1070.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 60016 0 0 0 106515 264 0 0 25 0 1 0 1854857237 252702720 52571 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61695 52571 145 145 0 61550 0 [pid=15143] vsize: 246780 Current children cumulated CPU time (s) 1067.81 Current children cumulated vsize (Kb) 248904 [startup+1080.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 60023 0 0 0 107515 264 0 0 25 0 1 0 1854857237 252731392 52578 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61702 52578 145 145 0 61557 0 [pid=15143] vsize: 246808 Current children cumulated CPU time (s) 1077.81 Current children cumulated vsize (Kb) 248932 [startup+1090.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 60032 0 0 0 108515 264 0 0 25 0 1 0 1854857237 252764160 52587 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61710 52587 145 145 0 61565 0 [pid=15143] vsize: 246840 Current children cumulated CPU time (s) 1087.81 Current children cumulated vsize (Kb) 248964 [startup+1100.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 60046 0 0 0 109515 265 0 0 25 0 1 0 1854857237 252817408 52601 4294967295 134512640 135094434 3221224432 3221223136 134559010 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61723 52601 145 145 0 61578 0 [pid=15143] vsize: 246892 Current children cumulated CPU time (s) 1097.82 Current children cumulated vsize (Kb) 249016 [startup+1110.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 60056 0 0 0 110515 265 0 0 25 0 1 0 1854857237 252858368 52611 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61733 52611 145 145 0 61588 0 [pid=15143] vsize: 246932 Current children cumulated CPU time (s) 1107.82 Current children cumulated vsize (Kb) 249056 [startup+1120.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 60143 0 0 0 111515 265 0 0 25 0 1 0 1854857237 252891136 52698 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61741 52698 145 145 0 61596 0 [pid=15143] vsize: 246964 Current children cumulated CPU time (s) 1117.82 Current children cumulated vsize (Kb) 249088 [startup+1130.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 60162 0 0 0 112515 265 0 0 25 0 1 0 1854857237 252964864 52717 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61759 52717 145 145 0 61614 0 [pid=15143] vsize: 247036 Current children cumulated CPU time (s) 1127.82 Current children cumulated vsize (Kb) 249160 [startup+1140.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 60175 0 0 0 113515 265 0 0 25 0 1 0 1854857237 253014016 52730 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61771 52730 145 145 0 61626 0 [pid=15143] vsize: 247084 Current children cumulated CPU time (s) 1137.82 Current children cumulated vsize (Kb) 249208 [startup+1150.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 60186 0 0 0 114515 266 0 0 25 0 1 0 1854857237 253059072 52741 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61782 52741 145 145 0 61637 0 [pid=15143] vsize: 247128 Current children cumulated CPU time (s) 1147.83 Current children cumulated vsize (Kb) 249252 [startup+1160.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 60201 0 0 0 115515 266 0 0 25 0 1 0 1854857237 253116416 52756 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61796 52756 145 145 0 61651 0 [pid=15143] vsize: 247184 Current children cumulated CPU time (s) 1157.83 Current children cumulated vsize (Kb) 249308 [startup+1170.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 60223 0 0 0 116515 266 0 0 25 0 1 0 1854857237 253202432 52778 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61817 52778 145 145 0 61672 0 [pid=15143] vsize: 247268 Current children cumulated CPU time (s) 1167.83 Current children cumulated vsize (Kb) 249392 [startup+1180.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 60257 0 0 0 117514 266 0 0 25 0 1 0 1854857237 253333504 52812 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61849 52812 145 145 0 61704 0 [pid=15143] vsize: 247396 Current children cumulated CPU time (s) 1177.82 Current children cumulated vsize (Kb) 249520 [startup+1190.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 60293 0 0 0 118514 267 0 0 25 0 1 0 1854857237 253472768 52848 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61883 52848 145 145 0 61738 0 [pid=15143] vsize: 247532 Current children cumulated CPU time (s) 1187.83 Current children cumulated vsize (Kb) 249656 [startup+1200.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 60344 0 0 0 119513 267 0 0 25 0 1 0 1854857237 253673472 52899 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15143/statm): 61932 52899 145 145 0 61787 0 [pid=15143] vsize: 247728 Current children cumulated CPU time (s) 1197.82 Current children cumulated vsize (Kb) 249852 [startup+1210.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 60520 0 0 0 120510 268 0 0 25 0 1 0 1854857237 254373888 53075 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15143/statm): 62103 53075 145 145 0 61958 0 [pid=15143] vsize: 248412 Current children cumulated CPU time (s) 1207.8 Current children cumulated vsize (Kb) 250536 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15143 Raw data (/proc/15139/stat): 15139 (minisat+_script) S 15138 15139 21452 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1854857232 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/15139/statm): 531 226 485 147 0 384 0 [pid=15139] vsize: 2124 Raw data (/proc/15143/stat): 15143 (minisat+_64-bit) R 15139 15139 21452 0 -1 0 60520 0 0 0 120510 268 0 0 25 0 1 0 1854857237 254373888 53075 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15143/statm): 62103 53075 145 145 0 61958 0 [pid=15143] vsize: 248412 Current children cumulated CPU time (s) 1207.8 Current children cumulated vsize (Kb) 250536 Sending SIGTERM to -15139 Sleeping 2 seconds One traced child (pid=15139) ended because it received signal 15 (SIGTERM) One traced child (pid=15143) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.2 CPU time (s): 1207.9 CPU user time (s): 1205.11 CPU system time (s): 2.79157 CPU usage (%): 99.8098 Max. virtual memory (cumulated for all children) (Kb): 250536
ERROR: no interpretation found !