Name | submitted/een/normalized-lseu.opb |
MD5SUM | a578bf261896413ca78de4dc6db2447f |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 1120 |
Optimality of the best value was proved | YES |
Number of terms in the objective function | 85 |
Biggest coefficient in the objective function | 517 |
Number of bits for the biggest coefficient in the objective function | 10 |
Sum of the numbers in the objective function | 15494 |
Number of bits of the sum of numbers in the objective function | 14 |
Biggest number in a constraint | 1656 |
Number of bits of the biggest number in a constraint | 11 |
Biggest sum of numbers in a constraint | 15494 |
Number of bits of the biggest sum of numbers | 14 |
Best result obtained on this benchmark | OPTIMUM FOUND |
Best CPU time to get the best result obtained on this benchmark | 526.298 |
Number of variables | 89 |
Total number of constraints | 28 |
Number of constraints which are clauses | 2 |
Number of constraints which are cardinality constraints (but not clauses) | 15 |
Number of constraints which are nor clauses,nor cardinality constraints | 11 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 47 |
LAUNCH ON wulflinc27 THE 2005-09-18 18:19:16 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2616 boxname=wulflinc27 idbench=272 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: a578bf261896413ca78de4dc6db2447f /oldhome/oroussel/tmp/wulflinc27/normalized-lseu.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc27/normalized-lseu.opb IDLAUNCH: 2616 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.169 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 : 3 cpu MHz : 451.169 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: 911464 kB Buffers: 35976 kB Cached: 55264 kB SwapCached: 764 kB Active: 66848 kB Inactive: 26984 kB HighTotal: 131008 kB HighFree: 73164 kB LowTotal: 903652 kB LowFree: 838300 kB SwapTotal: 2097892 kB SwapFree: 2096616 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5724 kB Slab: 23864 kB Committed_AS: 64232 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 18:28:02 (client local time) WITH STATUS 30 IN 526.298 SECONDS stats: 2616 0 526.298 30
c Parsing PB file... c Converting 28 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: # c -- Clauses(.)/Splits(s): .....s c ---[ 26]---> BDD-cost: 3 c ---[ 25]---> BDD-cost: 3 c ---[ 24]---> BDD-cost: 3 c ---[ 23]---> BDD-cost: 3 c ---[ 22]---> BDD-cost: 3 c ---[ 21]---> BDD-cost: 5 c ---[ 20]---> BDD-cost: 5 c ---[ 19]---> BDD-cost: 5 c ---[ 17]---> BDD-cost: 5 c ---[ 16]---> BDD-cost: 7 c ---[ 15]---> BDD-cost: 7 c ---[ 14]---> BDD-cost: 7 c ---[ 13]---> BDD-cost: 7 c ---[ 12]---> BDD-cost: 7 c ---[ 9]---> BDD-cost: 11 c ---[ 8]---> BDD-cost: 16 c ---[ 7]---> BDD-cost: 28 c ---[ 6]---> BDD-cost: 202 c ---[ 4]---> Sorter-cost: 1747 Base: 5 2 2 2 c ---[ 3]---> Sorter-cost: 1884 Base: 5 2 2 3 c ---[ 1]---> Sorter-cost: 3158 Base: 5 2 2 3 c ---[ 0]---> BDD-cost: 32 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 16046 38074 | 5348 0 0 nan | 0.000 % | c | 100 | 15635 37138 | 5882 84 320 3.8 | 2.411 % | c ============================================================================== c [1mFound solution: 4214[0m c ---[ 0]---> Sorter-cost:12454 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 165 | 44577 104802 | 14859 126 495 3.9 | 2.411 % | c | 265 | 44148 103822 | 16344 204 1226 6.0 | 2.633 % | c | 416 | 42786 100729 | 17979 340 2419 7.1 | 4.977 % | c ============================================================================== c [1mFound solution: 4091[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 516 | 43053 101446 | 14351 436 4111 9.4 | 4.977 % | c | 617 | 42937 101186 | 15786 533 4805 9.0 | 5.472 % | c ============================================================================== c [1mFound solution: 2600[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 640 | 43156 101738 | 14385 553 5096 9.2 | 5.472 % | c ============================================================================== c [1mFound solution: 2564[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 733 | 43234 101950 | 14411 640 6902 10.8 | 5.472 % | c | 833 | 42467 100186 | 15852 705 8115 11.5 | 7.152 % | c | 984 | 42275 99752 | 17437 854 11226 13.1 | 7.490 % | c | 1209 | 41845 98792 | 19181 1068 14405 13.5 | 8.265 % | c ============================================================================== c [1mFound solution: 2366[0m c ---[ 0]---> Sorter-cost: 3 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1405 | 41854 98818 | 13951 1262 19196 15.2 | 8.265 % | c | 1505 | 41819 98739 | 15346 1359 20565 15.1 | 8.375 % | c | 1658 | 41819 98739 | 16880 1512 22650 15.0 | 8.375 % | c | 1886 | 41819 98739 | 18568 1740 26014 15.0 | 8.375 % | c ============================================================================== c [1mFound solution: 2325[0m c ---[ 0]---> Sorter-cost: 4 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2148 | 41870 98883 | 13956 2001 37066 18.5 | 8.375 % | c | 2248 | 41870 98883 | 15351 2101 38353 18.3 | 8.415 % | c | 2398 | 41718 98530 | 16886 2237 41178 18.4 | 8.688 % | c ============================================================================== c [1mFound solution: 2113[0m c ---[ 0]---> Sorter-cost: 6 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2526 | 41859 98891 | 13953 2365 43488 18.4 | 8.688 % | c | 2626 | 41859 98891 | 15348 2465 45485 18.5 | 8.664 % | c | 2776 | 40589 95970 | 16883 2550 46881 18.4 | 10.901 % | c | 3001 | 40500 95764 | 18571 2771 49031 17.7 | 11.062 % | c ============================================================================== c [1mFound solution: 2077[0m c ---[ 0]---> Sorter-cost: 4 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3040 | 40584 95973 | 13528 2810 49423 17.6 | 11.062 % | c | 3140 | 40559 95916 | 14880 2909 50766 17.5 | 11.092 % | c | 3290 | 40559 95916 | 16368 3059 56749 18.6 | 11.092 % | c | 3515 | 40515 95820 | 18005 3281 61210 18.7 | 11.184 % | c | 3852 | 40515 95820 | 19806 3618 65648 18.1 | 11.184 % | c | 4358 | 40515 95820 | 21786 4124 88847 21.5 | 11.184 % | c | 5117 | 40196 95082 | 23965 4861 105377 21.7 | 11.755 % | c ============================================================================== c [1mFound solution: 2039[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 5461 | 40281 95290 | 13427 5205 111999 21.5 | 11.755 % | c | 5561 | 40281 95290 | 14769 5305 113810 21.5 | 11.737 % | c | 5713 | 40281 95290 | 16246 5457 119781 21.9 | 11.737 % | c | 5941 | 40138 94960 | 17871 5682 123620 21.8 | 12.002 % | c | 6278 | 40056 94769 | 19658 6012 139893 23.3 | 12.145 % | c | 6785 | 40056 94769 | 21624 6519 154678 23.7 | 12.145 % | c | 7544 | 40056 94769 | 23786 7278 185023 25.4 | 12.145 % | c ============================================================================== c [1mFound solution: 2010[0m c ---[ 0]---> Sorter-cost: 7 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 7994 | 40046 94775 | 13348 7727 201707 26.1 | 12.145 % | c | 8094 | 40046 94775 | 14682 7827 203566 26.0 | 12.180 % | c | 8247 | 40046 94775 | 16151 7980 207754 26.0 | 12.180 % | c | 8472 | 40046 94775 | 17766 8205 218952 26.7 | 12.180 % | c | 8811 | 39869 94368 | 19542 8543 242672 28.4 | 12.478 % | c | 9317 | 39869 94368 | 21497 9049 265341 29.3 | 12.479 % | c | 10079 | 39716 94014 | 23646 9808 297070 30.3 | 12.725 % | c ============================================================================== c [1mFound solution: 1959[0m c ---[ 0]---> Sorter-cost: 4 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 10263 | 39721 94026 | 13240 9992 307859 30.8 | 12.725 % | c | 10364 | 39721 94026 | 14564 10093 309197 30.6 | 12.729 % | c | 10516 | 39721 94026 | 16020 10245 318608 31.1 | 12.729 % | c | 10741 | 39642 93844 | 17622 10469 325530 31.1 | 12.855 % | c | 11078 | 39642 93844 | 19384 10806 334232 30.9 | 12.855 % | c | 11584 | 39642 93844 | 21323 11312 343314 30.3 | 12.855 % | c | 12343 | 39642 93844 | 23455 12071 395208 32.7 | 12.855 % | c ============================================================================== c [1mFound solution: 1886[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 13200 | 39659 93888 | 13219 12928 450474 34.8 | 12.855 % | c | 13303 | 39659 93888 | 14540 13031 452979 34.8 | 12.853 % | c | 13454 | 38672 91602 | 15994 13170 458874 34.8 | 14.632 % | c | 13679 | 38263 90657 | 17594 13381 465007 34.8 | 15.366 % | c | 14018 | 38263 90657 | 19353 13720 474081 34.6 | 15.366 % | c | 14524 | 38117 90317 | 21289 14212 486103 34.2 | 15.647 % | c | 15284 | 38117 90317 | 23418 14972 516201 34.5 | 15.647 % | c | 16423 | 38096 90271 | 25760 16110 576733 35.8 | 15.688 % | c | 18132 | 38096 90271 | 28336 17819 637141 35.8 | 15.687 % | c ============================================================================== c [1mFound solution: 1856[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19713 | 37961 89969 | 12653 19397 724840 37.4 | 15.687 % | c | 19814 | 37961 89969 | 13918 9800 342591 35.0 | 15.953 % | c | 19964 | 37961 89969 | 15310 9950 348722 35.0 | 15.953 % | c | 20191 | 37961 89969 | 16841 10177 365079 35.9 | 15.953 % | c | 20528 | 37757 89497 | 18525 10510 372889 35.5 | 16.320 % | c | 21038 | 37757 89497 | 20377 11020 391939 35.6 | 16.320 % | c | 21797 | 37757 89497 | 22415 11779 428095 36.3 | 16.320 % | c | 22936 | 37757 89497 | 24657 12918 478718 37.1 | 16.320 % | c | 24644 | 37739 89455 | 27122 14624 564886 38.6 | 16.354 % | c | 27206 | 37739 89455 | 29835 17186 670859 39.0 | 16.356 % | c ============================================================================== c [1mFound solution: 1839[0m c ---[ 0]---> Sorter-cost: 4 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 28163 | 37595 89142 | 12531 18140 701282 38.7 | 16.356 % | c ============================================================================== c [1mFound solution: 1664[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 28226 | 37603 89161 | 12534 9133 312313 34.2 | 16.356 % | c | 28329 | 37381 88644 | 13787 9234 317012 34.3 | 17.034 % | c | 28480 | 37342 88554 | 15166 9384 320198 34.1 | 17.108 % | c | 28706 | 37342 88554 | 16682 9610 330983 34.4 | 17.108 % | c | 29043 | 37319 88502 | 18351 9946 337229 33.9 | 17.148 % | c | 29551 | 37253 88349 | 20186 10451 354605 33.9 | 17.263 % | c | 30310 | 37253 88349 | 22204 11210 376924 33.6 | 17.263 % | c | 31450 | 37176 88173 | 24425 12348 421282 34.1 | 17.395 % | c ============================================================================== c [1mFound solution: 1652[0m c ---[ 0]---> Sorter-cost: 3 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 32430 | 37181 88185 | 12393 13328 478161 35.9 | 17.395 % | c | 32531 | 37181 88185 | 13632 13429 481643 35.9 | 17.398 % | c ============================================================================== c [1mFound solution: 1651[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 32556 | 37188 88201 | 12396 13454 483056 35.9 | 17.398 % | c | 32657 | 37188 88201 | 13635 13555 488293 36.0 | 17.399 % | c ============================================================================== c [1mFound solution: 1645[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 32681 | 37193 88212 | 12397 13579 489409 36.0 | 17.399 % | c ============================================================================== c [1mFound solution: 1641[0m c ---[ 0]---> Sorter-cost: 4 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 32709 | 37199 88239 | 12399 13607 490510 36.0 | 17.399 % | c ============================================================================== c [1mFound solution: 1626[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 32722 | 37206 88255 | 12402 13620 491045 36.1 | 17.399 % | c ============================================================================== c [1mFound solution: 1572[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 32812 | 37222 88295 | 12407 13710 495909 36.2 | 17.399 % | c | 32912 | 37222 88295 | 13647 13810 500499 36.2 | 17.401 % | c | 33062 | 37222 88295 | 15012 13960 505960 36.2 | 17.401 % | c | 33288 | 37222 88295 | 16513 14186 515084 36.3 | 17.401 % | c ============================================================================== c [1mFound solution: 1569[0m c ---[ 0]---> Sorter-cost: 3 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 33417 | 37227 88310 | 12409 14315 523217 36.6 | 17.401 % | c | 33523 | 37227 88310 | 13649 14421 526997 36.5 | 17.403 % | c ============================================================================== c [1mFound solution: 1561[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 33536 | 37233 88325 | 12411 14434 527364 36.5 | 17.403 % | c | 33636 | 37233 88325 | 13652 14534 532924 36.7 | 17.405 % | c | 33786 | 37233 88325 | 15017 14684 542227 36.9 | 17.405 % | c ============================================================================== c [1mFound solution: 1553[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 33951 | 37239 88340 | 12413 14849 553272 37.3 | 17.405 % | c ============================================================================== c [1mFound solution: 1538[0m c ---[ 0]---> Sorter-cost: 4 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 34010 | 37245 88354 | 12415 14908 556476 37.3 | 17.405 % | c ============================================================================== c [1mFound solution: 1472[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 34072 | 37250 88365 | 12416 14970 558955 37.3 | 17.405 % | c ============================================================================== c [1mFound solution: 1456[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 34088 | 37256 88378 | 12418 14986 559491 37.3 | 17.405 % | c ============================================================================== c [1mFound solution: 1452[0m c ---[ 0]---> Sorter-cost: 4 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 34119 | 37263 88397 | 12421 15017 560717 37.3 | 17.405 % | c | 34223 | 37263 88397 | 13663 15121 564578 37.3 | 17.415 % | c | 34374 | 37263 88397 | 15029 15272 566776 37.1 | 17.415 % | c | 34600 | 37212 88281 | 16532 15497 570014 36.8 | 17.507 % | c | 34937 | 37212 88281 | 18185 15834 579121 36.6 | 17.507 % | c | 35443 | 37200 88253 | 20004 16339 598956 36.7 | 17.530 % | c | 36204 | 37200 88253 | 22004 17100 610536 35.7 | 17.530 % | c | 37345 | 37200 88253 | 24205 18241 664918 36.5 | 17.530 % | c ============================================================================== c [1mFound solution: 1447[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 37458 | 37206 88268 | 12402 18354 668483 36.4 | 17.530 % | c | 37559 | 37206 88268 | 13642 9278 289999 31.3 | 17.531 % | c | 37710 | 37206 88268 | 15006 9429 292072 31.0 | 17.531 % | c | 37935 | 37206 88268 | 16507 9654 294931 30.6 | 17.532 % | c ============================================================================== c [1mFound solution: 1443[0m c ---[ 0]---> Sorter-cost: 4 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 38158 | 37211 88295 | 12403 9877 303179 30.7 | 17.532 % | c | 38258 | 37211 88295 | 13643 9977 306001 30.7 | 17.533 % | c | 38410 | 37211 88295 | 15007 10129 311348 30.7 | 17.533 % | c | 38635 | 37211 88295 | 16508 10354 318865 30.8 | 17.533 % | c | 38972 | 37211 88295 | 18159 10691 334629 31.3 | 17.533 % | c ============================================================================== c [1mFound solution: 1416[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 39137 | 37214 88302 | 12404 10856 341941 31.5 | 17.533 % | c | 39237 | 37214 88302 | 13644 10956 346578 31.6 | 17.537 % | c ============================================================================== c [1mFound solution: 1408[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 39385 | 37222 88321 | 12407 11104 354963 32.0 | 17.537 % | c | 39486 | 37222 88321 | 13647 11205 359650 32.1 | 17.538 % | c ============================================================================== c [1mFound solution: 1402[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 39559 | 37228 88336 | 12409 11278 363189 32.2 | 17.538 % | c | 39660 | 37228 88336 | 13649 11379 369106 32.4 | 17.539 % | c | 39810 | 37228 88336 | 15014 11529 374970 32.5 | 17.539 % | c ============================================================================== c [1mFound solution: 1394[0m c ---[ 0]---> Sorter-cost: 3 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 39904 | 37232 88346 | 12410 11623 382319 32.9 | 17.539 % | c ============================================================================== c [1mFound solution: 1377[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 39989 | 37235 88353 | 12411 11708 385879 33.0 | 17.539 % | c ============================================================================== c [1mFound solution: 1358[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 40014 | 37242 88369 | 12414 11733 386311 32.9 | 17.539 % | c ============================================================================== c [1mFound solution: 1338[0m c ---[ 0]---> Sorter-cost: 3 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 40098 | 37247 88381 | 12415 11817 391980 33.2 | 17.539 % | c ============================================================================== c [1mFound solution: 1321[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 40114 | 37254 88397 | 12418 11833 393663 33.3 | 17.539 % | c | 40215 | 37254 88397 | 13659 11934 398464 33.4 | 17.552 % | c ============================================================================== c [1mFound solution: 1315[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 40255 | 37261 88413 | 12420 11974 401118 33.5 | 17.552 % | c | 40356 | 37261 88413 | 13662 12075 405622 33.6 | 17.553 % | c ============================================================================== c [1mFound solution: 1270[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 40457 | 37278 88469 | 12426 12176 409843 33.7 | 17.553 % | c | 40557 | 37278 88469 | 13668 12276 414230 33.7 | 17.548 % | c | 40708 | 37278 88469 | 15035 12427 421195 33.9 | 17.548 % | c | 40935 | 37278 88469 | 16539 12654 429895 34.0 | 17.548 % | c ============================================================================== c [1mFound solution: 1260[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 41007 | 37282 88481 | 12427 12726 433324 34.1 | 17.548 % | c | 41108 | 37282 88481 | 13669 12827 435629 34.0 | 17.551 % | c | 41258 | 37282 88481 | 15036 12977 442812 34.1 | 17.551 % | c | 41483 | 37282 88481 | 16540 13202 450647 34.1 | 17.551 % | c | 41820 | 37282 88481 | 18194 13539 465424 34.4 | 17.551 % | c ============================================================================== c [1mFound solution: 1251[0m c ---[ 0]---> Sorter-cost: 3 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 41958 | 37286 88491 | 12428 13677 472983 34.6 | 17.551 % | c | 42058 | 37286 88491 | 13670 13777 475577 34.5 | 17.554 % | c | 42209 | 37286 88491 | 15037 13928 480858 34.5 | 17.554 % | c | 42434 | 37286 88491 | 16541 14153 489371 34.6 | 17.554 % | c | 42771 | 37286 88491 | 18195 14490 504565 34.8 | 17.554 % | c ============================================================================== c [1mFound solution: 1236[0m c ---[ 0]---> Sorter-cost: 3 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 43097 | 37290 88501 | 12430 14816 517926 35.0 | 17.554 % | c | 43201 | 37290 88501 | 13673 14920 520576 34.9 | 17.556 % | c | 43352 | 37290 88501 | 15040 15071 524544 34.8 | 17.556 % | c | 43578 | 37290 88501 | 16544 15297 529541 34.6 | 17.556 % | c | 43915 | 37249 88407 | 18198 15632 546898 35.0 | 17.630 % | c | 44421 | 37249 88407 | 20018 16138 572561 35.5 | 17.630 % | c | 45180 | 37249 88407 | 22020 16897 599477 35.5 | 17.630 % | c | 46319 | 37249 88407 | 24222 18036 663826 36.8 | 17.630 % | c | 48027 | 37159 88200 | 26644 19742 733345 37.1 | 17.784 % | c ============================================================================== c [1mFound solution: 1232[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 48159 | 37162 88207 | 12387 19874 739448 37.2 | 17.784 % | c | 48261 | 37162 88207 | 13625 10039 311227 31.0 | 17.788 % | c | 48411 | 37162 88207 | 14988 10189 320968 31.5 | 17.788 % | c | 48636 | 37162 88207 | 16487 10414 330060 31.7 | 17.788 % | c | 48976 | 37162 88207 | 18135 10754 347428 32.3 | 17.788 % | c | 49482 | 37162 88207 | 19949 11260 374286 33.2 | 17.788 % | c ============================================================================== c [1mFound solution: 1224[0m c ---[ 0]---> Sorter-cost: 4 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 49511 | 37168 88221 | 12389 11289 375722 33.3 | 17.788 % | c | 49611 | 37168 88221 | 13627 11389 377638 33.2 | 17.790 % | c | 49762 | 37168 88221 | 14990 11540 379388 32.9 | 17.790 % | c | 49987 | 37168 88221 | 16489 11765 382453 32.5 | 17.790 % | c | 50324 | 37168 88221 | 18138 12102 386606 31.9 | 17.790 % | c | 50830 | 37095 88046 | 19952 12607 411468 32.6 | 17.926 % | c | 51589 | 37095 88046 | 21947 13366 457483 34.2 | 17.926 % | c ============================================================================== c [1mFound solution: 1164[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 51730 | 37102 88062 | 12367 13507 463432 34.3 | 17.926 % | c ============================================================================== c [1mFound solution: 1149[0m c ---[ 0]---> Sorter-cost: 3 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 51773 | 37106 88071 | 12368 13550 465084 34.3 | 17.926 % | c ============================================================================== c [1mFound solution: 1145[0m c ---[ 0]---> Sorter-cost: 4 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 51800 | 37111 88082 | 12370 13577 466661 34.4 | 17.926 % | c | 51901 | 37111 88082 | 13607 13678 470120 34.4 | 17.935 % | c | 52053 | 37050 87942 | 14967 13829 473685 34.3 | 18.043 % | c | 52280 | 36992 87807 | 16464 14054 482775 34.4 | 18.140 % | c | 52617 | 36992 87807 | 18110 14391 494648 34.4 | 18.140 % | c | 53123 | 36932 87669 | 19922 14896 514713 34.6 | 18.248 % | c | 53883 | 36905 87606 | 21914 15654 548585 35.0 | 18.305 % | c | 55023 | 36839 87452 | 24105 16790 597435 35.6 | 18.430 % | c | 56732 | 36839 87452 | 26516 18499 683813 37.0 | 18.430 % | c | 59294 | 36575 86839 | 29167 21056 779119 37.0 | 18.891 % | c ============================================================================== c [1mFound solution: 1143[0m c ---[ 0]---> Sorter-cost: 1 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 62257 | 36529 86733 | 12176 24018 940108 39.1 | 18.891 % | c | 62357 | 36529 86733 | 13393 12109 411396 34.0 | 18.968 % | c | 62507 | 36529 86733 | 14732 12259 416196 34.0 | 18.968 % | c | 62736 | 36529 86733 | 16206 12488 424299 34.0 | 18.968 % | c | 63074 | 36525 86724 | 17826 12824 435716 34.0 | 18.973 % | c | 63580 | 36525 86724 | 19609 13330 453755 34.0 | 18.973 % | c | 64340 | 36525 86724 | 21570 14090 483252 34.3 | 18.973 % | c | 65480 | 36525 86724 | 23727 15230 531010 34.9 | 18.973 % | c ============================================================================== c [1mFound solution: 1136[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 66364 | 36531 86739 | 12177 16114 566145 35.1 | 18.973 % | c | 66465 | 36531 86739 | 13394 8158 210937 25.9 | 18.975 % | c | 66617 | 36531 86739 | 14734 8310 214915 25.9 | 18.975 % | c | 66845 | 36531 86739 | 16207 8538 226913 26.6 | 18.975 % | c | 67185 | 36531 86739 | 17828 8878 240121 27.0 | 18.975 % | c | 67691 | 36531 86739 | 19611 9384 254470 27.1 | 18.975 % | c | 68450 | 36531 86739 | 21572 10143 285357 28.1 | 18.975 % | c | 69589 | 36531 86739 | 23729 11282 325499 28.9 | 18.975 % | c | 71298 | 36531 86739 | 26102 12991 388992 29.9 | 18.975 % | c | 73862 | 36531 86739 | 28712 15555 499400 32.1 | 18.975 % | c | 77706 | 36531 86739 | 31584 19399 641893 33.1 | 18.975 % | c | 83473 | 36531 86739 | 34742 25166 851867 33.8 | 18.975 % | c ============================================================================== c [1mFound solution: 1128[0m c ---[ 0]---> Sorter-cost:10819 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 83855 | 48846 115593 | 16282 9881 252889 25.6 | 18.975 % | c | 83955 | 48846 115593 | 17910 9981 256387 25.7 | 13.426 % | c | 84108 | 48846 115593 | 19701 10134 262174 25.9 | 13.426 % | c | 84335 | 48846 115593 | 21671 10361 273735 26.4 | 13.426 % | c | 84674 | 48846 115593 | 23838 10700 287638 26.9 | 13.426 % | c | 85180 | 48846 115593 | 26222 11206 302850 27.0 | 13.426 % | c | 85939 | 48846 115593 | 28844 11965 328037 27.4 | 13.426 % | c | 87080 | 48846 115593 | 31729 13106 363663 27.7 | 13.426 % | c | 88789 | 48846 115593 | 34901 14815 448569 30.3 | 13.426 % | c | 91351 | 48842 115584 | 38392 17376 574966 33.1 | 13.430 % | c | 95195 | 48842 115584 | 42231 21220 715548 33.7 | 13.430 % | c | 100962 | 48832 115561 | 46454 26986 948975 35.2 | 13.441 % | c ============================================================================== c [1mFound solution: 1120[0m c ---[ 0]---> Sorter-cost: 6 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 102576 | 58954 139062 | 19651 28600 999476 34.9 | 13.441 % | c | 102676 | 58954 139062 | 21616 14400 427455 29.7 | 16.672 % | c | 102826 | 58954 139062 | 23777 14550 429765 29.5 | 16.672 % | c | 103052 | 58954 139062 | 26155 14776 433516 29.3 | 16.672 % | c | 103390 | 58314 137610 | 28771 14316 428116 29.9 | 17.465 % | c | 103898 | 58250 137467 | 31648 14819 442265 29.8 | 17.541 % | c | 104661 | 58250 137467 | 34812 15582 470141 30.2 | 17.541 % | c | 105802 | 58250 137467 | 38294 16723 498243 29.8 | 17.541 % | c | 107510 | 58250 137467 | 42123 18431 562484 30.5 | 17.541 % | c | 110076 | 58250 137467 | 46336 20997 665926 31.7 | 17.541 % | c | 113921 | 58250 137467 | 50969 24842 808229 32.5 | 17.541 % | c ============================================================================== c [1mOptimal solution: 1120[0m s OPTIMUM FOUND v x0 x1 -x2 -x3 -x4 -x5 -x6 -x7 -x8 x9 -x10 -x11 -x12 -x13 -x14 -x15 -x16 -x17 -x18 -x19 -x20 -x21 x22 -x23 -x24 -x25 -x26 -x27 -x28 -x29 x30 -x31 -x32 -x33 x34 -x35 -x36 -x37 x38 -x39 -x40 -x41 -x42 -x43 -x44 -x45 x46 -x47 x48 -x49 -x50 -x51 -x52 -x53 -x54 -x55 -x56 -x57 -x58 x59 -x60 x61 -x62 -x63 -x64 -x65 -x66 -x67 -x68 -x69 -x70 -x71 -x72 -x73 -x74 -x75 -x76 -x77 -x78 -x79 -x80 x81 -x82 -x83 -x84 -x85 x86 -x87 -x88 c _______________________________________________________________________________ c c restarts : 222 c conflicts : 114741 (218 /sec) c decisions : 222002 (422 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 525.999 s c _______________________________________________________________________________
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/9468/stat): 9468 (minisat+_script) R 9467 9468 28974 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843345786 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/9468/statm): 174 3 169 147 0 27 0 [pid=9468] 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=9469 New process pid=9470 New process pid=9471 execve syscall for /bin/sed executable open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 One traced child (pid=9470) exited with status: 0 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=9471) exited with status: 0 One traced child (pid=9469) exited with status: 0 New process pid=9472 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc27/normalized-lseu.opb [startup+10.0035 s] Raw data (loadavg): 0.93 0.96 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 1621 0 0 0 984 5 0 0 25 0 1 0 1843345791 7946240 1597 4294967295 134512640 135094434 3221224448 3221223104 134557882 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9472/statm): 1940 1597 145 145 0 1795 0 [pid=9472] vsize: 7760 Current children cumulated CPU time (s) 9.89 Current children cumulated vsize (Kb) 9884 [startup+20.0053 s] Raw data (loadavg): 0.94 0.96 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 1777 0 0 0 1981 6 0 0 25 0 1 0 1843345791 8585216 1753 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 2096 1753 145 145 0 1951 0 [pid=9472] vsize: 8384 Current children cumulated CPU time (s) 19.87 Current children cumulated vsize (Kb) 10508 [startup+30.0071 s] Raw data (loadavg): 0.95 0.96 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 1959 0 0 0 2977 8 0 0 25 0 1 0 1843345791 9355264 1935 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 2284 1935 145 145 0 2139 0 [pid=9472] vsize: 9136 Current children cumulated CPU time (s) 29.85 Current children cumulated vsize (Kb) 11260 [startup+40.0079 s] Raw data (loadavg): 0.96 0.96 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) T 9468 9468 28974 0 -1 0 2118 0 0 0 3975 9 0 0 25 0 1 0 1843345791 9986048 2094 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/9472/statm): 2438 2094 145 145 0 2293 0 [pid=9472] vsize: 9752 Current children cumulated CPU time (s) 39.84 Current children cumulated vsize (Kb) 11876 [startup+50.0088 s] Raw data (loadavg): 0.96 0.96 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2263 0 0 0 4972 10 0 0 25 0 1 0 1843345791 10571776 2239 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 2581 2239 145 145 0 2436 0 [pid=9472] vsize: 10324 Current children cumulated CPU time (s) 49.82 Current children cumulated vsize (Kb) 12448 [startup+60.0096 s] Raw data (loadavg): 0.97 0.96 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2389 0 0 0 5971 11 0 0 25 0 1 0 1843345791 11141120 2365 4294967295 134512640 135094434 3221224448 3221223136 134554687 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9472/statm): 2720 2365 145 145 0 2575 0 [pid=9472] vsize: 10880 Current children cumulated CPU time (s) 59.82 Current children cumulated vsize (Kb) 13004 [startup+70.0104 s] Raw data (loadavg): 0.97 0.96 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2452 0 0 0 6969 11 0 0 25 0 1 0 1843345791 11395072 2428 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 2782 2428 145 145 0 2637 0 [pid=9472] vsize: 11128 Current children cumulated CPU time (s) 69.8 Current children cumulated vsize (Kb) 13252 [startup+80.0122 s] Raw data (loadavg): 0.98 0.96 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2452 0 0 0 7969 12 0 0 25 0 1 0 1843345791 11395072 2428 4294967295 134512640 135094434 3221224448 3221223072 134557630 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 2782 2428 145 145 0 2637 0 [pid=9472] vsize: 11128 Current children cumulated CPU time (s) 79.81 Current children cumulated vsize (Kb) 13252 [startup+90.013 s] Raw data (loadavg): 0.98 0.96 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2460 0 0 0 8970 12 0 0 25 0 1 0 1843345791 11431936 2436 4294967295 134512640 135094434 3221224448 3221223136 134554687 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 2791 2436 145 145 0 2646 0 [pid=9472] vsize: 11164 Current children cumulated CPU time (s) 89.82 Current children cumulated vsize (Kb) 13288 [startup+100.014 s] Raw data (loadavg): 0.98 0.96 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2486 0 0 0 9969 12 0 0 25 0 1 0 1843345791 11534336 2462 4294967295 134512640 135094434 3221224448 3221223136 134554717 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 2816 2462 145 145 0 2671 0 [pid=9472] vsize: 11264 Current children cumulated CPU time (s) 99.81 Current children cumulated vsize (Kb) 13388 [startup+110.016 s] Raw data (loadavg): 0.98 0.97 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2486 0 0 0 10969 12 0 0 25 0 1 0 1843345791 11534336 2462 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 2816 2462 145 145 0 2671 0 [pid=9472] vsize: 11264 Current children cumulated CPU time (s) 109.81 Current children cumulated vsize (Kb) 13388 [startup+120.016 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2486 0 0 0 11969 12 0 0 25 0 1 0 1843345791 11534336 2462 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 2816 2462 145 145 0 2671 0 [pid=9472] vsize: 11264 Current children cumulated CPU time (s) 119.81 Current children cumulated vsize (Kb) 13388 [startup+130.017 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2486 0 0 0 12969 12 0 0 25 0 1 0 1843345791 11534336 2462 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 2816 2462 145 145 0 2671 0 [pid=9472] vsize: 11264 Current children cumulated CPU time (s) 129.81 Current children cumulated vsize (Kb) 13388 [startup+140.018 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2486 0 0 0 13969 13 0 0 25 0 1 0 1843345791 11534336 2462 4294967295 134512640 135094434 3221224448 3221223088 134562224 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 2816 2462 145 145 0 2671 0 [pid=9472] vsize: 11264 Current children cumulated CPU time (s) 139.82 Current children cumulated vsize (Kb) 13388 [startup+150.019 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2487 0 0 0 14969 13 0 0 25 0 1 0 1843345791 11534336 2463 4294967295 134512640 135094434 3221224448 3221221488 134519148 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 2816 2463 145 145 0 2671 0 [pid=9472] vsize: 11264 Current children cumulated CPU time (s) 149.82 Current children cumulated vsize (Kb) 13388 [startup+160.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2487 0 0 0 15970 13 0 0 25 0 1 0 1843345791 11534336 2463 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 2816 2463 145 145 0 2671 0 [pid=9472] vsize: 11264 Current children cumulated CPU time (s) 159.83 Current children cumulated vsize (Kb) 13388 [startup+170.021 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2490 0 0 0 16970 13 0 0 25 0 1 0 1843345791 11546624 2466 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 2819 2466 145 145 0 2674 0 [pid=9472] vsize: 11276 Current children cumulated CPU time (s) 169.83 Current children cumulated vsize (Kb) 13400 [startup+180.022 s] Raw data (loadavg): 0.99 0.97 0.92 1/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) T 9468 9468 28974 0 -1 0 2591 0 0 0 17967 14 0 0 25 0 1 0 1843345791 11968512 2567 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/9472/statm): 2922 2567 145 145 0 2777 0 [pid=9472] vsize: 11688 Current children cumulated CPU time (s) 179.81 Current children cumulated vsize (Kb) 13812 [startup+190.023 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2616 0 0 0 18967 14 0 0 25 0 1 0 1843345791 12070912 2592 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 2947 2592 145 145 0 2802 0 [pid=9472] vsize: 11788 Current children cumulated CPU time (s) 189.81 Current children cumulated vsize (Kb) 13912 [startup+200.024 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2616 0 0 0 19967 14 0 0 25 0 1 0 1843345791 12070912 2592 4294967295 134512640 135094434 3221224448 3221223040 134556812 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 2947 2592 145 145 0 2802 0 [pid=9472] vsize: 11788 Current children cumulated CPU time (s) 199.81 Current children cumulated vsize (Kb) 13912 [startup+210.025 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2616 0 0 0 20967 14 0 0 25 0 1 0 1843345791 12070912 2592 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 2947 2592 145 145 0 2802 0 [pid=9472] vsize: 11788 Current children cumulated CPU time (s) 209.81 Current children cumulated vsize (Kb) 13912 [startup+220.026 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2616 0 0 0 21968 14 0 0 25 0 1 0 1843345791 12070912 2592 4294967295 134512640 135094434 3221224448 3221223136 134554685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 2947 2592 145 145 0 2802 0 [pid=9472] vsize: 11788 Current children cumulated CPU time (s) 219.82 Current children cumulated vsize (Kb) 13912 [startup+230.028 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2628 0 0 0 22968 14 0 0 25 0 1 0 1843345791 12115968 2604 4294967295 134512640 135094434 3221224448 3221223040 134557227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 2958 2604 145 145 0 2813 0 [pid=9472] vsize: 11832 Current children cumulated CPU time (s) 229.82 Current children cumulated vsize (Kb) 13956 [startup+240.028 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2734 0 0 0 23965 15 0 0 25 0 1 0 1843345791 12541952 2710 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 3062 2710 145 145 0 2917 0 [pid=9472] vsize: 12248 Current children cumulated CPU time (s) 239.8 Current children cumulated vsize (Kb) 14372 [startup+250.029 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2853 0 0 0 24963 17 0 0 25 0 1 0 1843345791 13033472 2829 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 3182 2829 145 145 0 3037 0 [pid=9472] vsize: 12728 Current children cumulated CPU time (s) 249.8 Current children cumulated vsize (Kb) 14852 [startup+260.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2870 0 0 0 25963 17 0 0 25 0 1 0 1843345791 13103104 2846 4294967295 134512640 135094434 3221224448 3221223040 134557004 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 3199 2846 145 145 0 3054 0 [pid=9472] vsize: 12796 Current children cumulated CPU time (s) 259.8 Current children cumulated vsize (Kb) 14920 [startup+270.031 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2876 0 0 0 26963 17 0 0 25 0 1 0 1843345791 13127680 2852 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 3205 2852 145 145 0 3060 0 [pid=9472] vsize: 12820 Current children cumulated CPU time (s) 269.8 Current children cumulated vsize (Kb) 14944 [startup+280.032 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2876 0 0 0 27963 17 0 0 25 0 1 0 1843345791 13127680 2852 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 3205 2852 145 145 0 3060 0 [pid=9472] vsize: 12820 Current children cumulated CPU time (s) 279.8 Current children cumulated vsize (Kb) 14944 [startup+290.032 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2876 0 0 0 28963 17 0 0 25 0 1 0 1843345791 13127680 2852 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 3205 2852 145 145 0 3060 0 [pid=9472] vsize: 12820 Current children cumulated CPU time (s) 289.8 Current children cumulated vsize (Kb) 14944 [startup+300.033 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2876 0 0 0 29964 17 0 0 25 0 1 0 1843345791 13127680 2852 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 3205 2852 145 145 0 3060 0 [pid=9472] vsize: 12820 Current children cumulated CPU time (s) 299.81 Current children cumulated vsize (Kb) 14944 [startup+310.034 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2876 0 0 0 30964 17 0 0 25 0 1 0 1843345791 13127680 2852 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 3205 2852 145 145 0 3060 0 [pid=9472] vsize: 12820 Current children cumulated CPU time (s) 309.81 Current children cumulated vsize (Kb) 14944 [startup+320.035 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2876 0 0 0 31964 17 0 0 25 0 1 0 1843345791 13127680 2852 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 3205 2852 145 145 0 3060 0 [pid=9472] vsize: 12820 Current children cumulated CPU time (s) 319.81 Current children cumulated vsize (Kb) 14944 [startup+330.036 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2879 0 0 0 32964 17 0 0 25 0 1 0 1843345791 13144064 2855 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 3209 2855 145 145 0 3064 0 [pid=9472] vsize: 12836 Current children cumulated CPU time (s) 329.81 Current children cumulated vsize (Kb) 14960 [startup+340.037 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2891 0 0 0 33965 17 0 0 25 0 1 0 1843345791 13209600 2867 4294967295 134512640 135094434 3221224448 3221223040 134556765 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 3225 2867 145 145 0 3080 0 [pid=9472] vsize: 12900 Current children cumulated CPU time (s) 339.82 Current children cumulated vsize (Kb) 15024 [startup+350.037 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2904 0 0 0 34965 17 0 0 25 0 1 0 1843345791 13307904 2880 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 3249 2880 145 145 0 3104 0 [pid=9472] vsize: 12996 Current children cumulated CPU time (s) 349.82 Current children cumulated vsize (Kb) 15120 [startup+360.039 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 3163 0 0 0 35964 18 0 0 25 0 1 0 1843345791 13574144 3097 4294967295 134512640 135094434 3221224448 3221223072 134557726 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 3314 3097 145 145 0 3169 0 [pid=9472] vsize: 13256 Current children cumulated CPU time (s) 359.82 Current children cumulated vsize (Kb) 15380 [startup+370.039 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 3163 0 0 0 36964 18 0 0 25 0 1 0 1843345791 13574144 3097 4294967295 134512640 135094434 3221224448 3221223072 134562085 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 3314 3097 145 145 0 3169 0 [pid=9472] vsize: 13256 Current children cumulated CPU time (s) 369.82 Current children cumulated vsize (Kb) 15380 [startup+380.04 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 3163 0 0 0 37964 18 0 0 25 0 1 0 1843345791 13574144 3097 4294967295 134512640 135094434 3221224448 3221223040 134557389 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 3314 3097 145 145 0 3169 0 [pid=9472] vsize: 13256 Current children cumulated CPU time (s) 379.82 Current children cumulated vsize (Kb) 15380 [startup+390.041 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 3167 0 0 0 38964 19 0 0 25 0 1 0 1843345791 13590528 3101 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 3318 3101 145 145 0 3173 0 [pid=9472] vsize: 13272 Current children cumulated CPU time (s) 389.83 Current children cumulated vsize (Kb) 15396 [startup+400.04 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 3252 0 0 0 39963 19 0 0 25 0 1 0 1843345791 13934592 3186 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 3402 3186 145 145 0 3257 0 [pid=9472] vsize: 13608 Current children cumulated CPU time (s) 399.82 Current children cumulated vsize (Kb) 15732 [startup+410.041 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 3341 0 0 0 40961 20 0 0 25 0 1 0 1843345791 14299136 3275 4294967295 134512640 135094434 3221224448 3221223040 134557182 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 3491 3275 145 145 0 3346 0 [pid=9472] vsize: 13964 Current children cumulated CPU time (s) 409.81 Current children cumulated vsize (Kb) 16088 [startup+420.042 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 3423 0 0 0 41960 21 0 0 25 0 1 0 1843345791 14639104 3357 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 3574 3357 145 145 0 3429 0 [pid=9472] vsize: 14296 Current children cumulated CPU time (s) 419.81 Current children cumulated vsize (Kb) 16420 [startup+430.043 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 3516 0 0 0 42958 22 0 0 25 0 1 0 1843345791 15015936 3450 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 3666 3450 145 145 0 3521 0 [pid=9472] vsize: 14664 Current children cumulated CPU time (s) 429.8 Current children cumulated vsize (Kb) 16788 [startup+440.044 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 3601 0 0 0 43957 22 0 0 25 0 1 0 1843345791 15380480 3535 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 3755 3535 145 145 0 3610 0 [pid=9472] vsize: 15020 Current children cumulated CPU time (s) 439.79 Current children cumulated vsize (Kb) 17144 [startup+450.045 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 3761 0 0 0 44955 24 0 0 25 0 1 0 1843345791 15998976 3695 4294967295 134512640 135094434 3221224448 3221223072 134557612 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 3906 3695 145 145 0 3761 0 [pid=9472] vsize: 15624 Current children cumulated CPU time (s) 449.79 Current children cumulated vsize (Kb) 17748 [startup+460.045 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 3766 0 0 0 45955 24 0 0 25 0 1 0 1843345791 16031744 3700 4294967295 134512640 135094434 3221224448 3221223104 134557882 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 3914 3700 145 145 0 3769 0 [pid=9472] vsize: 15656 Current children cumulated CPU time (s) 459.79 Current children cumulated vsize (Kb) 17780 [startup+470.046 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 3767 0 0 0 46956 24 0 0 25 0 1 0 1843345791 16031744 3701 4294967295 134512640 135094434 3221224448 3221223104 134557890 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 3914 3701 145 145 0 3769 0 [pid=9472] vsize: 15656 Current children cumulated CPU time (s) 469.8 Current children cumulated vsize (Kb) 17780 [startup+480.047 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 3779 0 0 0 47956 24 0 0 25 0 1 0 1843345791 16105472 3713 4294967295 134512640 135094434 3221224448 3221223040 134557404 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 3932 3713 145 145 0 3787 0 [pid=9472] vsize: 15728 Current children cumulated CPU time (s) 479.8 Current children cumulated vsize (Kb) 17852 [startup+490.048 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 3779 0 0 0 48956 24 0 0 25 0 1 0 1843345791 16105472 3713 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 3932 3713 145 145 0 3787 0 [pid=9472] vsize: 15728 Current children cumulated CPU time (s) 489.8 Current children cumulated vsize (Kb) 17852 [startup+500.049 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 3779 0 0 0 49956 24 0 0 25 0 1 0 1843345791 16105472 3713 4294967295 134512640 135094434 3221224448 3221223040 134556843 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 3932 3713 145 145 0 3787 0 [pid=9472] vsize: 15728 Current children cumulated CPU time (s) 499.8 Current children cumulated vsize (Kb) 17852 [startup+510.05 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 3779 0 0 0 50956 24 0 0 25 0 1 0 1843345791 16105472 3713 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 3932 3713 145 145 0 3787 0 [pid=9472] vsize: 15728 Current children cumulated CPU time (s) 509.8 Current children cumulated vsize (Kb) 17852 [startup+520.05 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 9472 Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9468/statm): 531 226 485 147 0 384 0 [pid=9468] vsize: 2124 Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 3812 0 0 0 51956 24 0 0 25 0 1 0 1843345791 16261120 3746 4294967295 134512640 135094434 3221224448 3221223072 134557726 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9472/statm): 3970 3746 145 145 0 3825 0 [pid=9472] vsize: 15880 Current children cumulated CPU time (s) 519.8 Current children cumulated vsize (Kb) 18004 One traced child (pid=9472) exited with status: 30 One traced child (pid=9468) exited with status: 30 All traced children have exited ! Game is over. Child status: 30 Real time (s): 526.512 CPU time (s): 526.298 CPU user time (s): 526.025 CPU system time (s): 0.272958 CPU usage (%): 99.9594 Max. virtual memory (cumulated for all children) (Kb): 18004
Verifier: OK 1120