Name | mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-egout.opb |
MD5SUM | fd101f0ba1a3813e843a38997ab7ed84 |
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 | 1246.13 |
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 wulflinc10 THE 2005-09-20 04:14:30 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3352 boxname=wulflinc10 idbench=1008 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: fd101f0ba1a3813e843a38997ab7ed84 /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-egout.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-egout.opb IDLAUNCH: 3352 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 785220 kB Buffers: 38492 kB Cached: 183640 kB SwapCached: 228 kB Active: 83860 kB Inactive: 141236 kB HighTotal: 131008 kB HighFree: 6160 kB LowTotal: 903652 kB LowFree: 779060 kB SwapTotal: 2097136 kB SwapFree: 2096756 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6280 kB Slab: 18668 kB Committed_AS: 64148 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-20 04:34:40 (client local time) WITH STATUS 10 IN 1209.39 SECONDS stats: 3352 7 1209.39 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/14531/stat): 14531 (minisat+_script) R 14530 14531 22582 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1797383461 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/14531/statm): 174 3 169 147 0 27 0 [pid=14531] 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=14532 New process pid=14533 New process pid=14534 execve syscall for /bin/sed executable One traced child (pid=14533) 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=14534) exited with status: 0 One traced child (pid=14532) exited with status: 0 New process pid=14535 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-egout.opb [startup+10.004 s] Raw data (loadavg): 0.93 0.95 0.90 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 7994 0 0 0 932 32 0 0 25 0 1 0 1797383466 35749888 7665 4294967295 134512640 135094434 3221224432 3221223064 134557561 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14535/statm): 8728 7665 145 145 0 8583 0 [pid=14535] vsize: 34912 Current children cumulated CPU time (s) 9.66 Current children cumulated vsize (Kb) 37036 [startup+20.0046 s] Raw data (loadavg): 0.94 0.96 0.91 1/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) T 14531 14531 22582 0 -1 0 8301 0 0 0 1930 33 0 0 25 0 1 0 1797383466 36872192 7972 4294967295 134512640 135094434 3221224432 3221219788 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/14535/statm): 9002 7972 145 145 0 8857 0 [pid=14535] vsize: 36008 Current children cumulated CPU time (s) 19.65 Current children cumulated vsize (Kb) 38132 [startup+30.0052 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 16568 0 0 0 2862 69 0 0 25 0 1 0 1797383466 73404416 15909 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14535/statm): 17921 15909 145 145 0 17776 0 [pid=14535] vsize: 71684 Current children cumulated CPU time (s) 29.33 Current children cumulated vsize (Kb) 73808 [startup+40.0057 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 16653 0 0 0 3861 69 0 0 25 0 1 0 1797383466 73613312 15994 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 17972 15994 145 145 0 17827 0 [pid=14535] vsize: 71888 Current children cumulated CPU time (s) 39.32 Current children cumulated vsize (Kb) 74012 [startup+50.0062 s] Raw data (loadavg): 0.96 0.96 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 16815 0 0 0 4860 70 0 0 25 0 1 0 1797383466 73949184 16156 4294967295 134512640 135094434 3221224432 3221223092 134553519 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 18054 16156 145 145 0 17909 0 [pid=14535] vsize: 72216 Current children cumulated CPU time (s) 49.32 Current children cumulated vsize (Kb) 74340 [startup+60.0068 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 16905 0 0 0 5860 70 0 0 25 0 1 0 1797383466 73969664 16168 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14535/statm): 18059 16168 145 145 0 17914 0 [pid=14535] vsize: 72236 Current children cumulated CPU time (s) 59.32 Current children cumulated vsize (Kb) 74360 [startup+70.0074 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 16918 0 0 0 6858 71 0 0 25 0 1 0 1797383466 74018816 16181 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 18071 16181 145 145 0 17926 0 [pid=14535] vsize: 72284 Current children cumulated CPU time (s) 69.31 Current children cumulated vsize (Kb) 74408 [startup+80.0079 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 16941 0 0 0 7858 71 0 0 25 0 1 0 1797383466 74113024 16204 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 18094 16204 145 145 0 17949 0 [pid=14535] vsize: 72376 Current children cumulated CPU time (s) 79.31 Current children cumulated vsize (Kb) 74500 [startup+90.0085 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 16979 0 0 0 8858 71 0 0 25 0 1 0 1797383466 74268672 16242 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 18132 16242 145 145 0 17987 0 [pid=14535] vsize: 72528 Current children cumulated CPU time (s) 89.31 Current children cumulated vsize (Kb) 74652 [startup+100.009 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17078 0 0 0 9857 72 0 0 25 0 1 0 1797383466 74522624 16305 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 18194 16305 145 145 0 18049 0 [pid=14535] vsize: 72776 Current children cumulated CPU time (s) 99.31 Current children cumulated vsize (Kb) 74900 [startup+110.01 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17139 0 0 0 10857 72 0 0 25 0 1 0 1797383466 74477568 16294 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 18183 16294 145 145 0 18038 0 [pid=14535] vsize: 72732 Current children cumulated CPU time (s) 109.31 Current children cumulated vsize (Kb) 74856 [startup+120.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17200 0 0 0 11856 72 0 0 25 0 1 0 1797383466 74567680 16316 4294967295 134512640 135094434 3221224432 3221222160 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 18205 16316 145 145 0 18060 0 [pid=14535] vsize: 72820 Current children cumulated CPU time (s) 119.3 Current children cumulated vsize (Kb) 74944 [startup+130.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17236 0 0 0 12856 72 0 0 25 0 1 0 1797383466 74559488 16315 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 18203 16315 145 145 0 18058 0 [pid=14535] vsize: 72812 Current children cumulated CPU time (s) 129.3 Current children cumulated vsize (Kb) 74936 [startup+140.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17278 0 0 0 13856 73 0 0 25 0 1 0 1797383466 74760192 16357 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 18252 16357 145 145 0 18107 0 [pid=14535] vsize: 73008 Current children cumulated CPU time (s) 139.31 Current children cumulated vsize (Kb) 75132 [startup+150.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17395 0 0 0 14855 74 0 0 25 0 1 0 1797383466 75280384 16474 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 18379 16474 145 145 0 18234 0 [pid=14535] vsize: 73516 Current children cumulated CPU time (s) 149.31 Current children cumulated vsize (Kb) 75640 [startup+160.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17410 0 0 0 15854 74 0 0 25 0 1 0 1797383466 75337728 16489 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 18393 16489 145 145 0 18248 0 [pid=14535] vsize: 73572 Current children cumulated CPU time (s) 159.3 Current children cumulated vsize (Kb) 75696 [startup+170.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17447 0 0 0 16854 74 0 0 25 0 1 0 1797383466 75489280 16526 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 18430 16526 145 145 0 18285 0 [pid=14535] vsize: 73720 Current children cumulated CPU time (s) 169.3 Current children cumulated vsize (Kb) 75844 [startup+180.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17456 0 0 0 17855 74 0 0 25 0 1 0 1797383466 75526144 16535 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 18439 16535 145 145 0 18294 0 [pid=14535] vsize: 73756 Current children cumulated CPU time (s) 179.31 Current children cumulated vsize (Kb) 75880 [startup+190.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17465 0 0 0 18855 74 0 0 25 0 1 0 1797383466 75558912 16544 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 18447 16544 145 145 0 18302 0 [pid=14535] vsize: 73788 Current children cumulated CPU time (s) 189.31 Current children cumulated vsize (Kb) 75912 [startup+200.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17474 0 0 0 19855 74 0 0 25 0 1 0 1797383466 75595776 16553 4294967295 134512640 135094434 3221224432 3221223056 134557568 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 18456 16553 145 145 0 18311 0 [pid=14535] vsize: 73824 Current children cumulated CPU time (s) 199.31 Current children cumulated vsize (Kb) 75948 [startup+210.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17505 0 0 0 20855 74 0 0 25 0 1 0 1797383466 75735040 16584 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 18490 16584 145 145 0 18345 0 [pid=14535] vsize: 73960 Current children cumulated CPU time (s) 209.31 Current children cumulated vsize (Kb) 76084 [startup+220.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17587 0 0 0 21855 74 0 0 25 0 1 0 1797383466 76107776 16666 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 18581 16666 145 145 0 18436 0 [pid=14535] vsize: 74324 Current children cumulated CPU time (s) 219.31 Current children cumulated vsize (Kb) 76448 [startup+230.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17588 0 0 0 22855 74 0 0 25 0 1 0 1797383466 76107776 16667 4294967295 134512640 135094434 3221224432 3221223084 134675711 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 18581 16667 145 145 0 18436 0 [pid=14535] vsize: 74324 Current children cumulated CPU time (s) 229.31 Current children cumulated vsize (Kb) 76448 [startup+240.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17588 0 0 0 23855 74 0 0 25 0 1 0 1797383466 76107776 16667 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 18581 16667 145 145 0 18436 0 [pid=14535] vsize: 74324 Current children cumulated CPU time (s) 239.31 Current children cumulated vsize (Kb) 76448 [startup+250.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17653 0 0 0 24855 75 0 0 25 0 1 0 1797383466 76070912 16657 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 18572 16657 145 145 0 18427 0 [pid=14535] vsize: 74288 Current children cumulated CPU time (s) 249.32 Current children cumulated vsize (Kb) 76412 [startup+260.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17667 0 0 0 25855 75 0 0 25 0 1 0 1797383466 76120064 16671 4294967295 134512640 135094434 3221224432 3221222976 134562057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 18584 16671 145 145 0 18439 0 [pid=14535] vsize: 74336 Current children cumulated CPU time (s) 259.32 Current children cumulated vsize (Kb) 76460 [startup+270.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17678 0 0 0 26854 75 0 0 25 0 1 0 1797383466 76165120 16682 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 18595 16682 145 145 0 18450 0 [pid=14535] vsize: 74380 Current children cumulated CPU time (s) 269.31 Current children cumulated vsize (Kb) 76504 [startup+280.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17715 0 0 0 27854 75 0 0 25 0 1 0 1797383466 76316672 16719 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 18632 16719 145 145 0 18487 0 [pid=14535] vsize: 74528 Current children cumulated CPU time (s) 279.31 Current children cumulated vsize (Kb) 76652 [startup+290.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17827 0 0 0 28854 76 0 0 25 0 1 0 1797383466 76611584 16792 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 18704 16792 145 145 0 18559 0 [pid=14535] vsize: 74816 Current children cumulated CPU time (s) 289.32 Current children cumulated vsize (Kb) 76940 [startup+300.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17904 0 0 0 29853 76 0 0 25 0 1 0 1797383466 76619776 16794 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 18706 16794 145 145 0 18561 0 [pid=14535] vsize: 74824 Current children cumulated CPU time (s) 299.31 Current children cumulated vsize (Kb) 76948 [startup+310.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17933 0 0 0 30853 76 0 0 25 0 1 0 1797383466 76738560 16823 4294967295 134512640 135094434 3221224432 3221223024 134557196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 18735 16823 145 145 0 18590 0 [pid=14535] vsize: 74940 Current children cumulated CPU time (s) 309.31 Current children cumulated vsize (Kb) 77064 [startup+320.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17953 0 0 0 31854 76 0 0 25 0 1 0 1797383466 76816384 16843 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 18754 16843 145 145 0 18609 0 [pid=14535] vsize: 75016 Current children cumulated CPU time (s) 319.32 Current children cumulated vsize (Kb) 77140 [startup+330.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18037 0 0 0 32852 77 0 0 25 0 1 0 1797383466 77217792 16927 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 18852 16927 145 145 0 18707 0 [pid=14535] vsize: 75408 Current children cumulated CPU time (s) 329.31 Current children cumulated vsize (Kb) 77532 [startup+340.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18086 0 0 0 33852 77 0 0 25 0 1 0 1797383466 77414400 16976 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 18900 16976 145 145 0 18755 0 [pid=14535] vsize: 75600 Current children cumulated CPU time (s) 339.31 Current children cumulated vsize (Kb) 77724 [startup+350.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18099 0 0 0 34852 77 0 0 25 0 1 0 1797383466 77467648 16989 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 18913 16989 145 145 0 18768 0 [pid=14535] vsize: 75652 Current children cumulated CPU time (s) 349.31 Current children cumulated vsize (Kb) 77776 [startup+360.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18187 0 0 0 35852 78 0 0 25 0 1 0 1797383466 77529088 17001 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 18928 17001 145 145 0 18783 0 [pid=14535] vsize: 75712 Current children cumulated CPU time (s) 359.32 Current children cumulated vsize (Kb) 77836 [startup+370.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18200 0 0 0 36851 78 0 0 25 0 1 0 1797383466 77565952 17014 4294967295 134512640 135094434 3221224432 3221223088 134557984 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 18937 17014 145 145 0 18792 0 [pid=14535] vsize: 75748 Current children cumulated CPU time (s) 369.31 Current children cumulated vsize (Kb) 77872 [startup+380.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18215 0 0 0 37852 78 0 0 25 0 1 0 1797383466 77627392 17029 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 18952 17029 145 145 0 18807 0 [pid=14535] vsize: 75808 Current children cumulated CPU time (s) 379.32 Current children cumulated vsize (Kb) 77932 [startup+390.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18233 0 0 0 38851 78 0 0 25 0 1 0 1797383466 77701120 17047 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 18970 17047 145 145 0 18825 0 [pid=14535] vsize: 75880 Current children cumulated CPU time (s) 389.31 Current children cumulated vsize (Kb) 78004 [startup+400.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18243 0 0 0 39851 78 0 0 25 0 1 0 1797383466 77742080 17057 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 18980 17057 145 145 0 18835 0 [pid=14535] vsize: 75920 Current children cumulated CPU time (s) 399.31 Current children cumulated vsize (Kb) 78044 [startup+410.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18276 0 0 0 40851 78 0 0 25 0 1 0 1797383466 77873152 17090 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19012 17090 145 145 0 18867 0 [pid=14535] vsize: 76048 Current children cumulated CPU time (s) 409.31 Current children cumulated vsize (Kb) 78172 [startup+420.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18362 0 0 0 41850 79 0 0 25 0 1 0 1797383466 78065664 17137 4294967295 134512640 135094434 3221224432 3221220752 134677310 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19059 17137 145 145 0 18914 0 [pid=14535] vsize: 76236 Current children cumulated CPU time (s) 419.31 Current children cumulated vsize (Kb) 78360 [startup+430.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18397 0 0 0 42850 79 0 0 25 0 1 0 1797383466 78053376 17134 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19056 17134 145 145 0 18911 0 [pid=14535] vsize: 76224 Current children cumulated CPU time (s) 429.31 Current children cumulated vsize (Kb) 78348 [startup+440.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18488 0 0 0 43850 79 0 0 25 0 1 0 1797383466 78114816 17149 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19071 17149 145 145 0 18926 0 [pid=14535] vsize: 76284 Current children cumulated CPU time (s) 439.31 Current children cumulated vsize (Kb) 78408 [startup+450.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18508 0 0 0 44849 80 0 0 25 0 1 0 1797383466 78196736 17169 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19091 17169 145 145 0 18946 0 [pid=14535] vsize: 76364 Current children cumulated CPU time (s) 449.31 Current children cumulated vsize (Kb) 78488 [startup+460.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18535 0 0 0 45850 80 0 0 25 0 1 0 1797383466 78303232 17196 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19117 17196 145 145 0 18972 0 [pid=14535] vsize: 76468 Current children cumulated CPU time (s) 459.32 Current children cumulated vsize (Kb) 78592 [startup+470.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18554 0 0 0 46850 80 0 0 25 0 1 0 1797383466 78376960 17215 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19135 17215 145 145 0 18990 0 [pid=14535] vsize: 76540 Current children cumulated CPU time (s) 469.32 Current children cumulated vsize (Kb) 78664 [startup+480.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18568 0 0 0 47850 80 0 0 25 0 1 0 1797383466 78434304 17229 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19149 17229 145 145 0 19004 0 [pid=14535] vsize: 76596 Current children cumulated CPU time (s) 479.32 Current children cumulated vsize (Kb) 78720 [startup+490.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18583 0 0 0 48849 80 0 0 25 0 1 0 1797383466 78495744 17244 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19164 17244 145 145 0 19019 0 [pid=14535] vsize: 76656 Current children cumulated CPU time (s) 489.31 Current children cumulated vsize (Kb) 78780 [startup+500.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18609 0 0 0 49850 80 0 0 25 0 1 0 1797383466 78602240 17270 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19190 17270 145 145 0 19045 0 [pid=14535] vsize: 76760 Current children cumulated CPU time (s) 499.32 Current children cumulated vsize (Kb) 78884 [startup+510.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18702 0 0 0 50849 81 0 0 25 0 1 0 1797383466 78823424 17324 4294967295 134512640 135094434 3221224432 3221221456 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19244 17324 145 145 0 19099 0 [pid=14535] vsize: 76976 Current children cumulated CPU time (s) 509.32 Current children cumulated vsize (Kb) 79100 [startup+520.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18865 0 0 0 51848 81 0 0 25 0 1 0 1797383466 78868480 17336 4294967295 134512640 135094434 3221224432 3221221516 134677228 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19255 17336 145 145 0 19110 0 [pid=14535] vsize: 77020 Current children cumulated CPU time (s) 519.31 Current children cumulated vsize (Kb) 79144 [startup+530.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18898 0 0 0 52848 81 0 0 25 0 1 0 1797383466 78856192 17333 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19252 17333 145 145 0 19107 0 [pid=14535] vsize: 77008 Current children cumulated CPU time (s) 529.31 Current children cumulated vsize (Kb) 79132 [startup+540.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18926 0 0 0 53848 82 0 0 25 0 1 0 1797383466 78970880 17361 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19280 17361 145 145 0 19135 0 [pid=14535] vsize: 77120 Current children cumulated CPU time (s) 539.32 Current children cumulated vsize (Kb) 79244 [startup+550.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18949 0 0 0 54848 82 0 0 25 0 1 0 1797383466 79065088 17384 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19303 17384 145 145 0 19158 0 [pid=14535] vsize: 77212 Current children cumulated CPU time (s) 549.32 Current children cumulated vsize (Kb) 79336 [startup+560.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18965 0 0 0 55848 82 0 0 25 0 1 0 1797383466 79126528 17400 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19318 17400 145 145 0 19173 0 [pid=14535] vsize: 77272 Current children cumulated CPU time (s) 559.32 Current children cumulated vsize (Kb) 79396 [startup+570.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18982 0 0 0 56847 82 0 0 25 0 1 0 1797383466 79196160 17417 4294967295 134512640 135094434 3221224432 3221223088 134558398 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19335 17417 145 145 0 19190 0 [pid=14535] vsize: 77340 Current children cumulated CPU time (s) 569.31 Current children cumulated vsize (Kb) 79464 [startup+580.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19006 0 0 0 57847 82 0 0 25 0 1 0 1797383466 79294464 17441 4294967295 134512640 135094434 3221224432 3221223024 134556993 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19359 17441 145 145 0 19214 0 [pid=14535] vsize: 77436 Current children cumulated CPU time (s) 579.31 Current children cumulated vsize (Kb) 79560 [startup+590.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19032 0 0 0 58847 82 0 0 25 0 1 0 1797383466 79396864 17467 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19384 17467 145 145 0 19239 0 [pid=14535] vsize: 77536 Current children cumulated CPU time (s) 589.31 Current children cumulated vsize (Kb) 79660 [startup+600.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19101 0 0 0 59847 83 0 0 25 0 1 0 1797383466 79515648 17496 4294967295 134512640 135094434 3221224432 3221222224 134677091 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19413 17496 145 145 0 19268 0 [pid=14535] vsize: 77652 Current children cumulated CPU time (s) 599.32 Current children cumulated vsize (Kb) 79776 [startup+610.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19146 0 0 0 60846 83 0 0 25 0 1 0 1797383466 79548416 17505 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19421 17505 145 145 0 19276 0 [pid=14535] vsize: 77684 Current children cumulated CPU time (s) 609.31 Current children cumulated vsize (Kb) 79808 [startup+620.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19157 0 0 0 61846 83 0 0 25 0 1 0 1797383466 79585280 17516 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19430 17516 145 145 0 19285 0 [pid=14535] vsize: 77720 Current children cumulated CPU time (s) 619.31 Current children cumulated vsize (Kb) 79844 [startup+630.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19181 0 0 0 62846 84 0 0 25 0 1 0 1797383466 79683584 17540 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19454 17540 145 145 0 19309 0 [pid=14535] vsize: 77816 Current children cumulated CPU time (s) 629.32 Current children cumulated vsize (Kb) 79940 [startup+640.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19195 0 0 0 63846 84 0 0 25 0 1 0 1797383466 79745024 17554 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19469 17554 145 145 0 19324 0 [pid=14535] vsize: 77876 Current children cumulated CPU time (s) 639.32 Current children cumulated vsize (Kb) 80000 [startup+650.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19280 0 0 0 64845 84 0 0 25 0 1 0 1797383466 79773696 17562 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19476 17562 145 145 0 19331 0 [pid=14535] vsize: 77904 Current children cumulated CPU time (s) 649.31 Current children cumulated vsize (Kb) 80028 [startup+660.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19291 0 0 0 65845 84 0 0 25 0 1 0 1797383466 79814656 17573 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19486 17573 145 145 0 19341 0 [pid=14535] vsize: 77944 Current children cumulated CPU time (s) 659.31 Current children cumulated vsize (Kb) 80068 [startup+670.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19307 0 0 0 66845 85 0 0 25 0 1 0 1797383466 79880192 17589 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19502 17589 145 145 0 19357 0 [pid=14535] vsize: 78008 Current children cumulated CPU time (s) 669.32 Current children cumulated vsize (Kb) 80132 [startup+680.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19320 0 0 0 67845 85 0 0 25 0 1 0 1797383466 79933440 17602 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19515 17602 145 145 0 19370 0 [pid=14535] vsize: 78060 Current children cumulated CPU time (s) 679.32 Current children cumulated vsize (Kb) 80184 [startup+690.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19333 0 0 0 68844 85 0 0 25 0 1 0 1797383466 79986688 17615 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19528 17615 145 145 0 19383 0 [pid=14535] vsize: 78112 Current children cumulated CPU time (s) 689.31 Current children cumulated vsize (Kb) 80236 [startup+700.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19365 0 0 0 69844 85 0 0 25 0 1 0 1797383466 80121856 17647 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19561 17647 145 145 0 19416 0 [pid=14535] vsize: 78244 Current children cumulated CPU time (s) 699.31 Current children cumulated vsize (Kb) 80368 [startup+710.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19399 0 0 0 70844 85 0 0 25 0 1 0 1797383466 80257024 17681 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19594 17681 145 145 0 19449 0 [pid=14535] vsize: 78376 Current children cumulated CPU time (s) 709.31 Current children cumulated vsize (Kb) 80500 [startup+720.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19408 0 0 0 71844 85 0 0 25 0 1 0 1797383466 80289792 17690 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19602 17690 145 145 0 19457 0 [pid=14535] vsize: 78408 Current children cumulated CPU time (s) 719.31 Current children cumulated vsize (Kb) 80532 [startup+730.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19414 0 0 0 72845 85 0 0 25 0 1 0 1797383466 80314368 17696 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19608 17696 145 145 0 19463 0 [pid=14535] vsize: 78432 Current children cumulated CPU time (s) 729.32 Current children cumulated vsize (Kb) 80556 [startup+740.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19414 0 0 0 73845 85 0 0 25 0 1 0 1797383466 80314368 17696 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19608 17696 145 145 0 19463 0 [pid=14535] vsize: 78432 Current children cumulated CPU time (s) 739.32 Current children cumulated vsize (Kb) 80556 [startup+750.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19431 0 0 0 74845 85 0 0 25 0 1 0 1797383466 80384000 17713 4294967295 134512640 135094434 3221224432 3221223120 134554742 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19625 17713 145 145 0 19480 0 [pid=14535] vsize: 78500 Current children cumulated CPU time (s) 749.32 Current children cumulated vsize (Kb) 80624 [startup+760.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19521 0 0 0 75845 85 0 0 25 0 1 0 1797383466 80441344 17727 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19639 17727 145 145 0 19494 0 [pid=14535] vsize: 78556 Current children cumulated CPU time (s) 759.32 Current children cumulated vsize (Kb) 80680 [startup+770.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19542 0 0 0 76845 86 0 0 25 0 1 0 1797383466 80527360 17748 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19660 17748 145 145 0 19515 0 [pid=14535] vsize: 78640 Current children cumulated CPU time (s) 769.33 Current children cumulated vsize (Kb) 80764 [startup+780.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19553 0 0 0 77845 86 0 0 25 0 1 0 1797383466 80572416 17759 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19671 17759 145 145 0 19526 0 [pid=14535] vsize: 78684 Current children cumulated CPU time (s) 779.33 Current children cumulated vsize (Kb) 80808 [startup+790.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19565 0 0 0 78845 86 0 0 25 0 1 0 1797383466 80617472 17771 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19682 17771 145 145 0 19537 0 [pid=14535] vsize: 78728 Current children cumulated CPU time (s) 789.33 Current children cumulated vsize (Kb) 80852 [startup+800.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19583 0 0 0 79845 86 0 0 25 0 1 0 1797383466 80695296 17789 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19701 17789 145 145 0 19556 0 [pid=14535] vsize: 78804 Current children cumulated CPU time (s) 799.33 Current children cumulated vsize (Kb) 80928 [startup+810.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19597 0 0 0 80845 86 0 0 25 0 1 0 1797383466 80748544 17803 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19714 17803 145 145 0 19569 0 [pid=14535] vsize: 78856 Current children cumulated CPU time (s) 809.33 Current children cumulated vsize (Kb) 80980 [startup+820.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19614 0 0 0 81845 86 0 0 25 0 1 0 1797383466 80814080 17820 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19730 17820 145 145 0 19585 0 [pid=14535] vsize: 78920 Current children cumulated CPU time (s) 819.33 Current children cumulated vsize (Kb) 81044 [startup+830.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19634 0 0 0 82845 86 0 0 25 0 1 0 1797383466 80896000 17840 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19750 17840 145 145 0 19605 0 [pid=14535] vsize: 79000 Current children cumulated CPU time (s) 829.33 Current children cumulated vsize (Kb) 81124 [startup+840.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19652 0 0 0 83845 86 0 0 25 0 1 0 1797383466 80969728 17858 4294967295 134512640 135094434 3221224432 3221223024 134556961 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19768 17858 145 145 0 19623 0 [pid=14535] vsize: 79072 Current children cumulated CPU time (s) 839.33 Current children cumulated vsize (Kb) 81196 [startup+850.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19666 0 0 0 84845 86 0 0 25 0 1 0 1797383466 81027072 17872 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19782 17872 145 145 0 19637 0 [pid=14535] vsize: 79128 Current children cumulated CPU time (s) 849.33 Current children cumulated vsize (Kb) 81252 [startup+860.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19684 0 0 0 85844 86 0 0 25 0 1 0 1797383466 81096704 17890 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19799 17890 145 145 0 19654 0 [pid=14535] vsize: 79196 Current children cumulated CPU time (s) 859.32 Current children cumulated vsize (Kb) 81320 [startup+870.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19693 0 0 0 86844 87 0 0 25 0 1 0 1797383466 81133568 17899 4294967295 134512640 135094434 3221224432 3221223056 134562139 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19808 17899 145 145 0 19663 0 [pid=14535] vsize: 79232 Current children cumulated CPU time (s) 869.33 Current children cumulated vsize (Kb) 81356 [startup+880.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19708 0 0 0 87844 87 0 0 25 0 1 0 1797383466 81195008 17914 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19823 17914 145 145 0 19678 0 [pid=14535] vsize: 79292 Current children cumulated CPU time (s) 879.33 Current children cumulated vsize (Kb) 81416 [startup+890.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19723 0 0 0 88844 87 0 0 25 0 1 0 1797383466 81256448 17929 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19838 17929 145 145 0 19693 0 [pid=14535] vsize: 79352 Current children cumulated CPU time (s) 889.33 Current children cumulated vsize (Kb) 81476 [startup+900.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19761 0 0 0 89844 87 0 0 25 0 1 0 1797383466 81543168 17967 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19908 17967 145 145 0 19763 0 [pid=14535] vsize: 79632 Current children cumulated CPU time (s) 899.33 Current children cumulated vsize (Kb) 81756 [startup+910.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19817 0 0 0 90844 87 0 0 25 0 1 0 1797383466 81608704 17984 4294967295 134512640 135094434 3221224432 3221223024 134556864 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19924 17984 145 145 0 19779 0 [pid=14535] vsize: 79696 Current children cumulated CPU time (s) 909.33 Current children cumulated vsize (Kb) 81820 [startup+920.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19817 0 0 0 91844 87 0 0 25 0 1 0 1797383466 81608704 17984 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19924 17984 145 145 0 19779 0 [pid=14535] vsize: 79696 Current children cumulated CPU time (s) 919.33 Current children cumulated vsize (Kb) 81820 [startup+930.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19830 0 0 0 92844 87 0 0 25 0 1 0 1797383466 81666048 17997 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19938 17997 145 145 0 19793 0 [pid=14535] vsize: 79752 Current children cumulated CPU time (s) 929.33 Current children cumulated vsize (Kb) 81876 [startup+940.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19848 0 0 0 93844 87 0 0 25 0 1 0 1797383466 81739776 18015 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19956 18015 145 145 0 19811 0 [pid=14535] vsize: 79824 Current children cumulated CPU time (s) 939.33 Current children cumulated vsize (Kb) 81948 [startup+950.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19864 0 0 0 94844 88 0 0 25 0 1 0 1797383466 81801216 18031 4294967295 134512640 135094434 3221224432 3221223076 134558261 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19971 18031 145 145 0 19826 0 [pid=14535] vsize: 79884 Current children cumulated CPU time (s) 949.34 Current children cumulated vsize (Kb) 82008 [startup+960.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19884 0 0 0 95844 88 0 0 25 0 1 0 1797383466 81883136 18051 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 19991 18051 145 145 0 19846 0 [pid=14535] vsize: 79964 Current children cumulated CPU time (s) 959.34 Current children cumulated vsize (Kb) 82088 [startup+970.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19908 0 0 0 96844 88 0 0 25 0 1 0 1797383466 81985536 18075 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 20016 18075 145 145 0 19871 0 [pid=14535] vsize: 80064 Current children cumulated CPU time (s) 969.34 Current children cumulated vsize (Kb) 82188 [startup+980.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19922 0 0 0 97844 88 0 0 25 0 1 0 1797383466 82034688 18089 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 20028 18089 145 145 0 19883 0 [pid=14535] vsize: 80112 Current children cumulated CPU time (s) 979.34 Current children cumulated vsize (Kb) 82236 [startup+990.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19937 0 0 0 98845 88 0 0 25 0 1 0 1797383466 82092032 18104 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 20042 18104 145 145 0 19897 0 [pid=14535] vsize: 80168 Current children cumulated CPU time (s) 989.35 Current children cumulated vsize (Kb) 82292 [startup+1000.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19959 0 0 0 99845 88 0 0 25 0 1 0 1797383466 82186240 18126 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 20065 18126 145 145 0 19920 0 [pid=14535] vsize: 80260 Current children cumulated CPU time (s) 999.35 Current children cumulated vsize (Kb) 82384 [startup+1010.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19971 0 0 0 100845 88 0 0 25 0 1 0 1797383466 82231296 18138 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 20076 18138 145 145 0 19931 0 [pid=14535] vsize: 80304 Current children cumulated CPU time (s) 1009.35 Current children cumulated vsize (Kb) 82428 [startup+1020.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19989 0 0 0 101845 88 0 0 25 0 1 0 1797383466 82305024 18156 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 20094 18156 145 145 0 19949 0 [pid=14535] vsize: 80376 Current children cumulated CPU time (s) 1019.35 Current children cumulated vsize (Kb) 82500 [startup+1030.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) T 14531 14531 22582 0 -1 0 20008 0 0 0 102845 88 0 0 25 0 1 0 1797383466 82391040 18175 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/14535/statm): 20115 18175 145 145 0 19970 0 [pid=14535] vsize: 80460 Current children cumulated CPU time (s) 1029.35 Current children cumulated vsize (Kb) 82584 [startup+1040.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 20034 0 0 0 103845 88 0 0 25 0 1 0 1797383466 82497536 18201 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 20141 18201 145 145 0 19996 0 [pid=14535] vsize: 80564 Current children cumulated CPU time (s) 1039.35 Current children cumulated vsize (Kb) 82688 [startup+1050.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 20113 0 0 0 104844 89 0 0 25 0 1 0 1797383466 82825216 18280 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 20221 18280 145 145 0 20076 0 [pid=14535] vsize: 80884 Current children cumulated CPU time (s) 1049.35 Current children cumulated vsize (Kb) 83008 [startup+1060.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 20141 0 0 0 105844 89 0 0 25 0 1 0 1797383466 82927616 18308 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 20246 18308 145 145 0 20101 0 [pid=14535] vsize: 80984 Current children cumulated CPU time (s) 1059.35 Current children cumulated vsize (Kb) 83108 [startup+1070.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 20161 0 0 0 106844 89 0 0 25 0 1 0 1797383466 83009536 18328 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 20266 18328 145 145 0 20121 0 [pid=14535] vsize: 81064 Current children cumulated CPU time (s) 1069.35 Current children cumulated vsize (Kb) 83188 [startup+1080.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 20192 0 0 0 107844 89 0 0 25 0 1 0 1797383466 83136512 18359 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 20297 18359 145 145 0 20152 0 [pid=14535] vsize: 81188 Current children cumulated CPU time (s) 1079.35 Current children cumulated vsize (Kb) 83312 [startup+1090.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 20210 0 0 0 108843 89 0 0 25 0 1 0 1797383466 83206144 18377 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 20314 18377 145 145 0 20169 0 [pid=14535] vsize: 81256 Current children cumulated CPU time (s) 1089.34 Current children cumulated vsize (Kb) 83380 [startup+1100.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 20236 0 0 0 109843 90 0 0 25 0 1 0 1797383466 83312640 18403 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 20340 18403 145 145 0 20195 0 [pid=14535] vsize: 81360 Current children cumulated CPU time (s) 1099.35 Current children cumulated vsize (Kb) 83484 [startup+1110.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 20253 0 0 0 110843 90 0 0 25 0 1 0 1797383466 83382272 18420 4294967295 134512640 135094434 3221224432 3221223024 134557372 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 20357 18420 145 145 0 20212 0 [pid=14535] vsize: 81428 Current children cumulated CPU time (s) 1109.35 Current children cumulated vsize (Kb) 83552 [startup+1120.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 20275 0 0 0 111843 90 0 0 25 0 1 0 1797383466 83476480 18442 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 20380 18442 145 145 0 20235 0 [pid=14535] vsize: 81520 Current children cumulated CPU time (s) 1119.35 Current children cumulated vsize (Kb) 83644 [startup+1130.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 20289 0 0 0 112843 90 0 0 25 0 1 0 1797383466 83537920 18456 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 20395 18456 145 145 0 20250 0 [pid=14535] vsize: 81580 Current children cumulated CPU time (s) 1129.35 Current children cumulated vsize (Kb) 83704 [startup+1140.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 20312 0 0 0 113843 90 0 0 25 0 1 0 1797383466 83632128 18479 4294967295 134512640 135094434 3221224432 3221223068 134557639 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 20418 18479 145 145 0 20273 0 [pid=14535] vsize: 81672 Current children cumulated CPU time (s) 1139.35 Current children cumulated vsize (Kb) 83796 [startup+1150.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 20330 0 0 0 114843 90 0 0 25 0 1 0 1797383466 83701760 18497 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 20435 18497 145 145 0 20290 0 [pid=14535] vsize: 81740 Current children cumulated CPU time (s) 1149.35 Current children cumulated vsize (Kb) 83864 [startup+1160.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 20351 0 0 0 115844 90 0 0 25 0 1 0 1797383466 83787776 18518 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 20456 18518 145 145 0 20311 0 [pid=14535] vsize: 81824 Current children cumulated CPU time (s) 1159.36 Current children cumulated vsize (Kb) 83948 [startup+1170.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 20366 0 0 0 116843 90 0 0 25 0 1 0 1797383466 83853312 18533 4294967295 134512640 135094434 3221224432 3221223088 134558281 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 20472 18533 145 145 0 20327 0 [pid=14535] vsize: 81888 Current children cumulated CPU time (s) 1169.35 Current children cumulated vsize (Kb) 84012 [startup+1180.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 20372 0 0 0 117844 90 0 0 25 0 1 0 1797383466 83873792 18539 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 20477 18539 145 145 0 20332 0 [pid=14535] vsize: 81908 Current children cumulated CPU time (s) 1179.36 Current children cumulated vsize (Kb) 84032 [startup+1190.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 20387 0 0 0 118844 91 0 0 25 0 1 0 1797383466 83931136 18554 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 20491 18554 145 145 0 20346 0 [pid=14535] vsize: 81964 Current children cumulated CPU time (s) 1189.37 Current children cumulated vsize (Kb) 84088 [startup+1200.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 20401 0 0 0 119843 91 0 0 25 0 1 0 1797383466 83988480 18568 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 20505 18568 145 145 0 20360 0 [pid=14535] vsize: 82020 Current children cumulated CPU time (s) 1199.36 Current children cumulated vsize (Kb) 84144 [startup+1210.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 20414 0 0 0 120844 91 0 0 25 0 1 0 1797383466 84054016 18581 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 20521 18581 145 145 0 20376 0 [pid=14535] vsize: 82084 Current children cumulated CPU time (s) 1209.37 Current children cumulated vsize (Kb) 84208 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14535 Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14531/statm): 531 226 485 147 0 384 0 [pid=14531] vsize: 2124 Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 20414 0 0 0 120844 91 0 0 25 0 1 0 1797383466 84054016 18581 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14535/statm): 20521 18581 145 145 0 20376 0 [pid=14535] vsize: 82084 Current children cumulated CPU time (s) 1209.37 Current children cumulated vsize (Kb) 84208 Sending SIGTERM to -14531 Sleeping 2 seconds One traced child (pid=14531) ended because it received signal 15 (SIGTERM) One traced child (pid=14535) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.11 CPU time (s): 1209.39 CPU user time (s): 1208.44 CPU system time (s): 0.948855 CPU usage (%): 99.9405 Max. virtual memory (cumulated for all children) (Kb): 84208
ERROR: no interpretation found !