| Name | mps-v2-13-7/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-neos16.opb |
| MD5SUM | 44281820d2b00a47b643433ffa4e2d73 |
| Bench Category | optimization, small integers (OPTSMALLINT) |
| Has Objective Function | YES |
| Satisfiable | YES |
| (Un)Satisfiability was proved | YES |
| Best value of the objective function | 117 |
| Optimality of the best value was proved | NO |
| Number of terms in the objective function | 8 |
| Biggest coefficient in the objective function | 128 |
| Number of bits for the biggest coefficient in the objective function | 8 |
| Sum of the numbers in the objective function | 255 |
| Number of bits of the sum of numbers in the objective function | 8 |
| Biggest number in a constraint | 138 |
| Number of bits of the biggest number in a constraint | 8 |
| Biggest sum of numbers in a constraint | 535 |
| Number of bits of the biggest sum of numbers | 10 |
| Best result obtained on this benchmark | SAT |
| Best CPU time to get the best result obtained on this benchmark | 1195.48 |
| Number of variables | 464 |
| Total number of constraints | 1395 |
| Number of constraints which are clauses | 336 |
| Number of constraints which are cardinality constraints (but not clauses) | 336 |
| Number of constraints which are nor clauses,nor cardinality constraints | 723 |
| Minimum length of a constraint | 1 |
| Maximum length of a constraint | 128 |
LAUNCH ON wulflinc5 THE 2005-09-20 05:16:15 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3451 boxname=wulflinc5 idbench=1107 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 44281820d2b00a47b643433ffa4e2d73 /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-neos16.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-neos16.opb IDLAUNCH: 3451 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 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: 907108 kB Buffers: 13940 kB Cached: 89288 kB SwapCached: 744 kB Active: 25108 kB Inactive: 80780 kB HighTotal: 131008 kB HighFree: 37520 kB LowTotal: 903652 kB LowFree: 869588 kB SwapTotal: 2097136 kB SwapFree: 2095884 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5756 kB Slab: 15996 kB Committed_AS: 64300 kB PageTables: 332 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-20 05:36:15 (client local time) WITH STATUS 10 IN 1200 SECONDS stats: 3451 7 1200 10
c Parsing PB file... c Converting 1069 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ########## c -- Clauses(.)/Splits(s): ........................................................................................................................................................................................................................................................................................................................................................................................ c ---[1028]---> BDD-cost: 7 c ---[1026]---> Sorter-cost: 252 Base: 2 2 c ---[1024]---> Sorter-cost: 252 Base: 2 2 c ---[1022]---> Sorter-cost: 251 Base: 2 2 c ---[1020]---> Sorter-cost: 252 Base: 2 2 c ---[1018]---> Sorter-cost: 251 Base: 2 2 c ---[1016]---> Sorter-cost: 252 Base: 2 2 c ---[1014]---> Sorter-cost: 252 Base: 2 2 c ---[1012]---> Sorter-cost: 252 Base: 2 2 c ---[1010]---> Sorter-cost: 251 Base: 2 2 c ---[1009]---> BDD-cost: 11 c ---[1008]---> BDD-cost: 11 c ---[1007]---> BDD-cost: 11 c ---[1006]---> BDD-cost: 11 c ---[1005]---> BDD-cost: 11 c ---[1004]---> BDD-cost: 11 c ---[1003]---> BDD-cost: 11 c ---[1002]---> BDD-cost: 11 c ---[1001]---> BDD-cost: 11 c ---[1000]---> BDD-cost: 11 c ---[ 999]---> BDD-cost: 11 c ---[ 998]---> BDD-cost: 11 c ---[ 997]---> BDD-cost: 11 c ---[ 996]---> BDD-cost: 11 c ---[ 995]---> BDD-cost: 11 c ---[ 994]---> BDD-cost: 11 c ---[ 993]---> BDD-cost: 11 c ---[ 992]---> BDD-cost: 11 c ---[ 991]---> BDD-cost: 11 c ---[ 990]---> BDD-cost: 11 c ---[ 989]---> BDD-cost: 11 c ---[ 988]---> BDD-cost: 11 c ---[ 987]---> BDD-cost: 11 c ---[ 986]---> BDD-cost: 11 c ---[ 985]---> BDD-cost: 11 c ---[ 984]---> BDD-cost: 11 c ---[ 983]---> BDD-cost: 11 c ---[ 982]---> BDD-cost: 11 c ---[ 981]---> BDD-cost: 11 c ---[ 980]---> BDD-cost: 11 c ---[ 979]---> BDD-cost: 11 c ---[ 978]---> BDD-cost: 11 c ---[ 977]---> BDD-cost: 11 c ---[ 976]---> BDD-cost: 11 c ---[ 975]---> BDD-cost: 11 c ---[ 974]---> BDD-cost: 11 c ---[ 973]---> BDD-cost: 11 c ---[ 972]---> BDD-cost: 11 c ---[ 971]---> BDD-cost: 11 c ---[ 970]---> BDD-cost: 11 c ---[ 969]---> BDD-cost: 11 c ---[ 968]---> BDD-cost: 11 c ---[ 967]---> BDD-cost: 11 c ---[ 966]---> BDD-cost: 11 c ---[ 965]---> BDD-cost: 11 c ---[ 964]---> BDD-cost: 11 c ---[ 963]---> BDD-cost: 11 c ---[ 962]---> BDD-cost: 11 c ---[ 961]---> BDD-cost: 11 c ---[ 960]---> BDD-cost: 11 c ---[ 959]---> BDD-cost: 11 c ---[ 958]---> BDD-cost: 11 c ---[ 957]---> BDD-cost: 11 c ---[ 956]---> BDD-cost: 11 c ---[ 955]---> BDD-cost: 11 c ---[ 954]---> BDD-cost: 11 c ---[ 953]---> BDD-cost: 11 c ---[ 952]---> BDD-cost: 11 c ---[ 951]---> BDD-cost: 11 c ---[ 950]---> BDD-cost: 11 c ---[ 949]---> BDD-cost: 11 c ---[ 948]---> BDD-cost: 11 c ---[ 947]---> BDD-cost: 11 c ---[ 946]---> BDD-cost: 11 c ---[ 945]---> BDD-cost: 11 c ---[ 944]---> BDD-cost: 11 c ---[ 943]---> BDD-cost: 11 c ---[ 942]---> BDD-cost: 11 c ---[ 941]---> BDD-cost: 11 c ---[ 940]---> BDD-cost: 11 c ---[ 939]---> BDD-cost: 11 c ---[ 938]---> BDD-cost: 11 c ---[ 937]---> BDD-cost: 11 c ---[ 936]---> BDD-cost: 11 c ---[ 935]---> BDD-cost: 11 c ---[ 934]---> BDD-cost: 11 c ---[ 933]---> BDD-cost: 11 c ---[ 932]---> BDD-cost: 11 c ---[ 931]---> BDD-cost: 11 c ---[ 930]---> BDD-cost: 11 c ---[ 929]---> BDD-cost: 11 c ---[ 928]---> BDD-cost: 11 c ---[ 927]---> BDD-cost: 11 c ---[ 926]---> BDD-cost: 11 c ---[ 925]---> BDD-cost: 6 c ---[ 924]---> BDD-cost: 6 c ---[ 923]---> BDD-cost: 6 c ---[ 922]---> BDD-cost: 6 c ---[ 921]---> BDD-cost: 6 c ---[ 920]---> BDD-cost: 6 c ---[ 919]---> BDD-cost: 6 c ---[ 918]---> BDD-cost: 6 c ---[ 917]---> BDD-cost: 6 c ---[ 916]---> BDD-cost: 6 c ---[ 915]---> BDD-cost: 6 c ---[ 914]---> BDD-cost: 6 c ---[ 913]---> BDD-cost: 6 c ---[ 912]---> BDD-cost: 6 c ---[ 911]---> BDD-cost: 6 c ---[ 910]---> BDD-cost: 6 c ---[ 909]---> BDD-cost: 6 c ---[ 908]---> BDD-cost: 6 c ---[ 907]---> BDD-cost: 6 c ---[ 906]---> BDD-cost: 6 c ---[ 905]---> BDD-cost: 6 c ---[ 904]---> BDD-cost: 6 c ---[ 903]---> BDD-cost: 6 c ---[ 902]---> BDD-cost: 6 c ---[ 901]---> BDD-cost: 6 c ---[ 900]---> BDD-cost: 6 c ---[ 899]---> BDD-cost: 6 c ---[ 898]---> BDD-cost: 6 c ---[ 897]---> BDD-cost: 6 c ---[ 896]---> BDD-cost: 6 c ---[ 895]---> BDD-cost: 6 c ---[ 894]---> BDD-cost: 6 c ---[ 893]---> BDD-cost: 6 c ---[ 892]---> BDD-cost: 6 c ---[ 891]---> BDD-cost: 6 c ---[ 890]---> BDD-cost: 6 c ---[ 889]---> BDD-cost: 6 c ---[ 888]---> BDD-cost: 6 c ---[ 887]---> BDD-cost: 6 c ---[ 886]---> BDD-cost: 6 c ---[ 885]---> BDD-cost: 6 c ---[ 884]---> BDD-cost: 6 c ---[ 883]---> BDD-cost: 6 c ---[ 882]---> BDD-cost: 6 c ---[ 881]---> BDD-cost: 6 c ---[ 880]---> BDD-cost: 6 c ---[ 879]---> BDD-cost: 6 c ---[ 878]---> BDD-cost: 6 c ---[ 877]---> BDD-cost: 6 c ---[ 876]---> BDD-cost: 6 c ---[ 875]---> BDD-cost: 6 c ---[ 874]---> BDD-cost: 6 c ---[ 873]---> BDD-cost: 6 c ---[ 872]---> BDD-cost: 6 c ---[ 871]---> BDD-cost: 6 c ---[ 870]---> BDD-cost: 6 c ---[ 869]---> BDD-cost: 6 c ---[ 868]---> BDD-cost: 6 c ---[ 867]---> BDD-cost: 6 c ---[ 866]---> BDD-cost: 6 c ---[ 865]---> BDD-cost: 6 c ---[ 864]---> BDD-cost: 6 c ---[ 863]---> BDD-cost: 6 c ---[ 862]---> BDD-cost: 6 c ---[ 861]---> BDD-cost: 6 c ---[ 860]---> BDD-cost: 6 c ---[ 859]---> BDD-cost: 6 c ---[ 858]---> BDD-cost: 6 c ---[ 857]---> BDD-cost: 6 c ---[ 856]---> BDD-cost: 6 c ---[ 855]---> BDD-cost: 6 c ---[ 854]---> BDD-cost: 6 c ---[ 853]---> BDD-cost: 6 c ---[ 852]---> BDD-cost: 6 c ---[ 851]---> BDD-cost: 6 c ---[ 850]---> BDD-cost: 6 c ---[ 849]---> BDD-cost: 6 c ---[ 848]---> BDD-cost: 6 c ---[ 847]---> BDD-cost: 6 c ---[ 846]---> BDD-cost: 6 c ---[ 845]---> BDD-cost: 6 c ---[ 844]---> BDD-cost: 6 c ---[ 843]---> BDD-cost: 6 c ---[ 842]---> BDD-cost: 6 c ---[ 841]---> BDD-cost: 6 c ---[ 840]---> BDD-cost: 6 c ---[ 839]---> BDD-cost: 6 c ---[ 838]---> BDD-cost: 6 c ---[ 837]---> BDD-cost: 6 c ---[ 836]---> BDD-cost: 6 c ---[ 835]---> BDD-cost: 6 c ---[ 834]---> BDD-cost: 6 c ---[ 833]---> BDD-cost: 6 c ---[ 832]---> BDD-cost: 6 c ---[ 831]---> BDD-cost: 6 c ---[ 830]---> BDD-cost: 6 c ---[ 829]---> BDD-cost: 6 c ---[ 828]---> BDD-cost: 6 c ---[ 827]---> BDD-cost: 6 c ---[ 826]---> BDD-cost: 6 c ---[ 825]---> BDD-cost: 6 c ---[ 824]---> BDD-cost: 6 c ---[ 823]---> BDD-cost: 6 c ---[ 822]---> BDD-cost: 6 c ---[ 821]---> BDD-cost: 6 c ---[ 820]---> BDD-cost: 6 c ---[ 819]---> BDD-cost: 6 c ---[ 818]---> BDD-cost: 6 c ---[ 817]---> BDD-cost: 6 c ---[ 816]---> BDD-cost: 6 c ---[ 815]---> BDD-cost: 6 c ---[ 814]---> BDD-cost: 6 c ---[ 813]---> BDD-cost: 6 c ---[ 812]---> BDD-cost: 6 c ---[ 811]---> BDD-cost: 6 c ---[ 810]---> BDD-cost: 6 c ---[ 809]---> BDD-cost: 6 c ---[ 808]---> BDD-cost: 6 c ---[ 807]---> BDD-cost: 6 c ---[ 806]---> BDD-cost: 6 c ---[ 805]---> BDD-cost: 6 c ---[ 804]---> BDD-cost: 6 c ---[ 803]---> BDD-cost: 6 c ---[ 802]---> BDD-cost: 6 c ---[ 801]---> BDD-cost: 6 c ---[ 800]---> BDD-cost: 6 c ---[ 799]---> BDD-cost: 6 c ---[ 798]---> BDD-cost: 6 c ---[ 797]---> BDD-cost: 6 c ---[ 796]---> BDD-cost: 6 c ---[ 795]---> BDD-cost: 6 c ---[ 794]---> BDD-cost: 6 c ---[ 793]---> BDD-cost: 6 c ---[ 792]---> BDD-cost: 6 c ---[ 791]---> BDD-cost: 6 c ---[ 790]---> BDD-cost: 6 c ---[ 789]---> BDD-cost: 6 c ---[ 788]---> BDD-cost: 6 c ---[ 787]---> BDD-cost: 6 c ---[ 786]---> BDD-cost: 6 c ---[ 785]---> BDD-cost: 6 c ---[ 784]---> BDD-cost: 6 c ---[ 783]---> BDD-cost: 6 c ---[ 782]---> BDD-cost: 6 c ---[ 781]---> BDD-cost: 6 c ---[ 780]---> BDD-cost: 6 c ---[ 779]---> BDD-cost: 6 c ---[ 778]---> BDD-cost: 6 c ---[ 777]---> BDD-cost: 6 c ---[ 776]---> BDD-cost: 6 c ---[ 775]---> BDD-cost: 6 c ---[ 774]---> BDD-cost: 6 c ---[ 773]---> BDD-cost: 6 c ---[ 772]---> BDD-cost: 6 c ---[ 771]---> BDD-cost: 6 c ---[ 770]---> BDD-cost: 6 c ---[ 769]---> BDD-cost: 6 c ---[ 768]---> BDD-cost: 6 c ---[ 767]---> BDD-cost: 6 c ---[ 766]---> BDD-cost: 6 c ---[ 765]---> BDD-cost: 6 c ---[ 764]---> BDD-cost: 6 c ---[ 763]---> BDD-cost: 6 c ---[ 762]---> BDD-cost: 6 c ---[ 761]---> BDD-cost: 6 c ---[ 760]---> BDD-cost: 6 c ---[ 759]---> BDD-cost: 6 c ---[ 758]---> BDD-cost: 6 c ---[ 757]---> BDD-cost: 1 c ---[ 756]---> BDD-cost: 1 c ---[ 755]---> BDD-cost: 1 c ---[ 754]---> BDD-cost: 1 c ---[ 753]---> BDD-cost: 1 c ---[ 752]---> BDD-cost: 1 c ---[ 751]---> BDD-cost: 1 c ---[ 750]---> BDD-cost: 1 c ---[ 749]---> BDD-cost: 1 c ---[ 748]---> BDD-cost: 1 c ---[ 747]---> BDD-cost: 1 c ---[ 746]---> BDD-cost: 1 c ---[ 745]---> BDD-cost: 1 c ---[ 744]---> BDD-cost: 1 c ---[ 743]---> BDD-cost: 1 c ---[ 742]---> BDD-cost: 1 c ---[ 741]---> BDD-cost: 1 c ---[ 740]---> BDD-cost: 1 c ---[ 739]---> BDD-cost: 1 c ---[ 738]---> BDD-cost: 1 c ---[ 737]---> BDD-cost: 1 c ---[ 736]---> BDD-cost: 1 c ---[ 735]---> BDD-cost: 1 c ---[ 734]---> BDD-cost: 1 c ---[ 733]---> BDD-cost: 1 c ---[ 732]---> BDD-cost: 1 c ---[ 731]---> BDD-cost: 1 c ---[ 730]---> BDD-cost: 1 c ---[ 729]---> BDD-cost: 1 c ---[ 728]---> BDD-cost: 1 c ---[ 727]---> BDD-cost: 1 c ---[ 726]---> BDD-cost: 1 c ---[ 725]---> BDD-cost: 1 c ---[ 724]---> BDD-cost: 1 c ---[ 723]---> BDD-cost: 1 c ---[ 722]---> BDD-cost: 1 c ---[ 721]---> BDD-cost: 1 c ---[ 720]---> BDD-cost: 1 c ---[ 719]---> BDD-cost: 1 c ---[ 718]---> BDD-cost: 1 c ---[ 717]---> BDD-cost: 1 c ---[ 716]---> BDD-cost: 1 c ---[ 715]---> BDD-cost: 1 c ---[ 714]---> BDD-cost: 1 c ---[ 713]---> BDD-cost: 1 c ---[ 712]---> BDD-cost: 1 c ---[ 711]---> BDD-cost: 1 c ---[ 710]---> BDD-cost: 1 c ---[ 709]---> BDD-cost: 1 c ---[ 708]---> BDD-cost: 1 c ---[ 707]---> BDD-cost: 1 c ---[ 706]---> BDD-cost: 1 c ---[ 705]---> BDD-cost: 1 c ---[ 704]---> BDD-cost: 1 c ---[ 703]---> BDD-cost: 1 c ---[ 702]---> BDD-cost: 1 c ---[ 701]---> BDD-cost: 1 c ---[ 700]---> BDD-cost: 1 c ---[ 699]---> BDD-cost: 1 c ---[ 698]---> BDD-cost: 1 c ---[ 697]---> BDD-cost: 1 c ---[ 696]---> BDD-cost: 1 c ---[ 695]---> BDD-cost: 1 c ---[ 694]---> BDD-cost: 1 c ---[ 693]---> BDD-cost: 1 c ---[ 692]---> BDD-cost: 1 c ---[ 691]---> BDD-cost: 1 c ---[ 690]---> BDD-cost: 1 c ---[ 689]---> BDD-cost: 1 c ---[ 688]---> BDD-cost: 1 c ---[ 687]---> BDD-cost: 1 c ---[ 686]---> BDD-cost: 1 c ---[ 685]---> BDD-cost: 1 c ---[ 684]---> BDD-cost: 1 c ---[ 683]---> BDD-cost: 1 c ---[ 682]---> BDD-cost: 1 c ---[ 681]---> BDD-cost: 1 c ---[ 680]---> BDD-cost: 1 c ---[ 679]---> BDD-cost: 1 c ---[ 678]---> BDD-cost: 1 c ---[ 677]---> BDD-cost: 1 c ---[ 676]---> BDD-cost: 1 c ---[ 675]---> BDD-cost: 1 c ---[ 674]---> BDD-cost: 1 c ---[ 505]---> BDD-cost: 11 c ---[ 504]---> BDD-cost: 11 c ---[ 503]---> BDD-cost: 11 c ---[ 502]---> BDD-cost: 11 c ---[ 501]---> BDD-cost: 11 c ---[ 500]---> BDD-cost: 11 c ---[ 499]---> BDD-cost: 11 c ---[ 498]---> BDD-cost: 11 c ---[ 497]---> BDD-cost: 11 c ---[ 496]---> BDD-cost: 11 c ---[ 495]---> BDD-cost: 11 c ---[ 494]---> BDD-cost: 11 c ---[ 493]---> BDD-cost: 11 c ---[ 492]---> BDD-cost: 11 c ---[ 491]---> BDD-cost: 11 c ---[ 490]---> BDD-cost: 11 c ---[ 489]---> BDD-cost: 11 c ---[ 488]---> BDD-cost: 11 c ---[ 487]---> BDD-cost: 11 c ---[ 486]---> BDD-cost: 11 c ---[ 485]---> BDD-cost: 11 c ---[ 484]---> BDD-cost: 11 c ---[ 483]---> BDD-cost: 11 c ---[ 482]---> BDD-cost: 11 c ---[ 481]---> BDD-cost: 11 c ---[ 480]---> BDD-cost: 11 c ---[ 479]---> BDD-cost: 11 c ---[ 478]---> BDD-cost: 11 c ---[ 477]---> BDD-cost: 11 c ---[ 476]---> BDD-cost: 11 c ---[ 475]---> BDD-cost: 11 c ---[ 474]---> BDD-cost: 11 c ---[ 473]---> BDD-cost: 11 c ---[ 472]---> BDD-cost: 11 c ---[ 471]---> BDD-cost: 11 c ---[ 470]---> BDD-cost: 11 c ---[ 469]---> BDD-cost: 11 c ---[ 468]---> BDD-cost: 11 c ---[ 467]---> BDD-cost: 11 c ---[ 466]---> BDD-cost: 11 c ---[ 465]---> BDD-cost: 11 c ---[ 464]---> BDD-cost: 11 c ---[ 463]---> BDD-cost: 11 c ---[ 462]---> BDD-cost: 11 c ---[ 461]---> BDD-cost: 11 c ---[ 460]---> BDD-cost: 11 c ---[ 459]---> BDD-cost: 11 c ---[ 458]---> BDD-cost: 11 c ---[ 457]---> BDD-cost: 11 c ---[ 456]---> BDD-cost: 11 c ---[ 455]---> BDD-cost: 11 c ---[ 454]---> BDD-cost: 11 c ---[ 453]---> BDD-cost: 11 c ---[ 452]---> BDD-cost: 11 c ---[ 451]---> BDD-cost: 11 c ---[ 450]---> BDD-cost: 11 c ---[ 449]---> BDD-cost: 11 c ---[ 448]---> BDD-cost: 11 c ---[ 447]---> BDD-cost: 11 c ---[ 446]---> BDD-cost: 11 c ---[ 445]---> BDD-cost: 11 c ---[ 444]---> BDD-cost: 11 c ---[ 443]---> BDD-cost: 11 c ---[ 442]---> BDD-cost: 11 c ---[ 441]---> BDD-cost: 11 c ---[ 440]---> BDD-cost: 11 c ---[ 439]---> BDD-cost: 11 c ---[ 438]---> BDD-cost: 11 c ---[ 437]---> BDD-cost: 11 c ---[ 436]---> BDD-cost: 11 c ---[ 435]---> BDD-cost: 11 c ---[ 434]---> BDD-cost: 11 c ---[ 433]---> BDD-cost: 11 c ---[ 432]---> BDD-cost: 11 c ---[ 431]---> BDD-cost: 11 c ---[ 430]---> BDD-cost: 11 c ---[ 429]---> BDD-cost: 11 c ---[ 428]---> BDD-cost: 11 c ---[ 427]---> BDD-cost: 11 c ---[ 426]---> BDD-cost: 11 c ---[ 425]---> BDD-cost: 11 c ---[ 424]---> BDD-cost: 11 c ---[ 423]---> BDD-cost: 11 c ---[ 422]---> BDD-cost: 11 c ---[ 421]---> BDD-cost: 6 c ---[ 420]---> BDD-cost: 6 c ---[ 419]---> BDD-cost: 6 c ---[ 418]---> BDD-cost: 6 c ---[ 417]---> BDD-cost: 6 c ---[ 416]---> BDD-cost: 6 c ---[ 415]---> BDD-cost: 6 c ---[ 414]---> BDD-cost: 6 c ---[ 413]---> BDD-cost: 6 c ---[ 412]---> BDD-cost: 6 c ---[ 411]---> BDD-cost: 6 c ---[ 410]---> BDD-cost: 6 c ---[ 409]---> BDD-cost: 6 c ---[ 408]---> BDD-cost: 6 c ---[ 407]---> BDD-cost: 6 c ---[ 406]---> BDD-cost: 6 c ---[ 405]---> BDD-cost: 6 c ---[ 404]---> BDD-cost: 6 c ---[ 403]---> BDD-cost: 6 c ---[ 402]---> BDD-cost: 6 c ---[ 401]---> BDD-cost: 6 c ---[ 400]---> BDD-cost: 6 c ---[ 399]---> BDD-cost: 6 c ---[ 398]---> BDD-cost: 6 c ---[ 397]---> BDD-cost: 6 c ---[ 396]---> BDD-cost: 6 c ---[ 395]---> BDD-cost: 6 c ---[ 394]---> BDD-cost: 6 c ---[ 393]---> BDD-cost: 6 c ---[ 392]---> BDD-cost: 6 c ---[ 391]---> BDD-cost: 6 c ---[ 390]---> BDD-cost: 6 c ---[ 389]---> BDD-cost: 6 c ---[ 388]---> BDD-cost: 6 c ---[ 387]---> BDD-cost: 6 c ---[ 386]---> BDD-cost: 6 c ---[ 385]---> BDD-cost: 6 c ---[ 384]---> BDD-cost: 6 c ---[ 383]---> BDD-cost: 6 c ---[ 382]---> BDD-cost: 6 c ---[ 381]---> BDD-cost: 6 c ---[ 380]---> BDD-cost: 6 c ---[ 379]---> BDD-cost: 6 c ---[ 378]---> BDD-cost: 6 c ---[ 377]---> BDD-cost: 6 c ---[ 376]---> BDD-cost: 6 c ---[ 375]---> BDD-cost: 6 c ---[ 374]---> BDD-cost: 6 c ---[ 373]---> BDD-cost: 6 c ---[ 372]---> BDD-cost: 6 c ---[ 371]---> BDD-cost: 6 c ---[ 370]---> BDD-cost: 6 c ---[ 369]---> BDD-cost: 6 c ---[ 368]---> BDD-cost: 6 c ---[ 367]---> BDD-cost: 6 c ---[ 366]---> BDD-cost: 6 c ---[ 365]---> BDD-cost: 6 c ---[ 364]---> BDD-cost: 6 c ---[ 363]---> BDD-cost: 6 c ---[ 362]---> BDD-cost: 6 c ---[ 361]---> BDD-cost: 6 c ---[ 360]---> BDD-cost: 6 c ---[ 359]---> BDD-cost: 6 c ---[ 358]---> BDD-cost: 6 c ---[ 357]---> BDD-cost: 6 c ---[ 356]---> BDD-cost: 6 c ---[ 355]---> BDD-cost: 6 c ---[ 354]---> BDD-cost: 6 c ---[ 353]---> BDD-cost: 6 c ---[ 352]---> BDD-cost: 6 c ---[ 351]---> BDD-cost: 6 c ---[ 350]---> BDD-cost: 6 c ---[ 349]---> BDD-cost: 6 c ---[ 348]---> BDD-cost: 6 c ---[ 347]---> BDD-cost: 6 c ---[ 346]---> BDD-cost: 6 c ---[ 345]---> BDD-cost: 6 c ---[ 344]---> BDD-cost: 6 c ---[ 343]---> BDD-cost: 6 c ---[ 342]---> BDD-cost: 6 c ---[ 341]---> BDD-cost: 6 c ---[ 340]---> BDD-cost: 6 c ---[ 339]---> BDD-cost: 6 c ---[ 338]---> BDD-cost: 6 c ---[ 337]---> BDD-cost: 6 c ---[ 336]---> BDD-cost: 6 c ---[ 335]---> BDD-cost: 6 c ---[ 334]---> BDD-cost: 6 c ---[ 333]---> BDD-cost: 6 c ---[ 332]---> BDD-cost: 6 c ---[ 331]---> BDD-cost: 6 c ---[ 330]---> BDD-cost: 6 c ---[ 329]---> BDD-cost: 6 c ---[ 328]---> BDD-cost: 6 c ---[ 327]---> BDD-cost: 6 c ---[ 326]---> BDD-cost: 6 c ---[ 325]---> BDD-cost: 6 c ---[ 324]---> BDD-cost: 6 c ---[ 323]---> BDD-cost: 6 c ---[ 322]---> BDD-cost: 6 c ---[ 321]---> BDD-cost: 6 c ---[ 320]---> BDD-cost: 6 c ---[ 319]---> BDD-cost: 6 c ---[ 318]---> BDD-cost: 6 c ---[ 317]---> BDD-cost: 6 c ---[ 316]---> BDD-cost: 6 c ---[ 315]---> BDD-cost: 6 c ---[ 314]---> BDD-cost: 6 c ---[ 313]---> BDD-cost: 6 c ---[ 312]---> BDD-cost: 6 c ---[ 311]---> BDD-cost: 6 c ---[ 310]---> BDD-cost: 6 c ---[ 309]---> BDD-cost: 6 c ---[ 308]---> BDD-cost: 6 c ---[ 307]---> BDD-cost: 6 c ---[ 306]---> BDD-cost: 6 c ---[ 305]---> BDD-cost: 6 c ---[ 304]---> BDD-cost: 6 c ---[ 303]---> BDD-cost: 6 c ---[ 302]---> BDD-cost: 6 c ---[ 301]---> BDD-cost: 6 c ---[ 300]---> BDD-cost: 6 c ---[ 299]---> BDD-cost: 6 c ---[ 298]---> BDD-cost: 6 c ---[ 297]---> BDD-cost: 6 c ---[ 296]---> BDD-cost: 6 c ---[ 295]---> BDD-cost: 6 c ---[ 294]---> BDD-cost: 6 c ---[ 293]---> BDD-cost: 6 c ---[ 292]---> BDD-cost: 6 c ---[ 291]---> BDD-cost: 6 c ---[ 290]---> BDD-cost: 6 c ---[ 289]---> BDD-cost: 6 c ---[ 288]---> BDD-cost: 6 c ---[ 287]---> BDD-cost: 6 c ---[ 286]---> BDD-cost: 6 c ---[ 285]---> BDD-cost: 6 c ---[ 284]---> BDD-cost: 6 c ---[ 283]---> BDD-cost: 6 c ---[ 282]---> BDD-cost: 6 c ---[ 281]---> BDD-cost: 6 c ---[ 280]---> BDD-cost: 6 c ---[ 279]---> BDD-cost: 6 c ---[ 278]---> BDD-cost: 6 c ---[ 277]---> BDD-cost: 6 c ---[ 276]---> BDD-cost: 6 c ---[ 275]---> BDD-cost: 6 c ---[ 274]---> BDD-cost: 6 c ---[ 273]---> BDD-cost: 6 c ---[ 272]---> BDD-cost: 6 c ---[ 271]---> BDD-cost: 6 c ---[ 270]---> BDD-cost: 6 c ---[ 269]---> BDD-cost: 6 c ---[ 268]---> BDD-cost: 6 c ---[ 267]---> BDD-cost: 6 c ---[ 266]---> BDD-cost: 6 c ---[ 265]---> BDD-cost: 6 c ---[ 264]---> BDD-cost: 6 c ---[ 263]---> BDD-cost: 6 c ---[ 262]---> BDD-cost: 6 c ---[ 261]---> BDD-cost: 6 c ---[ 260]---> BDD-cost: 6 c ---[ 259]---> BDD-cost: 6 c ---[ 258]---> BDD-cost: 6 c ---[ 257]---> BDD-cost: 6 c ---[ 256]---> BDD-cost: 6 c ---[ 255]---> BDD-cost: 6 c ---[ 254]---> BDD-cost: 6 c ---[ 253]---> BDD-cost: 1 c ---[ 252]---> BDD-cost: 1 c ---[ 251]---> BDD-cost: 1 c ---[ 250]---> BDD-cost: 1 c ---[ 249]---> BDD-cost: 1 c ---[ 248]---> BDD-cost: 1 c ---[ 247]---> BDD-cost: 1 c ---[ 246]---> BDD-cost: 1 c ---[ 245]---> BDD-cost: 1 c ---[ 244]---> BDD-cost: 1 c ---[ 243]---> BDD-cost: 1 c ---[ 242]---> BDD-cost: 1 c ---[ 241]---> BDD-cost: 1 c ---[ 240]---> BDD-cost: 1 c ---[ 239]---> BDD-cost: 1 c ---[ 238]---> BDD-cost: 1 c ---[ 237]---> BDD-cost: 1 c ---[ 236]---> BDD-cost: 1 c ---[ 235]---> BDD-cost: 1 c ---[ 234]---> BDD-cost: 1 c ---[ 233]---> BDD-cost: 1 c ---[ 232]---> BDD-cost: 1 c ---[ 231]---> BDD-cost: 1 c ---[ 230]---> BDD-cost: 1 c ---[ 229]---> BDD-cost: 1 c ---[ 228]---> BDD-cost: 1 c ---[ 227]---> BDD-cost: 1 c ---[ 226]---> BDD-cost: 1 c ---[ 225]---> BDD-cost: 1 c ---[ 224]---> BDD-cost: 1 c ---[ 223]---> BDD-cost: 1 c ---[ 222]---> BDD-cost: 1 c ---[ 221]---> BDD-cost: 1 c ---[ 220]---> BDD-cost: 1 c ---[ 219]---> BDD-cost: 1 c ---[ 218]---> BDD-cost: 1 c ---[ 217]---> BDD-cost: 1 c ---[ 216]---> BDD-cost: 1 c ---[ 215]---> BDD-cost: 1 c ---[ 214]---> BDD-cost: 1 c ---[ 213]---> BDD-cost: 1 c ---[ 212]---> BDD-cost: 1 c ---[ 211]---> BDD-cost: 1 c ---[ 210]---> BDD-cost: 1 c ---[ 209]---> BDD-cost: 1 c ---[ 208]---> BDD-cost: 1 c ---[ 207]---> BDD-cost: 1 c ---[ 206]---> BDD-cost: 1 c ---[ 205]---> BDD-cost: 1 c ---[ 204]---> BDD-cost: 1 c ---[ 203]---> BDD-cost: 1 c ---[ 202]---> BDD-cost: 1 c ---[ 201]---> BDD-cost: 1 c ---[ 200]---> BDD-cost: 1 c ---[ 199]---> BDD-cost: 1 c ---[ 198]---> BDD-cost: 1 c ---[ 197]---> BDD-cost: 1 c ---[ 196]---> BDD-cost: 1 c ---[ 195]---> BDD-cost: 1 c ---[ 194]---> BDD-cost: 1 c ---[ 193]---> BDD-cost: 1 c ---[ 192]---> BDD-cost: 1 c ---[ 191]---> BDD-cost: 1 c ---[ 190]---> BDD-cost: 1 c ---[ 189]---> BDD-cost: 1 c ---[ 188]---> BDD-cost: 1 c ---[ 187]---> BDD-cost: 1 c ---[ 186]---> BDD-cost: 1 c ---[ 185]---> BDD-cost: 1 c ---[ 184]---> BDD-cost: 1 c ---[ 183]---> BDD-cost: 1 c ---[ 182]---> BDD-cost: 1 c ---[ 181]---> BDD-cost: 1 c ---[ 180]---> BDD-cost: 1 c ---[ 179]---> BDD-cost: 1 c ---[ 178]---> BDD-cost: 1 c ---[ 177]---> BDD-cost: 1 c ---[ 176]---> BDD-cost: 1 c ---[ 175]---> BDD-cost: 1 c ---[ 174]---> BDD-cost: 1 c ---[ 173]---> BDD-cost: 1 c ---[ 172]---> BDD-cost: 1 c ---[ 171]---> BDD-cost: 1 c ---[ 170]---> BDD-cost: 1 c ---[ 0]---> Adder-cost: 245 maxlim: 255 bits: 9/8 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 18533 50267 | 6177 0 0 nan | 0.000 % | c | 100 | 18533 50267 | 6794 100 890 8.9 | 14.349 % | c | 252 | 18533 50267 | 7474 252 2814 11.2 | 14.349 % | c | 478 | 18533 50267 | 8221 478 5356 11.2 | 14.349 % | c | 815 | 18533 50267 | 9043 815 10568 13.0 | 14.349 % | c | 1321 | 18533 50267 | 9948 1321 21019 15.9 | 14.349 % | c | 2080 | 18533 50267 | 10942 2080 33047 15.9 | 14.349 % | c ============================================================================== c [1mFound solution: 129[0m c ---[ 0]---> BDD-cost: 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2896 | 18541 50284 | 6180 2896 46509 16.1 | 14.349 % | c | 2996 | 18541 50284 | 6798 2996 47641 15.9 | 14.361 % | c ============================================================================== c [1mFound solution: 128[0m c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3140 | 18517 50206 | 6172 3140 49548 15.8 | 14.361 % | c | 3240 | 18517 50206 | 6789 3240 50991 15.7 | 14.446 % | c | 3390 | 18517 50206 | 7468 3390 53797 15.9 | 14.446 % | c | 3615 | 18517 50206 | 8214 3615 58020 16.0 | 14.446 % | c | 3953 | 18517 50206 | 9036 3953 63164 16.0 | 14.446 % | c | 4459 | 18517 50206 | 9940 4459 70204 15.7 | 14.446 % | c | 5218 | 18517 50206 | 10934 5218 81000 15.5 | 14.446 % | c | 6358 | 18494 50155 | 12027 6356 103792 16.3 | 14.548 % | c | 8066 | 18494 50155 | 13230 8064 135540 16.8 | 14.548 % | c ============================================================================== c [1mFound solution: 125[0m c ---[ 0]---> BDD-cost: 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 8441 | 18497 50166 | 6165 8439 141638 16.8 | 14.548 % | c | 8542 | 18497 50166 | 6781 4321 69554 16.1 | 14.560 % | c | 8692 | 18497 50166 | 7459 4471 72404 16.2 | 14.560 % | c | 8917 | 18497 50166 | 8205 4696 76156 16.2 | 14.560 % | c | 9254 | 18497 50166 | 9026 5033 82784 16.4 | 14.560 % | c | 9760 | 18497 50166 | 9928 5539 90858 16.4 | 14.560 % | c | 10519 | 18497 50166 | 10921 6298 103301 16.4 | 14.560 % | c ============================================================================== c [1mFound solution: 124[0m c ---[ 0]---> BDD-cost: 4 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 11318 | 18498 50172 | 6166 7097 119916 16.9 | 14.560 % | c | 11418 | 18498 50172 | 6782 3649 54698 15.0 | 14.575 % | c | 11568 | 18498 50172 | 7460 3799 56305 14.8 | 14.575 % | c | 11793 | 18498 50172 | 8206 4024 60750 15.1 | 14.575 % | c | 12130 | 18498 50172 | 9027 4361 67204 15.4 | 14.575 % | c | 12636 | 18498 50172 | 9930 4867 78978 16.2 | 14.575 % | c | 13396 | 18498 50172 | 10923 5627 93422 16.6 | 14.575 % | c | 14537 | 18498 50172 | 12015 6768 116999 17.3 | 14.575 % | c | 16246 | 18498 50172 | 13217 8477 158788 18.7 | 14.575 % | c | 18808 | 18498 50172 | 14539 11039 221711 20.1 | 14.575 % | c ============================================================================== c [1mFound solution: 121[0m c ---[ 0]---> BDD-cost: 4 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19858 | 18501 50182 | 6167 12089 245364 20.3 | 14.575 % | c | 19959 | 18501 50182 | 6783 6146 119000 19.4 | 14.587 % | c | 20109 | 18501 50182 | 7462 6296 123193 19.6 | 14.587 % | c | 20334 | 18501 50182 | 8208 6521 128925 19.8 | 14.587 % | c | 20671 | 18501 50182 | 9029 6858 133031 19.4 | 14.587 % | c | 21180 | 18501 50182 | 9932 7367 145768 19.8 | 14.587 % | c | 21940 | 18501 50182 | 10925 8127 161508 19.9 | 14.587 % | c | 23080 | 18501 50182 | 12017 9267 184427 19.9 | 14.587 % | c | 24788 | 18501 50182 | 13219 10975 219776 20.0 | 14.587 % | c | 27350 | 18501 50182 | 14541 13537 272603 20.1 | 14.587 % | c ============================================================================== c [1mFound solution: 120[0m c ---[ 0]---> BDD-cost: 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 28855 | 18502 50187 | 6167 15042 305144 20.3 | 14.587 % | c | 28955 | 18502 50187 | 6783 3861 62264 16.1 | 14.602 % | c | 29106 | 18502 50187 | 7462 4012 64320 16.0 | 14.601 % | c | 29331 | 18502 50187 | 8208 4237 69154 16.3 | 14.601 % | c | 29668 | 18502 50187 | 9029 4574 76548 16.7 | 14.601 % | c | 30176 | 18502 50187 | 9932 5082 85349 16.8 | 14.601 % | c | 30935 | 18502 50187 | 10925 5841 95625 16.4 | 14.602 % | c | 32074 | 18502 50187 | 12017 6980 124319 17.8 | 14.601 % | c | 33784 | 18502 50187 | 13219 8690 167359 19.3 | 14.602 % | c | 36346 | 18502 50187 | 14541 11252 230172 20.5 | 14.601 % | c | 40190 | 18502 50187 | 15995 15096 327602 21.7 | 14.602 % | c | 45956 | 18502 50187 | 17595 11754 274054 23.3 | 14.601 % | c | 54605 | 18479 50136 | 19354 10792 241427 22.4 | 14.703 % | c | 67579 | 18479 50136 | 21290 12998 321982 24.8 | 14.703 % | c ============================================================================== c [1mFound solution: 119[0m c ---[ 0]---> BDD-cost: 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 72978 | 18483 50148 | 6161 18397 481891 26.2 | 14.703 % | c | 73078 | 18483 50148 | 6777 4700 90823 19.3 | 14.713 % | c | 73229 | 18483 50148 | 7454 4851 92976 19.2 | 14.713 % | c | 73454 | 18483 50148 | 8200 5076 97788 19.3 | 14.713 % | c | 73791 | 18483 50148 | 9020 5413 102283 18.9 | 14.713 % | c | 74300 | 18483 50148 | 9922 5922 110733 18.7 | 14.713 % | c | 75059 | 18483 50148 | 10914 6681 130035 19.5 | 14.713 % | c | 76198 | 18483 50148 | 12006 7820 154948 19.8 | 14.713 % | c | 77907 | 18483 50148 | 13206 9529 195763 20.5 | 14.713 % | c | 80470 | 18483 50148 | 14527 12092 251406 20.8 | 14.713 % | c | 84315 | 18483 50148 | 15980 15937 343990 21.6 | 14.713 % | c | 90083 | 18460 50097 | 17578 13116 287033 21.9 | 14.815 % | c | 98734 | 18460 50097 | 19335 12154 304038 25.0 | 14.815 % | c | 111708 | 18436 50044 | 21269 14667 344861 23.5 | 14.917 % | c | 131169 | 18436 50044 | 23396 22644 555453 24.5 | 14.917 % | c ============================================================================== c [1mFound solution: 118[0m c ---[ 0]---> BDD-cost: 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 133487 | 18440 50056 | 6146 24962 612096 24.5 | 14.917 % | c | 133587 | 18440 50056 | 6760 6341 111186 17.5 | 14.926 % | c | 133737 | 18440 50056 | 7436 6491 113652 17.5 | 14.926 % | c | 133962 | 18440 50056 | 8180 6716 118022 17.6 | 14.926 % | c | 134299 | 18440 50056 | 8998 7053 124497 17.7 | 14.926 % | c | 134806 | 18440 50056 | 9898 7560 136742 18.1 | 14.926 % | c | 135565 | 18440 50056 | 10888 8319 154287 18.5 | 14.926 % | c | 136707 | 18440 50056 | 11976 9461 180914 19.1 | 14.926 % | c | 138415 | 18440 50056 | 13174 11169 221880 19.9 | 14.926 % | c | 140979 | 18440 50056 | 14491 13733 282298 20.6 | 14.926 % | c | 144823 | 18440 50056 | 15941 9483 199015 21.0 | 14.926 % | c | 150591 | 18440 50056 | 17535 15251 340745 22.3 | 14.926 % | c | 159242 | 18440 50056 | 19288 14262 333014 23.3 | 14.926 % | c | 172218 | 18440 50056 | 21217 16566 443477 26.8 | 14.926 % | c | 191680 | 18440 50056 | 23339 13016 282963 21.7 | 14.926 % | c | 220874 | 18440 50056 | 25673 17229 411469 23.9 | 14.926 % | c | 264663 | 18440 50056 | 28240 20216 453614 22.4 | 14.926 % | c | 330347 | 18440 50056 | 31064 25851 717410 27.8 | 14.926 % | c | 428873 | 18440 50056 | 34171 25715 628734 24.5 | 14.926 % | c c *** TERMINATED *** s SATISFIABLE v -C0377_bit0 C0377_bit1 C0377_bit2 -C0377_bit3 C0377_bit4 C0377_bit5 C0377_bit6 -C0377_bit7 C0001_bit0 C0002_bit0 C0003_bit0 C0004_bit0 C0005_bit0 C0006_bit0 C0007_bit0 C0008_bit0 C0009_bit0 C0010_bit0 C0011_bit0 C0012_bit0 C0013_bit0 C0014_bit0 C0015_bit0 -C0016_bit0 C0017_bit0 -C0018_bit0 C0019_bit0 C0020_bit0 -C0021_bit0 C0022_bit0 C0023_bit0 C0024_bit0 C0025_bit0 C0026_bit0 -C0027_bit0 C0028_bit0 C0029_bit0 C0030_bit0 C0031_bit0 -C0032_bit0 -C0033_bit0 C0034_bit0 C0035_bit0 -C0036_bit0 C0037_bit0 C0038_bit0 -C0039_bit0 C0040_bit0 -C0041_bit0 -C0042_bit0 -C0043_bit0 -C0044_bit0 -C0045_bit0 -C0046_bit0 -C0047_bit0 -C0048_bit0 C0049_bit0 -C0050_bit0 C0051_bit0 C0052_bit0 -C0053_bit0 -C0054_bit0 -C0055_bit0 -C0056_bit0 -C0057_bit0 C0058_bit0 C0059_bit0 C0060_bit0 -C0061_bit0 -C0062_bit0 -C0063_bit0 C0064_bit0 C0065_bit0 -C0066_bit0 -C0067_bit0 -C0068_bit0 C0069_bit0 C0070_bit0 -C0071_bit0 -C0072_bit0 -C0073_bit0 C0074_bit0 -C0075_bit0 -C0076_bit0 -C0077_bit0 -C0078_bit0 -C0079_bit0 -C0080_bit0 C0081_bit0 -C0082_bit0 C0083_bit0 C0084_bit0 -C0085_bit0 -C0086_bit0 -C0087_bit0 -C0088_bit0 -C0089_bit0 -C0090_bit0 -C0091_bit0 -C0092_bit0 -C0093_bit0 -C0094_bit0 -C0095_bit0 -C0096_bit0 -C0097_bit0 -C0098_bit0 -C0099_bit0 C0100_bit0 -C0101_bit0 C0102_bit0 -C0103_bit0 -C0104_bit0 C0105_bit0 -C0106_bit0 -C0107_bit0 -C0108_bit0 -C0109_bit0 -C0110_bit0 C0111_bit0 -C0112_bit0 -C0113_bit0 -C0114_bit0 -C0115_bit0 C0116_bit0 C0117_bit0 -C0118_bit0 -C0119_bit0 C0120_bit0 -C0121_bit0 -C0122_bit0 C0123_bit0 -C0124_bit0 C0125_bit0 C0126_bit0 C0127_bit0 C0128_bit0 C0129_bit0 C0130_bit0 C0131_bit0 C0132_bit0 -C0133_bit0 C0134_bit0 -C0135_bit0 -C0136_bit0 C0137_bit0 C0138_bit0 C0139_bit0 C0140_bit0 C0141_bit0 -C0142_bit0 -C0143_bit0 -C0144_bit0 C0145_bit0 C0146_bit0 C0147_bit0 -C0148_bit0 -C0149_bit0 C0150_bit0 C0151_bit0 C0152_bit0 -C0153_bit0 -C0154_bit0 C0155_bit0 C0156_bit0 C0157_bit0 -C0158_bit0 C0159_bit0 C0160_bit0 C0161_bit0 C0162_bit0 C0163_bit0 C0164_bit0 -C0165_bit0 C0166_bit0 -C0167_bit0 -C0168_bit0 C0169_bit0 C0170_bit0 C0171_bit0 C0172_bit0 C0173_bit0 C0174_bit0 -C0175_bit0 -C0176_bit0 C0177_bit0 -C0178_bit0 -C0179_bit0 C0180_bit0 C0181_bit0 C0182_bit0 C0183_bit0 C0184_bit0 C0185_bit0 C0186_bit0 -C0187_bit0 -C0188_bit0 -C0189_bit0 C0190_bit0 C0191_bit0 -C0192_bit0 C0193_bit0 -C0194_bit0 C0195_bit0 C0196_bit0 -C0197_bit0 C0198_bit0 -C0199_bit0 C0200_bit0 -C0201_bit0 C0202_bit0 -C0203_bit0 C0204_bit0 C0205_bit0 -C0206_bit0 C0207_bit0 -C0208_bit0 C0209_bit0 C0210_bit0 -C0211_bit0 C0212_bit0 C0213_bit0 C0214_bit0 -C0215_bit0 -C0216_bit0 C0217_bit0 C0218_bit0 C0219_bit0 -C0220_bit0 -C0221_bit0 C0222_bit0 -C0223_bit0 -C0224_bit0 -C0225_bit0 -C0226_bit0 -C0227_bit0 -C0228_bit0 -C0229_bit0 -C0230_bit0 C0231_bit0 -C0232_bit0 -C0233_bit0 C0234_bit0 -C0235_bit0 -C0236_bit0 C0237_bit0 -C0238_bit0 C0239_bit0 -C0240_bit0 -C0241_bit0 C0242_bit0 C0243_bit0 C0244_bit0 C0245_bit0 C0246_bit0 -C0247_bit0 -C0248_bit0 -C0249_bit0 C0250_bit0 C0251_bit0 C0252_bit0 -C0253_bit0 -C0254_bit0 -C0255_bit0 -C0256_bit0 -C0257_bit0 -C0258_bit0 C0259_bit0 C0260_bit0 -C0261_bit0 C0262_bit0 C0263_bit0 -C0264_bit0 -C0265_bit0 -C0266_bit0 -C0267_bit0 -C0268_bit0 -C0269_bit0 -C0270_bit0 C0271_bit0 C0272_bit0 C0273_bit0 -C0274_bit0 -C0275_bit0 C0276_bit0 -C0277_bit0 C0278_bit0 -C0279_bit0 -C0280_bit0 C0281_bit0 -C0282_bit0 C0283_bit0 -C0284_bit0 C0285_bit0 -C0286_bit0 C0287_bit0 -C0288_bit0 -C0289_bit0 C0290_bit0 -C0291_bit0 C0292_bit0 -C0293_bit0 -C0294_bit0 C0295_bit0 -C0296_bit0 -C0297_bit0 -C0298_bit0 C0299_bit0 C0300_bit0 -C0301_bit0 -C0302_bit0 -C0303_bit0 C0304_bit0 C0305_bit0 -C0306_bit0 C0307_bit0 C0308_bit0 C0309_bit0 C0310_bit0 C0311_bit0 C0312_bit0 C0313_bit0 C0314_bit0 -C0315_bit0 C0316_bit0 C0317_bit0 -C0318_bit0 C0319_bit0 C0320_bit0 -C0321_bit0 C0322_bit0 -C0323_bit0 C0324_bit0 C0325_bit0 -C0326_bit0 -C0327_bit0 -C0328_bit0 -C0329_bit0 -C0330_bit0 C0331_bit0 C0332_bit0 C0333_bit0 -C0334_bit0 -C0335_bit0 -C0336_bit0 -C0337_bit0 -C0337_bit1 -C0337_bit2 C0338_bit0 -C0338_bit1 -C0338_bit2 -C0339_bit0 C0339_bit1 -C0339_
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/25643/stat): 25643 (minisat+_script) R 25642 25643 824 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1797722615 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/25643/statm): 174 3 169 147 0 27 0 [pid=25643] 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=25644 New process pid=25645 New process pid=25646 execve syscall for /bin/sed executable One traced child (pid=25645) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=25646) exited with status: 0 One traced child (pid=25644) exited with status: 0 New process pid=25647 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-neos16.opb [startup+10.0036 s] Raw data (loadavg): 0.93 0.95 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 898 0 0 0 985 4 0 0 25 0 1 0 1797722620 4165632 884 4294967295 134512640 135094434 3221224432 3221223088 134558144 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25647/statm): 1017 884 145 145 0 872 0 [pid=25647] vsize: 4068 Current children cumulated CPU time (s) 9.9 Current children cumulated vsize (Kb) 6192 [startup+20.0043 s] Raw data (loadavg): 0.94 0.96 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1029 0 0 0 1983 5 0 0 25 0 1 0 1797722620 4702208 1015 4294967295 134512640 135094434 3221224432 3221223104 134555945 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1148 1015 145 145 0 1003 0 [pid=25647] vsize: 4592 Current children cumulated CPU time (s) 19.89 Current children cumulated vsize (Kb) 6716 [startup+30.0061 s] Raw data (loadavg): 0.95 0.96 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1113 0 0 0 2981 6 0 0 25 0 1 0 1797722620 5046272 1099 4294967295 134512640 135094434 3221224432 3221223088 134558153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1232 1099 145 145 0 1087 0 [pid=25647] vsize: 4928 Current children cumulated CPU time (s) 29.88 Current children cumulated vsize (Kb) 7052 [startup+40.0068 s] Raw data (loadavg): 0.95 0.96 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1155 0 0 0 3980 7 0 0 25 0 1 0 1797722620 5218304 1141 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1274 1141 145 145 0 1129 0 [pid=25647] vsize: 5096 Current children cumulated CPU time (s) 39.88 Current children cumulated vsize (Kb) 7220 [startup+50.0076 s] Raw data (loadavg): 0.96 0.96 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1256 0 0 0 4979 7 0 0 25 0 1 0 1797722620 5681152 1242 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1387 1242 145 145 0 1242 0 [pid=25647] vsize: 5548 Current children cumulated CPU time (s) 49.87 Current children cumulated vsize (Kb) 7672 [startup+60.0083 s] Raw data (loadavg): 0.97 0.96 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1311 0 0 0 5978 8 0 0 25 0 1 0 1797722620 5906432 1297 4294967295 134512640 135094434 3221224432 3221223100 134553522 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25647/statm): 1442 1297 145 145 0 1297 0 [pid=25647] vsize: 5768 Current children cumulated CPU time (s) 59.87 Current children cumulated vsize (Kb) 7892 [startup+70.0091 s] Raw data (loadavg): 0.97 0.96 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1378 0 0 0 6976 9 0 0 25 0 1 0 1797722620 6176768 1364 4294967295 134512640 135094434 3221224432 3221223024 134551780 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1508 1364 145 145 0 1363 0 [pid=25647] vsize: 6032 Current children cumulated CPU time (s) 69.86 Current children cumulated vsize (Kb) 8156 [startup+80.0098 s] Raw data (loadavg): 0.98 0.96 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1388 0 0 0 7975 9 0 0 25 0 1 0 1797722620 6225920 1374 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1520 1374 145 145 0 1375 0 [pid=25647] vsize: 6080 Current children cumulated CPU time (s) 79.85 Current children cumulated vsize (Kb) 8204 [startup+90.0105 s] Raw data (loadavg): 0.98 0.96 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1447 0 0 0 8975 9 0 0 25 0 1 0 1797722620 6467584 1433 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1579 1433 145 145 0 1434 0 [pid=25647] vsize: 6316 Current children cumulated CPU time (s) 89.85 Current children cumulated vsize (Kb) 8440 [startup+100.012 s] Raw data (loadavg): 0.98 0.96 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1501 0 0 0 9974 10 0 0 25 0 1 0 1797722620 6684672 1487 4294967295 134512640 135094434 3221224432 3221223104 134556288 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1632 1487 145 145 0 1487 0 [pid=25647] vsize: 6528 Current children cumulated CPU time (s) 99.85 Current children cumulated vsize (Kb) 8652 [startup+110.013 s] Raw data (loadavg): 0.98 0.96 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1507 0 0 0 10974 10 0 0 25 0 1 0 1797722620 6733824 1493 4294967295 134512640 135094434 3221224432 3221223056 134562139 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1644 1493 145 145 0 1499 0 [pid=25647] vsize: 6576 Current children cumulated CPU time (s) 109.85 Current children cumulated vsize (Kb) 8700 [startup+120.014 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1507 0 0 0 11974 10 0 0 25 0 1 0 1797722620 6733824 1493 4294967295 134512640 135094434 3221224432 3221223056 134557675 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1644 1493 145 145 0 1499 0 [pid=25647] vsize: 6576 Current children cumulated CPU time (s) 119.85 Current children cumulated vsize (Kb) 8700 [startup+130.015 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1508 0 0 0 12974 10 0 0 25 0 1 0 1797722620 6733824 1494 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1644 1494 145 145 0 1499 0 [pid=25647] vsize: 6576 Current children cumulated CPU time (s) 129.85 Current children cumulated vsize (Kb) 8700 [startup+140.014 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1508 0 0 0 13974 10 0 0 25 0 1 0 1797722620 6733824 1494 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1644 1494 145 145 0 1499 0 [pid=25647] vsize: 6576 Current children cumulated CPU time (s) 139.85 Current children cumulated vsize (Kb) 8700 [startup+150.016 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1510 0 0 0 14975 10 0 0 25 0 1 0 1797722620 6733824 1496 4294967295 134512640 135094434 3221224432 3221223088 134557956 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1644 1496 145 145 0 1499 0 [pid=25647] vsize: 6576 Current children cumulated CPU time (s) 149.86 Current children cumulated vsize (Kb) 8700 [startup+160.017 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1514 0 0 0 15975 10 0 0 25 0 1 0 1797722620 6750208 1500 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1648 1500 145 145 0 1503 0 [pid=25647] vsize: 6592 Current children cumulated CPU time (s) 159.86 Current children cumulated vsize (Kb) 8716 [startup+170.016 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1539 0 0 0 16974 10 0 0 25 0 1 0 1797722620 6848512 1525 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1672 1525 145 145 0 1527 0 [pid=25647] vsize: 6688 Current children cumulated CPU time (s) 169.85 Current children cumulated vsize (Kb) 8812 [startup+180.017 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1545 0 0 0 17975 10 0 0 25 0 1 0 1797722620 6881280 1531 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1680 1531 145 145 0 1535 0 [pid=25647] vsize: 6720 Current children cumulated CPU time (s) 179.86 Current children cumulated vsize (Kb) 8844 [startup+190.018 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1565 0 0 0 18974 10 0 0 25 0 1 0 1797722620 6963200 1551 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1700 1551 145 145 0 1555 0 [pid=25647] vsize: 6800 Current children cumulated CPU time (s) 189.85 Current children cumulated vsize (Kb) 8924 [startup+200.019 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1591 0 0 0 19974 10 0 0 25 0 1 0 1797722620 7065600 1577 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1725 1577 145 145 0 1580 0 [pid=25647] vsize: 6900 Current children cumulated CPU time (s) 199.85 Current children cumulated vsize (Kb) 9024 [startup+210.019 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1598 0 0 0 20975 10 0 0 25 0 1 0 1797722620 7098368 1584 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1733 1584 145 145 0 1588 0 [pid=25647] vsize: 6932 Current children cumulated CPU time (s) 209.86 Current children cumulated vsize (Kb) 9056 [startup+220.02 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1669 0 0 0 21973 11 0 0 25 0 1 0 1797722620 7389184 1655 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1804 1655 145 145 0 1659 0 [pid=25647] vsize: 7216 Current children cumulated CPU time (s) 219.85 Current children cumulated vsize (Kb) 9340 [startup+230.021 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1669 0 0 0 22973 11 0 0 25 0 1 0 1797722620 7389184 1655 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1804 1655 145 145 0 1659 0 [pid=25647] vsize: 7216 Current children cumulated CPU time (s) 229.85 Current children cumulated vsize (Kb) 9340 [startup+240.022 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1669 0 0 0 23974 11 0 0 25 0 1 0 1797722620 7389184 1655 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1804 1655 145 145 0 1659 0 [pid=25647] vsize: 7216 Current children cumulated CPU time (s) 239.86 Current children cumulated vsize (Kb) 9340 [startup+250.022 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1669 0 0 0 24974 11 0 0 25 0 1 0 1797722620 7389184 1655 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1804 1655 145 145 0 1659 0 [pid=25647] vsize: 7216 Current children cumulated CPU time (s) 249.86 Current children cumulated vsize (Kb) 9340 [startup+260.023 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1669 0 0 0 25974 11 0 0 25 0 1 0 1797722620 7389184 1655 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1804 1655 145 145 0 1659 0 [pid=25647] vsize: 7216 Current children cumulated CPU time (s) 259.86 Current children cumulated vsize (Kb) 9340 [startup+270.024 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1669 0 0 0 26974 11 0 0 25 0 1 0 1797722620 7389184 1655 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1804 1655 145 145 0 1659 0 [pid=25647] vsize: 7216 Current children cumulated CPU time (s) 269.86 Current children cumulated vsize (Kb) 9340 [startup+280.025 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1669 0 0 0 27974 11 0 0 25 0 1 0 1797722620 7389184 1655 4294967295 134512640 135094434 3221224432 3221223120 134554739 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1804 1655 145 145 0 1659 0 [pid=25647] vsize: 7216 Current children cumulated CPU time (s) 279.86 Current children cumulated vsize (Kb) 9340 [startup+290.025 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1669 0 0 0 28974 11 0 0 25 0 1 0 1797722620 7389184 1655 4294967295 134512640 135094434 3221224432 3221223024 134557271 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1804 1655 145 145 0 1659 0 [pid=25647] vsize: 7216 Current children cumulated CPU time (s) 289.86 Current children cumulated vsize (Kb) 9340 [startup+300.026 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1671 0 0 0 29975 11 0 0 25 0 1 0 1797722620 7401472 1657 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1807 1657 145 145 0 1662 0 [pid=25647] vsize: 7228 Current children cumulated CPU time (s) 299.87 Current children cumulated vsize (Kb) 9352 [startup+310.027 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1707 0 0 0 30974 12 0 0 25 0 1 0 1797722620 7561216 1693 4294967295 134512640 135094434 3221224432 3221223104 134556291 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1846 1693 145 145 0 1701 0 [pid=25647] vsize: 7384 Current children cumulated CPU time (s) 309.87 Current children cumulated vsize (Kb) 9508 [startup+320.028 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1711 0 0 0 31975 12 0 0 25 0 1 0 1797722620 7577600 1697 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1850 1697 145 145 0 1705 0 [pid=25647] vsize: 7400 Current children cumulated CPU time (s) 319.88 Current children cumulated vsize (Kb) 9524 [startup+330.028 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1717 0 0 0 32975 12 0 0 25 0 1 0 1797722620 7610368 1703 4294967295 134512640 135094434 3221224432 3221223104 134556533 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1858 1703 145 145 0 1713 0 [pid=25647] vsize: 7432 Current children cumulated CPU time (s) 329.88 Current children cumulated vsize (Kb) 9556 [startup+340.029 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1727 0 0 0 33975 12 0 0 25 0 1 0 1797722620 7643136 1713 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25647/statm): 1866 1713 145 145 0 1721 0 [pid=25647] vsize: 7464 Current children cumulated CPU time (s) 339.88 Current children cumulated vsize (Kb) 9588 [startup+350.031 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1728 0 0 0 34974 12 0 0 25 0 1 0 1797722620 7643136 1714 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1866 1714 145 145 0 1721 0 [pid=25647] vsize: 7464 Current children cumulated CPU time (s) 349.87 Current children cumulated vsize (Kb) 9588 [startup+360.032 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1728 0 0 0 35975 12 0 0 25 0 1 0 1797722620 7643136 1714 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1866 1714 145 145 0 1721 0 [pid=25647] vsize: 7464 Current children cumulated CPU time (s) 359.88 Current children cumulated vsize (Kb) 9588 [startup+370.032 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1731 0 0 0 36975 12 0 0 25 0 1 0 1797722620 7659520 1717 4294967295 134512640 135094434 3221224432 3221223088 134557849 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1870 1717 145 145 0 1725 0 [pid=25647] vsize: 7480 Current children cumulated CPU time (s) 369.88 Current children cumulated vsize (Kb) 9604 [startup+380.033 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1732 0 0 0 37975 12 0 0 25 0 1 0 1797722620 7659520 1718 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1870 1718 145 145 0 1725 0 [pid=25647] vsize: 7480 Current children cumulated CPU time (s) 379.88 Current children cumulated vsize (Kb) 9604 [startup+390.033 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1734 0 0 0 38975 12 0 0 25 0 1 0 1797722620 7667712 1720 4294967295 134512640 135094434 3221224432 3221223088 134558156 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1872 1720 145 145 0 1727 0 [pid=25647] vsize: 7488 Current children cumulated CPU time (s) 389.88 Current children cumulated vsize (Kb) 9612 [startup+400.035 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1759 0 0 0 39975 12 0 0 25 0 1 0 1797722620 7786496 1745 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1901 1745 145 145 0 1756 0 [pid=25647] vsize: 7604 Current children cumulated CPU time (s) 399.88 Current children cumulated vsize (Kb) 9728 [startup+410.035 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1763 0 0 0 40976 12 0 0 25 0 1 0 1797722620 7802880 1749 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1905 1749 145 145 0 1760 0 [pid=25647] vsize: 7620 Current children cumulated CPU time (s) 409.89 Current children cumulated vsize (Kb) 9744 [startup+420.036 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1770 0 0 0 41976 12 0 0 25 0 1 0 1797722620 7835648 1756 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1913 1756 145 145 0 1768 0 [pid=25647] vsize: 7652 Current children cumulated CPU time (s) 419.89 Current children cumulated vsize (Kb) 9776 [startup+430.037 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1830 0 0 0 42975 12 0 0 25 0 1 0 1797722620 8060928 1816 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1968 1816 145 145 0 1823 0 [pid=25647] vsize: 7872 Current children cumulated CPU time (s) 429.88 Current children cumulated vsize (Kb) 9996 [startup+440.038 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1846 0 0 0 43975 12 0 0 25 0 1 0 1797722620 8130560 1832 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1985 1832 145 145 0 1840 0 [pid=25647] vsize: 7940 Current children cumulated CPU time (s) 439.88 Current children cumulated vsize (Kb) 10064 [startup+450.038 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1854 0 0 0 44975 12 0 0 25 0 1 0 1797722620 8163328 1840 4294967295 134512640 135094434 3221224432 3221223120 134554705 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 1993 1840 145 145 0 1848 0 [pid=25647] vsize: 7972 Current children cumulated CPU time (s) 449.88 Current children cumulated vsize (Kb) 10096 [startup+460.039 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1856 0 0 0 45975 12 0 0 25 0 1 0 1797722620 8228864 1842 4294967295 134512640 135094434 3221224432 3221223088 134557925 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2009 1842 145 145 0 1864 0 [pid=25647] vsize: 8036 Current children cumulated CPU time (s) 459.88 Current children cumulated vsize (Kb) 10160 [startup+470.04 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1856 0 0 0 46976 12 0 0 25 0 1 0 1797722620 8228864 1842 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2009 1842 145 145 0 1864 0 [pid=25647] vsize: 8036 Current children cumulated CPU time (s) 469.89 Current children cumulated vsize (Kb) 10160 [startup+480.041 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1858 0 0 0 47976 12 0 0 25 0 1 0 1797722620 8228864 1844 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2009 1844 145 145 0 1864 0 [pid=25647] vsize: 8036 Current children cumulated CPU time (s) 479.89 Current children cumulated vsize (Kb) 10160 [startup+490.041 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1870 0 0 0 48976 12 0 0 25 0 1 0 1797722620 8269824 1856 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2019 1856 145 145 0 1874 0 [pid=25647] vsize: 8076 Current children cumulated CPU time (s) 489.89 Current children cumulated vsize (Kb) 10200 [startup+500.042 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1872 0 0 0 49976 12 0 0 25 0 1 0 1797722620 8318976 1858 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2031 1858 145 145 0 1886 0 [pid=25647] vsize: 8124 Current children cumulated CPU time (s) 499.89 Current children cumulated vsize (Kb) 10248 [startup+510.043 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1872 0 0 0 50976 12 0 0 25 0 1 0 1797722620 8318976 1858 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2031 1858 145 145 0 1886 0 [pid=25647] vsize: 8124 Current children cumulated CPU time (s) 509.89 Current children cumulated vsize (Kb) 10248 [startup+520.044 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1877 0 0 0 51977 12 0 0 25 0 1 0 1797722620 8318976 1863 4294967295 134512640 135094434 3221224432 3221223120 134554793 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2031 1863 145 145 0 1886 0 [pid=25647] vsize: 8124 Current children cumulated CPU time (s) 519.9 Current children cumulated vsize (Kb) 10248 [startup+530.044 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1883 0 0 0 52976 12 0 0 25 0 1 0 1797722620 8347648 1869 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2038 1869 145 145 0 1893 0 [pid=25647] vsize: 8152 Current children cumulated CPU time (s) 529.89 Current children cumulated vsize (Kb) 10276 [startup+540.045 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1884 0 0 0 53977 12 0 0 25 0 1 0 1797722620 8347648 1870 4294967295 134512640 135094434 3221224432 3221223084 134558036 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2038 1870 145 145 0 1893 0 [pid=25647] vsize: 8152 Current children cumulated CPU time (s) 539.9 Current children cumulated vsize (Kb) 10276 [startup+550.046 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1965 0 0 0 54974 13 0 0 25 0 1 0 1797722620 8675328 1951 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2118 1951 145 145 0 1973 0 [pid=25647] vsize: 8472 Current children cumulated CPU time (s) 549.88 Current children cumulated vsize (Kb) 10596 [startup+560.047 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1975 0 0 0 55975 13 0 0 25 0 1 0 1797722620 8732672 1961 4294967295 134512640 135094434 3221224432 3221223088 134557792 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2132 1961 145 145 0 1987 0 [pid=25647] vsize: 8528 Current children cumulated CPU time (s) 559.89 Current children cumulated vsize (Kb) 10652 [startup+570.047 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1976 0 0 0 56975 13 0 0 25 0 1 0 1797722620 8732672 1962 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2132 1962 145 145 0 1987 0 [pid=25647] vsize: 8528 Current children cumulated CPU time (s) 569.89 Current children cumulated vsize (Kb) 10652 [startup+580.048 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 1980 0 0 0 57975 13 0 0 25 0 1 0 1797722620 8749056 1966 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2136 1966 145 145 0 1991 0 [pid=25647] vsize: 8544 Current children cumulated CPU time (s) 579.89 Current children cumulated vsize (Kb) 10668 [startup+590.049 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2040 0 0 0 58974 14 0 0 25 0 1 0 1797722620 8982528 2026 4294967295 134512640 135094434 3221224432 3221223088 134558162 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2193 2026 145 145 0 2048 0 [pid=25647] vsize: 8772 Current children cumulated CPU time (s) 589.89 Current children cumulated vsize (Kb) 10896 [startup+600.051 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2043 0 0 0 59974 14 0 0 25 0 1 0 1797722620 8998912 2029 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2197 2029 145 145 0 2052 0 [pid=25647] vsize: 8788 Current children cumulated CPU time (s) 599.89 Current children cumulated vsize (Kb) 10912 [startup+610.052 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2054 0 0 0 60974 14 0 0 25 0 1 0 1797722620 9097216 2040 4294967295 134512640 135094434 3221224432 3221223088 134558011 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2221 2040 145 145 0 2076 0 [pid=25647] vsize: 8884 Current children cumulated CPU time (s) 609.89 Current children cumulated vsize (Kb) 11008 [startup+620.052 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2055 0 0 0 61975 14 0 0 25 0 1 0 1797722620 9097216 2041 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2221 2041 145 145 0 2076 0 [pid=25647] vsize: 8884 Current children cumulated CPU time (s) 619.9 Current children cumulated vsize (Kb) 11008 [startup+630.053 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2055 0 0 0 62975 14 0 0 25 0 1 0 1797722620 9097216 2041 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2221 2041 145 145 0 2076 0 [pid=25647] vsize: 8884 Current children cumulated CPU time (s) 629.9 Current children cumulated vsize (Kb) 11008 [startup+640.053 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2055 0 0 0 63975 14 0 0 25 0 1 0 1797722620 9097216 2041 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2221 2041 145 145 0 2076 0 [pid=25647] vsize: 8884 Current children cumulated CPU time (s) 639.9 Current children cumulated vsize (Kb) 11008 [startup+650.054 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2059 0 0 0 64975 14 0 0 25 0 1 0 1797722620 9097216 2045 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2221 2045 145 145 0 2076 0 [pid=25647] vsize: 8884 Current children cumulated CPU time (s) 649.9 Current children cumulated vsize (Kb) 11008 [startup+660.055 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2059 0 0 0 65976 14 0 0 25 0 1 0 1797722620 9097216 2045 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2221 2045 145 145 0 2076 0 [pid=25647] vsize: 8884 Current children cumulated CPU time (s) 659.91 Current children cumulated vsize (Kb) 11008 [startup+670.056 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2089 0 0 0 66975 14 0 0 25 0 1 0 1797722620 9220096 2075 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2251 2075 145 145 0 2106 0 [pid=25647] vsize: 9004 Current children cumulated CPU time (s) 669.9 Current children cumulated vsize (Kb) 11128 [startup+680.056 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2091 0 0 0 67975 14 0 0 25 0 1 0 1797722620 9228288 2077 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2253 2077 145 145 0 2108 0 [pid=25647] vsize: 9012 Current children cumulated CPU time (s) 679.9 Current children cumulated vsize (Kb) 11136 [startup+690.057 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2100 0 0 0 68975 14 0 0 25 0 1 0 1797722620 9261056 2086 4294967295 134512640 135094434 3221224432 3221223056 134557702 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2261 2086 145 145 0 2116 0 [pid=25647] vsize: 9044 Current children cumulated CPU time (s) 689.9 Current children cumulated vsize (Kb) 11168 [startup+700.059 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2100 0 0 0 69975 15 0 0 25 0 1 0 1797722620 9261056 2086 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2261 2086 145 145 0 2116 0 [pid=25647] vsize: 9044 Current children cumulated CPU time (s) 699.91 Current children cumulated vsize (Kb) 11168 [startup+710.06 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2174 0 0 0 70973 15 0 0 25 0 1 0 1797722620 9572352 2160 4294967295 134512640 135094434 3221224432 3221223104 134555413 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2337 2160 145 145 0 2192 0 [pid=25647] vsize: 9348 Current children cumulated CPU time (s) 709.89 Current children cumulated vsize (Kb) 11472 [startup+720.06 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2190 0 0 0 71973 16 0 0 25 0 1 0 1797722620 9646080 2176 4294967295 134512640 135094434 3221224432 3221223088 134557914 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2355 2176 145 145 0 2210 0 [pid=25647] vsize: 9420 Current children cumulated CPU time (s) 719.9 Current children cumulated vsize (Kb) 11544 [startup+730.061 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2196 0 0 0 72973 16 0 0 25 0 1 0 1797722620 9662464 2182 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2359 2182 145 145 0 2214 0 [pid=25647] vsize: 9436 Current children cumulated CPU time (s) 729.9 Current children cumulated vsize (Kb) 11560 [startup+740.062 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2196 0 0 0 73974 16 0 0 25 0 1 0 1797722620 9662464 2182 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2359 2182 145 145 0 2214 0 [pid=25647] vsize: 9436 Current children cumulated CPU time (s) 739.91 Current children cumulated vsize (Kb) 11560 [startup+750.063 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2196 0 0 0 74974 16 0 0 25 0 1 0 1797722620 9662464 2182 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2359 2182 145 145 0 2214 0 [pid=25647] vsize: 9436 Current children cumulated CPU time (s) 749.91 Current children cumulated vsize (Kb) 11560 [startup+760.063 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2211 0 0 0 75974 16 0 0 25 0 1 0 1797722620 9760768 2197 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2383 2197 145 145 0 2238 0 [pid=25647] vsize: 9532 Current children cumulated CPU time (s) 759.91 Current children cumulated vsize (Kb) 11656 [startup+770.063 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2212 0 0 0 76974 16 0 0 25 0 1 0 1797722620 9760768 2198 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2383 2198 145 145 0 2238 0 [pid=25647] vsize: 9532 Current children cumulated CPU time (s) 769.91 Current children cumulated vsize (Kb) 11656 [startup+780.064 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2213 0 0 0 77974 16 0 0 25 0 1 0 1797722620 9760768 2199 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2383 2199 145 145 0 2238 0 [pid=25647] vsize: 9532 Current children cumulated CPU time (s) 779.91 Current children cumulated vsize (Kb) 11656 [startup+790.065 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2213 0 0 0 78974 16 0 0 25 0 1 0 1797722620 9760768 2199 4294967295 134512640 135094434 3221224432 3221223056 134557726 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2383 2199 145 145 0 2238 0 [pid=25647] vsize: 9532 Current children cumulated CPU time (s) 789.91 Current children cumulated vsize (Kb) 11656 [startup+800.065 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2213 0 0 0 79975 16 0 0 25 0 1 0 1797722620 9760768 2199 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2383 2199 145 145 0 2238 0 [pid=25647] vsize: 9532 Current children cumulated CPU time (s) 799.92 Current children cumulated vsize (Kb) 11656 [startup+810.066 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2213 0 0 0 80975 16 0 0 25 0 1 0 1797722620 9760768 2199 4294967295 134512640 135094434 3221224432 3221223088 134557882 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2383 2199 145 145 0 2238 0 [pid=25647] vsize: 9532 Current children cumulated CPU time (s) 809.92 Current children cumulated vsize (Kb) 11656 [startup+820.067 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2214 0 0 0 81975 16 0 0 25 0 1 0 1797722620 9760768 2200 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2383 2200 145 145 0 2238 0 [pid=25647] vsize: 9532 Current children cumulated CPU time (s) 819.92 Current children cumulated vsize (Kb) 11656 [startup+830.068 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2215 0 0 0 82975 16 0 0 25 0 1 0 1797722620 9760768 2201 4294967295 134512640 135094434 3221224432 3221223088 134558141 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2383 2201 145 145 0 2238 0 [pid=25647] vsize: 9532 Current children cumulated CPU time (s) 829.92 Current children cumulated vsize (Kb) 11656 [startup+840.068 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2215 0 0 0 83976 16 0 0 25 0 1 0 1797722620 9760768 2201 4294967295 134512640 135094434 3221224432 3221223056 134557636 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2383 2201 145 145 0 2238 0 [pid=25647] vsize: 9532 Current children cumulated CPU time (s) 839.93 Current children cumulated vsize (Kb) 11656 [startup+850.069 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2248 0 0 0 84976 16 0 0 25 0 1 0 1797722620 10022912 2234 4294967295 134512640 135094434 3221224432 3221223088 134557882 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2447 2234 145 145 0 2302 0 [pid=25647] vsize: 9788 Current children cumulated CPU time (s) 849.93 Current children cumulated vsize (Kb) 11912 [startup+860.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2248 0 0 0 85976 16 0 0 25 0 1 0 1797722620 10022912 2234 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2447 2234 145 145 0 2302 0 [pid=25647] vsize: 9788 Current children cumulated CPU time (s) 859.93 Current children cumulated vsize (Kb) 11912 [startup+870.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2248 0 0 0 86976 16 0 0 25 0 1 0 1797722620 10022912 2234 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2447 2234 145 145 0 2302 0 [pid=25647] vsize: 9788 Current children cumulated CPU time (s) 869.93 Current children cumulated vsize (Kb) 11912 [startup+880.071 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2248 0 0 0 87977 16 0 0 25 0 1 0 1797722620 10022912 2234 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2447 2234 145 145 0 2302 0 [pid=25647] vsize: 9788 Current children cumulated CPU time (s) 879.94 Current children cumulated vsize (Kb) 11912 [startup+890.072 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2248 0 0 0 88977 16 0 0 25 0 1 0 1797722620 10022912 2234 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2447 2234 145 145 0 2302 0 [pid=25647] vsize: 9788 Current children cumulated CPU time (s) 889.94 Current children cumulated vsize (Kb) 11912 [startup+900.073 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2269 0 0 0 89977 16 0 0 25 0 1 0 1797722620 10153984 2255 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2479 2255 145 145 0 2334 0 [pid=25647] vsize: 9916 Current children cumulated CPU time (s) 899.94 Current children cumulated vsize (Kb) 12040 [startup+910.074 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2269 0 0 0 90977 16 0 0 25 0 1 0 1797722620 10153984 2255 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2479 2255 145 145 0 2334 0 [pid=25647] vsize: 9916 Current children cumulated CPU time (s) 909.94 Current children cumulated vsize (Kb) 12040 [startup+920.073 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2269 0 0 0 91977 16 0 0 25 0 1 0 1797722620 10153984 2255 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2479 2255 145 145 0 2334 0 [pid=25647] vsize: 9916 Current children cumulated CPU time (s) 919.94 Current children cumulated vsize (Kb) 12040 [startup+930.074 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2269 0 0 0 92978 16 0 0 25 0 1 0 1797722620 10153984 2255 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2479 2255 145 145 0 2334 0 [pid=25647] vsize: 9916 Current children cumulated CPU time (s) 929.95 Current children cumulated vsize (Kb) 12040 [startup+940.075 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2270 0 0 0 93978 16 0 0 25 0 1 0 1797722620 10153984 2256 4294967295 134512640 135094434 3221224432 3221223088 134558254 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2479 2256 145 145 0 2334 0 [pid=25647] vsize: 9916 Current children cumulated CPU time (s) 939.95 Current children cumulated vsize (Kb) 12040 [startup+950.076 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2270 0 0 0 94978 16 0 0 25 0 1 0 1797722620 10153984 2256 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2479 2256 145 145 0 2334 0 [pid=25647] vsize: 9916 Current children cumulated CPU time (s) 949.95 Current children cumulated vsize (Kb) 12040 [startup+960.076 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2272 0 0 0 95979 16 0 0 25 0 1 0 1797722620 10153984 2258 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2479 2258 145 145 0 2334 0 [pid=25647] vsize: 9916 Current children cumulated CPU time (s) 959.96 Current children cumulated vsize (Kb) 12040 [startup+970.077 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2272 0 0 0 96979 16 0 0 25 0 1 0 1797722620 10153984 2258 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2479 2258 145 145 0 2334 0 [pid=25647] vsize: 9916 Current children cumulated CPU time (s) 969.96 Current children cumulated vsize (Kb) 12040 [startup+980.078 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2294 0 0 0 97978 16 0 0 25 0 1 0 1797722620 10285056 2280 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25647/statm): 2511 2280 145 145 0 2366 0 [pid=25647] vsize: 10044 Current children cumulated CPU time (s) 979.95 Current children cumulated vsize (Kb) 12168 [startup+990.079 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2295 0 0 0 98978 16 0 0 25 0 1 0 1797722620 10285056 2281 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2511 2281 145 145 0 2366 0 [pid=25647] vsize: 10044 Current children cumulated CPU time (s) 989.95 Current children cumulated vsize (Kb) 12168 [startup+1000.08 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2297 0 0 0 99978 16 0 0 25 0 1 0 1797722620 10285056 2283 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2511 2283 145 145 0 2366 0 [pid=25647] vsize: 10044 Current children cumulated CPU time (s) 999.95 Current children cumulated vsize (Kb) 12168 [startup+1010.08 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2301 0 0 0 100978 16 0 0 25 0 1 0 1797722620 10293248 2287 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2513 2287 145 145 0 2368 0 [pid=25647] vsize: 10052 Current children cumulated CPU time (s) 1009.95 Current children cumulated vsize (Kb) 12176 [startup+1020.08 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2307 0 0 0 101978 16 0 0 25 0 1 0 1797722620 10326016 2293 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2521 2293 145 145 0 2376 0 [pid=25647] vsize: 10084 Current children cumulated CPU time (s) 1019.95 Current children cumulated vsize (Kb) 12208 [startup+1030.08 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2307 0 0 0 102978 16 0 0 25 0 1 0 1797722620 10326016 2293 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2521 2293 145 145 0 2376 0 [pid=25647] vsize: 10084 Current children cumulated CPU time (s) 1029.95 Current children cumulated vsize (Kb) 12208 [startup+1040.08 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2307 0 0 0 103979 17 0 0 25 0 1 0 1797722620 10326016 2293 4294967295 134512640 135094434 3221224432 3221223056 134562088 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2521 2293 145 145 0 2376 0 [pid=25647] vsize: 10084 Current children cumulated CPU time (s) 1039.97 Current children cumulated vsize (Kb) 12208 [startup+1050.08 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2308 0 0 0 104979 17 0 0 25 0 1 0 1797722620 10326016 2294 4294967295 134512640 135094434 3221224432 3221223088 134557914 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2521 2294 145 145 0 2376 0 [pid=25647] vsize: 10084 Current children cumulated CPU time (s) 1049.97 Current children cumulated vsize (Kb) 12208 [startup+1060.08 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2317 0 0 0 105979 17 0 0 25 0 1 0 1797722620 10391552 2303 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2537 2303 145 145 0 2392 0 [pid=25647] vsize: 10148 Current children cumulated CPU time (s) 1059.97 Current children cumulated vsize (Kb) 12272 [startup+1070.08 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2337 0 0 0 106979 17 0 0 25 0 1 0 1797722620 10473472 2323 4294967295 134512640 135094434 3221224432 3221223056 134557726 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2557 2323 145 145 0 2412 0 [pid=25647] vsize: 10228 Current children cumulated CPU time (s) 1069.97 Current children cumulated vsize (Kb) 12352 [startup+1080.08 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2344 0 0 0 107979 17 0 0 25 0 1 0 1797722620 10502144 2330 4294967295 134512640 135094434 3221224432 3221223072 134562085 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2564 2330 145 145 0 2419 0 [pid=25647] vsize: 10256 Current children cumulated CPU time (s) 1079.97 Current children cumulated vsize (Kb) 12380 [startup+1090.09 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2344 0 0 0 108979 17 0 0 25 0 1 0 1797722620 10502144 2330 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2564 2330 145 145 0 2419 0 [pid=25647] vsize: 10256 Current children cumulated CPU time (s) 1089.97 Current children cumulated vsize (Kb) 12380 [startup+1100.09 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2354 0 0 0 109979 17 0 0 25 0 1 0 1797722620 10567680 2340 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2580 2340 145 145 0 2435 0 [pid=25647] vsize: 10320 Current children cumulated CPU time (s) 1099.97 Current children cumulated vsize (Kb) 12444 [startup+1110.09 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2355 0 0 0 110980 17 0 0 25 0 1 0 1797722620 10567680 2341 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2580 2341 145 145 0 2435 0 [pid=25647] vsize: 10320 Current children cumulated CPU time (s) 1109.98 Current children cumulated vsize (Kb) 12444 [startup+1120.09 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2355 0 0 0 111980 17 0 0 25 0 1 0 1797722620 10567680 2341 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2580 2341 145 145 0 2435 0 [pid=25647] vsize: 10320 Current children cumulated CPU time (s) 1119.98 Current children cumulated vsize (Kb) 12444 [startup+1130.09 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2355 0 0 0 112980 17 0 0 25 0 1 0 1797722620 10567680 2341 4294967295 134512640 135094434 3221224432 3221223104 134555599 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2580 2341 145 145 0 2435 0 [pid=25647] vsize: 10320 Current children cumulated CPU time (s) 1129.98 Current children cumulated vsize (Kb) 12444 [startup+1140.09 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2356 0 0 0 113980 17 0 0 25 0 1 0 1797722620 10567680 2342 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2580 2342 145 145 0 2435 0 [pid=25647] vsize: 10320 Current children cumulated CPU time (s) 1139.98 Current children cumulated vsize (Kb) 12444 [startup+1150.09 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2356 0 0 0 114981 17 0 0 25 0 1 0 1797722620 10567680 2342 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2580 2342 145 145 0 2435 0 [pid=25647] vsize: 10320 Current children cumulated CPU time (s) 1149.99 Current children cumulated vsize (Kb) 12444 [startup+1160.09 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2356 0 0 0 115981 17 0 0 25 0 1 0 1797722620 10567680 2342 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2580 2342 145 145 0 2435 0 [pid=25647] vsize: 10320 Current children cumulated CPU time (s) 1159.99 Current children cumulated vsize (Kb) 12444 [startup+1170.09 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2356 0 0 0 116981 17 0 0 25 0 1 0 1797722620 10567680 2342 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2580 2342 145 145 0 2435 0 [pid=25647] vsize: 10320 Current children cumulated CPU time (s) 1169.99 Current children cumulated vsize (Kb) 12444 [startup+1180.09 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2356 0 0 0 117981 17 0 0 25 0 1 0 1797722620 10567680 2342 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2580 2342 145 145 0 2435 0 [pid=25647] vsize: 10320 Current children cumulated CPU time (s) 1179.99 Current children cumulated vsize (Kb) 12444 [startup+1190.09 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2356 0 0 0 118982 17 0 0 25 0 1 0 1797722620 10567680 2342 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2580 2342 145 145 0 2435 0 [pid=25647] vsize: 10320 Current children cumulated CPU time (s) 1190 Current children cumulated vsize (Kb) 12444 [startup+1200.09 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2356 0 0 0 119982 17 0 0 25 0 1 0 1797722620 10567680 2342 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2580 2342 145 145 0 2435 0 [pid=25647] vsize: 10320 Current children cumulated CPU time (s) 1200 Current children cumulated vsize (Kb) 12444 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1200.1 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 25647 Raw data (/proc/25643/stat): 25643 (minisat+_script) S 25642 25643 824 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1797722615 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25643/statm): 531 226 485 147 0 384 0 [pid=25643] vsize: 2124 Raw data (/proc/25647/stat): 25647 (minisat+_64-bit) R 25643 25643 824 0 -1 0 2356 0 0 0 119982 17 0 0 25 0 1 0 1797722620 10567680 2342 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25647/statm): 2580 2342 145 145 0 2435 0 [pid=25647] vsize: 10320 Current children cumulated CPU time (s) 1200 Current children cumulated vsize (Kb) 12444 Sending SIGTERM to -25643 Sleeping 2 seconds One traced child (pid=25643) ended because it received signal 15 (SIGTERM) One traced child (pid=25647) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1200.11 CPU time (s): 1200 CPU user time (s): 1199.83 CPU system time (s): 0.177972 CPU usage (%): 99.9916 Max. virtual memory (cumulated for all children) (Kb): 12444
ERROR: no interpretation found !