Name | normalized-opb/mps-v2-20-10/plato.asu.edu/pub/fctp/normalized-mps-v2-20-10-ran10x12.opb |
MD5SUM | 503b63cdbe2445afec2ea38c5efde5e4 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 4990860 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 3720 |
Biggest coefficient in the objective function | 5368709120 |
Number of bits for the biggest coefficient in the objective function | 33 |
Sum of the numbers in the objective function | 679702048135 |
Number of bits of the sum of numbers in the objective function | 40 |
Biggest number in a constraint | 5368709120 |
Number of bits of the biggest number in a constraint | 33 |
Biggest sum of numbers in a constraint | 679702048135 |
Number of bits of the biggest sum of numbers | 40 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1225.37 |
Number of variables | 3720 |
Total number of constraints | 142 |
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 | 142 |
Minimum length of a constraint | 31 |
Maximum length of a constraint | 360 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc20 THE 2005-05-25 20:27:41 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=22280 boxname=wulflinc20 idbench=1096 idsolver=15 numberseed=0 MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814 /oldhome/oroussel/solvers/minisat+_script MD5SUM BENCH: 503b63cdbe2445afec2ea38c5efde5e4 /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-ran10x12.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-ran10x12.opb IDLAUNCH: 22280 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.215 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.215 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: 171724 kB Buffers: 37828 kB Cached: 795136 kB SwapCached: 716 kB Active: 72576 kB Inactive: 767220 kB HighTotal: 131008 kB HighFree: 728 kB LowTotal: 903652 kB LowFree: 170996 kB SwapTotal: 2097892 kB SwapFree: 2096336 kB Dirty: 32 kB Writeback: 0 kB Mapped: 5072 kB Slab: 17496 kB Committed_AS: 63600 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-25 20:48:11 (client local time) WITH STATUS 152 IN 1229.89 SECONDS stats: 22280 7 1229.89 152 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 164 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ###################### c -- Clauses(.)/Splits(s): (none) c ---[ 162]---> Adder-cost: 288 maxlim: 104436 bits: 17/17 c ---[ 160]---> Adder-cost: 296 maxlim: 162804 bits: 18/18 c ---[ 158]---> Adder-cost: 296 maxlim: 153588 bits: 18/18 c ---[ 156]---> Adder-cost: 296 maxlim: 166900 bits: 18/18 c ---[ 154]---> Adder-cost: 288 maxlim: 110580 bits: 17/17 c ---[ 152]---> Adder-cost: 288 maxlim: 108532 bits: 17/17 c ---[ 150]---> Adder-cost: 296 maxlim: 155636 bits: 18/18 c ---[ 148]---> Adder-cost: 280 maxlim: 72692 bits: 17/17 c ---[ 146]---> Adder-cost: 280 maxlim: 72692 bits: 17/17 c ---[ 144]---> Adder-cost: 288 maxlim: 106484 bits: 17/17 c ---[ 142]---> Sorter-cost: 2306 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 140]---> Sorter-cost: 2522 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 138]---> Sorter-cost: 2522 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 136]---> Sorter-cost: 2810 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 134]---> Adder-cost: 250 maxlim: 134134 bits: 18/18 c ---[ 132]---> Sorter-cost: 2306 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 130]---> Sorter-cost: 2810 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 128]---> Sorter-cost: 2810 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 126]---> Sorter-cost: 2306 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 124]---> Sorter-cost: 2306 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 122]---> Sorter-cost: 2810 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 120]---> Sorter-cost: 2306 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 119]---> BDD-cost: 13 c ---[ 118]---> BDD-cost: 16 c ---[ 117]---> BDD-cost: 16 c ---[ 116]---> BDD-cost: 16 c ---[ 115]---> BDD-cost: 16 c ---[ 114]---> BDD-cost: 13 c ---[ 113]---> BDD-cost: 13 c ---[ 112]---> BDD-cost: 16 c ---[ 111]---> BDD-cost: 13 c ---[ 110]---> BDD-cost: 16 c ---[ 109]---> BDD-cost: 16 c ---[ 108]---> BDD-cost: 13 c ---[ 107]---> BDD-cost: 16 c ---[ 106]---> BDD-cost: 17 c ---[ 105]---> BDD-cost: 16 c ---[ 104]---> BDD-cost: 14 c ---[ 103]---> BDD-cost: 16 c ---[ 102]---> BDD-cost: 16 c ---[ 101]---> BDD-cost: 13 c ---[ 100]---> BDD-cost: 13 c ---[ 99]---> BDD-cost: 16 c ---[ 98]---> BDD-cost: 13 c ---[ 97]---> BDD-cost: 16 c ---[ 96]---> BDD-cost: 16 c ---[ 95]---> BDD-cost: 13 c ---[ 94]---> BDD-cost: 16 c ---[ 93]---> BDD-cost: 18 c ---[ 92]---> BDD-cost: 14 c ---[ 91]---> BDD-cost: 20 c ---[ 90]---> BDD-cost: 16 c ---[ 89]---> BDD-cost: 13 c ---[ 88]---> BDD-cost: 13 c ---[ 87]---> BDD-cost: 18 c ---[ 86]---> BDD-cost: 20 c ---[ 85]---> BDD-cost: 13 c ---[ 84]---> BDD-cost: 16 c ---[ 83]---> BDD-cost: 20 c ---[ 82]---> BDD-cost: 13 c ---[ 81]---> BDD-cost: 16 c ---[ 80]---> BDD-cost: 18 c ---[ 79]---> BDD-cost: 14 c ---[ 78]---> BDD-cost: 18 c ---[ 77]---> BDD-cost: 16 c ---[ 76]---> BDD-cost: 14 c ---[ 75]---> BDD-cost: 13 c ---[ 74]---> BDD-cost: 13 c ---[ 73]---> BDD-cost: 20 c ---[ 72]---> BDD-cost: 13 c ---[ 71]---> BDD-cost: 16 c ---[ 70]---> BDD-cost: 19 c ---[ 69]---> BDD-cost: 13 c ---[ 68]---> BDD-cost: 16 c ---[ 67]---> BDD-cost: 18 c ---[ 66]---> BDD-cost: 14 c ---[ 65]---> BDD-cost: 17 c ---[ 64]---> BDD-cost: 20 c ---[ 63]---> BDD-cost: 16 c ---[ 62]---> BDD-cost: 13 c ---[ 61]---> BDD-cost: 13 c ---[ 60]---> BDD-cost: 20 c ---[ 59]---> BDD-cost: 13 c ---[ 58]---> BDD-cost: 16 c ---[ 57]---> BDD-cost: 20 c ---[ 56]---> BDD-cost: 13 c ---[ 55]---> BDD-cost: 16 c ---[ 54]---> BDD-cost: 17 c ---[ 53]---> BDD-cost: 15 c ---[ 52]---> BDD-cost: 14 c ---[ 51]---> BDD-cost: 15 c ---[ 50]---> BDD-cost: 15 c ---[ 49]---> BDD-cost: 13 c ---[ 48]---> BDD-cost: 13 c ---[ 47]---> BDD-cost: 15 c ---[ 46]---> BDD-cost: 13 c ---[ 45]---> BDD-cost: 16 c ---[ 44]---> BDD-cost: 15 c ---[ 43]---> BDD-cost: 13 c ---[ 42]---> BDD-cost: 13 c ---[ 41]---> BDD-cost: 16 c ---[ 40]---> BDD-cost: 17 c ---[ 39]---> BDD-cost: 14 c ---[ 38]---> BDD-cost: 17 c ---[ 37]---> BDD-cost: 17 c ---[ 36]---> BDD-cost: 13 c ---[ 35]---> BDD-cost: 13 c ---[ 34]---> BDD-cost: 17 c ---[ 33]---> BDD-cost: 13 c ---[ 32]---> BDD-cost: 13 c ---[ 31]---> BDD-cost: 16 c ---[ 30]---> BDD-cost: 17 c ---[ 29]---> BDD-cost: 13 c ---[ 28]---> BDD-cost: 16 c ---[ 27]---> BDD-cost: 18 c ---[ 26]---> BDD-cost: 14 c ---[ 25]---> BDD-cost: 18 c ---[ 24]---> BDD-cost: 16 c ---[ 23]---> BDD-cost: 13 c ---[ 22]---> BDD-cost: 13 c ---[ 21]---> BDD-cost: 17 c ---[ 20]---> BDD-cost: 18 c ---[ 19]---> BDD-cost: 13 c ---[ 18]---> BDD-cost: 16 c ---[ 17]---> BDD-cost: 18 c ---[ 16]---> BDD-cost: 13 c ---[ 15]---> BDD-cost: 16 c ---[ 14]---> BDD-cost: 16 c ---[ 13]---> BDD-cost: 14 c ---[ 12]---> BDD-cost: 16 c ---[ 11]---> BDD-cost: 16 c ---[ 10]---> BDD-cost: 13 c ---[ 9]---> BDD-cost: 13 c ---[ 8]---> BDD-cost: 13 c ---[ 7]---> BDD-cost: 16 c ---[ 6]---> BDD-cost: 13 c ---[ 5]---> BDD-cost: 16 c ---[ 4]---> BDD-cost: 16 c ---[ 3]---> BDD-cost: 13 c ---[ 2]---> BDD-cost: 16 c ---[ 1]---> BDD-cost: 16 c ---[ 0]---> BDD-cost: 14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 96880 253132 | 32293 0 0 nan | 0.000 % | c | 100 | 96880 253132 | 35522 100 458 4.6 | 9.494 % | c | 251 | 96457 252165 | 39074 243 1073 4.4 | 9.910 % | c | 476 | 96457 252165 | 42981 468 2209 4.7 | 9.909 % | c | 813 | 96385 252002 | 47280 779 3687 4.7 | 9.971 % | c | 1319 | 96378 251979 | 52008 1283 6071 4.7 | 9.975 % | c | 2078 | 96378 251979 | 57209 2042 9944 4.9 | 9.975 % | c | 3217 | 96058 251229 | 62929 3145 15220 4.8 | 10.241 % | c | 4925 | 95806 250641 | 69222 4812 23669 4.9 | 10.461 % | c | 7487 | 94956 248615 | 76145 7324 35668 4.9 | 11.240 % | c | 11331 | 93657 245527 | 83759 11107 56727 5.1 | 12.455 % | c | 17097 | 92446 242685 | 92135 16756 88900 5.3 | 13.577 % | c | 25746 | 91652 240694 | 101349 25290 160050 6.3 | 14.272 % | c ============================================================================== c [1mFound solution: 24178633[0m c ---[ 0]---> Adder-cost: 5970 maxlim: 7187902 bits: 24/23 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 31583 | 132712 388142 | 44237 31052 211285 6.8 | 14.272 % | c | 31683 | 132712 388142 | 48660 31152 211858 6.8 | 12.579 % | c | 31833 | 132712 388142 | 53526 31302 212768 6.8 | 12.579 % | c | 32058 | 132712 388142 | 58879 31527 214162 6.8 | 12.579 % | c | 32395 | 132712 388142 | 64767 31864 216577 6.8 | 12.579 % | c | 32901 | 132712 388142 | 71244 32370 223562 6.9 | 12.579 % | c | 33660 | 132583 387797 | 78368 33118 230861 7.0 | 12.678 % | c | 34799 | 132557 387736 | 86205 34256 244051 7.1 | 12.705 % | c ============================================================================== c [1mFound solution: 23768415[0m c ---[ 0]---> Adder-cost: 0 maxlim: 7598120 bits: 24/23 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 36083 | 132581 387925 | 44193 35540 256279 7.2 | 12.705 % | c | 36183 | 132581 387925 | 48612 35640 256904 7.2 | 12.727 % | c | 36334 | 132581 387925 | 53473 35791 258507 7.2 | 12.727 % | c | 36559 | 132581 387925 | 58820 36016 260752 7.2 | 12.727 % | c | 36896 | 132581 387925 | 64702 36353 263791 7.3 | 12.727 % | c | 37402 | 132581 387925 | 71173 36859 268441 7.3 | 12.727 % | c | 38163 | 132581 387925 | 78290 37620 274818 7.3 | 12.727 % | c | 39302 | 132581 387925 | 86119 38759 311473 8.0 | 12.727 % | c ============================================================================== c [1mFound solution: 22939841[0m c ---[ 0]---> Adder-cost: 2 maxlim: 8426694 bits: 25/24 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 40740 | 132613 388159 | 44204 40197 351381 8.7 | 12.727 % | c | 40840 | 132605 388141 | 48624 40296 351977 8.7 | 12.755 % | c | 40990 | 132605 388141 | 53486 40446 352943 8.7 | 12.755 % | c | 41215 | 132590 388107 | 58835 40670 354136 8.7 | 12.768 % | c | 41553 | 132590 388107 | 64719 41008 356177 8.7 | 12.768 % | c | 42059 | 132581 388087 | 71190 41513 359436 8.7 | 12.773 % | c | 42818 | 132517 387929 | 78310 42270 366696 8.7 | 12.828 % | c | 43957 | 132443 387758 | 86141 43407 382281 8.8 | 12.891 % | c | 45665 | 132443 387758 | 94755 45115 576623 12.8 | 12.891 % | c ============================================================================== c [1mFound solution: 18046835[0m c ---[ 0]---> Adder-cost: 0 maxlim: 13319700 bits: 25/24 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 46485 | 132443 387909 | 44147 45934 587360 12.8 | 12.891 % | c | 46585 | 132172 387280 | 48561 46016 588036 12.8 | 13.161 % | c | 46735 | 132138 387201 | 53417 46156 589084 12.8 | 13.187 % | c | 46960 | 132138 387201 | 58759 46381 594958 12.8 | 13.187 % | c | 47299 | 132138 387201 | 64635 46720 600104 12.8 | 13.187 % | c | 47805 | 132138 387201 | 71099 47226 639826 13.5 | 13.187 % | c | 48564 | 132127 387174 | 78209 47978 648201 13.5 | 13.195 % | c | 49703 | 132127 387174 | 86030 49117 677009 13.8 | 13.195 % | c | 51411 | 132127 387174 | 94633 50825 723676 14.2 | 13.195 % | c | 53973 | 132111 387130 | 104096 53384 790269 14.8 | 13.205 % | c | 57820 | 132111 387130 | 114505 57231 911630 15.9 | 13.205 % | c ============================================================================== c [1mFound solution: 17731408[0m c ---[ 0]---> Adder-cost: 0 maxlim: 13635127 bits: 25/24 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 59459 | 132117 387240 | 44039 58869 966378 16.4 | 13.205 % | c | 59560 | 132060 387108 | 48442 23669 367940 15.5 | 13.269 % | c | 59710 | 132060 387108 | 53287 23819 368761 15.5 | 13.269 % | c | 59935 | 132060 387108 | 58615 24044 370999 15.4 | 13.269 % | c | 60272 | 132060 387108 | 64477 24381 373210 15.3 | 13.269 % | c | 60778 | 132044 387070 | 70925 24885 376034 15.1 | 13.305 % | c | 61537 | 132013 386997 | 78017 25642 385556 15.0 | 13.311 % | c | 62676 | 131926 386788 | 85819 26770 395269 14.8 | 13.379 % | c | 64384 | 131926 386788 | 94401 28478 473358 16.6 | 13.379 % | c | 66946 | 131869 386658 | 103841 31034 588776 19.0 | 13.423 % | c | 70792 | 131824 386548 | 114225 34873 627844 18.0 | 13.460 % | c | 76558 | 131796 386484 | 125648 40636 790708 19.5 | 13.486 % | c | 85209 | 131782 386452 | 138213 49286 1236638 25.1 | 13.499 % | c ============================================================================== c [1mFound solution: 15591890[0m c ---[ 0]---> Adder-cost: 0 maxlim: 15774645 bits: 25/24 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 90963 | 131673 386364 | 43891 55030 1338064 24.3 | 13.499 % | c | 91063 | 131673 386364 | 48280 26122 491684 18.8 | 13.635 % | c | 91214 | 131673 386364 | 53108 26273 492464 18.7 | 13.635 % | c | 91439 | 131660 386334 | 58418 26497 493893 18.6 | 13.646 % | c | 91776 | 131660 386334 | 64260 26834 498037 18.6 | 13.646 % | c | 92283 | 131578 386147 | 70686 27335 500616 18.3 | 13.711 % | c | 93042 | 131578 386147 | 77755 28094 506461 18.0 | 13.711 % | c | 94181 | 131578 386147 | 85531 29233 514851 17.6 | 13.711 % | c | 95889 | 131410 385759 | 94084 30917 534891 17.3 | 13.847 % | c | 98451 | 131410 385759 | 103492 33479 596504 17.8 | 13.847 % | c | 102295 | 131410 385759 | 113841 37323 996931 26.7 | 13.847 % | c | 108064 | 131410 385759 | 125226 43092 1352018 31.4 | 13.847 % | c | 116715 | 131410 385759 | 137748 51743 1688999 32.6 | 13.847 % | c | 129691 | 131410 385759 | 151523 64719 3482086 53.8 | 13.847 % | c | 149152 | 131410 385759 | 166675 84180 4487700 53.3 | 13.847 % | c | 178344 | 131378 385666 | 183343 113364 6003263 53.0 | 13.862 % | c ============================================================================== c [1mFound solution: 11587982[0m c ---[ 0]---> Adder-cost: 0 maxlim: 19778553 bits: 25/25 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 217248 | 131190 384893 | 43730 152100 8303042 54.6 | 13.862 % | c | 217349 | 131001 384457 | 48103 29148 881289 30.2 | 14.182 % | c | 217499 | 131001 384457 | 52913 29298 883121 30.1 | 14.182 % | c | 217724 | 131001 384457 | 58204 29523 884793 30.0 | 14.182 % | c | 218061 | 131001 384457 | 64025 29860 886693 29.7 | 14.182 % | c | 218567 | 131001 384457 | 70427 30366 890262 29.3 | 14.182 % | c | 219326 | 130907 384241 | 77470 31099 916109 29.5 | 14.250 % | c | 220465 | 130907 384241 | 85217 32238 932696 28.9 | 14.250 % | c | 222173 | 130907 384241 | 93739 33946 1101358 32.4 | 14.250 % | c | 224736 | 130907 384241 | 103113 36509 1181379 32.4 | 14.250 % | c | 228581 | 130907 384241 | 113424 40354 1374959 34.1 | 14.250 % | c | 234348 | 130857 384129 | 124766 46112 1772603 38.4 | 14.287 % | c | 242997 | 130699 383760 | 137243 54755 2436039 44.5 | 14.417 % | c | 255973 | 130583 383487 | 150967 67724 3358510 49.6 | 14.524 % | c | 275438 | 130568 383451 | 166064 87187 4467068 51.2 | 14.540 % | c | 304632 | 130550 383409 | 182671 116380 6775666 58.2 | 14.553 % | c | 348422 | 130544 383389 | 200938 160169 14025041 87.6 | 14.556 % | c | 414106 | 130532 383361 | 221031 225852 22603575 100.1 | 14.569 % | /oldhome/oroussel/solvers/minisat+_script: line 9: 8630 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.92 0.95 0.90 2/54 8626 Raw data (stat): 8626 (runsolver) R 8625 25399 25398 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 841756101 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 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+9.99993 s] Raw data (loadavg): 0.93 0.96 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+20.0012 s] Raw data (loadavg): 0.94 0.96 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+30.0017 s] Raw data (loadavg): 0.95 0.96 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+40.0011 s] Raw data (loadavg): 0.96 0.96 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+50.0024 s] Raw data (loadavg): 0.96 0.96 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+60.0028 s] Raw data (loadavg): 0.97 0.96 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+70.0033 s] Raw data (loadavg): 0.97 0.96 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+80.0043 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+90.004 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+100.004 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+110.004 s] Raw data (loadavg): 0.98 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+120.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+130.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+140.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+150.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+160.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+170.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+180.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+190.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+200.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+210.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+220.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+230.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+240.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+250.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+260.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+270.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+280.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+290.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+300.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+310.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+320.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+330.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+340.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+350.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+360.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+370.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+380.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+390.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+400.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+410.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+420.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+430.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+440.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+450.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+460.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+470.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+480.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+490.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+500.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+510.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+520.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+530.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+540.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+550.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+560.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+570.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+580.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+590.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+600.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+610.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+620.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+630.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+640.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+650.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+660.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+670.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+680.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+690.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+700.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+710.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+720.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+730.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+740.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+750.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+760.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+770.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+780.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+790.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+800.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+810.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+820.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+830.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+840.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+850.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+860.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+870.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+880.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+890.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+900.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+910.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+920.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+930.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+940.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+950.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+960.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+970.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+980.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+990.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1000.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1010.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1020.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1030.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1040.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1050.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1060.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1070.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1080.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1090.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1100.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1110.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1120.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1130.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1140.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1150.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1160.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1170.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1180.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1190.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1200.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1210.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1220.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1229.74 s] Raw data (loadavg): 0.99 0.97 0.91 1/53 8630 Raw data (stat): 8626 (minisat+_script) S 8625 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841756101 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 0 Child status: 152 Real time (s): 1229.74 CPU time (s): 1229.89 CPU user time (s): 1228.95 CPU system time (s): 0.938857 CPU usage (%): 100.012 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####