Name | normalized-opb/mps-v2-20-10/plato.asu.edu/pub/fctp/normalized-mps-v2-20-10-gr4x6.opb |
MD5SUM | d90fce7408f7990dccb3ba4f8fa1c8f6 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 23403520 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 744 |
Biggest coefficient in the objective function | 151934468096 |
Number of bits for the biggest coefficient in the objective function | 38 |
Sum of the numbers in the objective function | 3470370333536 |
Number of bits of the sum of numbers in the objective function | 42 |
Biggest number in a constraint | 151934468096 |
Number of bits of the biggest number in a constraint | 38 |
Biggest sum of numbers in a constraint | 3470370333536 |
Number of bits of the biggest sum of numbers | 42 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1247.15 |
Number of variables | 744 |
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 | 31 |
Maximum length of a constraint | 180 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc24 THE 2005-05-27 07:46:22 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=23433 boxname=wulflinc24 idbench=1077 idsolver=16 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: d90fce7408f7990dccb3ba4f8fa1c8f6 /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-gr4x6.opb REAL COMMAND: minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-gr4x6.opb IDLAUNCH: 23433 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.080 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.080 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: 902744 kB Buffers: 4920 kB Cached: 105876 kB SwapCached: 588 kB Active: 18364 kB Inactive: 94544 kB HighTotal: 131008 kB HighFree: 22540 kB LowTotal: 903652 kB LowFree: 880204 kB SwapTotal: 2097892 kB SwapFree: 2096412 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5152 kB Slab: 13360 kB Committed_AS: 63604 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-27 08:06:52 (client local time) WITH STATUS 152 IN 1229.87 SECONDS stats: 23433 7 1229.87 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]---> BDD-cost: 648 c ---[ 40]---> BDD-cost: 641 c ---[ 38]---> BDD-cost: 616 c ---[ 36]---> BDD-cost: 588 c ---[ 34]---> BDD-cost: 300 c ---[ 32]---> BDD-cost: 290 c ---[ 30]---> BDD-cost: 290 c ---[ 28]---> BDD-cost: 270 c ---[ 26]---> BDD-cost: 243 c ---[ 24]---> BDD-cost: 243 c ---[ 23]---> BDD-cost: 22 c ---[ 22]---> BDD-cost: 19 c ---[ 21]---> BDD-cost: 16 c ---[ 20]---> BDD-cost: 16 c ---[ 19]---> BDD-cost: 18 c ---[ 18]---> BDD-cost: 18 c ---[ 17]---> BDD-cost: 18 c ---[ 16]---> BDD-cost: 18 c ---[ 15]---> BDD-cost: 16 c ---[ 14]---> BDD-cost: 16 c ---[ 13]---> BDD-cost: 18 c ---[ 12]---> BDD-cost: 18 c ---[ 11]---> BDD-cost: 20 c ---[ 10]---> BDD-cost: 18 c ---[ 9]---> BDD-cost: 18 c ---[ 8]---> BDD-cost: 16 c ---[ 7]---> BDD-cost: 16 c ---[ 6]---> BDD-cost: 18 c ---[ 5]---> BDD-cost: 16 c ---[ 4]---> BDD-cost: 16 c ---[ 3]---> BDD-cost: 22 c ---[ 2]---> BDD-cost: 19 c ---[ 1]---> BDD-cost: 20 c ---[ 0]---> BDD-cost: 18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 11617 32387 | 3872 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 48691753[0m c ---[ 0]---> Sorter-cost:80611 Base: 2 2 2 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 | 5 | 236688 557920 | 78896 5 55 11.0 | 0.000 % | c | 105 | 236688 557920 | 86785 105 1411 13.4 | 0.514 % | c | 259 | 236688 557920 | 95464 259 5125 19.8 | 0.514 % | c | 485 | 236486 557468 | 105010 482 7402 15.4 | 0.577 % | c | 822 | 236463 557417 | 115511 817 9236 11.3 | 0.585 % | c ============================================================================== c [1mFound solution: 45575547[0m c ---[ 0]---> Sorter-cost: 19 Base: 2 2 2 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 | 917 | 237945 561642 | 79315 912 10999 12.1 | 0.585 % | c | 1017 | 237945 561642 | 87246 1012 14323 14.2 | 0.582 % | c | 1167 | 237945 561642 | 95971 1162 20550 17.7 | 0.582 % | c | 1392 | 237945 561642 | 105568 1387 25337 18.3 | 0.582 % | c | 1729 | 237945 561642 | 116125 1724 38211 22.2 | 0.582 % | c ============================================================================== c [1mFound solution: 40055195[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 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 | 1931 | 238258 562586 | 79419 1925 43078 22.4 | 0.582 % | c | 2031 | 238258 562586 | 87360 2025 43804 21.6 | 0.587 % | c | 2181 | 238174 562395 | 96096 2172 45567 21.0 | 0.617 % | c ============================================================================== c [1mFound solution: 30202779[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 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 | 2215 | 238578 563394 | 79526 2206 46578 21.1 | 0.617 % | c | 2315 | 238578 563394 | 87478 2306 47489 20.6 | 0.617 % | c | 2465 | 238578 563394 | 96226 2456 48371 19.7 | 0.617 % | c | 2691 | 238578 563394 | 105849 2682 50888 19.0 | 0.617 % | c | 3028 | 238578 563394 | 116434 3019 53766 17.8 | 0.617 % | c | 3535 | 238578 563394 | 128077 3526 59212 16.8 | 0.617 % | c | 4294 | 238578 563394 | 140885 4285 74604 17.4 | 0.617 % | c | 5434 | 238578 563394 | 154973 5425 130319 24.0 | 0.617 % | c ============================================================================== c [1mFound solution: 28809484[0m c ---[ 0]---> Sorter-cost: 20 Base: 2 2 2 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 | 6105 | 238644 563626 | 79548 6096 239376 39.3 | 0.617 % | c | 6205 | 238623 563581 | 87502 6195 244741 39.5 | 0.625 % | c | 6359 | 237961 562076 | 96253 6321 253317 40.1 | 0.848 % | c | 6585 | 237961 562076 | 105878 6547 262281 40.1 | 0.848 % | c | 6922 | 237961 562076 | 116466 6884 305812 44.4 | 0.848 % | c | 7429 | 237672 561417 | 128112 7387 333070 45.1 | 0.953 % | c ============================================================================== c [1mFound solution: 28111150[0m c ---[ 0]---> Sorter-cost: 20 Base: 2 2 2 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 | 7735 | 237700 561493 | 79233 7693 362688 47.1 | 0.953 % | c | 7837 | 237691 561474 | 87156 7791 366681 47.1 | 0.958 % | c | 7988 | 237691 561474 | 95871 7942 369138 46.5 | 0.958 % | c | 8214 | 237691 561474 | 105459 8168 392009 48.0 | 0.958 % | c | 8551 | 237691 561474 | 116005 8505 394331 46.4 | 0.958 % | c | 9057 | 237606 561278 | 127605 9008 505126 56.1 | 0.987 % | c ============================================================================== c [1mFound solution: 27973568[0m c ---[ 0]---> Sorter-cost: 19 Base: 2 2 2 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 | 9601 | 237434 560955 | 79144 9547 536925 56.2 | 0.987 % | c | 9701 | 237247 560538 | 87058 9646 537698 55.7 | 1.117 % | c | 9851 | 237247 560538 | 95764 9796 541141 55.2 | 1.117 % | c | 10076 | 237199 560429 | 105340 10017 543135 54.2 | 1.134 % | c | 10413 | 237125 560262 | 115874 10352 583135 56.3 | 1.157 % | c | 10919 | 237081 560162 | 127462 10857 598701 55.1 | 1.171 % | c | 11678 | 236932 559819 | 140208 11614 693529 59.7 | 1.226 % | c | 12819 | 236799 559516 | 154229 12743 850777 66.8 | 1.273 % | c | 14530 | 236562 558977 | 169652 14429 995265 69.0 | 1.360 % | c | 17094 | 236562 558977 | 186617 16993 1115259 65.6 | 1.360 % | c ============================================================================== c [1mFound solution: 27222016[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 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 | 19004 | 236596 559067 | 78865 18903 1485651 78.6 | 1.360 % | c | 19104 | 236500 558852 | 86751 19000 1486489 78.2 | 1.391 % | c | 19254 | 236500 558852 | 95426 19150 1487266 77.7 | 1.391 % | c | 19479 | 236500 558852 | 104969 19375 1488847 76.8 | 1.391 % | c | 19816 | 236500 558852 | 115466 19712 1492868 75.7 | 1.391 % | c | 20322 | 236500 558852 | 127012 20218 1568395 77.6 | 1.391 % | c | 21081 | 236500 558852 | 139714 20977 1766583 84.2 | 1.391 % | c ============================================================================== c [1mFound solution: 26855680[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 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 | 21639 | 236519 558900 | 78839 21535 1816938 84.4 | 1.391 % | c | 21741 | 236519 558900 | 86722 21637 1819285 84.1 | 1.392 % | c | 21891 | 236519 558900 | 95395 21787 1820885 83.6 | 1.392 % | c | 22116 | 236519 558900 | 104934 22012 1822961 82.8 | 1.392 % | c | 22453 | 236519 558900 | 115428 22349 1826350 81.7 | 1.392 % | c | 22959 | 236021 557774 | 126970 22806 1834705 80.4 | 1.564 % | c | 23719 | 236021 557774 | 139668 23566 1893709 80.4 | 1.564 % | c | 24859 | 236021 557774 | 153634 24706 2067506 83.7 | 1.564 % | c | 26567 | 236021 557774 | 168998 26414 2186803 82.8 | 1.564 % | c | 29129 | 236021 557774 | 185898 28976 2705628 93.4 | 1.564 % | c ============================================================================== c [1mFound solution: 25936064[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 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 | 32463 | 236052 557857 | 78684 32310 3253581 100.7 | 1.564 % | c | 32563 | 236052 557857 | 86552 32410 3256165 100.5 | 1.565 % | c | 32713 | 235948 557623 | 95207 32551 3257448 100.1 | 1.599 % | c | 32939 | 235948 557623 | 104728 32777 3259317 99.4 | 1.599 % | c | 33276 | 235948 557623 | 115201 33114 3277087 99.0 | 1.599 % | c | 33782 | 235948 557623 | 126721 33620 3330355 99.1 | 1.599 % | c | 34542 | 235948 557623 | 139393 34380 3421927 99.5 | 1.599 % | c ============================================================================== c [1mFound solution: 24208395[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 2 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 | 35475 | 235989 557726 | 78663 35313 3454165 97.8 | 1.599 % | c ============================================================================== c [1mFound solution: 24208384[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 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 | 35533 | 236004 557765 | 78668 35371 3468959 98.1 | 1.599 % | c | 35634 | 236004 557765 | 86534 35472 3470838 97.8 | 1.601 % | c | 35785 | 236004 557765 | 95188 35623 3472153 97.5 | 1.601 % | c | 36010 | 235997 557751 | 104707 35847 3473649 96.9 | 1.606 % | c | 36349 | 235997 557751 | 115177 36186 3484885 96.3 | 1.606 % | c | 36855 | 235997 557751 | 126695 36692 3494565 95.2 | 1.606 % | c | 37614 | 235763 557224 | 139365 36810 3494663 94.9 | 1.684 % | c | 38753 | 235557 556758 | 153301 37394 3536838 94.6 | 1.753 % | c | 40464 | 235557 556758 | 168631 39105 3672650 93.9 | 1.753 % | c | 43026 | 235557 556758 | 185495 41667 3938637 94.5 | 1.753 % | c | 46872 | 235557 556758 | 204044 45513 4363177 95.9 | 1.753 % | c | 52639 | 235497 556624 | 224448 51275 4800457 93.6 | 1.776 % | c | 61290 | 235451 556520 | 246893 59925 5595278 93.4 | 1.792 % | c | 74265 | 235451 556520 | 271583 72900 7313023 100.3 | 1.792 % | c | 93726 | 235451 556520 | 298741 92361 9922891 107.4 | 1.792 % | /oldhome/oroussel/solvers/minisat+_script: line 9: 1877 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.87 0.95 0.91 2/54 1873 Raw data (stat): 1873 (runsolver) R 1872 4613 4612 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 854467936 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0003 s] Raw data (loadavg): 0.89 0.95 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+20.0027 s] Raw data (loadavg): 0.91 0.96 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+30.003 s] Raw data (loadavg): 0.92 0.96 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+40.0024 s] Raw data (loadavg): 0.93 0.96 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+50.0031 s] Raw data (loadavg): 0.94 0.96 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+60.0028 s] Raw data (loadavg): 0.95 0.96 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+70.0025 s] Raw data (loadavg): 0.96 0.96 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+80.0035 s] Raw data (loadavg): 0.96 0.96 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+90.0028 s] Raw data (loadavg): 0.97 0.96 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+100.003 s] Raw data (loadavg): 0.97 0.96 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+110.002 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+120.002 s] Raw data (loadavg): 0.98 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+130.002 s] Raw data (loadavg): 0.98 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+140.006 s] Raw data (loadavg): 0.98 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+150.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+160.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+170.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+180.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+190.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+200.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+210.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+220.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+230.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+240.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+250.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+260.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+270.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+280.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+290.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+300.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+310.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+320.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+330.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+340.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+350.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+360.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+370.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+380.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+390.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+400.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+410.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+420.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+430.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+440.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+450.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+460.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+470.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+480.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+490.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+500.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+510.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+520.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+530.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+540.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+550.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+560.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+570.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+580.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+590.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+600.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+610.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+620.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+630.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+640.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+650.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+660.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+670.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+680.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+690.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+700.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+710.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+720.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+730.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+740.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+750.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+760.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+770.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+780.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+790.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+800.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+810.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+820.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 1877 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+830.057 s] Raw data (loadavg): 1.07 0.99 0.91 3/58 1886 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+840.068 s] Raw data (loadavg): 1.36 1.05 0.94 2/55 1930 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+850.069 s] Raw data (loadavg): 1.31 1.05 0.94 2/55 1930 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+860.069 s] Raw data (loadavg): 1.26 1.05 0.94 2/55 1930 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+870.068 s] Raw data (loadavg): 1.22 1.05 0.94 2/55 1930 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+880.069 s] Raw data (loadavg): 1.18 1.04 0.94 2/55 1930 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+890.069 s] Raw data (loadavg): 1.16 1.04 0.94 2/55 1930 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+900.069 s] Raw data (loadavg): 1.13 1.04 0.94 2/55 1930 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+910.07 s] Raw data (loadavg): 1.11 1.04 0.94 2/55 1932 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+920.07 s] Raw data (loadavg): 1.09 1.04 0.94 2/55 1932 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+930.07 s] Raw data (loadavg): 1.08 1.04 0.94 2/55 1932 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+940.07 s] Raw data (loadavg): 1.07 1.03 0.94 2/55 1932 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+950.071 s] Raw data (loadavg): 1.06 1.03 0.94 2/55 1932 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+960.07 s] Raw data (loadavg): 1.05 1.03 0.94 2/55 1932 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+970.07 s] Raw data (loadavg): 1.04 1.03 0.94 2/55 1932 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+980.071 s] Raw data (loadavg): 1.03 1.03 0.94 2/55 1932 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+990.07 s] Raw data (loadavg): 1.03 1.03 0.94 2/55 1932 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1000.07 s] Raw data (loadavg): 1.02 1.03 0.94 2/55 1932 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1010.07 s] Raw data (loadavg): 1.02 1.02 0.94 2/55 1932 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1020.07 s] Raw data (loadavg): 1.02 1.02 0.94 2/55 1932 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1030.07 s] Raw data (loadavg): 1.01 1.02 0.94 2/55 1932 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1040.07 s] Raw data (loadavg): 1.01 1.02 0.94 2/55 1932 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1050.07 s] Raw data (loadavg): 1.01 1.02 0.94 2/55 1932 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1060.07 s] Raw data (loadavg): 1.01 1.02 0.94 2/55 1932 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1070.07 s] Raw data (loadavg): 1.00 1.02 0.94 2/55 1932 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1080.07 s] Raw data (loadavg): 1.00 1.02 0.94 2/55 1932 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1090.07 s] Raw data (loadavg): 1.00 1.02 0.94 2/55 1932 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1100.07 s] Raw data (loadavg): 1.00 1.02 0.94 2/55 1932 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1110.07 s] Raw data (loadavg): 1.00 1.01 0.94 2/55 1932 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1120.07 s] Raw data (loadavg): 1.00 1.01 0.94 2/55 1932 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1130.07 s] Raw data (loadavg): 1.00 1.01 0.94 2/55 1932 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1140.07 s] Raw data (loadavg): 1.00 1.01 0.94 2/55 1932 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1150.07 s] Raw data (loadavg): 1.00 1.01 0.94 2/55 1932 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1160.07 s] Raw data (loadavg): 1.00 1.01 0.94 2/55 1932 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1170.07 s] Raw data (loadavg): 1.00 1.01 0.94 2/55 1932 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1180.07 s] Raw data (loadavg): 1.00 1.01 0.94 2/55 1932 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1190.07 s] Raw data (loadavg): 1.00 1.01 0.94 2/55 1932 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1200.07 s] Raw data (loadavg): 1.00 1.01 0.94 2/55 1932 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1210.07 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 1934 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1220.07 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 1934 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1229.7 s] Raw data (loadavg): 1.00 1.00 0.94 1/53 1934 Raw data (stat): 1873 (minisat+_script) S 1872 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854467936 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 0 Child status: 152 Real time (s): 1229.7 CPU time (s): 1229.87 CPU user time (s): 1229.23 CPU system time (s): 0.635903 CPU usage (%): 100.013 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####