Name | mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-pk1.opb |
MD5SUM | ca2f95c2509c09ae8cf1945e12d0eb97 |
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 wulflinc25 THE 2005-09-19 18:06:57 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3000 boxname=wulflinc25 idbench=656 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: ca2f95c2509c09ae8cf1945e12d0eb97 /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-pk1.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-pk1.opb IDLAUNCH: 3000 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.220 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.220 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 946952 kB Buffers: 3420 kB Cached: 57456 kB SwapCached: 868 kB Active: 10992 kB Inactive: 52532 kB HighTotal: 131008 kB HighFree: 69860 kB LowTotal: 903652 kB LowFree: 877092 kB SwapTotal: 2097892 kB SwapFree: 2096524 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5724 kB Slab: 18548 kB Committed_AS: 64132 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-19 18:27:08 (client local time) WITH STATUS 10 IN 1209.71 SECONDS stats: 3000 7 1209.71 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 -d_bit_10 -d_bit_9 -d_bit_8 -d_bit_7 d_bit_6 d_bit_5 d_bit_4 -d_bit_3 d_bit_2 d_bit_1 -d_bit0 d_bit1 -d_bit2 -d_bit3 d_bit4 -d_bit5 d_bit6 -d_bit7 -d_bit8 -d_bit9 -d_bit10 -d_bit11 -d_bit12 -d_bit13 -d_bit14 -d_bit15 -d_bit16 -d_bit17 -d_bit18 -d_bit19 -X1_bit0 -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 -S1_bit_10 -S1_bit_9 -S1_bit_8 -S1_bit_7 -S1_bit_6 -S1_bit_5 -S1_bit_4 -S1_bit_3 -S1_bit_2 -S1_bit_1 -S1_bit0 -S1_bit1 -S1_bit2 -S1_bit3 -S1_bit4 -S1_bit5 S1_bit6 -S1_bit7 -S1_bit8 -S1_bit9 -S1_bit10 -S1_bit11 -S1_bit12 -S1_bit13 -S1_bit14 -S1_bit15 -S1_bit16 -S1_bit17 -S1_bit18 -S1_bit19 -T1_bit_10 -T1_bit_9 -T1_bit_8 -T1_bit_7 -T1_bit_6 -T1_bit_5 -T1_bit_4 -T1_bit_3 -T1_bit_2 -T1_bit_1 T1_bit0 T1_bit1 T1_bit2 -T1_bit3 T1_bit4 -T1_bit5 -T1_bit6 -T1_bit7 -T1_bit8 -T1_bit9 -T1_bit10 -T1_bit11 -T1_bit12 -T1_bit13 -T1_bit14 -T1_bit15 -T1_bit16 -T1_bit17 -T1_bit18 -T1_bit19 -S10_bit_10 -S10_bit_9 -S10_bit_8 -S10_bit_7 -S10_bit_6 -S10_bit_5 -S10_bit_4 -S10_bit_3 -S10_bit_2 -S10_bit_1 -S10_bit0 -S10_bit1 -S10_bit2 -S10_bit3 -S10_bit4 -S10_bit5 -S10_bit6 -S10_bit7 -S10_bit8 -S10_bit9 -S10_bit10 -S10_bit11 -S10_bit12 -S10_bit13 -S10_bit14 -S10_bit15 -S10_bit16 -S10_bit17 -S10_bit18 -S10_bit19 -T10_bit_10 -T10_bit_9 -T10_bit_8 -T10_bit_7 -T10_bit_6 -T10_bit_5 -T10_bit_4 -T10_bit_3 -T10_bit_2 -T10_bit_1 T10_bit0 T10_bit1 T10_bit2 -T10_bit3 -T10_bit4 T10_bit5 -T10_bit6 -T10_bit7 -T10_bit8 -T10_bit9 -T10_bit10 -T10_bit11 -T10_bit12 -T10_bit13 -T10_bit14 -T10_bit15 -T10_bit16 -T10_bit17 -T10_bit18 -T10_bit19 -S11_bit_10 -S11_bit_9 -S11_bit_8 -S11_bit_7 -S11_bit_6 -S11_bit_5 -S11_bit_4 -S11_bit_3 -S11_bit_2 -S11_bit_1 -S11_bit0 -S11_bit1 -S11_bit2 -S11_bit3 S11_bit4 -S11_bit5 S11_bit6 -S11_bit7 -S11_bit8 -S11_bit9 -S11_bit10 -S11_bit11 -S11_bit12 -S11_bit13 -S11_bit14 -S11_bit15 -S11_bit16 -S11_bit17 -S11_bit18 -S11_bit19 -T11_bit_10 -T11_bit_9 -T11_bit_8 -T11_bit_7 -T11_bit_6 -T11_bit_5 -T11_bit_4 -T11_bit_3 -T11_bit_2 -T11_bit_1 T11_bit0 -T11_bit1 T11_bit2 -T11_bit3 -T11_bit4 -T11_bit5 -T11_bit6 -T11_bit7 -T11_bit8 -T11_bit9 -T11_bit10 -T11_bit11 -T11_bit12 -T11_bit13 -T11_bit14 -T11_bit15 -T11_bit16 -T11_bit17 -T11_bit18 -T11_bit19 -S12_bit_10 -S12_bit_9 -S12_bit_8 -S12_bit_7 -S12_bit_6 -S12_bit_5 -S12_bit_4 -S12_bit_3 -S12_bit_2 -S12_bit_1 -S12_bit0 S12_bit1 -S12_bit2 -S12_bit3 -S12_bit4 -S12_bit5 -S12_bit6 -S12_bit7 -S12_bit8 -S12_bit9 -S12_bit10 -S12_bit11 -S12_bit12 -S12_bit13 -S12_bit14 -S12_bit15 -S12_bit16 -S12_bit17 -S12_bit18 -S12_bit19 -T12_bit_10 -T12_bit_9 -T12_bit_8 -T12_bit_7 -T12_bit_6 -T12_bit_5 -T12_bit_4 -T12_bit_3 -T12_bit_2 -T12_bit_1 -T12_bit0 -T12_bit1 -T12_bit2 T12_bit3 -T12_bit4 -T12_bit5 T12_bit6 -T12_bit7 -T12_bit8 -T12_bit9 -T12_bit10 -T12_bit11 -T12_bit12 -T12_bit13 -T12_bit14 -T12_bit15 -T12_bit16 -T12_bit17 -T12_bit18 -T12_bit19 -S13_bit_10 -S13_bit_9 -S13_bit_8 -S13_bit_7 -S13_bit_6 -S13_bit_5 -S13_bit_4 -S13_bit_3 -S13_bit_2 -S13_bit_1 S13_bit0 -S13_bit1 S13_bit2 -S13_bit3 -S13_bit4 -S13_bit5 -S13_bit6 -S13_bit7 -S13_bit8 -S13_bit9 -S13_bit10 -S13_bit11 -S13_bit12 -S13_bit13 -S13_bit14 -S13_bit15 -S13_bit16 -S13_bit17 -S13_bit18 -S13_bit19 -T13_bit_10 -T13_bit_9 -T13_bit_8 -T13_bit_7 -T13_bit_6 -T13_bit_5 -T13_bit_4 -T13_bit_3 -T13_bit_2 -T13_bit_1 -T13_bit0 -T13_bit1 -T13_bit2 -T13_bit3 -T13_bit4 T13_bit5 -T13_bit6 -T13_bit7 -T13_bit8 -T13_bit9 -T13_bit10 -T13_bit11 -T13_bit12 -T13_bit13 -T13_bit14 -T13_bit15 -T13_bit16 -T13_bit17 -T13_bit18 -T13_bit19 -S14_bit_10 -S14_bit_9 -S14_bit_8 -S14_bit_7 -S14_bit_6 -S14_bit_5 -S14_bit_4 -S14_bit_3 -S14_bit_2 -S14_bit_1 -S14_bit0 -S14_bit1 -S14_bit2 -S14_bit3 -S14_bit4 S14_bit5 -S14_bit6 -S14_bit7 -S14_bit8 -S14_bit9 -S14_bit10 -S14_bit11 -S14_bit12 -S14_bit13 -S14_bit14 -S14_bit15 -S14_bit16 -S14_bit17 -S14_bit18 -S14_bit19 -T14_bit_10 -T14_bit_9 -T14_bit_8 -T14_bit_7 -T14_bit_6 -T14_bit_5 -T14_bit_4 -T14_bit_3 -T14_bit_2 -T14_bit_1 -T14_bit0 -T14_bit1 T14_bit2 T14_bit3 -T14_bit4 -T14_bit5 T14_bit6 -T14_bit7 -T14_bit8 -T14_bit9 -T14_bit10 -T14_bit11 -T14_bit12 -T14_bit13 -T14_bit14 -T14_bit15 -T14_bit16 -T14_bit17 -T14_bit18 -T14_bit19 -S15_bit_10 -S15_bit_9 -S15_bit_8 -S15_bit_7 -S15_bit_6 -S15_bit_5 -S15_bit_4 -S15_bit_3 -S15_bit_2 -S15_bit_1 -S15_bit0 -S15_bit1 -S15_bit2 S15_bit3 S15_bit4 -S15_bit5 -S15_bit6 -S15_bit7 -S15_bit8 -S15_bit9 -S15_bit10 -S15_bit11 -S15_bit12 -S15_bit13 -S15_bit14 -S15_bit15 -S15_bit16 -S15_bit17 -S15_bit18 -S15_bit19 -T15_bit_10 -T15_bit_9 -T15_bit_8 -T15_bit_7 -T15_bit_6 -T15_bit_5 -T15_bit_4 -T15_bit_3 -T15_bit_2 -T15_bit_1 -T15_bit0 -T15_bit1 -T15_bit2 T15_bit3 T15_bit4 -T15_bit5 -T15_bit6 -T15_bit7 -T15_bit8 -T15_bit9 -T15_bit10 -T15_bit11 -T15_bit12 -T15_bit13 -T15_bit14 -T15_bit15 -T15_bit16 -T15_bit17 -T15_bit18 -T15_bit19 -S2_bit_10 -S2_bit_9 -S2_bit_8 -S2_bit_7 -S2_bit_6 -S2_bit_5 -S2_bit_4 -S2_bit_3 -S2_bit_2 -S2_bit_1 -S2_bit0 S2_bit1 -S2_bit2 S2_bit3 S2_bit4 -S2_bit5 -S2_bit6 -S2_bit7 -S2_bit8 -S2_bit9 -S2_bit10 -S2_bit11 -S2_bit12 -S2_bit13 -S2_bit14 -S2_bit15 -S2_bit16 -S2_bit17 -S2_bit18 -S2_bit19 -T2_bit_10 -T2_bit_9 -T2_bit_8 -T2_bit_7 -T2_bit_6 -T2_bit_5 -T2_bit_4 -T2_bit_3 -T2_bit_2 -T2_bit_1 -T2_bit0 -T2_bit1 -T2_bit2 -T2_bit3 -T2_bit4 -T2_bit5 -T2_bit6 -T2_bit7 -T2_bit8 -T2_bit9 -T2_bit10 -T2_bit11 -T2_bit12 -T2_bit13 -T2_bit14 -T2_bit15 -T2_bit16 -T2_bit17 -T2_bit18 -T2_bit19 -S3_bit_10 -S3_bit_9 -S3_bit_8 -S3_bit_7 -S3_bit_6 -S3_bit_5 -S3_bit_4 -S3_bit_3 -S3_bit_2 -S3_bit_1 -S3_bit0 -S3_bit1 -S3_bit2 -S3_bit3 S3_bit4 -S3_bit5 S3_bit6 -S3_bit7 -S3_bit8 -S3_bit9 -S3_bit10 -S3_bit11 -S3_bit12 -S3_bit13 -S3_bit14 -S3_bit15 -S3_bit16 -S3_bit17 -S3_bit18 -S3_bit19 -T3_bit_10 -T3_bit_9 -T3_bit_8 -T3_bit_7 -T3_bit_6 -T3_bit_5 -T3_bit_4 -T3_bit_3 -T3_bit_2 -T3_bit_1 -T3_bit0 -T3_bit1 T3_bit2 -T3_bit3 -T3_bit4 -T3_bit5 -T3_bit6 -T3_bit7 -T3_bit8 -T3_bit9 -T3_bit10 -T3_bit11 -T3_bit12 -T3_bit13 -T3_bit14 -T3_bit15 -T3_bit16 -T3_bit17 -T3_bit18 -T3_bit19 -S4_bit_10 -S4_bit_9 -S4_bit_8 -S4_bit_7 -S4_bit_6 -S4_bit_5 -S4_bit_4 -S4_bit_3 -S4_bit_2 -S4_bit_1 -S4_bit0 S4_bit1 S4_bit2 -S4_bit3 S4_bit4 -S4_bit5 -S4_bit6 -S4_bit7 -S4_bit8 -S4_bit9 -S4_bit10 -S4_bit11 -S4_bit12 -S4_bit13 -S4_bit14 -S4_bit15 -S4_bit16 -S4_bit17 -S4_bit18 -S4_bit19 -T4_bit_10 -T4_bit_9 -T4_bit_8 -T4_bit_7 -T4_bit_6 -T4_bit_5 -T4_bit_4 -T4_bit_3 -T4_bit_2 -T4_bit_1 -T4_bit0 -T4_bit1 -T4_bit2 -T4_bit3 -T4_bit4 -T4_bit5 T4_bit6 -T4_bit7 -T4_bit8 -T4_bit9 -T4_bit10 -T4_bit11 -T4_bit12 -T4_bit13 -T4_bit14 -T4_bit15 -T4_bit16 -T4_bit17 -T4_bit18 -T4_bit19 -S5_bit_10 -S5_bit_9 -S5_bit_8 -S5_bit_7 -S5_bit_6 -S5_bit_5 -S5_bit_4 -S5_bit_3 -S5_bit_2 -S5_bit_1 -S5_bit0 -S5_bit1 S5_bit2 -S5_bit3 -S5_bit4 -S5_bit5 -S5_bit6 -S5_bit7 -S5_bit8 -S5_bit9 -S5_bit10 -S5_bit11 -S5_bit12 -S5_bit13 -S5_bit14 -S5_bit15 -S5_bit16 -S5_bit17 -S5_bit18 -S5_bit19 -T5_bit_10 -T5_bit_9 -T5_bit_8 -T5_bit_7 -T5_bit_6 -T5_bit_5 -T5_bit_4 -T5_bit_3 -T5_bit_2 -T5_bit_1 -T5_bit0 -T5_bit1 -T5_bit2 -T5_bit3 -T5_bit4 -T5_bit5 -T5_bit6 -T5_bit7 -T5_bit8 -T5_bit9 -T5_bit10 -T5_bit11 -T5_bit12 -T5_bit13 -T5_bit14 -T5_bit15 -T5_bit16 -T5_bit17 -T5_bit18 -T5_bit19 -S6_bit_10 -S6_bit_9 -S6_bit_8 -S6_bit_7 -S6_bit_6 -S6_bit_5 -S6_bit_4 -S6_bit_3 -S6_bit_2 -S6_bit_1 S6_bit0 -S6_bit1 -S6_bit2 S6_bit3 -S6_bit4 S6_bit5 -S6_bit6 -S6_bit7 -S6_bit8 -S6_bit9 -S6_bit10 -S6_bit11 -S6_bit12 -S6_bit13 -S6_bit14 -S6_bit15 -S6_bit16 -S6_bit17 -S6_bit18 -S6_bit19 -T6_bit_10 -T6_bit_9 -T6_bit_8 -T6_bit_7 -T6_bit_6 -T6_bit_5 -T6_bit_4 -T6_bit_3 -T6_bit_2 -T6_bit_1 -T6_bit0 -T6_bit1 T6_bit2 -T6_bit3 -T6_bit4 -T6_bit5 -T6_bit6 -T6_bit7 -T6_bit8 -T6_bit9 -T6_bit10 -T6_bit11 -T6_bit12 -T6_bit13 -T6_bit14 -T6_bit15 -T6_bit16 -T6_bit17 -T6_bit18 -T6_bit19 -S7_bit_10 -S7_bit_9 -S7_bit_8 -S7_bit_7 -S7_bit_6 -S7_bit_5 -S7_bit_4 -S7_bit_3
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/21961/stat): 21961 (minisat+_script) R 21960 21961 4419 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1851955858 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/21961/statm): 174 3 169 147 0 27 0 [pid=21961] 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=21962 New process pid=21963 New process pid=21964 execve syscall for /bin/sed executable One traced child (pid=21963) 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=21964) exited with status: 0 One traced child (pid=21962) exited with status: 0 New process pid=21965 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-pk1.opb [startup+10.0033 s] Raw data (loadavg): 0.93 0.95 0.88 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 1562 0 0 0 981 7 0 0 25 0 1 0 1851955863 6942720 1511 4294967295 134512640 135094434 3221224432 3221223056 134557598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21965/statm): 1695 1511 145 145 0 1550 0 [pid=21965] vsize: 6780 Current children cumulated CPU time (s) 9.89 Current children cumulated vsize (Kb) 8904 [startup+20.0049 s] Raw data (loadavg): 0.94 0.96 0.88 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 1771 0 0 0 1976 10 0 0 25 0 1 0 1851955863 7929856 1720 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21965/statm): 1936 1720 145 145 0 1791 0 [pid=21965] vsize: 7744 Current children cumulated CPU time (s) 19.87 Current children cumulated vsize (Kb) 9868 [startup+30.0065 s] Raw data (loadavg): 0.95 0.96 0.88 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 1801 0 0 0 2974 11 0 0 25 0 1 0 1851955863 8040448 1750 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 1963 1750 145 145 0 1818 0 [pid=21965] vsize: 7852 Current children cumulated CPU time (s) 29.86 Current children cumulated vsize (Kb) 9976 [startup+40.0071 s] Raw data (loadavg): 0.95 0.96 0.88 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 2143 0 0 0 3968 14 0 0 25 0 1 0 1851955863 9482240 2092 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 2315 2092 145 145 0 2170 0 [pid=21965] vsize: 9260 Current children cumulated CPU time (s) 39.83 Current children cumulated vsize (Kb) 11384 [startup+50.0077 s] Raw data (loadavg): 0.96 0.96 0.88 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 2262 0 0 0 4965 15 0 0 25 0 1 0 1851955863 9969664 2211 4294967295 134512640 135094434 3221224432 3221223088 134558176 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 2434 2211 145 145 0 2289 0 [pid=21965] vsize: 9736 Current children cumulated CPU time (s) 49.81 Current children cumulated vsize (Kb) 11860 [startup+60.0083 s] Raw data (loadavg): 0.97 0.96 0.89 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 2302 0 0 0 5964 16 0 0 25 0 1 0 1851955863 10133504 2251 4294967295 134512640 135094434 3221224432 3221223088 134557956 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 2474 2251 145 145 0 2329 0 [pid=21965] vsize: 9896 Current children cumulated CPU time (s) 59.81 Current children cumulated vsize (Kb) 12020 [startup+70.0089 s] Raw data (loadavg): 0.97 0.96 0.89 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 2400 0 0 0 6962 17 0 0 25 0 1 0 1851955863 10526720 2349 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21965/statm): 2570 2349 145 145 0 2425 0 [pid=21965] vsize: 10280 Current children cumulated CPU time (s) 69.8 Current children cumulated vsize (Kb) 12404 [startup+80.0105 s] Raw data (loadavg): 0.98 0.96 0.89 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 2401 0 0 0 7961 17 0 0 25 0 1 0 1851955863 10526720 2350 4294967295 134512640 135094434 3221224432 3221223056 134557585 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 2570 2350 145 145 0 2425 0 [pid=21965] vsize: 10280 Current children cumulated CPU time (s) 79.79 Current children cumulated vsize (Kb) 12404 [startup+90.0111 s] Raw data (loadavg): 0.98 0.96 0.89 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 2401 0 0 0 8962 17 0 0 25 0 1 0 1851955863 10526720 2350 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 2570 2350 145 145 0 2425 0 [pid=21965] vsize: 10280 Current children cumulated CPU time (s) 89.8 Current children cumulated vsize (Kb) 12404 [startup+100.012 s] Raw data (loadavg): 0.98 0.96 0.89 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 2660 0 0 0 9956 20 0 0 25 0 1 0 1851955863 11571200 2609 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 2825 2609 145 145 0 2680 0 [pid=21965] vsize: 11300 Current children cumulated CPU time (s) 99.77 Current children cumulated vsize (Kb) 13424 [startup+110.012 s] Raw data (loadavg): 0.98 0.96 0.89 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 2960 0 0 0 10952 23 0 0 25 0 1 0 1851955863 12906496 2909 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 3151 2909 145 145 0 3006 0 [pid=21965] vsize: 12604 Current children cumulated CPU time (s) 109.76 Current children cumulated vsize (Kb) 14728 [startup+120.013 s] Raw data (loadavg): 0.99 0.97 0.89 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 2980 0 0 0 11951 23 0 0 25 0 1 0 1851955863 12988416 2929 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 3171 2929 145 145 0 3026 0 [pid=21965] vsize: 12684 Current children cumulated CPU time (s) 119.75 Current children cumulated vsize (Kb) 14808 [startup+130.013 s] Raw data (loadavg): 0.99 0.97 0.89 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 2980 0 0 0 12951 23 0 0 25 0 1 0 1851955863 12988416 2929 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 3171 2929 145 145 0 3026 0 [pid=21965] vsize: 12684 Current children cumulated CPU time (s) 129.75 Current children cumulated vsize (Kb) 14808 [startup+140.014 s] Raw data (loadavg): 0.99 0.97 0.89 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 2980 0 0 0 13951 23 0 0 25 0 1 0 1851955863 12988416 2929 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 3171 2929 145 145 0 3026 0 [pid=21965] vsize: 12684 Current children cumulated CPU time (s) 139.75 Current children cumulated vsize (Kb) 14808 [startup+150.015 s] Raw data (loadavg): 0.99 0.97 0.89 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 2980 0 0 0 14951 24 0 0 25 0 1 0 1851955863 12988416 2929 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 3171 2929 145 145 0 3026 0 [pid=21965] vsize: 12684 Current children cumulated CPU time (s) 149.76 Current children cumulated vsize (Kb) 14808 [startup+160.014 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 2980 0 0 0 15951 24 0 0 25 0 1 0 1851955863 12988416 2929 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 3171 2929 145 145 0 3026 0 [pid=21965] vsize: 12684 Current children cumulated CPU time (s) 159.76 Current children cumulated vsize (Kb) 14808 [startup+170.015 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 3248 0 0 0 16947 26 0 0 25 0 1 0 1851955863 14073856 3197 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 3436 3197 145 145 0 3291 0 [pid=21965] vsize: 13744 Current children cumulated CPU time (s) 169.74 Current children cumulated vsize (Kb) 15868 [startup+180.015 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 3467 0 0 0 17943 28 0 0 25 0 1 0 1851955863 14954496 3416 4294967295 134512640 135094434 3221224432 3221223088 134558169 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 3651 3416 145 145 0 3506 0 [pid=21965] vsize: 14604 Current children cumulated CPU time (s) 179.72 Current children cumulated vsize (Kb) 16728 [startup+190.015 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 3560 0 0 0 18941 29 0 0 25 0 1 0 1851955863 15327232 3509 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 3742 3509 145 145 0 3597 0 [pid=21965] vsize: 14968 Current children cumulated CPU time (s) 189.71 Current children cumulated vsize (Kb) 17092 [startup+200.016 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 3570 0 0 0 19941 29 0 0 25 0 1 0 1851955863 15372288 3519 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 3753 3519 145 145 0 3608 0 [pid=21965] vsize: 15012 Current children cumulated CPU time (s) 199.71 Current children cumulated vsize (Kb) 17136 [startup+210.016 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 3574 0 0 0 20941 29 0 0 25 0 1 0 1851955863 15388672 3523 4294967295 134512640 135094434 3221224432 3221223104 134555945 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 3757 3523 145 145 0 3612 0 [pid=21965] vsize: 15028 Current children cumulated CPU time (s) 209.71 Current children cumulated vsize (Kb) 17152 [startup+220.018 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 3582 0 0 0 21941 29 0 0 25 0 1 0 1851955863 15421440 3531 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 3765 3531 145 145 0 3620 0 [pid=21965] vsize: 15060 Current children cumulated CPU time (s) 219.71 Current children cumulated vsize (Kb) 17184 [startup+230.018 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 3596 0 0 0 22941 29 0 0 25 0 1 0 1851955863 15486976 3545 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 3781 3545 145 145 0 3636 0 [pid=21965] vsize: 15124 Current children cumulated CPU time (s) 229.71 Current children cumulated vsize (Kb) 17248 [startup+240.019 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 3699 0 0 0 23940 30 0 0 25 0 1 0 1851955863 15925248 3648 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 3888 3648 145 145 0 3743 0 [pid=21965] vsize: 15552 Current children cumulated CPU time (s) 239.71 Current children cumulated vsize (Kb) 17676 [startup+250.02 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 3699 0 0 0 24940 30 0 0 25 0 1 0 1851955863 15925248 3648 4294967295 134512640 135094434 3221224432 3221223088 134557956 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 3888 3648 145 145 0 3743 0 [pid=21965] vsize: 15552 Current children cumulated CPU time (s) 249.71 Current children cumulated vsize (Kb) 17676 [startup+260.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 3699 0 0 0 25939 31 0 0 25 0 1 0 1851955863 15925248 3648 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 3888 3648 145 145 0 3743 0 [pid=21965] vsize: 15552 Current children cumulated CPU time (s) 259.71 Current children cumulated vsize (Kb) 17676 [startup+270.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 3699 0 0 0 26940 31 0 0 25 0 1 0 1851955863 15925248 3648 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 3888 3648 145 145 0 3743 0 [pid=21965] vsize: 15552 Current children cumulated CPU time (s) 269.72 Current children cumulated vsize (Kb) 17676 [startup+280.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 3699 0 0 0 27940 31 0 0 25 0 1 0 1851955863 15925248 3648 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 3888 3648 145 145 0 3743 0 [pid=21965] vsize: 15552 Current children cumulated CPU time (s) 279.72 Current children cumulated vsize (Kb) 17676 [startup+290.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 3699 0 0 0 28940 31 0 0 25 0 1 0 1851955863 15925248 3648 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 3888 3648 145 145 0 3743 0 [pid=21965] vsize: 15552 Current children cumulated CPU time (s) 289.72 Current children cumulated vsize (Kb) 17676 [startup+300.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 3699 0 0 0 29940 31 0 0 25 0 1 0 1851955863 15925248 3648 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 3888 3648 145 145 0 3743 0 [pid=21965] vsize: 15552 Current children cumulated CPU time (s) 299.72 Current children cumulated vsize (Kb) 17676 [startup+310.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 3699 0 0 0 30940 31 0 0 25 0 1 0 1851955863 15925248 3648 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 3888 3648 145 145 0 3743 0 [pid=21965] vsize: 15552 Current children cumulated CPU time (s) 309.72 Current children cumulated vsize (Kb) 17676 [startup+320.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 3699 0 0 0 31941 31 0 0 25 0 1 0 1851955863 15925248 3648 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 3888 3648 145 145 0 3743 0 [pid=21965] vsize: 15552 Current children cumulated CPU time (s) 319.73 Current children cumulated vsize (Kb) 17676 [startup+330.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 3699 0 0 0 32940 31 0 0 25 0 1 0 1851955863 15925248 3648 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 3888 3648 145 145 0 3743 0 [pid=21965] vsize: 15552 Current children cumulated CPU time (s) 329.72 Current children cumulated vsize (Kb) 17676 [startup+340.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 3699 0 0 0 33940 31 0 0 25 0 1 0 1851955863 15925248 3648 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 3888 3648 145 145 0 3743 0 [pid=21965] vsize: 15552 Current children cumulated CPU time (s) 339.72 Current children cumulated vsize (Kb) 17676 [startup+350.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 3699 0 0 0 34940 31 0 0 25 0 1 0 1851955863 15925248 3648 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 3888 3648 145 145 0 3743 0 [pid=21965] vsize: 15552 Current children cumulated CPU time (s) 349.72 Current children cumulated vsize (Kb) 17676 [startup+360.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 3699 0 0 0 35940 31 0 0 25 0 1 0 1851955863 15925248 3648 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 3888 3648 145 145 0 3743 0 [pid=21965] vsize: 15552 Current children cumulated CPU time (s) 359.72 Current children cumulated vsize (Kb) 17676 [startup+370.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 3699 0 0 0 36940 32 0 0 25 0 1 0 1851955863 15925248 3648 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 3888 3648 145 145 0 3743 0 [pid=21965] vsize: 15552 Current children cumulated CPU time (s) 369.73 Current children cumulated vsize (Kb) 17676 [startup+380.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 3699 0 0 0 37940 32 0 0 25 0 1 0 1851955863 15925248 3648 4294967295 134512640 135094434 3221224432 3221223088 134558240 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 3888 3648 145 145 0 3743 0 [pid=21965] vsize: 15552 Current children cumulated CPU time (s) 379.73 Current children cumulated vsize (Kb) 17676 [startup+390.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 3699 0 0 0 38940 32 0 0 25 0 1 0 1851955863 15925248 3648 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 3888 3648 145 145 0 3743 0 [pid=21965] vsize: 15552 Current children cumulated CPU time (s) 389.73 Current children cumulated vsize (Kb) 17676 [startup+400.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 3699 0 0 0 39940 32 0 0 25 0 1 0 1851955863 15925248 3648 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 3888 3648 145 145 0 3743 0 [pid=21965] vsize: 15552 Current children cumulated CPU time (s) 399.73 Current children cumulated vsize (Kb) 17676 [startup+410.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 3699 0 0 0 40940 32 0 0 25 0 1 0 1851955863 15925248 3648 4294967295 134512640 135094434 3221224432 3221223088 134557882 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 3888 3648 145 145 0 3743 0 [pid=21965] vsize: 15552 Current children cumulated CPU time (s) 409.73 Current children cumulated vsize (Kb) 17676 [startup+420.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 3699 0 0 0 41940 32 0 0 25 0 1 0 1851955863 15925248 3648 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 3888 3648 145 145 0 3743 0 [pid=21965] vsize: 15552 Current children cumulated CPU time (s) 419.73 Current children cumulated vsize (Kb) 17676 [startup+430.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 3943 0 0 0 42936 34 0 0 25 0 1 0 1851955863 16924672 3892 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 4132 3892 145 145 0 3987 0 [pid=21965] vsize: 16528 Current children cumulated CPU time (s) 429.71 Current children cumulated vsize (Kb) 18652 [startup+440.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4046 0 0 0 43934 34 0 0 25 0 1 0 1851955863 17342464 3995 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 4234 3995 145 145 0 4089 0 [pid=21965] vsize: 16936 Current children cumulated CPU time (s) 439.69 Current children cumulated vsize (Kb) 19060 [startup+450.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4046 0 0 0 44934 34 0 0 25 0 1 0 1851955863 17342464 3995 4294967295 134512640 135094434 3221224432 3221222912 134780996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 4234 3995 145 145 0 4089 0 [pid=21965] vsize: 16936 Current children cumulated CPU time (s) 449.69 Current children cumulated vsize (Kb) 19060 [startup+460.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4046 0 0 0 45934 34 0 0 25 0 1 0 1851955863 17342464 3995 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 4234 3995 145 145 0 4089 0 [pid=21965] vsize: 16936 Current children cumulated CPU time (s) 459.69 Current children cumulated vsize (Kb) 19060 [startup+470.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4046 0 0 0 46934 34 0 0 25 0 1 0 1851955863 17342464 3995 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 4234 3995 145 145 0 4089 0 [pid=21965] vsize: 16936 Current children cumulated CPU time (s) 469.69 Current children cumulated vsize (Kb) 19060 [startup+480.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4046 0 0 0 47934 34 0 0 25 0 1 0 1851955863 17342464 3995 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 4234 3995 145 145 0 4089 0 [pid=21965] vsize: 16936 Current children cumulated CPU time (s) 479.69 Current children cumulated vsize (Kb) 19060 [startup+490.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4046 0 0 0 48934 35 0 0 25 0 1 0 1851955863 17342464 3995 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 4234 3995 145 145 0 4089 0 [pid=21965] vsize: 16936 Current children cumulated CPU time (s) 489.7 Current children cumulated vsize (Kb) 19060 [startup+500.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4046 0 0 0 49934 35 0 0 25 0 1 0 1851955863 17342464 3995 4294967295 134512640 135094434 3221224432 3221223088 134557925 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 4234 3995 145 145 0 4089 0 [pid=21965] vsize: 16936 Current children cumulated CPU time (s) 499.7 Current children cumulated vsize (Kb) 19060 [startup+510.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4046 0 0 0 50934 35 0 0 25 0 1 0 1851955863 17342464 3995 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 4234 3995 145 145 0 4089 0 [pid=21965] vsize: 16936 Current children cumulated CPU time (s) 509.7 Current children cumulated vsize (Kb) 19060 [startup+520.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4046 0 0 0 51933 36 0 0 25 0 1 0 1851955863 17342464 3995 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 4234 3995 145 145 0 4089 0 [pid=21965] vsize: 16936 Current children cumulated CPU time (s) 519.7 Current children cumulated vsize (Kb) 19060 [startup+530.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4046 0 0 0 52933 37 0 0 25 0 1 0 1851955863 17342464 3995 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 4234 3995 145 145 0 4089 0 [pid=21965] vsize: 16936 Current children cumulated CPU time (s) 529.71 Current children cumulated vsize (Kb) 19060 [startup+540.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4046 0 0 0 53933 37 0 0 25 0 1 0 1851955863 17342464 3995 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 4234 3995 145 145 0 4089 0 [pid=21965] vsize: 16936 Current children cumulated CPU time (s) 539.71 Current children cumulated vsize (Kb) 19060 [startup+550.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4046 0 0 0 54933 37 0 0 25 0 1 0 1851955863 17342464 3995 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 4234 3995 145 145 0 4089 0 [pid=21965] vsize: 16936 Current children cumulated CPU time (s) 549.71 Current children cumulated vsize (Kb) 19060 [startup+560.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4106 0 0 0 55932 38 0 0 25 0 1 0 1851955863 17588224 4055 4294967295 134512640 135094434 3221224432 3221223024 134557182 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 4294 4055 145 145 0 4149 0 [pid=21965] vsize: 17176 Current children cumulated CPU time (s) 559.71 Current children cumulated vsize (Kb) 19300 [startup+570.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4208 0 0 0 56930 39 0 0 25 0 1 0 1851955863 18006016 4157 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 4396 4157 145 145 0 4251 0 [pid=21965] vsize: 17584 Current children cumulated CPU time (s) 569.7 Current children cumulated vsize (Kb) 19708 [startup+580.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4208 0 0 0 57929 39 0 0 25 0 1 0 1851955863 18006016 4157 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 4396 4157 145 145 0 4251 0 [pid=21965] vsize: 17584 Current children cumulated CPU time (s) 579.69 Current children cumulated vsize (Kb) 19708 [startup+590.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4212 0 0 0 58930 39 0 0 25 0 1 0 1851955863 18022400 4161 4294967295 134512640 135094434 3221224432 3221223088 134558026 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 4400 4161 145 145 0 4255 0 [pid=21965] vsize: 17600 Current children cumulated CPU time (s) 589.7 Current children cumulated vsize (Kb) 19724 [startup+600.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4214 0 0 0 59930 40 0 0 25 0 1 0 1851955863 18030592 4163 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 4402 4163 145 145 0 4257 0 [pid=21965] vsize: 17608 Current children cumulated CPU time (s) 599.71 Current children cumulated vsize (Kb) 19732 [startup+610.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4484 0 0 0 60924 43 0 0 25 0 1 0 1851955863 19136512 4433 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 4672 4433 145 145 0 4527 0 [pid=21965] vsize: 18688 Current children cumulated CPU time (s) 609.68 Current children cumulated vsize (Kb) 20812 [startup+620.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4707 0 0 0 61919 45 0 0 25 0 1 0 1851955863 20029440 4656 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 4890 4656 145 145 0 4745 0 [pid=21965] vsize: 19560 Current children cumulated CPU time (s) 619.65 Current children cumulated vsize (Kb) 21684 [startup+630.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4707 0 0 0 62919 45 0 0 25 0 1 0 1851955863 20029440 4656 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 4890 4656 145 145 0 4745 0 [pid=21965] vsize: 19560 Current children cumulated CPU time (s) 629.65 Current children cumulated vsize (Kb) 21684 [startup+640.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4708 0 0 0 63919 45 0 0 25 0 1 0 1851955863 20029440 4657 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 4890 4657 145 145 0 4745 0 [pid=21965] vsize: 19560 Current children cumulated CPU time (s) 639.65 Current children cumulated vsize (Kb) 21684 [startup+650.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4708 0 0 0 64919 45 0 0 25 0 1 0 1851955863 20029440 4657 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 4890 4657 145 145 0 4745 0 [pid=21965] vsize: 19560 Current children cumulated CPU time (s) 649.65 Current children cumulated vsize (Kb) 21684 [startup+660.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4708 0 0 0 65919 46 0 0 25 0 1 0 1851955863 20029440 4657 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 4890 4657 145 145 0 4745 0 [pid=21965] vsize: 19560 Current children cumulated CPU time (s) 659.66 Current children cumulated vsize (Kb) 21684 [startup+670.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4708 0 0 0 66919 46 0 0 25 0 1 0 1851955863 20029440 4657 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 4890 4657 145 145 0 4745 0 [pid=21965] vsize: 19560 Current children cumulated CPU time (s) 669.66 Current children cumulated vsize (Kb) 21684 [startup+680.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4708 0 0 0 67919 46 0 0 25 0 1 0 1851955863 20029440 4657 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 4890 4657 145 145 0 4745 0 [pid=21965] vsize: 19560 Current children cumulated CPU time (s) 679.66 Current children cumulated vsize (Kb) 21684 [startup+690.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4708 0 0 0 68920 46 0 0 25 0 1 0 1851955863 20029440 4657 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 4890 4657 145 145 0 4745 0 [pid=21965] vsize: 19560 Current children cumulated CPU time (s) 689.67 Current children cumulated vsize (Kb) 21684 [startup+700.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4708 0 0 0 69920 46 0 0 25 0 1 0 1851955863 20029440 4657 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 4890 4657 145 145 0 4745 0 [pid=21965] vsize: 19560 Current children cumulated CPU time (s) 699.67 Current children cumulated vsize (Kb) 21684 [startup+710.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4708 0 0 0 70920 46 0 0 25 0 1 0 1851955863 20029440 4657 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 4890 4657 145 145 0 4745 0 [pid=21965] vsize: 19560 Current children cumulated CPU time (s) 709.67 Current children cumulated vsize (Kb) 21684 [startup+720.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4708 0 0 0 71920 46 0 0 25 0 1 0 1851955863 20029440 4657 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 4890 4657 145 145 0 4745 0 [pid=21965] vsize: 19560 Current children cumulated CPU time (s) 719.67 Current children cumulated vsize (Kb) 21684 [startup+730.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4708 0 0 0 72920 46 0 0 25 0 1 0 1851955863 20029440 4657 4294967295 134512640 135094434 3221224432 3221223088 134558156 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 4890 4657 145 145 0 4745 0 [pid=21965] vsize: 19560 Current children cumulated CPU time (s) 729.67 Current children cumulated vsize (Kb) 21684 [startup+740.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4708 0 0 0 73921 46 0 0 25 0 1 0 1851955863 20029440 4657 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 4890 4657 145 145 0 4745 0 [pid=21965] vsize: 19560 Current children cumulated CPU time (s) 739.68 Current children cumulated vsize (Kb) 21684 [startup+750.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4708 0 0 0 74921 46 0 0 25 0 1 0 1851955863 20029440 4657 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 4890 4657 145 145 0 4745 0 [pid=21965] vsize: 19560 Current children cumulated CPU time (s) 749.68 Current children cumulated vsize (Kb) 21684 [startup+760.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4708 0 0 0 75921 46 0 0 25 0 1 0 1851955863 20029440 4657 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 4890 4657 145 145 0 4745 0 [pid=21965] vsize: 19560 Current children cumulated CPU time (s) 759.68 Current children cumulated vsize (Kb) 21684 [startup+770.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4708 0 0 0 76921 46 0 0 25 0 1 0 1851955863 20029440 4657 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 4890 4657 145 145 0 4745 0 [pid=21965] vsize: 19560 Current children cumulated CPU time (s) 769.68 Current children cumulated vsize (Kb) 21684 [startup+780.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4709 0 0 0 77921 46 0 0 25 0 1 0 1851955863 20029440 4658 4294967295 134512640 135094434 3221224432 3221223088 134557956 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 4890 4658 145 145 0 4745 0 [pid=21965] vsize: 19560 Current children cumulated CPU time (s) 779.68 Current children cumulated vsize (Kb) 21684 [startup+790.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4709 0 0 0 78922 46 0 0 25 0 1 0 1851955863 20029440 4658 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 4890 4658 145 145 0 4745 0 [pid=21965] vsize: 19560 Current children cumulated CPU time (s) 789.69 Current children cumulated vsize (Kb) 21684 [startup+800.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4852 0 0 0 79919 47 0 0 25 0 1 0 1851955863 20627456 4801 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5036 4801 145 145 0 4891 0 [pid=21965] vsize: 20144 Current children cumulated CPU time (s) 799.67 Current children cumulated vsize (Kb) 22268 [startup+810.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4994 0 0 0 80917 48 0 0 25 0 1 0 1851955863 21192704 4943 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5174 4943 145 145 0 5029 0 [pid=21965] vsize: 20696 Current children cumulated CPU time (s) 809.66 Current children cumulated vsize (Kb) 22820 [startup+820.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4994 0 0 0 81917 48 0 0 25 0 1 0 1851955863 21192704 4943 4294967295 134512640 135094434 3221224432 3221223136 134554401 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5174 4943 145 145 0 5029 0 [pid=21965] vsize: 20696 Current children cumulated CPU time (s) 819.66 Current children cumulated vsize (Kb) 22820 [startup+830.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4994 0 0 0 82918 48 0 0 25 0 1 0 1851955863 21192704 4943 4294967295 134512640 135094434 3221224432 3221223104 134555849 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5174 4943 145 145 0 5029 0 [pid=21965] vsize: 20696 Current children cumulated CPU time (s) 829.67 Current children cumulated vsize (Kb) 22820 [startup+840.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4994 0 0 0 83918 48 0 0 25 0 1 0 1851955863 21192704 4943 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5174 4943 145 145 0 5029 0 [pid=21965] vsize: 20696 Current children cumulated CPU time (s) 839.67 Current children cumulated vsize (Kb) 22820 [startup+850.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4994 0 0 0 84918 48 0 0 25 0 1 0 1851955863 21192704 4943 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5174 4943 145 145 0 5029 0 [pid=21965] vsize: 20696 Current children cumulated CPU time (s) 849.67 Current children cumulated vsize (Kb) 22820 [startup+860.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4994 0 0 0 85918 49 0 0 25 0 1 0 1851955863 21192704 4943 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5174 4943 145 145 0 5029 0 [pid=21965] vsize: 20696 Current children cumulated CPU time (s) 859.68 Current children cumulated vsize (Kb) 22820 [startup+870.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 4997 0 0 0 86918 49 0 0 25 0 1 0 1851955863 21209088 4946 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5178 4946 145 145 0 5033 0 [pid=21965] vsize: 20712 Current children cumulated CPU time (s) 869.68 Current children cumulated vsize (Kb) 22836 [startup+880.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 5130 0 0 0 87916 50 0 0 25 0 1 0 1851955863 21762048 5079 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5313 5079 145 145 0 5168 0 [pid=21965] vsize: 21252 Current children cumulated CPU time (s) 879.67 Current children cumulated vsize (Kb) 23376 [startup+890.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 5371 0 0 0 88912 52 0 0 25 0 1 0 1851955863 22749184 5320 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5554 5320 145 145 0 5409 0 [pid=21965] vsize: 22216 Current children cumulated CPU time (s) 889.65 Current children cumulated vsize (Kb) 24340 [startup+900.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 5607 0 0 0 89909 53 0 0 25 0 1 0 1851955863 23715840 5556 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5790 5556 145 145 0 5645 0 [pid=21965] vsize: 23160 Current children cumulated CPU time (s) 899.63 Current children cumulated vsize (Kb) 25284 [startup+910.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 5608 0 0 0 90909 53 0 0 25 0 1 0 1851955863 23719936 5557 4294967295 134512640 135094434 3221224432 3221223024 134557236 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5791 5557 145 145 0 5646 0 [pid=21965] vsize: 23164 Current children cumulated CPU time (s) 909.63 Current children cumulated vsize (Kb) 25288 [startup+920.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 5608 0 0 0 91909 53 0 0 25 0 1 0 1851955863 23719936 5557 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5791 5557 145 145 0 5646 0 [pid=21965] vsize: 23164 Current children cumulated CPU time (s) 919.63 Current children cumulated vsize (Kb) 25288 [startup+930.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 5608 0 0 0 92909 54 0 0 25 0 1 0 1851955863 23719936 5557 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5791 5557 145 145 0 5646 0 [pid=21965] vsize: 23164 Current children cumulated CPU time (s) 929.64 Current children cumulated vsize (Kb) 25288 [startup+940.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 5608 0 0 0 93909 54 0 0 25 0 1 0 1851955863 23719936 5557 4294967295 134512640 135094434 3221224432 3221223104 134556465 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5791 5557 145 145 0 5646 0 [pid=21965] vsize: 23164 Current children cumulated CPU time (s) 939.64 Current children cumulated vsize (Kb) 25288 [startup+950.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 5608 0 0 0 94909 54 0 0 25 0 1 0 1851955863 23719936 5557 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5791 5557 145 145 0 5646 0 [pid=21965] vsize: 23164 Current children cumulated CPU time (s) 949.64 Current children cumulated vsize (Kb) 25288 [startup+960.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 5608 0 0 0 95909 54 0 0 25 0 1 0 1851955863 23719936 5557 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5791 5557 145 145 0 5646 0 [pid=21965] vsize: 23164 Current children cumulated CPU time (s) 959.64 Current children cumulated vsize (Kb) 25288 [startup+970.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 5608 0 0 0 96909 54 0 0 25 0 1 0 1851955863 23719936 5557 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5791 5557 145 145 0 5646 0 [pid=21965] vsize: 23164 Current children cumulated CPU time (s) 969.64 Current children cumulated vsize (Kb) 25288 [startup+980.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 5608 0 0 0 97909 54 0 0 25 0 1 0 1851955863 23719936 5557 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5791 5557 145 145 0 5646 0 [pid=21965] vsize: 23164 Current children cumulated CPU time (s) 979.64 Current children cumulated vsize (Kb) 25288 [startup+990.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 5608 0 0 0 98909 54 0 0 25 0 1 0 1851955863 23719936 5557 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5791 5557 145 145 0 5646 0 [pid=21965] vsize: 23164 Current children cumulated CPU time (s) 989.64 Current children cumulated vsize (Kb) 25288 [startup+1000.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 5608 0 0 0 99909 55 0 0 25 0 1 0 1851955863 23719936 5557 4294967295 134512640 135094434 3221224432 3221223088 134558174 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5791 5557 145 145 0 5646 0 [pid=21965] vsize: 23164 Current children cumulated CPU time (s) 999.65 Current children cumulated vsize (Kb) 25288 [startup+1010.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 5608 0 0 0 100909 55 0 0 25 0 1 0 1851955863 23719936 5557 4294967295 134512640 135094434 3221224432 3221223072 134562161 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5791 5557 145 145 0 5646 0 [pid=21965] vsize: 23164 Current children cumulated CPU time (s) 1009.65 Current children cumulated vsize (Kb) 25288 [startup+1020.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 5608 0 0 0 101909 55 0 0 25 0 1 0 1851955863 23719936 5557 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5791 5557 145 145 0 5646 0 [pid=21965] vsize: 23164 Current children cumulated CPU time (s) 1019.65 Current children cumulated vsize (Kb) 25288 [startup+1030.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 5608 0 0 0 102910 55 0 0 25 0 1 0 1851955863 23719936 5557 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5791 5557 145 145 0 5646 0 [pid=21965] vsize: 23164 Current children cumulated CPU time (s) 1029.66 Current children cumulated vsize (Kb) 25288 [startup+1040.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 5608 0 0 0 103910 55 0 0 25 0 1 0 1851955863 23719936 5557 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5791 5557 145 145 0 5646 0 [pid=21965] vsize: 23164 Current children cumulated CPU time (s) 1039.66 Current children cumulated vsize (Kb) 25288 [startup+1050.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 5608 0 0 0 104910 55 0 0 25 0 1 0 1851955863 23719936 5557 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5791 5557 145 145 0 5646 0 [pid=21965] vsize: 23164 Current children cumulated CPU time (s) 1049.66 Current children cumulated vsize (Kb) 25288 [startup+1060.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 5608 0 0 0 105910 55 0 0 25 0 1 0 1851955863 23719936 5557 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5791 5557 145 145 0 5646 0 [pid=21965] vsize: 23164 Current children cumulated CPU time (s) 1059.66 Current children cumulated vsize (Kb) 25288 [startup+1070.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 5608 0 0 0 106911 55 0 0 25 0 1 0 1851955863 23719936 5557 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5791 5557 145 145 0 5646 0 [pid=21965] vsize: 23164 Current children cumulated CPU time (s) 1069.67 Current children cumulated vsize (Kb) 25288 [startup+1080.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 5608 0 0 0 107911 55 0 0 25 0 1 0 1851955863 23719936 5557 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5791 5557 145 145 0 5646 0 [pid=21965] vsize: 23164 Current children cumulated CPU time (s) 1079.67 Current children cumulated vsize (Kb) 25288 [startup+1090.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 5608 0 0 0 108911 55 0 0 25 0 1 0 1851955863 23719936 5557 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5791 5557 145 145 0 5646 0 [pid=21965] vsize: 23164 Current children cumulated CPU time (s) 1089.67 Current children cumulated vsize (Kb) 25288 [startup+1100.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 5608 0 0 0 109911 55 0 0 25 0 1 0 1851955863 23719936 5557 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5791 5557 145 145 0 5646 0 [pid=21965] vsize: 23164 Current children cumulated CPU time (s) 1099.67 Current children cumulated vsize (Kb) 25288 [startup+1110.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 5608 0 0 0 110911 55 0 0 25 0 1 0 1851955863 23719936 5557 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5791 5557 145 145 0 5646 0 [pid=21965] vsize: 23164 Current children cumulated CPU time (s) 1109.67 Current children cumulated vsize (Kb) 25288 [startup+1120.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 5608 0 0 0 111910 57 0 0 25 0 1 0 1851955863 23719936 5557 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21965/statm): 5791 5557 145 145 0 5646 0 [pid=21965] vsize: 23164 Current children cumulated CPU time (s) 1119.68 Current children cumulated vsize (Kb) 25288 [startup+1130.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 5608 0 0 0 112909 57 0 0 25 0 1 0 1851955863 23719936 5557 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5791 5557 145 145 0 5646 0 [pid=21965] vsize: 23164 Current children cumulated CPU time (s) 1129.67 Current children cumulated vsize (Kb) 25288 [startup+1140.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 5608 0 0 0 113909 58 0 0 25 0 1 0 1851955863 23719936 5557 4294967295 134512640 135094434 3221224432 3221223024 134557950 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5791 5557 145 145 0 5646 0 [pid=21965] vsize: 23164 Current children cumulated CPU time (s) 1139.68 Current children cumulated vsize (Kb) 25288 [startup+1150.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 5608 0 0 0 114909 58 0 0 25 0 1 0 1851955863 23719936 5557 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5791 5557 145 145 0 5646 0 [pid=21965] vsize: 23164 Current children cumulated CPU time (s) 1149.68 Current children cumulated vsize (Kb) 25288 [startup+1160.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 5608 0 0 0 115908 58 0 0 25 0 1 0 1851955863 23719936 5557 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5791 5557 145 145 0 5646 0 [pid=21965] vsize: 23164 Current children cumulated CPU time (s) 1159.67 Current children cumulated vsize (Kb) 25288 [startup+1170.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 5608 0 0 0 116909 58 0 0 25 0 1 0 1851955863 23719936 5557 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5791 5557 145 145 0 5646 0 [pid=21965] vsize: 23164 Current children cumulated CPU time (s) 1169.68 Current children cumulated vsize (Kb) 25288 [startup+1180.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 5608 0 0 0 117909 59 0 0 25 0 1 0 1851955863 23719936 5557 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5791 5557 145 145 0 5646 0 [pid=21965] vsize: 23164 Current children cumulated CPU time (s) 1179.69 Current children cumulated vsize (Kb) 25288 [startup+1190.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 5608 0 0 0 118909 59 0 0 25 0 1 0 1851955863 23719936 5557 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5791 5557 145 145 0 5646 0 [pid=21965] vsize: 23164 Current children cumulated CPU time (s) 1189.69 Current children cumulated vsize (Kb) 25288 [startup+1200.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 5608 0 0 0 119909 59 0 0 25 0 1 0 1851955863 23719936 5557 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5791 5557 145 145 0 5646 0 [pid=21965] vsize: 23164 Current children cumulated CPU time (s) 1199.69 Current children cumulated vsize (Kb) 25288 [startup+1210.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 5608 0 0 0 120909 59 0 0 25 0 1 0 1851955863 23719936 5557 4294967295 134512640 135094434 3221224432 3221223068 134562980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5791 5557 145 145 0 5646 0 [pid=21965] vsize: 23164 Current children cumulated CPU time (s) 1209.69 Current children cumulated vsize (Kb) 25288 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21965 Raw data (/proc/21961/stat): 21961 (minisat+_script) S 21960 21961 4419 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1851955858 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21961/statm): 531 226 485 147 0 384 0 [pid=21961] vsize: 2124 Raw data (/proc/21965/stat): 21965 (minisat+_64-bit) R 21961 21961 4419 0 -1 0 5608 0 0 0 120909 59 0 0 25 0 1 0 1851955863 23719936 5557 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21965/statm): 5791 5557 145 145 0 5646 0 [pid=21965] vsize: 23164 Current children cumulated CPU time (s) 1209.69 Current children cumulated vsize (Kb) 25288 Sending SIGTERM to -21961 Sleeping 2 seconds One traced child (pid=21961) ended because it received signal 15 (SIGTERM) One traced child (pid=21965) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.11 CPU time (s): 1209.71 CPU user time (s): 1209.1 CPU system time (s): 0.606907 CPU usage (%): 99.9667 Max. virtual memory (cumulated for all children) (Kb): 25288
ERROR: no interpretation found !