| Name | mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-pk1.opb |
| MD5SUM | 4d8544323b5554a497d5d3c2a3b0ca03 |
| Bench Category | optimization, big integers (OPTBIGINT) |
| Has Objective Function | YES |
| Satisfiable | |
| (Un)Satisfiability was proved | |
| Best value of the objective function | |
| Optimality of the best value was proved | |
| Number of terms in the objective function | 30 |
| Biggest coefficient in the objective function | 536870912 |
| Number of bits for the biggest coefficient in the objective function | 30 |
| Sum of the numbers in the objective function | 1073741823 |
| Number of bits of the sum of numbers in the objective function | 30 |
| Biggest number in a constraint | 536870912 |
| Number of bits of the biggest number in a constraint | 30 |
| Biggest sum of numbers in a constraint | 2150078462 |
| Number of bits of the biggest sum of numbers | 32 |
| Best result obtained on this benchmark | |
| Best CPU time to get the best result obtained on this benchmark | |
| Number of variables | 985 |
| Total number of constraints | 100 |
| Number of constraints which are clauses | 0 |
| Number of constraints which are cardinality constraints (but not clauses) | 55 |
| Number of constraints which are nor clauses,nor cardinality constraints | 45 |
| Minimum length of a constraint | 1 |
| Maximum length of a constraint | 115 |
LAUNCH ON wulflinc7 THE 2005-09-19 03:49:37 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2934 boxname=wulflinc7 idbench=590 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 4d8544323b5554a497d5d3c2a3b0ca03 /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-pk1.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-pk1.opb IDLAUNCH: 2934 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.050 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.050 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: 891544 kB Buffers: 37008 kB Cached: 81592 kB SwapCached: 740 kB Active: 74684 kB Inactive: 46544 kB HighTotal: 131008 kB HighFree: 47320 kB LowTotal: 903652 kB LowFree: 844224 kB SwapTotal: 2097136 kB SwapFree: 2095892 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5716 kB Slab: 16256 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-19 04:09:47 (client local time) WITH STATUS 10 IN 1209.68 SECONDS stats: 2934 7 1209.68 10
c Parsing PB file... c Converting 60 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ############### c -- Clauses(.)/Splits(s): (none) c ---[ 58]---> Adder-cost: 392 maxlim: 1074568191 bits: 32/31 c ---[ 56]---> Adder-cost: 416 maxlim: 1074819071 bits: 32/31 c ---[ 54]---> Adder-cost: 372 maxlim: 1074435071 bits: 32/31 c ---[ 52]---> Adder-cost: 396 maxlim: 1074839551 bits: 32/31 c ---[ 50]---> Adder-cost: 394 maxlim: 1074648063 bits: 32/31 c ---[ 48]---> Adder-cost: 388 maxlim: 1074828287 bits: 32/31 c ---[ 46]---> Adder-cost: 396 maxlim: 1074605055 bits: 32/31 c ---[ 45]---> BDD-cost: 88 c ---[ 44]---> BDD-cost: 88 c ---[ 43]---> BDD-cost: 88 c ---[ 42]---> BDD-cost: 88 c ---[ 40]---> Adder-cost: 386 maxlim: 1074768895 bits: 32/31 c ---[ 39]---> BDD-cost: 88 c ---[ 38]---> BDD-cost: 88 c ---[ 37]---> BDD-cost: 88 c ---[ 36]---> BDD-cost: 88 c ---[ 35]---> BDD-cost: 88 c ---[ 34]---> BDD-cost: 88 c ---[ 33]---> BDD-cost: 88 c ---[ 32]---> BDD-cost: 88 c ---[ 31]---> BDD-cost: 88 c ---[ 30]---> BDD-cost: 88 c ---[ 28]---> Adder-cost: 402 maxlim: 1074600959 bits: 32/31 c ---[ 27]---> BDD-cost: 88 c ---[ 26]---> BDD-cost: 88 c ---[ 25]---> BDD-cost: 88 c ---[ 24]---> BDD-cost: 88 c ---[ 23]---> BDD-cost: 88 c ---[ 22]---> BDD-cost: 88 c ---[ 21]---> BDD-cost: 88 c ---[ 20]---> BDD-cost: 88 c ---[ 19]---> BDD-cost: 88 c ---[ 18]---> BDD-cost: 88 c ---[ 16]---> Adder-cost: 396 maxlim: 1074780159 bits: 32/31 c ---[ 15]---> BDD-cost: 88 c ---[ 14]---> BDD-cost: 88 c ---[ 13]---> BDD-cost: 88 c ---[ 12]---> BDD-cost: 88 c ---[ 11]---> BDD-cost: 88 c ---[ 10]---> BDD-cost: 88 c ---[ 8]---> Adder-cost: 408 maxlim: 1074831359 bits: 32/31 c ---[ 6]---> Adder-cost: 382 maxlim: 1074711551 bits: 32/31 c ---[ 4]---> Adder-cost: 386 maxlim: 1074513919 bits: 32/31 c ---[ 2]---> Adder-cost: 402 maxlim: 1074724863 bits: 32/31 c ---[ 0]---> Adder-cost: 418 maxlim: 1074755583 bits: 32/31 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 43698 149820 | 14566 0 0 nan | 0.000 % | c | 101 | 43692 149802 | 16022 100 377 3.8 | 9.737 % | c | 251 | 43613 149543 | 17624 231 940 4.1 | 9.846 % | c | 476 | 43597 149491 | 19387 454 3460 7.6 | 9.866 % | c | 813 | 43567 149395 | 21326 787 6282 8.0 | 9.906 % | c | 1320 | 43543 149317 | 23458 1290 11743 9.1 | 9.946 % | c | 2079 | 43503 149187 | 25804 2045 20784 10.2 | 9.986 % | c | 3219 | 43441 148985 | 28385 3177 39069 12.3 | 10.066 % | c | 4927 | 43404 148866 | 31223 4880 70116 14.4 | 10.116 % | c | 7489 | 43309 148555 | 34345 7420 130706 17.6 | 10.245 % | c | 11333 | 42855 147069 | 37780 11152 226478 20.3 | 10.884 % | c ============================================================================== c [1mFound solution: 805027836[0m c ---[ 0]---> BDD-cost: 27 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 13349 | 42695 146557 | 14231 13128 274827 20.9 | 10.884 % | c | 13451 | 42695 146557 | 15654 13230 275914 20.9 | 11.126 % | c | 13601 | 42636 146362 | 17219 13366 277761 20.8 | 11.205 % | c ============================================================================== c [1mFound solution: 798154732[0m c ---[ 0]---> BDD-cost: 26 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 13673 | 42657 146423 | 14219 13438 279094 20.8 | 11.205 % | c | 13773 | 42657 146423 | 15640 13538 279709 20.7 | 11.201 % | c | 13925 | 42586 146190 | 17204 13672 282532 20.7 | 11.300 % | c | 14150 | 42507 145931 | 18925 13877 285277 20.6 | 11.410 % | c ============================================================================== c [1mFound solution: 540245492[0m c ---[ 0]---> BDD-cost: 27 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14180 | 42529 145990 | 14176 13907 285736 20.5 | 11.410 % | c | 14280 | 42458 145757 | 15593 13991 286661 20.5 | 11.508 % | c | 14430 | 42445 145716 | 17152 14139 289446 20.5 | 11.528 % | c ============================================================================== c [1mFound solution: 539639736[0m c ---[ 0]---> BDD-cost: 26 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14488 | 42469 145777 | 14156 14197 290546 20.5 | 11.528 % | c | 14590 | 42469 145777 | 15571 14299 292064 20.4 | 11.525 % | c | 14740 | 42469 145777 | 17128 14449 293676 20.3 | 11.525 % | c ============================================================================== c [1mFound solution: 538131452[0m c ---[ 0]---> BDD-cost: 20 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14775 | 42491 145834 | 14163 14484 294161 20.3 | 11.525 % | c | 14875 | 42491 145834 | 15579 14584 296858 20.4 | 11.525 % | c ============================================================================== c [1mFound solution: 537607156[0m c ---[ 0]---> BDD-cost: 21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14919 | 42513 145886 | 14171 14628 297337 20.3 | 11.525 % | c | 15020 | 42513 145886 | 15588 14729 298287 20.3 | 11.524 % | c | 15170 | 42505 145860 | 17146 14878 299506 20.1 | 11.534 % | c ============================================================================== c [1mFound solution: 537540604[0m c ---[ 0]---> BDD-cost: 19 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 15330 | 42470 145720 | 14156 15021 302374 20.1 | 11.534 % | c ============================================================================== c [1mFound solution: 537475964[0m c ---[ 0]---> BDD-cost: 23 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 15399 | 42496 145783 | 14165 15090 302938 20.1 | 11.534 % | c | 15499 | 42488 145757 | 15581 15189 304992 20.1 | 11.620 % | c | 15649 | 42488 145757 | 17139 15339 307104 20.0 | 11.620 % | c ============================================================================== c [1mFound solution: 537475956[0m c ---[ 0]---> BDD-cost: 23 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 15802 | 42514 145820 | 14171 15492 308832 19.9 | 11.620 % | c | 15902 | 42514 145820 | 15588 7846 149031 19.0 | 11.618 % | c | 16052 | 42514 145820 | 17146 7996 149817 18.7 | 11.618 % | c | 16277 | 42514 145820 | 18861 8221 153301 18.6 | 11.618 % | c | 16614 | 42506 145794 | 20747 8557 158056 18.5 | 11.627 % | c ============================================================================== c [1mFound solution: 537472860[0m c ---[ 0]---> BDD-cost: 25 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 17090 | 42535 145862 | 14178 9033 168804 18.7 | 11.627 % | c | 17190 | 42535 145862 | 15595 9133 169955 18.6 | 11.622 % | c | 17340 | 42535 145862 | 17155 9283 171592 18.5 | 11.622 % | c | 17565 | 42535 145862 | 18870 9508 176033 18.5 | 11.622 % | c | 17903 | 42520 145813 | 20758 9843 181582 18.4 | 11.642 % | c ============================================================================== c [1mFound solution: 537071036[0m c ---[ 0]---> BDD-cost: 24 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 18144 | 42546 145873 | 14182 10084 184557 18.3 | 11.642 % | c | 18244 | 42546 145873 | 15600 10184 185379 18.2 | 11.642 % | c | 18394 | 42546 145873 | 17160 10334 187144 18.1 | 11.642 % | c ============================================================================== c [1mFound solution: 537070552[0m c ---[ 0]---> BDD-cost: 25 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 18470 | 42572 145934 | 14190 10410 188109 18.1 | 11.642 % | c | 18570 | 42572 145934 | 15609 10510 191448 18.2 | 11.641 % | c ============================================================================== c [1mFound solution: 537005740[0m c ---[ 0]---> BDD-cost: 24 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 18644 | 42599 145995 | 14199 10584 192583 18.2 | 11.641 % | c | 18744 | 42599 145995 | 15618 10684 195492 18.3 | 11.641 % | c ============================================================================== c [1mFound solution: 537005548[0m c ---[ 0]---> BDD-cost: 21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 18763 | 42623 146050 | 14207 10703 195777 18.3 | 11.641 % | c ============================================================================== c [1mFound solution: 537004860[0m c ---[ 0]---> BDD-cost: 23 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 18786 | 42649 146107 | 14216 10726 196254 18.3 | 11.641 % | c ============================================================================== c [1mFound solution: 536940244[0m c ---[ 0]---> BDD-cost: 25 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 18871 | 42676 146169 | 14225 10811 197191 18.2 | 11.641 % | c | 18971 | 42676 146169 | 15647 10911 198639 18.2 | 11.643 % | c ============================================================================== c [1mFound solution: 536939124[0m c ---[ 0]---> BDD-cost: 22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19060 | 42702 146225 | 14234 11000 199724 18.2 | 11.643 % | c | 19160 | 42702 146225 | 15657 11100 201842 18.2 | 11.643 % | c | 19310 | 42702 146225 | 17223 11250 204081 18.1 | 11.643 % | c ============================================================================== c [1mFound solution: 536938968[0m c ---[ 0]---> BDD-cost: 21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19404 | 42727 146281 | 14242 11344 205549 18.1 | 11.643 % | c | 19505 | 42727 146281 | 15666 11445 207194 18.1 | 11.645 % | c ============================================================================== c [1mFound solution: 536909164[0m c ---[ 0]---> BDD-cost: 23 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19541 | 42756 146345 | 14252 11481 207677 18.1 | 11.645 % | c | 19641 | 42756 146345 | 15677 11581 211464 18.3 | 11.642 % | c ============================================================================== c [1mFound solution: 536906332[0m c ---[ 0]---> BDD-cost: 22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19672 | 42782 146401 | 14260 11612 212040 18.3 | 11.642 % | c | 19772 | 42782 146401 | 15686 11712 214383 18.3 | 11.643 % | c ============================================================================== c [1mFound solution: 536904860[0m c ---[ 0]---> BDD-cost: 24 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19857 | 42810 146461 | 14270 11797 215294 18.2 | 11.643 % | c ============================================================================== c [1mFound solution: 536904668[0m c ---[ 0]---> BDD-cost: 23 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19936 | 42833 146512 | 14277 11876 215997 18.2 | 11.643 % | c ============================================================================== c [1mFound solution: 536904380[0m c ---[ 0]---> BDD-cost: 22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19997 | 42859 146568 | 14286 11937 217189 18.2 | 11.643 % | c | 20097 | 42859 146568 | 15714 12037 218594 18.2 | 11.650 % | c | 20248 | 42859 146568 | 17286 12188 219876 18.0 | 11.650 % | c ============================================================================== c [1mFound solution: 536904048[0m c ---[ 0]---> BDD-cost: 25 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 20307 | 42886 146627 | 14295 12247 220917 18.0 | 11.650 % | c | 20407 | 42886 146627 | 15724 12347 222032 18.0 | 11.652 % | c ============================================================================== c [1mFound solution: 536903816[0m c ---[ 0]---> BDD-cost: 26 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 20519 | 42907 146662 | 14302 12458 224026 18.0 | 11.652 % | c | 20619 | 42907 146662 | 15732 12558 226087 18.0 | 11.664 % | c ============================================================================== c [1mFound solution: 536874796[0m c ---[ 0]---> BDD-cost: 23 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 20651 | 42929 146711 | 14309 12590 226712 18.0 | 11.664 % | c ============================================================================== c [1mFound solution: 536874716[0m c ---[ 0]---> BDD-cost: 22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 20737 | 42952 146762 | 14317 12676 228632 18.0 | 11.664 % | c | 20837 | 42952 146762 | 15748 12776 230546 18.0 | 11.673 % | c | 20988 | 42945 146739 | 17323 12926 232964 18.0 | 11.683 % | c ============================================================================== c [1mFound solution: 536873812[0m c ---[ 0]---> BDD-cost: 23 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21046 | 42971 146796 | 14323 12984 233528 18.0 | 11.683 % | c ============================================================================== c [1mFound solution: 536871352[0m c ---[ 0]---> BDD-cost: 21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21137 | 42994 146845 | 14331 13075 235855 18.0 | 11.683 % | c ============================================================================== c [1mFound solution: 136250084[0m c ---[ 0]---> BDD-cost: 24 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21164 | 42298 144714 | 14099 13100 236408 18.0 | 11.683 % | c ============================================================================== c [1mFound solution: 67715672[0m c ---[ 0]---> BDD-cost: 20 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21193 | 41956 143651 | 13985 13127 236927 18.0 | 11.683 % | c ============================================================================== c [1mFound solution: 16925420[0m c ---[ 0]---> BDD-cost: 17 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21228 | 41260 141543 | 13753 13162 237702 18.1 | 11.683 % | c ============================================================================== c [1mFound solution: 16843216[0m c ---[ 0]---> BDD-cost: 20 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21243 | 41281 141590 | 13760 13177 237963 18.1 | 11.683 % | c ============================================================================== c [1mFound solution: 16843088[0m c ---[ 0]---> BDD-cost: 18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21276 | 41303 141638 | 13767 13210 238384 18.0 | 11.683 % | c ============================================================================== c [1mFound solution: 16843048[0m c ---[ 0]---> BDD-cost: 20 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21333 | 41328 141692 | 13776 13267 239350 18.0 | 11.683 % | c ============================================================================== c [1mFound solution: 16842952[0m c ---[ 0]---> BDD-cost: 19 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21360 | 41350 141740 | 13783 13294 239609 18.0 | 11.683 % | c ============================================================================== c [1mFound solution: 16842824[0m c ---[ 0]---> BDD-cost: 18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21376 | 41371 141785 | 13790 13310 239981 18.0 | 11.683 % | c | 21477 | 41371 141785 | 15169 13411 243658 18.2 | 17.571 % | c ============================================================================== c [1mFound solution: 16842800[0m c ---[ 0]---> BDD-cost: 19 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21480 | 41393 141832 | 13797 13414 243694 18.2 | 17.571 % | c ============================================================================== c [1mFound solution: 16802120[0m c ---[ 0]---> BDD-cost: 17 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21482 | 41413 141876 | 13804 13416 243714 18.2 | 17.571 % | c ============================================================================== c [1mFound solution: 16801992[0m c ---[ 0]---> BDD-cost: 12 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21483 | 41431 141915 | 13810 13417 243718 18.2 | 17.571 % | c ============================================================================== c [1mFound solution: 16794312[0m c ---[ 0]---> BDD-cost: 16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21494 | 41451 141958 | 13817 13428 244036 18.2 | 17.571 % | c ============================================================================== c [1mFound solution: 1089872[0m c ---[ 0]---> BDD-cost: 8 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21505 | 39988 137582 | 13329 13438 244139 18.2 | 17.571 % | c ============================================================================== c [1mFound solution: 1057360[0m c ---[ 0]---> BDD-cost: 13 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21548 | 40004 137617 | 13334 13481 244974 18.2 | 17.571 % | c | 21649 | 40004 137617 | 14667 13582 246362 18.1 | 22.246 % | c ============================================================================== c [1mFound solution: 549488[0m c ---[ 0]---> BDD-cost: 12 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21781 | 39647 136538 | 13215 13714 247951 18.1 | 22.246 % | c | 21882 | 39647 136538 | 14536 13815 249902 18.1 | 23.410 % | c ============================================================================== c [1mFound solution: 541128[0m c ---[ 0]---> BDD-cost: 12 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21900 | 39661 136569 | 13220 13833 250160 18.1 | 23.410 % | c ============================================================================== c [1mFound solution: 541104[0m c ---[ 0]---> BDD-cost: 13 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21958 | 39677 136605 | 13225 13891 251335 18.1 | 23.410 % | c ============================================================================== c [1mFound solution: 533096[0m c ---[ 0]---> BDD-cost: 14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 22011 | 39694 136643 | 13231 13944 251906 18.1 | 23.410 % | c ============================================================================== c [1mFound solution: 532912[0m c ---[ 0]---> BDD-cost: 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 22046 | 39707 136671 | 13235 13979 252255 18.0 | 23.410 % | c | 22146 | 39707 136671 | 14558 14079 254404 18.1 | 23.399 % | c | 22297 | 39707 136671 | 16014 14230 258111 18.1 | 23.399 % | c ============================================================================== c [1mFound solution: 524840[0m c ---[ 0]---> BDD-cost: 12 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 22356 | 39721 136701 | 13240 14289 259053 18.1 | 23.399 % | c | 22457 | 39721 136701 | 14564 14390 261256 18.2 | 23.400 % | c ============================================================================== c [1mFound solution: 524456[0m c ---[ 0]---> BDD-cost: 13 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 22508 | 39737 136735 | 13245 14441 262006 18.1 | 23.400 % | c | 22608 | 39737 136735 | 14569 14541 263909 18.1 | 23.400 % | c ============================================================================== c [1mFound solution: 417904[0m c ---[ 0]---> BDD-cost: 10 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 22757 | 39369 135629 | 13123 14687 266746 18.2 | 23.400 % | c | 22858 | 39369 135629 | 14435 14788 267487 18.1 | 24.565 % | c | 23008 | 39369 135629 | 15878 14938 270083 18.1 | 24.565 % | c | 23233 | 39369 135629 | 17466 15163 274070 18.1 | 24.565 % | c ============================================================================== c [1mFound solution: 395688[0m c ---[ 0]---> BDD-cost: 11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 23423 | 39381 135657 | 13127 15353 278644 18.1 | 24.565 % | c | 23523 | 39381 135657 | 14439 15453 279656 18.1 | 24.563 % | c ============================================================================== c [1mFound solution: 393904[0m c ---[ 0]---> BDD-cost: 11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 23553 | 39394 135687 | 13131 15483 279943 18.1 | 24.563 % | c | 23653 | 39394 135687 | 14444 15583 283566 18.2 | 24.560 % | c | 23804 | 39394 135687 | 15888 15734 285775 18.2 | 24.560 % | c | 24029 | 39394 135687 | 17477 15959 290529 18.2 | 24.560 % | c ============================================================================== c [1mFound solution: 393808[0m c ---[ 0]---> BDD-cost: 6 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 24085 | 39400 135701 | 13133 16015 291264 18.2 | 24.560 % | c | 24185 | 39400 135701 | 14446 8108 112118 13.8 | 24.565 % | c | 24335 | 39400 135701 | 15890 8258 114874 13.9 | 24.565 % | c | 24560 | 39400 135701 | 17480 8483 117944 13.9 | 24.565 % | c | 24897 | 39400 135701 | 19228 8820 126749 14.4 | 24.565 % | c ============================================================================== c [1mFound solution: 260392[0m c ---[ 0]---> BDD-cost: 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 25195 | 39021 134582 | 13007 9089 131044 14.4 | 24.565 % | c | 25295 | 39021 134582 | 14307 9189 132553 14.4 | 25.732 % | c ============================================================================== c [1mFound solution: 207024[0m c ---[ 0]---> BDD-cost: 9 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 25444 | 39032 134608 | 13010 9338 134811 14.4 | 25.732 % | c | 25546 | 39032 134608 | 14311 9440 136342 14.4 | 25.727 % | c | 25696 | 39032 134608 | 15742 9590 138193 14.4 | 25.727 % | c | 25922 | 39032 134608 | 17316 9816 142910 14.6 | 25.727 % | c | 26259 | 39032 134608 | 19047 10153 154922 15.3 | 25.727 % | c | 26765 | 39032 134608 | 20952 10659 162075 15.2 | 25.727 % | c ============================================================================== c [1mFound solution: 205128[0m c ---[ 0]---> BDD-cost: 4 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 26880 | 39037 134621 | 13012 10774 163689 15.2 | 25.727 % | c | 26980 | 39037 134621 | 14313 10874 166829 15.3 | 25.729 % | c ============================================================================== c [1mFound solution: 133232[0m c ---[ 0]---> BDD-cost: 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 27062 | 39048 134645 | 13016 10956 168619 15.4 | 25.729 % | c | 27163 | 39048 134645 | 14317 11057 170329 15.4 | 25.729 % | c | 27313 | 39048 134645 | 15749 11207 173065 15.4 | 25.729 % | c | 27538 | 39048 134645 | 17324 11432 178462 15.6 | 25.729 % | c | 27875 | 39048 134645 | 19056 11769 182810 15.5 | 25.729 % | c ============================================================================== c [1mFound solution: 133200[0m c ---[ 0]---> BDD-cost: 9 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 28325 | 39059 134669 | 13019 12219 193689 15.9 | 25.729 % | c | 28425 | 39059 134669 | 14320 12319 194556 15.8 | 25.729 % | c | 28576 | 39059 134669 | 15752 12470 196514 15.8 | 25.729 % | c | 28801 | 39059 134669 | 17328 12695 201451 15.9 | 25.729 % | c | 29139 | 39059 134669 | 19061 13033 208907 16.0 | 25.729 % | c | 29645 | 39051 134643 | 20967 13538 226639 16.7 | 25.738 % | c | 30404 | 39051 134643 | 23063 14297 253608 17.7 | 25.738 % | c | 31544 | 39051 134643 | 25370 15437 286261 18.5 | 25.738 % | c | 33252 | 39051 134643 | 27907 17145 345047 20.1 | 25.738 % | c | 35814 | 39051 134643 | 30698 19707 458444 23.3 | 25.738 % | c ============================================================================== c [1mFound solution: 133180[0m c ---[ 0]---> BDD-cost: 10 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 38108 | 39063 134669 | 13021 22001 535927 24.4 | 25.738 % | c | 38208 | 39063 134669 | 14323 11101 337736 30.4 | 25.738 % | c | 38358 | 39063 134669 | 15755 11251 338644 30.1 | 25.738 % | c | 38583 | 39063 134669 | 17330 11476 340916 29.7 | 25.738 % | c | 38920 | 39063 134669 | 19064 11813 349902 29.6 | 25.738 % | c | 39426 | 39063 134669 | 20970 12319 362901 29.5 | 25.738 % | c | 40185 | 39063 134669 | 23067 13078 387122 29.6 | 25.738 % | c ============================================================================== c [1mFound solution: 131384[0m c ---[ 0]---> BDD-cost: 11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 40644 | 39076 134697 | 13025 13537 399586 29.5 | 25.738 % | c | 40744 | 39076 134697 | 14327 13637 400951 29.4 | 25.738 % | c | 40894 | 39076 134697 | 15760 13787 402020 29.2 | 25.738 % | c | 41120 | 39076 134697 | 17336 14013 406130 29.0 | 25.738 % | c | 41457 | 39076 134697 | 19069 14350 415137 28.9 | 25.738 % | c | 41963 | 39076 134697 | 20976 14856 424000 28.5 | 25.738 % | c | 42724 | 39076 134697 | 23074 15617 445193 28.5 | 25.738 % | c | 43864 | 39076 134697 | 25382 16757 482375 28.8 | 25.738 % | c | 45572 | 39076 134697 | 27920 18465 536753 29.1 | 25.738 % | c ============================================================================== c [1mFound solution: 131380[0m c ---[ 0]---> BDD-cost: 12 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 47718 | 39091 134730 | 13030 20611 615821 29.9 | 25.738 % | c | 47818 | 39091 134730 | 14333 10406 270410 26.0 | 25.735 % | c | 47968 | 39091 134730 | 15766 10556 272937 25.9 | 25.735 % | c | 48193 | 39091 134730 | 17342 10781 278006 25.8 | 25.735 % | c | 48530 | 39091 134730 | 19077 11118 287532 25.9 | 25.735 % | c | 49037 | 39091 134730 | 20984 11625 299319 25.7 | 25.735 % | c | 49796 | 39091 134730 | 23083 12384 312167 25.2 | 25.735 % | c | 50936 | 39091 134730 | 25391 13524 348770 25.8 | 25.735 % | c ============================================================================== c [1mFound solution: 131204[0m c ---[ 0]---> BDD-cost: 13 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 51868 | 39106 134762 | 13035 14456 378584 26.2 | 25.735 % | c | 51969 | 39106 134762 | 14338 14557 379741 26.1 | 25.735 % | c | 52121 | 39106 134762 | 15772 14709 383251 26.1 | 25.735 % | c | 52347 | 39106 134762 | 17349 14935 384408 25.7 | 25.735 % | c | 52685 | 39106 134762 | 19084 15273 392157 25.7 | 25.735 % | c | 53193 | 39106 134762 | 20992 15781 406678 25.8 | 25.735 % | c | 53954 | 39106 134762 | 23092 16542 423868 25.6 | 25.735 % | c | 55093 | 39106 134762 | 25401 17681 462147 26.1 | 25.735 % | c | 56802 | 39106 134762 | 27941 19390 534136 27.5 | 25.735 % | c | 59364 | 39106 134762 | 30735 21952 641075 29.2 | 25.735 % | c ============================================================================== c [1mFound solution: 131156[0m c ---[ 0]---> BDD-cost: 10 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 61234 | 39117 134785 | 13039 23822 706396 29.7 | 25.735 % | c | 61337 | 39117 134785 | 14342 12014 354465 29.5 | 25.739 % | c | 61487 | 39117 134785 | 15777 12164 356251 29.3 | 25.739 % | c | 61713 | 39117 134785 | 17354 12390 358485 28.9 | 25.739 % | c ============================================================================== c [1mFound solution: 131108[0m c ---[ 0]---> BDD-cost: 12 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 61998 | 39131 134815 | 13043 12675 364164 28.7 | 25.739 % | c | 62099 | 39125 134797 | 14347 12775 364738 28.6 | 25.751 % | c | 62249 | 39125 134797 | 15782 12925 366990 28.4 | 25.751 % | c | 62476 | 39125 134797 | 17360 13152 369268 28.1 | 25.751 % | c | 62813 | 39125 134797 | 19096 13489 381222 28.3 | 25.751 % | c | 63319 | 39125 134797 | 21005 13995 391288 28.0 | 25.751 % | c | 64079 | 39125 134797 | 23106 14755 405724 27.5 | 25.751 % | c | 65218 | 39125 134797 | 25417 15894 448008 28.2 | 25.751 % | c | 66926 | 39125 134797 | 27958 17602 527035 29.9 | 25.751 % | c ============================================================================== c [1mFound solution: 131104[0m c ---[ 0]---> BDD-cost: 12 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 67828 | 39138 134824 | 13046 18504 547478 29.6 | 25.751 % | c | 67929 | 39138 134824 | 14350 9353 230557 24.7 | 25.756 % | c | 68079 | 39138 134824 | 15785 9503 233676 24.6 | 25.756 % | c | 68307 | 39138 134824 | 17364 9731 237018 24.4 | 25.756 % | c | 68644 | 39138 134824 | 19100 10068 244283 24.3 | 25.756 % | c | 69151 | 39138 134824 | 21010 10575 260658 24.6 | 25.756 % | c | 69910 | 39138 134824 | 23111 11334 281405 24.8 | 25.756 % | c ============================================================================== c [1mFound solution: 131100[0m c ---[ 0]---> BDD-cost: 11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 71036 | 39150 134849 | 13050 12460 310068 24.9 | 25.756 % | c | 71136 | 39150 134849 | 14355 12560 310767 24.7 | 25.760 % | c | 71286 | 39150 134849 | 15790 12710 312186 24.6 | 25.760 % | c | 71511 | 39150 134849 | 17369 12935 315165 24.4 | 25.760 % | c | 71849 | 39150 134849 | 19106 13273 321417 24.2 | 25.760 % | c | 72357 | 39150 134849 | 21017 13781 328981 23.9 | 25.760 % | c ============================================================================== c [1mFound solution: 131096[0m c ---[ 0]---> BDD-cost: 12 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 72614 | 39163 134876 | 13054 14038 333829 23.8 | 25.760 % | c | 72715 | 39163 134876 | 14359 14139 335158 23.7 | 25.765 % | c | 72865 | 39163 134876 | 15795 14289 336963 23.6 | 25.765 % | c | 73090 | 39163 134876 | 17374 14514 343417 23.7 | 25.765 % | c | 73427 | 39163 134876 | 19112 14851 348569 23.5 | 25.765 % | c | 73935 | 39163 134876 | 21023 15359 359386 23.4 | 25.765 % | c | 74694 | 39163 134876 | 23125 16118 389148 24.1 | 25.765 % | c ============================================================================== c [1mFound solution: 131092[0m c ---[ 0]---> BDD-cost: 12 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 75061 | 39176 134903 | 13058 16485 399370 24.2 | 25.765 % | c | 75162 | 39176 134903 | 14363 8344 162481 19.5 | 25.770 % | c | 75313 | 39176 134903 | 15800 8495 164035 19.3 | 25.770 % | c | 75540 | 39176 134903 | 17380 8722 168515 19.3 | 25.770 % | c | 75878 | 39176 134903 | 19118 9060 170735 18.8 | 25.770 % | c | 76384 | 39176 134903 | 21030 9566 180752 18.9 | 25.770 % | c | 77143 | 39176 134903 | 23133 10325 200571 19.4 | 25.770 % | c | 78282 | 39176 134903 | 25446 11464 232693 20.3 | 25.770 % | c | 79991 | 39176 134903 | 27990 13173 280335 21.3 | 25.770 % | c | 82555 | 39176 134903 | 30790 15737 366968 23.3 | 25.770 % | c | 86400 | 39176 134903 | 33869 19582 523768 26.7 | 25.770 % | c | 92166 | 39176 134903 | 37255 25348 797014 31.4 | 25.770 % | c | 100815 | 39176 134903 | 40981 33997 1125918 33.1 | 25.770 % | c ============================================================================== c [1mFound solution: 131084[0m c ---[ 0]---> BDD-cost: 13 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 101117 | 39190 134932 | 13063 34299 1133621 33.1 | 25.770 % | c | 101218 | 39190 134932 | 14369 13602 482280 35.5 | 25.774 % | c | 101369 | 39190 134932 | 15806 13753 485715 35.3 | 25.774 % | c | 101594 | 39190 134932 | 17386 13978 490408 35.1 | 25.774 % | c | 101931 | 39190 134932 | 19125 14315 497476 34.8 | 25.774 % | c | 102437 | 39190 134932 | 21038 14821 515337 34.8 | 25.774 % | c | 103196 | 39190 134932 | 23141 15580 540109 34.7 | 25.774 % | c | 104335 | 39190 134932 | 25456 16719 576829 34.5 | 25.774 % | c | 106043 | 39190 134932 | 28001 18427 628147 34.1 | 25.774 % | c | 108605 | 39190 134932 | 30801 20989 714744 34.1 | 25.774 % | c ============================================================================== c [1mFound solution: 131076[0m c ---[ 0]---> BDD-cost: 11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 109167 | 39202 134957 | 13067 21551 729617 33.9 | 25.774 % | c | 109267 | 39202 134957 | 14373 10876 284939 26.2 | 25.779 % | c | 109418 | 39202 134957 | 15811 11027 287980 26.1 | 25.779 % | c | 109643 | 39202 134957 | 17392 11252 293622 26.1 | 25.779 % | c | 109980 | 39202 134957 | 19131 11589 302450 26.1 | 25.779 % | c | 110487 | 39202 134957 | 21044 12096 321704 26.6 | 25.779 % | c | 111247 | 39202 134957 | 23148 12856 351889 27.4 | 25.779 % | c | 112389 | 39202 134957 | 25463 13998 384964 27.5 | 25.779 % | c | 114098 | 39202 134957 | 28010 15707 439623 28.0 | 25.779 % | c ============================================================================== c [1mFound solution: 131072[0m c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 115519 | 38806 133760 | 12935 16932 473338 28.0 | 25.779 % | c | 115619 | 38806 133760 | 14228 8566 220962 25.8 | 26.936 % | c | 115770 | 38806 133760 | 15651 8717 221968 25.5 | 26.936 % | c | 115996 | 38806 133760 | 17216 8943 224909 25.1 | 26.936 % | c | 116333 | 38806 133760 | 18938 9280 227719 24.5 | 26.936 % | c | 116839 | 38806 133760 | 20831 9786 241119 24.6 | 26.936 % | c | 117598 | 38806 133760 | 22915 10545 258680 24.5 | 26.936 % | c | 118738 | 38806 133760 | 25206 11685 287935 24.6 | 26.936 % | c ============================================================================== c [1mFound solution: 126120[0m c ---[ 0]---> BDD-cost: 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 119383 | 38813 133780 | 12937 12330 303880 24.6 | 26.936 % | c | 119483 | 38813 133780 | 14230 12430 304420 24.5 | 26.935 % | c | 119634 | 38813 133780 | 15653 12581 307440 24.4 | 26.935 % | c | 119859 | 38813 133780 | 17219 12806 311397 24.3 | 26.935 % | c | 120197 | 38813 133780 | 18941 13144 323645 24.6 | 26.935 % | c | 120703 | 38813 133780 | 20835 13650 337601 24.7 | 26.935 % | c | 121464 | 38813 133780 | 22918 14411 357327 24.8 | 26.935 % | c | 122604 | 38813 133780 | 25210 15551 395203 25.4 | 26.935 % | c | 124312 | 38813 133780 | 27731 17259 444838 25.8 | 26.935 % | c | 126874 | 38813 133780 | 30504 19821 558537 28.2 | 26.935 % | c ============================================================================== c [1mFound solution: 123028[0m c ---[ 0]---> BDD-cost: 10 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 127912 | 38823 133805 | 12941 20859 586339 28.1 | 26.935 % | c | 128012 | 38823 133805 | 14235 10530 294234 27.9 | 26.934 % | c | 128162 | 38823 133805 | 15658 10680 298948 28.0 | 26.934 % | c | 128389 | 38823 133805 | 17224 10907 302544 27.7 | 26.934 % | c ============================================================================== c [1mFound solution: 123024[0m c ---[ 0]---> BDD-cost: 11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 128649 | 38833 133830 | 12944 11167 306992 27.5 | 26.934 % | c | 128749 | 38833 133830 | 14238 11267 309252 27.4 | 26.933 % | c | 128900 | 38833 133830 | 15662 11418 310352 27.2 | 26.933 % | c | 129127 | 38833 133830 | 17228 11645 315950 27.1 | 26.933 % | c | 129466 | 38827 133812 | 18951 11983 318482 26.6 | 26.943 % | c ============================================================================== c [1mFound solution: 121364[0m c ---[ 0]---> BDD-cost: 8 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 129839 | 38837 133838 | 12945 12356 326480 26.4 | 26.943 % | c | 129940 | 38837 133838 | 14239 12457 327047 26.3 | 26.937 % | c | 130091 | 38837 133838 | 15663 12608 331504 26.3 | 26.937 % | c | 130318 | 38837 133838 | 17229 12835 333781 26.0 | 26.937 % | c | 130655 | 38837 133838 | 18952 13172 340629 25.9 | 26.937 % | c | 131161 | 38837 133838 | 20848 13678 347246 25.4 | 26.937 % | c | 131922 | 38837 133838 | 22932 14439 368863 25.5 | 26.937 % | c | 133061 | 38837 133838 | 25226 15578 397869 25.5 | 26.937 % | c | 134769 | 38837 133838 | 27748 17286 457795 26.5 | 26.937 % | c | 137331 | 38837 133838 | 30523 19848 549990 27.7 | 26.937 % | c | 141175 | 38837 133838 | 33575 23692 713378 30.1 | 26.937 % | c | 146941 | 38837 133838 | 36933 29458 983956 33.4 | 26.937 % | c | 155590 | 38837 133838 | 40626 38107 1306102 34.3 | 26.937 % | c | 168564 | 38837 133838 | 44689 21147 791029 37.4 | 26.937 % | c | 188026 | 38837 133838 | 49158 40609 1510764 37.2 | 26.937 % | c ============================================================================== c [1mFound solution: 114912[0m c ---[ 0]---> BDD-cost: 11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 188582 | 38846 133861 | 12948 41165 1524272 37.0 | 26.937 % | c | 188683 | 38846 133861 | 14242 14167 454792 32.1 | 26.939 % | c | 188838 | 38846 133861 | 15667 14322 459367 32.1 | 26.939 % | c | 189064 | 38846 133861 | 17233 14548 462200 31.8 | 26.939 % | c | 189402 | 38846 133861 | 18957 14886 470357 31.6 | 26.939 % | c | 189908 | 38846 133861 | 20852 15392 481020 31.3 | 26.939 % | c | 190668 | 38846 133861 | 22938 16152 502435 31.1 | 26.939 % | c | 191808 | 38846 133861 | 25231 17292 544452 31.5 | 26.939 % | c | 193518 | 38840 133843 | 27755 19001 593245 31.2 | 26.948 % | c | 196080 | 38840 133843 | 30530 21563 664136 30.8 | 26.948 % | c | 199926 | 38840 133843 | 33583 25409 827199 32.6 | 26.948 % | c ============================================================================== c [1mFound solution: 111236[0m c ---[ 0]---> BDD-cost: 8 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 202521 | 38850 133868 | 12950 28004 912712 32.6 | 26.948 % | c | 202621 | 38850 133868 | 14245 12227 386405 31.6 | 26.943 % | c | 202771 | 38850 133868 | 15669 12377 387224 31.3 | 26.943 % | c | 202996 | 38850 133868 | 17236 12602 389800 30.9 | 26.943 % | c | 203334 | 38850 133868 | 18960 12940 395488 30.6 | 26.943 % | c | 203840 | 38850 133868 | 20856 13446 408903 30.4 | 26.943 % | c | 204600 | 38850 133868 | 22941 14206 425580 30.0 | 26.943 % | c | 205740 | 38850 133868 | 25235 15346 460683 30.0 | 26.943 % | c | 207450 | 38850 133868 | 27759 17056 511710 30.0 | 26.943 % | c ============================================================================== c [1mFound solution: 108220[0m c ---[ 0]---> BDD-cost: 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 207792 | 38858 133888 | 12952 17398 515518 29.6 | 26.943 % | c | 207893 | 38858 133888 | 14247 8800 211655 24.1 | 26.939 % | c | 208044 | 38858 133888 | 15671 8951 214209 23.9 | 26.939 % | c | 208269 | 38858 133888 | 17239 9176 217859 23.7 | 26.939 % | c | 208606 | 38858 133888 | 18963 9513 221146 23.2 | 26.939 % | c | 209112 | 38858 133888 | 20859 10019 235755 23.5 | 26.939 % | c | 209871 | 38858 133888 | 22945 10778 252841 23.5 | 26.939 % | c | 211011 | 38858 133888 | 25239 11918 289774 24.3 | 26.939 % | c | 212719 | 38858 133888 | 27763 13626 330797 24.3 | 26.939 % | c ============================================================================== c [1mFound solution: 108200[0m c ---[ 0]---> BDD-cost: 8 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 214294 | 38868 133913 | 12956 15201 375364 24.7 | 26.939 % | c | 214396 | 38868 133913 | 14251 15303 376546 24.6 | 26.933 % | c | 214548 | 38868 133913 | 15676 15455 379112 24.5 | 26.933 % | c | 214773 | 38868 133913 | 17244 15680 381928 24.4 | 26.933 % | c | 215111 | 38868 133913 | 18968 16018 391625 24.4 | 26.933 % | c | 215617 | 38868 133913 | 20865 16524 408652 24.7 | 26.933 % | c | 216376 | 38868 133913 | 22952 17283 427024 24.7 | 26.933 % | c | 217516 | 38868 133913 | 25247 18423 469541 25.5 | 26.933 % | c | 219224 | 38868 133913 | 27772 20131 525952 26.1 | 26.933 % | c | 221786 | 38868 133913 | 30549 22693 627608 27.7 | 26.933 % | c | 225631 | 38868 133913 | 33604 26538 792211 29.9 | 26.933 % | c | 231399 | 38868 133913 | 36964 32306 1056093 32.7 | 26.933 % | c | 240048 | 38868 133913 | 40661 14371 543117 37.8 | 26.933 % | c ============================================================================== c [1mFound solution: 107848[0m c ---[ 0]---> BDD-cost: 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 246754 | 38878 133937 | 12959 21077 813482 38.6 | 26.933 % | c | 246855 | 38878 133937 | 14254 10640 371697 34.9 | 26.927 % | c | 247005 | 38878 133937 | 15680 10790 373900 34.7 | 26.927 % | c | 247232 | 38878 133937 | 17248 11017 376730 34.2 | 26.927 % | c | 247569 | 38878 133937 | 18973 11354 382411 33.7 | 26.927 % | c | 248075 | 38878 133937 | 20870 11860 391947 33.0 | 26.927 % | c | 248834 | 38878 133937 | 22957 12619 409489 32.5 | 26.927 % | c | 249973 | 38878 133937 | 25253 13758 448235 32.6 | 26.927 % | c | 251681 | 38878 133937 | 27778 15466 501764 32.4 | 26.927 % | c | 254243 | 38878 133937 | 30556 18028 583608 32.4 | 26.927 % | c | 258088 | 38878 133937 | 33612 21873 716094 32.7 | 26.927 % | c ============================================================================== c [1mFound solution: 107564[0m c ---[ 0]---> BDD-cost: 9 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 258916 | 38889 133963 | 12963 22701 735933 32.4 | 26.927 % | c | 259017 | 38889 133963 | 14259 11452 333513 29.1 | 26.922 % | c | 259168 | 38889 133963 | 15685 11603 335752 28.9 | 26.922 % | c | 259393 | 38889 133963 | 17253 11828 341207 28.8 | 26.922 % | c | 259732 | 38889 133963 | 18979 12167 348465 28.6 | 26.922 % | c | 260239 | 38889 133963 | 20877 12674 361972 28.6 | 26.922 % | c | 260998 | 38889 133963 | 22964 13433 382482 28.5 | 26.922 % | c | 262138 | 38889 133963 | 25261 14573 426046 29.2 | 26.922 % | c | 263846 | 38889 133963 | 27787 16281 479903 29.5 | 26.922 % | c | 266408 | 38889 133963 | 30566 18843 596010 31.6 | 26.922 % | c | 270252 | 38889 133963 | 33622 22687 753437 33.2 | 26.922 % | c ============================================================================== c [1mFound solution: 107476[0m c ---[ 0]---> BDD-cost: 9 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 270933 | 38898 133986 | 12966 23368 775588 33.2 | 26.922 % | c | 271033 | 38898 133986 | 14262 11784 392745 33.3 | 26.918 % | c | 271186 | 38898 133986 | 15688 11937 395577 33.1 | 26.918 % | c | 271413 | 38898 133986 | 17257 12164 396863 32.6 | 26.918 % | c | 271751 | 38898 133986 | 18983 12502 401619 32.1 | 26.918 % | c | 272258 | 38898 133986 | 20881 13009 414256 31.8 | 26.918 % | c | 273017 | 38898 133986 | 22970 13768 435381 31.6 | 26.918 % | c | 274157 | 38898 133986 | 25267 14908 456285 30.6 | 26.918 % | c | 275865 | 38898 133986 | 27793 16616 516588 31.1 | 26.918 % | c | 278428 | 38898 133986 | 30573 19179 598051 31.2 | 26.918 % | c ============================================================================== c [1mFound solution: 106804[0m c ---[ 0]---> BDD-cost: 4 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 279286 | 38907 134007 | 12969 20037 619114 30.9 | 26.918 % | c | 279386 | 38907 134007 | 14265 10119 238307 23.6 | 26.918 % | c | 279536 | 38907 134007 | 15692 10269 240223 23.4 | 26.918 % | c | 279762 | 38907 134007 | 17261 10495 243969 23.2 | 26.918 % | c | 280100 | 38907 134007 | 18987 10833 248654 23.0 | 26.918 % | c | 280607 | 38907 134007 | 20886 11340 260665 23.0 | 26.918 % | c ============================================================================== c [1mFound solution: 104616[0m c ---[ 0]---> BDD-cost: 6 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 281188 | 38914 134025 | 12971 11921 273133 22.9 | 26.918 % | c | 281291 | 38914 134025 | 14268 12024 273810 22.8 | 26.917 % | c | 281441 | 38914 134025 | 15694 12174 276538 22.7 | 26.917 % | c | 281666 | 38914 134025 | 17264 12399 281289 22.7 | 26.917 % | c | 282003 | 38914 134025 | 18990 12736 287643 22.6 | 26.917 % | c | 282510 | 38914 134025 | 20889 13243 303095 22.9 | 26.917 % | c | 283269 | 38914 134025 | 22978 14002 332397 23.7 | 26.917 % | c | 284410 | 38914 134025 | 25276 15143 372583 24.6 | 26.917 % | c | 286119 | 38914 134025 | 27804 16852 433958 25.8 | 26.917 % | c | 288681 | 38914 134025 | 30584 19414 527372 27.2 | 26.917 % | c | 292525 | 38914 134025 | 33643 23258 698734 30.0 | 26.917 % | c ============================================================================== c [1mFound solution: 102696[0m c ---[ 0]---> BDD-cost: 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 297223 | 38921 134042 | 12973 27956 869879 31.1 | 26.917 % | c | 297326 | 38921 134042 | 14270 13421 445740 33.2 | 26.916 % | c | 297476 | 38921 134042 | 15697 13571 446951 32.9 | 26.916 % | c | 297701 | 38921 134042 | 17267 13796 451238 32.7 | 26.916 % | c | 298038 | 38921 134042 | 18993 14133 455250 32.2 | 26.916 % | c | 298544 | 38921 134042 | 20893 14639 475977 32.5 | 26.916 % | c | 299303 | 38921 134042 | 22982 15398 501467 32.6 | 26.916 % | c ============================================================================== c [1mFound solution: 102692[0m c ---[ 0]---> BDD-cost: 9 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 299988 | 38934 134072 | 12978 16083 521737 32.4 | 26.916 % | c | 300088 | 38934 134072 | 14275 8142 207776 25.5 | 26.910 % | c | 300240 | 38934 134072 | 15703 8294 209888 25.3 | 26.910 % | c | 300465 | 38934 134072 | 17273 8519 214352 25.2 | 26.910 % | c | 300803 | 38934 134072 | 19001 8857 221516 25.0 | 26.910 % | c | 301309 | 38934 134072 | 20901 9363 233973 25.0 | 26.910 % | c | 302069 | 38934 134072 | 22991 10123 252495 24.9 | 26.910 % | c | 303210 | 38934 134072 | 25290 11264 287941 25.6 | 26.910 % | c | 304918 | 38934 134072 | 27819 12972 355470 27.4 | 26.910 % | c ============================================================================== c [1mFound solution: 102680[0m c ---[ 0]---> BDD-cost: 9 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 306525 | 38947 134102 | 12982 14579 412429 28.3 | 26.910 % | c | 306626 | 38947 134102 | 14280 14680 412990 28.1 | 26.904 % | c | 306777 | 38947 134102 | 15708 14831 415673 28.0 | 26.904 % | c | 307002 | 38947 134102 | 17279 15056 417571 27.7 | 26.904 % | c | 307340 | 38947 134102 | 19006 15394 421855 27.4 | 26.904 % | c | 307846 | 38947 134102 | 20907 15900 433221 27.2 | 26.904 % | c | 308606 | 38947 134102 | 22998 16660 457665 27.5 | 26.904 % | c | 309745 | 38947 134102 | 25298 17799 492631 27.7 | 26.904 % | c | 311453 | 38947 134102 | 27828 19507 551067 28.2 | 26.904 % | c | 314017 | 38947 134102 | 30610 22071 643869 29.2 | 26.904 % | c | 317862 | 38947 134102 | 33671 25916 781974 30.2 | 26.904 % | c ============================================================================== c [1mFound solution: 102584[0m c ---[ 0]---> BDD-cost: 9 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 323254 | 38958 134128 | 12986 31308 1005523 32.1 | 26.904 % | c | 323356 | 38958 134128 | 14284 13784 450075 32.7 | 26.901 % | c | 323506 | 38958 134128 | 15713 13934 453548 32.5 | 26.901 % | c | 323731 | 38958 134128 | 17284 14159 456333 32.2 | 26.901 % | c | 324069 | 38958 134128 | 19012 14497 464818 32.1 | 26.901 % | c ============================================================================== c [1mFound solution: 102572[0m c ---[ 0]---> BDD-cost: 8 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 324232 | 38967 134149 | 12989 14660 468187 31.9 | 26.901 % | c | 324333 | 38967 134149 | 14287 14761 468993 31.8 | 26.900 % | c | 324485 | 38967 134149 | 15716 14913 471539 31.6 | 26.900 % | c | 324710 | 38967 134149 | 17288 15138 476523 31.5 | 26.900 % | c | 325048 | 38967 134149 | 19017 15476 481757 31.1 | 26.900 % | c | 325555 | 38967 134149 | 20918 15983 496698 31.1 | 26.900 % | c | 326314 | 38967 134149 | 23010 16742 514528 30.7 | 26.900 % | c | 327453 | 38967 134149 | 25311 17881 544551 30.5 | 26.900 % | c ============================================================================== c [1mFound solution: 101972[0m c ---[ 0]---> BDD-cost: 8 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 328218 | 38975 134170 | 12991 18646 567951 30.5 | 26.900 % | c | 328318 | 38975 134170 | 14290 9423 255648 27.1 | 26.900 % | c | 328468 | 38975 134170 | 15719 9573 257567 26.9 | 26.900 % | c | 328693 | 38975 134170 | 17291 9798 260473 26.6 | 26.900 % | c | 329030 | 38975 134170 | 19020 10135 269089 26.6 | 26.900 % | c | 329537 | 38975 134170 | 20922 10642 277671 26.1 | 26.900 % | c | 330296 | 38975 134170 | 23014 11401 299092 26.2 | 26.900 % | c | 331436 | 38975 134170 | 25315 12541 321346 25.6 | 26.900 % | c | 333144 | 38975 134170 | 27847 14249 366429 25.7 | 26.900 % | c | 335706 | 38975 134170 | 30632 16811 469487 27.9 | 26.900 % | c | 339551 | 38975 134170 | 33695 20656 586898 28.4 | 26.900 % | c | 345318 | 38975 134170 | 37064 26423 879941 33.3 | 26.900 % | c | 353973 | 38975 134170 | 40771 35078 1191024 34.0 | 26.900 % | c | 366947 | 38975 134170 | 44848 16636 638450 38.4 | 26.900 % | c ============================================================================== c [1mFound solution: 101660[0m c ---[ 0]---> BDD-cost: 9 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 377932 | 38986 134197 | 12995 27621 1064351 38.5 | 26.900 % | c | 378032 | 38986 134197 | 14294 12695 437381 34.5 | 26.894 % | c | 378184 | 38986 134197 | 15723 12847 440767 34.3 | 26.894 % | c | 378410 | 38986 134197 | 17296 13073 443101 33.9 | 26.894 % | c | 378748 | 38986 134197 | 19025 13411 450447 33.6 | 26.894 % | c | 379254 | 38986 134197 | 20928 13917 459632 33.0 | 26.894 % | c | 380014 | 38986 134197 | 23021 14677 472908 32.2 | 26.894 % | c | 381153 | 38986 134197 | 25323 15816 500902 31.7 | 26.894 % | c | 382861 | 38986 134197 | 27855 17524 570805 32.6 | 26.894 % | c | 385424 | 38986 134197 | 30641 20087 656576 32.7 | 26.894 % | c | 389270 | 38986 134197 | 33705 23933 810023 33.8 | 26.894 % | c ============================================================================== c [1mFound solution: 101092[0m c ---[ 0]---> BDD-cost: 6 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 390371 | 38994 134216 | 12998 25034 846132 33.8 | 26.894 % | c | 390471 | 38994 134216 | 14297 12617 385734 30.6 | 26.893 % | c | 390621 | 38994 134216 | 15727 12767 386584 30.3 | 26.893 % | c | 390846 | 38994 134216 | 17300 12992 389827 30.0 | 26.893 % | c | 391183 | 38994 134216 | 19030 13329 394309 29.6 | 26.893 % | c | 391691 | 38994 134216 | 20933 13837 406148 29.4 | 26.893 % | c | 392450 | 38994 134216 | 23026 14596 424495 29.1 | 26.893 % | c ============================================================================== c [1mFound solution: 98960[0m c ---[ 0]---> BDD-cost: 8 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 393084 | 39004 134239 | 13001 15230 442436 29.1 | 26.893 % | c | 393184 | 39004 134239 | 14301 15330 443760 28.9 | 26.893 % | c | 393334 | 39004 134239 | 15731 15480 447180 28.9 | 26.893 % | c | 393559 | 39004 134239 | 17304 15705 451817 28.8 | 26.893 % | c | 393899 | 39004 134239 | 19034 16045 459791 28.7 | 26.893 % | c | 394405 | 39004 134239 | 20938 16551 472460 28.5 | 26.893 % | c | 395164 | 39004 134239 | 23032 17310 486635 28.1 | 26.893 % | c | 396303 | 39004 134239 | 25335 18449 521891 28.3 | 26.893 % | c | 398012 | 39004 134239 | 27868 20158 589186 29.2 | 26.893 % | c | 400576 | 39004 134239 | 30655 22722 699275 30.8 | 26.893 % | c ============================================================================== c [1mFound solution: 98564[0m c ---[ 0]---> BDD-cost: 9 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 401698 | 39015 134264 | 13005 23844 735046 30.8 | 26.893 % | c | 401798 | 39015 134264 | 14305 12022 323983 26.9 | 26.892 % | c | 401948 | 39015 134264 | 15736 12172 325991 26.8 | 26.892 % | c | 402173 | 39015 134264 | 17309 12397 332905 26.9 | 26.892 % | c | 402513 | 39015 134264 | 19040 12737 343499 27.0 | 26.892 % | c | 403019 | 39015 134264 | 20944 13243 357174 27.0 | 26.892 % | c | 403778 | 39015 134264 | 23039 14002 375780 26.8 | 26.892 % | c | 404917 | 39015 134264 | 25343 15141 405505 26.8 | 26.892 % | c | 406627 | 39015 134264 | 27877 16851 479981 28.5 | 26.892 % | c | 409189 | 39015 134264 | 30665 19413 558925 28.8 | 26.892 % | c | 413034 | 39015 134264 | 33731 23258 720645 31.0 | 26.892 % | c | 418800 | 39015 134264 | 37104 29024 954518 32.9 | 26.892 % | c ============================================================================== c [1mFound solution: 98492[0m c ---[ 0]---> BDD-cost: 8 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 423892 | 39023 134282 | 13007 34116 1195413 35.0 | 26.892 % | c | 423992 | 39023 134282 | 14307 13590 503963 37.1 | 26.896 % | c | 424142 | 39023 134282 | 15738 13740 505340 36.8 | 26.896 % | c | 424367 | 39023 134282 | 17312 13965 507358 36.3 | 26.896 % | c | 424704 | 39023 134282 | 19043 14302 516329 36.1 | 26.896 % | c | 425210 | 39023 134282 | 20947 14808 531153 35.9 | 26.896 % | c | 425969 | 39023 134282 | 23042 15567 558577 35.9 | 26.896 % | c | 427112 | 39023 134282 | 25346 16710 592352 35.4 | 26.896 % | c | 428820 | 39023 134282 | 27881 18418 662951 36.0 | 26.896 % | c ============================================================================== c [1mFound solution: 98488[0m c ---[ 0]---> BDD-cost: 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 430221 | 39028 134294 | 13009 19819 705104 35.6 | 26.896 % | c | 430321 | 39028 134294 | 14309 10010 275928 27.6 | 26.901 % | c | 430473 | 39028 134294 | 15740 10162 278029 27.4 | 26.901 % | c | 430699 | 39028 134294 | 17314 10388 281521 27.1 | 26.901 % | c | 431037 | 39028 134294 | 19046 10726 290406 27.1 | 26.901 % | c | 431544 | 39028 134294 | 20951 11233 298961 26.6 | 26.901 % | c ============================================================================== c [1mFound solution: 98420[0m c ---[ 0]---> BDD-cost: 8 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 432060 | 39036 134312 | 13012 11749 316135 26.9 | 26.901 % | c | 432160 | 39036 134312 | 14313 11849 317207 26.8 | 26.905 % | c | 432311 | 39036 134312 | 15744 12000 318165 26.5 | 26.905 % | c | 432539 | 39036 134312 | 17318 12228 323458 26.5 | 26.905 % | c | 432876 | 39036 134312 | 19050 12565 328807 26.2 | 26.905 % | c | 433382 | 39036 134312 | 20955 13071 345266 26.4 | 26.905 % | c | 434142 | 39036 134312 | 23051 13831 373766 27.0 | 26.905 % | c | 435281 | 39036 134312 | 25356 14970 408441 27.3 | 26.905 % | c | 436989 | 39036 134312 | 27892 16678 480889 28.8 | 26.905 % | c | 439551 | 39036 134312 | 30681 19240 572878 29.8 | 26.905 % | c | 443396 | 39036 134312 | 33749 23085 727825 31.5 | 26.905 % | c | 449164 | 39036 134312 | 37124 28853 974885 33.8 | 26.905 % | c | 457814 | 39036 134312 | 40837 37503 1427237 38.1 | 26.905 % | c | 470790 | 39036 134312 | 44920 21336 788658 37.0 | 26.905 % | c | 490253 | 39036 134312 | 49413 40799 1756540 43.1 | 26.905 % | c ============================================================================== c [1mFound solution: 98384[0m c ---[ 0]---> BDD-cost: 6 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 498799 | 39042 134326 | 13014 49345 2093267 42.4 | 26.905 % | c | 498899 | 39042 134326 | 14315 14463 506614 35.0 | 26.909 % | c | 499050 | 39042 134326 | 15746 14614 508135 34.8 | 26.909 % | c | 499275 | 39042 134326 | 17321 14839 510992 34.4 | 26.909 % | c | 499616 | 39042 134326 | 19053 15180 519693 34.2 | 26.909 % | c | 500122 | 39042 134326 | 20959 15686 526328 33.6 | 26.909 % | c | 500881 | 39042 134326 | 23055 16445 550493 33.5 | 26.909 % | c | 502020 | 39042 134326 | 25360 17584 597166 34.0 | 26.909 % | c | 503729 | 39042 134326 | 27896 19293 647513 33.6 | 26.909 % | c | 506292 | 39042 134326 | 30686 21856 753169 34.5 | 26.909 % | c | 510136 | 39042 134326 | 33754 25700 858752 33.4 | 26.909 % | c ============================================================================== c [1mFound solution: 98376[0m c ---[ 0]---> BDD-cost: 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 514825 | 39044 134323 | 13014 30388 1021143 33.6 | 26.909 % | c | 514925 | 39044 134323 | 14315 13637 387924 28.4 | 26.923 % | c | 515075 | 39044 134323 | 15746 13787 391676 28.4 | 26.923 % | c | 515301 | 39044 134323 | 17321 14013 396877 28.3 | 26.923 % | c | 515638 | 39044 134323 | 19053 14350 405012 28.2 | 26.923 % | c | 516145 | 39044 134323 | 20959 14857 414304 27.9 | 26.923 % | c | 516904 | 39044 134323 | 23055 15616 434972 27.9 | 26.923 % | c | 518045 | 39044 134323 | 25360 16757 475363 28.4 | 26.923 % | c | 519754 | 39044 134323 | 27896 18466 534669 29.0 | 26.923 % | c | 522317 | 39044 134323 | 30686 21029 624404 29.7 | 26.923 % | c | 526161 | 39044 134323 | 33754 24873 794160 31.9 | 26.923 % | c ============================================================================== c [1mFound solution: 98364[0m c ---[ 0]---> BDD-cost: 6 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 529300 | 39050 134337 | 13016 28012 906795 32.4 | 26.923 % | c | 529401 | 39050 134337 | 14317 13477 436871 32.4 | 26.927 % | c | 529551 | 39050 134337 | 15749 13627 439386 32.2 | 26.927 % | c | 529776 | 39050 134337 | 17324 13852 442420 31.9 | 26.927 % | c | 530113 | 39050 134337 | 19056 14189 449139 31.7 | 26.927 % | c | 530619 | 39050 134337 | 20962 14695 461544 31.4 | 26.927 % | c | 531379 | 39050 134337 | 23058 15455 489145 31.6 | 26.927 % | c | 532520 | 39050 134337 | 25364 16596 513405 30.9 | 26.927 % | c | 534229 | 39050 134337 | 27900 18305 574288 31.4 | 26.927 % | c | 536792 | 39050 134337 | 30691 20868 660406 31.6 | 26.927 % | c | 540638 | 39050 134337 | 33760 24714 817020 33.1 | 26.927 % | c ============================================================================== c [1mFound solution: 96912[0m c ---[ 0]---> BDD-cost: 6 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 543725 | 39056 134354 | 13018 27801 947634 34.1 | 26.927 % | c | 543825 | 39056 134354 | 14319 13170 438732 33.3 | 26.927 % | c | 543976 | 39056 134354 | 15751 13321 440064 33.0 | 26.927 % | c | 544201 | 39056 134354 | 17326 13546 444730 32.8 | 26.927 % | c | 544538 | 39056 134354 | 19059 13883 453714 32.7 | 26.927 % | c | 545045 | 39056 134354 | 20965 14390 461535 32.1 | 26.927 % | c | 545804 | 39056 134354 | 23062 15149 473010 31.2 | 26.927 % | c | 546943 | 39056 134354 | 25368 16288 522762 32.1 | 26.927 % | c | 548652 | 39056 134354 | 27905 17997 572215 31.8 | 26.927 % | c | 551214 | 39056 134354 | 30695 20559 667064 32.4 | 26.927 % | c | 555058 | 39056 134354 | 33765 24403 800149 32.8 | 26.927 % | c | 560824 | 39056 134354 | 37141 30169 1020883 33.8 | 26.927 % | c | 569475 | 39056 134354 | 40856 38820 1433629 36.9 | 26.927 % | c | 582449 | 39056 134354 | 44941 21696 803877 37.1 | 26.927 % | c | 601910 | 39056 134354 | 49435 41157 1681755 40.9 | 26.927 % | c | 631102 | 39049 134331 | 54379 31917 1213914 38.0 | 26.936 % | c | 674891 | 39049 134331 | 59817 32625 1616167 49.5 | 26.936 % | c ============================================================================== c [1mFound solution: 91248[0m c ---[ 0]---> BDD-cost: 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 675520 | 39059 134355 | 13019 33254 1631721 49.1 | 26.936 % | c | 675620 | 39059 134355 | 14320 14958 614359 41.1 | 26.930 % | c | 675770 | 39059 134355 | 15752 15108 615858 40.8 | 26.930 % | c | 675996 | 39059 134355 | 17328 15334 620509 40.5 | 26.930 % | c | 676334 | 39059 134355 | 19061 15672 630125 40.2 | 26.930 % | c | 676840 | 39059 134355 | 20967 16178 635665 39.3 | 26.930 % | c | 677601 | 39059 134355 | 23063 16939 652571 38.5 | 26.930 % | c | 678740 | 39059 134355 | 25370 18078 684726 37.9 | 26.930 % | c | 680449 | 39059 134355 | 27907 19787 737295 37.3 | 26.930 % | c | 683013 | 39059 134355 | 30698 22351 833970 37.3 | 26.930 % | c | 686857 | 39059 134355 | 33767 26195 975474 37.2 | 26.930 % | c | 692624 | 39059 134355 | 37144 31962 1204054 37.7 | 26.930 % | c ============================================================================== c [1mFound solution: 91228[0m c ---[ 0]---> BDD-cost: 8 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 695748 | 39069 134379 | 13023 35086 1305430 37.2 | 26.930 % | c | 695848 | 39069 134379 | 14325 13977 436474 31.2 | 26.925 % | c | 695998 | 39069 134379 | 15757 14127 437559 31.0 | 26.925 % | c | 696223 | 39069 134379 | 17333 14352 439359 30.6 | 26.925 % | c | 696563 | 39069 134379 | 19066 14692 445397 30.3 | 26.925 % | c | 697069 | 39069 134379 | 20973 15198 460349 30.3 | 26.925 % | c | 697828 | 39069 134379 | 23071 15957 479984 30.1 | 26.925 % | c | 698968 | 39069 134379 | 25378 17097 510148 29.8 | 26.925 % | c | 700676 | 39069 134379 | 27915 18805 575493 30.6 | 26.925 % | c | 703238 | 39069 134379 | 30707 21367 660313 30.9 | 26.925 % | c | 707082 | 39069 134379 | 33778 25211 837198 33.2 | 26.925 % | c ============================================================================== c [1mFound solution: 90408[0m c ---[ 0]---> BDD-cost: 4 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 711732 | 39075 134394 | 13025 29861 976240 32.7 | 26.925 % | c | 711832 | 39075 134394 | 14327 12988 412978 31.8 | 26.924 % | c | 711982 | 39075 134394 | 15760 13138 414593 31.6 | 26.924 % | c | 712208 | 39075 134394 | 17336 13364 418198 31.3 | 26.924 % | c | 712547 | 39075 134394 | 19069 13703 423593 30.9 | 26.924 % | c | 713053 | 39075 134394 | 20976 14209 430380 30.3 | 26.924 % | c | 713812 | 39075 134394 | 23074 14968 452677 30.2 | 26.924 % | c | 714951 | 39075 134394 | 25382 16107 489959 30.4 | 26.924 % | c | 716660 | 39075 134394 | 27920 17816 549637 30.9 | 26.924 % | c | 719222 | 39075 134394 | 30712 20378 646133 31.7 | 26.924 % | c | 723066 | 39075 134394 | 33783 24222 779906 32.2 | 26.924 % | c | 728834 | 39075 134394 | 37161 29990 1037115 34.6 | 26.924 % | c ============================================================================== c [1mFound solution: 87528[0m c ---[ 0]---> BDD-cost: 10 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 732754 | 39088 134426 | 13029 33910 1167611 34.4 | 26.924 % | c | 732854 | 39088 134426 | 14331 13646 458372 33.6 | 26.910 % | c | 733007 | 39088 134426 | 15765 13799 463197 33.6 | 26.910 % | c | 733234 | 39088 134426 | 17341 14026 465900 33.2 | 26.910 % | c | 733571 | 39088 134426 | 19075 14363 469698 32.7 | 26.910 % | c | 734078 | 39088 134426 | 20983 14870 479722 32.3 | 26.910 % | c | 734837 | 39088 134426 | 23081 15629 504126 32.3 | 26.910 % | c | 735976 | 39088 134426 | 25389 16768 541375 32.3 | 26.910 % | c | 737684 | 39088 134426 | 27928 18476 592886 32.1 | 26.910 % | c | 740246 | 39088 134426 | 30721 21038 681674 32.4 | 26.910 % | c | 744091 | 39088 134426 | 33793 24883 821493 33.0 | 26.910 % | c | 749859 | 39088 134426 | 37173 30651 1069853 34.9 | 26.910 % | c ============================================================================== c [1mFound solution: 85408[0m c ---[ 0]---> BDD-cost: 10 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 752381 | 39101 134458 | 13033 33173 1156953 34.9 | 26.910 % | c | 752482 | 39101 134458 | 14336 13729 454552 33.1 | 26.900 % | c | 752633 | 39101 134458 | 15769 13880 458204 33.0 | 26.900 % | c | 752858 | 39101 134458 | 17346 14105 459709 32.6 | 26.900 % | c | 753196 | 39101 134458 | 19081 14443 464968 32.2 | 26.900 % | c | 753703 | 39101 134458 | 20989 14950 477833 32.0 | 26.900 % | c | 754464 | 39101 134458 | 23088 15711 501517 31.9 | 26.900 % | c | 755603 | 39101 134458 | 25397 16850 541911 32.2 | 26.900 % | c | 757311 | 39101 134458 | 27937 18558 588805 31.7 | 26.900 % | c | 759875 | 39101 134458 | 30731 21122 690605 32.7 | 26.900 % | c | 763719 | 39101 134458 | 33804 24966 829981 33.2 | 26.900 % | c | 769487 | 39101 134458 | 37184 30734 1114803 36.3 | 26.900 % | c | 778136 | 39101 134458 | 40903 39383 1508729 38.3 | 26.900 % | c | 791111 | 39101 134458 | 44993 21690 844837 39.0 | 26.900 % | c | 810572 | 39101 134458 | 49492 41151 1626364 39.5 | 26.900 % | c | 839764 | 39101 134458 | 54442 31155 1379928 44.3 | 26.900 % | c ============================================================================== c [1mFound solution: 84848[0m c ---[ 0]---> BDD-cost: 8 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 857408 | 39112 134484 | 13037 48799 2033293 41.7 | 26.900 % | c | 857508 | 39112 134484 | 14340 14817 483145 32.6 | 26.891 % | c | 857658 | 39112 134484 | 15774 14967 484114 32.3 | 26.891 % | c | 857883 | 39112 134484 | 17352 15192 487336 32.1 | 26.891 % | c | 858221 | 39112 134484 | 19087 15530 495363 31.9 | 26.891 % | c | 858727 | 39112 134484 | 20996 16036 505249 31.5 | 26.891 % | c | 859488 | 39112 134484 | 23095 16797 521087 31.0 | 26.891 % | c | 860627 | 39112 134484 | 25405 17936 547850 30.5 | 26.891 % | c | 862335 | 39112 134484 | 27945 19644 612236 31.2 | 26.891 % | c c *** TERMINATED *** s SATISFIABLE v -x1_bit_10 -x1_bit_9 -x1_bit_8 -x1_bit_7 x1_bit_6 x1_bit_5 x1_bit_4 -x1_bit_3 x1_bit_2 x1_bit_1 -x1_bit0 x1_bit1 -x1_bit2 -x1_bit3 x1_bit4 -x1_bit5 x1_bit6 -x1_bit7 -x1_bit8 -x1_bit9 -x1_bit10 -x1_bit11 -x1_bit12 -x1_bit13 -x1_bit14 -x1_bit15 -x1_bit16 -x1_bit17 -x1_bit18 -x1_bit19 -x2_bit0 -x3_bit0 -x4_bit0 -x5_bit0 -x6_bit0 x7_bit0 -x8_bit0 -x9_bit0 x10_bit0 -x11_bit0 x12_bit0 x13_bit0 x14_bit0 x15_bit0 -x16_bit0 x17_bit0 x18_bit0 x19_bit0 -x20_bit0 x21_bit0 -x22_bit0 x23_bit0 x24_bit0 x25_bit0 -x26_bit0 x27_bit0 -x28_bit0 x29_bit0 -x30_bit0 x31_bit0 -x32_bit0 x33_bit0 -x34_bit0 -x35_bit0 x36_bit0 -x37_bit0 -x38_bit0 x39_bit0 -x40_bit0 -x41_bit0 -x42_bit0 -x43_bit0 x44_bit0 -x45_bit0 x46_bit0 -x47_bit0 x48_bit0 -x49_bit0 -x50_bit0 -x51_bit0 x52_bit0 x53_bit0 -x54_bit0 -x55_bit0 -x56_bit0 -x57_bit_10 -x57_bit_9 -x57_bit_8 -x57_bit_7 -x57_bit_6 -x57_bit_5 -x57_bit_4 -x57_bit_3 -x57_bit_2 -x57_bit_1 -x57_bit0 -x57_bit1 -x57_bit2 -x57_bit3 -x57_bit4 -x57_bit5 x57_bit6 -x57_bit7 -x57_bit8 -x57_bit9 -x57_bit10 -x57_bit11 -x57_bit12 -x57_bit13 -x57_bit14 -x57_bit15 -x57_bit16 -x57_bit17 -x57_bit18 -x57_bit19 -x58_bit_10 -x58_bit_9 -x58_bit_8 -x58_bit_7 -x58_bit_6 -x58_bit_5 -x58_bit_4 -x58_bit_3 -x58_bit_2 -x58_bit_1 x58_bit0 x58_bit1 x58_bit2 -x58_bit3 x58_bit4 -x58_bit5 -x58_bit6 -x58_bit7 -x58_bit8 -x58_bit9 -x58_bit10 -x58_bit11 -x58_bit12 -x58_bit13 -x58_bit14 -x58_bit15 -x58_bit16 -x58_bit17 -x58_bit18 -x58_bit19 -x75_bit_10 -x75_bit_9 -x75_bit_8 -x75_bit_7 -x75_bit_6 -x75_bit_5 -x75_bit_4 -x75_bit_3 -x75_bit_2 -x75_bit_1 -x75_bit0 -x75_bit1 -x75_bit2 -x75_bit3 -x75_bit4 -x75_bit5 -x75_bit6 -x75_bit7 -x75_bit8 -x75_bit9 -x75_bit10 -x75_bit11 -x75_bit12 -x75_bit13 -x75_bit14 -x75_bit15 -x75_bit16 -x75_bit17 -x75_bit18 -x75_bit19 -x76_bit_10 -x76_bit_9 -x76_bit_8 -x76_bit_7 -x76_bit_6 -x76_bit_5 -x76_bit_4 -x76_bit_3 -x76_bit_2 -x76_bit_1 x76_bit0 x76_bit1 x76_bit2 -x76_bit3 -x76_bit4 x76_bit5 -x76_bit6 -x76_bit7 -x76_bit8 -x76_bit9 -x76_bit10 -x76_bit11 -x76_bit12 -x76_bit13 -x76_bit14 -x76_bit15 -x76_bit16 -x76_bit17 -x76_bit18 -x76_bit19 -x77_bit_10 -x77_bit_9 -x77_bit_8 -x77_bit_7 -x77_bit_6 -x77_bit_5 -x77_bit_4 -x77_bit_3 -x77_bit_2 -x77_bit_1 -x77_bit0 -x77_bit1 -x77_bit2 -x77_bit3 x77_bit4 -x77_bit5 x77_bit6 -x77_bit7 -x77_bit8 -x77_bit9 -x77_bit10 -x77_bit11 -x77_bit12 -x77_bit13 -x77_bit14 -x77_bit15 -x77_bit16 -x77_bit17 -x77_bit18 -x77_bit19 -x78_bit_10 -x78_bit_9 -x78_bit_8 -x78_bit_7 -x78_bit_6 -x78_bit_5 -x78_bit_4 -x78_bit_3 -x78_bit_2 -x78_bit_1 x78_bit0 -x78_bit1 x78_bit2 -x78_bit3 -x78_bit4 -x78_bit5 -x78_bit6 -x78_bit7 -x78_bit8 -x78_bit9 -x78_bit10 -x78_bit11 -x78_bit12 -x78_bit13 -x78_bit14 -x78_bit15 -x78_bit16 -x78_bit17 -x78_bit18 -x78_bit19 -x79_bit_10 -x79_bit_9 -x79_bit_8 -x79_bit_7 -x79_bit_6 -x79_bit_5 -x79_bit_4 -x79_bit_3 -x79_bit_2 -x79_bit_1 -x79_bit0 x79_bit1 -x79_bit2 -x79_bit3 -x79_bit4 -x79_bit5 -x79_bit6 -x79_bit7 -x79_bit8 -x79_bit9 -x79_bit10 -x79_bit11 -x79_bit12 -x79_bit13 -x79_bit14 -x79_bit15 -x79_bit16 -x79_bit17 -x79_bit18 -x79_bit19 -x80_bit_10 -x80_bit_9 -x80_bit_8 -x80_bit_7 -x80_bit_6 -x80_bit_5 -x80_bit_4 -x80_bit_3 -x80_bit_2 -x80_bit_1 -x80_bit0 -x80_bit1 -x80_bit2 x80_bit3 -x80_bit4 -x80_bit5 x80_bit6 -x80_bit7 -x80_bit8 -x80_bit9 -x80_bit10 -x80_bit11 -x80_bit12 -x80_bit13 -x80_bit14 -x80_bit15 -x80_bit16 -x80_bit17 -x80_bit18 -x80_bit19 -x81_bit_10 -x81_bit_9 -x81_bit_8 -x81_bit_7 -x81_bit_6 -x81_bit_5 -x81_bit_4 -x81_bit_3 -x81_bit_2 -x81_bit_1 x81_bit0 -x81_bit1 x81_bit2 -x81_bit3 -x81_bit4 -x81_bit5 -x81_bit6 -x81_bit7 -x81_bit8 -x81_bit9 -x81_bit10 -x81_bit11 -x81_bit12 -x81_bit13 -x81_bit14 -x81_bit15 -x81_bit16 -x81_bit17 -x81_bit18 -x81_bit19 -x82_bit_10 -x82_bit_9 -x82_bit_8 -x82_bit_7 -x82_bit_6 -x82_bit_5 -x82_bit_4 -x82_bit_3 -x82_bit_2 -x82_bit_1 -x82_bit0 -x82_bit1 -x82_bit2 -x82_bit3 -x82_bit4 x82_bit5 -x82_bit6 -x82_bit7 -x82_bit8 -x82_bit9 -x82_bit10 -x82_bit11 -x82_bit12 -x82_bit13 -x82_bit14 -x82_bit15 -x82_bit16 -x82_bit17 -x82_bit18 -x82_bit19 -x83_bit_10 -x83_bit_9 -x83_bit_8 -x83_bit_7 -x83_bit_6 -x83_bit_5 -x83_bit_4 -x83_bit_3 -x83_bit_2 -x83_bit_1 -x83_bit0 -x83_bit1 -x83_bit2 -x83_bit3 -x83_bit4 x83_bit5 -x83_bit6 -x83_bit7 -x83_bit8 -x83_bit9 -x83_bit10 -x83_bit11 -x83_bit12 -x83_bit13 -x83_bit14 -x83_bit15 -x83_bit16 -x83_bit17 -x83_bit18 -x83_bit19 -x84_bit_10 -x84_bit_9 -x84_bit_8 -x84_bit_7 -x84_bit_6 -x84_bit_5 -x84_bit_4 -x84_bit_3 -x84_bit_2 -x84_bit_1 -x84_bit0 -x84_bit1 x84_bit2 x84_bit3 -x84_bit4 -x84_bit5 x84_bit6 -x84_bit7 -x84_bit8 -x84_bit9 -x84_bit10 -x84_bit11 -x84_bit12 -x84_bit13 -x84_bit14 -x84_bit15 -x84_bit16 -x84_bit17 -x84_bit18 -x84_bit19 -x85_bit_10 -x85_bit_9 -x85_bit_8 -x85_bit_7 -x85_bit_6 -x85_bit_5 -x85_bit_4 -x85_bit_3 -x85_bit_2 -x85_bit_1 -x85_bit0 -x85_bit1 -x85_bit2 x85_bit3 x85_bit4 -x85_bit5 -x85_bit6 -x85_bit7 -x85_bit8 -x85_bit9 -x85_bit10 -x85_bit11 -x85_bit12 -x85_bit13 -x85_bit14 -x85_bit15 -x85_bit16 -x85_bit17 -x85_bit18 -x85_bit19 -x86_bit_10 -x86_bit_9 -x86_bit_8 -x86_bit_7 -x86_bit_6 -x86_bit_5 -x86_bit_4 -x86_bit_3 -x86_bit_2 -x86_bit_1 -x86_bit0 -x86_bit1 -x86_bit2 x86_bit3 x86_bit4 -x86_bit5 -x86_bit6 -x86_bit7 -x86_bit8 -x86_bit9 -x86_bit10 -x86_bit11 -x86_bit12 -x86_bit13 -x86_bit14 -x86_bit15 -x86_bit16 -x86_bit17 -x86_bit18 -x86_bit19 -x59_bit_10 -x59_bit_9 -x59_bit_8 -x59_bit_7 -x59_bit_6 -x59_bit_5 -x59_bit_4 -x59_bit_3 -x59_bit_2 -x59_bit_1 -x59_bit0 x59_bit1 -x59_bit2 x59_bit3 x59_bit4 -x59_bit5 -x59_bit6 -x59_bit7 -x59_bit8 -x59_bit9 -x59_bit10 -x59_bit11 -x59_bit12 -x59_bit13 -x59_bit14 -x59_bit15 -x59_bit16 -x59_bit17 -x59_bit18 -x59_bit19 -x60_bit_10 -x60_bit_9 -x60_bit_8 -x60_bit_7 -x60_bit_6 -x60_bit_5 -x60_bit_4 -x60_bit_3 -x60_bit_2 -x60_bit_1 -x60_bit0 -x60_bit1 -x60_bit2 -x60_bit3 -x60_bit4 -x60_bit5 -x60_bit6 -x60_bit7 -x60_bit8 -x60_bit9 -x60_bit10 -x60_bit11 -x60_bit12 -x60_bit13 -x60_bit14 -x60_bit15 -x60_bit16 -x60_bit17 -x60_bit18 -x60_bit19 -x61_bit_10 -x61_bit_9 -x61_bit_8 -x61_bit_7 -x61_bit_6 -x61_bit_5 -x61_bit_4 -x61_bit_3 -x61_bit_2 -x61_bit_1 -x61_bit0 -x61_bit1 -x61_bit2 -x61_bit3 x61_bit4 -x61_bit5 x61_bit6 -x61_bit7 -x61_bit8 -x61_bit9 -x61_bit10 -x61_bit11 -x61_bit12 -x61_bit13 -x61_bit14 -x61_bit15 -x61_bit16 -x61_bit17 -x61_bit18 -x61_bit19 -x62_bit_10 -x62_bit_9 -x62_bit_8 -x62_bit_7 -x62_bit_6 -x62_bit_5 -x62_bit_4 -x62_bit_3 -x62_bit_2 -x62_bit_1 -x62_bit0 -x62_bit1 x62_bit2 -x62_bit3 -x62_bit4 -x62_bit5 -x62_bit6 -x62_bit7 -x62_bit8 -x62_bit9 -x62_bit10 -x62_bit11 -x62_bit12 -x62_bit13 -x62_bit14 -x62_bit15 -x62_bit16 -x62_bit17 -x62_bit18 -x62_bit19 -x63_bit_10 -x63_bit_9 -x63_bit_8 -x63_bit_7 -x63_bit_6 -x63_bit_5 -x63_bit_4 -x63_bit_3 -x63_bit_2 -x63_bit_1 -x63_bit0 x63_bit1 x63_bit2 -x63_bit3 x63_bit4 -x63_bit5 -x63_bit6 -x63_bit7 -x63_bit8 -x63_bit9 -x63_bit10 -x63_bit11 -x63_bit12 -x63_bit13 -x63_bit14 -x63_bit15 -x63_bit16 -x63_bit17 -x63_bit18 -x63_bit19 -x64_bit_10 -x64_bit_9 -x64_bit_8 -x64_bit_7 -x64_bit_6 -x64_bit_5 -x64_bit_4 -x64_bit_3 -x64_bit_2 -x64_bit_1 -x64_bit0 -x64_bit1 -x64_bit2 -x64_bit3 -x64_bit4 -x64_bit5 x64_bit6 -x64_bit7 -x64_bit8 -x64_bit9 -x64_bit10 -x64_bit11 -x64_bit12 -x64_bit13 -x64_bit14 -x64_bit15 -x64_bit16 -x64_bit17 -x64_bit18 -x64_bit19 -x65_bit_10 -x65_bit_9 -x65_bit_8 -x65_bit_7 -x65_bit_6 -x65_bit_5 -x65_bit_4 -x65_bit_3 -x65_bit_2 -x65_bit_1 -x65_bit0 -x65_bit1 x65_bit2 -x65_bit3 -x65_bit4 -x65_bit5 -x65_bit6 -x65_bit7 -x65_bit8 -x65_bit9 -x65_bit10 -x65_bit11 -x65_bit12 -x65_bit13 -x65_bit14 -x65_bit15 -x65_bit16 -x65_bit17 -x65_bit18 -x65_bit19 -x66_bit_10 -x66_bit_9 -x66_bit_8 -x66_bit_7 -x66_bit_6 -x66_bit_5 -x66_bit_4 -x66_bit_3 -x66_bit_2 -x66_bit_1 -x66_bit0 -x66_bit1 -x66_bit2 -x66_bit3 -x66_bit4 -x66_bit5 -x66_bit6 -x66_bit7 -x66_bit8 -x66_bit9 -x66_bit10 -x66_bit11 -x66_bit12 -x66_bit13 -x66_bit14 -x66_bit15 -x66_bit16 -x66_bit17 -x66_bit18 -x66_bit19 -x67_bit_10 -x67_bit_9 -x67_bit_8 -x67_bit_7 -x67_bit_6 -x67_bit_5 -x67_bit_4 -x67_bit_3 -x67_bit_2 -x67_bit_1 x67_bit0 -x67_bit1 -x67_bit2 x67_bit3 -x67_bit4 x67_bit5 -x67_bit6 -x67_bit7 -x67_bit8 -x67_bit9 -x67_bit10 -x67_bit11 -x67_bit12 -x67_bit13 -x67_bit14 -x67_bit15 -x67_bit16 -x67_bit17 -x67_bit18 -x67_bit19 -x68_bit_
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing Stack size limit: 67108864 bytes Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb Enforcing VSIZE limit: 994918400 bytes Current StackSize limit: 67108864 bytes Raw data (/proc/1078/stat): 1078 (minisat+_script) R 1077 1078 15400 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1788580299 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/1078/statm): 174 3 169 147 0 27 0 [pid=1078] vsize: 696 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libtermcap.so.2 open syscall for file tls/i686/libtermcap.so.2 open syscall for file tls/mmx/libtermcap.so.2 open syscall for file tls/libtermcap.so.2 open syscall for file i686/mmx/libtermcap.so.2 open syscall for file i686/libtermcap.so.2 open syscall for file mmx/libtermcap.so.2 open syscall for file libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/libtermcap.so.2 open syscall for file /etc/ld.so.cache open syscall for file /lib/libtermcap.so.2 open syscall for file tls/i686/mmx/libdl.so.2 open syscall for file tls/i686/libdl.so.2 open syscall for file tls/mmx/libdl.so.2 open syscall for file tls/libdl.so.2 open syscall for file i686/mmx/libdl.so.2 open syscall for file i686/libdl.so.2 open syscall for file mmx/libdl.so.2 open syscall for file libdl.so.2 open syscall for file /oldhome/oroussel/lib/libdl.so.2 open syscall for file /lib/libdl.so.2 open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /lib/tls/libc.so.6 open syscall for file /dev/tty open syscall for file /etc/mtab open syscall for file /proc/meminfo open syscall for file /oldhome/oroussel/solvers/minisat+_script New process pid=1079 New process pid=1080 New process pid=1081 execve syscall for /bin/sed executable One traced child (pid=1080) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=1081) exited with status: 0 One traced child (pid=1079) exited with status: 0 New process pid=1082 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-pk1.opb [startup+10.0029 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 1560 0 0 0 979 7 0 0 25 0 1 0 1788580304 6934528 1509 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 1693 1509 145 145 0 1548 0 [pid=1082] vsize: 6772 Current children cumulated CPU time (s) 9.87 Current children cumulated vsize (Kb) 8896 [startup+20.0046 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 1771 0 0 0 1976 9 0 0 25 0 1 0 1788580304 7929856 1720 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1082/statm): 1936 1720 145 145 0 1791 0 [pid=1082] vsize: 7744 Current children cumulated CPU time (s) 19.86 Current children cumulated vsize (Kb) 9868 [startup+30.0062 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 1801 0 0 0 2973 10 0 0 25 0 1 0 1788580304 8040448 1750 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1082/statm): 1963 1750 145 145 0 1818 0 [pid=1082] vsize: 7852 Current children cumulated CPU time (s) 29.84 Current children cumulated vsize (Kb) 9976 [startup+40.0069 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 2143 0 0 0 3967 13 0 0 25 0 1 0 1788580304 9482240 2092 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1082/statm): 2315 2092 145 145 0 2170 0 [pid=1082] vsize: 9260 Current children cumulated CPU time (s) 39.81 Current children cumulated vsize (Kb) 11384 [startup+50.0085 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 2262 0 0 0 4964 14 0 0 25 0 1 0 1788580304 9969664 2211 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1082/statm): 2434 2211 145 145 0 2289 0 [pid=1082] vsize: 9736 Current children cumulated CPU time (s) 49.79 Current children cumulated vsize (Kb) 11860 [startup+60.0091 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 2306 0 0 0 5963 15 0 0 25 0 1 0 1788580304 10149888 2255 4294967295 134512640 135094434 3221224448 3221223104 134558227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1082/statm): 2478 2255 145 145 0 2333 0 [pid=1082] vsize: 9912 Current children cumulated CPU time (s) 59.79 Current children cumulated vsize (Kb) 12036 [startup+70.0108 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 2400 0 0 0 6960 16 0 0 25 0 1 0 1788580304 10526720 2349 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1082/statm): 2570 2349 145 145 0 2425 0 [pid=1082] vsize: 10280 Current children cumulated CPU time (s) 69.77 Current children cumulated vsize (Kb) 12404 [startup+80.0114 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 2401 0 0 0 7959 17 0 0 25 0 1 0 1788580304 10526720 2350 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1082/statm): 2570 2350 145 145 0 2425 0 [pid=1082] vsize: 10280 Current children cumulated CPU time (s) 79.77 Current children cumulated vsize (Kb) 12404 [startup+90.012 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 2401 0 0 0 8959 18 0 0 25 0 1 0 1788580304 10526720 2350 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1082/statm): 2570 2350 145 145 0 2425 0 [pid=1082] vsize: 10280 Current children cumulated CPU time (s) 89.78 Current children cumulated vsize (Kb) 12404 [startup+100.014 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 2670 0 0 0 9954 20 0 0 25 0 1 0 1788580304 11612160 2619 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1082/statm): 2835 2619 145 145 0 2690 0 [pid=1082] vsize: 11340 Current children cumulated CPU time (s) 99.75 Current children cumulated vsize (Kb) 13464 [startup+110.014 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 2977 0 0 0 10950 22 0 0 25 0 1 0 1788580304 12976128 2926 4294967295 134512640 135094434 3221224448 3221223060 134563055 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1082/statm): 3168 2926 145 145 0 3023 0 [pid=1082] vsize: 12672 Current children cumulated CPU time (s) 109.73 Current children cumulated vsize (Kb) 14796 [startup+120.016 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 2980 0 0 0 11949 23 0 0 25 0 1 0 1788580304 12988416 2929 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1082/statm): 3171 2929 145 145 0 3026 0 [pid=1082] vsize: 12684 Current children cumulated CPU time (s) 119.73 Current children cumulated vsize (Kb) 14808 [startup+130.017 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 2980 0 0 0 12949 23 0 0 25 0 1 0 1788580304 12988416 2929 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1082/statm): 3171 2929 145 145 0 3026 0 [pid=1082] vsize: 12684 Current children cumulated CPU time (s) 129.73 Current children cumulated vsize (Kb) 14808 [startup+140.017 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 2980 0 0 0 13948 24 0 0 25 0 1 0 1788580304 12988416 2929 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1082/statm): 3171 2929 145 145 0 3026 0 [pid=1082] vsize: 12684 Current children cumulated CPU time (s) 139.73 Current children cumulated vsize (Kb) 14808 [startup+150.019 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 2980 0 0 0 14947 24 0 0 25 0 1 0 1788580304 12988416 2929 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1082/statm): 3171 2929 145 145 0 3026 0 [pid=1082] vsize: 12684 Current children cumulated CPU time (s) 149.72 Current children cumulated vsize (Kb) 14808 [startup+160.019 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 2980 0 0 0 15947 25 0 0 25 0 1 0 1788580304 12988416 2929 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1082/statm): 3171 2929 145 145 0 3026 0 [pid=1082] vsize: 12684 Current children cumulated CPU time (s) 159.73 Current children cumulated vsize (Kb) 14808 [startup+170.021 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 3279 0 0 0 16941 27 0 0 25 0 1 0 1788580304 14196736 3228 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 3466 3228 145 145 0 3321 0 [pid=1082] vsize: 13864 Current children cumulated CPU time (s) 169.69 Current children cumulated vsize (Kb) 15988 [startup+180.022 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 3484 0 0 0 17937 28 0 0 25 0 1 0 1788580304 15020032 3433 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 3667 3433 145 145 0 3522 0 [pid=1082] vsize: 14668 Current children cumulated CPU time (s) 179.66 Current children cumulated vsize (Kb) 16792 [startup+190.022 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 3563 0 0 0 18935 29 0 0 25 0 1 0 1788580304 15343616 3512 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 3746 3512 145 145 0 3601 0 [pid=1082] vsize: 14984 Current children cumulated CPU time (s) 189.65 Current children cumulated vsize (Kb) 17108 [startup+200.023 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 3574 0 0 0 19935 30 0 0 25 0 1 0 1788580304 15388672 3523 4294967295 134512640 135094434 3221224448 3221223088 134562085 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 3757 3523 145 145 0 3612 0 [pid=1082] vsize: 15028 Current children cumulated CPU time (s) 199.66 Current children cumulated vsize (Kb) 17152 [startup+210.024 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 3574 0 0 0 20935 30 0 0 25 0 1 0 1788580304 15388672 3523 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 3757 3523 145 145 0 3612 0 [pid=1082] vsize: 15028 Current children cumulated CPU time (s) 209.66 Current children cumulated vsize (Kb) 17152 [startup+220.025 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 3582 0 0 0 21935 30 0 0 25 0 1 0 1788580304 15421440 3531 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 3765 3531 145 145 0 3620 0 [pid=1082] vsize: 15060 Current children cumulated CPU time (s) 219.66 Current children cumulated vsize (Kb) 17184 [startup+230.026 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 3597 0 0 0 22935 30 0 0 25 0 1 0 1788580304 15486976 3546 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 3781 3546 145 145 0 3636 0 [pid=1082] vsize: 15124 Current children cumulated CPU time (s) 229.66 Current children cumulated vsize (Kb) 17248 [startup+240.025 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 3699 0 0 0 23934 31 0 0 25 0 1 0 1788580304 15925248 3648 4294967295 134512640 135094434 3221224448 3221223104 134557972 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 3888 3648 145 145 0 3743 0 [pid=1082] vsize: 15552 Current children cumulated CPU time (s) 239.66 Current children cumulated vsize (Kb) 17676 [startup+250.027 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 3699 0 0 0 24934 31 0 0 25 0 1 0 1788580304 15925248 3648 4294967295 134512640 135094434 3221224448 3221223104 134557945 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 3888 3648 145 145 0 3743 0 [pid=1082] vsize: 15552 Current children cumulated CPU time (s) 249.66 Current children cumulated vsize (Kb) 17676 [startup+260.028 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 3699 0 0 0 25934 31 0 0 25 0 1 0 1788580304 15925248 3648 4294967295 134512640 135094434 3221224448 3221223084 134557639 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 3888 3648 145 145 0 3743 0 [pid=1082] vsize: 15552 Current children cumulated CPU time (s) 259.66 Current children cumulated vsize (Kb) 17676 [startup+270.028 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 3699 0 0 0 26934 31 0 0 25 0 1 0 1788580304 15925248 3648 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 3888 3648 145 145 0 3743 0 [pid=1082] vsize: 15552 Current children cumulated CPU time (s) 269.66 Current children cumulated vsize (Kb) 17676 [startup+280.029 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 3699 0 0 0 27934 31 0 0 25 0 1 0 1788580304 15925248 3648 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 3888 3648 145 145 0 3743 0 [pid=1082] vsize: 15552 Current children cumulated CPU time (s) 279.66 Current children cumulated vsize (Kb) 17676 [startup+290.03 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 3699 0 0 0 28934 31 0 0 25 0 1 0 1788580304 15925248 3648 4294967295 134512640 135094434 3221224448 3221223104 134558162 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 3888 3648 145 145 0 3743 0 [pid=1082] vsize: 15552 Current children cumulated CPU time (s) 289.66 Current children cumulated vsize (Kb) 17676 [startup+300.03 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 3699 0 0 0 29935 31 0 0 25 0 1 0 1788580304 15925248 3648 4294967295 134512640 135094434 3221224448 3221223104 134558162 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 3888 3648 145 145 0 3743 0 [pid=1082] vsize: 15552 Current children cumulated CPU time (s) 299.67 Current children cumulated vsize (Kb) 17676 [startup+310.031 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 3699 0 0 0 30935 31 0 0 25 0 1 0 1788580304 15925248 3648 4294967295 134512640 135094434 3221224448 3221223104 134557896 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 3888 3648 145 145 0 3743 0 [pid=1082] vsize: 15552 Current children cumulated CPU time (s) 309.67 Current children cumulated vsize (Kb) 17676 [startup+320.033 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 3699 0 0 0 31935 31 0 0 25 0 1 0 1788580304 15925248 3648 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 3888 3648 145 145 0 3743 0 [pid=1082] vsize: 15552 Current children cumulated CPU time (s) 319.67 Current children cumulated vsize (Kb) 17676 [startup+330.033 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 3699 0 0 0 32935 32 0 0 25 0 1 0 1788580304 15925248 3648 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 3888 3648 145 145 0 3743 0 [pid=1082] vsize: 15552 Current children cumulated CPU time (s) 329.68 Current children cumulated vsize (Kb) 17676 [startup+340.034 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 3699 0 0 0 33935 32 0 0 25 0 1 0 1788580304 15925248 3648 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 3888 3648 145 145 0 3743 0 [pid=1082] vsize: 15552 Current children cumulated CPU time (s) 339.68 Current children cumulated vsize (Kb) 17676 [startup+350.035 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 3699 0 0 0 34935 32 0 0 25 0 1 0 1788580304 15925248 3648 4294967295 134512640 135094434 3221224448 3221223104 134558227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 3888 3648 145 145 0 3743 0 [pid=1082] vsize: 15552 Current children cumulated CPU time (s) 349.68 Current children cumulated vsize (Kb) 17676 [startup+360.036 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 3699 0 0 0 35935 32 0 0 25 0 1 0 1788580304 15925248 3648 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 3888 3648 145 145 0 3743 0 [pid=1082] vsize: 15552 Current children cumulated CPU time (s) 359.68 Current children cumulated vsize (Kb) 17676 [startup+370.038 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 3699 0 0 0 36935 32 0 0 25 0 1 0 1788580304 15925248 3648 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 3888 3648 145 145 0 3743 0 [pid=1082] vsize: 15552 Current children cumulated CPU time (s) 369.68 Current children cumulated vsize (Kb) 17676 [startup+380.039 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 3699 0 0 0 37935 32 0 0 25 0 1 0 1788580304 15925248 3648 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 3888 3648 145 145 0 3743 0 [pid=1082] vsize: 15552 Current children cumulated CPU time (s) 379.68 Current children cumulated vsize (Kb) 17676 [startup+390.039 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 3699 0 0 0 38935 32 0 0 25 0 1 0 1788580304 15925248 3648 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 3888 3648 145 145 0 3743 0 [pid=1082] vsize: 15552 Current children cumulated CPU time (s) 389.68 Current children cumulated vsize (Kb) 17676 [startup+400.04 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 3699 0 0 0 39936 32 0 0 25 0 1 0 1788580304 15925248 3648 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 3888 3648 145 145 0 3743 0 [pid=1082] vsize: 15552 Current children cumulated CPU time (s) 399.69 Current children cumulated vsize (Kb) 17676 [startup+410.04 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 3699 0 0 0 40936 32 0 0 25 0 1 0 1788580304 15925248 3648 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 3888 3648 145 145 0 3743 0 [pid=1082] vsize: 15552 Current children cumulated CPU time (s) 409.69 Current children cumulated vsize (Kb) 17676 [startup+420.042 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 3699 0 0 0 41936 32 0 0 25 0 1 0 1788580304 15925248 3648 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 3888 3648 145 145 0 3743 0 [pid=1082] vsize: 15552 Current children cumulated CPU time (s) 419.69 Current children cumulated vsize (Kb) 17676 [startup+430.043 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 3944 0 0 0 42932 34 0 0 25 0 1 0 1788580304 16928768 3893 4294967295 134512640 135094434 3221224448 3221223072 134557648 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 4133 3893 145 145 0 3988 0 [pid=1082] vsize: 16532 Current children cumulated CPU time (s) 429.67 Current children cumulated vsize (Kb) 18656 [startup+440.043 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4046 0 0 0 43931 34 0 0 25 0 1 0 1788580304 17342464 3995 4294967295 134512640 135094434 3221224448 3221223072 134557655 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 4234 3995 145 145 0 4089 0 [pid=1082] vsize: 16936 Current children cumulated CPU time (s) 439.66 Current children cumulated vsize (Kb) 19060 [startup+450.044 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4046 0 0 0 44931 34 0 0 25 0 1 0 1788580304 17342464 3995 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 4234 3995 145 145 0 4089 0 [pid=1082] vsize: 16936 Current children cumulated CPU time (s) 449.66 Current children cumulated vsize (Kb) 19060 [startup+460.044 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4046 0 0 0 45931 35 0 0 25 0 1 0 1788580304 17342464 3995 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 4234 3995 145 145 0 4089 0 [pid=1082] vsize: 16936 Current children cumulated CPU time (s) 459.67 Current children cumulated vsize (Kb) 19060 [startup+470.046 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4046 0 0 0 46931 35 0 0 25 0 1 0 1788580304 17342464 3995 4294967295 134512640 135094434 3221224448 3221223180 134670016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 4234 3995 145 145 0 4089 0 [pid=1082] vsize: 16936 Current children cumulated CPU time (s) 469.67 Current children cumulated vsize (Kb) 19060 [startup+480.047 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4046 0 0 0 47931 35 0 0 25 0 1 0 1788580304 17342464 3995 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 4234 3995 145 145 0 4089 0 [pid=1082] vsize: 16936 Current children cumulated CPU time (s) 479.67 Current children cumulated vsize (Kb) 19060 [startup+490.047 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4046 0 0 0 48931 35 0 0 25 0 1 0 1788580304 17342464 3995 4294967295 134512640 135094434 3221224448 3221223152 134554526 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 4234 3995 145 145 0 4089 0 [pid=1082] vsize: 16936 Current children cumulated CPU time (s) 489.67 Current children cumulated vsize (Kb) 19060 [startup+500.048 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4046 0 0 0 49932 35 0 0 25 0 1 0 1788580304 17342464 3995 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 4234 3995 145 145 0 4089 0 [pid=1082] vsize: 16936 Current children cumulated CPU time (s) 499.68 Current children cumulated vsize (Kb) 19060 [startup+510.049 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4046 0 0 0 50932 35 0 0 25 0 1 0 1788580304 17342464 3995 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 4234 3995 145 145 0 4089 0 [pid=1082] vsize: 16936 Current children cumulated CPU time (s) 509.68 Current children cumulated vsize (Kb) 19060 [startup+520.049 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4046 0 0 0 51932 35 0 0 25 0 1 0 1788580304 17342464 3995 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 4234 3995 145 145 0 4089 0 [pid=1082] vsize: 16936 Current children cumulated CPU time (s) 519.68 Current children cumulated vsize (Kb) 19060 [startup+530.05 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4046 0 0 0 52932 35 0 0 25 0 1 0 1788580304 17342464 3995 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 4234 3995 145 145 0 4089 0 [pid=1082] vsize: 16936 Current children cumulated CPU time (s) 529.68 Current children cumulated vsize (Kb) 19060 [startup+540.051 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4046 0 0 0 53932 35 0 0 25 0 1 0 1788580304 17342464 3995 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 4234 3995 145 145 0 4089 0 [pid=1082] vsize: 16936 Current children cumulated CPU time (s) 539.68 Current children cumulated vsize (Kb) 19060 [startup+550.051 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4046 0 0 0 54932 35 0 0 25 0 1 0 1788580304 17342464 3995 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 4234 3995 145 145 0 4089 0 [pid=1082] vsize: 16936 Current children cumulated CPU time (s) 549.68 Current children cumulated vsize (Kb) 19060 [startup+560.052 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4098 0 0 0 55932 36 0 0 25 0 1 0 1788580304 17555456 4047 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 4286 4047 145 145 0 4141 0 [pid=1082] vsize: 17144 Current children cumulated CPU time (s) 559.69 Current children cumulated vsize (Kb) 19268 [startup+570.052 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4208 0 0 0 56930 36 0 0 25 0 1 0 1788580304 18006016 4157 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 4396 4157 145 145 0 4251 0 [pid=1082] vsize: 17584 Current children cumulated CPU time (s) 569.67 Current children cumulated vsize (Kb) 19708 [startup+580.053 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4208 0 0 0 57930 36 0 0 25 0 1 0 1788580304 18006016 4157 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 4396 4157 145 145 0 4251 0 [pid=1082] vsize: 17584 Current children cumulated CPU time (s) 579.67 Current children cumulated vsize (Kb) 19708 [startup+590.054 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4212 0 0 0 58930 36 0 0 25 0 1 0 1788580304 18022400 4161 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 4400 4161 145 145 0 4255 0 [pid=1082] vsize: 17600 Current children cumulated CPU time (s) 589.67 Current children cumulated vsize (Kb) 19724 [startup+600.054 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4214 0 0 0 59930 37 0 0 25 0 1 0 1788580304 18030592 4163 4294967295 134512640 135094434 3221224448 3221223104 134557852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 4402 4163 145 145 0 4257 0 [pid=1082] vsize: 17608 Current children cumulated CPU time (s) 599.68 Current children cumulated vsize (Kb) 19732 [startup+610.055 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4474 0 0 0 60925 39 0 0 25 0 1 0 1788580304 19095552 4423 4294967295 134512640 135094434 3221224448 3221223104 134555975 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 4662 4423 145 145 0 4517 0 [pid=1082] vsize: 18648 Current children cumulated CPU time (s) 609.65 Current children cumulated vsize (Kb) 20772 [startup+620.057 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4707 0 0 0 61922 41 0 0 25 0 1 0 1788580304 20029440 4656 4294967295 134512640 135094434 3221224448 3221223104 134558218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 4890 4656 145 145 0 4745 0 [pid=1082] vsize: 19560 Current children cumulated CPU time (s) 619.64 Current children cumulated vsize (Kb) 21684 [startup+630.057 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4707 0 0 0 62922 41 0 0 25 0 1 0 1788580304 20029440 4656 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 4890 4656 145 145 0 4745 0 [pid=1082] vsize: 19560 Current children cumulated CPU time (s) 629.64 Current children cumulated vsize (Kb) 21684 [startup+640.058 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4708 0 0 0 63922 41 0 0 25 0 1 0 1788580304 20029440 4657 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 4890 4657 145 145 0 4745 0 [pid=1082] vsize: 19560 Current children cumulated CPU time (s) 639.64 Current children cumulated vsize (Kb) 21684 [startup+650.059 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4708 0 0 0 64922 41 0 0 25 0 1 0 1788580304 20029440 4657 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 4890 4657 145 145 0 4745 0 [pid=1082] vsize: 19560 Current children cumulated CPU time (s) 649.64 Current children cumulated vsize (Kb) 21684 [startup+660.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4708 0 0 0 65923 41 0 0 25 0 1 0 1788580304 20029440 4657 4294967295 134512640 135094434 3221224448 3221223104 134558162 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 4890 4657 145 145 0 4745 0 [pid=1082] vsize: 19560 Current children cumulated CPU time (s) 659.65 Current children cumulated vsize (Kb) 21684 [startup+670.061 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4708 0 0 0 66923 41 0 0 25 0 1 0 1788580304 20029440 4657 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 4890 4657 145 145 0 4745 0 [pid=1082] vsize: 19560 Current children cumulated CPU time (s) 669.65 Current children cumulated vsize (Kb) 21684 [startup+680.061 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4708 0 0 0 67923 41 0 0 25 0 1 0 1788580304 20029440 4657 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 4890 4657 145 145 0 4745 0 [pid=1082] vsize: 19560 Current children cumulated CPU time (s) 679.65 Current children cumulated vsize (Kb) 21684 [startup+690.062 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4708 0 0 0 68923 41 0 0 25 0 1 0 1788580304 20029440 4657 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 4890 4657 145 145 0 4745 0 [pid=1082] vsize: 19560 Current children cumulated CPU time (s) 689.65 Current children cumulated vsize (Kb) 21684 [startup+700.063 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4708 0 0 0 69923 41 0 0 25 0 1 0 1788580304 20029440 4657 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 4890 4657 145 145 0 4745 0 [pid=1082] vsize: 19560 Current children cumulated CPU time (s) 699.65 Current children cumulated vsize (Kb) 21684 [startup+710.063 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4708 0 0 0 70924 41 0 0 25 0 1 0 1788580304 20029440 4657 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 4890 4657 145 145 0 4745 0 [pid=1082] vsize: 19560 Current children cumulated CPU time (s) 709.66 Current children cumulated vsize (Kb) 21684 [startup+720.065 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4708 0 0 0 71924 41 0 0 25 0 1 0 1788580304 20029440 4657 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 4890 4657 145 145 0 4745 0 [pid=1082] vsize: 19560 Current children cumulated CPU time (s) 719.66 Current children cumulated vsize (Kb) 21684 [startup+730.066 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4708 0 0 0 72924 41 0 0 25 0 1 0 1788580304 20029440 4657 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 4890 4657 145 145 0 4745 0 [pid=1082] vsize: 19560 Current children cumulated CPU time (s) 729.66 Current children cumulated vsize (Kb) 21684 [startup+740.065 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4708 0 0 0 73924 41 0 0 25 0 1 0 1788580304 20029440 4657 4294967295 134512640 135094434 3221224448 3221223136 134554667 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 4890 4657 145 145 0 4745 0 [pid=1082] vsize: 19560 Current children cumulated CPU time (s) 739.66 Current children cumulated vsize (Kb) 21684 [startup+750.066 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4708 0 0 0 74924 41 0 0 25 0 1 0 1788580304 20029440 4657 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 4890 4657 145 145 0 4745 0 [pid=1082] vsize: 19560 Current children cumulated CPU time (s) 749.66 Current children cumulated vsize (Kb) 21684 [startup+760.066 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4708 0 0 0 75924 41 0 0 25 0 1 0 1788580304 20029440 4657 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 4890 4657 145 145 0 4745 0 [pid=1082] vsize: 19560 Current children cumulated CPU time (s) 759.66 Current children cumulated vsize (Kb) 21684 [startup+770.068 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4708 0 0 0 76925 41 0 0 25 0 1 0 1788580304 20029440 4657 4294967295 134512640 135094434 3221224448 3221223136 134554739 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 4890 4657 145 145 0 4745 0 [pid=1082] vsize: 19560 Current children cumulated CPU time (s) 769.67 Current children cumulated vsize (Kb) 21684 [startup+780.069 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4709 0 0 0 77925 41 0 0 25 0 1 0 1788580304 20029440 4658 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 4890 4658 145 145 0 4745 0 [pid=1082] vsize: 19560 Current children cumulated CPU time (s) 779.67 Current children cumulated vsize (Kb) 21684 [startup+790.069 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4709 0 0 0 78924 42 0 0 25 0 1 0 1788580304 20029440 4658 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 4890 4658 145 145 0 4745 0 [pid=1082] vsize: 19560 Current children cumulated CPU time (s) 789.67 Current children cumulated vsize (Kb) 21684 [startup+800.07 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4843 0 0 0 79922 43 0 0 25 0 1 0 1788580304 20590592 4792 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5027 4792 145 145 0 4882 0 [pid=1082] vsize: 20108 Current children cumulated CPU time (s) 799.66 Current children cumulated vsize (Kb) 22232 [startup+810.071 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4994 0 0 0 80919 45 0 0 25 0 1 0 1788580304 21192704 4943 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5174 4943 145 145 0 5029 0 [pid=1082] vsize: 20696 Current children cumulated CPU time (s) 809.65 Current children cumulated vsize (Kb) 22820 [startup+820.072 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4994 0 0 0 81919 45 0 0 25 0 1 0 1788580304 21192704 4943 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5174 4943 145 145 0 5029 0 [pid=1082] vsize: 20696 Current children cumulated CPU time (s) 819.65 Current children cumulated vsize (Kb) 22820 [startup+830.075 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4994 0 0 0 82919 45 0 0 25 0 1 0 1788580304 21192704 4943 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5174 4943 145 145 0 5029 0 [pid=1082] vsize: 20696 Current children cumulated CPU time (s) 829.65 Current children cumulated vsize (Kb) 22820 [startup+840.075 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4994 0 0 0 83919 45 0 0 25 0 1 0 1788580304 21192704 4943 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5174 4943 145 145 0 5029 0 [pid=1082] vsize: 20696 Current children cumulated CPU time (s) 839.65 Current children cumulated vsize (Kb) 22820 [startup+850.075 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4994 0 0 0 84919 46 0 0 25 0 1 0 1788580304 21192704 4943 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5174 4943 145 145 0 5029 0 [pid=1082] vsize: 20696 Current children cumulated CPU time (s) 849.66 Current children cumulated vsize (Kb) 22820 [startup+860.076 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4994 0 0 0 85920 46 0 0 25 0 1 0 1788580304 21192704 4943 4294967295 134512640 135094434 3221224448 3221223104 134557882 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5174 4943 145 145 0 5029 0 [pid=1082] vsize: 20696 Current children cumulated CPU time (s) 859.67 Current children cumulated vsize (Kb) 22820 [startup+870.076 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 4997 0 0 0 86920 46 0 0 25 0 1 0 1788580304 21209088 4946 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5178 4946 145 145 0 5033 0 [pid=1082] vsize: 20712 Current children cumulated CPU time (s) 869.67 Current children cumulated vsize (Kb) 22836 [startup+880.077 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 5119 0 0 0 87918 47 0 0 25 0 1 0 1788580304 21716992 5068 4294967295 134512640 135094434 3221224448 3221223040 134556815 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5302 5068 145 145 0 5157 0 [pid=1082] vsize: 21208 Current children cumulated CPU time (s) 879.66 Current children cumulated vsize (Kb) 23332 [startup+890.078 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 5359 0 0 0 88913 49 0 0 25 0 1 0 1788580304 22700032 5308 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5542 5308 145 145 0 5397 0 [pid=1082] vsize: 22168 Current children cumulated CPU time (s) 889.63 Current children cumulated vsize (Kb) 24292 [startup+900.079 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 5591 0 0 0 89909 51 0 0 25 0 1 0 1788580304 23650304 5540 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5774 5540 145 145 0 5629 0 [pid=1082] vsize: 23096 Current children cumulated CPU time (s) 899.61 Current children cumulated vsize (Kb) 25220 [startup+910.08 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 5608 0 0 0 90909 51 0 0 25 0 1 0 1788580304 23719936 5557 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5791 5557 145 145 0 5646 0 [pid=1082] vsize: 23164 Current children cumulated CPU time (s) 909.61 Current children cumulated vsize (Kb) 25288 [startup+920.082 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 5608 0 0 0 91909 51 0 0 25 0 1 0 1788580304 23719936 5557 4294967295 134512640 135094434 3221224448 3221223060 134563024 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5791 5557 145 145 0 5646 0 [pid=1082] vsize: 23164 Current children cumulated CPU time (s) 919.61 Current children cumulated vsize (Kb) 25288 [startup+930.082 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 5608 0 0 0 92909 51 0 0 25 0 1 0 1788580304 23719936 5557 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5791 5557 145 145 0 5646 0 [pid=1082] vsize: 23164 Current children cumulated CPU time (s) 929.61 Current children cumulated vsize (Kb) 25288 [startup+940.083 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 5608 0 0 0 93910 51 0 0 25 0 1 0 1788580304 23719936 5557 4294967295 134512640 135094434 3221224448 3221223104 134558420 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5791 5557 145 145 0 5646 0 [pid=1082] vsize: 23164 Current children cumulated CPU time (s) 939.62 Current children cumulated vsize (Kb) 25288 [startup+950.085 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 5608 0 0 0 94908 52 0 0 25 0 1 0 1788580304 23719936 5557 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1082/statm): 5791 5557 145 145 0 5646 0 [pid=1082] vsize: 23164 Current children cumulated CPU time (s) 949.61 Current children cumulated vsize (Kb) 25288 [startup+960.085 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 5608 0 0 0 95908 52 0 0 25 0 1 0 1788580304 23719936 5557 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5791 5557 145 145 0 5646 0 [pid=1082] vsize: 23164 Current children cumulated CPU time (s) 959.61 Current children cumulated vsize (Kb) 25288 [startup+970.087 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 5608 0 0 0 96908 52 0 0 25 0 1 0 1788580304 23719936 5557 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5791 5557 145 145 0 5646 0 [pid=1082] vsize: 23164 Current children cumulated CPU time (s) 969.61 Current children cumulated vsize (Kb) 25288 [startup+980.087 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 5608 0 0 0 97909 52 0 0 25 0 1 0 1788580304 23719936 5557 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5791 5557 145 145 0 5646 0 [pid=1082] vsize: 23164 Current children cumulated CPU time (s) 979.62 Current children cumulated vsize (Kb) 25288 [startup+990.088 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 5608 0 0 0 98908 52 0 0 25 0 1 0 1788580304 23719936 5557 4294967295 134512640 135094434 3221224448 3221223120 134556465 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5791 5557 145 145 0 5646 0 [pid=1082] vsize: 23164 Current children cumulated CPU time (s) 989.61 Current children cumulated vsize (Kb) 25288 [startup+1000.09 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 5608 0 0 0 99909 52 0 0 25 0 1 0 1788580304 23719936 5557 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5791 5557 145 145 0 5646 0 [pid=1082] vsize: 23164 Current children cumulated CPU time (s) 999.62 Current children cumulated vsize (Kb) 25288 [startup+1010.09 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 5608 0 0 0 100909 52 0 0 25 0 1 0 1788580304 23719936 5557 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5791 5557 145 145 0 5646 0 [pid=1082] vsize: 23164 Current children cumulated CPU time (s) 1009.62 Current children cumulated vsize (Kb) 25288 [startup+1020.09 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 5608 0 0 0 101909 53 0 0 25 0 1 0 1788580304 23719936 5557 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5791 5557 145 145 0 5646 0 [pid=1082] vsize: 23164 Current children cumulated CPU time (s) 1019.63 Current children cumulated vsize (Kb) 25288 [startup+1030.09 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 5608 0 0 0 102909 53 0 0 25 0 1 0 1788580304 23719936 5557 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5791 5557 145 145 0 5646 0 [pid=1082] vsize: 23164 Current children cumulated CPU time (s) 1029.63 Current children cumulated vsize (Kb) 25288 [startup+1040.09 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 5608 0 0 0 103909 53 0 0 25 0 1 0 1788580304 23719936 5557 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5791 5557 145 145 0 5646 0 [pid=1082] vsize: 23164 Current children cumulated CPU time (s) 1039.63 Current children cumulated vsize (Kb) 25288 [startup+1050.09 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 5608 0 0 0 104909 53 0 0 25 0 1 0 1788580304 23719936 5557 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5791 5557 145 145 0 5646 0 [pid=1082] vsize: 23164 Current children cumulated CPU time (s) 1049.63 Current children cumulated vsize (Kb) 25288 [startup+1060.09 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 5608 0 0 0 105910 53 0 0 25 0 1 0 1788580304 23719936 5557 4294967295 134512640 135094434 3221224448 3221223040 134557377 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5791 5557 145 145 0 5646 0 [pid=1082] vsize: 23164 Current children cumulated CPU time (s) 1059.64 Current children cumulated vsize (Kb) 25288 [startup+1070.09 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 5608 0 0 0 106910 53 0 0 25 0 1 0 1788580304 23719936 5557 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5791 5557 145 145 0 5646 0 [pid=1082] vsize: 23164 Current children cumulated CPU time (s) 1069.64 Current children cumulated vsize (Kb) 25288 [startup+1080.09 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 5608 0 0 0 107910 53 0 0 25 0 1 0 1788580304 23719936 5557 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5791 5557 145 145 0 5646 0 [pid=1082] vsize: 23164 Current children cumulated CPU time (s) 1079.64 Current children cumulated vsize (Kb) 25288 [startup+1090.1 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 5608 0 0 0 108910 53 0 0 25 0 1 0 1788580304 23719936 5557 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5791 5557 145 145 0 5646 0 [pid=1082] vsize: 23164 Current children cumulated CPU time (s) 1089.64 Current children cumulated vsize (Kb) 25288 [startup+1100.1 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 5608 0 0 0 109910 53 0 0 25 0 1 0 1788580304 23719936 5557 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5791 5557 145 145 0 5646 0 [pid=1082] vsize: 23164 Current children cumulated CPU time (s) 1099.64 Current children cumulated vsize (Kb) 25288 [startup+1110.1 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 5608 0 0 0 110911 53 0 0 25 0 1 0 1788580304 23719936 5557 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5791 5557 145 145 0 5646 0 [pid=1082] vsize: 23164 Current children cumulated CPU time (s) 1109.65 Current children cumulated vsize (Kb) 25288 [startup+1120.1 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 5608 0 0 0 111911 53 0 0 25 0 1 0 1788580304 23719936 5557 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5791 5557 145 145 0 5646 0 [pid=1082] vsize: 23164 Current children cumulated CPU time (s) 1119.65 Current children cumulated vsize (Kb) 25288 [startup+1130.1 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 5608 0 0 0 112911 53 0 0 25 0 1 0 1788580304 23719936 5557 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5791 5557 145 145 0 5646 0 [pid=1082] vsize: 23164 Current children cumulated CPU time (s) 1129.65 Current children cumulated vsize (Kb) 25288 [startup+1140.1 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 5608 0 0 0 113911 53 0 0 25 0 1 0 1788580304 23719936 5557 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5791 5557 145 145 0 5646 0 [pid=1082] vsize: 23164 Current children cumulated CPU time (s) 1139.65 Current children cumulated vsize (Kb) 25288 [startup+1150.1 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 5608 0 0 0 114911 53 0 0 25 0 1 0 1788580304 23719936 5557 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5791 5557 145 145 0 5646 0 [pid=1082] vsize: 23164 Current children cumulated CPU time (s) 1149.65 Current children cumulated vsize (Kb) 25288 [startup+1160.1 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 5608 0 0 0 115912 53 0 0 25 0 1 0 1788580304 23719936 5557 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5791 5557 145 145 0 5646 0 [pid=1082] vsize: 23164 Current children cumulated CPU time (s) 1159.66 Current children cumulated vsize (Kb) 25288 [startup+1170.1 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 5608 0 0 0 116912 53 0 0 25 0 1 0 1788580304 23719936 5557 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5791 5557 145 145 0 5646 0 [pid=1082] vsize: 23164 Current children cumulated CPU time (s) 1169.66 Current children cumulated vsize (Kb) 25288 [startup+1180.1 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 5608 0 0 0 117912 53 0 0 25 0 1 0 1788580304 23719936 5557 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5791 5557 145 145 0 5646 0 [pid=1082] vsize: 23164 Current children cumulated CPU time (s) 1179.66 Current children cumulated vsize (Kb) 25288 [startup+1190.1 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 5608 0 0 0 118912 53 0 0 25 0 1 0 1788580304 23719936 5557 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5791 5557 145 145 0 5646 0 [pid=1082] vsize: 23164 Current children cumulated CPU time (s) 1189.66 Current children cumulated vsize (Kb) 25288 [startup+1200.1 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 5608 0 0 0 119912 53 0 0 25 0 1 0 1788580304 23719936 5557 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5791 5557 145 145 0 5646 0 [pid=1082] vsize: 23164 Current children cumulated CPU time (s) 1199.66 Current children cumulated vsize (Kb) 25288 [startup+1210.1 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 5608 0 0 0 120913 53 0 0 25 0 1 0 1788580304 23719936 5557 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5791 5557 145 145 0 5646 0 [pid=1082] vsize: 23164 Current children cumulated CPU time (s) 1209.67 Current children cumulated vsize (Kb) 25288 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.1 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 1082 Raw data (/proc/1078/stat): 1078 (minisat+_script) S 1077 1078 15400 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788580299 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1078/statm): 531 226 485 147 0 384 0 [pid=1078] vsize: 2124 Raw data (/proc/1082/stat): 1082 (minisat+_64-bit) R 1078 1078 15400 0 -1 0 5608 0 0 0 120913 53 0 0 25 0 1 0 1788580304 23719936 5557 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1082/statm): 5791 5557 145 145 0 5646 0 [pid=1082] vsize: 23164 Current children cumulated CPU time (s) 1209.67 Current children cumulated vsize (Kb) 25288 Sending SIGTERM to -1078 Sleeping 2 seconds One traced child (pid=1078) ended because it received signal 15 (SIGTERM) One traced child (pid=1082) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.12 CPU time (s): 1209.68 CPU user time (s): 1209.13 CPU system time (s): 0.547916 CPU usage (%): 99.9637 Max. virtual memory (cumulated for all children) (Kb): 25288
ERROR: no interpretation found !