Name | mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-nsrand-ipx.opb |
MD5SUM | 6b39a5ca45e18a6e9e3dc91f7594e22c |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 1258323967 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 31 |
Biggest coefficient in the objective function | 1073741824 |
Number of bits for the biggest coefficient in the objective function | 31 |
Sum of the numbers in the objective function | 2147483647 |
Number of bits of the sum of numbers in the objective function | 31 |
Biggest number in a constraint | 1073741824 |
Number of bits of the biggest number in a constraint | 31 |
Biggest sum of numbers in a constraint | 26715880447 |
Number of bits of the biggest sum of numbers | 35 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1195.13 |
Number of variables | 6651 |
Total number of constraints | 7355 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 6951 |
Number of constraints which are nor clauses,nor cardinality constraints | 404 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 6651 |
LAUNCH ON wulflinc1 THE 2005-09-19 17:43:10 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2956 boxname=wulflinc1 idbench=612 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 6b39a5ca45e18a6e9e3dc91f7594e22c /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-nsrand-ipx.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-nsrand-ipx.opb IDLAUNCH: 2956 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.053 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.053 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: 935988 kB Buffers: 2036 kB Cached: 66828 kB SwapCached: 1176 kB Active: 17832 kB Inactive: 53640 kB HighTotal: 131008 kB HighFree: 60452 kB LowTotal: 903652 kB LowFree: 875536 kB SwapTotal: 2097136 kB SwapFree: 2095264 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5740 kB Slab: 21396 kB Committed_AS: 92588 kB PageTables: 332 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-19 18:03:21 (client local time) WITH STATUS 0 IN 1208.5 SECONDS stats: 2956 7 1208.5 0
c Parsing PB file... c Converting 721 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ===== c -- Clauses(.)/Splits(s): sssssssss.s.ssss.ssss.ssssss.ssss..ssss..s.ssssssss.s.s.s.s.s.sss.sssss.ss.s.ss.s.ss.sssssssssssss.ssss.ssssssss.s.sssss.sss.ss.s.ss.sssssssssssssssssssssssssssssssssssssssssssss..sssssssssssssssssssss.sssss.sssssssss.ss.ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss..sss.sssssssss.ssss.ssssssssssssss.ssssssssss.s.s.ssssssssssss.ss.ss.ss c ---[1049]---> Adder-cost: 38230 maxlim: 24568396799 bits: 35/35 c ---[1048]---> BDD-cost: 37 c ---[1047]---> BDD-cost: 37 c ---[1046]---> BDD-cost: 37 c ---[1045]---> BDD-cost: 37 c ---[1044]---> BDD-cost: 37 c ---[1043]---> BDD-cost: 37 c ---[1042]---> BDD-cost: 37 c ---[1041]---> BDD-cost: 37 c ---[1040]---> BDD-cost: 37 c ---[1039]---> BDD-cost: 37 c ---[1038]---> BDD-cost: 37 c ---[1037]---> BDD-cost: 37 c ---[1036]---> BDD-cost: 37 c ---[1035]---> BDD-cost: 37 c ---[1034]---> BDD-cost: 37 c ---[1033]---> BDD-cost: 37 c ---[1032]---> BDD-cost: 37 c ---[1031]---> BDD-cost: 37 c ---[1030]---> BDD-cost: 37 c ---[1029]---> BDD-cost: 37 c ---[1028]---> BDD-cost: 37 c ---[1027]---> BDD-cost: 37 c ---[1026]---> BDD-cost: 37 c ---[1025]---> BDD-cost: 37 c ---[1024]---> BDD-cost: 37 c ---[1023]---> BDD-cost: 37 c ---[1022]---> BDD-cost: 37 c ---[1021]---> BDD-cost: 37 c ---[1020]---> BDD-cost: 37 c ---[1019]---> BDD-cost: 37 c ---[1018]---> BDD-cost: 37 c ---[1017]---> BDD-cost: 37 c ---[1016]---> BDD-cost: 37 c ---[1015]---> BDD-cost: 37 c ---[1014]---> BDD-cost: 37 c ---[1013]---> BDD-cost: 37 c ---[1012]---> BDD-cost: 37 c ---[1011]---> BDD-cost: 37 c ---[1010]---> BDD-cost: 37 c ---[1009]---> BDD-cost: 37 c ---[1008]---> BDD-cost: 37 c ---[1007]---> BDD-cost: 37 c ---[1006]---> BDD-cost: 37 c ---[1005]---> BDD-cost: 37 c ---[1004]---> BDD-cost: 37 c ---[1003]---> BDD-cost: 37 c ---[1002]---> BDD-cost: 37 c ---[1001]---> BDD-cost: 37 c ---[1000]---> BDD-cost: 37 c ---[ 999]---> BDD-cost: 37 c ---[ 998]---> BDD-cost: 37 c ---[ 997]---> BDD-cost: 37 c ---[ 996]---> BDD-cost: 37 c ---[ 995]---> BDD-cost: 37 c ---[ 994]---> BDD-cost: 37 c ---[ 993]---> BDD-cost: 37 c ---[ 992]---> BDD-cost: 37 c ---[ 991]---> BDD-cost: 37 c ---[ 990]---> BDD-cost: 37 c ---[ 989]---> BDD-cost: 37 c ---[ 988]---> BDD-cost: 37 c ---[ 987]---> BDD-cost: 37 c ---[ 986]---> BDD-cost: 37 c ---[ 985]---> BDD-cost: 37 c ---[ 984]---> BDD-cost: 37 c ---[ 983]---> BDD-cost: 37 c ---[ 982]---> BDD-cost: 37 c ---[ 981]---> BDD-cost: 37 c ---[ 980]---> BDD-cost: 37 c ---[ 979]---> BDD-cost: 37 c ---[ 978]---> BDD-cost: 37 c ---[ 977]---> BDD-cost: 37 c ---[ 976]---> BDD-cost: 37 c ---[ 975]---> BDD-cost: 37 c ---[ 974]---> BDD-cost: 37 c ---[ 973]---> BDD-cost: 37 c ---[ 972]---> BDD-cost: 37 c ---[ 971]---> BDD-cost: 37 c ---[ 970]---> BDD-cost: 37 c ---[ 969]---> BDD-cost: 37 c ---[ 968]---> BDD-cost: 37 c ---[ 967]---> BDD-cost: 37 c ---[ 966]---> BDD-cost: 37 c ---[ 965]---> BDD-cost: 37 c ---[ 964]---> BDD-cost: 37 c ---[ 963]---> BDD-cost: 37 c ---[ 962]---> BDD-cost: 37 c ---[ 961]---> BDD-cost: 37 c ---[ 960]---> BDD-cost: 37 c ---[ 959]---> BDD-cost: 37 c ---[ 958]---> BDD-cost: 37 c ---[ 957]---> BDD-cost: 37 c ---[ 956]---> BDD-cost: 37 c ---[ 955]---> BDD-cost: 37 c ---[ 954]---> BDD-cost: 37 c ---[ 953]---> BDD-cost: 37 c ---[ 952]---> BDD-cost: 37 c ---[ 951]---> BDD-cost: 37 c ---[ 950]---> BDD-cost: 37 c ---[ 949]---> BDD-cost: 37 c ---[ 948]---> BDD-cost: 37 c ---[ 947]---> BDD-cost: 37 c ---[ 946]---> BDD-cost: 37 c ---[ 945]---> BDD-cost: 37 c ---[ 944]---> BDD-cost: 37 c ---[ 943]---> BDD-cost: 37 c ---[ 942]---> BDD-cost: 37 c ---[ 941]---> BDD-cost: 37 c ---[ 940]---> BDD-cost: 37 c ---[ 939]---> BDD-cost: 37 c ---[ 938]---> BDD-cost: 37 c ---[ 937]---> BDD-cost: 37 c ---[ 936]---> BDD-cost: 37 c ---[ 935]---> BDD-cost: 37 c ---[ 934]---> BDD-cost: 37 c ---[ 933]---> BDD-cost: 37 c ---[ 932]---> BDD-cost: 37 c ---[ 931]---> BDD-cost: 37 c ---[ 930]---> BDD-cost: 37 c ---[ 929]---> BDD-cost: 37 c ---[ 928]---> BDD-cost: 37 c ---[ 927]---> BDD-cost: 37 c ---[ 926]---> BDD-cost: 37 c ---[ 925]---> BDD-cost: 37 c ---[ 924]---> BDD-cost: 37 c ---[ 923]---> BDD-cost: 37 c ---[ 922]---> BDD-cost: 37 c ---[ 921]---> BDD-cost: 37 c ---[ 920]---> BDD-cost: 37 c ---[ 919]---> BDD-cost: 37 c ---[ 918]---> BDD-cost: 37 c ---[ 917]---> BDD-cost: 37 c ---[ 916]---> BDD-cost: 37 c ---[ 915]---> BDD-cost: 37 c ---[ 914]---> BDD-cost: 37 c ---[ 913]---> BDD-cost: 37 c ---[ 912]---> BDD-cost: 37 c ---[ 911]---> BDD-cost: 37 c ---[ 910]---> BDD-cost: 37 c ---[ 909]---> BDD-cost: 37 c ---[ 908]---> BDD-cost: 37 c ---[ 907]---> BDD-cost: 37 c ---[ 906]---> BDD-cost: 37 c ---[ 905]---> BDD-cost: 37 c ---[ 904]---> BDD-cost: 37 c ---[ 903]---> BDD-cost: 37 c ---[ 902]---> BDD-cost: 37 c ---[ 901]---> BDD-cost: 37 c ---[ 900]---> BDD-cost: 37 c ---[ 899]---> BDD-cost: 37 c ---[ 898]---> BDD-cost: 37 c ---[ 897]---> BDD-cost: 37 c ---[ 896]---> BDD-cost: 37 c ---[ 895]---> BDD-cost: 37 c ---[ 894]---> BDD-cost: 37 c ---[ 893]---> BDD-cost: 37 c ---[ 892]---> BDD-cost: 37 c ---[ 891]---> BDD-cost: 37 c ---[ 890]---> BDD-cost: 37 c ---[ 889]---> BDD-cost: 37 c ---[ 888]---> BDD-cost: 37 c ---[ 887]---> BDD-cost: 37 c ---[ 886]---> BDD-cost: 37 c ---[ 885]---> BDD-cost: 37 c ---[ 884]---> BDD-cost: 37 c ---[ 883]---> BDD-cost: 37 c ---[ 882]---> BDD-cost: 37 c ---[ 881]---> BDD-cost: 37 c ---[ 880]---> BDD-cost: 37 c ---[ 879]---> BDD-cost: 37 c ---[ 878]---> BDD-cost: 37 c ---[ 877]---> BDD-cost: 37 c ---[ 876]---> BDD-cost: 37 c ---[ 875]---> BDD-cost: 37 c ---[ 874]---> BDD-cost: 37 c ---[ 873]---> BDD-cost: 37 c ---[ 872]---> BDD-cost: 37 c ---[ 871]---> BDD-cost: 37 c ---[ 870]---> BDD-cost: 37 c ---[ 869]---> BDD-cost: 37 c ---[ 868]---> BDD-cost: 37 c ---[ 867]---> BDD-cost: 37 c ---[ 866]---> BDD-cost: 37 c ---[ 865]---> BDD-cost: 37 c ---[ 864]---> BDD-cost: 37 c ---[ 863]---> BDD-cost: 37 c ---[ 862]---> BDD-cost: 37 c ---[ 861]---> BDD-cost: 37 c ---[ 860]---> BDD-cost: 37 c ---[ 859]---> BDD-cost: 37 c ---[ 858]---> BDD-cost: 37 c ---[ 857]---> BDD-cost: 37 c ---[ 856]---> BDD-cost: 37 c ---[ 855]---> BDD-cost: 37 c ---[ 854]---> BDD-cost: 37 c ---[ 853]---> BDD-cost: 37 c ---[ 852]---> BDD-cost: 37 c ---[ 851]---> BDD-cost: 37 c ---[ 850]---> BDD-cost: 37 c ---[ 849]---> BDD-cost: 37 c ---[ 848]---> BDD-cost: 37 c ---[ 847]---> BDD-cost: 37 c ---[ 846]---> BDD-cost: 37 c ---[ 845]---> BDD-cost: 37 c ---[ 844]---> BDD-cost: 37 c ---[ 843]---> BDD-cost: 37 c ---[ 842]---> BDD-cost: 37 c ---[ 841]---> BDD-cost: 37 c ---[ 840]---> BDD-cost: 37 c ---[ 839]---> BDD-cost: 37 c ---[ 838]---> BDD-cost: 37 c ---[ 837]---> BDD-cost: 37 c ---[ 836]---> BDD-cost: 37 c ---[ 835]---> BDD-cost: 37 c ---[ 834]---> BDD-cost: 37 c ---[ 833]---> BDD-cost: 37 c ---[ 832]---> BDD-cost: 37 c ---[ 831]---> BDD-cost: 37 c ---[ 830]---> BDD-cost: 37 c ---[ 829]---> BDD-cost: 37 c ---[ 828]---> BDD-cost: 37 c ---[ 827]---> BDD-cost: 37 c ---[ 826]---> BDD-cost: 37 c ---[ 825]---> BDD-cost: 37 c ---[ 824]---> BDD-cost: 37 c ---[ 823]---> BDD-cost: 37 c ---[ 822]---> BDD-cost: 37 c ---[ 821]---> BDD-cost: 37 c ---[ 820]---> BDD-cost: 37 c ---[ 819]---> BDD-cost: 37 c ---[ 818]---> BDD-cost: 37 c ---[ 817]---> BDD-cost: 37 c ---[ 816]---> BDD-cost: 37 c ---[ 815]---> BDD-cost: 37 c ---[ 814]---> BDD-cost: 37 c ---[ 813]---> BDD-cost: 37 c ---[ 812]---> BDD-cost: 37 c ---[ 811]---> BDD-cost: 37 c ---[ 810]---> BDD-cost: 37 c ---[ 809]---> BDD-cost: 37 c ---[ 808]---> BDD-cost: 37 c ---[ 807]---> BDD-cost: 37 c ---[ 806]---> BDD-cost: 37 c ---[ 805]---> BDD-cost: 37 c ---[ 804]---> BDD-cost: 37 c ---[ 803]---> BDD-cost: 37 c ---[ 802]---> BDD-cost: 37 c ---[ 801]---> BDD-cost: 37 c ---[ 800]---> BDD-cost: 37 c ---[ 799]---> BDD-cost: 37 c ---[ 798]---> BDD-cost: 37 c ---[ 797]---> BDD-cost: 37 c ---[ 796]---> BDD-cost: 37 c ---[ 795]---> BDD-cost: 37 c ---[ 794]---> BDD-cost: 37 c ---[ 793]---> BDD-cost: 37 c ---[ 792]---> BDD-cost: 37 c ---[ 791]---> BDD-cost: 37 c ---[ 790]---> BDD-cost: 37 c ---[ 783]---> BDD-cost: 37 c ---[ 772]---> BDD-cost: 37 c ---[ 761]---> BDD-cost: 37 c ---[ 750]---> BDD-cost: 37 c ---[ 739]---> BDD-cost: 37 c ---[ 728]---> BDD-cost: 37 c ---[ 717]---> BDD-cost: 37 c ---[ 716]---> BDD-cost: 37 c ---[ 705]---> BDD-cost: 37 c ---[ 694]---> BDD-cost: 37 c ---[ 683]---> BDD-cost: 37 c ---[ 672]---> BDD-cost: 37 c ---[ 661]---> BDD-cost: 37 c ---[ 650]---> BDD-cost: 37 c ---[ 639]---> BDD-cost: 37 c ---[ 628]---> BDD-cost: 37 c ---[ 617]---> BDD-cost: 37 c ---[ 608]---> BDD-cost: 37 c ---[ 607]---> BDD-cost: 37 c ---[ 600]---> Adder-cost: 2264 maxlim: 44 bits: 7/6 c ---[ 599]---> Adder-cost: 1410 maxlim: 36 bits: 7/6 c ---[ 598]---> Adder-cost: 1190 maxlim: 36 bits: 7/6 c ---[ 597]---> BDD-cost: 37 c ---[ 587]---> BDD-cost: 37 c ---[ 582]---> Adder-cost: 2364 maxlim: 37 bits: 7/6 c ---[ 581]---> Adder-cost: 1680 maxlim: 32 bits: 7/6 c ---[ 576]---> BDD-cost: 37 c ---[ 567]---> BDD-cost: 37 c ---[ 556]---> BDD-cost: 37 c ---[ 546]---> BDD-cost: 37 c ---[ 536]---> BDD-cost: 37 c ---[ 525]---> BDD-cost: 37 c ---[ 514]---> BDD-cost: 37 c ---[ 503]---> BDD-cost: 37 c ---[ 502]---> BDD-cost: 37 c ---[ 492]---> BDD-cost: 37 c ---[ 482]---> BDD-cost: 37 c ---[ 472]---> BDD-cost: 37 c ---[ 462]---> BDD-cost: 37 c ---[ 451]---> BDD-cost: 37 c ---[ 440]---> BDD-cost: 37 c ---[ 429]---> BDD-cost: 37 c ---[ 418]---> BDD-cost: 37 c ---[ 407]---> BDD-cost: 37 c ---[ 396]---> BDD-cost: 37 c ---[ 395]---> BDD-cost: 37 c ---[ 384]---> BDD-cost: 37 c ---[ 373]---> BDD-cost: 37 c ---[ 363]---> BDD-cost: 37 c ---[ 356]---> BDD-cost: 37 c ---[ 355]---> BDD-cost: 37 c ---[ 354]---> BDD-cost: 37 c ---[ 353]---> BDD-cost: 37 c ---[ 352]---> BDD-cost: 37 c ---[ 351]---> BDD-cost: 37 c ---[ 350]---> BDD-cost: 37 c ---[ 349]---> BDD-cost: 37 c ---[ 348]---> BDD-cost: 37 c ---[ 347]---> BDD-cost: 37 c ---[ 346]---> BDD-cost: 37 c ---[ 345]---> BDD-cost: 37 c ---[ 344]---> BDD-cost: 37 c ---[ 343]---> BDD-cost: 37 c ---[ 342]---> BDD-cost: 37 c ---[ 341]---> BDD-cost: 37 c ---[ 340]---> BDD-cost: 37 c ---[ 339]---> BDD-cost: 37 c ---[ 338]---> BDD-cost: 37 c ---[ 337]---> BDD-cost: 37 c ---[ 336]---> BDD-cost: 37 c ---[ 335]---> BDD-cost: 37 c ---[ 334]---> BDD-cost: 37 c ---[ 333]---> BDD-cost: 37 c ---[ 332]---> BDD-cost: 37 c ---[ 331]---> BDD-cost: 37 c ---[ 330]---> BDD-cost: 37 c ---[ 329]---> BDD-cost: 37 c ---[ 328]---> BDD-cost: 34 c ---[ 327]---> BDD-cost: 1577 c ---[ 326]---> Adder-cost: 1245 maxlim: 13 bits: 5/4 c ---[ 325]---> BDD-cost: 2212 c ---[ 324]---> Adder-cost: 791 maxlim: 11 bits: 5/4 c ---[ 323]---> BDD-cost: 930 c ---[ 322]---> Adder-cost: 626 maxlim: 14 bits: 5/4 c ---[ 321]---> Adder-cost: 344 maxlim: 10 bits: 5/4 c ---[ 320]---> Adder-cost: 366 maxlim: 13 bits: 5/4 c ---[ 319]---> BDD-cost: 36 c ---[ 318]---> BDD-cost: 1 c ---[ 317]---> Adder-cost: 375 maxlim: 12 bits: 5/4 c ---[ 316]---> BDD-cost: 816 c ---[ 315]---> Adder-cost: 159 maxlim: 11 bits: 5/4 c ---[ 314]---> BDD-cost: 1 c ---[ 313]---> Adder-cost: 259 maxlim: 13 bits: 5/4 c ---[ 312]---> BDD-cost: 1 c ---[ 311]---> Adder-cost: 159 maxlim: 11 bits: 5/4 c ---[ 310]---> BDD-cost: 817 c ---[ 309]---> BDD-cost: 51 c ---[ 308]---> BDD-cost: 253 c ---[ 307]---> Adder-cost: 426 maxlim: 10 bits: 5/4 c ---[ 306]---> BDD-cost: 565 c ---[ 305]---> BDD-cost: 802 c ---[ 304]---> BDD-cost: 164 c ---[ 303]---> BDD-cost: 72 c ---[ 302]---> BDD-cost: 93 c ---[ 301]---> Adder-cost: 772 maxlim: 14 bits: 5/4 c ---[ 300]---> Adder-cost: 287 maxlim: 12 bits: 5/4 c ---[ 299]---> BDD-cost: 157 c ---[ 298]---> BDD-cost: 249 c ---[ 297]---> Adder-cost: 472 maxlim: 15 bits: 5/4 c ---[ 296]---> Adder-cost: 203 maxlim: 12 bits: 5/4 c ---[ 295]---> BDD-cost: 2 c ---[ 294]---> BDD-cost: 906 c ---[ 293]---> BDD-cost: 62 c ---[ 292]---> BDD-cost: 167 c ---[ 291]---> BDD-cost: 4 c ---[ 290]---> BDD-cost: 20 c ---[ 289]---> BDD-cost: 1 c ---[ 288]---> BDD-cost: 1 c ---[ 287]---> BDD-cost: 2 c ---[ 286]---> BDD-cost: 8 c ---[ 285]---> BDD-cost: 147 c ---[ 284]---> BDD-cost: 745 c ---[ 283]---> BDD-cost: 1 c ---[ 282]---> BDD-cost: 1 c ---[ 281]---> BDD-cost: 1 c ---[ 280]---> BDD-cost: 24 c ---[ 279]---> BDD-cost: 54 c ---[ 278]---> Adder-cost: 1107 maxlim: 10 bits: 5/4 c ---[ 277]---> BDD-cost: 32 c ---[ 276]---> BDD-cost: 879 c ---[ 275]---> Adder-cost: 1319 maxlim: 13 bits: 5/4 c ---[ 274]---> BDD-cost: 2088 c ---[ 273]---> Adder-cost: 2950 maxlim: 17 bits: 6/5 c ---[ 272]---> BDD-cost: 1 c ---[ 271]---> BDD-cost: 2736 c ---[ 270]---> Adder-cost: 2699 maxlim: 19 bits: 6/5 c ---[ 269]---> BDD-cost: 492 c ---[ 268]---> BDD-cost: 1 c ---[ 267]---> Adder-cost: 748 maxlim: 16 bits: 6/5 c ---[ 266]---> BDD-cost: 1 c ---[ 265]---> BDD-cost: 72 c ---[ 264]---> BDD-cost: 100 c ---[ 263]---> Adder-cost: 1013 maxlim: 19 bits: 6/5 c ---[ 262]---> BDD-cost: 1 c ---[ 261]---> BDD-cost: 2 c ---[ 260]---> Adder-cost: 446 maxlim: 18 bits: 6/5 c ---[ 259]---> BDD-cost: 767 c ---[ 258]---> Adder-cost: 912 maxlim: 9 bits: 5/4 c ---[ 257]---> Adder-cost: 1474 maxlim: 21 bits: 6/5 c ---[ 256]---> BDD-cost: 889 c ---[ 255]---> Adder-cost: 1032 maxlim: 17 bits: 6/5 c ---[ 254]---> Adder-cost: 577 maxlim: 9 bits: 5/4 c ---[ 253]---> BDD-cost: 1704 c ---[ 252]---> Adder-cost: 371 maxlim: 19 bits: 6/5 c ---[ 251]---> BDD-cost: 932 c ---[ 250]---> Adder-cost: 1365 maxlim: 24 bits: 6/5 c ---[ 249]---> BDD-cost: 1516 c ---[ 248]---> Adder-cost: 1521 maxlim: 17 bits: 6/5 c ---[ 247]---> BDD-cost: 242 c ---[ 246]---> Adder-cost: 324 maxlim: 24 bits: 6/5 c ---[ 245]---> BDD-cost: 1 c ---[ 244]---> Adder-cost: 749 maxlim: 20 bits: 6/5 c ---[ 243]---> BDD-cost: 1 c ---[ 242]---> Adder-cost: 615 maxlim: 17 bits: 6/5 c ---[ 241]---> BDD-cost: 18 c ---[ 240]---> BDD-cost: 497 c ---[ 239]---> Adder-cost: 430 maxlim: 16 bits: 6/5 c ---[ 238]---> BDD-cost: 151 c ---[ 237]---> BDD-cost: 101 c ---[ 236]---> Adder-cost: 941 maxlim: 14 bits: 5/4 c ---[ 235]---> BDD-cost: 46 c ---[ 234]---> Adder-cost: 705 maxlim: 11 bits: 5/4 c ---[ 233]---> BDD-cost: 70 c ---[ 232]---> BDD-cost: 1 c ---[ 231]---> Adder-cost: 150 maxlim: 11 bits: 5/4 c ---[ 230]---> BDD-cost: 1 c ---[ 229]---> BDD-cost: 1 c ---[ 228]---> BDD-cost: 2 c ---[ 227]---> BDD-cost: 79 c ---[ 226]---> Adder-cost: 523 maxlim: 17 bits: 6/5 c ---[ 225]---> Adder-cost: 610 maxlim: 21 bits: 6/5 c ---[ 224]---> BDD-cost: 32 c ---[ 223]---> Adder-cost: 1071 maxlim: 14 bits: 5/4 c ---[ 222]---> BDD-cost: 24 c ---[ 221]---> BDD-cost: 1540 c ---[ 220]---> BDD-cost: 2152 c ---[ 219]---> BDD-cost: 115 c ---[ 218]---> BDD-cost: 1715 c ---[ 217]---> Adder-cost: 1994 maxlim: 23 bits: 6/5 c ---[ 216]---> BDD-cost: 135 c ---[ 215]---> Adder-cost: 902 maxlim: 19 bits: 6/5 c ---[ 214]---> BDD-cost: 1261 c ---[ 213]---> BDD-cost: 1 c ---[ 212]---> BDD-cost: 1 c ---[ 211]---> Adder-cost: 231 maxlim: 23 bits: 6/5 c ---[ 210]---> BDD-cost: 1 c ---[ 209]---> Adder-cost: 509 maxlim: 20 bits: 6/5 c ---[ 208]---> BDD-cost: 1 c ---[ 207]---> BDD-cost: 382 c ---[ 206]---> BDD-cost: 656 c ---[ 205]---> Adder-cost: 1492 maxlim: 16 bits: 6/5 c ---[ 204]---> BDD-cost: 14 c ---[ 203]---> BDD-cost: 308 c ---[ 202]---> Adder-cost: 508 maxlim: 12 bits: 5/4 c ---[ 201]---> Adder-cost: 967 maxlim: 10 bits: 5/4 c ---[ 200]---> BDD-cost: 1 c ---[ 199]---> BDD-cost: 1 c ---[ 198]---> Adder-cost: 858 maxlim: 13 bits: 5/4 c ---[ 197]---> BDD-cost: 1 c ---[ 196]---> BDD-cost: 1 c ---[ 195]---> Adder-cost: 300 maxlim: 13 bits: 5/4 c ---[ 194]---> BDD-cost: 1 c ---[ 193]---> BDD-cost: 68 c ---[ 192]---> Adder-cost: 157 maxlim: 12 bits: 5/4 c ---[ 191]---> Adder-cost: 748 maxlim: 28 bits: 6/5 c ---[ 190]---> BDD-cost: 156 c ---[ 189]---> Adder-cost: 568 maxlim: 10 bits: 5/4 c ---[ 188]---> BDD-cost: 1 c ---[ 187]---> BDD-cost: 1 c ---[ 186]---> Adder-cost: 157 maxlim: 12 bits: 5/4 c ---[ 185]---> BDD-cost: 26 c ---[ 184]---> BDD-cost: 37 c ---[ 183]---> Adder-cost: 257 maxlim: 10 bits: 5/4 c ---[ 182]---> Adder-cost: 257 maxlim: 10 bits: 5/4 c ---[ 181]---> BDD-cost: 32 c ---[ 180]---> Adder-cost: 805 maxlim: 16 bits: 6/5 c ---[ 179]---> Adder-cost: 988 maxlim: 20 bits: 6/5 c ---[ 178]---> BDD-cost: 19 c ---[ 177]---> Adder-cost: 802 maxlim: 17 bits: 6/5 c ---[ 176]---> Adder-cost: 516 maxlim: 16 bits: 6/5 c ---[ 175]---> Adder-cost: 607 maxlim: 20 bits: 6/5 c ---[ 174]---> BDD-cost: 18 c ---[ 173]---> BDD-cost: 19 c ---[ 172]---> Adder-cost: 565 maxlim: 17 bits: 6/5 c ---[ 171]---> BDD-cost: 1 c ---[ 170]---> Adder-cost: 166 maxlim: 17 bits: 6/5 c ---[ 169]---> Adder-cost: 262 maxlim: 22 bits: 6/5 c ---[ 168]---> Adder-cost: 539 maxlim: 20 bits: 6/5 c ---[ 167]---> BDD-cost: 1 c ---[ 166]---> BDD-cost: 1 c ---[ 165]---> Adder-cost: 231 maxlim: 23 bits: 6/5 c ---[ 164]---> BDD-cost: 1 c ---[ 163]---> Adder-cost: 343 maxlim: 20 bits: 6/5 c ---[ 162]---> BDD-cost: 1 c ---[ 161]---> Adder-cost: 1639 maxlim: 15 bits: 5/4 c ---[ 160]---> Adder-cost: 936 maxlim: 13 bits: 5/4 c ---[ 159]---> BDD-cost: 64 c ---[ 158]---> BDD-cost: 250 c ---[ 157]---> Adder-cost: 579 maxlim: 9 bits: 5/4 c ---[ 156]---> BDD-cost: 769 c ---[ 155]---> BDD-cost: 37 c ---[ 154]---> BDD-cost: 977 c ---[ 153]---> BDD-cost: 171 c ---[ 152]---> BDD-cost: 40 c ---[ 151]---> BDD-cost: 250 c ---[ 150]---> BDD-cost: 1 c ---[ 149]---> Adder-cost: 206 maxlim: 10 bits: 5/4 c ---[ 148]---> BDD-cost: 32 c ---[ 147]---> BDD-cost: 88 c ---[ 146]---> BDD-cost: 491 c ---[ 145]---> BDD-cost: 1 c ---[ 144]---> BDD-cost: 375 c ---[ 143]---> BDD-cost: 471 c ---[ 142]---> Adder-cost: 2678 maxlim: 22 bits: 6/5 c ---[ 141]---> Adder-cost: 1141 maxlim: 12 bits: 5/4 c ---[ 140]---> Adder-cost: 1301 maxlim: 12 bits: 5/4 c ---[ 139]---> BDD-cost: 326 c ---[ 138]---> Adder-cost: 752 maxlim: 12 bits: 5/4 c ---[ 137]---> BDD-cost: 394 c ---[ 136]---> Adder-cost: 1099 maxlim: 12 bits: 5/4 c ---[ 135]---> BDD-cost: 232 c ---[ 134]---> BDD-cost: 1615 c ---[ 133]---> Adder-cost: 2350 maxlim: 19 bits: 6/5 c ---[ 132]---> BDD-cost: 2419 c ---[ 131]---> Adder-cost: 1509 maxlim: 17 bits: 6/5 c ---[ 130]---> BDD-cost: 1026 c ---[ 129]---> BDD-cost: 1706 c ---[ 128]---> BDD-cost: 242 c ---[ 127]---> Adder-cost: 1293 maxlim: 14 bits: 5/4 c ---[ 126]---> BDD-cost: 1 c ---[ 125]---> BDD-cost: 1 c ---[ 124]---> Adder-cost: 539 maxlim: 22 bits: 6/5 c ---[ 123]---> Adder-cost: 362 maxlim: 12 bits: 5/4 c ---[ 122]---> Adder-cost: 384 maxlim: 12 bits: 5/4 c ---[ 121]---> BDD-cost: 1 c ---[ 120]---> Adder-cost: 303 maxlim: 12 bits: 5/4 c ---[ 119]---> BDD-cost: 1 c ---[ 118]---> Adder-cost: 355 maxlim: 12 bits: 5/4 c ---[ 117]---> BDD-cost: 1 c ---[ 116]---> BDD-cost: 1 c ---[ 115]---> Adder-cost: 603 maxlim: 21 bits: 6/5 c ---[ 114]---> Adder-cost: 362 maxlim: 12 bits: 5/4 c ---[ 113]---> Adder-cost: 384 maxlim: 12 bits: 5/4 c ---[ 112]---> BDD-cost: 1 c ---[ 111]---> Adder-cost: 303 maxlim: 12 bits: 5/4 c ---[ 110]---> BDD-cost: 1 c ---[ 109]---> Adder-cost: 355 maxlim: 12 bits: 5/4 c ---[ 108]---> Adder-cost: 544 maxlim: 10 bits: 5/4 c ---[ 107]---> BDD-cost: 65 c ---[ 106]---> BDD-cost: 871 c ---[ 105]---> BDD-cost: 1115 c ---[ 104]---> BDD-cost: 32 c ---[ 103]---> BDD-cost: 25 c ---[ 102]---> Adder-cost: 821 maxlim: 10 bits: 5/4 c ---[ 101]---> BDD-cost: 107 c ---[ 100]---> Adder-cost: 505 maxlim: 9 bits: 5/4 c ---[ 99]---> Adder-cost: 1073 maxlim: 20 bits: 6/5 c ---[ 98]---> Adder-cost: 280 maxlim: 10 bits: 5/4 c ---[ 97]---> Adder-cost: 363 maxlim: 10 bits: 5/4 c ---[ 96]---> Adder-cost: 698 maxlim: 19 bits: 6/5 c ---[ 95]---> BDD-cost: 795 c ---[ 94]---> Adder-cost: 565 maxlim: 14 bits: 5/4 c ---[ 93]---> BDD-cost: 65 c ---[ 92]---> BDD-cost: 102 c ---[ 91]---> Adder-cost: 479 maxlim: 21 bits: 6/5 c ---[ 90]---> Adder-cost: 362 maxlim: 12 bits: 5/4 c ---[ 89]---> Adder-cost: 384 maxlim: 12 bits: 5/4 c ---[ 88]---> BDD-cost: 78 c ---[ 87]---> Adder-cost: 303 maxlim: 12 bits: 5/4 c ---[ 86]---> BDD-cost: 90 c ---[ 85]---> Adder-cost: 355 maxlim: 12 bits: 5/4 c ---[ 84]---> BDD-cost: 1 c ---[ 83]---> Adder-cost: 861 maxlim: 15 bits: 5/4 c ---[ 82]---> BDD-cost: 2 c ---[ 81]---> BDD-cost: 1376 c ---[ 80]---> Adder-cost: 635 maxlim: 19 bits: 6/5 c ---[ 79]---> BDD-cost: 1 c ---[ 78]---> BDD-cost: 688 c ---[ 77]---> Adder-cost: 325 maxlim: 20 bits: 6/5 c ---[ 76]---> BDD-cost: 96 c ---[ 75]---> BDD-cost: 1 c ---[ 74]---> Adder-cost: 325 maxlim: 20 bits: 6/5 c ---[ 73]---> BDD-cost: 161 c ---[ 72]---> BDD-cost: 170 c ---[ 71]---> Adder-cost: 513 maxlim: 18 bits: 6/5 c ---[ 70]---> BDD-cost: 1 c ---[ 69]---> BDD-cost: 1 c ---[ 68]---> Adder-cost: 215 maxlim: 19 bits: 6/5 c ---[ 67]---> BDD-cost: 1 c ---[ 66]---> BDD-cost: 1 c ---[ 65]---> Adder-cost: 291 maxlim: 18 bits: 6/5 c ---[ 64]---> BDD-cost: 2 c ---[ 63]---> BDD-cost: 1 c ---[ 62]---> BDD-cost: 1 c ---[ 61]---> Adder-cost: 357 maxlim: 11 bits: 5/4 c ---[ 60]---> BDD-cost: 30 c ---[ 59]---> BDD-cost: 1 c ---[ 58]---> BDD-cost: 1 c ---[ 57]---> Adder-cost: 253 maxlim: 13 bits: 5/4 c ---[ 56]---> BDD-cost: 72 c ---[ 55]---> BDD-cost: 75 c ---[ 54]---> BDD-cost: 302 c ---[ 53]---> BDD-cost: 303 c ---[ 52]---> BDD-cost: 2 c ---[ 51]---> BDD-cost: 46 c ---[ 50]---> BDD-cost: 532 c ---[ 49]---> Adder-cost: 480 maxlim: 10 bits: 5/4 c ---[ 48]---> Adder-cost: 807 maxlim: 22 bits: 6/5 c ---[ 47]---> BDD-cost: 12 c ---[ 46]---> BDD-cost: 86 c ---[ 45]---> BDD-cost: 971 c ---[ 44]---> Adder-cost: 1489 maxlim: 21 bits: 6/5 c ---[ 43]---> BDD-cost: 173 c ---[ 42]---> Adder-cost: 687 maxlim: 10 bits: 5/4 c ---[ 41]---> BDD-cost: 1 c ---[ 40]---> BDD-cost: 170 c ---[ 39]---> Adder-cost: 793 maxlim: 19 bits: 6/5 c ---[ 38]---> BDD-cost: 1 c ---[ 37]---> BDD-cost: 1 c ---[ 36]---> Adder-cost: 211 maxlim: 19 bits: 6/5 c ---[ 35]---> BDD-cost: 78 c ---[ 34]---> BDD-cost: 98 c ---[ 33]---> Adder-cost: 211 maxlim: 19 bits: 6/5 c ---[ 32]---> BDD-cost: 1 c ---[ 31]---> BDD-cost: 1 c ---[ 30]---> Adder-cost: 687 maxlim: 17 bits: 6/5 c ---[ 29]---> BDD-cost: 1 c ---[ 28]---> Adder-cost: 542 maxlim: 16 bits: 6/5 c ---[ 27]---> BDD-cost: 33 c ---[ 26]---> BDD-cost: 92 c ---[ 25]---> BDD-cost: 9 c ---[ 24]---> BDD-cost: 22 c ---[ 23]---> BDD-cost: 1 c ---[ 22]---> BDD-cost: 1 c ---[ 21]---> BDD-cost: 1 c ---[ 20]---> BDD-cost: 1 c ---[ 19]---> BDD-cost: 1 c ---[ 18]---> BDD-cost: 1 c ---[ 17]---> BDD-cost: 1 c ---[ 16]---> BDD-cost: 1 c ---[ 15]---> BDD-cost: 1 c ---[ 14]---> Adder-cost: 253 maxlim: 13 bits: 5/4 c ---[ 13]---> BDD-cost: 182 c ---[ 12]---> Adder-cost: 367 maxlim: 12 bits: 5/4 c ---[ 11]---> BDD-cost: 135 c ---[ 10]---> BDD-cost: 35 c ---[ 9]---> BDD-cost: 505 c ---[ 8]---> Adder-cost: 743 maxlim: 15 bits: 5/4 c ---[ 7]---> BDD-cost: 1 c ---[ 6]---> Adder-cost: 206 maxlim: 10 bits: 5/4 c ---[ 5]---> BDD-cost: 1 c ---[ 4]---> BDD-cost: 794 c ---[ 3]---> BDD-cost: 1 c ---[ 2]---> BDD-cost: 1 c ---[ 1]---> BDD-cost: 132 c ---[ 0]---> BDD-cost: 1 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 890342 3228172 | 296780 0 0 nan | 0.000 % | c | 100 | 890342 3228172 | 326458 100 391 3.9 | 0.500 % | c | 250 | 890342 3228172 | 359103 250 1189 4.8 | 0.500 % | c | 475 | 890342 3228172 | 395014 475 2169 4.6 | 0.500 % | c | 812 | 890342 3228172 | 434515 812 4071 5.0 | 0.500 % | c | 1318 | 890289 3227973 | 477967 1315 7137 5.4 | 0.500 % | c | 2077 | 890235 3227771 | 525763 2069 13297 6.4 | 0.502 % | c | 3216 | 890141 3227421 | 578340 3201 22061 6.9 | 0.504 % | c | 4924 | 890090 3227230 | 636174 4906 37004 7.5 | 0.505 % | c | 7486 | 890061 3227123 | 699791 7465 60333 8.1 | 0.506 % | c | 11330 | 890061 3227123 | 769770 11309 103784 9.2 | 0.506 % | c | 17096 | 889945 3226691 | 846747 17070 153842 9.0 | 0.507 % | c | 25746 | 889777 3226077 | 931422 25697 227105 8.8 | 0.514 % | c | 38720 | 889165 3223843 | 1024565 38622 346417 9.0 | 0.534 % | c | 58182 | 889134 3223728 | 1127021 58081 922227 15.9 | 0.535 % | c | 87375 | 889087 3223555 | 1239723 87272 1737010 19.9 | 0.536 % | c | 131164 | 886745 3215029 | 1363696 130863 2238984 17.1 | 0.632 % |
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/11152/stat): 11152 (minisat+_script) R 11151 11152 10120 0 -1 0 18 0 0 0 0 0 0 0 22 0 1 0 1736702643 712704 3 4294967295 134512640 135087896 3221221664 3221221664 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/11152/statm): 174 3 169 147 0 27 0 [pid=11152] vsize: 696 open syscall for file /etc/ld.so.preload open syscall for file /usr/local/intel-8.0-20031016/lib/tls/i686/mmx/libtermcap.so.2 open syscall for file /usr/local/intel-8.0-20031016/lib/tls/i686/libtermcap.so.2 open syscall for file /usr/local/intel-8.0-20031016/lib/tls/mmx/libtermcap.so.2 open syscall for file /usr/local/intel-8.0-20031016/lib/tls/libtermcap.so.2 open syscall for file /usr/local/intel-8.0-20031016/lib/i686/mmx/libtermcap.so.2 open syscall for file /usr/local/intel-8.0-20031016/lib/i686/libtermcap.so.2 open syscall for file /usr/local/intel-8.0-20031016/lib/mmx/libtermcap.so.2 open syscall for file /usr/local/intel-8.0-20031016/lib/libtermcap.so.2 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/i686/mmx/libtermcap.so.2 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/i686/libtermcap.so.2 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/mmx/libtermcap.so.2 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/libtermcap.so.2 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/i686/mmx/libtermcap.so.2 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/i686/libtermcap.so.2 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/mmx/libtermcap.so.2 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/libtermcap.so.2 open syscall for file /usr/local/globus-2.4.3/lib/tls/i686/mmx/libtermcap.so.2 open syscall for file /usr/local/globus-2.4.3/lib/tls/i686/libtermcap.so.2 open syscall for file /usr/local/globus-2.4.3/lib/tls/mmx/libtermcap.so.2 open syscall for file /usr/local/globus-2.4.3/lib/tls/libtermcap.so.2 open syscall for file /usr/local/globus-2.4.3/lib/i686/mmx/libtermcap.so.2 open syscall for file /usr/local/globus-2.4.3/lib/i686/libtermcap.so.2 open syscall for file /usr/local/globus-2.4.3/lib/mmx/libtermcap.so.2 open syscall for file /usr/local/globus-2.4.3/lib/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 /usr/local/intel-8.0-20031016/lib/libdl.so.2 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/libdl.so.2 open syscall for file /usr/local/globus-2.4.3/lib/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 /usr/local/intel-8.0-20031016/lib/libc.so.6 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/libc.so.6 open syscall for file /usr/local/globus-2.4.3/lib/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 /usr/lib/locale/locale-archive open syscall for file /etc/mtab open syscall for file /proc/meminfo open syscall for file /oldhome/oroussel/solvers/minisat+_script open syscall for file /usr/lib/gconv/gconv-modules.cache New process pid=11153 New process pid=11154 New process pid=11155 execve syscall for /bin/sed executable One traced child (pid=11154) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file /usr/local/intel-8.0-20031016/lib/tls/i686/mmx/libc.so.6 open syscall for file /usr/local/intel-8.0-20031016/lib/tls/i686/libc.so.6 open syscall for file /usr/local/intel-8.0-20031016/lib/tls/mmx/libc.so.6 open syscall for file /usr/local/intel-8.0-20031016/lib/tls/libc.so.6 open syscall for file /usr/local/intel-8.0-20031016/lib/i686/mmx/libc.so.6 open syscall for file /usr/local/intel-8.0-20031016/lib/i686/libc.so.6 open syscall for file /usr/local/intel-8.0-20031016/lib/mmx/libc.so.6 open syscall for file /usr/local/intel-8.0-20031016/lib/libc.so.6 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/i686/mmx/libc.so.6 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/i686/libc.so.6 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/mmx/libc.so.6 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/libc.so.6 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/i686/mmx/libc.so.6 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/i686/libc.so.6 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/mmx/libc.so.6 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/libc.so.6 open syscall for file /usr/local/globus-2.4.3/lib/tls/i686/mmx/libc.so.6 open syscall for file /usr/local/globus-2.4.3/lib/tls/i686/libc.so.6 open syscall for file /usr/local/globus-2.4.3/lib/tls/mmx/libc.so.6 open syscall for file /usr/local/globus-2.4.3/lib/tls/libc.so.6 open syscall for file /usr/local/globus-2.4.3/lib/i686/mmx/libc.so.6 open syscall for file /usr/local/globus-2.4.3/lib/i686/libc.so.6 open syscall for file /usr/local/globus-2.4.3/lib/mmx/libc.so.6 open syscall for file /usr/local/globus-2.4.3/lib/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 open syscall for file /usr/lib/locale/locale-archive open syscall for file /usr/lib/gconv/gconv-modules.cache One traced child (pid=11155) exited with status: 0 One traced child (pid=11153) exited with status: 0 New process pid=11156 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-nsrand-ipx.opb [startup+10.0032 s] Raw data (loadavg): 0.90 0.93 0.80 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 8072 0 0 0 934 32 0 0 25 0 1 0 1736702649 25169920 5575 4294967295 134512640 135094434 3221221600 3221217040 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 6145 5575 145 145 0 6000 0 [pid=11156] vsize: 24580 Current children cumulated CPU time (s) 9.67 Current children cumulated vsize (Kb) 28776 [startup+20.004 s] Raw data (loadavg): 0.92 0.93 0.80 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 11921 0 0 0 1919 42 0 0 25 0 1 0 1736702649 24748032 5492 4294967295 134512640 135094434 3221221600 3221217920 134677330 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11156/statm): 6042 5492 145 145 0 5897 0 [pid=11156] vsize: 24168 Current children cumulated CPU time (s) 19.62 Current children cumulated vsize (Kb) 28364 [startup+30.0058 s] Raw data (loadavg): 0.93 0.93 0.80 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 16126 0 0 0 2906 50 0 0 25 0 1 0 1736702649 24649728 5465 4294967295 134512640 135094434 3221221600 3221218272 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 6018 5465 145 145 0 5873 0 [pid=11156] vsize: 24072 Current children cumulated CPU time (s) 29.57 Current children cumulated vsize (Kb) 28268 [startup+40.0056 s] Raw data (loadavg): 0.94 0.93 0.80 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 20343 0 0 0 3893 58 0 0 25 0 1 0 1736702649 24715264 5479 4294967295 134512640 135094434 3221221600 3221218244 134676244 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 6034 5479 145 145 0 5889 0 [pid=11156] vsize: 24136 Current children cumulated CPU time (s) 39.52 Current children cumulated vsize (Kb) 28332 [startup+50.0084 s] Raw data (loadavg): 0.95 0.94 0.81 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 24532 0 0 0 4876 70 0 0 25 0 1 0 1736702649 24977408 5534 4294967295 134512640 135094434 3221221600 3221217744 134601016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11156/statm): 6098 5534 145 145 0 5953 0 [pid=11156] vsize: 24392 Current children cumulated CPU time (s) 49.47 Current children cumulated vsize (Kb) 28588 [startup+60.0091 s] Raw data (loadavg): 0.96 0.94 0.81 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 28901 0 0 0 5860 80 0 0 25 0 1 0 1736702649 24682496 5478 4294967295 134512640 135094434 3221221600 3221218272 134677333 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11156/statm): 6026 5478 145 145 0 5881 0 [pid=11156] vsize: 24104 Current children cumulated CPU time (s) 59.41 Current children cumulated vsize (Kb) 28300 [startup+70.0109 s] Raw data (loadavg): 0.96 0.94 0.81 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 33230 0 0 0 6846 89 0 0 25 0 1 0 1736702649 24158208 5366 4294967295 134512640 135094434 3221221600 3221219504 134676480 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11156/statm): 5898 5366 145 145 0 5753 0 [pid=11156] vsize: 23592 Current children cumulated CPU time (s) 69.36 Current children cumulated vsize (Kb) 27788 [startup+80.0127 s] Raw data (loadavg): 0.97 0.94 0.81 1/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) T 11152 11152 10120 0 -1 0 39510 0 0 0 7822 105 0 0 25 0 1 0 1736702649 31068160 7085 4294967295 134512640 135094434 3221221600 3221216060 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/11156/statm): 7585 7085 145 145 0 7440 0 [pid=11156] vsize: 30340 Current children cumulated CPU time (s) 79.28 Current children cumulated vsize (Kb) 34536 [startup+90.0135 s] Raw data (loadavg): 0.97 0.94 0.81 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 48062 0 0 0 8779 134 0 0 25 0 1 0 1736702649 60497920 13660 4294967295 134512640 135094434 3221221600 3221219248 134519312 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 14770 13660 145 145 0 14625 0 [pid=11156] vsize: 59080 Current children cumulated CPU time (s) 89.14 Current children cumulated vsize (Kb) 63276 [startup+100.014 s] Raw data (loadavg): 0.98 0.94 0.82 1/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) T 11152 11152 10120 0 -1 0 58566 0 0 0 9694 176 0 0 21 0 1 0 1736702649 108564480 24143 4294967295 134512640 135094434 3221221600 3221217036 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/11156/statm): 26505 24143 145 145 0 26360 0 [pid=11156] vsize: 106020 Current children cumulated CPU time (s) 98.71 Current children cumulated vsize (Kb) 110216 [startup+110.015 s] Raw data (loadavg): 0.98 0.94 0.82 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 59825 0 0 0 10678 183 0 0 25 0 1 0 1736702649 113287168 25402 4294967295 134512640 135094434 3221221600 3221220256 134557928 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11156/statm): 27658 25402 145 145 0 27513 0 [pid=11156] vsize: 110632 Current children cumulated CPU time (s) 108.62 Current children cumulated vsize (Kb) 114828 [startup+120.016 s] Raw data (loadavg): 0.98 0.95 0.82 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60045 0 0 0 11673 186 0 0 25 0 1 0 1736702649 114176000 25622 4294967295 134512640 135094434 3221221600 3221220256 134557846 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 27875 25622 145 145 0 27730 0 [pid=11156] vsize: 111500 Current children cumulated CPU time (s) 118.6 Current children cumulated vsize (Kb) 115696 [startup+130.017 s] Raw data (loadavg): 0.98 0.95 0.82 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60272 0 0 0 12670 187 0 0 25 0 1 0 1736702649 115040256 25849 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 28086 25849 145 145 0 27941 0 [pid=11156] vsize: 112344 Current children cumulated CPU time (s) 128.58 Current children cumulated vsize (Kb) 116540 [startup+140.017 s] Raw data (loadavg): 0.99 0.95 0.82 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60475 0 0 0 13667 189 0 0 25 0 1 0 1736702649 115818496 26052 4294967295 134512640 135094434 3221221600 3221220212 134563089 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 28276 26052 145 145 0 28131 0 [pid=11156] vsize: 113104 Current children cumulated CPU time (s) 138.57 Current children cumulated vsize (Kb) 117300 [startup+150.018 s] Raw data (loadavg): 0.99 0.95 0.82 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60556 0 0 0 14665 190 0 0 25 0 1 0 1736702649 116129792 26133 4294967295 134512640 135094434 3221221600 3221220256 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 28352 26133 145 145 0 28207 0 [pid=11156] vsize: 113408 Current children cumulated CPU time (s) 148.56 Current children cumulated vsize (Kb) 117604 [startup+160.019 s] Raw data (loadavg): 0.99 0.95 0.82 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60597 0 0 0 15665 190 0 0 25 0 1 0 1736702649 116293632 26174 4294967295 134512640 135094434 3221221600 3221220256 134558221 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 28392 26174 145 145 0 28247 0 [pid=11156] vsize: 113568 Current children cumulated CPU time (s) 158.56 Current children cumulated vsize (Kb) 117764 [startup+170.019 s] Raw data (loadavg): 0.99 0.95 0.82 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60647 0 0 0 16664 190 0 0 25 0 1 0 1736702649 116453376 26224 4294967295 134512640 135094434 3221221600 3221220212 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 28431 26224 145 145 0 28286 0 [pid=11156] vsize: 113724 Current children cumulated CPU time (s) 168.55 Current children cumulated vsize (Kb) 117920 [startup+180.019 s] Raw data (loadavg): 0.99 0.95 0.83 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60704 0 0 0 17664 191 0 0 25 0 1 0 1736702649 116707328 26281 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 28493 26281 145 145 0 28348 0 [pid=11156] vsize: 113972 Current children cumulated CPU time (s) 178.56 Current children cumulated vsize (Kb) 118168 [startup+190.02 s] Raw data (loadavg): 0.99 0.95 0.83 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60728 0 0 0 18663 191 0 0 25 0 1 0 1736702649 116781056 26305 4294967295 134512640 135094434 3221221600 3221220212 134563059 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11156/statm): 28511 26305 145 145 0 28366 0 [pid=11156] vsize: 114044 Current children cumulated CPU time (s) 188.55 Current children cumulated vsize (Kb) 118240 [startup+200.021 s] Raw data (loadavg): 0.99 0.95 0.83 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60742 0 0 0 19663 192 0 0 25 0 1 0 1736702649 116834304 26319 4294967295 134512640 135094434 3221221600 3221220260 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11156/statm): 28524 26319 145 145 0 28379 0 [pid=11156] vsize: 114096 Current children cumulated CPU time (s) 198.56 Current children cumulated vsize (Kb) 118292 [startup+210.022 s] Raw data (loadavg): 0.99 0.95 0.83 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60755 0 0 0 20661 192 0 0 25 0 1 0 1736702649 116887552 26332 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11156/statm): 28537 26332 145 145 0 28392 0 [pid=11156] vsize: 114148 Current children cumulated CPU time (s) 208.54 Current children cumulated vsize (Kb) 118344 [startup+220.023 s] Raw data (loadavg): 0.99 0.95 0.83 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60770 0 0 0 21661 192 0 0 25 0 1 0 1736702649 116944896 26347 4294967295 134512640 135094434 3221221600 3221220224 134557696 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 28551 26347 145 145 0 28406 0 [pid=11156] vsize: 114204 Current children cumulated CPU time (s) 218.54 Current children cumulated vsize (Kb) 118400 [startup+230.023 s] Raw data (loadavg): 0.99 0.96 0.83 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60782 0 0 0 22661 192 0 0 25 0 1 0 1736702649 116989952 26359 4294967295 134512640 135094434 3221221600 3221220256 134557872 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 28562 26359 145 145 0 28417 0 [pid=11156] vsize: 114248 Current children cumulated CPU time (s) 228.54 Current children cumulated vsize (Kb) 118444 [startup+240.024 s] Raw data (loadavg): 0.99 0.96 0.83 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60792 0 0 0 23661 192 0 0 25 0 1 0 1736702649 117030912 26369 4294967295 134512640 135094434 3221221600 3221220288 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 28572 26369 145 145 0 28427 0 [pid=11156] vsize: 114288 Current children cumulated CPU time (s) 238.54 Current children cumulated vsize (Kb) 118484 [startup+250.025 s] Raw data (loadavg): 0.99 0.96 0.83 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60805 0 0 0 24661 192 0 0 25 0 1 0 1736702649 117080064 26382 4294967295 134512640 135094434 3221221600 3221220212 134563046 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 28584 26382 145 145 0 28439 0 [pid=11156] vsize: 114336 Current children cumulated CPU time (s) 248.54 Current children cumulated vsize (Kb) 118532 [startup+260.026 s] Raw data (loadavg): 0.99 0.96 0.83 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60814 0 0 0 25661 192 0 0 25 0 1 0 1736702649 117116928 26391 4294967295 134512640 135094434 3221221600 3221220224 134557696 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 28593 26391 145 145 0 28448 0 [pid=11156] vsize: 114372 Current children cumulated CPU time (s) 258.54 Current children cumulated vsize (Kb) 118568 [startup+270.026 s] Raw data (loadavg): 0.99 0.96 0.83 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60825 0 0 0 26660 193 0 0 25 0 1 0 1736702649 117157888 26402 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 28603 26402 145 145 0 28458 0 [pid=11156] vsize: 114412 Current children cumulated CPU time (s) 268.54 Current children cumulated vsize (Kb) 118608 [startup+280.026 s] Raw data (loadavg): 0.99 0.96 0.83 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60835 0 0 0 27661 193 0 0 25 0 1 0 1736702649 117198848 26412 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 28613 26412 145 145 0 28468 0 [pid=11156] vsize: 114452 Current children cumulated CPU time (s) 278.55 Current children cumulated vsize (Kb) 118648 [startup+290.027 s] Raw data (loadavg): 0.99 0.96 0.84 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60848 0 0 0 28661 193 0 0 25 0 1 0 1736702649 117248000 26425 4294967295 134512640 135094434 3221221600 3221220212 134563112 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 28625 26425 145 145 0 28480 0 [pid=11156] vsize: 114500 Current children cumulated CPU time (s) 288.55 Current children cumulated vsize (Kb) 118696 [startup+300.028 s] Raw data (loadavg): 0.99 0.96 0.84 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60858 0 0 0 29661 193 0 0 25 0 1 0 1736702649 117284864 26435 4294967295 134512640 135094434 3221221600 3221220256 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 28634 26435 145 145 0 28489 0 [pid=11156] vsize: 114536 Current children cumulated CPU time (s) 298.55 Current children cumulated vsize (Kb) 118732 [startup+310.029 s] Raw data (loadavg): 0.99 0.96 0.84 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60872 0 0 0 30661 193 0 0 25 0 1 0 1736702649 117342208 26449 4294967295 134512640 135094434 3221221600 3221220288 134554709 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 28648 26449 145 145 0 28503 0 [pid=11156] vsize: 114592 Current children cumulated CPU time (s) 308.55 Current children cumulated vsize (Kb) 118788 [startup+320.028 s] Raw data (loadavg): 0.99 0.96 0.84 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60884 0 0 0 31661 193 0 0 25 0 1 0 1736702649 117387264 26461 4294967295 134512640 135094434 3221221600 3221220256 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11156/statm): 28659 26461 145 145 0 28514 0 [pid=11156] vsize: 114636 Current children cumulated CPU time (s) 318.55 Current children cumulated vsize (Kb) 118832 [startup+330.03 s] Raw data (loadavg): 0.99 0.97 0.84 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60915 0 0 0 32660 193 0 0 25 0 1 0 1736702649 117456896 26492 4294967295 134512640 135094434 3221221600 3221220256 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 28676 26492 145 145 0 28531 0 [pid=11156] vsize: 114704 Current children cumulated CPU time (s) 328.54 Current children cumulated vsize (Kb) 118900 [startup+340.031 s] Raw data (loadavg): 0.99 0.97 0.84 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60931 0 0 0 33660 194 0 0 25 0 1 0 1736702649 117518336 26508 4294967295 134512640 135094434 3221221600 3221220288 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 28691 26508 145 145 0 28546 0 [pid=11156] vsize: 114764 Current children cumulated CPU time (s) 338.55 Current children cumulated vsize (Kb) 118960 [startup+350.032 s] Raw data (loadavg): 0.99 0.97 0.84 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60945 0 0 0 34660 194 0 0 25 0 1 0 1736702649 117575680 26522 4294967295 134512640 135094434 3221221600 3221220212 134563092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 28705 26522 145 145 0 28560 0 [pid=11156] vsize: 114820 Current children cumulated CPU time (s) 348.55 Current children cumulated vsize (Kb) 119016 [startup+360.033 s] Raw data (loadavg): 0.99 0.97 0.84 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60965 0 0 0 35660 194 0 0 25 0 1 0 1736702649 117653504 26542 4294967295 134512640 135094434 3221221600 3221220256 134557866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 28724 26542 145 145 0 28579 0 [pid=11156] vsize: 114896 Current children cumulated CPU time (s) 358.55 Current children cumulated vsize (Kb) 119092 [startup+370.033 s] Raw data (loadavg): 0.99 0.97 0.84 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60980 0 0 0 36660 194 0 0 25 0 1 0 1736702649 117710848 26557 4294967295 134512640 135094434 3221221600 3221220260 134553497 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 28738 26557 145 145 0 28593 0 [pid=11156] vsize: 114952 Current children cumulated CPU time (s) 368.55 Current children cumulated vsize (Kb) 119148 [startup+380.034 s] Raw data (loadavg): 0.99 0.97 0.84 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60991 0 0 0 37660 194 0 0 25 0 1 0 1736702649 117751808 26568 4294967295 134512640 135094434 3221221600 3221220256 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 28748 26568 145 145 0 28603 0 [pid=11156] vsize: 114992 Current children cumulated CPU time (s) 378.55 Current children cumulated vsize (Kb) 119188 [startup+390.035 s] Raw data (loadavg): 0.99 0.97 0.85 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 61001 0 0 0 38660 194 0 0 25 0 1 0 1736702649 117792768 26578 4294967295 134512640 135094434 3221221600 3221220256 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 28758 26578 145 145 0 28613 0 [pid=11156] vsize: 115032 Current children cumulated CPU time (s) 388.55 Current children cumulated vsize (Kb) 119228 [startup+400.037 s] Raw data (loadavg): 0.99 0.97 0.85 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 61013 0 0 0 39660 194 0 0 25 0 1 0 1736702649 117837824 26590 4294967295 134512640 135094434 3221221600 3221220256 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 28769 26590 145 145 0 28624 0 [pid=11156] vsize: 115076 Current children cumulated CPU time (s) 398.55 Current children cumulated vsize (Kb) 119272 [startup+410.037 s] Raw data (loadavg): 0.99 0.97 0.85 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 61057 0 0 0 40660 194 0 0 25 0 1 0 1736702649 118149120 26634 4294967295 134512640 135094434 3221221600 3221220256 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 28845 26634 145 145 0 28700 0 [pid=11156] vsize: 115380 Current children cumulated CPU time (s) 408.55 Current children cumulated vsize (Kb) 119576 [startup+420.037 s] Raw data (loadavg): 0.99 0.97 0.85 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 61058 0 0 0 41660 194 0 0 25 0 1 0 1736702649 118149120 26635 4294967295 134512640 135094434 3221221600 3221220256 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 28845 26635 145 145 0 28700 0 [pid=11156] vsize: 115380 Current children cumulated CPU time (s) 418.55 Current children cumulated vsize (Kb) 119576 [startup+430.039 s] Raw data (loadavg): 0.99 0.97 0.85 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 61059 0 0 0 42660 194 0 0 25 0 1 0 1736702649 118149120 26636 4294967295 134512640 135094434 3221221600 3221220256 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 28845 26636 145 145 0 28700 0 [pid=11156] vsize: 115380 Current children cumulated CPU time (s) 428.55 Current children cumulated vsize (Kb) 119576 [startup+440.04 s] Raw data (loadavg): 0.99 0.97 0.85 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 61073 0 0 0 43660 194 0 0 25 0 1 0 1736702649 118202368 26650 4294967295 134512640 135094434 3221221600 3221220256 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 28858 26650 145 145 0 28713 0 [pid=11156] vsize: 115432 Current children cumulated CPU time (s) 438.55 Current children cumulated vsize (Kb) 119628 [startup+450.041 s] Raw data (loadavg): 0.99 0.97 0.85 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 61086 0 0 0 44660 195 0 0 25 0 1 0 1736702649 118251520 26663 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 28870 26663 145 145 0 28725 0 [pid=11156] vsize: 115480 Current children cumulated CPU time (s) 448.56 Current children cumulated vsize (Kb) 119676 [startup+460.041 s] Raw data (loadavg): 0.99 0.97 0.85 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 61097 0 0 0 45661 195 0 0 25 0 1 0 1736702649 118296576 26674 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 28881 26674 145 145 0 28736 0 [pid=11156] vsize: 115524 Current children cumulated CPU time (s) 458.57 Current children cumulated vsize (Kb) 119720 [startup+470.042 s] Raw data (loadavg): 0.99 0.97 0.85 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 61113 0 0 0 46661 195 0 0 25 0 1 0 1736702649 118358016 26690 4294967295 134512640 135094434 3221221600 3221220212 134563134 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 28896 26690 145 145 0 28751 0 [pid=11156] vsize: 115584 Current children cumulated CPU time (s) 468.57 Current children cumulated vsize (Kb) 119780 [startup+480.043 s] Raw data (loadavg): 0.99 0.97 0.85 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 61128 0 0 0 47661 195 0 0 25 0 1 0 1736702649 118415360 26705 4294967295 134512640 135094434 3221221600 3221220256 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 28910 26705 145 145 0 28765 0 [pid=11156] vsize: 115640 Current children cumulated CPU time (s) 478.57 Current children cumulated vsize (Kb) 119836 [startup+490.044 s] Raw data (loadavg): 0.99 0.97 0.86 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 61149 0 0 0 48660 195 0 0 25 0 1 0 1736702649 118497280 26726 4294967295 134512640 135094434 3221221600 3221220256 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11156/statm): 28930 26726 145 145 0 28785 0 [pid=11156] vsize: 115720 Current children cumulated CPU time (s) 488.56 Current children cumulated vsize (Kb) 119916 [startup+500.046 s] Raw data (loadavg): 0.99 0.97 0.86 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 61162 0 0 0 49660 195 0 0 25 0 1 0 1736702649 118550528 26739 4294967295 134512640 135094434 3221221600 3221220288 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 28943 26739 145 145 0 28798 0 [pid=11156] vsize: 115772 Current children cumulated CPU time (s) 498.56 Current children cumulated vsize (Kb) 119968 [startup+510.046 s] Raw data (loadavg): 0.99 0.97 0.86 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 61187 0 0 0 50660 196 0 0 25 0 1 0 1736702649 118648832 26764 4294967295 134512640 135094434 3221221600 3221220256 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 28967 26764 145 145 0 28822 0 [pid=11156] vsize: 115868 Current children cumulated CPU time (s) 508.57 Current children cumulated vsize (Kb) 120064 [startup+520.046 s] Raw data (loadavg): 0.99 0.97 0.86 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 61211 0 0 0 51659 196 0 0 25 0 1 0 1736702649 118743040 26788 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 28990 26788 145 145 0 28845 0 [pid=11156] vsize: 115960 Current children cumulated CPU time (s) 518.56 Current children cumulated vsize (Kb) 120156 [startup+530.047 s] Raw data (loadavg): 0.99 0.97 0.86 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 61559 0 0 0 52653 199 0 0 25 0 1 0 1736702649 120131584 27136 4294967295 134512640 135094434 3221221600 3221220256 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 29329 27136 145 145 0 29184 0 [pid=11156] vsize: 117316 Current children cumulated CPU time (s) 528.53 Current children cumulated vsize (Kb) 121512 [startup+540.048 s] Raw data (loadavg): 0.99 0.97 0.86 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 61912 0 0 0 53647 201 0 0 25 0 1 0 1736702649 121581568 27489 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 29683 27489 145 145 0 29538 0 [pid=11156] vsize: 118732 Current children cumulated CPU time (s) 538.49 Current children cumulated vsize (Kb) 122928 [startup+550.048 s] Raw data (loadavg): 0.99 0.97 0.86 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 61925 0 0 0 54647 201 0 0 25 0 1 0 1736702649 121630720 27502 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 29695 27502 145 145 0 29550 0 [pid=11156] vsize: 118780 Current children cumulated CPU time (s) 548.49 Current children cumulated vsize (Kb) 122976 [startup+560.049 s] Raw data (loadavg): 0.99 0.97 0.86 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 61966 0 0 0 55647 201 0 0 25 0 1 0 1736702649 121790464 27543 4294967295 134512640 135094434 3221221600 3221220260 134562166 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 29734 27543 145 145 0 29589 0 [pid=11156] vsize: 118936 Current children cumulated CPU time (s) 558.49 Current children cumulated vsize (Kb) 123132 [startup+570.05 s] Raw data (loadavg): 0.99 0.97 0.86 1/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) T 11152 11152 10120 0 -1 0 62053 0 0 0 56646 202 0 0 25 0 1 0 1736702649 122134528 27630 4294967295 134512640 135094434 3221221600 3221219980 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/11156/statm): 29818 27630 145 145 0 29673 0 [pid=11156] vsize: 119272 Current children cumulated CPU time (s) 568.49 Current children cumulated vsize (Kb) 123468 [startup+580.051 s] Raw data (loadavg): 0.99 0.97 0.86 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 62518 0 0 0 57638 205 0 0 25 0 1 0 1736702649 124264448 28095 4294967295 134512640 135094434 3221221600 3221220256 134558402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 30338 28095 145 145 0 30193 0 [pid=11156] vsize: 121352 Current children cumulated CPU time (s) 578.44 Current children cumulated vsize (Kb) 125548 [startup+590.052 s] Raw data (loadavg): 0.99 0.97 0.87 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 62827 0 0 0 58633 207 0 0 25 0 1 0 1736702649 125509632 28404 4294967295 134512640 135094434 3221221600 3221220256 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 30642 28404 145 145 0 30497 0 [pid=11156] vsize: 122568 Current children cumulated CPU time (s) 588.41 Current children cumulated vsize (Kb) 126764 [startup+600.052 s] Raw data (loadavg): 0.99 0.97 0.87 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63036 0 0 0 59630 208 0 0 25 0 1 0 1736702649 126365696 28613 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 30851 28613 145 145 0 30706 0 [pid=11156] vsize: 123404 Current children cumulated CPU time (s) 598.39 Current children cumulated vsize (Kb) 127600 [startup+610.053 s] Raw data (loadavg): 0.99 0.97 0.87 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63071 0 0 0 60630 209 0 0 25 0 1 0 1736702649 126504960 28648 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 30885 28648 145 145 0 30740 0 [pid=11156] vsize: 123540 Current children cumulated CPU time (s) 608.4 Current children cumulated vsize (Kb) 127736 [startup+620.053 s] Raw data (loadavg): 0.99 0.97 0.87 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63104 0 0 0 61630 209 0 0 25 0 1 0 1736702649 126656512 28681 4294967295 134512640 135094434 3221221600 3221220260 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 30922 28681 145 145 0 30777 0 [pid=11156] vsize: 123688 Current children cumulated CPU time (s) 618.4 Current children cumulated vsize (Kb) 127884 [startup+630.054 s] Raw data (loadavg): 0.99 0.97 0.87 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63138 0 0 0 62629 209 0 0 25 0 1 0 1736702649 126787584 28715 4294967295 134512640 135094434 3221221600 3221220256 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 30954 28715 145 145 0 30809 0 [pid=11156] vsize: 123816 Current children cumulated CPU time (s) 628.39 Current children cumulated vsize (Kb) 128012 [startup+640.055 s] Raw data (loadavg): 0.99 0.97 0.87 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63159 0 0 0 63628 210 0 0 25 0 1 0 1736702649 126881792 28736 4294967295 134512640 135094434 3221221600 3221220240 134562098 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 30977 28736 145 145 0 30832 0 [pid=11156] vsize: 123908 Current children cumulated CPU time (s) 638.39 Current children cumulated vsize (Kb) 128104 [startup+650.055 s] Raw data (loadavg): 0.99 0.97 0.87 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63174 0 0 0 64628 211 0 0 25 0 1 0 1736702649 126943232 28751 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 30992 28751 145 145 0 30847 0 [pid=11156] vsize: 123968 Current children cumulated CPU time (s) 648.4 Current children cumulated vsize (Kb) 128164 [startup+660.056 s] Raw data (loadavg): 0.99 0.97 0.87 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63192 0 0 0 65628 212 0 0 25 0 1 0 1736702649 127008768 28769 4294967295 134512640 135094434 3221221600 3221220260 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31008 28769 145 145 0 30863 0 [pid=11156] vsize: 124032 Current children cumulated CPU time (s) 658.41 Current children cumulated vsize (Kb) 128228 [startup+670.057 s] Raw data (loadavg): 0.99 0.97 0.87 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63214 0 0 0 66627 212 0 0 25 0 1 0 1736702649 127107072 28791 4294967295 134512640 135094434 3221221600 3221220256 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31032 28791 145 145 0 30887 0 [pid=11156] vsize: 124128 Current children cumulated CPU time (s) 668.4 Current children cumulated vsize (Kb) 128324 [startup+680.058 s] Raw data (loadavg): 0.99 0.97 0.87 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63251 0 0 0 67627 213 0 0 25 0 1 0 1736702649 127250432 28828 4294967295 134512640 135094434 3221221600 3221220288 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31067 28828 145 145 0 30922 0 [pid=11156] vsize: 124268 Current children cumulated CPU time (s) 678.41 Current children cumulated vsize (Kb) 128464 [startup+690.059 s] Raw data (loadavg): 0.99 0.97 0.87 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63269 0 0 0 68627 213 0 0 25 0 1 0 1736702649 127320064 28846 4294967295 134512640 135094434 3221221600 3221220256 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31084 28846 145 145 0 30939 0 [pid=11156] vsize: 124336 Current children cumulated CPU time (s) 688.41 Current children cumulated vsize (Kb) 128532 [startup+700.059 s] Raw data (loadavg): 0.99 0.97 0.88 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63287 0 0 0 69627 213 0 0 25 0 1 0 1736702649 127389696 28864 4294967295 134512640 135094434 3221221600 3221220256 134558221 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31101 28864 145 145 0 30956 0 [pid=11156] vsize: 124404 Current children cumulated CPU time (s) 698.41 Current children cumulated vsize (Kb) 128600 [startup+710.06 s] Raw data (loadavg): 0.99 0.97 0.88 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63310 0 0 0 70626 213 0 0 25 0 1 0 1736702649 127483904 28887 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31124 28887 145 145 0 30979 0 [pid=11156] vsize: 124496 Current children cumulated CPU time (s) 708.4 Current children cumulated vsize (Kb) 128692 [startup+720.06 s] Raw data (loadavg): 0.99 0.97 0.88 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63328 0 0 0 71626 214 0 0 25 0 1 0 1736702649 127545344 28905 4294967295 134512640 135094434 3221221600 3221220260 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31139 28905 145 145 0 30994 0 [pid=11156] vsize: 124556 Current children cumulated CPU time (s) 718.41 Current children cumulated vsize (Kb) 128752 [startup+730.061 s] Raw data (loadavg): 0.99 0.97 0.88 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63350 0 0 0 72626 214 0 0 25 0 1 0 1736702649 127631360 28927 4294967295 134512640 135094434 3221221600 3221220256 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31160 28927 145 145 0 31015 0 [pid=11156] vsize: 124640 Current children cumulated CPU time (s) 728.41 Current children cumulated vsize (Kb) 128836 [startup+740.062 s] Raw data (loadavg): 0.99 0.97 0.88 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63365 0 0 0 73626 214 0 0 25 0 1 0 1736702649 127688704 28942 4294967295 134512640 135094434 3221221600 3221220256 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31174 28942 145 145 0 31029 0 [pid=11156] vsize: 124696 Current children cumulated CPU time (s) 738.41 Current children cumulated vsize (Kb) 128892 [startup+750.064 s] Raw data (loadavg): 0.99 0.97 0.88 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63376 0 0 0 74626 215 0 0 25 0 1 0 1736702649 127733760 28953 4294967295 134512640 135094434 3221221600 3221220288 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31185 28953 145 145 0 31040 0 [pid=11156] vsize: 124740 Current children cumulated CPU time (s) 748.42 Current children cumulated vsize (Kb) 128936 [startup+760.064 s] Raw data (loadavg): 0.99 0.97 0.88 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63389 0 0 0 75626 215 0 0 25 0 1 0 1736702649 127782912 28966 4294967295 134512640 135094434 3221221600 3221220256 134557879 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31197 28966 145 145 0 31052 0 [pid=11156] vsize: 124788 Current children cumulated CPU time (s) 758.42 Current children cumulated vsize (Kb) 128984 [startup+770.064 s] Raw data (loadavg): 0.99 0.97 0.88 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63396 0 0 0 76626 215 0 0 25 0 1 0 1736702649 127811584 28973 4294967295 134512640 135094434 3221221600 3221220224 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31204 28973 145 145 0 31059 0 [pid=11156] vsize: 124816 Current children cumulated CPU time (s) 768.42 Current children cumulated vsize (Kb) 129012 [startup+780.065 s] Raw data (loadavg): 0.99 0.97 0.88 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63408 0 0 0 77625 215 0 0 25 0 1 0 1736702649 127852544 28985 4294967295 134512640 135094434 3221221600 3221220288 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11156/statm): 31214 28985 145 145 0 31069 0 [pid=11156] vsize: 124856 Current children cumulated CPU time (s) 778.41 Current children cumulated vsize (Kb) 129052 [startup+790.066 s] Raw data (loadavg): 0.99 0.97 0.88 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63424 0 0 0 78625 216 0 0 25 0 1 0 1736702649 127913984 29001 4294967295 134512640 135094434 3221221600 3221220232 134562981 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31229 29001 145 145 0 31084 0 [pid=11156] vsize: 124916 Current children cumulated CPU time (s) 788.42 Current children cumulated vsize (Kb) 129112 [startup+800.067 s] Raw data (loadavg): 0.99 0.97 0.89 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63440 0 0 0 79625 216 0 0 25 0 1 0 1736702649 127979520 29017 4294967295 134512640 135094434 3221221600 3221220256 134557964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31245 29017 145 145 0 31100 0 [pid=11156] vsize: 124980 Current children cumulated CPU time (s) 798.42 Current children cumulated vsize (Kb) 129176 [startup+810.068 s] Raw data (loadavg): 0.99 0.97 0.89 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63452 0 0 0 80625 216 0 0 25 0 1 0 1736702649 128028672 29029 4294967295 134512640 135094434 3221221600 3221220288 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31257 29029 145 145 0 31112 0 [pid=11156] vsize: 125028 Current children cumulated CPU time (s) 808.42 Current children cumulated vsize (Kb) 129224 [startup+820.068 s] Raw data (loadavg): 0.99 0.97 0.89 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63462 0 0 0 81625 216 0 0 25 0 1 0 1736702649 128065536 29039 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31266 29039 145 145 0 31121 0 [pid=11156] vsize: 125064 Current children cumulated CPU time (s) 818.42 Current children cumulated vsize (Kb) 129260 [startup+830.069 s] Raw data (loadavg): 0.99 0.97 0.89 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63478 0 0 0 82624 217 0 0 25 0 1 0 1736702649 128126976 29055 4294967295 134512640 135094434 3221221600 3221220260 134553536 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31281 29055 145 145 0 31136 0 [pid=11156] vsize: 125124 Current children cumulated CPU time (s) 828.42 Current children cumulated vsize (Kb) 129320 [startup+840.07 s] Raw data (loadavg): 0.99 0.97 0.89 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63498 0 0 0 83624 217 0 0 25 0 1 0 1736702649 128204800 29075 4294967295 134512640 135094434 3221221600 3221220256 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31300 29075 145 145 0 31155 0 [pid=11156] vsize: 125200 Current children cumulated CPU time (s) 838.42 Current children cumulated vsize (Kb) 129396 [startup+850.072 s] Raw data (loadavg): 0.99 0.97 0.89 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63510 0 0 0 84624 217 0 0 25 0 1 0 1736702649 128249856 29087 4294967295 134512640 135094434 3221221600 3221220256 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31311 29087 145 145 0 31166 0 [pid=11156] vsize: 125244 Current children cumulated CPU time (s) 848.42 Current children cumulated vsize (Kb) 129440 [startup+860.073 s] Raw data (loadavg): 0.99 0.97 0.89 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63522 0 0 0 85624 217 0 0 25 0 1 0 1736702649 128299008 29099 4294967295 134512640 135094434 3221221600 3221220288 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31323 29099 145 145 0 31178 0 [pid=11156] vsize: 125292 Current children cumulated CPU time (s) 858.42 Current children cumulated vsize (Kb) 129488 [startup+870.072 s] Raw data (loadavg): 0.99 0.97 0.89 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63534 0 0 0 86624 217 0 0 25 0 1 0 1736702649 128344064 29111 4294967295 134512640 135094434 3221221600 3221220212 134563094 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31334 29111 145 145 0 31189 0 [pid=11156] vsize: 125336 Current children cumulated CPU time (s) 868.42 Current children cumulated vsize (Kb) 129532 [startup+880.073 s] Raw data (loadavg): 0.99 0.97 0.89 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63549 0 0 0 87624 218 0 0 25 0 1 0 1736702649 128401408 29126 4294967295 134512640 135094434 3221221600 3221220256 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31348 29126 145 145 0 31203 0 [pid=11156] vsize: 125392 Current children cumulated CPU time (s) 878.43 Current children cumulated vsize (Kb) 129588 [startup+890.074 s] Raw data (loadavg): 0.99 0.97 0.89 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63558 0 0 0 88624 218 0 0 25 0 1 0 1736702649 128438272 29135 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31357 29135 145 145 0 31212 0 [pid=11156] vsize: 125428 Current children cumulated CPU time (s) 888.43 Current children cumulated vsize (Kb) 129624 [startup+900.075 s] Raw data (loadavg): 0.99 0.97 0.90 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63581 0 0 0 89624 218 0 0 25 0 1 0 1736702649 128532480 29158 4294967295 134512640 135094434 3221221600 3221220256 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31380 29158 145 145 0 31235 0 [pid=11156] vsize: 125520 Current children cumulated CPU time (s) 898.43 Current children cumulated vsize (Kb) 129716 [startup+910.076 s] Raw data (loadavg): 0.99 0.97 0.90 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63595 0 0 0 90624 218 0 0 25 0 1 0 1736702649 128585728 29172 4294967295 134512640 135094434 3221221600 3221220256 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31393 29172 145 145 0 31248 0 [pid=11156] vsize: 125572 Current children cumulated CPU time (s) 908.43 Current children cumulated vsize (Kb) 129768 [startup+920.077 s] Raw data (loadavg): 0.99 0.97 0.90 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63622 0 0 0 91624 218 0 0 25 0 1 0 1736702649 128659456 29199 4294967295 134512640 135094434 3221221600 3221220256 134557903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31411 29199 145 145 0 31266 0 [pid=11156] vsize: 125644 Current children cumulated CPU time (s) 918.43 Current children cumulated vsize (Kb) 129840 [startup+930.078 s] Raw data (loadavg): 0.99 0.97 0.90 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63640 0 0 0 92623 218 0 0 25 0 1 0 1736702649 128729088 29217 4294967295 134512640 135094434 3221221600 3221220256 134558402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31428 29217 145 145 0 31283 0 [pid=11156] vsize: 125712 Current children cumulated CPU time (s) 928.42 Current children cumulated vsize (Kb) 129908 [startup+940.078 s] Raw data (loadavg): 0.99 0.97 0.90 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63657 0 0 0 93623 218 0 0 25 0 1 0 1736702649 128798720 29234 4294967295 134512640 135094434 3221221600 3221220256 134557945 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31445 29234 145 145 0 31300 0 [pid=11156] vsize: 125780 Current children cumulated CPU time (s) 938.42 Current children cumulated vsize (Kb) 129976 [startup+950.079 s] Raw data (loadavg): 0.99 0.97 0.90 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63676 0 0 0 94623 219 0 0 25 0 1 0 1736702649 128872448 29253 4294967295 134512640 135094434 3221221600 3221220256 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31463 29253 145 145 0 31318 0 [pid=11156] vsize: 125852 Current children cumulated CPU time (s) 948.43 Current children cumulated vsize (Kb) 130048 [startup+960.08 s] Raw data (loadavg): 0.99 0.97 0.90 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63692 0 0 0 95623 219 0 0 25 0 1 0 1736702649 128933888 29269 4294967295 134512640 135094434 3221221600 3221220212 134563055 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31478 29269 145 145 0 31333 0 [pid=11156] vsize: 125912 Current children cumulated CPU time (s) 958.43 Current children cumulated vsize (Kb) 130108 [startup+970.081 s] Raw data (loadavg): 0.99 0.97 0.90 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63707 0 0 0 96623 219 0 0 25 0 1 0 1736702649 128991232 29284 4294967295 134512640 135094434 3221221600 3221220240 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31492 29284 145 145 0 31347 0 [pid=11156] vsize: 125968 Current children cumulated CPU time (s) 968.43 Current children cumulated vsize (Kb) 130164 [startup+980.082 s] Raw data (loadavg): 0.99 0.97 0.90 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63741 0 0 0 97623 219 0 0 25 0 1 0 1736702649 129138688 29318 4294967295 134512640 135094434 3221221600 3221220256 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31528 29318 145 145 0 31383 0 [pid=11156] vsize: 126112 Current children cumulated CPU time (s) 978.43 Current children cumulated vsize (Kb) 130308 [startup+990.083 s] Raw data (loadavg): 0.99 0.97 0.90 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63774 0 0 0 98622 220 0 0 25 0 1 0 1736702649 129269760 29351 4294967295 134512640 135094434 3221221600 3221220256 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31560 29351 145 145 0 31415 0 [pid=11156] vsize: 126240 Current children cumulated CPU time (s) 988.43 Current children cumulated vsize (Kb) 130436 [startup+1000.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63788 0 0 0 99622 220 0 0 25 0 1 0 1736702649 129323008 29365 4294967295 134512640 135094434 3221221600 3221220256 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31573 29365 145 145 0 31428 0 [pid=11156] vsize: 126292 Current children cumulated CPU time (s) 998.43 Current children cumulated vsize (Kb) 130488 [startup+1010.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63813 0 0 0 100622 220 0 0 25 0 1 0 1736702649 129421312 29390 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31597 29390 145 145 0 31452 0 [pid=11156] vsize: 126388 Current children cumulated CPU time (s) 1008.43 Current children cumulated vsize (Kb) 130584 [startup+1020.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63840 0 0 0 101621 221 0 0 25 0 1 0 1736702649 129527808 29417 4294967295 134512640 135094434 3221221600 3221220240 134562085 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31623 29417 145 145 0 31478 0 [pid=11156] vsize: 126492 Current children cumulated CPU time (s) 1018.43 Current children cumulated vsize (Kb) 130688 [startup+1030.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63855 0 0 0 102621 221 0 0 25 0 1 0 1736702649 129585152 29432 4294967295 134512640 135094434 3221221600 3221220288 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31637 29432 145 145 0 31492 0 [pid=11156] vsize: 126548 Current children cumulated CPU time (s) 1028.43 Current children cumulated vsize (Kb) 130744 [startup+1040.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63871 0 0 0 103621 221 0 0 25 0 1 0 1736702649 129650688 29448 4294967295 134512640 135094434 3221221600 3221220256 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31653 29448 145 145 0 31508 0 [pid=11156] vsize: 126612 Current children cumulated CPU time (s) 1038.43 Current children cumulated vsize (Kb) 130808 [startup+1050.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63884 0 0 0 104621 221 0 0 25 0 1 0 1736702649 129699840 29461 4294967295 134512640 135094434 3221221600 3221220256 134558420 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31665 29461 145 145 0 31520 0 [pid=11156] vsize: 126660 Current children cumulated CPU time (s) 1048.43 Current children cumulated vsize (Kb) 130856 [startup+1060.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 11156 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63898 0 0 0 105621 221 0 0 25 0 1 0 1736702649 129753088 29475 4294967295 134512640 135094434 3221221600 3221220256 134557832 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31678 29475 145 145 0 31533 0 [pid=11156] vsize: 126712 Current children cumulated CPU time (s) 1058.43 Current children cumulated vsize (Kb) 130908 [startup+1070.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 11158 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63913 0 0 0 106621 221 0 0 25 0 1 0 1736702649 129814528 29490 4294967295 134512640 135094434 3221221600 3221220256 134557964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31693 29490 145 145 0 31548 0 [pid=11156] vsize: 126772 Current children cumulated CPU time (s) 1068.43 Current children cumulated vsize (Kb) 130968 [startup+1080.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 11158 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63927 0 0 0 107621 221 0 0 25 0 1 0 1736702649 129867776 29504 4294967295 134512640 135094434 3221221600 3221220256 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31706 29504 145 145 0 31561 0 [pid=11156] vsize: 126824 Current children cumulated CPU time (s) 1078.43 Current children cumulated vsize (Kb) 131020 [startup+1090.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 11158 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63939 0 0 0 108621 222 0 0 25 0 1 0 1736702649 129916928 29516 4294967295 134512640 135094434 3221221600 3221220256 134557950 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31718 29516 145 145 0 31573 0 [pid=11156] vsize: 126872 Current children cumulated CPU time (s) 1088.44 Current children cumulated vsize (Kb) 131068 [startup+1100.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 11158 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63963 0 0 0 109620 222 0 0 25 0 1 0 1736702649 130007040 29540 4294967295 134512640 135094434 3221221600 3221220256 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31740 29540 145 145 0 31595 0 [pid=11156] vsize: 126960 Current children cumulated CPU time (s) 1098.43 Current children cumulated vsize (Kb) 131156 [startup+1110.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 11158 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63990 0 0 0 110620 222 0 0 25 0 1 0 1736702649 130101248 29567 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31763 29567 145 145 0 31618 0 [pid=11156] vsize: 127052 Current children cumulated CPU time (s) 1108.43 Current children cumulated vsize (Kb) 131248 [startup+1120.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 11158 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 64002 0 0 0 111621 222 0 0 25 0 1 0 1736702649 130150400 29579 4294967295 134512640 135094434 3221221600 3221220256 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31775 29579 145 145 0 31630 0 [pid=11156] vsize: 127100 Current children cumulated CPU time (s) 1118.44 Current children cumulated vsize (Kb) 131296 [startup+1130.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 11158 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 64023 0 0 0 112620 222 0 0 25 0 1 0 1736702649 130232320 29600 4294967295 134512640 135094434 3221221600 3221220212 134563085 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31795 29600 145 145 0 31650 0 [pid=11156] vsize: 127180 Current children cumulated CPU time (s) 1128.43 Current children cumulated vsize (Kb) 131376 [startup+1140.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 11158 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 64032 0 0 0 113620 222 0 0 25 0 1 0 1736702649 130269184 29609 4294967295 134512640 135094434 3221221600 3221220260 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11156/statm): 31804 29609 145 145 0 31659 0 [pid=11156] vsize: 127216 Current children cumulated CPU time (s) 1138.43 Current children cumulated vsize (Kb) 131412 [startup+1150.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 11158 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 64042 0 0 0 114620 223 0 0 25 0 1 0 1736702649 130830336 29619 4294967295 134512640 135094434 3221221600 3221220256 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11156/statm): 31941 29619 145 145 0 31796 0 [pid=11156] vsize: 127764 Current children cumulated CPU time (s) 1148.44 Current children cumulated vsize (Kb) 131960 [startup+1160.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 11158 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 64054 0 0 0 115620 223 0 0 25 0 1 0 1736702649 130875392 29631 4294967295 134512640 135094434 3221221600 3221220256 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11156/statm): 31952 29631 145 145 0 31807 0 [pid=11156] vsize: 127808 Current children cumulated CPU time (s) 1158.44 Current children cumulated vsize (Kb) 132004 [startup+1170.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 11158 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 64066 0 0 0 116620 223 0 0 25 0 1 0 1736702649 130924544 29643 4294967295 134512640 135094434 3221221600 3221220236 134557560 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11156/statm): 31964 29643 145 145 0 31819 0 [pid=11156] vsize: 127856 Current children cumulated CPU time (s) 1168.44 Current children cumulated vsize (Kb) 132052 [startup+1180.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 11158 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 64077 0 0 0 117619 224 0 0 25 0 1 0 1736702649 130965504 29654 4294967295 134512640 135094434 3221221600 3221220288 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11156/statm): 31974 29654 145 145 0 31829 0 [pid=11156] vsize: 127896 Current children cumulated CPU time (s) 1178.44 Current children cumulated vsize (Kb) 132092 [startup+1190.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 11158 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 64091 0 0 0 118619 224 0 0 25 0 1 0 1736702649 131022848 29668 4294967295 134512640 135094434 3221221600 3221220256 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 31988 29668 145 145 0 31843 0 [pid=11156] vsize: 127952 Current children cumulated CPU time (s) 1188.44 Current children cumulated vsize (Kb) 132148 [startup+1200.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 11158 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 64104 0 0 0 119619 224 0 0 25 0 1 0 1736702649 131076096 29681 4294967295 134512640 135094434 3221221600 3221220212 134563092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 32001 29681 145 145 0 31856 0 [pid=11156] vsize: 128004 Current children cumulated CPU time (s) 1198.44 Current children cumulated vsize (Kb) 132200 [startup+1210.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 11158 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 64114 0 0 0 120619 224 0 0 25 0 1 0 1736702649 131117056 29691 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 32011 29691 145 145 0 31866 0 [pid=11156] vsize: 128044 Current children cumulated CPU time (s) 1208.44 Current children cumulated vsize (Kb) 132240 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 11158 Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0 [pid=11152] vsize: 4196 Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 64114 0 0 0 120619 224 0 0 25 0 1 0 1736702649 131117056 29691 4294967295 134512640 135094434 3221221600 3221220212 134563055 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11156/statm): 32011 29691 145 145 0 31866 0 [pid=11156] vsize: 128044 Current children cumulated CPU time (s) 1208.44 Current children cumulated vsize (Kb) 132240 Sending SIGTERM to -11152 Sleeping 2 seconds One traced child (pid=11152) ended because it received signal 15 (SIGTERM) One traced child (pid=11156) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.16 CPU time (s): 1208.5 CPU user time (s): 1206.19 CPU system time (s): 2.30365 CPU usage (%): 99.8624 Max. virtual memory (cumulated for all children) (Kb): 132240
ERROR: no interpretation found !