Name | normalized-opb/mps-v2-13-7/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-gr4x6.opb |
MD5SUM | c1c7537cd9b3e10215a81ec1ca3be5cb |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 2605440 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 504 |
Biggest coefficient in the objective function | 148373504 |
Number of bits for the biggest coefficient in the objective function | 28 |
Sum of the numbers in the objective function | 3393589600 |
Number of bits of the sum of numbers in the objective function | 32 |
Biggest number in a constraint | 148373504 |
Number of bits of the biggest number in a constraint | 28 |
Biggest sum of numbers in a constraint | 3393589600 |
Number of bits of the biggest sum of numbers | 32 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1189.01 |
Number of variables | 504 |
Total number of constraints | 34 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 34 |
Minimum length of a constraint | 21 |
Maximum length of a constraint | 120 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc13 THE 2005-05-25 23:24:24 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=22645 boxname=wulflinc13 idbench=1461 idsolver=15 numberseed=0 MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814 /oldhome/oroussel/solvers/minisat+_script MD5SUM BENCH: c1c7537cd9b3e10215a81ec1ca3be5cb /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-gr4x6.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-gr4x6.opb IDLAUNCH: 22645 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.242 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.242 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 901728 kB Buffers: 21464 kB Cached: 91548 kB SwapCached: 412 kB Active: 17484 kB Inactive: 97852 kB HighTotal: 131008 kB HighFree: 105252 kB LowTotal: 903652 kB LowFree: 796476 kB SwapTotal: 2097136 kB SwapFree: 2096060 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5948 kB Slab: 11972 kB Committed_AS: 63592 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-05-25 23:44:54 (client local time) WITH STATUS 152 IN 1229.86 SECONDS stats: 22645 7 1229.86 152 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 44 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ########## c -- Clauses(.)/Splits(s): (none) c ---[ 42]---> Sorter-cost: 972 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 40]---> Sorter-cost: 972 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 38]---> Sorter-cost: 900 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 36]---> Sorter-cost: 888 Base: 2 2 2 2 2 2 2 2 2 c ---[ 34]---> Sorter-cost: 471 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 32]---> Sorter-cost: 455 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 30]---> Sorter-cost: 455 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 28]---> Sorter-cost: 399 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 26]---> Sorter-cost: 359 Base: 2 2 2 2 2 2 2 2 2 c ---[ 24]---> Sorter-cost: 359 Base: 2 2 2 2 2 2 2 2 2 c ---[ 23]---> BDD-cost: 19 c ---[ 22]---> BDD-cost: 16 c ---[ 21]---> BDD-cost: 13 c ---[ 20]---> BDD-cost: 13 c ---[ 19]---> BDD-cost: 15 c ---[ 18]---> BDD-cost: 15 c ---[ 17]---> BDD-cost: 15 c ---[ 16]---> BDD-cost: 15 c ---[ 15]---> BDD-cost: 13 c ---[ 14]---> BDD-cost: 13 c ---[ 13]---> BDD-cost: 15 c ---[ 12]---> BDD-cost: 15 c ---[ 11]---> BDD-cost: 17 c ---[ 10]---> BDD-cost: 15 c ---[ 9]---> BDD-cost: 15 c ---[ 8]---> BDD-cost: 13 c ---[ 7]---> BDD-cost: 13 c ---[ 6]---> BDD-cost: 15 c ---[ 5]---> BDD-cost: 13 c ---[ 4]---> BDD-cost: 13 c ---[ 3]---> BDD-cost: 19 c ---[ 2]---> BDD-cost: 16 c ---[ 1]---> BDD-cost: 17 c ---[ 0]---> BDD-cost: 15 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 15349 36385 | 5116 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 5885984[0m c ---[ 0]---> Sorter-cost:63755 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 78 | 192309 449611 | 64103 78 360 4.6 | 0.000 % | c | 179 | 192309 449611 | 70513 179 1995 11.1 | 0.939 % | c | 330 | 192309 449611 | 77564 330 2915 8.8 | 0.939 % | c | 555 | 192309 449611 | 85321 555 4340 7.8 | 0.939 % | c | 892 | 192309 449611 | 93853 892 6726 7.5 | 0.939 % | c | 1399 | 192309 449611 | 103238 1399 14459 10.3 | 0.939 % | c | 2158 | 192215 449400 | 113562 2155 30502 14.2 | 0.975 % | c | 3297 | 192215 449400 | 124918 3294 177563 53.9 | 0.975 % | c ============================================================================== c [1mFound solution: 4547392[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3400 | 192789 451295 | 64263 3389 179355 52.9 | 0.975 % | c | 3500 | 192789 451295 | 70689 3489 184974 53.0 | 1.010 % | c | 3651 | 192769 451250 | 77758 3639 186369 51.2 | 1.017 % | c | 3876 | 192357 450318 | 85534 3857 190287 49.3 | 1.191 % | c ============================================================================== c [1mFound solution: 4505992[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4161 | 192378 450633 | 64126 4129 197031 47.7 | 1.191 % | c | 4261 | 192378 450633 | 70538 4229 198431 46.9 | 1.360 % | c | 4411 | 192279 450409 | 77592 4377 200682 45.8 | 1.402 % | c | 4636 | 192244 450331 | 85351 4599 203524 44.3 | 1.417 % | c | 4973 | 192244 450331 | 93886 4936 248916 50.4 | 1.417 % | c | 5480 | 192244 450331 | 103275 5443 257646 47.3 | 1.417 % | c | 6239 | 192244 450331 | 113603 6202 282898 45.6 | 1.417 % | c | 7379 | 192111 450029 | 124963 7106 316426 44.5 | 1.473 % | c | 9089 | 191828 449383 | 137459 8807 401005 45.5 | 1.593 % | c | 11653 | 191808 449338 | 151205 11369 430975 37.9 | 1.600 % | c | 15499 | 191615 448906 | 166326 15206 784188 51.6 | 1.684 % | c ============================================================================== c [1mFound solution: 3607624[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 16365 | 191688 449214 | 63896 16043 812376 50.6 | 1.684 % | c ============================================================================== c [1mFound solution: 3423277[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 16372 | 191727 449409 | 63909 16050 812415 50.6 | 1.684 % | c | 16472 | 191727 449409 | 70299 16150 822793 50.9 | 1.805 % | c | 16622 | 191727 449409 | 77329 16300 832150 51.1 | 1.805 % | c | 16847 | 191727 449409 | 85062 16525 848482 51.3 | 1.805 % | c | 17185 | 191727 449409 | 93569 16863 864612 51.3 | 1.805 % | c | 17691 | 191727 449409 | 102926 17369 939920 54.1 | 1.805 % | c | 18450 | 191663 449264 | 113218 18127 990313 54.6 | 1.830 % | c ============================================================================== c [1mFound solution: 3400032[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19266 | 191676 449301 | 63892 18943 1179458 62.3 | 1.830 % | c | 19367 | 191588 449103 | 70281 19024 1183836 62.2 | 1.871 % | c | 19518 | 191416 448715 | 77309 19149 1190402 62.2 | 1.954 % | c | 19744 | 191368 448606 | 85040 19374 1203086 62.1 | 1.975 % | c | 20082 | 191368 448606 | 93544 19712 1240205 62.9 | 1.975 % | c | 20591 | 191368 448606 | 102898 20221 1291193 63.9 | 1.975 % | c | 21351 | 190404 446406 | 113188 20892 1335676 63.9 | 2.419 % | c | 22490 | 190404 446406 | 124507 22031 1452208 65.9 | 2.419 % | c | 24198 | 190404 446406 | 136958 23739 1636081 68.9 | 2.419 % | c ============================================================================== c [1mFound solution: 3367610[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 24649 | 190424 446476 | 63474 24181 1665305 68.9 | 2.419 % | c ============================================================================== c [1mFound solution: 3298476[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 24667 | 190445 446527 | 63481 24199 1665514 68.8 | 2.419 % | c | 24767 | 190445 446527 | 69829 24299 1677707 69.0 | 2.422 % | c | 24917 | 190445 446527 | 76812 24449 1680953 68.8 | 2.422 % | c | 25143 | 190445 446527 | 84493 24675 1700084 68.9 | 2.422 % | c | 25480 | 190445 446527 | 92942 25012 1704985 68.2 | 2.422 % | c | 25988 | 190445 446527 | 102236 25520 1713199 67.1 | 2.422 % | c | 26747 | 190445 446527 | 112460 26279 1847940 70.3 | 2.422 % | c | 27886 | 190408 446443 | 123706 27412 2018790 73.6 | 2.440 % | c | 29595 | 190388 446399 | 136077 29115 2098475 72.1 | 2.448 % | c ============================================================================== c [1mFound solution: 3268695[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 30664 | 190409 446461 | 63469 30181 2278674 75.5 | 2.448 % | c | 30764 | 190409 446461 | 69815 30281 2280211 75.3 | 2.457 % | c | 30915 | 190409 446461 | 76797 30432 2286100 75.1 | 2.457 % | c | 31141 | 190409 446461 | 84477 30658 2295700 74.9 | 2.457 % | c | 31478 | 190409 446461 | 92924 30995 2327171 75.1 | 2.457 % | c ============================================================================== c [1mFound solution: 3134720[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 31735 | 190420 446494 | 63473 31252 2353209 75.3 | 2.457 % | c | 31835 | 190379 446400 | 69820 31351 2358121 75.2 | 2.475 % | c | 31986 | 190379 446400 | 76802 31502 2369464 75.2 | 2.475 % | c | 32211 | 190379 446400 | 84482 31727 2395563 75.5 | 2.475 % | c | 32550 | 190379 446400 | 92930 32066 2438868 76.1 | 2.475 % | c | 33056 | 190379 446400 | 102223 32572 2483971 76.3 | 2.475 % | c | 33817 | 190379 446400 | 112446 33333 2627192 78.8 | 2.475 % | c | 34956 | 190379 446400 | 123690 34472 2710906 78.6 | 2.475 % | c | 36664 | 190317 446259 | 136060 36177 2807464 77.6 | 2.502 % | c | 39226 | 190317 446259 | 149666 38739 3106741 80.2 | 2.502 % | c | 43070 | 190317 446259 | 164632 42583 3440355 80.8 | 2.502 % | c | 48838 | 190110 445788 | 181095 48336 3908973 80.9 | 2.592 % | c | 57487 | 190110 445788 | 199205 56985 4842937 85.0 | 2.592 % | c | 70462 | 190110 445788 | 219126 69960 5996043 85.7 | 2.592 % | c ============================================================================== c [1mFound solution: 3127040[0m c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 80923 | 190122 445817 | 63374 80421 6986009 86.9 | 2.592 % | c | 81023 | 190122 445817 | 69711 21093 1212194 57.5 | 2.593 % | c | 81173 | 190122 445817 | 76682 21243 1225608 57.7 | 2.593 % | c | 81398 | 190122 445817 | 84350 21468 1245486 58.0 | 2.593 % | c | 81739 | 190122 445817 | 92785 21809 1271020 58.3 | 2.593 % | c | 82247 | 190122 445817 | 102064 22317 1310224 58.7 | 2.593 % | c | 83007 | 190122 445817 | 112270 23077 1358767 58.9 | 2.593 % | c | 84146 | 190122 445817 | 123497 24216 1430249 59.1 | 2.593 % | c | 85854 | 190122 445817 | 135847 25924 1605179 61.9 | 2.593 % | c ============================================================================== c [1mFound solution: 3059840[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 86384 | 190155 445901 | 63385 26454 1655034 62.6 | 2.593 % | c | 86484 | 190155 445901 | 69723 26554 1660764 62.5 | 2.593 % | c | 86636 | 190155 445901 | 76695 26706 1670505 62.6 | 2.593 % | c | 86863 | 190155 445901 | 84365 26933 1691632 62.8 | 2.593 % | c | 87200 | 190155 445901 | 92801 27270 1713092 62.8 | 2.593 % | c | 87711 | 190148 445886 | 102082 27780 1742338 62.7 | 2.596 % | c | 88471 | 190148 445886 | 112290 28540 1794240 62.9 | 2.596 % | c | 89614 | 190148 445886 | 123519 29683 1899441 64.0 | 2.596 % | c | 91323 | 190148 445886 | 135871 31392 2052966 65.4 | 2.596 % | c | 93886 | 190148 445886 | 149458 33955 2331342 68.7 | 2.596 % | c | 97731 | 190148 445886 | 164404 37800 2635628 69.7 | 2.596 % | c | 103499 | 190042 445647 | 180844 43566 3104488 71.3 | 2.640 % | c ============================================================================== c [1mFound solution: 3058432[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 104294 | 190008 445577 | 63336 44357 3167623 71.4 | 2.640 % | c | 104398 | 190008 445577 | 69669 44461 3169160 71.3 | 2.660 % | c | 104548 | 190008 445577 | 76636 44611 3171196 71.1 | 2.660 % | c | 104774 | 190008 445577 | 84300 44837 3199431 71.4 | 2.660 % | c | 105111 | 190008 445577 | 92730 45174 3234046 71.6 | 2.660 % | c | 105617 | 190008 445577 | 102003 45680 3273663 71.7 | 2.660 % | c | 106376 | 190008 445577 | 112203 46439 3351421 72.2 | 2.660 % | c | 107516 | 190008 445577 | 123423 47579 3467405 72.9 | 2.660 % | c | 109224 | 190008 445577 | 135766 49287 3626707 73.6 | 2.660 % | c | 111787 | 190008 445577 | 149342 51850 3823598 73.7 | 2.660 % | /oldhome/oroussel/solvers/minisat+_script: line 9: 17898 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.83 0.93 0.91 2/54 17894 Raw data (stat): 17894 (runsolver) R 17893 1269 1268 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 784601913 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+9.99918 s] Raw data (loadavg): 0.86 0.93 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+20.0002 s] Raw data (loadavg): 0.88 0.93 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+30.0007 s] Raw data (loadavg): 0.90 0.93 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+40.0014 s] Raw data (loadavg): 0.91 0.93 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+50.0025 s] Raw data (loadavg): 0.92 0.94 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+60.0017 s] Raw data (loadavg): 0.94 0.94 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+70.0028 s] Raw data (loadavg): 0.94 0.94 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+80.0034 s] Raw data (loadavg): 0.95 0.94 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+90.0037 s] Raw data (loadavg): 0.96 0.94 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+100.003 s] Raw data (loadavg): 0.97 0.94 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+110.003 s] Raw data (loadavg): 0.97 0.94 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+120.004 s] Raw data (loadavg): 0.97 0.95 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+130.004 s] Raw data (loadavg): 0.98 0.95 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+140.004 s] Raw data (loadavg): 0.98 0.95 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+150.005 s] Raw data (loadavg): 0.98 0.95 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+160.004 s] Raw data (loadavg): 0.99 0.95 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+170.004 s] Raw data (loadavg): 0.99 0.95 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+180.004 s] Raw data (loadavg): 0.99 0.95 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+190.005 s] Raw data (loadavg): 0.99 0.95 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+200.004 s] Raw data (loadavg): 0.99 0.95 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+210.004 s] Raw data (loadavg): 0.99 0.95 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+220.004 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+230.011 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+240.012 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+250.012 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+260.011 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+270.012 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+280.011 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+290.02 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+300.02 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+310.02 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+320.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+330.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+340.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+350.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+360.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+370.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+380.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+390.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+400.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+410.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+420.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+430.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+440.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+450.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+460.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+470.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+480.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+490.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+500.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+510.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+520.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+530.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+540.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+550.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+560.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+570.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+580.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+590.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+600.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+610.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+620.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+630.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+640.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+650.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+660.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+670.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+680.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+690.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+700.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+710.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+720.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+730.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+740.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+750.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+760.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+770.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+780.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+790.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+800.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+810.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+820.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+830.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+840.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+850.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+860.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+870.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+880.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+890.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+900.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+910.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+920.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+930.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+940.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+950.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+960.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+970.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+980.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+990.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1000.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1010.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1020.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1030.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1040.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1050.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1060.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1070.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1080.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1090.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1100.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1110.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1120.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1130.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1140.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1150.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1160.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1170.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1180.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1190.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1200.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1210.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1220.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1229.71 s] Raw data (loadavg): 0.99 0.97 0.91 1/53 17898 Raw data (stat): 17894 (minisat+_script) S 17893 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784601913 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 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.86 CPU user time (s): 1229.31 CPU system time (s): 0.542917 CPU usage (%): 100.012 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####