Name | normalized-opb/mps-v2-20-10/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-neos5.opb |
MD5SUM | e6bff154156b54af3a9a38f7579209b6 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 17324 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 163 |
Biggest coefficient in the objective function | 1024 |
Number of bits for the biggest coefficient in the objective function | 11 |
Sum of the numbers in the objective function | 74742 |
Number of bits of the sum of numbers in the objective function | 17 |
Biggest number in a constraint | 8192 |
Number of bits of the biggest number in a constraint | 14 |
Biggest sum of numbers in a constraint | 74742 |
Number of bits of the biggest sum of numbers | 17 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.06984 |
Number of variables | 163 |
Total number of constraints | 126 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 56 |
Number of constraints which are nor clauses,nor cardinality constraints | 70 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 102 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc29 THE 2005-05-25 20:49:17 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=22316 boxname=wulflinc29 idbench=1132 idsolver=15 numberseed=0 MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814 /oldhome/oroussel/solvers/minisat+_script MD5SUM BENCH: e6bff154156b54af3a9a38f7579209b6 /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-neos5.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-neos5.opb IDLAUNCH: 22316 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.020 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.020 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: 548556 kB Buffers: 35340 kB Cached: 425656 kB SwapCached: 452 kB Active: 30468 kB Inactive: 435992 kB HighTotal: 131008 kB HighFree: 26432 kB LowTotal: 903652 kB LowFree: 522124 kB SwapTotal: 2097892 kB SwapFree: 2096752 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5612 kB Slab: 13908 kB Committed_AS: 63600 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-25 21:09:47 (client local time) WITH STATUS 152 IN 1229.85 SECONDS stats: 22316 7 1229.85 152 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 73 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 72]---> BDD-cost: 10 c ---[ 71]---> BDD-cost: 10 c ---[ 70]---> BDD-cost: 10 c ---[ 69]---> BDD-cost: 10 c ---[ 68]---> BDD-cost: 10 c ---[ 67]---> BDD-cost: 10 c ---[ 66]---> BDD-cost: 10 c ---[ 65]---> BDD-cost: 10 c ---[ 64]---> BDD-cost: 10 c ---[ 63]---> BDD-cost: 10 c ---[ 62]---> Sorter-cost: 382 Base: c ---[ 61]---> Sorter-cost: 831 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 60]---> Sorter-cost: 417 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 59]---> Sorter-cost: 1471 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 58]---> Sorter-cost: 1060 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 57]---> Sorter-cost: 429 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 56]---> Sorter-cost: 1241 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 55]---> Sorter-cost: 1058 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 54]---> Sorter-cost: 1090 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 53]---> Sorter-cost: 445 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 52]---> Sorter-cost: 1269 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 51]---> Sorter-cost: 216 Base: c ---[ 50]---> Sorter-cost: 1042 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 49]---> Sorter-cost: 1289 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 48]---> Sorter-cost: 548 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 47]---> Sorter-cost: 329 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 46]---> Sorter-cost: 373 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 45]---> Sorter-cost: 405 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 44]---> Sorter-cost: 343 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 43]---> Sorter-cost: 365 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 42]---> Sorter-cost: 397 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 41]---> Sorter-cost: 379 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 40]---> Sorter-cost: 351 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 39]---> Sorter-cost: 399 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 38]---> Sorter-cost: 1195 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 37]---> Sorter-cost: 345 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 36]---> Sorter-cost: 365 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 35]---> Sorter-cost: 397 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 34]---> Sorter-cost: 379 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 33]---> Sorter-cost: 399 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 32]---> Sorter-cost: 1215 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 31]---> Sorter-cost: 405 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 30]---> Sorter-cost: 417 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 29]---> Sorter-cost: 311 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 28]---> Sorter-cost: 1020 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 27]---> Sorter-cost: 1259 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 26]---> Sorter-cost: 337 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 25]---> Sorter-cost: 329 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 24]---> Sorter-cost: 319 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 23]---> Sorter-cost: 365 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 22]---> Sorter-cost: 397 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 21]---> Sorter-cost: 329 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 20]---> Sorter-cost: 319 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 19]---> Sorter-cost: 365 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 18]---> Sorter-cost: 319 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 17]---> Sorter-cost: 397 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 16]---> Sorter-cost: 329 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 15]---> Sorter-cost: 355 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 14]---> Sorter-cost: 387 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 13]---> Sorter-cost: 389 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 12]---> Sorter-cost: 409 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 11]---> Sorter-cost: 996 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 10]---> Sorter-cost: 329 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 9]---> Sorter-cost: 329 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 8]---> Sorter-cost: 319 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 7]---> Sorter-cost: 319 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 6]---> Sorter-cost: 329 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 5]---> Sorter-cost: 355 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 4]---> Sorter-cost: 387 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 3]---> Sorter-cost: 319 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 2]---> Sorter-cost: 130 Base: c ---[ 1]---> Sorter-cost: 301 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 0]---> Sorter-cost: 301 Base: 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 | 0 | 28562 68458 | 9520 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 62463[0m c ---[ 0]---> Sorter-cost: 2662 Base: 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 | 3 | 34861 83214 | 11620 3 28 9.3 | 0.000 % | c | 103 | 34861 83214 | 12782 103 670 6.5 | 0.366 % | c | 253 | 34861 83214 | 14060 253 2273 9.0 | 0.366 % | c | 479 | 34861 83214 | 15466 479 4345 9.1 | 0.366 % | c ============================================================================== c [1mFound solution: 28022[0m c ---[ 0]---> Sorter-cost: 11 Base: 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 | 581 | 35195 84026 | 11731 581 4989 8.6 | 0.366 % | c ============================================================================== c [1mFound solution: 27718[0m c ---[ 0]---> Sorter-cost: 8 Base: 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 | 614 | 35214 84093 | 11738 614 5230 8.5 | 0.366 % | c ============================================================================== c [1mFound solution: 25668[0m c ---[ 0]---> Sorter-cost: 11 Base: 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 | 679 | 35257 84224 | 11752 679 5833 8.6 | 0.366 % | c ============================================================================== c [1mFound solution: 24642[0m c ---[ 0]---> Sorter-cost: 10 Base: 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 | 748 | 35275 84271 | 11758 748 6397 8.6 | 0.366 % | c ============================================================================== c [1mFound solution: 21602[0m c ---[ 0]---> Sorter-cost: 7 Base: 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 | 754 | 35316 84375 | 11772 754 6433 8.5 | 0.366 % | c ============================================================================== c [1mFound solution: 21588[0m c ---[ 0]---> Sorter-cost: 8 Base: 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 | 811 | 35330 84412 | 11776 811 6969 8.6 | 0.366 % | c | 911 | 35330 84412 | 12953 911 7622 8.4 | 0.408 % | c | 1062 | 35330 84412 | 14248 1062 9064 8.5 | 0.408 % | c ============================================================================== c [1mFound solution: 21586[0m c ---[ 0]---> Sorter-cost: 8 Base: 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 | 1282 | 35340 84435 | 11780 1282 12314 9.6 | 0.408 % | c ============================================================================== c [1mFound solution: 19478[0m c ---[ 0]---> Sorter-cost: 7 Base: 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 | 1331 | 35365 84497 | 11788 1331 12873 9.7 | 0.408 % | c | 1431 | 35365 84497 | 12966 1431 13984 9.8 | 0.417 % | c | 1581 | 35365 84497 | 14263 1581 15343 9.7 | 0.417 % | c | 1807 | 35365 84497 | 15689 1807 18631 10.3 | 0.417 % | c | 2145 | 35365 84497 | 17258 2145 22255 10.4 | 0.417 % | c | 2651 | 35365 84497 | 18984 2651 30097 11.4 | 0.417 % | c ============================================================================== c [1mFound solution: 19442[0m c ---[ 0]---> Sorter-cost: 7 Base: 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 | 3201 | 35373 84523 | 11791 3201 38247 11.9 | 0.417 % | c | 3302 | 35373 84523 | 12970 3302 42625 12.9 | 0.422 % | c | 3453 | 35373 84523 | 14267 3453 44963 13.0 | 0.422 % | c ============================================================================== c [1mFound solution: 18497[0m c ---[ 0]---> Sorter-cost: 10 Base: 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 | 3593 | 35380 84540 | 11793 3588 46216 12.9 | 0.422 % | c | 3693 | 35380 84540 | 12972 3688 47161 12.8 | 0.441 % | c | 3843 | 35376 84532 | 14269 3837 49398 12.9 | 0.450 % | c | 4069 | 35376 84532 | 15696 4063 54615 13.4 | 0.450 % | c | 4406 | 35376 84532 | 17266 4400 62454 14.2 | 0.450 % | c | 4913 | 35376 84532 | 18992 4907 72842 14.8 | 0.450 % | c ============================================================================== c [1mFound solution: 18496[0m c ---[ 0]---> Sorter-cost: 10 Base: 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 | 5193 | 35369 84515 | 11789 5127 76175 14.9 | 0.450 % | c | 5293 | 35369 84515 | 12967 5227 76920 14.7 | 0.492 % | c | 5444 | 35369 84515 | 14264 5378 77796 14.5 | 0.492 % | c | 5669 | 35369 84515 | 15691 5603 81751 14.6 | 0.492 % | c | 6006 | 35369 84515 | 17260 5940 86807 14.6 | 0.492 % | c ============================================================================== c [1mFound solution: 18479[0m c ---[ 0]---> Sorter-cost: 8 Base: 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 | 6132 | 35377 84534 | 11792 6066 88960 14.7 | 0.492 % | c | 6232 | 35377 84534 | 12971 6166 89891 14.6 | 0.497 % | c | 6384 | 35376 84531 | 14268 6229 93681 15.0 | 0.501 % | c | 6610 | 35376 84531 | 15695 6455 98851 15.3 | 0.501 % | c | 6947 | 35376 84531 | 17264 6792 102991 15.2 | 0.501 % | c ============================================================================== c [1mFound solution: 18478[0m c ---[ 0]---> Sorter-cost: 9 Base: 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 | 7182 | 35386 84554 | 11795 7018 106716 15.2 | 0.501 % | c | 7282 | 35386 84554 | 12974 7118 108642 15.3 | 0.510 % | c | 7432 | 35386 84554 | 14271 7268 110081 15.1 | 0.510 % | c | 7657 | 35386 84554 | 15699 7493 114199 15.2 | 0.510 % | c ============================================================================== c [1mFound solution: 18454[0m c ---[ 0]---> Sorter-cost: 2 Base: 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 | 7900 | 35383 84547 | 11794 7723 118775 15.4 | 0.510 % | c | 8000 | 35383 84547 | 12973 7823 120762 15.4 | 0.548 % | c | 8152 | 35383 84547 | 14270 7975 123675 15.5 | 0.548 % | c ============================================================================== c [1mFound solution: 18444[0m c ---[ 0]---> Sorter-cost: 9 Base: 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 | 8212 | 35395 84574 | 11798 8035 124725 15.5 | 0.548 % | c ============================================================================== c [1mFound solution: 18442[0m c ---[ 0]---> Sorter-cost: 9 Base: 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 | 8258 | 35406 84598 | 11802 8081 125191 15.5 | 0.548 % | c ============================================================================== c [1mFound solution: 17417[0m c ---[ 0]---> Sorter-cost: 9 Base: 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 | 8323 | 35430 84655 | 11810 8146 126409 15.5 | 0.548 % | c ============================================================================== c [1mFound solution: 17416[0m c ---[ 0]---> Sorter-cost: 9 Base: 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 | 8388 | 35442 84684 | 11814 8211 127824 15.6 | 0.548 % | c | 8488 | 35442 84684 | 12995 8311 129724 15.6 | 0.585 % | c | 8638 | 35425 84647 | 14294 8441 132371 15.7 | 0.631 % | c ============================================================================== c [1mFound solution: 17415[0m c ---[ 0]---> Sorter-cost: 7 Base: 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 | 8796 | 35433 84664 | 11811 8599 137170 16.0 | 0.631 % | c ============================================================================== c [1mFound solution: 17414[0m c ---[ 0]---> Sorter-cost: 6 Base: 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 | 8869 | 35440 84679 | 11813 8672 138705 16.0 | 0.631 % | c | 8969 | 35440 84679 | 12994 8772 140927 16.1 | 0.640 % | c | 9120 | 35440 84679 | 14293 8923 143280 16.1 | 0.641 % | c | 9345 | 35440 84679 | 15723 9148 147150 16.1 | 0.640 % | c ============================================================================== c [1mFound solution: 17413[0m c ---[ 0]---> Sorter-cost: 10 Base: 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 | 9542 | 35450 84702 | 11816 9345 154406 16.5 | 0.640 % | c | 9642 | 35450 84702 | 12997 9445 155445 16.5 | 0.645 % | c | 9792 | 35444 84688 | 14297 9593 159836 16.7 | 0.664 % | c ============================================================================== c [1mFound solution: 17412[0m c ---[ 0]---> Sorter-cost: 6 Base: 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 | 9841 | 35451 84703 | 11817 9642 160546 16.7 | 0.664 % | c ============================================================================== c [1mFound solution: 17411[0m c ---[ 0]---> Sorter-cost: 9 Base: 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 | 9865 | 35461 84725 | 11820 9666 161146 16.7 | 0.664 % | c | 9966 | 35461 84725 | 13002 9767 162491 16.6 | 0.673 % | c | 10116 | 35460 84722 | 14302 9885 167135 16.9 | 0.678 % | c ============================================================================== c [1mFound solution: 17410[0m c ---[ 0]---> Sorter-cost: 6 Base: 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 | 10276 | 35467 84737 | 11822 10045 170200 16.9 | 0.678 % | c | 10377 | 35467 84737 | 13004 10146 171182 16.9 | 0.682 % | c ============================================================================== c [1mFound solution: 17409[0m c ---[ 0]---> Sorter-cost: 6 Base: 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 | 10491 | 35474 84752 | 11824 10260 174333 17.0 | 0.682 % | c ============================================================================== c [1mFound solution: 17408[0m c ---[ 0]---> Sorter-cost: 6 Base: 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 | 10528 | 35479 84763 | 11826 10294 175434 17.0 | 0.682 % | c | 10628 | 35479 84763 | 13008 10394 177101 17.0 | 0.696 % | c | 10778 | 35477 84759 | 14309 10543 179233 17.0 | 0.701 % | c | 11004 | 35477 84759 | 15740 10769 185541 17.2 | 0.701 % | c | 11341 | 35477 84759 | 17314 11106 187815 16.9 | 0.701 % | c ============================================================================== c [1mFound solution: 17318[0m c ---[ 0]---> Sorter-cost: 7 Base: 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 | 11751 | 35489 84790 | 11829 11516 199908 17.4 | 0.701 % | c | 11851 | 35489 84790 | 13011 11616 201664 17.4 | 0.705 % | c | 12001 | 35489 84790 | 14313 11766 202751 17.2 | 0.705 % | c | 12226 | 35489 84790 | 15744 11991 214489 17.9 | 0.705 % | c | 12563 | 35489 84790 | 17318 12328 242106 19.6 | 0.705 % | c | 13069 | 35488 84787 | 19050 12814 280719 21.9 | 0.710 % | c | 13828 | 35486 84783 | 20955 13572 292108 21.5 | 0.715 % | c | 14967 | 35486 84783 | 23051 14711 344167 23.4 | 0.715 % | c ============================================================================== c [1mFound solution: 16613[0m c ---[ 0]---> Sorter-cost: 7 Base: 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 | 15651 | 35494 84803 | 11831 15395 378123 24.6 | 0.715 % | c | 15751 | 35494 84803 | 13014 7798 221350 28.4 | 0.719 % | c | 15901 | 35494 84803 | 14315 7948 225362 28.4 | 0.719 % | c | 16127 | 35494 84803 | 15747 8174 234611 28.7 | 0.719 % | c | 16465 | 35494 84803 | 17321 8512 248038 29.1 | 0.719 % | c | 16974 | 35494 84803 | 19053 9021 270699 30.0 | 0.719 % | c ============================================================================== c [1mFound solution: 16389[0m c ---[ 0]---> Sorter-cost: 2 Base: 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 | 17391 | 35503 84822 | 11834 9438 296263 31.4 | 0.719 % | c | 17491 | 35503 84822 | 13017 9538 298646 31.3 | 0.724 % | c | 17642 | 35503 84822 | 14319 9689 303656 31.3 | 0.724 % | c | 17868 | 35503 84822 | 15751 9915 307827 31.0 | 0.724 % | c | 18205 | 35498 84811 | 17326 10250 338402 33.0 | 0.738 % | c | 18711 | 35498 84811 | 19058 10756 347783 32.3 | 0.738 % | c ============================================================================== c [1mFound solution: 16388[0m c ---[ 0]---> Sorter-cost: 2 Base: 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 | 19431 | 35506 84828 | 11835 11476 378534 33.0 | 0.738 % | c | 19531 | 35506 84828 | 13018 11576 379899 32.8 | 0.742 % | c | 19682 | 35506 84828 | 14320 11727 382261 32.6 | 0.742 % | c | 19907 | 35506 84828 | 15752 11952 386048 32.3 | 0.742 % | c | 20244 | 35506 84828 | 17327 12289 391868 31.9 | 0.742 % | c | 20752 | 35506 84828 | 19060 12797 400846 31.3 | 0.742 % | c | 21513 | 35506 84828 | 20966 13558 420260 31.0 | 0.742 % | c ============================================================================== c [1mFound solution: 16386[0m c ---[ 0]---> Sorter-cost: 2 Base: 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 | 22643 | 35514 84845 | 11838 14688 444209 30.2 | 0.742 % | c | 22743 | 35514 84845 | 13021 7444 148246 19.9 | 0.747 % | c | 22896 | 35514 84845 | 14323 7597 155471 20.5 | 0.747 % | c | 23122 | 35514 84845 | 15756 7823 159906 20.4 | 0.747 % | c | 23459 | 35514 84845 | 17332 8160 166784 20.4 | 0.747 % | c | 23966 | 35511 84838 | 19065 8324 173446 20.8 | 0.756 % | c | 24725 | 35511 84838 | 20971 9083 213515 23.5 | 0.756 % | c ============================================================================== c [1mFound solution: 16385[0m c ---[ 0]---> Sorter-cost: 2 Base: 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 | 24919 | 35519 84855 | 11839 9277 222451 24.0 | 0.756 % | c | 25019 | 35519 84855 | 13022 9377 223734 23.9 | 0.761 % | c | 25172 | 35519 84855 | 14325 9530 225560 23.7 | 0.761 % | c | 25397 | 35519 84855 | 15757 9755 234476 24.0 | 0.761 % | c | 25734 | 35519 84855 | 17333 10092 245223 24.3 | 0.761 % | c | 26240 | 35519 84855 | 19066 10598 262188 24.7 | 0.761 % | c | 26999 | 35519 84855 | 20973 11357 293708 25.9 | 0.761 % | c ============================================================================== c [1mFound solution: 16384[0m c ---[ 0]---> Sorter-cost: 2 Base: 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 | 27112 | 35527 84872 | 11842 11470 299692 26.1 | 0.761 % | c | 27213 | 35527 84872 | 13026 11571 301172 26.0 | 0.765 % | c | 27363 | 35527 84872 | 14328 11721 302788 25.8 | 0.765 % | c | 27588 | 35527 84872 | 15761 11946 306328 25.6 | 0.765 % | c | 27926 | 35527 84872 | 17337 12284 318191 25.9 | 0.765 % | c | 28432 | 35527 84872 | 19071 12790 330313 25.8 | 0.765 % | c | 29196 | 35512 84841 | 20978 13525 342328 25.3 | 0.803 % | c | 30336 | 35512 84841 | 23076 14665 389391 26.6 | 0.803 % | c | 32044 | 35508 84833 | 25384 16370 459588 28.1 | 0.812 % | c | 34607 | 35508 84833 | 27922 18933 657462 34.7 | 0.812 % | c | 38451 | 35508 84833 | 30715 22777 797266 35.0 | 0.812 % | c ============================================================================== c [1mFound solution: 16379[0m c ---[ 0]---> Sorter-cost: 9 Base: 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 | 38650 | 35518 84854 | 11839 22976 807513 35.1 | 0.812 % | c | 38750 | 35518 84854 | 13022 11588 426450 36.8 | 0.817 % | c | 38902 | 35518 84854 | 14325 11740 431937 36.8 | 0.817 % | c | 39127 | 35518 84854 | 15757 11965 438219 36.6 | 0.817 % | c | 39464 | 35518 84854 | 17333 12302 449818 36.6 | 0.817 % | c | 39970 | 35518 84854 | 19066 12808 460415 35.9 | 0.817 % | c | 40729 | 35518 84854 | 20973 13567 490726 36.2 | 0.816 % | c | 41868 | 35513 84843 | 23070 14659 550778 37.6 | 0.831 % | c | 43576 | 35513 84843 | 25377 16367 607793 37.1 | 0.831 % | c | 46138 | 35513 84843 | 27915 18929 729632 38.5 | 0.830 % | c | 49983 | 35513 84843 | 30707 22774 1076270 47.3 | 0.831 % | c ============================================================================== c [1mFound solution: 16378[0m c ---[ 0]---> Sorter-cost: 8 Base: 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 | 50585 | 35522 84862 | 11840 23376 1104731 47.3 | 0.831 % | c | 50685 | 35522 84862 | 13024 11788 537643 45.6 | 0.835 % | c | 50838 | 35522 84862 | 14326 11941 539044 45.1 | 0.835 % | c | 51063 | 35519 84854 | 15759 12041 545252 45.3 | 0.844 % | c | 51401 | 35519 84854 | 17334 12379 552992 44.7 | 0.844 % | c | 51908 | 35519 84854 | 19068 12886 610287 47.4 | 0.844 % | c | 52667 | 35519 84854 | 20975 13645 624728 45.8 | 0.844 % | c | 53806 | 35519 84854 | 23072 14784 682766 46.2 | 0.844 % | c | 55514 | 35519 84854 | 25380 16492 728301 44.2 | 0.844 % | c | 58078 | 35519 84854 | 27918 19056 817063 42.9 | 0.844 % | c | 61922 | 35519 84854 | 30709 22900 929759 40.6 | 0.844 % | c | 67689 | 35519 84854 | 33780 28667 1131507 39.5 | 0.844 % | c ============================================================================== c [1mFound solution: 16377[0m c ---[ 0]---> Sorter-cost: 8 Base: 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 | 74135 | 35528 84873 | 11842 35113 1446648 41.2 | 0.844 % | c | 74235 | 35528 84873 | 13026 8879 166722 18.8 | 0.849 % | c | 74388 | 35497 84808 | 14328 9019 169524 18.8 | 0.928 % | c | 74613 | 35497 84808 | 15761 9244 177704 19.2 | 0.928 % | c | 74950 | 35497 84808 | 17337 9581 190723 19.9 | 0.928 % | c | 75456 | 35489 84790 | 19071 10086 209656 20.8 | 0.952 % | c | 76215 | 35483 84778 | 20978 10843 227527 21.0 | 0.966 % | c | 77354 | 35483 84778 | 23076 11982 267451 22.3 | 0.966 % | c | 79062 | 35483 84778 | 25384 13690 312826 22.9 | 0.966 % | c | 81624 | 35483 84778 | 27922 16252 419884 25.8 | 0.966 % | c | 85469 | 35475 84762 | 30715 20095 496432 24.7 | 0.984 % | c | 91236 | 35475 84762 | 33786 25862 666510 25.8 | 0.984 % | c ============================================================================== c [1mFound solution: 16374[0m c ---[ 0]---> Sorter-cost: 5 Base: 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 | 93282 | 35487 84793 | 11829 27908 746410 26.7 | 0.984 % | c | 93383 | 35487 84793 | 13011 7078 120743 17.1 | 1.002 % | c | 93534 | 35487 84793 | 14313 7229 128111 17.7 | 1.002 % | c | 93759 | 35487 84793 | 15744 7454 133926 18.0 | 1.002 % | c | 94096 | 35429 84668 | 17318 7779 142656 18.3 | 1.114 % | c | 94602 | 35369 84547 | 19050 8275 156852 19.0 | 1.250 % | c | 95361 | 35369 84547 | 20955 9034 172585 19.1 | 1.250 % | c ============================================================================== c [1mFound solution: 16373[0m c ---[ 0]---> Sorter-cost: 8 Base: 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 | 95608 | 35374 84566 | 11791 9281 182561 19.7 | 1.250 % | c | 95709 | 35374 84566 | 12970 9382 184357 19.7 | 1.254 % | c | 95859 | 35374 84566 | 14267 9532 188152 19.7 | 1.254 % | c | 96084 | 35374 84566 | 15693 9757 192412 19.7 | 1.254 % | c | 96421 | 35374 84566 | 17263 10094 203836 20.2 | 1.254 % | c | 96927 | 35374 84566 | 18989 10600 223940 21.1 | 1.254 % | c | 97686 | 35374 84566 | 20888 11359 243431 21.4 | 1.254 % | c | 98827 | 35372 84562 | 22977 12499 297644 23.8 | 1.259 % | c | 100535 | 35372 84562 | 25275 14207 342049 24.1 | 1.259 % | c | 103097 | 35364 84546 | 27802 16768 433604 25.9 | 1.277 % | c | 106942 | 35355 84527 | 30582 20609 492584 23.9 | 1.301 % | c | 112709 | 35355 84527 | 33641 26376 599837 22.7 | 1.301 % | c | 121359 | 35355 84527 | 37005 35026 1304901 37.3 | 1.301 % | c ============================================================================== c [1mFound solution: 16372[0m c ---[ 0]---> Sorter-cost: 7 Base: 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 | 129822 | 35359 84541 | 11786 20555 887351 43.2 | 1.301 % | c | 129926 | 35359 84541 | 12964 10382 267450 25.8 | 1.305 % | c | 130077 | 35359 84541 | 14261 10533 270492 25.7 | 1.305 % | c | 130302 | 35359 84541 | 15687 10758 274374 25.5 | 1.305 % | c | 130642 | 35359 84541 | 17255 11098 293613 26.5 | 1.305 % | c | 131148 | 35359 84541 | 18981 11604 300344 25.9 | 1.305 % | c | 131909 | 35359 84541 | 20879 12365 306743 24.8 | 1.305 % | c | 133049 | 35359 84541 | 22967 13505 408446 30.2 | 1.305 % | c | 134757 | 35307 84428 | 25264 15201 454665 29.9 | 1.426 % | c | 137319 | 35307 84428 | 27790 17763 504562 28.4 | 1.426 % | c | 141164 | 35307 84428 | 30569 21608 754993 34.9 | 1.426 % | c ============================================================================== c [1mFound solution: 16370[0m c ---[ 0]---> Sorter-cost: 2 Base: 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 | 142890 | 35300 84415 | 11766 23333 801569 34.4 | 1.426 % | c | 142990 | 35300 84415 | 12942 11767 344585 29.3 | 1.454 % | c | 143141 | 35300 84415 | 14236 11918 352269 29.6 | 1.454 % | c ============================================================================== c [1mFound solution: 16368[0m c ---[ 0]---> Sorter-cost: 8 Base: 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 | 143317 | 35304 84430 | 11768 12094 357237 29.5 | 1.454 % | c | 143417 | 35304 84430 | 12944 6147 70829 11.5 | 1.459 % | c | 143568 | 35304 84430 | 14239 6298 74871 11.9 | 1.459 % | c | 143793 | 35304 84430 | 15663 6523 79668 12.2 | 1.459 % | c | 144130 | 35304 84430 | 17229 6860 103779 15.1 | 1.459 % | c | 144636 | 35292 84406 | 18952 7365 110974 15.1 | 1.486 % | c | 145395 | 35292 84406 | 20847 8124 137915 17.0 | 1.486 % | c | 146535 | 35286 84394 | 22932 9263 200019 21.6 | 1.501 % | c | 148247 | 35276 84374 | 25225 10969 235738 21.5 | 1.524 % | c | 150809 | 35276 84374 | 27748 13531 375590 27.8 | 1.524 % | c | 154653 | 35276 84374 | 30523 17375 481786 27.7 | 1.524 % | c ============================================================================== c [1mFound solution: 16182[0m c ---[ 0]---> Sorter-cost: 6 Base: 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 | 159767 | 35284 84394 | 11761 22489 583554 25.9 | 1.524 % | c | 159867 | 35284 84394 | 12937 11345 162153 14.3 | 1.528 % | c | 160017 | 35284 84394 | 14230 11495 165778 14.4 | 1.528 % | c | 160243 | 35284 84394 | 15653 11721 178167 15.2 | 1.528 % | c | 160580 | 35272 84370 | 17219 12055 190971 15.8 | 1.556 % | c | 161086 | 35272 84370 | 18941 12561 231677 18.4 | 1.556 % | c | 161845 | 35272 84370 | 20835 13320 265684 19.9 | 1.556 % | c | 162984 | 35272 84370 | 22918 14459 311641 21.6 | 1.556 % | c | 164694 | 35272 84370 | 25210 16169 371354 23.0 | 1.556 % | c | 167256 | 35272 84370 | 27731 18731 526320 28.1 | 1.556 % | c | 171101 | 35272 84370 | 30505 22576 926819 41.1 | 1.556 % | c | 176869 | 35272 84370 | 33555 28344 1571366 55.4 | 1.556 % | c ============================================================================== c [1mFound solution: 16180[0m c ---[ 0]---> Sorter-cost: 6 Base: 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 | 183256 | 35280 84390 | 11760 34731 1824941 52.5 | 1.556 % | c | 183356 | 35280 84390 | 12936 8388 172686 20.6 | 1.560 % | c | 183506 | 35280 84390 | 14229 8538 175539 20.6 | 1.560 % | c | 183732 | 35260 84348 | 15652 8750 183779 21.0 | 1.612 % | c | 184070 | 35180 84165 | 17217 9069 191837 21.2 | 1.789 % | c | 184576 | 35152 84101 | 18939 9564 204206 21.4 | 1.873 % | c | 185335 | 35152 84101 | 20833 10323 232728 22.5 | 1.872 % | c | 186474 | 35152 84101 | 22916 11462 261772 22.8 | 1.872 % | c | 188186 | 35152 84101 | 25208 13174 420648 31.9 | 1.872 % | c | 190748 | 35152 84101 | 27729 15736 534414 34.0 | 1.872 % | c | 194592 | 35134 84063 | 30502 19576 767684 39.2 | 1.919 % | c | 200358 | 35134 84063 | 33552 25342 1158847 45.7 | 1.919 % | c | 209008 | 35134 84063 | 36907 33992 1672385 49.2 | 1.919 % | c | 221982 | 35134 84063 | 40598 19295 1086840 56.3 | 1.919 % | c ============================================================================== c [1mFound solution: 16179[0m c ---[ 0]---> Sorter-cost: 8 Base: 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 | 236727 | 35134 84068 | 11711 34039 2223941 65.3 | 1.919 % | c | 236827 | 35134 84068 | 12882 8610 153797 17.9 | 1.942 % | c | 236979 | 35131 84061 | 14170 8761 157277 18.0 | 1.951 % | c | 237205 | 35121 84039 | 15587 8982 161179 17.9 | 1.979 % | c | 237542 | 35111 84019 | 17146 9316 171848 18.4 | 2.002 % | c | 238049 | 35111 84019 | 18860 9823 191365 19.5 | 2.002 % | c | 238810 | 35086 83963 | 20746 10554 213205 20.2 | 2.058 % | c | 239951 | 35078 83945 | 22821 11693 258260 22.1 | 2.081 % | c | 241659 | 35074 83935 | 25103 13398 349645 26.1 | 2.095 % | c | 244221 | 35074 83935 | 27613 15960 451885 28.3 | 2.096 % | c | 248065 | 35074 83935 | 30375 19804 720708 36.4 | 2.095 % | c | 253831 | 35064 83915 | 33412 25569 1046013 40.9 | 2.119 % | c ============================================================================== c [1mFound solution: 16178[0m c ---[ 0]---> Sorter-cost: 6 Base: 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 | 259485 | 35054 83899 | 11684 31220 1408668 45.1 | 2.119 % | c | 259586 | 35054 83899 | 12852 7906 171546 21.7 | 2.165 % | c | 259736 | 35054 83899 | 14137 8056 174230 21.6 | 2.165 % | c | 259961 | 35054 83899 | 15551 8281 179052 21.6 | 2.165 % | c | 260298 | 35054 83899 | 17106 8618 195671 22.7 | 2.165 % | c | 260804 | 35054 83899 | 18817 9124 211111 23.1 | 2.165 % | c | 261563 | 35054 83899 | 20698 9883 258658 26.2 | 2.165 % | c | 262703 | 35054 83899 | 22768 11023 291377 26.4 | 2.165 % | c | 264411 | 35054 83899 | 25045 12731 370236 29.1 | 2.165 % | c ============================================================================== c [1mFound solution: 16118[0m c ---[ 0]---> Sorter-cost: 4 Base: 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 | 265329 | 35061 83916 | 11687 13649 406288 29.8 | 2.165 % | c | 265433 | 35053 83900 | 12855 6927 81243 11.7 | 2.188 % | c | 265585 | 35053 83900 | 14141 7079 89507 12.6 | 2.188 % | c | 265810 | 35043 83880 | 15555 7303 96354 13.2 | 2.211 % | c | 266147 | 35043 83880 | 17110 7640 108378 14.2 | 2.211 % | c | 266655 | 35043 83880 | 18822 8148 131177 16.1 | 2.211 % | c | 267414 | 35043 83880 | 20704 8907 152900 17.2 | 2.211 % | c | 268554 | 35043 83880 | 22774 10047 177411 17.7 | 2.211 % | c ============================================================================== c [1mFound solution: 16117[0m c ---[ 0]---> Sorter-cost: 4 Base: 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 | 269483 | 35050 83900 | 11683 10976 226410 20.6 | 2.211 % | c | 269586 | 35050 83900 | 12851 11079 228675 20.6 | 2.215 % | c | 269738 | 35050 83900 | 14136 11231 232623 20.7 | 2.215 % | c | 269965 | 35044 83886 | 15550 11456 238346 20.8 | 2.234 % | c | 270302 | 34737 83233 | 17105 11746 250620 21.3 | 2.918 % | c | 270808 | 34734 83226 | 18815 12250 276586 22.6 | 2.927 % | c | 271567 | 34727 83211 | 20697 13003 304016 23.4 | 2.946 % | c | 272707 | 34727 83211 | 22766 14143 365781 25.9 | 2.946 % | c | 274416 | 34727 83211 | 25043 15852 462932 29.2 | 2.946 % | c | 276978 | 34727 83211 | 27547 18414 660017 35.8 | 2.946 % | c | 280822 | 34727 83211 | 30302 22258 765041 34.4 | 2.946 % | c | 286589 | 34727 83211 | 33332 28025 1213832 43.3 | 2.946 % | c | 295238 | 34705 83167 | 36666 36668 2215407 60.4 | 2.987 % | c | 308212 | 34699 83154 | 40332 28832 2249748 78.0 | 2.997 % | c ============================================================================== c [1mFound solution: 16116[0m c ---[ 0]---> Sorter-cost: 4 Base: 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 | 314712 | 34697 83153 | 11565 35330 2567057 72.7 | 2.997 % | c | 314813 | 34697 83153 | 12721 8934 165532 18.5 | 3.024 % | c | 314964 | 34697 83153 | 13993 9085 168231 18.5 | 3.024 % | c | 315189 | 34697 83153 | 15393 9310 173303 18.6 | 3.024 % | c | 315526 | 34697 83153 | 16932 9647 184718 19.1 | 3.024 % | c | 316032 | 34697 83153 | 18625 10153 208876 20.6 | 3.024 % | c | 316791 | 34697 83153 | 20488 10912 236818 21.7 | 3.024 % | c | 317933 | 34697 83153 | 22536 12054 295954 24.6 | 3.024 % | c | 319641 | 34685 83125 | 24790 13755 377282 27.4 | 3.061 % | c | 322205 | 34685 83125 | 27269 16319 557138 34.1 | 3.061 % | c | 326049 | 34685 83125 | 29996 20163 818384 40.6 | 3.061 % | c ============================================================================== c [1mFound solution: 15990[0m c ---[ 0]---> Sorter-cost: 4 Base: 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 | 327390 | 34685 83125 | 11561 21501 864903 40.2 | 3.061 % | c | 327491 | 34685 83125 | 12717 10852 303674 28.0 | 3.084 % | c | 327641 | 34685 83125 | 13988 11002 307758 28.0 | 3.084 % | c | 327870 | 34675 83103 | 15387 11228 312746 27.9 | 3.112 % | c | 328207 | 34675 83103 | 16926 11565 339526 29.4 | 3.112 % | c | 328715 | 34675 83103 | 18619 12073 360651 29.9 | 3.112 % | c | 329474 | 34675 83103 | 20481 12832 405674 31.6 | 3.112 % | c | 330614 | 34675 83103 | 22529 13972 455546 32.6 | 3.112 % | c | 332324 | 34675 83103 | 24782 15682 537323 34.3 | 3.112 % | c ============================================================================== c [1mFound solution: 15989[0m c ---[ 0]---> Sorter-cost: 5 Base: 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 | 332519 | 34683 83124 | 11561 15877 542783 34.2 | 3.112 % | c | 332619 | 34683 83124 | 12717 8039 121748 15.1 | 3.116 % | c | 332771 | 34683 83124 | 13988 8191 124578 15.2 | 3.116 % | c | 332996 | 34683 83124 | 15387 8416 132510 15.7 | 3.116 % | c | 333334 | 34683 83124 | 16926 8754 147664 16.9 | 3.116 % | c | 333841 | 34683 83124 | 18619 9261 178758 19.3 | 3.116 % | c | 334601 | 34683 83124 | 20481 10021 206358 20.6 | 3.116 % | c ============================================================================== c [1mFound solution: 15925[0m c ---[ 0]---> Sorter-cost: 6 Base: 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 | 334973 | 34692 83146 | 11564 10393 216399 20.8 | 3.116 % | c | 335075 | 34692 83146 | 12720 10495 218494 20.8 | 3.120 % | c | 335229 | 34692 83146 | 13992 10649 223205 21.0 | 3.120 % | c | 335456 | 34692 83146 | 15391 10876 230925 21.2 | 3.120 % | c | 335796 | 34692 83146 | 16930 11216 247406 22.1 | 3.120 % | c | 336305 | 34692 83146 | 18623 11725 262641 22.4 | 3.120 % | c | 337064 | 34684 83128 | 20486 12481 291182 23.3 | 3.143 % | c | 338203 | 34684 83128 | 22534 13620 325969 23.9 | 3.143 % | c | 339911 | 34684 83128 | 24788 15328 391851 25.6 | 3.143 % | c | 342473 | 34684 83128 | 27267 17890 489510 27.4 | 3.143 % | c | 346317 | 34684 83128 | 29994 21734 748012 34.4 | 3.143 % | c ============================================================================== c [1mFound solution: 15910[0m c ---[ 0]---> Sorter-cost: 5 Base: 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 | 349192 | 34691 83144 | 11563 24609 951224 38.7 | 3.143 % | c | 349292 | 34682 83125 | 12719 6251 61443 9.8 | 3.170 % | c | 349442 | 34682 83125 | 13991 6401 67635 10.6 | 3.170 % | c | 349667 | 34682 83125 | 15390 6626 75197 11.3 | 3.170 % | c | 350007 | 34657 83071 | 16929 6960 87240 12.5 | 3.226 % | c | 350513 | 34654 83064 | 18622 7464 111076 14.9 | 3.235 % | c | 351272 | 34654 83064 | 20484 8223 144330 17.6 | 3.235 % | c | 352411 | 34654 83064 | 22533 9362 200327 21.4 | 3.235 % | c | 354120 | 34654 83064 | 24786 11071 358556 32.4 | 3.235 % | c | 356684 | 34654 83064 | 27264 13635 595110 43.6 | 3.235 % | c | 360528 | 34654 83064 | 29991 17479 1015840 58.1 | 3.235 % | c | 366294 | 34654 83064 | 32990 23245 1660242 71.4 | 3.235 % | c ============================================================================== c [1mFound solution: 15894[0m c ---[ 0]---> Sorter-cost: 3 Base: 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 | 371891 | 34657 83072 | 11552 28841 2177328 75.5 | 3.235 % | c | 371991 | 34657 83072 | 12707 7311 113680 15.5 | 3.253 % | c | 372142 | 34645 83047 | 13977 7453 115579 15.5 | 3.281 % | c | 372367 | 34632 83018 | 15375 7607 118767 15.6 | 3.318 % | c | 372704 | 34632 83018 | 16913 7944 129243 16.3 | 3.318 % | c | 373212 | 34625 83003 | 18604 8450 151345 17.9 | 3.337 % | c | 373971 | 34625 83003 | 20465 9209 199994 21.7 | 3.337 % | c | 375112 | 34619 82991 | 22511 10348 253789 24.5 | 3.351 % | c | 376822 | 34619 82991 | 24762 12058 406225 33.7 | 3.351 % | c | 379385 | 34606 82962 | 27239 14619 536781 36.7 | 3.388 % | c ============================================================================== c [1mFound solution: 15893[0m c ---[ 0]---> Sorter-cost: 7 Base: 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 | 380196 | 34608 82967 | 11536 15429 575996 37.3 | 3.388 % | c | 380298 | 34608 82967 | 12689 7817 129723 16.6 | 3.415 % | c | 380450 | 34608 82967 | 13958 7969 133742 16.8 | 3.415 % | c | 380676 | 34608 82967 | 15354 8195 143216 17.5 | 3.415 % | c | 381013 | 34605 82960 | 16889 8520 150908 17.7 | 3.424 % | c | 381519 | 34605 82960 | 18578 9026 178653 19.8 | 3.425 % | c | 382278 | 34605 82960 | 20436 9785 210764 21.5 | 3.424 % | c | 383418 | 34605 82960 | 22480 10925 258868 23.7 | 3.424 % | c | 385126 | 34605 82960 | 24728 12633 366990 29.1 | 3.424 % | c | 387688 | 34597 82941 | 27201 14969 480408 32.1 | 3.448 % | c | 391532 | 34576 82894 | 29921 18804 798432 42.5 | 3.508 % | c ============================================================================== c [1mFound solution: 15884[0m c ---[ 0]---> Sorter-cost: 3 Base: 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 | 392902 | 34585 82914 | 11528 20174 845624 41.9 | 3.508 % | c | 393004 | 34585 82914 | 12680 10189 281709 27.6 | 3.512 % | c | 393154 | 34585 82914 | 13948 10339 290203 28.1 | 3.512 % | c | 393379 | 34585 82914 | 15343 10564 301336 28.5 | 3.512 % | c | 393717 | 34585 82914 | 16878 10902 313278 28.7 | 3.512 % | c | 394223 | 34585 82914 | 18565 11408 326068 28.6 | 3.512 % | c | 394983 | 34585 82914 | 20422 12168 349476 28.7 | 3.512 % | c ============================================================================== c [1mFound solution: 15878[0m c ---[ 0]---> Sorter-cost: 3 Base: 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 | 395809 | 34593 82932 | 11531 12994 390156 30.0 | 3.512 % | c | 395909 | 34593 82932 | 12684 6597 56989 8.6 | 3.516 % | c | 396059 | 34593 82932 | 13952 6747 64702 9.6 | 3.516 % | c | 396284 | 34593 82932 | 15347 6972 72081 10.3 | 3.516 % | c | 396624 | 34593 82932 | 16882 7312 86221 11.8 | 3.516 % | c | 397132 | 34593 82932 | 18570 7820 103764 13.3 | 3.516 % | c | 397893 | 34593 82932 | 20427 8581 151592 17.7 | 3.516 % | c ============================================================================== c [1mFound solution: 15877[0m c ---[ 0]---> Sorter-cost: 3 Base: 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 | 398834 | 34602 82952 | 11534 9522 193264 20.3 | 3.516 % | c | 398934 | 34602 82952 | 12687 9622 196981 20.5 | 3.520 % | c | 399084 | 34602 82952 | 13956 9772 200190 20.5 | 3.520 % | c | 399310 | 34602 82952 | 15351 9998 207390 20.7 | 3.520 % | c | 399651 | 34602 82952 | 16886 10339 229744 22.2 | 3.520 % | c | 400157 | 34602 82952 | 18575 10845 246052 22.7 | 3.520 % | c | 400916 | 34602 82952 | 20433 11604 301779 26.0 | 3.520 % | c | 402055 | 34602 82952 | 22476 12743 373400 29.3 | 3.520 % | c | 403763 | 34602 82952 | 24724 14451 450964 31.2 | 3.520 % | c | 406325 | 34602 82952 | 27196 17013 560156 32.9 | 3.520 % | c | 410170 | 34602 82952 | 29916 20858 852653 40.9 | 3.520 % | c ============================================================================== c [1mFound solution: 15876[0m c ---[ 0]---> Sorter-cost: 3 Base: 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 | 415001 | 34610 82970 | 11536 25689 1113351 43.3 | 3.520 % | c | 415101 | 34610 82970 | 12689 6523 68241 10.5 | 3.524 % | c | 415253 | 34610 82970 | 13958 6675 73828 11.1 | 3.524 % | c | 415478 | 34601 82951 | 15354 6899 79352 11.5 | 3.547 % | c | 415815 | 34601 82951 | 16889 7236 97703 13.5 | 3.547 % | c | 416321 | 34601 82951 | 18578 7742 118010 15.2 | 3.547 % | c | 417080 | 34601 82951 | 20436 8501 138642 16.3 | 3.547 % | c | 418219 | 34601 82951 | 22480 9640 210486 21.8 | 3.547 % | c ============================================================================== c [1mFound solution: 15875[0m c ---[ 0]---> Sorter-cost: 3 Base: 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 | 419175 | 34602 82954 | 11534 10595 235459 22.2 | 3.547 % | c | 419275 | 34602 82954 | 12687 10695 238166 22.3 | 3.574 % | c | 419426 | 34602 82954 | 13956 10846 240943 22.2 | 3.575 % | c | 419653 | 34602 82954 | 15351 11073 247548 22.4 | 3.574 % | c | 419991 | 34602 82954 | 16886 11411 263394 23.1 | 3.574 % | c | 420499 | 34602 82954 | 18575 11919 280370 23.5 | 3.575 % | c | 421259 | 34602 82954 | 20433 12679 334150 26.4 | 3.575 % | c | 422398 | 34591 82929 | 22476 13816 381315 27.6 | 3.607 % | c ============================================================================== c [1mFound solution: 15873[0m c ---[ 0]---> Sorter-cost: 3 Base: 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 | 423043 | 34599 82947 | 11533 14461 409344 28.3 | 3.607 % | c | 423144 | 34599 82947 | 12686 7332 71936 9.8 | 3.611 % | c | 423294 | 34599 82947 | 13954 7482 75287 10.1 | 3.611 % | c | 423519 | 34599 82947 | 15350 7707 82530 10.7 | 3.611 % | c | 423856 | 34599 82947 | 16885 8044 92701 11.5 | 3.611 % | c | 424363 | 34599 82947 | 18574 8551 111070 13.0 | 3.611 % | c | 425122 | 34599 82947 | 20431 9310 151025 16.2 | 3.611 % | c | 426262 | 34599 82947 | 22474 10450 185862 17.8 | 3.611 % | c | 427971 | 34599 82947 | 24722 12159 292947 24.1 | 3.611 % | c | 430534 | 34599 82947 | 27194 14722 365461 24.8 | 3.611 % | c ============================================================================== c [1mFound solution: 15872[0m c ---[ 0]---> Sorter-cost: 3 Base: 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 | 433938 | 34593 82937 | 11531 18125 443975 24.5 | 3.611 % | c | 434038 | 34593 82937 | 12684 9163 83902 9.2 | 3.647 % | c | 434188 | 34593 82937 | 13952 9313 86703 9.3 | 3.647 % | c | 434413 | 34593 82937 | 15347 9538 93482 9.8 | 3.647 % | c | 434751 | 34593 82937 | 16882 9876 109902 11.1 | 3.647 % | c | 435258 | 34578 82904 | 18570 10377 130823 12.6 | 3.689 % | c | 436017 | 34578 82904 | 20427 11136 170820 15.3 | 3.689 % | c | 437156 | 34573 82893 | 22470 12273 248739 20.3 | 3.703 % | c | 438864 | 34573 82893 | 24717 13981 296453 21.2 | 3.703 % | c | 441426 | 34573 82893 | 27189 16543 421400 25.5 | 3.703 % | c | 445271 | 34573 82893 | 29908 20388 893733 43.8 | 3.703 % | c | 451037 | 34573 82893 | 32899 26154 1230018 47.0 | 3.703 % | c | 459686 | 34573 82893 | 36189 34803 1806221 51.9 | 3.703 % | c | 472660 | 34573 82893 | 39808 28152 1236074 43.9 | 3.703 % | c | 492123 | 34573 82893 | 43788 20971 470841 22.5 | 3.703 % | c | 521316 | 34569 82885 | 48167 22801 620855 27.2 | 3.708 % | c | 565105 | 34569 82885 | 52984 33501 2612555 78.0 | 3.708 % | c | 630789 | 34569 82885 | 58283 27174 924872 34.0 | 3.708 % | c | 729315 | 34551 82846 | 64111 36423 1660579 45.6 | 3.731 % | /oldhome/oroussel/solvers/minisat+_script: line 9: 5011 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@" #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.87 0.93 0.94 2/54 5007 Raw data (stat): 5007 (runsolver) R 5006 20001 20000 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 841881479 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+10.001 s] Raw data (loadavg): 0.89 0.93 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.0022 s] Raw data (loadavg): 0.91 0.94 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.003 s] Raw data (loadavg): 0.92 0.94 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.0031 s] Raw data (loadavg): 0.93 0.94 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.0035 s] Raw data (loadavg): 0.94 0.94 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.0035 s] Raw data (loadavg): 0.95 0.94 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.0044 s] Raw data (loadavg): 0.96 0.94 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.0049 s] Raw data (loadavg): 0.96 0.94 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.0047 s] Raw data (loadavg): 0.97 0.95 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.005 s] Raw data (loadavg): 0.97 0.95 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.005 s] Raw data (loadavg): 0.98 0.95 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.006 s] Raw data (loadavg): 0.98 0.95 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.006 s] Raw data (loadavg): 0.98 0.95 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.006 s] Raw data (loadavg): 0.98 0.95 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.006 s] Raw data (loadavg): 0.99 0.95 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.006 s] Raw data (loadavg): 0.99 0.95 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.007 s] Raw data (loadavg): 0.99 0.95 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.009 s] Raw data (loadavg): 0.99 0.95 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.008 s] Raw data (loadavg): 0.99 0.96 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.008 s] Raw data (loadavg): 0.99 0.96 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.008 s] Raw data (loadavg): 0.99 0.96 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.009 s] Raw data (loadavg): 0.99 0.96 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.009 s] Raw data (loadavg): 0.99 0.96 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.009 s] Raw data (loadavg): 0.99 0.96 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.009 s] Raw data (loadavg): 0.99 0.96 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.009 s] Raw data (loadavg): 0.99 0.96 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.01 s] Raw data (loadavg): 0.99 0.96 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.011 s] Raw data (loadavg): 0.99 0.96 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.01 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.01 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.01 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.011 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.011 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.01 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.011 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.011 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.012 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.011 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.011 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.012 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.012 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.013 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.013 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.013 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.013 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.014 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.014 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.014 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.015 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.015 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.015 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.016 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.017 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.016 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.016 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.017 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.017 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.017 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.017 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.018 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.018 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.019 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.019 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.019 s] Raw data (loadavg): 0.99 0.97 0.94 2/55 5011 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.02 s] Raw data (loadavg): 0.99 0.97 0.94 3/58 5051 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.021 s] Raw data (loadavg): 1.07 0.99 0.95 2/55 5064 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.022 s] Raw data (loadavg): 1.06 0.99 0.95 2/55 5064 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.022 s] Raw data (loadavg): 1.05 0.99 0.95 2/55 5064 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.022 s] Raw data (loadavg): 1.04 0.99 0.95 2/55 5064 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.023 s] Raw data (loadavg): 1.03 0.99 0.95 2/55 5064 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.023 s] Raw data (loadavg): 1.03 0.99 0.95 2/55 5064 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.023 s] Raw data (loadavg): 1.02 0.99 0.95 2/55 5064 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.024 s] Raw data (loadavg): 1.02 0.99 0.95 2/55 5066 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.024 s] Raw data (loadavg): 1.02 0.99 0.95 2/55 5066 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.024 s] Raw data (loadavg): 1.01 0.99 0.95 2/55 5066 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.025 s] Raw data (loadavg): 1.01 0.99 0.95 2/55 5066 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.026 s] Raw data (loadavg): 1.01 0.99 0.95 2/55 5066 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.026 s] Raw data (loadavg): 1.01 0.99 0.95 2/55 5066 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.027 s] Raw data (loadavg): 1.00 0.99 0.95 2/55 5066 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.028 s] Raw data (loadavg): 1.00 0.99 0.95 2/55 5066 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.027 s] Raw data (loadavg): 1.00 0.99 0.95 2/55 5066 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.028 s] Raw data (loadavg): 1.00 0.99 0.95 2/55 5066 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.029 s] Raw data (loadavg): 1.00 0.99 0.95 2/55 5066 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.029 s] Raw data (loadavg): 1.00 0.99 0.95 2/55 5066 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.029 s] Raw data (loadavg): 1.00 0.99 0.95 2/55 5066 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.029 s] Raw data (loadavg): 1.00 0.99 0.95 2/55 5066 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.03 s] Raw data (loadavg): 1.00 0.99 0.95 2/55 5066 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.031 s] Raw data (loadavg): 1.00 0.99 0.95 2/55 5066 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.031 s] Raw data (loadavg): 1.00 0.99 0.95 2/55 5066 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.031 s] Raw data (loadavg): 1.00 0.99 0.95 2/55 5066 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.032 s] Raw data (loadavg): 1.00 0.99 0.95 2/55 5066 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.033 s] Raw data (loadavg): 1.00 0.99 0.95 2/55 5066 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.033 s] Raw data (loadavg): 1.00 0.99 0.95 2/55 5066 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.034 s] Raw data (loadavg): 1.00 0.99 0.95 2/55 5066 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.034 s] Raw data (loadavg): 1.00 0.99 0.95 2/55 5066 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.034 s] Raw data (loadavg): 1.00 0.99 0.95 2/55 5066 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.035 s] Raw data (loadavg): 1.00 0.99 0.95 2/55 5066 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.036 s] Raw data (loadavg): 1.00 0.99 0.95 2/55 5068 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.035 s] Raw data (loadavg): 1.00 0.99 0.95 2/55 5068 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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): 1.00 0.99 0.95 2/55 5068 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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): 1.00 0.99 0.95 2/55 5068 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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): 1.00 0.99 0.95 2/55 5068 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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): 1.00 0.99 0.95 2/55 5068 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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): 1.00 0.99 0.95 2/55 5068 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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): 1.00 0.99 0.95 2/55 5068 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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): 1.00 0.99 0.95 2/55 5068 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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): 1.00 0.99 0.95 2/55 5068 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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): 1.00 0.99 0.95 2/55 5068 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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): 1.00 0.99 0.95 2/55 5068 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.04 s] Raw data (loadavg): 1.00 0.99 0.95 2/55 5068 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.04 s] Raw data (loadavg): 1.00 0.99 0.95 2/55 5068 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.04 s] Raw data (loadavg): 1.00 0.99 0.95 2/55 5068 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.04 s] Raw data (loadavg): 1.00 0.99 0.95 2/55 5068 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.04 s] Raw data (loadavg): 1.00 0.99 0.95 2/55 5068 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.04 s] Raw data (loadavg): 1.00 0.99 0.95 2/55 5068 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.04 s] Raw data (loadavg): 1.00 0.99 0.95 2/55 5068 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.04 s] Raw data (loadavg): 1.00 0.99 0.95 2/55 5068 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.04 s] Raw data (loadavg): 1.00 0.99 0.95 2/55 5068 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.04 s] Raw data (loadavg): 1.00 0.99 0.95 2/55 5068 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.04 s] Raw data (loadavg): 1.00 0.99 0.95 2/55 5068 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.04 s] Raw data (loadavg): 1.00 0.99 0.95 2/55 5068 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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): 1.00 0.99 0.95 2/55 5068 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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): 1.00 0.99 0.95 1/53 5068 Raw data (stat): 5007 (minisat+_script) S 5006 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841881479 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.85 CPU user time (s): 1229.41 CPU system time (s): 0.438933 CPU usage (%): 100.009 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####