Name | normalized-opb/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 | NO |
(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 | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 0.063989 |
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 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc21 THE 2005-05-25 20:06:07 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=22243 boxname=wulflinc21 idbench=1059 idsolver=15 numberseed=0 MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814 /oldhome/oroussel/solvers/minisat+_script MD5SUM BENCH: ca2f95c2509c09ae8cf1945e12d0eb97 /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-pk1.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-pk1.opb IDLAUNCH: 22243 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.161 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.161 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 849128 kB Buffers: 4684 kB Cached: 159860 kB SwapCached: 968 kB Active: 17072 kB Inactive: 149616 kB HighTotal: 131008 kB HighFree: 109284 kB LowTotal: 903652 kB LowFree: 739844 kB SwapTotal: 2097892 kB SwapFree: 2096008 kB Dirty: 32 kB Writeback: 0 kB Mapped: 5112 kB Slab: 13184 kB Committed_AS: 63880 kB PageTables: 332 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-25 20:26:37 (client local time) WITH STATUS 152 IN 1229.84 SECONDS stats: 22243 7 1229.84 152 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### 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 | 864897 | 39112 134484 | 30740 22206 702334 31.6 | 26.891 % | c | 868741 | 39112 134484 | 33814 26050 877801 33.7 | 26.891 % | c | 874507 | 39112 134484 | 37196 31816 1089923 34.3 | 26.891 % | /oldhome/oroussel/solvers/minisat+_script: line 9: 17761 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@" #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.91 0.95 0.90 2/55 17757 Raw data (stat): 17757 (runsolver) R 17756 32363 32362 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 718892173 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0001 s] Raw data (loadavg): 0.92 0.95 0.90 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+20.0006 s] Raw data (loadavg): 0.93 0.96 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+30.0014 s] Raw data (loadavg): 0.94 0.96 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+40.0011 s] Raw data (loadavg): 0.95 0.96 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+50.0017 s] Raw data (loadavg): 0.96 0.96 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+60.0014 s] Raw data (loadavg): 0.97 0.96 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+70.002 s] Raw data (loadavg): 0.97 0.96 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+80.0027 s] Raw data (loadavg): 0.97 0.96 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+90.0023 s] Raw data (loadavg): 0.98 0.96 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+100.003 s] Raw data (loadavg): 0.98 0.96 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+110.004 s] Raw data (loadavg): 0.98 0.96 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+120.004 s] Raw data (loadavg): 0.98 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+130.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+140.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+150.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+160.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+170.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+180.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+190.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+200.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+210.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+220.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+230.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+240.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+250.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+260.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+270.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+280.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+290.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+300.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+310.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+320.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+330.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+340.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+350.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+360.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+370.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+380.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+390.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+400.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+410.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+420.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+430.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+440.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+450.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+460.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+470.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+480.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+490.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+500.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+510.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+520.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+530.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+540.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+550.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+560.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+570.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+580.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+590.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+600.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+610.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+620.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+630.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+640.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+650.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+660.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+670.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+680.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+690.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+700.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+710.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+720.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+730.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+740.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+750.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+760.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+770.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+780.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+790.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+800.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+810.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+820.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+830.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+840.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+850.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+860.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+870.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+880.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+890.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+900.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+910.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+920.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+930.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+940.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+950.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+960.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+970.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+980.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+990.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1000 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1010 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1020 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1030 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1040 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1050 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1060 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1070 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1080 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1090 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1100 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1110 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1120 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1130 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1140 s] Raw data (loadavg): 1.07 0.99 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1150 s] Raw data (loadavg): 1.06 0.99 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1160 s] Raw data (loadavg): 1.05 0.99 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1170 s] Raw data (loadavg): 1.04 0.99 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1180 s] Raw data (loadavg): 1.04 0.99 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1190 s] Raw data (loadavg): 1.03 0.99 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1200 s] Raw data (loadavg): 1.03 0.99 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1210 s] Raw data (loadavg): 1.02 0.99 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1220 s] Raw data (loadavg): 1.02 0.99 0.91 2/56 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1229.69 s] Raw data (loadavg): 1.01 0.99 0.91 1/54 17761 Raw data (stat): 17757 (minisat+_script) S 17756 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 718892173 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 0 Child status: 152 Real time (s): 1229.69 CPU time (s): 1229.84 CPU user time (s): 1229.51 CPU system time (s): 0.328949 CPU usage (%): 100.013 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####