Name | mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-egout.opb |
MD5SUM | 46c4db5f8baf54496e00a723c85beb20 |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 65869824 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 1095 |
Biggest coefficient in the objective function | 533200896 |
Number of bits for the biggest coefficient in the objective function | 29 |
Sum of the numbers in the objective function | 14929722305 |
Number of bits of the sum of numbers in the objective function | 34 |
Biggest number in a constraint | 533200896 |
Number of bits of the biggest number in a constraint | 29 |
Biggest sum of numbers in a constraint | 14929722305 |
Number of bits of the biggest sum of numbers | 34 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1257.65 |
Number of variables | 1155 |
Total number of constraints | 153 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 55 |
Number of constraints which are nor clauses,nor cardinality constraints | 98 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 280 |
LAUNCH ON wulflinc13 THE 2005-09-20 03:08:36 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3235 boxname=wulflinc13 idbench=891 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 46c4db5f8baf54496e00a723c85beb20 /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-egout.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-egout.opb IDLAUNCH: 3235 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.242 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.242 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 : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 901452 kB Buffers: 28588 kB Cached: 77608 kB SwapCached: 700 kB Active: 32924 kB Inactive: 75852 kB HighTotal: 131008 kB HighFree: 49504 kB LowTotal: 903652 kB LowFree: 851948 kB SwapTotal: 2097136 kB SwapFree: 2095936 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5740 kB Slab: 18828 kB Committed_AS: 64164 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-20 03:28:46 (client local time) WITH STATUS 10 IN 1209.42 SECONDS stats: 3235 7 1209.42 10
c Parsing PB file... c Converting 115 PB-constraints to clauses... c -- Unit propagations: pppppppppppppppppppppppppppppppppppp c -- Detecting intervals from adjacent constraints: ########################### c -- Clauses(.)/Splits(s): (none) c ---[ 113]---> Adder-cost: 273 maxlim: 13440 bits: 15/14 c ---[ 111]---> BDD-cost: 40 c ---[ 109]---> BDD-cost: 25 c ---[ 107]---> BDD-cost: 45 c ---[ 105]---> BDD-cost: 83 c ---[ 101]---> BDD-cost: 39 c ---[ 99]---> BDD-cost: 100 c ---[ 97]---> BDD-cost: 34 c ---[ 91]---> BDD-cost: 55 c ---[ 89]---> BDD-cost: 40 c ---[ 85]---> BDD-cost: 128 c ---[ 83]---> BDD-cost: 40 c ---[ 81]---> BDD-cost: 112 c ---[ 79]---> BDD-cost: 49 c ---[ 75]---> BDD-cost: 45 c ---[ 73]---> BDD-cost: 28 c ---[ 71]---> Sorter-cost: 514 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 69]---> BDD-cost: 55 c ---[ 67]---> Sorter-cost: 294 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 65]---> BDD-cost: 118 c ---[ 59]---> BDD-cost: 51 c ---[ 57]---> BDD-cost: 40 c ---[ 55]---> BDD-cost: 40 c ---[ 53]---> BDD-cost: 51 c ---[ 49]---> Sorter-cost: 309 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 47]---> Sorter-cost: 309 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 45]---> BDD-cost: 49 c ---[ 44]---> BDD-cost: 9 c ---[ 43]---> BDD-cost: 9 c ---[ 42]---> BDD-cost: 9 c ---[ 41]---> BDD-cost: 10 c ---[ 40]---> BDD-cost: 10 c ---[ 39]---> BDD-cost: 11 c ---[ 37]---> BDD-cost: 12 c ---[ 36]---> BDD-cost: 12 c ---[ 35]---> BDD-cost: 12 c ---[ 34]---> BDD-cost: 12 c ---[ 31]---> BDD-cost: 12 c ---[ 30]---> BDD-cost: 12 c ---[ 29]---> BDD-cost: 13 c ---[ 27]---> BDD-cost: 26 c ---[ 26]---> BDD-cost: 26 c ---[ 25]---> BDD-cost: 26 c ---[ 24]---> BDD-cost: 26 c ---[ 23]---> BDD-cost: 26 c ---[ 21]---> BDD-cost: 10 c ---[ 20]---> BDD-cost: 10 c ---[ 19]---> BDD-cost: 10 c ---[ 18]---> BDD-cost: 26 c ---[ 17]---> BDD-cost: 26 c ---[ 16]---> BDD-cost: 12 c ---[ 15]---> BDD-cost: 12 c ---[ 14]---> BDD-cost: 26 c ---[ 13]---> BDD-cost: 26 c ---[ 12]---> BDD-cost: 26 c ---[ 9]---> BDD-cost: 26 c ---[ 8]---> BDD-cost: 26 c ---[ 7]---> BDD-cost: 26 c ---[ 6]---> BDD-cost: 26 c ---[ 4]---> BDD-cost: 26 c ---[ 3]---> BDD-cost: 26 c ---[ 2]---> BDD-cost: 26 c ---[ 1]---> BDD-cost: 26 c ---[ 0]---> BDD-cost: 26 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 8871 23614 | 2957 0 0 nan | 0.000 % | c | 100 | 8706 23213 | 3252 62 334 5.4 | 23.506 % | c | 250 | 8614 23023 | 3577 176 817 4.6 | 24.498 % | c | 477 | 8528 22841 | 3935 375 2437 6.5 | 25.341 % | c ============================================================================== c [1mFound solution: 98251161[0m c ---[ 0]---> Sorter-cost:93899 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 730 | 274243 643179 | 91414 601 3802 6.3 | 25.341 % | c | 830 | 273012 640414 | 100555 689 4783 6.9 | 1.488 % | c | 980 | 272757 639831 | 110610 835 6097 7.3 | 1.557 % | c | 1209 | 272173 638509 | 121672 1057 7316 6.9 | 1.728 % | c | 1546 | 271248 636409 | 133839 1388 10219 7.4 | 2.008 % | c | 2053 | 270967 635780 | 147223 1885 16941 9.0 | 2.090 % | c ============================================================================== c [1mFound solution: 90380944[0m c ---[ 0]---> Sorter-cost:56645 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2528 | 421107 986844 | 140369 2270 26867 11.8 | 2.090 % | c | 2628 | 420986 986571 | 154405 2368 27410 11.6 | 2.870 % | c | 2778 | 418881 981794 | 169846 2509 29164 11.6 | 3.270 % | c ============================================================================== c [1mFound solution: 83601220[0m c ---[ 0]---> Sorter-cost:51266 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2859 | 560988 1313562 | 186996 2590 37268 14.4 | 3.270 % | c | 2959 | 560234 1311863 | 205695 2684 37786 14.1 | 2.647 % | c | 3109 | 560085 1311520 | 226265 2833 52989 18.7 | 2.671 % | c | 3334 | 559906 1311131 | 248891 3057 54077 17.7 | 2.703 % | c | 3672 | 559906 1311131 | 273780 3395 57914 17.1 | 2.703 % | c ============================================================================== c [1mFound solution: 75080280[0m c ---[ 0]---> Sorter-cost: 20 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3889 | 560311 1312659 | 186770 3605 66861 18.5 | 2.703 % | c | 3989 | 560053 1312084 | 205447 3701 67324 18.2 | 2.799 % | c | 4139 | 559865 1311660 | 225991 3849 71131 18.5 | 2.827 % | c | 4364 | 559744 1311385 | 248590 4073 72701 17.8 | 2.846 % | c | 4701 | 559733 1311361 | 273449 4409 75036 17.0 | 2.848 % | c | 5207 | 559649 1311172 | 300794 4914 78073 15.9 | 2.858 % | c ============================================================================== c [1mFound solution: 72902771[0m c ---[ 0]---> Sorter-cost: 21 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 5394 | 559424 1310762 | 186474 5083 83077 16.3 | 2.858 % | c | 5494 | 559424 1310762 | 205121 5183 84108 16.2 | 2.900 % | c | 5644 | 559424 1310762 | 225633 5333 94640 17.7 | 2.899 % | c | 5869 | 559350 1310597 | 248196 5557 103255 18.6 | 2.910 % | c | 6207 | 559293 1310471 | 273016 5888 119017 20.2 | 2.918 % | c | 6715 | 558850 1309460 | 300318 6394 140155 21.9 | 2.985 % | c ============================================================================== c [1mFound solution: 70799895[0m c ---[ 0]---> Sorter-cost: 19 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 7150 | 557562 1306544 | 185854 6823 185362 27.2 | 2.985 % | c | 7250 | 557562 1306544 | 204439 6923 191283 27.6 | 3.180 % | c | 7400 | 557562 1306544 | 224883 7073 196159 27.7 | 3.180 % | c ============================================================================== c [1mFound solution: 68823191[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 7433 | 557596 1306628 | 185865 7106 197145 27.7 | 3.180 % | c | 7535 | 557596 1306628 | 204451 7208 207757 28.8 | 3.181 % | c | 7689 | 557596 1306628 | 224896 7362 210303 28.6 | 3.181 % | c ============================================================================== c [1mFound solution: 66801712[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 7739 | 557622 1306690 | 185874 7412 211372 28.5 | 3.181 % | c | 7839 | 557622 1306690 | 204461 7512 214674 28.6 | 3.181 % | c | 7990 | 557622 1306690 | 224907 7663 221258 28.9 | 3.181 % | c | 8215 | 557575 1306584 | 247398 7887 224224 28.4 | 3.187 % | c | 8553 | 556893 1305042 | 272138 8018 226835 28.3 | 3.287 % | c | 9059 | 556893 1305042 | 299351 8524 351418 41.2 | 3.287 % | c | 9818 | 556828 1304894 | 329287 9282 372202 40.1 | 3.297 % | c | 10957 | 555966 1302938 | 362215 10397 418014 40.2 | 3.424 % | c ============================================================================== c [1mFound solution: 65961920[0m c ---[ 0]---> Sorter-cost: 19 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 12376 | 555644 1302223 | 185214 11760 470077 40.0 | 3.424 % | c | 12477 | 555644 1302223 | 203735 11861 473070 39.9 | 3.486 % | c | 12628 | 555140 1301079 | 224108 12008 479077 39.9 | 3.560 % | c | 12853 | 555140 1301079 | 246519 12233 483370 39.5 | 3.560 % | c | 13193 | 555140 1301079 | 271171 12572 490526 39.0 | 3.573 % | c ============================================================================== c [1mFound solution: 65957568[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 13361 | 554865 1300533 | 184955 12724 500141 39.3 | 3.573 % | c | 13464 | 554865 1300533 | 203450 12827 503589 39.3 | 3.603 % | c | 13618 | 554865 1300533 | 223795 12981 514623 39.6 | 3.603 % | c | 13843 | 554865 1300533 | 246175 13206 519440 39.3 | 3.603 % | c | 14180 | 554865 1300533 | 270792 13543 529329 39.1 | 3.603 % | c ============================================================================== c [1mFound solution: 64888022[0m c ---[ 0]---> Sorter-cost: 19 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14535 | 554886 1300584 | 184962 13898 594958 42.8 | 3.603 % | c | 14636 | 554872 1300551 | 203458 13996 595705 42.6 | 3.606 % | c | 14788 | 554843 1300486 | 223804 14134 596715 42.2 | 3.610 % | c ============================================================================== c [1mFound solution: 64714286[0m c ---[ 0]---> Sorter-cost: 19 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14980 | 554864 1300536 | 184954 14326 613466 42.8 | 3.610 % | c | 15081 | 554864 1300536 | 203449 14427 616582 42.7 | 3.611 % | c | 15231 | 554864 1300536 | 223794 14577 625465 42.9 | 3.611 % | c | 15456 | 554864 1300536 | 246173 14802 646941 43.7 | 3.611 % | c | 15795 | 554864 1300536 | 270791 15141 669297 44.2 | 3.611 % | c | 16301 | 554864 1300536 | 297870 15647 708282 45.3 | 3.611 % | c | 17060 | 554730 1300230 | 327657 16373 715663 43.7 | 3.633 % | c | 18200 | 554730 1300230 | 360423 17513 730350 41.7 | 3.633 % | c ============================================================================== c [1mFound solution: 64484352[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19484 | 554438 1299569 | 184812 18777 796102 42.4 | 3.633 % | c | 19584 | 554438 1299569 | 203293 18877 799033 42.3 | 3.678 % | c | 19735 | 554438 1299569 | 223622 19028 800696 42.1 | 3.678 % | c | 19961 | 554438 1299569 | 245984 19254 807646 41.9 | 3.678 % | c | 20299 | 554346 1299358 | 270583 19587 822303 42.0 | 3.696 % | c | 20808 | 554342 1299350 | 297641 20093 845460 42.1 | 3.698 % | c ============================================================================== c [1mFound solution: 64437712[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21505 | 554360 1299393 | 184786 20790 904089 43.5 | 3.698 % | c | 21606 | 554360 1299393 | 203264 20891 909522 43.5 | 3.698 % | c | 21757 | 554360 1299393 | 223591 21042 912661 43.4 | 3.698 % | c ============================================================================== c [1mFound solution: 64396544[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21945 | 554376 1299432 | 184792 21230 918944 43.3 | 3.698 % | c | 22046 | 554376 1299432 | 203271 21331 922113 43.2 | 3.698 % | c | 22196 | 554376 1299432 | 223598 21481 931036 43.3 | 3.698 % | c | 22421 | 554376 1299432 | 245958 21706 950010 43.8 | 3.698 % | c | 22759 | 554376 1299432 | 270553 22044 962059 43.6 | 3.698 % | c | 23266 | 554376 1299432 | 297609 22551 985413 43.7 | 3.698 % | c | 24025 | 554376 1299432 | 327370 23310 1062588 45.6 | 3.698 % | c ============================================================================== c [1mFound solution: 62242606[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 24056 | 554406 1299510 | 184802 23341 1064546 45.6 | 3.698 % | c ============================================================================== c [1mFound solution: 62227456[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 24064 | 554420 1299552 | 184806 23349 1065485 45.6 | 3.698 % | c ============================================================================== c [1mFound solution: 61803904[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 24109 | 554437 1299595 | 184812 23394 1073902 45.9 | 3.698 % | c | 24209 | 554437 1299595 | 203293 23494 1080333 46.0 | 3.699 % | c | 24359 | 554437 1299595 | 223622 23644 1085303 45.9 | 3.699 % | c | 24585 | 554437 1299595 | 245984 23870 1090840 45.7 | 3.699 % | c | 24922 | 554437 1299595 | 270583 24207 1126010 46.5 | 3.699 % | c | 25429 | 554437 1299595 | 297641 24714 1143562 46.3 | 3.699 % | c | 26188 | 554437 1299595 | 327405 25473 1189554 46.7 | 3.699 % | c ============================================================================== c [1mFound solution: 61163008[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 26618 | 554456 1299640 | 184818 25903 1208767 46.7 | 3.699 % | c | 26718 | 554456 1299640 | 203299 26003 1211182 46.6 | 3.699 % | c | 26868 | 554456 1299640 | 223629 26153 1216316 46.5 | 3.699 % | c | 27097 | 554456 1299640 | 245992 26382 1226946 46.5 | 3.699 % | c | 27434 | 554456 1299640 | 270592 26719 1256775 47.0 | 3.699 % | c ============================================================================== c [1mFound solution: 61074176[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 27834 | 554469 1299675 | 184823 27119 1270285 46.8 | 3.699 % | c | 27937 | 554469 1299675 | 203305 27222 1273811 46.8 | 3.700 % | c | 28088 | 554469 1299675 | 223635 27373 1277562 46.7 | 3.700 % | c | 28313 | 554469 1299675 | 245999 27598 1281403 46.4 | 3.700 % | c | 28650 | 554368 1299448 | 270599 27338 1282042 46.9 | 3.716 % | c | 29157 | 554368 1299448 | 297659 27845 1311748 47.1 | 3.716 % | c | 29916 | 554368 1299448 | 327425 28604 1384699 48.4 | 3.716 % | c | 31056 | 554270 1299227 | 360167 28464 1403177 49.3 | 3.736 % | c ============================================================================== c [1mFound solution: 60755072[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 31220 | 554285 1299261 | 184761 28628 1411761 49.3 | 3.736 % | c | 31322 | 554285 1299261 | 203237 28730 1418292 49.4 | 3.737 % | c | 31473 | 554285 1299261 | 223560 28881 1422836 49.3 | 3.737 % | c | 31698 | 554285 1299261 | 245916 29106 1431324 49.2 | 3.737 % | c | 32035 | 554278 1299246 | 270508 29441 1440465 48.9 | 3.738 % | c | 32541 | 554278 1299246 | 297559 29947 1458101 48.7 | 3.738 % | c | 33300 | 554278 1299246 | 327315 30706 1493978 48.7 | 3.738 % | c | 34440 | 554078 1298787 | 360046 31691 1539085 48.6 | 3.771 % | c ============================================================================== c [1mFound solution: 60662144[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 35760 | 554090 1298817 | 184696 33011 1588723 48.1 | 3.771 % | c | 35862 | 554090 1298817 | 203165 33113 1591007 48.0 | 3.771 % | c | 36012 | 554090 1298817 | 223482 33263 1597886 48.0 | 3.771 % | c | 36238 | 554090 1298817 | 245830 33489 1605823 48.0 | 3.771 % | c | 36575 | 554090 1298817 | 270413 33826 1614991 47.7 | 3.771 % | c | 37081 | 554080 1298795 | 297454 34330 1637375 47.7 | 3.772 % | c | 37840 | 554080 1298795 | 327200 35089 1664108 47.4 | 3.772 % | c | 38980 | 554080 1298795 | 359920 36229 1727605 47.7 | 3.773 % | c | 40688 | 554080 1298795 | 395912 37937 1878610 49.5 | 3.772 % | c | 43254 | 554032 1298686 | 435503 40502 2026738 50.0 | 3.784 % | c c *** TERMINATED *** s SATISFIABLE v I_0x2e_001_0x2e__0x2e__0x2e__bit0 -I_0x2e_001003_bit0 -I_0x2e_002003_bit0 -I_0x2e_002_0x2e__0x2e__0x2e__bit0 -I_0x2e_003005_bit0 I_0x2e_004005_bit0 -I_0x2e_004_0x2e__0x2e__0x2e__bit0 I_0x2e_005007_bit0 I_0x2e_006007_bit0 I_0x2e_007008_bit0 I_0x2e_008_0x2e__0x2e__0x2e__bit0 -I_0x2e_008009_bit0 I_0x2e_010012_bit0 I_0x2e_011012_bit0 -I_0x2e_012_0x2e__0x2e__0x2e__bit0 I_0x2e_012013_bit0 I_0x2e_013016_bit0 -I_0x2e_014015_bit0 I_0x2e_015016_bit0 I_0x2e_016_0x2e__0x2e__0x2e__bit0 -I_0x2e_016017_bit0 -I_0x2e_017018_bit0 -I_0x2e_009018_bit0 -I_0x2e_018019_bit0 I_0x2e_019024_bit0 -I_0x2e_024_0x2e__0x2e__0x2e__bit0 -I_0x2e_023024_bit0 -I_0x2e_022023_bit0 -I_0x2e_020022_bit0 I_0x2e_021022_bit0 I_0x2e_022_0x2e__0x2e__0x2e__bit0 I_0x2e_024026_bit0 I_0x2e_025026_bit0 -I_0x2e_025_0x2e__0x2e__0x2e__bit0 I_0x2e_026027_bit0 I_0x2e_027_0x2e__0x2e__0x2e__bit0 -I_0x2e_027032_bit0 -I_0x2e_030031_bit0 I_0x2e_031032_bit0 I_0x2e_029031_bit0 -I_0x2e_028029_bit0 -I_0x2e_028_0x2e__0x2e__0x2e__bit0 I_0x2e_032033_bit0 I_0x2e_033037_bit0 -I_0x2e_036037_bit0 -I_0x2e_034036_bit0 -I_0x2e_035036_bit0 I_0x2e_037038_bit0 I_0x2e_038040_bit0 I_0x2e_039040_bit0 -I_0x2e_040_0x2e__0x2e__0x2e__bit0 -I_0x2e_041_0x2e__0x2e__0x2e__bit0 I_0x2e_040041_bit0 I_0x2e_041042_bit0 I_0x2e_042_0x2e__0x2e__0x2e__bit0 -F_0x2e_001_0x2e__0x2e__0x2e__bit_7 -F_0x2e_001_0x2e__0x2e__0x2e__bit_6 -F_0x2e_001_0x2e__0x2e__0x2e__bit_5 -F_0x2e_001_0x2e__0x2e__0x2e__bit_4 -F_0x2e_001_0x2e__0x2e__0x2e__bit_3 -F_0x2e_001_0x2e__0x2e__0x2e__bit_2 -F_0x2e_001_0x2e__0x2e__0x2e__bit_1 -F_0x2e_001_0x2e__0x2e__0x2e__bit0 F_0x2e_001_0x2e__0x2e__0x2e__bit1 -F_0x2e_001_0x2e__0x2e__0x2e__bit2 -F_0x2e_001_0x2e__0x2e__0x2e__bit3 -F_0x2e_001_0x2e__0x2e__0x2e__bit4 -F_0x2e_001_0x2e__0x2e__0x2e__bit5 -F_0x2e_001_0x2e__0x2e__0x2e__bit6 -F_0x2e_001_0x2e__0x2e__0x2e__bit7 -F_0x2e_001_0x2e__0x2e__0x2e__bit8 -F_0x2e_001_0x2e__0x2e__0x2e__bit9 -F_0x2e_001_0x2e__0x2e__0x2e__bit10 -F_0x2e_001_0x2e__0x2e__0x2e__bit11 -F_0x2e_001_0x2e__0x2e__0x2e__bit12 -F_0x2e_001003_bit_7 -F_0x2e_001003_bit_6 -F_0x2e_001003_bit_5 -F_0x2e_001003_bit_4 -F_0x2e_001003_bit_3 -F_0x2e_001003_bit_2 -F_0x2e_001003_bit_1 -F_0x2e_001003_bit0 -F_0x2e_001003_bit1 -F_0x2e_001003_bit2 -F_0x2e_001003_bit3 -F_0x2e_001003_bit4 -F_0x2e_001003_bit5 -F_0x2e_001003_bit6 -F_0x2e_001003_bit7 -F_0x2e_001003_bit8 -F_0x2e_001003_bit9 -F_0x2e_001003_bit10 -F_0x2e_001003_bit11 -F_0x2e_001003_bit12 -F_0x2e_002003_bit_7 -F_0x2e_002003_bit_6 -F_0x2e_002003_bit_5 -F_0x2e_002003_bit_4 -F_0x2e_002003_bit_3 -F_0x2e_002003_bit_2 -F_0x2e_002003_bit_1 -F_0x2e_002003_bit0 -F_0x2e_002003_bit1 -F_0x2e_002003_bit2 -F_0x2e_002003_bit3 -F_0x2e_002003_bit4 -F_0x2e_002003_bit5 -F_0x2e_002003_bit6 -F_0x2e_002003_bit7 -F_0x2e_002003_bit8 -F_0x2e_002003_bit9 -F_0x2e_002003_bit10 -F_0x2e_002003_bit11 -F_0x2e_002003_bit12 -F_0x2e_002_0x2e__0x2e__0x2e__bit_7 -F_0x2e_002_0x2e__0x2e__0x2e__bit_6 -F_0x2e_002_0x2e__0x2e__0x2e__bit_5 -F_0x2e_002_0x2e__0x2e__0x2e__bit_4 -F_0x2e_002_0x2e__0x2e__0x2e__bit_3 -F_0x2e_002_0x2e__0x2e__0x2e__bit_2 -F_0x2e_002_0x2e__0x2e__0x2e__bit_1 -F_0x2e_002_0x2e__0x2e__0x2e__bit0 -F_0x2e_002_0x2e__0x2e__0x2e__bit1 -F_0x2e_002_0x2e__0x2e__0x2e__bit2 -F_0x2e_002_0x2e__0x2e__0x2e__bit3 -F_0x2e_002_0x2e__0x2e__0x2e__bit4 -F_0x2e_002_0x2e__0x2e__0x2e__bit5 -F_0x2e_002_0x2e__0x2e__0x2e__bit6 -F_0x2e_002_0x2e__0x2e__0x2e__bit7 -F_0x2e_002_0x2e__0x2e__0x2e__bit8 -F_0x2e_002_0x2e__0x2e__0x2e__bit9 -F_0x2e_002_0x2e__0x2e__0x2e__bit10 -F_0x2e_002_0x2e__0x2e__0x2e__bit11 -F_0x2e_002_0x2e__0x2e__0x2e__bit12 -F_0x2e_003005_bit_7 -F_0x2e_003005_bit_6 -F_0x2e_003005_bit_5 -F_0x2e_003005_bit_4 -F_0x2e_003005_bit_3 -F_0x2e_003005_bit_2 -F_0x2e_003005_bit_1 -F_0x2e_003005_bit0 -F_0x2e_003005_bit1 -F_0x2e_003005_bit2 -F_0x2e_003005_bit3 -F_0x2e_003005_bit4 -F_0x2e_003005_bit5 -F_0x2e_003005_bit6 -F_0x2e_003005_bit7 -F_0x2e_003005_bit8 -F_0x2e_003005_bit9 -F_0x2e_003005_bit10 -F_0x2e_003005_bit11 -F_0x2e_003005_bit12 -F_0x2e_004005_bit_7 -F_0x2e_004005_bit_6 -F_0x2e_004005_bit_5 -F_0x2e_004005_bit_4 -F_0x2e_004005_bit_3 -F_0x2e_004005_bit_2 -F_0x2e_004005_bit_1 F_0x2e_004005_bit0 F_0x2e_004005_bit1 F_0x2e_004005_bit2 -F_0x2e_004005_bit3 -F_0x2e_004005_bit4 -F_0x2e_004005_bit5 -F_0x2e_004005_bit6 -F_0x2e_004005_bit7 -F_0x2e_004005_bit8 -F_0x2e_004005_bit9 -F_0x2e_004005_bit10 -F_0x2e_004005_bit11 -F_0x2e_004005_bit12 -F_0x2e_004_0x2e__0x2e__0x2e__bit_7 -F_0x2e_004_0x2e__0x2e__0x2e__bit_6 -F_0x2e_004_0x2e__0x2e__0x2e__bit_5 -F_0x2e_004_0x2e__0x2e__0x2e__bit_4 -F_0x2e_004_0x2e__0x2e__0x2e__bit_3 -F_0x2e_004_0x2e__0x2e__0x2e__bit_2 -F_0x2e_004_0x2e__0x2e__0x2e__bit_1 -F_0x2e_004_0x2e__0x2e__0x2e__bit0 -F_0x2e_004_0x2e__0x2e__0x2e__bit1 -F_0x2e_004_0x2e__0x2e__0x2e__bit2 -F_0x2e_004_0x2e__0x2e__0x2e__bit3 -F_0x2e_004_0x2e__0x2e__0x2e__bit4 -F_0x2e_004_0x2e__0x2e__0x2e__bit5 -F_0x2e_004_0x2e__0x2e__0x2e__bit6 -F_0x2e_004_0x2e__0x2e__0x2e__bit7 -F_0x2e_004_0x2e__0x2e__0x2e__bit8 -F_0x2e_004_0x2e__0x2e__0x2e__bit9 -F_0x2e_004_0x2e__0x2e__0x2e__bit10 -F_0x2e_004_0x2e__0x2e__0x2e__bit11 -F_0x2e_004_0x2e__0x2e__0x2e__bit12 -F_0x2e_005007_bit_7 -F_0x2e_005007_bit_6 -F_0x2e_005007_bit_5 -F_0x2e_005007_bit_4 -F_0x2e_005007_bit_3 -F_0x2e_005007_bit_2 -F_0x2e_005007_bit_1 F_0x2e_005007_bit0 F_0x2e_005007_bit1 F_0x2e_005007_bit2 -F_0x2e_005007_bit3 -F_0x2e_005007_bit4 -F_0x2e_005007_bit5 -F_0x2e_005007_bit6 -F_0x2e_005007_bit7 -F_0x2e_005007_bit8 -F_0x2e_005007_bit9 -F_0x2e_005007_bit10 -F_0x2e_005007_bit11 -F_0x2e_005007_bit12 -F_0x2e_006007_bit_7 -F_0x2e_006007_bit_6 -F_0x2e_006007_bit_5 -F_0x2e_006007_bit_4 -F_0x2e_006007_bit_3 -F_0x2e_006007_bit_2 -F_0x2e_006007_bit_1 -F_0x2e_006007_bit0 -F_0x2e_006007_bit1 F_0x2e_006007_bit2 -F_0x2e_006007_bit3 -F_0x2e_006007_bit4 -F_0x2e_006007_bit5 -F_0x2e_006007_bit6 -F_0x2e_006007_bit7 -F_0x2e_006007_bit8 -F_0x2e_006007_bit9 -F_0x2e_006007_bit10 -F_0x2e_006007_bit11 -F_0x2e_006007_bit12 -F_0x2e_007008_bit_7 -F_0x2e_007008_bit_6 -F_0x2e_007008_bit_5 -F_0x2e_007008_bit_4 -F_0x2e_007008_bit_3 -F_0x2e_007008_bit_2 -F_0x2e_007008_bit_1 -F_0x2e_007008_bit0 -F_0x2e_007008_bit1 F_0x2e_007008_bit2 F_0x2e_007008_bit3 -F_0x2e_007008_bit4 -F_0x2e_007008_bit5 -F_0x2e_007008_bit6 -F_0x2e_007008_bit7 -F_0x2e_007008_bit8 -F_0x2e_007008_bit9 -F_0x2e_007008_bit10 -F_0x2e_007008_bit11 -F_0x2e_007008_bit12 -F_0x2e_008_0x2e__0x2e__0x2e__bit_7 -F_0x2e_008_0x2e__0x2e__0x2e__bit_6 -F_0x2e_008_0x2e__0x2e__0x2e__bit_5 -F_0x2e_008_0x2e__0x2e__0x2e__bit_4 -F_0x2e_008_0x2e__0x2e__0x2e__bit_3 -F_0x2e_008_0x2e__0x2e__0x2e__bit_2 -F_0x2e_008_0x2e__0x2e__0x2e__bit_1 -F_0x2e_008_0x2e__0x2e__0x2e__bit0 -F_0x2e_008_0x2e__0x2e__0x2e__bit1 F_0x2e_008_0x2e__0x2e__0x2e__bit2 F_0x2e_008_0x2e__0x2e__0x2e__bit3 -F_0x2e_008_0x2e__0x2e__0x2e__bit4 -F_0x2e_008_0x2e__0x2e__0x2e__bit5 -F_0x2e_008_0x2e__0x2e__0x2e__bit6 -F_0x2e_008_0x2e__0x2e__0x2e__bit7 -F_0x2e_008_0x2e__0x2e__0x2e__bit8 -F_0x2e_008_0x2e__0x2e__0x2e__bit9 -F_0x2e_008_0x2e__0x2e__0x2e__bit10 -F_0x2e_008_0x2e__0x2e__0x2e__bit11 -F_0x2e_008_0x2e__0x2e__0x2e__bit12 -F_0x2e_008009_bit_7 -F_0x2e_008009_bit_6 -F_0x2e_008009_bit_5 -F_0x2e_008009_bit_4 -F_0x2e_008009_bit_3 -F_0x2e_008009_bit_2 -F_0x2e_008009_bit_1 -F_0x2e_008009_bit0 -F_0x2e_008009_bit1 -F_0x2e_008009_bit2 -F_0x2e_008009_bit3 -F_0x2e_008009_bit4 -F_0x2e_008009_bit5 -F_0x2e_008009_bit6 -F_0x2e_008009_bit7 -F_0x2e_008009_bit8 -F_0x2e_008009_bit9 -F_0x2e_008009_bit10 -F_0x2e_008009_bit11 -F_0x2e_008009_bit12 -F_0x2e_010012_bit_7 -F_0x2e_010012_bit_6 -F_0x2e_010012_bit_5 -F_0x2e_010012_bit_4 -F_0x2e_010012_bit_3 -F_0x2e_010012_bit_2 -F_0x2e_010012_bit_1 F_0x2e_010012_bit0 -F_0x2e_010012_bit1 -F_0x2e_010012_bit2 -F_0x2e_010012_bit3 -F_0x2e_010012_bit4 -F_0x2e_010012_bit5 -F_0x2e_010012_bit6 -F_0x2e_010012_bit7 -F_0x2e_010012_bit8 -F_0x2e_010012_bit9 -F_0x2e_010012_bit10 -F_0x2e_010012_bit11 -F_0x2e_010012_bit12 -F_0x2e_012_0x2e__0x2e__0x2e__bit_7 -F_0x2e_012_0x2e__0x2e__0x2e__bit_6 -F_0x2e_012_0x2e__0x2e__0x2e__bit_5 -F_0x2e_012_0x2e__0x2e__0x2e__bit_4 -F_0x2e_012_0x2e__0x2e__0x2e__bit_3 -F_0x2e_012_0x2e__0x2e__0x2e__bit_2 -F_0x2e_012_0x2e__0x2e__0x2e__bit_1 -F_0x2e_012_0x2e__0x2e__0x2e__bit0 -F_0x2e_012_0x2e__0x2e__0x2e__bit1 -F_0x2e_012_0x2e__0x2e__0x2e__bit2 -F_0x2e_012_0x2e__0x2e__0x2e__bit3 -F_0x2e_012_0x2e__0x2e__0x2e__bit4 -F_0x2e_012_0x2e__0x2e__0x2e__bit5 -F_0x2e_012_0x2e__0x2e__0x2e__bit6 -F_0x2e_012_0x2e__0x2e__0x2e__bit7 -F_0x2e_012_0x2e__0x2e__0x2e__bit8 -F_0x2e_012_0x2e__0x2e__0x2e__bit9 -F_0x2e_012_0x2e__0x2e__0x2e__bit10 -F_0x2e_012_0x2e__0x2e__0x2e__bit11 -F_0x2e_012_0x2e__0x2e__0x2e__bit12 -F_0x2e_012013_bit_7 -F_0x2e_012013_bit_6 -F_0x2e_012013_bit_5 -F_0x2e_012013_bit_4 -F_0x2e_012013_bit_3 -F_0x2e_012013_bit_2 -F_0x2e_012013_bit_1 -F_0x2e_012013_bit0 F_0x2e_012013_bit1 F_0x2e_012013_bit2 -F_0x2e_012013_bit3 F_0x2e_012013_bit4 -F_0x2e_012013_bit5 -F_0x2e_012013_bit6 -F_0x2e_012013_bit7 -F_0x2e_012013_bit8 -F_0x2e_012013_bit9 -F_0x2e_012013_bit10 -F_0x2e_012013_bit11 -F_0x2e_012013_bit12 -F_0x2e_013016_bit_7 -F_0x2e_013016_bit_6 -F_0x2e_013016_bit_5 -F_0x2e_013016_bit_4 -F_0x2e_013016_bit_3 -F_0x2e_013016_bit_2 -F_0x2e_013016_bit_1 -F_0x2e_013016_bit0 F_0x2e_013016_bit1 -F_0x2e_013016_bit2 F_0x2e_013016_bit3 F_0x2e_013016_bit4 -F_0x2e_013016_bit5 -F_0x2e_013016_bit6 -F_0x2e_013016_bit7 -F_0x2e_013016_bit8 -F_0x2e_013016_bit9 -F_0x2e_013016_bit10 -F_0x2e_013016_bit11 -F_0x2e_013016_bit12 -F_0x2e_014015_bit_7 -F_0x2e_014015_bit_6 -F_0x2e_014015_bit_5 -F_0x2e_014015_bit_4 -F_0x2e_014015_bit_3 -F_0x2e_014015_bit_2 -F_0x2e_014015_bit_1 -F_0x2e_014015_bit0 -F_0x2e_014015_bit1 -F_0x2e_014015_bit2 -F_0x2e_014015_bit3 -F_0x2e_014015_bit4 -F_0x2e_014015_bit5 -F_0x2e_014015_bit6 -F_0x2e_014015_bit7 -F_0x2e_014015_bit8 -F_0x2e_014015_bit9 -F_0x2e_014015_bit10 -F_0x2e_014015_bit11 -F_0x2e_014015_bit12 -F_0x2e_015016_bit_7 -F_0x2e_015016_bit_6 -F_0x2e_015016_bit_5 -F_0x2e_015016_bit_4 -F_0x2e_015016_bit_3 -F_0x2e_015016_bit_2 -F_0x2e_015016_bit_1 F_0x2e_015016_bit0 -F_0x2e_015016_bit1 -F_0x2e_015016_bit2 -F_0x2e_015016_bit3 -F_0x2e_015016_bit4 -F_0x2e_015016_bit5 -F_0x2e_015016_bit6 -F_0x2e_015016_bit7 -F_0x2e_015016_bit8 -F_0x2e_015016_bit9 -F_0x2e_015016_bit10 -F_0x2e_015016_bit11 -F_0x2e_015016_bit12 -F_0x2e_016_0x2e__0x2e__0x2e__bit_7 -F_0x2e_016_0x2e__0x2e__0x2e__bit_6 -F_0x2e_016_0x2e__0x2e__0x2e__bit_5 -F_0x2e_016_0x2e__0x2e__0x2e__bit_4 -F_0x2e_016_0x2e__0x2e__0x2e__bit_3 -F_0x2e_016_0x2e__0x2e__0x2e__bit_2 -F_0x2e_016_0x2e__0x2e__0x2e__bit_1 F_0x2e_016_0x2e__0x2e__0x2e__bit0 F_0x2e_016_0x2e__0x2e__0x2e__bit1 -F_0x2e_016_0x2e__0x2e__0x2e__bit2 F_0x2e_016_0x2e__0x2e__0x2e__bit3 F_0x2e_016_0x2e__0x2e__0x2e__bit4 -F_0x2e_016_0x2e__0x2e__0x2e__bit5 -F_0x2e_016_0x2e__0x2e__0x2e__bit6 -F_0x2e_016_0x2e__0x2e__0x2e__bit7 -F_0x2e_016_0x2e__0x2e__0x2e__bit8 -F_0x2e_016_0x2e__0x2e__0x2e__bit9 -F_0x2e_016_0x2e__0x2e__0x2e__bit10 -F_0x2e_016_0x2e__0x2e__0x2e__bit11 -F_0x2e_016_0x2e__0x2e__0x2e__bit12 -F_0x2e_016017_bit_7 -F_0x2e_016017_bit_6 -F_0x2e_016017_bit_5 -F_0x2e_016017_bit_4 -F_0x2e_016017_bit_3 -F_0x2e_016017_bit_2 -F_0x2e_016017_bit_1 -F_0x2e_016017_bit0 -F_0x2e_016017_bit1 -F_0x2e_016017_bit2 -F_0x2e_016017_bit3 -F_0x2e_016017_bit4 -F_0x2e_016017_bit5 -F_0x2e_016017_bit6 -F_0x2e_016017_bit7 -F_0x2e_016017_bit8 -F_0x2e_016017_bit9 -F_0x2e_016017_bit10 -F_0x2e_016017_bit11 -F_0x2e_016017_bit12 -F_0x2e_017018_bit_7 -F_0x2e_017018_bit_6 -F_0x2e_017018_bit_5 -F_0x2e_017018_bit_4 -F_0x2e_017018_bit_3 -F_0x2e_017018_bit_2 -F_0x2e_017018_bit_1 -F_0x2e_017018_bit0 -F_0x2e_017018_bit1 -F_0x2e_017018_bit2 -F_0x2e_017018_bit3 -F_0x2e_017018_bit4 -F_0x2e_017018_bit5 -F_0x2e_017018_bit6 -F_0x2e_017018_bit7 -F_0x2e_017018_bit8 -F_0x2e_017018_bit9 -F_0x2e_017018_bit10 -F_0x2e_017018_bit11 -F_0x2e_017018_bit12 -F_0x2e_009018_bit_7 -F_0x2e_009018_bit_6 -F_0x2e_009018_bit_5 -F_0x2e_009018_bit_4 -F_0x2e_009018_bit_3 -F_0x2e_009018_bit_2 -F_0x2e_009018_bit_1 -F_0x2e_009018_bit0 -F_0x2e_009018_bit1 -F_0x2e_009018_bit2 -F_0x2e_009018_bit3 -F_0x2e_009018_bit4 -F_0x2e_009018_bit5 -F_0x2e_009018_bit6 -F_0x2e_009018_bit7 -F_0x2e_009018_bit8 -F_0x2e_009018_bit9 -F_0x2e_009018_bit10 -F_0x2e_009018_bit11 -F_0x2e_009018_bit12 -F_0x2e_018019_bit_7 -F_0x2e_018019_bit_6 -F_0x2e_018019_bit_5 -F_0x2e_018019_bit_4 -F_0x2e_018019_bit_3 -F_0x2e_018019_bit_2 -F_0x2e_018019_bit_1 -F_0x2e_018019_bit0 -F_0x2e_018019_bit1 -F_0x2e_018019_bit2 -F_0x2e_018019_bit3 -F_0x2e_018019_bit4 -F_0x2e_018019_bit5 -F_0x2e_018019_bit6 -F_0x2e_018019_bit7 -F_0x2e_018019_bit8 -F_0x2e_018019_bit9 -F_0x2e_018019_bit10 -F_0x2e_018019_bit11 -F_0x2e_018019_bit12 -F_0x2e_019024_bit_7 -F_0x2e_019024_bit_6 -F_0x2e_019024_bit_5 -F_0x2e_019024_bit_4 -F_0x2e_019024_bit_3 -F_0x2e_019024_bit_2 -F_0x2e_019024_bit_1 -F_0x2e_019024_bit0 F_0x2e_019024_bit1 -F_0x2e_019024_bit2 -F_0x2e_019024_bit3 -F_0x2e_019024_bit4 -F_0x2e_019024_bit5 -F_0x2e_019024_bit6 -F_0x2e_019024_bit7 -F_0x2e_019024_bit8 -F_0x2e_019024_bit9 -F_0x2e_019024_bit10 -F_0x2e_019024_bit11 -F_0x2e_019024_bit12 -F_0x2e_024_0x2e__0x2e__0x2e__bit_7 -F_0x2e_024_0x2e__0x2e__0x2e__bit_6 -F_0x2e_024_0x2e__0x2e__0x2e__bit_5 -F_0x2e_024_0x2e__0x2e__0x2e__bit_4 -F_0x2e_024_0x2e__0x2e__0x2e__bit_3 -F_0x2e_024_0x2e__0x2e__0x2e__bit_2 -F_0x2e_024_0x2e__0x2e__0x2e__bit_1 -F_0x2e_024_0x2e__0x2e__0x2e__bit0 -F_0x2e_024_0x2e__0x2e__0x2e__bit1 -F_0x2e_024_0x2e__0x2e__0x2e__bit2 -F_0x2e_024_0x2e__0x2e__0x2e__bit3 -F_0x2e_024_0x2e__0x2e__0x2e__bit4 -F_0x2e_024_0x2e__0x2e__0x2e__bit5 -F_0x2e_024_0x2e__0x2e__0x2e__bit6 -F_0x2e_024_0x2e__0x2e__0x2e__bit7 -F_0x2e_024_0x2e__0x2e__0x2e__bit8 -F_0x2e_024_0x2e__0x2e__0x2e__bit9 -F_0x2e_024_0x2e__0x2e__0x2e__bit10 -F_0x2e_024_0x2e__0x2e__0x2e__bit11 -F_0x2e_024_0x2e__0x2e__0x2e__bit12 -F_0x2e_023024_bit_7 -F_0x2e_023024_bit_6 -F_0x2e_023024_bit_5 -F_0x2e_023024_bit_4 -F_0x2e_023024_bit_3 -F_0x2e_023024_bit_2 -F_0x2e_023024_bit_1 -F_0x2e_023024_bit0 -F_0x2e_023024_bit1 -F_0x2e_023024_bit2 -F_0x2e_023024_bit3 -F_0x2e_023024_bit4 -F_0x2e_023024_bit5 -F_0x2e_023024_bit6 -F_0x2e_023024_bit7 -F_0x2e_023024_bit8 -F_0x2e_023024_bit9 -F_0x2e_023024_bit10 -F_0x2e_023024_bit11 -F_0x2e_023024_bit12 -F_0x2e_022023_bit_7 -F_0x2e_022023_bit_6 -F_0x2e_022023_bit_5 -F_0x2e_022023_bit_4 -F_0x2e_022023_bit_3 -F_0x2e_022023_bit_2 -F_0x2e_022023_bit_1 -F_0x2e_022023_bit0 -F_0x2e_022023_bit1 -F_0x2e_022023_bit2 -F_0x2e_022023_bit3 -F_0x2e_022023_bit4 -F_0x2e_022023_bit5 -F_0x2e_022023_bit6 -F_0x2e_022023_bit7 -F_0x2e_022023_bit8 -F_0x2e_022023_bit9 -F_0x2e_022023_bit10 -F_0x2e_022023_bit11 -F_0x2e_022023_bit12 -F_0x2e_020022_bit_7 -F_0x2e_020022_bit_6 -F_0x2e_020022_bit_5 -F_0x2e_020022_bit_4 -F_0x2e_020022_bit_3 -F_0x2e_020022_bit_2 -F_0x2e_020022_bit_1 -F_0x2e_020022_bit0 -F_0x2e_020022_bit1 -F_0x2e_020022_bit2 -F_0x2e_020022_bit3 -F_0x2e_020022_bit4 -F_0x2e_020022_bit5 -F_0x2e_020022_bit6 -F_0x2e_020022_bit7 -F_0x2e_020022_bit8 -F_0x2e_020022_bit9 -F_0x2e_020022_bit10 -F_0x2e_020022_bit11 -F_0x2e_020022_bit12 -F_0x2e_021022_bit_7 -F_0x2e_021022_bit_6 -F_0x2e_021022_bit_5 -F_0x2e_021022_bit_4 -F_0x2e_021022_bit_3 -F_0x2e_021022_bit_2 -F_0x2e_021022_bit_1 F_0x2e_021022_bit0 F_0x2e_021022_bit1 F_0x2e_021022_bit2 -F_0x2e_021022_bit3 -F_0x2e_021022_bit4 -F_0x2e_021022_bit5 -F_0x2e_021022_bit6 -F_0x2e_021022_bit7 -F_0x2e_021022_bit8 -F_0x2e_021022_bit9 -F_0x2e_021022_bit10 -F_0x2e_021022_bit11 -F_0x2e_021022_bit12 -F_0x2e_022_0x2e__0x2e__0x2e__bit_7 -F_0x2e_022_0x2e__0x2e__0x2e__bit_6 -F_0x2e_022_0x2e__0x2e__0x2e__bit_5 -F_0x2e_022_0x2e__0x2e__0x2e__bit_4 -F_0x2e_022_0x2e__0x2e__0x2e__bit_3 -F_0x2e_022_0x2e__0x2e__0x2e__bit_2 -F_0x2e_022_0x2e__0x2e__0x2e__bit_1 F_0x2e_022_0x2e__0x2e__0x2e__bit0 F_0x2e_022_0x2e__0x2e__0x2e__bit1 F_0x2e_022_0x2e__0x2e__0x2e__bit2 -F_0x2e_022_0x2e__0x2e__0x2e__bit3 -F_0x2e_022_0x2e__0x2e__0x2e__bit4 -F_0x2e_022_0x2e__0x2e__0x2e__bit5 -F_0x2e_022_0x2e__0x2e__0x2e__bit6 -F_0x2e_022_0x2e__0x2e__0x2e__bit7 -F_0x2e_022_0x2e__0x2e__0x2e__bit8 -F_0x2e_022_0x2e__0x2e__0x2e__bit9 -F_0x2e_022_0x2e__0x2e__0x2e__bit10 -F_0x2e_022_0x2e__0x2e__0x2e__bit11 -F_0x2e_022_0x2e__0x2e__0x2e__bit12 -F_0x2e_024026_bit_7 -F_0x2e_024026_bit_6 -F_0x2e_024026_bit_5 -F_0x2e_024026_bit_4 -F_0x2e_024026_bit_3 -F_0x2e_024026_bit_2 -F_0x2e_024026_bit_1 -F_0x2e_024026_bit0 F_0x2e_024026_bit1 -F_0x2e_024026_bit2 -F_0x2e_024026_bit3 -F_0x2e_024026_bit4 -F_0x2e_024026_bit5 -F_0x2e_024026_bit6 -F_0x2e_024026_bit7 -F_0x2e_024026_bit8 -F_0x2e_024026_bit9 -F_0x2e_024026_bit10 -F_0x2e_024026_bit11 -F_0x2e_024026_bit12 -F_0x2e_025026_bit_7 -F_0x2e_025026_bit_6 -F_0x2e_025026_bit_5 -F_0x2e_025026_bit_4 -F_0x2e_025026_bit_3 -F_0x2e_025026_bit_2 -F_0x2e_025026_bit_1 F_0x2e_025026_bit0 F_0x2e_025026_bit1 -F_0x2e_025026_bit2 -F_0x2e_025026_bit3 F_0x2e_025026_bit4 -F_0x2e_025026_bit5 -F_0x2e_025026_bit6 -F_0x2e_025026_bit7 -F_0x2e_025026_bit8 -F_0x2e_025026_bit9 -F_0x2e_025026_bit10 -F_0x2e_025026_bit11 -F_0x2e_025026_bit12 -F_0x2e_025_0x2e__0x2e__0x2e__bit_7 -F_0x2e_025_0x2e__0x2e__0x2e__bit_6 -F_0x2e_025_0x2e__0x2e__0x2e__bit_5 -F_0x2e_025_0x2e__0x2e__0x2e__bit_4 -F_0x2e_025_0x2e__0x2e__0x2e__bit_3 -F_0x2e_025_0x2e__0x2e__0x2e__bit_2 -F_0x2e_025_0x2e__0x2e__0x2e__bit_1 -F_0x2e_025_0x2e__0x2e__0x2e__bit0 -F_0x2e_025_0x2e__0x2e__0x2e__bit1 -F_0x2e_025_0x2e__0x2e__0x2e__bit2 -F_0x2e_025_0x2e__0x2e__0x2e__bit3 -F_0x2e_025_0x2e__0x2e__0x2e__bit4 -F_0x2e_025_0x2e__0x2e__0x2e__bit5 -F_0x2e_025_0x2e__0x2e__0x2e__bit6 -F_0x2e_025_0x2e__0x2e__0x2e__bit7 -F_0x2e_025_0x2e__0x2e__0x2e__bit8 -F_0x2e_025_0x2e__0x2e__0x2e__bit9 -F_0x2e_025_0x2e__0x2e__0x2e__bit10 -F_0x2e_025_0x2e__0x2e__0x2e__bit11 -F_0x2e_025_0x2e__0x2e__0x2e__bit12 -F_0x2e_026027_bit_7 -F_0x2e_026027_bit_6 -F_0x2e_026027_bit_5 -F_0x2e_026027_bit_4 -F_0x2e_026027_bit_3 -F_0x2e_026027_bit_2 -F_0x2e_026027_bit_1 F_0x2e_026027_bit0 F_0x2e_026027_bit1 F_0x2e_026027_bit2 F_0x2e_026027_bit3 F_0x2e_026027_bit4 -F_0x2e_026027_bit5 -F_0x2e_026027_bit6 -F_0x2e_026027_bit7 -F_0x2e_026027_bit8 -F_0x2e_026027_bit9 -F_0x2e_026027_bit10 -F_0x2e_026027_bit11 -F_0x2e_026027_bit12 -F_0x2e_027_0x2e__0x2e__0x2e__bit_7 -F_0x2e_027_0x2e__0x2e__0x2e__bit_6 -F_0x2e_027_0x2e__0x2e__0x2e__bit_5 -F_0x2e_027_0x2e__0x2e__0x2e__bit_4 -F_0x2e_027_0x2e__0x2e__0x2e__bit_3 -F_0x2e_027_0x2e__0x2e__0x2e__bit_2 -F_0x2e_027_0x2e__0x2e__0x2e__bit_1 F_0x2e_027_0x2e__0x2e__0x2e__bit0 F_0x2e_027_0x2e__0x2e__0x2e__bit1 F_0x2e_027_0x2e__0x2e__0x2e__bit2 F_0x2e_027_0x2e__0x2e__0x2e__bit3 F_0x2e_027_0x2e__0x2e__0x2e__bit4 -F_0x2e_027_0x2e__0x2e__0x2e__bit5 -F_0x2e_027_0x2e__0x2e__0x2e__bit6 -F_0x2e_027_0x2e__0x2e__0x2e__bit7 -F_0x2e_027_0x2e__0x2e__0x2e__bit8 -F_0x2e_027_0x2e__0x2e__0x2e__bit9 -F_0x2e_027_0x2e__0x2e__0x2e__bit10 -F_0x2e_027_0x2e__0x2e__0x2e__bit11 -F_0x2e_027_0x2e__0x2e__0x2e__bit12 -F_0x2e_027032_bit_7 -F_0x2e_027032_bit_6 -F_0x2e_027032_bit_5 -F_0x2e_027032_bit_4 -F_0x2e_027032_bit_3 -F_0x2e_027032_bit_2 -F_0x2e_027032_bit_1 -F_0x2e_027032_bit0 -F_0x2e_027032_bit1 -F_0x2e_027032_bit2 -F_0x2e_027032_bit3 -F_0x2e_027032_bit4 -F_0x2e_027032_bit5 -F_0x2e_027032_bit6 -F_0x2e_027032_bit7 -F_0x2e_027032_bit8 -F_0x2e_027032_bit9 -F_0x2e_027032_bit10 -F_0x2e_027032_bit11 -F_0x2e_027032_bit12 -F_0x2e_030031_bit_7 -F_0x2e_030031_bit_6 -F_0x2e_030031_bit_5 -F_0x2e_030031_bit_4 -F_0x2e_030031_bit_3 -F_0x2e_030031_bit_2 -F_0x2e_030031_bit_1 -F_0x2e_030031_bit0 -F_0x2e_030031_bit1 -F_0x2e_030031_bit2 -F_0x2e_030031_bit3 -F_0x2e_030031_bit4 -F_0x2e_030031_bit5 -F_0x2e_030031_bit6 -F_0x2e_030031_bit7 -F_0x2e_030031_bit8 -F_0x2e_030031_bit9 -F_0x2e_030031_bit10 -F_0x2e_030031_bit11 -F_0x2e_030031_bit12 -F_0x2e_031032_bit_7 -F_0x2e_031032_bit_6 -F_0x2e_031032_bit_5 -F_0x2e_031032_bit_4 -F_0x2e_031032_bit_3 -F_0x2e_031032_bit_2 -F_0x2e_031032_bit_1 F_0x2e_031032_bit0 -F_0x2e_031032_bit1 F_0x2e_031032_bit2 -F_0x2e_031032_bit3 -F_0x2e_031032_bit4 -F_0x2e_031032_bit5 -F_0x2e_031032_bit6 -F_0x2e_031032_bit7 -F_0x2e_031032_bit8 -F_0x2e_031032_bit9 -F_0x2e_031032_bit10 -F_0x2e_031032_bit11 -F_0x2e_031032_bit12 -F_0x2e_029031_bit_7 -F_0x2e_029031_bit_6 -F_0x2e_029031_bit_5 -F_0x2e_029031_bit_4 -F_0x2e_029031_bit_3 -F_0x2e_029031_bit_2 -F_0x2e_029031_bit_1 F_0x2e_029031_bit0 -F_0x2e_029031_bit1 F_0x2e_029031_bit2 -F_0x2e_029031_bit3 -F_0x2e_029031_bit4 -F_0x2e_029031_bit5 -F_0x2e_029031_bit6 -F_0x2e_029031_bit7 -F_0x2e_029031_bit8 -F_0x2e_029031_bit9 -F_0x2e_029031_bit10 -F_0x2e_029031_bit11 -F_0x2e_029031_bit12 -F_0x2e_028029_bit_7 -F_0x2e_028029_bit_6 -F_0x2e_028029_bit_5 -F_0x2e_028029_bit_4 -F_0x2e_028029_bit_3 -F_0x2e_028029_bit_2 -F_0x2e_028029_bit_1 -F_0x2e_028029_bit0 -F_0x2e_028029_bit1 -F_0x2e_028029_bit2 -F_0x2e_028029_bit3 -F_0x2e_028029_bit4 -F_0x2e_028029_bit5 -F_0x2e_028029_bit6 -F_0x2e_028029_bit7 -F_0x2e_028029_bit8 -F_0x2e_028029_bit9 -F_0x2e_028029_bit10 -F_0x2e_028029_bit11 -F_0x2e_028029_bit12 -F_0x2e_028_0x2e__0x2e__0x2e__bit_7 -F_0x2e_028_0x2e__0x2e__0x2e__bit_6 -F_0x2e_028_0x2e__0x2e__0x2e__bit_5 -F_0x2e_028_0x2e__0x2e__0x2e__bit_4 -F_0x2e_028_0x2e__0x2e__0x2e__bit_3 -F_0x2e_028_0x2e__0x2e__0x2e__bit_2 -F_0x2e_028_0x2e__0x2e__0x2e__bit_1 -F_0x2e_028_0x2e__0x2e__0x2e__bit0 -F_0x2e_028_0x2e__0x2e__0x2e__bit1 -F_0x2e_028_0x2e__0x2e__0x2e__bit2 -F_0x2e_028_0x2e__0x2e__0x2e__bit3 -F_0x2e_028_0x2e__0x2e__0x2e__bit4 -F_0x2e_028_0x2e__0x2e__0x2e__bit5 -F_0x2e_028_0x2e__0x2e__0x2e__bit6 -F_0x2e_028_0x2e__0x2e__0x2e__bit7 -F_0x2e_028_0x2e__0x2e__0x2e__bit8 -F_0x2e_028_0x2e__0x2e__0x2e__bit9 -F_0x2e_028_0x2e__0x2e__0x2e__bit10 -F_0x2e_028_0x2e__0x2e__0x2e__bit11 -F_0x2e_028_0x2e__0x2e__0x2e__bit12 -F_0x2e_032033_bit_7 -F_0x2e_032033_bit_6 -F_0x2e_032033_bit_5 -F_0x2e_032033_bit_4 -F_0x2e_032033_bit_3 -F_0x2e_032033_bit_2 -F_0x2e_032033_bit_1 F_0x2e_032033_bit0 -F_0x2e_032033_bit1 F_0x2e_032033_bit2 -F_0x2e_032033_bit3 -F_0x2e_032033_bit4 -F_0x2e_032033_bit5 -F_0x2e_032033_bit6 -F_0x2e_032033_bit7 -F_0x2e_032033_bit8 -F_0x2e_032033_bit9 -F_0x2e_032033_bit10 -F_0x2e_032033_bit11 -F_0x2e_032033_bit12 -F_0x2e_033037_bit_7 -F_0x2e_033037_bit_6 -F_0x2e_033037_bit_5 -F_0x2e_033037_bit_4 -F_0x2e_033037_bit_3 -F_0x2e_033037_bit_2 -F_0x2e_033037_bit_1 F_0x2e_033037_bit0 -F_0x2e_033037_bit1 F_0x2e_033037_bit2 -F_0x2e_033037_bit3 -F_0x2e_033037_bit4 -F_0x2e_033037_bit5 -F_0x2e_033037_bit6 -F_0x2e_033037_bit7 -F_0x2e_033037_bit8 -F_0x2e_033037_bit9 -F_0x2e_033037_bit10 -F_0x2e_033037_bit11 -F_0x2e_033037_bit12 -F_0x2e_034036_bit_7 -F_0x2e_034036_bit_6 -F_0x2e_034036_bit_5 -F_0x2e_034036_bit_4 -F_0x2e_034036_bit_3 -F_0x2e_034036_bit_2 -F_0x2e_034036_bit_1 -F_0x2e_034036_bit0 -F_0x2e_034036_bit1 -F_0x2e_034036_bit2 -F_0x2e_034036_bit3 -F_0x2e_034036_bit4 -F_0x2e_034036_bit5 -F_0x2e_034036_bit6 -F_0x2e_034036_bit7 -F_0x2e_034036_bit8 -F_0x2e_034036_bit9 -F_0x2e_034036_bit10 -F_0x2e_034036_bit11 -F_0x2e_034036_bit12 -F_0x2e_035036_bit_7 -F_0x2e_035036_bit_6 -F_0x2e_035036_bit_5 -F_0x2e_035036_bit_4 -F_0x2e_035036_bit_3 -F_0x2e_035036_bit_2 -F_0x2e_035036_bit_1 -F_0x2e_035036_bit0 -F_0x2e_035036_bit1 -F_0x2e_035036_bit2 -F_0x2e_035036_bit3 -F_0x2e_035036_bit4 -F_0x2e_035036_bit5 -F_0x2e_035036_bit6 -F_0x2e_035036_bit7 -F_0x2e_035036_bit8 -F_0x2e_035036_bit9 -F_0x2e_035036_bit10 -F_0x2e_035036_bit11 -F_0x2e_035036_bit12 -F_0x2e_037038_bit_7 -F_0x2e_037038_bit_6 -F_0x2e_037038_bit_5 -F_0x2e_037038_bit_4 -F_0x2e_037038_bit_3 -F_0x2e_037038_bit_2 -F_0x2e_037038_bit_1 F_0x2e_037038_bit0 -F_0x2e_037038_bit1 F_0x2e_037038_bit2 -F_0x2e_037038_bit3 -F_0x2e_037038_bit4 -F_0x2e_037038_bit5 -F_0x2e_037038_bit6 -F_0x2e_037038_bit7 -F_0x2e_037038_bit8 -F_0x2e_037038_bit9 -F_0x2e_037038_bit10 -F_0x2e_037038_bit11 -F_0x2e_037038_bit12 -F_0x2e_039040_bit_7 -F_0x2e_039040_bit_6 -F_0x2e_039040_bit_5 -F_0x2e_039040_bit_4 -F_0x2e_039040_bit_3 -F_0x2e_039040_bit_2 -F_0x2e_039040_bit_1 F_0x2e_039040_bit0 -F_0x2e_039040_bit1 F_0x2e_039040_bit2 -F_0x2e_039040_bit3 -F_0x2e_039040_bit4 -F_0x2e_039040_bit5 -F_0x2e_039040_bit6 -F_0x2e_039040_bit7 -F_0x2e_039040_bit8 -F_0x2e_039040_bit9 -F_0x2e_039040_bit10 -F_0x2e_039040_bit11 -F_0x2e_039040_bit12 -F_0x2e_040_0x2e__0x2e__0x2e__bit_7 -F_0x2e_040_0x2e__0x2e__0x2e__bit_6 -F_0x2e_040_0x2e__0x2e__0x2e__bit_5 -F_0x2e_040_0x2e__0x2e__0x2e__bit_4 -F_0x2e_040_0x2e__0x2e__0x2e__bit_3 -F_0x2e_040_0x2e__0x2e__0x2e__bit_2 -F_0x2e_040_0x2e__0x2e__0x2e__bit_1 -F_0x2e_040_0x2e__0x2e__0x2e__bit0 -F_0x2e_040_0x2e__0x2e__0x2e__bit1 -F_0x2e_040_0x2e__0x2e__0x2e__bit2 -F_0x2e_040_0x2e__0x2e__0x2e__bit3 -F_0x2e_040_0x2e__0x2e__0x2e__bit4 -F_0x2e_040_0x2e__0x2e__0x2e__bit5 -F_0x2e_040_0x2e__0x2e__0x2e__bit6 -F_0x2e_040_0x2e__0x2e__0x2e__bit7 -F_0x2e_040_0x2e__0x2e__0x2e__bit8 -F_0x2e_040_0x2e__0x2e__0x2e__bit9 -F_0x2e_040_0x2e__0x2e__0x2e__bit10 -F_0x2e_040_0x2e__0x2e__0x2e__bit11 -F_0x2e_040_0x2e__0x2e__0x2e__bit12 -F_0x2e_041_0x2e__0x2e__0x2e__bi
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/21774/stat): 21774 (minisat+_script) R 21773 21774 1333 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1796971020 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/21774/statm): 174 3 169 147 0 27 0 [pid=21774] 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=21775 New process pid=21776 New process pid=21777 execve syscall for /bin/sed executable One traced child (pid=21776) 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=21777) exited with status: 0 One traced child (pid=21775) exited with status: 0 New process pid=21778 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-egout.opb [startup+10.0034 s] Raw data (loadavg): 0.81 0.92 0.68 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 7994 0 0 0 935 31 0 0 25 0 1 0 1796971025 35749888 7665 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 8728 7665 145 145 0 8583 0 [pid=21778] vsize: 34912 Current children cumulated CPU time (s) 9.66 Current children cumulated vsize (Kb) 37036 [startup+20.0041 s] Raw data (loadavg): 0.84 0.93 0.69 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 8221 0 0 0 1933 32 0 0 25 0 1 0 1796971025 36712448 7892 4294967295 134512640 135094434 3221224432 3221222144 134600246 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 8963 7892 145 145 0 8818 0 [pid=21778] vsize: 35852 Current children cumulated CPU time (s) 19.65 Current children cumulated vsize (Kb) 37976 [startup+30.0058 s] Raw data (loadavg): 0.86 0.93 0.69 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 16568 0 0 0 2869 63 0 0 25 0 1 0 1796971025 73404416 15909 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21778/statm): 17921 15909 145 145 0 17776 0 [pid=21778] vsize: 71684 Current children cumulated CPU time (s) 29.32 Current children cumulated vsize (Kb) 73808 [startup+40.0064 s] Raw data (loadavg): 0.88 0.93 0.69 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 16626 0 0 0 3868 63 0 0 25 0 1 0 1796971025 73613312 15967 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 17972 15967 145 145 0 17827 0 [pid=21778] vsize: 71888 Current children cumulated CPU time (s) 39.31 Current children cumulated vsize (Kb) 74012 [startup+50.008 s] Raw data (loadavg): 0.90 0.93 0.70 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 16815 0 0 0 4868 64 0 0 25 0 1 0 1796971025 73949184 16156 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 18054 16156 145 145 0 17909 0 [pid=21778] vsize: 72216 Current children cumulated CPU time (s) 49.32 Current children cumulated vsize (Kb) 74340 [startup+60.0087 s] Raw data (loadavg): 0.91 0.93 0.70 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 16905 0 0 0 5867 64 0 0 25 0 1 0 1796971025 73969664 16168 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21778/statm): 18059 16168 145 145 0 17914 0 [pid=21778] vsize: 72236 Current children cumulated CPU time (s) 59.31 Current children cumulated vsize (Kb) 74360 [startup+70.0094 s] Raw data (loadavg): 0.93 0.93 0.70 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 16916 0 0 0 6867 64 0 0 25 0 1 0 1796971025 74010624 16179 4294967295 134512640 135094434 3221224432 3221223092 134553475 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 18069 16179 145 145 0 17924 0 [pid=21778] vsize: 72276 Current children cumulated CPU time (s) 69.31 Current children cumulated vsize (Kb) 74400 [startup+80.01 s] Raw data (loadavg): 0.94 0.94 0.70 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 16939 0 0 0 7866 65 0 0 25 0 1 0 1796971025 74104832 16202 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 18092 16202 145 145 0 17947 0 [pid=21778] vsize: 72368 Current children cumulated CPU time (s) 79.31 Current children cumulated vsize (Kb) 74492 [startup+90.0106 s] Raw data (loadavg): 0.95 0.94 0.71 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 16975 0 0 0 8865 65 0 0 25 0 1 0 1796971025 74252288 16238 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 18128 16238 145 145 0 17983 0 [pid=21778] vsize: 72512 Current children cumulated CPU time (s) 89.3 Current children cumulated vsize (Kb) 74636 [startup+100.011 s] Raw data (loadavg): 0.95 0.94 0.71 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17078 0 0 0 9865 65 0 0 25 0 1 0 1796971025 74522624 16305 4294967295 134512640 135094434 3221224432 3221223088 134557849 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 18194 16305 145 145 0 18049 0 [pid=21778] vsize: 72776 Current children cumulated CPU time (s) 99.3 Current children cumulated vsize (Kb) 74900 [startup+110.012 s] Raw data (loadavg): 0.96 0.94 0.71 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17138 0 0 0 10865 65 0 0 25 0 1 0 1796971025 74477568 16293 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 18183 16293 145 145 0 18038 0 [pid=21778] vsize: 72732 Current children cumulated CPU time (s) 109.3 Current children cumulated vsize (Kb) 74856 [startup+120.013 s] Raw data (loadavg): 0.97 0.94 0.72 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17200 0 0 0 11864 66 0 0 25 0 1 0 1796971025 74567680 16316 4294967295 134512640 135094434 3221224432 3221221104 134600314 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 18205 16316 145 145 0 18060 0 [pid=21778] vsize: 72820 Current children cumulated CPU time (s) 119.3 Current children cumulated vsize (Kb) 74944 [startup+130.013 s] Raw data (loadavg): 0.97 0.94 0.72 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17234 0 0 0 12864 66 0 0 25 0 1 0 1796971025 74551296 16313 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 18201 16313 145 145 0 18056 0 [pid=21778] vsize: 72804 Current children cumulated CPU time (s) 129.3 Current children cumulated vsize (Kb) 74928 [startup+140.014 s] Raw data (loadavg): 0.98 0.95 0.72 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17255 0 0 0 13864 66 0 0 25 0 1 0 1796971025 74637312 16334 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 18222 16334 145 145 0 18077 0 [pid=21778] vsize: 72888 Current children cumulated CPU time (s) 139.3 Current children cumulated vsize (Kb) 75012 [startup+150.016 s] Raw data (loadavg): 0.98 0.95 0.72 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17395 0 0 0 14862 67 0 0 25 0 1 0 1796971025 75280384 16474 4294967295 134512640 135094434 3221224432 3221223072 134558269 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 18379 16474 145 145 0 18234 0 [pid=21778] vsize: 73516 Current children cumulated CPU time (s) 149.29 Current children cumulated vsize (Kb) 75640 [startup+160.016 s] Raw data (loadavg): 0.98 0.95 0.73 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17407 0 0 0 15862 67 0 0 25 0 1 0 1796971025 75325440 16486 4294967295 134512640 135094434 3221224432 3221223056 134557675 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 18390 16486 145 145 0 18245 0 [pid=21778] vsize: 73560 Current children cumulated CPU time (s) 159.29 Current children cumulated vsize (Kb) 75684 [startup+170.016 s] Raw data (loadavg): 0.98 0.95 0.73 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17446 0 0 0 16862 67 0 0 25 0 1 0 1796971025 75485184 16525 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 18429 16525 145 145 0 18284 0 [pid=21778] vsize: 73716 Current children cumulated CPU time (s) 169.29 Current children cumulated vsize (Kb) 75840 [startup+180.016 s] Raw data (loadavg): 0.99 0.95 0.73 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17454 0 0 0 17862 67 0 0 25 0 1 0 1796971025 75517952 16533 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 18437 16533 145 145 0 18292 0 [pid=21778] vsize: 73748 Current children cumulated CPU time (s) 179.29 Current children cumulated vsize (Kb) 75872 [startup+190.017 s] Raw data (loadavg): 0.99 0.95 0.73 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17463 0 0 0 18862 68 0 0 25 0 1 0 1796971025 75550720 16542 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 18445 16542 145 145 0 18300 0 [pid=21778] vsize: 73780 Current children cumulated CPU time (s) 189.3 Current children cumulated vsize (Kb) 75904 [startup+200.018 s] Raw data (loadavg): 0.99 0.95 0.74 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17471 0 0 0 19862 68 0 0 25 0 1 0 1796971025 75583488 16550 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 18453 16550 145 145 0 18308 0 [pid=21778] vsize: 73812 Current children cumulated CPU time (s) 199.3 Current children cumulated vsize (Kb) 75936 [startup+210.018 s] Raw data (loadavg): 0.99 0.95 0.74 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) T 21774 21774 1333 0 -1 0 17486 0 0 0 20863 68 0 0 25 0 1 0 1796971025 75644928 16565 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/21778/statm): 18468 16565 145 145 0 18323 0 [pid=21778] vsize: 73872 Current children cumulated CPU time (s) 209.31 Current children cumulated vsize (Kb) 75996 [startup+220.019 s] Raw data (loadavg): 0.99 0.95 0.74 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17587 0 0 0 21862 68 0 0 25 0 1 0 1796971025 76107776 16666 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 18581 16666 145 145 0 18436 0 [pid=21778] vsize: 74324 Current children cumulated CPU time (s) 219.3 Current children cumulated vsize (Kb) 76448 [startup+230.02 s] Raw data (loadavg): 0.99 0.95 0.74 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17588 0 0 0 22862 68 0 0 25 0 1 0 1796971025 76107776 16667 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 18581 16667 145 145 0 18436 0 [pid=21778] vsize: 74324 Current children cumulated CPU time (s) 229.3 Current children cumulated vsize (Kb) 76448 [startup+240.02 s] Raw data (loadavg): 0.99 0.95 0.74 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17588 0 0 0 23862 68 0 0 25 0 1 0 1796971025 76107776 16667 4294967295 134512640 135094434 3221224432 3221223056 134562088 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 18581 16667 145 145 0 18436 0 [pid=21778] vsize: 74324 Current children cumulated CPU time (s) 239.3 Current children cumulated vsize (Kb) 76448 [startup+250.021 s] Raw data (loadavg): 0.99 0.96 0.75 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17588 0 0 0 24862 68 0 0 25 0 1 0 1796971025 76107776 16667 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 18581 16667 145 145 0 18436 0 [pid=21778] vsize: 74324 Current children cumulated CPU time (s) 249.3 Current children cumulated vsize (Kb) 76448 [startup+260.022 s] Raw data (loadavg): 0.99 0.96 0.75 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17663 0 0 0 25862 68 0 0 25 0 1 0 1796971025 76103680 16667 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 18580 16667 145 145 0 18435 0 [pid=21778] vsize: 74320 Current children cumulated CPU time (s) 259.3 Current children cumulated vsize (Kb) 76444 [startup+270.022 s] Raw data (loadavg): 0.99 0.96 0.75 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17675 0 0 0 26861 70 0 0 25 0 1 0 1796971025 76152832 16679 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 18592 16679 145 145 0 18447 0 [pid=21778] vsize: 74368 Current children cumulated CPU time (s) 269.31 Current children cumulated vsize (Kb) 76492 [startup+280.023 s] Raw data (loadavg): 0.99 0.96 0.75 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17689 0 0 0 27860 71 0 0 25 0 1 0 1796971025 76210176 16693 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 18606 16693 145 145 0 18461 0 [pid=21778] vsize: 74424 Current children cumulated CPU time (s) 279.31 Current children cumulated vsize (Kb) 76548 [startup+290.024 s] Raw data (loadavg): 0.99 0.96 0.75 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17827 0 0 0 28858 72 0 0 25 0 1 0 1796971025 76611584 16792 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 18704 16792 145 145 0 18559 0 [pid=21778] vsize: 74816 Current children cumulated CPU time (s) 289.3 Current children cumulated vsize (Kb) 76940 [startup+300.024 s] Raw data (loadavg): 0.99 0.96 0.76 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17896 0 0 0 29858 72 0 0 25 0 1 0 1796971025 76595200 16786 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 18700 16786 145 145 0 18555 0 [pid=21778] vsize: 74800 Current children cumulated CPU time (s) 299.3 Current children cumulated vsize (Kb) 76924 [startup+310.025 s] Raw data (loadavg): 0.99 0.96 0.76 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17924 0 0 0 30858 73 0 0 25 0 1 0 1796971025 76701696 16814 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 18726 16814 145 145 0 18581 0 [pid=21778] vsize: 74904 Current children cumulated CPU time (s) 309.31 Current children cumulated vsize (Kb) 77028 [startup+320.025 s] Raw data (loadavg): 0.99 0.96 0.76 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17949 0 0 0 31858 73 0 0 25 0 1 0 1796971025 76800000 16839 4294967295 134512640 135094434 3221224432 3221223088 134557859 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 18750 16839 145 145 0 18605 0 [pid=21778] vsize: 75000 Current children cumulated CPU time (s) 319.31 Current children cumulated vsize (Kb) 77124 [startup+330.026 s] Raw data (loadavg): 0.99 0.96 0.76 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17997 0 0 0 32857 74 0 0 25 0 1 0 1796971025 76996608 16887 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 18798 16887 145 145 0 18653 0 [pid=21778] vsize: 75192 Current children cumulated CPU time (s) 329.31 Current children cumulated vsize (Kb) 77316 [startup+340.027 s] Raw data (loadavg): 0.99 0.96 0.76 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18060 0 0 0 33856 74 0 0 25 0 1 0 1796971025 77312000 16950 4294967295 134512640 135094434 3221224432 3221223056 134557574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 18875 16950 145 145 0 18730 0 [pid=21778] vsize: 75500 Current children cumulated CPU time (s) 339.3 Current children cumulated vsize (Kb) 77624 [startup+350.028 s] Raw data (loadavg): 0.99 0.97 0.77 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18096 0 0 0 34856 74 0 0 25 0 1 0 1796971025 77455360 16986 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 18910 16986 145 145 0 18765 0 [pid=21778] vsize: 75640 Current children cumulated CPU time (s) 349.3 Current children cumulated vsize (Kb) 77764 [startup+360.028 s] Raw data (loadavg): 0.99 0.97 0.77 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18161 0 0 0 35855 75 0 0 25 0 1 0 1796971025 77561856 17012 4294967295 134512640 135094434 3221224432 3221222040 134676609 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 18936 17012 145 145 0 18791 0 [pid=21778] vsize: 75744 Current children cumulated CPU time (s) 359.3 Current children cumulated vsize (Kb) 77868 [startup+370.029 s] Raw data (loadavg): 0.99 0.97 0.77 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18190 0 0 0 36855 75 0 0 25 0 1 0 1796971025 77529088 17004 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 18928 17004 145 145 0 18783 0 [pid=21778] vsize: 75712 Current children cumulated CPU time (s) 369.3 Current children cumulated vsize (Kb) 77836 [startup+380.029 s] Raw data (loadavg): 0.99 0.97 0.77 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18201 0 0 0 37855 75 0 0 25 0 1 0 1796971025 77570048 17015 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 18938 17015 145 145 0 18793 0 [pid=21778] vsize: 75752 Current children cumulated CPU time (s) 379.3 Current children cumulated vsize (Kb) 77876 [startup+390.03 s] Raw data (loadavg): 0.99 0.97 0.77 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18223 0 0 0 38855 76 0 0 25 0 1 0 1796971025 77660160 17037 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 18960 17037 145 145 0 18815 0 [pid=21778] vsize: 75840 Current children cumulated CPU time (s) 389.31 Current children cumulated vsize (Kb) 77964 [startup+400.032 s] Raw data (loadavg): 0.99 0.97 0.77 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18239 0 0 0 39855 76 0 0 25 0 1 0 1796971025 77725696 17053 4294967295 134512640 135094434 3221224432 3221223056 134557660 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 18976 17053 145 145 0 18831 0 [pid=21778] vsize: 75904 Current children cumulated CPU time (s) 399.31 Current children cumulated vsize (Kb) 78028 [startup+410.032 s] Raw data (loadavg): 0.99 0.97 0.78 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18257 0 0 0 40854 76 0 0 25 0 1 0 1796971025 77795328 17071 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 18993 17071 145 145 0 18848 0 [pid=21778] vsize: 75972 Current children cumulated CPU time (s) 409.3 Current children cumulated vsize (Kb) 78096 [startup+420.033 s] Raw data (loadavg): 0.99 0.97 0.78 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18292 0 0 0 41854 76 0 0 25 0 1 0 1796971025 77938688 17106 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19028 17106 145 145 0 18883 0 [pid=21778] vsize: 76112 Current children cumulated CPU time (s) 419.3 Current children cumulated vsize (Kb) 78236 [startup+430.035 s] Raw data (loadavg): 0.99 0.97 0.78 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18391 0 0 0 42852 77 0 0 25 0 1 0 1796971025 78032896 17128 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19051 17128 145 145 0 18906 0 [pid=21778] vsize: 76204 Current children cumulated CPU time (s) 429.29 Current children cumulated vsize (Kb) 78328 [startup+440.035 s] Raw data (loadavg): 0.99 0.97 0.78 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18460 0 0 0 43852 78 0 0 25 0 1 0 1796971025 78151680 17158 4294967295 134512640 135094434 3221224432 3221220320 134677021 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19080 17158 145 145 0 18935 0 [pid=21778] vsize: 76320 Current children cumulated CPU time (s) 439.3 Current children cumulated vsize (Kb) 78444 [startup+450.037 s] Raw data (loadavg): 0.99 0.97 0.78 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18497 0 0 0 44851 78 0 0 25 0 1 0 1796971025 78151680 17158 4294967295 134512640 135094434 3221224432 3221223024 134556941 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19080 17158 145 145 0 18935 0 [pid=21778] vsize: 76320 Current children cumulated CPU time (s) 449.29 Current children cumulated vsize (Kb) 78444 [startup+460.038 s] Raw data (loadavg): 0.99 0.97 0.79 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18518 0 0 0 45852 78 0 0 25 0 1 0 1796971025 78233600 17179 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19100 17179 145 145 0 18955 0 [pid=21778] vsize: 76400 Current children cumulated CPU time (s) 459.3 Current children cumulated vsize (Kb) 78524 [startup+470.038 s] Raw data (loadavg): 0.99 0.97 0.79 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18541 0 0 0 46852 78 0 0 25 0 1 0 1796971025 78327808 17202 4294967295 134512640 135094434 3221224432 3221223088 134557804 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19123 17202 145 145 0 18978 0 [pid=21778] vsize: 76492 Current children cumulated CPU time (s) 469.3 Current children cumulated vsize (Kb) 78616 [startup+480.039 s] Raw data (loadavg): 0.99 0.97 0.79 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18558 0 0 0 47852 78 0 0 25 0 1 0 1796971025 78393344 17219 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19139 17219 145 145 0 18994 0 [pid=21778] vsize: 76556 Current children cumulated CPU time (s) 479.3 Current children cumulated vsize (Kb) 78680 [startup+490.04 s] Raw data (loadavg): 0.99 0.97 0.79 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18574 0 0 0 48851 79 0 0 25 0 1 0 1796971025 78458880 17235 4294967295 134512640 135094434 3221224432 3221223088 134558284 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19155 17235 145 145 0 19010 0 [pid=21778] vsize: 76620 Current children cumulated CPU time (s) 489.3 Current children cumulated vsize (Kb) 78744 [startup+500.041 s] Raw data (loadavg): 0.99 0.97 0.79 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18589 0 0 0 49852 79 0 0 25 0 1 0 1796971025 78520320 17250 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19170 17250 145 145 0 19025 0 [pid=21778] vsize: 76680 Current children cumulated CPU time (s) 499.31 Current children cumulated vsize (Kb) 78804 [startup+510.042 s] Raw data (loadavg): 0.99 0.97 0.80 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18629 0 0 0 50851 79 0 0 25 0 1 0 1796971025 78684160 17290 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19210 17290 145 145 0 19065 0 [pid=21778] vsize: 76840 Current children cumulated CPU time (s) 509.3 Current children cumulated vsize (Kb) 78964 [startup+520.043 s] Raw data (loadavg): 0.99 0.97 0.80 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18779 0 0 0 51850 80 0 0 25 0 1 0 1796971025 78831616 17326 4294967295 134512640 135094434 3221224432 3221221280 134600254 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19246 17326 145 145 0 19101 0 [pid=21778] vsize: 76984 Current children cumulated CPU time (s) 519.3 Current children cumulated vsize (Kb) 79108 [startup+530.043 s] Raw data (loadavg): 0.99 0.97 0.80 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18891 0 0 0 52849 81 0 0 25 0 1 0 1796971025 78835712 17326 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19247 17326 145 145 0 19102 0 [pid=21778] vsize: 76988 Current children cumulated CPU time (s) 529.3 Current children cumulated vsize (Kb) 79112 [startup+540.044 s] Raw data (loadavg): 0.99 0.97 0.80 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18902 0 0 0 53849 81 0 0 25 0 1 0 1796971025 78872576 17337 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19256 17337 145 145 0 19111 0 [pid=21778] vsize: 77024 Current children cumulated CPU time (s) 539.3 Current children cumulated vsize (Kb) 79148 [startup+550.045 s] Raw data (loadavg): 0.99 0.97 0.80 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18939 0 0 0 54849 81 0 0 25 0 1 0 1796971025 79024128 17374 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19293 17374 145 145 0 19148 0 [pid=21778] vsize: 77172 Current children cumulated CPU time (s) 549.3 Current children cumulated vsize (Kb) 79296 [startup+560.045 s] Raw data (loadavg): 0.99 0.97 0.81 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18957 0 0 0 55849 81 0 0 25 0 1 0 1796971025 79097856 17392 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19311 17392 145 145 0 19166 0 [pid=21778] vsize: 77244 Current children cumulated CPU time (s) 559.3 Current children cumulated vsize (Kb) 79368 [startup+570.046 s] Raw data (loadavg): 0.99 0.97 0.81 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18969 0 0 0 56849 81 0 0 25 0 1 0 1796971025 79142912 17404 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19322 17404 145 145 0 19177 0 [pid=21778] vsize: 77288 Current children cumulated CPU time (s) 569.3 Current children cumulated vsize (Kb) 79412 [startup+580.047 s] Raw data (loadavg): 0.99 0.97 0.81 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18988 0 0 0 57849 81 0 0 25 0 1 0 1796971025 79220736 17423 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19341 17423 145 145 0 19196 0 [pid=21778] vsize: 77364 Current children cumulated CPU time (s) 579.3 Current children cumulated vsize (Kb) 79488 [startup+590.047 s] Raw data (loadavg): 0.99 0.97 0.81 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19018 0 0 0 58849 82 0 0 25 0 1 0 1796971025 79339520 17453 4294967295 134512640 135094434 3221224432 3221223024 134557334 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19370 17453 145 145 0 19225 0 [pid=21778] vsize: 77480 Current children cumulated CPU time (s) 589.31 Current children cumulated vsize (Kb) 79604 [startup+600.049 s] Raw data (loadavg): 0.99 0.97 0.81 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19034 0 0 0 59849 82 0 0 25 0 1 0 1796971025 79405056 17469 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19386 17469 145 145 0 19241 0 [pid=21778] vsize: 77544 Current children cumulated CPU time (s) 599.31 Current children cumulated vsize (Kb) 79668 [startup+610.049 s] Raw data (loadavg): 0.99 0.97 0.82 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19124 0 0 0 60848 83 0 0 25 0 1 0 1796971025 79454208 17483 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19398 17483 145 145 0 19253 0 [pid=21778] vsize: 77592 Current children cumulated CPU time (s) 609.31 Current children cumulated vsize (Kb) 79716 [startup+620.049 s] Raw data (loadavg): 0.99 0.97 0.82 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19146 0 0 0 61848 83 0 0 25 0 1 0 1796971025 79548416 17505 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19421 17505 145 145 0 19276 0 [pid=21778] vsize: 77684 Current children cumulated CPU time (s) 619.31 Current children cumulated vsize (Kb) 79808 [startup+630.051 s] Raw data (loadavg): 0.99 0.97 0.82 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19161 0 0 0 62848 83 0 0 25 0 1 0 1796971025 79601664 17520 4294967295 134512640 135094434 3221224432 3221223088 134558276 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19434 17520 145 145 0 19289 0 [pid=21778] vsize: 77736 Current children cumulated CPU time (s) 629.31 Current children cumulated vsize (Kb) 79860 [startup+640.051 s] Raw data (loadavg): 0.99 0.97 0.82 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19183 0 0 0 63848 83 0 0 25 0 1 0 1796971025 79691776 17542 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19456 17542 145 145 0 19311 0 [pid=21778] vsize: 77824 Current children cumulated CPU time (s) 639.31 Current children cumulated vsize (Kb) 79948 [startup+650.052 s] Raw data (loadavg): 0.99 0.97 0.82 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19253 0 0 0 64848 83 0 0 25 0 1 0 1796971025 79818752 17573 4294967295 134512640 135094434 3221224432 3221220576 134676489 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19487 17573 145 145 0 19342 0 [pid=21778] vsize: 77948 Current children cumulated CPU time (s) 649.31 Current children cumulated vsize (Kb) 80072 [startup+660.053 s] Raw data (loadavg): 0.99 0.97 0.82 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19282 0 0 0 65847 83 0 0 25 0 1 0 1796971025 79781888 17564 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19478 17564 145 145 0 19333 0 [pid=21778] vsize: 77912 Current children cumulated CPU time (s) 659.3 Current children cumulated vsize (Kb) 80036 [startup+670.053 s] Raw data (loadavg): 0.99 0.97 0.82 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19294 0 0 0 66847 83 0 0 25 0 1 0 1796971025 79831040 17576 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19490 17576 145 145 0 19345 0 [pid=21778] vsize: 77960 Current children cumulated CPU time (s) 669.3 Current children cumulated vsize (Kb) 80084 [startup+680.054 s] Raw data (loadavg): 0.99 0.97 0.82 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19307 0 0 0 67847 84 0 0 25 0 1 0 1796971025 79880192 17589 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19502 17589 145 145 0 19357 0 [pid=21778] vsize: 78008 Current children cumulated CPU time (s) 679.31 Current children cumulated vsize (Kb) 80132 [startup+690.055 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19323 0 0 0 68847 84 0 0 25 0 1 0 1796971025 79945728 17605 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19518 17605 145 145 0 19373 0 [pid=21778] vsize: 78072 Current children cumulated CPU time (s) 689.31 Current children cumulated vsize (Kb) 80196 [startup+700.056 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19333 0 0 0 69847 84 0 0 25 0 1 0 1796971025 79986688 17615 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19528 17615 145 145 0 19383 0 [pid=21778] vsize: 78112 Current children cumulated CPU time (s) 699.31 Current children cumulated vsize (Kb) 80236 [startup+710.057 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19370 0 0 0 70847 84 0 0 25 0 1 0 1796971025 80142336 17652 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19566 17652 145 145 0 19421 0 [pid=21778] vsize: 78264 Current children cumulated CPU time (s) 709.31 Current children cumulated vsize (Kb) 80388 [startup+720.058 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19400 0 0 0 71847 84 0 0 25 0 1 0 1796971025 80257024 17682 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19594 17682 145 145 0 19449 0 [pid=21778] vsize: 78376 Current children cumulated CPU time (s) 719.31 Current children cumulated vsize (Kb) 80500 [startup+730.058 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19408 0 0 0 72847 84 0 0 25 0 1 0 1796971025 80289792 17690 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19602 17690 145 145 0 19457 0 [pid=21778] vsize: 78408 Current children cumulated CPU time (s) 729.31 Current children cumulated vsize (Kb) 80532 [startup+740.059 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19414 0 0 0 73847 84 0 0 25 0 1 0 1796971025 80314368 17696 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19608 17696 145 145 0 19463 0 [pid=21778] vsize: 78432 Current children cumulated CPU time (s) 739.31 Current children cumulated vsize (Kb) 80556 [startup+750.061 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19414 0 0 0 74847 85 0 0 25 0 1 0 1796971025 80314368 17696 4294967295 134512640 135094434 3221224432 3221223072 134558043 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19608 17696 145 145 0 19463 0 [pid=21778] vsize: 78432 Current children cumulated CPU time (s) 749.32 Current children cumulated vsize (Kb) 80556 [startup+760.061 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19432 0 0 0 75847 85 0 0 25 0 1 0 1796971025 80388096 17714 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19626 17714 145 145 0 19481 0 [pid=21778] vsize: 78504 Current children cumulated CPU time (s) 759.32 Current children cumulated vsize (Kb) 80628 [startup+770.062 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) T 21774 21774 1333 0 -1 0 19527 0 0 0 76847 85 0 0 25 0 1 0 1796971025 80465920 17733 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19645 17733 145 145 0 19500 0 [pid=21778] vsize: 78580 Current children cumulated CPU time (s) 769.32 Current children cumulated vsize (Kb) 80704 [startup+780.063 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19542 0 0 0 77847 85 0 0 25 0 1 0 1796971025 80527360 17748 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19660 17748 145 145 0 19515 0 [pid=21778] vsize: 78640 Current children cumulated CPU time (s) 779.32 Current children cumulated vsize (Kb) 80764 [startup+790.063 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19553 0 0 0 78847 85 0 0 25 0 1 0 1796971025 80572416 17759 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19671 17759 145 145 0 19526 0 [pid=21778] vsize: 78684 Current children cumulated CPU time (s) 789.32 Current children cumulated vsize (Kb) 80808 [startup+800.064 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19569 0 0 0 79847 85 0 0 25 0 1 0 1796971025 80633856 17775 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19686 17775 145 145 0 19541 0 [pid=21778] vsize: 78744 Current children cumulated CPU time (s) 799.32 Current children cumulated vsize (Kb) 80868 [startup+810.066 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19583 0 0 0 80847 85 0 0 25 0 1 0 1796971025 80695296 17789 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19701 17789 145 145 0 19556 0 [pid=21778] vsize: 78804 Current children cumulated CPU time (s) 809.32 Current children cumulated vsize (Kb) 80928 [startup+820.066 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19597 0 0 0 81847 85 0 0 25 0 1 0 1796971025 80748544 17803 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19714 17803 145 145 0 19569 0 [pid=21778] vsize: 78856 Current children cumulated CPU time (s) 819.32 Current children cumulated vsize (Kb) 80980 [startup+830.067 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19614 0 0 0 82847 85 0 0 25 0 1 0 1796971025 80814080 17820 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19730 17820 145 145 0 19585 0 [pid=21778] vsize: 78920 Current children cumulated CPU time (s) 829.32 Current children cumulated vsize (Kb) 81044 [startup+840.067 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19634 0 0 0 83847 86 0 0 25 0 1 0 1796971025 80896000 17840 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19750 17840 145 145 0 19605 0 [pid=21778] vsize: 79000 Current children cumulated CPU time (s) 839.33 Current children cumulated vsize (Kb) 81124 [startup+850.069 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19652 0 0 0 84847 86 0 0 25 0 1 0 1796971025 80969728 17858 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19768 17858 145 145 0 19623 0 [pid=21778] vsize: 79072 Current children cumulated CPU time (s) 849.33 Current children cumulated vsize (Kb) 81196 [startup+860.07 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19665 0 0 0 85847 86 0 0 25 0 1 0 1796971025 81022976 17871 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19781 17871 145 145 0 19636 0 [pid=21778] vsize: 79124 Current children cumulated CPU time (s) 859.33 Current children cumulated vsize (Kb) 81248 [startup+870.07 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19681 0 0 0 86846 87 0 0 25 0 1 0 1796971025 81084416 17887 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19796 17887 145 145 0 19651 0 [pid=21778] vsize: 79184 Current children cumulated CPU time (s) 869.33 Current children cumulated vsize (Kb) 81308 [startup+880.072 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19691 0 0 0 87845 88 0 0 25 0 1 0 1796971025 81125376 17897 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19806 17897 145 145 0 19661 0 [pid=21778] vsize: 79224 Current children cumulated CPU time (s) 879.33 Current children cumulated vsize (Kb) 81348 [startup+890.073 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19705 0 0 0 88845 88 0 0 25 0 1 0 1796971025 81182720 17911 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19820 17911 145 145 0 19675 0 [pid=21778] vsize: 79280 Current children cumulated CPU time (s) 889.33 Current children cumulated vsize (Kb) 81404 [startup+900.074 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19721 0 0 0 89845 88 0 0 25 0 1 0 1796971025 81248256 17927 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19836 17927 145 145 0 19691 0 [pid=21778] vsize: 79344 Current children cumulated CPU time (s) 899.33 Current children cumulated vsize (Kb) 81468 [startup+910.075 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19761 0 0 0 90845 89 0 0 25 0 1 0 1796971025 81543168 17967 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19908 17967 145 145 0 19763 0 [pid=21778] vsize: 79632 Current children cumulated CPU time (s) 909.34 Current children cumulated vsize (Kb) 81756 [startup+920.075 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19817 0 0 0 91844 89 0 0 25 0 1 0 1796971025 81608704 17984 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19924 17984 145 145 0 19779 0 [pid=21778] vsize: 79696 Current children cumulated CPU time (s) 919.33 Current children cumulated vsize (Kb) 81820 [startup+930.076 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19817 0 0 0 92844 90 0 0 25 0 1 0 1796971025 81608704 17984 4294967295 134512640 135094434 3221224432 3221223056 134557612 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19924 17984 145 145 0 19779 0 [pid=21778] vsize: 79696 Current children cumulated CPU time (s) 929.34 Current children cumulated vsize (Kb) 81820 [startup+940.077 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19826 0 0 0 93844 90 0 0 25 0 1 0 1796971025 81649664 17993 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19934 17993 145 145 0 19789 0 [pid=21778] vsize: 79736 Current children cumulated CPU time (s) 939.34 Current children cumulated vsize (Kb) 81860 [startup+950.078 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19848 0 0 0 94844 90 0 0 25 0 1 0 1796971025 81739776 18015 4294967295 134512640 135094434 3221224432 3221223072 134558048 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19956 18015 145 145 0 19811 0 [pid=21778] vsize: 79824 Current children cumulated CPU time (s) 949.34 Current children cumulated vsize (Kb) 81948 [startup+960.078 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19861 0 0 0 95844 90 0 0 25 0 1 0 1796971025 81788928 18028 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19968 18028 145 145 0 19823 0 [pid=21778] vsize: 79872 Current children cumulated CPU time (s) 959.34 Current children cumulated vsize (Kb) 81996 [startup+970.079 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19881 0 0 0 96844 90 0 0 25 0 1 0 1796971025 81870848 18048 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 19988 18048 145 145 0 19843 0 [pid=21778] vsize: 79952 Current children cumulated CPU time (s) 969.34 Current children cumulated vsize (Kb) 82076 [startup+980.08 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19908 0 0 0 97844 91 0 0 25 0 1 0 1796971025 81985536 18075 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 20016 18075 145 145 0 19871 0 [pid=21778] vsize: 80064 Current children cumulated CPU time (s) 979.35 Current children cumulated vsize (Kb) 82188 [startup+990.08 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19920 0 0 0 98844 91 0 0 25 0 1 0 1796971025 82026496 18087 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 20026 18087 145 145 0 19881 0 [pid=21778] vsize: 80104 Current children cumulated CPU time (s) 989.35 Current children cumulated vsize (Kb) 82228 [startup+1000.08 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19931 0 0 0 99844 91 0 0 25 0 1 0 1796971025 82071552 18098 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 20037 18098 145 145 0 19892 0 [pid=21778] vsize: 80148 Current children cumulated CPU time (s) 999.35 Current children cumulated vsize (Kb) 82272 [startup+1010.08 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19949 0 0 0 100843 91 0 0 25 0 1 0 1796971025 82141184 18116 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 20054 18116 145 145 0 19909 0 [pid=21778] vsize: 80216 Current children cumulated CPU time (s) 1009.34 Current children cumulated vsize (Kb) 82340 [startup+1020.08 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19967 0 0 0 101844 91 0 0 25 0 1 0 1796971025 82214912 18134 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 20072 18134 145 145 0 19927 0 [pid=21778] vsize: 80288 Current children cumulated CPU time (s) 1019.35 Current children cumulated vsize (Kb) 82412 [startup+1030.08 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19982 0 0 0 102844 91 0 0 25 0 1 0 1796971025 82276352 18149 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 20087 18149 145 145 0 19942 0 [pid=21778] vsize: 80348 Current children cumulated CPU time (s) 1029.35 Current children cumulated vsize (Kb) 82472 [startup+1040.08 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 20000 0 0 0 103844 91 0 0 25 0 1 0 1796971025 82345984 18167 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 20104 18167 145 145 0 19959 0 [pid=21778] vsize: 80416 Current children cumulated CPU time (s) 1039.35 Current children cumulated vsize (Kb) 82540 [startup+1050.09 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 20025 0 0 0 104843 92 0 0 25 0 1 0 1796971025 82456576 18192 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 20131 18192 145 145 0 19986 0 [pid=21778] vsize: 80524 Current children cumulated CPU time (s) 1049.35 Current children cumulated vsize (Kb) 82648 [startup+1060.09 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 20084 0 0 0 105843 92 0 0 25 0 1 0 1796971025 82706432 18251 4294967295 134512640 135094434 3221224432 3221223064 134557561 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 20192 18251 145 145 0 20047 0 [pid=21778] vsize: 80768 Current children cumulated CPU time (s) 1059.35 Current children cumulated vsize (Kb) 82892 [startup+1070.09 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 20132 0 0 0 106843 92 0 0 25 0 1 0 1796971025 82890752 18299 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 20237 18299 145 145 0 20092 0 [pid=21778] vsize: 80948 Current children cumulated CPU time (s) 1069.35 Current children cumulated vsize (Kb) 83072 [startup+1080.09 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 20152 0 0 0 107843 92 0 0 25 0 1 0 1796971025 82972672 18319 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 20257 18319 145 145 0 20112 0 [pid=21778] vsize: 81028 Current children cumulated CPU time (s) 1079.35 Current children cumulated vsize (Kb) 83152 [startup+1090.09 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 20178 0 0 0 108843 93 0 0 25 0 1 0 1796971025 83079168 18345 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 20283 18345 145 145 0 20138 0 [pid=21778] vsize: 81132 Current children cumulated CPU time (s) 1089.36 Current children cumulated vsize (Kb) 83256 [startup+1100.09 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 20202 0 0 0 109842 93 0 0 25 0 1 0 1796971025 83173376 18369 4294967295 134512640 135094434 3221224432 3221223076 134558261 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 20306 18369 145 145 0 20161 0 [pid=21778] vsize: 81224 Current children cumulated CPU time (s) 1099.35 Current children cumulated vsize (Kb) 83348 [startup+1110.09 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 20226 0 0 0 110842 93 0 0 25 0 1 0 1796971025 83271680 18393 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 20330 18393 145 145 0 20185 0 [pid=21778] vsize: 81320 Current children cumulated CPU time (s) 1109.35 Current children cumulated vsize (Kb) 83444 [startup+1120.09 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 20249 0 0 0 111842 93 0 0 25 0 1 0 1796971025 83365888 18416 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 20353 18416 145 145 0 20208 0 [pid=21778] vsize: 81412 Current children cumulated CPU time (s) 1119.35 Current children cumulated vsize (Kb) 83536 [startup+1130.09 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 20266 0 0 0 112842 93 0 0 25 0 1 0 1796971025 83435520 18433 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 20370 18433 145 145 0 20225 0 [pid=21778] vsize: 81480 Current children cumulated CPU time (s) 1129.35 Current children cumulated vsize (Kb) 83604 [startup+1140.09 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 20284 0 0 0 113842 93 0 0 25 0 1 0 1796971025 83517440 18451 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 20390 18451 145 145 0 20245 0 [pid=21778] vsize: 81560 Current children cumulated CPU time (s) 1139.35 Current children cumulated vsize (Kb) 83684 [startup+1150.09 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 20308 0 0 0 114842 94 0 0 25 0 1 0 1796971025 83623936 18475 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 20416 18475 145 145 0 20271 0 [pid=21778] vsize: 81664 Current children cumulated CPU time (s) 1149.36 Current children cumulated vsize (Kb) 83788 [startup+1160.09 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 20319 0 0 0 115842 94 0 0 25 0 1 0 1796971025 83660800 18486 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 20425 18486 145 145 0 20280 0 [pid=21778] vsize: 81700 Current children cumulated CPU time (s) 1159.36 Current children cumulated vsize (Kb) 83824 [startup+1170.1 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 20345 0 0 0 116842 94 0 0 25 0 1 0 1796971025 83763200 18512 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 20450 18512 145 145 0 20305 0 [pid=21778] vsize: 81800 Current children cumulated CPU time (s) 1169.36 Current children cumulated vsize (Kb) 83924 [startup+1180.1 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 20358 0 0 0 117842 94 0 0 25 0 1 0 1796971025 83816448 18525 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 20463 18525 145 145 0 20318 0 [pid=21778] vsize: 81852 Current children cumulated CPU time (s) 1179.36 Current children cumulated vsize (Kb) 83976 [startup+1190.1 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 20367 0 0 0 118842 94 0 0 25 0 1 0 1796971025 83853312 18534 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 20472 18534 145 145 0 20327 0 [pid=21778] vsize: 81888 Current children cumulated CPU time (s) 1189.36 Current children cumulated vsize (Kb) 84012 [startup+1200.1 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 20384 0 0 0 119843 94 0 0 25 0 1 0 1796971025 83922944 18551 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 20489 18551 145 145 0 20344 0 [pid=21778] vsize: 81956 Current children cumulated CPU time (s) 1199.37 Current children cumulated vsize (Kb) 84080 [startup+1210.1 s] Raw data (loadavg): 0.99 0.97 0.88 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 20395 0 0 0 120842 94 0 0 25 0 1 0 1796971025 83963904 18562 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 20499 18562 145 145 0 20354 0 [pid=21778] vsize: 81996 Current children cumulated CPU time (s) 1209.36 Current children cumulated vsize (Kb) 84120 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.1 s] Raw data (loadavg): 0.99 0.97 0.88 2/57 21778 Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21774/statm): 531 226 485 147 0 384 0 [pid=21774] vsize: 2124 Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 20395 0 0 0 120842 94 0 0 25 0 1 0 1796971025 83963904 18562 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21778/statm): 20499 18562 145 145 0 20354 0 [pid=21778] vsize: 81996 Current children cumulated CPU time (s) 1209.36 Current children cumulated vsize (Kb) 84120 Sending SIGTERM to -21774 Sleeping 2 seconds One traced child (pid=21774) ended because it received signal 15 (SIGTERM) One traced child (pid=21778) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.15 CPU time (s): 1209.42 CPU user time (s): 1208.43 CPU system time (s): 0.98485 CPU usage (%): 99.9396 Max. virtual memory (cumulated for all children) (Kb): 84120
ERROR: no interpretation found !