Name | normalized-opb/mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-markshare1.opb |
MD5SUM | 10386fd19d9976c249ce2be861b38a70 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 63488 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 180 |
Biggest coefficient in the objective function | 536870912 |
Number of bits for the biggest coefficient in the objective function | 30 |
Sum of the numbers in the objective function | 6442450938 |
Number of bits of the sum of numbers in the objective function | 33 |
Biggest number in a constraint | 536870912 |
Number of bits of the biggest number in a constraint | 30 |
Biggest sum of numbers in a constraint | 6442450938 |
Number of bits of the biggest sum of numbers | 33 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1175.12 |
Number of variables | 230 |
Total number of constraints | 56 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 50 |
Number of constraints which are nor clauses,nor cardinality constraints | 6 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 80 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc11 THE 2005-04-22 00:57:37 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=12646 boxname=wulflinc11 idbench=973 idsolver=10 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 10386fd19d9976c249ce2be861b38a70 /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-markshare1.opb REAL COMMAND: minisat+ -ca /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-markshare1.opb /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-markshare1.opb IDLAUNCH: 12646 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.028 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.028 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: 246400 kB Buffers: 36172 kB Cached: 730392 kB SwapCached: 0 kB Active: 382132 kB Inactive: 387172 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 246148 kB SwapTotal: 2097136 kB SwapFree: 2097048 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6820 kB Slab: 13264 kB Committed_AS: 63592 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-22 01:17:42 (client local time) WITH STATUS 10 IN 1200.53 SECONDS stats: 12646 7 1200.53 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 12 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ###### c -- Clauses(.)/Splits(s): (none) c ---[ 10]---> Adder-cost: 304 maxlim: 3240959 bits: 23/22 c ---[ 8]---> Adder-cost: 314 maxlim: 3453951 bits: 23/22 c ---[ 6]---> Adder-cost: 348 maxlim: 3482623 bits: 23/22 c ---[ 4]---> Adder-cost: 318 maxlim: 3294207 bits: 23/22 c ---[ 2]---> Adder-cost: 312 maxlim: 3286015 bits: 23/22 c ---[ 0]---> Adder-cost: 314 maxlim: 3289087 bits: 23/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 12820 45524 | 4273 0 0 nan | 0.000 % | c | 100 | 12820 45524 | 4700 100 594 5.9 | 14.261 % | c ============================================================================== c [1mFound solution: 4615168[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 110 maxlim: 7775 bits: 14/13 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 141 | 13530 48047 | 4510 141 1027 7.3 | 14.261 % | c | 241 | 13530 48047 | 4961 241 10551 43.8 | 13.848 % | c | 391 | 13530 48047 | 5457 391 26628 68.1 | 13.848 % | c ============================================================================== c [1mFound solution: 4451328[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 7935 bits: 14/13 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 543 | 13531 48054 | 4510 543 37699 69.4 | 13.848 % | c | 643 | 13531 48054 | 4961 643 51023 79.4 | 13.884 % | c ============================================================================== c [1mFound solution: 4440064[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 7946 bits: 14/13 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 697 | 13554 48177 | 4518 696 53533 76.9 | 13.884 % | c | 798 | 13554 48177 | 4969 797 61190 76.8 | 14.005 % | c ============================================================================== c [1mFound solution: 4252672[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 8129 bits: 14/13 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 821 | 13561 48224 | 4520 820 62616 76.4 | 14.005 % | c ============================================================================== c [1mFound solution: 4208640[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 8172 bits: 14/13 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 831 | 13571 48296 | 4523 830 63428 76.4 | 14.005 % | c ============================================================================== c [1mFound solution: 3886080[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 8487 bits: 14/14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 833 | 13546 48127 | 4515 832 63542 76.4 | 14.005 % | c ============================================================================== c [1mFound solution: 3854336[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 8518 bits: 14/14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 917 | 13550 48170 | 4516 916 70229 76.7 | 14.005 % | c | 1019 | 13550 48170 | 4967 1018 80774 79.3 | 14.666 % | c | 1170 | 13550 48170 | 5464 1169 94999 81.3 | 14.666 % | c | 1395 | 13550 48170 | 6010 1394 107700 77.3 | 14.666 % | c ============================================================================== c [1mFound solution: 3727360[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 8642 bits: 14/14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1604 | 13541 48162 | 4513 1601 110127 68.8 | 14.666 % | c ============================================================================== c [1mFound solution: 3437568[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 8925 bits: 14/14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1650 | 13552 48237 | 4517 1647 111474 67.7 | 14.666 % | c | 1751 | 13552 48237 | 4968 1748 115080 65.8 | 15.118 % | c | 1903 | 13536 48185 | 5465 1898 125446 66.1 | 15.200 % | c | 2128 | 13536 48185 | 6012 2123 136831 64.5 | 15.200 % | c | 2467 | 13536 48185 | 6613 2462 158186 64.3 | 15.200 % | c | 2974 | 13530 48167 | 7274 2968 179281 60.4 | 15.242 % | c | 3733 | 13530 48167 | 8002 3727 252187 67.7 | 15.242 % | c ============================================================================== c [1mFound solution: 3383296[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 8978 bits: 14/14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4363 | 13528 48183 | 4509 4356 299872 68.8 | 15.242 % | c | 4463 | 13528 48183 | 4959 4456 306852 68.9 | 15.410 % | c | 4613 | 13528 48183 | 5455 4606 320504 69.6 | 15.410 % | c | 4838 | 13528 48183 | 6001 4831 328970 68.1 | 15.410 % | c | 5175 | 13528 48183 | 6601 5168 348729 67.5 | 15.410 % | c | 5681 | 13528 48183 | 7261 5674 397146 70.0 | 15.410 % | c ============================================================================== c [1mFound solution: 1483776[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 10833 bits: 14/14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 5719 | 13509 48008 | 4503 5712 397801 69.6 | 15.410 % | c | 5819 | 13494 47955 | 4953 2954 175354 59.4 | 15.688 % | c | 5969 | 13494 47955 | 5448 3104 181479 58.5 | 15.688 % | c | 6194 | 13485 47926 | 5993 3328 188021 56.5 | 15.770 % | c | 6531 | 13476 47897 | 6592 3664 212311 57.9 | 15.852 % | c | 7039 | 13476 47897 | 7252 4172 246404 59.1 | 15.852 % | c | 7798 | 13476 47897 | 7977 4931 292836 59.4 | 15.852 % | c | 8937 | 13476 47897 | 8775 6070 352287 58.0 | 15.852 % | c ============================================================================== c [1mFound solution: 927744[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 4 maxlim: 5232 bits: 13/13 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 9673 | 13411 47683 | 4470 6327 303187 47.9 | 15.852 % | c | 9773 | 13384 47590 | 4917 3249 122154 37.6 | 16.680 % | c | 9923 | 13384 47590 | 5408 3399 128458 37.8 | 16.680 % | c | 10151 | 13384 47590 | 5949 3627 132423 36.5 | 16.680 % | c | 10488 | 13364 47508 | 6544 3961 144082 36.4 | 16.844 % | c | 10997 | 13364 47508 | 7198 4470 167186 37.4 | 16.844 % | c | 11756 | 13364 47508 | 7918 5229 211751 40.5 | 16.844 % | c | 12895 | 13364 47508 | 8710 6368 264424 41.5 | 16.844 % | c | 14604 | 13364 47508 | 9581 8077 327632 40.6 | 16.844 % | c | 17168 | 13364 47508 | 10540 5402 170299 31.5 | 16.844 % | c | 21013 | 13356 47482 | 11594 9246 322961 34.9 | 16.885 % | c | 26779 | 13356 47482 | 12753 8878 354009 39.9 | 16.885 % | c ============================================================================== c [1mFound solution: 903168[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 5256 bits: 13/13 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 27249 | 13355 47491 | 4451 9347 366285 39.2 | 16.885 % | c | 27349 | 13355 47491 | 4896 4774 154490 32.4 | 17.013 % | c | 27499 | 13355 47491 | 5385 4924 158418 32.2 | 17.013 % | c | 27725 | 13355 47491 | 5924 5150 165179 32.1 | 17.013 % | c | 28062 | 13355 47491 | 6516 5487 177942 32.4 | 17.013 % | c | 28568 | 13355 47491 | 7168 5993 214401 35.8 | 17.013 % | c | 29328 | 13355 47491 | 7885 6753 237395 35.2 | 17.013 % | c | 30467 | 13355 47491 | 8673 7892 276790 35.1 | 17.013 % | c | 32175 | 13355 47491 | 9541 4859 147414 30.3 | 17.013 % | c | 34737 | 13355 47491 | 10495 7421 288843 38.9 | 17.013 % | c | 38581 | 13355 47491 | 11544 5669 168162 29.7 | 17.013 % | c | 44347 | 13355 47491 | 12699 11435 459721 40.2 | 17.013 % | c | 52997 | 13355 47491 | 13969 13287 578129 43.5 | 17.013 % | c | 65971 | 13355 47491 | 15366 11480 521835 45.5 | 17.013 % | c | 85433 | 13347 47465 | 16902 14916 611237 41.0 | 17.054 % | c ============================================================================== c [1mFound solution: 882688[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 5276 bits: 13/13 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 87954 | 13347 47486 | 4449 17436 712189 40.8 | 17.054 % | c | 88054 | 13347 47486 | 4893 4459 127533 28.6 | 17.243 % | c | 88204 | 13347 47486 | 5383 4609 131398 28.5 | 17.243 % | c | 88429 | 13347 47486 | 5921 4834 140062 29.0 | 17.243 % | c | 88767 | 13347 47486 | 6513 5172 147960 28.6 | 17.243 % | c | 89274 | 13347 47486 | 7165 5679 164313 28.9 | 17.243 % | c | 90033 | 13347 47486 | 7881 6438 189471 29.4 | 17.243 % | c | 91173 | 13347 47486 | 8669 7578 231147 30.5 | 17.243 % | c | 92881 | 13347 47486 | 9536 9286 299139 32.2 | 17.243 % | c | 95444 | 13347 47486 | 10490 6595 232398 35.2 | 17.243 % | c | 99290 | 13347 47486 | 11539 10441 370636 35.5 | 17.243 % | c | 105056 | 13347 47486 | 12693 10042 474029 47.2 | 17.243 % | c ============================================================================== c [1mFound solution: 858112[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 5300 bits: 13/13 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 113494 | 13344 47495 | 4448 11758 493407 42.0 | 17.243 % | c | 113595 | 13344 47495 | 4892 3041 90912 29.9 | 17.411 % | c | 113746 | 13344 47495 | 5382 3192 95378 29.9 | 17.411 % | c | 113971 | 13344 47495 | 5920 3417 99422 29.1 | 17.411 % | c | 114309 | 13344 47495 | 6512 3755 109697 29.2 | 17.411 % | c | 114818 | 13344 47495 | 7163 4264 126350 29.6 | 17.411 % | c | 115577 | 13344 47495 | 7879 5023 155249 30.9 | 17.411 % | c | 116717 | 13344 47495 | 8667 6163 186944 30.3 | 17.411 % | c | 118428 | 13344 47495 | 9534 7874 256826 32.6 | 17.411 % | c | 120991 | 13344 47495 | 10488 5237 154424 29.5 | 17.411 % | c | 124836 | 13344 47495 | 11536 9082 295207 32.5 | 17.411 % | c | 130602 | 13344 47495 | 12690 8760 316223 36.1 | 17.411 % | c | 139251 | 13344 47495 | 13959 10694 416323 38.9 | 17.411 % | c ============================================================================== c [1mFound solution: 804864[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 5352 bits: 13/13 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 139760 | 13352 47531 | 4450 11203 429990 38.4 | 17.411 % | c | 139860 | 13352 47531 | 4895 2901 69400 23.9 | 17.516 % | c | 140011 | 13352 47531 | 5384 3052 73400 24.0 | 17.516 % | c | 140237 | 13352 47531 | 5922 3278 79590 24.3 | 17.516 % | c | 140574 | 13352 47531 | 6515 3615 87691 24.3 | 17.516 % | c | 141080 | 13352 47531 | 7166 4121 103617 25.1 | 17.516 % | c | 141839 | 13352 47531 | 7883 4880 129239 26.5 | 17.516 % | c | 142981 | 13352 47531 | 8671 6022 159801 26.5 | 17.516 % | c | 144689 | 13352 47531 | 9538 7730 219162 28.4 | 17.516 % | c | 147254 | 13352 47531 | 10492 5167 175302 33.9 | 17.516 % | c | 151098 | 13352 47531 | 11542 9011 310621 34.5 | 17.516 % | c | 156864 | 13352 47531 | 12696 8600 309753 36.0 | 17.516 % | c | 165513 | 13344 47505 | 13966 10520 383759 36.5 | 17.557 % | c | 178487 | 13336 47479 | 15362 8719 325619 37.3 | 17.597 % | c | 197952 | 13336 47479 | 16898 11995 546454 45.6 | 17.597 % | c ============================================================================== c [1mFound solution: 777216[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 5379 bits: 13/13 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 225463 | 13339 47493 | 4446 12756 758258 59.4 | 17.597 % | c | 225563 | 13339 47493 | 4890 3289 125236 38.1 | 17.657 % | c | 225714 | 13339 47493 | 5379 3440 130923 38.1 | 17.657 % | c | 225941 | 13339 47493 | 5917 3667 138975 37.9 | 17.657 % | c | 226278 | 13339 47493 | 6509 4004 148650 37.1 | 17.657 % | c | 226784 | 13339 47493 | 7160 4510 169570 37.6 | 17.657 % | c | 227544 | 13339 47493 | 7876 5270 196710 37.3 | 17.657 % | c | 228685 | 13339 47493 | 8663 6411 241027 37.6 | 17.657 % | c | 230393 | 13339 47493 | 9530 8119 305665 37.6 | 17.657 % | c | 232955 | 13339 47493 | 10483 5482 186331 34.0 | 17.657 % | c | 236799 | 13339 47493 | 11531 9326 341455 36.6 | 17.657 % | c | 242566 | 13339 47493 | 12684 9040 301421 33.3 | 17.657 % | c | 251215 | 13339 47493 | 13953 10994 518003 47.1 | 17.657 % | c | 264191 | 13339 47493 | 15348 9237 371491 40.2 | 17.657 % | c | 283653 | 13339 47493 | 16883 12634 507143 40.1 | 17.657 % | c | 312846 | 13339 47493 | 18572 15231 683793 44.9 | 17.657 % | c ============================================================================== c [1mFound solution: 686080[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 5468 bits: 13/13 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 319011 | 13349 47537 | 4449 11744 568430 48.4 | 17.657 % | c | 319112 | 13349 47537 | 4893 3037 106777 35.2 | 17.787 % | c | 319262 | 13349 47537 | 5383 3187 108078 33.9 | 17.787 % | c | 319487 | 13349 47537 | 5921 3412 111411 32.7 | 17.787 % | c | 319824 | 13349 47537 | 6513 3749 117788 31.4 | 17.787 % | c | 320333 | 13349 47537 | 7165 4258 126307 29.7 | 17.787 % | c | 321092 | 13349 47537 | 7881 5017 139976 27.9 | 17.787 % | c | 322231 | 13349 47537 | 8669 6156 175471 28.5 | 17.787 % | c | 323940 | 13349 47537 | 9536 7865 249752 31.8 | 17.787 % | c | 326502 | 13349 47537 | 10490 5264 176857 33.6 | 17.787 % | c | 330348 | 13349 47537 | 11539 9110 329613 36.2 | 17.787 % | c | 336115 | 13349 47537 | 12693 8801 313362 35.6 | 17.787 % | c | 344765 | 13349 47537 | 13962 10757 436205 40.6 | 17.787 % | c | 357739 | 13349 47537 | 15359 8973 349043 38.9 | 17.787 % | c | 377200 | 13349 47537 | 16895 12379 488048 39.4 | 17.787 % | c | 406392 | 13349 47537 | 18584 15136 610751 40.4 | 17.787 % | c | 450182 | 13349 47537 | 20443 11000 456954 41.5 | 17.787 % | c | 515867 | 13349 47537 | 22487 12981 594905 45.8 | 17.787 % | c | 614393 | 13349 47537 | 24736 18384 763506 41.5 | 17.787 % | c | 762182 | 13349 47537 | 27209 12886 488584 37.9 | 17.787 % | #### 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.75 0.86 0.87 2/54 15287 Raw data (stat): 15287 (runsolver) R 15286 32461 32460 0 -1 64 1 0 0 0 0 0 0 0 19 0 1 0 491353053 1052672 97 4294967295 134512640 135381576 3221224432 3221219804 135024803 0 0 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 97 215 215 0 42 0 vsize: 1028 [startup+10.0008 s] Raw data (loadavg): 0.79 0.86 0.87 2/54 15287 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 1038 0 0 0 996 2 0 0 25 0 1 0 491353053 5865472 1016 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1432 1016 603 41 0 1391 0 vsize: 5728 [startup+20.0145 s] Raw data (loadavg): 0.82 0.86 0.87 2/54 15287 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 1132 0 0 0 1996 3 0 0 25 0 1 0 491353053 6303744 1110 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1539 1110 603 41 0 1498 0 vsize: 6156 [startup+30.0152 s] Raw data (loadavg): 0.85 0.87 0.87 2/54 15287 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 1205 0 0 0 2996 3 0 0 25 0 1 0 491353053 6574080 1183 4294967295 134512640 134672761 3221224528 3221223664 134565092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1605 1183 603 41 0 1564 0 vsize: 6420 [startup+40.0161 s] Raw data (loadavg): 0.87 0.87 0.88 2/54 15287 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 1343 0 0 0 3995 4 0 0 25 0 1 0 491353053 7110656 1321 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1736 1321 603 41 0 1695 0 vsize: 6944 [startup+50.0282 s] Raw data (loadavg): 0.89 0.87 0.88 2/54 15287 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 1467 0 0 0 4996 4 0 0 25 0 1 0 491353053 7647232 1445 4294967295 134512640 134672761 3221224528 3221223712 134559599 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1867 1445 603 41 0 1826 0 vsize: 7468 [startup+60.0357 s] Raw data (loadavg): 0.91 0.88 0.88 2/54 15287 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 1467 0 0 0 5996 5 0 0 25 0 1 0 491353053 7647232 1445 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1867 1445 603 41 0 1826 0 vsize: 7468 [startup+70.0497 s] Raw data (loadavg): 0.92 0.88 0.88 2/54 15287 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 1572 0 0 0 6997 6 0 0 25 0 1 0 491353053 8048640 1550 4294967295 134512640 134672761 3221224528 3221223632 134559841 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1965 1550 603 41 0 1924 0 vsize: 7860 [startup+80.0548 s] Raw data (loadavg): 0.93 0.89 0.88 2/54 15287 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 1574 0 0 0 7997 6 0 0 25 0 1 0 491353053 8048640 1552 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1965 1552 603 41 0 1924 0 vsize: 7860 [startup+90.0551 s] Raw data (loadavg): 0.94 0.89 0.88 2/54 15287 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 1617 0 0 0 8996 7 0 0 25 0 1 0 491353053 8286208 1595 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2023 1595 603 41 0 1982 0 vsize: 8092 [startup+100.055 s] Raw data (loadavg): 0.95 0.89 0.88 2/54 15287 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 1617 0 0 0 9996 7 0 0 25 0 1 0 491353053 8286208 1595 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2023 1595 603 41 0 1982 0 vsize: 8092 [startup+110.065 s] Raw data (loadavg): 0.96 0.89 0.88 2/54 15287 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 1618 0 0 0 10997 7 0 0 25 0 1 0 491353053 8286208 1596 4294967295 134512640 134672761 3221224528 3221223664 134560667 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2023 1596 603 41 0 1982 0 vsize: 8092 [startup+120.065 s] Raw data (loadavg): 0.96 0.90 0.88 2/54 15287 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 1618 0 0 0 11997 8 0 0 25 0 1 0 491353053 8286208 1596 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2023 1596 603 41 0 1982 0 vsize: 8092 [startup+130.181 s] Raw data (loadavg): 0.97 0.90 0.88 2/54 15287 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 1618 0 0 0 13008 8 0 0 25 0 1 0 491353053 8286208 1596 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2023 1596 603 41 0 1982 0 vsize: 8092 [startup+140.298 s] Raw data (loadavg): 0.97 0.90 0.89 2/54 15287 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 1618 0 0 0 14019 8 0 0 25 0 1 0 491353053 8286208 1596 4294967295 134512640 134672761 3221224528 3221223696 134560858 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2023 1596 603 41 0 1982 0 vsize: 8092 [startup+150.324 s] Raw data (loadavg): 1.06 0.92 0.89 2/56 15295 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 1618 0 0 0 15019 11 0 0 25 0 1 0 491353053 8286208 1596 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2023 1596 603 41 0 1982 0 vsize: 8092 [startup+160.341 s] Raw data (loadavg): 1.20 0.96 0.90 3/58 15332 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 1618 0 0 0 16020 11 0 0 25 0 1 0 491353053 8286208 1596 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2023 1596 603 41 0 1982 0 vsize: 8092 [startup+170.361 s] Raw data (loadavg): 1.32 0.99 0.91 2/54 15340 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 1734 0 0 0 17023 11 0 0 25 0 1 0 491353053 8814592 1712 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2152 1712 603 41 0 2111 0 vsize: 8608 [startup+180.361 s] Raw data (loadavg): 1.27 0.99 0.91 2/54 15340 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 1846 0 0 0 18022 11 0 0 25 0 1 0 491353053 9216000 1824 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2250 1824 603 41 0 2209 0 vsize: 9000 [startup+190.361 s] Raw data (loadavg): 1.23 0.99 0.91 2/54 15340 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 1960 0 0 0 19022 12 0 0 25 0 1 0 491353053 9744384 1938 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2379 1938 603 41 0 2338 0 vsize: 9516 [startup+200.369 s] Raw data (loadavg): 1.19 0.99 0.91 2/54 15340 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2029 0 0 0 20022 12 0 0 25 0 1 0 491353053 10010624 2007 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2444 2007 603 41 0 2403 0 vsize: 9776 [startup+210.369 s] Raw data (loadavg): 1.16 0.99 0.91 2/54 15340 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2144 0 0 0 21022 12 0 0 25 0 1 0 491353053 10534912 2122 4294967295 134512640 134672761 3221224528 3221223664 134565045 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2572 2122 603 41 0 2531 0 vsize: 10288 [startup+220.391 s] Raw data (loadavg): 1.14 0.99 0.91 2/54 15340 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2176 0 0 0 22024 12 0 0 25 0 1 0 491353053 10665984 2154 4294967295 134512640 134672761 3221224528 3221223728 134557897 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2604 2154 603 41 0 2563 0 vsize: 10416 [startup+230.39 s] Raw data (loadavg): 1.11 0.99 0.91 2/54 15342 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2176 0 0 0 23024 12 0 0 25 0 1 0 491353053 10657792 2154 4294967295 134512640 134672761 3221224528 3221223712 134559182 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2602 2154 603 41 0 2561 0 vsize: 10408 [startup+240.391 s] Raw data (loadavg): 1.10 0.99 0.91 2/54 15342 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2176 0 0 0 24025 12 0 0 25 0 1 0 491353053 10657792 2154 4294967295 134512640 134672761 3221224528 3221223696 134561154 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2602 2154 603 41 0 2561 0 vsize: 10408 [startup+250.391 s] Raw data (loadavg): 1.08 0.99 0.91 2/54 15342 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2176 0 0 0 25025 12 0 0 25 0 1 0 491353053 10657792 2154 4294967295 134512640 134672761 3221224528 3221223696 134560852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2602 2154 603 41 0 2561 0 vsize: 10408 [startup+260.392 s] Raw data (loadavg): 1.07 0.99 0.91 2/54 15342 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2176 0 0 0 26025 12 0 0 25 0 1 0 491353053 10657792 2154 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2602 2154 603 41 0 2561 0 vsize: 10408 [startup+270.391 s] Raw data (loadavg): 1.06 0.99 0.91 2/54 15342 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2176 0 0 0 27025 12 0 0 25 0 1 0 491353053 10657792 2154 4294967295 134512640 134672761 3221224528 3221223696 134561215 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2602 2154 603 41 0 2561 0 vsize: 10408 [startup+280.397 s] Raw data (loadavg): 1.05 0.99 0.91 2/54 15342 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2176 0 0 0 28026 12 0 0 25 0 1 0 491353053 10657792 2154 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2602 2154 603 41 0 2561 0 vsize: 10408 [startup+290.402 s] Raw data (loadavg): 1.04 0.99 0.91 2/54 15342 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2176 0 0 0 29026 12 0 0 25 0 1 0 491353053 10657792 2154 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2602 2154 603 41 0 2561 0 vsize: 10408 [startup+300.401 s] Raw data (loadavg): 1.03 0.99 0.91 2/54 15342 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2176 0 0 0 30027 12 0 0 25 0 1 0 491353053 10657792 2154 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2602 2154 603 41 0 2561 0 vsize: 10408 [startup+310.402 s] Raw data (loadavg): 1.03 0.99 0.91 2/54 15342 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2176 0 0 0 31027 12 0 0 25 0 1 0 491353053 10657792 2154 4294967295 134512640 134672761 3221224528 3221223696 134561205 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2602 2154 603 41 0 2561 0 vsize: 10408 [startup+320.402 s] Raw data (loadavg): 1.02 0.99 0.91 2/54 15342 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2186 0 0 0 32027 12 0 0 25 0 1 0 491353053 10657792 2164 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2602 2164 603 41 0 2561 0 vsize: 10408 [startup+330.402 s] Raw data (loadavg): 1.02 0.99 0.91 2/54 15342 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2190 0 0 0 33026 12 0 0 25 0 1 0 491353053 10657792 2168 4294967295 134512640 134672761 3221224528 3221223712 134559304 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2602 2168 603 41 0 2561 0 vsize: 10408 [startup+340.402 s] Raw data (loadavg): 1.02 0.99 0.91 2/54 15342 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2190 0 0 0 34026 12 0 0 25 0 1 0 491353053 10657792 2168 4294967295 134512640 134672761 3221224528 3221223696 134560917 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2602 2168 603 41 0 2561 0 vsize: 10408 [startup+350.402 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 15342 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2190 0 0 0 35026 12 0 0 25 0 1 0 491353053 10657792 2168 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2602 2168 603 41 0 2561 0 vsize: 10408 [startup+360.402 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 15342 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2190 0 0 0 36027 13 0 0 25 0 1 0 491353053 10657792 2168 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2602 2168 603 41 0 2561 0 vsize: 10408 [startup+370.402 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 15342 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2190 0 0 0 37027 13 0 0 25 0 1 0 491353053 10657792 2168 4294967295 134512640 134672761 3221224528 3221223632 134560267 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2602 2168 603 41 0 2561 0 vsize: 10408 [startup+380.402 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 15342 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2190 0 0 0 38027 13 0 0 25 0 1 0 491353053 10657792 2168 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2602 2168 603 41 0 2561 0 vsize: 10408 [startup+390.402 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15342 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2190 0 0 0 39027 13 0 0 25 0 1 0 491353053 10657792 2168 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2602 2168 603 41 0 2561 0 vsize: 10408 [startup+400.402 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15342 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2190 0 0 0 40027 13 0 0 25 0 1 0 491353053 10657792 2168 4294967295 134512640 134672761 3221224528 3221223632 134560243 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2602 2168 603 41 0 2561 0 vsize: 10408 [startup+410.405 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15342 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2190 0 0 0 41028 13 0 0 25 0 1 0 491353053 10657792 2168 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2602 2168 603 41 0 2561 0 vsize: 10408 [startup+420.405 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15342 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2200 0 0 0 42028 13 0 0 25 0 1 0 491353053 10657792 2178 4294967295 134512640 134672761 3221224528 3221223696 134560864 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2602 2178 603 41 0 2561 0 vsize: 10408 [startup+430.405 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15342 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2213 0 0 0 43028 13 0 0 25 0 1 0 491353053 10805248 2191 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2638 2191 603 41 0 2597 0 vsize: 10552 [startup+440.406 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15342 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2305 0 0 0 44028 13 0 0 25 0 1 0 491353053 11075584 2283 4294967295 134512640 134672761 3221224528 3221223632 134560492 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2704 2283 603 41 0 2663 0 vsize: 10816 [startup+450.405 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15342 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2320 0 0 0 45027 13 0 0 25 0 1 0 491353053 11218944 2298 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2739 2298 603 41 0 2698 0 vsize: 10956 [startup+460.406 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15342 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2320 0 0 0 46028 13 0 0 25 0 1 0 491353053 11218944 2298 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2739 2298 603 41 0 2698 0 vsize: 10956 [startup+470.406 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15342 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2323 0 0 0 47028 13 0 0 25 0 1 0 491353053 11218944 2301 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2739 2301 603 41 0 2698 0 vsize: 10956 [startup+480.405 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2414 0 0 0 48028 14 0 0 25 0 1 0 491353053 11616256 2392 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2836 2392 603 41 0 2795 0 vsize: 11344 [startup+490.406 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2511 0 0 0 49028 14 0 0 25 0 1 0 491353053 12017664 2489 4294967295 134512640 134672761 3221224528 3221223712 134559540 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2934 2489 603 41 0 2893 0 vsize: 11736 [startup+500.406 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2518 0 0 0 50028 14 0 0 25 0 1 0 491353053 12017664 2496 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2934 2496 603 41 0 2893 0 vsize: 11736 [startup+510.407 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2588 0 0 0 51028 14 0 0 25 0 1 0 491353053 12279808 2566 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2998 2566 603 41 0 2957 0 vsize: 11992 [startup+520.407 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2600 0 0 0 52028 14 0 0 25 0 1 0 491353053 12414976 2578 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3031 2578 603 41 0 2990 0 vsize: 12124 [startup+530.407 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2608 0 0 0 53028 14 0 0 25 0 1 0 491353053 12414976 2586 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3031 2586 603 41 0 2990 0 vsize: 12124 [startup+540.407 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2614 0 0 0 54028 14 0 0 25 0 1 0 491353053 12414976 2592 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3031 2592 603 41 0 2990 0 vsize: 12124 [startup+550.408 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2634 0 0 0 55028 14 0 0 25 0 1 0 491353053 12546048 2612 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3063 2612 603 41 0 3022 0 vsize: 12252 [startup+560.408 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2638 0 0 0 56029 14 0 0 25 0 1 0 491353053 12546048 2616 4294967295 134512640 134672761 3221224528 3221223600 134553549 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3063 2616 603 41 0 3022 0 vsize: 12252 [startup+570.409 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2645 0 0 0 57029 14 0 0 25 0 1 0 491353053 12546048 2623 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3063 2623 603 41 0 3022 0 vsize: 12252 [startup+580.409 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2663 0 0 0 58029 14 0 0 25 0 1 0 491353053 12693504 2641 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3099 2641 603 41 0 3058 0 vsize: 12396 [startup+590.409 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2667 0 0 0 59029 14 0 0 25 0 1 0 491353053 12693504 2645 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3099 2645 603 41 0 3058 0 vsize: 12396 [startup+600.41 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2667 0 0 0 60029 14 0 0 25 0 1 0 491353053 12693504 2645 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3099 2645 603 41 0 3058 0 vsize: 12396 [startup+610.411 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2695 0 0 0 61030 14 0 0 25 0 1 0 491353053 12828672 2673 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3132 2673 603 41 0 3091 0 vsize: 12528 [startup+620.412 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2724 0 0 0 62030 15 0 0 25 0 1 0 491353053 12959744 2702 4294967295 134512640 134672761 3221224528 3221223696 134561207 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3164 2702 603 41 0 3123 0 vsize: 12656 [startup+630.411 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2759 0 0 0 63030 15 0 0 25 0 1 0 491353053 13094912 2737 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3197 2737 603 41 0 3156 0 vsize: 12788 [startup+640.412 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2767 0 0 0 64030 15 0 0 25 0 1 0 491353053 13094912 2745 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3197 2745 603 41 0 3156 0 vsize: 12788 [startup+650.412 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2768 0 0 0 65030 15 0 0 25 0 1 0 491353053 13094912 2746 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3197 2746 603 41 0 3156 0 vsize: 12788 [startup+660.413 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2791 0 0 0 66030 15 0 0 25 0 1 0 491353053 13234176 2769 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3231 2769 603 41 0 3190 0 vsize: 12924 [startup+670.414 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2796 0 0 0 67030 15 0 0 25 0 1 0 491353053 13234176 2774 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3231 2774 603 41 0 3190 0 vsize: 12924 [startup+680.413 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2797 0 0 0 68030 15 0 0 25 0 1 0 491353053 13234176 2775 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3231 2775 603 41 0 3190 0 vsize: 12924 [startup+690.414 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2803 0 0 0 69031 15 0 0 25 0 1 0 491353053 13234176 2781 4294967295 134512640 134672761 3221224528 3221223632 134554642 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3231 2781 603 41 0 3190 0 vsize: 12924 [startup+700.414 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2804 0 0 0 70031 15 0 0 25 0 1 0 491353053 13234176 2782 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3231 2782 603 41 0 3190 0 vsize: 12924 [startup+710.416 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2806 0 0 0 71031 15 0 0 25 0 1 0 491353053 13234176 2784 4294967295 134512640 134672761 3221224528 3221223668 134560556 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3231 2784 603 41 0 3190 0 vsize: 12924 [startup+720.415 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2806 0 0 0 72031 15 0 0 25 0 1 0 491353053 13234176 2784 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3231 2784 603 41 0 3190 0 vsize: 12924 [startup+730.416 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2806 0 0 0 73031 15 0 0 25 0 1 0 491353053 13234176 2784 4294967295 134512640 134672761 3221224528 3221223696 134560906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3231 2784 603 41 0 3190 0 vsize: 12924 [startup+740.416 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2811 0 0 0 74031 15 0 0 25 0 1 0 491353053 13398016 2789 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3271 2789 603 41 0 3230 0 vsize: 13084 [startup+750.416 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2812 0 0 0 75031 15 0 0 25 0 1 0 491353053 13398016 2790 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3271 2790 603 41 0 3230 0 vsize: 13084 [startup+760.417 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2907 0 0 0 76031 15 0 0 25 0 1 0 491353053 13668352 2885 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3337 2885 603 41 0 3296 0 vsize: 13348 [startup+770.417 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2907 0 0 0 77032 15 0 0 25 0 1 0 491353053 13668352 2885 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3337 2885 603 41 0 3296 0 vsize: 13348 [startup+780.416 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2929 0 0 0 78032 15 0 0 25 0 1 0 491353053 13807616 2907 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3371 2907 603 41 0 3330 0 vsize: 13484 [startup+790.417 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2933 0 0 0 79032 15 0 0 25 0 1 0 491353053 13807616 2911 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3371 2911 603 41 0 3330 0 vsize: 13484 [startup+800.417 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2943 0 0 0 80032 15 0 0 25 0 1 0 491353053 13963264 2921 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3409 2921 603 41 0 3368 0 vsize: 13636 [startup+810.417 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2948 0 0 0 81032 15 0 0 25 0 1 0 491353053 13963264 2926 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3409 2926 603 41 0 3368 0 vsize: 13636 [startup+820.418 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2948 0 0 0 82032 15 0 0 25 0 1 0 491353053 13963264 2926 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3409 2926 603 41 0 3368 0 vsize: 13636 [startup+830.417 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2948 0 0 0 83033 15 0 0 25 0 1 0 491353053 13963264 2926 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3409 2926 603 41 0 3368 0 vsize: 13636 [startup+840.418 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 2948 0 0 0 84033 15 0 0 25 0 1 0 491353053 13963264 2926 4294967295 134512640 134672761 3221224528 3221223696 134560852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3409 2926 603 41 0 3368 0 vsize: 13636 [startup+850.418 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3004 0 0 0 85033 15 0 0 25 0 1 0 491353053 14094336 2982 4294967295 134512640 134672761 3221224528 3221223696 134561190 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3441 2982 603 41 0 3400 0 vsize: 13764 [startup+860.419 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3018 0 0 0 86033 16 0 0 25 0 1 0 491353053 14229504 2996 4294967295 134512640 134672761 3221224528 3221223712 134558687 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3474 2996 603 41 0 3433 0 vsize: 13896 [startup+870.418 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3034 0 0 0 87033 16 0 0 25 0 1 0 491353053 14372864 3012 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3509 3012 603 41 0 3468 0 vsize: 14036 [startup+880.418 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3035 0 0 0 88033 16 0 0 25 0 1 0 491353053 14372864 3013 4294967295 134512640 134672761 3221224528 3221223696 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3509 3013 603 41 0 3468 0 vsize: 14036 [startup+890.419 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3041 0 0 0 89033 16 0 0 25 0 1 0 491353053 14372864 3019 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3509 3019 603 41 0 3468 0 vsize: 14036 [startup+900.419 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3041 0 0 0 90034 16 0 0 25 0 1 0 491353053 14372864 3019 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3509 3019 603 41 0 3468 0 vsize: 14036 [startup+910.42 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3041 0 0 0 91033 16 0 0 25 0 1 0 491353053 14372864 3019 4294967295 134512640 134672761 3221224528 3221223696 134560942 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3509 3019 603 41 0 3468 0 vsize: 14036 [startup+920.422 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3043 0 0 0 92032 16 0 0 25 0 1 0 491353053 14372864 3021 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3509 3021 603 41 0 3468 0 vsize: 14036 [startup+930.421 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3043 0 0 0 93031 17 0 0 25 0 1 0 491353053 14372864 3021 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3509 3021 603 41 0 3468 0 vsize: 14036 [startup+940.421 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3043 0 0 0 94031 17 0 0 25 0 1 0 491353053 14372864 3021 4294967295 134512640 134672761 3221224528 3221223696 134561205 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3509 3021 603 41 0 3468 0 vsize: 14036 [startup+950.422 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3046 0 0 0 95030 17 0 0 25 0 1 0 491353053 14372864 3024 4294967295 134512640 134672761 3221224528 3221223696 134561205 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3509 3024 603 41 0 3468 0 vsize: 14036 [startup+960.422 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3059 0 0 0 96030 18 0 0 25 0 1 0 491353053 14372864 3037 4294967295 134512640 134672761 3221224528 3221223696 134561198 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3509 3037 603 41 0 3468 0 vsize: 14036 [startup+970.423 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3063 0 0 0 97030 18 0 0 25 0 1 0 491353053 14372864 3041 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3509 3041 603 41 0 3468 0 vsize: 14036 [startup+980.423 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3067 0 0 0 98030 18 0 0 25 0 1 0 491353053 14372864 3045 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3509 3045 603 41 0 3468 0 vsize: 14036 [startup+990.424 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3078 0 0 0 99030 18 0 0 25 0 1 0 491353053 14520320 3056 4294967295 134512640 134672761 3221224528 3221223696 134560956 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3545 3056 603 41 0 3504 0 vsize: 14180 [startup+1000.42 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3085 0 0 0 100030 18 0 0 25 0 1 0 491353053 14520320 3063 4294967295 134512640 134672761 3221224528 3221223696 134560785 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3545 3063 603 41 0 3504 0 vsize: 14180 [startup+1010.42 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3093 0 0 0 101030 18 0 0 25 0 1 0 491353053 14520320 3071 4294967295 134512640 134672761 3221224528 3221223696 134560979 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3545 3071 603 41 0 3504 0 vsize: 14180 [startup+1020.43 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3094 0 0 0 102030 19 0 0 25 0 1 0 491353053 14520320 3072 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3545 3072 603 41 0 3504 0 vsize: 14180 [startup+1030.43 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3106 0 0 0 103030 19 0 0 25 0 1 0 491353053 14663680 3084 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3580 3084 603 41 0 3539 0 vsize: 14320 [startup+1040.43 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3107 0 0 0 104029 20 0 0 25 0 1 0 491353053 14663680 3085 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3580 3085 603 41 0 3539 0 vsize: 14320 [startup+1050.43 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3107 0 0 0 105029 20 0 0 25 0 1 0 491353053 14663680 3085 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3580 3085 603 41 0 3539 0 vsize: 14320 [startup+1060.43 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3107 0 0 0 106029 20 0 0 25 0 1 0 491353053 14663680 3085 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3580 3085 603 41 0 3539 0 vsize: 14320 [startup+1070.43 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3107 0 0 0 107029 20 0 0 25 0 1 0 491353053 14663680 3085 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3580 3085 603 41 0 3539 0 vsize: 14320 [startup+1080.43 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3118 0 0 0 108029 20 0 0 25 0 1 0 491353053 14663680 3096 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3580 3096 603 41 0 3539 0 vsize: 14320 [startup+1090.43 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3156 0 0 0 109029 20 0 0 25 0 1 0 491353053 14794752 3134 4294967295 134512640 134672761 3221224528 3221223696 134561154 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3612 3134 603 41 0 3571 0 vsize: 14448 [startup+1100.43 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3172 0 0 0 110029 20 0 0 25 0 1 0 491353053 14942208 3150 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3648 3150 603 41 0 3607 0 vsize: 14592 [startup+1110.43 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3186 0 0 0 111029 21 0 0 25 0 1 0 491353053 14942208 3164 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3648 3164 603 41 0 3607 0 vsize: 14592 [startup+1120.43 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3193 0 0 0 112029 21 0 0 25 0 1 0 491353053 15089664 3171 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3684 3171 603 41 0 3643 0 vsize: 14736 [startup+1130.43 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3203 0 0 0 113029 21 0 0 25 0 1 0 491353053 15089664 3181 4294967295 134512640 134672761 3221224528 3221223684 134561032 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3684 3181 603 41 0 3643 0 vsize: 14736 [startup+1140.43 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3210 0 0 0 114029 21 0 0 25 0 1 0 491353053 15089664 3188 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3684 3188 603 41 0 3643 0 vsize: 14736 [startup+1150.43 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3215 0 0 0 115030 21 0 0 25 0 1 0 491353053 15089664 3193 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3684 3193 603 41 0 3643 0 vsize: 14736 [startup+1160.43 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3216 0 0 0 116030 21 0 0 25 0 1 0 491353053 15089664 3194 4294967295 134512640 134672761 3221224528 3221223696 134561118 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3684 3194 603 41 0 3643 0 vsize: 14736 [startup+1170.43 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3226 0 0 0 117030 21 0 0 25 0 1 0 491353053 15253504 3204 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3724 3204 603 41 0 3683 0 vsize: 14896 [startup+1180.43 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3227 0 0 0 118030 21 0 0 25 0 1 0 491353053 15253504 3205 4294967295 134512640 134672761 3221224528 3221223696 134561148 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3724 3205 603 41 0 3683 0 vsize: 14896 [startup+1190.43 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3236 0 0 0 119030 21 0 0 25 0 1 0 491353053 15253504 3214 4294967295 134512640 134672761 3221224528 3221223696 134561205 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3724 3214 603 41 0 3683 0 vsize: 14896 [startup+1200.43 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 15344 Raw data (stat): 15287 (minisat+) R 15286 32461 32460 0 -1 0 3237 0 0 0 120030 21 0 0 25 0 1 0 491353053 15253504 3215 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3724 3215 603 41 0 3683 0 vsize: 14896 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.44 s] Raw data (loadavg): 1.00 0.99 0.91 1/54 15344 Raw data (stat): 15287 (minisat+) Z 15286 32461 32460 0 -1 12 3240 0 0 0 120030 22 0 0 25 0 1 0 491353053 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 10 Real time (s): 1200.44 CPU time (s): 1200.53 CPU user time (s): 1200.31 CPU system time (s): 0.221966 CPU usage (%): 100.008 Max. virtual memory (Kb): 14896 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####