Name | normalized-opb/mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-markshare1.opb |
MD5SUM | 10386fd19d9976c249ce2be861b38a70 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 63488 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 180 |
Biggest coefficient in the objective function | 536870912 |
Number of bits for the biggest coefficient in the objective function | 30 |
Sum of the numbers in the objective function | 6442450938 |
Number of bits of the sum of numbers in the objective function | 33 |
Biggest number in a constraint | 536870912 |
Number of bits of the biggest number in a constraint | 30 |
Biggest sum of numbers in a constraint | 6442450938 |
Number of bits of the biggest sum of numbers | 33 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1175.12 |
Number of variables | 230 |
Total number of constraints | 56 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 50 |
Number of constraints which are nor clauses,nor cardinality constraints | 6 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 80 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc17 THE 2005-05-27 07:02:44 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=23329 boxname=wulflinc17 idbench=973 idsolver=16 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 10386fd19d9976c249ce2be861b38a70 /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-markshare1.opb REAL COMMAND: minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-markshare1.opb IDLAUNCH: 23329 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.072 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.072 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: 810564 kB Buffers: 33308 kB Cached: 169628 kB SwapCached: 520 kB Active: 47956 kB Inactive: 157128 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 810312 kB SwapTotal: 2097892 kB SwapFree: 2096560 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5296 kB Slab: 13256 kB Committed_AS: 63604 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-27 07:23:14 (client local time) WITH STATUS 152 IN 1229.87 SECONDS stats: 23329 7 1229.87 152 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 12 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ###### c -- Clauses(.)/Splits(s): (none) c ---[ 10]---> BDD-cost:23440 c ---[ 8]---> BDD-cost:28410 c ---[ 6]---> BDD-cost:25975 c ---[ 4]---> BDD-cost:24801 c ---[ 2]---> BDD-cost:25034 c ---[ 0]---> BDD-cost:24120 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 436767 1274769 | 145589 0 0 nan | 0.000 % | c | 101 | 436767 1274769 | 160147 101 7599 75.2 | 0.040 % | c ============================================================================== c [1mFound solution: 6404096[0m c ---[ 0]---> Sorter-cost: 1725 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 101 | 441175 1285058 | 147058 101 7599 75.2 | 0.040 % | c ============================================================================== c [1mFound solution: 5898240[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 102 | 441198 1285135 | 147066 102 7622 74.7 | 0.040 % | c ============================================================================== c [1mFound solution: 5855232[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 125 | 441212 1285169 | 147070 125 9078 72.6 | 0.040 % | c ============================================================================== c [1mFound solution: 5680128[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 139 | 441234 1285220 | 147078 139 9626 69.3 | 0.040 % | c ============================================================================== c [1mFound solution: 5663744[0m c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 186 | 441243 1285242 | 147081 186 11744 63.1 | 0.040 % | c ============================================================================== c [1mFound solution: 5647360[0m c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 268 | 441251 1285261 | 147083 268 15602 58.2 | 0.040 % | c ============================================================================== c [1mFound solution: 5596160[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 307 | 441266 1285297 | 147088 307 17285 56.3 | 0.040 % | c ============================================================================== c [1mFound solution: 5487616[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 382 | 441275 1285321 | 147091 382 20883 54.7 | 0.040 % | c | 482 | 441275 1285321 | 161800 482 24693 51.2 | 0.044 % | c | 632 | 441275 1285321 | 177980 632 30326 48.0 | 0.044 % | c ============================================================================== c [1mFound solution: 5464064[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 730 | 441287 1285350 | 147095 730 35225 48.3 | 0.044 % | c | 830 | 441287 1285350 | 161804 830 39533 47.6 | 0.045 % | c ============================================================================== c [1mFound solution: 5440512[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 904 | 441297 1285373 | 147099 904 43500 48.1 | 0.045 % | c ============================================================================== c [1mFound solution: 5271552[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 978 | 441308 1285399 | 147102 978 46652 47.7 | 0.045 % | c | 1078 | 441308 1285399 | 161812 1078 50655 47.0 | 0.046 % | c | 1229 | 441308 1285399 | 177993 1229 57259 46.6 | 0.046 % | c | 1457 | 441308 1285399 | 195792 1457 68298 46.9 | 0.046 % | c | 1796 | 441308 1285399 | 215372 1796 83053 46.2 | 0.046 % | c | 2303 | 441308 1285399 | 236909 2303 106417 46.2 | 0.046 % | c ============================================================================== c [1mFound solution: 5121024[0m c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2367 | 441325 1285442 | 147108 2367 109675 46.3 | 0.046 % | c | 2468 | 441325 1285442 | 161818 2468 113846 46.1 | 0.047 % | c ============================================================================== c [1mFound solution: 5060608[0m c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2522 | 441335 1285468 | 147111 2522 116155 46.1 | 0.047 % | c | 2623 | 441335 1285468 | 161822 2623 119822 45.7 | 0.048 % | c | 2776 | 441335 1285468 | 178004 2776 131258 47.3 | 0.048 % | c ============================================================================== c [1mFound solution: 5022720[0m c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2826 | 441345 1285492 | 147115 2826 133538 47.3 | 0.048 % | c | 2926 | 441345 1285492 | 161826 2926 137038 46.8 | 0.048 % | c ============================================================================== c [1mFound solution: 4892672[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2993 | 441361 1285530 | 147120 2993 140517 46.9 | 0.048 % | c | 3093 | 441361 1285530 | 161832 3093 144868 46.8 | 0.049 % | c | 3243 | 441361 1285530 | 178015 3243 151155 46.6 | 0.049 % | c | 3468 | 441361 1285530 | 195816 3468 162183 46.8 | 0.049 % | c | 3805 | 441361 1285530 | 215398 3805 177916 46.8 | 0.049 % | c | 4313 | 441361 1285530 | 236938 4313 203493 47.2 | 0.049 % | c | 5073 | 441361 1285530 | 260632 5073 238215 47.0 | 0.049 % | c | 6212 | 441361 1285530 | 286695 6212 290626 46.8 | 0.049 % | c | 7925 | 441361 1285530 | 315364 7925 373140 47.1 | 0.049 % | c | 10487 | 441361 1285530 | 346901 10487 502342 47.9 | 0.049 % | c ============================================================================== c [1mFound solution: 3130368[0m c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 11357 | 441373 1285563 | 147124 11357 548645 48.3 | 0.049 % | c ============================================================================== c [1mFound solution: 3030016[0m c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 11368 | 441383 1285588 | 147127 11368 548955 48.3 | 0.049 % | c | 11468 | 441383 1285588 | 161839 11468 553078 48.2 | 0.050 % | c ============================================================================== c [1mFound solution: 2987008[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 11526 | 441396 1285620 | 147132 11526 555621 48.2 | 0.050 % | c | 11627 | 441396 1285620 | 161845 11627 559847 48.2 | 0.051 % | c ============================================================================== c [1mFound solution: 2855936[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 11752 | 441403 1285637 | 147134 11752 565521 48.1 | 0.051 % | c | 11855 | 441403 1285637 | 161847 11855 569209 48.0 | 0.052 % | c | 12005 | 441403 1285637 | 178032 12005 578630 48.2 | 0.052 % | c | 12230 | 441403 1285637 | 195835 12230 588352 48.1 | 0.052 % | c ============================================================================== c [1mFound solution: 2851840[0m c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 12386 | 441412 1285660 | 147137 12386 595871 48.1 | 0.052 % | c ============================================================================== c [1mFound solution: 2816000[0m c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 12476 | 441422 1285685 | 147140 12476 599897 48.1 | 0.052 % | c | 12576 | 441415 1285670 | 161854 12571 604076 48.1 | 0.054 % | c ============================================================================== c [1mFound solution: 2775040[0m c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 12595 | 441424 1285691 | 147141 12590 604749 48.0 | 0.054 % | c | 12695 | 441424 1285691 | 161855 12690 608940 48.0 | 0.055 % | c | 12846 | 441424 1285691 | 178040 12841 616100 48.0 | 0.055 % | c ============================================================================== c [1mFound solution: 2662400[0m c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 12972 | 441436 1285719 | 147145 12967 622239 48.0 | 0.055 % | c | 13072 | 441436 1285719 | 161859 13067 626166 47.9 | 0.056 % | c | 13222 | 441436 1285719 | 178045 13217 633053 47.9 | 0.056 % | c | 13448 | 441436 1285719 | 195849 13443 643739 47.9 | 0.056 % | c | 13785 | 441436 1285719 | 215434 13780 659014 47.8 | 0.056 % | c | 14291 | 441436 1285719 | 236978 14286 680978 47.7 | 0.056 % | c | 15050 | 441436 1285719 | 260676 15045 715068 47.5 | 0.056 % | c ============================================================================== c [1mFound solution: 2650112[0m c ---[ 0]---> Sorter-cost: 3 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 15554 | 441445 1285739 | 147148 15549 738967 47.5 | 0.056 % | c | 15654 | 441440 1285729 | 161862 15644 742466 47.5 | 0.057 % | c | 15805 | 441440 1285729 | 178049 15795 748653 47.4 | 0.057 % | c | 16031 | 441440 1285729 | 195853 16021 759741 47.4 | 0.057 % | c | 16369 | 441440 1285729 | 215439 16359 777405 47.5 | 0.057 % | c ============================================================================== c [1mFound solution: 2510848[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 16562 | 441452 1285758 | 147150 16552 785530 47.5 | 0.057 % | c ============================================================================== c [1mFound solution: 2456576[0m c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 16639 | 441463 1285784 | 147154 16629 788726 47.4 | 0.057 % | c | 16739 | 441463 1285784 | 161869 16729 792734 47.4 | 0.059 % | c | 16889 | 441463 1285784 | 178056 16879 799286 47.4 | 0.059 % | c | 17114 | 441463 1285784 | 195861 17104 809644 47.3 | 0.059 % | c | 17451 | 441463 1285784 | 215448 17441 825471 47.3 | 0.059 % | c | 17957 | 441463 1285784 | 236992 17947 850339 47.4 | 0.059 % | c ============================================================================== c [1mFound solution: 2454528[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 18184 | 441474 1285811 | 147158 18174 861848 47.4 | 0.059 % | c ============================================================================== c [1mFound solution: 2437120[0m c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 18214 | 441486 1285839 | 147162 18204 863992 47.5 | 0.059 % | c | 18315 | 441486 1285839 | 161878 18305 867683 47.4 | 0.060 % | c ============================================================================== c [1mFound solution: 2432000[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 18354 | 441499 1285869 | 147166 18344 869636 47.4 | 0.060 % | c | 18455 | 441499 1285869 | 161882 18445 873073 47.3 | 0.061 % | c | 18607 | 441499 1285869 | 178070 18597 884539 47.6 | 0.061 % | c | 18832 | 441499 1285869 | 195877 18822 898770 47.8 | 0.061 % | c ============================================================================== c [1mFound solution: 2405376[0m c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 18988 | 441511 1285897 | 147170 18978 904556 47.7 | 0.061 % | c ============================================================================== c [1mFound solution: 2371584[0m c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19036 | 441519 1285915 | 147173 19026 906591 47.7 | 0.061 % | c | 19136 | 441519 1285915 | 161890 19126 910640 47.6 | 0.062 % | c | 19286 | 441519 1285915 | 178079 19276 917023 47.6 | 0.062 % | c | 19511 | 441519 1285915 | 195887 19501 926601 47.5 | 0.062 % | c ============================================================================== c [1mFound solution: 2337792[0m c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19570 | 441525 1285930 | 147175 19560 929041 47.5 | 0.062 % | c ============================================================================== c [1mFound solution: 2190336[0m c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19602 | 441534 1285950 | 147178 19592 930390 47.5 | 0.062 % | c | 19704 | 441534 1285950 | 161895 19694 934818 47.5 | 0.063 % | c | 19857 | 441534 1285950 | 178085 19847 941270 47.4 | 0.063 % | c | 20085 | 441516 1285910 | 195893 20046 949831 47.4 | 0.067 % | c ============================================================================== c [1mFound solution: 2168832[0m c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 20272 | 441526 1285932 | 147175 20233 956629 47.3 | 0.067 % | c | 20374 | 441526 1285932 | 161892 20335 960960 47.3 | 0.067 % | c ============================================================================== c [1mFound solution: 2154496[0m c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 20514 | 441534 1285950 | 147178 20475 967662 47.3 | 0.067 % | c | 20614 | 441534 1285950 | 161895 20575 972104 47.2 | 0.068 % | c | 20769 | 441534 1285950 | 178085 20730 978293 47.2 | 0.068 % | c ============================================================================== c [1mFound solution: 2117632[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 20947 | 441540 1285963 | 147180 20908 986503 47.2 | 0.068 % | c | 21047 | 441540 1285963 | 161898 21008 990370 47.1 | 0.069 % | c | 21197 | 441540 1285963 | 178087 21158 997355 47.1 | 0.069 % | c | 21422 | 441540 1285963 | 195896 21383 1007184 47.1 | 0.069 % | c ============================================================================== c [1mFound solution: 2114560[0m c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21696 | 441549 1285983 | 147183 21657 1019168 47.1 | 0.069 % | c ============================================================================== c [1mFound solution: 1947648[0m c ---[ 0]---> Sorter-cost: 4 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21730 | 441557 1286002 | 147185 21691 1020931 47.1 | 0.069 % | c ============================================================================== c [1mFound solution: 1937408[0m c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21744 | 441566 1286025 | 147188 21705 1021695 47.1 | 0.069 % | c | 21844 | 441566 1286025 | 161906 21805 1026027 47.1 | 0.070 % | c ============================================================================== c [1mFound solution: 1893376[0m c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21949 | 441574 1286045 | 147191 21910 1029023 47.0 | 0.070 % | c | 22049 | 441574 1286045 | 161910 22010 1033110 46.9 | 0.071 % | c | 22199 | 441574 1286045 | 178101 22160 1038508 46.9 | 0.071 % | c ============================================================================== c [1mFound solution: 1881088[0m c ---[ 0]---> Sorter-cost: 3 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 22225 | 441578 1286055 | 147192 22186 1039839 46.9 | 0.071 % | c ============================================================================== c [1mFound solution: 1748992[0m c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 22319 | 441590 1286083 | 147196 22280 1043648 46.8 | 0.071 % | c | 22419 | 441590 1286083 | 161915 22380 1047923 46.8 | 0.072 % | c ============================================================================== c [1mFound solution: 1742848[0m c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 22427 | 441602 1286111 | 147200 22388 1048258 46.8 | 0.072 % | c ============================================================================== c [1mFound solution: 1703936[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 22453 | 441605 1286118 | 147201 22414 1049690 46.8 | 0.072 % | c | 22555 | 441605 1286118 | 161921 22516 1054292 46.8 | 0.074 % | c | 22705 | 441605 1286118 | 178113 22666 1061590 46.8 | 0.074 % | c | 22931 | 441605 1286118 | 195924 22892 1071090 46.8 | 0.074 % | c | 23268 | 441605 1286118 | 215516 23229 1088121 46.8 | 0.074 % | c ============================================================================== c [1mFound solution: 1601536[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 23453 | 441608 1286125 | 147202 23414 1096341 46.8 | 0.074 % | c | 23555 | 441608 1286125 | 161922 23516 1098789 46.7 | 0.074 % | c | 23705 | 441608 1286125 | 178114 23666 1105702 46.7 | 0.074 % | c ============================================================================== c [1mFound solution: 1558528[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 23717 | 441615 1286145 | 147205 23678 1106109 46.7 | 0.074 % | c ============================================================================== c [1mFound solution: 1415168[0m c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 23734 | 441623 1286164 | 147207 23695 1106742 46.7 | 0.074 % | c ============================================================================== c [1mFound solution: 1394688[0m c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 23797 | 441634 1286190 | 147211 23758 1109356 46.7 | 0.074 % | c | 23897 | 441627 1286175 | 161932 23853 1112691 46.6 | 0.078 % | c | 24047 | 441627 1286175 | 178125 24003 1119318 46.6 | 0.078 % | c | 24272 | 441627 1286175 | 195937 24228 1131072 46.7 | 0.078 % | c ============================================================================== c [1mFound solution: 1338368[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 24446 | 441634 1286191 | 147211 24402 1138915 46.7 | 0.078 % | c | 24547 | 441634 1286191 | 161932 24503 1145546 46.8 | 0.078 % | c ============================================================================== c [1mFound solution: 1326080[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 24682 | 441641 1286207 | 147213 24638 1150434 46.7 | 0.078 % | c ============================================================================== c [1mFound solution: 1316864[0m c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 24715 | 441649 1286225 | 147216 24671 1151706 46.7 | 0.078 % | c | 24815 | 441649 1286225 | 161937 24771 1155628 46.7 | 0.080 % | c ============================================================================== c [1mFound solution: 1281024[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 24842 | 441658 1286247 | 147219 24798 1156594 46.6 | 0.080 % | c ============================================================================== c [1mFound solution: 1177600[0m c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 24907 | 441665 1286263 | 147221 24863 1159311 46.6 | 0.080 % | c | 25008 | 441665 1286263 | 161943 24964 1164044 46.6 | 0.081 % | c | 25158 | 441665 1286263 | 178137 25114 1172031 46.7 | 0.081 % | c | 25384 | 441665 1286263 | 195951 25340 1181976 46.6 | 0.081 % | c ============================================================================== c [1mFound solution: 1070080[0m c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 25476 | 441676 1286287 | 147225 25432 1185106 46.6 | 0.081 % | c ============================================================================== c [1mFound solution: 1029120[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 25551 | 441653 1286224 | 147217 24181 1129685 46.7 | 0.081 % | c | 25651 | 441632 1286176 | 161938 22327 1030708 46.2 | 0.094 % | c ============================================================================== c [1mFound solution: 959488[0m c ---[ 0]---> Sorter-cost: 4 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 25753 | 441638 1286191 | 147212 22429 1033691 46.1 | 0.094 % | c ============================================================================== c [1mFound solution: 914432[0m c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 25851 | 441645 1286209 | 147215 22527 1037806 46.1 | 0.094 % | c | 25951 | 441645 1286209 | 161936 22627 1041265 46.0 | 0.095 % | c | 26102 | 441645 1286209 | 178130 22778 1047328 46.0 | 0.095 % | c ============================================================================== c [1mFound solution: 880640[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 26239 | 441654 1286230 | 147218 22915 1053422 46.0 | 0.095 % | c | 26339 | 441573 1286043 | 161939 20824 956529 45.9 | 0.113 % | c | 26490 | 441573 1286043 | 178133 20975 963244 45.9 | 0.113 % | c | 26715 | 441573 1286043 | 195947 21200 972484 45.9 | 0.113 % | c ============================================================================== c [1mFound solution: 842752[0m c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 26791 | 441583 1286067 | 147194 21276 975610 45.9 | 0.113 % | c | 26891 | 441583 1286067 | 161913 21376 979130 45.8 | 0.114 % | /oldhome/oroussel/solvers/minisat+_script: line 9: 4704 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.93 0.97 0.91 2/54 4700 Raw data (stat): 4700 (runsolver) R 4699 7475 7474 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 854220668 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0002 s] Raw data (loadavg): 0.94 0.97 0.91 2/55 4704 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+20.0003 s] Raw data (loadavg): 0.95 0.97 0.91 2/55 4704 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+30.0013 s] Raw data (loadavg): 0.96 0.97 0.91 2/55 4704 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+40.0008 s] Raw data (loadavg): 0.96 0.97 0.91 2/55 4704 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+50.001 s] Raw data (loadavg): 0.97 0.97 0.91 2/55 4704 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+60.0009 s] Raw data (loadavg): 0.97 0.97 0.91 2/55 4704 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+70.0007 s] Raw data (loadavg): 0.98 0.97 0.91 2/55 4704 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+80.0008 s] Raw data (loadavg): 0.98 0.97 0.91 2/55 4704 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+90.0007 s] Raw data (loadavg): 0.98 0.97 0.91 2/55 4704 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+100.001 s] Raw data (loadavg): 0.98 0.97 0.91 2/55 4704 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+110.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4704 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+120.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4704 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+130.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4704 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+140.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4704 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+150.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4704 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+160.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4704 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+170.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4704 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+180.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+190.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+200.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+210.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+220.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+230.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+240.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+250.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+260.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+270.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+280.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+290.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+300.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+310.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+320.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+330.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+340.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+350.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+360.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+370.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+380.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+390.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+400.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+410.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+420.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+430.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+440.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+450.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+460.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+470.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+480.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+490.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+500.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+510.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+520.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+530.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+540.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+550.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+560.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+570.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+580.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+590.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+600.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+610.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+620.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+630.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+640.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+650.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+660.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+670.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+680.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+690.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+700.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+710.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+720.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+730.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+740.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+750.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+760.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+770.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+780.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+790.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+800.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+810.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+820.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+830.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+840.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+850.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+860.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+870.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+880.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+890.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+900.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+910.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+920.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+930.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+940.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+950.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+960.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+970.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+980.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+990.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1000.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1010.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1020.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1030.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1040.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1050.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1060.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1070.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1080.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1090.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1100.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1110.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1120.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1130.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1140.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1150.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1160.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1170.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1180.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1190.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1200.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1210.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1220.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1229.8 s] Raw data (loadavg): 0.99 0.97 0.91 1/53 4706 Raw data (stat): 4700 (minisat+_script) S 4699 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854220668 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 0 Child status: 152 Real time (s): 1229.8 CPU time (s): 1229.87 CPU user time (s): 1229.43 CPU system time (s): 0.433934 CPU usage (%): 100.006 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####