Name | web/www.ps.uni-sb.de/~walser/benchmarks/course-ass/normalized-ss97-4.opb |
MD5SUM | 417d3abd60fd3b9eb4200ff5119a92c4 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 818 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 1798 |
Biggest coefficient in the objective function | 349 |
Number of bits for the biggest coefficient in the objective function | 9 |
Sum of the numbers in the objective function | 104116 |
Number of bits of the sum of numbers in the objective function | 17 |
Biggest number in a constraint | 349 |
Number of bits of the biggest number in a constraint | 9 |
Biggest sum of numbers in a constraint | 104116 |
Number of bits of the biggest sum of numbers | 17 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1267.1 |
Number of variables | 2289 |
Total number of constraints | 3052 |
Number of constraints which are clauses | 360 |
Number of constraints which are cardinality constraints (but not clauses) | 2692 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 195 |
LAUNCH ON wulflinc21 THE 2005-09-18 19:05:32 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2726 boxname=wulflinc21 idbench=382 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 417d3abd60fd3b9eb4200ff5119a92c4 /oldhome/oroussel/tmp/wulflinc21/normalized-ss97-4.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc21/normalized-ss97-4.opb IDLAUNCH: 2726 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.161 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.161 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: 894868 kB Buffers: 35108 kB Cached: 77476 kB SwapCached: 908 kB Active: 79100 kB Inactive: 36196 kB HighTotal: 131008 kB HighFree: 57288 kB LowTotal: 903652 kB LowFree: 837580 kB SwapTotal: 2097892 kB SwapFree: 2096472 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5804 kB Slab: 18840 kB Committed_AS: 64332 kB PageTables: 340 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 19:25:42 (client local time) WITH STATUS 0 IN 1207.69 SECONDS stats: 2726 7 1207.69 0
c Parsing PB file... c Converting 1139 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ######################################################################################################################################################################################################################################################################################################################################################################################### c -- Clauses(.)/Splits(s): ........................................................................................................................................................................................................................................................................................................................................................................ c ---[1138]---> Adder-cost: 354 maxlim: 132 bits: 8/8 c ---[1137]---> Adder-cost: 354 maxlim: 132 bits: 8/8 c ---[1136]---> Adder-cost: 354 maxlim: 132 bits: 8/8 c ---[1135]---> Adder-cost: 352 maxlim: 131 bits: 8/8 c ---[1134]---> Adder-cost: 382 maxlim: 167 bits: 8/8 c ---[1133]---> Adder-cost: 382 maxlim: 167 bits: 8/8 c ---[1132]---> Adder-cost: 382 maxlim: 168 bits: 8/8 c ---[1131]---> Adder-cost: 382 maxlim: 167 bits: 8/8 c ---[1130]---> Adder-cost: 382 maxlim: 167 bits: 8/8 c ---[1129]---> Adder-cost: 382 maxlim: 167 bits: 8/8 c ---[1128]---> Adder-cost: 382 maxlim: 168 bits: 8/8 c ---[1127]---> Adder-cost: 382 maxlim: 167 bits: 8/8 c ---[1126]---> Adder-cost: 48 maxlim: 35 bits: 7/6 c ---[1125]---> Adder-cost: 48 maxlim: 35 bits: 7/6 c ---[1124]---> Adder-cost: 48 maxlim: 35 bits: 7/6 c ---[1123]---> Adder-cost: 32 maxlim: 35 bits: 7/6 c ---[1122]---> Adder-cost: 56 maxlim: 18 bits: 6/5 c ---[1121]---> Adder-cost: 56 maxlim: 18 bits: 6/5 c ---[1120]---> Adder-cost: 20 maxlim: 18 bits: 6/5 c ---[1119]---> Adder-cost: 56 maxlim: 18 bits: 6/5 c ---[1118]---> Adder-cost: 56 maxlim: 18 bits: 6/5 c ---[1117]---> Adder-cost: 56 maxlim: 18 bits: 6/5 c ---[1116]---> Adder-cost: 20 maxlim: 18 bits: 6/5 c ---[1115]---> Adder-cost: 56 maxlim: 18 bits: 6/5 c ---[1113]---> BDD-cost: 5 c ---[1111]---> BDD-cost: 13 c ---[1109]---> BDD-cost: 5 c ---[1107]---> BDD-cost: 13 c ---[1105]---> BDD-cost: 5 c ---[1103]---> BDD-cost: 13 c ---[1101]---> BDD-cost: 5 c ---[1099]---> BDD-cost: 13 c ---[1097]---> BDD-cost: 5 c ---[1095]---> BDD-cost: 13 c ---[1093]---> BDD-cost: 5 c ---[1091]---> BDD-cost: 13 c ---[1089]---> BDD-cost: 5 c ---[1087]---> BDD-cost: 13 c ---[1085]---> BDD-cost: 5 c ---[1083]---> BDD-cost: 13 c ---[1081]---> BDD-cost: 5 c ---[1079]---> BDD-cost: 13 c ---[1077]---> BDD-cost: 5 c ---[1075]---> BDD-cost: 13 c ---[1073]---> BDD-cost: 5 c ---[1071]---> BDD-cost: 13 c ---[1069]---> BDD-cost: 5 c ---[1067]---> BDD-cost: 13 c ---[1065]---> BDD-cost: 5 c ---[1063]---> BDD-cost: 13 c ---[1061]---> BDD-cost: 5 c ---[1059]---> BDD-cost: 13 c ---[1057]---> BDD-cost: 5 c ---[1055]---> BDD-cost: 13 c ---[1053]---> BDD-cost: 5 c ---[1051]---> BDD-cost: 13 c ---[1049]---> BDD-cost: 5 c ---[1047]---> BDD-cost: 13 c ---[1045]---> BDD-cost: 5 c ---[1043]---> BDD-cost: 13 c ---[1041]---> BDD-cost: 5 c ---[1039]---> BDD-cost: 13 c ---[1037]---> BDD-cost: 5 c ---[1035]---> BDD-cost: 13 c ---[1033]---> BDD-cost: 5 c ---[1031]---> BDD-cost: 13 c ---[1029]---> BDD-cost: 5 c ---[1027]---> BDD-cost: 13 c ---[1025]---> BDD-cost: 5 c ---[1023]---> BDD-cost: 13 c ---[1021]---> BDD-cost: 5 c ---[1019]---> BDD-cost: 13 c ---[1017]---> BDD-cost: 5 c ---[1015]---> BDD-cost: 13 c ---[1013]---> BDD-cost: 5 c ---[1011]---> BDD-cost: 13 c ---[1009]---> BDD-cost: 13 c ---[1007]---> BDD-cost: 5 c ---[1005]---> BDD-cost: 13 c ---[1003]---> BDD-cost: 5 c ---[1001]---> BDD-cost: 13 c ---[ 999]---> BDD-cost: 5 c ---[ 997]---> BDD-cost: 13 c ---[ 995]---> BDD-cost: 5 c ---[ 993]---> BDD-cost: 13 c ---[ 991]---> BDD-cost: 13 c ---[ 989]---> BDD-cost: 5 c ---[ 987]---> BDD-cost: 13 c ---[ 985]---> BDD-cost: 5 c ---[ 983]---> BDD-cost: 13 c ---[ 981]---> BDD-cost: 5 c ---[ 979]---> BDD-cost: 13 c ---[ 977]---> BDD-cost: 5 c ---[ 975]---> BDD-cost: 13 c ---[ 973]---> BDD-cost: 5 c ---[ 971]---> BDD-cost: 13 c ---[ 969]---> BDD-cost: 5 c ---[ 967]---> BDD-cost: 13 c ---[ 965]---> BDD-cost: 5 c ---[ 963]---> BDD-cost: 13 c ---[ 961]---> BDD-cost: 5 c ---[ 959]---> BDD-cost: 13 c ---[ 957]---> BDD-cost: 5 c ---[ 955]---> BDD-cost: 13 c ---[ 953]---> BDD-cost: 5 c ---[ 951]---> BDD-cost: 13 c ---[ 949]---> BDD-cost: 5 c ---[ 947]---> BDD-cost: 13 c ---[ 945]---> BDD-cost: 5 c ---[ 943]---> BDD-cost: 13 c ---[ 941]---> BDD-cost: 5 c ---[ 939]---> BDD-cost: 13 c ---[ 937]---> BDD-cost: 5 c ---[ 935]---> BDD-cost: 13 c ---[ 933]---> BDD-cost: 5 c ---[ 931]---> BDD-cost: 13 c ---[ 929]---> BDD-cost: 5 c ---[ 927]---> BDD-cost: 13 c ---[ 925]---> BDD-cost: 5 c ---[ 923]---> BDD-cost: 13 c ---[ 921]---> BDD-cost: 5 c ---[ 919]---> BDD-cost: 13 c ---[ 917]---> BDD-cost: 5 c ---[ 915]---> BDD-cost: 13 c ---[ 913]---> BDD-cost: 5 c ---[ 911]---> BDD-cost: 13 c ---[ 909]---> BDD-cost: 5 c ---[ 907]---> BDD-cost: 13 c ---[ 905]---> BDD-cost: 13 c ---[ 903]---> BDD-cost: 5 c ---[ 901]---> BDD-cost: 13 c ---[ 899]---> BDD-cost: 5 c ---[ 897]---> BDD-cost: 13 c ---[ 895]---> BDD-cost: 5 c ---[ 893]---> BDD-cost: 13 c ---[ 891]---> BDD-cost: 5 c ---[ 889]---> BDD-cost: 13 c ---[ 887]---> BDD-cost: 5 c ---[ 885]---> BDD-cost: 13 c ---[ 883]---> BDD-cost: 5 c ---[ 881]---> BDD-cost: 13 c ---[ 879]---> BDD-cost: 5 c ---[ 877]---> BDD-cost: 13 c ---[ 875]---> BDD-cost: 5 c ---[ 873]---> BDD-cost: 13 c ---[ 871]---> BDD-cost: 5 c ---[ 869]---> BDD-cost: 13 c ---[ 867]---> BDD-cost: 5 c ---[ 865]---> BDD-cost: 13 c ---[ 863]---> BDD-cost: 5 c ---[ 861]---> BDD-cost: 13 c ---[ 859]---> BDD-cost: 5 c ---[ 857]---> BDD-cost: 13 c ---[ 855]---> BDD-cost: 5 c ---[ 853]---> BDD-cost: 13 c ---[ 851]---> BDD-cost: 5 c ---[ 849]---> BDD-cost: 13 c ---[ 847]---> BDD-cost: 5 c ---[ 845]---> BDD-cost: 13 c ---[ 843]---> BDD-cost: 5 c ---[ 841]---> BDD-cost: 13 c ---[ 839]---> BDD-cost: 5 c ---[ 837]---> BDD-cost: 13 c ---[ 835]---> BDD-cost: 5 c ---[ 833]---> BDD-cost: 13 c ---[ 831]---> BDD-cost: 5 c ---[ 829]---> BDD-cost: 13 c ---[ 827]---> BDD-cost: 5 c ---[ 825]---> BDD-cost: 13 c ---[ 823]---> BDD-cost: 13 c ---[ 821]---> BDD-cost: 5 c ---[ 819]---> BDD-cost: 13 c ---[ 817]---> BDD-cost: 5 c ---[ 815]---> BDD-cost: 13 c ---[ 813]---> BDD-cost: 5 c ---[ 811]---> BDD-cost: 13 c ---[ 809]---> BDD-cost: 5 c ---[ 807]---> BDD-cost: 13 c ---[ 805]---> BDD-cost: 5 c ---[ 803]---> BDD-cost: 13 c ---[ 801]---> BDD-cost: 5 c ---[ 799]---> BDD-cost: 13 c ---[ 797]---> BDD-cost: 5 c ---[ 795]---> BDD-cost: 13 c ---[ 793]---> BDD-cost: 13 c ---[ 791]---> BDD-cost: 5 c ---[ 789]---> BDD-cost: 13 c ---[ 787]---> BDD-cost: 5 c ---[ 785]---> BDD-cost: 13 c ---[ 783]---> BDD-cost: 13 c ---[ 781]---> BDD-cost: 5 c ---[ 779]---> BDD-cost: 13 c ---[ 777]---> BDD-cost: 5 c ---[ 775]---> BDD-cost: 13 c ---[ 773]---> BDD-cost: 5 c ---[ 771]---> BDD-cost: 13 c ---[ 769]---> BDD-cost: 5 c ---[ 767]---> BDD-cost: 13 c ---[ 765]---> BDD-cost: 5 c ---[ 763]---> BDD-cost: 13 c ---[ 761]---> BDD-cost: 13 c ---[ 759]---> BDD-cost: 5 c ---[ 757]---> BDD-cost: 13 c ---[ 755]---> BDD-cost: 5 c ---[ 753]---> BDD-cost: 13 c ---[ 751]---> BDD-cost: 5 c ---[ 749]---> BDD-cost: 13 c ---[ 747]---> BDD-cost: 5 c ---[ 745]---> BDD-cost: 13 c ---[ 743]---> BDD-cost: 5 c ---[ 741]---> BDD-cost: 13 c ---[ 739]---> BDD-cost: 5 c ---[ 737]---> BDD-cost: 13 c ---[ 735]---> BDD-cost: 5 c ---[ 733]---> BDD-cost: 13 c ---[ 731]---> BDD-cost: 5 c ---[ 729]---> BDD-cost: 13 c ---[ 727]---> BDD-cost: 5 c ---[ 725]---> BDD-cost: 13 c ---[ 723]---> BDD-cost: 5 c ---[ 721]---> BDD-cost: 13 c ---[ 719]---> BDD-cost: 5 c ---[ 717]---> BDD-cost: 13 c ---[ 715]---> BDD-cost: 13 c ---[ 713]---> BDD-cost: 5 c ---[ 711]---> BDD-cost: 13 c ---[ 709]---> BDD-cost: 13 c ---[ 707]---> BDD-cost: 5 c ---[ 705]---> BDD-cost: 13 c ---[ 703]---> BDD-cost: 5 c ---[ 701]---> BDD-cost: 13 c ---[ 699]---> BDD-cost: 5 c ---[ 697]---> BDD-cost: 13 c ---[ 695]---> BDD-cost: 5 c ---[ 693]---> BDD-cost: 13 c ---[ 691]---> BDD-cost: 5 c ---[ 689]---> BDD-cost: 13 c ---[ 687]---> BDD-cost: 5 c ---[ 685]---> BDD-cost: 13 c ---[ 683]---> BDD-cost: 5 c ---[ 681]---> BDD-cost: 13 c ---[ 679]---> BDD-cost: 5 c ---[ 677]---> BDD-cost: 13 c ---[ 675]---> BDD-cost: 5 c ---[ 673]---> BDD-cost: 13 c ---[ 671]---> BDD-cost: 5 c ---[ 669]---> BDD-cost: 13 c ---[ 667]---> BDD-cost: 5 c ---[ 665]---> BDD-cost: 13 c ---[ 663]---> BDD-cost: 5 c ---[ 661]---> BDD-cost: 13 c ---[ 659]---> BDD-cost: 5 c ---[ 657]---> BDD-cost: 13 c ---[ 655]---> BDD-cost: 5 c ---[ 653]---> BDD-cost: 13 c ---[ 651]---> BDD-cost: 5 c ---[ 649]---> BDD-cost: 13 c ---[ 647]---> BDD-cost: 5 c ---[ 645]---> BDD-cost: 13 c ---[ 643]---> BDD-cost: 5 c ---[ 641]---> BDD-cost: 13 c ---[ 639]---> BDD-cost: 5 c ---[ 637]---> BDD-cost: 13 c ---[ 635]---> BDD-cost: 5 c ---[ 633]---> BDD-cost: 13 c ---[ 631]---> BDD-cost: 5 c ---[ 629]---> BDD-cost: 13 c ---[ 627]---> BDD-cost: 5 c ---[ 625]---> BDD-cost: 13 c ---[ 623]---> BDD-cost: 5 c ---[ 621]---> BDD-cost: 13 c ---[ 619]---> BDD-cost: 5 c ---[ 617]---> BDD-cost: 13 c ---[ 615]---> BDD-cost: 5 c ---[ 613]---> BDD-cost: 13 c ---[ 611]---> BDD-cost: 5 c ---[ 609]---> BDD-cost: 13 c ---[ 607]---> BDD-cost: 5 c ---[ 605]---> BDD-cost: 13 c ---[ 603]---> BDD-cost: 3 c ---[ 601]---> BDD-cost: 1 c ---[ 599]---> BDD-cost: 5 c ---[ 597]---> BDD-cost: 13 c ---[ 595]---> BDD-cost: 5 c ---[ 593]---> BDD-cost: 13 c ---[ 591]---> BDD-cost: 5 c ---[ 589]---> BDD-cost: 13 c ---[ 587]---> BDD-cost: 5 c ---[ 585]---> BDD-cost: 5 c ---[ 583]---> BDD-cost: 13 c ---[ 581]---> BDD-cost: 5 c ---[ 579]---> BDD-cost: 13 c ---[ 577]---> BDD-cost: 5 c ---[ 575]---> BDD-cost: 13 c ---[ 573]---> BDD-cost: 5 c ---[ 571]---> BDD-cost: 13 c ---[ 569]---> BDD-cost: 5 c ---[ 567]---> BDD-cost: 13 c ---[ 565]---> BDD-cost: 5 c ---[ 563]---> BDD-cost: 13 c ---[ 561]---> BDD-cost: 5 c ---[ 559]---> BDD-cost: 13 c ---[ 557]---> BDD-cost: 5 c ---[ 555]---> BDD-cost: 13 c ---[ 553]---> BDD-cost: 5 c ---[ 551]---> BDD-cost: 13 c ---[ 549]---> BDD-cost: 5 c ---[ 547]---> BDD-cost: 13 c ---[ 545]---> BDD-cost: 5 c ---[ 543]---> BDD-cost: 13 c ---[ 541]---> BDD-cost: 5 c ---[ 539]---> BDD-cost: 13 c ---[ 537]---> BDD-cost: 13 c ---[ 535]---> BDD-cost: 5 c ---[ 533]---> BDD-cost: 13 c ---[ 531]---> BDD-cost: 5 c ---[ 529]---> BDD-cost: 13 c ---[ 527]---> BDD-cost: 5 c ---[ 525]---> BDD-cost: 13 c ---[ 523]---> BDD-cost: 5 c ---[ 521]---> BDD-cost: 13 c ---[ 519]---> BDD-cost: 5 c ---[ 517]---> BDD-cost: 13 c ---[ 515]---> BDD-cost: 13 c ---[ 513]---> BDD-cost: 13 c ---[ 511]---> BDD-cost: 13 c ---[ 509]---> BDD-cost: 5 c ---[ 507]---> BDD-cost: 13 c ---[ 505]---> BDD-cost: 5 c ---[ 503]---> BDD-cost: 13 c ---[ 501]---> BDD-cost: 5 c ---[ 499]---> BDD-cost: 13 c ---[ 497]---> BDD-cost: 5 c ---[ 495]---> BDD-cost: 13 c ---[ 493]---> BDD-cost: 5 c ---[ 491]---> BDD-cost: 13 c ---[ 489]---> BDD-cost: 5 c ---[ 487]---> BDD-cost: 13 c ---[ 485]---> BDD-cost: 5 c ---[ 483]---> BDD-cost: 13 c ---[ 481]---> BDD-cost: 5 c ---[ 479]---> BDD-cost: 13 c ---[ 477]---> BDD-cost: 5 c ---[ 475]---> BDD-cost: 13 c ---[ 473]---> BDD-cost: 5 c ---[ 471]---> BDD-cost: 13 c ---[ 469]---> BDD-cost: 5 c ---[ 467]---> BDD-cost: 13 c ---[ 465]---> BDD-cost: 5 c ---[ 463]---> BDD-cost: 13 c ---[ 461]---> BDD-cost: 5 c ---[ 459]---> BDD-cost: 13 c ---[ 457]---> BDD-cost: 5 c ---[ 455]---> BDD-cost: 13 c ---[ 453]---> BDD-cost: 5 c ---[ 451]---> BDD-cost: 13 c ---[ 449]---> BDD-cost: 5 c ---[ 447]---> BDD-cost: 13 c ---[ 445]---> BDD-cost: 5 c ---[ 443]---> BDD-cost: 13 c ---[ 441]---> BDD-cost: 5 c ---[ 439]---> BDD-cost: 13 c ---[ 437]---> BDD-cost: 5 c ---[ 435]---> BDD-cost: 13 c ---[ 433]---> BDD-cost: 5 c ---[ 431]---> BDD-cost: 13 c ---[ 429]---> BDD-cost: 5 c ---[ 427]---> BDD-cost: 13 c ---[ 425]---> BDD-cost: 5 c ---[ 423]---> BDD-cost: 13 c ---[ 421]---> BDD-cost: 5 c ---[ 419]---> BDD-cost: 13 c ---[ 417]---> BDD-cost: 5 c ---[ 415]---> BDD-cost: 13 c ---[ 413]---> BDD-cost: 13 c ---[ 411]---> BDD-cost: 5 c ---[ 409]---> BDD-cost: 13 c ---[ 407]---> BDD-cost: 5 c ---[ 405]---> BDD-cost: 13 c ---[ 403]---> BDD-cost: 5 c ---[ 401]---> BDD-cost: 13 c ---[ 399]---> BDD-cost: 5 c ---[ 397]---> BDD-cost: 13 c ---[ 395]---> BDD-cost: 5 c ---[ 393]---> BDD-cost: 13 c ---[ 391]---> BDD-cost: 5 c ---[ 389]---> BDD-cost: 13 c ---[ 387]---> BDD-cost: 5 c ---[ 385]---> BDD-cost: 13 c ---[ 383]---> BDD-cost: 5 c ---[ 381]---> BDD-cost: 13 c ---[ 379]---> BDD-cost: 5 c ---[ 377]---> BDD-cost: 13 c ---[ 375]---> BDD-cost: 5 c ---[ 373]---> BDD-cost: 13 c ---[ 371]---> BDD-cost: 5 c ---[ 369]---> BDD-cost: 13 c ---[ 367]---> BDD-cost: 5 c ---[ 365]---> BDD-cost: 13 c ---[ 363]---> BDD-cost: 5 c ---[ 361]---> BDD-cost: 13 c ---[ 0]---> BDD-cost: 6 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 42588 143418 | 14196 0 0 nan | 0.000 % | c | 100 | 42588 143418 | 15615 100 1381 13.8 | 4.341 % | c | 250 | 42583 143405 | 17177 248 1825 7.4 | 4.360 % | c | 476 | 42562 143336 | 18894 468 2925 6.2 | 4.387 % | c | 813 | 42546 143282 | 20784 803 5007 6.2 | 4.406 % | c | 1319 | 42513 143171 | 22862 1301 7660 5.9 | 4.462 % | c | 2079 | 42487 143083 | 25149 2048 11155 5.4 | 4.508 % | c | 3220 | 42465 143013 | 27663 3175 21980 6.9 | 4.545 % | c | 4928 | 42404 142811 | 30430 4729 29647 6.3 | 4.676 % | c | 7490 | 42302 142471 | 33473 7244 85196 11.8 | 4.852 % | c | 11334 | 42240 142263 | 36820 11072 126027 11.4 | 4.954 % | c | 17100 | 42234 142243 | 40502 14819 191852 12.9 | 4.982 % | c | 25750 | 42234 142243 | 44553 23469 868690 37.0 | 4.982 % | c | 38724 | 42234 142243 | 49008 36443 2774011 76.1 | 4.982 % | c | 58186 | 42234 142243 | 53909 16247 841211 51.8 | 4.982 % | c | 87380 | 42225 142212 | 59300 45438 3613633 79.5 | 4.992 % | c | 131169 | 42181 142066 | 65230 40602 1529090 37.7 | 5.112 % | c | 196854 | 42181 142066 | 71753 50993 6418011 125.9 | 5.112 % | c | 295380 | 42181 142066 | 78928 29223 7186333 245.9 | 5.112 % | c | 443169 | 42181 142066 | 86821 45867 13533259 295.1 | 5.112 % |
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/30972/stat): 30972 (minisat+_script) R 30971 30972 20602 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1720908837 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/30972/statm): 174 3 169 147 0 27 0 [pid=30972] vsize: 696 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libtermcap.so.2 open syscall for file tls/i686/libtermcap.so.2 open syscall for file tls/mmx/libtermcap.so.2 open syscall for file tls/libtermcap.so.2 open syscall for file i686/mmx/libtermcap.so.2 open syscall for file i686/libtermcap.so.2 open syscall for file mmx/libtermcap.so.2 open syscall for file libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/libtermcap.so.2 open syscall for file /etc/ld.so.cache open syscall for file /lib/libtermcap.so.2 open syscall for file tls/i686/mmx/libdl.so.2 open syscall for file tls/i686/libdl.so.2 open syscall for file tls/mmx/libdl.so.2 open syscall for file tls/libdl.so.2 open syscall for file i686/mmx/libdl.so.2 open syscall for file i686/libdl.so.2 open syscall for file mmx/libdl.so.2 open syscall for file libdl.so.2 open syscall for file /oldhome/oroussel/lib/libdl.so.2 open syscall for file /lib/libdl.so.2 open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /lib/tls/libc.so.6 open syscall for file /dev/tty open syscall for file /etc/mtab open syscall for file /proc/meminfo open syscall for file /oldhome/oroussel/solvers/minisat+_script New process pid=30973 New process pid=30974 New process pid=30975 execve syscall for /bin/sed executable open syscall for file /etc/ld.so.preload One traced child (pid=30974) exited with status: 0 open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=30975) exited with status: 0 One traced child (pid=30973) exited with status: 0 New process pid=30976 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc21/normalized-ss97-4.opb [startup+10.0031 s] Raw data (loadavg): 0.93 0.95 0.90 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 1415 0 0 0 983 7 0 0 25 0 1 0 1720908842 6316032 1360 4294967295 134512640 135094434 3221224448 3221223104 134557920 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30976/statm): 1542 1360 145 145 0 1397 0 [pid=30976] vsize: 6168 Current children cumulated CPU time (s) 9.91 Current children cumulated vsize (Kb) 8292 [startup+20.0038 s] Raw data (loadavg): 0.94 0.96 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 2536 0 0 0 1968 13 0 0 25 0 1 0 1720908842 10903552 2481 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30976/statm): 2662 2481 145 145 0 2517 0 [pid=30976] vsize: 10648 Current children cumulated CPU time (s) 19.82 Current children cumulated vsize (Kb) 12772 [startup+30.0044 s] Raw data (loadavg): 0.95 0.96 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 3902 0 0 0 2947 23 0 0 25 0 1 0 1720908842 16609280 3847 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30976/statm): 4055 3847 145 145 0 3910 0 [pid=30976] vsize: 16220 Current children cumulated CPU time (s) 29.71 Current children cumulated vsize (Kb) 18344 [startup+40.0051 s] Raw data (loadavg): 0.95 0.96 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 5049 0 0 0 3932 29 0 0 25 0 1 0 1720908842 21237760 4994 4294967295 134512640 135094434 3221224448 3221223040 134557404 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30976/statm): 5185 4994 145 145 0 5040 0 [pid=30976] vsize: 20740 Current children cumulated CPU time (s) 39.62 Current children cumulated vsize (Kb) 22864 [startup+50.0058 s] Raw data (loadavg): 0.96 0.96 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 5406 0 0 0 4926 33 0 0 25 0 1 0 1720908842 22712320 5351 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30976/statm): 5545 5351 145 145 0 5400 0 [pid=30976] vsize: 22180 Current children cumulated CPU time (s) 49.6 Current children cumulated vsize (Kb) 24304 [startup+60.0065 s] Raw data (loadavg): 0.97 0.96 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 5406 0 0 0 5926 33 0 0 25 0 1 0 1720908842 22712320 5351 4294967295 134512640 135094434 3221224448 3221223112 134562037 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30976/statm): 5545 5351 145 145 0 5400 0 [pid=30976] vsize: 22180 Current children cumulated CPU time (s) 59.6 Current children cumulated vsize (Kb) 24304 [startup+70.0071 s] Raw data (loadavg): 0.97 0.96 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 5406 0 0 0 6926 33 0 0 25 0 1 0 1720908842 22712320 5351 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 5545 5351 145 145 0 5400 0 [pid=30976] vsize: 22180 Current children cumulated CPU time (s) 69.6 Current children cumulated vsize (Kb) 24304 [startup+80.0078 s] Raw data (loadavg): 0.98 0.96 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 6032 0 0 0 7917 37 0 0 25 0 1 0 1720908842 25268224 5977 4294967295 134512640 135094434 3221224448 3221223120 134556450 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 6169 5977 145 145 0 6024 0 [pid=30976] vsize: 24676 Current children cumulated CPU time (s) 79.55 Current children cumulated vsize (Kb) 26800 [startup+90.0085 s] Raw data (loadavg): 0.98 0.96 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 6347 0 0 0 8912 39 0 0 25 0 1 0 1720908842 26550272 6292 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 6482 6292 145 145 0 6337 0 [pid=30976] vsize: 25928 Current children cumulated CPU time (s) 89.52 Current children cumulated vsize (Kb) 28052 [startup+100.009 s] Raw data (loadavg): 0.98 0.96 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 6347 0 0 0 9913 39 0 0 25 0 1 0 1720908842 26550272 6292 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 6482 6292 145 145 0 6337 0 [pid=30976] vsize: 25928 Current children cumulated CPU time (s) 99.53 Current children cumulated vsize (Kb) 28052 [startup+110.01 s] Raw data (loadavg): 0.98 0.96 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 6347 0 0 0 10913 39 0 0 25 0 1 0 1720908842 26550272 6292 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 6482 6292 145 145 0 6337 0 [pid=30976] vsize: 25928 Current children cumulated CPU time (s) 109.53 Current children cumulated vsize (Kb) 28052 [startup+120.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 6348 0 0 0 11913 39 0 0 25 0 1 0 1720908842 26550272 6293 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 6482 6293 145 145 0 6337 0 [pid=30976] vsize: 25928 Current children cumulated CPU time (s) 119.53 Current children cumulated vsize (Kb) 28052 [startup+130.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 6819 0 0 0 12906 41 0 0 25 0 1 0 1720908842 28717056 6764 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30976/statm): 7011 6764 145 145 0 6866 0 [pid=30976] vsize: 28044 Current children cumulated CPU time (s) 129.48 Current children cumulated vsize (Kb) 30168 [startup+140.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 6819 0 0 0 13906 41 0 0 25 0 1 0 1720908842 28717056 6764 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 7011 6764 145 145 0 6866 0 [pid=30976] vsize: 28044 Current children cumulated CPU time (s) 139.48 Current children cumulated vsize (Kb) 30168 [startup+150.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 6819 0 0 0 14906 41 0 0 25 0 1 0 1720908842 28717056 6764 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 7011 6764 145 145 0 6866 0 [pid=30976] vsize: 28044 Current children cumulated CPU time (s) 149.48 Current children cumulated vsize (Kb) 30168 [startup+160.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 7937 0 0 0 15887 49 0 0 25 0 1 0 1720908842 33296384 7882 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 8129 7882 145 145 0 7984 0 [pid=30976] vsize: 32516 Current children cumulated CPU time (s) 159.37 Current children cumulated vsize (Kb) 34640 [startup+170.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 8918 0 0 0 16870 55 0 0 25 0 1 0 1720908842 37318656 8863 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30976/statm): 9111 8863 145 145 0 8966 0 [pid=30976] vsize: 36444 Current children cumulated CPU time (s) 169.26 Current children cumulated vsize (Kb) 38568 [startup+180.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 9847 0 0 0 17854 62 0 0 25 0 1 0 1720908842 41123840 9792 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30976/statm): 10040 9792 145 145 0 9895 0 [pid=30976] vsize: 40160 Current children cumulated CPU time (s) 179.17 Current children cumulated vsize (Kb) 42284 [startup+190.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 10706 0 0 0 18841 67 0 0 25 0 1 0 1720908842 44642304 10651 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 10899 10651 145 145 0 10754 0 [pid=30976] vsize: 43596 Current children cumulated CPU time (s) 189.09 Current children cumulated vsize (Kb) 45720 [startup+200.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 11176 0 0 0 19834 70 0 0 25 0 1 0 1720908842 46546944 11121 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 11364 11121 145 145 0 11219 0 [pid=30976] vsize: 45456 Current children cumulated CPU time (s) 199.05 Current children cumulated vsize (Kb) 47580 [startup+210.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 11176 0 0 0 20834 70 0 0 25 0 1 0 1720908842 46546944 11121 4294967295 134512640 135094434 3221224448 3221223060 134563083 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 11364 11121 145 145 0 11219 0 [pid=30976] vsize: 45456 Current children cumulated CPU time (s) 209.05 Current children cumulated vsize (Kb) 47580 [startup+220.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 11176 0 0 0 21834 70 0 0 25 0 1 0 1720908842 46546944 11121 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 11364 11121 145 145 0 11219 0 [pid=30976] vsize: 45456 Current children cumulated CPU time (s) 219.05 Current children cumulated vsize (Kb) 47580 [startup+230.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 11176 0 0 0 22834 70 0 0 25 0 1 0 1720908842 46546944 11121 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 11364 11121 145 145 0 11219 0 [pid=30976] vsize: 45456 Current children cumulated CPU time (s) 229.05 Current children cumulated vsize (Kb) 47580 [startup+240.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 11176 0 0 0 23835 70 0 0 25 0 1 0 1720908842 46546944 11121 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 11364 11121 145 145 0 11219 0 [pid=30976] vsize: 45456 Current children cumulated CPU time (s) 239.06 Current children cumulated vsize (Kb) 47580 [startup+250.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 11176 0 0 0 24835 70 0 0 25 0 1 0 1720908842 46546944 11121 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 11364 11121 145 145 0 11219 0 [pid=30976] vsize: 45456 Current children cumulated CPU time (s) 249.06 Current children cumulated vsize (Kb) 47580 [startup+260.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 11178 0 0 0 25835 70 0 0 25 0 1 0 1720908842 46546944 11123 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 11364 11123 145 145 0 11219 0 [pid=30976] vsize: 45456 Current children cumulated CPU time (s) 259.06 Current children cumulated vsize (Kb) 47580 [startup+270.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 11178 0 0 0 26835 70 0 0 25 0 1 0 1720908842 46546944 11123 4294967295 134512640 135094434 3221224448 3221223104 134558011 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 11364 11123 145 145 0 11219 0 [pid=30976] vsize: 45456 Current children cumulated CPU time (s) 269.06 Current children cumulated vsize (Kb) 47580 [startup+280.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 11178 0 0 0 27836 70 0 0 25 0 1 0 1720908842 46546944 11123 4294967295 134512640 135094434 3221224448 3221223104 134558029 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 11364 11123 145 145 0 11219 0 [pid=30976] vsize: 45456 Current children cumulated CPU time (s) 279.07 Current children cumulated vsize (Kb) 47580 [startup+290.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 11178 0 0 0 28836 70 0 0 25 0 1 0 1720908842 46546944 11123 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 11364 11123 145 145 0 11219 0 [pid=30976] vsize: 45456 Current children cumulated CPU time (s) 289.07 Current children cumulated vsize (Kb) 47580 [startup+300.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 11178 0 0 0 29836 70 0 0 25 0 1 0 1720908842 46546944 11123 4294967295 134512640 135094434 3221224448 3221223060 134563071 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30976/statm): 11364 11123 145 145 0 11219 0 [pid=30976] vsize: 45456 Current children cumulated CPU time (s) 299.07 Current children cumulated vsize (Kb) 47580 [startup+310.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 11178 0 0 0 30835 71 0 0 25 0 1 0 1720908842 46546944 11123 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30976/statm): 11364 11123 145 145 0 11219 0 [pid=30976] vsize: 45456 Current children cumulated CPU time (s) 309.07 Current children cumulated vsize (Kb) 47580 [startup+320.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 11864 0 0 0 31824 75 0 0 25 0 1 0 1720908842 49364992 11809 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30976/statm): 12052 11809 145 145 0 11907 0 [pid=30976] vsize: 48208 Current children cumulated CPU time (s) 319 Current children cumulated vsize (Kb) 50332 [startup+330.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 12858 0 0 0 32806 83 0 0 25 0 1 0 1720908842 53428224 12803 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30976/statm): 13044 12803 145 145 0 12899 0 [pid=30976] vsize: 52176 Current children cumulated CPU time (s) 328.9 Current children cumulated vsize (Kb) 54300 [startup+340.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 13828 0 0 0 33790 90 0 0 25 0 1 0 1720908842 57438208 13773 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 14023 13773 145 145 0 13878 0 [pid=30976] vsize: 56092 Current children cumulated CPU time (s) 338.81 Current children cumulated vsize (Kb) 58216 [startup+350.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 14636 0 0 0 34777 95 0 0 25 0 1 0 1720908842 60776448 14581 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 14838 14581 145 145 0 14693 0 [pid=30976] vsize: 59352 Current children cumulated CPU time (s) 348.73 Current children cumulated vsize (Kb) 61476 [startup+360.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 15309 0 0 0 35767 99 0 0 25 0 1 0 1720908842 63545344 15254 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 15514 15254 145 145 0 15369 0 [pid=30976] vsize: 62056 Current children cumulated CPU time (s) 358.67 Current children cumulated vsize (Kb) 64180 [startup+370.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) T 30972 30972 20602 0 -1 0 16034 0 0 0 36756 104 0 0 25 0 1 0 1720908842 66502656 15979 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/30976/statm): 16236 15979 145 145 0 16091 0 [pid=30976] vsize: 64944 Current children cumulated CPU time (s) 368.61 Current children cumulated vsize (Kb) 67068 [startup+380.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 17018 0 0 0 37740 110 0 0 25 0 1 0 1720908842 70508544 16963 4294967295 134512640 135094434 3221224448 3221223040 134551465 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 17214 16963 145 145 0 17069 0 [pid=30976] vsize: 68856 Current children cumulated CPU time (s) 378.51 Current children cumulated vsize (Kb) 70980 [startup+390.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 17018 0 0 0 38740 110 0 0 25 0 1 0 1720908842 70508544 16963 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 17214 16963 145 145 0 17069 0 [pid=30976] vsize: 68856 Current children cumulated CPU time (s) 388.51 Current children cumulated vsize (Kb) 70980 [startup+400.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 17018 0 0 0 39740 110 0 0 25 0 1 0 1720908842 70508544 16963 4294967295 134512640 135094434 3221224448 3221223040 134557175 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 17214 16963 145 145 0 17069 0 [pid=30976] vsize: 68856 Current children cumulated CPU time (s) 398.51 Current children cumulated vsize (Kb) 70980 [startup+410.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 17018 0 0 0 40741 110 0 0 25 0 1 0 1720908842 70508544 16963 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 17214 16963 145 145 0 17069 0 [pid=30976] vsize: 68856 Current children cumulated CPU time (s) 408.52 Current children cumulated vsize (Kb) 70980 [startup+420.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 17018 0 0 0 41741 110 0 0 25 0 1 0 1720908842 70508544 16963 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 17214 16963 145 145 0 17069 0 [pid=30976] vsize: 68856 Current children cumulated CPU time (s) 418.52 Current children cumulated vsize (Kb) 70980 [startup+430.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 17018 0 0 0 42741 110 0 0 25 0 1 0 1720908842 70508544 16963 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 17214 16963 145 145 0 17069 0 [pid=30976] vsize: 68856 Current children cumulated CPU time (s) 428.52 Current children cumulated vsize (Kb) 70980 [startup+440.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 17018 0 0 0 43741 110 0 0 25 0 1 0 1720908842 70508544 16963 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 17214 16963 145 145 0 17069 0 [pid=30976] vsize: 68856 Current children cumulated CPU time (s) 438.52 Current children cumulated vsize (Kb) 70980 [startup+450.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 17018 0 0 0 44742 110 0 0 25 0 1 0 1720908842 70508544 16963 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 17214 16963 145 145 0 17069 0 [pid=30976] vsize: 68856 Current children cumulated CPU time (s) 448.53 Current children cumulated vsize (Kb) 70980 [startup+460.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 17018 0 0 0 45742 110 0 0 25 0 1 0 1720908842 70508544 16963 4294967295 134512640 135094434 3221224448 3221223040 134551906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 17214 16963 145 145 0 17069 0 [pid=30976] vsize: 68856 Current children cumulated CPU time (s) 458.53 Current children cumulated vsize (Kb) 70980 [startup+470.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 17018 0 0 0 46742 110 0 0 25 0 1 0 1720908842 70508544 16963 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 17214 16963 145 145 0 17069 0 [pid=30976] vsize: 68856 Current children cumulated CPU time (s) 468.53 Current children cumulated vsize (Kb) 70980 [startup+480.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 17018 0 0 0 47742 110 0 0 25 0 1 0 1720908842 70508544 16963 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 17214 16963 145 145 0 17069 0 [pid=30976] vsize: 68856 Current children cumulated CPU time (s) 478.53 Current children cumulated vsize (Kb) 70980 [startup+490.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 17018 0 0 0 48743 110 0 0 25 0 1 0 1720908842 70508544 16963 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 17214 16963 145 145 0 17069 0 [pid=30976] vsize: 68856 Current children cumulated CPU time (s) 488.54 Current children cumulated vsize (Kb) 70980 [startup+500.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 17251 0 0 0 49739 112 0 0 25 0 1 0 1720908842 71462912 17196 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 17447 17196 145 145 0 17302 0 [pid=30976] vsize: 69788 Current children cumulated CPU time (s) 498.52 Current children cumulated vsize (Kb) 71912 [startup+510.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 18079 0 0 0 50725 118 0 0 25 0 1 0 1720908842 74862592 18024 4294967295 134512640 135094434 3221224448 3221223040 134557168 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 18277 18024 145 145 0 18132 0 [pid=30976] vsize: 73108 Current children cumulated CPU time (s) 508.44 Current children cumulated vsize (Kb) 75232 [startup+520.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 18629 0 0 0 51715 122 0 0 25 0 1 0 1720908842 77119488 18574 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 18828 18574 145 145 0 18683 0 [pid=30976] vsize: 75312 Current children cumulated CPU time (s) 518.38 Current children cumulated vsize (Kb) 77436 [startup+530.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 19152 0 0 0 52705 126 0 0 25 0 1 0 1720908842 79269888 19097 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 19353 19097 145 145 0 19208 0 [pid=30976] vsize: 77412 Current children cumulated CPU time (s) 528.32 Current children cumulated vsize (Kb) 79536 [startup+540.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 19882 0 0 0 53693 131 0 0 25 0 1 0 1720908842 82255872 19827 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 20082 19827 145 145 0 19937 0 [pid=30976] vsize: 80328 Current children cumulated CPU time (s) 538.25 Current children cumulated vsize (Kb) 82452 [startup+550.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 20538 0 0 0 54684 134 0 0 25 0 1 0 1720908842 84955136 20483 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 20741 20483 145 145 0 20596 0 [pid=30976] vsize: 82964 Current children cumulated CPU time (s) 548.19 Current children cumulated vsize (Kb) 85088 [startup+560.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 21167 0 0 0 55673 138 0 0 25 0 1 0 1720908842 87539712 21112 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 21372 21112 145 145 0 21227 0 [pid=30976] vsize: 85488 Current children cumulated CPU time (s) 558.12 Current children cumulated vsize (Kb) 87612 [startup+570.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 21794 0 0 0 56661 143 0 0 25 0 1 0 1720908842 90120192 21739 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 22002 21739 145 145 0 21857 0 [pid=30976] vsize: 88008 Current children cumulated CPU time (s) 568.05 Current children cumulated vsize (Kb) 90132 [startup+580.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 22375 0 0 0 57654 146 0 0 25 0 1 0 1720908842 92495872 22320 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 22582 22320 145 145 0 22437 0 [pid=30976] vsize: 90328 Current children cumulated CPU time (s) 578.01 Current children cumulated vsize (Kb) 92452 [startup+590.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 22943 0 0 0 58645 149 0 0 25 0 1 0 1720908842 94822400 22888 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 23150 22888 145 145 0 23005 0 [pid=30976] vsize: 92600 Current children cumulated CPU time (s) 587.95 Current children cumulated vsize (Kb) 94724 [startup+600.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 23511 0 0 0 59634 154 0 0 25 0 1 0 1720908842 97157120 23456 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 23720 23456 145 145 0 23575 0 [pid=30976] vsize: 94880 Current children cumulated CPU time (s) 597.89 Current children cumulated vsize (Kb) 97004 [startup+610.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 24005 0 0 0 60627 157 0 0 25 0 1 0 1720908842 99192832 23950 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 24217 23950 145 145 0 24072 0 [pid=30976] vsize: 96868 Current children cumulated CPU time (s) 607.85 Current children cumulated vsize (Kb) 98992 [startup+620.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 24554 0 0 0 61617 161 0 0 25 0 1 0 1720908842 101441536 24499 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 24766 24499 145 145 0 24621 0 [pid=30976] vsize: 99064 Current children cumulated CPU time (s) 617.79 Current children cumulated vsize (Kb) 101188 [startup+630.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 25138 0 0 0 62608 164 0 0 25 0 1 0 1720908842 103833600 25083 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 25350 25083 145 145 0 25205 0 [pid=30976] vsize: 101400 Current children cumulated CPU time (s) 627.73 Current children cumulated vsize (Kb) 103524 [startup+640.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 25772 0 0 0 63599 169 0 0 25 0 1 0 1720908842 106434560 25717 4294967295 134512640 135094434 3221224448 3221223104 134555975 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 25985 25717 145 145 0 25840 0 [pid=30976] vsize: 103940 Current children cumulated CPU time (s) 637.69 Current children cumulated vsize (Kb) 106064 [startup+650.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26286 0 0 0 64590 172 0 0 25 0 1 0 1720908842 108552192 26231 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26502 26231 145 145 0 26357 0 [pid=30976] vsize: 106008 Current children cumulated CPU time (s) 647.63 Current children cumulated vsize (Kb) 108132 [startup+660.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26583 0 0 0 65586 174 0 0 25 0 1 0 1720908842 109768704 26528 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26528 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 657.61 Current children cumulated vsize (Kb) 109320 [startup+670.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26583 0 0 0 66586 174 0 0 25 0 1 0 1720908842 109768704 26528 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26528 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 667.61 Current children cumulated vsize (Kb) 109320 [startup+680.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26583 0 0 0 67586 174 0 0 25 0 1 0 1720908842 109768704 26528 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26528 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 677.61 Current children cumulated vsize (Kb) 109320 [startup+690.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26583 0 0 0 68586 174 0 0 25 0 1 0 1720908842 109768704 26528 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26528 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 687.61 Current children cumulated vsize (Kb) 109320 [startup+700.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26584 0 0 0 69586 175 0 0 25 0 1 0 1720908842 109768704 26529 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26529 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 697.62 Current children cumulated vsize (Kb) 109320 [startup+710.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26585 0 0 0 70587 175 0 0 25 0 1 0 1720908842 109768704 26530 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26530 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 707.63 Current children cumulated vsize (Kb) 109320 [startup+720.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26585 0 0 0 71587 175 0 0 25 0 1 0 1720908842 109768704 26530 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26530 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 717.63 Current children cumulated vsize (Kb) 109320 [startup+730.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26585 0 0 0 72587 175 0 0 25 0 1 0 1720908842 109768704 26530 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26530 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 727.63 Current children cumulated vsize (Kb) 109320 [startup+740.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26585 0 0 0 73587 175 0 0 25 0 1 0 1720908842 109768704 26530 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26530 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 737.63 Current children cumulated vsize (Kb) 109320 [startup+750.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26585 0 0 0 74588 175 0 0 25 0 1 0 1720908842 109768704 26530 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26530 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 747.64 Current children cumulated vsize (Kb) 109320 [startup+760.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26585 0 0 0 75588 175 0 0 25 0 1 0 1720908842 109768704 26530 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26530 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 757.64 Current children cumulated vsize (Kb) 109320 [startup+770.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26585 0 0 0 76588 175 0 0 25 0 1 0 1720908842 109768704 26530 4294967295 134512640 135094434 3221224448 3221223060 134563140 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26530 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 767.64 Current children cumulated vsize (Kb) 109320 [startup+780.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26585 0 0 0 77588 175 0 0 25 0 1 0 1720908842 109768704 26530 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26530 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 777.64 Current children cumulated vsize (Kb) 109320 [startup+790.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26585 0 0 0 78588 175 0 0 25 0 1 0 1720908842 109768704 26530 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26530 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 787.64 Current children cumulated vsize (Kb) 109320 [startup+800.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26585 0 0 0 79589 175 0 0 25 0 1 0 1720908842 109768704 26530 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26530 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 797.65 Current children cumulated vsize (Kb) 109320 [startup+810.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26585 0 0 0 80589 175 0 0 25 0 1 0 1720908842 109768704 26530 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26530 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 807.65 Current children cumulated vsize (Kb) 109320 [startup+820.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26585 0 0 0 81589 175 0 0 25 0 1 0 1720908842 109768704 26530 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26530 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 817.65 Current children cumulated vsize (Kb) 109320 [startup+830.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26585 0 0 0 82589 175 0 0 25 0 1 0 1720908842 109768704 26530 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26530 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 827.65 Current children cumulated vsize (Kb) 109320 [startup+840.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26587 0 0 0 83589 175 0 0 25 0 1 0 1720908842 109768704 26532 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26532 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 837.65 Current children cumulated vsize (Kb) 109320 [startup+850.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26589 0 0 0 84590 175 0 0 25 0 1 0 1720908842 109768704 26534 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26534 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 847.66 Current children cumulated vsize (Kb) 109320 [startup+860.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26592 0 0 0 85590 175 0 0 25 0 1 0 1720908842 109768704 26537 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26537 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 857.66 Current children cumulated vsize (Kb) 109320 [startup+870.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 86590 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223040 134557509 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 867.66 Current children cumulated vsize (Kb) 109320 [startup+880.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 87590 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223040 134557263 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 877.66 Current children cumulated vsize (Kb) 109320 [startup+890.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 88591 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 887.67 Current children cumulated vsize (Kb) 109320 [startup+900.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 89591 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223120 134556252 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 897.67 Current children cumulated vsize (Kb) 109320 [startup+910.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 90591 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 907.67 Current children cumulated vsize (Kb) 109320 [startup+920.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 91591 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 917.67 Current children cumulated vsize (Kb) 109320 [startup+930.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 92592 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 927.68 Current children cumulated vsize (Kb) 109320 [startup+940.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 93592 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223040 134557277 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 937.68 Current children cumulated vsize (Kb) 109320 [startup+950.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 94592 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 947.68 Current children cumulated vsize (Kb) 109320 [startup+960.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 95592 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 957.68 Current children cumulated vsize (Kb) 109320 [startup+970.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 96593 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223040 134557429 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 967.69 Current children cumulated vsize (Kb) 109320 [startup+980.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 97593 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223040 134557275 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 977.69 Current children cumulated vsize (Kb) 109320 [startup+990.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 98593 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223040 134551702 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 987.69 Current children cumulated vsize (Kb) 109320 [startup+1000.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 99593 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 997.69 Current children cumulated vsize (Kb) 109320 [startup+1010.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 100594 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 1007.7 Current children cumulated vsize (Kb) 109320 [startup+1020.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 101594 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 1017.7 Current children cumulated vsize (Kb) 109320 [startup+1030.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 102594 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 1027.7 Current children cumulated vsize (Kb) 109320 [startup+1040.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 103594 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223040 134557488 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 1037.7 Current children cumulated vsize (Kb) 109320 [startup+1050.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 104594 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 1047.7 Current children cumulated vsize (Kb) 109320 [startup+1060.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 105595 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 1057.71 Current children cumulated vsize (Kb) 109320 [startup+1070.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 106595 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 1067.71 Current children cumulated vsize (Kb) 109320 [startup+1080.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 107595 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 1077.71 Current children cumulated vsize (Kb) 109320 [startup+1090.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 108595 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223040 134557271 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 1087.71 Current children cumulated vsize (Kb) 109320 [startup+1100.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 109596 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 1097.72 Current children cumulated vsize (Kb) 109320 [startup+1110.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26595 0 0 0 110596 175 0 0 25 0 1 0 1720908842 109768704 26540 4294967295 134512640 135094434 3221224448 3221223120 134556410 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26540 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 1107.72 Current children cumulated vsize (Kb) 109320 [startup+1120.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26595 0 0 0 111596 175 0 0 25 0 1 0 1720908842 109768704 26540 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26540 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 1117.72 Current children cumulated vsize (Kb) 109320 [startup+1130.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26595 0 0 0 112596 175 0 0 25 0 1 0 1720908842 109768704 26540 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26540 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 1127.72 Current children cumulated vsize (Kb) 109320 [startup+1140.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26595 0 0 0 113597 175 0 0 25 0 1 0 1720908842 109768704 26540 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 26799 26540 145 145 0 26654 0 [pid=30976] vsize: 107196 Current children cumulated CPU time (s) 1137.73 Current children cumulated vsize (Kb) 109320 [startup+1150.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26817 0 0 0 114593 177 0 0 25 0 1 0 1720908842 110678016 26762 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 27021 26762 145 145 0 26876 0 [pid=30976] vsize: 108084 Current children cumulated CPU time (s) 1147.71 Current children cumulated vsize (Kb) 110208 [startup+1160.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 27325 0 0 0 115584 181 0 0 25 0 1 0 1720908842 112787456 27270 4294967295 134512640 135094434 3221224448 3221223060 134563124 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 27536 27270 145 145 0 27391 0 [pid=30976] vsize: 110144 Current children cumulated CPU time (s) 1157.66 Current children cumulated vsize (Kb) 112268 [startup+1170.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 27465 0 0 0 116582 181 0 0 25 0 1 0 1720908842 113381376 27410 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 27681 27410 145 145 0 27536 0 [pid=30976] vsize: 110724 Current children cumulated CPU time (s) 1167.64 Current children cumulated vsize (Kb) 112848 [startup+1180.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 27695 0 0 0 117579 183 0 0 25 0 1 0 1720908842 114331648 27640 4294967295 134512640 135094434 3221224448 3221222928 134780803 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 27913 27640 145 145 0 27768 0 [pid=30976] vsize: 111652 Current children cumulated CPU time (s) 1177.63 Current children cumulated vsize (Kb) 113776 [startup+1190.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 27695 0 0 0 118579 183 0 0 25 0 1 0 1720908842 114331648 27640 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 27913 27640 145 145 0 27768 0 [pid=30976] vsize: 111652 Current children cumulated CPU time (s) 1187.63 Current children cumulated vsize (Kb) 113776 [startup+1200.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 27695 0 0 0 119579 183 0 0 25 0 1 0 1720908842 114331648 27640 4294967295 134512640 135094434 3221224448 3221223040 134557413 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 27913 27640 145 145 0 27768 0 [pid=30976] vsize: 111652 Current children cumulated CPU time (s) 1197.63 Current children cumulated vsize (Kb) 113776 [startup+1210.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 27695 0 0 0 120579 183 0 0 25 0 1 0 1720908842 114331648 27640 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 27913 27640 145 145 0 27768 0 [pid=30976] vsize: 111652 Current children cumulated CPU time (s) 1207.63 Current children cumulated vsize (Kb) 113776 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 30976 Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/30972/statm): 531 226 485 147 0 384 0 [pid=30972] vsize: 2124 Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 27695 0 0 0 120579 183 0 0 25 0 1 0 1720908842 114331648 27640 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30976/statm): 27913 27640 145 145 0 27768 0 [pid=30976] vsize: 111652 Current children cumulated CPU time (s) 1207.63 Current children cumulated vsize (Kb) 113776 Sending SIGTERM to -30972 Sleeping 2 seconds One traced child (pid=30972) ended because it received signal 15 (SIGTERM) One traced child (pid=30976) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.13 CPU time (s): 1207.69 CPU user time (s): 1205.8 CPU system time (s): 1.88471 CPU usage (%): 99.7982 Max. virtual memory (cumulated for all children) (Kb): 113776
ERROR: no interpretation found !