Name | normalized-opb/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 | 58880896 |
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 | 1.04984 |
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 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc8 THE 2005-05-25 22:55:52 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=22592 boxname=wulflinc8 idbench=1408 idsolver=15 numberseed=0 MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814 /oldhome/oroussel/solvers/minisat+_script MD5SUM BENCH: fd101f0ba1a3813e843a38997ab7ed84 /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-egout.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-egout.opb IDLAUNCH: 22592 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 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: 348756 kB Buffers: 37636 kB Cached: 621896 kB SwapCached: 0 kB Active: 31668 kB Inactive: 634816 kB HighTotal: 131008 kB HighFree: 8512 kB LowTotal: 903652 kB LowFree: 340244 kB SwapTotal: 2097136 kB SwapFree: 2097136 kB Dirty: 28 kB Writeback: 0 kB Mapped: 7068 kB Slab: 13736 kB Committed_AS: 63732 kB PageTables: 320 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-05-25 23:16:21 (client local time) WITH STATUS 152 IN 1229.87 SECONDS stats: 22592 7 1229.87 152 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### 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 % | /oldhome/oroussel/solvers/minisat+_script: line 9: 23181 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@" #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.91 0.98 0.92 2/54 23177 Raw data (stat): 23177 (runsolver) R 23176 3132 3131 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 770858261 1052672 99 4294967295 134512640 135381576 3221224496 3221219704 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0006 s] Raw data (loadavg): 0.93 0.98 0.92 2/55 23181 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+20.001 s] Raw data (loadavg): 0.94 0.98 0.92 2/55 23181 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+30.0009 s] Raw data (loadavg): 0.95 0.98 0.92 2/55 23181 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+40.0005 s] Raw data (loadavg): 0.95 0.98 0.92 2/55 23181 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+50.0013 s] Raw data (loadavg): 0.96 0.98 0.92 2/55 23181 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+60.0012 s] Raw data (loadavg): 0.97 0.98 0.92 2/55 23181 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+70.0022 s] Raw data (loadavg): 0.97 0.98 0.92 2/55 23181 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+80.0026 s] Raw data (loadavg): 0.98 0.98 0.92 2/55 23181 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+90.0024 s] Raw data (loadavg): 0.98 0.98 0.92 2/55 23181 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+100.003 s] Raw data (loadavg): 0.98 0.98 0.92 2/55 23181 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+110.003 s] Raw data (loadavg): 0.98 0.98 0.92 2/55 23181 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+120.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23181 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+130.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23181 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+140.003 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23181 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+150.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23181 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+160.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23181 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+170.005 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23181 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+180.005 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23181 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+190.005 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23181 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+200.006 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23181 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+210.006 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23181 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+220.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23181 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+230.006 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23181 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+240.006 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23181 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+250.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23181 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+260.006 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23234 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+270.008 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23234 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+280.008 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23234 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+290.008 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23234 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+300.008 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23234 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+310.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23234 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+320.008 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23234 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+330.008 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23236 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+340.008 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23236 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+350.008 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23236 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+360.008 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23236 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+370.009 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23236 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+380.01 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23236 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+390.01 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23236 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+400.01 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23236 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+410.01 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23236 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+420.011 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23236 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+430.011 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23236 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+440.01 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23236 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+450.012 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23236 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+460.012 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23236 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+470.013 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23236 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+480.012 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23236 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+490.012 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23236 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+500.012 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23236 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+510.012 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23236 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+520.013 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23236 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+530.012 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23236 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+540.012 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23236 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+550.012 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23236 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+560.012 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23236 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+570.013 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+580.013 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+590.013 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+600.013 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+610.012 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+620.013 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+630.014 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+640.014 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+650.014 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+660.013 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+670.014 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+680.014 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+690.014 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+700.015 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+710.014 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+720.015 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+730.016 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+740.015 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+750.015 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+760.015 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+770.016 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+780.015 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+790.016 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+800.016 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+810.016 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+820.017 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+830.017 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+840.017 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+850.017 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+860.017 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+870.018 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+880.019 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+890.018 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+900.018 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+910.018 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+920.018 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+930.018 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+940.018 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+950.018 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+960.017 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+970.019 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+980.019 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+990.019 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1000.02 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1010.02 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1020.02 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1030.02 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1040.02 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1050.02 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1060.02 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1070.02 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1080.02 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1090.02 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1100.02 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1110.02 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1120.02 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1130.02 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1140.02 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1150.03 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1160.02 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1170.03 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1180.03 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1190.03 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1200.03 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1210.03 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1220.03 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1229.71 s] Raw data (loadavg): 0.99 0.98 0.92 1/53 23238 Raw data (stat): 23177 (minisat+_script) S 23176 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 770858261 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 0 Child status: 152 Real time (s): 1229.71 CPU time (s): 1229.87 CPU user time (s): 1229.29 CPU system time (s): 0.582911 CPU usage (%): 100.013 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####