Name | mps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-d6cube.opb |
MD5SUM | 889599bea53ff906bd4dd516c552c027 |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | NO |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 123680 |
Biggest coefficient in the objective function | 524288 |
Number of bits for the biggest coefficient in the objective function | 20 |
Sum of the numbers in the objective function | 6484387800 |
Number of bits of the sum of numbers in the objective function | 33 |
Biggest number in a constraint | 188743680 |
Number of bits of the biggest number in a constraint | 28 |
Biggest sum of numbers in a constraint | 10767194085 |
Number of bits of the biggest sum of numbers | 34 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 28.7566 |
Number of variables | 123680 |
Total number of constraints | 404 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 404 |
Minimum length of a constraint | 20 |
Maximum length of a constraint | 123680 |
LAUNCH ON wulflinc22 THE 2005-09-20 02:35:17 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3149 boxname=wulflinc22 idbench=805 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 889599bea53ff906bd4dd516c552c027 /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-d6cube.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-d6cube.opb IDLAUNCH: 3149 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.031 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.031 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 890008 kB Buffers: 1796 kB Cached: 115564 kB SwapCached: 484 kB Active: 29368 kB Inactive: 90424 kB HighTotal: 131008 kB HighFree: 11872 kB LowTotal: 903652 kB LowFree: 878136 kB SwapTotal: 2097892 kB SwapFree: 2096748 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5676 kB Slab: 18996 kB Committed_AS: 64132 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 02:55:28 (client local time) WITH STATUS 0 IN 1202.14 SECONDS stats: 3149 7 1202.14 0
c Parsing PB file... c Converting 808 PB-constraints to clauses... c -- Unit propagations: pppp c -- Detecting intervals from adjacent constraints: ################################################################################################################################################################################################################################################################################################################################################################################################################### c -- Clauses(.)/Splits(s): (none) c ---[ 806]---> Adder-cost: 1066 maxlim: 2752486 bits: 22/22 c ---[ 804]---> Sorter-cost: 1184 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 802]---> Adder-cost: 782 maxlim: 1376234 bits: 21/21 c ---[ 800]---> Adder-cost: 482 maxlim: 688118 bits: 21/20 c ---[ 798]---> Adder-cost: 1006 maxlim: 1867753 bits: 22/21 c ---[ 796]---> Adder-cost: 614 maxlim: 1048562 bits: 21/20 c ---[ 794]---> Adder-cost: 970 maxlim: 1867753 bits: 22/21 c ---[ 792]---> Adder-cost: 1336 maxlim: 2621408 bits: 22/22 c ---[ 790]---> Adder-cost: 1396 maxlim: 2654175 bits: 22/22 c ---[ 788]---> Adder-cost: 1366 maxlim: 2654175 bits: 22/22 c ---[ 786]---> Adder-cost: 920 maxlim: 2031594 bits: 22/21 c ---[ 784]---> Adder-cost: 1010 maxlim: 1834986 bits: 22/21 c ---[ 782]---> Adder-cost: 1004 maxlim: 1900520 bits: 22/21 c ---[ 780]---> Adder-cost: 1366 maxlim: 2686942 bits: 22/22 c ---[ 778]---> Adder-cost: 552 maxlim: 1146868 bits: 21/21 c ---[ 776]---> Adder-cost: 948 maxlim: 1802219 bits: 22/21 c ---[ 774]---> Adder-cost: 1538 maxlim: 2293734 bits: 23/22 c ---[ 772]---> Adder-cost: 1537 maxlim: 2293734 bits: 23/22 c ---[ 770]---> Adder-cost: 644 maxlim: 1114096 bits: 21/21 c ---[ 768]---> Adder-cost: 1062 maxlim: 1933285 bits: 22/21 c ---[ 766]---> Adder-cost: 1092 maxlim: 1900518 bits: 22/21 c ---[ 764]---> Adder-cost: 644 maxlim: 1179631 bits: 21/21 c ---[ 762]---> Adder-cost: 1017 maxlim: 1048558 bits: 21/20 c ---[ 760]---> Adder-cost: 1184 maxlim: 1277932 bits: 22/21 c ---[ 758]---> Adder-cost: 730 maxlim: 688116 bits: 21/20 c ---[ 756]---> Adder-cost: 934 maxlim: 1179631 bits: 22/21 c ---[ 754]---> Adder-cost: 310 maxlim: 393208 bits: 20/19 c ---[ 752]---> Adder-cost: 602 maxlim: 786420 bits: 21/20 c ---[ 750]---> Adder-cost: 934 maxlim: 1441774 bits: 22/21 c ---[ 748]---> Adder-cost: 348 maxlim: 491512 bits: 20/19 c ---[ 746]---> Adder-cost: 332 maxlim: 393206 bits: 19/19 c ---[ 744]---> Adder-cost: 810 maxlim: 1392621 bits: 22/21 c ---[ 742]---> Adder-cost: 902 maxlim: 1638378 bits: 22/21 c ---[ 740]---> Adder-cost: 902 maxlim: 1638378 bits: 22/21 c ---[ 738]---> Adder-cost: 1446 maxlim: 2850777 bits: 22/22 c ---[ 736]---> Adder-cost: 1022 maxlim: 1245164 bits: 22/21 c ---[ 734]---> Adder-cost: 578 maxlim: 524280 bits: 20/19 c ---[ 732]---> Adder-cost: 798 maxlim: 851955 bits: 21/20 c ---[ 730]---> Adder-cost: 1288 maxlim: 1572840 bits: 22/21 c ---[ 728]---> Adder-cost: 1286 maxlim: 1507306 bits: 22/21 c ---[ 726]---> Adder-cost: 948 maxlim: 1441778 bits: 22/21 c ---[ 724]---> Adder-cost: 1022 maxlim: 1179630 bits: 22/21 c ---[ 722]---> Adder-cost: 1286 maxlim: 1474539 bits: 22/21 c ---[ 720]---> Adder-cost: 949 maxlim: 1015797 bits: 21/20 c ---[ 718]---> Adder-cost: 749 maxlim: 819190 bits: 21/20 c ---[ 716]---> Adder-cost: 473 maxlim: 393209 bits: 20/19 c ---[ 714]---> Adder-cost: 905 maxlim: 1015793 bits: 21/20 c ---[ 712]---> Adder-cost: 1106 maxlim: 1900514 bits: 22/21 c ---[ 710]---> Adder-cost: 924 maxlim: 1572839 bits: 22/21 c ---[ 708]---> Adder-cost: 1410 maxlim: 2113505 bits: 22/22 c ---[ 706]---> Adder-cost: 1350 maxlim: 1982437 bits: 22/21 c ---[ 704]---> Adder-cost: 1408 maxlim: 2080738 bits: 22/21 c ---[ 702]---> Adder-cost: 1318 maxlim: 1966054 bits: 22/21 c ---[ 700]---> Adder-cost: 908 maxlim: 1409007 bits: 22/21 c ---[ 698]---> Adder-cost: 798 maxlim: 1146865 bits: 21/21 c ---[ 696]---> Adder-cost: 734 maxlim: 1114097 bits: 21/21 c ---[ 694]---> Adder-cost: 1260 maxlim: 1933287 bits: 22/21 c ---[ 692]---> Adder-cost: 836 maxlim: 1245166 bits: 22/21 c ---[ 690]---> Adder-cost: 1066 maxlim: 2949093 bits: 22/22 c ---[ 688]---> Adder-cost: 1080 maxlim: 1523688 bits: 22/21 c ---[ 686]---> Adder-cost: 886 maxlim: 1261549 bits: 21/21 c ---[ 684]---> Adder-cost: 748 maxlim: 540659 bits: 21/20 c ---[ 682]---> Adder-cost: 724 maxlim: 475126 bits: 20/19 c ---[ 680]---> Adder-cost: 659 maxlim: 442358 bits: 20/19 c ---[ 678]---> Adder-cost: 406 maxlim: 376825 bits: 20/19 c ---[ 676]---> Adder-cost: 520 maxlim: 688114 bits: 20/20 c ---[ 674]---> Adder-cost: 1037 maxlim: 884718 bits: 21/20 c ---[ 672]---> Adder-cost: 698 maxlim: 458744 bits: 20/19 c ---[ 670]---> Adder-cost: 1143 maxlim: 851953 bits: 21/20 c ---[ 668]---> Adder-cost: 533 maxlim: 360440 bits: 20/19 c ---[ 666]---> Adder-cost: 730 maxlim: 491511 bits: 20/19 c ---[ 664]---> Adder-cost: 1064 maxlim: 3145698 bits: 22/22 c ---[ 662]---> Adder-cost: 978 maxlim: 1196013 bits: 22/21 c ---[ 660]---> Adder-cost: 1334 maxlim: 1654758 bits: 22/21 c ---[ 658]---> Adder-cost: 896 maxlim: 1081329 bits: 22/21 c ---[ 656]---> Adder-cost: 630 maxlim: 770035 bits: 21/20 c ---[ 654]---> Adder-cost: 396 maxlim: 131066 bits: 18/17 c ---[ 652]---> Adder-cost: 426 maxlim: 442357 bits: 20/19 c ---[ 650]---> Adder-cost: 796 maxlim: 1228782 bits: 21/21 c ---[ 648]---> Adder-cost: 1052 maxlim: 1753062 bits: 22/21 c ---[ 646]---> Adder-cost: 766 maxlim: 1228782 bits: 21/21 c ---[ 644]---> Adder-cost: 704 maxlim: 409594 bits: 20/19 c ---[ 642]---> Adder-cost: 1300 maxlim: 1196011 bits: 22/21 c ---[ 640]---> Adder-cost: 631 maxlim: 475127 bits: 20/19 c ---[ 638]---> Adder-cost: 1085 maxlim: 901106 bits: 21/20 c ---[ 636]---> Adder-cost: 1360 maxlim: 1261546 bits: 22/21 c ---[ 634]---> Adder-cost: 1208 maxlim: 1130476 bits: 22/21 c ---[ 632]---> Adder-cost: 959 maxlim: 770037 bits: 21/20 c ---[ 630]---> Adder-cost: 756 maxlim: 540661 bits: 21/20 c ---[ 628]---> Adder-cost: 758 maxlim: 638964 bits: 21/20 c ---[ 626]---> Adder-cost: 333 maxlim: 114682 bits: 18/17 c ---[ 624]---> Adder-cost: 1068 maxlim: 1589222 bits: 22/21 c ---[ 622]---> Adder-cost: 730 maxlim: 835571 bits: 21/20 c ---[ 620]---> Adder-cost: 542 maxlim: 704503 bits: 21/20 c ---[ 618]---> Adder-cost: 978 maxlim: 1245165 bits: 22/21 c ---[ 616]---> Adder-cost: 898 maxlim: 1196015 bits: 22/21 c ---[ 614]---> Adder-cost: 838 maxlim: 1146986 bits: 21/21 c ---[ 612]---> Adder-cost: 1068 maxlim: 1327210 bits: 22/21 c ---[ 610]---> Adder-cost: 1010 maxlim: 1310826 bits: 22/21 c ---[ 608]---> Adder-cost: 971 maxlim: 491508 bits: 20/19 c ---[ 606]---> Adder-cost: 1305 maxlim: 884716 bits: 21/20 c ---[ 604]---> Adder-cost: 874 maxlim: 507892 bits: 20/19 c ---[ 602]---> Adder-cost: 655 maxlim: 344055 bits: 20/19 c ---[ 600]---> Adder-cost: 774 maxlim: 917487 bits: 21/20 c ---[ 598]---> Adder-cost: 722 maxlim: 786547 bits: 21/20 c ---[ 596]---> Adder-cost: 1264 maxlim: 1474538 bits: 22/21 c ---[ 594]---> Adder-cost: 602 maxlim: 163832 bits: 19/18 c ---[ 592]---> Adder-cost: 870 maxlim: 770034 bits: 21/20 c ---[ 590]---> Adder-cost: 844 maxlim: 491509 bits: 20/19 c ---[ 588]---> Adder-cost: 653 maxlim: 425974 bits: 20/19 c ---[ 586]---> Adder-cost: 859 maxlim: 458868 bits: 20/19 c ---[ 584]---> Adder-cost: 739 maxlim: 360566 bits: 20/19 c ---[ 582]---> Adder-cost: 1096 maxlim: 3080163 bits: 22/22 c ---[ 580]---> Adder-cost: 759 maxlim: 196599 bits: 19/18 c ---[ 578]---> Adder-cost: 214792 maxlim: 783178288 bits: 30/30 c ---[ 576]---> Adder-cost: 125388 maxlim: 586954496 bits: 30/30 c ---[ 574]---> Adder-cost: 76899 maxlim: 488500119 bits: 29/29 c ---[ 572]---> Adder-cost: 60290 maxlim: 571647874 bits: 30/30 c ---[ 570]---> Adder-cost: 65668 maxlim: 921819109 bits: 30/30 c ---[ 566]---> Adder-cost: 1038 maxlim: 2752488 bits: 22/22 c ---[ 564]---> Adder-cost: 1070 maxlim: 2818023 bits: 22/22 c ---[ 562]---> Adder-cost: 698 maxlim: 983023 bits: 21/20 c ---[ 560]---> Adder-cost: 756 maxlim: 1114091 bits: 21/21 c ---[ 558]---> Adder-cost: 698 maxlim: 983023 bits: 21/20 c ---[ 556]---> Adder-cost: 860 maxlim: 2031596 bits: 22/21 c ---[ 554]---> Adder-cost: 892 maxlim: 1409001 bits: 21/21 c ---[ 552]---> Adder-cost: 652 maxlim: 1441776 bits: 21/21 c ---[ 550]---> Adder-cost: 702 maxlim: 1703920 bits: 22/21 c ---[ 548]---> Adder-cost: 893 maxlim: 2228202 bits: 22/22 c ---[ 546]---> Adder-cost: 1006 maxlim: 2883559 bits: 22/22 c ---[ 544]---> Adder-cost: 133886 maxlim: 516959487 bits: 30/29 c ---[ 542]---> Adder-cost: 13882 maxlim: 43122275 bits: 26/26 c ---[ 540]---> Adder-cost: 45292 maxlim: 90176735 bits: 28/27 c ---[ 538]---> Adder-cost: 60472 maxlim: 112245487 bits: 28/27 c ---[ 536]---> Adder-cost: 54534 maxlim: 137460392 bits: 28/28 c ---[ 534]---> Adder-cost: 17012 maxlim: 40304183 bits: 26/26 c ---[ 532]---> Adder-cost: 5799 maxlim: 9207713 bits: 25/24 c ---[ 530]---> Adder-cost: 3107 maxlim: 3047374 bits: 23/22 c ---[ 528]---> Adder-cost: 3199 maxlim: 6291373 bits: 24/23 c ---[ 526]---> Adder-cost: 33808 maxlim: 51838357 bits: 27/26 c ---[ 524]---> Adder-cost: 7908 maxlim: 13041496 bits: 25/24 c ---[ 522]---> Adder-cost: 4977 maxlim: 4489151 bits: 24/23 c ---[ 520]---> Adder-cost: 11088 maxlim: 17497923 bits: 26/25 c ---[ 518]---> Adder-cost: 286 maxlim: 425978 bits: 20/19 c ---[ 516]---> Adder-cost: 2505 maxlim: 4718536 bits: 23/23 c ---[ 514]---> Adder-cost: 6709 maxlim: 6553504 bits: 24/23 c ---[ 512]---> Adder-cost: 4987 maxlim: 5636020 bits: 24/23 c ---[ 510]---> Adder-cost: 722 maxlim: 1048557 bits: 21/20 c ---[ 508]---> Adder-cost: 1008 maxlim: 1474533 bits: 21/21 c ---[ 506]---> Adder-cost: 946 maxlim: 1343465 bits: 21/21 c ---[ 504]---> Adder-cost: 1008 maxlim: 1507300 bits: 21/21 c ---[ 502]---> Adder-cost: 696 maxlim: 1015790 bits: 21/20 c ---[ 500]---> Adder-cost: 700 maxlim: 1015790 bits: 21/20 c ---[ 498]---> Adder-cost: 672 maxlim: 1638385 bits: 22/21 c ---[ 496]---> Adder-cost: 652 maxlim: 1507312 bits: 21/21 c ---[ 494]---> Adder-cost: 416 maxlim: 327668 bits: 19/19 c ---[ 492]---> Adder-cost: 376 maxlim: 491510 bits: 20/19 c ---[ 490]---> Adder-cost: 728 maxlim: 1146858 bits: 21/21 c ---[ 488]---> Adder-cost: 668 maxlim: 1048558 bits: 21/20 c ---[ 486]---> Adder-cost: 678 maxlim: 524269 bits: 20/19 c ---[ 484]---> Adder-cost: 946 maxlim: 1408999 bits: 21/21 c ---[ 482]---> Adder-cost: 564 maxlim: 393202 bits: 20/19 c ---[ 480]---> Adder-cost: 1004 maxlim: 3014630 bits: 22/22 c ---[ 478]---> Adder-cost: 950 maxlim: 2949096 bits: 22/22 c ---[ 476]---> Adder-cost: 924 maxlim: 1343465 bits: 21/21 c ---[ 474]---> Adder-cost: 412 maxlim: 589813 bits: 20/20 c ---[ 472]---> Adder-cost: 916 maxlim: 1474535 bits: 21/21 c ---[ 470]---> Adder-cost: 696 maxlim: 1081324 bits: 21/21 c ---[ 468]---> Adder-cost: 416 maxlim: 753652 bits: 20/20 c ---[ 466]---> Adder-cost: 414 maxlim: 622581 bits: 20/20 c ---[ 464]---> Adder-cost: 740 maxlim: 2162669 bits: 22/22 c ---[ 462]---> Adder-cost: 740 maxlim: 2228205 bits: 22/22 c ---[ 460]---> Adder-cost: 974 maxlim: 2949095 bits: 22/22 c ---[ 458]---> Adder-cost: 576 maxlim: 1703922 bits: 22/21 c ---[ 456]---> Adder-cost: 636 maxlim: 1048559 bits: 21/20 c ---[ 454]---> Adder-cost: 416 maxlim: 327668 bits: 19/19 c ---[ 452]---> Adder-cost: 638 maxlim: 1769456 bits: 22/21 c ---[ 450]---> Adder-cost: 638 maxlim: 1507313 bits: 22/21 c ---[ 448]---> Adder-cost: 768 maxlim: 2293739 bits: 22/22 c ---[ 446]---> Adder-cost: 706 maxlim: 2228205 bits: 22/22 c ---[ 444]---> Adder-cost: 740 maxlim: 2162669 bits: 22/22 c ---[ 442]---> Adder-cost: 916 maxlim: 1474535 bits: 21/21 c ---[ 440]---> Adder-cost: 412 maxlim: 720885 bits: 20/20 c ---[ 438]---> Adder-cost: 406 maxlim: 622578 bits: 20/20 c ---[ 436]---> Adder-cost: 972 maxlim: 3014631 bits: 22/22 c ---[ 434]---> Adder-cost: 696 maxlim: 1015790 bits: 21/20 c ---[ 432]---> Adder-cost: 1004 maxlim: 2883559 bits: 22/22 c ---[ 430]---> Adder-cost: 982 maxlim: 2818024 bits: 22/22 c ---[ 428]---> Adder-cost: 916 maxlim: 1474535 bits: 21/21 c ---[ 426]---> Adder-cost: 638 maxlim: 1015791 bits: 21/20 c ---[ 424]---> Adder-cost: 650 maxlim: 524269 bits: 20/19 c ---[ 422]---> Adder-cost: 436 maxlim: 655347 bits: 20/20 c ---[ 420]---> Adder-cost: 330 maxlim: 246008 bits: 19/18 c ---[ 418]---> Adder-cost: 948 maxlim: 2523110 bits: 22/22 c ---[ 416]---> Adder-cost: 438 maxlim: 819188 bits: 20/20 c ---[ 414]---> Adder-cost: 576 maxlim: 1376240 bits: 21/21 c ---[ 412]---> Adder-cost: 578 maxlim: 1277937 bits: 21/21 c ---[ 410]---> Adder-cost: 1322 maxlim: 3964889 bits: 23/22 c ---[ 408]---> Adder-cost: 286 maxlim: 327674 bits: 20/19 c ---[ 406]---> Adder-cost: 948 maxlim: 2457573 bits: 22/22 c ---[ 404]---> Adder-cost: 1318 maxlim: 4030425 bits: 23/22 c ---[ 402]---> Adder-cost: 948 maxlim: 2392038 bits: 22/22 c ---[ 400]---> Adder-cost: 969 maxlim: 2424805 bits: 22/22 c ---[ 398]---> Adder-cost: 1329 maxlim: 4161497 bits: 23/22 c ---[ 396]---> Adder-cost: 956 maxlim: 2785253 bits: 22/22 c ---[ 394]---> Adder-cost: 922 maxlim: 2785253 bits: 22/22 c ---[ 392]---> Adder-cost: 684 maxlim: 933868 bits: 21/20 c ---[ 390]---> Adder-cost: 789 maxlim: 2424809 bits: 22/22 c ---[ 388]---> Adder-cost: 1319 maxlim: 4292568 bits: 23/23 c ---[ 386]---> Adder-cost: 1066 maxlim: 3014628 bits: 22/22 c ---[ 384]---> Adder-cost: 822 maxlim: 2326505 bits: 22/22 c ---[ 382]---> Adder-cost: 598 maxlim: 999405 bits: 21/20 c ---[ 380]---> Adder-cost: 528 maxlim: 819184 bits: 20/20 c ---[ 378]---> Adder-cost: 1300 maxlim: 2162667 bits: 23/22 c ---[ 376]---> Adder-cost: 786 maxlim: 2064361 bits: 22/21 c ---[ 374]---> Adder-cost: 828 maxlim: 1277938 bits: 22/21 c ---[ 372]---> Adder-cost: 1310 maxlim: 2555882 bits: 23/22 c ---[ 370]---> Adder-cost: 1309 maxlim: 2424811 bits: 23/22 c ---[ 368]---> Adder-cost: 1301 maxlim: 2293739 bits: 23/22 c ---[ 366]---> Adder-cost: 1310 maxlim: 2555882 bits: 23/22 c ---[ 364]---> Adder-cost: 1304 maxlim: 2228204 bits: 23/22 c ---[ 362]---> Adder-cost: 1310 maxlim: 2424811 bits: 23/22 c ---[ 360]---> Adder-cost: 524 maxlim: 1376242 bits: 21/21 c ---[ 358]---> Adder-cost: 1301 maxlim: 2424811 bits: 23/22 c ---[ 356]---> Adder-cost: 784 maxlim: 1736684 bits: 22/21 c ---[ 354]---> Adder-cost: 1064 maxlim: 2752486 bits: 22/22 c ---[ 352]---> Adder-cost: 918 maxlim: 917488 bits: 21/20 c ---[ 350]---> Adder-cost: 788 maxlim: 753651 bits: 21/20 c ---[ 348]---> Adder-cost: 1284 maxlim: 2424811 bits: 23/22 c ---[ 346]---> Adder-cost: 1243 maxlim: 2424811 bits: 23/22 c ---[ 344]---> Adder-cost: 1295 maxlim: 2359276 bits: 23/22 c ---[ 342]---> Adder-cost: 1310 maxlim: 2424811 bits: 23/22 c ---[ 340]---> Adder-cost: 1076 maxlim: 2818023 bits: 23/22 c ---[ 338]---> Adder-cost: 1281 maxlim: 2424811 bits: 23/22 c ---[ 336]---> Adder-cost: 882 maxlim: 1966059 bits: 22/21 c ---[ 334]---> Adder-cost: 1098 maxlim: 2818021 bits: 22/22 c ---[ 332]---> Adder-cost: 918 maxlim: 917488 bits: 21/20 c ---[ 330]---> Adder-cost: 738 maxlim: 1114096 bits: 21/21 c ---[ 328]---> Adder-cost: 816 maxlim: 1245168 bits: 22/21 c ---[ 326]---> Adder-cost: 945 maxlim: 1572844 bits: 22/21 c ---[ 324]---> Adder-cost: 982 maxlim: 1507308 bits: 22/21 c ---[ 322]---> Adder-cost: 1247 maxlim: 2064360 bits: 22/21 c ---[ 320]---> Adder-cost: 1246 maxlim: 2260965 bits: 22/22 c ---[ 318]---> Adder-cost: 1282 maxlim: 2129895 bits: 22/22 c ---[ 316]---> Adder-cost: 612 maxlim: 524275 bits: 20/19 c ---[ 314]---> Adder-cost: 1259 maxlim: 2228197 bits: 23/22 c ---[ 312]---> Adder-cost: 1313 maxlim: 2195430 bits: 22/22 c ---[ 310]---> Adder-cost: 1064 maxlim: 1900525 bits: 22/21 c ---[ 308]---> Adder-cost: 836 maxlim: 720879 bits: 21/20 c ---[ 306]---> Adder-cost: 582 maxlim: 491508 bits: 20/19 c ---[ 304]---> Adder-cost: 790 maxlim: 1966060 bits: 22/21 c ---[ 302]---> Adder-cost: 1158 maxlim: 1867756 bits: 22/21 c ---[ 300]---> Adder-cost: 1258 maxlim: 2129895 bits: 23/22 c ---[ 298]---> Adder-cost: 1088 maxlim: 966634 bits: 21/20 c ---[ 296]---> Adder-cost: 888 maxlim: 1540078 bits: 22/21 c ---[ 294]---> Adder-cost: 562 maxlim: 1114102 bits: 21/21 c ---[ 292]---> Adder-cost: 408 maxlim: 344057 bits: 20/19 c ---[ 290]---> Adder-cost: 1028 maxlim: 1834990 bits: 22/21 c ---[ 288]---> Adder-cost: 1096 maxlim: 1802221 bits: 22/21 c ---[ 286]---> Adder-cost: 406 maxlim: 360440 bits: 20/19 c ---[ 284]---> Adder-cost: 324 maxlim: 327670 bits: 19/19 c ---[ 282]---> Adder-cost: 618 maxlim: 1146859 bits: 21/21 c ---[ 280]---> Adder-cost: 358 maxlim: 393204 bits: 19/19 c ---[ 278]---> Adder-cost: 896 maxlim: 1474540 bits: 22/21 c ---[ 276]---> Adder-cost: 914 maxlim: 1540078 bits: 22/21 c ---[ 274]---> Adder-cost: 669 maxlim: 1245170 bits: 21/21 c ---[ 272]---> Adder-cost: 1149 maxlim: 2883556 bits: 23/22 c ---[ 270]---> Adder-cost: 783 maxlim: 1769451 bits: 22/21 c ---[ 268]---> Adder-cost: 1180 maxlim: 2555877 bits: 22/22 c ---[ 266]---> Adder-cost: 1135 maxlim: 2621413 bits: 23/22 c ---[ 264]---> Adder-cost: 1184 maxlim: 2555878 bits: 23/22 c ---[ 262]---> Adder-cost: 1150 maxlim: 2621413 bits: 22/22 c ---[ 260]---> Adder-cost: 925 maxlim: 1900523 bits: 22/21 c ---[ 258]---> Adder-cost: 848 maxlim: 1638383 bits: 22/21 c ---[ 256]---> Adder-cost: 1166 maxlim: 2621413 bits: 22/22 c ---[ 254]---> Adder-cost: 768 maxlim: 2162668 bits: 22/22 c ---[ 252]---> Adder-cost: 1137 maxlim: 2686948 bits: 22/22 c ---[ 250]---> Adder-cost: 850 maxlim: 1703916 bits: 22/21 c ---[ 248]---> Adder-cost: 1147 maxlim: 2752483 bits: 22/22 c ---[ 246]---> Adder-cost: 1097 maxlim: 2490343 bits: 22/22 c ---[ 244]---> Adder-cost: 1140 maxlim: 2490343 bits: 23/22 c ---[ 242]---> Adder-cost: 1062 maxlim: 1245159 bits: 21/21 c ---[ 240]---> Adder-cost: 896 maxlim: 1703918 bits: 22/21 c ---[ 238]---> Adder-cost: 1180 maxlim: 2424806 bits: 22/22 c ---[ 236]---> Adder-cost: 879 maxlim: 1638381 bits: 22/21 c ---[ 234]---> Adder-cost: 860 maxlim: 1703918 bits: 22/21 c ---[ 232]---> Adder-cost: 1112 maxlim: 2490343 bits: 22/22 c ---[ 230]---> Adder-cost: 560 maxlim: 540661 bits: 20/20 c ---[ 228]---> Adder-cost: 598 maxlim: 671731 bits: 21/20 c ---[ 226]---> Adder-cost: 710 maxlim: 1638383 bits: 22/21 c ---[ 224]---> Adder-cost: 724 maxlim: 1507312 bits: 22/21 c ---[ 222]---> Adder-cost: 1192 maxlim: 2621413 bits: 22/22 c ---[ 220]---> Adder-cost: 1026 maxlim: 1245159 bits: 21/21 c ---[ 218]---> Adder-cost: 1168 maxlim: 2555878 bits: 22/22 c ---[ 216]---> Adder-cost: 1092 maxlim: 2424808 bits: 22/22 c ---[ 214]---> Adder-cost: 918 maxlim: 1097708 bits: 21/21 c ---[ 212]---> Adder-cost: 1360 maxlim: 2949084 bits: 22/22 c ---[ 210]---> Adder-cost: 984 maxlim: 2129896 bits: 22/22 c ---[ 208]---> Adder-cost: 984 maxlim: 2064360 bits: 22/21 c ---[ 206]---> Adder-cost: 1348 maxlim: 2981854 bits: 23/22 c ---[ 204]---> Adder-cost: 963 maxlim: 2162663 bits: 22/22 c ---[ 202]---> Adder-cost: 924 maxlim: 2162664 bits: 22/22 c ---[ 200]---> Adder-cost: 960 maxlim: 2260968 bits: 22/22 c ---[ 198]---> Adder-cost: 1285 maxlim: 3243997 bits: 23/22 c ---[ 196]---> Adder-cost: 969 maxlim: 2129896 bits: 22/22 c ---[ 194]---> Adder-cost: 960 maxlim: 2326504 bits: 22/22 c ---[ 192]---> Adder-cost: 1306 maxlim: 3178461 bits: 23/22 c ---[ 190]---> Adder-cost: 1016 maxlim: 2129896 bits: 22/22 c ---[ 188]---> Adder-cost: 1347 maxlim: 3047390 bits: 23/22 c ---[ 186]---> Adder-cost: 1375 maxlim: 3047388 bits: 23/22 c ---[ 184]---> Adder-cost: 1334 maxlim: 2981854 bits: 23/22 c ---[ 182]---> Adder-cost: 708 maxlim: 835565 bits: 21/20 c ---[ 180]---> Adder-cost: 668 maxlim: 786414 bits: 21/20 c ---[ 178]---> Adder-cost: 1171 maxlim: 1736684 bits: 22/21 c ---[ 176]---> Adder-cost: 1537 maxlim: 2457575 bits: 23/22 c ---[ 174]---> Adder-cost: 1179 maxlim: 1834988 bits: 22/21 c ---[ 172]---> Adder-cost: 1497 maxlim: 2490342 bits: 23/22 c ---[ 170]---> Adder-cost: 1165 maxlim: 1834988 bits: 22/21 c ---[ 168]---> Adder-cost: 1549 maxlim: 2424808 bits: 23/22 c ---[ 166]---> Adder-cost: 1066 maxlim: 3080164 bits: 22/22 c ---[ 164]---> Adder-cost: 633 maxlim: 688114 bits: 21/20 c ---[ 162]---> Adder-cost: 786 maxlim: 1376236 bits: 21/21 c ---[ 160]---> Adder-cost: 646 maxlim: 1343471 bits: 21/21 c ---[ 158]---> Adder-cost: 1065 maxlim: 2359266 bits: 22/22 c ---[ 156]---> Adder-cost: 1095 maxlim: 2260963 bits: 22/22 c ---[ 154]---> Adder-cost: 1058 maxlim: 2490338 bits: 22/22 c ---[ 152]---> Adder-cost: 1000 maxlim: 1343469 bits: 22/21 c ---[ 150]---> Adder-cost: 1032 maxlim: 1441771 bits: 22/21 c ---[ 148]---> Adder-cost: 936 maxlim: 1245167 bits: 22/21 c ---[ 146]---> Adder-cost: 1287 maxlim: 1867751 bits: 22/21 c ---[ 144]---> Adder-cost: 840 maxlim: 1146861 bits: 22/21 c ---[ 142]---> Adder-cost: 1315 maxlim: 1933285 bits: 22/21 c ---[ 140]---> Adder-cost: 1311 maxlim: 1900518 bits: 22/21 c ---[ 138]---> Adder-cost: 1323 maxlim: 1900518 bits: 22/21 c ---[ 136]---> Adder-cost: 1016 maxlim: 1703919 bits: 22/21 c ---[ 134]---> Adder-cost: 882 maxlim: 1146865 bits: 22/21 c ---[ 132]---> Adder-cost: 1325 maxlim: 1867751 bits: 22/21 c ---[ 130]---> Adder-cost: 1070 maxlim: 1507310 bits: 22/21 c ---[ 128]---> Adder-cost: 1042 maxlim: 770285 bits: 21/20 c ---[ 126]---> Adder-cost: 1206 maxlim: 1703914 bits: 22/21 c ---[ 124]---> Adder-cost: 958 maxlim: 1572847 bits: 22/21 c ---[ 122]---> Adder-cost: 1078 maxlim: 1638381 bits: 22/21 c ---[ 120]---> Adder-cost: 948 maxlim: 688369 bits: 21/20 c ---[ 118]---> Adder-cost: 1168 maxlim: 1638379 bits: 22/21 c ---[ 116]---> Adder-cost: 1049 maxlim: 1540079 bits: 22/21 c ---[ 114]---> Adder-cost: 330 maxlim: 622585 bits: 21/20 c ---[ 112]---> Adder-cost: 1029 maxlim: 1638377 bits: 22/21 c ---[ 110]---> Adder-cost: 1413 maxlim: 2392031 bits: 22/22 c ---[ 108]---> Adder-cost: 1000 maxlim: 1540076 bits: 22/21 c ---[ 106]---> Adder-cost: 950 maxlim: 1540076 bits: 22/21 c ---[ 104]---> Adder-cost: 1048 maxlim: 1114092 bits: 22/21 c ---[ 102]---> Adder-cost: 1039 maxlim: 1048557 bits: 21/20 c ---[ 100]---> Adder-cost: 730 maxlim: 720887 bits: 21/20 c ---[ 98]---> Adder-cost: 1225 maxlim: 1212396 bits: 22/21 c ---[ 96]---> Adder-cost: 730 maxlim: 720887 bits: 21/20 c ---[ 94]---> Adder-cost: 748 maxlim: 655351 bits: 21/20 c ---[ 92]---> Adder-cost: 541 maxlim: 458745 bits: 20/19 c ---[ 90]---> Adder-cost: 977 maxlim: 1015790 bits: 21/20 c ---[ 88]---> Adder-cost: 768 maxlim: 688118 bits: 21/20 c ---[ 86]---> Adder-cost: 1241 maxlim: 1212396 bits: 22/21 c ---[ 84]---> Adder-cost: 479 maxlim: 425978 bits: 20/19 c ---[ 82]---> Sorter-cost: 762 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 80]---> Adder-cost: 456 maxlim: 819189 bits: 20/20 c ---[ 78]---> Adder-cost: 926 maxlim: 2490342 bits: 22/22 c ---[ 76]---> Adder-cost: 967 maxlim: 2457573 bits: 22/22 c ---[ 74]---> Adder-cost: 744 maxlim: 1834988 bits: 22/21 c ---[ 72]---> Adder-cost: 936 maxlim: 2424807 bits: 22/22 c ---[ 70]---> Adder-cost: 1317 maxlim: 3506140 bits: 23/22 c ---[ 68]---> Adder-cost: 386 maxlim: 917494 bits: 21/20 c ---[ 66]---> Adder-cost: 777 maxlim: 2195433 bits: 22/22 c ---[ 64]---> Sorter-cost: 1593 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 62]---> Adder-cost: 910 maxlim: 1376240 bits: 22/21 c ---[ 60]---> Adder-cost: 1428 maxlim: 2523112 bits: 23/22 c ---[ 58]---> Adder-cost: 1409 maxlim: 2523112 bits: 23/22 c ---[ 56]---> Adder-cost: 880 maxlim: 1540081 bits: 22/21 c ---[ 54]---> Adder-cost: 767 maxlim: 1638377 bits: 21/21 c ---[ 52]---> Adder-cost: 1030 maxlim: 2392035 bits: 22/22 c ---[ 50]---> Adder-cost: 897 maxlim: 1933287 bits: 22/21 c ---[ 48]---> Adder-cost: 322 maxlim: 688119 bits: 20/20 c ---[ 46]---> Adder-cost: 972 maxlim: 1376237 bits: 22/21 c ---[ 44]---> Adder-cost: 1262 maxlim: 2031590 bits: 22/21 c ---[ 42]---> Adder-cost: 885 maxlim: 1277936 bits: 22/21 c ---[ 40]---> Adder-cost: 966 maxlim: 1343470 bits: 22/21 c ---[ 38]---> Adder-cost: 906 maxlim: 1343471 bits: 22/21 c ---[ 36]---> Adder-cost: 1301 maxlim: 2031590 bits: 22/21 c ---[ 34]---> Adder-cost: 965 maxlim: 1409004 bits: 22/21 c ---[ 32]---> Adder-cost: 1061 maxlim: 1769451 bits: 22/21 c ---[ 30]---> Adder-cost: 883 maxlim: 1179634 bits: 22/21 c ---[ 28]---> Adder-cost: 367 maxlim: 229370 bits: 19/18 c ---[ 26]---> Adder-cost: 735 maxlim: 917491 bits: 21/20 c ---[ 24]---> Adder-cost: 816 maxlim: 1146867 bits: 22/21 c ---[ 22]---> Adder-cost: 460 maxlim: 655351 bits: 21/20 c ---[ 20]---> Adder-cost: 866 maxlim: 1245168 bits: 22/21 c ---[ 18]---> Adder-cost: 1274 maxlim: 2097125 bits: 22/21 c ---[ 16]---> Adder-cost: 1203 maxlim: 1834986 bits: 22/21 c ---[ 14]---> Adder-cost: 812 maxlim: 1179633 bits: 22/21 c ---[ 12]---> Adder-cost: 807 maxlim: 1179634 bits: 22/21 c ---[ 10]---> Adder-cost: 968 maxlim: 1409005 bits: 22/21 c ---[ 8]---> Adder-cost: 888 maxlim: 1277936 bits: 22/21 c ---[ 6]---> Adder-cost: 433 maxlim: 458744 bits: 20/19 c ---[ 4]---> Adder-cost: 768 maxlim: 1146863 bits: 21/21 c ---[ 2]---> Adder-cost: 812 maxlim: 1245167 bits: 22/21 c ---[ 0]---> Adder-cost: 934 maxlim: 1507309 bits: 22/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 9053897 32289967 | 3017965 0 0 nan | 0.000 % | c | 100 | 9053897 32289967 | 3319761 100 306 3.1 | 2.734 % | c | 250 | 9053881 32289915 | 3651737 248 812 3.3 | 2.734 % | c | 475 | 9053875 32289897 | 4016911 472 1559 3.3 | 2.734 % | c | 812 | 9053859 32289845 | 4418602 807 2796 3.5 | 2.734 % | c | 1318 | 9053843 32289793 | 4860462 1311 4505 3.4 | 2.734 % | c | 2077 | 9053811 32289689 | 5346509 2066 7129 3.5 | 2.734 % | c | 3216 | 9053787 32289611 | 5881160 3202 11071 3.5 | 2.735 % | c | 4924 | 9053735 32289441 | 6469276 4903 17494 3.6 | 2.735 % | c | 7486 | 9053654 32289178 | 7116203 7455 26970 3.6 | 2.736 % | c | 11330 | 9053544 32288822 | 7827823 11285 41338 3.7 | 2.737 % | c | 17096 | 9051397 32281251 | 8610606 16772 61287 3.7 | 2.762 % |
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/15252/stat): 15252 (minisat+_script) R 15251 15252 21452 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1854979659 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/15252/statm): 174 3 169 147 0 27 0 [pid=15252] 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=15253 New process pid=15254 New process pid=15255 execve syscall for /bin/sed executable One traced child (pid=15254) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=15255) exited with status: 0 One traced child (pid=15253) exited with status: 0 New process pid=15256 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-d6cube.opb [startup+10.0034 s] Raw data (loadavg): 0.94 0.96 0.91 1/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) T 15252 15252 21452 0 -1 0 28822 0 0 0 813 107 0 0 20 0 1 0 1854979664 71692288 9277 4294967295 134512640 135094434 3221224432 3221222652 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/15256/statm): 17503 9277 145 145 0 17358 0 [pid=15256] vsize: 70012 Current children cumulated CPU time (s) 9.2 Current children cumulated vsize (Kb) 72136 [startup+20.0041 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 1775 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134580034 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 18.99 Current children cumulated vsize (Kb) 88328 [startup+30.0048 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 2775 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134580024 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 28.99 Current children cumulated vsize (Kb) 88328 [startup+40.0055 s] Raw data (loadavg): 0.96 0.96 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 3776 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134579970 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 39 Current children cumulated vsize (Kb) 88328 [startup+50.0062 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 4776 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134581225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 49 Current children cumulated vsize (Kb) 88328 [startup+60.0069 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 5776 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134579970 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 59 Current children cumulated vsize (Kb) 88328 [startup+70.0076 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 6776 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134581225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 69 Current children cumulated vsize (Kb) 88328 [startup+80.0083 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 7777 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134581225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 79.01 Current children cumulated vsize (Kb) 88328 [startup+90.009 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 8777 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134581225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 89.01 Current children cumulated vsize (Kb) 88328 [startup+100.009 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 9777 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134579997 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 99.01 Current children cumulated vsize (Kb) 88328 [startup+110.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 10777 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134580048 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 109.01 Current children cumulated vsize (Kb) 88328 [startup+120.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 11777 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134579970 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 119.01 Current children cumulated vsize (Kb) 88328 [startup+130.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 12777 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134579970 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 129.01 Current children cumulated vsize (Kb) 88328 [startup+140.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 13777 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134581225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 139.01 Current children cumulated vsize (Kb) 88328 [startup+150.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 14778 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134581225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 149.02 Current children cumulated vsize (Kb) 88328 [startup+160.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 15778 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134579970 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 159.02 Current children cumulated vsize (Kb) 88328 [startup+170.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 16778 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134581225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 169.02 Current children cumulated vsize (Kb) 88328 [startup+180.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 17778 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134579968 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 179.02 Current children cumulated vsize (Kb) 88328 [startup+190.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 18779 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134579970 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 189.03 Current children cumulated vsize (Kb) 88328 [startup+200.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 19779 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134580034 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 199.03 Current children cumulated vsize (Kb) 88328 [startup+210.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 20779 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134580075 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 209.03 Current children cumulated vsize (Kb) 88328 [startup+220.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 21779 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134580048 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 219.03 Current children cumulated vsize (Kb) 88328 [startup+230.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 22779 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134581212 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 229.03 Current children cumulated vsize (Kb) 88328 [startup+240.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 23780 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134581225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 239.04 Current children cumulated vsize (Kb) 88328 [startup+250.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 24780 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134579970 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 249.04 Current children cumulated vsize (Kb) 88328 [startup+260.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 25780 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134581225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 259.04 Current children cumulated vsize (Kb) 88328 [startup+270.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 26780 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134581225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 269.04 Current children cumulated vsize (Kb) 88328 [startup+280.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 27781 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134581225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 279.05 Current children cumulated vsize (Kb) 88328 [startup+290.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 28781 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134580017 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 289.05 Current children cumulated vsize (Kb) 88328 [startup+300.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 29781 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134580081 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 299.05 Current children cumulated vsize (Kb) 88328 [startup+310.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 30781 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134581225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 309.05 Current children cumulated vsize (Kb) 88328 [startup+320.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 31782 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134581225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 319.06 Current children cumulated vsize (Kb) 88328 [startup+330.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 32782 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134581225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 329.06 Current children cumulated vsize (Kb) 88328 [startup+340.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 33782 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134580034 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 339.06 Current children cumulated vsize (Kb) 88328 [startup+350.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 34782 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134580048 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 349.06 Current children cumulated vsize (Kb) 88328 [startup+360.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 35783 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134580024 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 359.07 Current children cumulated vsize (Kb) 88328 [startup+370.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 36783 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134581225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 369.07 Current children cumulated vsize (Kb) 88328 [startup+380.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 37783 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134581225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 379.07 Current children cumulated vsize (Kb) 88328 [startup+390.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 38783 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134581225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 389.07 Current children cumulated vsize (Kb) 88328 [startup+400.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 39783 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134579970 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 399.07 Current children cumulated vsize (Kb) 88328 [startup+410.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 40784 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134581225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 409.08 Current children cumulated vsize (Kb) 88328 [startup+420.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 41784 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134580028 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 419.08 Current children cumulated vsize (Kb) 88328 [startup+430.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 33230 0 0 0 42784 124 0 0 25 0 1 0 1854979664 88272896 13322 4294967295 134512640 135094434 3221224432 3221223248 134579970 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 21551 13322 145 145 0 21406 0 [pid=15256] vsize: 86204 Current children cumulated CPU time (s) 429.08 Current children cumulated vsize (Kb) 88328 [startup+440.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 39241 0 0 0 43771 138 0 0 25 0 1 0 1854979664 110428160 18608 4294967295 134512640 135094434 3221224432 3203806560 134596860 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 26960 18608 145 145 0 26815 0 [pid=15256] vsize: 107840 Current children cumulated CPU time (s) 439.09 Current children cumulated vsize (Kb) 109964 [startup+450.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 48908 0 0 0 44726 164 0 0 25 0 1 0 1854979664 134586368 23877 4294967295 134512640 135094434 3221224432 3221221808 134601016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 32858 23877 145 145 0 32713 0 [pid=15256] vsize: 131432 Current children cumulated CPU time (s) 448.9 Current children cumulated vsize (Kb) 133556 [startup+460.034 s] Raw data (loadavg): 0.99 0.97 0.91 1/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) T 15252 15252 21452 0 -1 0 67335 0 0 0 45649 216 0 0 23 0 1 0 1854979664 186015744 35726 4294967295 134512640 135094434 3221224432 3221221212 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/15256/statm): 45414 35726 145 145 0 45269 0 [pid=15256] vsize: 181656 Current children cumulated CPU time (s) 458.65 Current children cumulated vsize (Kb) 183780 [startup+470.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 93124 0 0 0 46521 292 0 0 25 0 1 0 1854979664 263110656 53721 4294967295 134512640 135094434 3221224432 3210860288 134597014 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15256/statm): 64236 53721 145 145 0 64091 0 [pid=15256] vsize: 256944 Current children cumulated CPU time (s) 468.13 Current children cumulated vsize (Kb) 259068 [startup+480.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 97671 0 0 0 47504 304 0 0 25 0 1 0 1854979664 263004160 53695 4294967295 134512640 135094434 3221224432 3215684656 134597418 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15256/statm): 64210 53695 145 145 0 64065 0 [pid=15256] vsize: 256840 Current children cumulated CPU time (s) 478.08 Current children cumulated vsize (Kb) 258964 [startup+490.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 101823 0 0 0 48487 316 0 0 25 0 1 0 1854979664 261255168 53171 4294967295 134512640 135094434 3221224432 3221221984 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15256/statm): 63783 53171 145 145 0 63638 0 [pid=15256] vsize: 255132 Current children cumulated CPU time (s) 488.03 Current children cumulated vsize (Kb) 257256 [startup+500.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 105216 0 0 0 49475 324 0 0 25 0 1 0 1854979664 260730880 53089 4294967295 134512640 135094434 3221224432 3221222576 134677091 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15256/statm): 63655 53089 145 145 0 63510 0 [pid=15256] vsize: 254620 Current children cumulated CPU time (s) 497.99 Current children cumulated vsize (Kb) 256744 [startup+510.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 109594 0 0 0 50457 338 0 0 25 0 1 0 1854979664 263352320 53654 4294967295 134512640 135094434 3221224432 3221222160 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15256/statm): 64295 53654 145 145 0 64150 0 [pid=15256] vsize: 257180 Current children cumulated CPU time (s) 507.95 Current children cumulated vsize (Kb) 259304 [startup+520.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 112056 0 0 0 51448 345 0 0 25 0 1 0 1854979664 260206592 53012 4294967295 134512640 135094434 3221224432 3221223120 134596445 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15256/statm): 63527 53012 145 145 0 63382 0 [pid=15256] vsize: 254108 Current children cumulated CPU time (s) 517.93 Current children cumulated vsize (Kb) 256232 [startup+530.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 115522 0 0 0 52435 355 0 0 25 0 1 0 1854979664 260206592 53012 4294967295 134512640 135094434 3221224432 3221223120 134596398 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15256/statm): 63527 53012 145 145 0 63382 0 [pid=15256] vsize: 254108 Current children cumulated CPU time (s) 527.9 Current children cumulated vsize (Kb) 256232 [startup+540.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 116323 0 0 0 53432 356 0 0 25 0 1 0 1854979664 260206592 53012 4294967295 134512640 135094434 3221224432 3221222708 134520000 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15256/statm): 63527 53012 145 145 0 63382 0 [pid=15256] vsize: 254108 Current children cumulated CPU time (s) 537.88 Current children cumulated vsize (Kb) 256232 [startup+550.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 116323 0 0 0 54432 356 0 0 25 0 1 0 1854979664 260206592 53012 4294967295 134512640 135094434 3221224432 3221220448 134680380 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15256/statm): 63527 53012 145 145 0 63382 0 [pid=15256] vsize: 254108 Current children cumulated CPU time (s) 547.88 Current children cumulated vsize (Kb) 256232 [startup+560.044 s] Raw data (loadavg): 0.99 0.97 0.91 1/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) T 15252 15252 21452 0 -1 0 133266 0 0 0 55302 423 0 0 21 0 1 0 1854979664 307818496 67346 4294967295 134512640 135094434 3221224432 3221212764 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/15256/statm): 75151 67346 145 145 0 75006 0 [pid=15256] vsize: 300604 Current children cumulated CPU time (s) 557.25 Current children cumulated vsize (Kb) 302728 [startup+570.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 161687 0 0 0 56037 548 0 0 22 0 1 0 1854979664 437772288 95767 4294967295 134512640 135094434 3221224432 3221213840 134553146 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15256/statm): 106878 95767 145 145 0 106733 0 [pid=15256] vsize: 427512 Current children cumulated CPU time (s) 565.85 Current children cumulated vsize (Kb) 429636 [startup+580.045 s] Raw data (loadavg): 0.99 0.97 0.91 1/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) T 15252 15252 21452 0 -1 0 190315 0 0 0 56780 668 0 0 22 0 1 0 1854979664 550719488 124395 4294967295 134512640 135094434 3221224432 3221216540 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/15256/statm): 134453 124395 145 145 0 134308 0 [pid=15256] vsize: 537812 Current children cumulated CPU time (s) 574.48 Current children cumulated vsize (Kb) 539936 [startup+590.046 s] Raw data (loadavg): 0.99 0.97 0.91 1/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) T 15252 15252 21452 0 -1 0 219282 0 0 0 57514 792 0 0 21 0 1 0 1854979664 704372736 153362 4294967295 134512640 135094434 3221224432 3221216444 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/15256/statm): 171966 153362 145 145 0 171821 0 [pid=15256] vsize: 687864 Current children cumulated CPU time (s) 583.06 Current children cumulated vsize (Kb) 689988 [startup+600.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 241571 0 0 0 58311 890 0 0 25 0 1 0 1854979664 819052544 175651 4294967295 134512640 135094434 3221224432 3221223248 134558992 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 199964 175651 145 145 0 199819 0 [pid=15256] vsize: 799856 Current children cumulated CPU time (s) 592.01 Current children cumulated vsize (Kb) 801980 [startup+610.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 241581 0 0 0 59311 890 0 0 25 0 1 0 1854979664 819060736 175661 4294967295 134512640 135094434 3221224432 3221223136 134559005 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15256/statm): 199966 175661 145 145 0 199821 0 [pid=15256] vsize: 799864 Current children cumulated CPU time (s) 602.01 Current children cumulated vsize (Kb) 801988 [startup+620.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 241583 0 0 0 60311 891 0 0 25 0 1 0 1854979664 819068928 175663 4294967295 134512640 135094434 3221224432 3221223100 134553438 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 199968 175663 145 145 0 199823 0 [pid=15256] vsize: 799872 Current children cumulated CPU time (s) 612.02 Current children cumulated vsize (Kb) 801996 [startup+630.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 241588 0 0 0 61311 891 0 0 25 0 1 0 1854979664 819093504 175668 4294967295 134512640 135094434 3221224432 3221223116 134553432 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 199974 175668 145 145 0 199829 0 [pid=15256] vsize: 799896 Current children cumulated CPU time (s) 622.02 Current children cumulated vsize (Kb) 802020 [startup+640.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 241599 0 0 0 62311 891 0 0 25 0 1 0 1854979664 819138560 175679 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 199985 175679 145 145 0 199840 0 [pid=15256] vsize: 799940 Current children cumulated CPU time (s) 632.02 Current children cumulated vsize (Kb) 802064 [startup+650.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 241705 0 0 0 63309 891 0 0 25 0 1 0 1854979664 819568640 175785 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 200090 175785 145 145 0 199945 0 [pid=15256] vsize: 800360 Current children cumulated CPU time (s) 642 Current children cumulated vsize (Kb) 802484 [startup+660.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 241783 0 0 0 64308 892 0 0 25 0 1 0 1854979664 819888128 175863 4294967295 134512640 135094434 3221224432 3221223120 134558992 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 200168 175863 145 145 0 200023 0 [pid=15256] vsize: 800672 Current children cumulated CPU time (s) 652 Current children cumulated vsize (Kb) 802796 [startup+670.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 241852 0 0 0 65308 892 0 0 25 0 1 0 1854979664 820183040 175932 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 200240 175932 145 145 0 200095 0 [pid=15256] vsize: 800960 Current children cumulated CPU time (s) 662 Current children cumulated vsize (Kb) 803084 [startup+680.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 242033 0 0 0 66305 893 0 0 25 0 1 0 1854979664 820920320 176113 4294967295 134512640 135094434 3221224432 3221223044 134563110 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 200420 176113 145 145 0 200275 0 [pid=15256] vsize: 801680 Current children cumulated CPU time (s) 671.98 Current children cumulated vsize (Kb) 803804 [startup+690.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 242060 0 0 0 67305 893 0 0 25 0 1 0 1854979664 821039104 176140 4294967295 134512640 135094434 3221224432 3221223092 134553494 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 200449 176140 145 145 0 200304 0 [pid=15256] vsize: 801796 Current children cumulated CPU time (s) 681.98 Current children cumulated vsize (Kb) 803920 [startup+700.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 242109 0 0 0 68304 894 0 0 25 0 1 0 1854979664 821235712 176189 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 200497 176189 145 145 0 200352 0 [pid=15256] vsize: 801988 Current children cumulated CPU time (s) 691.98 Current children cumulated vsize (Kb) 804112 [startup+710.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 242216 0 0 0 69302 895 0 0 25 0 1 0 1854979664 821669888 176296 4294967295 134512640 135094434 3221224432 3221223092 134553533 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 200603 176296 145 145 0 200458 0 [pid=15256] vsize: 802412 Current children cumulated CPU time (s) 701.97 Current children cumulated vsize (Kb) 804536 [startup+720.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 242322 0 0 0 70301 895 0 0 25 0 1 0 1854979664 822104064 176402 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 200709 176402 145 145 0 200564 0 [pid=15256] vsize: 802836 Current children cumulated CPU time (s) 711.96 Current children cumulated vsize (Kb) 804960 [startup+730.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 242431 0 0 0 71299 896 0 0 25 0 1 0 1854979664 822546432 176511 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 200817 176511 145 145 0 200672 0 [pid=15256] vsize: 803268 Current children cumulated CPU time (s) 721.95 Current children cumulated vsize (Kb) 805392 [startup+740.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 242503 0 0 0 72298 896 0 0 25 0 1 0 1854979664 822870016 176583 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 200896 176583 145 145 0 200751 0 [pid=15256] vsize: 803584 Current children cumulated CPU time (s) 731.94 Current children cumulated vsize (Kb) 805708 [startup+750.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 242628 0 0 0 73296 897 0 0 25 0 1 0 1854979664 823377920 176708 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 201020 176708 145 145 0 200875 0 [pid=15256] vsize: 804080 Current children cumulated CPU time (s) 741.93 Current children cumulated vsize (Kb) 806204 [startup+760.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 242726 0 0 0 74294 897 0 0 25 0 1 0 1854979664 823779328 176806 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 201118 176806 145 145 0 200973 0 [pid=15256] vsize: 804472 Current children cumulated CPU time (s) 751.91 Current children cumulated vsize (Kb) 806596 [startup+770.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 242861 0 0 0 75292 898 0 0 25 0 1 0 1854979664 824328192 176941 4294967295 134512640 135094434 3221224432 3221223044 134563069 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 201252 176941 145 145 0 201107 0 [pid=15256] vsize: 805008 Current children cumulated CPU time (s) 761.9 Current children cumulated vsize (Kb) 807132 [startup+780.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 242979 0 0 0 76290 900 0 0 25 0 1 0 1854979664 824803328 177059 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 201368 177059 145 145 0 201223 0 [pid=15256] vsize: 805472 Current children cumulated CPU time (s) 771.9 Current children cumulated vsize (Kb) 807596 [startup+790.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243109 0 0 0 77288 901 0 0 25 0 1 0 1854979664 825335808 177189 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 201498 177189 145 145 0 201353 0 [pid=15256] vsize: 805992 Current children cumulated CPU time (s) 781.89 Current children cumulated vsize (Kb) 808116 [startup+800.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243180 0 0 0 78287 902 0 0 25 0 1 0 1854979664 825622528 177260 4294967295 134512640 135094434 3221224432 3221223072 134562108 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 201568 177260 145 145 0 201423 0 [pid=15256] vsize: 806272 Current children cumulated CPU time (s) 791.89 Current children cumulated vsize (Kb) 808396 [startup+810.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243345 0 0 0 79285 903 0 0 25 0 1 0 1854979664 826298368 177425 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 201733 177425 145 145 0 201588 0 [pid=15256] vsize: 806932 Current children cumulated CPU time (s) 801.88 Current children cumulated vsize (Kb) 809056 [startup+820.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243366 0 0 0 80285 903 0 0 25 0 1 0 1854979664 826380288 177446 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 201753 177446 145 145 0 201608 0 [pid=15256] vsize: 807012 Current children cumulated CPU time (s) 811.88 Current children cumulated vsize (Kb) 809136 [startup+830.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243400 0 0 0 81284 903 0 0 25 0 1 0 1854979664 826519552 177480 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 201787 177480 145 145 0 201642 0 [pid=15256] vsize: 807148 Current children cumulated CPU time (s) 821.87 Current children cumulated vsize (Kb) 809272 [startup+840.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243400 0 0 0 82285 903 0 0 25 0 1 0 1854979664 826519552 177480 4294967295 134512640 135094434 3221224432 3221223116 134553526 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 201787 177480 145 145 0 201642 0 [pid=15256] vsize: 807148 Current children cumulated CPU time (s) 831.88 Current children cumulated vsize (Kb) 809272 [startup+850.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243414 0 0 0 83284 903 0 0 25 0 1 0 1854979664 826576896 177494 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 201801 177494 145 145 0 201656 0 [pid=15256] vsize: 807204 Current children cumulated CPU time (s) 841.87 Current children cumulated vsize (Kb) 809328 [startup+860.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243434 0 0 0 84284 903 0 0 25 0 1 0 1854979664 826658816 177514 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 201821 177514 145 145 0 201676 0 [pid=15256] vsize: 807284 Current children cumulated CPU time (s) 851.87 Current children cumulated vsize (Kb) 809408 [startup+870.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243450 0 0 0 85284 903 0 0 25 0 1 0 1854979664 826724352 177530 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 201837 177530 145 145 0 201692 0 [pid=15256] vsize: 807348 Current children cumulated CPU time (s) 861.87 Current children cumulated vsize (Kb) 809472 [startup+880.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243463 0 0 0 86284 904 0 0 25 0 1 0 1854979664 826777600 177543 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 201850 177543 145 145 0 201705 0 [pid=15256] vsize: 807400 Current children cumulated CPU time (s) 871.88 Current children cumulated vsize (Kb) 809524 [startup+890.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243520 0 0 0 87283 904 0 0 25 0 1 0 1854979664 827011072 177600 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 201907 177600 145 145 0 201762 0 [pid=15256] vsize: 807628 Current children cumulated CPU time (s) 881.87 Current children cumulated vsize (Kb) 809752 [startup+900.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243520 0 0 0 88283 904 0 0 25 0 1 0 1854979664 827011072 177600 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 201907 177600 145 145 0 201762 0 [pid=15256] vsize: 807628 Current children cumulated CPU time (s) 891.87 Current children cumulated vsize (Kb) 809752 [startup+910.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243556 0 0 0 89283 905 0 0 25 0 1 0 1854979664 827158528 177636 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 201943 177636 145 145 0 201798 0 [pid=15256] vsize: 807772 Current children cumulated CPU time (s) 901.88 Current children cumulated vsize (Kb) 809896 [startup+920.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243556 0 0 0 90283 905 0 0 25 0 1 0 1854979664 827158528 177636 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 201943 177636 145 145 0 201798 0 [pid=15256] vsize: 807772 Current children cumulated CPU time (s) 911.88 Current children cumulated vsize (Kb) 809896 [startup+930.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243575 0 0 0 91283 905 0 0 25 0 1 0 1854979664 827236352 177655 4294967295 134512640 135094434 3221224432 3221223100 134550364 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 201962 177655 145 145 0 201817 0 [pid=15256] vsize: 807848 Current children cumulated CPU time (s) 921.88 Current children cumulated vsize (Kb) 809972 [startup+940.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243584 0 0 0 92283 905 0 0 25 0 1 0 1854979664 827273216 177664 4294967295 134512640 135094434 3221224432 3221223044 134563069 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 201971 177664 145 145 0 201826 0 [pid=15256] vsize: 807884 Current children cumulated CPU time (s) 931.88 Current children cumulated vsize (Kb) 810008 [startup+950.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243610 0 0 0 93283 905 0 0 25 0 1 0 1854979664 827379712 177690 4294967295 134512640 135094434 3221224432 3221223136 134559005 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 201997 177690 145 145 0 201852 0 [pid=15256] vsize: 807988 Current children cumulated CPU time (s) 941.88 Current children cumulated vsize (Kb) 810112 [startup+960.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243610 0 0 0 94283 905 0 0 25 0 1 0 1854979664 827379712 177690 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 201997 177690 145 145 0 201852 0 [pid=15256] vsize: 807988 Current children cumulated CPU time (s) 951.88 Current children cumulated vsize (Kb) 810112 [startup+970.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243628 0 0 0 95283 905 0 0 25 0 1 0 1854979664 827453440 177708 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 202015 177708 145 145 0 201870 0 [pid=15256] vsize: 808060 Current children cumulated CPU time (s) 961.88 Current children cumulated vsize (Kb) 810184 [startup+980.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243666 0 0 0 96282 905 0 0 25 0 1 0 1854979664 827609088 177746 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 202053 177746 145 145 0 201908 0 [pid=15256] vsize: 808212 Current children cumulated CPU time (s) 971.87 Current children cumulated vsize (Kb) 810336 [startup+990.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243676 0 0 0 97282 906 0 0 25 0 1 0 1854979664 827650048 177756 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 202063 177756 145 145 0 201918 0 [pid=15256] vsize: 808252 Current children cumulated CPU time (s) 981.88 Current children cumulated vsize (Kb) 810376 [startup+1000.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243696 0 0 0 98282 906 0 0 25 0 1 0 1854979664 827727872 177776 4294967295 134512640 135094434 3221224432 3221223116 134553432 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 202082 177776 145 145 0 201937 0 [pid=15256] vsize: 808328 Current children cumulated CPU time (s) 991.88 Current children cumulated vsize (Kb) 810452 [startup+1010.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243721 0 0 0 99281 906 0 0 25 0 1 0 1854979664 827830272 177801 4294967295 134512640 135094434 3221224432 3221223044 134563089 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 202107 177801 145 145 0 201962 0 [pid=15256] vsize: 808428 Current children cumulated CPU time (s) 1001.87 Current children cumulated vsize (Kb) 810552 [startup+1020.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243732 0 0 0 100281 906 0 0 25 0 1 0 1854979664 827875328 177812 4294967295 134512640 135094434 3221224432 3221223100 134553438 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 202118 177812 145 145 0 201973 0 [pid=15256] vsize: 808472 Current children cumulated CPU time (s) 1011.87 Current children cumulated vsize (Kb) 810596 [startup+1030.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243751 0 0 0 101281 906 0 0 25 0 1 0 1854979664 827953152 177831 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 202137 177831 145 145 0 201992 0 [pid=15256] vsize: 808548 Current children cumulated CPU time (s) 1021.87 Current children cumulated vsize (Kb) 810672 [startup+1040.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243784 0 0 0 102281 907 0 0 25 0 1 0 1854979664 828088320 177864 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 202170 177864 145 145 0 202025 0 [pid=15256] vsize: 808680 Current children cumulated CPU time (s) 1031.88 Current children cumulated vsize (Kb) 810804 [startup+1050.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243785 0 0 0 103281 907 0 0 25 0 1 0 1854979664 828092416 177865 4294967295 134512640 135094434 3221224432 3221223092 134553494 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 202171 177865 145 145 0 202026 0 [pid=15256] vsize: 808684 Current children cumulated CPU time (s) 1041.88 Current children cumulated vsize (Kb) 810808 [startup+1060.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243803 0 0 0 104280 907 0 0 25 0 1 0 1854979664 828166144 177883 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 202189 177883 145 145 0 202044 0 [pid=15256] vsize: 808756 Current children cumulated CPU time (s) 1051.87 Current children cumulated vsize (Kb) 810880 [startup+1070.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243835 0 0 0 105280 907 0 0 25 0 1 0 1854979664 828297216 177915 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 202221 177915 145 145 0 202076 0 [pid=15256] vsize: 808884 Current children cumulated CPU time (s) 1061.87 Current children cumulated vsize (Kb) 811008 [startup+1080.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243846 0 0 0 106280 907 0 0 25 0 1 0 1854979664 828342272 177926 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 202232 177926 145 145 0 202087 0 [pid=15256] vsize: 808928 Current children cumulated CPU time (s) 1071.87 Current children cumulated vsize (Kb) 811052 [startup+1090.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243846 0 0 0 107280 907 0 0 25 0 1 0 1854979664 828342272 177926 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 202232 177926 145 145 0 202087 0 [pid=15256] vsize: 808928 Current children cumulated CPU time (s) 1081.87 Current children cumulated vsize (Kb) 811052 [startup+1100.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243860 0 0 0 108280 907 0 0 25 0 1 0 1854979664 828399616 177940 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 202246 177940 145 145 0 202101 0 [pid=15256] vsize: 808984 Current children cumulated CPU time (s) 1091.87 Current children cumulated vsize (Kb) 811108 [startup+1110.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243876 0 0 0 109280 908 0 0 25 0 1 0 1854979664 828465152 177956 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 202262 177956 145 145 0 202117 0 [pid=15256] vsize: 809048 Current children cumulated CPU time (s) 1101.88 Current children cumulated vsize (Kb) 811172 [startup+1120.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 243908 0 0 0 110280 908 0 0 25 0 1 0 1854979664 828620800 177988 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 202300 177988 145 145 0 202155 0 [pid=15256] vsize: 809200 Current children cumulated CPU time (s) 1111.88 Current children cumulated vsize (Kb) 811324 [startup+1130.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 244008 0 0 0 111278 909 0 0 25 0 1 0 1854979664 829026304 178088 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 202399 178088 145 145 0 202254 0 [pid=15256] vsize: 809596 Current children cumulated CPU time (s) 1121.87 Current children cumulated vsize (Kb) 811720 [startup+1140.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 244095 0 0 0 112277 909 0 0 25 0 1 0 1854979664 829382656 178175 4294967295 134512640 135094434 3221224432 3221223092 134553487 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 202486 178175 145 145 0 202341 0 [pid=15256] vsize: 809944 Current children cumulated CPU time (s) 1131.86 Current children cumulated vsize (Kb) 812068 [startup+1150.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 244149 0 0 0 113276 910 0 0 25 0 1 0 1854979664 829603840 178229 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 202540 178229 145 145 0 202395 0 [pid=15256] vsize: 810160 Current children cumulated CPU time (s) 1141.86 Current children cumulated vsize (Kb) 812284 [startup+1160.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 244195 0 0 0 114275 910 0 0 25 0 1 0 1854979664 829853696 178275 4294967295 134512640 135094434 3221224432 3221223044 134563074 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 202601 178275 145 145 0 202456 0 [pid=15256] vsize: 810404 Current children cumulated CPU time (s) 1151.85 Current children cumulated vsize (Kb) 812528 [startup+1170.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 244381 0 0 0 115271 911 0 0 25 0 1 0 1854979664 830611456 178461 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 202786 178461 145 145 0 202641 0 [pid=15256] vsize: 811144 Current children cumulated CPU time (s) 1161.82 Current children cumulated vsize (Kb) 813268 [startup+1180.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 244444 0 0 0 116270 912 0 0 25 0 1 0 1854979664 830861312 178524 4294967295 134512640 135094434 3221224432 3221223024 134551967 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 202847 178524 145 145 0 202702 0 [pid=15256] vsize: 811388 Current children cumulated CPU time (s) 1171.82 Current children cumulated vsize (Kb) 813512 [startup+1190.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 244559 0 0 0 117268 913 0 0 25 0 1 0 1854979664 831332352 178639 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 202962 178639 145 145 0 202817 0 [pid=15256] vsize: 811848 Current children cumulated CPU time (s) 1181.81 Current children cumulated vsize (Kb) 813972 [startup+1200.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 244685 0 0 0 118266 914 0 0 25 0 1 0 1854979664 831836160 178765 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 203085 178765 145 145 0 202940 0 [pid=15256] vsize: 812340 Current children cumulated CPU time (s) 1191.8 Current children cumulated vsize (Kb) 814464 [startup+1210.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 244876 0 0 0 119263 915 0 0 25 0 1 0 1854979664 832614400 178956 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 203275 178956 145 145 0 203130 0 [pid=15256] vsize: 813100 Current children cumulated CPU time (s) 1201.78 Current children cumulated vsize (Kb) 815224 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 15256 Raw data (/proc/15252/stat): 15252 (minisat+_script) S 15251 15252 21452 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1854979659 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15252/statm): 531 226 485 147 0 384 0 [pid=15252] vsize: 2124 Raw data (/proc/15256/stat): 15256 (minisat+_64-bit) R 15252 15252 21452 0 -1 0 244876 0 0 0 119263 915 0 0 25 0 1 0 1854979664 832614400 178956 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15256/statm): 203275 178956 145 145 0 203130 0 [pid=15256] vsize: 813100 Current children cumulated CPU time (s) 1201.78 Current children cumulated vsize (Kb) 815224 Sending SIGTERM to -15252 Sleeping 2 seconds One traced child (pid=15252) ended because it received signal 15 (SIGTERM) One traced child (pid=15256) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.45 CPU time (s): 1202.14 CPU user time (s): 1192.63 CPU system time (s): 9.50855 CPU usage (%): 99.3138 Max. virtual memory (cumulated for all children) (Kb): 815224
ERROR: no interpretation found !